Enable concurrent speculative checking with thread-safe irept

Make irept reference counting thread-safe with std::atomic<unsigned>.
Use fetch_sub(1)==1 for the decrement+check pattern. Performance
impact: ~2% (within noise).

Add per-thread merge_irept isolation: swap in a fresh merge_irept
for symex during the concurrent phase so new steps don't share the
hash table with existing steps that the speculative thread reads.

Add thread-local stream_message_handlert for the speculative thread,
with captured output printed after join.

Add set_message_handler() and swap_merge_irep() public methods to
symex_target_equationt.

The speculative thread now runs concurrently with symex: it reads
existing steps (safe with atomic ref_count and isolated merge pools)
while symex appends new steps with its own merge_irep.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

doc/man/cbmc.1

@@ -436,6 +436,11 @@ threads. Symbolic execution pauses every N steps (set via
 \fB\-\-incremental\-check\-interval\fR) and hands off to the solver.
 Requires \fB\-\-incremental\-check\-interval\fR.
 .TP
+\fB\-\-speculative\-check\fR
+speculatively check assertions on partial equations using
+cone\-of\-influence slicing. Use with
+\fB\-\-incremental\-check\-interval\fR.
+.TP
 \fB\-\-show\-vcc\fR
 show the verification conditions
 .TP

doc/man/jbmc.1

@@ -350,6 +350,11 @@ threads. Symbolic execution pauses every N steps (set via
 \fB\-\-incremental\-check\-interval\fR) and hands off to the solver.
 Requires \fB\-\-incremental\-check\-interval\fR.
 .TP
+\fB\-\-speculative\-check\fR
+speculatively check assertions on partial equations using
+cone\-of\-influence slicing. Use with
+\fB\-\-incremental\-check\-interval\fR.
+.TP
 \fB\-\-show\-vcc\fR
 show the verification conditions
 .TP

src/cbmc/cbmc_parse_options.cpp

@@ -449,6 +449,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("concurrent-incremental"))
     options.set_option("concurrent-incremental", true);
 
+  if(cmdline.isset("speculative-check"))
+    options.set_option("speculative-check", true);
+
   if(cmdline.isset("graphml-witness"))
   {
     options.set_option("graphml-witness", cmdline.get_value("graphml-witness"));

src/goto-checker/bmc_util.h

@@ -201,6 +201,7 @@ std::chrono::duration<double> prepare_property_decider_incremental(
   "(incremental-loop):"                                                        \
   "(incremental-check-interval):"                                              \
   "(concurrent-incremental)"                                                   \
+  "(speculative-check)"                                                        \
   "(unwind-min):"                                                              \
   "(unwind-max):"                                                              \
   "(ignore-properties-before-unwind-min)"                                      \
@@ -231,6 +232,10 @@ std::chrono::duration<double> prepare_property_decider_incremental(
   " {y--concurrent-incremental} \t "                                           \
   "run symbolic execution and SAT solving concurrently in separate "           \
   "threads (use with {y--incremental-check-interval})\n"                       \
+  " {y--speculative-check} \t "                                                \
+  "speculatively check assertions on partial equations using "                 \
+  "cone-of-influence slicing (use with "                                       \
+  "{y--incremental-check-interval})\n"                                         \
   " {y--unwind-min} {unr} \t "                                                 \
   "start incremental-loop after {unr} unwindings but before solving that "     \
   "iteration. If for example it is 1, then the loop will be unwound once, "    \

src/goto-checker/concurrent_incremental_symex_checker.cpp

@@ -343,12 +343,13 @@ concurrent_incremental_symex_checkert::operator()(propertiest &properties)
 
     full_equation_generated = sync.symex_done;
 
-    revert_slice(equation);
-
+    // New steps from symex will be converted on the next iteration
+    // by prepare_property_decider_incremental. We do NOT revert the
+    // slice or reset current_equation_converted, because re-converting
+    // the entire equation into the same solver creates duplicate
+    // Tseitin clauses that corrupt the formula.
     update_properties_status_from_symex_target_equation(
       properties, result.updated_properties, equation);
-
-    current_equation_converted = false;
   }
 
   return result;

src/goto-checker/concurrent_incremental_symex_checker.h

@@ -14,7 +14,6 @@ Author: CBMC Contributors
 #ifndef CPROVER_GOTO_CHECKER_CONCURRENT_INCREMENTAL_SYMEX_CHECKER_H
 #define CPROVER_GOTO_CHECKER_CONCURRENT_INCREMENTAL_SYMEX_CHECKER_H
 
-
 #include <goto-programs/unwindset.h>
 
 #include <goto-symex/path_storage.h>

src/goto-checker/periodic_incremental_symex_checker.cpp

@@ -13,15 +13,17 @@ Author: CBMC Contributors
 
 #include "periodic_incremental_symex_checker.h"
 
+#include <util/std_expr.h>
 #include <util/ui_message.h>
 
 #include <goto-symex/slice.h>
+#include <solvers/prop/prop_conv_solver.h>
 
 #include "bmc_util.h"
+#include "counterexample_beautification.h"
 #include "solver_factory.h"
+
 #include <sstream>
-#include <solvers/prop/prop_conv_solver.h>
-#include "counterexample_beautification.h"
 
 // --- symex_bmc_periodic_stept implementation ---
 
@@ -119,6 +121,7 @@ periodic_incremental_symex_checkert::periodic_incremental_symex_checkert(
       unwindset,
       static_cast<unsigned>(
         options.get_signed_int_option("incremental-check-interval"))),
+    speculative_checking_enabled(options.get_bool_option("speculative-check")),
     property_decider(options, ui_message_handler, equation, ns)
 {
   unwindset.parse_unwind(options.get_option("unwind"));
@@ -147,7 +150,6 @@ periodic_incremental_symex_checkert::operator()(propertiest &properties)
     full_equation_generated = !symex.from_entry_point_of(
       goto_symext::get_goto_function(goto_model), symex_symbol_table);
 
-    // This might add new properties such as unwinding assertions.
     update_properties_status_from_symex_target_equation(
       properties, result.updated_properties, equation);
 
@@ -181,8 +183,7 @@ periodic_incremental_symex_checkert::operator()(propertiest &properties)
         ++solver_calls;
         log.status()
           << "Periodic check #" << solver_calls << ": running "
-          << property_decider.get_decision_procedure()
-               .decision_procedure_text()
+          << property_decider.get_decision_procedure().decision_procedure_text()
           << messaget::eom;
 
         decision_proceduret::resultt dec_result = property_decider.solve();
@@ -193,8 +194,8 @@ periodic_incremental_symex_checkert::operator()(propertiest &properties)
         const auto solver_stop = std::chrono::steady_clock::now();
         solver_runtime +=
           std::chrono::duration<double>(solver_stop - solver_start);
-        log.status() << "Runtime decision procedure: "
-                     << solver_runtime.count() << "s" << messaget::eom;
+        log.status() << "Runtime decision procedure: " << solver_runtime.count()
+                     << "s" << messaget::eom;
 
         result.progress =
           dec_result == decision_proceduret::resultt::D_SATISFIABLE
@@ -206,74 +207,80 @@ periodic_incremental_symex_checkert::operator()(propertiest &properties)
 
         property_decider.pop_incremental_assumptions();
       }
-      else
+      else if(speculative_checking_enabled)
       {
-        // Partial equation: launch speculative check in a thread.
-        // Save equation state before the speculative check modifies it.
-        saved_step_state.clear();
-        saved_step_state.reserve(equation.SSA_steps.size());
-        for(const auto &step : equation.SSA_steps)
-          saved_step_state.push_back(
-            {step.converted, step.cond_handle, step.guard_handle});
+        // Speculative cone-of-influence check on partial equation.
+        // Only check the most recently discovered assertion to
+        // minimize overhead.
+        const std::size_t current_assertions = equation.count_assertions();
+        if(current_assertions > last_speculative_assertion_count)
+        {
+          last_speculative_assertion_count = current_assertions;
 
-        ++solver_calls;
-        log.status() << "Speculative check #" << solver_calls
-                     << " on partial equation (" << equation.SSA_steps.size()
-                     << " steps)" << messaget::eom;
-
-        speculative_sat = false;
-        // Snapshot the current equation size. The speculative thread
-        // will only process steps up to this point. Symex may append
-        // new steps concurrently, but the thread won't see them.
-        const std::size_t snapshot_size = equation.SSA_steps.size();
-        speculative_thread = std::make_unique<std::thread>(
-          [this, snapshot_size]()
-          {
-            std::ostringstream spec_log_stream;
-            stream_message_handlert spec_mh(spec_log_stream);
-            spec_mh.set_verbosity(
-              ui_message_handler.get_verbosity());
-
-            solver_factoryt solvers(
-              options, ns, spec_mh, false);
-            auto spec_solver = solvers.get_solver();
-            auto &spec_dp = spec_solver->decision_procedure();
-
-            auto *prop_conv =
-              dynamic_cast<prop_conv_solvert *>(&spec_dp);
-            if(prop_conv)
-              prop_conv->set_all_frozen();
-
-            // Only convert the snapshot (existing steps).
-            // New steps appended by symex are not touched.
-            std::size_t count = 0;
-            for(auto &step : equation.SSA_steps)
+          ++solver_calls;
+          log.status() << "Speculative check #" << solver_calls
+                       << " on partial equation (" << equation.SSA_steps.size()
+                       << " steps)" << messaget::eom;
+
+          speculative_sat = false;
+          const std::size_t snapshot_size = equation.SSA_steps.size();
+          speculative_thread = std::make_unique<std::thread>(
+            [this, snapshot_size]()
             {
-              if(count >= snapshot_size)
-                break;
-              if(!step.ignore)
+              std::ostringstream spec_log_stream;
+              stream_message_handlert spec_mh(spec_log_stream);
+              spec_mh.set_verbosity(ui_message_handler.get_verbosity());
+
+              // Find the last assertion in the snapshot.
+              symex_target_equationt::SSA_stepst::const_iterator last_assert;
+              bool found = false;
+              std::size_t count = 0;
+              for(auto it = equation.SSA_steps.begin();
+                  it != equation.SSA_steps.end() && count < snapshot_size;
+                  ++it, ++count)
+              {
+                if(it->is_assert() && !it->ignore)
+                {
+                  last_assert = it;
+                  found = true;
+                }
+              }
+
+              if(!found)
+              {
+                speculative_log_output = spec_log_stream.str();
+                return;
+              }
+
+              auto cone = cone_of_influence(
+                equation.SSA_steps, last_assert, snapshot_size);
+
+              solver_factoryt solvers(options, ns, spec_mh, false);
+              auto spec_solver = solvers.get_solver();
+              auto &dp = spec_solver->decision_procedure();
+
+              for(const auto *step : cone)
               {
-                step.guard_handle = spec_dp.handle(step.guard);
-                if(step.is_assume())
-                  step.cond_handle = spec_dp.handle(step.cond_expr);
-                else if(step.is_assignment() || step.is_constraint())
-                  spec_dp.set_to_true(step.cond_expr);
-                else if(step.is_assert())
+                if(step->is_assignment() || step->is_constraint())
+                  dp.set_to_true(step->cond_expr);
+                else if(step->is_assume())
+                {
+                  exprt g = dp.handle(step->guard);
+                  dp.set_to_true(implies_exprt(g, step->cond_expr));
+                }
+                else if(step->is_assert())
                 {
-                  step.cond_handle = spec_dp.handle(step.cond_expr);
-                  spec_dp.set_to_false(step.cond_expr);
+                  exprt g = dp.handle(step->guard);
+                  dp.set_to_true(implies_exprt(g, not_exprt(step->cond_expr)));
                 }
               }
-              ++count;
-            }
 
-            auto r = spec_solver->decision_procedure()();
-            speculative_sat =
-              (r == decision_proceduret::resultt::D_SATISFIABLE);
+              if(dp() == decision_proceduret::resultt::D_SATISFIABLE)
+                speculative_sat = true;
 
-            speculative_log_output = spec_log_stream.str();
-          });
-        // Symex continues immediately — speculative thread runs concurrently.
+              speculative_log_output = spec_log_stream.str();
+            });
+        }
       }
     }
 
