Skip to content

Commit d74a8d8

Browse files
owen-mc-diffblueowen-mc-diffblue
authored
Merge pull request #5091 from owen-mc-diffblue/goto-symex-propagate-notequal-conditions-for-boolean-types
[TG-9390] GOTO-symex: propagate notequal conditions for boolean types
2 parents fcbbb59 + a2cbcc2 commit d74a8d8

File tree

9 files changed

+327
-18
lines changed

9 files changed

+327
-18
lines changed

‎jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/ClassWithStaticInit.class

428 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/ClassWithStaticInit.java

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
public class ClassWithStaticInit {
2+
public static int x;
3+
4+
static { x = 42; }
5+
6+
public static int getStaticValue() { return x; }
7+
}

‎jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/Test.class

821 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/Test.java

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
public class Test {
2+
public static void test(boolean b) {
3+
int x;
4+
if (b) {
5+
x = ClassWithStaticInit.getStaticValue();
6+
}
7+
x = ClassWithStaticInit.getStaticValue();
8+
x = ClassWithStaticInit.getStaticValue();
9+
x = ClassWithStaticInit.getStaticValue();
10+
x = ClassWithStaticInit.getStaticValue();
11+
x = ClassWithStaticInit.getStaticValue();
12+
x = ClassWithStaticInit.getStaticValue();
13+
x = ClassWithStaticInit.getStaticValue();
14+
x = ClassWithStaticInit.getStaticValue();
15+
x = ClassWithStaticInit.getStaticValue();
16+
x = ClassWithStaticInit.getStaticValue();
17+
x = ClassWithStaticInit.getStaticValue();
18+
x = ClassWithStaticInit.getStaticValue();
19+
x = ClassWithStaticInit.getStaticValue();
20+
x = ClassWithStaticInit.getStaticValue();
21+
x = ClassWithStaticInit.getStaticValue();
22+
x = ClassWithStaticInit.getStaticValue();
23+
x = ClassWithStaticInit.getStaticValue();
24+
x = ClassWithStaticInit.getStaticValue();
25+
x = ClassWithStaticInit.getStaticValue();
26+
assert (false);
27+
}
28+
}

‎jbmc/regression/jbmc/symex_can_track_when_clinits_have_definitely_been_run/test.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
Test.class
3+
--function Test.test --verbosity 10
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
--
7+
^BMC at file ClassWithStaticInit.java line .* function java::ClassWithStaticInit.<clinit>:\(\)V bytecode-index .* \(depth [1-9][0-9][0-9]\)$
8+
^warning: ignoring
9+
--
10+
If symex isn't able to determine that the static initialiser has already been
11+
run after the second call to getStaticValue() then it will keep on entering the
12+
static initialiser, and it will eventually do so with a depth greater than or
13+
equal to 100.

‎src/goto-symex/goto_state.cpp

