diff --git a/Makefile b/Makefile index 8d742883e..f1f4f1396 100644 --- a/Makefile +++ b/Makefile @@ -108,6 +108,7 @@ SUBDIR += src SUBDIR += tests/capture SUBDIR += tests/complement SUBDIR += tests/gen +SUBDIR += tests/idmap SUBDIR += tests/intersect #SUBDIR += tests/ir # XXX: fragile due to state numbering SUBDIR += tests/eclosure diff --git a/fuzz/run_fuzzer b/fuzz/run_fuzzer index be8ba1d95..429ffa961 100755 --- a/fuzz/run_fuzzer +++ b/fuzz/run_fuzzer @@ -4,6 +4,8 @@ BUILD=../build FUZZER=${BUILD}/fuzz/fuzzer SEEDS=${BUILD}/fuzz/fuzzer_seeds +ARG=$1 + SECONDS=${SECONDS:-60} WORKERS=${WORKERS:-4} SEEDS=${SEEDS:-seeds} @@ -25,5 +27,9 @@ if [ ! -d "${SEEDS}" ]; then mkdir -p "${SEEDS}" fi -echo "\n==== ${FUZZER}" -${FUZZER} -jobs=${WORKERS} -workers=${WORKERS} -max_total_time=${SECONDS} ${SEEDS} +if [ -z "${ARG}" ]; then + echo "\n==== ${FUZZER}" + exec ${FUZZER} -jobs=${WORKERS} -workers=${WORKERS} -max_total_time=${SECONDS} ${SEEDS} +else + exec ${FUZZER} ${ARG} +fi \ No newline at end of file diff --git a/include/adt/idmap.h b/include/adt/idmap.h new file mode 100644 index 000000000..064fd15d1 --- /dev/null +++ b/include/adt/idmap.h @@ -0,0 +1,58 @@ +#ifndef IDMAP_H +#define IDMAP_H + +/* Mapping between one fsm_state_t and a set of + * unsigned IDs. The implementation assumes that both + * IDs are sequentially assigned and don't need a sparse + * mapping -- it will handle 10 -> [1, 3, 47] well, but + * not 1000000 -> [14, 524288, 1073741823]. */ + +#include + +#include "fsm/fsm.h" +#include "fsm/alloc.h" + +struct idmap; /* Opaque handle. */ + +struct idmap * +idmap_new(const struct fsm_alloc *alloc); + +void +idmap_free(struct idmap *m); + +/* Associate a value with a state (if not already present.) + * Returns 1 on success, or 0 on allocation failure. */ +int +idmap_set(struct idmap *m, fsm_state_t state_id, unsigned value); + +/* How many values are associated with an ID? */ +size_t +idmap_get_value_count(const struct idmap *m, fsm_state_t state_id); + +/* Get the values associated with an ID. + * + * Returns 1 on success and writes them into the buffer, in ascending + * order, with the count in *written (if non-NULL). + * + * Returns 0 on error (insufficient buffer space). */ +int +idmap_get(const struct idmap *m, fsm_state_t state_id, + size_t buf_size, unsigned *buf, size_t *written); + +/* Iterator callback. */ +typedef void +idmap_iter_fun(fsm_state_t state_id, unsigned value, void *opaque); + +/* Iterate over the ID map. State IDs may be yielded out of order, + * values will be in ascending order. */ +void +idmap_iter(const struct idmap *m, + idmap_iter_fun *cb, void *opaque); + +/* Iterate over the values associated with a single state + * (in ascending order). */ +void +idmap_iter_for_state(const struct idmap *m, fsm_state_t state_id, + idmap_iter_fun *cb, void *opaque); + +#endif diff --git a/src/adt/Makefile b/src/adt/Makefile index 05199f2dc..64ad7429f 100644 --- a/src/adt/Makefile +++ b/src/adt/Makefile @@ -2,6 +2,7 @@ SRC += src/adt/alloc.c SRC += src/adt/bitmap.c +SRC += src/adt/idmap.c SRC += src/adt/internedstateset.c SRC += src/adt/priq.c SRC += src/adt/path.c diff --git a/src/adt/idmap.c b/src/adt/idmap.c new file mode 100644 index 000000000..ca169b71e --- /dev/null +++ b/src/adt/idmap.c @@ -0,0 +1,392 @@ +/* + * Copyright 2021 Scott Vokes + * + * See LICENCE for the full copyright terms. + */ + +#include "adt/idmap.h" + +#include "adt/alloc.h" +#include "adt/hash.h" +#include "adt/u64bitset.h" + +#include +#include +#include + +#define NO_STATE ((fsm_state_t)-1) + +#define DEF_BUCKET_COUNT 4 + +struct idmap { + const struct fsm_alloc *alloc; + unsigned bucket_count; + unsigned buckets_used; + + /* All buckets' values are assumed to be large + * enough to store this value, and they will all + * grow as necessary. */ + unsigned max_value; + + /* Basic linear-probing, add-only hash table. */ + struct idmap_bucket { + fsm_state_t state; /* Key. NO_STATE when empty. */ + + /* values[] is always either NULL or has at least + * max_value + 1 bits; all grow on demand. */ + uint64_t *values; + } *buckets; +}; + +static unsigned +value_words(unsigned max_value) { + if (max_value == 0) { + /* Still allocate one word, for storing 0. */ + return 1; + } else { + return u64bitset_words(max_value); + } +} + +struct idmap * +idmap_new(const struct fsm_alloc *alloc) +{ + struct idmap *res = NULL; + struct idmap_bucket *buckets = NULL; + + res = f_malloc(alloc, sizeof(*res)); + if (res == NULL) { + goto cleanup; + } + + buckets = f_calloc(alloc, + DEF_BUCKET_COUNT, sizeof(buckets[0])); + if (buckets == NULL) { + goto cleanup; + } + + for (size_t i = 0; i < DEF_BUCKET_COUNT; i++) { + buckets[i].state = NO_STATE; + } + + res->alloc = alloc; + res->buckets_used = 0; + res->bucket_count = DEF_BUCKET_COUNT; + res->max_value = 0; + res->buckets = buckets; + + return res; + +cleanup: + f_free(alloc, res); + f_free(alloc, buckets); + return NULL; +} + +void +idmap_free(struct idmap *m) +{ + if (m == NULL) { + return; + } + + for (size_t i = 0; i < m->bucket_count; i++) { + if (m->buckets[i].state == NO_STATE) { + continue; + } + f_free(m->alloc, m->buckets[i].values); + } + + f_free(m->alloc, m->buckets); + f_free(m->alloc, m); +} + +static int +grow_bucket_values(struct idmap *m, unsigned old_words, unsigned new_words) +{ + assert(new_words > old_words); + + for (size_t b_i = 0; b_i < m->bucket_count; b_i++) { + struct idmap_bucket *b = &m->buckets[b_i]; + if (b->state == NO_STATE) { + assert(b->values == NULL); + continue; + } + + uint64_t *nv = f_calloc(m->alloc, + new_words, sizeof(nv[0])); + if (nv == NULL) { + return 0; + } + + for (size_t w_i = 0; w_i < old_words; w_i++) { + nv[w_i] = b->values[w_i]; + } + f_free(m->alloc, b->values); + b->values = nv; + } + return 1; +} + +static int +grow_buckets(struct idmap *m) +{ + const size_t ocount = m->bucket_count; + const size_t ncount = 2*ocount; + assert(ncount > m->bucket_count); + + struct idmap_bucket *nbuckets = f_calloc(m->alloc, + ncount, sizeof(nbuckets[0])); + if (nbuckets == NULL) { + return 0; + } + for (size_t nb_i = 0; nb_i < ncount; nb_i++) { + nbuckets[nb_i].state = NO_STATE; + } + + const size_t nmask = ncount - 1; + + for (size_t ob_i = 0; ob_i < ocount; ob_i++) { + const struct idmap_bucket *ob = &m->buckets[ob_i]; + if (ob->state == NO_STATE) { + continue; + } + + const uint64_t h = hash_id(ob->state); + for (size_t nb_i = 0; nb_i < ncount; nb_i++) { + struct idmap_bucket *nb = &nbuckets[(h + nb_i) & nmask]; + if (nb->state == NO_STATE) { + nb->state = ob->state; + nb->values = ob->values; + break; + } else { + assert(nb->state != ob->state); + /* collision */ + continue; + } + } + } + + f_free(m->alloc, m->buckets); + + m->buckets = nbuckets; + m->bucket_count = ncount; + + return 1; +} + +int +idmap_set(struct idmap *m, fsm_state_t state_id, + unsigned value) +{ + assert(state_id != NO_STATE); + + const uint64_t h = hash_id(state_id); + if (value > m->max_value) { + const unsigned ovw = value_words(m->max_value); + const unsigned nvw = value_words(value); + /* If this value won't fit in the existing value + * arrays, then grow them all. We do not track the + * number of bits in each individual array. */ + if (nvw > ovw && !grow_bucket_values(m, ovw, nvw)) { + return 0; + } + m->max_value = value; + } + + assert(m->max_value >= value); + + if (m->buckets_used >= m->bucket_count/2) { + if (!grow_buckets(m)) { + return 0; + } + } + + const uint64_t mask = m->bucket_count - 1; + for (size_t b_i = 0; b_i < m->bucket_count; b_i++) { + struct idmap_bucket *b = &m->buckets[(h + b_i) & mask]; + if (b->state == state_id) { + assert(b->values != NULL); + u64bitset_set(b->values, value); + return 1; + } else if (b->state == NO_STATE) { + b->state = state_id; + assert(b->values == NULL); + + const unsigned vw = value_words(m->max_value); + b->values = f_calloc(m->alloc, + vw, sizeof(b->values[0])); + if (b->values == NULL) { + return 0; + } + m->buckets_used++; + + u64bitset_set(b->values, value); + return 1; + } else { + continue; /* collision */ + } + + } + + assert(!"unreachable"); + return 0; +} + +static const struct idmap_bucket * +get_bucket(const struct idmap *m, fsm_state_t state_id) +{ + const uint64_t h = hash_id(state_id); + const uint64_t mask = m->bucket_count - 1; + for (size_t b_i = 0; b_i < m->bucket_count; b_i++) { + const struct idmap_bucket *b = &m->buckets[(h + b_i) & mask]; + if (b->state == NO_STATE) { + return NULL; + } else if (b->state == state_id) { + return b; + } + } + + return NULL; +} + +size_t +idmap_get_value_count(const struct idmap *m, fsm_state_t state_id) +{ + const struct idmap_bucket *b = get_bucket(m, state_id); + if (b == NULL) { + return 0; + } + assert(b->values != NULL); + + size_t res = 0; + const size_t words = value_words(m->max_value); + for (size_t w_i = 0; w_i < words; w_i++) { + const uint64_t w = b->values[w_i]; + /* This could use popcount64(w). */ + if (w == 0) { + continue; + } + for (uint64_t bit = 1; bit; bit <<= 1) { + if (w & bit) { + res++; + } + } + } + + return res; +} + +int +idmap_get(const struct idmap *m, fsm_state_t state_id, + size_t buf_size, unsigned *buf, size_t *written) +{ + const struct idmap_bucket *b = get_bucket(m, state_id); + if (b == NULL) { + if (written != NULL) { + *written = 0; + } + return 1; + } + + size_t buf_offset = 0; + const size_t words = value_words(m->max_value); + for (size_t w_i = 0; w_i < words; w_i++) { + const uint64_t w = b->values[w_i]; + if (w == 0) { + continue; + } + + for (uint64_t b_i = 0; b_i < 64; b_i++) { + if (w & ((uint64_t)1 << b_i)) { + if (buf_offset * sizeof(buf[0]) >= buf_size) { + return 0; + } + buf[buf_offset] = 64*w_i + b_i; + buf_offset++; + } + } + } + + if (written != NULL) { + *written = buf_offset; + } + return 1; +} + +void +idmap_iter(const struct idmap *m, + idmap_iter_fun *cb, void *opaque) +{ + const size_t words = value_words(m->max_value); + + for (size_t b_i = 0; b_i < m->bucket_count; b_i++) { + const struct idmap_bucket *b = &m->buckets[b_i]; + if (b->state == NO_STATE) { + continue; + } + + for (size_t w_i = 0; w_i < words; w_i++) { + const uint64_t w = b->values[w_i]; + if (w == 0) { + continue; + } + for (uint64_t b_i = 0; b_i < 64; b_i++) { + if (w & ((uint64_t)1 << b_i)) { + const unsigned v = 64*w_i + b_i; + cb(b->state, v, opaque); + } + } + } + } +} + +void +idmap_iter_for_state(const struct idmap *m, fsm_state_t state_id, + idmap_iter_fun *cb, void *opaque) +{ + const size_t words = value_words(m->max_value); + const struct idmap_bucket *b = get_bucket(m, state_id); + if (b == NULL) { + return; + } + + for (size_t w_i = 0; w_i < words; w_i++) { + const uint64_t w = b->values[w_i]; + if (w == 0) { + continue; + } + /* if N contiguous bits are all zero, skip them all at once */ +#define BLOCK_BITS 16 + uint64_t block = ((uint64_t)1 << BLOCK_BITS) - 1; + size_t block_count = 0; + + uint64_t b_i = 0; + while (b_i < 64) { + if ((w & block) == 0) { + block <<= BLOCK_BITS; + b_i += BLOCK_BITS; + continue; + } + + if (w & ((uint64_t)1 << b_i)) { + const unsigned v = 64*w_i + b_i; + cb(b->state, v, opaque); + block_count++; + } + b_i++; + block <<= 1; + } + +#define CHECK 0 +#if CHECK + size_t check_count = 0; + for (uint64_t b_i = 0; b_i < 64; b_i++) { + if (w & ((uint64_t)1 << b_i)) { + check_count++; + } + } + assert(block_count == check_count); +#endif + } +} diff --git a/src/libfsm/determinise.c b/src/libfsm/determinise.c index 56e135afd..e6611dda6 100644 --- a/src/libfsm/determinise.c +++ b/src/libfsm/determinise.c @@ -1339,6 +1339,7 @@ to_set_htab_check(struct analyze_closures_env *env, if (b->count == 0) { return 0; /* empty bucket -> not found */ } else if (b->count == count) { + assert(env->to_sets.buf != NULL); assert(b->offset + count <= env->to_sets.used); const fsm_state_t *ids = &env->to_sets.buf[b->offset]; if (0 == memcmp(ids, dst, count * sizeof(dst[0]))) { @@ -1465,6 +1466,7 @@ save_to_set(struct analyze_closures_env *env, env->to_sets.ceil = nceil; env->to_sets.buf = nbuf; } + assert(env->to_sets.buf != NULL); #if LOG_TO_SET static size_t to_set_id; diff --git a/src/libfsm/mode.c b/src/libfsm/mode.c index 76c60b8ad..87af0bdf9 100644 --- a/src/libfsm/mode.c +++ b/src/libfsm/mode.c @@ -28,6 +28,7 @@ fsm_findmode(const struct fsm *fsm, fsm_state_t state, unsigned int *freq) } mode; mode.freq = 1; + mode.state = (fsm_state_t)-1; edge_set_group_iter_reset(fsm->states[state].edges, EDGE_GROUP_ITER_ALL, &iter); while (edge_set_group_iter_next(&iter, &info)) { @@ -46,6 +47,9 @@ fsm_findmode(const struct fsm *fsm, fsm_state_t state, unsigned int *freq) *freq = mode.freq; } + /* It's not meaningful to call this on a state without edges. */ + assert(mode.state != (fsm_state_t)-1); + assert(mode.freq >= 1); return mode.state; } diff --git a/src/libfsm/vm/v1.c b/src/libfsm/vm/v1.c index a326b88d8..de1f6ea93 100644 --- a/src/libfsm/vm/v1.c +++ b/src/libfsm/vm/v1.c @@ -217,7 +217,9 @@ encode_opasm_v1(const struct dfavm_vm_op *instr, size_t ninstr, size_t total_byt return ret; error: - /* XXX - cleanup */ + if (ret != NULL) { + free(ret); + } return NULL; } diff --git a/src/libfsm/vm/v2.c b/src/libfsm/vm/v2.c index c85edff98..07eb12ef4 100644 --- a/src/libfsm/vm/v2.c +++ b/src/libfsm/vm/v2.c @@ -155,7 +155,10 @@ encode_opasm_v2(const struct dfavm_vm_op *instr, size_t ninstr) return ret; error: - /* XXX - cleanup */ + if (ret != NULL) { + free(ret); + } + return NULL; } diff --git a/tests/idmap/Makefile b/tests/idmap/Makefile new file mode 100644 index 000000000..aee01f565 --- /dev/null +++ b/tests/idmap/Makefile @@ -0,0 +1,19 @@ +.include "../../share/mk/top.mk" + +TEST.tests/idmap != ls -1 tests/idmap/idmap*.c +TEST_SRCDIR.tests/idmap = tests/idmap +TEST_OUTDIR.tests/idmap = ${BUILD}/tests/idmap + +.for n in ${TEST.tests/idmap:T:R:C/^idmap//} +INCDIR.${TEST_SRCDIR.tests/idmap}/idmap${n}.c += src/adt +.endfor + +.for n in ${TEST.tests/idmap:T:R:C/^idmap//} +test:: ${TEST_OUTDIR.tests/idmap}/res${n} +SRC += ${TEST_SRCDIR.tests/idmap}/idmap${n}.c +CFLAGS.${TEST_SRCDIR.tests/idmap}/idmap${n}.c += -UNDEBUG -D_DEFAULT_SOURCE -std=c99 +${TEST_OUTDIR.tests/idmap}/run${n}: ${TEST_OUTDIR.tests/idmap}/idmap${n}.o ${BUILD}/lib/adt.o + ${CC} ${CFLAGS} ${CFLAGS.${TEST_SRCDIR.tests/idmap}/idmap${n}.c} -o ${TEST_OUTDIR.tests/idmap}/run${n} ${TEST_OUTDIR.tests/idmap}/idmap${n}.o ${BUILD}/lib/adt.o +${TEST_OUTDIR.tests/idmap}/res${n}: ${TEST_OUTDIR.tests/idmap}/run${n} + ( ${TEST_OUTDIR.tests/idmap}/run${n} 1>&2 && echo PASS || echo FAIL ) > ${TEST_OUTDIR.tests/idmap}/res${n} +.endfor diff --git a/tests/idmap/idmap_basic.c b/tests/idmap/idmap_basic.c new file mode 100644 index 000000000..19f44d56e --- /dev/null +++ b/tests/idmap/idmap_basic.c @@ -0,0 +1,136 @@ +/* + * Copyright 2021 Scott Vokes + * + * See LICENCE for the full copyright terms. + */ + +#include +#include +#include + +#include + +#define DEF_LIMIT 10 +#define DEF_SEED 0 + +/* Thes numbers were chose to get a reasonable variety, + * but also some duplicated values as the input grows. */ +#define MAX_GEN_VALUES 23 +#define ID_MASK ((1 << 9) - 1) +#define VALUE_MASK ((1 << 10) - 1) + +static void +dump_cb(fsm_state_t state_id, unsigned value, void *opaque) +{ + /* fprintf(stderr, " -- state %d, value %u\n", state_id, value); */ + assert(state_id <= ID_MASK); + assert(value <= VALUE_MASK); + (void)opaque; +} + +static int +cmp_u(const void *pa, const void *pb) +{ + const unsigned a = *(unsigned *)pa; + const unsigned b = *(unsigned *)pb; + return a < b ? -1 : a > b ? 1 : 0; +} + +int main(int argc, char **argv) { + const size_t limit = (argc > 1 ? atoi(argv[1]) : DEF_LIMIT); + const unsigned seed = (argc > 2 ? atoi(argv[2]) : DEF_SEED); + + (void)argc; + (void)argv; + struct idmap *m = idmap_new(NULL); + + srandom(seed); + + /* Fill the table with random data */ + for (size_t id_i = 0; id_i < limit; id_i++) { + const fsm_state_t id = (fsm_state_t)(random() & ID_MASK); + const size_t value_count = random() % MAX_GEN_VALUES; + + for (size_t v_i = 0; v_i < value_count; v_i++) { + const unsigned v = random() & VALUE_MASK; + if (!idmap_set(m, id, v)) { + assert(!"failed to set"); + } + } + } + + idmap_iter(m, dump_cb, NULL); + + srandom(seed); + + size_t got_buf_ceil = MAX_GEN_VALUES; + unsigned *got_buf = malloc(got_buf_ceil * sizeof(got_buf[0])); + assert(got_buf != NULL); + + /* Reset the PRNG and read back the same data. */ + for (size_t id_i = 0; id_i < limit; id_i++) { + const fsm_state_t id = (fsm_state_t)(random() & ID_MASK); + const size_t generated_value_count = random() % MAX_GEN_VALUES; + + /* Note: This can occasionally differ from + * generated_value_count, because the same id or values + * may have been generated more than once. As long as + * all the values match, it's fine. */ + const size_t value_count = idmap_get_value_count(m, id); + + if (value_count > got_buf_ceil) { + size_t nceil = got_buf_ceil; + while (nceil <= value_count) { + nceil *= 2; + } + free(got_buf); + got_buf = malloc(nceil * sizeof(got_buf[0])); + assert(got_buf != NULL); + got_buf_ceil = nceil; + } + + size_t written; + if (!idmap_get(m, id, + got_buf_ceil * sizeof(got_buf[0]), got_buf, + &written)) { + assert(!"failed to get"); + } + assert(written == value_count); + + unsigned gen_buf[MAX_GEN_VALUES]; + + for (size_t v_i = 0; v_i < generated_value_count; v_i++) { + const unsigned v = random() & VALUE_MASK; + gen_buf[v_i] = v; + } + qsort(gen_buf, generated_value_count, sizeof(gen_buf[0]), cmp_u); + + /* Every generated value should appear in the buffer. + * There may be more in the buffer; ignore them. */ + size_t v_i = 0; + for (size_t gen_i = 0; gen_i < generated_value_count; gen_i++) { + int found = 0; + const unsigned gv = gen_buf[gen_i]; + assert(value_count <= got_buf_ceil); + /* got_buf should be sorted, so we can pick up where we left off */ + while (v_i < value_count) { + if (gv == got_buf[v_i]) { + /* Intentionally don't increment v_i on match, + * because gen_buf can repeat values. */ + found = 1; + break; + } + v_i++; + } + if (!found) { + fprintf(stderr, "NOT FOUND: state %d -- value: %u\n", + id, gv); + return EXIT_FAILURE; + } + } + } + + free(got_buf); + idmap_free(m); + return EXIT_SUCCESS; +} diff --git a/tests/pcre-anchor/in81.re b/tests/pcre-anchor/in81.re new file mode 100644 index 000000000..8b5fad7c3 --- /dev/null +++ b/tests/pcre-anchor/in81.re @@ -0,0 +1 @@ +($x)* \ No newline at end of file diff --git a/tests/pcre-anchor/out81.fsm b/tests/pcre-anchor/out81.fsm new file mode 100644 index 000000000..2cdc2f023 --- /dev/null +++ b/tests/pcre-anchor/out81.fsm @@ -0,0 +1,5 @@ +0 -> 0 ?; +0 -> 1 "\n"; + +start: 0; +end: 0, 1; \ No newline at end of file diff --git a/theft/Makefile b/theft/Makefile index 0d38d8cfc..921c482a9 100644 --- a/theft/Makefile +++ b/theft/Makefile @@ -6,7 +6,6 @@ SRC += theft/util.c SRC += theft/wrap.c SRC += theft/fuzz_adt_edge_set.c -SRC += theft/fuzz_adt_ipriq.c SRC += theft/fuzz_adt_priq.c SRC += theft/fuzz_capture_string_set.c SRC += theft/fuzz_literals.c diff --git a/theft/fuzz_adt_ipriq.c b/theft/fuzz_adt_ipriq.c deleted file mode 100644 index 1847ef6ce..000000000 --- a/theft/fuzz_adt_ipriq.c +++ /dev/null @@ -1,197 +0,0 @@ -/* - * Copyright 2021 Scott Vokes - * - * See LICENCE for the full copyright terms. - */ - -#include "type_info_adt_ipriq.h" - -#include -#include - -struct model { - size_t used; - size_t entries[]; -}; - -static enum ipriq_cmp_res -cmp_size_t(size_t a, size_t b, void *opaque) -{ - (void)opaque; - return a < b ? IPRIQ_CMP_LT : - a > b ? IPRIQ_CMP_GT : IPRIQ_CMP_EQ; -} - -static int exec_add(size_t x, struct model *m, struct ipriq *pq) -{ - if (!ipriq_add(pq, x)) { - return 0; - } - - m->entries[m->used] = x; - m->used++; - return 1; -} - -static int find_min_pos(const struct model *m, size_t *pos) -{ - size_t i; - if (m->used == 0) { - return 0; - } - - size_t res, min; - res = 0; - min = m->entries[0]; - - for (i = 1; i < m->used; i++) { - if (m->entries[i] < min) { - res = i; - min = m->entries[i]; - } - } - *pos = res; - return 1; -} - -static int exec_peek(struct model *m, struct ipriq *pq) -{ - size_t res; - - if (!ipriq_peek(pq, &res)) { - return m->used == 0; - } - - size_t pos; - if (!find_min_pos(m, &pos)) { - assert(!"unreachable (peek)"); - } - - return res == m->entries[pos]; -} - -static int exec_pop(struct model *m, struct ipriq *pq) -{ - size_t res; - - if (!ipriq_pop(pq, &res)) { - return m->used == 0; - } - - size_t pos; - if (!find_min_pos(m, &pos)) { - assert(!"unreachable (pop)"); - } - - if (res != m->entries[pos]) { - return 0; - } - - assert(m->used > 0); - if (pos < m->used - 1) { - m->entries[pos] = m->entries[m->used - 1]; - } - m->used--; - return 1; -} - -static enum theft_trial_res -compare_against_model(const struct ipriq_scenario *scen) -{ - enum theft_trial_res res = THEFT_TRIAL_FAIL; - size_t i; - - struct model *m = malloc(sizeof(*m) - + scen->count * sizeof(m->entries[0])); - if (m == NULL) { - return THEFT_TRIAL_ERROR; - } - m->used = 0; - - struct ipriq *pq = ipriq_new(NULL, cmp_size_t, NULL); - if (pq == NULL) { - return THEFT_TRIAL_ERROR; - } - - for (i = 0; i < scen->count; i++) { - const struct ipriq_op *op = &scen->ops[i]; - - switch (op->t) { - case IPRIQ_OP_ADD: - if (!exec_add(op->u.add.x, m, pq)) { - goto cleanup; - } - break; - - case IPRIQ_OP_PEEK: - if (!exec_peek(m, pq)) { - goto cleanup; - } - break; - - case IPRIQ_OP_POP: - if (!exec_pop(m, pq)) { - goto cleanup; - } - break; - - default: - assert(false); break; - } - } - - res = THEFT_TRIAL_PASS; - -cleanup: - free(m); - - return res; -} - -static enum theft_trial_res -prop_ipriq_model(struct theft *t, void *arg1) -{ - const struct ipriq_scenario *scen = arg1; - (void)t; - return compare_against_model(scen); -} - -static bool -test_ipriq(theft_seed seed, uintptr_t limit) -{ - enum theft_run_res res; - - struct ipriq_hook_env env = { - .tag = 'I', - .limit = limit, - }; - - struct theft_run_config config = { - .name = __func__, - .prop1 = prop_ipriq_model, - .type_info = { &type_info_adt_ipriq }, - .trials = 1000, - .hooks = { - .trial_pre = theft_hook_first_fail_halt, - .env = &env, - }, - .fork = { - .enable = true, - }, - - .seed = seed, - }; - - (void)limit; - - res = theft_run(&config); - printf("%s: %s\n", __func__, theft_run_res_str(res)); - - return res == THEFT_RUN_PASS; -} - -void -register_test_adt_ipriq(void) -{ - reg_test1("adt_ipriq", test_ipriq, 10000); -}