Merge pull request #5975 from diffblue/rw_ok_expr

Introduce expression classes for r_ok and w_ok

Author: tautschnig

src/analyses/goto_check.cpp

@@ -1261,7 +1261,7 @@ void goto_checkt::pointer_primitive_check(
     return;
 
   const exprt pointer = (expr.id() == ID_r_ok || expr.id() == ID_w_ok)
-                          ? to_binary_expr(expr).lhs()
+                          ? to_r_or_w_ok_expr(expr).pointer()
                           : to_unary_expr(expr).op();
 
   CHECK_RETURN(pointer.type().id() == ID_pointer);
@@ -1822,7 +1822,7 @@ optionalt<exprt> goto_checkt::rw_ok_check(exprt expr)
       expr.operands().size() == 2, "r/w_ok must have two operands");
 
     const auto conditions = get_pointer_dereferenceable_conditions(
-      to_binary_expr(expr).op0(), to_binary_expr(expr).op1());
+      to_r_or_w_ok_expr(expr).pointer(), to_r_or_w_ok_expr(expr).size());
 
     exprt::operandst conjuncts;
 

src/ansi-c/c_typecheck_expr.cpp

@@ -2550,8 +2550,7 @@ exprt c_typecheck_baset::do_special_functions(
 
     irep_idt id = identifier == CPROVER_PREFIX "r_ok" ? ID_r_ok : ID_w_ok;
 
-    binary_predicate_exprt ok_expr(
-      expr.arguments()[0], id, expr.arguments()[1]);
+    r_or_w_ok_exprt ok_expr(id, expr.arguments()[0], expr.arguments()[1]);
     ok_expr.add_source_location() = source_location;
 
     return std::move(ok_expr);

src/util/pointer_expr.h

@@ -462,4 +462,69 @@ class null_pointer_exprt : public constant_exprt
   }
 };
 
+/// \brief A base class for a predicate that indicates that an
+/// address range is ok to read or write
+class r_or_w_ok_exprt : public binary_predicate_exprt
+{
+public:
+  explicit r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
+    : binary_predicate_exprt(std::move(pointer), id, std::move(size))
+  {
+  }
+
+  const exprt &pointer() const
+  {
+    return op0();
+  }
+
+  const exprt &size() const
+  {
+    return op1();
+  }
+};
+
+inline const r_or_w_ok_exprt &to_r_or_w_ok_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_r_ok || expr.id() == ID_w_ok);
+  auto &ret = static_cast<const r_or_w_ok_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \brief A predicate that indicates that an address range is ok to read
+class r_ok_exprt : public r_or_w_ok_exprt
+{
+public:
+  explicit r_ok_exprt(exprt pointer, exprt size)
+    : r_or_w_ok_exprt(ID_r_ok, std::move(pointer), std::move(size))
+  {
+  }
+};
+
+inline const r_ok_exprt &to_r_ok_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_r_ok);
+  const r_ok_exprt &ret = static_cast<const r_ok_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \brief A predicate that indicates that an address range is ok to write
+class w_ok_exprt : public r_or_w_ok_exprt
+{
+public:
+  explicit w_ok_exprt(exprt pointer, exprt size)
+    : r_or_w_ok_exprt(ID_w_ok, std::move(pointer), std::move(size))
+  {
+  }
+};
+
+inline const w_ok_exprt &to_w_ok_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_w_ok);
+  const w_ok_exprt &ret = static_cast<const w_ok_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_UTIL_POINTER_EXPR_H