Lines changed: 69 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -44,15 +44,50 @@ void goto_statet::apply_condition(
4444
const goto_symex_statet &previous_state,
4545
const namespacet &ns)
4646
{
47-
if(condition.id() == ID_and)
47+
if(auto and_expr = expr_try_dynamic_cast<and_exprt>(condition))
4848
{
49-
for(const auto &op : condition.operands())
49+
// A == B && C == D && E == F ...
50+
// -->
51+
// Apply each condition individually
52+
for(const auto &op : and_expr->operands())
5053
apply_condition(op, previous_state, ns);
5154
}
52-
else if(condition.id() == ID_equal)
55+
else if(auto not_expr = expr_try_dynamic_cast<not_exprt>(condition))
5356
{
54-
exprt lhs = to_equal_expr(condition).lhs();
55-
exprt rhs = to_equal_expr(condition).rhs();
57+
const exprt &operand = not_expr->op();
58+
if(auto notequal_expr = expr_try_dynamic_cast<notequal_exprt>(operand))
59+
{
60+
// !(A != B)
61+
// -->
62+
// A == B
63+
apply_condition(
64+
equal_exprt{notequal_expr->lhs(), notequal_expr->rhs()},
65+
previous_state,
66+
ns);
67+
}
68+
else if(auto equal_expr = expr_try_dynamic_cast<equal_exprt>(operand))
69+
{
70+
// !(A == B)
71+
// -->
72+
// A != B
73+
apply_condition(
74+
notequal_exprt{equal_expr->lhs(), equal_expr->rhs()},
75+
previous_state,
76+
ns);
77+
}
78+
else
79+
{
80+
// !A
81+
// -->
82+
// A == false
83+
apply_condition(equal_exprt{operand, false_exprt{}}, previous_state, ns);
84+
}
85+
}
86+
else if(auto equal_expr = expr_try_dynamic_cast<equal_exprt>(condition))
87+
{
88+
// Base case: try to apply a single equality constraint
89+
exprt lhs = equal_expr->lhs();
90+
exprt rhs = equal_expr->rhs();
5691
if(is_ssa_expr(rhs))
5792
std::swap(lhs, rhs);
5893

@@ -84,4 +119,33 @@ void goto_statet::apply_condition(
84119
}
85120
}
86121
}
122+
else if(
123+
can_cast_expr<symbol_exprt>(condition) && condition.type() == bool_typet())
124+
{
125+
// A
126+
// -->
127+
// A == true
128+
apply_condition(equal_exprt{condition, true_exprt()}, previous_state, ns);
129+
}
130+
else if(
131+
can_cast_expr<notequal_exprt>(condition) &&
132+
expr_checked_cast<notequal_exprt>(condition).lhs().type() == bool_typet{})
133+
{
134+
// A != (true|false)
135+
// -->
136+
// A == (false|true)
137+
const notequal_exprt &notequal_expr =
138+
expr_dynamic_cast<notequal_exprt>(condition);
139+
exprt lhs = notequal_expr.lhs();
140+
exprt rhs = notequal_expr.rhs();
141+
if(is_ssa_expr(rhs))
142+
std::swap(lhs, rhs);
143+
144+
if(rhs.is_true())
145+
apply_condition(equal_exprt{lhs, false_exprt{}}, previous_state, ns);
146+
else if(rhs.is_false())
147+
apply_condition(equal_exprt{lhs, true_exprt{}}, previous_state, ns);
148+
else
149+
UNREACHABLE;
150+
}
87151
}

‎src/goto-symex/symex_goto.cpp

Lines changed: 2 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -55,21 +55,10 @@ void goto_symext::apply_goto_condition(
5555

5656
jump_taken_state.apply_condition(new_guard, current_state, ns);
5757

58-
// Try to find a negative condition that implies an equality constraint on
59-
// the branch-not-taken path.
6058
// Could use not_exprt + simplify, but let's avoid paying that cost on quite
6159
// a hot path:
62-
if(new_guard.id() == ID_not)
63-
jump_not_taken_state.apply_condition(
64-
to_not_expr(new_guard).op(), current_state, ns);
65-
else if(new_guard.id() == ID_notequal)
66-
{
67-
auto &not_equal_expr = to_notequal_expr(new_guard);
68-
jump_not_taken_state.apply_condition(
69-
equal_exprt(not_equal_expr.lhs(), not_equal_expr.rhs()),
70-
current_state,
71-
ns);
72-
}
60+
const exprt negated_new_guard = boolean_negate(new_guard);
61+
jump_not_taken_state.apply_condition(negated_new_guard, current_state, ns);
7362
}
7463

7564
/// Try to evaluate a simple pointer comparison.

‎unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ SRC += analyses/ai/ai.cpp \
3131
goto-programs/osx_fat_reader.cpp \
3232
goto-programs/remove_returns.cpp \
3333
goto-programs/xml_expr.cpp \
34+
goto-symex/apply_condition.cpp \
3435
goto-symex/expr_skeleton.cpp \
3536
goto-symex/goto_symex_state.cpp \
3637
goto-symex/ssa_equation.cpp \

