Fix multiple bugs in loop acceleration by tautschnig · Pull Request #8874 · diffblue/cbmc

tautschnig · 2026-03-17T17:56:45Z

The loop accelerator (goto-instrument --accelerate) has been largely non-functional due to several interacting bugs. This PR fixes four root causes and promotes 11 previously-KNOWNBUG regression tests to CORE.

Bug fixes:

Swapped conditions in path enumerator (sat_path_enumerator::build_fixed): Forward-jump conditions were inverted — jumps outside the loop were treated as within-loop and vice versa. Additionally, modifying fixedt->targets while iterating over t->targets lost multi-target GOTO information. Fixed by correcting the condition logic and collecting target decisions before mutation.
Symex depth limit of 0 in scratch programs: scratch_programt::get_default_options() did not set the depth option, causing symex_configt::max_depth to default to 0. This killed all paths after the first instruction, making SAT-based path enumeration and polynomial fitting completely non-functional. Fixed by setting depth to UINT_MAX.
Wrong coefficient parsing in polynomial extraction: extract_polynomial() used binary2integer() to parse coefficient values, but constant_exprt stores values in bvrep format (hex via integer2bvrep), not binary. This caused coefficient 1 to be misread as -1 and coefficient 2 to be parsed as 0. Fixed by using bvrep2integer().
False overflow rejection for unsigned targets: The polynomial fitting overflow check rejected negative signed coefficients when cast to unsigned, blocking acceleration of decrementing loops (e.g., x -= 2). Since unsigned wrapping is well-defined, the overflow check is skipped for unsigned target variables.

Test changes:

10 KNOWNBUG acceleration tests promoted to CORE
4 array_safe tests promoted to CORE with smt-backend tag (require Z3 for quantified array reasoning)
simple_unsafe4 (decrementing unsigned loop) promoted to CORE
nested_unsafe1 documented as KNOWNBUG because the accelerator only handles innermost loops

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

…enumerator In sat_path_enumerator::build_fixed(), the conditions for forward jumps were inverted: !loop.contains(target) (target outside loop) was treated as 'within the loop' and vice versa. Additionally, modifying fixedt->targets while iterating over t->targets caused loss of multi-target GOTO information. Fix by: 1. Correcting the condition: forward jumps outside the loop are killed, forward jumps within the loop are kept. 2. Collecting all target decisions before modifying fixedt->targets. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

scratch_programt::get_default_options() did not set the 'depth' option, causing symex_configt::max_depth to default to 0. This made symex kill all paths after the very first instruction, rendering the entire SAT-based path enumeration and polynomial fitting non-functional. Set depth to UINT_MAX so scratch programs can be fully explored. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

extract_polynomial() used binary2integer() to parse coefficient values, but constant_exprt stores bitvector values in bvrep format (hexadecimal strings via integer2bvrep), not binary strings. This caused coefficient 1 to be interpreted as signed 1-bit binary (-1) and coefficient 2 to be parsed as invalid binary (0), producing completely wrong polynomials. Fix by using bvrep2integer() which correctly handles the bvrep format. Also switch the scratch program's decision procedure back to the SAT solver (bv_pointerst) from Z3 (smt2_dect). Promotes 10 KNOWNBUG acceleration tests to CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

The polynomial fitting overflow check rejected negative signed coefficients when cast to unsigned, preventing acceleration of decrementing loops like 'x -= 2'. For unsigned target variables, wrapping arithmetic is well-defined, so the overflow check on the polynomial expression is unnecessary. Promotes simple_unsafe4 (decrementing unsigned loop) to CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Array-safe tests require Z3 (smt-backend tag) since proving correctness requires the quantified array constraints to be interpreted. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

The loop accelerator only handles innermost loops. The outer loop contains a nested inner loop, so it is skipped. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Copilot

Pull request overview

Fixes several root causes that made goto-instrument --accelerate largely non-functional, and promotes multiple previously-KNOWNBUG regression tests to CORE.

Changes:

Fixes loop path “fixed edge” rewriting, symex default depth configuration, and polynomial coefficient decoding.
Adjusts polynomial fitting overflow handling for unsigned targets.
Promotes multiple acceleration/array regression tests (and documents one remaining limitation).

Reviewed changes

Copilot reviewed 21 out of 21 changed files in this pull request and generated 6 comments.

Show a summary per file

