cprover
Loading...
Searching...
No Matches
instrument_spec_assigns.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Instrument assigns clauses in code contracts.
4
5Author: Remi Delmas
6
7Date: January 2022
8
9\*******************************************************************/
10
13
14#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_INSTRUMENT_SPEC_ASSIGNS_H
15#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_INSTRUMENT_SPEC_ASSIGNS_H
16
17#include <optional>
18#include <unordered_map>
19#include <unordered_set>
20
21#include <ansi-c/c_expr.h>
22
24#include <util/message.h>
25
26#include "utils.h"
27
28// forward declarations
30class namespacet;
31class symbol_tablet;
32class symbolt;
33
36{
37public:
38 conditional_target_exprt(const exprt &_condition, const exprt &_target)
39 : exprt(irep_idt{}, typet{}, {_condition, _target})
40 {
42 !has_subexpr(_condition, ID_side_effect),
43 "condition must have no side_effect sub-expression");
44 add_source_location() = _target.source_location();
45 }
46
48 const exprt &condition() const
49 {
50 return operands()[0];
51 }
52
54 const exprt &target() const
55 {
56 return operands()[1];
57 }
58};
59
66class car_exprt : public exprt
67{
68public:
70 const exprt &_condition,
71 const exprt &_target,
72 const exprt &_target_start_address,
73 const exprt &_target_size,
74 const symbol_exprt &_validity_var,
75 const symbol_exprt &_lower_bound_var,
76 const symbol_exprt &_upper_bound_var)
77 : exprt(
78 irep_idt{},
79 typet{},
80 {_condition,
81 _target,
82 _target_start_address,
83 _target_size,
84 _validity_var,
85 _lower_bound_var,
86 _upper_bound_var})
87 {
88 add_source_location() = _target.source_location();
89 }
90
92 const exprt &condition() const
93 {
94 return operands()[0];
95 }
96
98 const exprt &target() const
99 {
100 return operands()[1];
101 }
102
105 {
106 return operands()[2];
107 }
108
110 const exprt &target_size() const
111 {
112 return operands()[3];
113 }
114
116 const symbol_exprt &valid_var() const
117 {
118 return to_symbol_expr(operands()[4]);
119 }
120
123 {
124 return to_symbol_expr(operands()[5]);
125 }
126
129 {
130 return to_symbol_expr(operands()[6]);
131 }
132};
133
143{
144public:
152 const irep_idt &_function_id,
153 const goto_functionst &_functions,
154 symbol_tablet &_st,
155 message_handlert &_message_handler)
156 : function_id(_function_id),
157 functions(_functions),
158 st(_st),
159 ns(_st),
160 log(_message_handler)
161 {
162 }
163
166 void track_spec_target(const exprt &expr, goto_programt &dest);
167
169 void
170 track_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest);
171
173 bool stack_allocated_is_tracked(const symbol_exprt &symbol_expr) const;
174
178 const symbol_exprt &symbol_expr,
179 goto_programt &dest);
180
183 void track_heap_allocated(const exprt &expr, goto_programt &dest);
184
191
202 const exprt &lhs,
203 optionalt<cfg_infot> &cfg_info_opt,
204 goto_programt &dest);
205
215 const exprt &expr,
216 optionalt<cfg_infot> &cfg_info_opt,
217 goto_programt &dest);
218
219protected:
222
225
228
231
234
239 goto_programt &dest);
240
243 void track_plain_spec_target(const exprt &expr, goto_programt &dest);
244
248 const std::string &suffix,
249 const typet &type,
250 const source_locationt &location) const;
251
253 void create_snapshot(const car_exprt &car, goto_programt &dest) const;
254
256 exprt
257 target_validity_expr(const car_exprt &car, bool allow_null_target) const;
258
264 const car_exprt &car,
265 bool allow_null_target,
266 goto_programt &dest) const;
267
270 const car_exprt &lhs,
271 const car_exprt &candidate_car) const;
272
281 const car_exprt &lhs,
282 bool allow_null_lhs,
283 bool include_stack_allocated,
284 optionalt<cfg_infot> &cfg_info_opt) const;
285
295 const car_exprt &lhs,
296 bool allow_null_lhs,
297 bool include_stack_allocated,
298 optionalt<cfg_infot> &cfg_info_opt,
299 goto_programt &dest) const;
300
303 void invalidate_car(
304 const car_exprt &tracked_car,
305 const car_exprt &freed_car,
306 goto_programt &result) const;
307
312 const car_exprt &freed_car,
313 goto_programt &dest) const;
314
316 unordered_map<const conditional_target_exprt, const car_exprt, irep_hash>;
317
321
322 const car_exprt &
323 create_car_from_spec_assigns(const exprt &condition, const exprt &target);
324
326 std::unordered_map<const symbol_exprt, const car_exprt, irep_hash>;
327
330
332
334 std::unordered_map<const exprt, const car_exprt, irep_hash>;
335
338
339 const car_exprt &create_car_from_heap_alloc(const exprt &target);
340
343 car_exprt create_car_expr(const exprt &condition, const exprt &target) const;
344};
345
346#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_INSTRUMENT_SPEC_ASSIGNS_H
API to expression classes that are internal to the C frontend.
Class that represents a normalized conditional address range, with:
const symbol_exprt & upper_bound_var() const
Identifier of the upper address bound snapshot variable.
const exprt & target_start_address() const
Start address of the target.
const symbol_exprt & valid_var() const
Identifier of the validity snapshot variable.
const exprt & target() const
The target expression.
const symbol_exprt & lower_bound_var() const
Identifier of the lower address bound snapshot variable.
const exprt & target_size() const
Size of the target in bytes.
car_exprt(const exprt &_condition, const exprt &_target, const exprt &_target_start_address, const exprt &_target_size, const symbol_exprt &_validity_var, const symbol_exprt &_lower_bound_var, const symbol_exprt &_upper_bound_var)
const exprt & condition() const
Condition expression. When this condition holds the target is allowed.
Class that represents a single conditional target.
const exprt & condition() const
Condition expression.
const exprt & target() const
Target expression.
conditional_target_exprt(const exprt &_condition, const exprt &_target)
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition c_expr.h:232
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
operandst & operands()
Definition expr.h:92
source_locationt & add_source_location()
Definition expr.h:235
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
A class that generates instrumentation for assigns clause checking.
void invalidate_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest)
Generate instructions to invalidate a stack-allocated object that goes DEAD in dest.
const goto_functionst & functions
Other functions of the model.
instrument_spec_assignst(const irep_idt &_function_id, const goto_functionst &_functions, symbol_tablet &_st, message_handlert &_message_handler)
Class constructor.
void track_spec_target(const exprt &expr, goto_programt &dest)
Track an assigns clause target and generate snaphsot instructions and well-definedness assertions in ...
symbol_exprt_to_car_mapt from_stack_alloc
Map to from DECL symbols to corresponding conditional address ranges.
void track_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest)
Track a stack-allocated object and generate snaphsot instructions in dest.
void inclusion_check_assertion(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest) const
Returns an inclusion check assertion of lhs over all tracked cars.
cond_target_exprt_to_car_mapt from_spec_assigns
Map to from conditional target expressions of assigns clauses to corresponding conditional address ra...
void track_heap_allocated(const exprt &expr, goto_programt &dest)
Track a whole heap-alloc object and generate snaphsot instructions in dest.
std::unordered_map< const symbol_exprt, const car_exprt, irep_hash > symbol_exprt_to_car_mapt
const car_exprt & create_car_from_spec_assigns(const exprt &condition, const exprt &target)
void invalidate_car(const car_exprt &tracked_car, const car_exprt &freed_car, goto_programt &result) const
Adds an assignment in dest to invalidate the tracked car if was valid before and was pointing to the ...
exprt_to_car_mapt from_heap_alloc
Map to from malloc'd symbols to corresponding conditional address ranges.
car_exprt create_car_expr(const exprt &condition, const exprt &target) const
Creates a conditional address range expression from a cleaned-up condition and target expression.
void track_spec_target_group(const conditional_target_group_exprt &group, goto_programt &dest)
Track and generate snaphsot instructions and target validity checking assertions for a conditional ta...
void target_validity_assertion(const car_exprt &car, bool allow_null_target, goto_programt &dest) const
Generates the target validity assertion for the given car and adds it to dest.
exprt inclusion_check_full(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, optionalt< cfg_infot > &cfg_info_opt) const
Returns an inclusion check expression of lhs over all tracked cars.
void track_static_locals(goto_programt &dest)
Search the call graph reachable from the instrumented function to identify local static variables use...
void track_plain_spec_target(const exprt &expr, goto_programt &dest)
Track and generate snaphsot instructions and target validity checking assertions for a conditional ta...
std::unordered_map< const exprt, const car_exprt, irep_hash > exprt_to_car_mapt
const symbolt create_fresh_symbol(const std::string &suffix, const typet &type, const source_locationt &location) const
Creates a fresh symbolt with given suffix, scoped to function_id.
void invalidate_heap_and_spec_aliases(const car_exprt &freed_car, goto_programt &dest) const
Generates instructions to invalidate all targets aliased with a car that was passed to free,...
const car_exprt & create_car_from_stack_alloc(const symbol_exprt &target)
std::unordered_map< const conditional_target_exprt, const car_exprt, irep_hash > cond_target_exprt_to_car_mapt
const car_exprt & create_car_from_heap_alloc(const exprt &target)
exprt inclusion_check_single(const car_exprt &lhs, const car_exprt &candidate_car) const
Returns inclusion check expression for a single candidate location.
const namespacet ns
Program namespace.
exprt target_validity_expr(const car_exprt &car, bool allow_null_target) const
Returns the target validity expression for a car_exprt.
void create_snapshot(const car_exprt &car, goto_programt &dest) const
Returns snapshot instructions for a car_exprt.
symbol_tablet & st
Program symbol table.
const irep_idt & function_id
Name of the instrumented function.
void check_inclusion_assignment(const exprt &lhs, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest)
Generates inclusion check instructions for an assignment, havoc or havoc_object instruction.
bool stack_allocated_is_tracked(const symbol_exprt &symbol_expr) const
Returns true if the expression is tracked.
void check_inclusion_heap_allocated_and_invalidate_aliases(const exprt &expr, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest)
Generates inclusion check instructions for an argument passed to free.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Expression to hold a symbol (variable)
Definition std_expr.h:80
The symbol table.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Concrete Goto Program.
nonstd::optional< T > optionalt
Definition optional.h:35
#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