cprover
Loading...
Searching...
No Matches
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/make_unique.h>
13#include <util/simplify_expr.h>
14
16
22
23#include "context_abstract_object.h" // IWYU pragma: keep
24
25#include <algorithm>
26
28{
29public:
30 const exprt &current() const override
31 {
32 return nil;
33 }
34 bool advance_to_next() override
35 {
36 return false;
37 }
39 {
41 }
42
43private:
45};
46
59
64
66{
67 return value;
68}
69
71{
72 bool a = available;
73 available = false;
74 return a;
75}
76
81
86
88{
89public:
94
95 const abstract_object_pointert &current() const override
96 {
97 return value;
98 }
99 bool advance_to_next() override
100 {
101 bool a = available;
102 available = false;
103 return a;
104 }
106 {
108 }
109
110private:
113};
114
120
122 const exprt &expr,
123 const std::vector<abstract_object_pointert> &operands,
124 const abstract_environmentt &environment,
125 const namespacet &ns);
127 const exprt &expr,
128 const std::vector<abstract_object_pointert> &operands,
129 const abstract_environmentt &environment,
130 const namespacet &ns);
132 const exprt &expr,
133 const std::vector<abstract_object_pointert> &operands,
134 const abstract_environmentt &environment,
135 const namespacet &ns);
136
137template <class representation_type>
138bool any_of_type(const std::vector<abstract_object_pointert> &operands)
139{
140 return std::find_if(
141 operands.begin(),
142 operands.end(),
143 [](const abstract_object_pointert &p) {
144 return (!p->is_top()) &&
145 (std::dynamic_pointer_cast<const representation_type>(p) !=
146 nullptr);
147 }) != operands.end();
148}
149
150bool any_value_sets(const std::vector<abstract_object_pointert> &operands)
151{
153}
154
155bool any_intervals(const std::vector<abstract_object_pointert> &operands)
156{
158}
159
161 const exprt &expr,
162 const std::vector<abstract_object_pointert> &operands,
163 const abstract_environmentt &environment,
164 const namespacet &ns)
165{
166 if(any_value_sets(operands))
167 return value_set_expression_transform(expr, operands, environment, ns);
168 if(any_intervals(operands))
169 return intervals_expression_transform(expr, operands, environment, ns);
170 return constants_expression_transform(expr, operands, environment, ns);
171}
172
174 const exprt &expr,
175 const std::vector<abstract_object_pointert> &operands,
176 const abstract_environmentt &environment,
177 const namespacet &ns) const
178{
179 return transform(expr, operands, environment, ns);
180}
181
183 abstract_environmentt &environment,
184 const namespacet &ns,
185 const std::stack<exprt> &stack,
186 const exprt &specifier,
187 const abstract_object_pointert &value,
188 bool merging_write) const
189{
190 UNREACHABLE; // Should not ever call write on a value;
191}
192
194 const abstract_object_pointert &other,
195 const widen_modet &widen_mode) const
196{
197 auto cast_other =
198 std::dynamic_pointer_cast<const abstract_value_objectt>(other);
199 if(cast_other)
201
202 return abstract_objectt::merge(other, widen_mode);
203}
204
207{
208 auto cast_other =
209 std::dynamic_pointer_cast<const abstract_value_objectt>(other);
210 if(cast_other)
212
213 return abstract_objectt::meet(other);
214}
215
216// evaluation helpers
217template <class representation_type>
219{
220 return std::make_shared<representation_type>(type, true, false);
221}
222
223// constant_abstract_value expression transfrom
225{
226public:
228 const exprt &e,
229 const std::vector<abstract_object_pointert> &ops,
231 const namespacet &n)
233 {
234 }
235
237 {
238 // try finding the rounding mode. If it's not constant, try
239 // seeing if we can get the same result with all rounding modes
242
243 return transform();
244 }
245
246private:
248 {
250
251 auto operand_is_top = false;
252 for(size_t i = 0; i != operands.size(); ++i)
253 {
254 auto lhs_value = operands[i]->to_constant();
255
256 // do not give up if a sub-expression is not a constant,
257 // because the whole expression may still be simplified in some cases
258 // (eg multiplication by zero)
259 if(lhs_value.is_not_nil())
260 expr.operands()[i] = lhs_value;
261 else
262 operand_is_top = true;
263 }
264
265 auto simplified = simplify_expr(expr, ns);
266
267 if(simplified.has_operands() && operand_is_top)
268 return top(simplified.type());
269
270 // the expression is fully simplified
271 return std::make_shared<constant_abstract_valuet>(
273 }
274
276 {
278
279 auto results_differ = [](
281 const abstract_object_pointert &cur) {
282 if(prev == nullptr)
283 return false;
284 return prev->to_constant() != cur->to_constant();
285 };
286
287 for(auto rounding_mode : all_rounding_modes)
288 {
289 auto child_env(environment_with_rounding_mode(rounding_mode));
290 auto child_operands =
292
293 auto result =
295
296 if(result->is_top() || results_differ(last_result, result))
297 return top(expression.type());
298 last_result = result;
299 }
300
301 return last_result;
302 }
303
306 {
308 child_env.assign(
310 child_env.abstract_object_factory(
311 signedbv_typet(32),
313 mp_integer(static_cast<unsigned long>(rm)), signedbv_typet(32)),
314 ns),
315 ns);
316 return child_env;
317 }
318
329
330 static std::vector<abstract_object_pointert> reeval_operands(
331 const exprt::operandst &ops,
333 const namespacet &ns)
334 {
335 auto reevaled_operands = std::vector<abstract_object_pointert>{};
336 std::transform(
337 ops.cbegin(),
338 ops.end(),
339 std::back_inserter(reevaled_operands),
340 [&env, &ns](const exprt &op) { return env.eval(op, ns); });
341 return reevaled_operands;
342 }
343
345 {
347 }
348
350 {
351 auto rounding_mode =
352 environment.eval(rounding_mode_symbol, ns)->to_constant();
353 return rounding_mode.is_nil();
354 }
355
357 mutable std::vector<abstract_object_pointert> operands;
360
362
363 using rounding_modes = std::vector<ieee_floatt::rounding_modet>;
365};
366
368 symbol_exprt(CPROVER_PREFIX "rounding_mode", signedbv_typet(32));
369
375
377 const exprt &expr,
378 const std::vector<abstract_object_pointert> &operands,
379 const abstract_environmentt &environment,
380 const namespacet &ns)
381{
382 auto evaluator = constants_evaluator(expr, operands, environment, ns);
383 return evaluator();
384}
385
387// intervals expression transform
389{
390public:
392 const exprt &e,
393 const std::vector<abstract_object_pointert> &ops,
395 const namespacet &n)
397 {
398 PRECONDITION(expression.operands().size() == operands.size());
399 }
400
402 {
403 return transform();
404 }
405
406private:
409
411 {
413 auto num_operands = interval_operands.size();
414
415 if(num_operands != operands.size())
416 {
417 // We could not convert all operands into intervals,
418 // e.g. if its type is not something we can represent as an interval,
419 // try dispatching the expression_transform under that type instead.
422 }
423
424 if(num_operands == 0)
426
427 if(expression.id() == ID_if)
429
430 if(num_operands == 1)
432
434
435 for(size_t opIndex = 1; opIndex != interval_operands.size(); ++opIndex)
436 {
438 result = result.eval(expression.id(), interval_next);
439 }
440
441 INVARIANT(
442 result.type() == expression.type(),
443 "Type of result interval should match expression type");
444 return make_interval(result);
445 }
446
447 std::vector<constant_interval_exprt> operands_as_intervals() const
448 {
449 std::vector<constant_interval_exprt> interval_operands;
450
451 for(const auto &op : operands)
452 {
453 auto iav = std::dynamic_pointer_cast<const interval_abstract_valuet>(op);
454 if(!iav)
455 {
456 // The operand isn't an interval
457 // if it's an integral constant we can convert it into an interval.
458 if(constant_interval_exprt::is_int(op->type()))
459 {
460 const auto op_as_constant = op->to_constant();
461 if(op_as_constant.is_nil())
462 return std::vector<constant_interval_exprt>();
463
465 }
467 !std::dynamic_pointer_cast<const context_abstract_objectt>(iav));
468 }
469
470 if(iav)
471 interval_operands.push_back(iav->to_interval());
472 }
473
474 return interval_operands;
475 }
476
478 const std::vector<constant_interval_exprt> &interval_operands) const
479 {
480 auto const &condition_interval = interval_operands[0];
481 auto const &true_interval = interval_operands[1];
482 auto const &false_interval = interval_operands[2];
483
484 auto condition_result = condition_interval.is_definitely_true();
485
486 if(condition_result.is_unknown())
487 {
488 // Value of the condition is both true and false, so
489 // combine the intervals of both the true and false expressions
492 true_interval.get_lower(), false_interval.get_lower()),
494 true_interval.get_upper(), false_interval.get_upper())));
495 }
496
499 }
500
502 const std::vector<constant_interval_exprt> &interval_operands) const
503 {
505
506 if(expression.id() == ID_typecast)
507 {
509
511 operand_expr.typecast(tce.type());
512
513 INVARIANT(
514 new_interval.type() == expression.type(),
515 "Type of result interval should match expression type");
516
518 }
519
521 operand_expr.eval(expression.id());
522 INVARIANT(
523 interval_result.type() == expression.type(),
524 "Type of result interval should match expression type");
526 }
527
532
534 const std::vector<abstract_object_pointert> &operands;
537};
538
540 const exprt &expr,
541 const std::vector<abstract_object_pointert> &operands,
542 const abstract_environmentt &environment,
543 const namespacet &ns)
544{
545 auto evaluator = interval_evaluator(expr, operands, environment, ns);
546 return evaluator();
547}
548
550// value_set expression transform
552{
553public:
555 const exprt &e,
556 const std::vector<abstract_object_pointert> &ops,
558 const namespacet &n)
560 {
561 PRECONDITION(expression.operands().size() == operands.size());
562 }
563
565 {
566 return transform();
567 }
568
569private:
581
586 evaluate_each_combination(const std::vector<value_ranget> &value_ranges) const
587 {
589 std::vector<abstract_object_pointert> combination;
591 return results;
592 }
593
596 const std::vector<value_ranget> &value_ranges,
597 std::vector<abstract_object_pointert> &combination) const
598 {
599 size_t n = combination.size();
600 if(n == value_ranges.size())
601 {
604 results.insert(result);
605 }
606 else
607 {
608 for(const auto &value : value_ranges[n])
609 {
610 combination.push_back(value);
612 combination.pop_back();
613 }
614 }
615 }
616
617 exprt
618 rewrite_expression(const std::vector<abstract_object_pointert> &ops) const
619 {
621 for(size_t i = 0; i != expression.operands().size(); ++i)
622 {
623 const auto &v = ops[i];
624 if(is_constant_value(v))
625 operands_expr.push_back(v->to_constant());
626 else
627 operands_expr.push_back(expression.operands()[i]);
628 }
629 auto rewritten_expr =
630 exprt(expression.id(), expression.type(), std::move(operands_expr));
631 return rewritten_expr;
632 }
633
635 {
636 return std::dynamic_pointer_cast<const constant_abstract_valuet>(v) !=
637 nullptr;
638 }
639
640 std::vector<value_ranget> operands_as_ranges() const
641 {
642 auto unwrapped = std::vector<value_ranget>{};
643
644 for(const auto &op : operands)
645 {
646 auto av = std::dynamic_pointer_cast<const abstract_value_objectt>(
647 op->unwrap_context());
648 INVARIANT(av, "should be an abstract value object");
649 unwrapped.emplace_back(av->value_range());
650 }
651
652 return unwrapped;
653 }
654
656 evaluate_conditional(const std::vector<value_ranget> &ops)
657 {
658 auto const &condition = ops[0];
659
660 auto const &true_result = ops[1];
661 auto const &false_result = ops[2];
662
663 auto all_true = true;
664 auto all_false = true;
665 for(const auto &v : condition)
666 {
667 auto expr = v->to_constant();
668 all_true = all_true && expr.is_true();
669 all_false = all_false && expr.is_false();
670 }
671 auto indeterminate = !all_true && !all_false;
672
674 if(all_true || indeterminate)
676 if(all_false || indeterminate)
679 }
680
682 const std::vector<abstract_object_pointert> &operands;
685};
686
688 const exprt &expr,
689 const std::vector<abstract_object_pointert> &operands,
690 const abstract_environmentt &environment,
691 const namespacet &ns)
692{
693 auto evaluator = value_set_evaluator(expr, operands, environment, ns);
694 return evaluator();
695}
696
699{
700 return std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
701}
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:563
Represents an interval of values.
Definition interval.h:52
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:3026
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:113
Semantic type conversion.
Definition std_expr.h:2017
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:18
#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:2051
Value Set Abstract Object.