cprover
Loading...
Searching...
No Matches
variable_sensitivity_domain.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Abstract Interpretation
4
5Author: Martin Brain
6
7Date: 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
25 const irep_idt &function_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 {
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
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
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>{};
200 std::transform(
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
213
218
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{
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 {
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
274
276{
277 return abstract_state.is_top();
278}
279
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
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 {
331
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);
366 code_type.parameters();
367
368 code_typet::parameterst::const_iterator parameter_it =
370
371 for(const exprt &called_arg : called_arguments)
372 {
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)
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
388 parameter_it->get_identifier(), called_arg.type());
390
391 ++parameter_it;
392 }
393
394 // Too few arguments so invalid code
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) !=
421}
422
424 const ai_domain_baset &function_call,
427 const namespacet &ns)
428{
430 static_cast<const variable_sensitivity_domaint &>(function_call);
431
433 static_cast<const variable_sensitivity_domaint &>(function_start);
434
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());
443 std::transform(
444 modified_symbol_names.begin(),
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
475variable_sensitivity_domaint::gather_statistics(const namespacet &ns) const
476{
478}
479#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.
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Boolean AND.
Definition std_expr.h:1974
Base type of functions.
Definition std_types.h:539
std::vector< parametert > parameterst
Definition std_types.h:542
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.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
exprt guard
Guard for gotos, assume, assert Use condition() method to access.
goto_program_instruction_typet type() const
What kind of instruction?
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().
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
@ ATOMIC_END
@ DEAD
@ LOCATION
@ END_FUNCTION
@ ASSIGN
@ ASSERT
@ SET_RETURN_VALUE
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ THROW
@ DECL
@ OTHER
@ GOTO
@ INCOMPLETE_GOTO
@ ASSUME
#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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
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.