Fix multiple bugs in loop acceleration

regression/acceleration/array_safe1/test.desc

@@ -1,6 +1,7 @@
-CORE
+CORE smt-backend
 main.c
---no-unwinding-assertions
+--no-unwinding-assertions --z3 --no-bounds-check --no-signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--

regression/acceleration/array_safe2/test.desc

@@ -1,6 +1,7 @@
-CORE
+CORE smt-backend
 main.c
---no-unwinding-assertions
+--no-unwinding-assertions --z3 --no-bounds-check --no-signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--

regression/acceleration/array_safe3/test.desc

@@ -1,6 +1,7 @@
-CORE
+CORE smt-backend
 main.c
---no-unwinding-assertions
+--no-unwinding-assertions --z3 --no-bounds-check --no-signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--

regression/acceleration/array_safe4/test.desc

@@ -1,6 +1,7 @@
-CORE
+CORE smt-backend
 main.c
---no-unwinding-assertions
+--no-unwinding-assertions --z3 --no-bounds-check --no-signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--

regression/acceleration/array_unsafe1/test.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
-The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/array_unsafe2/test.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
-The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/array_unsafe3/test.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
-The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/array_unsafe4/test.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
-The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/const_unsafe1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$

regression/acceleration/diamond_unsafe1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$

regression/acceleration/functions_unsafe1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$

regression/acceleration/nested_unsafe1/test.desc

@@ -5,4 +5,8 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
-The result spuriously is VERIFICATION SUCCESSFUL.
+The loop accelerator only handles innermost loops. The outer loop
+(while x < 0x0fffffff) contains a nested inner loop (while y < 10),
+so it is skipped by the contains_nested_loops check in accelerate_loop.
+Only the inner loop is accelerated, which is insufficient to reach the
+assertion after the outer loop within the --unwind bound.

regression/acceleration/overflow_unsafe1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$

regression/acceleration/phases_unsafe1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$

regression/acceleration/simple_unsafe1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$

regression/acceleration/simple_unsafe4/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --no-unwinding-assertions
 ^EXIT=10$

src/goto-instrument/accelerate/acceleration_utils.cpp

@@ -1209,7 +1209,10 @@ void acceleration_utilst::extract_polynomial(
     constant_exprt concrete_term=to_constant_expr(program.eval(coefficient));
     std::map<exprt, int> degrees;
 
-    mp_integer mp=binary2integer(concrete_term.get_value().c_str(), true);
+    mp_integer mp = bvrep2integer(
+      concrete_term.get_value(),
+      to_bitvector_type(concrete_term.type()).get_width(),
+      true);
     monomial.coeff = numeric_cast_v<int>(mp);
 
     if(monomial.coeff==0)

src/goto-instrument/accelerate/polynomial_accelerator.cpp

@@ -589,7 +589,8 @@ void polynomial_acceleratort::assert_for_values(
   exprt overflow_expr;
   overflow.overflow_expr(rhs, overflow_expr);
 
-  program.add(goto_programt::make_assumption(not_exprt(overflow_expr)));
+  if(target.type().id() != ID_unsignedbv)
+    program.add(goto_programt::make_assumption(not_exprt(overflow_expr)));
 
   rhs=typecast_exprt(rhs, target.type());
 

src/goto-instrument/accelerate/sat_path_enumerator.cpp

@@ -274,41 +274,50 @@ void sat_path_enumeratort::build_fixed()
       // header we're happy & redirect it to our end-of-body sentinel.
       // If it jumps somewhere else, it's part of a nested loop and we
       // kill it.
+      //
+      // We handle all targets at once to avoid invalidating the fixed
+      // copy's target list while iterating over the original's targets.
+      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;
           }
         }
       }
+
+      if(dominated_by_kill)
+      {
+        fixedt->targets.clear();
+        fixedt->targets.push_back(kill);
+      }
+      else if(!new_targets.empty())
+      {
+        fixedt->targets = new_targets;
+      }
+      // else: all targets are forward jumps within the loop, keep as-is
     }
   }
 

src/goto-instrument/accelerate/scratch_program.cpp

@@ -11,6 +11,8 @@ Author: Matt Lewis
 
 #include "scratch_program.h"
 
+#include <limits>
+
 #include <solvers/decision_procedure.h>
 
 #include <goto-symex/slice.h>
@@ -220,5 +222,6 @@ optionst scratch_programt::get_default_options()
 {
   optionst ret;
   ret.set_option("simplify", true);
+  ret.set_option("depth", std::numeric_limits<unsigned>::max());
   return ret;
 }

src/goto-instrument/accelerate/scratch_program.h

@@ -75,7 +75,7 @@ class scratch_programt:public goto_programt
       satcheck(std::make_unique<satcheckt>(mh)),
       satchecker(ns, *satcheck, mh),
       z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3, "", mh),
-      checker(&z3) // checker(&satchecker)
+      checker(&satchecker)
   {
   }