Merge pull request #6401 from thomasspriggs/tas/short_circuit_implies

Add short circuit evaluation to implies operator `==>`

Author: thomasspriggs

regression/cbmc/short_circuit_implies/false_implies_failure_side_effect.c

@@ -0,0 +1,15 @@
+#include <stdbool.h>
+
+bool fail()
+{
+  __CPROVER_assert(false, "fail function");
+  return true;
+}
+
+void main()
+{
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
+  __CPROVER_assert(false ==> fail(), "fail function");
+  // clang-format on
+}

regression/cbmc/short_circuit_implies/false_implies_failure_side_effect.desc

@@ -0,0 +1,14 @@
+CORE
+false_implies_failure_side_effect.c
+
+^EXIT=0$
+^SIGNAL=0$
+line 5 fail function: SUCCESS
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring
+--
+Test that side effects on the right hand side of the ==> operator that would
+otherwise result in verification failure do not do so when the left hand side
+is false. This confirms that the ==> operator employs short circuiting
+evaluation in the same way as the && and || operators.

regression/cbmc/short_circuit_implies/short-circuit-memory-checks.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+int main()
+{
+  int *c = NULL;
+
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
+  assert(false ==> *c == 0);
+  assert(true ==> *c == 0);
+  // clang-format on
+}

regression/cbmc/short_circuit_implies/short-circuit-memory-checks.desc

@@ -0,0 +1,14 @@
+CORE
+short-circuit-memory-checks.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+line 11 dereference failure: pointer NULL in \*c: SUCCESS
+line 12 dereference failure: pointer NULL in \*c: FAILURE
+VERIFICATION FAILED
+--
+^warning: ignoring
+--
+Test that side effects on the right hand side of the ==> operator are correctly
+short-circuited or not where the side effect is a pointer check. Note that this
+test is based upon the originally reported github issue 6319.

regression/cbmc/short_circuit_implies/true_implies_failure_side_effect.c

@@ -0,0 +1,15 @@
+#include <stdbool.h>
+
+bool fail()
+{
+  __CPROVER_assert(false, "fail function");
+  return true;
+}
+
+void main()
+{
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
+  __CPROVER_assert(true ==> fail(), "fail function");
+  // clang-format on
+}

regression/cbmc/short_circuit_implies/true_implies_failure_side_effect.desc

@@ -0,0 +1,12 @@
+CORE
+true_implies_failure_side_effect.c
+
+^EXIT=10$
+^SIGNAL=0$
+line 5 fail function: FAILURE
+VERIFICATION FAILED
+--
+^warning: ignoring
+--
+Test that side effects on the right hand side of the ==> operator can result
+in verification failure in the case where the left hand side is true.

src/goto-programs/goto_clean_expr.cpp

@@ -106,7 +106,8 @@ bool goto_convertt::needs_cleaning(const exprt &expr)
 /// re-write boolean operators into ?:
 void goto_convertt::rewrite_boolean(exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_and || expr.id() == ID_or);
+  PRECONDITION(
+    expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
   PRECONDITION_WITH_DIAGNOSTICS(
     expr.is_boolean(),
     expr.find_source_location(),
@@ -115,6 +116,16 @@ void goto_convertt::rewrite_boolean(exprt &expr)
     "' must be Boolean, but got ",
     irep_pretty_diagnosticst{expr});
 
+  // re-write "a ==> b" into a?b:1
+  if(auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
+  {
+    expr = if_exprt{std::move(implies->lhs()),
+                    std::move(implies->rhs()),
+                    true_exprt{},
+                    bool_typet{}};
+    return;
+  }
+
   // re-write "a && b" into nested a?b:0
   // re-write "a || b" into nested a?1:b
 
@@ -144,12 +155,15 @@ void goto_convertt::rewrite_boolean(exprt &expr)
     {
       if_exprt if_e(op, tmp, false_exprt());
       tmp.swap(if_e);
+      continue;
     }
-    else // ID_or
+    if(expr.id() == ID_or)
     {
       if_exprt if_e(op, true_exprt(), tmp);
       tmp.swap(if_e);
+      continue;
     }
+    UNREACHABLE;
   }
 
   expr.swap(tmp);
@@ -162,7 +176,7 @@ void goto_convertt::clean_expr(
   bool result_is_used)
 {
   // this cleans:
-  //   && || ?: comma (control-dependency)
+  //   && || ==> ?: comma (control-dependency)
   //   function calls
   //   object constructors like arrays, string constants, structs
   //   ++ -- (pre and post)
@@ -172,7 +186,7 @@ void goto_convertt::clean_expr(
   if(!needs_cleaning(expr))
     return;
 
-  if(expr.id()==ID_and || expr.id()==ID_or)
+  if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
   {
     // rewrite into ?:
     rewrite_boolean(expr);