Implement incremental symex with periodic and concurrent SAT solving

doc/architectural/incremental-symex-goals.md

@@ -0,0 +1,77 @@
+# Incremental Symex Goal Construction
+
+## Overview
+
+CBMC's standard verification flow runs symbolic execution to completion,
+then converts all assertions into a single SAT query. The incremental
+goal construction feature allows the SAT solver to be invoked at
+intermediate points during symbolic execution, enabling early detection
+of property violations and concurrent solver execution.
+
+## Algorithm
+
+The standard `convert_assertions` builds a single disjunction:
+
+    NOT(a1) OR NOT(a2) OR ... OR NOT(aN)
+
+where each `ai` is an assertion condition (under its path assumption).
+The solver checks whether any assertion can fail.
+
+The incremental variant (`convert_assertions_incremental`) adds a free
+"goal extender" variable `v` to make the disjunction extensible:
+
+    NOT(a1) OR NOT(a2) OR ... OR v
+
+The solver is called with the assumption `NOT(v)`, which effectively
+closes the disjunction. On the next call (after more symex steps
+produce new assertions), a new clause links to the previous extender:
+
+    NOT(v) OR NOT(a3) OR NOT(a4) OR ... OR v2
+
+With assumption `NOT(v2)`, the solver now checks all assertions from
+both batches. The chain of extender variables allows arbitrary
+incremental extension without rebuilding earlier clauses.
+
+## Components
+
+### `symex_target_equationt::convert_assertions_incremental`
+
+Core algorithm in `src/goto-symex/symex_target_equation.cpp`. Tracks:
+- `current_goal_extender`: the latest extender variable
+- `incremental_last_converted`: iterator to resume from
+- `incremental_assumption`: accumulated path assumptions
+
+### `periodic_incremental_symex_checker`
+
+In `src/goto-checker/`. Subclasses `symex_bmct` to count symex steps
+and pause every N steps (set via `--incremental-check-interval`).
+The main loop alternates between symex and solver invocations.
+
+### `concurrent_incremental_symex_checker`
+
+In `src/goto-checker/`. Runs symex in a separate thread. Uses
+mutex + condition variable for handoff: symex pauses and sets
+`symex_paused=true`, the solver thread processes the equation, then
+sets `solver_done=true` to resume symex. The equation is only accessed
+by one thread at a time (no concurrent reads/writes).
+
+## Usage
+
+    # Check every 50 symex steps:
+    cbmc program.c --incremental-check-interval 50
+
+    # Same, but with concurrent symex and solving:
+    cbmc program.c --incremental-check-interval 50 --concurrent-incremental
+
+    # With the existing incremental-loop mode:
+    cbmc program.c --incremental-loop main.0 --unwind-max 20
+
+## Limitations
+
+- The incremental check interval is measured in symex steps, not
+  assertions. A small interval increases solver overhead; a large
+  interval reduces the benefit of early detection.
+- The concurrent mode uses a single solver thread. The symex thread
+  is blocked while the solver runs (and vice versa), so the speedup
+  comes from overlapping symex work with solver work, not from
+  parallel solving.

doc/man/cbmc.1

@@ -424,6 +424,23 @@ stop incremental\-loop after nr unwindings
 do not check properties before unwind\-min
 when using incremental\-loop
 .TP
+\fB\-\-incremental\-check\-interval\fR N
+invoke the SAT solver every N symbolic execution steps to check
+assertions discovered so far, using incremental goal construction
+to avoid rebuilding the assertion disjunction from scratch.
+Can find property violations before symbolic execution completes.
+.TP
+\fB\-\-concurrent\-incremental\fR
+run symbolic execution and SAT solving concurrently in separate
+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

@@ -339,6 +339,22 @@ stop incremental\-loop after nr unwindings
 do not check properties before unwind\-min
 when using incremental\-loop
 .TP
+\fB\-\-incremental\-check\-interval\fR N
+invoke the SAT solver every N symbolic execution steps to check
+assertions discovered so far, using incremental goal construction.
+Can find property violations before symbolic execution completes.
+.TP
+\fB\-\-concurrent\-incremental\fR
+run symbolic execution and SAT solving concurrently in separate
+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

jbmc/src/jbmc/Makefile

@@ -43,7 +43,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
 
 INCLUDES= -I .. -I ../$(CPROVER_DIR)/src
 
-LIBS =
+LIBS = -lpthread
 
 include ../config.inc
 include ../$(CPROVER_DIR)/src/config.inc

jbmc/unit/Makefile

@@ -133,6 +133,8 @@ N_CATCH_TESTS = $(shell \
                   cat $$(find . -name "*.cpp" ) | \
                   grep -c -E "(SCENARIO|TEST_CASE)")
 
+LIBS = -lpthread
+
 CLEANFILES = $(CATCH_TEST) java-testing-utils/java-testing-utils$(LIBEXT)
 
 # only add a dependency for libraries to avoid triggering implicit rules, which

regression/cbmc-incr-oneloop/concurrent-check-fail1/main.c

@@ -0,0 +1,13 @@
+extern int nondet_int();
+int main()
+{
+  int x = nondet_int();
+  __CPROVER_assume(0 <= x && x <= 5);
+  int sum = 0;
+  while(x > 0)
+  {
+    sum = sum + x;
+    x = x - 1;
+  }
+  assert(sum <= 10);
+}

