cprover
value_set_abstract_value.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity variable-sensitivity-value-set
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
10 
11 #include <ansi-c/expr2c.h>
12 #include <util/simplify_expr.h>
13 
15  const typet &type,
16  bool top,
17  bool bottom)
18  : abstract_objectt{type, top, bottom}, values{}
19 {
20 }
21 
24 {
25  PRECONDITION(!is_top());
27  return values;
28 }
29 
32 {
33  if(is_top())
34  {
35  return shared_from_this();
36  }
37 
38  if(other->is_top())
39  {
40  return other;
41  }
42 
43  if(is_bottom())
44  {
45  return other;
46  }
47 
48  if(other->is_bottom())
49  {
50  return shared_from_this();
51  }
52 
53  if(
54  auto other_value_set =
55  dynamic_cast<const value_set_abstract_valuet *>(other.get()))
56  {
57  valuest merged_values{values};
58  auto const &other_values = other_value_set->get_values();
59  merged_values.insert(other_values.begin(), other_values.end());
60  return std::make_shared<value_set_abstract_valuet>(
61  type(), std::move(merged_values));
62  }
63  return abstract_objectt::merge(other);
64 }
65 
67  const typet &type,
68  valuest values)
70  values{std::move(values)}
71 {
72  if(values.size() > max_value_set_size)
73  {
74  this->values.clear();
75  }
76 }
77 
79  exprt expr,
80  const abstract_environmentt &environment,
81  const namespacet &ns)
82  : value_set_abstract_valuet{expr.type(), valuest{expr}}
83 {
84 }
85 
87 {
88  if(!is_top() && !is_bottom() && values.size() == 1)
89  {
90  return *values.begin();
91  }
92  else
93  {
94  return nil_exprt{};
95  }
96 }
97 
99  std::ostream &out,
100  const class ai_baset &,
101  const namespacet &ns) const
102 {
103  if(is_bottom())
104  {
105  out << "BOTTOM";
106  return;
107  }
108  else if(is_top())
109  {
110  out << "TOP";
111  return;
112  }
113 
114  std::vector<std::string> vals;
115  for(const auto &elem : values)
116  {
117  vals.push_back(expr2c(elem, ns));
118  }
119 
120  std::sort(vals.begin(), vals.end());
121 
122  out << "{ ";
123  for(const auto &val : vals)
124  {
125  out << val << " ";
126  }
127  out << "}";
128 }
129 
131  std::shared_ptr<const value_set_abstract_valuet> &out_value,
132  const exprt &expr,
133  const std::vector<const value_set_abstract_valuet *> &operand_value_sets,
134  const namespacet &ns,
135  std::vector<exprt> &operands_so_far)
136 {
137  if(expr.operands().size() == operands_so_far.size())
138  {
139  exprt expr_with_evaluated_operands_filled_in = expr;
140  expr_with_evaluated_operands_filled_in.operands() = operands_so_far;
141  simplify(expr_with_evaluated_operands_filled_in, ns);
142  if(expr_with_evaluated_operands_filled_in.is_constant())
143  {
144  auto post_merge = abstract_objectt::merge(
145  out_value,
146  std::make_shared<value_set_abstract_valuet>(
147  expr.type(),
149  expr_with_evaluated_operands_filled_in}));
150  if(
151  auto post_merge_casted =
152  std::dynamic_pointer_cast<const value_set_abstract_valuet>(
153  post_merge))
154  {
155  out_value = post_merge_casted;
156  return;
157  }
158  }
159  out_value = std::make_shared<value_set_abstract_valuet>(expr.type());
160  }
161  else
162  {
163  for(auto const &operand_value :
164  operand_value_sets[operands_so_far.size()]->get_values())
165  {
166  operands_so_far.push_back(operand_value);
168  out_value, expr, operand_value_sets, ns, operands_so_far);
169  operands_so_far.pop_back();
170  }
171  }
172 }
173 
174 static std::shared_ptr<const value_set_abstract_valuet>
176  const exprt &expr,
177  const std::vector<const value_set_abstract_valuet *> &operand_value_sets,
178  const namespacet &ns)
179 {
180  const bool is_top = false;
181  const bool is_bottom = true;
182  auto result_abstract_value =
183  std::make_shared<const value_set_abstract_valuet>(
184  expr.type(), is_top, is_bottom);
185  auto operands_so_far = std::vector<exprt>{};
187  result_abstract_value, expr, operand_value_sets, ns, operands_so_far);
188  return result_abstract_value;
189 }
190 
192  const exprt &expr,
193  const std::vector<abstract_object_pointert> &operands,
194  const abstract_environmentt &environment,
195  const namespacet &ns) const
196 {
197  // TODO possible special case handling for things like
198  // __CPROVER_rounding_mode where we know what valid values look like
199  // which we could make use of in place of TOP
200  auto operand_value_sets = std::vector<const value_set_abstract_valuet *>{};
201  for(auto const &possible_value_set : operands)
202  {
203  PRECONDITION(possible_value_set != nullptr);
204  const auto as_value_set =
205  dynamic_cast<const value_set_abstract_valuet *>(possible_value_set.get());
206  if(
207  as_value_set == nullptr || as_value_set->is_top() ||
208  as_value_set->is_bottom())
209  {
210  return std::make_shared<value_set_abstract_valuet>(expr.type());
211  }
212  operand_value_sets.push_back(as_value_set);
213  }
214  return merge_all_possible_results(expr, operand_value_sets, ns);
215 }
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
value_set_abstract_value.h
Value sets for primitives.
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
value_set_abstract_valuet::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 override
Interface for transforms.
Definition: value_set_abstract_value.cpp:191
typet
The type of an expression, extends irept.
Definition: type.h:28
abstract_objectt::type
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
Definition: abstract_object.cpp:53
value_set_abstract_valuet::to_constant
exprt to_constant() const override
Converts to a constant expression if possible.
Definition: value_set_abstract_value.cpp:86
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
value_set_abstract_valuet::max_value_set_size
static constexpr CLONE std::size_t max_value_set_size
TODO arbitrary limit, make configurable.
Definition: value_set_abstract_value.h:43
value_set_abstract_valuet::valuest
std::unordered_set< exprt, irep_hash > valuest
Definition: value_set_abstract_value.h:24
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
value_set_abstract_valuet::value_set_abstract_valuet
value_set_abstract_valuet(const typet &type, bool top=true, bool bottom=false)
Definition: value_set_abstract_value.cpp:14
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
expr2c.h
expr2c
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3921
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
nil_exprt
The NIL expression.
Definition: std_expr.h:2735
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2524
value_set_abstract_valuet::values
valuest values
If BOTTOM then empty.
Definition: value_set_abstract_value.h:63
abstract_objectt::bottom
bool bottom
Definition: abstract_object.h:362
simplify_expr.h
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:40
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
merge_all_possible_results
static void merge_all_possible_results(std::shared_ptr< const value_set_abstract_valuet > &out_value, const exprt &expr, const std::vector< const value_set_abstract_valuet * > &operand_value_sets, const namespacet &ns, std::vector< exprt > &operands_so_far)
Definition: value_set_abstract_value.cpp:130
value_set_abstract_valuet::output
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override
Print the value of the abstract object.
Definition: value_set_abstract_value.cpp:98
value_set_abstract_valuet
Definition: value_set_abstract_value.h:22
exprt::operands
operandst & operands()
Definition: expr.h:96
abstract_objectt::top
bool top
Definition: abstract_object.h:363
value_set_abstract_valuet::get_values
const valuest & get_values() const
Get the possible values for this abstract object.
Definition: value_set_abstract_value.cpp:23
abstract_objectt
Definition: abstract_object.h:79
abstract_objectt::is_bottom
virtual bool is_bottom() const
Find out if the abstract object is bottom.
Definition: abstract_object.cpp:155
value_set_abstract_valuet::merge
abstract_object_pointert merge(abstract_object_pointert other) const override
Create a new abstract object that is the result of the merge, unless the object would be unchanged,...
Definition: value_set_abstract_value.cpp:31