From 69d0a18bd816f1204176a1bc983a883a2a9fe713 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lukas=20Gr=C3=A4tz?= Date: Thu, 8 May 2025 20:17:36 +0200 Subject: [PATCH 1/3] Feature to --retrace a single control flow path Adds a feature to retrace and verify a single control flow path. The path can be given using `--retrace` as a string of 0s and 1s. From a very brief evaluation test, it seems to be faster than bounded loop unwinding. Only that it might be challenging to find a path to retrace. The 0s and 1s in the input retrace string follow the goto decisions in cbmc's internal goto program representation. During symbolic execution, files and line numbers for each decision are logged to the console, so the interactive use should be intuitive. Co-authored-by: Yosephine Setiawan --- doc/man/cbmc.1 | 3 + doc/man/jbmc.1 | 3 + src/cbmc/cbmc_parse_options.cpp | 15 +++ src/goto-checker/bmc_util.cpp | 9 +- src/goto-checker/bmc_util.h | 3 + src/goto-symex/goto_symex.h | 3 + src/goto-symex/symex_config.h | 3 + src/goto-symex/symex_goto.cpp | 191 +++++++++++++++++++++++++++++++- src/goto-symex/symex_main.cpp | 6 +- 9 files changed, 232 insertions(+), 4 deletions(-) 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/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..ae57c424263 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")), @@ -641,7 +643,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); From 5719ed9aae0048ff933c1740192625a98c45373b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lukas=20Gr=C3=A4tz?= Date: Thu, 8 May 2025 20:18:48 +0200 Subject: [PATCH 2/3] Make clang-format happy I have not changed these lines but check-clang-format failed nonetheless. Thus, I added this extra commit. --- src/goto-symex/symex_main.cpp | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index ae57c424263..b3191d89b93 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -44,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")} From e99e11dfcb41c05d4175246cb2f10e0d6e87d430 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lukas=20Gr=C3=A4tz?= Date: Fri, 9 May 2025 15:54:02 +0200 Subject: [PATCH 3/3] Retracing test simple goto This adds one test file for the new --retrace feature. --- regression/book-examples/simple-goto/C00.desc | 6 ++++++ regression/book-examples/simple-goto/C01.desc | 6 ++++++ regression/book-examples/simple-goto/C10.desc | 6 ++++++ .../book-examples/simple-goto/simple_goto.c | 18 ++++++++++++++++++ 4 files changed, 36 insertions(+) create mode 100644 regression/book-examples/simple-goto/C00.desc create mode 100644 regression/book-examples/simple-goto/C01.desc create mode 100644 regression/book-examples/simple-goto/C10.desc create mode 100644 regression/book-examples/simple-goto/simple_goto.c 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); +}