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  {
76  if(flow_sensitivity == flow_sensitivityt::sensitive)
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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_typet::has_ellipsis
bool has_ellipsis() const
Definition: std_types.h:816
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:746
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:337
variable_sensitivity_domaint::is_bottom
bool is_bottom() const override
Find out if the domain is currently unreachable.
Definition: variable_sensitivity_domain.cpp:242
variable_sensitivity_domaint::merge
virtual bool merge(const variable_sensitivity_domaint &b, locationt from, locationt to)
Computes the join between "this" and "b".
Definition: variable_sensitivity_domain.cpp:198
variable_sensitivity_domaint::ignore_function_call_transform
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...
Definition: variable_sensitivity_domain.cpp:381
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
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
goto_programt::instructiont::decl_symbol
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:212
ai_domain_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:78
variable_sensitivity_domaint::get_modified_symbols
std::vector< irep_idt > get_modified_symbols(const variable_sensitivity_domaint &other) const
Get symbols that have been modified since this domain and other.
Definition: variable_sensitivity_domain.cpp:252
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
variable_sensitivity_domaint::make_bottom
void make_bottom() override
Sets the domain to bottom (no states / unreachable).
Definition: variable_sensitivity_domain.cpp:182
THROW
@ THROW
Definition: goto_program.h:51
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
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
GOTO
@ GOTO
Definition: goto_program.h:35
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
abstract_object_statisticst
Definition: abstract_object_statistics.h:19
goto_programt::instructiont::dead_symbol
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:254
variable_sensitivity_domaint::apply_domain
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.
Definition: variable_sensitivity_domain.cpp:429
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:183
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
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
variable_sensitivity_domaint::merge_three_way_function_return
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...
Definition: variable_sensitivity_domain.cpp:397
variable_sensitivity_domaint::abstract_state
abstract_environmentt abstract_state
Definition: variable_sensitivity_domain.h:216
abstract_objectt::locationst
std::set< goto_programt::const_targett > locationst
Definition: abstract_object.h:215
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:34
variable_sensitivity_domaint::transform
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.
Definition: variable_sensitivity_domain.cpp:24
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
code_typet
Base type of functions.
Definition: std_types.h:744
OTHER
@ OTHER
Definition: goto_program.h:38
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
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1224
variable_sensitivity_domaint::is_top
bool is_top() const override
Is the domain completely top at this state.
Definition: variable_sensitivity_domain.cpp:247
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:43
SKIP
@ SKIP
Definition: goto_program.h:39
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:860
cprover_prefix.h
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
variable_sensitivity_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Basic text output of the abstract domain.
Definition: variable_sensitivity_domain.cpp:174
simplify_expr.h
RETURN
@ RETURN
Definition: goto_program.h:46
ASSIGN
@ ASSIGN
Definition: goto_program.h:47
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:77
variable_sensitivity_domaint::ai_simplify
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.
Definition: variable_sensitivity_domain.cpp:215
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::merge
virtual bool merge(const abstract_environmentt &env)
Computes the join between "this" and "b".
Definition: abstract_environment.cpp:288
CATCH
@ CATCH
Definition: goto_program.h:52
DECL
@ DECL
Definition: goto_program.h:48
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
symbolt
Symbol table entry.
Definition: symbol.h:28
ASSUME
@ ASSUME
Definition: goto_program.h:36
variable_sensitivity_domain.h
There are different ways of handling arrays, structures, unions and pointers.
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
goto_programt::instructiont::guard
exprt guard
Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write.
Definition: goto_program.h:341
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
variable_sensitivity_domaint
Definition: variable_sensitivity_domain.h:76
variable_sensitivity_domaint::make_entry
void make_entry() override
Set up a reasonable entry-point state.
Definition: variable_sensitivity_domain.cpp:193
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
START_THREAD
@ START_THREAD
Definition: goto_program.h:40
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:50
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
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:45
DEAD
@ DEAD
Definition: goto_program.h:49
exprt::operands
operandst & operands()
Definition: expr.h:96
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:44
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
message.h
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:59
LOCATION
@ LOCATION
Definition: goto_program.h:42
variable_sensitivity_domaint::make_top
void make_top() override
Sets the domain to top (all states).
Definition: variable_sensitivity_domain.cpp:188
ASSERT
@ ASSERT
Definition: goto_program.h:37
variable_sensitivity_domaint::flow_sensitivity
flow_sensitivityt flow_sensitivity
Definition: variable_sensitivity_domain.h:217
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
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
END_THREAD
@ END_THREAD
Definition: goto_program.h:41
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:53
abstract_environmentt::erase
void erase(const symbol_exprt &expr)
Delete a symbol from the map.
Definition: abstract_environment.cpp:398
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
variable_sensitivity_domaint::transform_function_call
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.
Definition: variable_sensitivity_domain.cpp:259
not_exprt
Boolean negation.
Definition: std_expr.h:2042
abstract_environmentt::assume
virtual bool assume(const exprt &expr, const namespacet &ns)
Reduces the domain based on a condition.
Definition: abstract_environment.cpp:203