Merge pull request #7024 from tautschnig/bugfixes/value_set-shift

Value sets: track pointers through shifts

Author: tautschnig

regression/cbmc/Pointer2/main.c

@@ -0,0 +1,10 @@
+int main()
+{
+  int x;
+  unsigned long long x_i;
+  _Static_assert(sizeof(&x) == sizeof(x_i), "pointer width");
+  __CPROVER_assert(((unsigned long long)&x & 0x1ULL) == 0, "LSB is zero");
+  x_i = (unsigned long long)&x >> 1;
+  x_i <<= 1;
+  __CPROVER_assert(*(int *)x_i == x, "pointer to x is tracked through shifts");
+}

regression/cbmc/Pointer2/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Value sets must also track pointers the integer conversion of which is subject
+to shifts (just like we already tracked them through other bit operations).

src/pointer-analysis/value_set.cpp

@@ -760,6 +760,24 @@ void value_sett::get_value_set_rec(
       insert(dest, it->first, offset);
     }
   }
+  else if(expr.id() == ID_lshr || expr.id() == ID_ashr || expr.id() == ID_shl)
+  {
+    const binary_exprt &binary_expr = to_binary_expr(expr);
+
+    object_mapt pointer_expr_set;
+    get_value_set_rec(
+      binary_expr.op0(), pointer_expr_set, "", binary_expr.op0().type(), ns);
+
+    for(const auto &object_map_entry : pointer_expr_set.read())
+    {
+      offsett offset = object_map_entry.second;
+
+      // kill any offset
+      offset.reset();
+
+      insert(dest, object_map_entry.first, offset);
+    }
+  }
   else if(expr.id()==ID_side_effect)
   {
     const irep_idt &statement = to_side_effect_expr(expr).get_statement();