cprover
Loading...
Searching...
No Matches
simplify_expr_with_value_set.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Variant of simplify_exprt that uses a value_sett
4
5Author: Michael Tautschnig
6
7\*******************************************************************/
8
10
11#include <util/expr_util.h>
12#include <util/pointer_expr.h>
13#include <util/simplify_expr.h>
14#include <util/ssa_expr.h>
15
19
21
33static std::optional<exprt> try_evaluate_pointer_comparison(
34 const irep_idt &operation,
35 const symbol_exprt &symbol_expr,
36 const exprt &other_operand,
37 const value_sett &value_set,
38 const irep_idt language_mode,
39 const namespacet &ns)
40{
41 const constant_exprt *constant_expr =
43
44 if(
45 skip_typecast(other_operand).id() != ID_address_of &&
46 (!constant_expr || !constant_expr->is_null_pointer()))
47 {
48 return {};
49 }
50
51 const ssa_exprt *ssa_symbol_expr =
53
54 ssa_exprt l1_expr{*ssa_symbol_expr};
55 l1_expr.remove_level_2();
56 const std::vector<exprt> value_set_elements =
57 value_set.get_value_set(l1_expr, ns);
58
59 bool constant_found = false;
60
61 for(const auto &value_set_element : value_set_elements)
62 {
63 if(
64 value_set_element.id() == ID_unknown ||
65 value_set_element.id() == ID_invalid ||
67 to_object_descriptor_expr(value_set_element).root_object()) ||
68 to_object_descriptor_expr(value_set_element).offset().id() == ID_unknown)
69 {
70 // We can't conclude anything about the value-set
71 return {};
72 }
73
74 if(!constant_found)
75 {
77 value_set_element, false, language_mode))
78 {
79 continue;
80 }
81
84 value_set_element, symbol_expr, ns);
85
86 // use the simplifier to test equality as we need to skip over typecasts
87 // and cannot rely on canonical representations, which would permit a
88 // simple syntactic equality test
89 exprt test_equal = simplify_expr(
91 typecast_exprt::conditional_cast(value.pointer, other_operand.type()),
92 other_operand},
93 ns);
94 if(test_equal.is_true())
95 {
96 constant_found = true;
97 // We can't break because we have to make sure we find any instances of
98 // ID_unknown or ID_invalid
99 }
100 else if(!test_equal.is_false())
101 {
102 // We can't conclude anything about the value-set
103 return {};
104 }
105 }
106 }
107
108 if(!constant_found)
109 {
110 // The symbol cannot possibly have the value \p other_operand because it
111 // isn't in the symbol's value-set
112 return operation == ID_equal ? static_cast<exprt>(false_exprt{})
113 : static_cast<exprt>(true_exprt{});
114 }
115 else if(value_set_elements.size() == 1)
116 {
117 // The symbol must have the value \p other_operand because it is the only
118 // thing in the symbol's value-set
119 return operation == ID_equal ? static_cast<exprt>(true_exprt{})
120 : static_cast<exprt>(false_exprt{});
121 }
122 else
123 {
124 return {};
125 }
126}
127
129 const binary_relation_exprt &expr)
130{
131 if(expr.id() != ID_equal && expr.id() != ID_notequal)
133
134 if(!can_cast_type<pointer_typet>(to_binary_expr(expr).op0().type()))
136
137 exprt lhs = to_binary_expr(expr).op0(), rhs = to_binary_expr(expr).op1();
139 std::swap(lhs, rhs);
140
141 const symbol_exprt *symbol_expr_lhs =
143
144 if(!symbol_expr_lhs)
146
149
150 auto maybe_constant = try_evaluate_pointer_comparison(
151 expr.id(), *symbol_expr_lhs, rhs, value_set, language_mode, ns);
152 if(maybe_constant.has_value())
153 return changed(*maybe_constant);
154 else
155 return unchanged(expr);
156}
157
160 const binary_relation_exprt &expr)
161{
162 PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
163 PRECONDITION(expr.is_boolean());
164
165 auto collect_objects = [this](const exprt &pointer)
166 {
167 std::set<exprt> objects;
168 if(auto address_of = expr_try_dynamic_cast<address_of_exprt>(pointer))
169 {
170 objects.insert(
171 object_descriptor_exprt::root_object(address_of->object()));
172 }
173 else if(auto ssa_expr = expr_try_dynamic_cast<ssa_exprt>(pointer))
174 {
175 ssa_exprt l1_expr{*ssa_expr};
176 l1_expr.remove_level_2();
177 const std::vector<exprt> value_set_elements =
178 value_set.get_value_set(l1_expr, ns);
179
180 for(const auto &value_set_element : value_set_elements)
181 {
182 if(
183 value_set_element.id() == ID_unknown ||
184 value_set_element.id() == ID_invalid ||
186 to_object_descriptor_expr(value_set_element).root_object()))
187 {
188 objects.clear();
189 break;
190 }
191
192 objects.insert(
193 to_object_descriptor_expr(value_set_element).root_object());
194 }
195 }
196 return objects;
197 };
198
199 auto lhs_objects =
200 collect_objects(to_pointer_object_expr(expr.lhs()).pointer());
201 auto rhs_objects =
202 collect_objects(to_pointer_object_expr(expr.rhs()).pointer());
203
204 if(lhs_objects.size() == 1 && lhs_objects == rhs_objects)
205 {
206 // there is exactly one pointed-to object on both left-hand and right-hand
207 // side, and that object is the same
208 return expr.id() == ID_equal ? changed(static_cast<exprt>(true_exprt{}))
209 : changed(static_cast<exprt>(false_exprt{}));
210 }
211
212 std::list<exprt> intersection;
213 std::set_intersection(
214 lhs_objects.begin(),
215 lhs_objects.end(),
216 rhs_objects.begin(),
217 rhs_objects.end(),
218 std::back_inserter(intersection));
219 if(!lhs_objects.empty() && !rhs_objects.empty() && intersection.empty())
220 {
221 // all pointed-to objects on the left-hand side are different from any of
222 // the pointed-to objects on the right-hand side
223 return expr.id() == ID_equal ? changed(static_cast<exprt>(false_exprt{}))
224 : changed(static_cast<exprt>(true_exprt{}));
225 }
226
228}
229
232 const pointer_offset_exprt &expr)
233{
234 const exprt &ptr = expr.pointer();
235
236 if(ptr.type().id() != ID_pointer)
237 return unchanged(expr);
238
239 const ssa_exprt *ssa_symbol_expr = expr_try_dynamic_cast<ssa_exprt>(ptr);
240
241 if(!ssa_symbol_expr)
243
244 ssa_exprt l1_expr{*ssa_symbol_expr};
245 l1_expr.remove_level_2();
246 const std::vector<exprt> value_set_elements =
247 value_set.get_value_set(l1_expr, ns);
248
249 std::optional<exprt> offset;
250
251 for(const auto &value_set_element : value_set_elements)
252 {
253 if(
254 value_set_element.id() == ID_unknown ||
255 value_set_element.id() == ID_invalid ||
257 to_object_descriptor_expr(value_set_element).root_object()) ||
258 to_object_descriptor_expr(value_set_element).offset().id() == ID_unknown)
259 {
260 offset.reset();
261 break;
262 }
263
264 exprt this_offset = to_object_descriptor_expr(value_set_element).offset();
265 if(
266 this_offset.id() == ID_unknown ||
267 (offset.has_value() && this_offset != *offset))
268 {
269 offset.reset();
270 break;
271 }
272 else if(!offset.has_value())
273 {
274 offset = this_offset;
275 }
276 }
277
278 if(!offset.has_value())
280
281 return changed(
283}
Pointer Dereferencing.
bool is_failed_symbol(const exprt &expr)
Return true if, and only if, expr is the result of failed dereferencing.
exprt & lhs()
Definition std_expr.h:668
exprt & rhs()
Definition std_expr.h:678
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
A constant literal expression.
Definition std_expr.h:3122
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition std_expr.cpp:25
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
typet & type()
Return the type of the expression.
Definition expr.h:84
The Boolean constant false.
Definition std_expr.h:3204
const irep_idt & id() const
Definition irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
static const exprt & root_object(const exprt &expr)
The offset (in bytes) of a pointer relative to the object.
resultt simplify_pointer_offset(const pointer_offset_exprt &) override
resultt simplify_inequality(const binary_relation_exprt &) override
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_inequality_pointer_object(const binary_relation_exprt &) override
When all candidates in the value set have the same offset we can replace a pointer_offset expression ...
const namespacet & ns
static resultt changed(resultt<> result)
resultt simplify_rec(const exprt &)
virtual resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
virtual resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
static resultt unchanged(exprt expr)
virtual resultt simplify_pointer_offset(const pointer_offset_exprt &)
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
void remove_level_2()
Definition ssa_expr.cpp:199
Expression to hold a symbol (variable)
Definition std_expr.h:131
The Boolean constant true.
Definition std_expr.h:3195
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
Return value for build_reference_to; see that method for documentation.
static valuet build_reference_to(const exprt &what, const exprt &pointer, const namespacet &ns)
static bool should_ignore_value(const exprt &what, bool exclude_null_derefs, const irep_idt &language_mode)
Determine whether possible alias what should be ignored when replacing a pointer by its referees.
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition value_set.h:43
std::vector< exprt > get_value_set(exprt expr, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
GOTO Symex constant propagation.
void intersection(const typename graph_nodet< E >::edgest &a, const typename graph_nodet< E >::edgest &b, typename graph_nodet< E >::edgest &dest)
Compute intersection of two edge sets, in linear time.
Definition graph.h:115
API to expression classes for Pointers.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
exprt simplify_expr(exprt src, const namespacet &ns)
static std::optional< exprt > try_evaluate_pointer_comparison(const irep_idt &operation, const symbol_exprt &symbol_expr, const exprt &other_operand, const value_sett &value_set, const irep_idt language_mode, const namespacet &ns)
Try to evaluate a simple pointer comparison.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
Value Set.
Pointer Dereferencing.
dstringt irep_idt