variants of r/w_ok

This adds

1) a new predicate rw_ok, which is the conjunction of r_ok and w_ok;

2) variants of r_ok, w_ok and rw_ok that only have one parameter, a pointer.
The size of the memory range that is ok to read or write is given implicitly
by the size of the subtype of the pointer argument.

Author: kroening

doc/cprover-manual/api.md

@@ -191,16 +191,25 @@ option to verify the preconditions of the primitives.
 ```C
 __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *p);
 _Bool __CPROVER_DYNAMIC_OBJECT(const void *p);
+void __CPROVER_r_ok(const T *p);
 void __CPROVER_r_ok(const void *p, size_t size);
+void __CPROVER_w_ok(const T *p);
 void __CPROVER_w_ok(const void *p, size_t size);
+void __CPROVER_rw_ok(const T *p);
+void __CPROVER_rw_ok(const void *p, size_t size);
 ```
 
 The function **\_\_CPROVER_\_OBJECT\_SIZE** returns the size of the object the
 given pointer points to. The function **\_\_CPROVER\_DYNAMIC\_OBJECT** returns
 true if the pointer passed as an argument points to a dynamically allocated
-object. The function **\_\_CPROVER\_r_ok** returns true if reading the piece of
-memory starting at the given pointer with the given size is safe.
-**\_\_CPROVER\_w_ok** does the same with writing.
+object.
+
+The function **\_\_CPROVER\_r_ok** returns true if reading the piece of
+memory starting at the given pointer with the given size is safe. 
+**\_\_CPROVER\_w_ok** does the same with writing, and **\_\_CPROVER\_rw_ok**
+returns true when it is safe to do both.  These predicates can be given an
+optional size; when the size argument is not given, the size of the subtype
+(which must not be **void**) of the pointer type is used.
 
 ### Predefined Types and Symbols
 

regression/cbmc/pointer-primitive-check-01/test.desc

@@ -19,14 +19,14 @@ main.c
 \[main.pointer_primitives.14\] line \d+ deallocated dynamic object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
 \[main.pointer_primitives.15\] line \d+ dead object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
 \[main.pointer_primitives.16\] line \d+ pointer outside object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
-\[main.pointer_primitives.17\] line \d+ pointer invalid in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): FAILURE
-\[main.pointer_primitives.18\] line \d+ deallocated dynamic object in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): SUCCESS
-\[main.pointer_primitives.19\] line \d+ dead object in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): SUCCESS
-\[main.pointer_primitives.20\] line \d+ pointer outside object bounds in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): FAILURE
-\[main.pointer_primitives.21\] line \d+ pointer invalid in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): FAILURE
-\[main.pointer_primitives.22\] line \d+ deallocated dynamic object in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): SUCCESS
-\[main.pointer_primitives.23\] line \d+ dead object in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): SUCCESS
-\[main.pointer_primitives.24\] line \d+ pointer outside object bounds in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): FAILURE
+\[main.pointer_primitives.17\] line \d+ pointer invalid in R_OK\(p5, .*1\): FAILURE
+\[main.pointer_primitives.18\] line \d+ deallocated dynamic object in R_OK\(p5, .*1\): SUCCESS
+\[main.pointer_primitives.19\] line \d+ dead object in R_OK\(p5, .*1\): SUCCESS
+\[main.pointer_primitives.20\] line \d+ pointer outside object bounds in R_OK\(p5, .*1\): FAILURE
+\[main.pointer_primitives.21\] line \d+ pointer invalid in W_OK\(p6, \(.*\)1\): FAILURE
+\[main.pointer_primitives.22\] line \d+ deallocated dynamic object in W_OK\(p6, .*1\): SUCCESS
+\[main.pointer_primitives.23\] line \d+ dead object in W_OK\(p6, .*1\): SUCCESS
+\[main.pointer_primitives.24\] line \d+ pointer outside object bounds in W_OK\(p6, .*1\): FAILURE
 \[main.pointer_primitives.25\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
 \[main.pointer_primitives.26\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
 \[main.pointer_primitives.27\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS

regression/cbmc/pointer-primitive-check-04/test.desc

@@ -3,10 +3,10 @@ main.c
 --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
-\[main.pointer_primitives.1\] line \d+ pointer invalid in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): FAILURE
-\[main.pointer_primitives.2\] line \d+ deallocated dynamic object in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): SUCCESS
-\[main.pointer_primitives.3\] line \d+ dead object in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): SUCCESS
-\[main.pointer_primitives.4\] line \d+ pointer outside object bounds in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): FAILURE
+\[main.pointer_primitives.1\] line \d+ pointer invalid in R_OK\(p, .*1\): FAILURE
+\[main.pointer_primitives.2\] line \d+ deallocated dynamic object in R_OK\(p, .*1\): SUCCESS
+\[main.pointer_primitives.3\] line \d+ dead object in R_OK\(p, .*1\): SUCCESS
+\[main.pointer_primitives.4\] line \d+ pointer outside object bounds in R_OK\(p, .*1\): FAILURE
 --
 ^warning: ignoring
 --

