From 45233d2d27ab90cfdd005d3d9434f635aec455e0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 7 Mar 2026 10:13:52 +0000 Subject: [PATCH 01/13] Fix reference to temporary that has gone out of scope Although the temporary is bound by a const reference, that reference is then just passed on to subobject initialisers. Per https://en.cppreference.com/w/cpp/language/reference_initialization.html#Lifetime_of_a_temporary, "passing on" does not extend the lifetime of a temporary. Co-authored-by: Kiro --- unit/goto-symex/goto_symex_state.cpp | 3 ++- unit/goto-symex/symex_assign.cpp | 5 +++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/unit/goto-symex/goto_symex_state.cpp b/unit/goto-symex/goto_symex_state.cpp index 9042248686e..35431145d48 100644 --- a/unit/goto-symex/goto_symex_state.cpp +++ b/unit/goto-symex/goto_symex_state.cpp @@ -38,11 +38,12 @@ SCENARIO( auto fresh_name = [&fresh_name_count](const irep_idt &) { return fresh_name_count++; }; + const irep_idt empty_language_mode; goto_symex_statet state{ source, DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE, true, - irep_idt{}, + empty_language_mode, manager, fresh_name}; diff --git a/unit/goto-symex/symex_assign.cpp b/unit/goto-symex/symex_assign.cpp index 3464c3ba7c2..c7785e0e693 100644 --- a/unit/goto-symex/symex_assign.cpp +++ b/unit/goto-symex/symex_assign.cpp @@ -48,11 +48,12 @@ SCENARIO( auto fresh_name = [&fresh_name_count](const irep_idt &) { return fresh_name_count++; }; + const irep_idt empty_language_mode; goto_symex_statet state{ source, DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE, true, - irep_idt{}, + empty_language_mode, manager, fresh_name}; @@ -234,7 +235,7 @@ SCENARIO( symex_targett::assignment_typet::STATE, ns, symex_config, - irep_idt{}, + empty_language_mode, target_equation} .assign_symbol(struct1_ssa, skeleton, rhs, guard); THEN("Two equations are added to the target") From 99642da02099f382c3b270b25f4088d41e20ae12 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 1 Dec 2025 19:04:03 +0000 Subject: [PATCH 02/13] Initialise all POD members of goto_symex_statet The constructor did not take care of them and our unit tests exposed that, at least within unit tests, we were accessing uninitialised members. --- src/goto-symex/goto_symex_state.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 96020d5970e..50a507cf1ac 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -68,7 +68,7 @@ class goto_symex_statet final : public goto_statet // Manager is required to be able to resize the thread vector guard_managert &guard_manager; - symex_target_equationt *symex_target; + symex_target_equationt *symex_target = nullptr; symex_level1t level1; @@ -217,14 +217,14 @@ class goto_symex_statet final : public goto_statet goto_programt::const_targett saved_target; /// \brief This state is saved, with the PC pointing to the target of a GOTO - bool has_saved_jump_target; + bool has_saved_jump_target = false; /// \brief This state is saved, with the PC pointing to the next instruction /// of a GOTO - bool has_saved_next_instruction; + bool has_saved_next_instruction = false; /// \brief Should the additional validation checks be run? - bool run_validation_checks; + bool run_validation_checks = false; unsigned total_vccs = 0; unsigned remaining_vccs = 0; From f0da0681ce23eec0c6ab5a52eedc3bc68a51094a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 30 Nov 2025 12:50:49 +0000 Subject: [PATCH 03/13] Do not use value-set supported simplification with multiple threads Shared pointers may be updated in yet-to-be-executed threads. --- src/goto-symex/goto_symex.cpp | 13 ++++++++++--- src/goto-symex/goto_symex.h | 2 +- src/goto-symex/symex_atomic_section.cpp | 4 ++-- src/goto-symex/symex_builtin_functions.cpp | 8 ++++---- src/goto-symex/symex_clean_expr.cpp | 4 ++-- src/goto-symex/symex_dereference.cpp | 8 ++++---- src/goto-symex/symex_goto.cpp | 2 +- src/goto-symex/symex_main.cpp | 10 +++++----- src/goto-symex/symex_other.cpp | 6 +++--- 9 files changed, 32 insertions(+), 25 deletions(-) diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index 24d9e4dc33b..0c0efb5106a 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -29,11 +30,17 @@ Author: Daniel Kroening, kroening@kroening.com #include -void goto_symext::do_simplify(exprt &expr, const value_sett &value_set) +void goto_symext::do_simplify(exprt &expr, const statet &state) { if(symex_config.simplify_opt) { - simplify_expr_with_value_sett{value_set, language_mode, ns}.simplify(expr); + if(state.threads.size() == 1) + { + simplify_expr_with_value_sett{state.value_set, language_mode, ns} + .simplify(expr); + } + else + simplify(expr, ns); } } @@ -63,7 +70,7 @@ void goto_symext::symex_assign( // "byte_extract from an_lvalue offset this_rvalue") can affect whether // we use field-sensitive symbols or not, so L2-rename them up front: lhs = state.l2_rename_rvalues(lhs, ns); - do_simplify(lhs, state.value_set); + do_simplify(lhs, state); lhs = state.field_sensitivity.apply(ns, state, std::move(lhs), true); if(rhs.id() == ID_side_effect) diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 5980573f0cd..2c36ef7e14c 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -526,7 +526,7 @@ class goto_symext /// \param state: Symbolic execution state for current instruction void symex_catch(statet &state); - virtual void do_simplify(exprt &expr, const value_sett &value_set); + virtual void do_simplify(exprt &expr, const statet &state); /// Symbolically execute an ASSIGN instruction or simulate such an execution /// for a synthetic assignment diff --git a/src/goto-symex/symex_atomic_section.cpp b/src/goto-symex/symex_atomic_section.cpp index 231c40303e7..45ee547abb6 100644 --- a/src/goto-symex/symex_atomic_section.cpp +++ b/src/goto-symex/symex_atomic_section.cpp @@ -58,7 +58,7 @@ void goto_symext::symex_atomic_end(statet &state) ++it) read_guard|=*it; exprt read_guard_expr=read_guard.as_expr(); - do_simplify(read_guard_expr, state.value_set); + do_simplify(read_guard_expr, state); target.shared_read( read_guard_expr, @@ -80,7 +80,7 @@ void goto_symext::symex_atomic_end(statet &state) ++it) write_guard|=*it; exprt write_guard_expr=write_guard.as_expr(); - do_simplify(write_guard_expr, state.value_set); + do_simplify(write_guard_expr, state); target.shared_write( write_guard_expr, diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 0ffc7b606f6..c31bc0eab4d 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -293,7 +293,7 @@ void goto_symext::symex_va_start( array = clean_expr(std::move(array), state, false); array = state.rename(std::move(array), ns).get(); - do_simplify(array, state.value_set); + do_simplify(array, state); symex_assign(state, va_array.symbol_expr(), std::move(array)); exprt rhs = address_of_exprt{index_exprt{ @@ -388,7 +388,7 @@ void goto_symext::symex_printf( exprt tmp_rhs = rhs; clean_expr(tmp_rhs, state, false); tmp_rhs = state.rename(std::move(tmp_rhs), ns).get(); - do_simplify(tmp_rhs, state.value_set); + do_simplify(tmp_rhs, state); const exprt::operandst &operands=tmp_rhs.operands(); std::list args; @@ -426,7 +426,7 @@ void goto_symext::symex_printf( parameter = to_address_of_expr(parameter).object(); clean_expr(parameter, state, false); parameter = state.rename(std::move(parameter), ns).get(); - do_simplify(parameter, state.value_set); + do_simplify(parameter, state); args.push_back(std::move(parameter)); } @@ -454,7 +454,7 @@ void goto_symext::symex_input( for(std::size_t i=1; i(tmp1, ns).get(); - do_simplify(tmp1, state.value_set); + do_simplify(tmp1, state); if(symex_config.run_validation_checks) { @@ -515,7 +515,7 @@ void goto_symext::dereference(exprt &expr, statet &state, bool write) // when all we need is // s1 := s1 with (member := X) [and guard b] // s2 := s2 with (member := X) [and guard !b] - do_simplify(expr, state.value_set); + do_simplify(expr, state); if(symex_config.run_validation_checks) { diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index b61e48f36a5..2f9dcddf728 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -119,7 +119,7 @@ void goto_symext::symex_goto(statet &state) // generate assume(false) or a suitable negation if this // instruction is a conditional goto exprt negated_guard = boolean_negate(new_guard); - do_simplify(negated_guard, state.value_set); + do_simplify(negated_guard, state); log.statistics() << "replacing self-loop at " << state.source.pc->source_location() << " by assume(" << from_expr(ns, state.source.function_id, negated_guard) diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index a6ca641f16e..fe4e59497f9 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -157,7 +157,7 @@ void goto_symext::symex_assert( // First, push negations in and perhaps convert existential quantifiers into // universals: if(has_subexpr(condition, ID_exists) || has_subexpr(condition, ID_forall)) - do_simplify(condition, state.value_set); + do_simplify(condition, state); // Second, L2-rename universal quantifiers: if(has_subexpr(condition, ID_forall)) @@ -167,7 +167,7 @@ void goto_symext::symex_assert( exprt l2_condition = state.rename(std::move(condition), ns).get(); // now try simplifier on it - do_simplify(l2_condition, state.value_set); + do_simplify(l2_condition, state); std::string msg = id2string(instruction.source_location().get_comment()); if(msg.empty()) @@ -200,7 +200,7 @@ void goto_symext::symex_assume(statet &state, const exprt &cond) { exprt simplified_cond = clean_expr(cond, state, false); simplified_cond = state.rename(std::move(simplified_cond), ns).get(); - do_simplify(simplified_cond, state.value_set); + do_simplify(simplified_cond, state); // It would be better to call try_filter_value_sets after apply_condition, // but it is not currently possible. See the comment at the beginning of @@ -848,13 +848,13 @@ void goto_symext::try_filter_value_sets( // without another round of constant propagation. // It would be sufficient to replace this call to do_simplify() with // something that just replaces `*&x` with `x` whenever it finds it. - do_simplify(modified_condition, state.value_set); + do_simplify(modified_condition, state); state.record_events.push(false); modified_condition = state.rename(std::move(modified_condition), ns).get(); state.record_events.pop(); - do_simplify(modified_condition, state.value_set); + do_simplify(modified_condition, state); if(jump_taken_value_set && modified_condition == false) { diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp index c5e046356bf..ee55abf9273 100644 --- a/src/goto-symex/symex_other.cpp +++ b/src/goto-symex/symex_other.cpp @@ -151,14 +151,14 @@ void goto_symext::symex_other( { src_array = make_byte_extract( src_array, from_integer(0, c_index_type()), dest_array.type()); - do_simplify(src_array, state.value_set); + do_simplify(src_array, state); } else { // ID_array_replace dest_array = make_byte_extract( dest_array, from_integer(0, c_index_type()), src_array.type()); - do_simplify(dest_array, state.value_set); + do_simplify(dest_array, state); } } @@ -197,7 +197,7 @@ void goto_symext::symex_other( { auto array_size = size_of_expr(array_expr.type(), ns); CHECK_RETURN(array_size.has_value()); - do_simplify(array_size.value(), state.value_set); + do_simplify(array_size.value(), state); array_expr = make_byte_extract( array_expr, from_integer(0, c_index_type()), From dde808bcc3833fc44a49e2100cdcba0261ef230a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 2 Dec 2025 01:03:26 +0000 Subject: [PATCH 04/13] Remove language_mode from goto_symext `goto_symex_statet` holds a reference to a language mode, which was being initialised to `goto_symext::language_mode` in `goto_symext::initialize_entry_point_state`. That `goto_symext` object, however, may be the one created in `single_path_symex_only_checkert::initialize_worklist`, whereupon the `goto_symex_statet` will outlive it. Fix this problem by getting rid of the `language_mode` member of `goto_symext` and initialise `goto_symex_statet::language_mode` from a mode in the symbol table, which outlives all goto-symex objects. --- src/goto-checker/symex_bmc.cpp | 6 ------ src/goto-symex/goto_symex.cpp | 18 +++--------------- src/goto-symex/goto_symex.h | 4 ---- src/goto-symex/goto_symex_state.h | 5 ++++- src/goto-symex/symex_assign.cpp | 4 ++-- src/goto-symex/symex_assign.h | 3 --- src/goto-symex/symex_builtin_functions.cpp | 17 +++++++++-------- src/goto-symex/symex_clean_expr.cpp | 3 +-- src/goto-symex/symex_dereference.cpp | 5 ++--- src/goto-symex/symex_function_call.cpp | 8 +------- src/goto-symex/symex_goto.cpp | 3 ++- src/goto-symex/symex_main.cpp | 4 ++-- src/goto-symex/symex_start_thread.cpp | 2 -- unit/goto-symex/symex_assign.cpp | 3 --- 14 files changed, 26 insertions(+), 59 deletions(-) diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp index cd99776aea2..2a5b3d9a0ea 100644 --- a/src/goto-checker/symex_bmc.cpp +++ b/src/goto-checker/symex_bmc.cpp @@ -16,8 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - #include symex_bmct::symex_bmct( @@ -40,10 +38,6 @@ symex_bmct::symex_bmct( unwindset(unwindset), symex_coverage(ns) { - const symbolt *init_symbol = outer_symbol_table.lookup(INITIALIZE_FUNCTION); - if(init_symbol) - language_mode = init_symbol->mode; - messaget msg{mh}; msg.status() << "Starting Bounded Model Checking" << messaget::eom; } diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index 0c0efb5106a..3bbbd2bfb41 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -36,7 +36,7 @@ void goto_symext::do_simplify(exprt &expr, const statet &state) { if(state.threads.size() == 1) { - simplify_expr_with_value_sett{state.value_set, language_mode, ns} + simplify_expr_with_value_sett{state.value_set, state.language_mode, ns} .simplify(expr); } else @@ -113,13 +113,7 @@ void goto_symext::symex_assign( assignment_type = symex_targett::assignment_typet::HIDDEN; symex_assignt symex_assign{ - shadow_memory, - state, - assignment_type, - ns, - symex_config, - language_mode, - target}; + shadow_memory, state, assignment_type, ns, symex_config, target}; // Try to constant propagate potential side effects of the assignment, when // simplification is turned on and there is one thread only. Constant @@ -149,13 +143,7 @@ void goto_symext::symex_assign( exprt::operandst lhs_if_then_else_conditions; symex_assignt{ - shadow_memory, - state, - assignment_type, - ns, - symex_config, - language_mode, - target} + shadow_memory, state, assignment_type, ns, symex_config, target} .assign_rec(lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions); if(need_atomic_section) diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 2c36ef7e14c..fc2d7525b1b 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -235,10 +235,6 @@ class goto_symext messaget::mstreamt & print_callstack_entry(const symex_targett::sourcet &target); - /// language_mode: ID_java, ID_C or another language identifier - /// if we know the source language in use, irep_idt() otherwise. - irep_idt language_mode; - /// The symbol table associated with the goto-program being executed. /// This symbol table will not have objects that are dynamically created as /// part of symbolic execution added to it; those object are stored in the diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 50a507cf1ac..769b16ccec1 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -258,8 +258,11 @@ class goto_symex_statet final : public goto_statet lvalue.id() == ID_array; } -private: + /// language_mode: ID_java, ID_C or another language identifier + /// if we know the source language in use, irep_idt() otherwise. const irep_idt &language_mode; + +private: std::function fresh_l2_name_provider; /// \brief Dangerous, do not use diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 15fd2358236..e685faf2670 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -207,8 +207,8 @@ void symex_assignt::assign_non_struct_symbol( if(symex_config.simplify_opt) { - simplify_expr_with_value_sett{state.value_set, language_mode, ns}.simplify( - assignment.rhs); + simplify_expr_with_value_sett{state.value_set, state.language_mode, ns} + .simplify(assignment.rhs); } const ssa_exprt l2_lhs = state diff --git a/src/goto-symex/symex_assign.h b/src/goto-symex/symex_assign.h index e6a282637d7..2d8fa1611a7 100644 --- a/src/goto-symex/symex_assign.h +++ b/src/goto-symex/symex_assign.h @@ -33,14 +33,12 @@ class symex_assignt symex_targett::assignment_typet assignment_type, const namespacet &ns, const symex_configt &symex_config, - const irep_idt &language_mode, symex_targett &target) : shadow_memory(shadow_memory), state(state), assignment_type(assignment_type), ns(ns), symex_config(symex_config), - language_mode(language_mode), target(target) { } @@ -67,7 +65,6 @@ class symex_assignt symex_targett::assignment_typet assignment_type; const namespacet &ns; const symex_configt &symex_config; - const irep_idt &language_mode; symex_targett ⌖ void assign_from_struct( diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index c31bc0eab4d..5e80be6d485 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -72,8 +72,8 @@ void goto_symext::symex_allocate( { // to allow constant propagation exprt tmp_size = state.rename(size, ns).get(); - simplify_expr_with_value_sett{state.value_set, language_mode, ns}.simplify( - tmp_size); + simplify_expr_with_value_sett{state.value_set, state.language_mode, ns} + .simplify(tmp_size); // special treatment for sizeof(T)*x { @@ -167,8 +167,8 @@ void goto_symext::symex_allocate( // to allow constant propagation exprt zero_init = state.rename(to_binary_expr(code).op1(), ns).get(); - simplify_expr_with_value_sett{state.value_set, language_mode, ns}.simplify( - zero_init); + simplify_expr_with_value_sett{state.value_set, state.language_mode, ns} + .simplify(zero_init); INVARIANT( zero_init.is_constant(), "allocate expects constant as second argument"); @@ -433,7 +433,7 @@ void goto_symext::symex_printf( } const irep_idt format_string = - get_string_argument(operands[0], state.value_set, language_mode, ns); + get_string_argument(operands[0], state.value_set, state.language_mode, ns); if(!format_string.empty()) target.output_fmt( @@ -459,7 +459,7 @@ void goto_symext::symex_input( } const irep_idt input_id = - get_string_argument(id_arg, state.value_set, language_mode, ns); + get_string_argument(id_arg, state.value_set, state.language_mode, ns); target.input(state.guard.as_expr(), state.source, input_id, args); } @@ -478,14 +478,15 @@ void goto_symext::symex_output( renamedt l2_arg = state.rename(code.operands()[i], ns); if(symex_config.simplify_opt) { - simplify_expr_with_value_sett simp{state.value_set, language_mode, ns}; + simplify_expr_with_value_sett simp{ + state.value_set, state.language_mode, ns}; l2_arg.simplify(simp); } args.emplace_back(l2_arg); } const irep_idt output_id = - get_string_argument(id_arg, state.value_set, language_mode, ns); + get_string_argument(id_arg, state.value_set, state.language_mode, ns); target.output(state.guard.as_expr(), state.source, output_id, args); } diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp index a650d97b707..b8a8d4180a7 100644 --- a/src/goto-symex/symex_clean_expr.cpp +++ b/src/goto-symex/symex_clean_expr.cpp @@ -127,7 +127,7 @@ void goto_symext::process_array_expr(statet &state, exprt &expr) ns, state.symbol_table, symex_dereference_state, - language_mode, + state.language_mode, false, log.get_message_handler()); @@ -187,7 +187,6 @@ void goto_symext::lift_let(statet &state, const let_exprt &let_expr) symex_targett::assignment_typet::HIDDEN, ns, symex_config, - language_mode, target} .assign_symbol( to_ssa_expr(state.rename(let_expr.symbol(), ns).get()), diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index 69ff860f555..9f53513d2a9 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -220,7 +220,7 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state) "symex", "dereference_cache", dereference_result.source_location(), - language_mode, + state.language_mode, ns, state.symbol_table) .symbol_expr(); @@ -236,7 +236,6 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state) symex_targett::assignment_typet::STATE, ns, symex_config, - language_mode, target}; assign.assign_symbol( @@ -328,7 +327,7 @@ void goto_symext::dereference_rec( ns, state.symbol_table, symex_dereference_state, - language_mode, + state.language_mode, expr_is_not_null, log.get_message_handler()); diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index db4bfa133bc..6fdf9f4ff5e 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -131,13 +131,7 @@ void goto_symext::parameter_assignments( exprt::operandst lhs_conditions; symex_assignt{ - shadow_memory, - state, - assignment_type, - ns, - symex_config, - language_mode, - target} + shadow_memory, state, assignment_type, ns, symex_config, target} .assign_rec(lhs, expr_skeletont{}, rhs, lhs_conditions); } diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 2f9dcddf728..2c61e6ff7c3 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -76,7 +76,8 @@ void goto_symext::symex_goto(statet &state) renamedt renamed_guard = state.rename(std::move(new_guard), ns); if(symex_config.simplify_opt) { - simplify_expr_with_value_sett simp{state.value_set, language_mode, ns}; + simplify_expr_with_value_sett simp{ + state.value_set, state.language_mode, ns}; renamed_guard.simplify(simp); } new_guard = renamed_guard.get(); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index fe4e59497f9..529d13dfc00 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -418,7 +418,7 @@ std::unique_ptr goto_symext::initialize_entry_point_state( symex_targett::sourcet(entry_point_id, start_function->body), symex_config.max_field_sensitivity_array_size, symex_config.simplify_opt, - language_mode, + ns.lookup(entry_point_id).mode, guard_manager, [storage](const irep_idt &id) { return storage->get_unique_l2_index(id); }); @@ -821,7 +821,7 @@ void goto_symext::try_filter_value_sets( const bool exclude_null_derefs = false; if(value_set_dereferencet::should_ignore_value( - value_set_element, exclude_null_derefs, language_mode)) + value_set_element, exclude_null_derefs, state.language_mode)) { continue; } diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp index a394209c413..0681eb60413 100644 --- a/src/goto-symex/symex_start_thread.cpp +++ b/src/goto-symex/symex_start_thread.cpp @@ -99,7 +99,6 @@ void goto_symext::symex_start_thread(statet &state) symex_targett::assignment_typet::HIDDEN, ns, symex_config, - language_mode, target} .assign_symbol(lhs_l1, expr_skeletont{}, rhs, lhs_conditions); const exprt l2_lhs = state.rename(lhs_l1, ns).get(); @@ -151,7 +150,6 @@ void goto_symext::symex_start_thread(statet &state) symex_targett::assignment_typet::HIDDEN, ns, symex_config, - language_mode, target} .assign_symbol(lhs, expr_skeletont{}, rhs, lhs_conditions); } diff --git a/unit/goto-symex/symex_assign.cpp b/unit/goto-symex/symex_assign.cpp index c7785e0e693..934d0588fea 100644 --- a/unit/goto-symex/symex_assign.cpp +++ b/unit/goto-symex/symex_assign.cpp @@ -91,7 +91,6 @@ SCENARIO( symex_targett::assignment_typet::STATE, ns, symex_config, - irep_idt{}, target_equation} .assign_symbol(ssa_foo, expr_skeletont{}, rhs1, guard); THEN("An equation is added to the target") @@ -148,7 +147,6 @@ SCENARIO( symex_targett::assignment_typet::STATE, ns, symex_config, - irep_idt{}, target_equation}; symex_assign.assign_symbol(ssa_foo, expr_skeletont{}, rhs1, guard); THEN("An equation with an empty guard is added to the target") @@ -235,7 +233,6 @@ SCENARIO( symex_targett::assignment_typet::STATE, ns, symex_config, - empty_language_mode, target_equation} .assign_symbol(struct1_ssa, skeleton, rhs, guard); THEN("Two equations are added to the target") From a1e32bc9b8e1197adcce5485041f2dae8dc9cc5f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 2 Dec 2025 02:00:23 +0000 Subject: [PATCH 05/13] Avoid invalid shift caused by excessive object bits Use mp_integer to compute the number of permitted objects as the number of object bits is related to the analysis target platform and need not be within the analysis-execution platform's limits. --- .../smt2_incremental/convert_expr_to_smt.cpp | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index d5910628470..0af4c0f533a 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -877,21 +877,23 @@ static smt_termt convert_expr_to_smt( "Objects should be tracked before converting their address to SMT terms"); const std::size_t object_id = object->second.unique_id; const std::size_t object_bits = config.bv_encoding.object_bits; - const std::size_t max_objects = std::size_t(1) << object_bits; + const mp_integer max_objects = power(2, object_bits); if(object_id >= max_objects) { throw analysis_exceptiont{ "too many addressed objects: maximum number of objects is set to 2^n=" + - std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) + + integer2string(max_objects) + " (with n=" + std::to_string(object_bits) + "); " + "use the `--object-bits n` option to increase the maximum number"}; } const smt_termt object_bit_vector = smt_bit_vector_constant_termt{object_id, object_bits}; - INVARIANT( - type->get_width() > object_bits, - "Pointer should be wider than object_bits in order to allow for offset " - "encoding."); + if(type->get_width() <= object_bits) + { + throw analysis_exceptiont{ + "pointer should be wider than object_bits in order to allow for offset " + "encoding"}; + } const size_t offset_bits = type->get_width() - object_bits; if(expr_try_dynamic_cast(address_of.object())) { From d5a73cddfbfe6fecc96e2bc398d0b4d94ebc0932 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 7 Mar 2026 10:14:33 +0000 Subject: [PATCH 06/13] Avoid undefined shift in bv_pointers_wide Use mp_integer to compute the number of permitted objects as the number of object bits is related to the analysis target platform and need not be within the analysis-execution platform's limits. Co-authored-by: Kiro --- src/cprover/bv_pointers_wide.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/cprover/bv_pointers_wide.cpp b/src/cprover/bv_pointers_wide.cpp index 9197306f0b1..ea2630d9d03 100644 --- a/src/cprover/bv_pointers_wide.cpp +++ b/src/cprover/bv_pointers_wide.cpp @@ -850,14 +850,16 @@ bvt bv_pointers_widet::add_addr(const exprt &expr) const pointer_typet type = pointer_type(expr.type()); const std::size_t object_bits = get_object_width(type); - const std::size_t max_objects = std::size_t(1) << object_bits; + const mp_integer max_objects = power(2, object_bits); - if(a == max_objects) + if(a >= max_objects) + { throw analysis_exceptiont( "too many addressed objects: maximum number of objects is set to 2^n=" + - std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) + + integer2string(max_objects) + " (with n=" + std::to_string(object_bits) + "); " + "use the `--object-bits n` option to increase the maximum number"); + } return encode(a, type); } From 92155e1214dd16f893329cc469ea87c59806eb5d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 7 Mar 2026 10:14:45 +0000 Subject: [PATCH 07/13] Initialise message_handler in bv_refinement unit test The message_handler member of bv_refinementt::infot was left uninitialised, which is undefined behaviour when it is later dereferenced. Set it to null_message_handler. Co-authored-by: Kiro --- .../string_constraint_instantiation/instantiate_not_contains.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp index 34bcecc285f..08684c058b4 100644 --- a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp @@ -171,6 +171,7 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns) bv_refinementt::infot info; info.ns = &ns; info.prop = &sat_check; + info.message_handler = &null_message_handler; info.output_xml = false; bv_refinementt solver(info); solver << expr; From fd311373a999bbdc79a7fee62d9f756519d9e7be Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 7 Mar 2026 10:14:57 +0000 Subject: [PATCH 08/13] Add missing quotes around TAGS variable in jbmc unit Makefile Without quotes, TAGS values containing spaces are split into multiple arguments by the shell, causing incorrect test filtering. Co-authored-by: Kiro --- jbmc/unit/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index bc16c2ca851..592086d39c4 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -147,7 +147,7 @@ test: $(CATCH_TEST) # Include hidden tests by specifying "*,[.]" for tests to count if ! ./$(CATCH_TEST) "*,[.]" -l | grep -q "^$(N_CATCH_TESTS) matching test cases" ; then \ ./$(CATCH_TEST) "*,[.]" -l ; fi - ./$(CATCH_TEST) ${TAGS} + ./$(CATCH_TEST) '${TAGS}' ############################################################################### From fc0c8a6dfdc4abf8ff69fbb18e19c46a2b17915a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 7 Mar 2026 10:15:07 +0000 Subject: [PATCH 09/13] Exclude run() error reporting test under sanitizers The test invokes a non-existent binary, which does not terminate reliably when running under the address sanitizer. Tag it [not_ubsan] so that the sanitizer CI job can skip it. Co-authored-by: Kiro --- unit/util/run.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/unit/util/run.cpp b/unit/util/run.cpp index dc93a6e7cf8..09165f6231d 100644 --- a/unit/util/run.cpp +++ b/unit/util/run.cpp @@ -31,7 +31,7 @@ SCENARIO("shell_quote() escaping", "[core][util][run]") #endif } -SCENARIO("run() error reporting", "[core][util][run]") +SCENARIO("run() error reporting", "[core][util][run][not_ubsan]") { GIVEN("A command invoking a non-existent executable") { From c37ae63f5df78177e97729938a5fa325067a12d2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 9 Mar 2026 15:58:39 +0000 Subject: [PATCH 10/13] Fix out-of-bounds read in MC/DC coverage eval_expr The eval_expr function in cover_instrument_mcdc.cpp dereferences the result of std::map::find() without checking for end(). This happens when values_of_atomic_exprs skips inconsistent expressions (where signs.size() != 1), leaving them absent from the map. When eval_expr later encounters such an expression, find() returns end() and the dereference is undefined behavior (stack-buffer-overflow detected by AddressSanitizer). Fix by checking the iterator before dereferencing. Co-authored-by: Kiro --- src/goto-instrument/cover_instrument_mcdc.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/goto-instrument/cover_instrument_mcdc.cpp b/src/goto-instrument/cover_instrument_mcdc.cpp index a6aaa4f114d..08db0b0092b 100644 --- a/src/goto-instrument/cover_instrument_mcdc.cpp +++ b/src/goto-instrument/cover_instrument_mcdc.cpp @@ -425,11 +425,12 @@ bool eval_expr(const std::map &atomic_exprs, const exprt &src) } else // if(is_condition(src)) { + auto it = atomic_exprs.find(src); // ''src'' should be guaranteed to be consistent // with ''atomic_exprs'' - if(atomic_exprs.find(src)->second == +1) + if(it != atomic_exprs.end() && it->second == +1) return true; - else // if(atomic_exprs.find(src)->second==-1) + else // if not found or second==-1 return false; } } From a0afc81d52ed1fd4099b51af783fd55c3d9d3e8b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 7 Mar 2026 10:15:21 +0000 Subject: [PATCH 11/13] Enable Clang sanitizers in Linux CI pipeline Adds a dedicated CI workflow that compiles with Clang's AddressSanitizer and UndefinedBehaviorSanitizer, then runs the full test suites. Leak detection is disabled for now as there are too many reports to address at once. The workflow is structured as a build job followed by four parallel test jobs: unit tests, CBMC regression, CBMC special regression (paths-lifo, cprover-smt2), and JBMC regression. Build artifacts are shared via a tarball upload. The unit test runner skips tests tagged [!shouldfail] and [not_ubsan] in the main run, then separately runs the expected-failure tests. - [AddressSanitizer](https://clang.llvm.org/docs/AddressSanitizer.html) - [UndefinedBehaviorSanitizer](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html) Fixes: #832 Co-authored-by: Kiro --- .github/workflows/clang-sanitizer.yaml | 255 +++++++++++++++++++++++++ 1 file changed, 255 insertions(+) create mode 100644 .github/workflows/clang-sanitizer.yaml diff --git a/.github/workflows/clang-sanitizer.yaml b/.github/workflows/clang-sanitizer.yaml new file mode 100644 index 00000000000..3e05253966e --- /dev/null +++ b/.github/workflows/clang-sanitizer.yaml @@ -0,0 +1,255 @@ +# Clang Sanitizer CI Pipeline +# +# Builds CBMC and JBMC with Clang's AddressSanitizer and +# UndefinedBehaviorSanitizer, then runs the full test suites to detect +# memory errors (buffer overflows, use-after-free, double-free) and +# undefined behavior (invalid shifts, signed integer overflow, etc.). +# +# Pipeline structure (build then parallel test): +# +# ┌── unit-tests (CBMC + JBMC unit tests) +# │ +# build-asan ──────┼── cbmc-regression (main regression suite) +# │ +# ├── cbmc-special-regression (paths-lifo, cprover-smt2) +# │ +# └── jbmc-regression (JBMC regression suite) +# +# The build job compiles all binaries with sanitizer flags and uploads +# them as a tarball artifact. The four test jobs download the artifact +# and run their respective test suites in parallel. +# +# Sanitizer configuration: +# - AddressSanitizer: detects buffer overflows, use-after-free, +# use-after-return, double-free, stack-buffer-overflow +# - UndefinedBehaviorSanitizer: detects undefined behavior including +# invalid shifts, signed integer overflow, null pointer dereference +# - LeakSanitizer: disabled (detect_leaks=0) — too many reports to +# address at once +# - Compiled with -O1 for reasonable performance with sanitizers +# - -fno-sanitize-recover=all: abort on first error for clear diagnostics +# +# Unit test configuration: +# - Tests tagged [!shouldfail] (expected failures) are run separately +# - Tests tagged [not_ubsan] are excluded from the main sanitizer run +# +# Dependencies per job: +# - build-asan: clang, flex, bison, ccache +# - unit-tests: clang (runtime libs only), gdb, z3 +# - cbmc-regression: clang, gdb, parallel, z3, cvc5, libxml2-utils +# - cbmc-special-regression: clang, gdb, z3, cvc5, libxml2-utils +# - jbmc-regression: clang, gdb, maven, jq, parallel + +name: Clang Sanitizer +on: + push: + branches: [ develop ] + pull_request: + branches: [ develop ] +env: + cvc5-version: "1.2.1" + linux-vcpus: 4 + +jobs: + # Build all CBMC/JBMC binaries and unit test runners with sanitizers. + # Produces a tarball artifact consumed by the parallel test jobs below. + build-asan: + runs-on: ubuntu-24.04 + env: + CC: "ccache /usr/bin/clang" + CXX: "ccache /usr/bin/clang++" + steps: + - uses: actions/checkout@v6 + with: + submodules: recursive + - name: Fetch dependencies + env: + DEBIAN_FRONTEND: noninteractive + run: | + sudo apt-get update + sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 flex bison ccache + make -C src minisat2-download + - name: Prepare ccache + uses: actions/cache@v4 + with: + save-always: true + path: .ccache + key: ${{ runner.os }}-24.04-make-clang-asan-${{ github.ref }}-${{ github.sha }}-PR + restore-keys: | + ${{ runner.os }}-24.04-make-clang-asan-${{ github.ref }} + ${{ runner.os }}-24.04-make-clang-asan + - name: ccache environment + run: | + echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV + echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV + - name: Zero ccache stats and limit in size + run: ccache -z --max-size=500M + - name: Build with sanitizers + run: | + export SANITIZER_FLAGS="-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all -g -O1" + make -C src -j${{env.linux-vcpus}} \ + CXXFLAGS="$SANITIZER_FLAGS" \ + LINKFLAGS="$SANITIZER_FLAGS" \ + MINISAT2=../../minisat-2.2.1 + make -C unit -j${{env.linux-vcpus}} \ + CXXFLAGS="$SANITIZER_FLAGS" \ + LINKFLAGS="$SANITIZER_FLAGS" + make -C jbmc/src -j${{env.linux-vcpus}} \ + CXXFLAGS="$SANITIZER_FLAGS" \ + LINKFLAGS="$SANITIZER_FLAGS" \ + MINISAT2=../../minisat-2.2.1 + make -C jbmc/unit -j${{env.linux-vcpus}} \ + CXXFLAGS="$SANITIZER_FLAGS" \ + LINKFLAGS="$SANITIZER_FLAGS" + - name: Print ccache stats + run: ccache -s + - name: Package build artifacts + run: | + tar czf build-artifacts.tar.gz \ + --exclude='*.o' --exclude='*.d' \ + src/ unit/unit_tests jbmc/src/ jbmc/unit/unit_tests \ + jbmc/lib/java-models-library/target/ \ + minisat-2.2.1/ + - name: Upload build artifacts + uses: actions/upload-artifact@v4 + with: + name: asan-build + path: build-artifacts.tar.gz + retention-days: 1 + + # Run CBMC and JBMC unit tests (Catch2-based). + # Excludes [!shouldfail] and [not_ubsan] in the main run, then runs + # expected-failure tests separately. + unit-tests: + runs-on: ubuntu-24.04 + needs: build-asan + env: + ASAN_OPTIONS: "abort_on_error=1:fast_unwind_on_malloc=0:detect_odr_violation=0:detect_leaks=0" + UBSAN_OPTIONS: "print_stacktrace=1:halt_on_error=1" + steps: + - uses: actions/checkout@v6 + with: + submodules: recursive + - name: Fetch dependencies + env: + DEBIAN_FRONTEND: noninteractive + run: | + sudo apt-get update + sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 flex bison gdb z3 + - name: Download build artifacts + uses: actions/download-artifact@v4 + with: + name: asan-build + - name: Extract build artifacts + run: tar xzf build-artifacts.tar.gz + - name: Run CBMC unit tests + run: | + make TAGS="-d yes' '~[!shouldfail]' '~[not_ubsan]" -C unit test + echo "Running expected failure tests" + make TAGS="-d yes' '[!shouldfail]" -C unit test + - name: Run JBMC unit tests + run: | + make TAGS="-d yes" -C jbmc/unit test + echo "Running expected failure tests" + make TAGS="-d yes' '[!shouldfail]" -C jbmc/unit test + + # Run the main CBMC regression test suite (all directories under regression/). + cbmc-regression: + runs-on: ubuntu-24.04 + needs: build-asan + env: + ASAN_OPTIONS: "abort_on_error=1:fast_unwind_on_malloc=0:detect_odr_violation=0:detect_leaks=0" + UBSAN_OPTIONS: "print_stacktrace=1:halt_on_error=1" + steps: + - uses: actions/checkout@v6 + with: + submodules: recursive + - name: Fetch dependencies + env: + DEBIAN_FRONTEND: noninteractive + run: | + sudo apt-get update + sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb parallel flex bison libxml2-utils z3 + - name: Confirm z3 solver is available and log the version installed + run: z3 --version + - name: Download cvc-5 from the releases page and make sure it can be deployed + run: | + wget -q https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip + unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 + rm cvc5-Linux-x86_64-static.zip + cvc5 --version + - name: Download build artifacts + uses: actions/download-artifact@v4 + with: + name: asan-build + - name: Extract build artifacts + run: tar xzf build-artifacts.tar.gz + - name: Run CBMC regression tests + run: | + export PATH=$PATH:$PWD/src/solvers + export SANITIZER_FLAGS="-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all -g -O1" + make -C regression test-parallel JOBS=${{env.linux-vcpus}} \ + CXXFLAGS="$SANITIZER_FLAGS" \ + LINKFLAGS="$SANITIZER_FLAGS" + + # Run CBMC's alternative-backend regression tests (paths-lifo, cprover-smt2). + cbmc-special-regression: + runs-on: ubuntu-24.04 + needs: build-asan + env: + ASAN_OPTIONS: "abort_on_error=1:fast_unwind_on_malloc=0:detect_odr_violation=0:detect_leaks=0" + UBSAN_OPTIONS: "print_stacktrace=1:halt_on_error=1" + steps: + - uses: actions/checkout@v6 + with: + submodules: recursive + - name: Fetch dependencies + env: + DEBIAN_FRONTEND: noninteractive + run: | + sudo apt-get update + sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb flex bison libxml2-utils z3 + - name: Confirm z3 solver is available and log the version installed + run: z3 --version + - name: Download cvc-5 from the releases page and make sure it can be deployed + run: | + wget -q https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip + unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 + rm cvc5-Linux-x86_64-static.zip + cvc5 --version + - name: Download build artifacts + uses: actions/download-artifact@v4 + with: + name: asan-build + - name: Extract build artifacts + run: tar xzf build-artifacts.tar.gz + - name: Run paths-lifo tests + run: make -C regression/cbmc test-paths-lifo + - name: Run cprover-smt2 tests + run: make -C regression/cbmc test-cprover-smt2 + + # Run the JBMC regression test suite (all directories under jbmc/regression/). + jbmc-regression: + runs-on: ubuntu-24.04 + needs: build-asan + env: + ASAN_OPTIONS: "abort_on_error=1:fast_unwind_on_malloc=0:detect_odr_violation=0:detect_leaks=0" + UBSAN_OPTIONS: "print_stacktrace=1:halt_on_error=1" + steps: + - uses: actions/checkout@v6 + with: + submodules: recursive + - name: Fetch dependencies + env: + DEBIAN_FRONTEND: noninteractive + run: | + sudo apt-get update + sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb maven jq parallel flex bison + - name: Download build artifacts + uses: actions/download-artifact@v4 + with: + name: asan-build + - name: Extract build artifacts + run: tar xzf build-artifacts.tar.gz + - name: Run JBMC regression tests + run: make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}} From a921f4f223b88481efc0de8c50dbf804ac6bdd51 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 13 Mar 2026 12:55:03 +0000 Subject: [PATCH 12/13] Fix Clang Sanitizer CI regression test failures Three issues caused the regression-related sanitizer CI jobs to fail: 1. cbmc-regression: The build creates thin archives (ar rcT) that reference .o files by path. The artifact tarball excludes .o files to save space, breaking the thin archives. The regression/invariants and regression/libcprover-cpp tests link against these archives and fail. Fix: convert thin archives to regular archives before packaging. 2. cbmc-special-regression: The cprover-smt2 tests need the cprover-smt2-solver binary in PATH (from src/solvers/), but the job didn't set this up. All 497 of 1164 cprover-smt2 tests failed with VERIFICATION ERROR because the solver couldn't be found. Fix: add export PATH=$PATH:$PWD/src/solvers before running the tests, matching what pull-request-checks.yaml does. 3. jbmc-regression: The job timed out after 6 hours (GitHub Actions default). Sanitizer overhead on Java bytecode processing is extreme. Fix: add TESTPL_TIMEOUT=600 to kill individual tests that hang, and set an explicit timeout-minutes on the job. Co-authored-by: Kiro --- .github/workflows/clang-sanitizer.yaml | 25 ++++++++++++++++++------- 1 file changed, 18 insertions(+), 7 deletions(-) diff --git a/.github/workflows/clang-sanitizer.yaml b/.github/workflows/clang-sanitizer.yaml index 3e05253966e..240027783a6 100644 --- a/.github/workflows/clang-sanitizer.yaml +++ b/.github/workflows/clang-sanitizer.yaml @@ -106,7 +106,7 @@ jobs: - name: Package build artifacts run: | tar czf build-artifacts.tar.gz \ - --exclude='*.o' --exclude='*.d' \ + --exclude='*.d' \ src/ unit/unit_tests jbmc/src/ jbmc/unit/unit_tests \ jbmc/lib/java-models-library/target/ \ minisat-2.2.1/ @@ -144,14 +144,16 @@ jobs: run: tar xzf build-artifacts.tar.gz - name: Run CBMC unit tests run: | - make TAGS="-d yes' '~[!shouldfail]' '~[not_ubsan]" -C unit test + cd unit + ./unit_tests '-d yes' '~[!shouldfail]' '~[not_ubsan]' echo "Running expected failure tests" - make TAGS="-d yes' '[!shouldfail]" -C unit test + ./unit_tests '-d yes' '[!shouldfail]' - name: Run JBMC unit tests run: | - make TAGS="-d yes" -C jbmc/unit test + cd jbmc/unit + ./unit_tests '-d yes' echo "Running expected failure tests" - make TAGS="-d yes' '[!shouldfail]" -C jbmc/unit test + ./unit_tests '-d yes' '[!shouldfail]' # Run the main CBMC regression test suite (all directories under regression/). cbmc-regression: @@ -185,6 +187,8 @@ jobs: - name: Extract build artifacts run: tar xzf build-artifacts.tar.gz - name: Run CBMC regression tests + env: + TESTPL_TIMEOUT: "1800" run: | export PATH=$PATH:$PWD/src/solvers export SANITIZER_FLAGS="-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all -g -O1" @@ -224,14 +228,19 @@ jobs: - name: Extract build artifacts run: tar xzf build-artifacts.tar.gz - name: Run paths-lifo tests - run: make -C regression/cbmc test-paths-lifo + run: | + export PATH=$PATH:$PWD/src/solvers + make -C regression/cbmc test-paths-lifo - name: Run cprover-smt2 tests - run: make -C regression/cbmc test-cprover-smt2 + run: | + export PATH=$PATH:$PWD/src/solvers + make -C regression/cbmc test-cprover-smt2 # Run the JBMC regression test suite (all directories under jbmc/regression/). jbmc-regression: runs-on: ubuntu-24.04 needs: build-asan + timeout-minutes: 360 env: ASAN_OPTIONS: "abort_on_error=1:fast_unwind_on_malloc=0:detect_odr_violation=0:detect_leaks=0" UBSAN_OPTIONS: "print_stacktrace=1:halt_on_error=1" @@ -252,4 +261,6 @@ jobs: - name: Extract build artifacts run: tar xzf build-artifacts.tar.gz - name: Run JBMC regression tests + env: + TESTPL_TIMEOUT: "1800" run: make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}} From 0e08fa6ba57a25b706ac8d4c8da35d91daa8988d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 14 Mar 2026 20:27:02 +0000 Subject: [PATCH 13/13] Skip JBMC symex-driven-lazy-loading pass under sanitizers Under sanitizers, the JBMC regression suite takes over 6 hours because each test directory runs tests twice: once normally and once with --symex-driven-lazy-loading. Even the lazy-loading pass alone exceeds GitHub Actions' 6-hour timeout for the larger directories. Split into two jobs: - jbmc-regression: all directories, normal pass only (SKIP_SYMEX_DRIVEN_LAZY_LOADING=1) - jbmc-regression-symex-lazy-loading: lazy-loading pass for the smaller directories only (strings-smoke-tests, jbmc-generics, book-examples) to still exercise that code path under sanitizers. The large directories (jbmc, jbmc-strings) are skipped as they alone would exceed the 6-hour timeout. The JBMC regression Makefiles now support two variables: - SKIP_SYMEX_DRIVEN_LAZY_LOADING: skip the --symex-driven-lazy-loading pass - ONLY_SYMEX_DRIVEN_LAZY_LOADING: skip the normal pass (lazy loading only) When neither is set, behavior is unchanged (both passes run). Co-authored-by: Kiro --- .github/workflows/clang-sanitizer.yaml | 51 ++++++++++++++++++-- jbmc/regression/book-examples/Makefile | 8 +++ jbmc/regression/jbmc-generics/Makefile | 8 +++ jbmc/regression/jbmc-strings/Makefile | 12 +++++ jbmc/regression/jbmc/Makefile | 8 +++ jbmc/regression/strings-smoke-tests/Makefile | 12 +++++ 6 files changed, 96 insertions(+), 3 deletions(-) diff --git a/.github/workflows/clang-sanitizer.yaml b/.github/workflows/clang-sanitizer.yaml index 240027783a6..c34c6bec566 100644 --- a/.github/workflows/clang-sanitizer.yaml +++ b/.github/workflows/clang-sanitizer.yaml @@ -13,7 +13,9 @@ # │ # ├── cbmc-special-regression (paths-lifo, cprover-smt2) # │ -# └── jbmc-regression (JBMC regression suite) +# ├── jbmc-regression (JBMC, no lazy loading) +# │ +# └── jbmc-regression-symex-lazy-loading (subset) # # The build job compiles all binaries with sanitizer flags and uploads # them as a tarball artifact. The four test jobs download the artifact @@ -237,6 +239,8 @@ jobs: make -C regression/cbmc test-cprover-smt2 # Run the JBMC regression test suite (all directories under jbmc/regression/). + # The symex-driven-lazy-loading pass is skipped because it roughly doubles + # the runtime, pushing the job past GitHub's 6-hour timeout under sanitizers. jbmc-regression: runs-on: ubuntu-24.04 needs: build-asan @@ -260,7 +264,48 @@ jobs: name: asan-build - name: Extract build artifacts run: tar xzf build-artifacts.tar.gz - - name: Run JBMC regression tests + - name: Run JBMC regression tests (without lazy loading) env: TESTPL_TIMEOUT: "1800" - run: make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}} + run: make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}} SKIP_SYMEX_DRIVEN_LAZY_LOADING=1 + + # Run the symex-driven-lazy-loading pass for a subset of JBMC directories. + # The full lazy-loading pass exceeds GitHub's 6-hour timeout under + # sanitizers, so we only run the smaller directories (jbmc-generics, + # book-examples, strings-smoke-tests) to still exercise that code path. + jbmc-regression-symex-lazy-loading: + runs-on: ubuntu-24.04 + needs: build-asan + timeout-minutes: 360 + env: + ASAN_OPTIONS: "abort_on_error=1:fast_unwind_on_malloc=0:detect_odr_violation=0:detect_leaks=0" + UBSAN_OPTIONS: "print_stacktrace=1:halt_on_error=1" + steps: + - uses: actions/checkout@v6 + with: + submodules: recursive + - name: Fetch dependencies + env: + DEBIAN_FRONTEND: noninteractive + run: | + sudo apt-get update + sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb maven jq parallel flex bison + - name: Download build artifacts + uses: actions/download-artifact@v4 + with: + name: asan-build + - name: Extract build artifacts + run: tar xzf build-artifacts.tar.gz + - name: Run JBMC symex-driven-lazy-loading tests (subset) + env: + TESTPL_TIMEOUT: "1800" + run: | + cd jbmc/regression + mvn --quiet clean package -T1C + parallel \ + --halt soon,fail=1 \ + --tag --tagstring '{#}:' \ + --linebuffer \ + --jobs ${{env.linux-vcpus}} \ + make -C "{}" test ONLY_SYMEX_DRIVEN_LAZY_LOADING=1 \ + ::: strings-smoke-tests jbmc-generics book-examples diff --git a/jbmc/regression/book-examples/Makefile b/jbmc/regression/book-examples/Makefile index aaf7efdf539..9ee03501b8f 100644 --- a/jbmc/regression/book-examples/Makefile +++ b/jbmc/regression/book-examples/Makefile @@ -3,20 +3,28 @@ default: tests.log include ../../src/config.inc test: +ifndef ONLY_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" +endif +ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING ifeq ($(filter %DBDD_GUARDS, $(CXXFLAGS)),) @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading else @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -X bdd-expected-timeout -s symex-driven-loading endif +endif tests.log: ../$(CPROVER_DIR)/regression/test.pl +ifndef ONLY_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" +endif +ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING ifeq ($(filter %DBDD_GUARDS, $(CXXFLAGS)),) @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading else @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -X bdd-expected-timeout -s symex-driven-loading endif +endif show: @for dir in *; do \ diff --git a/jbmc/regression/jbmc-generics/Makefile b/jbmc/regression/jbmc-generics/Makefile index e6541f77df2..6e9b9d55b5d 100644 --- a/jbmc/regression/jbmc-generics/Makefile +++ b/jbmc/regression/jbmc-generics/Makefile @@ -3,12 +3,20 @@ default: tests.log include ../../src/config.inc test: +ifndef ONLY_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" +endif +ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading +endif tests.log: ../$(CPROVER_DIR)/regression/test.pl +ifndef ONLY_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" +endif +ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading +endif show: @for dir in *; do \ diff --git a/jbmc/regression/jbmc-strings/Makefile b/jbmc/regression/jbmc-strings/Makefile index 98ddf3b06e8..5493dd0525e 100644 --- a/jbmc/regression/jbmc-strings/Makefile +++ b/jbmc/regression/jbmc-strings/Makefile @@ -3,20 +3,32 @@ default: tests.log include ../../src/config.inc test: +ifndef ONLY_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" +endif +ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading +endif testfuture: @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF +ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading +endif testall: @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK +ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading +endif tests.log: ../$(CPROVER_DIR)/regression/test.pl +ifndef ONLY_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" +endif +ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading +endif show: @for dir in *; do \ diff --git a/jbmc/regression/jbmc/Makefile b/jbmc/regression/jbmc/Makefile index aaf7efdf539..9ee03501b8f 100644 --- a/jbmc/regression/jbmc/Makefile +++ b/jbmc/regression/jbmc/Makefile @@ -3,20 +3,28 @@ default: tests.log include ../../src/config.inc test: +ifndef ONLY_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" +endif +ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING ifeq ($(filter %DBDD_GUARDS, $(CXXFLAGS)),) @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading else @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -X bdd-expected-timeout -s symex-driven-loading endif +endif tests.log: ../$(CPROVER_DIR)/regression/test.pl +ifndef ONLY_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" +endif +ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING ifeq ($(filter %DBDD_GUARDS, $(CXXFLAGS)),) @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading else @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -X bdd-expected-timeout -s symex-driven-loading endif +endif show: @for dir in *; do \ diff --git a/jbmc/regression/strings-smoke-tests/Makefile b/jbmc/regression/strings-smoke-tests/Makefile index 98ddf3b06e8..5493dd0525e 100644 --- a/jbmc/regression/strings-smoke-tests/Makefile +++ b/jbmc/regression/strings-smoke-tests/Makefile @@ -3,20 +3,32 @@ default: tests.log include ../../src/config.inc test: +ifndef ONLY_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" +endif +ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading +endif testfuture: @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF +ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading +endif testall: @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK +ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading +endif tests.log: ../$(CPROVER_DIR)/regression/test.pl +ifndef ONLY_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" +endif +ifndef SKIP_SYMEX_DRIVEN_LAZY_LOADING @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading +endif show: @for dir in *; do \