cprover
constant_abstract_value.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: Thomas Kiley, thomas.kiley@diffblue.com
6 
7 \*******************************************************************/
8 
10 #include <util/namespace.h>
11 #include <util/std_expr.h>
12 #include <util/type.h>
13 
14 #include "abstract_environment.h"
16 
19 
21 {
22 public:
23  explicit constant_index_ranget(const exprt &val)
25  {
26  }
27 
29  {
31  }
32 };
33 
36 {
37  return util_make_unique<constant_index_ranget>(val);
38 }
39 
41  : abstract_value_objectt(t), value()
42 {
43 }
44 
46  : abstract_value_objectt(e.type(), false, false), value(e)
47 {
48 }
49 
51  const typet &t,
52  bool tp,
53  bool bttm)
54  : abstract_value_objectt(t, tp, bttm), value()
55 {
56 }
57 
59  const exprt &e,
60  const abstract_environmentt &environment,
61  const namespacet &ns)
62  : abstract_value_objectt(e.type(), false, false), value(e)
63 {
64 }
65 
68 {
69  exprt val = to_constant();
70  if(!val.is_constant())
72 
73  return make_constant_index_range(val);
74 }
75 
78 {
79  return make_single_value_range(shared_from_this());
80 }
81 
83 {
84  if(!is_top() && !is_bottom())
85  {
86  return this->value;
87  }
88  else
89  {
91  }
92 }
93 
95 {
97 }
98 
100  std::ostream &out,
101  const ai_baset &ai,
102  const namespacet &ns) const
103 {
104  if(!is_top() && !is_bottom())
105  {
107  }
108  else
109  {
110  abstract_objectt::output(out, ai, ns);
111  }
112 }
113 
116 {
117  auto cast_other =
118  std::dynamic_pointer_cast<const abstract_value_objectt>(other);
119  if(cast_other)
120  return merge_constant_constant(cast_other);
121 
122  return abstract_objectt::merge(other);
123 }
124 
126  const abstract_value_pointert &other) const
127 {
128  auto other_expr = other->to_constant();
129  if(is_bottom() && other_expr.is_constant())
130  return std::make_shared<constant_abstract_valuet>(other_expr);
131 
132  if(value == other_expr) // Can we actually merge these value
133  return shared_from_this();
134 
135  return abstract_objectt::merge(other);
136 }
137 
139  abstract_object_statisticst &statistics,
140  abstract_object_visitedt &visited,
141  const abstract_environmentt &env,
142  const namespacet &ns) const
143 {
144  abstract_objectt::get_statistics(statistics, visited, env, ns);
145  ++statistics.number_of_constants;
146  statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
147 }
single_value_index_ranget
Definition: abstract_value_object.h:109
abstract_value_pointert
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
Definition: abstract_value_object.h:297
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
abstract_objectt::is_top
virtual bool is_top() const
Find out if the abstract object is top.
Definition: abstract_object.cpp:150
abstract_objectt::merge
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
Definition: abstract_object.cpp:189
abstract_objectt::output
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
Definition: abstract_object.cpp:170
constant_abstract_valuet::to_constant
exprt to_constant() const override
Converts to a constant expression if possible.
Definition: constant_abstract_value.cpp:82
typet
The type of an expression, extends irept.
Definition: type.h:28
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
constant_abstract_valuet::merge
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Attempts to do a constant/constant merge if both are constants, otherwise falls back to the parent me...
Definition: constant_abstract_value.cpp:115
single_value_index_ranget::value
const exprt value
Definition: abstract_value_object.h:118
abstract_objectt::get_statistics
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
Definition: abstract_object.cpp:284
namespace.h
constant_abstract_valuet::value
exprt value
Definition: constant_abstract_value.h:86
constant_interval_exprt
Represents an interval of values.
Definition: interval.h:56
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
value_range_implementation_ptrt
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
Definition: abstract_value_object.h:130
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
constant_abstract_valuet::merge_constant_constant
abstract_object_pointert merge_constant_constant(const abstract_value_pointert &other) const
Merges another abstract value into this one.
Definition: constant_abstract_value.cpp:125
constant_abstract_valuet::value_range_implementation
value_range_implementation_ptrt value_range_implementation() const override
Definition: constant_abstract_value.cpp:77
constant_index_ranget
Definition: constant_abstract_value.cpp:21
constant_abstract_valuet::output
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
Definition: constant_abstract_value.cpp:99
abstract_object_statisticst
Definition: abstract_object_statistics.h:19
abstract_value_objectt
Definition: abstract_value_object.h:240
language_util.h
abstract_environment.h
An abstract version of a program environment.
abstract_objectt::to_constant
virtual exprt to_constant() const
Converts to a constant expression if possible.
Definition: abstract_object.cpp:165
abstract_object_visitedt
std::set< abstract_object_pointert > abstract_object_visitedt
Definition: abstract_object.h:76
constant_abstract_valuet::constant_abstract_valuet
constant_abstract_valuet(const typet &t)
Definition: constant_abstract_value.cpp:40
constant_index_ranget::constant_index_ranget
constant_index_ranget(const exprt &val)
Definition: constant_abstract_value.cpp:23
make_single_value_range
value_range_implementation_ptrt make_single_value_range(const abstract_object_pointert &value)
Definition: abstract_value_object.cpp:113
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:53
abstract_object_statisticst::objects_memory_usage
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.
Definition: abstract_object_statistics.h:28
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
abstract_object_statisticst::number_of_constants
std::size_t number_of_constants
Definition: abstract_object_statistics.h:25
make_constant_index_range
static index_range_implementation_ptrt make_constant_index_range(const exprt &val)
Definition: constant_abstract_value.cpp:35
constant_abstract_valuet::get_statistics
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
Definition: constant_abstract_value.cpp:138
index_range_implementation_ptrt
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
Definition: abstract_value_object.h:25
constant_index_ranget::reset
index_range_implementation_ptrt reset() const override
Definition: constant_abstract_value.cpp:28
abstract_objectt::is_bottom
virtual bool is_bottom() const
Find out if the abstract object is bottom.
Definition: abstract_object.cpp:155
constant_abstract_valuet::to_interval
constant_interval_exprt to_interval() const override
Definition: constant_abstract_value.cpp:94
std_expr.h
API to expression classes.
memory_sizet::from_bytes
static memory_sizet from_bytes(std::size_t bytes)
Definition: memory_units.cpp:38
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
make_indeterminate_index_range
index_range_implementation_ptrt make_indeterminate_index_range()
Definition: abstract_value_object.cpp:79
constant_abstract_valuet::index_range_implementation
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
Definition: constant_abstract_value.cpp:67
constant_abstract_value.h
An abstraction of a single value that just stores a constant.
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700