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