From ee0d4f79c5d79d613c5ec0f25bb6d53793c69b29 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 3 Feb 2023 14:39:47 -0600 Subject: [PATCH 1/3] Fix typos in contracts.h --- src/goto-instrument/contracts/contracts.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index c2ed71071df..c21fe45d9b1 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -75,7 +75,7 @@ class code_contractst /// with an assertion that the `requires` clause holds followed by an /// assumption that the `ensures` clause holds. In order to ensure that `F` /// actually abides by its `ensures` and `requires` clauses, you should - /// separately call `code_constractst::enforce_contracts()` on `F` and verify + /// separately call `code_contractst::enforce_contracts()` on `F` and verify /// it using `cbmc --function F`. void replace_calls(const std::set &to_replace); @@ -159,7 +159,7 @@ class code_contractst std::unordered_map original_loop_number_map; - /// Loop havoc instructions instrumneted during applying loop contracts. + /// Loop havoc instructions instrumented during applying loop contracts. std::unordered_set loop_havoc_set; From 89df5e910a279ac3a803469fb8e2285e211474c3 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 7 Feb 2023 11:47:03 -0600 Subject: [PATCH 2/3] Add an option to not unwind tranformed loops after applying loop contracts --- doc/man/goto-instrument.1 | 3 +++ .../contracts/loop_contracts_no_unwind/main.c | 14 ++++++++++++++ .../contracts/loop_contracts_no_unwind/test.desc | 10 ++++++++++ src/goto-instrument/contracts/contracts.cpp | 11 +++++++---- src/goto-instrument/contracts/contracts.h | 8 ++++++++ .../goto_instrument_parse_options.cpp | 11 +++++++++++ .../goto_instrument_parse_options.h | 1 + 7 files changed, 54 insertions(+), 4 deletions(-) create mode 100644 regression/contracts/loop_contracts_no_unwind/main.c create mode 100644 regression/contracts/loop_contracts_no_unwind/test.desc diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1 index 567ca6bb0fd..d162b4d5ba3 100644 --- a/doc/man/goto-instrument.1 +++ b/doc/man/goto-instrument.1 @@ -999,6 +999,9 @@ force aggressive slicer to preserve all direct paths \fB\-\-apply\-loop\-contracts\fR check and use loop contracts when provided .TP +\fB\-loop\-contracts\-no\-unwind\fR +do not unwind transformed loops +.TP \fB\-\-replace\-call\-with\-contract\fR \fIfun\fR replace calls to \fIfun\fR with \fIfun\fR's contract .TP diff --git a/regression/contracts/loop_contracts_no_unwind/main.c b/regression/contracts/loop_contracts_no_unwind/main.c new file mode 100644 index 00000000000..bff5fa3c56d --- /dev/null +++ b/regression/contracts/loop_contracts_no_unwind/main.c @@ -0,0 +1,14 @@ +#include + +int main() +{ + int x = 0; + + while(x < 10) + __CPROVER_loop_invariant(0 <= x && x <= 10); + { + x++; + } + + assert(x == 10); +} diff --git a/regression/contracts/loop_contracts_no_unwind/test.desc b/regression/contracts/loop_contracts_no_unwind/test.desc new file mode 100644 index 00000000000..c28026b8702 --- /dev/null +++ b/regression/contracts/loop_contracts_no_unwind/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--apply-loop-contracts --loop-contracts-no-unwind _ --unwind 1 --unwinding-assertions +^EXIT=10$ +^SIGNAL=0$ +\[main.unwind.\d+\] line \d+ unwinding assertion loop 0: FAILURE +^VERIFICATION FAILED$ +-- +-- +Check that transformed loop will not be unwound with flag --loop-contracts-no-unwind. diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 3292778110c..c48e074aab9 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -1445,10 +1445,13 @@ void code_contractst::apply_loop_contracts( nondet_static(goto_model, to_exclude_from_nondet_init); // unwind all transformed loops twice. - unwindsett unwindset{goto_model}; - unwindset.parse_unwindset(loop_names, log.get_message_handler()); - goto_unwindt goto_unwind; - goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME); + if(unwind_transformed_loops) + { + unwindsett unwindset{goto_model}; + unwindset.parse_unwindset(loop_names, log.get_message_handler()); + goto_unwindt goto_unwind; + goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME); + } remove_skip(goto_model); diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index c21fe45d9b1..50cd1adb33f 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -35,6 +35,11 @@ Date: February 2016 " --apply-loop-contracts\n" \ " check and use loop contracts when provided\n" +#define FLAG_LOOP_CONTRACTS_NO_UNWIND "loop-contracts-no-unwind" +#define HELP_LOOP_CONTRACTS_NO_UNWIND \ + " --loop-contracts-no-unwind\n" \ + " do not unwind transformed loops\n" + #define FLAG_REPLACE_CALL "replace-call-with-contract" #define HELP_REPLACE_CALL \ " --replace-call-with-contract [/contract]\n" \ @@ -139,6 +144,9 @@ class code_contractst namespacet ns; + // Unwind transformed loops after applying loop contracts or not. + bool unwind_transformed_loops = true; + protected: goto_modelt &goto_model; symbol_tablet &symbol_table; diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 978476edac2..29e2919dd12 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1237,7 +1237,17 @@ void goto_instrument_parse_optionst::instrument_goto_program() contracts.enforce_contracts(to_enforce, to_exclude_from_nondet_static); if(cmdline.isset(FLAG_LOOP_CONTRACTS)) + { + if(cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND)) + { + contracts.unwind_transformed_loops = false; + log.warning() << "**** WARNING: transformed loops will not be unwound " + << "after applying loop contracts. Remember to unwind " + << "them at least twice to pass unwinding-assertions." + << messaget::eom; + } contracts.apply_loop_contracts(to_exclude_from_nondet_static); + } } if(cmdline.isset("value-set-fi-fp-removal")) @@ -1966,6 +1976,7 @@ void goto_instrument_parse_optionst::help() "Code contracts:\n" HELP_DFCC HELP_LOOP_CONTRACTS + HELP_LOOP_CONTRACTS_NO_UNWIND HELP_REPLACE_CALL HELP_ENFORCE_CONTRACT HELP_ENFORCE_CONTRACT_REC diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 785ea7450a8..4af09d83634 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -97,6 +97,7 @@ Author: Daniel Kroening, kroening@kroening.com "(horn)(skip-loops):(model-argc-argv):" \ OPT_DFCC \ "(" FLAG_LOOP_CONTRACTS ")" \ + "(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \ "(" FLAG_REPLACE_CALL "):" \ "(" FLAG_ENFORCE_CONTRACT "):" \ OPT_ENFORCE_CONTRACT_REC \ From e6e813727918db504af7453f0e0ce8de6de6cf1a Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 7 Feb 2023 11:48:17 -0600 Subject: [PATCH 3/3] Add an option in goto-synthesizer to not unwind tranformed loops --- doc/man/goto-synthesizer.1 | 3 +++ src/goto-synthesizer/cegis_verifier.cpp | 1 + src/goto-synthesizer/goto_synthesizer_parse_options.cpp | 3 +++ src/goto-synthesizer/goto_synthesizer_parse_options.h | 3 +++ 4 files changed, 10 insertions(+) diff --git a/doc/man/goto-synthesizer.1 b/doc/man/goto-synthesizer.1 index da4e654b03b..0c304850a0c 100644 --- a/doc/man/goto-synthesizer.1 +++ b/doc/man/goto-synthesizer.1 @@ -17,6 +17,9 @@ program transformation for the synthesized contracts, and then writes the resulting program as GOTO binary on disk. .SH OPTIONS .TP +\fB\-loop\-contracts\-no\-unwind\fR +Do not unwind transformed loops after applying the synthesized loop contracts. +.TP \fB\-\-dump\-loop\-contracts Dump the synthesized loop contracts as JSON. .TP diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp index 2ecd10b6c79..b6254c56861 100644 --- a/src/goto-synthesizer/cegis_verifier.cpp +++ b/src/goto-synthesizer/cegis_verifier.cpp @@ -610,6 +610,7 @@ optionalt cegis_verifiert::verify() // Apply loop contracts we annotated. code_contractst cont(goto_model, log); + cont.unwind_transformed_loops = false; cont.apply_loop_contracts(); original_loop_number_map = cont.get_original_loop_number_map(); loop_havoc_set = cont.get_loop_havoc_set(); diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp index ca84601e276..a53fdbee854 100644 --- a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp +++ b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp @@ -110,6 +110,8 @@ int goto_synthesizer_parse_optionst::doit() cmdline.get_values("nondet-static-exclude").begin(), cmdline.get_values("nondet-static-exclude").end()); code_contractst contracts(goto_model, log); + contracts.unwind_transformed_loops = + !cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND); contracts.apply_loop_contracts(to_exclude_from_nondet_static); // recalculate numbers, etc. @@ -183,6 +185,7 @@ void goto_synthesizer_parse_optionst::help() "\n" "Main options:\n" HELP_DUMP_LOOP_CONTRACTS + HELP_LOOP_CONTRACTS_NO_UNWIND "\n" "Other options:\n" " --version show version and exit\n" diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.h b/src/goto-synthesizer/goto_synthesizer_parse_options.h index fd29a7edf54..214b99263a2 100644 --- a/src/goto-synthesizer/goto_synthesizer_parse_options.h +++ b/src/goto-synthesizer/goto_synthesizer_parse_options.h @@ -13,11 +13,14 @@ Author: Qinheping Hu #include +#include + #include "dump_loop_contracts.h" // clang-format off #define GOTO_SYNTHESIZER_OPTIONS \ OPT_DUMP_LOOP_CONTRACTS \ + "(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \ "(verbosity):(version)(xml-ui)(json-ui)" \ // empty last line