Skip to content

Commit a55f5ae

Browse files
committed
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.
1 parent 740976b commit a55f5ae

File tree

5 files changed

+71
-3
lines changed

5 files changed

+71
-3
lines changed
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#include <stdbool.h>
2+
3+
bool fail()
4+
{
5+
__CPROVER_assert(false, "fail function");
6+
return true;
7+
}
8+
9+
void main()
10+
{
11+
// clang-format off
12+
// clang-format would rewrite the "==>" as "== >"
13+
__CPROVER_assert(false ==> fail(), "fail function");
14+
// clang-format on
15+
}
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
false_implies_failure_side_effect.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
line 5 fail function: SUCCESS
7+
VERIFICATION SUCCESSFUL
8+
--
9+
^warning: ignoring
10+
--
11+
Test that side effects on the right hand side of the ==> operator that would
12+
otherwise result in verification failure do not do so when the left hand side
13+
is false. This confirms that the ==> operator employs short circuiting
14+
evaluation in the same way as the && and || operators.
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#include <assert.h>
2+
#include <stdbool.h>
3+
#include <stdlib.h>
4+
5+
int main()
6+
{
7+
int *c = NULL;
8+
9+
// clang-format off
10+
// clang-format would rewrite the "==>" as "== >"
11+
assert(false ==> *c == 0);
12+
assert(true ==> *c == 0);
13+
// clang-format on
14+
}
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
short-circuit-memory-checks.c
3+
--pointer-check
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
line 11 dereference failure: pointer NULL in \*c: SUCCESS
7+
line 12 dereference failure: pointer NULL in \*c: FAILURE
8+
VERIFICATION FAILED
9+
--
10+
^warning: ignoring
11+
--
12+
Test that side effects on the right hand side of the ==> operator are correctly
13+
short-circuited or not where the side effect is a pointer check. Note that this
14+
test is based upon the originally reported github issue 6319.

src/goto-programs/goto_clean_expr.cpp

Lines changed: 14 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,8 @@ bool goto_convertt::needs_cleaning(const exprt &expr)
106106
/// re-write boolean operators into ?:
107107
void goto_convertt::rewrite_boolean(exprt &expr)
108108
{
109-
PRECONDITION(expr.id() == ID_and || expr.id() == ID_or);
109+
PRECONDITION(
110+
expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
110111
PRECONDITION_WITH_DIAGNOSTICS(
111112
expr.is_boolean(),
112113
expr.find_source_location(),
@@ -115,6 +116,16 @@ void goto_convertt::rewrite_boolean(exprt &expr)
115116
"' must be Boolean, but got ",
116117
irep_pretty_diagnosticst{expr});
117118

119+
// re-write "a ==> b" into a?b:1
120+
if(auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
121+
{
122+
expr = if_exprt{std::move(implies->lhs()),
123+
std::move(implies->rhs()),
124+
true_exprt{},
125+
bool_typet{}};
126+
return;
127+
}
128+
118129
// re-write "a && b" into nested a?b:0
119130
// re-write "a || b" into nested a?1:b
120131

@@ -165,7 +176,7 @@ void goto_convertt::clean_expr(
165176
bool result_is_used)
166177
{
167178
// this cleans:
168-
// && || ?: comma (control-dependency)
179+
// && || ==> ?: comma (control-dependency)
169180
// function calls
170181
// object constructors like arrays, string constants, structs
171182
// ++ -- (pre and post)
@@ -175,7 +186,7 @@ void goto_convertt::clean_expr(
175186
if(!needs_cleaning(expr))
176187
return;
177188

178-
if(expr.id()==ID_and || expr.id()==ID_or)
189+
if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
179190
{
180191
// rewrite into ?:
181192
rewrite_boolean(expr);

0 commit comments

Comments
 (0)