src/analyses/goto_check.cpp

@@ -1260,9 +1260,10 @@ void goto_checkt::pointer_primitive_check(
   if(expr.source_location().is_built_in())
     return;
 
-  const exprt pointer = (expr.id() == ID_r_ok || expr.id() == ID_w_ok)
-                          ? to_r_or_w_ok_expr(expr).pointer()
-                          : to_unary_expr(expr).op();
+  const exprt pointer =
+    (expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
+      ? to_r_or_w_ok_expr(expr).pointer()
+      : to_unary_expr(expr).op();
 
   CHECK_RETURN(pointer.type().id() == ID_pointer);
 
@@ -1301,7 +1302,8 @@ bool goto_checkt::is_pointer_primitive(const exprt &expr)
   // during typechecking (see c_typecheck_expr.cpp)
   return expr.id() == ID_pointer_object || expr.id() == ID_pointer_offset ||
          expr.id() == ID_object_size || expr.id() == ID_r_ok ||
-         expr.id() == ID_w_ok || expr.id() == ID_is_dynamic_object;
+         expr.id() == ID_w_ok || expr.id() == ID_rw_ok ||
+         expr.id() == ID_is_dynamic_object;
 }
 
 goto_checkt::conditionst goto_checkt::get_pointer_dereferenceable_conditions(
@@ -1787,7 +1789,7 @@ void goto_checkt::check(const exprt &expr)
   check_rec(expr, guard);
 }
 
-/// expand the r_ok and w_ok predicates
+/// expand the r_ok, w_ok and rw_ok predicates
 optionalt<exprt> goto_checkt::rw_ok_check(exprt expr)
 {
   bool modified = false;
@@ -1802,7 +1804,7 @@ optionalt<exprt> goto_checkt::rw_ok_check(exprt expr)
     }
   }
 