regression/cbmc-incr-oneloop/concurrent-check-fail1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--no-standard-checks --concurrent-incremental --incremental-check-interval 15 --unwinding-assertions --unwind 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-incr-oneloop/concurrent-check1/main.c

@@ -0,0 +1,16 @@
+extern int nondet_int();
+int main()
+{
+  int x = nondet_int();
+  __CPROVER_assume(0 <= x && x <= 10);
+  int y = 0;
+  while(x > 0)
+  {
+    y = y + 1;
+    x = x - 1;
+    assert(y >= 1);
+    assert(x >= 0);
+  }
+  assert(y >= 0);
+  assert(x == 0);
+}

regression/cbmc-incr-oneloop/concurrent-check1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--no-standard-checks --concurrent-incremental --incremental-check-interval 20 --unwinding-assertions --unwind 15
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-incr-oneloop/early-detection1/main.c

@@ -0,0 +1,29 @@
+// Test that incremental checking detects failures before symex completes.
+extern int nondet_int();
+
+int compute(int *arr, int n)
+{
+  int sum = 0;
+  for(int i = 0; i < n; i++)
+  {
+    sum += arr[i];
+    assert(sum < 1000000);
+  }
+  return sum;
+}
+
+int main()
+{
+  int n = nondet_int();
+  __CPROVER_assume(n >= 1 && n <= 50);
+
+  int arr[50];
+  for(int i = 0; i < 50; i++)
+  {
+    arr[i] = nondet_int();
+    __CPROVER_assume(arr[i] >= 0 && arr[i] <= 100000);
+  }
+
+  int result = compute(arr, n);
+  assert(result >= 0);
+}

regression/cbmc-incr-oneloop/early-detection1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--no-standard-checks --incremental-check-interval 100 --unwinding-assertions --unwind 55
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Test that incremental checking finds the failure before symex completes

regression/cbmc-incr-oneloop/equivalence-check1/main.c

@@ -0,0 +1,21 @@
+extern int nondet_int();
+int main()
+{
+  int x = nondet_int();
+  __CPROVER_assume(0 <= x && x <= 8);
+  int sum = 0;
+  int count = 0;
+  while(x > 0)
+  {
+    sum = sum + x;
+    count = count + 1;
+    x = x - 1;
+    assert(count >= 1);   // always true
+    assert(sum >= count); // always true
+    assert(x >= 0);       // always true
+  }
+  assert(count <= 8); // always true
+  assert(sum <= 36);  // always true (max: 8+7+...+1 = 36)
+  assert(sum <= 10);  // FAILS for x >= 5
+  assert(x == 0);     // always true
+}

regression/cbmc-incr-oneloop/equivalence-check1/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--no-standard-checks --incremental-check-interval 10 --unwinding-assertions --unwind 10
+^EXIT=10$
+^SIGNAL=0$
+\[main\.assertion\.1\] .* count >= 1: SUCCESS
+\[main\.assertion\.2\] .* sum >= count: SUCCESS
+\[main\.assertion\.3\] .* x >= 0: SUCCESS
+\[main\.assertion\.4\] .* count <= 8: SUCCESS
+\[main\.assertion\.5\] .* sum <= 36: SUCCESS
+\[main\.assertion\.6\] .* sum <= 10: FAILURE
+\[main\.assertion\.7\] .* x == 0: SUCCESS
+--
+^warning: ignoring
+--
+Verify incremental checking produces identical verdicts to non-incremental

regression/cbmc-incr-oneloop/incremental-goals1/main.c

@@ -0,0 +1,12 @@
+extern int nondet_int();
+int main()
+{
+  int x = nondet_int();
+  __CPROVER_assume(0 <= x && x <= 1);
+  while(x < 5)
+  {
+    x = x + 1;
+    assert(x <= 5);
+  }
+  assert(x == 5);
+}

regression/cbmc-incr-oneloop/incremental-goals1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--no-standard-checks --incremental-loop main.0 --unwinding-assertions --unwind-max 10
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-incr-oneloop/periodic-check-fail1/main.c

@@ -0,0 +1,13 @@
+extern int nondet_int();
+int main()
+{
+  int x = nondet_int();
+  __CPROVER_assume(0 <= x && x <= 5);
+  int sum = 0;
+  while(x > 0)
+  {
+    sum = sum + x;
+    x = x - 1;
+  }
+  assert(sum <= 10);
+}

regression/cbmc-incr-oneloop/periodic-check-fail1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--no-standard-checks --incremental-check-interval 15 --unwinding-assertions --unwind 10
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-incr-oneloop/periodic-check1/main.c

@@ -0,0 +1,16 @@
+extern int nondet_int();
+int main()
+{
+  int x = nondet_int();
+  __CPROVER_assume(0 <= x && x <= 10);
+  int y = 0;
+  while(x > 0)
+  {
+    y = y + 1;
+    x = x - 1;
+    assert(y >= 1);
+    assert(x >= 0);
+  }
+  assert(y >= 0);
+  assert(x == 0);
+}

regression/cbmc-incr-oneloop/periodic-check1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--no-standard-checks --incremental-check-interval 20 --unwinding-assertions --unwind 15
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring