diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index edf0502fd85..b7a21500f46 100644 --- a/doc/man/cbmc.1 +++ b/doc/man/cbmc.1 @@ -366,6 +366,9 @@ explore paths one at a time \fB\-\-show\-symex\-strategies\fR list strategies for use with \fB\-\-paths\fR .TP +\fB\-\-retrace\fR [trace] +follow a single control flow path, given by a trace string of 0s and 1s +.TP \fB\-\-show\-goto\-symex\-steps\fR show which steps symex travels, includes diagnostic information diff --git a/doc/man/jbmc.1 b/doc/man/jbmc.1 index 24ca6ceccb0..00460fa1e7e 100644 --- a/doc/man/jbmc.1 +++ b/doc/man/jbmc.1 @@ -281,6 +281,9 @@ explore paths one at a time \fB\-\-show\-symex\-strategies\fR list strategies for use with \fB\-\-paths\fR .TP +\fB\-\-retrace\fR [trace] +follow a single control flow path, given by a trace string of 0s and 1s +.TP \fB\-\-show\-goto\-symex\-steps\fR show which steps symex travels, includes diagnostic information diff --git a/regression/book-examples/simple-goto/C00.desc b/regression/book-examples/simple-goto/C00.desc new file mode 100644 index 00000000000..952a8d2487e --- /dev/null +++ b/regression/book-examples/simple-goto/C00.desc @@ -0,0 +1,6 @@ +CORE +simple_goto.c +--function foo --retrace 00 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/regression/book-examples/simple-goto/C01.desc b/regression/book-examples/simple-goto/C01.desc new file mode 100644 index 00000000000..8ab787babde --- /dev/null +++ b/regression/book-examples/simple-goto/C01.desc @@ -0,0 +1,6 @@ +CORE +simple_goto.c +--function foo --retrace 01 +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ diff --git a/regression/book-examples/simple-goto/C10.desc b/regression/book-examples/simple-goto/C10.desc new file mode 100644 index 00000000000..3614c4ae12c --- /dev/null +++ b/regression/book-examples/simple-goto/C10.desc @@ -0,0 +1,6 @@ +CORE +simple_goto.c +--function foo --retrace 10 +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ diff --git a/regression/book-examples/simple-goto/simple_goto.c b/regression/book-examples/simple-goto/simple_goto.c new file mode 100644 index 00000000000..5dd3694c8cc --- /dev/null +++ b/regression/book-examples/simple-goto/simple_goto.c @@ -0,0 +1,18 @@ +#include +#include + +void foo(bool arg1, bool arg2) +{ + bool v1 = false; + bool v2 = false; + if(arg1) + goto l1; + v1 = true; +l1: + if(arg2) + goto l2; + v2 = true; +l2: + assert(v1); + assert(v2); +} diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 6548067d791..5951fc8b2e8 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -168,6 +168,21 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) exit(CPROVER_EXIT_USAGE_ERROR); } + if(cmdline.isset("retrace")) + { + auto retrace_input = cmdline.get_value("retrace"); + options.set_option("retrace", retrace_input); + + // check retrace input + for(auto &c : retrace_input) + if(c != '0' && c != '1') + { + log.error() << "--retrace input string must only contain 0s and 1s" + << messaget::eom; + exit(CPROVER_EXIT_USAGE_ERROR); + } + } + // We want to warn the user that if we are using standard checks (that enables // unwinding-assertions) and we did not disable them manually. if( diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index 6e31d312d77..963b99d5951 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -186,7 +186,14 @@ void setup_symex( if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol)) symex.language_mode = init_symbol->mode; - msg.status() << "Starting Bounded Model Checking" << messaget::eom; + if(options.is_set("retrace")) + { + msg.status() << "Starting Retrace Model Checking" << messaget::eom; + } + else + { + msg.status() << "Starting Bounded Model Checking" << messaget::eom; + } symex.last_source_location.make_nil(); diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index 92e0e3a82de..16d8a298755 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -182,6 +182,7 @@ void run_property_decider( "(partial-loops)" \ "(paths):" \ "(show-symex-strategies)" \ + "(retrace):" \ "(depth):" \ "(max-field-sensitivity-array-size):" \ "(no-array-field-sensitivity)" \ @@ -197,6 +198,8 @@ void run_property_decider( #define HELP_BMC \ " {y--paths} [strategy] \t explore paths one at a time\n" \ " {y--show-symex-strategies} \t list strategies for use with {y--paths}\n" \ + " {y--retrace} [trace] \t follow a single control flow path, given by a " \ + "trace string of 0s and 1s\n" \ " {y--show-goto-symex-steps} \t show which steps symex travels, includes " \ "diagnostic information\n" \ " {y--show-points-to-sets} \t show points-to sets for pointer dereference. " \ diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index ae06ad54072..71710bed986 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -318,6 +318,9 @@ class goto_symext /// Symbolically execute a GOTO instruction in the context of unreachable code /// \param state: Symbolic execution state for current instruction void symex_unreachable_goto(statet &state); + /// Symbolically execute a GOTO along a control flow retrace input path + /// \param state: Symbolic execution state for current instruction + void symex_goto_retrace(statet &state); /// Symbolically execute a SET_RETURN_VALUE instruction /// \param state: Symbolic execution state for current instruction /// \param return_value: The value to be returned diff --git a/src/goto-symex/symex_config.h b/src/goto-symex/symex_config.h index d9f65c46568..4d1aa5355a1 100644 --- a/src/goto-symex/symex_config.h +++ b/src/goto-symex/symex_config.h @@ -24,6 +24,9 @@ struct symex_configt final bool doing_path_exploration; + bool retracing; + std::string retrace_input; + bool allow_pointer_unsoundness; bool constant_propagation; diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 8dcd92c6078..2cb32102aa7 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -260,8 +260,7 @@ void goto_symext::symex_goto(statet &state) DATA_INVARIANT( instruction.targets.size() == 1, "no support for non-deterministic gotos"); - goto_programt::const_targett goto_target= - instruction.get_target(); + goto_programt::const_targett goto_target = instruction.get_target(); const bool backward = instruction.is_backwards_goto(); @@ -614,6 +613,194 @@ void goto_symext::symex_unreachable_goto(statet &state) symex_transition(state); } +void goto_symext::symex_goto_retrace(statet &state) +{ + // get guard, targets as in symex_goto() + const goto_programt::instructiont &instruction = *state.source.pc; + + exprt new_guard = clean_expr(instruction.condition(), state, false); + + renamedt renamed_guard = state.rename(std::move(new_guard), ns); + renamed_guard = try_evaluate_pointer_comparisons( + std::move(renamed_guard), state.value_set, language_mode, ns); + if(symex_config.simplify_opt) + renamed_guard.simplify(ns); + new_guard = renamed_guard.get(); + + target.goto_instruction(state.guard.as_expr(), renamed_guard, state.source); + + DATA_INVARIANT( + !instruction.targets.empty(), "goto should have at least one target"); + + // we only do deterministic gotos for now + DATA_INVARIANT( + instruction.targets.size() == 1, "no support for non-deterministic gotos"); + + goto_programt::const_targett goto_target = instruction.get_target(); + + const bool backward = instruction.is_backwards_goto(); + + goto_programt::const_targett next_instruction = state.source.pc; + next_instruction++; + + // goto or next depends on input trace from user + bool choose_goto; + static size_t retrace_index = 0; + if(retrace_index < symex_config.retrace_input.size()) + { + choose_goto = symex_config.retrace_input[retrace_index] == '1'; + } + else + { + choose_goto = false; + } + retrace_index++; + + // print goto choice + log.conditional_output( + log.status(), + [this, &state, &goto_target, &next_instruction, choose_goto]( + messaget::mstreamt &mstream) + { + source_locationt cur = state.source.pc->source_location(); + source_locationt goto_dest = goto_target->source_location(); + source_locationt next_dest = next_instruction->source_location(); + source_locationt t_dest = choose_goto ? goto_dest : next_dest; + source_locationt nt_dest = choose_goto ? next_dest : goto_dest; + + auto cur_file = cur.get_file(); + if(cur_file.empty()) + cur_file = ""; + auto t_file = t_dest.get_file(); + if(t_file.empty()) + t_file = ""; + auto nt_file = nt_dest.get_file(); + if(nt_file.empty()) + nt_file = ""; + + // print nothing when files are the same + if(cur_file == t_file) + t_file = ""; + if(cur_file == nt_file) + nt_file = ""; + + auto cur_line = cur.get_line(); + if(cur_line.empty()) + cur_line = "?"; + auto t_line = t_dest.get_line(); + if(t_line.empty()) + t_line = "?"; + auto nt_line = nt_dest.get_line(); + if(nt_line.empty()) + nt_line = "?"; + + std::string head = symex_config.retrace_input; + // add 0s in case input trace was shorter + head.resize(retrace_index - 1, '0'); + std::string decision = choose_goto ? "1" : "0"; + + std::string step = choose_goto ? " goto " : " next "; + + std::string padding_1 = + cur_line.size() < 3 ? std::string(3 - cur_line.size(), ' ') : ""; + std::string padding_2 = + t_line.size() < 3 ? std::string(3 - t_line.size(), ' ') : ""; + + mstream << "Retrace " << head << messaget::bold << decision + << messaget::reset << " at " << cur_file << ":" << cur_line + << padding_1 << step << t_file << ":" << t_line << padding_2 + << " (not " << nt_file << ":" << nt_line << ")" << messaget::eom; + }); + + // warn when not following unconditional goto + if(new_guard.is_true() && !choose_goto) + { + log.result() << "Retrace input " << messaget::red << "inconsistent" + << messaget::reset << ": 0/next although guard is true!" + << log.eom; + should_pause_symex = true; + } + else if(new_guard.is_false() && choose_goto) + { + log.result() << "Retrace input " << messaget::red << "inconsistent" + << messaget::reset << ": 1/goto although guard is false!" + << log.eom; + should_pause_symex = true; + } + + symex_targett::sourcet original_source = state.source; + goto_programt::const_targett new_state_pc; + + if(choose_goto) + { + // Jump to the jump target if the input is '1' + new_state_pc = goto_target; + symex_transition(state, new_state_pc, backward); + } + else + { + // Jump to the next instruction + new_state_pc = state.source.pc; + new_state_pc++; + symex_transition(state); + } + + // produce new guard symbol + exprt guard_expr; + + if( + new_guard.id() == ID_symbol || + (new_guard.id() == ID_not && to_not_expr(new_guard).op().id() == ID_symbol)) + { + guard_expr = new_guard; + } + else + { + symbol_exprt guard_symbol_expr = + symbol_exprt(statet::guard_identifier(), bool_typet()); + exprt new_rhs = boolean_negate(new_guard); + + ssa_exprt new_lhs = + state.rename_ssa(ssa_exprt{guard_symbol_expr}, ns).get(); + new_lhs = + state.assignment(std::move(new_lhs), new_rhs, ns, true, false).get(); + + guardt guard{true_exprt{}, guard_manager}; + + log.conditional_output( + log.debug(), + [this, &new_lhs](messaget::mstreamt &mstream) + { + mstream << "Assignment to " << new_lhs.get_identifier() << " [" + << pointer_offset_bits(new_lhs.type(), ns).value_or(0) + << " bits]" << messaget::eom; + }); + + target.assignment( + guard.as_expr(), + new_lhs, + new_lhs, + guard_symbol_expr, + new_rhs, + original_source, + symex_targett::assignment_typet::GUARD); + + guard_expr = state.rename(boolean_negate(guard_symbol_expr), ns).get(); + } + + if(choose_goto) + { + symex_assume_l2(state, guard_expr); + state.guard.add(guard_expr); + } + else + { + symex_assume_l2(state, boolean_negate(guard_expr)); + state.guard.add(boolean_negate(guard_expr)); + } + return; +} + bool goto_symext::check_break(const irep_idt &loop_id, unsigned unwind) { // dummy implementation diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index de1e7f1f388..b3191d89b93 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -30,6 +30,8 @@ Author: Daniel Kroening, kroening@kroening.com symex_configt::symex_configt(const optionst &options) : max_depth(options.get_unsigned_int_option("depth")), doing_path_exploration(options.is_set("paths")), + retracing(options.is_set("retrace")), + retrace_input(options.get_option("retrace")), allow_pointer_unsoundness( options.get_bool_option("allow-pointer-unsoundness")), constant_propagation(options.get_bool_option("propagation")), @@ -42,12 +44,10 @@ symex_configt::symex_configt(const optionst &options) show_symex_steps(options.get_bool_option("show-goto-symex-steps")), show_points_to_sets(options.get_bool_option("show-points-to-sets")), max_field_sensitivity_array_size( - options.is_set("no-array-field-sensitivity") - ? 0 - : options.is_set("max-field-sensitivity-array-size") - ? options.get_unsigned_int_option( - "max-field-sensitivity-array-size") - : DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE), + options.is_set("no-array-field-sensitivity") ? 0 + : options.is_set("max-field-sensitivity-array-size") + ? options.get_unsigned_int_option("max-field-sensitivity-array-size") + : DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE), complexity_limits_active( options.get_signed_int_option("symex-complexity-limit") > 0), cache_dereferences{options.get_bool_option("symex-cache-dereferences")} @@ -641,7 +641,9 @@ void goto_symext::execute_next_instruction( break; case GOTO: - if(state.reachable) + if(symex_config.retracing) + symex_goto_retrace(state); + else if(state.reachable) symex_goto(state); else symex_unreachable_goto(state);