Simplify pointer_offset using value set

When all candidates in the value set have the same offset we can replace
a pointer_offset expression by the offset value found in the value set.

Author: tautschnig

regression/cbmc/pointer-offset-02/main.c

@@ -0,0 +1,7 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *p = malloc(sizeof(int));
+  __CPROVER_assert(__CPROVER_POINTER_OFFSET(p) == 0, "");
+}

regression/cbmc/pointer-offset-02/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--verbosity 8
+^Generated \d+ VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/goto-symex/simplify_expr_with_value_set.cpp

@@ -154,3 +154,58 @@ simplify_exprt::resultt<> simplify_expr_with_value_sett::simplify_inequality(
   else
     return unchanged(expr);
 }
+
+simplify_exprt::resultt<>
+simplify_expr_with_value_sett::simplify_pointer_offset(
+  const pointer_offset_exprt &expr)
+{
+  const exprt &ptr = expr.pointer();
+
+  if(ptr.type().id() != ID_pointer)
+    return unchanged(expr);
+
+  const ssa_exprt *ssa_symbol_expr = expr_try_dynamic_cast<ssa_exprt>(ptr);
+
+  if(!ssa_symbol_expr)
+    return simplify_exprt::simplify_pointer_offset(expr);
+
+  ssa_exprt l1_expr{*ssa_symbol_expr};
+  l1_expr.remove_level_2();
+  const std::vector<exprt> value_set_elements =
+    value_set.get_value_set(l1_expr, ns);
+
+  std::optional<exprt> offset;
+
+  for(const auto &value_set_element : value_set_elements)
+  {
+    if(
+      value_set_element.id() == ID_unknown ||
+      value_set_element.id() == ID_invalid ||
+      is_failed_symbol(
+        to_object_descriptor_expr(value_set_element).root_object()) ||
+      to_object_descriptor_expr(value_set_element).offset().id() == ID_unknown)
+    {
+      offset.reset();
+      break;
+    }
+
+    exprt this_offset = to_object_descriptor_expr(value_set_element).offset();
+    if(
+      this_offset.id() == ID_unknown ||
+      (offset.has_value() && this_offset != *offset))
+    {
+      offset.reset();
+      break;
+    }
+    else if(!offset.has_value())
+    {
+      offset = this_offset;
+    }
+  }
+
+  if(!offset.has_value())
+    return simplify_exprt::simplify_pointer_offset(expr);
+
+  return changed(
+    simplify_rec(typecast_exprt::conditional_cast(*offset, expr.type())));
+}

src/goto-symex/simplify_expr_with_value_set.h

@@ -26,6 +26,10 @@ class simplify_expr_with_value_sett : public simplify_exprt
 
   [[nodiscard]] resultt<>
   simplify_inequality(const binary_relation_exprt &) override;
+  /// When all candidates in the value set have the same offset we can replace a
+  /// pointer_offset expression by the offset value found in the value set.
+  [[nodiscard]] resultt<>
+  simplify_pointer_offset(const pointer_offset_exprt &) override;
 
 protected:
   const value_sett &value_set;

src/util/simplify_expr_class.h

@@ -203,7 +203,8 @@ class simplify_exprt
   [[nodiscard]] resultt<>
   simplify_dereference_preorder(const dereference_exprt &);
   [[nodiscard]] resultt<> simplify_address_of(const address_of_exprt &);
-  [[nodiscard]] resultt<> simplify_pointer_offset(const pointer_offset_exprt &);
+  [[nodiscard]] virtual resultt<>
+  simplify_pointer_offset(const pointer_offset_exprt &);
   [[nodiscard]] resultt<> simplify_bswap(const bswap_exprt &);
   [[nodiscard]] resultt<> simplify_isinf(const unary_exprt &);
   [[nodiscard]] resultt<> simplify_isnan(const unary_exprt &);