cprover
Loading...
Searching...
No Matches
interval_abstract_value.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity intervals
4
5 Author: Diffblue Ltd.
6
7\*******************************************************************/
8
9#include <ostream>
10
11#include <util/arith_tools.h>
13#include <util/expr_util.h>
14#include <util/invariant.h>
15#include <util/make_unique.h>
16#include <util/simplify_expr.h>
17
21#include "widened_range.h"
22
24 const constant_interval_exprt &interval,
25 const namespacet &n);
26
28{
29public:
31 const constant_interval_exprt &interval_,
32 const namespacet &n)
33 : interval(interval_),
35 next(interval.get_lower()),
36 upper(interval.get_upper()),
37 ns(n)
38 {
39 }
40
41 const exprt &current() const override
42 {
43 return index;
44 }
45 bool advance_to_next() override
46 {
47 index = next;
50 .is_true();
51 }
52
54 {
56 }
57
58private:
59 static exprt next_element(const exprt &cur, const namespacet &ns)
60 {
61 return simplify_expr(plus_exprt(cur, from_integer(1, cur.type())), ns);
62 }
63
68 const namespacet &ns;
69};
70
72 const constant_interval_exprt &interval,
73 const namespacet &n)
74{
75 return util_make_unique<interval_index_ranget>(interval, n);
76}
77
78static inline bool
79bvint_value_is_max(const typet &type, const mp_integer &value)
80{
81 PRECONDITION(type.id() == ID_signedbv || type.id() == ID_unsignedbv);
82 if(type.id() == ID_signedbv)
83 {
84 return to_signedbv_type(type).largest() == value;
85 }
86 else
87 {
88 return to_unsignedbv_type(type).largest() == value;
89 }
90}
91
92static inline bool
93bvint_value_is_min(const typet &type, const mp_integer &value)
94{
95 PRECONDITION(type.id() == ID_signedbv || type.id() == ID_unsignedbv);
96 if(type.id() == ID_signedbv)
97 {
98 return to_signedbv_type(type).smallest() == value;
99 }
100 else
101 {
102 return to_unsignedbv_type(type).smallest() == value;
103 }
104}
105
106static inline constant_interval_exprt
108{
109 return constant_interval_exprt(min_exprt(value.type()), value);
110}
111
112static inline constant_interval_exprt
114{
115 return constant_interval_exprt(value, max_exprt(value.type()));
116}
117
118static inline mp_integer force_value_from_expr(const exprt &value)
119{
121 optionalt<mp_integer> maybe_integer_value = numeric_cast<mp_integer>(value);
122 INVARIANT(maybe_integer_value.has_value(), "Input has to have a value");
123 return maybe_integer_value.value();
124}
125
126static inline constant_interval_exprt
128{
129 mp_integer integer_value = force_value_from_expr(value);
130 if(!bvint_value_is_min(value.type(), integer_value))
132 min_exprt(value.type()), from_integer(integer_value - 1, value.type()));
133 else
135}
136
137static inline constant_interval_exprt
139{
140 mp_integer integer_value = force_value_from_expr(value);
141 if(!bvint_value_is_max(value.type(), integer_value))
143 from_integer(integer_value + 1, value.type()), max_exprt(value.type()));
144 else
146}
147
148static inline bool represents_interval(const exprt &expr)
149{
150 const exprt &e = skip_typecast(expr);
151 return (e.id() == ID_constant_interval || e.id() == ID_constant);
152}
153
155{
156 const exprt &e = skip_typecast(expr);
157
158 if(e.id() == ID_constant_interval)
159 {
161 }
162 else if(e.id() == ID_constant)
163 {
164 return constant_interval_exprt(e, e);
165 }
166 else
167 {
168 // not directly representable, so just return TOP
169 return constant_interval_exprt(e.type());
170 }
171}
172
173static inline irep_idt invert_relation(const irep_idt &relation)
174{
176 relation == ID_le || relation == ID_lt || relation == ID_ge ||
177 relation == ID_gt || relation == ID_equal);
178 if(relation == ID_le)
179 return ID_ge;
180 if(relation == ID_ge)
181 return ID_le;
182 if(relation == ID_lt)
183 return ID_gt;
184 if(relation == ID_gt)
185 return ID_lt;
186 return relation;
187}
188
195{
196 PRECONDITION(e.operands().size() == 2);
197 const auto &relation = e.id();
198 const auto &binary_e = to_binary_expr(e);
199 const auto &lhs = binary_e.lhs();
200 const auto &rhs = binary_e.rhs();
202 relation == ID_le || relation == ID_lt || relation == ID_ge ||
203 relation == ID_gt || relation == ID_equal);
204 PRECONDITION(lhs.id() == ID_constant || lhs.id() == ID_symbol);
205 PRECONDITION(rhs.id() == ID_constant || rhs.id() == ID_symbol);
206 PRECONDITION(lhs.id() != rhs.id());
207
208 const auto the_constant_part_of_the_relation =
209 (rhs.id() == ID_symbol ? lhs : rhs);
210 const auto maybe_inverted_relation =
211 (rhs.id() == ID_symbol ? invert_relation(relation) : relation);
212
213 if(maybe_inverted_relation == ID_le)
214 return interval_from_x_le_value(the_constant_part_of_the_relation);
215 if(maybe_inverted_relation == ID_lt)
216 return interval_from_x_lt_value(the_constant_part_of_the_relation);
217 if(maybe_inverted_relation == ID_ge)
218 return interval_from_x_ge_value(the_constant_part_of_the_relation);
219 if(maybe_inverted_relation == ID_gt)
220 return interval_from_x_gt_value(the_constant_part_of_the_relation);
221 INVARIANT(
222 maybe_inverted_relation == ID_equal, "We excluded other cases above");
224 the_constant_part_of_the_relation, the_constant_part_of_the_relation);
225}
226
228 : abstract_value_objectt(t), interval(t)
229{
230}
231
233 const typet &t,
234 bool tp,
235 bool bttm)
236 : abstract_value_objectt(t, tp, bttm), interval(t)
237{
238}
239
241{
242 if(e.is_top())
243 return true;
244
245 if(e.get_lower().is_false() && e.get_upper().is_true())
246 return true;
247 if(
248 e.type().id() == ID_c_bool && e.get_lower().is_zero() &&
249 e.get_upper().is_one())
250 return true;
251
252 return false;
253}
254
257 : abstract_value_objectt(e.type(), new_interval_is_top(e), e.is_bottom()),
258 interval(e)
259{
260}
261
263 const exprt &lower,
264 const exprt &upper)
266{
267}
268
270 const exprt &e,
271 const abstract_environmentt &environment,
272 const namespacet &ns)
276 : (e.operands().size() == 2 ? interval_from_relation(e)
277 : constant_interval_exprt(e.type())))
278{
279}
280
282{
283 // Attempt to reduce this interval to a constant expression
285 {
286 // Interval is the equivalent of a constant, so reduce it to a constant
288 }
290#if 0
291 if(!is_top() && !is_bottom())
292 {
293 return this->interval;
294 }
295 else
296 {
298 }
299#endif
300}
301
303{
305}
306
308{
309 return std::hash<std::string>{}(interval.pretty());
310}
311
313 const abstract_object_pointert &other) const
314{
315 auto cast_other =
316 std::dynamic_pointer_cast<const interval_abstract_valuet>(other);
317 return cast_other && interval == cast_other->interval;
318}
319
321 std::ostream &out,
322 const ai_baset &ai,
323 const namespacet &ns) const
324{
325 if(!is_top() && !is_bottom())
326 {
327 std::string lower_string;
328 std::string upper_string;
329
330 if(interval.get_lower().id() == ID_min)
331 {
332 lower_string = "-INF";
333 }
334 else
335 {
336 INVARIANT(
337 interval.get_lower().id() == ID_constant,
338 "We only support constant limits");
339 lower_string =
341 }
342
343 if(interval.get_upper().id() == ID_max)
344 {
345 upper_string = "+INF";
346 }
347 else
348 {
349 INVARIANT(
350 interval.get_upper().id() == ID_constant,
351 "We only support constant limits");
352 upper_string =
354 }
355
356 out << "[" << lower_string << ", " << upper_string << "]";
357 }
358 else
359 {
360 abstract_objectt::output(out, ai, ns);
361 }
362}
363
365 const constant_interval_exprt &lhs,
366 const constant_interval_exprt &rhs)
367{
368 auto widened = widened_ranget(lhs, rhs);
369
370 // new interval ...
371 auto new_interval = constant_interval_exprt(
372 widened.widened_lower_bound, widened.widened_upper_bound);
373 return interval_abstract_valuet::make_interval(new_interval);
374}
375
377 const abstract_value_pointert &other,
378 const widen_modet &widen_mode) const
379{
380 if(other->is_bottom())
381 return shared_from_this();
382
383 auto other_interval = other->to_interval();
384
385 if(is_bottom())
386 return make_interval(other_interval);
387
388 if(interval.contains(other_interval))
389 return shared_from_this();
390
391 if(widen_mode == widen_modet::could_widen)
392 return widening_merge(interval, other_interval);
393
394 auto lower_bound = constant_interval_exprt::get_min(
395 interval.get_lower(), other_interval.get_lower());
396 auto upper_bound = constant_interval_exprt::get_max(
397 interval.get_upper(), other_interval.get_upper());
398
399 return make_interval(lower_bound, upper_bound);
400}
401
403 const abstract_value_pointert &other) const
404{
405 auto other_interval = other->to_interval();
406
407 if(other_interval.contains(interval))
408 return shared_from_this();
409
410 if(interval.contains(other_interval))
411 return make_interval(other_interval);
412
413 auto lower_bound = constant_interval_exprt::get_max(
414 interval.get_lower(), other_interval.get_lower());
415 auto upper_bound = constant_interval_exprt::get_min(
416 interval.get_upper(), other_interval.get_upper());
417
418 // if the interval is valid, we have a meet!
419 if(constant_interval_exprt::less_than_or_equal(lower_bound, upper_bound))
420 return make_interval(constant_interval_exprt(lower_bound, upper_bound));
421
422 return make_interval(interval.type(), false, true);
423}
424
427{
428 if(is_top() || is_bottom() || interval.is_top() || interval.is_bottom())
429 return make_empty_index_range();
430 if(interval.get_lower().id() == ID_min || interval.get_upper().id() == ID_max)
431 return make_empty_index_range();
432
434}
435
438{
439 return make_single_value_range(shared_from_this());
440}
441
443 const exprt &lower,
444 const exprt &upper) const
445{
446 auto lower_bound =
448 auto upper_bound =
450
451 if(constant_interval_exprt::greater_than(lower_bound, upper_bound))
452 return as_value(mutable_clone());
453
454 auto constrained_interval = constant_interval_exprt(lower_bound, upper_bound);
455 return as_value(
456 make_interval(constant_interval_exprt(lower_bound, upper_bound)));
457}
458
460{
462 return equal_exprt(name, interval.get_lower());
463
464 auto lower_bound = binary_relation_exprt(interval.get_lower(), ID_le, name);
465 auto upper_bound = binary_relation_exprt(name, ID_le, interval.get_upper());
466
467 return and_exprt(lower_bound, upper_bound);
468}
469
471 abstract_object_statisticst &statistics,
473 const abstract_environmentt &env,
474 const namespacet &ns) const
475{
476 abstract_objectt::get_statistics(statistics, visited, env, ns);
479 {
481 }
482 statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
483}
An abstract version of a program environment.
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Statistics gathering for the variable senstivity domain.
index_range_implementation_ptrt make_empty_index_range()
value_range_implementation_ptrt make_single_value_range(const abstract_object_pointert &value)
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Pre-defined bitvector types.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
virtual exprt to_constant() const
Converts to a constant expression if possible.
virtual bool is_top() const
Find out if the abstract object is top.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual internal_abstract_object_pointert mutable_clone() const
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
sharing_ptrt< const abstract_value_objectt > as_value(const abstract_object_pointert &obj) const
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
Boolean AND.
Definition: std_expr.h:1974
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
const irep_idt & get_value() const
Definition: std_expr.h:2815
Represents an interval of values.
Definition: interval.h:48
static bool is_bottom(const constant_interval_exprt &a)
Definition: interval.cpp:1814
constant_interval_exprt bottom() const
Definition: interval.cpp:1057
tvt greater_than(const constant_interval_exprt &o) const
Definition: interval.cpp:398
tvt less_than_or_equal(const constant_interval_exprt &o) const
Definition: interval.cpp:404
static bool is_top(const constant_interval_exprt &a)
Definition: interval.cpp:1809
bool is_single_value_interval() const
Definition: interval.cpp:1864
bool contains(const constant_interval_exprt &interval) const
Definition: interval.cpp:1426
static exprt get_max(const exprt &a, const exprt &b)
Definition: interval.cpp:959
static exprt get_min(const exprt &a, const exprt &b)
Definition: interval.cpp:964
const exprt & get_lower() const
Definition: interval.cpp:29
const exprt & get_upper() const
Definition: interval.cpp:34
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:114
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
mp_integer largest() const
Return the largest value that can be represented using this type.
mp_integer smallest() const
Return the smallest value that can be represented using this type.
CLONE abstract_object_pointert merge_with_value(const abstract_value_pointert &other, const widen_modet &widen_mode) const override
Merge another interval abstract object with this one.
static std::shared_ptr< interval_abstract_valuet > make_interval(Args &&... args)
bool internal_equality(const abstract_object_pointert &other) const override
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
exprt to_constant() const override
Converts to a constant expression if possible.
abstract_value_pointert constrain(const exprt &lower, const exprt &upper) const override
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const override
Meet another interval abstract object with this one.
value_range_implementation_ptrt value_range_implementation() const override
size_t internal_hash() const override
constant_interval_exprt interval
const exprt & current() const override
index_range_implementation_ptrt reset() const override
static exprt next_element(const exprt &cur, const namespacet &ns)
interval_index_ranget(const constant_interval_exprt &interval_, const namespacet &n)
const constant_interval_exprt & interval
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irep_idt & id() const
Definition: irep.h:396
+∞ upper bound for intervals
Definition: interval.h:18
static memory_sizet from_bytes(std::size_t bytes)
-∞ upper bound for intervals
Definition: interval.h:31
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2874
The plus expression Associativity is not specified.
Definition: std_expr.h:914
The type of an expression, extends irept.
Definition: type.h:29
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:216
Deprecated expression utility functions.
const constant_interval_exprt & to_constant_interval_expr(const exprt &expr)
Definition: interval.h:458
bool new_interval_is_top(const constant_interval_exprt &e)
static constant_interval_exprt interval_from_relation(const exprt &e)
Builds an interval representing all values satisfying the input expression.
static bool represents_interval(const exprt &expr)
static bool bvint_value_is_min(const typet &type, const mp_integer &value)
static mp_integer force_value_from_expr(const exprt &value)
abstract_object_pointert widening_merge(const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
static index_range_implementation_ptrt make_interval_index_range(const constant_interval_exprt &interval, const namespacet &n)
static constant_interval_exprt interval_from_x_gt_value(const exprt &value)
static constant_interval_exprt make_interval_expr(const exprt &expr)
static bool bvint_value_is_max(const typet &type, const mp_integer &value)
static irep_idt invert_relation(const irep_idt &relation)
static constant_interval_exprt interval_from_x_ge_value(const exprt &value)
static constant_interval_exprt interval_from_x_lt_value(const exprt &value)
static constant_interval_exprt interval_from_x_le_value(const exprt &value)
An interval to represent a set of possible values.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
nonstd::optional< T > optionalt
Definition: optional.h:35
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:12
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.