cprover
instrument_spec_assigns.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Instrument assigns clauses in code contracts.
4 
5 Author: Remi Delmas
6 
7 Date: 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
30 class namespacet;
31 class symbol_tablet;
32 class symbolt;
33 
36 {
37 public:
38  conditional_target_exprt(const exprt &_condition, const exprt &_target)
39  : exprt(irep_idt{}, typet{}, {_condition, _target})
40  {
41  INVARIANT(
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 
66 class car_exprt : public exprt
67 {
68 public:
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 {
144 public:
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 
219 protected:
222 
225 
228 
230  const namespacet ns;
231 
234 
238  const conditional_target_group_exprt &group,
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 
331  const car_exprt &create_car_from_stack_alloc(const symbol_exprt &target);
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 exprt & target_size() const
Size of the target in bytes.
const symbol_exprt & upper_bound_var() const
Identifier of the upper address bound snapshot variable.
const exprt & condition() const
Condition expression. When this condition holds the target is allowed.
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.
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 & target_start_address() const
Start address of the target.
Class that represents a single conditional target.
const exprt & target() const
Target expression.
conditional_target_exprt(const exprt &_condition, const exprt &_target)
const exprt & condition() const
Condition expression.
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
source_locationt & add_source_location()
Definition: expr.h:235
operandst & operands()
Definition: expr.h:92
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
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.
Definition: symbol_table.h:14
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
Definition: expr_util.cpp:138
Concrete Goto Program.
nonstd::optional< T > optionalt
Definition: optional.h:35
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189