cprover
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 
15 
17 
18 #include <util/arith_tools.h>
19 #include <util/bitvector_types.h>
20 #include <util/ieee_float.h>
21 #include <util/make_unique.h>
22 #include <util/simplify_expr.h>
23 
25 {
26 public:
27  const exprt &current() const override
28  {
29  return nil;
30  }
31  bool advance_to_next() override
32  {
33  return false;
34  }
36  {
37  return make_empty_index_range();
38  }
39 
40 private:
42 };
43 
45 {
46 public:
48  {
49  }
50 
52  {
54  }
55 };
56 
58  : value(val), available(true)
59 {
60 }
61 
63 {
64  return value;
65 }
66 
68 {
69  bool a = available;
70  available = false;
71  return a;
72 }
73 
75 {
76  return util_make_unique<empty_index_ranget>();
77 }
78 
80 {
81  return util_make_unique<indeterminate_index_ranget>();
82 }
83 
85 {
86 public:
88  : value(val), available(true)
89  {
90  }
91 
92  const abstract_object_pointert &current() const override
93  {
94  return value;
95  }
96  bool advance_to_next() override
97  {
98  bool a = available;
99  available = false;
100  return a;
101  }
103  {
105  }
106 
107 private:
109  bool available;
110 };
111 
114 {
115  return util_make_unique<single_value_value_ranget>(value);
116 }
117 
119  const exprt &expr,
120  const std::vector<abstract_object_pointert> &operands,
121  const abstract_environmentt &environment,
122  const namespacet &ns);
124  const exprt &expr,
125  const std::vector<abstract_object_pointert> &operands,
126  const abstract_environmentt &environment,
127  const namespacet &ns);
129  const exprt &expr,
130  const std::vector<abstract_object_pointert> &operands,
131  const abstract_environmentt &environment,
132  const namespacet &ns);
133 
134 template <class representation_type>
135 bool any_of_type(const std::vector<abstract_object_pointert> &operands)
136 {
137  return std::find_if(
138  operands.begin(),
139  operands.end(),
140  [](const abstract_object_pointert &p) {
141  return (!p->is_top()) &&
142  (std::dynamic_pointer_cast<const representation_type>(p) !=
143  nullptr);
144  }) != operands.end();
145 }
146 
147 bool any_value_sets(const std::vector<abstract_object_pointert> &operands)
148 {
149  return any_of_type<value_set_abstract_objectt>(operands);
150 }
151 
152 bool any_intervals(const std::vector<abstract_object_pointert> &operands)
153 {
154  return any_of_type<interval_abstract_valuet>(operands);
155 }
156 
158  const exprt &expr,
159  const std::vector<abstract_object_pointert> &operands,
160  const abstract_environmentt &environment,
161  const namespacet &ns)
162 {
163  if(any_value_sets(operands))
164  return value_set_expression_transform(expr, operands, environment, ns);
165  if(any_intervals(operands))
166  return intervals_expression_transform(expr, operands, environment, ns);
167  return constants_expression_transform(expr, operands, environment, ns);
168 }
169 
171  const exprt &expr,
172  const std::vector<abstract_object_pointert> &operands,
173  const abstract_environmentt &environment,
174  const namespacet &ns) const
175 {
176  auto result = transform(expr, operands, environment, ns);
177  return environment.add_object_context(result);
178 }
179 
180 // evaluation helpers
181 template <class representation_type>
183 {
184  return std::make_shared<representation_type>(type, true, false);
185 }
186 
187 // constant_abstract_value expression transfrom
189 {
190 public:
192  const exprt &e,
193  const abstract_environmentt &env,
194  const namespacet &n)
195  : expression(e), environment(env), ns(n)
196  {
197  }
198 
200  {
201  // try finding the rounding mode. If it's not constant, try
202  // seeing if we can get the same result with all rounding modes
205 
206  return transform();
207  }
208 
209 private:
211  {
213  auto operands = expr.operands();
214  expr.operands().clear();
215 
216  // Two passes over the expression - one for simplification,
217  // another to check if there are any top subexpressions left
218  for(const exprt &op : operands)
219  {
220  auto lhs_value = eval_constant(op);
221 
222  // do not give up if a sub-expression is not a constant,
223  // because the whole expression may still be simplified in some cases
224  expr.operands().push_back(lhs_value.is_nil() ? op : lhs_value);
225  }
226 
227  exprt simplified = simplify_expr(expr, ns);
228  for(const exprt &op : simplified.operands())
229  {
230  auto lhs_value = eval_constant(op);
231  if(lhs_value.is_nil())
232  return top(simplified.type());
233  }
234 
235  // the expression is fully simplified
236  return std::make_shared<constant_abstract_valuet>(
237  simplified, environment, ns);
238  }
239 
241  {
242  std::vector<abstract_object_pointert> possible_results;
243  for(auto rounding_mode : all_rounding_modes)
244  {
245  auto child_env(environment_with_rounding_mode(rounding_mode));
246  possible_results.push_back(
247  constants_evaluator(expression, child_env, ns)());
248  }
249 
250  auto first = possible_results.front()->to_constant();
251  for(auto const &possible_result : possible_results)
252  {
253  auto current = possible_result->to_constant();
254  if(current.is_nil() || current != first)
255  return top(expression.type());
256  }
257  return possible_results.front();
258  }
259 
262  {
264  child_env.assign(
266  child_env.abstract_object_factory(
267  signedbv_typet(32),
268  from_integer(
269  mp_integer(static_cast<unsigned long>(rm)), signedbv_typet(32)),
270  ns),
271  ns);
272  return child_env;
273  }
274 
276  {
277  exprt adjusted_expr = expression;
278  adjust_float_expressions(adjusted_expr, ns);
279  return adjusted_expr;
280  }
281 
282  exprt eval_constant(const exprt &op) const
283  {
284  return environment.eval(op, ns)->to_constant();
285  }
286 
287  abstract_object_pointert top(const typet &type) const
288  {
289  return make_top<constant_abstract_valuet>(type);
290  }
291 
293  {
294  auto rounding_mode = eval_constant(rounding_mode_symbol);
295  return rounding_mode.is_nil();
296  }
297 
300  const namespacet &ns;
301 
303 
304  using rounding_modes = std::vector<ieee_floatt::rounding_modet>;
306 };
307 
309  symbol_exprt(CPROVER_PREFIX "rounding_mode", signedbv_typet(32));
310 
316 
318  const exprt &expr,
319  const std::vector<abstract_object_pointert> &operands,
320  const abstract_environmentt &environment,
321  const namespacet &ns)
322 {
323  auto evaluator = constants_evaluator(expr, environment, ns);
324  return evaluator();
325 }
326 
328 // intervals expression transform
330 {
331 public:
333  const exprt &e,
334  const std::vector<abstract_object_pointert> &ops,
335  const abstract_environmentt &env,
336  const namespacet &n)
337  : expression(e), operands(ops), environment(env), ns(n)
338  {
339  PRECONDITION(expression.operands().size() == operands.size());
340  }
341 
343  {
344  return transform();
345  }
346 
347 private:
350 
352  {
353  auto interval_operands = operands_as_intervals();
354  auto num_operands = interval_operands.size();
355 
356  if(num_operands != operands.size())
357  {
358  // We could not convert all operands into intervals,
359  // e.g. if its type is not something we can represent as an interval,
360  // try dispatching the expression_transform under that type instead.
363  }
364 
365  if(num_operands == 0)
366  return make_top<interval_abstract_valuet>(expression.type());
367 
368  if(expression.id() == ID_if)
369  return evaluate_conditional(interval_operands);
370 
371  if(num_operands == 1)
372  return evaluate_unary_expr(interval_operands);
373 
374  constant_interval_exprt result = interval_operands[0];
375 
376  for(size_t opIndex = 1; opIndex != interval_operands.size(); ++opIndex)
377  {
378  auto &interval_next = interval_operands[opIndex];
379  result = result.eval(expression.id(), interval_next);
380  }
381 
382  INVARIANT(
383  result.type() == expression.type(),
384  "Type of result interval should match expression type");
385  return make_interval(result);
386  }
387 
388  std::vector<constant_interval_exprt> operands_as_intervals() const
389  {
390  std::vector<constant_interval_exprt> interval_operands;
391 
392  for(const auto &op : operands)
393  {
394  auto iav = std::dynamic_pointer_cast<const interval_abstract_valuet>(op);
395  if(!iav)
396  {
397  // The operand isn't an interval
398  // if it's an integral constant we can convert it into an interval.
399  if(constant_interval_exprt::is_int(op->type()))
400  {
401  const auto op_as_constant = op->to_constant();
402  if(op_as_constant.is_nil())
403  return std::vector<constant_interval_exprt>();
404 
405  iav = make_interval(op_as_constant);
406  }
407  CHECK_RETURN(
408  !std::dynamic_pointer_cast<const context_abstract_objectt>(iav));
409  }
410 
411  if(iav)
412  interval_operands.push_back(iav->to_interval());
413  }
414 
415  return interval_operands;
416  }
417 
419  const std::vector<constant_interval_exprt> &interval_operands) const
420  {
421  auto const &condition_interval = interval_operands[0];
422  auto const &true_interval = interval_operands[1];
423  auto const &false_interval = interval_operands[2];
424 
425  auto condition_result = condition_interval.is_definitely_true();
426 
427  if(condition_result.is_unknown())
428  {
429  // Value of the condition is both true and false, so
430  // combine the intervals of both the true and false expressions
433  true_interval.get_lower(), false_interval.get_lower()),
435  true_interval.get_upper(), false_interval.get_upper())));
436  }
437 
438  return condition_result.is_true() ? make_interval(true_interval)
439  : make_interval(false_interval);
440  }
441 
443  const std::vector<constant_interval_exprt> &interval_operands) const
444  {
445  const constant_interval_exprt &operand_expr = interval_operands[0];
446 
447  if(expression.id() == ID_typecast)
448  {
450 
451  const constant_interval_exprt &new_interval =
452  operand_expr.typecast(tce.type());
453 
454  INVARIANT(
455  new_interval.type() == expression.type(),
456  "Type of result interval should match expression type");
457 
458  return make_interval(new_interval);
459  }
460 
461  const constant_interval_exprt &interval_result =
462  operand_expr.eval(expression.id());
463  INVARIANT(
464  interval_result.type() == expression.type(),
465  "Type of result interval should match expression type");
466  return make_interval(interval_result);
467  }
468 
470  {
471  return std::make_shared<interval_abstract_valuet>(expr, environment, ns);
472  }
473 
475  const std::vector<abstract_object_pointert> &operands;
477  const namespacet &ns;
478 };
479 
481  const exprt &expr,
482  const std::vector<abstract_object_pointert> &operands,
483  const abstract_environmentt &environment,
484  const namespacet &ns)
485 {
486  auto evaluator = interval_evaluator(expr, operands, environment, ns);
487  return evaluator();
488 }
489 
491 // value_set expression transform
493 {
494 public:
496  const exprt &e,
497  const std::vector<abstract_object_pointert> &ops,
498  const abstract_environmentt &env,
499  const namespacet &n)
500  : expression(e), operands(ops), environment(env), ns(n)
501  {
502  PRECONDITION(expression.operands().size() == operands.size());
503  }
504 
506  {
507  return transform();
508  }
509 
510 private:
512  {
513  auto ranges = operands_as_ranges();
514 
515  if(expression.id() == ID_if)
516  return evaluate_conditional(ranges);
517 
518  auto resulting_objects = evaluate_each_combination(ranges);
519 
520  return resolve_values(resulting_objects);
521  }
522 
527  evaluate_each_combination(const std::vector<value_ranget> &value_ranges) const
528  {
529  abstract_object_sett results;
530  std::vector<abstract_object_pointert> combination;
531  evaluate_combination(results, value_ranges, combination);
532  return results;
533  }
534 
536  abstract_object_sett &results,
537  const std::vector<value_ranget> &value_ranges,
538  std::vector<abstract_object_pointert> &combination) const
539  {
540  size_t n = combination.size();
541  if(n == value_ranges.size())
542  {
543  auto rewritten_expr = rewrite_expression(combination);
544  auto result = ::transform(rewritten_expr, combination, environment, ns);
545  results.insert(result);
546  }
547  else
548  {
549  for(const auto &value : value_ranges[n])
550  {
551  combination.push_back(value);
552  evaluate_combination(results, value_ranges, combination);
553  combination.pop_back();
554  }
555  }
556  }
557 
558  exprt
559  rewrite_expression(const std::vector<abstract_object_pointert> &ops) const
560  {
561  auto operands_expr = exprt::operandst{};
562  for(size_t i = 0; i != expression.operands().size(); ++i)
563  {
564  const auto &v = ops[i];
565  if(is_constant_value(v))
566  operands_expr.push_back(v->to_constant());
567  else
568  operands_expr.push_back(expression.operands()[i]);
569  }
570  auto rewritten_expr =
571  exprt(expression.id(), expression.type(), std::move(operands_expr));
572  return rewritten_expr;
573  }
574 
576  {
577  return std::dynamic_pointer_cast<const constant_abstract_valuet>(v) !=
578  nullptr;
579  }
580 
581  std::vector<value_ranget> operands_as_ranges() const
582  {
583  auto unwrapped = std::vector<value_ranget>{};
584 
585  for(const auto &op : operands)
586  {
587  auto av = std::dynamic_pointer_cast<const abstract_value_objectt>(
588  op->unwrap_context());
589  INVARIANT(av, "should be an abstract value object");
590  unwrapped.emplace_back(av->value_range());
591  }
592 
593  return unwrapped;
594  }
595 
596  static abstract_object_sett
598  {
599  abstract_object_sett unwrapped_values;
600  for(auto const &value : values)
601  {
602  unwrapped_values.insert(
603  maybe_extract_single_value(value->unwrap_context()));
604  }
605 
606  return unwrapped_values;
607  }
608 
611  {
612  auto const &value_as_set =
613  std::dynamic_pointer_cast<const value_set_tag>(maybe_singleton);
614  if(value_as_set)
615  {
616  PRECONDITION(value_as_set->get_values().size() == 1);
617  PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
618  value_as_set->get_values().first()));
619 
620  return value_as_set->get_values().first();
621  }
622  else
623  return maybe_singleton;
624  }
625 
628  {
629  PRECONDITION(!new_values.empty());
630 
631  auto unwrapped_values = unwrap_and_extract_values(new_values);
632 
633  if(unwrapped_values.size() > value_set_abstract_objectt::max_value_set_size)
634  return make_interval(unwrapped_values);
635 
636  return make_value_set(unwrapped_values);
637  }
638 
641  {
642  return std::make_shared<interval_abstract_valuet>(values.to_interval());
643  }
644 
647  {
648  const auto &type = values.first()->type();
649  auto value_set = std::make_shared<value_set_abstract_objectt>(type);
650  value_set->set_values(values);
651  return value_set;
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 
672  abstract_object_sett resulting_objects;
673  if(all_true || indeterminate)
674  resulting_objects.insert(true_result);
675  if(all_false || indeterminate)
676  resulting_objects.insert(false_result);
677  return resolve_values(resulting_objects);
678  }
679 
681  const std::vector<abstract_object_pointert> &operands;
683  const namespacet &ns;
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 }
value_set_evaluator::evaluate_combination
void evaluate_combination(abstract_object_sett &results, const std::vector< value_ranget > &value_ranges, std::vector< abstract_object_pointert > &combination) const
Definition: abstract_value_object.cpp:535
single_value_index_ranget
Definition: abstract_value_object.h:109
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
index_range_implementationt
Definition: abstract_value_object.h:28
arith_tools.h
interval_evaluator::evaluate_conditional
abstract_object_pointert evaluate_conditional(const std::vector< constant_interval_exprt > &interval_operands) const
Definition: abstract_value_object.cpp:418
constants_evaluator::eval_constant
exprt eval_constant(const exprt &op) const
Definition: abstract_value_object.cpp:282
interval_evaluator::interval_evaluator
interval_evaluator(const exprt &e, const std::vector< abstract_object_pointert > &ops, const abstract_environmentt &env, const namespacet &n)
Definition: abstract_value_object.cpp:332
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:28
transform
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
Definition: abstract_value_object.cpp:157
context_abstract_object.h
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
value_set_evaluator::environment
const abstract_environmentt & environment
Definition: abstract_value_object.cpp:682
constant_interval_exprt::get_max
static exprt get_max(const exprt &a, const exprt &b)
Definition: interval.cpp:959
value_set_evaluator::make_value_set
static abstract_object_pointert make_value_set(const abstract_object_sett &values)
Definition: abstract_value_object.cpp:646
value_set_evaluator::unwrap_and_extract_values
static abstract_object_sett unwrap_and_extract_values(const abstract_object_sett &values)
Definition: abstract_value_object.cpp:597
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
abstract_object_sett
Definition: abstract_object_set.h:19
indeterminate_index_ranget::indeterminate_index_ranget
indeterminate_index_ranget()
Definition: abstract_value_object.cpp:47
single_value_index_ranget::current
const exprt & current() const override
Definition: abstract_value_object.cpp:62
abstract_object_sett::empty
bool empty() const
Definition: abstract_object_set.h:65
abstract_environmentt::assign
virtual bool assign(const exprt &expr, const abstract_object_pointert &value, const namespacet &ns)
Assign a value to an expression.
Definition: abstract_environment.cpp:93
constants_evaluator::environment_with_rounding_mode
abstract_environmentt environment_with_rounding_mode(ieee_floatt::rounding_modet rm) const
Definition: abstract_value_object.cpp:261
any_intervals
bool any_intervals(const std::vector< abstract_object_pointert > &operands)
Definition: abstract_value_object.cpp:152
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
sharing_ptrt
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
Definition: abstract_object.h:73
single_value_index_ranget::value
const exprt value
Definition: abstract_value_object.h:118
constants_evaluator::top
abstract_object_pointert top(const typet &type) const
Definition: abstract_value_object.cpp:287
single_value_value_ranget::value
const abstract_object_pointert value
Definition: abstract_value_object.cpp:108
constants_evaluator::expression
const exprt & expression
Definition: abstract_value_object.cpp:298
constants_evaluator::adjust_expression_for_rounding_mode
exprt adjust_expression_for_rounding_mode() const
Definition: abstract_value_object.cpp:275
constants_evaluator::environment
const abstract_environmentt & environment
Definition: abstract_value_object.cpp:299
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
value_set_evaluator::evaluate_conditional
static abstract_object_pointert evaluate_conditional(const std::vector< value_ranget > &ops)
Definition: abstract_value_object.cpp:655
interval_evaluator::interval_abstract_value_pointert
sharing_ptrt< const interval_abstract_valuet > interval_abstract_value_pointert
Definition: abstract_value_object.cpp:349
value_set_evaluator::operator()
abstract_object_pointert operator()() const
Definition: abstract_value_object.cpp:505
constant_interval_exprt
Represents an interval of values.
Definition: interval.h:56
value_set_abstract_objectt::max_value_set_size
static const size_t max_value_set_size
The threshold size for value-sets: past this threshold the object is either converted to interval or ...
Definition: value_set_abstract_object.h:55
intervals_expression_transform
static abstract_object_pointert intervals_expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
Definition: abstract_value_object.cpp:480
empty_index_ranget
Definition: abstract_value_object.cpp:25
indeterminate_index_ranget
Definition: abstract_value_object.cpp:45
constant_interval_exprt::is_int
bool is_int() const
Definition: interval.cpp:1064
value_range_implementation_ptrt
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
Definition: abstract_value_object.h:130
constants_evaluator
Definition: abstract_value_object.cpp:189
interval_evaluator::transform
abstract_object_pointert transform() const
Definition: abstract_value_object.cpp:351
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
single_value_value_ranget::advance_to_next
bool advance_to_next() override
Definition: abstract_value_object.cpp:96
interval_evaluator::make_interval
interval_abstract_value_pointert make_interval(const exprt &expr) const
Definition: abstract_value_object.cpp:469
interval_evaluator::environment
const abstract_environmentt & environment
Definition: abstract_value_object.cpp:476
make_empty_index_range
index_range_implementation_ptrt make_empty_index_range()
Definition: abstract_value_object.cpp:74
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
constants_evaluator::transform
abstract_object_pointert transform() const
Definition: abstract_value_object.cpp:210
interval_evaluator::operands
const std::vector< abstract_object_pointert > & operands
Definition: abstract_value_object.cpp:475
make_unique.h
interval_evaluator
Definition: abstract_value_object.cpp:330
single_value_index_ranget::single_value_index_ranget
single_value_index_ranget(const exprt &val)
Definition: abstract_value_object.cpp:57
any_value_sets
bool any_value_sets(const std::vector< abstract_object_pointert > &operands)
Definition: abstract_value_object.cpp:147
constants_evaluator::try_transform_expr_with_all_rounding_modes
abstract_object_pointert try_transform_expr_with_all_rounding_modes() const
Definition: abstract_value_object.cpp:240
empty_index_ranget::reset
index_range_implementation_ptrt reset() const override
Definition: abstract_value_object.cpp:35
constants_evaluator::rounding_modes
std::vector< ieee_floatt::rounding_modet > rounding_modes
Definition: abstract_value_object.cpp:304
value_set_abstract_object.h
Value Set Abstract Object.
interval_evaluator::expression
const exprt & expression
Definition: abstract_value_object.cpp:474
interval_evaluator::evaluate_unary_expr
abstract_object_pointert evaluate_unary_expr(const std::vector< constant_interval_exprt > &interval_operands) const
Definition: abstract_value_object.cpp:442
abstract_environmentt::abstract_object_factory
virtual abstract_object_pointert abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const
Look at the configuration for the sensitivity and create an appropriate abstract_object.
Definition: abstract_environment.cpp:251
single_value_value_ranget::single_value_value_ranget
single_value_value_ranget(const abstract_object_pointert &val)
Definition: abstract_value_object.cpp:87
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
value_range_implementationt
Definition: abstract_value_object.h:133
constants_evaluator::ns
const namespacet & ns
Definition: abstract_value_object.cpp:300
nil_exprt
The NIL expression.
Definition: std_expr.h:2734
bitvector_types.h
Pre-defined bitvector types.
constant_interval_exprt::eval
constant_interval_exprt eval(const irep_idt &unary_operator) const
Definition: interval.cpp:792
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: bitvector_types.h:208
abstract_object_sett::insert
void insert(const abstract_object_pointert &o)
Definition: abstract_object_set.h:29
abstract_object_sett::first
abstract_object_pointert first() const
Definition: abstract_object_set.h:47
abstract_environment.h
An abstract version of a program environment.
constants_evaluator::rounding_mode_is_not_set
bool rounding_mode_is_not_set() const
Definition: abstract_value_object.cpp:292
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2557
value_set_evaluator::make_interval
static abstract_object_pointert make_interval(const abstract_object_sett &values)
Definition: abstract_value_object.cpp:640
make_top
abstract_object_pointert make_top(const typet &type)
Definition: abstract_value_object.cpp:182
constants_evaluator::operator()
abstract_object_pointert operator()() const
Definition: abstract_value_object.cpp:199
abstract_environmentt::eval
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
Definition: abstract_environment.cpp:37
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
ieee_floatt::rounding_modet
rounding_modet
Definition: ieee_float.h:126
indeterminate_index_ranget::reset
index_range_implementation_ptrt reset() const override
Definition: abstract_value_object.cpp:51
value_set_evaluator::maybe_extract_single_value
static abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton)
Definition: abstract_value_object.cpp:610
value_set_evaluator::rewrite_expression
exprt rewrite_expression(const std::vector< abstract_object_pointert > &ops) const
Definition: abstract_value_object.cpp:559
interval_evaluator::operands_as_intervals
std::vector< constant_interval_exprt > operands_as_intervals() const
Definition: abstract_value_object.cpp:388
simplify_expr.h
value_set_evaluator::transform
abstract_object_pointert transform() const
Definition: abstract_value_object.cpp:511
value_set_evaluator
Definition: abstract_value_object.cpp:493
interval_evaluator::ns
const namespacet & ns
Definition: abstract_value_object.cpp:477
constants_evaluator::rounding_mode_symbol
static const symbol_exprt rounding_mode_symbol
Definition: abstract_value_object.cpp:302
interval_evaluator::operator()
abstract_object_pointert operator()() const
Definition: abstract_value_object.cpp:342
abstract_environmentt::add_object_context
virtual abstract_object_pointert add_object_context(const abstract_object_pointert &abstract_object) const
Wraps an existing object in any configured context object.
Definition: abstract_environment.cpp:282
abstract_value_objectt::expression_transform
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.
Definition: abstract_value_object.cpp:170
make_single_value_range
value_range_implementation_ptrt make_single_value_range(const abstract_object_pointert &value)
Definition: abstract_value_object.cpp:113
ieee_floatt::ROUND_TO_PLUS_INF
@ ROUND_TO_PLUS_INF
Definition: ieee_float.h:128
ieee_floatt::ROUND_TO_EVEN
@ ROUND_TO_EVEN
Definition: ieee_float.h:127
value_set_evaluator::value_set_evaluator
value_set_evaluator(const exprt &e, const std::vector< abstract_object_pointert > &ops, const abstract_environmentt &env, const namespacet &n)
Definition: abstract_value_object.cpp:495
constant_interval_exprt::typecast
constant_interval_exprt typecast(const typet &type) const
Definition: interval.cpp:1623
empty_index_ranget::current
const exprt & current() const override
Definition: abstract_value_object.cpp:27
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
single_value_value_ranget::reset
value_range_implementation_ptrt reset() const override
Definition: abstract_value_object.cpp:102
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
ieee_float.h
interval_abstract_value.h
An interval to represent a set of possible values.
single_value_index_ranget::available
bool available
Definition: abstract_value_object.h:121
single_value_value_ranget::current
const abstract_object_pointert & current() const override
Definition: abstract_value_object.cpp:92
value_set_evaluator::is_constant_value
static bool is_constant_value(const abstract_object_pointert &v)
Definition: abstract_value_object.cpp:575
single_value_index_ranget::advance_to_next
bool advance_to_next() override
Definition: abstract_value_object.cpp:67
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
value_set_expression_transform
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)
Definition: abstract_value_object.cpp:686
single_value_value_ranget::available
bool available
Definition: abstract_value_object.cpp:109
empty_index_ranget::nil
exprt nil
Definition: abstract_value_object.cpp:41
adjust_float_expressions
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Definition: adjust_float_expressions.cpp:79
constant_interval_exprt::get_min
static exprt get_min(const exprt &a, const exprt &b)
Definition: interval.cpp:964
exprt::operands
operandst & operands()
Definition: expr.h:96
index_range_implementation_ptrt
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
Definition: abstract_value_object.h:25
value_set_evaluator::operands_as_ranges
std::vector< value_ranget > operands_as_ranges() const
Definition: abstract_value_object.cpp:581
any_of_type
bool any_of_type(const std::vector< abstract_object_pointert > &operands)
Definition: abstract_value_object.cpp:135
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
value_set_evaluator::resolve_values
static abstract_object_pointert resolve_values(const abstract_object_sett &new_values)
Definition: abstract_value_object.cpp:627
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
adjust_float_expressions.h
Symbolic Execution.
constants_evaluator::all_rounding_modes
static const rounding_modes all_rounding_modes
Definition: abstract_value_object.cpp:305
constants_evaluator::constants_evaluator
constants_evaluator(const exprt &e, const abstract_environmentt &env, const namespacet &n)
Definition: abstract_value_object.cpp:191
single_value_value_ranget
Definition: abstract_value_object.cpp:85
empty_index_ranget::advance_to_next
bool advance_to_next() override
Definition: abstract_value_object.cpp:31
abstract_object_sett::to_interval
constant_interval_exprt to_interval() const
Calculate the set of values as an interval.
Definition: abstract_object_set.cpp:40
make_indeterminate_index_range
index_range_implementation_ptrt make_indeterminate_index_range()
Definition: abstract_value_object.cpp:79
value_set_evaluator::operands
const std::vector< abstract_object_pointert > & operands
Definition: abstract_value_object.cpp:681
constants_expression_transform
static abstract_object_pointert constants_expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
Definition: abstract_value_object.cpp:317
ieee_floatt::ROUND_TO_MINUS_INF
@ ROUND_TO_MINUS_INF
Definition: ieee_float.h:127
value_set_evaluator::evaluate_each_combination
abstract_object_sett evaluate_each_combination(const std::vector< value_ranget > &value_ranges) const
Evaluate expression for every combination of values in value_ranges.
Definition: abstract_value_object.cpp:527
value_set_evaluator::ns
const namespacet & ns
Definition: abstract_value_object.cpp:683
ieee_floatt::ROUND_TO_ZERO
@ ROUND_TO_ZERO
Definition: ieee_float.h:128
constant_abstract_value.h
An abstraction of a single value that just stores a constant.
value_set_evaluator::expression
const exprt & expression
Definition: abstract_value_object.cpp:680
abstract_value_object.h
Common behaviour for abstract objects modelling values - constants, intervals, etc.