Skip to content

Commit 7af8e92

Browse files
jezhigginsjezhiggins
committed
vsd to_predicate(expr)
1 parent 664f021 commit 7af8e92

File tree

7 files changed

+156
-2
lines changed

7 files changed

+156
-2
lines changed

‎src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

+26
Original file line numberDiff line numberDiff line change
@@ -181,6 +181,32 @@ exprt variable_sensitivity_domaint::to_predicate() const
181181
return abstract_state.to_predicate();
182182
}
183183

184+
exprt variable_sensitivity_domaint::to_predicate(
185+
const exprt &expr,
186+
const namespacet &ns) const
187+
{
188+
auto result = abstract_state.eval(expr, ns);
189+
return result->to_predicate(expr);
190+
}
191+
192+
exprt variable_sensitivity_domaint::to_predicate(
193+
const exprt::operandst &exprs,
194+
const namespacet &ns) const
195+
{
196+
if(exprs.empty())
197+
return false_exprt();
198+
if(exprs.size() == 1)
199+
return to_predicate(exprs.front(), ns);
200+
201+
auto predicates = std::vector<exprt>{};
202+
std::transform(
203+
exprs.cbegin(),
204+
exprs.cend(),
205+
std::back_inserter(predicates),
206+
[this, &ns](const exprt &expr) { return to_predicate(expr, ns); });
207+
return and_exprt(predicates);
208+
}
209+
184210
void variable_sensitivity_domaint::make_bottom()
185211
{
186212
abstract_state.make_bottom();

‎src/analyses/variable-sensitivity/variable_sensitivity_domain.h

+3
Original file line numberDiff line numberDiff line change
@@ -152,6 +152,9 @@ class variable_sensitivity_domaint : public ai_domain_baset
152152
/// \return exprt describing the domain
153153
exprt to_predicate() const override;
154154

155+
exprt to_predicate(const exprt &expr, const namespacet &ns) const;
156+
exprt to_predicate(const exprt::operandst &exprs, const namespacet &ns) const;
157+
155158
/// Computes the join between "this" and "b".
156159
///
157160
/// \param b: the other domain

‎unit/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,7 @@ SRC += analyses/ai/ai.cpp \
4545
analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp \
4646
analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp \
4747
analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp \
48+
analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp \
4849
analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp \
4950
ansi-c/expr2c.cpp \
5051
ansi-c/max_malloc_size.cpp \

‎unit/analyses/variable-sensitivity/variable_sensitivity_domain/module_dependencies.txt

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
analyses
2+
testing-utils
3+
util

‎unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp

+105
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
/*******************************************************************\
2+
3+
Module: Tests for variable_sensitivity_domaint::to_predicate
4+
5+
Author: Jez Higgins
6+
7+
\*******************************************************************/
8+
9+
#include <analyses/variable-sensitivity/variable_sensitivity_domain.h>
10+
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
11+
#include <analyses/variable-sensitivity/variable_sensitivity_test_helpers.h>
12+
#include <testing-utils/use_catch.h>
13+
#include <util/arith_tools.h>
14+
#include <util/bitvector_types.h>
15+
#include <util/mathematical_types.h>
16+
17+
SCENARIO(
18+
"variable_sensitivity_domain to predicate",
19+
"[core][analyses][variable-sensitivity][variable_sensitivity_domain][to_"
20+
"predicate]")
21+
{
22+
auto config = vsd_configt::constant_domain();
23+
config.context_tracking.data_dependency_context = false;
24+
config.context_tracking.last_write_context = false;
25+
auto object_factory =
26+
variable_sensitivity_object_factoryt::configured_with(config);
27+
symbol_tablet symbol_table;
28+
namespacet ns(symbol_table);
29+
30+
GIVEN("to_predicate()")
31+
{
32+
WHEN("it is TOP")
33+
{
34+
auto domain = variable_sensitivity_domaint(object_factory, config);
35+
domain.make_top();
36+
THEN_PREDICATE(domain, "TRUE");
37+
}
38+
WHEN("it is BOTTOM")
39+
{
40+
auto domain = variable_sensitivity_domaint(object_factory, config);
41+
domain.make_bottom();
42+
THEN_PREDICATE(domain, "FALSE");
43+
}
44+
}
45+
GIVEN("to_predicate(expr)")
46+
{
47+
WHEN("1 + 2")
48+
{
49+
auto type = signedbv_typet(32);
50+
auto val1 = from_integer(1, type);
51+
auto val2 = from_integer(2, type);
52+
53+
auto domain = variable_sensitivity_domaint(object_factory, config);
54+
domain.make_top();
55+
56+
auto pred = domain.to_predicate(plus_exprt(val1, val2), ns);
57+
THEN("predicate is 1 + 2 == 3")
58+
{
59+
auto repr = expr_to_str(pred);
60+
REQUIRE(repr == "1 + 2 == 3");
61+
}
62+
}
63+
}
64+
GIVEN("to_predicate(std::vector<expr>)")
65+
{
66+
auto domain = variable_sensitivity_domaint(object_factory, config);
67+
domain.make_top();
68+
69+
auto type = signedbv_typet(32);
70+
auto val1 = from_integer(1, type);
71+
auto val2 = from_integer(2, type);
72+
auto val3 = from_integer(3, type);
73+
auto onePlusTwo = plus_exprt(val1, val2);
74+
auto twoPlusThree = plus_exprt(val2, val3);
75+
76+
WHEN("{ }")
77+
{
78+
auto pred = domain.to_predicate(std::vector<exprt>(), ns);
79+
THEN("predicate is FALSE")
80+
{
81+
auto repr = expr_to_str(pred);
82+
REQUIRE(repr == "FALSE");
83+
}
84+
}
85+
WHEN("{ 1 + 2 }")
86+
{
87+
auto pred = domain.to_predicate({onePlusTwo}, ns);
88+
THEN("predicate is 1 + 2 == 3")
89+
{
90+
auto repr = expr_to_str(pred);
91+
REQUIRE(repr == "1 + 2 == 3");
92+
}
93+
}
94+
95+
WHEN("{ 1 + 2, 2 + 3 }")
96+
{
97+
auto pred = domain.to_predicate({onePlusTwo, twoPlusThree}, ns);
98+
THEN("predicate is 1 + 2 == 3 && 2 + 3 == 5")
99+
{
100+
auto repr = expr_to_str(pred);
101+
REQUIRE(repr == "1 + 2 == 3 && 2 + 3 == 5");
102+
}
103+
}
104+
}
105+
}

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

+14-2
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
#include <analyses/variable-sensitivity/constant_abstract_value.h>
1313
#include <analyses/variable-sensitivity/interval_abstract_value.h>
1414
#include <analyses/variable-sensitivity/value_set_abstract_object.h>
15+
#include <analyses/variable-sensitivity/variable_sensitivity_domain.h>
1516

1617
#include <ansi-c/ansi_c_language.h>
1718

@@ -539,12 +540,23 @@ void THEN_PREDICATE(const abstract_object_pointert &obj, const std::string &out)
539540
}
540541
}
541542

