Value set: lift offset from numeric constants to expressions

We can safely track arbitrary expressions as pointer offsets rather than
limit ourselves to just constant offsets (and then treating all other
expressions as "unknown").

Author: tautschnig

regression/cbmc/array-cell-sensitivity11/test.desc

@@ -5,7 +5,6 @@ main::1::array!0@1#2\[\[0\]\]..y =
 ^EXIT=0$
 ^SIGNAL=0$
 --
-main::1::array!0@1#[2-9]\[\[[1-9]\]\]
 main::1::array!0@1#[3-9]\[\[[0-9]\]\]
 --
 This checks that an array access made via a pointer to a member of the array's

regression/cbmc/array-cell-sensitivity7/test.desc

@@ -15,7 +15,6 @@ main::1::array!0@1#3\[\[0\]\] =
 ^SIGNAL=0$
 --
 main::1::array!0@1#[2-9]\[[0-9]+\]
-main::1::array!0@1#3\[\[[1-9]\]\] =
 --
 This checks that a write with a non-constant index leads to a whole-array
 operation followed by expansion into individual array cells, while a write with

regression/cbmc/array-cell-sensitivity8/test.desc

@@ -10,7 +10,7 @@ main::1::array!0@1#2\[\[6\]\] =
 main::1::array!0@1#2\[\[7\]\] =
 main::1::array!0@1#2\[\[8\]\] =
 main::1::array!0@1#2\[\[9\]\] =
-main::1::array!0@1#3 =.*byte_extract_(big|little)_endian
+main::1::array!0@1#3 =.*byte_update_(big|little)_endian
 main::1::array!0@1#3\[\[0\]\] =
 main::1::array!0@1#3\[\[1\]\] =
 main::1::array!0@1#3\[\[2\]\] =

src/pointer-analysis/value_set.cpp

@@ -28,9 +28,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/xml.h>
 
 #ifdef DEBUG
-#include <iostream>
-#include <util/format_expr.h>
-#include <util/format_type.h>
+#  include <iostream>
 #endif
 
 #include "add_failed_symbols.h"
@@ -184,7 +182,7 @@ void value_sett::output(std::ostream &out, const std::string &indent) const
         stream << "<" << format(o) << ", ";
 
         if(o_it->second)
-          stream << *o_it->second;
+          stream << format(*o_it->second);
         else
           stream << '*';
 
@@ -261,7 +259,7 @@ exprt value_sett::to_expr(const object_map_dt::value_type &it) const
   od.object()=object;
 
   if(it.second)
-    od.offset() = from_integer(*it.second, c_index_type());
+    od.offset() = *it.second;
 
   od.type()=od.object().type();
 
@@ -352,7 +350,7 @@ bool value_sett::eval_pointer_offset(
         it=object_map.begin();
         it!=object_map.end();
         it++)
