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,13 +227,25 @@ 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{deallocated(pointer(), ns)},
+     not_exprt{dead_object(pointer(), ns)},
+     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()),
      same_object(op1(), op2()),
      r_ok_exprt(
-       op0(), minus_exprt(pointer_offset(op2()), pointer_offset(op0()))),
+       op0(), minus_exprt(pointer_offset(op2()), pointer_offset(op0())))
+       .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

@@ -386,7 +386,7 @@ class pointer_in_range_exprt : public ternary_exprt
   }
 
   // translate into equivalent conjunction
-  exprt lower() const;
+  exprt lower(const namespacet &ns) const;
 };
 
 template <>
@@ -816,6 +816,10 @@ class r_or_w_ok_exprt : public binary_predicate_exprt
   {
     return op1();
   }
+
+  /// Lower an r_or_w_ok_exprt to arithmetic and logic expressions.
+  /// \return Semantically equivalent expression
+  exprt lower(const namespacet &ns) const;
 };
 
 inline const r_or_w_ok_exprt &to_r_or_w_ok_expr(const exprt &expr)