Skip to content

Commit 6514482

Browse files
tautschnigtautschnig
authored
Merge pull request #4774 from romainbrenguier/unit-test/try-evaluate-pointer-comparison
Unit-test try_evaluate_pointer_comparison and bugfix
2 parents 81fb889 + 767d8f0 commit 6514482

File tree

4 files changed

+282
-12
lines changed

4 files changed

+282
-12
lines changed

‎src/goto-symex/goto_symex.h

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -726,4 +726,20 @@ void symex_transition(
726726
goto_programt::const_targett to,
727727
bool is_backwards_goto);
728728

729+
/// Try to evaluate pointer comparisons where they can be trivially determined
730+
/// using the value-set. This is optional as all it does is allow symex to
731+
/// resolve some comparisons itself and therefore create a simpler formula for
732+
/// the SAT solver.
733+
/// \param [in,out] condition: An L2-renamed expression with boolean type
734+
/// \param value_set: The value-set for determining what pointer-typed symbols
735+
/// might possibly point to
736+
/// \param language_mode: The language mode
737+
/// \param ns: A namespace
738+
/// \return The possibly modified condition
739+
renamedt<exprt, L2> try_evaluate_pointer_comparisons(
740+
renamedt<exprt, L2> condition,
741+
const value_sett &value_set,
742+
const irep_idt &language_mode,
743+
const namespacet &ns);
744+
729745
#endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H

‎src/goto-symex/symex_goto.cpp

Lines changed: 4 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -100,8 +100,10 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
100100
const ssa_exprt *ssa_symbol_expr =
101101
expr_try_dynamic_cast<ssa_exprt>(symbol_expr);
102102

103+
ssa_exprt l1_expr{*ssa_symbol_expr};
104+
l1_expr.remove_level_2();
103105
const std::vector<exprt> value_set_elements =
104-
value_set.get_value_set(ssa_symbol_expr->get_l1_object(), ns);
106+
value_set.get_value_set(l1_expr, ns);
105107

106108
bool constant_found = false;
107109

@@ -196,17 +198,7 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
196198
expr.id(), *symbol_expr_lhs, rhs, value_set, language_mode, ns);
197199
}
198200

