From 9795351466582f35784593bc74ea54e2510d25ac Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Wed, 6 May 2020 12:30:28 +0100 Subject: [PATCH 1/3] Ensure for unwind-min 1, assertions are checked after the first unwind --- src/goto-checker/symex_bmc_incremental_one_loop.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/goto-checker/symex_bmc_incremental_one_loop.cpp b/src/goto-checker/symex_bmc_incremental_one_loop.cpp index f7a1f19b72f..fb2c2632718 100644 --- a/src/goto-checker/symex_bmc_incremental_one_loop.cpp +++ b/src/goto-checker/symex_bmc_incremental_one_loop.cpp @@ -37,8 +37,12 @@ symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt( : 0), output_ui(output_ui) { + // the intended behaviour is to stop asserts that are violated before the + // unwind + // therefore if the min-unwind is 1, then we do one unwind and immediately + // start checking for properties ignore_assertions = - incr_min_unwind >= 1 && + incr_min_unwind > 1 && options.get_bool_option("ignore-properties-before-unwind-min"); } From 75cf8033a5f236225088dac79b5ab45c39548a68 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Wed, 6 May 2020 12:31:49 +0100 Subject: [PATCH 2/3] Update min-unwind tests for behaviour of different unwind values It is agreed that if --unwind N can find an error, that unwind-min N should find the same error. That is, we start checking immediately after doing N unwinds, rather than after doing N increments of the incremental unwinding (i.e. unwind + solve) --- .../ignore-before-unwind/include_first_unwind0.desc | 12 ++++++++++++ .../ignore-before-unwind/include_first_unwind1.desc | 12 ++++++++++++ .../ignore-before-unwind/skip_first_unwind.desc | 2 +- 3 files changed, 25 insertions(+), 1 deletion(-) create mode 100644 regression/cbmc-incr-oneloop/ignore-before-unwind/include_first_unwind0.desc create mode 100644 regression/cbmc-incr-oneloop/ignore-before-unwind/include_first_unwind1.desc diff --git a/regression/cbmc-incr-oneloop/ignore-before-unwind/include_first_unwind0.desc b/regression/cbmc-incr-oneloop/ignore-before-unwind/include_first_unwind0.desc new file mode 100644 index 00000000000..af7ca070aa6 --- /dev/null +++ b/regression/cbmc-incr-oneloop/ignore-before-unwind/include_first_unwind0.desc @@ -0,0 +1,12 @@ +CORE +main.c +--ignore-properties-before-unwind-min --incremental-loop main.0 --unwind-max 2 --unwind-min 0 +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.\d+\] line \d+ property: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +-- +This test correctly fails because the first iteration of the loop violates the +property. diff --git a/regression/cbmc-incr-oneloop/ignore-before-unwind/include_first_unwind1.desc b/regression/cbmc-incr-oneloop/ignore-before-unwind/include_first_unwind1.desc new file mode 100644 index 00000000000..dafffcff2ef --- /dev/null +++ b/regression/cbmc-incr-oneloop/ignore-before-unwind/include_first_unwind1.desc @@ -0,0 +1,12 @@ +CORE +main.c +--ignore-properties-before-unwind-min --incremental-loop main.0 --unwind-max 2 --unwind-min 1 +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.\d+\] line \d+ property: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +-- +This test correctly fails because the first iteration of the loop violates the +property. diff --git a/regression/cbmc-incr-oneloop/ignore-before-unwind/skip_first_unwind.desc b/regression/cbmc-incr-oneloop/ignore-before-unwind/skip_first_unwind.desc index f20aaa7ec62..bcb9d3d8813 100644 --- a/regression/cbmc-incr-oneloop/ignore-before-unwind/skip_first_unwind.desc +++ b/regression/cbmc-incr-oneloop/ignore-before-unwind/skip_first_unwind.desc @@ -1,6 +1,6 @@ CORE main.c ---ignore-properties-before-unwind-min --incremental-loop main.0 --unwind-max 2 --unwind-min 1 +--ignore-properties-before-unwind-min --incremental-loop main.0 --unwind-max 2 --unwind-min 2 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ From 293d469a6e02297755b1591c36bdb6ad028599a7 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Wed, 6 May 2020 12:37:26 +0100 Subject: [PATCH 3/3] Update the help documention for min-unwind It was somewhat ambiguous whether the checking started after N unwinds, or after N incremental solves. This documentation clarifies the checking is enabled after the Nth unwind, before the Nth solve. --- src/goto-checker/bmc_util.h | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index a9d65be6c6f..bc16f6142da 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -221,6 +221,11 @@ void run_property_decider( " of loop L\n" \ " (use --show-loops to get the loop IDs)\n" \ " --unwind-min nr start incremental-loop after nr unwindings\n" \ + " but before solving that iteration. If for\n" \ + " example it is 1, then the loop will be\n" \ + " unwound once, and immediately checked.\n" \ + " Note: this means for min-unwind 1 or\n"\ + " 0 all properties are checked.\n" \ " --unwind-max nr stop incremental-loop after nr unwindings\n" \ " --ignore-properties-before-unwind-min\n" \ " do not check properties before unwind-min\n" \