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 
11 #include <ostream>
12 
14 #include <util/message.h>
15 #include <util/simplify_expr.h>
16 
18 #include <util/cprover_prefix.h>
19 
20 #ifdef DEBUG
21 # include <iostream>
22 #endif
23 
25  const irep_idt &function_from,
26  trace_ptrt trace_from,
27  const irep_idt &function_to,
28  trace_ptrt trace_to,
29  ai_baset &ai,
30  const namespacet &ns)
31 {
32  locationt from{trace_from->current_location()};
33  locationt to{trace_to->current_location()};
34 
35 #ifdef DEBUG
36  std::cout << "Transform from/to:\n";
37  std::cout << from->location_number << " --> " << to->location_number << '\n';
38 #endif
39 
40  const goto_programt::instructiont &instruction = *from;
41  switch(instruction.type)
42  {
43  case DECL:
44  {
45  const abstract_objectt::locationst write_location = {from};
46  abstract_object_pointert top_object =
49  instruction.decl_symbol().type(), ns, true, false)
50  ->update_location_context(write_location, true);
51  abstract_state.assign(instruction.decl_symbol(), top_object, ns);
52  }
53  // We now store top.
54  break;
55 
56  case DEAD:
57  // Remove symbol from map, the only time this occurs now (keep TOP.)
58  // It should be the case that DEAD only provides symbols for deletion.
59  abstract_state.erase(instruction.dead_symbol());
60  break;
61 
62  case ASSIGN:
63  {
64  // TODO : check return values
65  const code_assignt &inst = to_code_assign(instruction.code);
66  const abstract_objectt::locationst write_location = {from};
68  abstract_state.eval(inst.rhs(), ns)
69  ->update_location_context(write_location, true);
70  abstract_state.assign(inst.lhs(), rhs, ns);
71  }
72  break;
73 
74  case GOTO:
75  {
77  {
78  // Get the next line
79  locationt next = from;
80  next++;
81  // Is this a GOTO to the next line (i.e. pointless)
82  if(next != from->get_target())
83  {
84  if(to == from->get_target())
85  {
86  // The AI is exploring the branch where the jump is taken
87  abstract_state.assume(instruction.guard, ns);
88  }
89  else
90  {
91  // Exploring the path where the jump is not taken - therefore assume
92  // the condition is false
93  abstract_state.assume(not_exprt(instruction.guard), ns);
94  }
95  }
96  // ignore jumps to the next line, we can assume nothing
97  }
98  }
99  break;
100 
101  case ASSUME:
102  abstract_state.assume(instruction.guard, ns);
103  break;
104 
105  case FUNCTION_CALL:
106  {
107  transform_function_call(from, to, ai, ns);
108  break;
109  }
110 
111  case END_FUNCTION:
112  {
113  // erase parameters
114 
115  const irep_idt id = function_from;
116  const symbolt &symbol = ns.lookup(id);
117 
118  const code_typet &type = to_code_type(symbol.type);
119 
120  for(const auto &param : type.parameters())
121  {
122  // Top the arguments to the function
124  symbol_exprt(param.get_identifier(), param.type()),
125  abstract_state.abstract_object_factory(param.type(), ns, true, false),
126  ns);
127  }
128 
129  break;
130  }
131 
132  /***************************************************************/
133 
134  case ASSERT:
135  // Conditions on the program, do not alter the data or information
136  // flow and thus can be ignored.
137  // Checking of assertions can only be reasonably done once the fix-point
138  // has been computed, i.e. after all of the calls to transform.
139  break;
140 
141  case SKIP:
142  case LOCATION:
143  // Can ignore
144  break;
145 
146  case RETURN:
147  throw "return instructions should be removed first";
148 
149  case START_THREAD:
150  case END_THREAD:
151  case ATOMIC_BEGIN:
152  case ATOMIC_END:
153  throw "threading not supported";
154 
155  case THROW:
156  case CATCH:
157  throw "exceptions not handled";
158 
159  case OTHER:
160  // throw "other";
161  break;
162 
163  case NO_INSTRUCTION_TYPE:
164  break;
165  case INCOMPLETE_GOTO:
166  break;
167  default:
168  throw "unrecognised instruction type";
169  }
170 
171  DATA_INVARIANT(abstract_state.verify(), "Structural invariant");
172 }
173 
175  std::ostream &out,
176  const ai_baset &ai,
177  const namespacet &ns) const
178 {
179  abstract_state.output(out, ai, ns);
180 }
181 
183 {
185  return;
186 }
187 
189 {
191 }
192 
194 {
196 }
197 
200  locationt from,
201  locationt to)
202 {
203 #ifdef DEBUG
204  std::cout << "Merging from/to:\n " << from->location_number << " --> "
205  << to->location_number << '\n';
206 #endif
207 
208  // Use the abstract_environment merge
209  bool any_changes = abstract_state.merge(b.abstract_state);
210 
211  DATA_INVARIANT(abstract_state.verify(), "Structural invariant");
212  return any_changes;
213 }
214 
216  exprt &condition,
217  const namespacet &ns) const
218 {
219  abstract_object_pointert res = abstract_state.eval(condition, ns);
220  exprt c = res->to_constant();
221 
222  if(c.id() == ID_nil)
223  {
224  bool no_simplification = true;
225 
226  // Try to simplify recursively any child operations
227  for(exprt &op : condition.operands())
228  {
229  no_simplification &= ai_simplify(op, ns);
230  }
231 
232  return no_simplification;
233  }
234  else
235  {
236  bool condition_changed = (condition != c);
237  condition = c;
238  return !condition_changed;
239  }
240 }
241 
243 {
244  return abstract_state.is_bottom();
245 }
246 
248 {
249  return abstract_state.is_top();
250 }
251 
253  const variable_sensitivity_domaint &other) const
254 {
257 }
258 
260  locationt from,
261  locationt to,
262  ai_baset &ai,
263  const namespacet &ns)
264 {
265  PRECONDITION(from->type == FUNCTION_CALL);
266 
267  const code_function_callt &function_call = to_code_function_call(from->code);
268  const exprt &function = function_call.function();
269 
270  const locationt next = std::next(from);
271 
272  if(function.id() == ID_symbol)
273  {
274  // called function identifier
275  const symbol_exprt &symbol_expr = to_symbol_expr(function);
276  const irep_idt function_id = symbol_expr.get_identifier();
277 
278  const code_function_callt::argumentst &called_arguments =
279  function_call.arguments();
280 
281  if(to->location_number == next->location_number)
282  {
283  if(ignore_function_call_transform(function_id))
284  {
285  return;
286  }
287 
288  if(0) // Sound on opaque function calls
289  {
290  abstract_state.havoc("opaque function call");
291  }
292  else
293  {
294  // For any parameter that is a non-const pointer, top the value it is
295  // pointing at.
296  for(const exprt &called_arg : called_arguments)
297  {
298  if(
299  called_arg.type().id() == ID_pointer &&
300  !called_arg.type().subtype().get_bool(ID_C_constant))
301  {
302  abstract_object_pointert pointer_value =
303  abstract_state.eval(called_arg, ns);
304 
305  CHECK_RETURN(pointer_value);
306 
307  // Write top to the pointer
308  pointer_value->write(
310  ns,
311  std::stack<exprt>(),
312  nil_exprt(),
314  called_arg.type().subtype(), ns, true, false),
315  false);
316  }
317  }
318 
319  // Top any global values
320  for(const auto &symbol : ns.get_symbol_table().symbols)
321  {
322  if(symbol.second.is_static_lifetime)
323  {
325  symbol_exprt(symbol.first, symbol.second.type),
327  symbol.second.type, ns, true, false),
328  ns);
329  }
330  }
331  }
332  }
333  else
334  {
335  // we have an actual call
336  const symbolt &symbol = ns.lookup(function_id);
337  const code_typet &code_type = to_code_type(symbol.type);
338  const code_typet::parameterst &declaration_parameters =
339  code_type.parameters();
340 
341  code_typet::parameterst::const_iterator parameter_it =
342  declaration_parameters.begin();
343 
344  for(const exprt &called_arg : called_arguments)
345  {
346  if(parameter_it == declaration_parameters.end())
347  {
348  INVARIANT(
349  code_type.has_ellipsis(), "Only case for insufficient args");
350  break;
351  }
352 
353  // Evaluate the expression that is being
354  // passed into the function call (called_arg)
355  abstract_object_pointert param_val =
356  abstract_state.eval(called_arg, ns)
357  ->update_location_context({from}, true);
358 
359  // Assign the evaluated value to the symbol associated with the
360  // parameter of the function
361  const symbol_exprt parameter_expr(
362  parameter_it->get_identifier(), called_arg.type());
363  abstract_state.assign(parameter_expr, param_val, ns);
364 
365  ++parameter_it;
366  }
367 
368  // Too few arguments so invalid code
370  parameter_it == declaration_parameters.end(),
371  "Number of arguments should match parameters");
372  }
373  }
374  else
375  {
376  PRECONDITION(to == next);
377  abstract_state.havoc("unknown opaque function call");
378  }
379 }
380 
382  const irep_idt &function_id) const
383 {
384  static const std::set<irep_idt> ignored_internal_function = {
385  CPROVER_PREFIX "set_must",
386  CPROVER_PREFIX "get_must",
387  CPROVER_PREFIX "set_may",
388  CPROVER_PREFIX "get_may",
389  CPROVER_PREFIX "cleanup",
390  CPROVER_PREFIX "clear_may",
391  CPROVER_PREFIX "clear_must"};
392 
393  return ignored_internal_function.find(function_id) !=
394  ignored_internal_function.cend();
395 }
396 
398  const ai_domain_baset &function_call,
399  const ai_domain_baset &function_start,
400  const ai_domain_baset &function_end,
401  const namespacet &ns)
402 {
403  const variable_sensitivity_domaint &cast_function_call =
404  static_cast<const variable_sensitivity_domaint &>(function_call);
405 
406  const variable_sensitivity_domaint &cast_function_start =
407  static_cast<const variable_sensitivity_domaint &>(function_start);
408 
409  const variable_sensitivity_domaint &cast_function_end =
410  static_cast<const variable_sensitivity_domaint &>(function_end);
411 
412  const std::vector<irep_idt> &modified_symbol_names =
413  cast_function_start.get_modified_symbols(cast_function_end);
414 
415  std::vector<symbol_exprt> modified_symbols;
416  modified_symbols.reserve(modified_symbol_names.size());
417  std::transform(
418  modified_symbol_names.begin(),
419  modified_symbol_names.end(),
420  std::back_inserter(modified_symbols),
421  [&ns](const irep_idt &id) { return ns.lookup(id).symbol_expr(); });
422 
423  abstract_state = cast_function_call.abstract_state;
424  apply_domain(modified_symbols, cast_function_end, ns);
425 
426  return;
427 }
428 
430  std::vector<symbol_exprt> modified_symbols,
431  const variable_sensitivity_domaint &source,
432  const namespacet &ns)
433 {
434  for(const auto &symbol : modified_symbols)
435  {
436  abstract_object_pointert value = source.abstract_state.eval(symbol, ns);
437  abstract_state.assign(symbol, value, ns);
438  }
439 }
440 
441 #ifdef ENABLE_STATS
443 variable_sensitivity_domaint::gather_statistics(const namespacet &ns) const
444 {
446 }
447 #endif
sharing_ptrt< class abstract_objectt > abstract_object_pointert
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.
virtual bool merge(const abstract_environmentt &env)
Computes the join between "this" and "b".
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
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.
std::set< goto_programt::const_targett > locationst
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:59
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
goto_programt::const_targett locationt
Definition: ai_domain.h:77
A codet representing an assignment in the program.
Definition: std_code.h:295
exprt & rhs()
Definition: std_code.h:317
exprt & lhs()
Definition: std_code.h:312
codet representation of a function call statement.
Definition: std_code.h:1215
exprt & function()
Definition: std_code.h:1250
argumentst & arguments()
Definition: std_code.h:1260
exprt::operandst argumentst
Definition: std_code.h:1224
Base type of functions.
Definition: std_types.h:744
std::vector< parametert > parameterst
Definition: std_types.h:746
bool has_ellipsis() const
Definition: std_types.h:816
const parameterst & parameters() const
Definition: std_types.h:860
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
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:96
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:183
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:337
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:254
exprt guard
Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write.
Definition: goto_program.h:341
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:212
const irep_idt & id() const
Definition: irep.h:407
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:124
The NIL expression.
Definition: std_expr.h:2735
Boolean negation.
Definition: std_expr.h:2042
Expression to hold a symbol (variable)
Definition: std_expr.h:81
const irep_idt & get_identifier() const
Definition: std_expr.h:110
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.
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.
virtual bool merge(const variable_sensitivity_domaint &b, locationt from, locationt to)
Computes the join between "this" and "b".
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.
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:50
@ ATOMIC_END
Definition: goto_program.h:45
@ DEAD
Definition: goto_program.h:49
@ END_FUNCTION
Definition: goto_program.h:43
@ RETURN
Definition: goto_program.h:46
@ ASSIGN
Definition: goto_program.h:47
@ ASSERT
Definition: goto_program.h:37
@ ATOMIC_BEGIN
Definition: goto_program.h:44
@ CATCH
Definition: goto_program.h:52
@ END_THREAD
Definition: goto_program.h:41
@ SKIP
Definition: goto_program.h:39
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:34
@ START_THREAD
Definition: goto_program.h:40
@ THROW
Definition: goto_program.h:51
@ DECL
Definition: goto_program.h:48
@ OTHER
Definition: goto_program.h:38
@ GOTO
Definition: goto_program.h:35
@ INCOMPLETE_GOTO
Definition: goto_program.h:53
@ ASSUME
Definition: goto_program.h:36
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
There are different ways of handling arrays, structures, unions and pointers.