Remove good_pointer, good_pointer_def

good_pointer(ptr) is equivalent to __CPROVER_r_ok(ptr, sizeof(*ptr)).

Author: tautschnig

src/ansi-c/expr2c.cpp

@@ -4001,7 +4001,6 @@ optionalt<std::string> expr2ct::convert_function(const exprt &src)
     {ID_gcc_builtin_va_arg, "gcc_builtin_va_arg"},
     {ID_get_may, CPROVER_PREFIX "get_may"},
     {ID_get_must, CPROVER_PREFIX "get_must"},
-    {ID_good_pointer, "GOOD_POINTER"},
     {ID_ieee_float_equal, "IEEE_FLOAT_EQUAL"},
     {ID_ieee_float_notequal, "IEEE_FLOAT_NOTEQUAL"},
     {ID_infinity, "INFINITY"},

src/goto-instrument/contracts/utils.cpp

@@ -16,6 +16,7 @@ Date: September 2021
 #include <util/mathematical_expr.h>
 #include <util/message.h>
 #include <util/pointer_expr.h>
+#include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 #include <util/simplify_expr.h>
 #include <util/symbol.h>
@@ -85,9 +86,13 @@ exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
 {
   exprt::operandst validity_checks;
 
-  if(expr.id() == ID_dereference)
-    validity_checks.push_back(
-      good_pointer_def(to_dereference_expr(expr).pointer(), ns));
+  if(auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
+  {
+    const auto size_of_expr_opt = size_of_expr(expr.type(), ns);
+    CHECK_RETURN(size_of_expr_opt.has_value());
+
+    validity_checks.push_back(r_ok_exprt{deref->pointer(), *size_of_expr_opt});
+  }
 
   for(const auto &op : expr.operands())
     validity_checks.push_back(all_dereferences_are_valid(op, ns));

src/goto-instrument/contracts/utils.h

@@ -62,8 +62,8 @@ class havoc_assigns_targetst : public havoc_if_validt
 ///
 /// This function generates a formula:
 ///
-///   good_pointer_def(pexpr_1, ns) &&
-///   good_pointer_def(pexpr_2, n2) &&
+///   r_ok_exprt(pexpr_1, sizeof(*pexpr_1)) &&
+///   r_ok_exprt(pexpr_2, sizeof(*pexpr_1)) &&
 ///   ...
 ///
 /// over all dereferenced pointer expressions *(pexpr_1), *(pexpr_2), ...

src/util/irep_ids.def

@@ -461,7 +461,6 @@ IREP_ID_TWO(C_dynamic, #dynamic)
 IREP_ID_ONE(pointer_in_range)
 IREP_ID_ONE(object_size)
 IREP_ID_ONE(separate)
-IREP_ID_ONE(good_pointer)
 IREP_ID_ONE(live_object)
 IREP_ID_ONE(writeable_object)
 IREP_ID_ONE(integer_address)

src/util/pointer_predicates.cpp

@@ -56,34 +56,6 @@ exprt dead_object(const exprt &pointer, const namespacet &ns)
   return same_object(pointer, deallocated_symbol.symbol_expr());
 }
 
-exprt good_pointer(const exprt &pointer)
-{
-  return unary_exprt(ID_good_pointer, pointer, bool_typet());
-}
-
-exprt good_pointer_def(
-  const exprt &pointer,
-  const namespacet &ns)
-{
-  const pointer_typet &pointer_type = to_pointer_type(pointer.type());
-  const typet &dereference_type = pointer_type.base_type();
-
-  const auto size_of_expr_opt = size_of_expr(dereference_type, ns);
-  CHECK_RETURN(size_of_expr_opt.has_value());
-
-  const exprt good_dynamic = not_exprt{deallocated(pointer, ns)};
-
-  const not_exprt not_null(null_object(pointer));
-
-  const not_exprt not_invalid{is_invalid_pointer_exprt{pointer}};
-
-  const and_exprt good_bounds{
-    not_exprt{object_lower_bound(pointer, nil_exprt())},
-    not_exprt{object_upper_bound(pointer, size_of_expr_opt.value())}};
-
-  return and_exprt(not_null, not_invalid, good_dynamic, good_bounds);
-}
-
 exprt null_object(const exprt &pointer)
 {
   null_pointer_exprt null_pointer(to_pointer_type(pointer.type()));

src/util/pointer_predicates.h

@@ -22,8 +22,6 @@ exprt dead_object(const exprt &pointer, const namespacet &);
 exprt pointer_offset(const exprt &pointer);
 exprt pointer_object(const exprt &pointer);
 exprt object_size(const exprt &pointer);
-exprt good_pointer(const exprt &pointer);
-exprt good_pointer_def(const exprt &pointer, const namespacet &);
 exprt null_object(const exprt &pointer);
 
 exprt integer_address(const exprt &pointer);

src/util/simplify_expr.cpp

@@ -2734,10 +2734,6 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node)
   {
     r = simplify_object_size(*object_size);
   }
-  else if(expr.id()==ID_good_pointer)
-  {
-    r = simplify_good_pointer(to_unary_expr(expr));
-  }
   else if(expr.id()==ID_div)
   {
     r = simplify_div(to_div_expr(expr));

src/util/simplify_expr_class.h

@@ -180,7 +180,6 @@ class simplify_exprt
   NODISCARD resultt<> simplify_object_size(const object_size_exprt &);
   NODISCARD resultt<> simplify_is_dynamic_object(const unary_exprt &);
   NODISCARD resultt<> simplify_is_invalid_pointer(const unary_exprt &);
-  NODISCARD resultt<> simplify_good_pointer(const unary_exprt &);
   NODISCARD resultt<> simplify_object(const exprt &);
   NODISCARD resultt<> simplify_unary_minus(const unary_minus_exprt &);
   NODISCARD resultt<> simplify_unary_plus(const unary_plus_exprt &);

src/util/simplify_expr_pointer.cpp

@@ -692,13 +692,3 @@ simplify_exprt::simplify_object_size(const object_size_exprt &expr)
   else
     return std::move(new_expr);
 }
-
-simplify_exprt::resultt<>
-simplify_exprt::simplify_good_pointer(const unary_exprt &expr)
-{
-  // we expand the definition
-  exprt def = good_pointer_def(expr.op(), ns);
-
-  // recursive call
-  return changed(simplify_rec(def));
-}