CBMC
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 <util/expr_util.h>
18 #include <util/message.h>
19 #include <util/namespace.h>
20 #include <util/symbol_table_base.h>
21 
23 
24 #include <algorithm>
25 #include <unordered_map>
26 #include <unordered_set>
27 
28 // forward declarations
30 class cfg_infot;
31 class goto_functionst;
32 
35 {
36 public:
37  conditional_target_exprt(const exprt &_condition, const exprt &_target)
38  : exprt(irep_idt{}, typet{}, {_condition, _target})
39  {
40  INVARIANT(
41  !has_subexpr(_condition, ID_side_effect),
42  "condition must have no side_effect sub-expression");
43  add_source_location() = _target.source_location();
44  }
45 
47  const exprt &condition() const
48  {
49  return operands()[0];
50  }
51 
53  const exprt &target() const
54  {
55  return operands()[1];
56  }
57 };
58 
61 {
65 };
66 
73 class car_exprt : public exprt
74 {
75 public:
77  const exprt &_condition,
78  const exprt &_target,
79  const exprt &_target_start_address,
80  const exprt &_target_size,
81  const symbol_exprt &_validity_var,
82  const symbol_exprt &_lower_bound_var,
83  const symbol_exprt &_upper_bound_var,
84  const car_havoc_methodt _havoc_method)
85  : exprt(
86  irep_idt{},
87  typet{},
88  {_condition,
89  _target,
90  _target_start_address,
91  _target_size,
92  _validity_var,
93  _lower_bound_var,
94  _upper_bound_var}),
95  havoc_method(_havoc_method)
96  {
97  add_source_location() = _target.source_location();
98  }
99 
102 
104  const exprt &condition() const
105  {
106  return operands()[0];
107  }
108 
110  const exprt &target() const
111  {
112  return operands()[1];
113  }
114 
117  {
118  return operands()[2];
119  }
120 
122  const exprt &target_size() const
123  {
124  return operands()[3];
125  }
126 
128  const symbol_exprt &valid_var() const
129  {
130  return to_symbol_expr(operands()[4]);
131  }
132 
135  {
136  return to_symbol_expr(operands()[5]);
137  }
138 
141  {
142  return to_symbol_expr(operands()[6]);
143  }
144 };
145 
149 
153 
158 // "unsigned-overflow-check", "conversion-check".
160 
163 
170 
177 
187 {
188 public:
197  const irep_idt &_function_id,
198  const goto_functionst &_functions,
199  cfg_infot &_cfg_info,
200  symbol_table_baset &_st,
201  message_handlert &_message_handler)
202  : function_id(_function_id),
203  functions(_functions),
204  cfg_info(_cfg_info),
205  st(_st),
206  ns(_st),
207  log(_message_handler),
208  mode(st.lookup_ref(function_id).mode)
209  {
210  }
211 
214  void track_spec_target(const exprt &expr, goto_programt &dest);
215 
217  void
218  track_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest);
219 
221  bool stack_allocated_is_tracked(const symbol_exprt &symbol_expr) const;
222 
226  const symbol_exprt &symbol_expr,
227  goto_programt &dest);
228 
231  void track_heap_allocated(const exprt &expr, goto_programt &dest);
232 
240 
252  goto_programt &dest);
253 
254 protected:
262  {
263  public:
266  {
267  min_line = std::numeric_limits<std::size_t>::max();
268  min_col = std::numeric_limits<std::size_t>::max();
269  max_line = std::numeric_limits<std::size_t>::min();
270  max_col = std::numeric_limits<std::size_t>::min();
271  }
272 
275  void anywhere()
276  {
277  min_line = std::numeric_limits<std::size_t>::min();
278  min_col = std::numeric_limits<std::size_t>::min();
279  max_line = std::numeric_limits<std::size_t>::max();
280  max_col = std::numeric_limits<std::size_t>::max();
281  }
282 
284  void update(const source_locationt &source_location)
285  {
286  PRECONDITION(source_location.is_not_nil());
287  // use pessimistic lowest value to update min for undefined
288  update_min(
290  source_location, std::numeric_limits<std::size_t>::min()),
292  source_location, std::numeric_limits<std::size_t>::min()));
293 
294  // use pessimistic highest value to update max for undefined
295  update_max(
297  source_location, std::numeric_limits<std::size_t>::max()),
299  source_location, std::numeric_limits<std::size_t>::max()));
300  }
301 
303  bool contains(const source_locationt &source_location)
304  {
305  if(source_location.is_not_nil())
306  {
307  return
308  // use pessimistic highest value to compare to min for undefined
309  is_lte(
310  min_line,
311  min_col,
313  source_location, std::numeric_limits<std::size_t>::max()),
315  source_location, std::numeric_limits<std::size_t>::max())) &&
316  // use pessimistic lowest value to compare to max for undefined
317  is_lte(
319  source_location, std::numeric_limits<std::size_t>::min()),
321  source_location, std::numeric_limits<std::size_t>::min()),
322  max_line,
323  max_col);
324  }
325  else
326  {
327  return true;
328  }
329  }
330 
331  private:
333  std::size_t col_to_size_t(
334  const source_locationt &source_location,
335  std::size_t default_value)
336  {
337  if(
338  source_location.get_line().empty() ||
339  source_location.get_column().empty())
340  {
341  return default_value;
342  }
343  else
344  {
345  std::stringstream stream(id2string(source_location.get_column()));
346  size_t res;
347  stream >> res;
348  return res;
349  }
350  }
351 
353  std::size_t line_to_size_t(
354  const source_locationt &source_location,
355  std::size_t default_value)
356  {
357  if(source_location.get_line().empty())
358  {
359  return default_value;
360  }
361  else
362  {
363  std::stringstream stream(id2string(source_location.get_line()));
364  size_t res;
365  stream >> res;
366  return res;
367  }
368  }
369 
371  static bool is_lte(size_t line0, size_t col0, size_t line1, size_t col1)
372  {
373  return (line0 < line1) || ((line0 == line1) && (col0 <= col1));
374  }
375 
378  void update_min(size_t line, size_t col)
379  {
380  if(is_lte(line, col, min_line, min_col))
381  {
382  min_line = line;
383  min_col = col;
384  }
385  }
386 
389  void update_max(size_t line, size_t col)
390  {
391  if(is_lte(max_line, max_col, line, col))
392  {
393  max_line = line;
394  max_col = col;
395  }
396  }
397 
398  std::size_t min_line;
399  std::size_t min_col;
400  std::size_t max_line;
401  std::size_t max_col;
402  };
403 
405  typedef std::unordered_map<irep_idt, location_intervalt> covered_locationst;
406  typedef std::unordered_set<symbol_exprt, irep_hash> propagated_static_localst;
407 
416  const irep_idt ambient_function_id,
419  covered_locationst &covered_locations,
420  propagated_static_localst &propagated) const;
421 
425  covered_locationst &covered_locations,
426  std::unordered_set<symbol_exprt, irep_hash> &dest);
427 
428 public:
433  void check_inclusion_assignment(const exprt &lhs, goto_programt &dest) const;
434 
439  const exprt &expr,
440  goto_programt &dest);
441 
453  goto_programt &body,
454  goto_programt::targett instruction_it,
455  const goto_programt::targett &instruction_end,
456  const std::function<bool(const goto_programt::targett &)> &pred = {});
457 
461  template <typename C>
462  void get_static_locals(std::insert_iterator<C> inserter) const
463  {
465  from_static_local.cbegin(),
466  from_static_local.cend(),
467  inserter,
468  // can use `const auto &` below once we switch to C++14
469  [](const symbol_exprt_to_car_mapt::value_type &s) { return s.first; });
470  }
471 
472 protected:
475 
478 
481 
484 
486  const namespacet ns;
487 
490 
492  const irep_idt &mode;
493 
497  const conditional_target_group_exprt &group,
498  goto_programt &dest);
499 
502  void track_plain_spec_target(const exprt &expr, goto_programt &dest);
503 
505  void create_snapshot(const car_exprt &car, goto_programt &dest) const;
506 
508  exprt
509  target_validity_expr(const car_exprt &car, bool allow_null_target) const;
510 
516  const car_exprt &car,
517  bool allow_null_target,
518  goto_programt &dest) const;
519 
522  const car_exprt &lhs,
523  const car_exprt &candidate_car) const;
524 
531  const car_exprt &lhs,
532  bool allow_null_lhs,
533  bool include_stack_allocated) const;
534 
542  const car_exprt &lhs,
543  bool allow_null_lhs,
544  bool include_stack_allocated,
545  goto_programt &dest) const;
546 
549  void invalidate_car(
550  const car_exprt &tracked_car,
551  const car_exprt &freed_car,
552  goto_programt &result) const;
553 
558  const car_exprt &freed_car,
559  goto_programt &dest) const;
560 
563  bool must_track_decl(const goto_programt::const_targett &target) const;
564 
567  bool must_track_dead(const goto_programt::const_targett &target) const;
568 
578  bool must_track_decl_or_dead(const irep_idt &ident) const;
579 
582 
587  goto_programt::targett &instruction_it,
588  goto_programt &body) const;
589 
594  goto_programt::targett &instruction_it,
595  goto_programt &body);
596 
598  unordered_map<const conditional_target_exprt, const car_exprt, irep_hash>;
599 
603 
604  const car_exprt &
605  create_car_from_spec_assigns(const exprt &condition, const exprt &target);
606 
608  std::unordered_map<const symbol_exprt, const car_exprt, irep_hash>;
609 
612 
613  const car_exprt &create_car_from_stack_alloc(const symbol_exprt &target);
614 
616  std::unordered_map<const exprt, const car_exprt, irep_hash>;
617 
619  using car_expr_listt = std::list<car_exprt>;
621 
622  const car_exprt &create_car_from_heap_alloc(const exprt &target);
623 
627 
629 
632  car_exprt create_car_expr(const exprt &condition, const exprt &target) const;
633 };
634 
635 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_INSTRUMENT_SPEC_ASSIGNS_H
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
Class that represents a normalized conditional address range, with:
const car_havoc_methodt havoc_method
Method to use to havod the target.
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.
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 car_havoc_methodt _havoc_method)
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_start_address() const
Start address of the target.
Stores information about a goto function computed from its CFG.
Definition: cfg_info.h:40
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:233
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
Base class for all expressions.
Definition: expr.h:56
source_locationt & add_source_location()
Definition: expr.h:236
operandst & operands()
Definition: expr.h:94
A collection of goto functions.
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
Represents an interval of source locations covered by the static local variable search.
bool contains(const source_locationt &source_location)
True iff the interval contains the given location.
void anywhere()
Grows the interval cover the maximum range [(size_t::min, size_t::min), (size_t::min,...
void update_min(size_t line, size_t col)
Updates the min_line and min_col in place using the given values iff they are smaller.
location_intervalt()
Initializes to the empty interval.
static bool is_lte(size_t line0, size_t col0, size_t line1, size_t col1)
True iff (line0, col0) <= (line1, col1) in lexicographic ordering.
std::size_t col_to_size_t(const source_locationt &source_location, std::size_t default_value)
If line or col is missing use default.
void update(const source_locationt &source_location)
Grows the interval to include the given (line, col) location.
std::size_t line_to_size_t(const source_locationt &source_location, std::size_t default_value)
If line is missing use default.
void update_max(size_t line, size_t col)
Updates the max_line and max_col in place using the given values iff they are larger.
A class that generates instrumentation for assigns clause checking.
bool must_track_dead(const goto_programt::const_targett &target) const
Returns true iff a DEAD x must be processed to update the write set.
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.
std::unordered_set< symbol_exprt, irep_hash > propagated_static_localst
const goto_functionst & functions
Other functions of the model.
void collect_static_symbols(covered_locationst &covered_locations, std::unordered_set< symbol_exprt, irep_hash > &dest)
Collects static symbols from the symbol table that have a source location included in one of the cove...
void track_spec_target(const exprt &expr, goto_programt &dest)
Track an assigns clause target and generate snaphsot instructions and well-definedness assertions in ...
bool must_check_assign(const goto_programt::const_targett &target)
Returns true iff an ASSIGN lhs := rhs instruction must be instrumented.
symbol_exprt_to_car_mapt from_stack_alloc
Map from DECL symbols to corresponding conditional address ranges.
void inclusion_check_assertion(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, goto_programt &dest) const
Returns an inclusion check assertion of lhs over all tracked cars.
void track_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest)
Track a stack-allocated object and generate snaphsot instructions in dest.
cond_target_exprt_to_car_mapt from_spec_assigns
Map from conditional target expressions of assigns clauses to corresponding conditional address range...
void instrument_assign_statement(goto_programt::targett &instruction_it, goto_programt &body) const
Inserts an assertion in body immediately before the assignment at instruction_it, to ensure that the ...
const car_exprt & create_car_from_static_local(const symbol_exprt &target)
void track_heap_allocated(const exprt &expr, goto_programt &dest)
Track a whole heap-alloc object and generate snaphsot instructions in dest.
symbol_table_baset & st
Program symbol table.
std::unordered_map< const symbol_exprt, const car_exprt, irep_hash > symbol_exprt_to_car_mapt
symbol_exprt_to_car_mapt from_static_local
Map to from detected or propagated static local symbols to corresponding conditional address ranges.
const car_exprt & create_car_from_spec_assigns(const exprt &condition, const exprt &target)
const irep_idt & mode
Language mode.
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 ...
std::list< car_exprt > car_expr_listt
List of malloc'd 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...
bool must_track_decl_or_dead(const irep_idt &ident) const
Returns true iff a function-local symbol must be tracked.
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.
void track_static_locals(goto_programt &dest)
Searches the goto instructions reachable from the start to the end of the instrumented function's ins...
void instrument_call_statement(goto_programt::targett &instruction_it, goto_programt &body)
Inserts an assertion in body immediately before the function call at instruction_it,...
void instrument_instructions(goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, const std::function< bool(const goto_programt::targett &)> &pred={})
Instruments a sequence of instructions with inclusion checks.
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...
void check_inclusion_heap_allocated_and_invalidate_aliases(const exprt &expr, goto_programt &dest)
Generates inclusion check instructions for an argument passed to free.
std::unordered_map< const exprt, const car_exprt, irep_hash > exprt_to_car_mapt
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,...
instrument_spec_assignst(const irep_idt &_function_id, const goto_functionst &_functions, cfg_infot &_cfg_info, symbol_table_baset &_st, message_handlert &_message_handler)
Class constructor.
void traverse_instructions(const irep_idt ambient_function_id, goto_programt::const_targett it, const goto_programt::const_targett end, covered_locationst &covered_locations, propagated_static_localst &propagated) const
Traverses the given list of instructions, updating the given coverage map, recursing into function ca...
void track_static_locals_between(goto_programt::const_targett it, const goto_programt::const_targett end, goto_programt &dest)
Searches the goto instructions reachable between the given it and end target instructions to identify...
bool must_track_decl(const goto_programt::const_targett &target) const
Returns true iff a DECL x must be explicitly added to the write set.
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
exprt inclusion_check_full(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated) const
Returns an inclusion check expression of lhs over all tracked cars.
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 check_inclusion_assignment(const exprt &lhs, goto_programt &dest) const
Generates inclusion check instructions for an assignment, havoc or havoc_object instruction.
cfg_infot & cfg_info
CFG information for simplification.
void create_snapshot(const car_exprt &car, goto_programt &dest) const
Returns snapshot instructions for a car_exprt.
const irep_idt & function_id
Name of the instrumented function.
bool stack_allocated_is_tracked(const symbol_exprt &symbol_expr) const
Returns true if the expression is tracked.
std::unordered_map< irep_idt, location_intervalt > covered_locationst
Map type from function identifiers to covered locations.
void get_static_locals(std::insert_iterator< C > inserter) const
Inserts the detected static local symbols into a target container.
bool is_not_nil() const
Definition: irep.h:372
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
const irep_idt & get_column() const
const irep_idt & get_line() const
Expression to hold a symbol (variable)
Definition: std_expr.h:131
The symbol table base class interface.
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:115
Deprecated expression utility functions.
Concrete Goto Program.
void add_pragma_disable_pointer_checks(source_locationt &source_location)
Adds a pragma on a source location disable all pointer checks.
bool has_propagate_static_local_pragma(source_locationt &source_location)
True iff the pragma to mark assignments to static local variables that need to be propagated upwards ...
void add_pragma_disable_assigns_check(source_locationt &source_location)
Adds a pragma on a source_locationt to disable inclusion checking.
car_havoc_methodt
method to use to havoc a target
void add_propagate_static_local_pragma(source_locationt &source_location)
Sets a pragma to mark assignments to static local variables that need to be propagated upwards in the...
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
Author: Diffblue Ltd.