199-
/// Try to evaluate pointer comparisons where they can be trivially determined
200-
/// using the value-set. This is optional as all it does is allow symex to
201-
/// resolve some comparisons itself and therefore create a simpler formula for
202-
/// the SAT solver.
203-
/// \param [in,out] condition: An L2-renamed expression with boolean type
204-
/// \param value_set: The value-set for determining what pointer-typed symbols
205-
/// might possibly point to
206-
/// \param language_mode: The language mode
207-
/// \param ns: A namespace
208-
/// \return The possibly modified condition
209-
static renamedt<exprt, L2> try_evaluate_pointer_comparisons(
201+
renamedt<exprt, L2> try_evaluate_pointer_comparisons(
210202
renamedt<exprt, L2> condition,
211203
const value_sett &value_set,
212204
const irep_idt &language_mode,

‎unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ SRC += analyses/ai/ai.cpp \
3535
goto-symex/is_constant.cpp \
3636
goto-symex/symex_level0.cpp \
3737
goto-symex/symex_level1.cpp \
38+
goto-symex/try_evaluate_pointer_comparisons.cpp \
3839
interpreter/interpreter.cpp \
3940
json/json_parser.cpp \
4041
json_symbol_table.cpp \

‎unit/goto-symex/try_evaluate_pointer_comparisons.cpp

Lines changed: 261 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,261 @@
1+
/*******************************************************************\
2+
3+
Module: Unit tests for try_evaluate_pointer_comparisons
4+
5+
Author: Romain Brenguier, [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+
#include <util/arith_tools.h>
14+
#include <util/c_types.h>
15+
16+
static void add_to_symbol_table(
17+
symbol_tablet &symbol_table,
18+
const symbol_exprt &symbol_expr)
19+
{
20+
symbolt symbol;
21+
symbol.name = symbol_expr.get_identifier();
22+
symbol.type = symbol_expr.type();
23+
symbol.value = symbol_expr;
24+
symbol.is_thread_local = true;
25+
symbol_table.insert(symbol);
26+
}
27+
28+
SCENARIO(
29+
"Try to evaluate pointer comparisons",
30+
"[core][goto-symex][try_evaluate_pointer_comparisons]")
31+
{
32+
const unsignedbv_typet int_type{32};
33+
const pointer_typet ptr_type = pointer_type(int_type);
34+
const symbol_exprt ptr1{"ptr1", ptr_type};
35+
const symbol_exprt ptr2{"ptr2", ptr_type};
36+
const symbol_exprt value1{"value1", int_type};
37+
const address_of_exprt address1{value1};
38+
const symbol_exprt value2{"value2", int_type};
39+
const address_of_exprt address2{value2};
40+
const symbol_exprt b{"b", bool_typet{}};
41+
const null_pointer_exprt null_ptr{ptr_type};
42+
43+
// Add symbols to symbol table
44+
symbol_tablet symbol_table;
45+
namespacet ns{symbol_table};
46+
add_to_symbol_table(symbol_table, ptr1);
47+
add_to_symbol_table(symbol_table, ptr2);
48+
add_to_symbol_table(symbol_table, value1);
49+
add_to_symbol_table(symbol_table, value2);
50+
add_to_symbol_table(symbol_table, b);
51+
52+
// Initialize goto state
53+
std::list<goto_programt::instructiont> target;
54+
symex_targett::sourcet source{"fun", target.begin()};
55+
guard_managert guard_manager;
56+
std::size_t count = 0;
57+
auto fresh_name = [&count](const irep_idt &) { return count++; };
58+
goto_symex_statet state{source, guard_manager, fresh_name};
59+
60+
GIVEN("A value set in which pointer symbol `ptr1` only points to `&value1`")
61+
{
62+
value_sett value_set;
63+
const renamedt<exprt, L1> ptr1_l1 = state.rename<L1>(ptr1, ns);
64+
const renamedt<exprt, L1> address1_l1 = state.rename<L1>(address1, ns);
65+
// ptr1 <- &value1
66+
value_set.assign(ptr1_l1.get(), address1_l1.get(), ns, false, false);
67+
68+
WHEN("Evaluating ptr1 == &value1")
69+
{
70+
const equal_exprt comparison{ptr1, address1};
71+
const renamedt<exprt, L2> renamed_comparison =
72+
state.rename(comparison, ns);
73+
auto result = try_evaluate_pointer_comparisons(
74+
renamed_comparison, value_set, ID_java, ns);
75+
THEN("Evaluation succeeds")
76+
{
77+
REQUIRE(result.get() == true_exprt{});
78+
}
79+
}
80+
81+
WHEN("Evaluating ptr1 != &value1")
82+
{
83+
const notequal_exprt comparison{ptr1, address1};
84+
const renamedt<exprt, L2> renamed_comparison =
85+
state.rename(comparison, ns);
86+
auto result = try_evaluate_pointer_comparisons(
87+
renamed_comparison, value_set, ID_java, ns);
88+
THEN("Evaluation succeeds")
89+
{
90+
REQUIRE(result.get() == false_exprt{});
91+
}
92+
}
93+
94+
WHEN("Evaluating ptr1 == ptr2")
95+
{
96+
const equal_exprt comparison{ptr1, ptr2};
97+
const renamedt<exprt, L2> renamed_comparison =
98+
state.rename(comparison, ns);
99+
auto result = try_evaluate_pointer_comparisons(
100+
renamed_comparison, value_set, ID_java, ns);
101+
THEN("Evaluation leaves the expression unchanged")
102+
{
103+
REQUIRE(result.get() == renamed_comparison.get());
104+
}
105+
}
106+
}
107+
108+
GIVEN(
109+
"A value set in which pointer symbol `ptr1` can point to `&value1` or "
110+
"`&value2`")
111+
{
112+
value_sett value_set;
113+
const if_exprt if_expr{b, address1, address2};
114+
const renamedt<exprt, L1> ptr1_l1 = state.rename<L1>(ptr1, ns);
115+
const renamedt<exprt, L1> if_expr_l1 = state.rename<L1>(if_expr, ns);
116+
// ptr1 <- b ? &value1 : &value2
117+
value_set.assign(ptr1_l1.get(), if_expr_l1.get(), ns, false, false);
118+
119+
WHEN("Evaluating ptr1 == &value1")
120+
{
121+
const equal_exprt comparison{ptr1, address1};
122+
const renamedt<exprt, L2> renamed_comparison =
123+
state.rename(comparison, ns);
124+
auto result = try_evaluate_pointer_comparisons(
125+
renamed_comparison, value_set, ID_java, ns);
126+
THEN("Evaluation leaves the expression unchanged")
127+
{
128+
REQUIRE(result.get() == renamed_comparison.get());
129+
}
130+
}
131+
132+
WHEN("Evaluating ptr1 != &value1")
133+
{
134+
const notequal_exprt comparison{ptr1, address1};
135+
const renamedt<exprt, L2> renamed_comparison =
136+
state.rename(comparison, ns);
137+
auto result = try_evaluate_pointer_comparisons(
138+
renamed_comparison, value_set, ID_java, ns);
139+
THEN("Evaluation leaves the expression unchanged")
140+
{
141+
REQUIRE(result.get() == renamed_comparison.get());
142+
}
143+
}
144+
145+
WHEN("Evaluating ptr1 != nullptr")
146+
{
147+
const notequal_exprt comparison{ptr1, null_ptr};
148+
const renamedt<exprt, L2> renamed_comparison =
149+
state.rename(comparison, ns);
150+
auto result = try_evaluate_pointer_comparisons(
151+
renamed_comparison, value_set, ID_java, ns);
152+
THEN("Evaluation succeeds")
153+
{
154+
REQUIRE(result.get() == true_exprt{});
155+
}
156+
}
157+
}
158+
159+
GIVEN(
160+
"A value set in which pointer symbol `ptr1` can point to `&value1` or "
161+
"`unknown`")
162+
{
163+
value_sett value_set;
164+
const exprt unknown_expr{ID_unknown, ptr_type};
165+
const if_exprt if_expr{b, address1, unknown_expr};
166+
const renamedt<exprt, L1> ptr1_l1 = state.rename<L1>(ptr1, ns);
167+
const renamedt<exprt, L1> if_expr_l1 = state.rename<L1>(if_expr, ns);
168+
// ptr1 <- b ? &value1 : unknown
169+
value_set.assign(ptr1_l1.get(), if_expr_l1.get(), ns, false, false);
170+
171+
WHEN("Evaluating ptr1 == &value1")
172+
{
173+
const equal_exprt comparison{ptr1, address1};
174+
const renamedt<exprt, L2> renamed_comparison =
175+
state.rename(comparison, ns);
176+
auto result = try_evaluate_pointer_comparisons(
177+
renamed_comparison, value_set, ID_java, ns);
178+
THEN("Evaluation leaves the expression unchanged")
179+
{
180+
REQUIRE(result.get() == renamed_comparison.get());
181+
}
182+
}
183+
184+
WHEN("Evaluating ptr1 != &value1")
185+
{
186+
const notequal_exprt comparison{ptr1, address1};
187+
const renamedt<exprt, L2> renamed_comparison =
188+
state.rename(comparison, ns);
189+
auto result = try_evaluate_pointer_comparisons(
190+
renamed_comparison, value_set, ID_java, ns);
191+
THEN("Evaluation leaves the expression unchanged")
192+
{
193+
REQUIRE(result.get() == renamed_comparison.get());
194+
}
195+
}
196+
197+
WHEN("Evaluating ptr1 != nullptr")
198+
{
199+
const notequal_exprt comparison{ptr1, null_ptr};
200+
const renamedt<exprt, L2> renamed_comparison =
201+
state.rename(comparison, ns);
202+
auto result = try_evaluate_pointer_comparisons(
203+
renamed_comparison, value_set, ID_java, ns);
204+
THEN("Evaluation leaves the expression unchanged")
205+
{
206+
REQUIRE(result.get() == renamed_comparison.get());
207+
}
208+
}
209+
}
210+
211+
GIVEN("A struct whose first element can only point to `&value1`")
212+
{
213+
// member is `struct_symbol.pointer_field`
214+
const member_exprt member = [&]() {
215+
std::vector<struct_typet::componentt> components;
216+
components.emplace_back("pointer_field", ptr_type);
217+
const struct_typet struct_type{components};
218+
const symbol_exprt struct_symbol{"struct_symbol", struct_type};
219+
add_to_symbol_table(symbol_table, struct_symbol);
220+
return member_exprt{struct_symbol, components.back()};
221+
}();
222+
223+
value_sett value_set;
224+
const renamedt<exprt, L1> member_l1 = state.rename<L1>(member, ns);
225+
const renamedt<exprt, L1> address1_l1 = state.rename<L1>(address1, ns);
226+
227+
// struct_symbol..pointer_field <- &value1
228+
{
229+
field_sensitivityt field_sensitivity;
230+
const exprt index_fs =
231+
field_sensitivity.apply(ns, state, member_l1.get(), true);
232+
value_set.assign(index_fs, address1_l1.get(), ns, false, false);
233+
}
234+
235+
WHEN("Evaluating struct_symbol.pointer_field == &value1")
236+
{
237+
const equal_exprt comparison{member, address1};
238+
const renamedt<exprt, L2> renamed_comparison =
239+
state.rename(comparison, ns);
240+
auto result = try_evaluate_pointer_comparisons(
241+
renamed_comparison, value_set, ID_java, ns);
242+
THEN("Evaluation succeeds")
243+
{
244+
REQUIRE(result.get() == true_exprt{});
245+
}
246+
}
247+
248+
WHEN("Evaluating struct_symbol.pointer_field == &value2")
249+
{
250+
const equal_exprt comparison{member, address2};
251+
const renamedt<exprt, L2> renamed_comparison =
252+
state.rename(comparison, ns);
253+
auto result = try_evaluate_pointer_comparisons(
254+
renamed_comparison, value_set, ID_java, ns);
255+
THEN("Evaluation succeeds")
256+
{
257+
REQUIRE(result.get() == false_exprt{});
258+
}
259+
}
260+
}
261+
}

0 commit comments

Comments
 (0)