File	Description
src/goto-instrument/accelerate/scratch_program.h	Changes the default decision procedure used by scratch programs.
src/goto-instrument/accelerate/scratch_program.cpp	Sets a non-zero default symex depth (effectively “unlimited”).
src/goto-instrument/accelerate/sat_path_enumerator.cpp	Reworks target handling when rewriting GOTOs in the fixed program.
src/goto-instrument/accelerate/polynomial_accelerator.cpp	Skips overflow assumptions when the acceleration target is unsigned.
src/goto-instrument/accelerate/acceleration_utils.cpp	Fixes coefficient parsing by decoding BV “bvrep” correctly.
regression/acceleration/simple_unsafe4/test.desc	Promotes test from KNOWNBUG to CORE.
regression/acceleration/simple_unsafe1/test.desc	Promotes test from KNOWNBUG to CORE.
regression/acceleration/phases_unsafe1/test.desc	Promotes test from KNOWNBUG to CORE.
regression/acceleration/overflow_unsafe1/test.desc	Promotes test from KNOWNBUG to CORE.
regression/acceleration/nested_unsafe1/test.desc	Documents why this test remains a KNOWNBUG scenario (nested loops).
regression/acceleration/functions_unsafe1/test.desc	Promotes test from KNOWNBUG to CORE.
regression/acceleration/diamond_unsafe1/test.desc	Promotes test from KNOWNBUG to CORE.
regression/acceleration/const_unsafe1/test.desc	Promotes test from KNOWNBUG to CORE.
regression/acceleration/array_unsafe4/test.desc	Promotes test from KNOWNBUG to CORE.
regression/acceleration/array_unsafe3/test.desc	Promotes test from KNOWNBUG to CORE.
regression/acceleration/array_unsafe2/test.desc	Promotes test from KNOWNBUG to CORE.
regression/acceleration/array_unsafe1/test.desc	Promotes test from KNOWNBUG to CORE.
regression/acceleration/array_safe4/test.desc	Tags as `smt-backend` and runs with Z3 + adjusted flags.
regression/acceleration/array_safe3/test.desc	Tags as `smt-backend` and runs with Z3 + adjusted flags.
regression/acceleration/array_safe2/test.desc	Tags as `smt-backend` and runs with Z3 + adjusted flags.
regression/acceleration/array_safe1/test.desc	Tags as `smt-backend` and runs with Z3 + adjusted flags.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

src/goto-instrument/accelerate/sat_path_enumerator.cpp

+      goto_programt::targetst new_targets;
+      bool dominated_by_kill = false;
+
      for(const auto &target : t->targets)
      {
        if(target->location_number > t->location_number)
        {
          // A forward jump...
          if(!loop.contains(target))
          {
-            // Case 1: a forward jump within the loop.  Do nothing.
-            continue;
-          }
-          else
-          {
-            // Case 2: a forward jump out of the loop.  Kill.
-            fixedt->targets.clear();
-            fixedt->targets.push_back(kill);
+            // A forward jump out of the loop.  Kill.
+            dominated_by_kill = true;
          }
+          // else: a forward jump within the loop.  Keep original target.
        }
        else
        {
          // A backwards jump...
-          if(target==loop_header)
+          if(target == loop_header)
          {
-            // Case 3: a backwards jump to the loop header.  Redirect
-            // to sentinel.
-            fixedt->targets.clear();
-            fixedt->targets.push_back(end);
+            // A backwards jump to the loop header.  Redirect to sentinel.
+            new_targets.push_back(end);
          }
          else
          {
-            // Case 4: a nested loop.  Kill.
-            fixedt->targets.clear();
-            fixedt->targets.push_back(kill);
+            // A nested loop.  Kill.
+            dominated_by_kill = true;
          }
        }
      }


src/goto-instrument/accelerate/sat_path_enumerator.cpp

+      else if(!new_targets.empty())
+      {
+        fixedt->targets = new_targets;
+      }


src/goto-instrument/accelerate/acceleration_utils.cpp

+    mp_integer mp = bvrep2integer(
+      concrete_term.get_value(),
+      to_bitvector_type(concrete_term.type()).get_width(),
+      true);


src/goto-instrument/accelerate/polynomial_accelerator.cpp

  overflow.overflow_expr(rhs, overflow_expr);

-  program.add(goto_programt::make_assumption(not_exprt(overflow_expr)));
+  if(target.type().id() != ID_unsignedbv)


src/goto-instrument/accelerate/scratch_program.h

      satchecker(ns, *satcheck, mh),
      z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3, "", mh),
-      checker(&z3) // checker(&satchecker)
+      checker(&satchecker)


regression/acceleration/array_safe1/test.desc

 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--


codecov · 2026-03-17T18:58:34Z

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.97%. Comparing base (85c204f) to head (b1bf383).

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8874      +/-   ##
===========================================
+ Coverage    80.41%   80.97%   +0.56%     
===========================================
  Files         1703     1703              
  Lines       188398   188404       +6     
  Branches        73       73              
===========================================
+ Hits        151498   152561    +1063     
+ Misses       36900    35843    -1057

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

tautschnig and others added 6 commits March 17, 2026 17:11

Promote array_safe acceleration tests to CORE using Z3

edcb91c

Array-safe tests require Z3 (smt-backend tag) since proving correctness requires the quantified array constraints to be interpreted. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Document nested_unsafe1 KNOWNBUG reason

b1bf383

The loop accelerator only handles innermost loops. The outer loop contains a nested inner loop, so it is skipped. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

tautschnig requested review from kroening, martin-cs and peterschrammel as code owners March 17, 2026 17:56

Copilot AI review requested due to automatic review settings March 17, 2026 17:56

tautschnig self-assigned this Mar 17, 2026

Copilot AI reviewed Mar 17, 2026

View reviewed changes

Copilot started reviewing on behalf of tautschnig March 17, 2026 18:56 View session

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix multiple bugs in loop acceleration#8874

Fix multiple bugs in loop acceleration#8874
tautschnig wants to merge 6 commits intodiffblue:developfrom
tautschnig:test-coverage/loop-acceleration

tautschnig commented Mar 17, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

codecov bot commented Mar 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

tautschnig commented Mar 17, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

codecov bot commented Mar 17, 2026

Codecov Report

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants