Merge pull request #6565 from tautschnig/simplify_rw_ok

Fix and cleanup __CPROVER_{r,w,rw}_ok expansion

Author: tautschnig

regression/cbmc/r_w_ok9/main.c

@@ -0,0 +1,14 @@
+int check(int cond)
+{
+  return cond;
+}
+
+int main()
+{
+  int x;
+  int *p = &x;
+  if(check(!__CPROVER_r_ok(p, sizeof(int))))
+  {
+    __CPROVER_assert(0, "must be unreachable");
+  }
+}

regression/cbmc/r_w_ok9/simplify.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+--
+false ∨
+∨ false
+--
+__CPROVER_{r,w,rw}_ok must be rewritten everywhere, and the resulting expression
+should be simplified (and, therefore, not contain "false" in a disjunction).

regression/cbmc/r_w_ok9/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+__CPROVER_{r,w,rw}_ok must be rewritten everywhere, which includes function call
+arguments.

regression/validate-trace-xml-schema/check.py

@@ -25,6 +25,7 @@
     ['integer-assignments1', 'integer-typecheck.desc'],
     ['destructors', 'compound_literal.desc'],
     ['destructors', 'enter_lexical_block.desc'],
+    ['r_w_ok9', 'simplify.desc'],
     ['reachability-slice-interproc2', 'test.desc'],
     # this one wants show-properties instead producing a trace
     ['show_properties1', 'test.desc'],

src/analyses/goto_check_c.cpp

@@ -1919,7 +1919,10 @@ optionalt<exprt> goto_check_ct::rw_ok_check(exprt expr)
     for(const auto &c : conditions)
       conjuncts.push_back(c.assertion);
 
-    return conjunction(conjuncts);
+    exprt c = conjunction(conjuncts);
+    if(enable_simplify)
+      simplify(c, ns);
+    return c;
   }
   else if(modified)
     return std::move(expr);
@@ -2068,16 +2071,6 @@ void goto_check_ct::goto_check(
     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 ||
-                  expr.id() == ID_rw_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?
@@ -2129,16 +2122,6 @@ void goto_check_ct::goto_check(
 
       // the LHS might invalidate any assertion
       invalidate(assign_lhs);
-
-      if(has_subexpr(assign_rhs, [](const exprt &expr) {
-           return expr.id() == ID_r_ok || expr.id() == ID_w_ok ||
-                  expr.id() == ID_rw_ok;
-         }))
-      {
-        auto rw_ok_cond = rw_ok_check(assign_rhs);
-        if(rw_ok_cond.has_value())
-          i.assign_rhs_nonconst() = *rw_ok_cond;
-      }
     }
     else if(i.is_function_call())
     {
@@ -2156,17 +2139,6 @@ void goto_check_ct::goto_check(
       check(i.return_value());
       // the return value invalidate any assertion
       invalidate(i.return_value());
-
-      if(has_subexpr(i.return_value(), [](const exprt &expr) {
-           return expr.id() == ID_r_ok || expr.id() == ID_w_ok ||
-                  expr.id() == ID_rw_ok;
-         }))
-      {
-        exprt &return_value = i.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())
     {
@@ -2288,6 +2260,8 @@ void goto_check_ct::goto_check(
       }
     }
 
+    i.transform([this](exprt expr) { return rw_ok_check(expr); });
+
     for(auto &instruction : new_code.instructions)
     {
       if(instruction.source_location().is_nil())