CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
abstract_value_object.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity
4
5 Author: Jez Higgins, jez@jezuk.co.uk
6
7\*******************************************************************/
8
9#include <util/arith_tools.h>
11#include <util/ieee_float.h>
12#include <util/simplify_expr.h>
13
15
21
22#include "context_abstract_object.h" // IWYU pragma: keep
23
24#include <algorithm>
25
27{
28public:
29 const exprt &current() const override
30 {
31 return nil;
32 }
33 bool advance_to_next() override
34 {
35 return false;
36 }
38 {
40 }
41
42private:
44};
45
58
63
65{
66 return value;
67}
68
70{
71 bool a = available;
72 available = false;
73 return a;
74}
75
77{
78 return std::make_unique<empty_index_ranget>();
79}
80
82{
83 return std::make_unique<indeterminate_index_ranget>();
84}
85
87{
88public:
93
94 const abstract_object_pointert &current() const override
95 {
96 return value;
97 }
98 bool advance_to_next() override
99 {
100 bool a = available;
101 available = false;
102 return a;
103 }
105 {
107 }
108
109private:
112};
113
116{
117 return std::make_unique<single_value_value_ranget>(value);
118}
119
121 const exprt &expr,
122 const std::vector<abstract_object_pointert> &operands,
123 const abstract_environmentt &environment,
124 const namespacet &ns);
126 const exprt &expr,
127 const std::vector<abstract_object_pointert> &operands,
128 const abstract_environmentt &environment,
129 const namespacet &ns);
131 const exprt &expr,
132 const std::vector<abstract_object_pointert> &operands,
133 const abstract_environmentt &environment,
134 const namespacet &ns);
135
136template <class representation_type>
137bool any_of_type(const std::vector<abstract_object_pointert> &operands)
138{
139 return std::find_if(
140 operands.begin(),
141 operands.end(),
142 [](const abstract_object_pointert &p) {
143 return (!p->is_top()) &&
144 (std::dynamic_pointer_cast<const representation_type>(p) !=
145 nullptr);
146 }) != operands.end();
147}
148
149bool any_value_sets(const std::vector<abstract_object_pointert> &operands)
150{
152}
153
154bool any_intervals(const std::vector<abstract_object_pointert> &operands)
155{
157}
158
160 const exprt &expr,
161 const std::vector<abstract_object_pointert> &operands,
162 const abstract_environmentt &environment,
163 const namespacet &ns)
164{
165 if(any_value_sets(operands))
166 return value_set_expression_transform(expr, operands, environment, ns);
167 if(any_intervals(operands))
168 return intervals_expression_transform(expr, operands, environment, ns);
169 return constants_expression_transform(expr, operands, environment, ns);
170}
171
173 const exprt &expr,
174 const std::vector<abstract_object_pointert> &operands,
175 const abstract_environmentt &environment,
176 const namespacet &ns) const
177{
178 return transform(expr, operands, environment, ns);
179}
180
182 abstract_environmentt &environment,
183 const namespacet &ns,
184 const std::stack<exprt> &stack,
185 const exprt &specifier,
186 const abstract_object_pointert &value,
187 bool merging_write) const
188{
189 UNREACHABLE; // Should not ever call write on a value;
190}
191
193 const abstract_object_pointert &other,
194 const widen_modet &widen_mode) const
195{
196 auto cast_other =
197 std::dynamic_pointer_cast<const abstract_value_objectt>(other);
198 if(cast_other)
200
201 return abstract_objectt::merge(other, widen_mode);
202}
203
206{
207 auto cast_other =
208 std::dynamic_pointer_cast<const abstract_value_objectt>(other);
209 if(cast_other)
211
212 return abstract_objectt::meet(other);
213}
214
215// evaluation helpers
216template <class representation_type>
218{
219 return std::make_shared<representation_type>(type, true, false);
220}
221
222// constant_abstract_value expression transfrom
224{
225public:
227 const exprt &e,
228 const std::vector<abstract_object_pointert> &ops,
230 const namespacet &n)
232 {
233 }
234
236 {
237 // try finding the rounding mode. If it's not constant, try
238 // seeing if we can get the same result with all rounding modes
241
242 return transform();
243 }
244
245private:
247 {
249
250 auto operand_is_top = false;
251 for(size_t i = 0; i != operands.size(); ++i)
252 {
253 auto lhs_value = operands[i]->to_constant();
254
255 // do not give up if a sub-expression is not a constant,
256 // because the whole expression may still be simplified in some cases
257 // (eg multiplication by zero)
258 if(lhs_value.is_not_nil())
259 expr.operands()[i] = lhs_value;
260 else
261 operand_is_top = true;
262 }
263
264 auto simplified = simplify_expr(expr, ns);
265
266 if(simplified.has_operands() && operand_is_top)
267 return top(simplified.type());
268
269 // the expression is fully simplified
270 return std::make_shared<constant_abstract_valuet>(
272 }
273
275 {
277
278 auto results_differ = [](
280 const abstract_object_pointert &cur) {
281 if(prev == nullptr)
282 return false;
283 return prev->to_constant() != cur->to_constant();
284 };
285
286 for(auto rounding_mode : all_rounding_modes)
287 {
288 auto child_env(environment_with_rounding_mode(rounding_mode));
289 auto child_operands =
291
292 auto result =
294
295 if(result->is_top() || results_differ(last_result, result))
296 return top(expression.type());
297 last_result = result;
298 }
299
300 return last_result;
301 }
302
305 {
307 child_env.assign(
309 child_env.abstract_object_factory(
310 signedbv_typet(32),
312 mp_integer(static_cast<unsigned long>(rm)), signedbv_typet(32)),
313 ns),
314 ns);
315 return child_env;
316 }
317
328
329 static std::vector<abstract_object_pointert> reeval_operands(
330 const exprt::operandst &ops,
332 const namespacet &ns)
333 {
334 auto reevaled_operands = std::vector<abstract_object_pointert>{};
335 std::transform(
336 ops.cbegin(),
337 ops.end(),
338 std::back_inserter(reevaled_operands),
339 [&env, &ns](const exprt &op) { return env.eval(op, ns); });
340 return reevaled_operands;
341 }
342
344 {
346 }
347
349 {
350 auto rounding_mode =
351 environment.eval(rounding_mode_symbol, ns)->to_constant();
352 return rounding_mode.is_nil();
353 }
354
356 mutable std::vector<abstract_object_pointert> operands;
359
361
362 using rounding_modes = std::vector<ieee_floatt::rounding_modet>;
364};
365
367 symbol_exprt(CPROVER_PREFIX "rounding_mode", signedbv_typet(32));
368
374
376 const exprt &expr,
377 const std::vector<abstract_object_pointert> &operands,
378 const abstract_environmentt &environment,
379 const namespacet &ns)
380{
381 auto evaluator = constants_evaluator(expr, operands, environment, ns);
382 return evaluator();
383}
384
386// intervals expression transform
388{
389public:
391 const exprt &e,
392 const std::vector<abstract_object_pointert> &ops,
394 const namespacet &n)
396 {
397 PRECONDITION(expression.operands().size() == operands.size());
398 }
399
401 {
402 return transform();
403 }
404
405private:
408
410 {
412 auto num_operands = interval_operands.size();
413
414 if(num_operands != operands.size())
415 {
416 // We could not convert all operands into intervals,
417 // e.g. if its type is not something we can represent as an interval,
418 // try dispatching the expression_transform under that type instead.
421 }
422
423 if(num_operands == 0)
425
426 if(expression.id() == ID_if)
428
429 if(num_operands == 1)
431
433
434 for(size_t opIndex = 1; opIndex != interval_operands.size(); ++opIndex)
435 {
437 result = result.eval(expression.id(), interval_next);
438 }
439
440 INVARIANT(
441 result.is_top() || result.type() == expression.type(),
442 "Type of result interval should match expression type");
443 return make_interval(result);
444 }
445
446 std::vector<constant_interval_exprt> operands_as_intervals() const
447 {
448 std::vector<constant_interval_exprt> interval_operands;
449
450 for(const auto &op : operands)
451 {
452 auto iav = std::dynamic_pointer_cast<const interval_abstract_valuet>(op);
453 if(!iav)
454 {
455 // The operand isn't an interval
456 // if it's an integral constant we can convert it into an interval.
457 if(constant_interval_exprt::is_int(op->type()))
458 {
459 const auto op_as_constant = op->to_constant();
460 if(op_as_constant.is_nil())
461 return std::vector<constant_interval_exprt>();
462
464 }
466 !std::dynamic_pointer_cast<const context_abstract_objectt>(iav));
467 }
468
469 if(iav)
470 interval_operands.push_back(iav->to_interval());
471 }
472
473 return interval_operands;
474 }
475
477 const std::vector<constant_interval_exprt> &interval_operands) const
478 {
479 auto const &condition_interval = interval_operands[0];
480 auto const &true_interval = interval_operands[1];
481 auto const &false_interval = interval_operands[2];
482
483 auto condition_result = condition_interval.is_definitely_true();
484
485 if(condition_result.is_unknown())
486 {
487 // Value of the condition is both true and false, so
488 // combine the intervals of both the true and false expressions
491 true_interval.get_lower(), false_interval.get_lower()),
493 true_interval.get_upper(), false_interval.get_upper())));
494 }
495
498 }
499
501 const std::vector<constant_interval_exprt> &interval_operands) const
502 {
504
505 if(expression.id() == ID_typecast)
506 {
508
510 operand_expr.typecast(tce.type());
511
512 INVARIANT(
513 new_interval.type() == expression.type(),
514 "Type of result interval should match expression type");
515
517 }
518
520 operand_expr.eval(expression.id());
521 INVARIANT(
522 interval_result.type() == expression.type(),
523 "Type of result interval should match expression type");
525 }
526
531
533 const std::vector<abstract_object_pointert> &operands;
536};
537
539 const exprt &expr,
540 const std::vector<abstract_object_pointert> &operands,
541 const abstract_environmentt &environment,
542 const namespacet &ns)
543{
544 auto evaluator = interval_evaluator(expr, operands, environment, ns);
545 return evaluator();
546}
547
549// value_set expression transform
551{
552public:
554 const exprt &e,
555 const std::vector<abstract_object_pointert> &ops,
557 const namespacet &n)
559 {
560 PRECONDITION(expression.operands().size() == operands.size());
561 }
562
564 {
565 return transform();
566 }
567
568private:
580
585 evaluate_each_combination(const std::vector<value_ranget> &value_ranges) const
586 {
588 std::vector<abstract_object_pointert> combination;
590 return results;
591 }
592
595 const std::vector<value_ranget> &value_ranges,
596 std::vector<abstract_object_pointert> &combination) const
597 {
598 size_t n = combination.size();
599 if(n == value_ranges.size())
600 {
603 results.insert(result);
604 }
605 else
606 {
607 for(const auto &value : value_ranges[n])
608 {
609 combination.push_back(value);
611 combination.pop_back();
612 }
613 }
614 }
615
616 exprt
617 rewrite_expression(const std::vector<abstract_object_pointert> &ops) const
618 {
620 for(size_t i = 0; i != expression.operands().size(); ++i)
621 {
622 const auto &v = ops[i];
623 if(is_constant_value(v))
624 operands_expr.push_back(v->to_constant());
625 else
626 operands_expr.push_back(expression.operands()[i]);
627 }
628 auto rewritten_expr =
629 exprt(expression.id(), expression.type(), std::move(operands_expr));
630 return rewritten_expr;
631 }
632
634 {
635 return std::dynamic_pointer_cast<const constant_abstract_valuet>(v) !=
636 nullptr;
637 }
638
639 std::vector<value_ranget> operands_as_ranges() const
640 {
641 auto unwrapped = std::vector<value_ranget>{};
642
643 for(const auto &op : operands)
644 {
645 auto av = std::dynamic_pointer_cast<const abstract_value_objectt>(
646 op->unwrap_context());
647 INVARIANT(av, "should be an abstract value object");
648 unwrapped.emplace_back(av->value_range());
649 }
650
651 return unwrapped;
652 }
653
655 evaluate_conditional(const std::vector<value_ranget> &ops)
656 {
657 auto const &condition = ops[0];
658
659 auto const &true_result = ops[1];
660 auto const &false_result = ops[2];
661
662 auto all_true = true;
663 auto all_false = true;
664 for(const auto &v : condition)
665 {
666 auto expr = v->to_constant();
667 all_true = all_true && expr.is_true();
668 all_false = all_false && expr.is_false();
669 }
670 auto indeterminate = !all_true && !all_false;
671
673 if(all_true || indeterminate)
675 if(all_false || indeterminate)
678 }
679
681 const std::vector<abstract_object_pointert> &operands;
684};
685
687 const exprt &expr,
688 const std::vector<abstract_object_pointert> &operands,
689 const abstract_environmentt &environment,
690 const namespacet &ns)
691{
692 auto evaluator = value_set_evaluator(expr, operands, environment, ns);
693 return evaluator();
694}
695
698{
699 return std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
700}
An abstract version of a program environment.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
bool any_value_sets(const std::vector< abstract_object_pointert > &operands)
static abstract_object_pointert intervals_expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
index_range_implementation_ptrt make_indeterminate_index_range()
static abstract_object_pointert constants_expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
abstract_object_pointert make_top(const typet &type)
static abstract_object_pointert value_set_expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
index_range_implementation_ptrt make_empty_index_range()
bool any_intervals(const std::vector< abstract_object_pointert > &operands)
value_range_implementation_ptrt make_single_value_range(const abstract_object_pointert &value)
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
bool any_of_type(const std::vector< abstract_object_pointert > &operands)
Common behaviour for abstract objects modelling values - constants, intervals, etc.
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Symbolic Execution.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Pre-defined bitvector types.
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
static combine_result meet(const abstract_object_pointert &op1, const abstract_object_pointert &op2)
Interface method for the meet operation.
sharing_ptrt< const abstract_value_objectt > as_value(const abstract_object_pointert &obj) const
abstract_object_pointert merge(const abstract_object_pointert &other, const widen_modet &widen_mode) const final
Attempts to do a value/value merge if both are constants, otherwise falls back to the parent merge.
virtual abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const =0
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const final
Interface for transforms.
abstract_object_pointert meet(const abstract_object_pointert &other) const final
Base implementation of the meet operation: only used if no more precise abstraction can be used,...
abstract_object_pointert write(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const final
A helper function to evaluate writing to a component of an abstract object.
virtual abstract_object_pointert merge_with_value(const abstract_value_pointert &other, const widen_modet &widen_mode) const =0
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Represents an interval of values.
Definition interval.h:52
static bool is_top(const constant_interval_exprt &a)
static exprt get_max(const exprt &a, const exprt &b)
Definition interval.cpp:960
static exprt get_min(const exprt &a, const exprt &b)
Definition interval.cpp:965
constant_interval_exprt eval(const irep_idt &unary_operator) const
Definition interval.cpp:793
abstract_object_pointert try_transform_expr_with_all_rounding_modes() const
abstract_object_pointert transform() const
static const rounding_modes all_rounding_modes
constants_evaluator(const exprt &e, const std::vector< abstract_object_pointert > &ops, const abstract_environmentt &env, const namespacet &n)
abstract_object_pointert operator()() const
exprt adjust_expression_for_rounding_mode() const
std::vector< abstract_object_pointert > operands
std::vector< ieee_floatt::rounding_modet > rounding_modes
static const symbol_exprt rounding_mode_symbol
abstract_environmentt environment_with_rounding_mode(ieee_floatt::rounding_modet rm) const
const abstract_environmentt & environment
abstract_object_pointert top(const typet &type) const
static std::vector< abstract_object_pointert > reeval_operands(const exprt::operandst &ops, const abstract_environmentt &env, const namespacet &ns)
const exprt & current() const override
bool advance_to_next() override
index_range_implementation_ptrt reset() const override
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
index_range_implementation_ptrt reset() const override
static std::shared_ptr< interval_abstract_valuet > make_interval(Args &&... args)
std::vector< constant_interval_exprt > operands_as_intervals() const
abstract_object_pointert operator()() const
const abstract_environmentt & environment
const std::vector< abstract_object_pointert > & operands
abstract_object_pointert evaluate_unary_expr(const std::vector< constant_interval_exprt > &interval_operands) const
abstract_object_pointert transform() const
abstract_object_pointert evaluate_conditional(const std::vector< constant_interval_exprt > &interval_operands) const
interval_evaluator(const exprt &e, const std::vector< abstract_object_pointert > &ops, const abstract_environmentt &env, const namespacet &n)
interval_abstract_value_pointert make_interval(const exprt &expr) const
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:3208
Fixed-width bit-vector with two's complement interpretation.
single_value_index_ranget(const exprt &val)
const exprt & current() const override
const abstract_object_pointert value
single_value_value_ranget(const abstract_object_pointert &val)
const abstract_object_pointert & current() const override
value_range_implementation_ptrt reset() const override
Expression to hold a symbol (variable)
Definition std_expr.h:131
Semantic type conversion.
Definition std_expr.h:2073
The type of an expression, extends irept.
Definition type.h:29
static abstract_object_pointert make_value_set(const abstract_object_sett &initial_values)
abstract_object_pointert transform() const
const std::vector< abstract_object_pointert > & operands
static abstract_object_pointert evaluate_conditional(const std::vector< value_ranget > &ops)
const abstract_environmentt & environment
std::vector< value_ranget > operands_as_ranges() const
value_set_evaluator(const exprt &e, const std::vector< abstract_object_pointert > &ops, const abstract_environmentt &env, const namespacet &n)
static bool is_constant_value(const abstract_object_pointert &v)
void evaluate_combination(abstract_object_sett &results, const std::vector< value_ranget > &value_ranges, std::vector< abstract_object_pointert > &combination) const
abstract_object_sett evaluate_each_combination(const std::vector< value_ranget > &value_ranges) const
Evaluate expression for every combination of values in value_ranges.
abstract_object_pointert operator()() const
exprt rewrite_expression(const std::vector< abstract_object_pointert > &ops) const
An abstraction of a single value that just stores a constant.
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
static exprt evaluator(const std::unordered_map< exprt, exprt, irep_hash > &memory, const decision_proceduret &solver, exprt src, const namespacet &ns)
#define CPROVER_PREFIX
An interval to represent a set of possible values.
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#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 typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
Value Set Abstract Object.