Enable Clang sanitizers in Linux/Clang CI pipeline

.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}}

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}'
 
 
 ###############################################################################

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;

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);
 }

src/goto-checker/symex_bmc.cpp

@@ -16,8 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/unwindset.h>
 
-#include <linking/static_lifetime_init.h>
-
 #include <limits>
 
 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;
 }

src/goto-symex/goto_symex.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
 #include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
 #include <util/simplify_utils.h>
 #include <util/std_code.h>
 #include <util/string_expr.h>
@@ -29,11 +30,17 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <climits>
 
-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 <type> 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)

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

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<std::size_t(const irep_idt &)> fresh_l2_name_provider;
 
   /// \brief Dangerous, do not use

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

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(

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,