From 25339d5e613306af9fa7b2ea560d0e7917828b85 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 25 Nov 2017 16:44:09 +0000 Subject: [PATCH] Add option not to transform self-loops into assumes This allows disabling an optimisation in goto-symex which is not compatible with termination checking. --- jbmc/src/jbmc/jbmc_parse_options.cpp | 5 +++++ regression/cbmc/self_loops_to_assumptions1/default.desc | 7 +++++++ regression/cbmc/self_loops_to_assumptions1/main.c | 8 ++++++++ regression/cbmc/self_loops_to_assumptions1/no-assume.desc | 7 +++++++ src/cbmc/bmc.h | 5 +++++ src/cbmc/cbmc_parse_options.cpp | 5 +++++ src/goto-symex/goto_symex.h | 2 ++ src/goto-symex/symex_goto.cpp | 8 +++++--- 8 files changed, 44 insertions(+), 3 deletions(-) create mode 100644 regression/cbmc/self_loops_to_assumptions1/default.desc create mode 100644 regression/cbmc/self_loops_to_assumptions1/main.c create mode 100644 regression/cbmc/self_loops_to_assumptions1/no-assume.desc diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index a498ab73879..18e8c39b142 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -152,6 +152,11 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) else options.set_option("propagation", true); + // transform self loops to assumptions + options.set_option( + "self-loops-to-assumptions", + !cmdline.isset("no-self-loops-to-assumptions")); + // all checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); diff --git a/regression/cbmc/self_loops_to_assumptions1/default.desc b/regression/cbmc/self_loops_to_assumptions1/default.desc new file mode 100644 index 00000000000..a7a038cf94d --- /dev/null +++ b/regression/cbmc/self_loops_to_assumptions1/default.desc @@ -0,0 +1,7 @@ +CORE +main.c +--unwind 1 --unwinding-assertions +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/cbmc/self_loops_to_assumptions1/main.c b/regression/cbmc/self_loops_to_assumptions1/main.c new file mode 100644 index 00000000000..2aefe91c35f --- /dev/null +++ b/regression/cbmc/self_loops_to_assumptions1/main.c @@ -0,0 +1,8 @@ +int main() +{ + while(1) + { + } + + return 0; +} diff --git a/regression/cbmc/self_loops_to_assumptions1/no-assume.desc b/regression/cbmc/self_loops_to_assumptions1/no-assume.desc new file mode 100644 index 00000000000..519dfddbd15 --- /dev/null +++ b/regression/cbmc/self_loops_to_assumptions1/no-assume.desc @@ -0,0 +1,7 @@ +CORE +main.c +--unwind 1 --unwinding-assertions --no-self-loops-to-assumptions +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index a61ba9e3e6c..d262fd22dcc 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -84,6 +84,8 @@ class bmct:public safety_checkert symex.constant_propagation=options.get_bool_option("propagation"); symex.record_coverage= !options.get_option("symex-coverage-report").empty(); + symex.self_loops_to_assumptions = + options.get_bool_option("self-loops-to-assumptions"); } virtual resultt run(const goto_functionst &goto_functions) @@ -292,6 +294,7 @@ class path_explorert : public bmct "(unwinding-assertions)" \ "(no-unwinding-assertions)" \ "(no-pretty-names)" \ + "(no-self-loops-to-assumptions)" \ "(partial-loops)" \ "(paths):" \ "(show-symex-strategies)" \ @@ -315,6 +318,8 @@ class path_explorert : public bmct " --unwinding-assertions generate unwinding assertions (cannot be\n" \ " used with --cover or --partial-loops)\n" \ " --partial-loops permit paths with partial loops\n" \ + " --no-self-loops-to-assumptions\n" \ + " do not simplify while(1){} to assume(0)\n" \ " --no-pretty-names do not simplify identifiers\n" \ " --graphml-witness filename write the witness in GraphML format to " \ "filename\n" // NOLINT(*) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index ec6fe1ee02e..9411a1b8c37 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -227,6 +227,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("no-propagation")) options.set_option("propagation", false); + // transform self loops to assumptions + options.set_option( + "self-loops-to-assumptions", + !cmdline.isset("no-self-loops-to-assumptions")); + // all checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 7c1389740b4..030337f855d 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -57,6 +57,7 @@ class goto_symext total_vccs(0), remaining_vccs(0), constant_propagation(true), + self_loops_to_assumptions(true), language_mode(), outer_symbol_table(outer_symbol_table), ns(outer_symbol_table), @@ -202,6 +203,7 @@ class goto_symext unsigned total_vccs, remaining_vccs; bool constant_propagation; + bool self_loops_to_assumptions; optionst options; diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 409de30c2c6..517b749e163 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -58,9 +58,11 @@ void goto_symext::symex_goto(statet &state) if(!forward) // backwards? { // is it label: goto label; or while(cond); - popular in SV-COMP - if(goto_target==state.source.pc || - (instruction.incoming_edges.size()==1 && - *instruction.incoming_edges.begin()==goto_target)) + if( + self_loops_to_assumptions && + (goto_target == state.source.pc || + (instruction.incoming_edges.size() == 1 && + *instruction.incoming_edges.begin() == goto_target))) { // generate assume(false) or a suitable negation if this // instruction is a conditional goto