Simplify {r,w,rw}_ok and pointer_in_range expressions

The rules replace the expression by a constant when (recursive)
simplification yields such, else leave the expression unmodified.

Author: tautschnig

src/util/simplify_expr.cpp

@@ -2905,6 +2905,14 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node)
   {
     r = simplify_bitreverse(to_bitreverse_expr(expr));
   }
+  else if(expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
+  {
+    r = simplify_r_or_w_ok(to_r_or_w_ok_expr(expr));
+  }
+  else if(expr.id() == ID_pointer_in_range)
+  {
+    r = simplify_pointer_in_range(to_pointer_in_range_expr(expr));
+  }
 
   if(!no_change_join_operands)
     r = changed(r);

src/util/simplify_expr_class.h

@@ -62,9 +62,11 @@ class not_exprt;
 class object_size_exprt;
 class overflow_result_exprt;
 class plus_exprt;
+class pointer_in_range_exprt;
 class pointer_object_exprt;
 class pointer_offset_exprt;
 class popcount_exprt;
+class r_or_w_ok_exprt;
 class refined_string_exprt;
 class shift_exprt;
 class sign_exprt;
@@ -228,6 +230,12 @@ class simplify_exprt
   /// Try to simplify find-first-set to a constant expression.
   NODISCARD resultt<> simplify_ffs(const find_first_set_exprt &);
 
+  /// Try to simplify {r,w,rw}_ok to a constant expression.
+  NODISCARD resultt<> simplify_r_or_w_ok(const r_or_w_ok_exprt &);
+
+  /// Try to simplify pointer_in_range to a constant expression.
+  NODISCARD resultt<> simplify_pointer_in_range(const pointer_in_range_exprt &);
+
   // auxiliary
   bool simplify_if_implies(
     exprt &expr, const exprt &cond, bool truth, bool &new_truth);

src/util/simplify_expr_pointer.cpp

@@ -692,3 +692,23 @@ simplify_exprt::simplify_object_size(const object_size_exprt &expr)
   else
     return std::move(new_expr);
 }
+
+simplify_exprt::resultt<>
+simplify_exprt::simplify_r_or_w_ok(const r_or_w_ok_exprt &expr)
+{
+  exprt new_expr = simplify_rec(expr.lower(ns));
+  if(!new_expr.is_constant())
+    return unchanged(expr);
+  else
+    return std::move(new_expr);
+}
+
+simplify_exprt::resultt<>
+simplify_exprt::simplify_pointer_in_range(const pointer_in_range_exprt &expr)
+{
+  exprt new_expr = simplify_rec(expr.lower(ns));
+  if(!new_expr.is_constant())
+    return unchanged(expr);
+  else
+    return std::move(new_expr);
+}