542-
void THEN_PREDICATE(const abstract_environmentt &env, const std::string &out)
543+
void THEN_PREDICATE(const exprt &pred, const std::string &out)
543544
{
544-
auto pred = env.to_predicate();
545545
THEN("predicate is " + out)
546546
{
547547
auto repr = expr_to_str(pred);
548548
REQUIRE(repr == out);
549549
}
550550
}
551+
552+
void THEN_PREDICATE(const abstract_environmentt &env, const std::string &out)
553+
{
554+
THEN_PREDICATE(env.to_predicate(), out);
555+
}
556+
557+
void THEN_PREDICATE(
558+
const variable_sensitivity_domaint &domain,
559+
const std::string &out)
560+
{
561+
THEN_PREDICATE(domain.to_predicate(), out);
562+
}

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

+4
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ class constant_abstract_valuet;
1818
class constant_interval_exprt;
1919
class interval_abstract_valuet;
2020
class value_set_abstract_objectt;
21+
class variable_sensitivity_domaint;
2122

2223
std::shared_ptr<const constant_abstract_valuet>
2324
make_constant(exprt val, abstract_environmentt &env, namespacet &ns);
@@ -256,5 +257,8 @@ void THEN_PREDICATE(
256257
const abstract_object_pointert &obj,
257258
const std::string &out);
258259
void THEN_PREDICATE(const abstract_environmentt &env, const std::string &out);
260+
void THEN_PREDICATE(
261+
const variable_sensitivity_domaint &domain,
262+
const std::string &out);
259263

260264
#endif

0 commit comments

Comments
 (0)