cprover
variable_sensitivity_domain.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Abstract Interpretation
4 
5 Author: Martin Brain
6 
7 Date: April 2016
8 
9 \*******************************************************************/
10 
12 
13 #include <util/cprover_prefix.h>
14 #include <util/symbol_table.h>
15 
16 #include <algorithm>
17 
18 #ifdef DEBUG
19 # include <iostream>
20 #endif
21 
23  const irep_idt &function_from,
24  trace_ptrt trace_from,
25  const irep_idt &function_to,
26  trace_ptrt trace_to,
27  ai_baset &ai,
28  const namespacet &ns)
29 {
30  locationt from{trace_from->current_location()};
31  locationt to{trace_to->current_location()};
32 
33 #ifdef DEBUG
34  std::cout << "Transform from/to:\n";
35  std::cout << from->location_number << " --> " << to->location_number << '\n';
36 #endif
37 
38  const goto_programt::instructiont &instruction = *from;
39  switch(instruction.type())
40  {
41  case DECL:
42  {
43  abstract_object_pointert top_object =
46  instruction.decl_symbol().type(), ns, true, false)
47  ->write_location_context(from);
48  abstract_state.assign(instruction.decl_symbol(), top_object, ns);
49  }
50  // We now store top.
51  break;
52 
53  case DEAD:
54  // Remove symbol from map, the only time this occurs now (keep TOP.)
55  // It should be the case that DEAD only provides symbols for deletion.
56  abstract_state.erase(instruction.dead_symbol());
57  break;
58 
59  case ASSIGN:
60  {
61  // TODO : check return values
63  abstract_state.eval(instruction.assign_rhs(), ns)
64  ->write_location_context(from);
65  abstract_state.assign(instruction.assign_lhs(), rhs, ns);
66  }
67  break;
68 
69  case GOTO:
70  {
72  {
73  // Get the next line
74  locationt next = from;
75  next++;
76  // Is this a GOTO to the next line (i.e. pointless)
77  if(next != from->get_target())
78  {
79  if(to == from->get_target())
80  {
81  // The AI is exploring the branch where the jump is taken
82  assume(instruction.guard, ns);
83  }
84  else
85  {
86  // Exploring the path where the jump is not taken - therefore assume
87  // the condition is false
88  assume(not_exprt(instruction.guard), ns);
89  }
90  }
91  // ignore jumps to the next line, we can assume nothing
92  }
93  }
94  break;
95 
96  case ASSUME:
97  assume(instruction.guard, ns);
98  break;
99 
100  case FUNCTION_CALL:
101  {
102  transform_function_call(from, to, ai, ns);
103  break;
104  }
105 
106  case END_FUNCTION:
107  {
108  // erase parameters
109 
110  const irep_idt id = function_from;
111  const symbolt &symbol = ns.lookup(id);
112 
113  const code_typet &type = to_code_type(symbol.type);
114 
115  for(const auto &param : type.parameters())
116  {
117  // Top the arguments to the function
119  symbol_exprt(param.get_identifier(), param.type()),
120  abstract_state.abstract_object_factory(param.type(), ns, true, false),
121  ns);
122  }
123 
124  break;
125  }
126 
127  /***************************************************************/
128 
129  case ASSERT:
130  // Conditions on the program, do not alter the data or information
131  // flow and thus can be ignored.
132  // Checking of assertions can only be reasonably done once the fix-point
133  // has been computed, i.e. after all of the calls to transform.
134  break;
135 
136  case SKIP:
137  case LOCATION:
138  // Can ignore
139  break;
140 
141  case SET_RETURN_VALUE:
142  throw "the SET_RETURN_VALUE instructions should be removed first";
143 
144  case START_THREAD:
145  case END_THREAD:
146  case ATOMIC_BEGIN:
147  case ATOMIC_END:
148  throw "threading not supported";
149 
150  case THROW:
151  case CATCH:
152  throw "exceptions not handled";
153 
154  case OTHER:
155  // throw "other";
156  break;
157 
158  case NO_INSTRUCTION_TYPE:
159  break;
160  case INCOMPLETE_GOTO:
161  break;
162  default:
163  throw "unrecognised instruction type";
164  }
165 
166  DATA_INVARIANT(abstract_state.verify(), "Structural invariant");
167 }
168 
170  std::ostream &out,
171  const ai_baset &ai,
172  const namespacet &ns) const
173 {
174  abstract_state.output(out, ai, ns);
175 }
176 
178 {
179  return abstract_state.to_predicate();
180 }
181 
183  const exprt &expr,
184  const namespacet &ns) const
185 {
186  auto result = abstract_state.eval(expr, ns);
187  return result->to_predicate(expr);
188 }
189 
191  const exprt::operandst &exprs,
192  const namespacet &ns) const
193 {
194  if(exprs.empty())
195  return false_exprt();
196  if(exprs.size() == 1)
197  return to_predicate(exprs.front(), ns);
198 
199  auto predicates = std::vector<exprt>{};
201  exprs.cbegin(),
202  exprs.cend(),
203  std::back_inserter(predicates),
204  [this, &ns](const exprt &expr) { return to_predicate(expr, ns); });
205  return and_exprt(predicates);
206 }
207 
209 {
211  return;
212 }
213 
215 {
217 }
218 
220 {
222 }
223 
226  trace_ptrt from,
227  trace_ptrt to)
228 {
229 #ifdef DEBUG
230  std::cout << "Merging from/to:\n " << from->location_number << " --> "
231  << to->location_number << '\n';
232 #endif
233  auto widen_mode =
234  from->should_widen(*to) ? widen_modet::could_widen : widen_modet::no;
235  // Use the abstract_environment merge
236  bool any_changes =
237  abstract_state.merge(b.abstract_state, to->current_location(), widen_mode);
238 
239  DATA_INVARIANT(abstract_state.verify(), "Structural invariant");
240  return any_changes;
241 }
242 
244  exprt &condition,
245  const namespacet &ns) const
246 {
247  abstract_object_pointert res = abstract_state.eval(condition, ns);
248  exprt c = res->to_constant();
249 
250  if(c.id() == ID_nil)
251  {
252  bool no_simplification = true;
253 
254  // Try to simplify recursively any child operations
255  for(exprt &op : condition.operands())
256  {
257  no_simplification &= ai_simplify(op, ns);
258  }
259 
260  return no_simplification;
261  }
262  else
263  {
264  bool condition_changed = (condition != c);
265  condition = c;
266  return !condition_changed;
267  }
268 }
269 
271 {
272  return abstract_state.is_bottom();
273 }
274 
276 {
277  return abstract_state.is_top();
278 }
279 
281  const variable_sensitivity_domaint &other) const
282 {
285 }
286 
288  locationt from,
289  locationt to,
290  ai_baset &ai,
291  const namespacet &ns)
292 {
293  PRECONDITION(from->type() == FUNCTION_CALL);
294 
295  const exprt &function = from->call_function();
296 
297  const locationt next = std::next(from);
298 
299  if(function.id() == ID_symbol)
300  {
301  // called function identifier
302  const symbol_exprt &symbol_expr = to_symbol_expr(function);
303  const irep_idt function_id = symbol_expr.get_identifier();
304 
305  const code_function_callt::argumentst &called_arguments =
306  from->call_arguments();
307 
308  if(to->location_number == next->location_number)
309  {
310  if(ignore_function_call_transform(function_id))
311  {
312  return;
313  }
314 
315  if(0) // Sound on opaque function calls
316  {
317  abstract_state.havoc("opaque function call");
318  }
319  else
320  {
321  // For any parameter that is a non-const pointer, top the value it is
322  // pointing at.
323  for(const exprt &called_arg : called_arguments)
324  {
325  if(
326  called_arg.type().id() == ID_pointer &&
327  !called_arg.type().subtype().get_bool(ID_C_constant))
328  {
329  abstract_object_pointert pointer_value =
330  abstract_state.eval(called_arg, ns);
331 
332  CHECK_RETURN(pointer_value);
333 
334  // Write top to the pointer
335  pointer_value->write(
337  ns,
338  std::stack<exprt>(),
339  nil_exprt(),
341  called_arg.type().subtype(), ns, true, false),
342  false);
343  }
344  }
345 
346  // Top any global values
347  for(const auto &symbol : ns.get_symbol_table().symbols)
348  {
349  if(symbol.second.is_static_lifetime)
350  {
352  symbol_exprt(symbol.first, symbol.second.type),
354  symbol.second.type, ns, true, false),
355  ns);
356  }
357  }
358  }
359  }
360  else
361  {
362  // we have an actual call
363  const symbolt &symbol = ns.lookup(function_id);
364  const code_typet &code_type = to_code_type(symbol.type);
365  const code_typet::parameterst &declaration_parameters =
366  code_type.parameters();
367 
368  code_typet::parameterst::const_iterator parameter_it =
369  declaration_parameters.begin();
370 
371  for(const exprt &called_arg : called_arguments)
372  {
373  if(parameter_it == declaration_parameters.end())
374  {
375  INVARIANT(
376  code_type.has_ellipsis(), "Only case for insufficient args");
377  break;
378  }
379 
380  // Evaluate the expression that is being
381  // passed into the function call (called_arg)
382  abstract_object_pointert param_val =
383  abstract_state.eval(called_arg, ns)->write_location_context(from);
384 
385  // Assign the evaluated value to the symbol associated with the
386  // parameter of the function
387  const symbol_exprt parameter_expr(
388  parameter_it->get_identifier(), called_arg.type());
389  abstract_state.assign(parameter_expr, param_val, ns);
390 
391  ++parameter_it;
392  }
393 
394  // Too few arguments so invalid code
396  parameter_it == declaration_parameters.end(),
397  "Number of arguments should match parameters");
398  }
399  }
400  else
401  {
402  PRECONDITION(to == next);
403  abstract_state.havoc("unknown opaque function call");
404  }
405 }
406 
408  const irep_idt &function_id) const
409 {
410  static const std::set<irep_idt> ignored_internal_function = {
411  CPROVER_PREFIX "set_must",
412  CPROVER_PREFIX "get_must",
413  CPROVER_PREFIX "set_may",
414  CPROVER_PREFIX "get_may",
415  CPROVER_PREFIX "cleanup",
416  CPROVER_PREFIX "clear_may",
417  CPROVER_PREFIX "clear_must"};
418 
419  return ignored_internal_function.find(function_id) !=
420  ignored_internal_function.cend();
421 }
422 
424  const ai_domain_baset &function_call,
425  const ai_domain_baset &function_start,
426  const ai_domain_baset &function_end,
427  const namespacet &ns)
428 {
429  const variable_sensitivity_domaint &cast_function_call =
430  static_cast<const variable_sensitivity_domaint &>(function_call);
431 
432  const variable_sensitivity_domaint &cast_function_start =
433  static_cast<const variable_sensitivity_domaint &>(function_start);
434 
435  const variable_sensitivity_domaint &cast_function_end =
436  static_cast<const variable_sensitivity_domaint &>(function_end);
437 
438  const std::vector<irep_idt> &modified_symbol_names =
439  cast_function_start.get_modified_symbols(cast_function_end);
440 
441  std::vector<symbol_exprt> modified_symbols;
442  modified_symbols.reserve(modified_symbol_names.size());
444  modified_symbol_names.begin(),
445  modified_symbol_names.end(),
446  std::back_inserter(modified_symbols),
447  [&ns](const irep_idt &id) { return ns.lookup(id).symbol_expr(); });
448 
449  abstract_state = cast_function_call.abstract_state;
450  apply_domain(modified_symbols, cast_function_end, ns);
451 
452  return;
453 }
454 
456  std::vector<symbol_exprt> modified_symbols,
457  const variable_sensitivity_domaint &source,
458  const namespacet &ns)
459 {
460  for(const auto &symbol : modified_symbols)
461  {
462  abstract_object_pointert value = source.abstract_state.eval(symbol, ns);
463  abstract_state.assign(symbol, value, ns);
464  }
465 }
466 
468 {
469  ai_simplify(expr, ns);
470  abstract_state.assume(expr, ns);
471 }
472 
473 #ifdef ENABLE_STATS
475 variable_sensitivity_domaint::gather_statistics(const namespacet &ns) const
476 {
478 }
479 #endif
sharing_ptrt< class abstract_objectt > abstract_object_pointert
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
virtual bool assume(const exprt &expr, const namespacet &ns)
Reduces the domain based on a condition.
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print out all the values in the abstract object map.
bool is_bottom() const
Gets whether the domain is bottom.
exprt to_predicate() const
Gives a boolean condition that is true for all values represented by the environment.
void make_top()
Set the domain to top (i.e. everything)
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
void erase(const symbol_exprt &expr)
Delete a symbol from the map.
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...
bool verify() const
Check the structural invariants are maintained.
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...
abstract_object_statisticst gather_statistics(const namespacet &ns) const
virtual bool merge(const abstract_environmentt &env, const goto_programt::const_targett &merge_location, widen_modet widen_mode)
Computes the join between "this" and "b".
void make_bottom()
Set the domain to top (i.e. no possible states / unreachable)
bool is_top() const
Gets whether the domain is top.
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.
virtual bool assign(const exprt &expr, const abstract_object_pointert &value, const namespacet &ns)
Assign a value to an expression.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:55
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:74
goto_programt::const_targett locationt
Definition: ai_domain.h:73
Boolean AND.
Definition: std_expr.h:1974
exprt::operandst argumentst
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:541
bool has_ellipsis() const
Definition: std_types.h:611
const parameterst & parameters() const
Definition: std_types.h:655
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
The Boolean constant false.
Definition: std_expr.h:2865
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:213
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:243
exprt guard
Guard for gotos, assume, assert Use condition() method to access.
Definition: goto_program.h:357
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:227
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:199
goto_program_instruction_typet type() const
What kind of instruction?
Definition: goto_program.h:343
const irep_idt & id() const
Definition: irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:123
The NIL expression.
Definition: std_expr.h:2874
Boolean negation.
Definition: std_expr.h:2181
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition: symbol.h:28
typet type
Type of symbol.
Definition: symbol.h:31
bool ai_simplify(exprt &condition, const namespacet &ns) const override
Use the information in the domain to simplify the expression with respect to the current location.
exprt to_predicate() const override
Gives a Boolean condition that is true for all values represented by the domain.
void make_bottom() override
Sets the domain to bottom (no states / unreachable).
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Basic text output of the abstract domain.
void make_top() override
Sets the domain to top (all states).
void apply_domain(std::vector< symbol_exprt > modified_symbols, const variable_sensitivity_domaint &target, const namespacet &ns)
Given a domain and some symbols, apply those symbols values to the current domain.
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) override
Compute the abstract transformer for a single instruction.
std::vector< irep_idt > get_modified_symbols(const variable_sensitivity_domaint &other) const
Get symbols that have been modified since this domain and other.
bool is_bottom() const override
Find out if the domain is currently unreachable.
virtual void merge_three_way_function_return(const ai_domain_baset &function_call, const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns)
Perform a context aware merge of the changes that have been applied between function_start and the cu...
void transform_function_call(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
Used by variable_sensitivity_domaint::transform to handle FUNCTION_CALL transforms.
virtual bool merge(const variable_sensitivity_domaint &b, trace_ptrt from, trace_ptrt to)
Computes the join between "this" and "b".
void assume(exprt expr, namespacet ns)
bool is_top() const override
Is the domain completely top at this state.
bool ignore_function_call_transform(const irep_idt &function_id) const
Used to specify which CPROVER internal functions should be skipped over when doing function call tran...
void make_entry() override
Set up a reasonable entry-point state.
#define CPROVER_PREFIX
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ END_FUNCTION
Definition: goto_program.h:42
@ ASSIGN
Definition: goto_program.h:46
@ ASSERT
Definition: goto_program.h:36
@ SET_RETURN_VALUE
Definition: goto_program.h:45
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ THROW
Definition: goto_program.h:50
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
@ GOTO
Definition: goto_program.h:34
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
Author: Diffblue Ltd.
There are different ways of handling arrays, structures, unions and pointers.