-  if(expr.id() == ID_r_ok || expr.id() == ID_w_ok)
+  if(expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
   {
     // these get an address as first argument and a size as second
     DATA_INVARIANT(
@@ -1917,7 +1919,8 @@ void goto_checkt::goto_check(
       check(i.get_condition());
 
       if(has_subexpr(i.get_condition(), [](const exprt &expr) {
-           return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
+           return expr.id() == ID_r_ok || expr.id() == ID_w_ok ||
+                  expr.id() == ID_rw_ok;
          }))
       {
         auto rw_ok_cond = rw_ok_check(i.get_condition());
@@ -1974,7 +1977,8 @@ void goto_checkt::goto_check(
       invalidate(code_assign.lhs());
 
       if(has_subexpr(code_assign.rhs(), [](const exprt &expr) {
-           return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
+           return expr.id() == ID_r_ok || expr.id() == ID_w_ok ||
+                  expr.id() == ID_rw_ok;
          }))
       {
         const exprt &rhs = i.get_assign().rhs();
@@ -2033,7 +2037,8 @@ void goto_checkt::goto_check(
       invalidate(i.return_value());
 
       if(has_subexpr(i.return_value(), [](const exprt &expr) {
-           return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
+           return expr.id() == ID_r_ok || expr.id() == ID_w_ok ||
+                  expr.id() == ID_rw_ok;
          }))
       {
         exprt &return_value = i.return_value();

src/ansi-c/c_typecheck_expr.cpp

@@ -2558,20 +2558,65 @@ exprt c_typecheck_baset::do_special_functions(
     return std::move(malloc_expr);
   }
   else if(
-    identifier == CPROVER_PREFIX "r_ok" || identifier == CPROVER_PREFIX "w_ok")
+    identifier == CPROVER_PREFIX "r_ok" ||
+    identifier == CPROVER_PREFIX "w_ok" || identifier == CPROVER_PREFIX "rw_ok")
   {
-    if(expr.arguments().size() != 2)
+    if(expr.arguments().size() != 1 && expr.arguments().size() != 2)
     {
       error().source_location = f_op.source_location();
-      error() << identifier << " expects two operands" << eom;
+      error() << identifier << " expects one or two operands" << eom;
       throw 0;
     }
 
     typecheck_function_call_arguments(expr);
 
-    irep_idt id = identifier == CPROVER_PREFIX "r_ok" ? ID_r_ok : ID_w_ok;
+    // the first argument must be a pointer
+    const auto &pointer_expr = expr.arguments()[0];
+    if(pointer_expr.type().id() != ID_pointer)
+    {
+      error().source_location = f_op.source_location();
+      error() << identifier << " expects a pointer as first argument" << eom;
+      throw 0;
+    }
+
+    // The second argument, when given, is a size_t.
+    // When not given, use the pointer subtype.
+    exprt size_expr;
+
+    if(expr.arguments().size() == 2)
+    {
+      implicit_typecast(expr.arguments()[1], size_type());
+      size_expr = expr.arguments()[1];
+    }
+    else
+    {
+      // Won't do void *
+      const auto &subtype = to_pointer_type(pointer_expr.type()).subtype();
+      if(subtype.id() == ID_empty)
+      {
+        error().source_location = f_op.source_location();
+        error() << identifier << " expects a size when given a void pointer"
+                << eom;
+        throw 0;
+      }
+
+      auto size_expr_opt = size_of_expr(subtype, *this);
+      if(!size_expr_opt.has_value())
+      {
+        error().source_location = f_op.source_location();
+        error() << identifier << " was given object pointer without size"
+                << eom;
+        throw 0;
+      }
+
+      size_expr = std::move(size_expr_opt.value());
+    }
+
+    irep_idt id = identifier == CPROVER_PREFIX "r_ok"
+                    ? ID_r_ok
+                    : identifier == CPROVER_PREFIX "w_ok" ? ID_w_ok : ID_rw_ok;
 
-    r_or_w_ok_exprt ok_expr(id, expr.arguments()[0], expr.arguments()[1]);
+    r_or_w_ok_exprt ok_expr(id, pointer_expr, size_expr);
     ok_expr.add_source_location() = source_location;
 
     return std::move(ok_expr);

src/ansi-c/cprover_builtin_headers.h

@@ -10,8 +10,9 @@ __CPROVER_bool __CPROVER_is_invalid_pointer(const void *);
 _Bool __CPROVER_is_zero_string(const void *);
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);
-__CPROVER_bool __CPROVER_r_ok(const void *, __CPROVER_size_t);
-__CPROVER_bool __CPROVER_w_ok(const void *, __CPROVER_size_t);
+__CPROVER_bool __CPROVER_r_ok();
+__CPROVER_bool __CPROVER_w_ok();
+__CPROVER_bool __CPROVER_rw_ok();
 
 // bitvector analysis
 __CPROVER_bool __CPROVER_get_flag(const void *, const char *);

src/ansi-c/expr2c.cpp

@@ -3847,6 +3847,7 @@ optionalt<std::string> expr2ct::convert_function(const exprt &src)
     {ID_pointer_offset, "POINTER_OFFSET"},
     {ID_r_ok, "R_OK"},
     {ID_w_ok, "W_OK"},
+    {ID_rw_ok, "RW_OK"},
     {ID_width, "WIDTH"},
   };
 

src/ansi-c/library/cprover.h

@@ -33,8 +33,9 @@ void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description);
 _Bool __CPROVER_is_zero_string(const void *);
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);
-__CPROVER_bool __CPROVER_r_ok(const void *, __CPROVER_size_t);
-__CPROVER_bool __CPROVER_w_ok(const void *, __CPROVER_size_t);
+__CPROVER_bool __CPROVER_r_ok();
+__CPROVER_bool __CPROVER_w_ok();
+__CPROVER_bool __CPROVER_rw_ok();
 
 #if 0
 __CPROVER_bool __CPROVER_equal();

src/util/irep_ids.def

@@ -687,6 +687,7 @@ IREP_ID_TWO(C_qualifier, #qualifier)
 IREP_ID_TWO(C_array_ini, #array_ini)
 IREP_ID_ONE(r_ok)
 IREP_ID_ONE(w_ok)
+IREP_ID_ONE(rw_ok)
 IREP_ID_ONE(super_class)
 IREP_ID_ONE(exceptions_thrown_list)
 IREP_ID_TWO(C_java_method_type, #java_method_type)

src/util/pointer_expr.h

@@ -698,7 +698,7 @@ 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
+/// address range is ok to read or write or both
 class r_or_w_ok_exprt : public binary_predicate_exprt
 {
 public:
@@ -720,7 +720,8 @@ class r_or_w_ok_exprt : public binary_predicate_exprt
 
 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);
+  PRECONDITION(
+    expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok);
   auto &ret = static_cast<const r_or_w_ok_exprt &>(expr);
   validate_expr(ret);
   return ret;