CBMC
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/c_types.h>
17 #include <util/expr_util.h>
18 #include <util/format_expr.h>
19 #include <util/fresh_symbol.h>
22 #include <util/prefix.h>
23 #include <util/simplify_expr.h>
24 
25 #include <ansi-c/c_expr.h>
27 #include <langapi/language_util.h>
28 
29 #include "cfg_info.h"
30 #include "utils.h"
31 
33 static const char LOG_HEADER[] = "assigns clause checking: ";
34 
36 static const char PROPAGATE_STATIC_LOCAL_PRAGMA[] =
37  "contracts:propagate-static-local";
38 
40 {
41  const auto &pragmas = source_location.get_pragmas();
42  return pragmas.find(PROPAGATE_STATIC_LOCAL_PRAGMA) != pragmas.end();
43 }
44 
46 {
48 }
49 
52  "contracts:disable:assigns-check";
53 
55 {
56  location.add_pragma("disable:pointer-check");
57  location.add_pragma("disable:pointer-primitive-check");
58  location.add_pragma("disable:pointer-overflow-check");
59  location.add_pragma("disable:signed-overflow-check");
60  location.add_pragma("disable:unsigned-overflow-check");
61  location.add_pragma("disable:conversion-check");
62 }
63 
67  const goto_programt::const_targett &target)
68 {
69  const auto &pragmas = target->source_location().get_pragmas();
70  return pragmas.find(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK) != pragmas.end();
71 }
72 
74 {
76 }
77 
80 {
82  return instr;
83 }
84 
86 {
89  return prog;
90 }
91 
93  const exprt &expr,
94  goto_programt &dest)
95 {
96  if(auto target = expr_try_dynamic_cast<conditional_target_group_exprt>(expr))
97  track_spec_target_group(*target, dest);
98  else
99  track_plain_spec_target(expr, dest);
100 }
101 
103  const symbol_exprt &symbol_expr,
104  goto_programt &dest)
105 {
106  create_snapshot(create_car_from_stack_alloc(symbol_expr), dest);
107 }
108 
110  const symbol_exprt &symbol_expr) const
111 {
112  return from_stack_alloc.find(symbol_expr) != from_stack_alloc.end();
113 }
114 
116  const symbol_exprt &symbol_expr,
117  goto_programt &dest)
118 {
119  // ensure it is tracked
121  stack_allocated_is_tracked(symbol_expr),
122  "symbol is not tracked :" + from_expr(ns, "", symbol_expr));
123 
124  const auto &car = from_stack_alloc.find(symbol_expr)->second;
125 
126  source_locationt source_location(symbol_expr.source_location());
127  add_pragma_disable_pointer_checks(source_location);
128  add_pragma_disable_assigns_check(source_location);
129 
131  car.valid_var(), false_exprt{}, source_location));
132 }
133 
135  const exprt &expr,
136  goto_programt &dest)
137 {
138  // insert in tracking set
139  const auto &car = create_car_from_heap_alloc(expr);
140 
141  // generate target validity check for this target.
142  target_validity_assertion(car, true, dest);
143 
144  // generate snapshot instructions for this target.
145  create_snapshot(car, dest);
146 }
147 
149  const exprt &lhs,
150  goto_programt &dest) const
151 {
152  // Don't check assignable for CPROVER symbol
153  if(
154  lhs.id() == ID_symbol &&
155  has_prefix(id2string(to_symbol_expr(lhs).get_identifier()), CPROVER_PREFIX))
156  {
157  return;
158  }
159  // create temporary car but do not track
160  const auto car = create_car_expr(true_exprt{}, lhs);
161  create_snapshot(car, dest);
162  inclusion_check_assertion(car, false, true, dest);
163 }
164 
166 {
167  const auto &found = functions.function_map.find(function_id);
168  INVARIANT(
169  found != functions.function_map.end(),
170  "the instrumented function must exist in the model");
171  const goto_programt &body = found->second.body;
172 
173  propagated_static_localst propagated;
174  covered_locationst covered_locations;
175  covered_locations[function_id].anywhere();
177  function_id,
178  body.instructions.begin(),
179  body.instructions.end(),
180  covered_locations,
181  propagated);
182 
183  std::unordered_set<symbol_exprt, irep_hash> symbols;
184  collect_static_symbols(covered_locations, symbols);
185 
186  for(const auto &expr : propagated)
188 
189  for(const auto &sym : symbols)
191 }
192 
196  goto_programt &dest)
197 {
198  propagated_static_localst propagated;
199  covered_locationst covered_locations;
200  traverse_instructions(function_id, it, end, covered_locations, propagated);
201 
202  std::unordered_set<symbol_exprt, irep_hash> symbols;
203  collect_static_symbols(covered_locations, symbols);
204 
205  for(const auto &sym : symbols)
207 
208  for(const auto &expr : propagated)
210 }
211 
213  const irep_idt ambient_function_id,
216  covered_locationst &covered_locations,
217  propagated_static_localst &propagated) const
218 {
219  for(; it != end; it++)
220  {
221  const auto &loc = it->source_location();
222  const auto &loc_fun = loc.get_function();
223  if(!loc_fun.empty())
224  {
225  auto &itv = covered_locations[loc_fun];
226  if(loc_fun == ambient_function_id)
227  {
228  itv.update(loc);
229  }
230  else
231  {
232  // we are on an instruction coming from some other function that the
233  // ambient function so we assume that the whole function was inlined
234  itv.anywhere();
235  }
236  }
237  else
238  {
239  log.debug() << "Ignoring instruction without function attribute"
240  << messaget::eom;
241  // ignore instructions with a source_location that
242  // have no function attribute
243  }
244 
245  // Collect assignments marked as "propagate static local"
246  // (these are generated by havoc_assigns_clause_targett)
248  {
249  INVARIANT(
250  it->is_assign() && can_cast_expr<symbol_exprt>(it->assign_lhs()) &&
251  can_cast_expr<side_effect_expr_nondett>(it->assign_rhs()),
252  "Expected an assignment of the form `symbol_exprt := "
253  "side_effect_expr_nondett`");
254  // must be a nondet assignment to a symbol
255  propagated.insert(to_symbol_expr(it->assign_lhs()));
256  }
257 
258  // recurse into bodies of called functions if available
259  if(it->is_function_call())
260  {
261  const auto &fun_expr = it->call_function();
262 
264  fun_expr.id() == ID_symbol,
265  "Local static search requires function pointer removal");
266  const irep_idt &fun_id = to_symbol_expr(fun_expr).get_identifier();
267 
268  const auto &found = functions.function_map.find(fun_id);
269  INVARIANT(
270  found != functions.function_map.end(),
271  "Function " + id2string(fun_id) + "not in function map");
272 
273  // do not recurse if the function was already seen before
274  if(covered_locations.find(fun_id) == covered_locations.end())
275  {
276  // consider all locations of this function covered
277  covered_locations[fun_id].anywhere();
278  const goto_programt &body = found->second.body;
279  if(!body.empty())
280  {
282  fun_id,
283  body.instructions.begin(),
284  body.instructions.end(),
285  covered_locations,
286  propagated);
287  }
288  }
289  }
290  }
291 }
292 
294  covered_locationst &covered_locations,
295  std::unordered_set<symbol_exprt, irep_hash> &dest)
296 {
297  for(const auto &sym_pair : st)
298  {
299  const auto &sym = sym_pair.second;
300  if(sym.is_static_lifetime)
301  {
302  const auto &loc = sym.location;
303  if(!loc.get_function().empty())
304  {
305  const auto &itv = covered_locations.find(loc.get_function());
306  if(itv != covered_locations.end() && itv->second.contains(sym.location))
307  dest.insert(sym.symbol_expr());
308  }
309  }
310  }
311 }
312 
315  const exprt &expr,
316 
317  goto_programt &dest)
318 {
319  // create temporary car but do not track
320  const auto car = create_car_expr(true_exprt{}, expr);
321 
322  // generate snapshot instructions for this target.
323  create_snapshot(car, dest);
324 
325  // check inclusion, allowing null and not allowing stack allocated locals
326  inclusion_check_assertion(car, true, false, dest);
327 
328  // invalidate aliases of the freed object
330 }
331 
333  goto_programt &body,
334  goto_programt::targett instruction_it,
335  const goto_programt::targett &instruction_end,
336  const std::function<bool(const goto_programt::targett &)> &pred)
337 {
338  while(instruction_it != instruction_end)
339  {
340  // Skip instructions marked as disabled for assigns clause checking
341  if(
342  has_disable_assigns_check_pragma(instruction_it) ||
343  (pred && !pred(instruction_it)))
344  {
345  instruction_it++;
346  continue;
347  }
348 
349  // Do not instrument this instruction again in the future,
350  // since we are going to instrument it now below.
351  add_pragma_disable_assigns_check(*instruction_it);
352 
353  if(instruction_it->is_decl() && must_track_decl(instruction_it))
354  {
355  // grab the declared symbol
356  const auto &decl_symbol = instruction_it->decl_symbol();
357  // move past the call and then insert the CAR
358  instruction_it++;
359  goto_programt payload;
360  track_stack_allocated(decl_symbol, payload);
361  insert_before_swap_and_advance(body, instruction_it, payload);
362  // since CAR was inserted *after* the DECL instruction,
363  // move the instruction pointer backward,
364  // because the enclosing while loop step takes
365  // care of the increment
366  instruction_it--;
367  }
368  else if(instruction_it->is_assign() && must_check_assign(instruction_it))
369  {
370  instrument_assign_statement(instruction_it, body);
371  }
372  else if(instruction_it->is_function_call())
373  {
374  instrument_call_statement(instruction_it, body);
375  }
376  else if(instruction_it->is_dead() && must_track_dead(instruction_it))
377  {
378  const auto &symbol = instruction_it->dead_symbol();
379  if(stack_allocated_is_tracked(symbol))
380  {
381  goto_programt payload;
382  invalidate_stack_allocated(symbol, payload);
383  insert_before_swap_and_advance(body, instruction_it, payload);
384  }
385  else
386  {
387  // Some variables declared outside of the loop
388  // can go `DEAD` (possible conditionally) when return
389  // statements exist inside the loop body.
390  // Since they are not DECL'd inside the loop, these locations
391  // are not automatically tracked in the stack_allocated map,
392  // so to be writable these variables must be listed in the assigns
393  // clause.
394  log.warning() << "Found a `DEAD` variable " << symbol.get_identifier()
395  << " without corresponding `DECL`, at: "
396  << instruction_it->source_location() << messaget::eom;
397  }
398  }
399  else if(
400  instruction_it->is_other() &&
401  instruction_it->get_other().get_statement() == ID_havoc_object)
402  {
403  auto havoc_argument = instruction_it->get_other().operands().front();
404  auto havoc_object = pointer_object(havoc_argument);
405  havoc_object.add_source_location() = instruction_it->source_location();
406  goto_programt payload;
407  check_inclusion_assignment(havoc_object, payload);
408  insert_before_swap_and_advance(body, instruction_it, payload);
409  }
410 
411  // Move to the next instruction
412  instruction_it++;
413  }
414 }
415 
417  const conditional_target_group_exprt &group,
418  goto_programt &dest)
419 {
420  // clean up side effects from the guard expression if needed
421  cleanert cleaner(st, log.get_message_handler());
422  exprt condition(group.condition());
423  std::list<irep_idt> new_vars;
424  if(has_subexpr(condition, ID_side_effect))
425  new_vars = cleaner.clean(condition, dest, mode);
426 
427  // create conditional address ranges by distributing the condition
428  for(const auto &target : group.targets())
429  {
430  // insert in tracking set
431  const auto &car = create_car_from_spec_assigns(condition, target);
432 
433  // generate target validity check for this target.
434  target_validity_assertion(car, true, dest);
435 
436  // generate snapshot instructions for this target.
437  create_snapshot(car, dest);
438  }
439 
440  destruct_locals(new_vars, dest, ns);
441 }
442 
444  const exprt &expr,
445  goto_programt &dest)
446 {
447  // insert in tracking set
448  const auto &car = create_car_from_spec_assigns(true_exprt{}, expr);
449 
450  // generate target validity check for this target.
451  target_validity_assertion(car, true, dest);
452 
453  // generate snapshot instructions for this target.
454  create_snapshot(car, dest);
455 }
456 
460  const std::string &suffix,
461  const typet &type,
462  const source_locationt &location,
463  const irep_idt &mode,
464  symbol_table_baset &symbol_table)
465 {
466  return get_fresh_aux_symbol(
467  type,
468  id2string(location.get_function()),
469  suffix,
470  location,
471  mode,
472  symbol_table)
473  .symbol_expr();
474 }
475 
477  const exprt &condition,
478  const exprt &target) const
479 {
480  const source_locationt &source_location = target.source_location();
481  const auto &valid_var =
482  create_fresh_symbol("__car_valid", bool_typet(), source_location, mode, st);
483 
484  const auto &lower_bound_var = create_fresh_symbol(
485  "__car_lb", pointer_type(char_type()), source_location, mode, st);
486 
487  const auto &upper_bound_var = create_fresh_symbol(
488  "__car_ub", pointer_type(char_type()), source_location, mode, st);
489 
490  if(target.id() == ID_pointer_object)
491  {
492  const auto &arg = to_pointer_object_expr(target).pointer();
493  return {
494  condition,
495  target,
496  minus_exprt(
498  pointer_offset(arg)),
500  valid_var,
501  lower_bound_var,
502  upper_bound_var,
504  }
506  {
507  const auto &funcall = to_side_effect_expr_function_call(target);
508  if(can_cast_expr<symbol_exprt>(funcall.function()))
509  {
510  const auto &ident = to_symbol_expr(funcall.function()).get_identifier();
511 
513  ident == CPROVER_PREFIX "object_from" ||
514  ident == CPROVER_PREFIX "object_upto" ||
515  ident == CPROVER_PREFIX "object_whole" ||
516  ident == CPROVER_PREFIX "assignable",
517  "call to function '" + id2string(ident) +
518  "' in assigns clause not supported yet");
519 
520  if(ident == CPROVER_PREFIX "object_from")
521  {
522  const auto &ptr = funcall.arguments().at(0);
523  return {
524  condition,
525  target,
526  // lb = ptr
528  // size = object_size(ptr) - pointer_offset(ptr)
530  minus_exprt{
532  object_size(ptr), signed_size_type()),
533  pointer_offset(ptr)},
534  size_type()),
535  valid_var,
536  lower_bound_var,
537  upper_bound_var,
539  }
540  else if(ident == CPROVER_PREFIX "object_upto")
541  {
542  const auto &ptr = funcall.arguments().at(0);
543  const auto &size = funcall.arguments().at(1);
544  return {
545  condition,
546  target,
547  // lb = ptr
549  // size = size
551  valid_var,
552  lower_bound_var,
553  upper_bound_var,
555  }
556  else if(ident == CPROVER_PREFIX "object_whole")
557  {
558  const auto &ptr = funcall.arguments().at(0);
559  return {
560  condition,
561  target,
562  // lb = ptr - pointer_offset(ptr)
563  minus_exprt(
565  pointer_offset(ptr)),
566  // size = object_size(ptr)
568  valid_var,
569  lower_bound_var,
570  upper_bound_var,
572  }
573  else if(ident == CPROVER_PREFIX "assignable")
574  {
575  const auto &ptr = funcall.arguments().at(0);
576  const auto &size = funcall.arguments().at(1);
577  const auto &is_ptr_to_ptr = funcall.arguments().at(2);
578  return {
579  condition,
580  target,
581  // lb = ptr
583  // size = size
585  valid_var,
586  lower_bound_var,
587  upper_bound_var,
588  is_ptr_to_ptr.is_true() ? car_havoc_methodt::NONDET_ASSIGN
590  }
591  }
592  }
593  else if(is_assignable(target))
594  {
595  const auto &size = size_of_expr(target.type(), ns);
596 
597  INVARIANT(
598  size.has_value(),
599  "no definite size for lvalue target:\n" + target.pretty());
600 
601  return {
602  condition,
603  target,
604  // lb = &target
607  // size = sizeof(target)
609  valid_var,
610  lower_bound_var,
611  upper_bound_var,
613  }
614 
615  UNREACHABLE;
616 }
617 
619  const car_exprt &car,
620  goto_programt &dest) const
621 {
622  source_locationt source_location(car.source_location());
623  add_pragma_disable_pointer_checks(source_location);
624  add_pragma_disable_assigns_check(source_location);
625 
626  dest.add(goto_programt::make_decl(car.valid_var(), source_location));
627 
629  car.valid_var(),
631  and_exprt{
633  ns),
634  source_location));
635 
636  dest.add(goto_programt::make_decl(car.lower_bound_var(), source_location));
637 
639  car.lower_bound_var(), car.target_start_address(), source_location));
640 
641  dest.add(goto_programt::make_decl(car.upper_bound_var(), source_location));
642 
644  car.upper_bound_var(),
647  source_location));
648 }
649 
651  const car_exprt &car,
652  bool allow_null_target) const
653 {
654  // If requested, we check that when guard condition is true,
655  // the target's `start_address` pointer satisfies w_ok with the expected size
656  // (or is NULL if we allow it explicitly).
657  // This assertion will be falsified whenever `start_address` is invalid or
658  // not of the right size (or is NULL if we do not allow it explicitly).
659  auto result = or_exprt{
660  boolean_negate(car.condition()),
662 
663  if(allow_null_target)
665 
666  return simplify_expr(result, ns);
667 }
668 
670  const car_exprt &car,
671  bool allow_null_target,
672  goto_programt &dest) const
673 {
674  // since assigns clauses are declared outside of their function body
675  // their source location might not have a function attribute
676  source_locationt source_location(car.source_location());
677  if(source_location.get_function().empty())
678  source_location.set_function(function_id);
679 
680  source_location.set_property_class("assigns");
681 
682  add_pragma_disable_pointer_checks(source_location);
683  add_pragma_disable_assigns_check(source_location);
684 
685  std::string comment = "Check that ";
686  comment += from_expr(ns, "", car.target());
687  comment += " is valid";
688  if(!car.condition().is_true())
689  {
690  comment += " when ";
691  comment += from_expr(ns, "", car.condition());
692  }
693 
694  source_location.set_comment(comment);
695 
697  target_validity_expr(car, allow_null_target), source_location));
698 }
699 
701  const car_exprt &car,
702  bool allow_null_lhs,
703  bool include_stack_allocated,
704  goto_programt &dest) const
705 {
706  source_locationt source_location(car.source_location());
707 
708  // since assigns clauses are declared outside of their function body
709  // their source location might not have a function attribute
710  if(source_location.get_function().empty())
711  source_location.set_function(function_id);
712 
713  add_pragma_disable_pointer_checks(source_location);
714  add_pragma_disable_assigns_check(source_location);
715 
716  source_location.set_property_class("assigns");
717 
718  const auto &orig_comment = source_location.get_comment();
719  std::string comment = "Check that ";
721  {
722  if(!car.condition().is_true())
723  comment += from_expr(ns, "", car.condition()) + ": ";
724  comment += from_expr(ns, "", car.target());
725  }
726  else
727  comment += id2string(orig_comment);
728 
729  comment += " is assignable";
730  source_location.set_comment(comment);
731 
732  exprt inclusion_check =
733  inclusion_check_full(car, allow_null_lhs, include_stack_allocated);
734  // Record what target is checked.
735  auto &checked_assigns =
736  static_cast<exprt &>(inclusion_check.add(ID_checked_assigns));
737  checked_assigns = car.target();
738 
739  dest.add(goto_programt::make_assertion(inclusion_check, source_location));
740 }
741 
743  const car_exprt &car,
744  const car_exprt &candidate_car) const
745 {
746  // remark: both lb and ub are derived from the same object so checking
747  // same_object(upper_bound_address_var, lhs.upper_bound_address_var)
748  // is redundant
749  return simplify_expr(
750  and_exprt{
751  {candidate_car.valid_var(),
752  same_object(candidate_car.lower_bound_var(), car.lower_bound_var()),
753  less_than_or_equal_exprt{pointer_offset(candidate_car.lower_bound_var()),
754  pointer_offset(car.lower_bound_var())},
756  pointer_offset(car.upper_bound_var()),
757  pointer_offset(candidate_car.upper_bound_var())}}},
758  ns);
759 }
760 
762  const car_exprt &car,
763  bool allow_null_lhs,
764  bool include_stack_allocated) const
765 {
766  bool no_targets = from_spec_assigns.empty() && from_heap_alloc.empty() &&
767  (!include_stack_allocated ||
768  (from_static_local.empty() && from_stack_alloc.empty()));
769 
770  // inclusion check expression
771  if(no_targets)
772  {
773  // if null lhs are allowed then we should have a null lhs when
774  // we reach this program point, otherwise we should never reach
775  // this program point
776  if(allow_null_lhs)
777  return null_object(car.target_start_address());
778  else
779  return false_exprt{};
780  }
781 
782  // Build a disjunction over all tracked locations
783  exprt::operandst disjuncts;
784  log.debug() << LOG_HEADER << " inclusion check: \n"
785  << from_expr_using_mode(ns, mode, car.target()) << " in {"
786  << messaget::eom;
787 
788  for(const auto &pair : from_spec_assigns)
789  {
790  disjuncts.push_back(inclusion_check_single(car, pair.second));
791  log.debug() << "\t(spec) "
792  << from_expr_using_mode(ns, mode, pair.second.target())
793  << messaget::eom;
794  }
795 
796  for(const auto &heap_car : from_heap_alloc)
797  {
798  disjuncts.push_back(inclusion_check_single(car, heap_car));
799  log.debug() << "\t(heap) "
800  << from_expr_using_mode(ns, mode, heap_car.target())
801  << messaget::eom;
802  }
803 
804  if(include_stack_allocated)
805  {
806  for(const auto &pair : from_stack_alloc)
807  {
808  disjuncts.push_back(inclusion_check_single(car, pair.second));
809  log.debug() << "\t(stack) "
810  << from_expr_using_mode(ns, mode, pair.second.target())
811  << messaget::eom;
812  }
813 
814  // static locals are stack allocated and can never be DEAD
815  for(const auto &pair : from_static_local)
816  {
817  disjuncts.push_back(inclusion_check_single(car, pair.second));
818  log.debug() << "\t(static) "
819  << from_expr_using_mode(ns, mode, pair.second.target())
820  << messaget::eom;
821  }
822  }
823  log.debug() << "}" << messaget::eom;
824 
825  if(allow_null_lhs)
826  return or_exprt{
828  and_exprt{car.valid_var(), disjunction(disjuncts)}};
829  else
830  return and_exprt{car.valid_var(), disjunction(disjuncts)};
831 }
832 
834  const exprt &condition,
835  const exprt &target)
836 {
837  conditional_target_exprt key{condition, target};
838  const auto &found = from_spec_assigns.find(key);
839  if(found != from_spec_assigns.end())
840  {
841  log.warning() << "Ignored duplicate expression '"
842  << from_expr(ns, target.id(), target)
843  << "' in assigns clause spec at "
844  << target.source_location().as_string() << messaget::eom;
845  return found->second;
846  }
847  else
848  {
849  log.debug() << LOG_HEADER << "creating CAR for assigns clause target "
850  << format(condition) << ": " << format(target) << messaget::eom;
851  from_spec_assigns.insert({key, create_car_expr(condition, target)});
852  return from_spec_assigns.find(key)->second;
853  }
854 }
855 
857  const symbol_exprt &target)
858 {
859  const auto &found = from_stack_alloc.find(target);
860  if(found != from_stack_alloc.end())
861  {
862  log.warning() << "Ignored duplicate stack-allocated target '"
863  << from_expr(ns, target.id(), target) << "' at "
864  << target.source_location().as_string() << messaget::eom;
865  return found->second;
866  }
867  else
868  {
869  log.debug() << LOG_HEADER << "creating CAR for stack-allocated target "
870  << format(target) << messaget::eom;
871  from_stack_alloc.insert({target, create_car_expr(true_exprt{}, target)});
872  return from_stack_alloc.find(target)->second;
873  }
874 }
875 
876 const car_exprt &
878 {
879  log.debug() << LOG_HEADER << "creating CAR for heap-allocated target "
880  << format(target) << messaget::eom;
881  from_heap_alloc.emplace_back(create_car_expr(true_exprt{}, target));
882  return from_heap_alloc.back();
883 }
884 
886  const symbol_exprt &target)
887 {
888  const auto &found = from_static_local.find(target);
889  if(found != from_static_local.end())
890  {
891  log.warning() << "Ignored duplicate static local var target '"
892  << from_expr(ns, target.id(), target) << "' at "
893  << target.source_location().as_string() << messaget::eom;
894  return found->second;
895  }
896  else
897  {
898  log.debug() << LOG_HEADER << "creating CAR for static local target "
899  << format(target) << messaget::eom;
900  from_static_local.insert({target, create_car_expr(true_exprt{}, target)});
901  return from_static_local.find(target)->second;
902  }
903 }
904 
906  const car_exprt &tracked_car,
907  const car_exprt &freed_car,
908  goto_programt &result) const
909 {
910  source_locationt source_location(freed_car.source_location());
911  add_pragma_disable_pointer_checks(source_location);
912  add_pragma_disable_assigns_check(source_location);
913 
915  tracked_car.valid_var(),
916  and_exprt{tracked_car.valid_var(),
917  not_exprt{same_object(
918  tracked_car.lower_bound_var(), freed_car.lower_bound_var())}},
919  source_location));
920 }
921 
923  const car_exprt &freed_car,
924  goto_programt &dest) const
925 {
926  for(const auto &pair : from_spec_assigns)
927  invalidate_car(pair.second, freed_car, dest);
928 
929  for(const auto &car : from_heap_alloc)
930  invalidate_car(car, freed_car, dest);
931 }
932 
935  const goto_programt::const_targett &target)
936 {
937  log.debug().source_location = target->source_location();
938 
939  if(can_cast_expr<symbol_exprt>(target->assign_lhs()))
940  {
941  const auto &symbol_expr = to_symbol_expr(target->assign_lhs());
942 
943  if(cfg_info.is_local(symbol_expr.get_identifier()))
944  {
945  log.debug() << LOG_HEADER
946  << "skipping checking on assignment to local symbol "
947  << format(symbol_expr) << messaget::eom;
948  return false;
949  }
950  else
951  {
952  log.debug() << LOG_HEADER << "checking assignment to non-local symbol "
953  << format(symbol_expr) << messaget::eom;
954  return true;
955  }
956 
957  log.debug() << LOG_HEADER << "checking assignment to symbol "
958  << format(symbol_expr) << messaget::eom;
959  return true;
960  }
961  else
962  {
963  // This is not a mere symbol.
964  // Since non-dirty locals are not tracked explicitly in the write set,
965  // we need to skip the check if we can verify that the expression describes
966  // an access to a non-dirty local symbol or an input parameter,
967  // otherwise the check will fail.
968  // In addition, the expression shall not contain address_of or dereference
969  // operators, regardless of the base symbol/object on which they apply.
970  // If the expression contains an address_of operation, the assignment gets
971  // checked. If the base object is a local or a parameter, it will also be
972  // flagged as dirty and will be tracked explicitly, and the check will pass.
973  // If the expression contains a dereference operation, the assignment gets
974  // checked. If the dereferenced address was computed from a local object,
975  // from a function parameter or returned by a local malloc,
976  // then the object will be tracked explicitly and the check will pass.
977  // In all other cases (address of a non-local object, or dereference of
978  // a non-locally computed address) the location must be given explicitly
979  // in the assigns clause to be tracked and we must check the assignment.
980  if(cfg_info.is_local_composite_access(target->assign_lhs()))
981  {
982  log.debug()
983  << LOG_HEADER
984  << "skipping check on assignment to local composite member expression "
985  << format(target->assign_lhs()) << messaget::eom;
986  return false;
987  }
988  log.debug() << LOG_HEADER << "checking assignment to expression "
989  << format(target->assign_lhs()) << messaget::eom;
990  return true;
991  }
992 }
993 
996  const irep_idt &ident) const
997 {
999 }
1000 
1003  const goto_programt::const_targett &target) const
1004 {
1005  log.debug().source_location = target->source_location();
1006  if(must_track_decl_or_dead(target->decl_symbol().get_identifier()))
1007  {
1008  log.debug() << LOG_HEADER << "explicitly tracking "
1009  << format(target->decl_symbol()) << " as assignable"
1010  << messaget::eom;
1011  return true;
1012  }
1013  else
1014  {
1015  log.debug() << LOG_HEADER << "implicitly tracking "
1016  << format(target->decl_symbol())
1017  << " as assignable (non-dirty local)" << messaget::eom;
1018  return false;
1019  }
1020 }
1021 
1025  const goto_programt::const_targett &target) const
1026 {
1027  return must_track_decl_or_dead(target->dead_symbol().get_identifier());
1028 }
1029 
1031  goto_programt::targett &instruction_it,
1032  goto_programt &program) const
1033 {
1034  auto lhs = instruction_it->assign_lhs();
1035  lhs.add_source_location() = instruction_it->source_location();
1036  goto_programt payload;
1037  check_inclusion_assignment(lhs, payload);
1038  insert_before_swap_and_advance(program, instruction_it, payload);
1039 }
1040 
1042  goto_programt::targett &instruction_it,
1043  goto_programt &body)
1044 {
1046  instruction_it->is_function_call(),
1047  "The first argument of instrument_call_statement should always be "
1048  "a function call");
1049 
1050  const auto &callee_name =
1051  to_symbol_expr(instruction_it->call_function()).get_identifier();
1052 
1053  if(callee_name == "malloc")
1054  {
1055  const auto &function_call = to_code_function_call(instruction_it->code());
1056  if(function_call.lhs().is_not_nil())
1057  {
1058  // grab the returned pointer from malloc
1059  auto object = pointer_object(function_call.lhs());
1060  object.add_source_location() = function_call.source_location();
1061  // move past the call and then insert the CAR
1062  instruction_it++;
1063  goto_programt payload;
1064  track_heap_allocated(object, payload);
1065  insert_before_swap_and_advance(body, instruction_it, payload);
1066  // since CAR was inserted *after* the malloc call,
1067  // move the instruction pointer backward,
1068  // because the caller increments it in a `for` loop
1069  instruction_it--;
1070  }
1071  }
1072  else if(callee_name == "free")
1073  {
1074  const auto &ptr = instruction_it->call_arguments().front();
1075  auto object = pointer_object(ptr);
1076  object.add_source_location() = instruction_it->source_location();
1077  goto_programt payload;
1079  insert_before_swap_and_advance(body, instruction_it, payload);
1080  }
1081 }
API to expression classes that are internal to the C frontend.
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:235
signedbv_typet signed_size_type()
Definition: c_types.cpp:66
bitvector_typet char_type()
Definition: c_types.cpp:106
Classes providing CFG-based information about symbols to guide simplifications in function and loop a...
Operator to return the address of an object.
Definition: pointer_expr.h:540
Boolean AND.
Definition: std_expr.h:2125
The Boolean type.
Definition: std_types.h:36
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.
virtual bool is_not_local_or_dirty_local(const irep_idt &ident) const =0
Returns true iff the given ident is either non-locally declared or is locally-declared but dirty.
virtual bool is_local(const irep_idt &ident) const =0
Returns true iff ident is locally declared.
bool is_local_composite_access(const exprt &expr) const
Returns true iff expr is an access to a locally declared symbol and does not contain dereference or a...
Definition: cfg_info.h:51
Class that allows to clean expressions of side effects and to generate havoc_slice expressions.
Definition: utils.h:37
std::list< irep_idt > clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
Definition: utils.h:47
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:233
const exprt & condition() const
Definition: c_expr.h:267
const exprt::operandst & targets() const
Definition: c_expr.h:277
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
std::vector< exprt > operandst
Definition: expr.h:58
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
const source_locationt & source_location() const
Definition: expr.h:231
typet & type()
Return the type of the expression.
Definition: expr.h:84
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:170
The Boolean constant false.
Definition: std_expr.h:3077
function_mapt function_map
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
source_locationt & source_location_nonconst()
Definition: goto_program.h:338
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
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:739
bool empty() const
Is the program empty?
Definition: goto_program.h:799
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:964
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:933
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.
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 ...
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.
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,...
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)
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.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:482
const irep_idt & id() const
Definition: irep.h:388
irept & add(const irep_idt &name)
Definition: irep.cpp:103
Binary less than or equal operator expression.
Definition: std_expr.h:870
source_locationt source_location
Definition: message.h:239
mstreamt & warning() const
Definition: message.h:396
mstreamt & debug() const
Definition: message.h:421
message_handlert & get_message_handler()
Definition: message.h:183
static eomt eom
Definition: message.h:289
Binary minus.
Definition: std_expr.h:1061
Boolean negation.
Definition: std_expr.h:2332
Boolean OR.
Definition: std_expr.h:2233
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
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)
const irept::named_subt & get_pragmas() const
void add_pragma(const irep_idt &pragma)
std::string as_string() const
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
The symbol table base class interface.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
The Boolean constant true.
Definition: std_expr.h:3068
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2081
The type of an expression, extends irept.
Definition: type.h:29
A predicate that indicates that an address range is ok to write.
Definition: pointer_expr.h:989
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
Definition: destructor.cpp:62
Destructor Calls.
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition: expr_util.cpp:24
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
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:103
Deprecated expression utility functions.
static format_containert< T > format(const T &o)
Definition: format.h:37
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
const code_function_callt & to_code_function_call(const goto_instruction_codet &code)
#define Forall_goto_program_instructions(it, program)
static const char PROPAGATE_STATIC_LOCAL_PRAGMA[]
Pragma used to mark assignments to static locals that need to be propagated.
void add_pragma_disable_pointer_checks(source_locationt &location)
Adds a pragma on a source location disable all pointer checks.
bool has_disable_assigns_check_pragma(const goto_programt::const_targett &target)
Returns true iff the target instruction is tagged with a 'CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK' prag...
bool has_propagate_static_local_pragma(const source_locationt &source_location)
const char CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK[]
A local pragma used to keep track and skip already instrumented instructions.
static const char LOG_HEADER[]
header for log messages
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...
static symbol_exprt create_fresh_symbol(const std::string &suffix, const typet &type, const source_locationt &location, const irep_idt &mode, symbol_table_baset &symbol_table)
Creates a fresh symbolt with given suffix, scoped to the function of location.
void add_pragma_disable_assigns_check(source_locationt &location)
Adds a pragma on a source_locationt to disable inclusion checking.
Specify write set in function contracts.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::string from_expr_using_mode(const namespacet &ns, const irep_idt &mode, const exprt &expr)
Formats an expression using the given namespace, using the given mode to retrieve the language printe...
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
std::optional< 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_object(const exprt &pointer)
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:108
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:525
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
Definition: std_code.h:1540
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1739
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
Definition: std_code.h:1730
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:71
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:256
#define size_type
Definition: unistd.c:347
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:338
void insert_before_swap_and_advance(goto_programt &destination, goto_programt::targett &target, goto_programt &payload)
Insert a goto program before a target instruction iterator and advance the iterator.
Definition: utils.cpp:237