Merge pull request #7337 from diffblue/smt2-pointer-plus

SMT2: fix pointer arithmetic

Author: tautschnig

regression/cbmc/Pointer24/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc/pointer-overflow3/no-simplify.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-overflow-check --no-simplify
 ^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE

src/solvers/smt2/smt2_conv.cpp

@@ -3644,21 +3644,35 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
         element_size = *element_size_opt;
       }
 
-      out << "(bvadd ";
+      // First convert the pointer operand
+      out << "(let ((?pointerop ";
       convert_expr(p);
-      out << " ";
+      out << ")) ";
+
+      // The addition is done on the offset part only.
+      const std::size_t pointer_width = boolbv_width(p.type());
+      const std::size_t offset_bits =
+        pointer_width - config.bv_encoding.object_bits;
+
+      out << "(concat ";
+      out << "((_ extract " << pointer_width - 1 << ' ' << offset_bits
+          << ") ?pointerop) ";
+      out << "(bvadd ((_ extract " << offset_bits - 1 << " 0) ?pointerop) ";
 
       if(element_size >= 2)
       {
-        out << "(bvmul ";
+        out << "(bvmul ((_ extract " << offset_bits - 1 << " 0) ";
         convert_expr(i);
-        out << " (_ bv" << element_size << " " << boolbv_width(expr.type())
-            << "))";
+        out << ") (_ bv" << element_size << " " << offset_bits << "))";
       }
       else
+      {
+        out << "((_ extract " << offset_bits - 1 << " 0) ";
         convert_expr(i);
+        out << ')'; // extract
+      }
 
-      out << ')';
+      out << ")))"; // bvadd, concat, let
     }
     else
     {