Skip to content

Commit 7b9f559

Browse files
jezhigginsjezhiggins
committed
constant_abstract_valuet expression_transform unit tests
Simple tests where all operands are constant_abstract_valuets, capturing and confirming existing behaviour.
1 parent bf8fc59 commit 7b9f559

File tree

6 files changed

+176
-65
lines changed

6 files changed

+176
-65
lines changed

‎unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ SRC += analyses/ai/ai.cpp \
1616
analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
1717
analyses/variable-sensitivity/abstract_object/merge.cpp \
1818
analyses/variable-sensitivity/abstract_object/index_range.cpp \
19+
analyses/variable-sensitivity/constant_abstract_value/expression_evaluation.cpp \
1920
analyses/variable-sensitivity/constant_abstract_value/merge.cpp \
2021
analyses/variable-sensitivity/full_array_abstract_object/merge.cpp \
2122
analyses/variable-sensitivity/eval.cpp \

‎unit/analyses/variable-sensitivity/constant_abstract_value/expression_evaluation.cpp

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
/*******************************************************************\
2+
3+
Module: Unit tests for constant_abstract_valuet::expression_transform
4+
5+
Author: Jez Higgins, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "../variable_sensitivity_test_helpers.h"
10+
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
11+
#include <testing-utils/use_catch.h>
12+
#include <util/arith_tools.h>
13+
#include <util/mathematical_types.h>
14+
15+
SCENARIO(
16+
"constants expression evaluation",
17+
"[core][analyses][variable-sensitivity][constant_abstract_value][expression_"
18+
"transform]")
19+
{
20+
const exprt val1 = from_integer(1, integer_typet());
21+
const exprt val2 = from_integer(2, integer_typet());
22+
const exprt val3 = from_integer(3, integer_typet());
23+
24+
auto config = vsd_configt::constant_domain();
25+
config.context_tracking.data_dependency_context = false;
26+
config.context_tracking.last_write_context = false;
27+
auto object_factory =
28+
variable_sensitivity_object_factoryt::configured_with(config);
29+
abstract_environmentt environment{object_factory};
30+
environment.make_top();
31+
symbol_tablet symbol_table;
32+
namespacet ns(symbol_table);
33+
34+
GIVEN("adding two constants")
35+
{
36+
WHEN("1 + 2")
37+
{
38+
auto op1 = make_constant(val1, environment, ns);
39+
auto op2 = make_constant(val2, environment, ns);
40+
auto result = add_as_constant(op1, op2, environment, ns);
41+
42+
THEN("= 3")
43+
{
44+
EXPECT(result, val3);
45+
}
46+
}
47+
WHEN("1 + TOP")
48+
{
49+
auto op1 = make_constant(val1, environment, ns);
50+
auto op2 = make_constant(val2, true);
51+
auto result = add_as_constant(op1, op2, environment, ns);
52+
53+
THEN("= TOP")
54+
{
55+
EXPECT_TOP(result);
56+
}
57+
}
58+
WHEN("TOP + 1")
59+
{
60+
auto op1 = make_constant(val1, true);
61+
auto op2 = make_constant(val2, environment, ns);
62+
auto result = add_as_constant(op1, op2, environment, ns);
63+
64+
THEN("= TOP")
65+
{
66+
EXPECT_TOP(result);
67+
}
68+
}
69+
}
70+
}

‎unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,8 @@
1414
#include <testing-utils/use_catch.h>
1515
#include <typeinfo>
1616
#include <util/arith_tools.h>
17-
#include <util/c_types.h>
1817
#include <util/mathematical_types.h>
1918
#include <util/namespace.h>
20-
#include <util/std_expr.h>
2119
#include <util/symbol_table.h>
2220

2321
struct constant_merge_result

‎unit/analyses/variable-sensitivity/value_set_abstract_object/expression_evaluation.cpp

Lines changed: 13 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -12,21 +12,10 @@
1212
#include <util/arith_tools.h>
1313
#include <util/mathematical_types.h>
1414

15-
static std::shared_ptr<const value_set_abstract_objectt> add_values(
16-
const abstract_object_pointert &op1,
17-
const abstract_object_pointert &op2,
18-
abstract_environmentt &environment,
19-
namespacet &ns);
20-
static std::shared_ptr<const value_set_abstract_objectt> add_values(
21-
const abstract_object_pointert &op1,
22-
const abstract_object_pointert &op2,
23-
const abstract_object_pointert &op3,
24-
abstract_environmentt &environment,
25-
namespacet &ns);
26-
2715
SCENARIO(
2816
"value_set expression evaluation",
29-
"[core][analyses][variable-sensitivity][value_set_abstract_object]")
17+
"[core][analyses][variable-sensitivity][value_set_abstract_object]["
18+
"expression_transform]")
3019
{
3120
const exprt val1 = from_integer(1, integer_typet());
3221
const exprt val2 = from_integer(2, integer_typet());
@@ -50,7 +39,7 @@ SCENARIO(
5039
{
5140
auto op1 = make_value_set(val1, environment, ns);
5241
auto op2 = make_value_set(val1, environment, ns);
53-
auto result = add_values(op1, op2, environment, ns);
42+
auto result = add_as_value_set(op1, op2, environment, ns);
5443

5544
THEN("= { 2 }")
5645
{
@@ -61,7 +50,7 @@ SCENARIO(
6150
{
6251
auto op1 = make_value_set({val1, val2}, environment, ns);
6352
auto op2 = make_value_set(val1, environment, ns);
64-
auto result = add_values(op1, op2, environment, ns);
53+
auto result = add_as_value_set(op1, op2, environment, ns);
6554

6655
THEN("= { 2, 3 }")
6756
{
@@ -72,7 +61,7 @@ SCENARIO(
7261
{
7362
auto op1 = make_value_set({val1, val2}, environment, ns);
7463
auto op2 = make_value_set(val1, environment, ns);
75-
auto result = add_values(op1, op2, environment, ns);
64+
auto result = add_as_value_set(op1, op2, environment, ns);
7665

7766
THEN("= { 2, 3 }")
7867
{
@@ -83,7 +72,7 @@ SCENARIO(
8372
{
8473
auto op1 = make_value_set({val1, val2}, environment, ns);
8574
auto op2 = make_value_set(val1, environment, ns);
86-
auto result = add_values(op1, op2, environment, ns);
75+
auto result = add_as_value_set(op1, op2, environment, ns);
8776

8877
THEN("= { 2, 3 }")
8978
{
@@ -94,7 +83,7 @@ SCENARIO(
9483
{
9584
auto op1 = make_value_set({val1, val2}, environment, ns);
9685
auto op2 = make_value_set({val1, val2, val3}, environment, ns);
97-
auto result = add_values(op1, op2, environment, ns);
86+
auto result = add_as_value_set(op1, op2, environment, ns);
9887

9988
THEN("= { 2, 3, 4, 5 }")
10089
{
@@ -108,7 +97,7 @@ SCENARIO(
10897
{
10998
auto op1 = make_value_set(val1, environment, ns);
11099
auto op2 = make_constant(val1, environment, ns);
111-
auto result = add_values(op1, op2, environment, ns);
100+
auto result = add_as_value_set(op1, op2, environment, ns);
112101

113102
THEN("= { 2 }")
114103
{
@@ -119,7 +108,7 @@ SCENARIO(
119108
{
120109
auto op1 = make_value_set({val2, val3, val4}, environment, ns);
121110
auto op2 = make_constant(val1, environment, ns);
122-
auto result = add_values(op1, op2, environment, ns);
111+
auto result = add_as_value_set(op1, op2, environment, ns);
123112

124113
THEN("= { 3, 4, 5 }")
125114
{
@@ -135,7 +124,7 @@ SCENARIO(
135124
auto op2 = make_constant(val1, environment, ns);
136125
auto op3 = make_constant(val1, environment, ns);
137126

138-
auto result = add_values(op1, op2, op3, environment, ns);
127+
auto result = add_as_value_set(op1, op2, op3, environment, ns);
139128

140129
THEN("= { 3, 4, 5 }")
141130
{
@@ -148,7 +137,7 @@ SCENARIO(
148137
auto op2 = make_value_set(val1, environment, ns);
149138
auto op3 = make_constant(val1, environment, ns);
150139

151-
auto result = add_values(op1, op2, op3, environment, ns);
140+
auto result = add_as_value_set(op1, op2, op3, environment, ns);
152141

153142
THEN("= { 3, 4, 5 }")
154143
{
@@ -164,7 +153,7 @@ SCENARIO(
164153
auto op2 = std::make_shared<constant_abstract_valuet>(val1.type());
165154
REQUIRE(op2->is_top());
166155

167-
auto result = add_values(op1, op2, environment, ns);
156+
auto result = add_as_value_set(op1, op2, environment, ns);
168157

169158
THEN("the result is top")
170159
{
@@ -177,7 +166,7 @@ SCENARIO(
177166
auto op2 = std::make_shared<value_set_abstract_objectt>(val1.type());
178167
REQUIRE(op2->is_top());
179168

180-
auto result = add_values(op1, op2, environment, ns);
169+
auto result = add_as_value_set(op1, op2, environment, ns);
181170

182171
THEN("the result is top")
183172
{
@@ -186,39 +175,3 @@ SCENARIO(
186175
}
187176
}
188177
}
189-
190-
static std::shared_ptr<const value_set_abstract_objectt> add_values(
191-
const abstract_object_pointert &op1,
192-
const abstract_object_pointert &op2,
193-
abstract_environmentt &environment,
194-
namespacet &ns)
195-
{
196-
auto op1_sym = symbol_exprt("op1", op1->type());
197-
auto op2_sym = symbol_exprt("op2", op2->type());
198-
environment.assign(op1_sym, op1, ns);
199-
environment.assign(op2_sym, op2, ns);
200-
201-
auto result = environment.eval(plus_exprt(op1_sym, op2_sym), ns);
202-
203-
return as_value_set(result);
204-
}
205-
206-
static std::shared_ptr<const value_set_abstract_objectt> add_values(
207-
const abstract_object_pointert &op1,
208-
const abstract_object_pointert &op2,
209-
const abstract_object_pointert &op3,
210-
abstract_environmentt &environment,
211-
namespacet &ns)
212-
{
213-
auto op1_sym = symbol_exprt("op1", op1->type());
214-
auto op2_sym = symbol_exprt("op2", op2->type());
215-
auto op3_sym = symbol_exprt("op3", op3->type());
216-
environment.assign(op1_sym, op1, ns);
217-
environment.assign(op2_sym, op2, ns);
218-
environment.assign(op3_sym, op3, ns);
219-
220-
auto result =
221-
environment.eval(plus_exprt(plus_exprt(op1_sym, op2_sym), op3_sym), ns);
222-
223-
return as_value_set(result);
224-
}

‎unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp

Lines changed: 74 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
\*******************************************************************/
88

