cprover
Loading...
Searching...
No Matches
instrument_spec_assigns.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Instrument assigns clauses in code contracts.
4
5Author: Remi Delmas
6
7Date: 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>
26
27#include "cfg_info.h"
28#include "utils.h"
29
31static const char LOG_HEADER[] = "assigns clause checking: ";
32
34static 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
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
75
82
89
91 const exprt &expr,
92 goto_programt &dest)
93{
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{
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();
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()) &&
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();
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
409 goto_programt &dest)
410{
411 // clean up side effects from the guard expression if needed
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{
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,
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)
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)
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,
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
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
864const 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
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.
unsignedbv_typet size_type()
Definition c_types.cpp:55
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
signedbv_typet signed_size_type()
Definition c_types.cpp:71
bitvector_typet char_type()
Definition c_types.cpp:111
Classes providing CFG-based information about symbols to guide simplifications in function and loop a...
Operator to return the address of an object.
Boolean AND.
Definition std_expr.h:2071
The Boolean type.
Definition std_types.h:36
Class that represents a normalized conditional address range, with:
const symbol_exprt & upper_bound_var() const
Identifier of the upper address bound snapshot variable.
const exprt & target_start_address() const
Start address of the target.
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_size() const
Size of the target in bytes.
const exprt & condition() const
Condition expression. When this condition holds the target is allowed.
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::operandst & targets() const
Definition c_expr.h:276
const exprt & condition() const
Definition c_expr.h:266
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
bool empty() const
Definition dstring.h:90
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
typet & type()
Return the type of the expression.
Definition expr.h:84
const source_locationt & source_location() const
Definition expr.h:223
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:162
The Boolean constant false.
Definition std_expr.h:3017
function_mapt function_map
This class represents an instruction in the GOTO intermediate representation.
source_locationt & source_location_nonconst()
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::iterator targett
instructionst::const_iterator const_targett
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.
bool empty() const
Is the program empty?
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
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:490
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
const irep_idt & id() const
Definition irep.h:396
irept & add(const irep_idt &name)
Definition irep.cpp:111
Binary less than or equal operator expression.
Definition std_expr.h:815
source_locationt source_location
Definition message.h:247
mstreamt & debug() const
Definition message.h:429
message_handlert & get_message_handler()
Definition message.h:184
mstreamt & warning() const
Definition message.h:404
static eomt eom
Definition message.h:297
Binary minus.
Definition std_expr.h:1006
Boolean negation.
Definition std_expr.h:2278
Boolean OR.
Definition std_expr.h:2179
The plus expression Associativity is not specified.
Definition std_expr.h:947
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
const irep_idt & get_function() const
void add_pragma(const irep_idt &pragma)
const irept::named_subt & get_pragmas() const
std::string as_string() const
const irep_idt & get_comment() const
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
Definition std_expr.h:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
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:3008
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
A predicate that indicates that an address range is ok to write.
#define CPROVER_PREFIX
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
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
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.
void add_pragma_disable_pointer_checks(source_locationt &source_location)
Adds a pragma on a source location disable all pointer checks.
bool has_propagate_static_local_pragma(source_locationt &source_location)
True iff the pragma to mark assignments to static local variables that need to be propagated upwards ...
void add_pragma_disable_assigns_check(source_locationt &source_location)
Adds a pragma on a source_locationt to disable inclusion checking.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
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.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt null_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)
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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
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:51
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition std_expr.h:206
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
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