@@ -288,56 +295,44 @@ periodic_incremental_symex_checkert::operator()(propertiest &properties)
       break;
     }
 
-    // We continue symbolic execution
+    // Resume symbolic execution
     if(!full_equation_generated)
     {
-      // Give symex a fresh merge_irep so new steps don't share
-      // the hash table with existing steps. This allows the
-      // speculative thread to safely read existing steps' ireps
-      // while symex appends new ones.
-      merge_irept saved_merge_irep =
-        equation.swap_merge_irep(merge_irept{});
-
-      // Resume symex concurrently with the speculative thread.
-      full_equation_generated =
-        !symex.resume(goto_symext::get_goto_function(goto_model));
-
-      // Join speculative thread after symex pauses.
-      if(speculative_thread)
+      if(speculative_checking_enabled)
       {
-        speculative_thread->join();
-        speculative_thread.reset();
+        // Swap merge_irep so speculative thread can safely read
+        // existing steps while symex appends new ones.
+        merge_irept saved = equation.swap_merge_irep(merge_irept{});
 
-        auto sit = saved_step_state.begin();
-        for(auto &step : equation.SSA_steps)
-        {
-          if(sit == saved_step_state.end())
-            break;
-          step.converted = sit->converted;
-          step.cond_handle = sit->cond_handle;
-          step.guard_handle = sit->guard_handle;
-          ++sit;
-        }
+        full_equation_generated =
+          !symex.resume(goto_symext::get_goto_function(goto_model));
 
-        if(speculative_sat)
+        if(speculative_thread)
         {
-          log.status() << "Speculative check found potential failure"
-                       << messaget::eom;
-        }
+          speculative_thread->join();
+          speculative_thread.reset();
 
-        equation.set_message_handler(ui_message_handler);
-        if(!speculative_log_output.empty())
-        {
-          log.debug() << speculative_log_output << messaget::eom;
+          if(speculative_sat)
+          {
+            log.status() << "Speculative check found potential failure"
+                         << messaget::eom;
+          }
+
+          equation.set_message_handler(ui_message_handler);
+          if(!speculative_log_output.empty())
+            log.debug() << speculative_log_output << messaget::eom;
         }
-      }
 
-      // Restore the original merge_irep (merges both pools).
-      equation.swap_merge_irep(std::move(saved_merge_irep));
+        equation.swap_merge_irep(std::move(saved));
+      }
+      else
+      {
+        full_equation_generated =
+          !symex.resume(goto_symext::get_goto_function(goto_model));
+      }
 
       revert_slice(equation);
 
-      // This might add new properties such as unwinding assertions.
       update_properties_status_from_symex_target_equation(
         properties, result.updated_properties, equation);