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)
69  : abstract_objectt{type, values.size() > max_value_set_size, values.empty()},
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 }
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual bool is_top() const
Find out if the abstract object is top.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
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.
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:40
operandst & operands()
Definition: expr.h:96
void clear()
Definition: irep.h:462
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The NIL expression.
Definition: std_expr.h:2735
The type of an expression, extends irept.
Definition: type.h:28
static constexpr CLONE std::size_t max_value_set_size
TODO arbitrary limit, make configurable.
const valuest & get_values() const
Get the possible values for this abstract object.
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.
valuest values
If BOTTOM then empty.
std::unordered_set< exprt, irep_hash > valuest
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override
Print the value of the abstract object.
exprt to_constant() const override
Converts to a constant expression if possible.
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,...
value_set_abstract_valuet(const typet &type, bool top=true, bool bottom=false)
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3921
bool simplify(exprt &expr, const namespacet &ns)
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
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)
Value sets for primitives.