cprover
Loading...
Searching...
No Matches
contracts.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Verify and use annotated loop and function contracts
4
5Author: Michael Tautschnig
6
7Date: February 2016
8
9\*******************************************************************/
10
13
14#include "contracts.h"
15
16#include <util/c_types.h>
18#include <util/expr_util.h>
19#include <util/find_symbols.h>
20#include <util/format_expr.h>
21#include <util/fresh_symbol.h>
22#include <util/graph.h>
24#include <util/message.h>
25#include <util/std_code.h>
26
30
32#include <ansi-c/c_expr.h>
38
39#include "cfg_info.h"
41#include "inlining_decorator.h"
43#include "memory_predicates.h"
44#include "utils.h"
45
46#include <algorithm>
47#include <map>
48
50 const irep_idt &function_name,
52 const local_may_aliast &local_may_alias,
55 const loopt &loop,
57 exprt invariant,
59 const irep_idt &mode)
60{
61 const auto loop_head_location = loop_head->source_location();
62 const auto loop_number = loop_end->loop_number;
63
64 // Vector representing a (possibly multidimensional) decreases clause
65 const auto &decreases_clause_exprs = decreases_clause.operands();
66
67 // Temporary variables for storing the multidimensional decreases clause
68 // at the start of and end of a loop body
69 std::vector<symbol_exprt> old_decreases_vars, new_decreases_vars;
70
71 // replace bound variables by fresh instances
72 if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall))
73 add_quantified_variable(symbol_table, invariant, mode);
74
75 // instrument
76 //
77 // ... preamble ...
78 // HEAD:
79 // ... eval guard ...
80 // if (!guard)
81 // goto EXIT;
82 // ... loop body ...
83 // goto HEAD;
84 // EXIT:
85 // ... postamble ...
86 //
87 // to
88 //
89 // ... preamble ...
90 // ,- initialize loop_entry history vars;
91 // | entered_loop = false
92 // loop assigns check | initial_invariant_val = invariant_expr;
93 // - unchecked, temps | in_base_case = true;
94 // func assigns check | snapshot (write_set);
95 // - disabled via pragma | goto HEAD;
96 // | STEP:
97 // --. | assert (initial_invariant_val);
98 // loop assigns check | | in_base_case = false;
99 // - not applicable >======= in_loop_havoc_block = true;
100 // func assigns check | | havoc (assigns_set);
101 // + deferred | | in_loop_havoc_block = false;
102 // --' | assume (invariant_expr);
103 // `- old_variant_val = decreases_clause_expr;
104 // * HEAD:
105 // loop assigns check ,- ... eval guard ...
106 // + assertions added | if (!guard)
107 // func assigns check | goto EXIT;
108 // - disabled via pragma `- ... loop body ...
109 // ,- entered_loop = true
110 // | if (in_base_case)
111 // | goto STEP;
112 // loop assigns check | assert (invariant_expr);
113 // - unchecked, temps | new_variant_val = decreases_clause_expr;
114 // func assigns check | assert (new_variant_val < old_variant_val);
115 // - disabled via pragma | dead old_variant_val, new_variant_val;
116 // | * assume (false);
117 // | * EXIT:
118 // To be inserted at ,~~~|~~~~ assert (entered_loop ==> !in_base_case);
119 // every unique EXIT | | dead loop_entry history vars, in_base_case;
120 // (break, goto etc.) `~~~`- ~~ dead initial_invariant_val, entered_loop;
121 // ... postamble ..
122 //
123 // Asterisks (*) denote anchor points (goto targets) for instrumentations.
124 // We insert generated code above and/below these targets.
125 //
126 // Assertions for assigns clause checking are inserted in the loop body.
127
128 // Process "loop_entry" history variables.
129 // We find and replace all "__CPROVER_loop_entry" subexpressions in invariant.
131 symbol_table, invariant, loop_head_location, mode);
132 invariant.swap(replace_history_result.expression_after_replacement);
133 const auto &history_var_map = replace_history_result.parameter_to_history;
134 // an intermediate goto_program to store generated instructions
135 // to be inserted before the loop head
137 replace_history_result.history_construction;
138
139 // Create a temporary to track if we entered the loop,
140 // i.e., the loop guard was satisfied.
141 const auto entered_loop =
143 bool_typet(),
144 id2string(loop_head_location.get_function()),
145 std::string(ENTERED_LOOP) + "__" + std::to_string(loop_number),
147 mode,
149 .symbol_expr();
154
155 // Create a snapshot of the invariant so that we can check the base case,
156 // if the loop is not vacuous and must be abstracted with contracts.
157 const auto initial_invariant_val =
159 bool_typet(),
160 id2string(loop_head_location.get_function()),
163 mode,
165 .symbol_expr();
168 {
169 // Although the invariant at this point will not have side effects,
170 // it is still a C expression, and needs to be "goto_convert"ed.
171 // Note that this conversion may emit many GOTO instructions.
173 initial_invariant_val, invariant};
174 initial_invariant_value_assignment.add_source_location() =
178 }
179
180 // Create a temporary variable to track base case vs inductive case
181 // instrumentation of the loop.
183 bool_typet(),
184 id2string(loop_head_location.get_function()),
185 "__in_base_case",
187 mode,
189 .symbol_expr();
194
195 // CAR snapshot instructions for checking assigns clause
197
198 loop_cfg_infot cfg_info(goto_function, loop);
199
200 // track static local symbols
202 function_name,
204 cfg_info,
207
208 instrument_spec_assigns.track_static_locals_between(
210
211 // set of targets to havoc
213
214 if(assigns_clause.is_nil())
215 {
216 // No assigns clause was specified for this loop.
217 // Infer memory locations assigned by the loop from the loop instructions
218 // and the inferred aliasing relation.
219 try
220 {
221 get_assigns(local_may_alias, loop, to_havoc);
222
223 // remove loop-local symbols from the inferred set
224 cfg_info.erase_locals(to_havoc);
225
226 // If the set contains pairs (i, a[i]),
227 // we widen them to (i, __CPROVER_POINTER_OBJECT(a))
229
230 log.debug() << "No loop assigns clause provided. Inferred targets: {";
231 // Add inferred targets to the loop assigns clause.
232 bool ran_once = false;
233 for(const auto &target : to_havoc)
234 {
235 if(ran_once)
236 log.debug() << ", ";
237 ran_once = true;
238 log.debug() << format(target);
239 instrument_spec_assigns.track_spec_target(
240 target, snapshot_instructions);
241 }
242 log.debug() << "}" << messaget::eom;
243
244 instrument_spec_assigns.get_static_locals(
245 std::inserter(to_havoc, to_havoc.end()));
246 }
247 catch(const analysis_exceptiont &exc)
248 {
249 log.error() << "Failed to infer variables being modified by the loop at "
251 << ".\nPlease specify an assigns clause.\nReason:"
252 << messaget::eom;
253 throw exc;
254 }
255 }
256 else
257 {
258 // An assigns clause was specified for this loop.
259 // Add the targets to the set of expressions to havoc.
260 for(const auto &target : assigns_clause.operands())
261 {
262 to_havoc.insert(target);
263 instrument_spec_assigns.track_spec_target(target, snapshot_instructions);
264 }
265 }
266
267 // Insert instrumentation
268 // This must be done before havocing the write set.
269 // FIXME: this is not true for write set targets that
270 // might depend on other write set targets.
272
273 // Insert a jump to the loop head
274 // (skipping over the step case initialization code below)
277
278 // The STEP case instructions follow.
279 // We skip past it initially, because of the unconditional jump above,
280 // but jump back here if we get past the loop guard while in_base_case.
281
282 const auto step_case_target =
285
286 // If we jump here, then the loop runs at least once,
287 // so add the base case assertion:
288 // assert(initial_invariant_val)
289 // We use a block scope for assertion, since it's immediately goto converted,
290 // and doesn't need to be kept around.
291 {
293 assertion.add_source_location() = loop_head_location;
294 assertion.add_source_location().set_comment(
295 "Check loop invariant before entry");
297 }
298
299 // Insert the first block of pre_loop_head_instrs,
300 // with a pragma to disable assigns clause checking.
301 // All of the initialization code so far introduces local temporaries,
302 // which need not be checked against the enclosing scope's assigns clause.
303 goto_function.body.destructive_insert(
305
306 // Generate havocing code for assignment targets.
307 // ASSIGN in_loop_havoc_block = true;
308 // havoc (assigns_set);
309 // ASSIGN in_loop_havoc_block = false;
310 const auto in_loop_havoc_block =
312 bool_typet(),
313 id2string(loop_head_location.get_function()),
314 std::string(IN_LOOP_HAVOC_BLOCK) + +"__" + std::to_string(loop_number),
316 mode,
318 .symbol_expr();
325 havoc_gen.append_full_havoc_code(loop_head_location, pre_loop_head_instrs);
328
329 // Insert the second block of pre_loop_head_instrs: the havocing code.
330 // We do not `add_pragma_disable_assigns_check`,
331 // so that the enclosing scope's assigns clause instrumentation
332 // would pick these havocs up for inclusion (subset) checks.
333 goto_function.body.destructive_insert(loop_head, pre_loop_head_instrs);
334
335 // Generate: assume(invariant) just after havocing
336 // We use a block scope for assumption, since it's immediately goto converted,
337 // and doesn't need to be kept around.
338 {
339 code_assumet assumption{invariant};
342 }
343
344 // Create fresh temporary variables that store the multidimensional
345 // decreases clause's value before and after the loop
346 for(const auto &clause : decreases_clause.operands())
347 {
348 const auto old_decreases_var =
350 clause.type(),
351 id2string(loop_head_location.get_function()),
352 "tmp_cc",
354 mode,
356 .symbol_expr();
360
361 const auto new_decreases_var =
363 clause.type(),
364 id2string(loop_head_location.get_function()),
365 "tmp_cc",
367 mode,
369 .symbol_expr();
373 }
374
375 // TODO: Fix loop contract handling for do/while loops.
376 if(loop_end->is_goto() && !loop_end->condition().is_true())
377 {
378 log.error() << "Loop contracts are unsupported on do/while loops: "
380 throw 0;
381
382 // non-deterministically skip the loop if it is a do-while loop.
383 // pre_loop_head_instrs.add(goto_programt::make_goto(
384 // loop_end, side_effect_expr_nondett(bool_typet(), loop_head_location)));
385 }
386
387 // Generate: assignments to store the multidimensional decreases clause's
388 // value just before the loop_head
389 if(!decreases_clause.is_nil())
390 {
391 for(size_t i = 0; i < old_decreases_vars.size(); i++)
392 {
395 old_decreases_assignment.add_source_location() = loop_head_location;
398 }
399
400 goto_function.body.destructive_insert(
402 }
403
404 // Insert the third and final block of pre_loop_head_instrs,
405 // with a pragma to disable assigns clause checking.
406 // The variables to store old variant value are local temporaries,
407 // which need not be checked against the enclosing scope's assigns clause.
408 goto_function.body.destructive_insert(
410
411 // Perform write set instrumentation on the entire loop.
412 instrument_spec_assigns.instrument_instructions(
413 goto_function.body,
414 loop_head,
415 loop_end,
416 [&loop](const goto_programt::targett &t) { return loop.contains(t); });
417
418 // Now we begin instrumenting at the loop_end.
419 // `pre_loop_end_instrs` are to be inserted before `loop_end`.
421
422 // Record that we entered the loop.
425
426 // Jump back to the step case to havoc the write set, assume the invariant,
427 // and execute an arbitrary iteration.
430
431 // The following code is only reachable in the step case,
432 // i.e., when in_base_case == false,
433 // because of the unconditional jump above.
434
435 // Generate the inductiveness check:
436 // assert(invariant)
437 // We use a block scope for assertion, since it's immediately goto converted,
438 // and doesn't need to be kept around.
439 {
440 code_assertt assertion{invariant};
442 assertion.add_source_location().set_comment(
443 "Check that loop invariant is preserved");
445 }
446
447 // Generate: assignments to store the multidimensional decreases clause's
448 // value after one iteration of the loop
449 if(!decreases_clause.is_nil())
450 {
451 for(size_t i = 0; i < new_decreases_vars.size(); i++)
452 {
455 new_decreases_assignment.add_source_location() = loop_head_location;
458 }
459
460 // Generate: assertion that the multidimensional decreases clause's value
461 // after the loop is lexicographically smaller than its initial value.
466 monotonic_decreasing_assertion.add_source_location().set_comment(
467 "Check decreases clause on loop iteration");
470
471 // Discard the temporary variables that store decreases clause's value
472 for(size_t i = 0; i < old_decreases_vars.size(); i++)
473 {
478 }
479 }
480
482 goto_function.body,
483 loop_end,
485
486 // change the back edge into assume(false) or assume(guard)
487 loop_end->turn_into_assume();
488 loop_end->condition_nonconst() = boolean_negate(loop_end->condition());
489
490 std::set<goto_programt::targett, goto_programt::target_less_than>
492 // Find all exit points of the loop, make temporary variables `DEAD`,
493 // and check that step case was checked for non-vacuous loops.
494 for(const auto &t : loop)
495 {
496 if(!t->is_goto())
497 continue;
498
499 auto exit_target = t->get_target();
500 if(
501 loop.contains(exit_target) ||
503 continue;
504
506
508 // Assertion to check that step case was checked if we entered the loop.
510 annotated_location.set_comment(
511 "Check that loop instrumentation was not truncated");
515 // Instructions to make all the temporaries go dead.
520 for(const auto &v : history_var_map)
521 {
524 }
525 // Insert these instructions, preserving the loop end target.
527 goto_function.body, exit_target, pre_loop_exit_instrs);
528 }
529}
530
533static void throw_on_unsupported(const goto_programt &program)
534{
535 for(const auto &it : program.instructions)
536 {
537 if(
538 it.is_function_call() && it.call_function().id() == ID_symbol &&
539 to_symbol_expr(it.call_function()).get_identifier() == CPROVER_PREFIX
540 "obeys_contract")
541 {
543 CPROVER_PREFIX "obeys_contract is not supported in this version",
544 it.source_location());
545 }
546 }
547}
548
552 symbol_tablet &symbol_table,
553 goto_convertt &converter,
555 const irep_idt &mode,
556 const std::function<void(goto_programt &)> &is_fresh_update,
557 goto_programt &program,
558 const source_locationt &location)
559{
560 if(
563 {
564 add_quantified_variable(symbol_table, instantiated_clause, mode);
565 }
566
567 goto_programt constraint;
568 if(location.get_property_class() == ID_assume)
569 {
570 converter.goto_convert(code_assumet(instantiated_clause), constraint, mode);
571 }
572 else
573 {
574 converter.goto_convert(code_assertt(instantiated_clause), constraint, mode);
575 }
576 constraint.instructions.back().source_location_nonconst() = location;
577 is_fresh_update(constraint);
578 throw_on_unsupported(constraint);
579 program.destructive_append(constraint);
580}
581
582static const code_with_contract_typet &
583get_contract(const irep_idt &function, const namespacet &ns)
584{
585 const std::string &function_str = id2string(function);
586 const auto &function_symbol = ns.lookup(function);
587
588 const symbolt *contract_sym;
589 if(ns.lookup("contract::" + function_str, contract_sym))
590 {
591 // no contract provided in the source or just an empty assigns clause
593 }
594
595 const auto &type = to_code_with_contract_type(contract_sym->type);
597 type == function_symbol.type,
598 "front-end should have rejected re-declarations with a different type");
599
600 return type;
601}
602
604 const irep_idt &function,
605 const source_locationt &location,
608{
609 const auto &const_target =
610 static_cast<const goto_programt::targett &>(target);
611 // Return if the function is not named in the call; currently we don't handle
612 // function pointers.
613 PRECONDITION(const_target->call_function().id() == ID_symbol);
614
615 const irep_idt &target_function =
616 to_symbol_expr(const_target->call_function()).get_identifier();
617 const symbolt &function_symbol = ns.lookup(target_function);
618 const code_typet &function_type = to_code_type(function_symbol.type);
619
620 // Isolate each component of the contract.
621 const auto &type = get_contract(target_function, ns);
622
623 // Prepare to instantiate expressions in the callee
624 // with expressions from the call site (e.g. the return value).
626
627 // keep track of the call's return expression to make it nondet later
629
630 // if true, the call return variable variable was created during replacement
631 bool call_ret_is_fresh_var = false;
632
633 if(function_type.return_type() != empty_typet())
634 {
635 // Check whether the function's return value is not disregarded.
636 if(target->call_lhs().is_not_nil())
637 {
638 // If so, have it replaced appropriately.
639 // For example, if foo() ensures that its return value is > 5, then
640 // rewrite calls to foo as follows:
641 // x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5)
642 auto &lhs_expr = const_target->call_lhs();
645 }
646 else
647 {
648 // If the function does return a value, but the return value is
649 // disregarded, check if the postcondition includes the return value.
650 if(std::any_of(
651 type.c_ensures().begin(),
652 type.c_ensures().end(),
653 [](const exprt &e) {
654 return has_symbol_expr(
655 to_lambda_expr(e).where(), CPROVER_PREFIX "return_value", true);
656 }))
657 {
658 // The postcondition does mention __CPROVER_return_value, so mint a
659 // fresh variable to replace __CPROVER_return_value with.
662 function_type.return_type(),
663 id2string(target_function),
664 "ignored_return_value",
665 const_target->source_location(),
666 symbol_table.lookup_ref(target_function).mode,
667 ns,
669 auto fresh_sym_expr = fresh.symbol_expr();
672 }
673 else
674 {
675 // unused, add a dummy with the right type
676 instantiation_values.push_back(
677 exprt{ID_nil, function_type.return_type()});
678 }
679 }
680 }
681
682 // Replace formal parameters
683 const auto &arguments = const_target->call_arguments();
685 instantiation_values.end(), arguments.begin(), arguments.end());
686
687 const auto &mode = function_symbol.mode;
688
689 // new program where all contract-derived instructions are added
691
693 goto_model, log.get_message_handler(), target_function);
694 is_fresh.create_declarations();
695 is_fresh.add_memory_map_decl(new_program);
696
697 // Generate: assert(requires)
698 for(const auto &clause : type.c_requires())
699 {
701 to_lambda_expr(clause).application(instantiation_values);
702 source_locationt _location = clause.source_location();
703 _location.set_line(location.get_line());
704 _location.set_comment(std::string("Check requires clause of ")
705 .append(target_function.c_str())
706 .append(" in ")
707 .append(function.c_str()));
708 _location.set_property_class(ID_precondition);
711 converter,
713 mode,
714 [&is_fresh](goto_programt &c_requires) {
715 is_fresh.update_requires(c_requires);
716 },
718 _location);
719 }
720
721 // Generate all the instructions required to initialize history variables
723 for(auto clause : type.c_ensures())
724 {
726 to_lambda_expr(clause).application(instantiation_values);
727 instantiated_clause.add_source_location() = clause.source_location();
731 }
732
733 // ASSIGNS clause should not refer to any quantified variables,
734 // and only refer to the common symbols to be replaced.
735 exprt::operandst targets;
736 for(auto &target : type.c_assigns())
737 targets.push_back(to_lambda_expr(target).application(instantiation_values));
738
739 // Create a sequence of non-deterministic assignments ...
740
741 // ... for the assigns clause targets and static locals
743 function_cfg_infot cfg_info({});
745 target_function,
746 targets,
748 cfg_info,
749 location,
752
753 havocker.get_instructions(havoc_instructions);
754
755 // ... for the return value
756 if(call_ret_opt.has_value())
757 {
758 auto &call_ret = call_ret_opt.value();
759 auto &loc = call_ret.source_location();
760 auto &type = call_ret.type();
761
762 // Declare if fresh
766
767 side_effect_expr_nondett expr(type, location);
769 code_assignt{call_ret, std::move(expr), loc}, loc));
770 }
771
772 // Insert havoc instructions immediately before the call site.
773 new_program.destructive_append(havoc_instructions);
774
775 // Generate: assume(ensures)
776 for(auto &clause : instantiated_ensures_clauses)
777 {
778 if(clause.is_false())
779 {
781 std::string("Attempt to assume false at ")
782 .append(clause.source_location().as_string())
783 .append(".\nPlease update ensures clause to avoid vacuity."));
784 }
785 source_locationt _location = clause.source_location();
786 _location.set_comment("Assume ensures clause");
787 _location.set_property_class(ID_assume);
790 converter,
791 clause,
792 mode,
793 [&is_fresh](goto_programt &ensures) { is_fresh.update_ensures(ensures); },
795 _location);
796 }
797
798 // Kill return value variable if fresh
800 {
802 log.warning(), [&target](messaget::mstreamt &mstream) {
803 target->output(mstream);
804 mstream << messaget::eom;
805 });
806 auto dead_inst =
808 function_body.insert_before_swap(target, dead_inst);
809 ++target;
810 }
811
812 is_fresh.add_memory_map_dead(new_program);
813
814 // Erase original function call
815 *target = goto_programt::make_skip();
816
817 // insert contract replacement instructions
819
820 // Add this function to the set of replaced functions.
821 summarized.insert(target_function);
822
823 // restore global goto_program consistency
825}
826
828 const irep_idt &function_name,
829 goto_functionst::goto_functiont &goto_function)
830{
831 const bool may_have_loops = std::any_of(
832 goto_function.body.instructions.begin(),
833 goto_function.body.instructions.end(),
834 [](const goto_programt::instructiont &instruction) {
835 return instruction.is_backwards_goto();
836 });
837
838 if(!may_have_loops)
839 return;
840
843 goto_functions, function_name, ns, log.get_message_handler());
844
845 INVARIANT(
846 decorated.get_recursive_call_set().size() == 0,
847 "Recursive functions found during inlining");
848
849 // restore internal invariants
851
852 local_may_aliast local_may_alias(goto_function);
853 natural_loops_mutablet natural_loops(goto_function.body);
854
855 // A graph node type that stores information about a loop.
856 // We create a DAG representing nesting of various loops in goto_function,
857 // sort them topologically, and instrument them in the top-sorted order.
858 //
859 // The goal here is not avoid explicit "subset checks" on nested write sets.
860 // When instrumenting in a top-sorted order,
861 // the outer loop would no longer observe the inner loop's write set,
862 // but only corresponding `havoc` statements,
863 // which can be instrumented in the usual way to achieve a "subset check".
864
865 struct loop_graph_nodet : public graph_nodet<empty_edget>
866 {
867 const typename natural_loops_mutablet::loopt &content;
870
872 const typename natural_loops_mutablet::loopt &loop,
873 const goto_programt::targett head,
874 const goto_programt::targett end,
875 const exprt &assigns,
876 const exprt &inv,
877 const exprt &decreases)
878 : content(loop),
879 head_target(head),
880 end_target(end),
881 assigns_clause(assigns),
882 invariant(inv),
883 decreases_clause(decreases)
884 {
885 }
886 };
888
889 std::list<size_t> to_check_contracts_on_children;
890
891 for(const auto &loop_head_and_content : natural_loops.loop_map)
892 {
893 const auto &loop_content = loop_head_and_content.second;
894 // Skip empty loops and self-looped node.
895 if(loop_content.size() <= 1)
896 continue;
897
898 auto loop_head = loop_head_and_content.first;
899 auto loop_end = loop_head;
900
901 // Find the last back edge to `loop_head`
902 for(const auto &t : loop_content)
903 {
904 if(
905 t->is_goto() && t->get_target() == loop_head &&
906 t->location_number > loop_end->location_number)
907 loop_end = t;
908 }
909
910 if(loop_end == loop_head)
911 {
912 log.error() << "Could not find end of the loop starting at: "
913 << loop_head->source_location() << messaget::eom;
914 throw 0;
915 }
916
917 // After loop-contract instrumentation, jumps to the `loop_head` will skip
918 // some instrumented instructions. So we want to make sure that there is
919 // only one jump targeting `loop_head` from `loop_end` before loop-contract
920 // instrumentation.
921 // Add a skip before `loop_head` and let all jumps (except for the
922 // `loop_end`) that target to the `loop_head` target to the skip
923 // instead.
925 goto_function.body, loop_head, goto_programt::make_skip());
926 loop_end->set_target(loop_head);
927
929 static_cast<const exprt &>(loop_end->condition().find(ID_C_spec_assigns));
930 exprt invariant = static_cast<const exprt &>(
931 loop_end->condition().find(ID_C_spec_loop_invariant));
932 exprt decreases_clause = static_cast<const exprt &>(
933 loop_end->condition().find(ID_C_spec_decreases));
934
935 if(invariant.is_nil())
936 {
937 if(decreases_clause.is_not_nil() || assigns_clause.is_not_nil())
938 {
939 invariant = true_exprt{};
940 // assigns clause is missing; we will try to automatic inference
941 log.warning()
942 << "The loop at " << loop_head->source_location().as_string()
943 << " does not have an invariant in its contract.\n"
944 << "Hence, a default invariant ('true') is being used.\n"
945 << "This choice is sound, but verification may fail"
946 << " if it is be too weak to prove the desired properties."
947 << messaget::eom;
948 }
949 }
950 else
951 {
952 invariant = conjunction(invariant.operands());
953 if(decreases_clause.is_nil())
954 {
955 log.warning() << "The loop at "
956 << loop_head->source_location().as_string()
957 << " does not have a decreases clause in its contract.\n"
958 << "Termination of this loop will not be verified."
959 << messaget::eom;
960 }
961 }
962
963 const auto idx = loop_nesting_graph.add_node(
965 loop_head,
966 loop_end,
968 invariant,
970
971 if(
972 assigns_clause.is_nil() && invariant.is_nil() &&
973 decreases_clause.is_nil())
974 continue;
975
976 to_check_contracts_on_children.push_back(idx);
977
978 // By definition the `loop_content` is a set of instructions computed
979 // by `natural_loops` based on the CFG.
980 // Since we perform assigns clause instrumentation by sequentially
981 // traversing instructions from `loop_head` to `loop_end`,
982 // here we ensure that all instructions in `loop_content` belong within
983 // the [loop_head, loop_end] target range
984
985 // Check 1. (i \in loop_content) ==> loop_head <= i <= loop_end
986 for(const auto &i : loop_content)
987 {
988 if(std::distance(loop_head, i) < 0 || std::distance(i, loop_end) < 0)
989 {
991 log.error(), [&i, &loop_head](messaget::mstreamt &mstream) {
992 mstream << "Computed loop at " << loop_head->source_location()
993 << "contains an instruction beyond [loop_head, loop_end]:"
994 << messaget::eom;
995 i->output(mstream);
996 mstream << messaget::eom;
997 });
998 throw 0;
999 }
1000 }
1001 }
1002
1003 for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer)
1004 {
1005 for(size_t inner = 0; inner < loop_nesting_graph.size(); ++inner)
1006 {
1007 if(inner == outer)
1008 continue;
1009
1010 if(loop_nesting_graph[outer].content.contains(
1011 loop_nesting_graph[inner].head_target))
1012 {
1013 if(!loop_nesting_graph[outer].content.contains(
1014 loop_nesting_graph[inner].end_target))
1015 {
1016 log.error()
1017 << "Overlapping loops at:\n"
1018 << loop_nesting_graph[outer].head_target->source_location()
1019 << "\nand\n"
1020 << loop_nesting_graph[inner].head_target->source_location()
1021 << "\nLoops must be nested or sequential for contracts to be "
1022 "enforced."
1023 << messaget::eom;
1024 }
1025 loop_nesting_graph.add_edge(inner, outer);
1026 }
1027 }
1028 }
1029
1030 // make sure all children of a contractified loop also have contracts
1031 while(!to_check_contracts_on_children.empty())
1032 {
1033 const auto loop_idx = to_check_contracts_on_children.front();
1035
1036 const auto &loop_node = loop_nesting_graph[loop_idx];
1037 if(
1038 loop_node.assigns_clause.is_nil() && loop_node.invariant.is_nil() &&
1039 loop_node.decreases_clause.is_nil())
1040 {
1041 log.error()
1042 << "Inner loop at: " << loop_node.head_target->source_location()
1043 << " does not have contracts, but an enclosing loop does.\n"
1044 << "Please provide contracts for this loop, or unwind it first."
1045 << messaget::eom;
1046 throw 0;
1047 }
1048
1049 for(const auto child_idx : loop_nesting_graph.get_predecessors(loop_idx))
1051 }
1052
1053 // Iterate over the (natural) loops in the function, in topo-sorted order,
1054 // and apply any loop contracts that we find.
1055 for(const auto &idx : loop_nesting_graph.topsort())
1056 {
1057 const auto &loop_node = loop_nesting_graph[idx];
1058 if(
1059 loop_node.assigns_clause.is_nil() && loop_node.invariant.is_nil() &&
1060 loop_node.decreases_clause.is_nil())
1061 continue;
1062
1063 // Computed loop "contents" needs to be refreshed to include any newly
1064 // introduced instrumentation, e.g. havoc instructions for assigns clause,
1065 // on inner loops in to the outer loop's contents.
1066 // Else, during the outer loop instrumentation these instructions will be
1067 // "masked" just as any other instruction not within its "contents."
1068
1070 natural_loops_mutablet updated_loops(goto_function.body);
1071
1072 // We will unwind all transformed loops twice. Store the names of
1073 // to-unwind-loops here and perform the unwinding after transformation done.
1074 // As described in `check_apply_loop_contracts`, loops with loop contracts
1075 // will be transformed to a loop that execute exactly twice: one for base
1076 // case and one for step case. So we unwind them here to avoid users
1077 // incorrectly unwind them only once.
1078 std::string to_unwind = id2string(function_name) + "." +
1079 std::to_string(loop_node.end_target->loop_number) +
1080 ":2";
1081 loop_names.push_back(to_unwind);
1082
1084 function_name,
1085 goto_function,
1086 local_may_alias,
1087 loop_node.head_target,
1088 loop_node.end_target,
1089 updated_loops.loop_map[loop_node.head_target],
1090 loop_node.assigns_clause,
1091 loop_node.invariant,
1092 loop_node.decreases_clause,
1093 symbol_table.lookup_ref(function_name).mode);
1094 }
1095}
1096
1098{
1099 // Get the function object before instrumentation.
1100 auto function_obj = goto_functions.function_map.find(function);
1101
1102 INVARIANT(
1104 "Function '" + id2string(function) + "'must exist in the goto program");
1105
1106 const auto &goto_function = function_obj->second;
1107 auto &function_body = function_obj->second.body;
1108
1109 function_cfg_infot cfg_info(goto_function);
1110
1112 function,
1114 cfg_info,
1117
1118 // Detect and track static local variables before inlining
1121
1122 // Full inlining of the function body
1123 // Inlining is performed so that function calls to a same function
1124 // occurring under different write sets get instrumented specifically
1125 // for each write set
1128
1129 decorated.throw_on_recursive_calls(log, 0);
1130
1131 // Clean up possible fake loops that are due to `IF 0!=0 GOTO i` instructions
1133
1134 // Restore internal coherence in the programs
1136
1137 INVARIANT(
1139 "Loops remain in function '" + id2string(function) +
1140 "', assigns clause checking instrumentation cannot be applied.");
1141
1142 // Start instrumentation
1143 auto instruction_it = function_body.instructions.begin();
1144
1145 // Inject local static snapshots
1148
1149 // Track targets mentioned in the specification
1150 const symbolt &function_symbol = ns.lookup(function);
1151 const code_typet &function_type = to_code_type(function_symbol.type);
1153 // assigns clauses cannot refer to the return value, but we still need an
1154 // element in there to apply the lambda function consistently
1155 if(function_type.return_type() != empty_typet())
1156 instantiation_values.push_back(exprt{ID_nil, function_type.return_type()});
1157 for(const auto &param : function_type.parameters())
1158 {
1159 instantiation_values.push_back(
1160 ns.lookup(param.get_identifier()).symbol_expr());
1161 }
1162 for(auto &target : get_contract(function, ns).c_assigns())
1163 {
1165 instrument_spec_assigns.track_spec_target(
1166 to_lambda_expr(target).application(instantiation_values), payload);
1168 }
1169
1170 // Track formal parameters
1172 for(const auto &param : function_type.parameters())
1173 {
1175 instrument_spec_assigns.track_stack_allocated(
1176 ns.lookup(param.get_identifier()).symbol_expr(), payload);
1178 }
1179
1180 // Restore internal coherence in the programs
1182
1183 // Insert write set inclusion checks.
1184 instrument_spec_assigns.instrument_instructions(
1185 function_body, instruction_it, function_body.instructions.end());
1186}
1187
1189{
1190 // Add statements to the source function
1191 // to ensure assigns clause is respected.
1193
1194 // Rename source function
1195 std::stringstream ss;
1196 ss << CPROVER_PREFIX << "contracts_original_" << function;
1197 const irep_idt mangled(ss.str());
1198 const irep_idt original(function);
1199
1201 INVARIANT(
1203 "Function to replace must exist in the program.");
1204
1205 std::swap(goto_functions.function_map[mangled], old_function->second);
1207
1208 // Place a new symbol with the mangled name into the symbol table
1210 sl.set_file("instrumented for code contracts");
1211 sl.set_line("0");
1214 mangled_sym.name = mangled;
1215 mangled_sym.base_name = mangled;
1216 mangled_sym.location = sl;
1217 const auto mangled_found = symbol_table.insert(std::move(mangled_sym));
1218 INVARIANT(
1219 mangled_found.second,
1220 "There should be no existing function called " + ss.str() +
1221 " in the symbol table because that name is a mangled name");
1222
1223 // Insert wrapper function into goto_functions
1225 INVARIANT(
1227 "There should be no function called " + id2string(function) +
1228 " in the function map because that function should have had its"
1229 " name mangled");
1230
1232 INVARIANT(
1234 "There should be a function called " + ss.str() +
1235 " in the function map because we inserted a fresh goto-program"
1236 " with that mangled name");
1237
1239 wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers;
1242}
1243
1247 goto_programt &dest)
1248{
1249 PRECONDITION(!dest.instructions.empty());
1250
1251 // build:
1252 // decl ret
1253 // decl parameter1 ...
1254 // decl history_parameter1 ... [optional]
1255 // assume(requires) [optional]
1256 // ret=function(parameter1, ...)
1257 // assert(ensures)
1258
1259 const auto &code_type = get_contract(wrapper_function, ns);
1260 goto_programt check;
1261
1262 // prepare function call including all declarations
1265
1266 // Prepare to instantiate expressions in the callee
1267 // with expressions from the call site (e.g. the return value).
1269
1270 source_locationt source_location = function_symbol.location;
1271 // Set function in source location to original function
1272 source_location.set_function(wrapper_function);
1273
1274 // decl ret
1276 if(code_type.return_type() != empty_typet())
1277 {
1279 code_type.return_type(),
1280 id2string(source_location.get_function()),
1281 "tmp_cc",
1282 source_location,
1283 function_symbol.mode,
1285 .symbol_expr();
1286 check.add(goto_programt::make_decl(r, source_location));
1287
1288 call.lhs() = r;
1290
1291 instantiation_values.push_back(r);
1292 }
1293
1294 // decl parameter1 ...
1295 goto_functionst::function_mapt::iterator f_it =
1298
1299 const goto_functionst::goto_functiont &gf = f_it->second;
1300 for(const auto &parameter : gf.parameter_identifiers)
1301 {
1302 PRECONDITION(!parameter.empty());
1305 parameter_symbol.type,
1306 id2string(source_location.get_function()),
1307 "tmp_cc",
1308 source_location,
1309 parameter_symbol.mode,
1311 .symbol_expr();
1312 check.add(goto_programt::make_decl(p, source_location));
1314 p, parameter_symbol.symbol_expr(), source_location));
1315
1316 call.arguments().push_back(p);
1317
1318 instantiation_values.push_back(p);
1319 }
1320
1323 visitor.create_declarations();
1324 visitor.add_memory_map_decl(check);
1325
1326 // Generate: assume(requires)
1327 for(const auto &clause : code_type.c_requires())
1328 {
1329 auto instantiated_clause =
1330 to_lambda_expr(clause).application(instantiation_values);
1331 if(instantiated_clause.is_false())
1332 {
1334 std::string("Attempt to assume false at ")
1335 .append(clause.source_location().as_string())
1336 .append(".\nPlease update requires clause to avoid vacuity."));
1337 }
1338 source_locationt _location = clause.source_location();
1339 _location.set_comment("Assume requires clause");
1340 _location.set_property_class(ID_assume);
1343 converter,
1345 function_symbol.mode,
1346 [&visitor](goto_programt &c_requires) {
1347 visitor.update_requires(c_requires);
1348 },
1349 check,
1350 _location);
1351 }
1352
1353 // Generate all the instructions required to initialize history variables
1355 for(auto clause : code_type.c_ensures())
1356 {
1357 auto instantiated_clause =
1358 to_lambda_expr(clause).application(instantiation_values);
1359 instantiated_clause.add_source_location() = clause.source_location();
1363 }
1364
1365 // ret=mangled_function(parameter1, ...)
1366 check.add(goto_programt::make_function_call(call, source_location));
1367
1368 // Generate: assert(ensures)
1369 for(auto &clause : instantiated_ensures_clauses)
1370 {
1371 source_locationt _location = clause.source_location();
1372 _location.set_comment("Check ensures clause");
1373 _location.set_property_class(ID_postcondition);
1376 converter,
1377 clause,
1378 function_symbol.mode,
1379 [&visitor](goto_programt &ensures) { visitor.update_ensures(ensures); },
1380 check,
1381 _location);
1382 }
1383
1384 if(code_type.return_type() != empty_typet())
1385 {
1387 return_stmt.value().return_value(), source_location));
1388 }
1389
1390 // kill the is_fresh memory map
1391 visitor.add_memory_map_dead(check);
1392
1393 // prepend the new code to dest
1394 dest.destructive_insert(dest.instructions.begin(), check);
1395
1396 // restore global goto_program consistency
1398}
1399
1401 const std::set<std::string> &functions) const
1402{
1403 for(const auto &function : functions)
1404 {
1405 if(
1406 goto_functions.function_map.find(function) ==
1408 {
1410 "Function '" + function + "' was not found in the GOTO program.");
1411 }
1412 }
1413}
1414
1415void code_contractst::replace_calls(const std::set<std::string> &to_replace)
1416{
1417 if(to_replace.empty())
1418 return;
1419
1420 log.status() << "Replacing function calls with contracts" << messaget::eom;
1421
1422 check_all_functions_found(to_replace);
1423
1424 for(auto &goto_function : goto_functions.function_map)
1425 {
1426 Forall_goto_program_instructions(ins, goto_function.second.body)
1427 {
1428 if(ins->is_function_call())
1429 {
1430 if(ins->call_function().id() != ID_symbol)
1431 continue;
1432
1433 const irep_idt &called_function =
1434 to_symbol_expr(ins->call_function()).get_identifier();
1435 auto found = std::find(
1436 to_replace.begin(), to_replace.end(), id2string(called_function));
1437 if(found == to_replace.end())
1438 continue;
1439
1441 goto_function.first,
1442 ins->source_location(),
1443 goto_function.second.body,
1444 ins);
1445 }
1446 }
1447 }
1448
1449 for(auto &goto_function : goto_functions.function_map)
1450 remove_skip(goto_function.second.body);
1451
1453}
1454
1456 const std::set<std::string> &to_exclude_from_nondet_init)
1457{
1458 for(auto &goto_function : goto_functions.function_map)
1459 apply_loop_contract(goto_function.first, goto_function.second);
1460
1461 log.status() << "Adding nondeterministic initialization "
1462 "of static/global variables."
1463 << messaget::eom;
1465
1466 // unwind all transformed loops twice.
1468 {
1469 unwindsett unwindset{goto_model};
1470 unwindset.parse_unwindset(loop_names, log.get_message_handler());
1473 }
1474
1476
1477 // Record original loop number for some instrumented instructions.
1479 {
1480 auto &goto_function = goto_function_entry.second;
1481 bool is_in_loop_havoc_block = false;
1482
1483 unsigned loop_number_of_loop_havoc = 0;
1485 goto_function.body.instructions.begin();
1486 it_instr != goto_function.body.instructions.end();
1487 it_instr++)
1488 {
1489 // Don't override original loop numbers.
1490 if(original_loop_number_map.count(it_instr) != 0)
1491 continue;
1492
1493 // Store loop number for two type of instrumented instructions.
1494 // ASSIGN ENTERED_LOOP = false --- head of transformed loops.
1495 // ASSIGN ENTERED_LOOP = true --- end of transformed loops.
1496 if(
1498 {
1499 const auto &assign_lhs =
1502 id2string(assign_lhs->get_identifier()),
1503 std::string(ENTERED_LOOP) + "__");
1504 continue;
1505 }
1506
1507 // Loop havocs are assignments between
1508 // ASSIGN IN_LOOP_HAVOC_BLOCK = true
1509 // and
1510 // ASSIGN IN_LOOP_HAVOC_BLOCK = false
1511
1512 // Entering the loop-havoc block.
1514 {
1515 is_in_loop_havoc_block = it_instr->assign_rhs() == true_exprt();
1516 const auto &assign_lhs =
1519 id2string(assign_lhs->get_identifier()),
1520 std::string(IN_LOOP_HAVOC_BLOCK) + "__");
1521 continue;
1522 }
1523
1524 // Assignments in loop-havoc block are loop havocs.
1525 if(is_in_loop_havoc_block && it_instr->is_assign())
1526 {
1527 loop_havoc_set.emplace(it_instr);
1528
1529 // Store loop number for loop havoc.
1531 }
1532 }
1533 }
1534}
1535
1537 const std::set<std::string> &to_enforce,
1538 const std::set<std::string> &to_exclude_from_nondet_init)
1539{
1540 if(to_enforce.empty())
1541 return;
1542
1543 log.status() << "Enforcing contracts" << messaget ::eom;
1544
1546
1547 for(const auto &function : to_enforce)
1548 enforce_contract(function);
1549
1550 log.status() << "Adding nondeterministic initialization "
1551 "of static/global variables."
1552 << messaget::eom;
1554}
API to expression classes that are internal to the C frontend.
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Definition c_types.h:467
Classes providing CFG-based information about symbols to guide simplifications in function and loop a...
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
The Boolean type.
Definition std_types.h:36
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition std_code.h:270
A goto_instruction_codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
Definition std_code.h:217
namespacet ns
Definition contracts.h:142
void apply_function_contract(const irep_idt &function, const source_locationt &location, goto_programt &function_body, goto_programt::targett &target)
Replaces function calls with assertions based on requires clauses, non-deterministic assignments for ...
void enforce_contract(const irep_idt &function)
Enforce contract of a single function.
goto_modelt & goto_model
Definition contracts.h:148
void check_apply_loop_contracts(const irep_idt &function_name, goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, goto_programt::targett loop_end, const loopt &loop, exprt assigns_clause, exprt invariant, exprt decreases_clause, const irep_idt &mode)
Definition contracts.cpp:49
void apply_loop_contract(const irep_idt &function, goto_functionst::goto_functiont &goto_function)
Apply loop contracts, whenever available, to all loops in function.
void check_all_functions_found(const std::set< std::string > &functions) const
Throws an exception if some function functions is found in the program.
void check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
messaget & log
Definition contracts.h:152
void apply_loop_contracts(const std::set< std::string > &to_exclude_from_nondet_init={})
Applies loop contract transformations.
symbol_tablet & symbol_table
Definition contracts.h:149
void enforce_contracts(const std::set< std::string > &to_enforce, const std::set< std::string > &to_exclude_from_nondet_init={})
Turn requires & ensures into assumptions and assertions for each of the named functions.
void replace_calls(const std::set< std::string > &to_replace)
Replace all calls to each function in the to_replace set with that function's contract.
std::unordered_set< irep_idt > summarized
Definition contracts.h:155
goto_convertt converter
Definition contracts.h:153
std::unordered_set< goto_programt::const_targett, const_target_hash > loop_havoc_set
Loop havoc instructions instrumented during applying loop contracts.
Definition contracts.h:169
std::list< std::string > loop_names
Name of loops we are going to unwind.
Definition contracts.h:158
goto_functionst & goto_functions
Definition contracts.h:150
std::unordered_map< goto_programt::const_targett, unsigned, const_target_hash > original_loop_number_map
Store the map from instrumented instructions for loop contracts to their original loop numbers.
Definition contracts.h:165
void add_contract_check(const irep_idt &wrapper_function, const irep_idt &mangled_function, goto_programt &dest)
Instruments wrapper_function adding assumptions based on requires clauses and assertions based on ens...
bool unwind_transformed_loops
Definition contracts.h:145
goto_instruction_codet representation of a function call statement.
goto_instruction_codet representation of a "return from a function" statement.
Base type of functions.
Definition std_types.h:539
const parameterst & parameters() const
Definition std_types.h:655
const typet & return_type() const
Definition std_types.h:645
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
const char * c_str() const
Definition dstring.h:117
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
operandst & operands()
Definition expr.h:94
source_locationt & add_source_location()
Definition expr.h:228
The Boolean constant false.
Definition std_expr.h:3017
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
instructionst::const_iterator const_targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
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())
This class represents a node in a directed graph.
Definition graph.h:35
Class to generate havocking instructions for target expressions of a function contract's assign claus...
A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_obje...
Definition utils.h:87
Decorator for a message_handlert used during function inlining that collect names of GOTO functions c...
A class that generates instrumentation for assigns clause checking.
Thrown when user-provided input cannot be processed.
Thrown when we can't handle something in an input source file.
void swap(irept &irep)
Definition irep.h:442
bool is_nil() const
Definition irep.h:376
loop_mapt loop_map
void erase_locals(std::set< exprt > &exprs)
Definition cfg_info.h:171
mstreamt & error() const
Definition message.h:399
mstreamt & debug() const
Definition message.h:429
message_handlert & get_message_handler()
Definition message.h:184
mstreamt & warning() const
Definition message.h:404
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
Definition message.cpp:139
static eomt eom
Definition message.h:297
mstreamt & status() const
Definition message.h:414
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Boolean negation.
Definition std_expr.h:2278
Boolean OR.
Definition std_expr.h:2179
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
const irep_idt & get_function() const
const irep_idt & get_line() const
const irep_idt & get_property_class() const
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
Definition std_expr.h:113
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition symbol.h:28
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 void generate_contract_constraints(symbol_tablet &symbol_table, goto_convertt &converter, exprt &instantiated_clause, const irep_idt &mode, const std::function< void(goto_programt &)> &is_fresh_update, goto_programt &program, const source_locationt &location)
This function generates instructions for all contract constraint, i.e., assumptions and assertions ba...
static const code_with_contract_typet & get_contract(const irep_idt &function, const namespacet &ns)
static void throw_on_unsupported(const goto_programt &program)
Throws an exception if a contract uses unsupported constructs like:
Verify and use annotated invariants and pre/post-conditions.
#define CPROVER_PREFIX
static const exprt::operandst & get_assigns(const goto_programt::const_targett &latch_target)
Extracts the assigns clause expression from the latch condition.
static const std::map< dfcc_funt, int > to_unwind
set of functions that need to be unwound to assigns clause size with corresponding loop identifiers.
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
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.
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Transitively inline all function calls made from a particular function.
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
Concrete Goto Program.
#define Forall_goto_program_instructions(it, program)
A Template Class for Graphs.
Havoc function assigns clauses.
Utilities for building havoc code for expressions.
std::set< exprt > assignst
Definition havoc_utils.h:24
optionalt< code_with_contract_typet > get_contract(const irep_idt &function_identifier, const namespacet &ns)
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:47
static int8_t r
Definition irep_hash.h:60
Field-insensitive, location-sensitive may-alias analysis.
natural_loops_mutablet::natural_loopt loopt
Definition loop_utils.h:20
API to expression classes for 'mathematical' expressions.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
Predicates to specify memory footprint in function contracts.
static void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:63
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
Loop unwinding.
Loop unwinding.
void generate_history_variables_initialization(symbol_table_baset &symbol_table, exprt &clause, const irep_idt &mode, goto_programt &program)
This function generates all the instructions required to initialize history variables.
Definition utils.cpp:549
bool is_assignment_to_instrumented_variable(const goto_programt::const_targett &target, std::string var_name)
Return true if target is an assignment to an instrumented variable with name var_name.
Definition utils.cpp:579
void insert_before_and_update_jumps(goto_programt &destination, goto_programt::targett &target, const goto_programt::instructiont &i)
Insert a goto instruction before a target instruction iterator and update targets of all jumps that p...
Definition utils.cpp:244
void add_quantified_variable(symbol_table_baset &symbol_table, exprt &expression, const irep_idt &mode)
This function recursively searches expression to find nested or non-nested quantified expressions.
Definition utils.cpp:367
bool is_loop_free(const goto_programt &goto_program, namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.
Definition utils.cpp:268
replace_history_parametert replace_history_loop_entry(symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode)
This function recursively identifies the "loop_entry" expressions within expr and replaces them with ...
Definition utils.cpp:530
bool is_transformed_loop_head(const goto_programt::const_targett &target)
Return true if target is the head of some transformed loop.
Definition utils.cpp:563
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
void widen_assigns(assignst &assigns, const namespacet &ns)
Widen expressions in assigns with the following strategy.
Definition utils.cpp:341
bool is_transformed_loop_end(const goto_programt::const_targett &target)
Return true if target is the end of some transformed loop.
Definition utils.cpp:571
void simplify_gotos(goto_programt &goto_program, namespacet &ns)
Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SK...
Definition utils.cpp:257
unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix)
Convert the suffix digits right after prefix of str into unsigned.
Definition utils.cpp:601
exprt generate_lexicographic_less_than_check(const std::vector< symbol_exprt > &lhs, const std::vector< symbol_exprt > &rhs)
Generate a lexicographic less-than comparison over ordered tuples.
Definition utils.cpp:190
#define ENTERED_LOOP
Definition utils.h:24
#define INIT_INVARIANT
Definition utils.h:26
#define IN_LOOP_HAVOC_BLOCK
Definition utils.h:25