Add short-circuit evaluation of implies operator

So that side effects of the right hand side are only evaluated in the
case where the left hand side is true. This allows for pointer checks to
be applied to assertions such as `assert(x != NULL ==> *x==2);` for
example.

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.

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
 
@@ -165,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)
@@ -175,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);