cprover
abstract_environment.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 
9 #include <analyses/ai.h>
18 #include <util/pointer_expr.h>
19 #include <util/simplify_expr.h>
20 
21 #include <algorithm>
22 #include <functional>
23 #include <map>
24 #include <ostream>
25 #include <stack>
26 
27 #ifdef DEBUG
28 # include <iostream>
29 #endif
30 
31 std::vector<abstract_object_pointert> eval_operands(
32  const exprt &expr,
33  const abstract_environmentt &env,
34  const namespacet &ns);
35 
37 abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
38 {
39  if(bottom)
40  return abstract_object_factory(expr.type(), ns, false, true);
41 
42  // first try to canonicalise, including constant folding
43  const exprt &simplified_expr = simplify_expr(expr, ns);
44 
45  const irep_idt simplified_id = simplified_expr.id();
46  if(simplified_id == ID_symbol)
47  return resolve_symbol(simplified_expr, ns);
48 
49  if(
50  simplified_id == ID_member || simplified_id == ID_index ||
51  simplified_id == ID_dereference)
52  {
53  auto access_expr = simplified_expr;
54  auto target = eval(access_expr.operands()[0], ns);
55 
56  return target->expression_transform(
57  access_expr, eval_operands(access_expr, *this, ns), *this, ns);
58  }
59 
60  if(
61  simplified_id == ID_array || simplified_id == ID_struct ||
62  simplified_id == ID_constant || simplified_id == ID_address_of)
63  {
64  return abstract_object_factory(simplified_expr.type(), simplified_expr, ns);
65  }
66 
67  // No special handling required by the abstract environment
68  // delegate to the abstract object
69  if(!simplified_expr.operands().empty())
70  {
71  return eval_expression(simplified_expr, ns);
72  }
73  else
74  {
75  // It is important that this is top as the abstract object may not know
76  // how to handle the expression
77  return abstract_object_factory(simplified_expr.type(), ns, true, false);
78  }
79 }
80 
82  const exprt &expr,
83  const namespacet &ns) const
84 {
85  const symbol_exprt &symbol(to_symbol_expr(expr));
86  const auto symbol_entry = map.find(symbol.get_identifier());
87 
88  if(symbol_entry.has_value())
89  return symbol_entry.value();
90  return abstract_object_factory(expr.type(), ns, true, false);
91 }
92 
94  const exprt &expr,
95  const abstract_object_pointert &value,
96  const namespacet &ns)
97 {
98  PRECONDITION(value);
99 
100  if(value->is_bottom())
101  {
102  bool bottom_at_start = this->is_bottom();
103  this->make_bottom();
104  return !bottom_at_start;
105  }
106 
107  abstract_object_pointert lhs_value = nullptr;
108  // Build a stack of index, member and dereference accesses which
109  // we will work through the relevant abstract objects
110  exprt s = expr;
111  std::stack<exprt> stactions; // I'm not a continuation, honest guv'
112  while(s.id() != ID_symbol)
113  {
114  if(s.id() == ID_index || s.id() == ID_member || s.id() == ID_dereference)
115  {
116  stactions.push(s);
117  s = s.operands()[0];
118  }
119  else
120  {
121  lhs_value = eval(s, ns);
122  break;
123  }
124  }
125 
126  if(!lhs_value)
127  {
128  INVARIANT(s.id() == ID_symbol, "Have a symbol or a stack");
129  lhs_value = resolve_symbol(s, ns);
130  }
131 
132  abstract_object_pointert final_value;
133 
134  // This is the root abstract object that is in the map of abstract objects
135  // It might not have the same type as value if the above stack isn't empty
136 
137  if(!stactions.empty())
138  {
139  // The symbol is not in the map - it is therefore top
140  final_value = write(lhs_value, value, stactions, ns, false);
141  }
142  else
143  {
144  // If we don't have a symbol on the LHS, then we must have some expression
145  // that we can write to (i.e. a pointer, an array, a struct) This appears
146  // to be none of that.
147  if(s.id() != ID_symbol)
148  {
149  throw std::runtime_error("invalid l-value");
150  }
151  // We can assign the AO directly to the symbol
152  final_value = value;
153  }
154 
155  const typet &lhs_type = ns.follow(lhs_value->type());
156  const typet &rhs_type = ns.follow(final_value->type());
157 
158  // Write the value for the root symbol back into the map
159  INVARIANT(
160  lhs_type == rhs_type,
161  "Assignment types must match"
162  "\n"
163  "lhs_type :" +
164  lhs_type.pretty() +
165  "\n"
166  "rhs_type :" +
167  rhs_type.pretty());
168 
169  // If LHS was directly the symbol
170  if(s.id() == ID_symbol)
171  {
172  symbol_exprt symbol_expr = to_symbol_expr(s);
173 
174  if(final_value != lhs_value)
175  {
176  CHECK_RETURN(!symbol_expr.get_identifier().empty());
177  map.insert_or_replace(symbol_expr.get_identifier(), final_value);
178  }
179  }
180  return true;
181 }
182 
184  const abstract_object_pointert &lhs,
185  const abstract_object_pointert &rhs,
186  std::stack<exprt> remaining_stack,
187  const namespacet &ns,
188  bool merge_write)
189 {
190  PRECONDITION(!remaining_stack.empty());
191  const exprt &next_expr = remaining_stack.top();
192  remaining_stack.pop();
193 
194  const irep_idt &stack_head_id = next_expr.id();
195  INVARIANT(
196  stack_head_id == ID_index || stack_head_id == ID_member ||
197  stack_head_id == ID_dereference,
198  "Write stack expressions must be index, member, or dereference");
199 
200  return lhs->write(*this, ns, remaining_stack, next_expr, rhs, merge_write);
201 }
202 
203 bool abstract_environmentt::assume(const exprt &expr, const namespacet &ns)
204 {
205  // We should only attempt to assume Boolean things
206  // This should be enforced by the well-structured-ness of the
207  // goto-program and the way assume is used.
208 
209  PRECONDITION(expr.type().id() == ID_bool);
210 
211  // Evaluate the expression
212  abstract_object_pointert res = eval(expr, ns);
213 
214  exprt possibly_constant = res->to_constant();
215 
216  if(possibly_constant.id() != ID_nil) // I.E. actually a value
217  {
218  // Should be of the right type
219  INVARIANT(
220  possibly_constant.type().id() == ID_bool, "simplication preserves type");
221 
222  if(possibly_constant.is_false())
223  {
224  bool currently_bottom = is_bottom();
225  make_bottom();
226  return !currently_bottom;
227  }
228  }
229 
230  /* TODO : full implementation here
231  * Note that this is *very* syntax dependent so some normalisation would help
232  * 1. split up conjuncts, handle each part separately
233  * 2. check how many variables the term contains
234  * 0 = this should have been simplified away
235  * 2+ = ignore as this is a non-relational domain
236  * 1 = extract the expression for the variable,
237  * care must be taken for things like a[i]
238  * which can be used if i can be resolved to a constant
239  * 3. use abstract_object_factory to build an abstract_objectt
240  * of the correct type (requires a little extension)
241  * This allows constant domains to handle x==23,
242  * intervals to handle x < 4, etc.
243  * 4. eval the current value of the variable
244  * 5. compute the meet (not merge!) of the two abstract_objectt's
245  * 6. assign the new value back to the environment.
246  */
247 
248  return false;
249 }
250 
252  const typet &type,
253  const namespacet &ns,
254  bool top,
255  bool bttm) const
256 {
257  exprt empty_constant_expr = nil_exprt();
259  type, top, bttm, empty_constant_expr, *this, ns);
260 }
261 
263  const typet &type,
264  const exprt &e,
265  const namespacet &ns) const
266 {
267  return abstract_object_factory(type, false, false, e, *this, ns);
268 }
269 
271  const typet &type,
272  bool top,
273  bool bttm,
274  const exprt &e,
275  const abstract_environmentt &environment,
276  const namespacet &ns) const
277 {
278  return object_factory->get_abstract_object(
279  type, top, bttm, e, environment, ns);
280 }
281 
283  const abstract_object_pointert &abstract_object) const
284 {
285  return object_factory->wrap_with_context(abstract_object);
286 }
287 
289 {
290  // for each entry in the incoming environment we need to either add it
291  // if it is new, or merge with the existing key if it is not present
292 
293  if(bottom)
294  {
295  *this = env;
296  return !env.bottom;
297  }
298  else if(env.bottom)
299  {
300  return false;
301  }
302  else
303  {
304  // For each element in the intersection of map and env.map merge
305  // If the result of the merge is top, remove from the map
306  bool modified = false;
307  decltype(env.map)::delta_viewt delta_view;
308  env.map.get_delta_view(map, delta_view);
309  for(const auto &entry : delta_view)
310  {
311  bool object_modified = false;
313  entry.get_other_map_value(), entry.m, object_modified);
314  modified |= object_modified;
315  map.replace(entry.k, new_object);
316  }
317 
318  return modified;
319  }
320 }
321 
322 void abstract_environmentt::havoc(const std::string &havoc_string)
323 {
324  // TODO(tkiley): error reporting
325  make_top();
326 }
327 
329 {
330  // since we assume anything is not in the map is top this is sufficient
331  map.clear();
332  bottom = false;
333 }
334 
336 {
337  map.clear();
338  bottom = true;
339 }
340 
342 {
343  return map.empty() && bottom;
344 }
345 
347 {
348  return map.empty() && !bottom;
349 }
350 
352  std::ostream &out,
353  const ai_baset &ai,
354  const namespacet &ns) const
355 {
356  out << "{\n";
357 
358  decltype(map)::viewt view;
359  map.get_view(view);
360  for(const auto &entry : view)
361  {
362  out << entry.first << " () -> ";
363  entry.second->output(out, ai, ns);
364  out << "\n";
365  }
366  out << "}\n";
367 }
368 
370 {
371  decltype(map)::viewt view;
372  map.get_view(view);
373  for(const auto &entry : view)
374  {
375  if(entry.second == nullptr)
376  {
377  return false;
378  }
379  }
380  return true;
381 }
382 
384  const exprt &e,
385  const namespacet &ns) const
386 {
387  // We create a temporary top abstract object (according to the
388  // type of the expression), and call expression transform on it.
389  // The value of the temporary abstract object is ignored, its
390  // purpose is just to dispatch the expression transform call to
391  // a concrete subtype of abstract_objectt.
392  auto eval_obj = abstract_object_factory(e.type(), ns, true, false);
393  auto operands = eval_operands(e, *this, ns);
394 
395  return eval_obj->expression_transform(e, operands, *this, ns);
396 }
397 
399 {
400  map.erase_if_exists(expr.get_identifier());
401 }
402 
403 std::vector<abstract_environmentt::map_keyt>
405  const abstract_environmentt &first,
406  const abstract_environmentt &second)
407 {
408  // Find all symbols who have different write locations in each map
409  std::vector<abstract_environmentt::map_keyt> symbols_diff;
410  decltype(first.map)::viewt view;
411  first.map.get_view(view);
412  for(const auto &entry : view)
413  {
414  const auto &second_entry = second.map.find(entry.first);
415  if(second_entry.has_value())
416  {
417  if(second_entry.value().get()->has_been_modified(entry.second))
418  {
419  CHECK_RETURN(!entry.first.empty());
420  symbols_diff.push_back(entry.first);
421  }
422  }
423  }
424 
425  // Add any symbols that are only in the second map
426  for(const auto &entry : second.map.get_view())
427  {
428  const auto &second_entry = first.map.find(entry.first);
429  if(!second_entry.has_value())
430  {
431  CHECK_RETURN(!entry.first.empty());
432  symbols_diff.push_back(entry.first);
433  }
434  }
435  return symbols_diff;
436 }
437 
438 static std::size_t count_globals(const namespacet &ns)
439 {
440  auto const &symtab = ns.get_symbol_table();
441  auto val = std::count_if(
442  symtab.begin(),
443  symtab.end(),
444  [](const symbol_tablet::const_iteratort::value_type &sym) {
445  return sym.second.is_lvalue && sym.second.is_static_lifetime;
446  });
447  return val;
448 }
449 
452 {
453  abstract_object_statisticst statistics = {};
454  statistics.number_of_globals = count_globals(ns);
455  decltype(map)::viewt view;
456  map.get_view(view);
457  abstract_object_visitedt visited;
458  for(auto const &object : view)
459  {
460  if(visited.find(object.second) == visited.end())
461  {
462  object.second->get_statistics(statistics, visited, *this, ns);
463  }
464  }
465  return statistics;
466 }
467 
468 std::vector<abstract_object_pointert> eval_operands(
469  const exprt &expr,
470  const abstract_environmentt &env,
471  const namespacet &ns)
472 {
473  std::vector<abstract_object_pointert> operands;
474 
475  for(const auto &op : expr.operands())
476  operands.push_back(env.eval(op, ns));
477 
478  return operands;
479 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
abstract_object_statisticst::number_of_globals
std::size_t number_of_globals
Definition: abstract_object_statistics.h:26
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
variable_sensitivity_object_factory.h
Tracks the user-supplied configuration for VSD and build the correct type of abstract object when nee...
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_environmentt::write
virtual abstract_object_pointert write(const abstract_object_pointert &lhs, const abstract_object_pointert &rhs, std::stack< exprt > remaining_stack, const namespacet &ns, bool merge_write)
Used within assign to do the actual dispatch.
Definition: abstract_environment.cpp:183
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:28
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:492
two_value_struct_abstract_object.h
The base of all structure abstractions.
abstract_environmentt::resolve_symbol
abstract_object_pointert resolve_symbol(const exprt &e, const namespacet &ns) const
Definition: abstract_environment.cpp:81
abstract_environmentt::bottom
bool bottom
Definition: abstract_environment.h:246
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
abstract_environmentt::verify
bool verify() const
Check the structural invariants are maintained.
Definition: abstract_environment.cpp:369
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
abstract_environmentt::output
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print out all the values in the abstract object map.
Definition: abstract_environment.cpp:351
abstract_environmentt::havoc
virtual void havoc(const std::string &havoc_string)
This should be used as a default case / everything else has failed The string is so that I can easily...
Definition: abstract_environment.cpp:322
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
abstract_environmentt::make_top
void make_top()
Set the domain to top (i.e. everything)
Definition: abstract_environment.cpp:328
abstract_object.h
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
abstract_environmentt::eval_expression
virtual abstract_object_pointert eval_expression(const exprt &e, const namespacet &ns) const
Definition: abstract_environment.cpp:383
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
abstract_environmentt::object_factory
variable_sensitivity_object_factory_ptrt object_factory
Definition: abstract_environment.h:280
abstract_environmentt::is_top
bool is_top() const
Gets whether the domain is top.
Definition: abstract_environment.cpp:346
two_value_pointer_abstract_object.h
abstract_object_statisticst
Definition: abstract_object_statistics.h:19
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
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
abstract_environmentt::make_bottom
void make_bottom()
Set the domain to top (i.e. no possible states / unreachable)
Definition: abstract_environment.cpp:335
nil_exprt
The NIL expression.
Definition: std_expr.h:2735
pointer_expr.h
API to expression classes for Pointers.
abstract_environment.h
An abstract version of a program environment.
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2529
abstract_environmentt::map
sharing_mapt< map_keyt, abstract_object_pointert > map
Definition: abstract_environment.h:255
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
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
dstringt::empty
bool empty() const
Definition: dstring.h:88
abstract_object_visitedt
std::set< abstract_object_pointert > abstract_object_visitedt
Definition: abstract_object.h:76
ai.h
Abstract Interpretation.
simplify_expr.h
namespacet::get_symbol_table
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:124
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_environmentt::merge
virtual bool merge(const abstract_environmentt &env)
Computes the join between "this" and "b".
Definition: abstract_environment.cpp:288
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
abstract_object_statistics.h
Statistics gathering for the variable senstivity domain.
two_value_array_abstract_object.h
The base type of all abstract array representations.
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
abstract_environmentt::modified_symbols
static std::vector< abstract_environmentt::map_keyt > modified_symbols(const abstract_environmentt &first, const abstract_environmentt &second)
For our implementation of variable sensitivity domains, we need to be able to efficiently find symbol...
Definition: abstract_environment.cpp:404
exprt::operands
operandst & operands()
Definition: expr.h:96
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
count_globals
static std::size_t count_globals(const namespacet &ns)
Definition: abstract_environment.cpp:438
eval_operands
std::vector< abstract_object_pointert > eval_operands(const exprt &expr, const abstract_environmentt &env, const namespacet &ns)
Definition: abstract_environment.cpp:468
abstract_environmentt::gather_statistics
abstract_object_statisticst gather_statistics(const namespacet &ns) const
Definition: abstract_environment.cpp:451
abstract_environmentt::is_bottom
bool is_bottom() const
Gets whether the domain is bottom.
Definition: abstract_environment.cpp:341
abstract_environmentt::erase
void erase(const symbol_exprt &expr)
Delete a symbol from the map.
Definition: abstract_environment.cpp:398
constant_abstract_value.h
An abstraction of a single value that just stores a constant.
abstract_environmentt::assume
virtual bool assume(const exprt &expr, const namespacet &ns)
Reduces the domain based on a condition.
Definition: abstract_environment.cpp:203