cprover
instrument_spec_assigns.cpp
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 
15 
16 #include <util/arith_tools.h>
17 #include <util/c_types.h>
18 #include <util/expr_util.h>
19 #include <util/format_expr.h>
22 #include <util/simplify_expr.h>
23 
24 #include <analyses/call_graph.h>
25 
26 #include <langapi/language_util.h>
27 
28 #include "utils.h"
29 
31 
33  const exprt &expr,
34  goto_programt &dest)
35 {
36  if(auto target = expr_try_dynamic_cast<conditional_target_group_exprt>(expr))
37  track_spec_target_group(*target, dest);
38  else
39  track_plain_spec_target(expr, dest);
40 }
41 
43  const symbol_exprt &symbol_expr,
44  goto_programt &dest)
45 {
46  create_snapshot(create_car_from_stack_alloc(symbol_expr), dest);
47 }
48 
50  const symbol_exprt &symbol_expr) const
51 {
52  return from_stack_alloc.find(symbol_expr) != from_stack_alloc.end();
53 }
54 
56  const symbol_exprt &symbol_expr,
57  goto_programt &dest)
58 {
59  // ensure it is tracked
61  stack_allocated_is_tracked(symbol_expr),
62  "symbol is not tracked :" + from_expr(ns, "", symbol_expr));
63 
64  const auto &car = from_stack_alloc.find(symbol_expr)->second;
65 
66  source_locationt source_location(symbol_expr.source_location());
67  add_pragma_disable_pointer_checks(source_location);
68  add_pragma_disable_assigns_check(source_location);
69 
71  car.valid_var(), false_exprt{}, source_location));
72 }
73 
75  const exprt &expr,
76  goto_programt &dest)
77 {
79 }
80 
82  const exprt &lhs,
83  optionalt<cfg_infot> &cfg_info_opt,
84  goto_programt &dest)
85 {
86  // create temporary car but do not track
87  const auto car = create_car_expr(true_exprt{}, lhs);
88  create_snapshot(car, dest);
89  inclusion_check_assertion(car, false, true, cfg_info_opt, dest);
90 }
91 
93 {
94  auto call_graph =
97 
98  for(const auto &sym_pair : st)
99  {
100  const auto &sym = sym_pair.second;
101  if(sym.is_static_lifetime)
102  {
103  auto fname = sym.location.get_function();
104  if(
105  !fname.empty() &&
106  (fname == function_id || call_graph.get_node_index(fname).has_value()))
107  {
108  // We found a symbol with
109  // - a static lifetime
110  // - non empty location function
111  // - this function appears in the call graph of the function
112 
113  // insert in tracking set and generate snapshot instructions
114  // for this target.
115  create_snapshot(create_car_from_stack_alloc(sym.symbol_expr()), dest);
116  }
117  }
118  }
119 }
120 
123  const exprt &expr,
124  optionalt<cfg_infot> &cfg_info_opt,
125  goto_programt &dest)
126 {
127  // create temporary car but do not track
128  const auto car = create_car_expr(true_exprt{}, expr);
129 
130  // generate snapshot instructions for this target.
131  create_snapshot(car, dest);
132 
133  // check inclusion, allowing null and not allowing stack allocated locals
134  inclusion_check_assertion(car, true, false, cfg_info_opt, dest);
135 
136  // invalidate aliases of the freed object
138 }
139 
141 
143  const conditional_target_group_exprt &group,
144  goto_programt &dest)
145 {
146  // clean up side effects from the guard expression if needed
147  cleanert cleaner(st, log.get_message_handler());
148  exprt condition(group.condition());
149  if(has_subexpr(condition, ID_side_effect))
150  cleaner.clean(condition, dest, st.lookup_ref(function_id).mode);
151 
152  // create conditional address ranges by distributing the condition
153  for(const auto &target : group.targets())
154  {
155  // insert in tracking set
156  const auto &car = create_car_from_spec_assigns(condition, target);
157 
158  // generate target validity check for this target.
159  target_validity_assertion(car, true, dest);
160 
161  // generate snapshot instructions for this target.
162  create_snapshot(car, dest);
163  }
164 }
165 
167  const exprt &expr,
168  goto_programt &dest)
169 {
170  // insert in tracking set
171  const auto &car = create_car_from_spec_assigns(true_exprt{}, expr);
172 
173  // generate target validity check for this target.
174  target_validity_assertion(car, true, dest);
175 
176  // generate snapshot instructions for this target.
177  create_snapshot(car, dest);
178 }
179 
181  const std::string &suffix,
182  const typet &type,
183  const source_locationt &location) const
184 {
185  return new_tmp_symbol(
186  type, location, st.lookup_ref(function_id).mode, st, suffix);
187 }
188 
190  const exprt &condition,
191  const exprt &target) const
192 {
193  const source_locationt &source_location = target.source_location();
194  const auto &valid_var =
195  create_fresh_symbol("__car_valid", bool_typet(), source_location)
196  .symbol_expr();
197 
198  const auto &lower_bound_var =
199  create_fresh_symbol("__car_lb", pointer_type(char_type()), source_location)
200  .symbol_expr();
201 
202  const auto &upper_bound_var =
203  create_fresh_symbol("__car_ub", pointer_type(char_type()), source_location)
204  .symbol_expr();
205 
206  if(target.id() == ID_pointer_object)
207  {
208  const auto &arg = to_unary_expr(target).op();
209  return {
210  condition,
211  target,
212  minus_exprt(
214  pointer_offset(arg)),
216  valid_var,
217  lower_bound_var,
218  upper_bound_var};
219  }
220  else if(is_assignable(target))
221  {
222  const auto &size = size_of_expr(target.type(), ns);
223 
224  INVARIANT(
225  size.has_value(),
226  "no definite size for lvalue target:\n" + target.pretty());
227 
228  return {condition,
229  target,
233  valid_var,
234  lower_bound_var,
235  upper_bound_var};
236  };
237 
238  UNREACHABLE;
239 }
240 
242  const car_exprt &car,
243  goto_programt &dest) const
244 {
245  source_locationt source_location(car.source_location());
246  add_pragma_disable_pointer_checks(source_location);
247  add_pragma_disable_assigns_check(source_location);
248 
249  dest.add(goto_programt::make_decl(car.valid_var(), source_location));
250 
252  car.valid_var(),
254  and_exprt{car.condition(),
256  ns),
257  source_location));
258 
259  dest.add(goto_programt::make_decl(car.lower_bound_var(), source_location));
260 
262  car.lower_bound_var(), car.target_start_address(), source_location));
263 
264  dest.add(goto_programt::make_decl(car.upper_bound_var(), source_location));
265 
267  car.upper_bound_var(),
270  source_location));
271 }
272 
274  const car_exprt &car,
275  bool allow_null_target) const
276 {
277  // If requested, we check that when guard condition is true,
278  // the target's `start_address` pointer satisfies w_ok with the expected size
279  // (or is NULL if we allow it explicitly).
280  // This assertion will be falsified whenever `start_address` is invalid or
281  // not of the right size (or is NULL if we dot not allow it expliclitly).
282  auto result =
285 
286  if(allow_null_target)
288 
289  return simplify_expr(result, ns);
290 }
291 
293  const car_exprt &car,
294  bool allow_null_target,
295  goto_programt &dest) const
296 {
297  // since assigns clauses are declared outside of their function body
298  // their source location might not have a function attribute
299  source_locationt source_location(car.source_location());
300  if(source_location.get_function().empty())
301  source_location.set_function(function_id);
302 
303  source_location.set_property_class("assigns");
304 
305  add_pragma_disable_pointer_checks(source_location);
306  add_pragma_disable_assigns_check(source_location);
307 
308  std::string comment = "Check that ";
309  comment += from_expr(ns, "", car.target());
310  comment += " is valid";
311  if(!car.condition().is_true())
312  {
313  comment += " when ";
314  comment += from_expr(ns, "", car.condition());
315  }
316 
317  source_location.set_comment(comment);
318 
320  target_validity_expr(car, allow_null_target), source_location));
321 }
322 
324  const car_exprt &car,
325  bool allow_null_lhs,
326  bool include_stack_allocated,
327  optionalt<cfg_infot> &cfg_info_opt,
328  goto_programt &dest) const
329 {
330  source_locationt source_location(car.source_location());
331 
332  // since assigns clauses are declared outside of their function body
333  // their source location might not have a function attribute
334  if(source_location.get_function().empty())
335  source_location.set_function(function_id);
336 
337  add_pragma_disable_pointer_checks(source_location);
338  add_pragma_disable_assigns_check(source_location);
339 
340  source_location.set_property_class("assigns");
341 
342  const auto &orig_comment = source_location.get_comment();
343  std::string comment = "Check that ";
345  {
346  if(!car.condition().is_true())
347  comment += from_expr(ns, "", car.condition()) + ": ";
348  comment += from_expr(ns, "", car.target());
349  }
350  else
351  comment += id2string(orig_comment);
352 
353  comment += " is assignable";
354  source_location.set_comment(comment);
355 
358  car, allow_null_lhs, include_stack_allocated, cfg_info_opt),
359  source_location));
360 }
361 
363  const car_exprt &car,
364  const car_exprt &candidate_car) const
365 {
366  // remark: both lb and ub are derived from the same object so checking
367  // same_object(upper_bound_address_var, lhs.upper_bound_address_var)
368  // is redundant
369  return simplify_expr(
370  and_exprt{
371  {candidate_car.valid_var(),
372  same_object(candidate_car.lower_bound_var(), car.lower_bound_var()),
373  less_than_or_equal_exprt{pointer_offset(candidate_car.lower_bound_var()),
374  pointer_offset(car.lower_bound_var())},
376  pointer_offset(car.upper_bound_var()),
377  pointer_offset(candidate_car.upper_bound_var())}}},
378  ns);
379 }
380 
382  const car_exprt &car,
383  bool allow_null_lhs,
384  bool include_stack_allocated,
385  optionalt<cfg_infot> &cfg_info_opt) const
386 {
387  bool no_targets = from_spec_assigns.empty() && from_heap_alloc.empty() &&
388  (!include_stack_allocated || from_stack_alloc.empty());
389 
390  // inclusion check expression
391  if(no_targets)
392  {
393  // if null lhs are allowed then we should have a null lhs when
394  // we reach this program point, otherwise we should never reach
395  // this program point
396  if(allow_null_lhs)
397  return null_pointer(car.target_start_address());
398  else
399  return false_exprt{};
400  }
401 
402  // Build a disjunction over all tracked locations
403  exprt::operandst disjuncts;
404 
405  for(const auto &pair : from_spec_assigns)
406  disjuncts.push_back(inclusion_check_single(car, pair.second));
407 
408  for(const auto &pair : from_heap_alloc)
409  disjuncts.push_back(inclusion_check_single(car, pair.second));
410 
411  if(include_stack_allocated)
412  {
413  for(const auto &pair : from_stack_alloc)
414  {
415  // skip dead targets
416  if(
417  cfg_info_opt.has_value() &&
418  !cfg_info_opt.value().is_maybe_alive(pair.first))
419  continue;
420 
421  disjuncts.push_back(inclusion_check_single(car, pair.second));
422  }
423  }
424 
425  if(allow_null_lhs)
427  and_exprt{car.valid_var(), disjunction(disjuncts)}};
428  else
429  return and_exprt{car.valid_var(), disjunction(disjuncts)};
430 }
431 
433  const exprt &condition,
434  const exprt &target)
435 {
436  conditional_target_exprt key{condition, target};
437  const auto &found = from_spec_assigns.find(key);
438  if(found != from_spec_assigns.end())
439  {
440  log.warning() << "Ignored duplicate expression '"
441  << from_expr(ns, target.id(), target)
442  << "' in assigns clause spec at "
443  << target.source_location().as_string() << messaget::eom;
444  return found->second;
445  }
446  else
447  {
448  from_spec_assigns.insert({key, create_car_expr(condition, target)});
449  return from_spec_assigns.find(key)->second;
450  }
451 }
452 
454  const symbol_exprt &target)
455 {
456  const auto &found = from_stack_alloc.find(target);
457  if(found != from_stack_alloc.end())
458  {
459  log.warning() << "Ignored duplicate stack-allocated target '"
460  << from_expr(ns, target.id(), target) << "' at "
461  << target.source_location().as_string() << messaget::eom;
462  return found->second;
463  }
464  else
465  {
466  from_stack_alloc.insert({target, create_car_expr(true_exprt{}, target)});
467  return from_stack_alloc.find(target)->second;
468  }
469 }
470 
471 const car_exprt &
473 {
474  const auto &found = from_heap_alloc.find(target);
475  if(found != from_heap_alloc.end())
476  {
477  log.warning() << "Ignored duplicate heap-allocated target '"
478  << from_expr(ns, target.id(), target) << "' at "
479  << target.source_location().as_string() << messaget::eom;
480  return found->second;
481  }
482  else
483  {
484  from_heap_alloc.insert({target, create_car_expr(true_exprt{}, target)});
485  return from_heap_alloc.find(target)->second;
486  }
487 }
488 
490  const car_exprt &tracked_car,
491  const car_exprt &freed_car,
492  goto_programt &result) const
493 {
494  source_locationt source_location(freed_car.source_location());
495  add_pragma_disable_pointer_checks(source_location);
496  add_pragma_disable_assigns_check(source_location);
497 
499  tracked_car.valid_var(),
500  and_exprt{tracked_car.valid_var(),
501  not_exprt{same_object(
502  tracked_car.lower_bound_var(), freed_car.lower_bound_var())}},
503  source_location));
504 }
505 
507  const car_exprt &freed_car,
508  goto_programt &dest) const
509 {
510  for(const auto &pair : from_spec_assigns)
511  invalidate_car(pair.second, freed_car, dest);
512 
513  for(const auto &pair : from_heap_alloc)
514  invalidate_car(pair.second, freed_car, dest);
515 }
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
signedbv_typet signed_size_type()
Definition: c_types.cpp:84
bitvector_typet char_type()
Definition: c_types.cpp:124
Function Call Graphs.
Operator to return the address of an object.
Definition: pointer_expr.h:361
Boolean AND.
Definition: std_expr.h:1974
The Boolean type.
Definition: std_types.h:36
directed_grapht get_directed_graph() const
Returns a grapht representation of this call graph, suitable for use with generic grapht algorithms.
Definition: call_graph.cpp:209
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Definition: call_graph.h:53
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.
const exprt & target_start_address() const
Start address of the target.
Allows to clean expressions of side effects.
Definition: utils.h:249
void clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
Definition: utils.h:258
Class that represents a single conditional target.
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition: c_expr.h:232
const exprt & condition() const
Definition: c_expr.h:266
const exprt::operandst & targets() const
Definition: c_expr.h:276
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
The Boolean constant false.
Definition: std_expr.h:2865
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:949
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:922
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.
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.
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...
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)
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.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irep_idt & id() const
Definition: irep.h:396
Binary less than or equal operator expression.
Definition: std_expr.h:782
mstreamt & warning() const
Definition: message.h:404
message_handlert & get_message_handler()
Definition: message.h:184
static eomt eom
Definition: message.h:297
Binary minus.
Definition: std_expr.h:973
Boolean negation.
Definition: std_expr.h:2181
Boolean OR.
Definition: std_expr.h:2082
The plus expression Associativity is not specified.
Definition: std_expr.h:914
const irep_idt & get_function() const
void set_comment(const irep_idt &comment)
const irep_idt & get_comment() const
void set_property_class(const irep_idt &property_class)
std::string as_string() const
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition: symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
irep_idt mode
Language mode.
Definition: symbol.h:49
The Boolean constant true.
Definition: std_expr.h:2856
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:293
A predicate that indicates that an address range is ok to write.
Definition: pointer_expr.h:781
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition: expr_util.cpp:21
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
Deprecated expression utility functions.
Specify write set in function contracts.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
nonstd::optional< T > optionalt
Definition: optional.h:35
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt null_pointer(const exprt &pointer)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:464
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:22
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
void add_pragma_disable_pointer_checks(source_locationt &location)
Adds a pragma on a source location disable all pointer checks.
Definition: utils.cpp:79
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &location, const irep_idt &mode, symbol_table_baset &symtab, std::string suffix, bool is_auxiliary)
Adds a fresh and uniquely named symbol to the symbol table.
Definition: utils.cpp:190
bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment)
Returns true if the given comment matches the type of comments created by make_assigns_clause_replace...
Definition: utils.cpp:278
void add_pragma_disable_assigns_check(source_locationt &location)
Adds a pragma on a source_locationt to disable inclusion checking.
Definition: utils.cpp:103