-      if(!it->second)
+      if(!it->second || !it->second->is_constant())
         return false;
       else
       {
@@ -362,7 +360,8 @@ bool value_sett::eval_pointer_offset(
         if(!ptr_offset.has_value())
           return false;
 
-        *ptr_offset += *it->second;
+        *ptr_offset +=
+          numeric_cast_v<mp_integer>(to_constant_expr(*it->second));
 
         if(mod && *ptr_offset != previous_offset)
           return false;
@@ -623,7 +622,7 @@ void value_sett::get_value_set_rec(
       insert(
         dest,
         exprt(ID_null_object, to_pointer_type(expr.type()).base_type()),
-        mp_integer{0});
+        from_integer(0, c_index_type()));
     }
     else if(
       expr.type().id() == ID_unsignedbv || expr.type().id() == ID_signedbv)
@@ -655,7 +654,10 @@ void value_sett::get_value_set_rec(
 
       if(op.is_zero())
       {
-        insert(dest, exprt(ID_null_object, empty_typet{}), mp_integer{0});
+        insert(
+          dest,
+          exprt(ID_null_object, empty_typet{}),
+          from_integer(0, c_index_type()));
       }
       else
       {
@@ -696,15 +698,14 @@ void value_sett::get_value_set_rec(
       throw expr.id_string()+" expected to have at least two operands";
 
     object_mapt pointer_expr_set;
-    std::optional<mp_integer> i;
+    std::optional<exprt> additional_offset;
 
     // special case for plus/minus and exactly one pointer
     std::optional<exprt> ptr_operand;
     if(
       expr.type().id() == ID_pointer &&
       (expr.id() == ID_plus || expr.id() == ID_minus))
     {
-      bool non_const_offset = false;
       for(const auto &op : expr.operands())
       {
         if(op.type().id() == ID_pointer)
@@ -717,24 +718,20 @@ void value_sett::get_value_set_rec(
 
           ptr_operand = op;
         }
-        else if(!non_const_offset)
+        else
         {
-          auto offset = numeric_cast<mp_integer>(op);
-          if(!offset.has_value())
-          {
-            i.reset();
-            non_const_offset = true;
-          }
+          if(!additional_offset.has_value())
+            additional_offset = op;
           else
           {
-            if(!i.has_value())
-              i = mp_integer{0};
-            i = *i + *offset;
+            additional_offset = plus_exprt{
+              *additional_offset,
+              typecast_exprt::conditional_cast(op, additional_offset->type())};
           }
         }
       }
 
-      if(ptr_operand.has_value() && i.has_value())
+      if(ptr_operand.has_value() && additional_offset.has_value())
       {
         typet pointer_base_type =
           to_pointer_type(ptr_operand->type()).base_type();
@@ -745,18 +742,22 @@ void value_sett::get_value_set_rec(
 
         if(!size.has_value() || (*size) == 0)
         {
-          i.reset();
+          additional_offset.reset();
         }
         else
         {
-          *i *= *size;
+          additional_offset = mult_exprt{
+            *additional_offset, from_integer(*size, additional_offset->type())};
 
           if(expr.id()==ID_minus)
           {
             DATA_INVARIANT(
               to_minus_expr(expr).lhs() == *ptr_operand,
               "unexpected subtraction of pointer from integer");
-            i->negate();
+            DATA_INVARIANT(
+              additional_offset->type().id() != ID_unsignedbv,
+              "offset type must support negation");
+            additional_offset = unary_minus_exprt{*additional_offset};
           }
         }
       }
@@ -790,8 +791,12 @@ void value_sett::get_value_set_rec(
       offsett offset = it->second;
 
       // adjust by offset
-      if(offset && i.has_value())
-        *offset += *i;
+      if(offset && additional_offset.has_value())
+      {
+        offset = plus_exprt{
+          *offset,
+          typecast_exprt::conditional_cast(*additional_offset, offset->type())};
+      }
       else
         offset.reset();
 
@@ -871,7 +876,7 @@ void value_sett::get_value_set_rec(
       dynamic_object.set_instance(location_number);
       dynamic_object.valid()=true_exprt();
 
-      insert(dest, dynamic_object, mp_integer{0});
+      insert(dest, dynamic_object, from_integer(0, c_index_type()));
     }
     else if(statement==ID_cpp_new ||
             statement==ID_cpp_new_array)
@@ -884,7 +889,7 @@ void value_sett::get_value_set_rec(
       dynamic_object.set_instance(location_number);
       dynamic_object.valid()=true_exprt();
 
-      insert(dest, dynamic_object, mp_integer{0});
+      insert(dest, dynamic_object, from_integer(0, c_index_type()));
     }
     else
       insert(dest, exprt(ID_unknown, original_type));
@@ -1336,7 +1341,7 @@ void value_sett::get_reference_set_rec(
       to_array_type(expr.type()).element_type().id() == ID_array)
       insert(dest, expr);
     else
-      insert(dest, expr, mp_integer{0});
+      insert(dest, expr, from_integer(0, c_index_type()));
 
     return;
   }
@@ -1365,7 +1370,7 @@ void value_sett::get_reference_set_rec(
 
     const index_exprt &index_expr=to_index_expr(expr);
     const exprt &array=index_expr.array();
-    const exprt &offset=index_expr.index();
+    const exprt &index = index_expr.index();
 
     DATA_INVARIANT(
       array.type().id() == ID_array, "index takes array-typed operand");
@@ -1393,22 +1398,22 @@ void value_sett::get_reference_set_rec(
           from_integer(0, c_index_type()));
 
         offsett o = a_it->second;
-        const auto i = numeric_cast<mp_integer>(offset);
 
-        if(offset.is_zero())
-        {
-        }
-        else if(i.has_value() && o)
+        if(!index.is_zero() && o.has_value())
         {
           auto size = pointer_offset_size(array_type.element_type(), ns);
 
           if(!size.has_value() || *size == 0)
             o.reset();
           else
-            *o = *i * (*size);
+          {
+            o = plus_exprt{
+              *o,
+              typecast_exprt::conditional_cast(
+                mult_exprt{index, from_integer(*size, index.type())},
+                o->type())};
+          }
         }
-        else
-          o.reset();
 
         insert(dest, deref_index_expr, o);
       }

src/pointer-analysis/value_set.h

@@ -76,9 +76,9 @@ class value_sett
   /// in value sets.
   static object_numberingt object_numbering;
 
-  /// Represents the offset into an object: either a unique integer offset,
-  /// or an unknown value, represented by `!offset`.
-  typedef std::optional<mp_integer> offsett;
+  /// Represents the offset into an object: either some (possibly constant)
+  /// expression, or an unknown value, represented by `!offset`.
+  typedef std::optional<exprt> offsett;
 
   /// Represents a set of expressions (`exprt` instances) with corresponding
   /// offsets (`offsett` instances). This is the RHS set of a single row of
@@ -140,20 +140,6 @@ class value_sett
     return insert(dest, object_numbering.number(src), offsett());
   }
 
-  /// Adds an expression to an object map, with known offset. If the
-  /// destination map has an existing element for the same expression
-  /// with a differing offset its offset is marked unknown.
-  /// \param dest: object map to update
-  /// \param src: expression to add
-  /// \param offset_value: offset into `src`
-  bool insert(
-    object_mapt &dest,
-    const exprt &src,
-    const mp_integer &offset_value) const
-  {
-    return insert(dest, object_numbering.number(src), offsett(offset_value));
-  }
-
   /// Adds a numbered expression and offset to an object map. If the
   /// destination map has an existing element for the same expression
   /// with a differing offset its offset is marked unknown.