Browse code

Add theft

John Hawthorn authored on 03/04/2017 09:11:20
Showing 13 changed files

... ...
@@ -13,7 +13,8 @@ INSTALL_DATA=${INSTALL} -m 644
13 13
 
14 14
 LIBS=-lpthread
15 15
 OBJECTS=src/fzy.o src/match.o src/tty.o src/choices.o src/options.o src/tty_interface.o
16
-TESTOBJECTS=test/fzytest.c src/match.o src/choices.o src/options.o
16
+THEFTDEPS = deps/theft/theft.o deps/theft/theft_bloom.o deps/theft/theft_mt.o deps/theft/theft_hash.o
17
+TESTOBJECTS=test/fzytest.c test/test_properties.c src/match.o src/choices.o src/options.o $(THEFTDEPS)
17 18
 
18 19
 all: fzy
19 20
 
20 21
new file mode 100644
... ...
@@ -0,0 +1,3 @@
1
+*.o
2
+test_theft
3
+libtheft.a
0 4
new file mode 100644
... ...
@@ -0,0 +1,13 @@
1
+Copyright (c) 2014 Scott Vokes <vokes.s@gmail.com>
2
+ 
3
+Permission to use, copy, modify, and/or distribute this software for any
4
+purpose with or without fee is hereby granted, provided that the above
5
+copyright notice and this permission notice appear in all copies.
6
+ 
7
+THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
8
+WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
9
+MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
10
+ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
11
+WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
12
+ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
13
+OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
0 14
new file mode 100644
... ...
@@ -0,0 +1,496 @@
1
+#include <string.h>
2
+
3
+#include "theft.h"
4
+#include "theft_types_internal.h"
5
+#include "theft_bloom.h"
6
+#include "theft_mt.h"
7
+
8
+/* Initialize a theft test runner.
9
+ * BLOOM_BITS sets the size of the table used for detecting
10
+ * combinations of arguments that have already been tested.
11
+ * If 0, a default size will be chosen based on trial count.
12
+ * (This will only be used if all property types have hash
13
+ * callbacks defined.) The bloom filter can also be disabled
14
+ * by setting BLOOM_BITS to THEFT_BLOOM_DISABLE.
15
+ * 
16
+ * Returns a NULL if malloc fails or BLOOM_BITS is out of bounds. */
17
+struct theft *theft_init(uint8_t bloom_bits) {
18
+    if ((bloom_bits != 0 && (bloom_bits < THEFT_BLOOM_BITS_MIN))
19
+        || ((bloom_bits > THEFT_BLOOM_BITS_MAX) &&
20
+            bloom_bits != THEFT_BLOOM_DISABLE)) {
21
+        return NULL;
22
+    }
23
+
24
+    theft *t = malloc(sizeof(*t));
25
+    if (t == NULL) { return NULL; }
26
+    memset(t, 0, sizeof(*t));
27
+
28
+    t->mt = theft_mt_init(DEFAULT_THEFT_SEED);
29
+    if (t->mt == NULL) {
30
+        free(t);
31
+        return NULL;
32
+    } else {
33
+        t->out = stdout;
34
+        t->requested_bloom_bits = bloom_bits;
35
+        return t;
36
+    }
37
+}
38
+
39
+/* (Re-)initialize the random number generator with a specific seed. */
40
+void theft_set_seed(struct theft *t, uint64_t seed) {
41
+    t->seed = seed;
42
+    theft_mt_reset(t->mt, seed);
43
+}
44
+
45
+/* Get a random 64-bit integer from the test runner's PRNG. */
46
+theft_seed theft_random(struct theft *t) {
47
+    theft_seed ns = (theft_seed)theft_mt_random(t->mt);
48
+    return ns;
49
+}
50
+
51
+/* Get a random double from the test runner's PRNG. */
52
+double theft_random_double(struct theft *t) {
53
+    return theft_mt_random_double(t->mt);
54
+}
55
+
56
+/* Change T's output stream handle to OUT. (Default: stdout.) */
57
+void theft_set_output_stream(struct theft *t, FILE *out) { t->out = out; }
58
+
59
+/* Check if all argument info structs have all required callbacks. */
60
+static bool
61
+check_all_args(struct theft_propfun_info *info, bool *all_hashable) {
62
+    bool ah = true;
63
+    for (int i = 0; i < info->arity; i++) {
64
+        struct theft_type_info *ti = info->type_info[i];
65
+        if (ti->alloc == NULL) { return false; }
66
+        if (ti->hash == NULL) { ah = false; }
67
+    }
68
+    *all_hashable = ah;
69
+    return true;
70
+}
71
+
72
+static theft_progress_callback_res
73
+default_progress_cb(struct theft_trial_info *info, void *env) {
74
+    (void)info;
75
+    (void)env;
76
+    return THEFT_PROGRESS_CONTINUE;
77
+}
78
+
79
+static void infer_arity(struct theft_propfun_info *info) {
80
+    for (int i = 0; i < THEFT_MAX_ARITY; i++) {
81
+        if (info->type_info[i] == NULL) {
82
+            info->arity = i;
83
+            break;
84
+        }
85
+    }
86
+}
87
+
88
+/* Run a series of randomized trials of a property function.
89
+ *
90
+ * Configuration is specified in CFG; many fields are optional.
91
+ * See the type definition in `theft_types.h`. */
92
+theft_run_res
93
+theft_run(struct theft *t, struct theft_cfg *cfg) {
94
+    if (t == NULL || cfg == NULL) {
95
+        return THEFT_RUN_ERROR_BAD_ARGS;
96
+    }
97
+
98
+    struct theft_propfun_info info;
99
+    memset(&info, 0, sizeof(info));
100
+    info.name = cfg->name;
101
+    info.fun = cfg->fun;
102
+    memcpy(info.type_info, cfg->type_info, sizeof(info.type_info));
103
+    info.always_seed_count = cfg->always_seed_count;
104
+    info.always_seeds = cfg->always_seeds;
105
+
106
+    if (cfg->seed) {
107
+        theft_set_seed(t, cfg->seed);
108
+    } else {
109
+        theft_set_seed(t, DEFAULT_THEFT_SEED);
110
+    }
111
+
112
+    if (cfg->trials == 0) { cfg->trials = THEFT_DEF_TRIALS; }
113
+
114
+    return theft_run_internal(t, &info, cfg->trials, cfg->progress_cb,
115
+        cfg->env, cfg->report);
116
+}
117
+
118
+/* Actually run the trials, with all arguments made explicit. */
119
+static theft_run_res
120
+theft_run_internal(struct theft *t, struct theft_propfun_info *info,
121
+        int trials, theft_progress_cb *cb, void *env,
122
+        struct theft_trial_report *r) {
123
+
124
+    struct theft_trial_report fake_report;
125
+    if (r == NULL) { r = &fake_report; }
126
+    memset(r, 0, sizeof(*r));
127
+    
128
+    infer_arity(info);
129
+    if (info->arity == 0) {
130
+        return THEFT_RUN_ERROR_BAD_ARGS;
131
+    }
132
+
133
+    if (t == NULL || info == NULL || info->fun == NULL
134
+        || info->arity == 0) {
135
+        return THEFT_RUN_ERROR_BAD_ARGS;
136
+    }
137
+    
138
+    bool all_hashable = false;
139
+    if (!check_all_args(info, &all_hashable)) {
140
+        return THEFT_RUN_ERROR_MISSING_CALLBACK;
141
+    }
142
+
143
+    if (cb == NULL) { cb = default_progress_cb; }
144
+
145
+    /* If all arguments are hashable, then attempt to use
146
+     * a bloom filter to avoid redundant checking. */
147
+    if (all_hashable) {
148
+        if (t->requested_bloom_bits == 0) {
149
+            t->requested_bloom_bits = theft_bloom_recommendation(trials);
150
+        }
151
+        if (t->requested_bloom_bits != THEFT_BLOOM_DISABLE) {
152
+            t->bloom = theft_bloom_init(t->requested_bloom_bits);
153
+        }
154
+    }
155
+    
156
+    theft_seed seed = t->seed;
157
+    theft_seed initial_seed = t->seed;
158
+    int always_seeds = info->always_seed_count;
159
+    if (info->always_seeds == NULL) { always_seeds = 0; }
160
+
161
+    void *args[THEFT_MAX_ARITY];
162
+    
163
+    theft_progress_callback_res cres = THEFT_PROGRESS_CONTINUE;
164
+
165
+    for (int trial = 0; trial < trials; trial++) {
166
+        memset(args, 0xFF, sizeof(args));
167
+        if (cres == THEFT_PROGRESS_HALT) { break; }
168
+
169
+        /* If any seeds to always run were specified, use those before
170
+         * reverting to the specified starting seed. */
171
+        if (trial < always_seeds) {
172
+            seed = info->always_seeds[trial];
173
+        } else if ((always_seeds > 0) && (trial == always_seeds)) {
174
+            seed = initial_seed;
175
+        }
176
+
177
+        struct theft_trial_info ti = {
178
+            .name = info->name,
179
+            .trial = trial,
180
+            .seed = seed,
181
+            .arity = info->arity,
182
+            .args = args
183
+        };
184
+
185
+        theft_set_seed(t, seed);
186
+        all_gen_res_t gres = gen_all_args(t, info, seed, args, env);
187
+        switch (gres) {
188
+        case ALL_GEN_SKIP:
189
+            /* skip generating these args */
190
+            ti.status = THEFT_TRIAL_SKIP;
191
+            r->skip++;
192
+            cres = cb(&ti, env);
193
+            break;
194
+        case ALL_GEN_DUP:
195
+            /* skip these args -- probably already tried */
196
+            ti.status = THEFT_TRIAL_DUP;
197
+            r->dup++;
198
+            cres = cb(&ti, env);
199
+            break;
200
+        default:
201
+        case ALL_GEN_ERROR:
202
+            /* Error while generating args */
203
+            ti.status = THEFT_TRIAL_ERROR;
204
+            cres = cb(&ti, env);
205
+            return THEFT_RUN_ERROR;
206
+        case ALL_GEN_OK:
207
+            /* (Extracted function to avoid deep nesting here.) */
208
+            if (!run_trial(t, info, args, cb, env, r, &ti, &cres)) {
209
+                return THEFT_RUN_ERROR;
210
+            }
211
+        }
212
+
213
+        free_args(info, args, env);
214
+
215
+        /* Restore last known seed and generate next. */
216
+        theft_set_seed(t, seed);
217
+        seed = theft_random(t);
218
+    }
219
+
220
+    if (r->fail > 0) {
221
+        return THEFT_RUN_FAIL;
222
+    } else {
223
+        return THEFT_RUN_PASS;
224
+    }
225
+}
226
+
227
+/* Now that arguments have been generated, run the trial and update
228
+ * counters, call cb with results, etc. */
229
+static bool run_trial(struct theft *t, struct theft_propfun_info *info,
230
+        void **args, theft_progress_cb *cb, void *env,
231
+        struct theft_trial_report *r, struct theft_trial_info *ti,
232
+        theft_progress_callback_res *cres) {
233
+    if (t->bloom) { mark_called(t, info, args, env); }
234
+    theft_trial_res tres = call_fun(info, args);
235
+    ti->status = tres;
236
+    switch (tres) {
237
+    case THEFT_TRIAL_PASS:
238
+        r->pass++;
239
+        *cres = cb(ti, env);
240
+        break;
241
+    case THEFT_TRIAL_FAIL:
242
+        if (!attempt_to_shrink(t, info, args, env)) {
243
+            ti->status = THEFT_TRIAL_ERROR;
244
+            *cres = cb(ti, env);
245
+            return false;
246
+        }
247
+        r->fail++;
248
+        *cres = report_on_failure(t, info, ti, cb, env);
249
+        break;
250
+    case THEFT_TRIAL_SKIP:
251
+        *cres = cb(ti, env);
252
+        r->skip++;
253
+        break;
254
+    case THEFT_TRIAL_DUP:
255
+        /* user callback should not return this; fall through */
256
+    case THEFT_TRIAL_ERROR:
257
+        *cres = cb(ti, env);
258
+        free_args(info, args, env);
259
+        return false;
260
+    }
261
+    return true;
262
+}
263
+
264
+static void free_args(struct theft_propfun_info *info,
265
+        void **args, void *env) {
266
+    for (int i = 0; i < info->arity; i++) {
267
+        theft_free_cb *fcb = info->type_info[i]->free;
268
+        if (fcb && args[i] != THEFT_SKIP) {
269
+            fcb(args[i], env);
270
+        }
271
+    }
272
+}
273
+
274
+void theft_free(struct theft *t) {
275
+    if (t->bloom) {
276
+        theft_bloom_dump(t->bloom);
277
+        theft_bloom_free(t->bloom);
278
+        t->bloom = NULL;
279
+    }
280
+    theft_mt_free(t->mt);
281
+    free(t);
282
+}
283
+
284
+/* Actually call the property function. Its number of arguments is not
285
+ * constrained by the typedef, but will be defined at the call site
286
+ * here. (If info->arity is wrong, it will probably crash.) */
287
+static theft_trial_res
288
+call_fun(struct theft_propfun_info *info, void **args) {
289
+    theft_trial_res res = THEFT_TRIAL_ERROR;
290
+    switch (info->arity) {
291
+    case 1:
292
+        res = info->fun(args[0]);
293
+        break;
294
+    case 2:
295
+        res = info->fun(args[0], args[1]);
296
+        break;
297
+    case 3:
298
+        res = info->fun(args[0], args[1], args[2]);
299
+        break;
300
+    case 4:
301
+        res = info->fun(args[0], args[1], args[2], args[3]);
302
+        break;
303
+    case 5:
304
+        res = info->fun(args[0], args[1], args[2], args[3], args[4]);
305
+        break;
306
+    case 6:
307
+        res = info->fun(args[0], args[1], args[2], args[3], args[4],
308
+            args[5]);
309
+        break;
310
+    case 7:
311
+        res = info->fun(args[0], args[1], args[2], args[3], args[4],
312
+            args[5], args[6]);
313
+        break;
314
+    case 8:
315
+        res = info->fun(args[0], args[1], args[2], args[3], args[4],
316
+            args[5], args[6], args[7]);
317
+        break;
318
+    case 9:
319
+        res = info->fun(args[0], args[1], args[2], args[3], args[4],
320
+            args[5], args[6], args[7], args[8]);
321
+        break;
322
+    case 10:
323
+        res = info->fun(args[0], args[1], args[2], args[3], args[4],
324
+            args[5], args[6], args[7], args[8], args[9]);
325
+        break;
326
+    /* ... */
327
+    default:
328
+        return THEFT_TRIAL_ERROR;
329
+    }
330
+    return res;
331
+}
332
+
333
+/* Attempt to instantiate arguments, starting with the current seed. */
334
+static all_gen_res_t
335
+gen_all_args(theft *t, struct theft_propfun_info *info,
336
+        theft_seed seed, void *args[THEFT_MAX_ARITY], void *env) {
337
+    for (int i = 0; i < info->arity; i++) {
338
+        struct theft_type_info *ti = info->type_info[i];
339
+        void *p = ti->alloc(t, seed, env);
340
+        if (p == THEFT_SKIP || p == THEFT_ERROR) {
341
+            for (int j = 0; j < i; j++) {
342
+                ti->free(args[j], env);
343
+            }
344
+            if (p == THEFT_SKIP) {
345
+                return ALL_GEN_SKIP;
346
+            } else {
347
+                return ALL_GEN_ERROR;
348
+            }
349
+        } else {
350
+            args[i] = p;
351
+        }
352
+        seed = theft_random(t);
353
+    }
354
+
355
+    /* check bloom filter */
356
+    if (t->bloom && check_called(t, info, args, env)) {
357
+        return ALL_GEN_DUP;
358
+    }
359
+    
360
+    return ALL_GEN_OK;
361
+}
362
+
363
+/* Attempt to simplify all arguments, breadth first. Continue as long as
364
+ * progress is made, i.e., until a local minima is reached. */
365
+static bool
366
+attempt_to_shrink(theft *t, struct theft_propfun_info *info,
367
+        void *args[], void *env) {
368
+    bool progress = false;
369
+    do {
370
+        progress = false;
371
+        for (int ai = 0; ai < info->arity; ai++) {
372
+            struct theft_type_info *ti = info->type_info[ai];
373
+            if (ti->shrink) {
374
+                /* attempt to simplify this argument by one step */
375
+                shrink_res rres = attempt_to_shrink_arg(t, info, args, env, ai);
376
+                switch (rres) {
377
+                case SHRINK_OK:
378
+                    progress = true;
379
+                    break;
380
+                case SHRINK_DEAD_END:
381
+                    break;
382
+                default:
383
+                case SHRINK_ERROR:
384
+                    return false;
385
+                }
386
+            }
387
+        }
388
+    } while (progress);
389
+
390
+    return true;
391
+}
392
+
393
+/* Simplify an argument by trying all of its simplification tactics, in
394
+ * order, and checking whether the property still fails. If it passes,
395
+ * then revert the simplification and try another tactic.
396
+ *
397
+ * If the bloom filter is being used (i.e., if all arguments have hash
398
+ * callbacks defined), then use it to skip over areas of the state
399
+ * space that have probably already been tried. */
400
+static shrink_res
401
+attempt_to_shrink_arg(theft *t, struct theft_propfun_info *info,
402
+        void *args[], void *env, int ai) {
403
+    struct theft_type_info *ti = info->type_info[ai];
404
+
405
+    for (uint32_t tactic = 0; tactic < THEFT_MAX_TACTICS; tactic++) {
406
+        void *cur = args[ai];
407
+        void *nv = ti->shrink(cur, tactic, env);
408
+        if (nv == THEFT_NO_MORE_TACTICS) {
409
+            return SHRINK_DEAD_END;
410
+        } else if (nv == THEFT_ERROR) {
411
+            return SHRINK_ERROR;
412
+        } else if (nv == THEFT_DEAD_END) {
413
+            continue;   /* try next tactic */
414
+        }
415
+        
416
+        args[ai] = nv;
417
+        if (t->bloom) {
418
+            if (check_called(t, info, args, env)) {
419
+                /* probably redundant */
420
+                if (ti->free) { ti->free(nv, env); }
421
+                args[ai] = cur;
422
+                continue;
423
+            } else {
424
+                mark_called(t, info, args, env);
425
+            }
426
+        }
427
+        theft_trial_res res = call_fun(info, args);
428
+        
429
+        switch (res) {
430
+        case THEFT_TRIAL_PASS:
431
+        case THEFT_TRIAL_SKIP:
432
+            /* revert */
433
+            args[ai] = cur;
434
+            if (ti->free) { ti->free(nv, env); }
435
+            break;
436
+        case THEFT_TRIAL_FAIL:
437
+            if (ti->free) { ti->free(cur, env); }
438
+            return SHRINK_OK;
439
+        case THEFT_TRIAL_DUP:  /* user callback should not return this */
440
+        case THEFT_TRIAL_ERROR:
441
+            return SHRINK_ERROR;
442
+        }
443
+    }
444
+    (void)t;
445
+    return SHRINK_DEAD_END;
446
+}
447
+
448
+/* Populate a buffer with hashes of all the arguments. */
449
+static void get_arg_hash_buffer(theft_hash *buffer,
450
+        struct theft_propfun_info *info, void **args, void *env) {
451
+    for (int i = 0; i < info->arity; i++) {
452
+        buffer[i] = info->type_info[i]->hash(args[i], env);
453
+    }    
454
+}
455
+
456
+/* Mark the tuple of argument instances as called in the bloom filter. */
457
+static void mark_called(theft *t, struct theft_propfun_info *info,
458
+        void **args, void *env) {
459
+    theft_hash buffer[THEFT_MAX_ARITY];
460
+    get_arg_hash_buffer(buffer, info, args, env);
461
+    theft_bloom_mark(t->bloom, (uint8_t *)buffer,
462
+        info->arity * sizeof(theft_hash));
463
+}
464
+
465
+/* Check if this combination of argument instances has been called. */
466
+static bool check_called(theft *t, struct theft_propfun_info *info,
467
+        void **args, void *env) {
468
+    theft_hash buffer[THEFT_MAX_ARITY];
469
+    get_arg_hash_buffer(buffer, info, args, env);
470
+    return theft_bloom_check(t->bloom, (uint8_t *)buffer,
471
+        info->arity * sizeof(theft_hash));
472
+}
473
+
474
+/* Print info about a failure. */
475
+static theft_progress_callback_res report_on_failure(theft *t,
476
+        struct theft_propfun_info *info,
477
+        struct theft_trial_info *ti, theft_progress_cb *cb, void *env) {
478
+    static theft_progress_callback_res cres;
479
+
480
+    int arity = info->arity;
481
+    fprintf(t->out, "\n\n -- Counter-Example: %s\n",
482
+        info->name ? info-> name : "");
483
+    fprintf(t->out, "    Trial %u, Seed 0x%016llx\n", ti->trial,
484
+        (uint64_t)ti->seed);
485
+    for (int i = 0; i < arity; i++) {
486
+        theft_print_cb *print = info->type_info[i]->print;
487
+        if (print) {
488
+            fprintf(t->out, "    Argument %d:\n", i);
489
+            print(t->out, ti->args[i], env);
490
+            fprintf(t->out, "\n");
491
+        }
492
+   }
493
+
494
+    cres = cb(ti, env);
495
+    return cres;
496
+}
0 497
new file mode 100644
... ...
@@ -0,0 +1,74 @@
1
+#ifndef THEFT_H
2
+#define THEFT_H
3
+
4
+#include <stdlib.h>
5
+#include <stdio.h>
6
+#include <stdint.h>
7
+#include <stdbool.h>
8
+
9
+/* Version 0.2.0 */
10
+#define THEFT_VERSION_MAJOR 0
11
+#define THEFT_VERSION_MINOR 2
12
+#define THEFT_VERSION_PATCH 0
13
+
14
+/* A property can have at most this many arguments. */
15
+#define THEFT_MAX_ARITY 10
16
+
17
+#include "theft_types.h"
18
+
19
+/* Default number of trials to run. */
20
+#define THEFT_DEF_TRIALS 100
21
+
22
+/* Min and max bits used to determine bloom filter size.
23
+ * (A larger value uses more memory, but reduces the odds of an
24
+ * untested argument combination being falsely skipped.) */
25
+#define THEFT_BLOOM_BITS_MIN 13 /* 1 KB */
26
+#define THEFT_BLOOM_BITS_MAX 33 /* 1 GB */
27
+
28
+/* Initialize a theft test runner.
29
+ * BLOOM_BITS sets the size of the table used for detecting
30
+ * combinations of arguments that have already been tested.
31
+ * If 0, a default size will be chosen based on trial count.
32
+ * (This will only be used if all property types have hash
33
+ * callbacks defined.) The bloom filter can also be disabled
34
+ * by setting BLOOM_BITS to THEFT_BLOOM_DISABLE.
35
+ * 
36
+ * Returns a NULL if malloc fails or BLOOM_BITS is out of bounds. */
37
+struct theft *theft_init(uint8_t bloom_bits);
38
+
39
+/* Free a property-test runner. */
40
+void theft_free(struct theft *t);
41
+
42
+/* (Re-)initialize the random number generator with a specific seed. */
43
+void theft_set_seed(struct theft *t, uint64_t seed);
44
+
45
+/* Get a random 64-bit integer from the test runner's PRNG. */
46
+theft_hash theft_random(struct theft *t);
47
+
48
+/* Get a random double from the test runner's PRNG. */
49
+double theft_random_double(struct theft *t);
50
+
51
+/* Change T's output stream handle to OUT. (Default: stdout.) */
52
+void theft_set_output_stream(struct theft *t, FILE *out);
53
+
54
+/* Run a series of randomized trials of a property function.
55
+ *
56
+ * Configuration is specified in CFG; many fields are optional.
57
+ * See the type definition in `theft_types.h`. */
58
+theft_run_res
59
+theft_run(struct theft *t, struct theft_cfg *cfg);
60
+
61
+/* Hash a buffer in one pass. (Wraps the below functions.) */
62
+theft_hash theft_hash_onepass(uint8_t *data, size_t bytes);
63
+
64
+/* Init/reset a hasher for incremental hashing.
65
+ * Returns true, or false if you gave it a NULL pointer. */
66
+void theft_hash_init(struct theft_hasher *h);
67
+
68
+/* Sink more data into an incremental hash. */
69
+void theft_hash_sink(struct theft_hasher *h, uint8_t *data, size_t bytes);
70
+
71
+/* Finish hashing and get the result. */
72
+theft_hash theft_hash_done(struct theft_hasher *h);
73
+
74
+#endif
0 75
new file mode 100644
... ...
@@ -0,0 +1,145 @@
1
+#include <string.h>
2
+#include <stdio.h>
3
+
4
+#include "theft.h"
5
+#include "theft_bloom.h"
6
+
7
+#define DEFAULT_BLOOM_BITS 17
8
+#define DEBUG_BLOOM_FILTER 0
9
+#define LOG2_BITS_PER_BYTE 3
10
+#define HASH_COUNT 4
11
+
12
+static uint8_t get_bits_set_count(uint8_t counts[256], uint8_t byte);
13
+
14
+/* Initialize a bloom filter. */
15
+struct theft_bloom *theft_bloom_init(uint8_t bit_size2) {
16
+    size_t sz = 1 << (bit_size2 - LOG2_BITS_PER_BYTE);
17
+    struct theft_bloom *b = malloc(sizeof(struct theft_bloom) + sz);
18
+    if (b) {
19
+        b->size = sz;
20
+        b->bit_count = bit_size2;
21
+        memset(b->bits, 0, sz);
22
+    }
23
+    return b;
24
+}
25
+
26
+/* Hash data and mark it in the bloom filter. */
27
+void theft_bloom_mark(struct theft_bloom *b, uint8_t *data, size_t data_size) {
28
+    uint64_t hash = theft_hash_onepass(data, data_size);
29
+    uint8_t bc = b->bit_count;
30
+    uint64_t mask = (1 << bc) - 1;
31
+
32
+    /* Use HASH_COUNT distinct slices of MASK bits as hashes for the bloom filter. */
33
+    int bit_inc = (64 - bc) / HASH_COUNT;
34
+
35
+    for (int i = 0; i < (64 - bc); i += bit_inc) {
36
+        uint64_t v = (hash & (mask << i)) >> i;
37
+        size_t offset = v / 8;
38
+        uint8_t bit = 1 << (v & 0x07);
39
+        b->bits[offset] |= bit;
40
+    }
41
+}
42
+
43
+/* Check whether the data's hash is in the bloom filter. */
44
+bool theft_bloom_check(struct theft_bloom *b, uint8_t *data, size_t data_size) {
45
+    uint64_t hash = theft_hash_onepass(data, data_size);
46
+    uint8_t bc = b->bit_count;
47
+    uint64_t mask = (1 << bc) - 1;
48
+
49
+    int bit_inc = (64 - bc) / HASH_COUNT;
50
+
51
+    for (int i = 0; i < (64 - bc); i += bit_inc) {
52
+        uint64_t v = (hash & (mask << i)) >> i;
53
+        size_t offset = v / 8;
54
+        uint8_t bit = 1 << (v & 0x07);
55
+        if (0 == (b->bits[offset] & bit)) { return false; }
56
+    }
57
+
58
+    return true;
59
+}
60
+
61
+/* Free the bloom filter. */
62
+void theft_bloom_free(struct theft_bloom *b) { free(b); }
63
+
64
+/* Dump the bloom filter's contents. (Debugging.) */
65
+void theft_bloom_dump(struct theft_bloom *b) {
66
+    uint8_t counts[256];
67
+    memset(counts, 0xFF, sizeof(counts));
68
+
69
+    size_t total = 0;
70
+    uint16_t row_total = 0;
71
+    
72
+    for (size_t i = 0; i < b->size; i++) {
73
+        uint8_t count = get_bits_set_count(counts, b->bits[i]);
74
+        total += count;
75
+        row_total += count;
76
+        #if DEBUG_BLOOM_FILTER > 1
77
+        char c = (count == 0 ? '.' : '0' + count);
78
+        printf("%c", c);
79
+        if ((i & 63) == 0 || i == b->size - 1) {
80
+            printf(" - %2.1f%%\n",
81
+                (100 * row_total) / (64.0 * 8));
82
+            row_total = 0;
83
+        }
84
+        #endif
85
+    }
86
+
87
+    #if DEBUG_BLOOM_FILTER
88
+    printf(" -- bloom filter: %zd of %zd bits set (%2d%%)\n",
89
+        total, 8*b->size, (int)((100.0 * total)/(8.0*b->size)));
90
+    #endif
91
+
92
+    /* If the total number of bits set is > the number of bytes
93
+     * in the table (i.e., > 1/8 full) then warn the user. */
94
+    if (total > b->size) {
95
+        fprintf(stderr, "\nWARNING: bloom filter is %zd%% full, "
96
+            "larger bloom_bits value recommended.\n",
97
+            (size_t)((100 * total) / (8 * b->size)));
98
+    }
99
+}
100
+
101
+/* Recommend a bloom filter size for a given number of trials. */
102
+uint8_t theft_bloom_recommendation(int trials) {
103
+    /* With a preferred priority of false positives under 0.1%,
104
+     * the required number of bits m in the bloom filter is:
105
+     *     m = -lg(0.001)/(lg(2)^2) == 14.378 ~= 14,
106
+     * so we want an array with 1 << ceil(log2(14*trials)) cells.
107
+     *
108
+     * Note: The above formula is for the *ideal* number of hash
109
+     * functions, but we're using a hardcoded count. It appears to work
110
+     * well enough in practice, though, and this can be adjusted later
111
+     * without impacting the API. */
112
+    #define TRIAL_MULTIPILER 14
113
+    uint8_t res = DEFAULT_BLOOM_BITS;
114
+
115
+    const uint8_t min = THEFT_BLOOM_BITS_MIN - LOG2_BITS_PER_BYTE;
116
+    const uint8_t max = THEFT_BLOOM_BITS_MAX - LOG2_BITS_PER_BYTE;
117
+
118
+    for (uint8_t i = min; i < max; i++) {
119
+        int32_t v = (1 << i);
120
+        if (v > (TRIAL_MULTIPILER * trials)) {
121
+            res = i + LOG2_BITS_PER_BYTE;
122
+            break;
123
+        }
124
+    }
125
+
126
+    #if DEBUG_BLOOM_FILTER
127
+    size_t sz = 1 << (res - LOG2_BITS_PER_BYTE);
128
+    printf("Using %zd bytes for bloom filter: %d trials -> bit_size2 %u\n",
129
+        sizeof(struct theft_bloom) + sz, trials, res);
130
+    #endif
131
+
132
+    return res;
133
+}
134
+
135
+/* Check a byte->bits set table, and lazily populate it. */
136
+static uint8_t get_bits_set_count(uint8_t counts[256], uint8_t byte) {
137
+    uint8_t v = counts[byte];
138
+    if (v != 0xFF) { return v; }
139
+    uint8_t t = 0;
140
+    for (uint8_t i = 0; i < 8; i++) {
141
+        if (byte & (1 << i)) { t++; }
142
+    }
143
+    counts[byte] = t;
144
+    return t;
145
+}
0 146
new file mode 100644
... ...
@@ -0,0 +1,33 @@
1
+#ifndef THEFT_BLOOM_H
2
+#define THEFT_BLOOM_H
3
+
4
+#include <stdlib.h>
5
+#include <stdint.h>
6
+#include <stdbool.h>
7
+
8
+struct theft_bloom {
9
+    uint8_t bit_count;
10
+    size_t size;
11
+    uint8_t bits[];
12
+};
13
+
14
+/* Initialize a bloom filter. */
15
+struct theft_bloom *theft_bloom_init(uint8_t bit_size2);
16
+
17
+/* Hash data and mark it in the bloom filter. */
18
+void theft_bloom_mark(struct theft_bloom *b, uint8_t *data, size_t data_size);
19
+
20
+/* Check whether the data's hash is in the bloom filter. */
21
+bool theft_bloom_check(struct theft_bloom *b, uint8_t *data, size_t data_size);
22
+
23
+/* Free the bloom filter. */
24
+void theft_bloom_free(struct theft_bloom *b);
25
+
26
+/* Dump the bloom filter's contents. (Debugging.) */
27
+void theft_bloom_dump(struct theft_bloom *b);
28
+
29
+/* Recommend a bloom filter size for a given number of trials. */
30
+uint8_t theft_bloom_recommendation(int trials);
31
+
32
+
33
+#endif
0 34
new file mode 100644
... ...
@@ -0,0 +1,37 @@
1
+#include "theft.h"
2
+
3
+/* Fowler/Noll/Vo hash, 64-bit FNV-1a.
4
+ * This hashing algorithm is in the public domain.
5
+ * For more details, see: http://www.isthe.com/chongo/tech/comp/fnv/. */
6
+static const uint64_t fnv64_prime = 1099511628211L;
7
+static const uint64_t fnv64_offset_basis = 14695981039346656037UL;
8
+
9
+/* Init a hasher for incremental hashing. */
10
+void theft_hash_init(struct theft_hasher *h) {
11
+    h->accum = fnv64_offset_basis;
12
+}
13
+
14
+/* Sink more data into an incremental hash. */
15
+void theft_hash_sink(struct theft_hasher *h, uint8_t *data, size_t bytes) {
16
+    if (h == NULL || data == NULL) { return; }
17
+    uint64_t a = h->accum;
18
+    for (size_t i = 0; i < bytes; i++) {
19
+        a = (a ^ data[i]) * fnv64_prime;
20
+    }
21
+    h->accum = a;
22
+}
23
+
24
+/* Finish hashing and get the result. */
25
+theft_hash theft_hash_done(struct theft_hasher *h) {
26
+    theft_hash res = h->accum;
27
+    theft_hash_init(h);                /* reset */
28
+    return res;
29
+}
30
+
31
+/* Hash a buffer in one pass. (Wraps the above functions.) */
32
+theft_hash theft_hash_onepass(uint8_t *data, size_t bytes) {
33
+    struct theft_hasher h;
34
+    theft_hash_init(&h);
35
+    theft_hash_sink(&h, data, bytes);
36
+    return theft_hash_done(&h);
37
+}
0 38
new file mode 100644
... ...
@@ -0,0 +1,144 @@
1
+/* 
2
+   A C-program for MT19937-64 (2004/9/29 version).
3
+   Coded by Takuji Nishimura and Makoto Matsumoto.
4
+
5
+   This is a 64-bit version of Mersenne Twister pseudorandom number
6
+   generator.
7
+
8
+   Before using, initialize the state by using init_genrand64(seed)  
9
+   or init_by_array64(init_key, key_length).
10
+
11
+   Copyright (C) 2004, Makoto Matsumoto and Takuji Nishimura,
12
+   All rights reserved.                          
13
+
14
+   Redistribution and use in source and binary forms, with or without
15
+   modification, are permitted provided that the following conditions
16
+   are met:
17
+
18
+     1. Redistributions of source code must retain the above copyright
19
+        notice, this list of conditions and the following disclaimer.
20
+
21
+     2. Redistributions in binary form must reproduce the above copyright
22
+        notice, this list of conditions and the following disclaimer in the
23
+        documentation and/or other materials provided with the distribution.
24
+
25
+     3. The names of its contributors may not be used to endorse or promote 
26
+        products derived from this software without specific prior written 
27
+        permission.
28
+
29
+   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
30
+   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
31
+   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
32
+   A PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT OWNER OR
33
+   CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
34
+   EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
35
+   PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
36
+   PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
37
+   LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
38
+   NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
39
+   SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
40
+
41
+   References:
42
+   T. Nishimura, ``Tables of 64-bit Mersenne Twisters''
43
+     ACM Transactions on Modeling and 
44
+     Computer Simulation 10. (2000) 348--357.
45
+   M. Matsumoto and T. Nishimura,
46
+     ``Mersenne Twister: a 623-dimensionally equidistributed
47
+       uniform pseudorandom number generator''
48
+     ACM Transactions on Modeling and 
49
+     Computer Simulation 8. (Jan. 1998) 3--30.
50
+
51
+   Any feedback is very welcome.
52
+   http://www.math.hiroshima-u.ac.jp/~m-mat/MT/emt.html
53
+   email: m-mat @ math.sci.hiroshima-u.ac.jp (remove spaces)
54
+*/
55
+
56
+/* The code has been modified to store internal state in heap/stack
57
+ * allocated memory, rather than statically allocated memory, to allow
58
+ * multiple instances running in the same address space. */
59
+
60
+#include <stdlib.h>
61
+#include <stdio.h>
62
+#include "theft_mt.h"
63
+
64
+#define NN THEFT_MT_PARAM_N
65
+#define MM 156
66
+#define MATRIX_A 0xB5026F5AA96619E9ULL
67
+#define UM 0xFFFFFFFF80000000ULL /* Most significant 33 bits */
68
+#define LM 0x7FFFFFFFULL /* Least significant 31 bits */
69
+
70
+static uint64_t genrand64_int64(struct theft_mt *r);
71
+
72
+/* Heap-allocate a mersenne twister struct. */
73
+struct theft_mt *theft_mt_init(uint64_t seed) {
74
+    struct theft_mt *mt = malloc(sizeof(struct theft_mt));
75
+    if (mt == NULL) { return NULL; }
76
+    theft_mt_reset(mt, seed);
77
+    return mt;
78
+}
79
+
80
+/* Free a heap-allocated mersenne twister struct. */
81
+void theft_mt_free(struct theft_mt *mt) {
82
+    free(mt);
83
+}
84
+
85
+/* initializes mt[NN] with a seed */
86
+void theft_mt_reset(struct theft_mt *mt, uint64_t seed)
87
+{
88
+    mt->mt[0] = seed;
89
+    uint16_t mti = 0;
90
+    for (mti=1; mti<NN; mti++) {
91
+        mt->mt[mti] = (6364136223846793005ULL *
92
+            (mt->mt[mti-1] ^ (mt->mt[mti-1] >> 62)) + mti);
93
+    }
94
+    mt->mti = mti;
95
+}
96
+
97
+/* Get a 64-bit random number. */
98
+uint64_t theft_mt_random(struct theft_mt *mt) {
99
+    return genrand64_int64(mt);
100
+}
101
+
102
+/* Generate a random number on [0,1]-real-interval. */
103
+double theft_mt_random_double(struct theft_mt *mt)
104
+{
105
+    return (genrand64_int64(mt) >> 11) * (1.0/9007199254740991.0);
106
+}
107
+
108
+/* generates a random number on [0, 2^64-1]-interval */
109
+static uint64_t genrand64_int64(struct theft_mt *r)
110
+{
111
+    int i;
112
+    uint64_t x;
113
+    static uint64_t mag01[2]={0ULL, MATRIX_A};
114
+
115
+    if (r->mti >= NN) { /* generate NN words at one time */
116
+
117
+        /* if init has not been called, */
118
+        /* a default initial seed is used */
119
+        if (r->mti == NN+1)
120
+            theft_mt_reset(r, 5489ULL);
121
+
122
+        for (i=0;i<NN-MM;i++) {
123
+            x = (r->mt[i]&UM)|(r->mt[i+1]&LM);
124
+            r->mt[i] = r->mt[i+MM] ^ (x>>1) ^ mag01[(int)(x&1ULL)];
125
+        }
126
+        for (;i<NN-1;i++) {
127
+            x = (r->mt[i]&UM)|(r->mt[i+1]&LM);
128
+            r->mt[i] = r->mt[i+(MM-NN)] ^ (x>>1) ^ mag01[(int)(x&1ULL)];
129
+        }
130
+        x = (r->mt[NN-1]&UM)|(r->mt[0]&LM);
131
+        r->mt[NN-1] = r->mt[MM-1] ^ (x>>1) ^ mag01[(int)(x&1ULL)];
132
+
133
+        r->mti = 0;
134
+    }
135
+  
136
+    x = r->mt[r->mti++];
137
+
138
+    x ^= (x >> 29) & 0x5555555555555555ULL;
139
+    x ^= (x << 17) & 0x71D67FFFEDA60000ULL;
140
+    x ^= (x << 37) & 0xFFF7EEE000000000ULL;
141
+    x ^= (x >> 43);
142
+
143
+    return x;
144
+}
0 145
new file mode 100644
... ...
@@ -0,0 +1,36 @@
1
+#ifndef THEFT_MT_H
2
+#define THEFT_MT_H
3
+
4
+#include <stdint.h>
5
+
6
+/* Wrapper for Mersenne Twister.
7
+ * See copyright and license in theft_mt.c, more details at:
8
+ *     http://www.math.sci.hiroshima-u.ac.jp/~m-mat/MT/emt.html
9
+ *
10
+ * The code has been modified to store internal state in heap/stack
11
+ * allocated memory, rather than statically allocated memory, to allow
12
+ * multiple instances running in the same address space. */
13
+
14
+#define THEFT_MT_PARAM_N 312
15
+
16
+struct theft_mt {
17
+    uint64_t mt[THEFT_MT_PARAM_N]; /* the array for the state vector  */
18
+    int16_t mti;
19
+};
20
+
21
+/* Heap-allocate a mersenne twister struct. */
22
+struct theft_mt *theft_mt_init(uint64_t seed);
23
+
24
+/* Free a heap-allocated mersenne twister struct. */
25
+void theft_mt_free(struct theft_mt *mt);
26
+
27
+/* Reset a mersenne twister struct, possibly stack-allocated. */
28
+void theft_mt_reset(struct theft_mt *mt, uint64_t seed);
29
+
30
+/* Get a 64-bit random number. */
31
+uint64_t theft_mt_random(struct theft_mt *mt);
32
+
33
+/* Generate a random number on [0,1]-real-interval. */
34
+double theft_mt_random_double(struct theft_mt *mt);
35
+
36
+#endif
0 37
new file mode 100644
... ...
@@ -0,0 +1,197 @@
1
+#ifndef THEFT_TYPES_H
2
+#define THEFT_TYPES_H
3
+
4
+/* A pseudo-random number/seed, used to generate instances. */
5
+typedef uint64_t theft_seed;
6
+
7
+/* A hash of an instance. */
8
+typedef uint64_t theft_hash;
9
+
10
+/* These are opaque, as far as the API is concerned. */
11
+struct theft_bloom;             /* bloom filter */
12
+struct theft_mt;                /* mersenne twister PRNG */
13
+
14
+/* Struct for property-testing state. */
15
+struct theft {
16
+    FILE *out;
17
+    theft_seed seed;
18
+    uint8_t requested_bloom_bits;
19
+    struct theft_bloom *bloom;  /* bloom filter */
20
+    struct theft_mt *mt;        /* random number generator */
21
+};
22
+
23
+/* Special sentinel values returned instead of instance pointers. */
24
+#define THEFT_SKIP ((void *)-1)
25
+#define THEFT_ERROR ((void *)-2)
26
+#define THEFT_DEAD_END ((void *)-1)
27
+#define THEFT_NO_MORE_TACTICS ((void *)-3)
28
+
29
+/* Explicitly disable using the bloom filter.
30
+ * Note that if you do this, you must be sure your simplify function
31
+ * *always* returns a simpler value, or it will loop forever. */
32
+#define THEFT_BLOOM_DISABLE ((uint8_t)-1)
33
+
34
+/* Allocate and return an instance of the type, based on a known
35
+ * pseudo-random number seed. To get additional seeds, use
36
+ * theft_random(t); this stream of numbers will be deterministic, so if
37
+ * the alloc callback is constructed appropriately, an identical
38
+ * instance can be constructed later from the same initial seed.
39
+ * 
40
+ * Returns a pointer to the instance, THEFT_ERROR, or THEFT_SKIP. */
41
+typedef void *(theft_alloc_cb)(struct theft *t, theft_seed seed, void *env);
42
+
43
+/* Free an instance. */
44
+typedef void (theft_free_cb)(void *instance, void *env);
45
+
46
+/* Hash an instance. Used to skip combinations of arguments which
47
+ * have probably already been checked. */
48
+typedef theft_hash (theft_hash_cb)(void *instance, void *env);
49
+
50
+/* Attempt to shrink an instance to a simpler instance.
51
+ * 
52
+ * For a given INSTANCE, there are likely to be multiple ways in which
53
+ * it can be simplified. For example, a list of unsigned ints could have
54
+ * the first element decremented, divided by 2, or dropped. This
55
+ * callback should return a pointer to a freshly allocated, simplified
56
+ * instance, or should return THEFT_DEAD_END to indicate that the
57
+ * instance cannot be simplified further by this method.
58
+ *
59
+ * These tactics will be lazily explored breadth-first, to
60
+ * try to find simpler versions of arguments that cause the
61
+ * property to no longer hold.
62
+ *
63
+ * If this callback is NULL, it is equivalent to always returning
64
+ * THEFT_NO_MORE_TACTICS. */
65
+typedef void *(theft_shrink_cb)(void *instance, uint32_t tactic, void *env);
66
+
67
+/* Print INSTANCE to output stream F.
68
+ * Used for displaying counter-examples. Can be NULL. */
69
+typedef void (theft_print_cb)(FILE *f, void *instance, void *env);
70
+
71
+/* Result from a single trial. */
72
+typedef enum {
73
+    THEFT_TRIAL_PASS,           /* property held */
74
+    THEFT_TRIAL_FAIL,           /* property contradicted */
75
+    THEFT_TRIAL_SKIP,           /* user requested skip; N/A */
76
+    THEFT_TRIAL_DUP,            /* args probably already tried */
77
+    THEFT_TRIAL_ERROR,          /* unrecoverable error, halt */
78
+} theft_trial_res;
79
+
80
+/* A test property function. Arguments must match the types specified by
81
+ * theft_cfg.type_info, or the result will be undefined. For example, a
82
+ * propfun `prop_foo(A x, B y, C z)` must have a type_info array of
83
+ * `{ info_A, info_B, info_C }`.
84
+ * 
85
+ * Should return:
86
+ *     THEFT_TRIAL_PASS if the property holds,
87
+ *     THEFT_TRIAL_FAIL if a counter-example is found,
88
+ *     THEFT_TRIAL_SKIP if the combination of args isn't applicable,
89
+ *  or THEFT_TRIAL_ERROR if the whole run should be halted. */
90
+typedef theft_trial_res (theft_propfun)( /* arguments unconstrained */ );
91
+
92
+/* Callbacks used for testing with random instances of a type.
93
+ * For more information, see comments on their typedefs. */
94
+struct theft_type_info {
95
+    /* Required: */
96
+    theft_alloc_cb *alloc;      /* gen random instance from seed */
97
+
98
+    /* Optional, but recommended: */
99
+    theft_free_cb *free;        /* free instance */
100
+    theft_hash_cb *hash;        /* instance -> hash */
101
+    theft_shrink_cb *shrink;    /* shrink instance */
102
+    theft_print_cb *print;      /* fprintf instance */
103
+};
104
+
105
+/* Result from an individual trial. */
106
+struct theft_trial_info {
107
+    const char *name;           /* property name */
108
+    int trial;                  /* N'th trial */
109
+    theft_seed seed;            /* Seed used */
110
+    theft_trial_res status;     /* Run status */
111
+    uint8_t arity;              /* Number of arguments */
112
+    void **args;                /* Arguments used */
113
+};
114
+
115
+/* Whether to keep running trials after N failures/skips/etc. */
116
+typedef enum {
117
+    THEFT_PROGRESS_CONTINUE,    /* keep running trials */
118
+    THEFT_PROGRESS_HALT,        /* no need to continue */
119
+} theft_progress_callback_res;
120
+
121
+/* Handle test results.
122
+ * Can be used to halt after too many failures, print '.' after
123
+ * every N trials, etc. */
124
+typedef theft_progress_callback_res
125
+(theft_progress_cb)(struct theft_trial_info *info, void *env);
126
+
127
+/* Result from a trial run. */
128
+typedef enum {
129
+    THEFT_RUN_PASS = 0,             /* no failures */
130
+    THEFT_RUN_FAIL = 1,             /* 1 or more failures */
131
+    THEFT_RUN_ERROR = 2,            /* an error occurred */
132
+    THEFT_RUN_ERROR_BAD_ARGS = -1,  /* API misuse */
133
+    /* Missing required callback for 1 or more types */
134
+    THEFT_RUN_ERROR_MISSING_CALLBACK = -2,
135
+} theft_run_res;
136
+
137
+/* Optional report from a trial run; same meanings as theft_trial_res. */
138
+struct theft_trial_report {
139
+    size_t pass;
140
+    size_t fail;
141
+    size_t skip;
142
+    size_t dup;
143
+};
144
+
145
+/* Configuration struct for a theft test.
146
+ * In C99, this struct can be specified as a literal, like this:
147
+ * 
148
+ *     struct theft_cfg cfg = {
149
+ *         .name = "example",
150
+ *         .fun = prop_fun,
151
+ *         .type_info = { type_arg_a, type_arg_b },
152
+ *         .seed = 0x7he5eed,
153
+ *     };
154
+ *
155
+ * and omitted fields will be set to defaults.
156
+ * */
157
+struct theft_cfg {
158
+    /* Property function under test, and info about its arguments.
159
+     * The function is called with as many arguments are there
160
+     * are values in TYPE_INFO, so it can crash if that is wrong. */
161
+    theft_propfun *fun;
162
+    struct theft_type_info *type_info[THEFT_MAX_ARITY];
163
+
164
+    /* -- All fields after this point are optional. -- */
165
+
166
+    /* Property name, displayed in test runner output. */
167
+    const char *name;
168
+
169
+    /* Array of seeds to always run, and its length.
170
+     * Can be used for regression tests. */
171
+    int always_seed_count;      /* number of seeds */
172
+    theft_seed *always_seeds;   /* seeds to always run */
173
+
174
+    /* Number of trials to run. Defaults to THEFT_DEF_TRIALS. */
175
+    int trials;
176
+
177
+    /* Progress callback, used to display progress in
178
+     * slow-running tests, halt early under certain conditions, etc. */
179
+    theft_progress_cb *progress_cb;
180
+
181
+    /* Environment pointer. This is completely opaque to theft itself,
182
+     * but will be passed along to all callbacks. */
183
+    void *env;
184
+
185
+    /* Struct to populate with more detailed test results. */
186
+    struct theft_trial_report *report;
187
+
188
+    /* Seed for the random number generator. */
189
+    theft_seed seed;
190
+};
191
+
192
+/* Internal state for incremental hashing. */
193
+struct theft_hasher {
194
+    theft_hash accum;
195
+};
196
+
197
+#endif
0 198
new file mode 100644
... ...
@@ -0,0 +1,73 @@
1
+#ifndef THEFT_TYPES_INTERNAL_H
2
+#define THEFT_TYPES_INTERNAL_H
3
+
4
+typedef struct theft theft;
5
+
6
+#define THEFT_MAX_TACTICS ((uint32_t)-1)
7
+#define DEFAULT_THEFT_SEED 0xa600d16b175eedL
8
+
9
+typedef enum {
10
+    ALL_GEN_OK,                 /* all arguments generated okay */
11
+    ALL_GEN_SKIP,               /* skip due to user constraints */
12
+    ALL_GEN_DUP,                /* skip probably duplicated trial */
13
+    ALL_GEN_ERROR,              /* memory error or other failure */
14
+} all_gen_res_t;
15
+
16
+typedef enum {
17
+    SHRINK_OK,                  /* simplified argument further */
18
+    SHRINK_DEAD_END,            /* at local minima */
19
+    SHRINK_ERROR,               /* hard error during shrinking */
20
+} shrink_res;
21
+
22
+/* Testing context for a specific property function. */
23
+struct theft_propfun_info {
24
+    const char *name;           /* property name, can be NULL */
25
+    theft_propfun *fun;         /* property function under test */
26
+
27
+    /* Type info for ARITY arguments. */
28
+    uint8_t arity;              /* number of arguments */
29
+    struct theft_type_info *type_info[THEFT_MAX_ARITY];
30
+
31
+    /* Optional array of seeds to always run.
32
+     * Can be used for regression tests. */
33
+    int always_seed_count;      /* number of seeds */
34
+    theft_seed *always_seeds;   /* seeds to always run */
35
+};
36
+
37
+static theft_trial_res
38
+call_fun(struct theft_propfun_info *info, void **args);
39
+
40
+static bool run_trial(struct theft *t, struct theft_propfun_info *info,
41
+    void **args, theft_progress_cb *cb, void *env,
42
+    struct theft_trial_report *r, struct theft_trial_info *ti,
43
+    theft_progress_callback_res *cres);
44
+
45
+static void mark_called(theft *t, struct theft_propfun_info *info,
46
+    void **args, void *env);
47
+
48
+static bool check_called(theft *t, struct theft_propfun_info *info,
49
+    void **args, void *env);
50
+
51
+static theft_progress_callback_res report_on_failure(theft *t,
52
+    struct theft_propfun_info *info,
53
+    struct theft_trial_info *ti, theft_progress_cb *cb, void *env);
54
+
55
+static all_gen_res_t gen_all_args(theft *t, struct theft_propfun_info *info,
56
+    theft_seed seed, void *args[THEFT_MAX_ARITY], void *env);
57
+
58
+static void free_args(struct theft_propfun_info *info,
59
+    void **args, void *env);
60
+
61
+static theft_run_res theft_run_internal(struct theft *t,
62
+    struct theft_propfun_info *info,
63
+    int trials, theft_progress_cb *cb, void *env,
64
+    struct theft_trial_report *r);
65
+
66
+static bool attempt_to_shrink(theft *t, struct theft_propfun_info *info,
67
+    void *args[], void *env);
68
+
69
+static shrink_res
70
+attempt_to_shrink_arg(theft *t, struct theft_propfun_info *info,
71
+    void *args[], void *env, int ai);
72
+
73
+#endif
0 74
new file mode 100644