‎unit/goto-symex/apply_condition.cpp

Lines changed: 207 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,207 @@
1+
/*******************************************************************\
2+
3+
Module: Unit tests for goto_statet::apply_condition
4+
5+
Author: Owen Mansel-Chan, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include <testing-utils/message.h>
10+
#include <testing-utils/use_catch.h>
11+
12+
#include <goto-symex/goto_symex.h>
13+
14+
static void add_to_symbol_table(
15+
symbol_tablet &symbol_table,
16+
const symbol_exprt &symbol_expr)
17+
{
18+
symbolt symbol;
19+
symbol.name = symbol_expr.get_identifier();
20+
symbol.type = symbol_expr.type();
21+
symbol.value = symbol_expr;
22+
symbol.is_thread_local = true;
23+
symbol_table.insert(symbol);
24+
}
25+
26+
SCENARIO(
27+
"Apply condition and update constant propagator and value-set",
28+
"[core][goto-symex][apply_condition]")
29+
{
30+
const symbol_exprt b{"b", bool_typet{}};
31+
const symbol_exprt c{"c", bool_typet{}};
32+
33+
// Add symbols to symbol table
34+
symbol_tablet symbol_table;
35+
namespacet ns{symbol_table};
36+
add_to_symbol_table(symbol_table, b);
37+
add_to_symbol_table(symbol_table, c);
38+
39+
// Initialize goto state
40+
std::list<goto_programt::instructiont> target;
41+
symex_targett::sourcet source{"fun", target.begin()};
42+
guard_managert guard_manager;
43+
std::size_t count = 0;
44+
auto fresh_name = [&count](const irep_idt &) { return count++; };
45+
goto_symex_statet state{source,
46+
DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
47+
guard_manager,
48+
fresh_name};
49+
50+
goto_statet goto_state{state};
51+
const exprt renamed_b = state.rename<L2>(b, ns).get();
52+
const exprt renamed_c = state.rename<L2>(c, ns).get();
53+
54+
WHEN("Applying the condition 'b'")
55+
{
56+
const exprt condition = renamed_b;
57+
goto_state.apply_condition(condition, state, ns);
58+
59+
THEN("b should be in the constant propagator with value 'true'")
60+
{
61+
auto it = goto_state.propagation.find(
62+
to_ssa_expr(renamed_b).get_l1_object_identifier());
63+
REQUIRE(it);
64+
REQUIRE(it->get() == true_exprt{});
65+
}
66+
}
67+
68+
WHEN("Applying the condition '!b'")
69+
{
70+
const exprt condition = not_exprt{renamed_b};
71+
goto_state.apply_condition(condition, state, ns);
72+
73+
THEN("b should be in the constant propagator with value 'false'")
74+
{
75+
auto it = goto_state.propagation.find(
76+
to_ssa_expr(renamed_b).get_l1_object_identifier());
77+
REQUIRE(it);
78+
REQUIRE(it->get() == false_exprt{});
79+
}
80+
}
81+
82+
WHEN("Applying the condition 'b == true'")
83+
{
84+
const exprt condition = equal_exprt{renamed_b, true_exprt{}};
85+
goto_state.apply_condition(condition, state, ns);
86+
87+
THEN("b should be in the constant propagator with value 'true'")
88+
{
89+
auto it = goto_state.propagation.find(
90+
to_ssa_expr(renamed_b).get_l1_object_identifier());
91+
REQUIRE(it);
92+
REQUIRE(it->get() == true_exprt{});
93+
}
94+
}
95+
96+
WHEN("Applying the condition 'b == false'")
97+
{
98+
const exprt condition = equal_exprt{renamed_b, false_exprt{}};
99+
goto_state.apply_condition(condition, state, ns);
100+
101+
THEN("b should be in the constant propagator with value 'false'")
102+
{
103+
auto it = goto_state.propagation.find(
104+
to_ssa_expr(renamed_b).get_l1_object_identifier());
105+
REQUIRE(it);
106+
REQUIRE(it->get() == false_exprt{});
107+
}
108+
}
109+
110+
WHEN("Applying the condition '!(b == true)'")
111+
{
112+
const exprt condition = not_exprt{equal_exprt{renamed_b, true_exprt{}}};
113+
goto_state.apply_condition(condition, state, ns);
114+
115+
THEN("b should be in the constant propagator with value 'false'")
116+
{
117+
auto it = goto_state.propagation.find(
118+
to_ssa_expr(renamed_b).get_l1_object_identifier());
119+
REQUIRE(it);
120+
REQUIRE(it->get() == false_exprt{});
121+
}
122+
}
123+
124+
WHEN("Applying the condition '!(b == false)'")
125+
{
126+
const exprt condition = not_exprt{equal_exprt{renamed_b, false_exprt{}}};
127+
goto_state.apply_condition(condition, state, ns);
128+
129+
THEN("b should be in the constant propagator with value 'true'")
130+
{
131+
auto it = goto_state.propagation.find(
132+
to_ssa_expr(renamed_b).get_l1_object_identifier());
133+
REQUIRE(it);
134+
REQUIRE(it->get() == true_exprt{});
135+
}
136+
}
137+
138+
WHEN("Applying the condition 'b != true'")
139+
{
140+
const exprt condition = notequal_exprt{renamed_b, true_exprt{}};
141+
goto_state.apply_condition(condition, state, ns);
142+
143+
THEN("b should be in the constant propagator with value 'false'")
144+
{
145+
auto it = goto_state.propagation.find(
146+
to_ssa_expr(renamed_b).get_l1_object_identifier());
147+
REQUIRE(it);
148+
REQUIRE(it->get() == false_exprt{});
149+
}
150+
}
151+
152+
WHEN("Applying the condition 'b != false'")
153+
{
154+
const exprt condition = notequal_exprt{renamed_b, false_exprt{}};
155+
goto_state.apply_condition(condition, state, ns);
156+
157+
THEN("b should be in the constant propagator with value 'true'")
158+
{
159+
auto it = goto_state.propagation.find(
160+
to_ssa_expr(renamed_b).get_l1_object_identifier());
161+
REQUIRE(it);
162+
REQUIRE(it->get() == true_exprt{});
163+
}
164+
}
165+
166+
WHEN("Applying the condition '!(b != true)'")
167+
{
168+
const exprt condition = not_exprt{notequal_exprt{renamed_b, true_exprt{}}};
169+
goto_state.apply_condition(condition, state, ns);
170+
171+
THEN("b should be in the constant propagator with value 'true'")
172+
{
173+
auto it = goto_state.propagation.find(
174+
to_ssa_expr(renamed_b).get_l1_object_identifier());
175+
REQUIRE(it);
176+
REQUIRE(it->get() == true_exprt{});
177+
}
178+
}
179+
180+
WHEN("Applying the condition '!(b != false)'")
181+
{
182+
const exprt condition = not_exprt{notequal_exprt{renamed_b, false_exprt{}}};
183+
goto_state.apply_condition(condition, state, ns);
184+
185+
THEN("b should be in the constant propagator with value 'false'")
186+
{
187+
auto it = goto_state.propagation.find(
188+
to_ssa_expr(renamed_b).get_l1_object_identifier());
189+
REQUIRE(it);
190+
REQUIRE(it->get() == false_exprt{});
191+
}
192+
}
193+
194+
WHEN("Applying the condition 'b && c'")
195+
{
196+
const exprt condition = and_exprt{renamed_b, renamed_c};
197+
goto_state.apply_condition(condition, state, ns);
198+
199+
THEN("b should be in the constant propagator with value 'true'")
200+
{
201+
auto it = goto_state.propagation.find(
202+
to_ssa_expr(renamed_b).get_l1_object_identifier());
203+
REQUIRE(it);
204+
REQUIRE(it->get() == true_exprt{});
205+
}
206+
}
207+
}

0 commit comments

Comments
 (0)