Value sets should permit any order of operands in pointer arithmetic

Previously, only <integer-constant> +/- pointer or
pointer-as-first-operand worked correctly. In all other cases, value
sets did not recurse on the correct operand.

Author: tautschnig

regression/cbmc/Pointer_Arithmetic19/main.c

@@ -0,0 +1,25 @@
+struct S
+{
+  int *p;
+  int s;
+};
+
+union U {
+  struct S st;
+  int i;
+};
+
+int main()
+{
+  int x;
+  int *ip = &x;
+
+  union U u;
+  u.st.p = ip;
+  u.st.s = 1;
+
+  int A[2] = {42, 43};
+  // the following should behave the same as "int *p = A + u.st.s;"
+  int *p = u.st.s + A;
+  assert(*p == 43);
+}

regression/cbmc/Pointer_Arithmetic19/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--program-only
+ASSERT\(\{ 42, 43 \}\[POINTER_OFFSET\(p!0@1#2\) / \d+l*\] == 43\)$
+^EXIT=0$
+^SIGNAL=0$
+--
+p\$object
+^warning: ignoring
+--
+Value sets should be sufficiently precise to infer that dereferencing p is an
+access into the array at some offset, and not an access into any other object
+(or perhaps the invalid object). If that were the case, the assert instruction
+would include "p$object," the absence of which we check for in the above.

regression/validate-trace-xml-schema/check.py

@@ -30,6 +30,7 @@
     ['show_properties1', 'test.desc'],
     # program-only instead of trace
     ['vla1', 'program-only.desc'],
+    ['Pointer_Arithmetic19', 'test.desc'],
     ['Quantifiers-simplify', 'simplify_not_forall.desc'],
     ['array-cell-sensitivity15', 'test.desc'],
     # these test for invalid command line handling

src/pointer-analysis/value_set.cpp

@@ -633,30 +633,45 @@ void value_sett::get_value_set_rec(
     object_mapt pointer_expr_set;
     optionalt<mp_integer> i;
 
-    // special case for pointer+integer
-
+    // special case for plus/minus and exactly one pointer
+    optionalt<exprt> ptr_operand;
     if(
-      expr.operands().size() == 2 && expr_type.id() == ID_pointer &&
+      expr_type.id() == ID_pointer &&
       (expr.id() == ID_plus || expr.id() == ID_minus))
     {
-      exprt ptr_operand;
-
-      if(
-        to_binary_expr(expr).op0().type().id() != ID_pointer &&
-        to_binary_expr(expr).op0().is_constant())
-      {
-        i = numeric_cast<mp_integer>(to_binary_expr(expr).op0());
-        ptr_operand = to_binary_expr(expr).op1();
-      }
-      else
+      bool non_const_offset = false;
+      for(const auto &op : expr.operands())
       {
-        i = numeric_cast<mp_integer>(to_binary_expr(expr).op1());
-        ptr_operand = to_binary_expr(expr).op0();
+        if(op.type().id() == ID_pointer)
+        {
+          if(ptr_operand.has_value())
+          {
+            ptr_operand.reset();
+            break;
+          }
+
+          ptr_operand = op;
+        }
+        else if(!non_const_offset)
+        {
+          auto offset = numeric_cast<mp_integer>(op);
+          if(!offset.has_value())
+          {
+            i.reset();
+            non_const_offset = true;
+          }
+          else
+          {
+            if(!i.has_value())
+              i = mp_integer{0};
+            i = *i + *offset;
+          }
+        }
       }
 
-      if(i.has_value())
+      if(ptr_operand.has_value() && i.has_value())
       {
-        typet pointer_sub_type=ptr_operand.type().subtype();
+        typet pointer_sub_type = ptr_operand->type().subtype();
         if(pointer_sub_type.id()==ID_empty)
           pointer_sub_type=char_type();
 
@@ -671,12 +686,20 @@ void value_sett::get_value_set_rec(
           *i *= *size;
 
           if(expr.id()==ID_minus)
+          {
+            DATA_INVARIANT(
+              to_minus_expr(expr).lhs() == *ptr_operand,
+              "unexpected subtraction of pointer from integer");
             i->negate();
+          }
         }
       }
+    }
 
+    if(ptr_operand.has_value())
+    {
       get_value_set_rec(
-        ptr_operand, pointer_expr_set, "", ptr_operand.type(), ns);
+        *ptr_operand, pointer_expr_set, "", ptr_operand->type(), ns);
     }
     else
     {