Merge pull request #4485 from tautschnig/cprover-rw-ok

Extend and cleanup usability of __CPROVER_{r,w}_ok

Author: tautschnig

regression/cbmc/r_w_ok1/main.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  int *p = NULL;
+
+  assert(!__CPROVER_r_ok(p, sizeof(int)));
+  assert(!__CPROVER_w_ok(p, sizeof(int)));
+
+  p = malloc(sizeof(int));
+
+  assert(__CPROVER_r_ok(p, 1));
+  assert(__CPROVER_w_ok(p, 1));
+  assert(__CPROVER_r_ok(p, sizeof(int)));
+  assert(__CPROVER_w_ok(p, sizeof(int)));
+
+  size_t n;
+  char *arbitrary_size = malloc(n);
+
+  assert(__CPROVER_r_ok(arbitrary_size, n));
+  assert(__CPROVER_w_ok(arbitrary_size, n));
+
+  assert(__CPROVER_r_ok(arbitrary_size, n + 1));
+  assert(__CPROVER_w_ok(arbitrary_size, n + 1));
+}

regression/cbmc/r_w_ok1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+__CPROVER_[rw]_ok\(arbitrary_size, n \+ 1\): FAILURE$
+^\*\* 2 of 10 failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/r_w_ok2/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int main()
+{
+  int *p = (int *)0;
+
+  _Bool not_ok = !__CPROVER_r_ok(p, sizeof(int));
+  assert(not_ok);
+
+  if(__CPROVER_w_ok(p, sizeof(int)))
+    assert(0);
+}

regression/cbmc/r_w_ok2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/r_w_ok3/main.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main()
+{
+  const char *str = "foobar";
+  assert(!__CPROVER_w_ok(str, 6));
+  assert(__CPROVER_r_ok(str, 6));
+}

regression/cbmc/r_w_ok3/test.desc

@@ -0,0 +1,12 @@
+KNOWNBUG
+main.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+We currently do not distinguish __CPROVER_r_ok and __CPROVER_w_ok at the
+implementation level. To make a meaningful distinction we would need to have
+predicates about lvalues vs rvalues.

src/analyses/goto_check.cpp

@@ -1076,9 +1076,7 @@ void goto_checkt::pointer_validity_check(
 goto_checkt::conditionst
 goto_checkt::address_check(const exprt &address, const exprt &size)
 {
-  if(!enable_pointer_check)
-    return {};
-
+  PRECONDITION(local_bitvector_analysis);
   PRECONDITION(address.type().id() == ID_pointer);
   const auto &pointer_type = to_pointer_type(address.type());
 
@@ -1700,9 +1698,8 @@ void goto_checkt::goto_check(
 
   bool did_something = false;
 
-  if(enable_pointer_check)
-    local_bitvector_analysis =
-      util_make_unique<local_bitvector_analysist>(goto_function, ns);
+  local_bitvector_analysis =
+    util_make_unique<local_bitvector_analysist>(goto_function, ns);
 
   goto_programt &goto_program=goto_function.body;
 
@@ -1721,8 +1718,19 @@ void goto_checkt::goto_check(
       assertions.clear();
 
     if(i.has_condition())
+    {
       check(i.get_condition());
 
+      if(has_subexpr(i.get_condition(), [](const exprt &expr) {
+           return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
+         }))
+      {
+        auto rw_ok_cond = rw_ok_check(i.get_condition());
+        if(rw_ok_cond.has_value())
+          i.set_condition(*rw_ok_cond);
+      }
+    }
+
     // magic ERROR label?
     for(const auto &label : error_labels)
     {
@@ -1765,6 +1773,16 @@ void goto_checkt::goto_check(
 
       // the LHS might invalidate any assertion
       invalidate(code_assign.lhs());
+
+      if(has_subexpr(code_assign.rhs(), [](const exprt &expr) {
+           return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
+         }))
+      {
+        exprt &rhs = to_code_assign(i.code).rhs();
+        auto rw_ok_cond = rw_ok_check(rhs);
+        if(rw_ok_cond.has_value())
+          rhs = *rw_ok_cond;
+      }
     }
     else if(i.is_function_call())
     {
@@ -1810,9 +1828,20 @@ void goto_checkt::goto_check(
     {
       if(i.code.operands().size()==1)
       {
-        check(i.code.op0());
+        const code_returnt &code_return = to_code_return(i.code);
+        check(code_return.return_value());
         // the return value invalidate any assertion
-        invalidate(i.code.op0());
+        invalidate(code_return.return_value());
+
+        if(has_subexpr(code_return.return_value(), [](const exprt &expr) {
+             return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
+           }))
+        {
+          exprt &return_value = to_code_return(i.code).return_value();
+          auto rw_ok_cond = rw_ok_check(return_value);
+          if(rw_ok_cond.has_value())
+            return_value = *rw_ok_cond;
+        }
       }
     }
     else if(i.is_throw())
@@ -1844,10 +1873,6 @@ void goto_checkt::goto_check(
     {
       bool is_user_provided=i.source_location.get_bool("user-provided");
 
-      auto rw_ok_cond = rw_ok_check(i.get_condition());
-      if(rw_ok_cond.has_value())
-        i.set_condition(*rw_ok_cond);
-
       if((is_user_provided && !enable_assertions &&
           i.source_location.get_property_class()!="error label") ||
          (!is_user_provided && !enable_built_in_assertions))