Add expression lowering to {r,w,rw}_ok

This prepares removal of expression rewriting in the front-end.

Author: tautschnig

src/ansi-c/goto_check_c.cpp

@@ -2032,7 +2032,7 @@ optionalt<exprt> goto_check_ct::expand_pointer_checks(exprt expr)
   {
     const auto &pointer_in_range_expr = to_pointer_in_range_expr(expr);
 
-    auto expanded = pointer_in_range_expr.lower();
+    auto expanded = pointer_in_range_expr.lower(ns);
 
     // rec. call
     auto expanded_rec_opt = expand_pointer_checks(expanded);

src/util/pointer_expr.cpp

@@ -227,7 +227,18 @@ void dereference_exprt::validate(
     "operand");
 }
 
-exprt pointer_in_range_exprt::lower() const
+exprt r_or_w_ok_exprt::lower(const namespacet &ns) const
+{
+  return conjunction(
+    {not_exprt{null_object(pointer())},
+     not_exprt{is_invalid_pointer_exprt{pointer()}},
+     not_exprt{same_object(pointer(), deallocated_ptr())},
+     not_exprt{same_object(pointer(), dead_ptr())},
+     not_exprt{object_lower_bound(pointer(), nil_exprt())},
+     not_exprt{object_upper_bound(pointer(), size())}});
+}
+
+exprt pointer_in_range_exprt::lower(const namespacet &ns) const
 {
   return and_exprt(
     {same_object(op0(), op1()),
@@ -236,7 +247,8 @@ exprt pointer_in_range_exprt::lower() const
        op0(),
        minus_exprt(pointer_offset(op2()), pointer_offset(op0())),
        deallocated_ptr(),
-       dead_ptr()),
+       dead_ptr())
+       .lower(ns),
      binary_relation_exprt(pointer_offset(op0()), ID_le, pointer_offset(op1())),
      binary_relation_exprt(
        pointer_offset(op1()), ID_le, pointer_offset(op2()))});

src/util/pointer_expr.h

@@ -418,7 +418,7 @@ class pointer_in_range_exprt : public expr_protectedt
   }
 
   // translate into equivalent conjunction
-  exprt lower() const;
+  exprt lower(const namespacet &ns) const;
 };
 
 template <>
@@ -869,6 +869,10 @@ class r_or_w_ok_exprt : public expr_protectedt
   {
     return op3();
   }
+
+  /// Lower an r_or_w_ok_exprt to arithmetic and logic expressions.
+  /// \return Semantically equivalent expression
+  exprt lower(const namespacet &ns) const;
 };
 
 template <>