Skip to content

Commit 49c9812

Browse files
Merge pull request #6401 from thomasspriggs/tas/short_circuit_implies
Add short circuit evaluation to implies operator `==>`
2 parents 038a53b + a55f5ae commit 49c9812

7 files changed

+102
-4
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.
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(true ==> fail(), "fail function");
14+
// clang-format on
15+
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
true_implies_failure_side_effect.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
line 5 fail function: FAILURE
7+
VERIFICATION FAILED
8+
--
9+
^warning: ignoring
10+
--
11+
Test that side effects on the right hand side of the ==> operator can result
12+
in verification failure in the case where the left hand side is true.

src/goto-programs/goto_clean_expr.cpp

Lines changed: 18 additions & 4 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

@@ -144,12 +155,15 @@ void goto_convertt::rewrite_boolean(exprt &expr)
144155
{
145156
if_exprt if_e(op, tmp, false_exprt());
146157
tmp.swap(if_e);
158+
continue;
147159
}
148-
else // ID_or
160+
if(expr.id() == ID_or)
149161
{
150162
if_exprt if_e(op, true_exprt(), tmp);
151163
tmp.swap(if_e);
164+
continue;
152165
}
166+
UNREACHABLE;
153167
}
154168

155169
expr.swap(tmp);
@@ -162,7 +176,7 @@ void goto_convertt::clean_expr(
162176
bool result_is_used)
163177
{
164178
// this cleans:
165-
// && || ?: comma (control-dependency)
179+
// && || ==> ?: comma (control-dependency)
166180
// function calls
167181
// object constructors like arrays, string constants, structs
168182
// ++ -- (pre and post)
@@ -172,7 +186,7 @@ void goto_convertt::clean_expr(
172186
if(!needs_cleaning(expr))
173187
return;
174188

175-
if(expr.id()==ID_and || expr.id()==ID_or)
189+
if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
176190
{
177191
// rewrite into ?:
178192
rewrite_boolean(expr);

0 commit comments

Comments
 (0)