99
#include "variable_sensitivity_test_helpers.h"
10+
#include <analyses/variable-sensitivity/abstract_environment.h>
1011
#include <ansi-c/ansi_c_language.h>
1112
#include <testing-utils/use_catch.h>
1213
#include <util/string_utils.h>
@@ -107,11 +108,14 @@ void EXPECT(
107108
{
108109
REQUIRE(result);
109110

110-
// Correctness of merge
111111
REQUIRE_FALSE(result->is_top());
112112
REQUIRE_FALSE(result->is_bottom());
113113

114-
REQUIRE(result->to_constant() == expected_value);
114+
auto result_expr = result->to_constant();
115+
INFO(
116+
"Expect " + expr_to_str(result_expr) + " to equal " +
117+
expr_to_str(expected_value));
118+
REQUIRE(result_expr == expected_value);
115119
}
116120

117121
void EXPECT(
@@ -120,7 +124,6 @@ void EXPECT(
120124
{
121125
REQUIRE(result);
122126

123-
// Correctness of merge
124127
REQUIRE_FALSE(result->is_top());
125128
REQUIRE_FALSE(result->is_bottom());
126129

@@ -190,3 +193,71 @@ void EXPECT_BOTTOM(std::shared_ptr<const abstract_objectt> result)
190193
REQUIRE_FALSE(result->is_top());
191194
REQUIRE(result->is_bottom());
192195
}
196+
197+
static std::shared_ptr<const abstract_objectt> add(
198+
const abstract_object_pointert &op1,
199+
const abstract_object_pointert &op2,
200+
abstract_environmentt &environment,
201+
namespacet &ns)
202+
{
203+
auto op1_sym = symbol_exprt("op1", op1->type());
204+
auto op2_sym = symbol_exprt("op2", op2->type());
205+
environment.assign(op1_sym, op1, ns);
206+
environment.assign(op2_sym, op2, ns);
207+
208+
auto result = environment.eval(plus_exprt(op1_sym, op2_sym), ns);
209+
210+
return result;
211+
}
212+
213+
std::shared_ptr<const constant_abstract_valuet> add_as_constant(
214+
const abstract_object_pointert &op1,
215+
const abstract_object_pointert &op2,
216+
abstract_environmentt &environment,
217+
namespacet &ns)
218+
{
219+
auto result = add(op1, op2, environment, ns);
220+
auto cv = as_constant(result);
221+
222+
INFO("Result should be a constant")
223+
REQUIRE(cv);
224+
return cv;
225+
}
226+
227+
std::shared_ptr<const value_set_abstract_objectt> add_as_value_set(
228+
const abstract_object_pointert &op1,
229+
const abstract_object_pointert &op2,
230+
abstract_environmentt &environment,
231+
namespacet &ns)
232+
{
233+
auto result = add(op1, op2, environment, ns);
234+
auto vs = as_value_set(result);
235+
236+
INFO("Result should be a value set")
237+
REQUIRE(vs);
238+
return vs;
239+
}
240+
241+
std::shared_ptr<const value_set_abstract_objectt> add_as_value_set(
242+
const abstract_object_pointert &op1,
243+
const abstract_object_pointert &op2,
244+
const abstract_object_pointert &op3,
245+
abstract_environmentt &environment,
246+
namespacet &ns)
247+
{
248+
auto op1_sym = symbol_exprt("op1", op1->type());
249+
auto op2_sym = symbol_exprt("op2", op2->type());
250+
auto op3_sym = symbol_exprt("op3", op3->type());
251+
environment.assign(op1_sym, op1, ns);
252+
environment.assign(op2_sym, op2, ns);
253+
environment.assign(op3_sym, op3, ns);
254+
255+
auto result =
256+
environment.eval(plus_exprt(plus_exprt(op1_sym, op2_sym), op3_sym), ns);
257+
258+
auto vs = as_value_set(result);
259+
260+
INFO("Result should be a value set")
261+
REQUIRE(vs);
262+
return vs;
263+
}

‎unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,3 +58,21 @@ void EXPECT_UNMODIFIED(
5858
std::shared_ptr<const value_set_abstract_objectt> &result,
5959
bool modified,
6060
const std::vector<exprt> &expected_values);
61+
62+
std::shared_ptr<const constant_abstract_valuet> add_as_constant(
63+
const abstract_object_pointert &op1,
64+
const abstract_object_pointert &op2,
65+
abstract_environmentt &environment,
66+
namespacet &ns);
67+
68+
std::shared_ptr<const value_set_abstract_objectt> add_as_value_set(
69+
const abstract_object_pointert &op1,
70+
const abstract_object_pointert &op2,
71+
abstract_environmentt &environment,
72+
namespacet &ns);
73+
std::shared_ptr<const value_set_abstract_objectt> add_as_value_set(
74+
const abstract_object_pointert &op1,
75+
const abstract_object_pointert &op2,
76+
const abstract_object_pointert &op3,
77+
abstract_environmentt &environment,
78+
namespacet &ns);

0 commit comments

Comments
 (0)