diff --git a/inc/theft.h b/inc/theft.h index 3835d12..5787365 100644 --- a/inc/theft.h +++ b/inc/theft.h @@ -171,6 +171,13 @@ const char *theft_trial_res_str(enum theft_trial_res res); /* Return a string name of a run result. */ const char *theft_run_res_str(enum theft_run_res res); +/* Tag the current failure type. This can be used to restrict + * shrinking to a specific kind of failure. A fail_id of + * `THEFT_FAILURE_TAG_NONE` clears the current tag, if any. */ +void theft_tag_failure(struct theft *t, size_t fail_id); +#define THEFT_FAILURE_TAG_NONE ((size_t)-2) + + /*********************** * Built-in generators * ***********************/ diff --git a/inc/theft_types.h b/inc/theft_types.h index fb1ea84..f429ece 100644 --- a/inc/theft_types.h +++ b/inc/theft_types.h @@ -325,6 +325,7 @@ struct theft_hook_trial_post_info { uint8_t arity; void **args; enum theft_trial_res result; + size_t failure_tag; bool repeat; }; typedef enum theft_hook_trial_post_res diff --git a/src/theft_aux.c b/src/theft_aux.c index b7aa78c..9a8fab3 100644 --- a/src/theft_aux.c +++ b/src/theft_aux.c @@ -218,3 +218,8 @@ const char *theft_trial_res_str(enum theft_trial_res res) { return "(matchfail)"; } } + +void theft_tag_failure(struct theft *t, size_t fail_id) { + t->trial.failure_tag = fail_id; +} + diff --git a/src/theft_run.c b/src/theft_run.c index 1f22139..be46438 100644 --- a/src/theft_run.c +++ b/src/theft_run.c @@ -225,6 +225,7 @@ run_step(struct theft *t, size_t trial, theft_seed *seed) { struct trial_info trial_info = { .trial = trial, .seed = *seed, + .failure_tag = THEFT_FAILURE_TAG_NONE, }; if (!init_arg_info(t, &trial_info)) { return RUN_STEP_GEN_ERROR; } diff --git a/src/theft_shrink.c b/src/theft_shrink.c index 95fe23c..07e342a 100644 --- a/src/theft_shrink.c +++ b/src/theft_shrink.c @@ -133,6 +133,8 @@ attempt_to_shrink_arg(struct theft *t, uint8_t arg_i) { } } + const size_t tagged_ft = t->trial.failure_tag; + enum theft_trial_res res; bool repeated = false; for (;;) { @@ -141,6 +143,19 @@ attempt_to_shrink_arg(struct theft *t, uint8_t arg_i) { res = theft_call(t, args); LOG(3 - LOG_SHRINK, "%s: call -> res %d\n", __func__, res); + const size_t new_ft = t->trial.failure_tag; + + /* If the trial found a tagged failure, and shrinking led to + * a different tag, skip this shrink. An untagged failure + * may be a completely new failure, so still switch over. */ + if (res == THEFT_TRIAL_FAIL && tagged_ft != THEFT_FAILURE_TAG_NONE + && new_ft != THEFT_FAILURE_TAG_NONE && tagged_ft != new_ft) { + LOG(1 - LOG_SHRINK, + "%s: skipping failure %zd, staying on tagged failure %zd\n", + __func__, new_ft, tagged_ft); + t->trial.failure_tag = tagged_ft; + res = THEFT_TRIAL_SKIP; + } if (!repeated) { if (res == THEFT_TRIAL_FAIL) { diff --git a/src/theft_trial.c b/src/theft_trial.c index fad6964..f95ce97 100644 --- a/src/theft_trial.c +++ b/src/theft_trial.c @@ -36,6 +36,7 @@ theft_trial_run(struct theft *t, .arity = t->prop.arity, .args = args, .result = tres, + .failure_tag = t->trial.failure_tag, }; switch (tres) { @@ -112,6 +113,7 @@ report_on_failure(struct theft *t, theft_hook_trial_post_cb *trial_post, void *trial_post_env) { theft_hook_counterexample_cb *counterexample = t->hooks.counterexample; + if (counterexample != NULL) { struct theft_hook_counterexample_info counterexample_hook_info = { .t = t, diff --git a/src/theft_types_internal.h b/src/theft_types_internal.h index 3149375..5d81b4f 100644 --- a/src/theft_types_internal.h +++ b/src/theft_types_internal.h @@ -105,6 +105,7 @@ struct trial_info { size_t shrink_count; size_t successful_shrinks; size_t failed_shrinks; + size_t failure_tag; struct arg_info args[THEFT_MAX_ARITY]; }; diff --git a/test/test_theft_integration.c b/test/test_theft_integration.c index db67c98..d3f8a81 100644 --- a/test/test_theft_integration.c +++ b/test/test_theft_integration.c @@ -1517,6 +1517,82 @@ TEST trial_post_hook_gets_correct_args(void) { PASS(); } +enum example_failure_tag { + EX_FAIL_TAG_ODD, + EX_FAIL_TAG_GTE_1000, +}; + +static enum theft_trial_res +prop_lt_1000_and_even(struct theft *t, void *arg1) { + uint64_t v = *(uint64_t *)arg1; + //fprintf(stderr, "PROP %u\n", v); + + if (v >= 1000) { + theft_tag_failure(t, EX_FAIL_TAG_GTE_1000); + return THEFT_TRIAL_FAIL; + } else if (v & 1) { + theft_tag_failure(t, EX_FAIL_TAG_ODD); + return THEFT_TRIAL_FAIL; + } + + return THEFT_TRIAL_PASS; +} + +static enum theft_hook_trial_post_res +trial_post_check_failure_tag(const struct theft_hook_trial_post_info *info, + void *env) +{ + bool *has_1000_failure = (bool *)env; + if (info->result == THEFT_TRIAL_FAIL && + info->failure_tag == EX_FAIL_TAG_GTE_1000) { + uint64_t v = *(uint64_t *)info->args[0]; + //fprintf(stderr, "TRIAL_POST %u\n", v); + if (v == 1000) { + *has_1000_failure = true; + } + } + + return THEFT_HOOK_TRIAL_POST_CONTINUE; +} + +static enum theft_hook_trial_pre_res +halt_once_flag_is_set(const struct theft_hook_trial_pre_info *info, + void *env) { + (void)info; + bool *has_1000_failure = (bool *)env; + return *has_1000_failure + ? THEFT_HOOK_TRIAL_PRE_HALT + : THEFT_HOOK_TRIAL_PRE_CONTINUE; +} + +/* For a trivially falsifiable property (for any uint64_t X, + * X is even and less than 1000), check that failure tagging + * can be used to keep shrinking following the X >= 1000 + * path. Without failure tagging, shrinking below 1000 + * and landing on an odd number would shadow the >= 1000 + * failure with the failure due to an odd number. */ +TEST failure_tagging_prevents_failure_shadowing(void) { + bool has_1000_failure = false; + + struct theft_run_config cfg = { + .name = __func__, + .prop1 = prop_lt_1000_and_even, + .type_info = { theft_get_builtin_type_info(THEFT_BUILTIN_uint64_t) }, + .trials = 1000, + .seed = theft_seed_of_time(), + .hooks = { + .trial_pre = halt_once_flag_is_set, + .trial_post = trial_post_check_failure_tag, + .env = (void *)&has_1000_failure, + }, + }; + + enum theft_run_res res = theft_run(&cfg); + ASSERT_ENUM_EQm("should fail", THEFT_RUN_FAIL, res, theft_run_res_str); + ASSERT(has_1000_failure); + PASS(); +} + SUITE(integration) { RUN_TEST(generated_unsigned_ints_are_positive); RUN_TEST(generated_int_list_with_cons_is_longer); @@ -1542,6 +1618,7 @@ SUITE(integration) { RUN_TEST(forking_privilege_drop_cpu_limit__slow); RUN_TEST(repeat_with_verbose_set_after_shrinking); + RUN_TEST(failure_tagging_prevents_failure_shadowing); // Regressions RUN_TEST(expected_seed_should_be_used_first);