diff --git a/.github/workflows/clang-sanitizer.yaml b/.github/workflows/clang-sanitizer.yaml new file mode 100644 index 00000000000..6fa997efb1a --- /dev/null +++ b/.github/workflows/clang-sanitizer.yaml @@ -0,0 +1,98 @@ +name: Clang Sanitizer +on: + push: + branches: [ develop ] + pull_request: + branches: [ develop ] +env: + cvc5-version: "1.2.1" + linux-vcpus: 4 + +jobs: + # This job takes approximately X to Y minutes + clang-asan-ubuntu-24_04-make: + runs-on: ubuntu-24.04 + env: + CC: "ccache /usr/bin/clang" + CXX: "ccache /usr/bin/clang++" + # AddressSanitizer configuration for optimal CI performance + ASAN_OPTIONS: "abort_on_error=1:fast_unwind_on_malloc=0:detect_odr_violation=0:detect_leaks=0" + # - `abort_on_error=1`: Terminate immediately on error + # - `fast_unwind_on_malloc=0`: Use slower but more accurate stack unwinding + # - `detect_odr_violation=0`: Disable One Definition Rule violation detection to reduce noise + # - `detect_leaks=0`: Disable leak detection + UBSAN_OPTIONS: "print_stacktrace=1:halt_on_error=1" + # - `print_stacktrace=1`: Show stack traces for undefined behavior + # - `halt_on_error=1`: Terminate on undefined behavior + 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 flex bison libxml2-utils ccache z3 + make -C src minisat2-download + - 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 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: 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 AddressSanitizer + run: | + # Build with sanitizers enabled - using -O1 for reasonable performance + # -fsanitize=address: detects buffer overflows, use-after-free, etc. + # -fsanitize=undefined: detects undefined behavior + # -fno-sanitize-recover=all: abort on first error for faster feedback + # -g: include debug symbols for better error reporting + 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: Run unit tests + run: | + make TAGS="-d yes' '~[!shouldfail]' '~[not_ubsan]" -C unit test + make TAGS="-d yes" -C jbmc/unit test + echo "Running expected failure tests" + make TAGS="-d yes' '[!shouldfail]" -C unit test + make TAGS="-d yes' '[!shouldfail]" -C jbmc/unit test + - name: Run regression tests + run: | + export PATH=$PATH:`pwd`/src/solvers + make -C regression test-parallel JOBS=${{env.linux-vcpus}} + make -C regression/cbmc test-paths-lifo + make -C regression/cbmc test-cprover-smt2 + make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}} 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}' ############################################################################### 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; 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); } 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 24d9e4dc33b..3bbbd2bfb41 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, state.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) @@ -106,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 @@ -142,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 5980573f0cd..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 @@ -526,7 +522,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/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 96020d5970e..769b16ccec1 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; @@ -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_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..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"); @@ -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,14 +426,14 @@ 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)); } } 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( @@ -454,12 +454,12 @@ void goto_symext::symex_input( for(std::size_t i=1; i 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 f065dbda360..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()); @@ -135,7 +135,7 @@ void goto_symext::process_array_expr(statet &state, exprt &expr) lift_lets(state, expr); ::process_array_expr(expr, ns); - do_simplify(expr, state.value_set); + do_simplify(expr, state); } /// Rewrite index/member expressions in byte_extract to offset @@ -178,7 +178,7 @@ void goto_symext::lift_let(statet &state, const let_exprt &let_expr) { exprt let_value = clean_expr(let_expr.value(), state, false); let_value = state.rename(std::move(let_value), ns).get(); - do_simplify(let_value, state.value_set); + do_simplify(let_value, state); exprt::operandst value_assignment_guard; symex_assignt{ @@ -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 6948502b67e..9f53513d2a9 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -101,7 +101,7 @@ exprt goto_symext::address_arithmetic( // recursive call result = address_arithmetic(be, state, keep_array); - do_simplify(result, state.value_set); + do_simplify(result, state); } else if(expr.id()==ID_dereference) { @@ -158,7 +158,7 @@ exprt goto_symext::address_arithmetic( result = address_arithmetic(be, state, keep_array); - do_simplify(result, state.value_set); + do_simplify(result, state); } else result=address_of_exprt(result); @@ -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( @@ -308,7 +307,7 @@ void goto_symext::dereference_rec( tmp1 = state.rename(tmp1, ns).get(); - do_simplify(tmp1, state.value_set); + do_simplify(tmp1, state); if(symex_config.run_validation_checks) { @@ -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()); @@ -515,7 +514,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_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 3bde290706b..6cb82a62d3b 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -75,7 +75,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(); @@ -118,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 4fe53bc7c61..7486f05949b 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 @@ -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; } @@ -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()), 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/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())) { 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..934d0588fea 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}; @@ -90,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") @@ -147,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") @@ -234,7 +233,6 @@ SCENARIO( symex_targett::assignment_typet::STATE, ns, symex_config, - irep_idt{}, target_equation} .assign_symbol(struct1_ssa, skeleton, rhs, guard); THEN("Two equations are added to the target") 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") {