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/simplify_expr.h>
23 
24 #include <ansi-c/c_expr.h>
25 #include <langapi/language_util.h>
26 
27 #include "cfg_info.h"
28 #include "utils.h"
29 
31 static const char LOG_HEADER[] = "assigns clause checking: ";
32 
34 static const char PROPAGATE_STATIC_LOCAL_PRAGMA[] =
35  "contracts:propagate-static-local";
36 
38 {
39  const auto &pragmas = source_location.get_pragmas();
40  return pragmas.find(PROPAGATE_STATIC_LOCAL_PRAGMA) != pragmas.end();
41 }
42 
44 {
46 }
47 
50  "contracts:disable:assigns-check";
51 
53 {
54  location.add_pragma("disable:pointer-check");
55  location.add_pragma("disable:pointer-primitive-check");
56  location.add_pragma("disable:pointer-overflow-check");
57  location.add_pragma("disable:signed-overflow-check");
58  location.add_pragma("disable:unsigned-overflow-check");
59  location.add_pragma("disable:conversion-check");
60 }
61 
65  const goto_programt::const_targett &target)
66 {
67  const auto &pragmas = target->source_location().get_pragmas();
68  return pragmas.find(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK) != pragmas.end();
69 }
70 
72 {
74 }
75 
78 {
80  return instr;
81 }
82 
84 {
87  return prog;
88 }
89 
91  const exprt &expr,
92  goto_programt &dest)
93 {
94  if(auto target = expr_try_dynamic_cast<conditional_target_group_exprt>(expr))
95  track_spec_target_group(*target, dest);
96  else
97  track_plain_spec_target(expr, dest);
98 }
99 
101  const symbol_exprt &symbol_expr,
102  goto_programt &dest)
103 {
104  create_snapshot(create_car_from_stack_alloc(symbol_expr), dest);
105 }
106 
108  const symbol_exprt &symbol_expr) const
109 {
110  return from_stack_alloc.find(symbol_expr) != from_stack_alloc.end();
111 }
112 
114  const symbol_exprt &symbol_expr,
115  goto_programt &dest)
116 {
117  // ensure it is tracked
119  stack_allocated_is_tracked(symbol_expr),
120  "symbol is not tracked :" + from_expr(ns, "", symbol_expr));
121 
122  const auto &car = from_stack_alloc.find(symbol_expr)->second;
123 
124  source_locationt source_location(symbol_expr.source_location());
125  add_pragma_disable_pointer_checks(source_location);
126  add_pragma_disable_assigns_check(source_location);
127 
129  car.valid_var(), false_exprt{}, source_location));
130 }
131 
133  const exprt &expr,
134  goto_programt &dest)
135 {
136  // insert in tracking set
137  const auto &car = create_car_from_heap_alloc(expr);
138 
139  // generate target validity check for this target.
140  target_validity_assertion(car, true, dest);
141 
142  // generate snapshot instructions for this target.
143  create_snapshot(car, dest);
144 }
145 
147  const exprt &lhs,
148  goto_programt &dest) const
149 {
150  // create temporary car but do not track
151  const auto car = create_car_expr(true_exprt{}, lhs);
152  create_snapshot(car, dest);
153  inclusion_check_assertion(car, false, true, dest);
154 }
155 
157 {
158  const auto &found = functions.function_map.find(function_id);
159  INVARIANT(
160  found != functions.function_map.end(),
161  "the instrumented function must exist in the model");
162  const goto_programt &body = found->second.body;
163 
164  propagated_static_localst propagated;
165  covered_locationst covered_locations;
166  covered_locations[function_id].anywhere();
168  function_id,
169  body.instructions.begin(),
170  body.instructions.end(),
171  covered_locations,
172  propagated);
173 
174  std::unordered_set<symbol_exprt, irep_hash> symbols;
175  collect_static_symbols(covered_locations, symbols);
176 
177  for(const auto &expr : propagated)
179 
180  for(const auto &sym : symbols)
182 }
183 
187  goto_programt &dest)
188 {
189  propagated_static_localst propagated;
190  covered_locationst covered_locations;
191  traverse_instructions(function_id, it, end, covered_locations, propagated);
192 
193  std::unordered_set<symbol_exprt, irep_hash> symbols;
194  collect_static_symbols(covered_locations, symbols);
195 
196  for(const auto &sym : symbols)
198 
199  for(const auto &expr : propagated)
201 }
202 
204  const irep_idt ambient_function_id,
207  covered_locationst &covered_locations,
208  propagated_static_localst &propagated) const
209 {
210  for(; it != end; it++)
211  {
212  const auto &loc = it->source_location();
213  const auto &loc_fun = loc.get_function();
214  if(!loc_fun.empty())
215  {
216  auto &itv = covered_locations[loc_fun];
217  if(loc_fun == ambient_function_id)
218  {
219  itv.update(loc);
220  }
221  else
222  {
223  // we are on an instruction coming from some other function that the
224  // ambient function so we assume that the whole function was inlined
225  itv.anywhere();
226  }
227  }
228  else
229  {
230  log.debug() << "Ignoring instruction without function attribute"
231  << messaget::eom;
232  // ignore instructions with a source_location that
233  // have no function attribute
234  }
235 
236  // Collect assignments marked as "propagate static local"
237  // (these are generated by havoc_assigns_clause_targett)
239  {
240  INVARIANT(
241  it->is_assign() && can_cast_expr<symbol_exprt>(it->assign_lhs()) &&
242  can_cast_expr<side_effect_expr_nondett>(it->assign_rhs()),
243  "Expected an assignment of the form `symbol_exprt := "
244  "side_effect_expr_nondett`");
245  // must be a nondet assignment to a symbol
246  propagated.insert(to_symbol_expr(it->assign_lhs()));
247  }
248 
249  // recurse into bodies of called functions if available
250  if(it->is_function_call())
251  {
252  const auto &fun_expr = it->call_function();
253 
255  fun_expr.id() == ID_symbol,
256  "Local static search requires function pointer removal");
257  const irep_idt &fun_id = to_symbol_expr(fun_expr).get_identifier();
258 
259  const auto &found = functions.function_map.find(fun_id);
260  INVARIANT(
261  found != functions.function_map.end(),
262  "Function " + id2string(fun_id) + "not in function map");
263 
264  // do not recurse if the function was already seen before
265  if(covered_locations.find(fun_id) == covered_locations.end())
266  {
267  // consider all locations of this function covered
268  covered_locations[fun_id].anywhere();
269  const goto_programt &body = found->second.body;
270  if(!body.empty())
271  {
273  fun_id,
274  body.instructions.begin(),
275  body.instructions.end(),
276  covered_locations,
277  propagated);
278  }
279  }
280  }
281  }
282 }
283 
285  covered_locationst &covered_locations,
286  std::unordered_set<symbol_exprt, irep_hash> &dest)
287 {
288  for(const auto &sym_pair : st)
289  {
290  const auto &sym = sym_pair.second;
291  if(sym.is_static_lifetime)
292  {
293  const auto &loc = sym.location;
294  if(!loc.get_function().empty())
295  {
296  const auto &itv = covered_locations.find(loc.get_function());
297  if(itv != covered_locations.end() && itv->second.contains(sym.location))
298  dest.insert(sym.symbol_expr());
299  }
300  }
301  }
302 }
303 
306  const exprt &expr,
307 
308  goto_programt &dest)
309 {
310  // create temporary car but do not track
311  const auto car = create_car_expr(true_exprt{}, expr);
312 
313  // generate snapshot instructions for this target.
314  create_snapshot(car, dest);
315 
316  // check inclusion, allowing null and not allowing stack allocated locals
317  inclusion_check_assertion(car, true, false, dest);
318 
319  // invalidate aliases of the freed object
321 }
322 
324  goto_programt &body,
325  goto_programt::targett instruction_it,
326  const goto_programt::targett &instruction_end,
327  const std::function<bool(const goto_programt::targett &)> &pred)
328 {
329  while(instruction_it != instruction_end)
330  {
331  // Skip instructions marked as disabled for assigns clause checking
332  if(
333  has_disable_assigns_check_pragma(instruction_it) ||
334  (pred && !pred(instruction_it)))
335  {
336  instruction_it++;
337  continue;
338  }
339 
340  // Do not instrument this instruction again in the future,
341  // since we are going to instrument it now below.
342  add_pragma_disable_assigns_check(*instruction_it);
343 
344  if(instruction_it->is_decl() && must_track_decl(instruction_it))
345  {
346  // grab the declared symbol
347  const auto &decl_symbol = instruction_it->decl_symbol();
348  // move past the call and then insert the CAR
349  instruction_it++;
350  goto_programt payload;
351  track_stack_allocated(decl_symbol, payload);
352  insert_before_swap_and_advance(body, instruction_it, payload);
353  // since CAR was inserted *after* the DECL instruction,
354  // move the instruction pointer backward,
355  // because the enclosing while loop step takes
356  // care of the increment
357  instruction_it--;
358  }
359  else if(instruction_it->is_assign() && must_check_assign(instruction_it))
360  {
361  instrument_assign_statement(instruction_it, body);
362  }
363  else if(instruction_it->is_function_call())
364  {
365  instrument_call_statement(instruction_it, body);
366  }
367  else if(instruction_it->is_dead() && must_track_dead(instruction_it))
368  {
369  const auto &symbol = instruction_it->dead_symbol();
370  if(stack_allocated_is_tracked(symbol))
371  {
372  goto_programt payload;
373  invalidate_stack_allocated(symbol, payload);
374  insert_before_swap_and_advance(body, instruction_it, payload);
375  }
376  else
377  {
378  // Some variables declared outside of the loop
379  // can go `DEAD` (possible conditionally) when return
380  // statements exist inside the loop body.
381  // Since they are not DECL'd inside the loop, these locations
382  // are not automatically tracked in the stack_allocated map,
383  // so to be writable these variables must be listed in the assigns
384  // clause.
385  log.warning() << "Found a `DEAD` variable " << symbol.get_identifier()
386  << " without corresponding `DECL`, at: "
387  << instruction_it->source_location() << messaget::eom;
388  }
389  }
390  else if(
391  instruction_it->is_other() &&
392  instruction_it->get_other().get_statement() == ID_havoc_object)
393  {
394  auto havoc_argument = instruction_it->get_other().operands().front();
395  auto havoc_object = pointer_object(havoc_argument);
396  havoc_object.add_source_location() = instruction_it->source_location();
397  goto_programt payload;
398  check_inclusion_assignment(havoc_object, payload);
399  insert_before_swap_and_advance(body, instruction_it, payload);
400  }
401 
402  // Move to the next instruction
403  instruction_it++;
404  }
405 }
406 
408  const conditional_target_group_exprt &group,
409  goto_programt &dest)
410 {
411  // clean up side effects from the guard expression if needed
412  cleanert cleaner(st, log.get_message_handler());
413  exprt condition(group.condition());
414  if(has_subexpr(condition, ID_side_effect))
415  cleaner.clean(condition, dest, mode);
416 
417  // create conditional address ranges by distributing the condition
418  for(const auto &target : group.targets())
419  {
420  // insert in tracking set
421  const auto &car = create_car_from_spec_assigns(condition, target);
422 
423  // generate target validity check for this target.
424  target_validity_assertion(car, true, dest);
425 
426  // generate snapshot instructions for this target.
427  create_snapshot(car, dest);
428  }
429 }
430 
432  const exprt &expr,
433  goto_programt &dest)
434 {
435  // insert in tracking set
436  const auto &car = create_car_from_spec_assigns(true_exprt{}, expr);
437 
438  // generate target validity check for this target.
439  target_validity_assertion(car, true, dest);
440 
441  // generate snapshot instructions for this target.
442  create_snapshot(car, dest);
443 }
444 
448  const std::string &suffix,
449  const typet &type,
450  const source_locationt &location,
451  const irep_idt &mode,
452  symbol_table_baset &symbol_table)
453 {
454  return get_fresh_aux_symbol(
455  type,
456  id2string(location.get_function()),
457  suffix,
458  location,
459  mode,
460  symbol_table)
461  .symbol_expr();
462 }
463 
465  const exprt &condition,
466  const exprt &target) const
467 {
468  const source_locationt &source_location = target.source_location();
469  const auto &valid_var =
470  create_fresh_symbol("__car_valid", bool_typet(), source_location, mode, st);
471 
472  const auto &lower_bound_var = create_fresh_symbol(
473  "__car_lb", pointer_type(char_type()), source_location, mode, st);
474 
475  const auto &upper_bound_var = create_fresh_symbol(
476  "__car_ub", pointer_type(char_type()), source_location, mode, st);
477 
478  if(target.id() == ID_pointer_object)
479  {
480  const auto &arg = to_pointer_object_expr(target).pointer();
481  return {
482  condition,
483  target,
484  minus_exprt(
486  pointer_offset(arg)),
488  valid_var,
489  lower_bound_var,
490  upper_bound_var,
492  }
494  {
495  const auto &funcall = to_side_effect_expr_function_call(target);
496  if(can_cast_expr<symbol_exprt>(funcall.function()))
497  {
498  const auto &ident = to_symbol_expr(funcall.function()).get_identifier();
499 
501  ident == CPROVER_PREFIX "object_from" ||
502  ident == CPROVER_PREFIX "object_upto" ||
503  ident == CPROVER_PREFIX "object_whole" ||
504  ident == CPROVER_PREFIX "assignable",
505  "call to function '" + id2string(ident) +
506  "' in assigns clause not supported yet");
507 
508  if(ident == CPROVER_PREFIX "object_from")
509  {
510  const auto &ptr = funcall.arguments().at(0);
511  return {
512  condition,
513  target,
514  // lb = ptr
516  // size = object_size(ptr) - pointer_offset(ptr)
518  minus_exprt{
520  object_size(ptr), signed_size_type()),
521  pointer_offset(ptr)},
522  size_type()),
523  valid_var,
524  lower_bound_var,
525  upper_bound_var,
527  }
528  else if(ident == CPROVER_PREFIX "object_upto")
529  {
530  const auto &ptr = funcall.arguments().at(0);
531  const auto &size = funcall.arguments().at(1);
532  return {
533  condition,
534  target,
535  // lb = ptr
537  // size = size
539  valid_var,
540  lower_bound_var,
541  upper_bound_var,
543  }
544  else if(ident == CPROVER_PREFIX "object_whole")
545  {
546  const auto &ptr = funcall.arguments().at(0);
547  return {
548  condition,
549  target,
550  // lb = ptr - pointer_offset(ptr)
551  minus_exprt(
553  pointer_offset(ptr)),
554  // size = object_size(ptr)
556  valid_var,
557  lower_bound_var,
558  upper_bound_var,
560  }
561  else if(ident == CPROVER_PREFIX "assignable")
562  {
563  const auto &ptr = funcall.arguments().at(0);
564  const auto &size = funcall.arguments().at(1);
565  const auto &is_ptr_to_ptr = funcall.arguments().at(2);
566  return {
567  condition,
568  target,
569  // lb = ptr
571  // size = size
573  valid_var,
574  lower_bound_var,
575  upper_bound_var,
576  is_ptr_to_ptr.is_true() ? car_havoc_methodt::NONDET_ASSIGN
578  }
579  }
580  }
581  else if(is_assignable(target))
582  {
583  const auto &size = size_of_expr(target.type(), ns);
584 
585  INVARIANT(
586  size.has_value(),
587  "no definite size for lvalue target:\n" + target.pretty());
588 
589  return {
590  condition,
591  target,
592  // lb = &target
595  // size = sizeof(target)
597  valid_var,
598  lower_bound_var,
599  upper_bound_var,
601  }
602 
603  UNREACHABLE;
604 }
605 
607  const car_exprt &car,
608  goto_programt &dest) const
609 {
610  source_locationt source_location(car.source_location());
611  add_pragma_disable_pointer_checks(source_location);
612  add_pragma_disable_assigns_check(source_location);
613 
614  dest.add(goto_programt::make_decl(car.valid_var(), source_location));
615 
617  car.valid_var(),
619  and_exprt{
621  ns),
622  source_location));
623 
624  dest.add(goto_programt::make_decl(car.lower_bound_var(), source_location));
625 
627  car.lower_bound_var(), car.target_start_address(), source_location));
628 
629  dest.add(goto_programt::make_decl(car.upper_bound_var(), source_location));
630 
632  car.upper_bound_var(),
635  source_location));
636 }
637 
639  const car_exprt &car,
640  bool allow_null_target) const
641 {
642  // If requested, we check that when guard condition is true,
643  // the target's `start_address` pointer satisfies w_ok with the expected size
644  // (or is NULL if we allow it explicitly).
645  // This assertion will be falsified whenever `start_address` is invalid or
646  // not of the right size (or is NULL if we do not allow it explicitly).
647  auto result =
650 
651  if(allow_null_target)
653 
654  return simplify_expr(result, ns);
655 }
656 
658  const car_exprt &car,
659  bool allow_null_target,
660  goto_programt &dest) const
661 {
662  // since assigns clauses are declared outside of their function body
663  // their source location might not have a function attribute
664  source_locationt source_location(car.source_location());
665  if(source_location.get_function().empty())
666  source_location.set_function(function_id);
667 
668  source_location.set_property_class("assigns");
669 
670  add_pragma_disable_pointer_checks(source_location);
671  add_pragma_disable_assigns_check(source_location);
672 
673  std::string comment = "Check that ";
674  comment += from_expr(ns, "", car.target());
675  comment += " is valid";
676  if(!car.condition().is_true())
677  {
678  comment += " when ";
679  comment += from_expr(ns, "", car.condition());
680  }
681 
682  source_location.set_comment(comment);
683 
685  target_validity_expr(car, allow_null_target), source_location));
686 }
687 
689  const car_exprt &car,
690  bool allow_null_lhs,
691  bool include_stack_allocated,
692  goto_programt &dest) const
693 {
694  source_locationt source_location(car.source_location());
695 
696  // since assigns clauses are declared outside of their function body
697  // their source location might not have a function attribute
698  if(source_location.get_function().empty())
699  source_location.set_function(function_id);
700 
701  add_pragma_disable_pointer_checks(source_location);
702  add_pragma_disable_assigns_check(source_location);
703 
704  source_location.set_property_class("assigns");
705 
706  const auto &orig_comment = source_location.get_comment();
707  std::string comment = "Check that ";
709  {
710  if(!car.condition().is_true())
711  comment += from_expr(ns, "", car.condition()) + ": ";
712  comment += from_expr(ns, "", car.target());
713  }
714  else
715  comment += id2string(orig_comment);
716 
717  comment += " is assignable";
718  source_location.set_comment(comment);
719 
720  exprt inclusion_check =
721  inclusion_check_full(car, allow_null_lhs, include_stack_allocated);
722  // Record what target is checked.
723  auto &checked_assigns =
724  static_cast<exprt &>(inclusion_check.add(ID_checked_assigns));
725  checked_assigns = car.target();
726 
727  dest.add(goto_programt::make_assertion(inclusion_check, source_location));
728 }
729 
731  const car_exprt &car,
732  const car_exprt &candidate_car) const
733 {
734  // remark: both lb and ub are derived from the same object so checking
735  // same_object(upper_bound_address_var, lhs.upper_bound_address_var)
736  // is redundant
737  return simplify_expr(
738  and_exprt{
739  {candidate_car.valid_var(),
740  same_object(candidate_car.lower_bound_var(), car.lower_bound_var()),
741  less_than_or_equal_exprt{pointer_offset(candidate_car.lower_bound_var()),
742  pointer_offset(car.lower_bound_var())},
744  pointer_offset(car.upper_bound_var()),
745  pointer_offset(candidate_car.upper_bound_var())}}},
746  ns);
747 }
748 
750  const car_exprt &car,
751  bool allow_null_lhs,
752  bool include_stack_allocated) const
753 {
754  bool no_targets = from_spec_assigns.empty() && from_heap_alloc.empty() &&
755  (!include_stack_allocated ||
756  (from_static_local.empty() && from_stack_alloc.empty()));
757 
758  // inclusion check expression
759  if(no_targets)
760  {
761  // if null lhs are allowed then we should have a null lhs when
762  // we reach this program point, otherwise we should never reach
763  // this program point
764  if(allow_null_lhs)
765  return null_object(car.target_start_address());
766  else
767  return false_exprt{};
768  }
769 
770  // Build a disjunction over all tracked locations
771  exprt::operandst disjuncts;
772  log.debug() << LOG_HEADER << " inclusion check: \n"
773  << from_expr_using_mode(ns, mode, car.target()) << " in {"
774  << messaget::eom;
775 
776  for(const auto &pair : from_spec_assigns)
777  {
778  disjuncts.push_back(inclusion_check_single(car, pair.second));
779  log.debug() << "\t(spec) "
780  << from_expr_using_mode(ns, mode, pair.second.target())
781  << messaget::eom;
782  }
783 
784  for(const auto &heap_car : from_heap_alloc)
785  {
786  disjuncts.push_back(inclusion_check_single(car, heap_car));
787  log.debug() << "\t(heap) "
788  << from_expr_using_mode(ns, mode, heap_car.target())
789  << messaget::eom;
790  }
791 
792  if(include_stack_allocated)
793  {
794  for(const auto &pair : from_stack_alloc)
795  {
796  disjuncts.push_back(inclusion_check_single(car, pair.second));
797  log.debug() << "\t(stack) "
798  << from_expr_using_mode(ns, mode, pair.second.target())
799  << messaget::eom;
800  }
801 
802  // static locals are stack allocated and can never be DEAD
803  for(const auto &pair : from_static_local)
804  {
805  disjuncts.push_back(inclusion_check_single(car, pair.second));
806  log.debug() << "\t(static) "
807  << from_expr_using_mode(ns, mode, pair.second.target())
808  << messaget::eom;
809  }
810  }
811  log.debug() << "}" << messaget::eom;
812 
813  if(allow_null_lhs)
814  return or_exprt{
816  and_exprt{car.valid_var(), disjunction(disjuncts)}};
817  else
818  return and_exprt{car.valid_var(), disjunction(disjuncts)};
819 }
820 
822  const exprt &condition,
823  const exprt &target)
824 {
825  conditional_target_exprt key{condition, target};
826  const auto &found = from_spec_assigns.find(key);
827  if(found != from_spec_assigns.end())
828  {
829  log.warning() << "Ignored duplicate expression '"
830  << from_expr(ns, target.id(), target)
831  << "' in assigns clause spec at "
832  << target.source_location().as_string() << messaget::eom;
833  return found->second;
834  }
835  else
836  {
837  log.debug() << LOG_HEADER << "creating CAR for assigns clause target "
838  << format(condition) << ": " << format(target) << messaget::eom;
839  from_spec_assigns.insert({key, create_car_expr(condition, target)});
840  return from_spec_assigns.find(key)->second;
841  }
842 }
843 
845  const symbol_exprt &target)
846 {
847  const auto &found = from_stack_alloc.find(target);
848  if(found != from_stack_alloc.end())
849  {
850  log.warning() << "Ignored duplicate stack-allocated target '"
851  << from_expr(ns, target.id(), target) << "' at "
852  << target.source_location().as_string() << messaget::eom;
853  return found->second;
854  }
855  else
856  {
857  log.debug() << LOG_HEADER << "creating CAR for stack-allocated target "
858  << format(target) << messaget::eom;
859  from_stack_alloc.insert({target, create_car_expr(true_exprt{}, target)});
860  return from_stack_alloc.find(target)->second;
861  }
862 }
863 
864 const car_exprt &
866 {
867  log.debug() << LOG_HEADER << "creating CAR for heap-allocated target "
868  << format(target) << messaget::eom;
869  from_heap_alloc.emplace_back(create_car_expr(true_exprt{}, target));
870  return from_heap_alloc.back();
871 }
872 
874  const symbol_exprt &target)
875 {
876  const auto &found = from_static_local.find(target);
877  if(found != from_static_local.end())
878  {
879  log.warning() << "Ignored duplicate static local var target '"
880  << from_expr(ns, target.id(), target) << "' at "
881  << target.source_location().as_string() << messaget::eom;
882  return found->second;
883  }
884  else
885  {
886  log.debug() << LOG_HEADER << "creating CAR for static local target "
887  << format(target) << messaget::eom;
888  from_static_local.insert({target, create_car_expr(true_exprt{}, target)});
889  return from_static_local.find(target)->second;
890  }
891 }
892 
894  const car_exprt &tracked_car,
895  const car_exprt &freed_car,
896  goto_programt &result) const
897 {
898  source_locationt source_location(freed_car.source_location());
899  add_pragma_disable_pointer_checks(source_location);
900  add_pragma_disable_assigns_check(source_location);
901 
903  tracked_car.valid_var(),
904  and_exprt{tracked_car.valid_var(),
905  not_exprt{same_object(
906  tracked_car.lower_bound_var(), freed_car.lower_bound_var())}},
907  source_location));
908 }
909 
911  const car_exprt &freed_car,
912  goto_programt &dest) const
913 {
914  for(const auto &pair : from_spec_assigns)
915  invalidate_car(pair.second, freed_car, dest);
916 
917  for(const auto &car : from_heap_alloc)
918  invalidate_car(car, freed_car, dest);
919 }
920 
923  const goto_programt::const_targett &target)
924 {
925  log.debug().source_location = target->source_location();
926 
927  if(can_cast_expr<symbol_exprt>(target->assign_lhs()))
928  {
929  const auto &symbol_expr = to_symbol_expr(target->assign_lhs());
930 
931  if(cfg_info.is_local(symbol_expr.get_identifier()))
932  {
933  log.debug() << LOG_HEADER
934  << "skipping checking on assignment to local symbol "
935  << format(symbol_expr) << messaget::eom;
936  return false;
937  }
938  else
939  {
940  log.debug() << LOG_HEADER << "checking assignment to non-local symbol "
941  << format(symbol_expr) << messaget::eom;
942  return true;
943  }
944 
945  log.debug() << LOG_HEADER << "checking assignment to symbol "
946  << format(symbol_expr) << messaget::eom;
947  return true;
948  }
949  else
950  {
951  // This is not a mere symbol.
952  // Since non-dirty locals are not tracked explicitly in the write set,
953  // we need to skip the check if we can verify that the expression describes
954  // an access to a non-dirty local symbol or an input parameter,
955  // otherwise the check will fail.
956  // In addition, the expression shall not contain address_of or dereference
957  // operators, regardless of the base symbol/object on which they apply.
958  // If the expression contains an address_of operation, the assignment gets
959  // checked. If the base object is a local or a parameter, it will also be
960  // flagged as dirty and will be tracked explicitly, and the check will pass.
961  // If the expression contains a dereference operation, the assignment gets
962  // checked. If the dereferenced address was computed from a local object,
963  // from a function parameter or returned by a local malloc,
964  // then the object will be tracked explicitly and the check will pass.
965  // In all other cases (address of a non-local object, or dereference of
966  // a non-locally computed address) the location must be given explicitly
967  // in the assigns clause to be tracked and we must check the assignment.
968  if(cfg_info.is_local_composite_access(target->assign_lhs()))
969  {
970  log.debug()
971  << LOG_HEADER
972  << "skipping check on assignment to local composite member expression "
973  << format(target->assign_lhs()) << messaget::eom;
974  return false;
975  }
976  log.debug() << LOG_HEADER << "checking assignment to expression "
977  << format(target->assign_lhs()) << messaget::eom;
978  return true;
979  }
980 }
981 
984  const irep_idt &ident) const
985 {
987 }
988 
991  const goto_programt::const_targett &target) const
992 {
993  log.debug().source_location = target->source_location();
994  if(must_track_decl_or_dead(target->decl_symbol().get_identifier()))
995  {
996  log.debug() << LOG_HEADER << "explicitly tracking "
997  << format(target->decl_symbol()) << " as assignable"
998  << messaget::eom;
999  return true;
1000  }
1001  else
1002  {
1003  log.debug() << LOG_HEADER << "implicitly tracking "
1004  << format(target->decl_symbol())
1005  << " as assignable (non-dirty local)" << messaget::eom;
1006  return false;
1007  }
1008 }
1009 
1013  const goto_programt::const_targett &target) const
1014 {
1015  return must_track_decl_or_dead(target->dead_symbol().get_identifier());
1016 }
1017 
1019  goto_programt::targett &instruction_it,
1020  goto_programt &program) const
1021 {
1022  auto lhs = instruction_it->assign_lhs();
1023  lhs.add_source_location() = instruction_it->source_location();
1024  goto_programt payload;
1025  check_inclusion_assignment(lhs, payload);
1026  insert_before_swap_and_advance(program, instruction_it, payload);
1027 }
1028 
1030  goto_programt::targett &instruction_it,
1031  goto_programt &body)
1032 {
1034  instruction_it->is_function_call(),
1035  "The first argument of instrument_call_statement should always be "
1036  "a function call");
1037 
1038  const auto &callee_name =
1039  to_symbol_expr(instruction_it->call_function()).get_identifier();
1040 
1041  if(callee_name == "malloc")
1042  {
1043  const auto &function_call = to_code_function_call(instruction_it->code());
1044  if(function_call.lhs().is_not_nil())
1045  {
1046  // grab the returned pointer from malloc
1047  auto object = pointer_object(function_call.lhs());
1048  object.add_source_location() = function_call.source_location();
1049  // move past the call and then insert the CAR
1050  instruction_it++;
1051  goto_programt payload;
1052  track_heap_allocated(object, payload);
1053  insert_before_swap_and_advance(body, instruction_it, payload);
1054  // since CAR was inserted *after* the malloc call,
1055  // move the instruction pointer backward,
1056  // because the caller increments it in a `for` loop
1057  instruction_it--;
1058  }
1059  }
1060  else if(callee_name == "free")
1061  {
1062  const auto &ptr = instruction_it->call_arguments().front();
1063  auto object = pointer_object(ptr);
1064  object.add_source_location() = instruction_it->source_location();
1065  goto_programt payload;
1067  insert_before_swap_and_advance(body, instruction_it, payload);
1068  }
1069 }
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:2120
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:35
void clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
Definition: utils.h:44
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
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:3064
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:384
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:247
mstreamt & warning() const
Definition: message.h:404
mstreamt & debug() const
Definition: message.h:429
message_handlert & get_message_handler()
Definition: message.h:184
static eomt eom
Definition: message.h:297
Binary minus.
Definition: std_expr.h:1061
Boolean negation.
Definition: std_expr.h:2327
Boolean OR.
Definition: std_expr.h:2228
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:3055
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2076
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
#define CPROVER_PREFIX
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:141
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:40
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:54
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:335
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:234