Skip to content

Commit e18cb15

Browse files
author
Daniel Kroening
authored
Merge pull request #1070 from thk123/bugfix/simplify-lhs
Fixing simplification of LHS
2 parents 8400c8f + d4d976a commit e18cb15

File tree

3 files changed

+182
-9
lines changed

3 files changed

+182
-9
lines changed

‎src/analyses/ai.cpp

+13-9
Original file line numberDiff line numberDiff line change
@@ -57,29 +57,33 @@ bool ai_domain_baset::ai_simplify_lhs(
5757
if(condition.id()==ID_index)
5858
{
5959
index_exprt ie=to_index_expr(condition);
60-
bool changed=ai_simplify(ie.index(), ns);
61-
if(changed)
60+
bool no_simplification=ai_simplify(ie.index(), ns);
61+
if(!no_simplification)
6262
condition=simplify_expr(ie, ns);
6363

64-
return !changed;
64+
return no_simplification;
6565
}
6666
else if(condition.id()==ID_dereference)
6767
{
6868
dereference_exprt de=to_dereference_expr(condition);
69-
bool changed=ai_simplify(de.pointer(), ns);
70-
if(changed)
69+
bool no_simplification=ai_simplify(de.pointer(), ns);
70+
if(!no_simplification)
7171
condition=simplify_expr(de, ns); // So *(&x) -> x
7272

73-
return !changed;
73+
return no_simplification;
7474
}
7575
else if(condition.id()==ID_member)
7676
{
7777
member_exprt me=to_member_expr(condition);
78-
bool changed=ai_simplify_lhs(me.compound(), ns); // <-- lhs!
79-
if(changed)
78+
// Since simplify_ai_lhs is required to return an addressable object
79+
// (so remains a valid left hand side), to simplify
80+
// `(something_simplifiable).b` we require that `something_simplifiable`
81+
// must also be addressable
82+
bool no_simplification=ai_simplify_lhs(me.compound(), ns);
83+
if(!no_simplification)
8084
condition=simplify_expr(me, ns);
8185

82-
return !changed;
86+
return no_simplification;
8387
}
8488
else
8589
return true;

‎unit/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ SRC = src/expr/require_expr.cpp \
77

88
# Test source files
99
SRC += unit_tests.cpp \
10+
analyses/ai/ai_simplify_lhs.cpp \
1011
analyses/does_remove_const/does_expr_lose_const.cpp \
1112
analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
1213
analyses/does_remove_const/is_type_at_least_as_const_as.cpp \

‎unit/analyses/ai/ai_simplify_lhs.cpp

+168
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,168 @@
1+
/*******************************************************************\
2+
3+
Module: Unit tests for ai_domain_baset::ai_simplify_lhs
4+
5+
Author: DiffBlue Limited. All rights reserved.
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Unit tests for ai_domain_baset::ai_simplify_lhs
11+
12+
#include <catch.hpp>
13+
14+
#include <analyses/ai.h>
15+
16+
#include <ansi-c/ansi_c_language.h>
17+
18+
#include <util/arith_tools.h>
19+
#include <util/config.h>
20+
#include <util/namespace.h>
21+
#include <util/ui_message.h>
22+
#include <util/simplify_expr.h>
23+
24+
class constant_simplification_mockt:public ai_domain_baset
25+
{
26+
public:
27+
void transform(locationt, locationt, ai_baset &, const namespacet &) override
28+
{}
29+
void make_bottom() override
30+
{}
31+
void make_top() override
32+
{}
33+
void make_entry() override
34+
{}
35+
36+
bool ai_simplify(exprt &condition, const namespacet &ns) const override;
37+
};
38+
39+
bool constant_simplification_mockt::ai_simplify(
40+
exprt &condition, const namespacet &ns) const
41+
{
42+
exprt simplified_expr=simplify_expr(condition, ns);
43+
// no simplification
44+
if(simplified_expr==condition)
45+
{
46+
return true;
47+
}
48+
// a simplification has occurred
49+
condition=simplified_expr;
50+
return false;
51+
}
52+
53+
SCENARIO("ai_domain_baset::ai_simplify_lhs",
54+
"[core][analyses][ai][ai_simplify_lhs]")
55+
{
56+
ui_message_handlert message_handler;
57+
ansi_c_languaget language;
58+
language.set_message_handler(message_handler);
59+
60+
symbol_tablet symbol_table;
61+
namespacet ns(symbol_table);
62+
63+
constant_simplification_mockt mock_ai_domain;
64+
65+
config.set_arch("none");
66+
67+
GIVEN("A index_exprt")
68+
{
69+
// Construct an expression that the simplify_expr can simplify
70+
exprt simplifiable_expression;
71+
bool compile_failed=
72+
language.to_expr("1 + 1", "", simplifiable_expression, ns);
73+
74+
const unsigned int array_size=5;
75+
array_typet array_type(
76+
signedbv_typet(32), constant_exprt::integer_constant(array_size));
77+
78+
// Verify the results of the setup
79+
REQUIRE_FALSE(compile_failed);\
80+
REQUIRE(simplifiable_expression.id()==ID_plus);
81+
exprt simplified_version=simplify_expr(simplifiable_expression, ns);
82+
REQUIRE(simplified_version.id()==ID_constant);
83+
84+
WHEN(
85+
"Simplifying an index expression with constant index but variable array")
86+
{
87+
const index_exprt &index_expr=
88+
index_exprt(symbol_exprt("a", array_type), simplifiable_expression);
89+
90+
THEN("Then only the index of the part of the expression should be "
91+
"simplified")
92+
{
93+
exprt out_expr=index_expr;
94+
bool no_simplification=mock_ai_domain.ai_simplify_lhs(out_expr, ns);
95+
REQUIRE_FALSE(no_simplification);
96+
REQUIRE(index_expr.id()==ID_index);
97+
98+
index_exprt simplified_index_expr=to_index_expr(out_expr);
99+
REQUIRE(simplified_index_expr.index().id()==ID_constant);
100+
101+
constant_exprt constant_index=
102+
to_constant_expr(simplified_index_expr.index());
103+
104+
mp_integer out_index;
105+
bool failed_to_integer=to_integer(constant_index, out_index);
106+
REQUIRE_FALSE(failed_to_integer);
107+
REQUIRE(out_index==2);
108+
}
109+
}
110+
WHEN("Simplifying an index expression with variable index and array")
111+
{
112+
// a[i]
113+
const index_exprt &index_expr=
114+
index_exprt(
115+
symbol_exprt("a", array_type), symbol_exprt("i", signedbv_typet(32)));
116+
117+
THEN("Then no simplification should occur")
118+
{
119+
exprt out_expr=index_expr;
120+
bool no_simplification=mock_ai_domain.ai_simplify_lhs(out_expr, ns);
121+
REQUIRE(no_simplification);
122+
REQUIRE(index_expr.id()==ID_index);
123+
124+
index_exprt simplified_index_expr=to_index_expr(out_expr);
125+
REQUIRE(simplified_index_expr.index().id()==ID_symbol);
126+
}
127+
}
128+
129+
// This fails since the implementation does do a constant simplification
130+
// on the array part. It isn't clear to me if this is correct
131+
#if 0
132+
WHEN(
133+
"Simplifying an index expression with constant index in a constant array")
134+
{
135+
array_exprt constant_array=array_exprt(array_type);
136+
for(unsigned int i=0; i<array_size; ++i)
137+
{
138+
REQUIRE(constant_array.operands().size()==i);
139+
constant_array.operands().push_back(
140+
constant_exprt::integer_constant(i));
141+
}
142+
143+
const index_exprt &index_expr=
144+
index_exprt(constant_array, simplifiable_expression);
145+
146+
THEN("Then only the index of the part of the expression should be "
147+
"simplified")
148+
{
149+
exprt out_expr=index_expr;
150+
bool no_simplification=mock_ai_domain.ai_simplify_lhs(out_expr, ns);
151+
REQUIRE_FALSE(no_simplification);
152+
REQUIRE(out_expr.id()==ID_index);
153+
154+
index_exprt simplified_index_expr=to_index_expr(out_expr);
155+
REQUIRE(simplified_index_expr.index().id()==ID_constant);
156+
157+
constant_exprt constant_index=
158+
to_constant_expr(simplified_index_expr.index());
159+
160+
mp_integer out_index;
161+
bool failed_to_integer=to_integer(constant_index, out_index);
162+
REQUIRE_FALSE(failed_to_integer);
163+
REQUIRE(out_index==2);
164+
}
165+
}
166+
#endif
167+
}
168+
}

0 commit comments

Comments
 (0)