CBMC
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>
17#include <util/format_expr.h>
18#include <util/fresh_symbol.h>
20
24
28
29#include "cfg_info.h"
31#include "inlining_decorator.h"
33#include "memory_predicates.h"
34#include "utils.h"
35
36#include <algorithm>
37#include <map>
38
40 const irep_idt &function_name,
42 const local_may_aliast &local_may_alias,
45 const loopt &loop,
47 exprt invariant,
49 const irep_idt &mode)
50{
51 const auto loop_head_location = loop_head->source_location();
52 const auto loop_number = loop_end->loop_number;
53
54 // Vector representing a (possibly multidimensional) decreases clause
55 const auto &decreases_clause_exprs = decreases_clause.operands();
56
57 // Temporary variables for storing the multidimensional decreases clause
58 // at the start of and end of a loop body
59 std::vector<symbol_exprt> old_decreases_vars, new_decreases_vars;
60
61 // instrument
62 //
63 // ... preamble ...
64 // HEAD:
65 // ... eval guard ...
66 // if (!guard)
67 // goto EXIT;
68 // ... loop body ...
69 // goto HEAD;
70 // EXIT:
71 // ... postamble ...
72 //
73 // to
74 //
75 // ... preamble ...
76 // ,- initialize loop_entry history vars;
77 // | entered_loop = false
78 // loop assigns check | initial_invariant_val = invariant_expr;
79 // - unchecked, temps | in_base_case = true;
80 // func assigns check | snapshot (write_set);
81 // - disabled via pragma | goto HEAD;
82 // | STEP:
83 // --. | assert (initial_invariant_val);
84 // loop assigns check | | in_base_case = false;
85 // - not applicable >======= in_loop_havoc_block = true;
86 // func assigns check | | havoc (assigns_set);
87 // + deferred | | in_loop_havoc_block = false;
88 // --' | assume (invariant_expr);
89 // `- old_variant_val = decreases_clause_expr;
90 // * HEAD:
91 // loop assigns check ,- ... eval guard ...
92 // + assertions added | if (!guard)
93 // func assigns check | goto EXIT;
94 // - disabled via pragma `- ... loop body ...
95 // ,- entered_loop = true
96 // | if (in_base_case)
97 // | goto STEP;
98 // loop assigns check | assert (invariant_expr);
99 // - unchecked, temps | new_variant_val = decreases_clause_expr;
100 // func assigns check | assert (new_variant_val < old_variant_val);
101 // - disabled via pragma | dead old_variant_val, new_variant_val;
102 // | * assume (false);
103 // | * EXIT:
104 // To be inserted at ,~~~|~~~~ assert (entered_loop ==> !in_base_case);
105 // every unique EXIT | | dead loop_entry history vars, in_base_case;
106 // (break, goto etc.) `~~~`- ~~ dead initial_invariant_val, entered_loop;
107 // ... postamble ..
108 //
109 // Asterisks (*) denote anchor points (goto targets) for instrumentations.
110 // We insert generated code above and/below these targets.
111 //
112 // Assertions for assigns clause checking are inserted in the loop body.
113
114 // Process "loop_entry" history variables.
115 // We find and replace all "__CPROVER_loop_entry" subexpressions in invariant.
117 symbol_table, invariant, loop_head_location, mode);
118 invariant.swap(replace_history_result.expression_after_replacement);
119 const auto &history_var_map = replace_history_result.parameter_to_history;
120 // an intermediate goto_program to store generated instructions
121 // to be inserted before the loop head
123 replace_history_result.history_construction;
124
125 // Create a temporary to track if we entered the loop,
126 // i.e., the loop guard was satisfied.
127 const auto entered_loop =
129 bool_typet(),
130 id2string(loop_head_location.get_function()),
131 std::string(ENTERED_LOOP) + "__" + std::to_string(loop_number),
133 mode,
135 .symbol_expr();
140
141 // Create a snapshot of the invariant so that we can check the base case,
142 // if the loop is not vacuous and must be abstracted with contracts.
143 const auto initial_invariant_val =
145 bool_typet(),
146 id2string(loop_head_location.get_function()),
149 mode,
151 .symbol_expr();
154 {
155 // Although the invariant at this point will not have side effects,
156 // it is still a C expression, and needs to be "goto_convert"ed.
157 // Note that this conversion may emit many GOTO instructions.
159 initial_invariant_val, invariant};
160 initial_invariant_value_assignment.add_source_location() =
162
164 converter.goto_convert(
166 }
167
168 // Create a temporary variable to track base case vs inductive case
169 // instrumentation of the loop.
171 bool_typet(),
172 id2string(loop_head_location.get_function()),
173 "__in_base_case",
175 mode,
177 .symbol_expr();
182
183 // CAR snapshot instructions for checking assigns clause
185
186 loop_cfg_infot cfg_info(goto_function, loop);
187
188 // track static local symbols
190 function_name,
192 cfg_info,
195
196 instrument_spec_assigns.track_static_locals_between(
198
199 // set of targets to havoc
201
202 if(assigns_clause.is_nil())
203 {
204 // No assigns clause was specified for this loop.
205 // Infer memory locations assigned by the loop from the loop instructions
206 // and the inferred aliasing relation.
207 try
208 {
209 infer_loop_assigns(local_may_alias, loop, to_havoc);
210
211 // remove loop-local symbols from the inferred set
212 cfg_info.erase_locals(to_havoc);
213
214 // If the set contains pairs (i, a[i]),
215 // we widen them to (i, __CPROVER_POINTER_OBJECT(a))
217
218 log.debug() << "No loop assigns clause provided. Inferred targets: {";
219 // Add inferred targets to the loop assigns clause.
220 bool ran_once = false;
221 for(const auto &target : to_havoc)
222 {
223 if(ran_once)
224 log.debug() << ", ";
225 ran_once = true;
226 log.debug() << format(target);
227 instrument_spec_assigns.track_spec_target(
228 target, snapshot_instructions);
229 }
230 log.debug() << "}" << messaget::eom;
231
232 instrument_spec_assigns.get_static_locals(
233 std::inserter(to_havoc, to_havoc.end()));
234 }
235 catch(const analysis_exceptiont &exc)
236 {
237 log.error() << "Failed to infer variables being modified by the loop at "
239 << ".\nPlease specify an assigns clause.\nReason:"
240 << messaget::eom;
241 throw exc;
242 }
243 }
244 else
245 {
246 // An assigns clause was specified for this loop.
247 // Add the targets to the set of expressions to havoc.
248 for(const auto &target : assigns_clause.operands())
249 {
250 to_havoc.insert(target);
251 instrument_spec_assigns.track_spec_target(target, snapshot_instructions);
252 }
253 }
254
255 // Insert instrumentation
256 // This must be done before havocing the write set.
257 // FIXME: this is not true for write set targets that
258 // might depend on other write set targets.
260
261 // Insert a jump to the loop head
262 // (skipping over the step case initialization code below)
265
266 // The STEP case instructions follow.
267 // We skip past it initially, because of the unconditional jump above,
268 // but jump back here if we get past the loop guard while in_base_case.
269
270 const auto step_case_target =
273
274 // If we jump here, then the loop runs at least once,
275 // so add the base case assertion:
276 // assert(initial_invariant_val)
277 // We use a block scope for assertion, since it's immediately goto converted,
278 // and doesn't need to be kept around.
279 {
281 assertion.add_source_location() = loop_head_location;
282 assertion.add_source_location().set_comment(
283 "Check loop invariant before entry");
284
286 converter.goto_convert(assertion, pre_loop_head_instrs, mode);
287 }
288
289 // Insert the first block of pre_loop_head_instrs,
290 // with a pragma to disable assigns clause checking.
291 // All of the initialization code so far introduces local temporaries,
292 // which need not be checked against the enclosing scope's assigns clause.
293 goto_function.body.destructive_insert(
295
296 // Generate havocing code for assignment targets.
297 // ASSIGN in_loop_havoc_block = true;
298 // havoc (assigns_set);
299 // ASSIGN in_loop_havoc_block = false;
300 const auto in_loop_havoc_block =
302 bool_typet(),
303 id2string(loop_head_location.get_function()),
304 std::string(IN_LOOP_HAVOC_BLOCK) + +"__" + std::to_string(loop_number),
306 mode,
308 .symbol_expr();
315 havoc_gen.append_full_havoc_code(loop_head_location, pre_loop_head_instrs);
318
319 // Insert the second block of pre_loop_head_instrs: the havocing code.
320 // We do not `add_pragma_disable_assigns_check`,
321 // so that the enclosing scope's assigns clause instrumentation
322 // would pick these havocs up for inclusion (subset) checks.
323 goto_function.body.destructive_insert(loop_head, pre_loop_head_instrs);
324
325 // Generate: assume(invariant) just after havocing
326 // We use a block scope for assumption, since it's immediately goto converted,
327 // and doesn't need to be kept around.
328 {
329 code_assumet assumption{invariant};
331
333 converter.goto_convert(assumption, pre_loop_head_instrs, mode);
334 }
335
336 // Create fresh temporary variables that store the multidimensional
337 // decreases clause's value before and after the loop
338 for(const auto &clause : decreases_clause.operands())
339 {
340 const auto old_decreases_var =
342 clause.type(),
343 id2string(loop_head_location.get_function()),
344 "tmp_cc",
346 mode,
348 .symbol_expr();
352
353 const auto new_decreases_var =
355 clause.type(),
356 id2string(loop_head_location.get_function()),
357 "tmp_cc",
359 mode,
361 .symbol_expr();
365 }
366
367 // TODO: Fix loop contract handling for do/while loops.
368 if(loop_end->is_goto() && !loop_end->condition().is_true())
369 {
370 log.error() << "Loop contracts are unsupported on do/while loops: "
372 throw 0;
373
374 // non-deterministically skip the loop if it is a do-while loop.
375 // pre_loop_head_instrs.add(goto_programt::make_goto(
376 // loop_end, side_effect_expr_nondett(bool_typet(), loop_head_location)));
377 }
378
379 // Generate: assignments to store the multidimensional decreases clause's
380 // value just before the loop_head
381 if(!decreases_clause.is_nil())
382 {
383 for(size_t i = 0; i < old_decreases_vars.size(); i++)
384 {
387 old_decreases_assignment.add_source_location() = loop_head_location;
388
390 converter.goto_convert(
392 }
393
394 goto_function.body.destructive_insert(
396 }
397
398 // Insert the third and final block of pre_loop_head_instrs,
399 // with a pragma to disable assigns clause checking.
400 // The variables to store old variant value are local temporaries,
401 // which need not be checked against the enclosing scope's assigns clause.
402 goto_function.body.destructive_insert(
404
405 // Perform write set instrumentation on the entire loop.
406 instrument_spec_assigns.instrument_instructions(
407 goto_function.body,
408 loop_head,
409 loop_end,
410 [&loop](const goto_programt::targett &t) { return loop.contains(t); });
411
412 // Now we begin instrumenting at the loop_end.
413 // `pre_loop_end_instrs` are to be inserted before `loop_end`.
415
416 // Record that we entered the loop.
419
420 // Jump back to the step case to havoc the write set, assume the invariant,
421 // and execute an arbitrary iteration.
424
425 // The following code is only reachable in the step case,
426 // i.e., when in_base_case == false,
427 // because of the unconditional jump above.
428
429 // Generate the inductiveness check:
430 // assert(invariant)
431 // We use a block scope for assertion, since it's immediately goto converted,
432 // and doesn't need to be kept around.
433 {
434 code_assertt assertion{invariant};
436 assertion.add_source_location().set_comment(
437 "Check that loop invariant is preserved");
438
440 converter.goto_convert(assertion, pre_loop_end_instrs, mode);
441 }
442
443 // Generate: assignments to store the multidimensional decreases clause's
444 // value after one iteration of the loop
445 if(!decreases_clause.is_nil())
446 {
447 for(size_t i = 0; i < new_decreases_vars.size(); i++)
448 {
451 new_decreases_assignment.add_source_location() = loop_head_location;
452
454 converter.goto_convert(
456 }
457
458 // Generate: assertion that the multidimensional decreases clause's value
459 // after the loop is lexicographically smaller than its initial value.
464 monotonic_decreasing_assertion.add_source_location().set_comment(
465 "Check decreases clause on loop iteration");
466
468 converter.goto_convert(
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 goto_programt constraint;
561 if(location.get_property_class() == ID_assume)
562 {
564 assumption.add_source_location() = location;
565 converter.goto_convert(assumption, constraint, mode);
566 }
567 else
568 {
570 assertion.add_source_location() = location;
571 converter.goto_convert(assertion, constraint, mode);
572 }
573 is_fresh_update(constraint);
574 throw_on_unsupported(constraint);
575 program.destructive_append(constraint);
576}
577
578static const code_with_contract_typet &
579get_contract(const irep_idt &function, const namespacet &ns)
580{
581 const std::string &function_str = id2string(function);
582 const auto &function_symbol = ns.lookup(function);
583
584 const symbolt *contract_sym;
585 if(ns.lookup("contract::" + function_str, contract_sym))
586 {
587 // no contract provided in the source or just an empty assigns clause
589 }
590
591 const auto &type = to_code_with_contract_type(contract_sym->type);
593 type == function_symbol.type,
594 "front-end should have rejected re-declarations with a different type");
595
596 return type;
597}
598
600 const irep_idt &function,
601 const source_locationt &location,
604{
605 const auto &const_target =
606 static_cast<const goto_programt::targett &>(target);
607 // Return if the function is not named in the call; currently we don't handle
608 // function pointers.
609 PRECONDITION(const_target->call_function().id() == ID_symbol);
610
611 const irep_idt &target_function =
612 to_symbol_expr(const_target->call_function()).get_identifier();
613 const symbolt &function_symbol = ns.lookup(target_function);
614 const code_typet &function_type = to_code_type(function_symbol.type);
615
616 // Isolate each component of the contract.
617 const auto &type = get_contract(target_function, ns);
618
619 // Prepare to instantiate expressions in the callee
620 // with expressions from the call site (e.g. the return value).
622
623 // keep track of the call's return expression to make it nondet later
624 std::optional<exprt> call_ret_opt = {};
625
626 // if true, the call return variable variable was created during replacement
627 bool call_ret_is_fresh_var = false;
628
629 if(function_type.return_type() != empty_typet())
630 {
631 // Check whether the function's return value is not disregarded.
632 if(target->call_lhs().is_not_nil())
633 {
634 // If so, have it replaced appropriately.
635 // For example, if foo() ensures that its return value is > 5, then
636 // rewrite calls to foo as follows:
637 // x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5)
638 auto &lhs_expr = const_target->call_lhs();
641 }
642 else
643 {
644 // If the function does return a value, but the return value is
645 // disregarded, check if the postcondition includes the return value.
646 if(std::any_of(
647 type.c_ensures().begin(),
648 type.c_ensures().end(),
649 [](const exprt &e) {
650 return has_symbol_expr(
651 to_lambda_expr(e).where(), CPROVER_PREFIX "return_value", true);
652 }))
653 {
654 // The postcondition does mention __CPROVER_return_value, so mint a
655 // fresh variable to replace __CPROVER_return_value with.
658 function_type.return_type(),
659 id2string(target_function),
660 "ignored_return_value",
661 const_target->source_location(),
662 symbol_table.lookup_ref(target_function).mode,
663 ns,
665 auto fresh_sym_expr = fresh.symbol_expr();
668 }
669 else
670 {
671 // unused, add a dummy with the right type
672 instantiation_values.push_back(
673 exprt{ID_nil, function_type.return_type()});
674 }
675 }
676 }
677
678 // Replace formal parameters
679 const auto &arguments = const_target->call_arguments();
681 instantiation_values.end(), arguments.begin(), arguments.end());
682
683 const auto &mode = function_symbol.mode;
684
685 // new program where all contract-derived instructions are added
687
689 goto_model, log.get_message_handler(), target_function);
690 is_fresh.create_declarations();
691 is_fresh.add_memory_map_decl(new_program);
692
693 // Generate: assert(requires)
694 for(const auto &clause : type.c_requires())
695 {
697 to_lambda_expr(clause).application(instantiation_values);
698 source_locationt _location = clause.source_location();
699 _location.set_line(location.get_line());
700 _location.set_comment(std::string("Check requires clause of ")
701 .append(target_function.c_str())
702 .append(" in ")
703 .append(function.c_str()));
704 _location.set_property_class(ID_precondition);
708 converter,
710 mode,
711 [&is_fresh](goto_programt &c_requires) {
712 is_fresh.update_requires(c_requires);
713 },
715 _location);
716 }
717
718 // Generate all the instructions required to initialize history variables
720 for(auto clause : type.c_ensures())
721 {
723 to_lambda_expr(clause).application(instantiation_values);
724 instantiated_clause.add_source_location() = clause.source_location();
728 }
729
730 // ASSIGNS clause should not refer to any quantified variables,
731 // and only refer to the common symbols to be replaced.
732 exprt::operandst targets;
733 for(auto &target : type.c_assigns())
734 targets.push_back(to_lambda_expr(target).application(instantiation_values));
735
736 // Create a sequence of non-deterministic assignments ...
737
738 // ... for the assigns clause targets and static locals
740 function_cfg_infot cfg_info({});
742 target_function,
743 targets,
745 cfg_info,
746 location,
749
750 havocker.get_instructions(havoc_instructions);
751
752 // ... for the return value
753 if(call_ret_opt.has_value())
754 {
755 auto &call_ret = call_ret_opt.value();
756 auto &loc = call_ret.source_location();
757 auto &type = call_ret.type();
758
759 // Declare if fresh
763
764 side_effect_expr_nondett expr(type, location);
766 code_assignt{call_ret, std::move(expr), loc}, loc));
767 }
768
769 // Insert havoc instructions immediately before the call site.
770 new_program.destructive_append(havoc_instructions);
771
772 // Generate: assume(ensures)
773 for(auto &clause : instantiated_ensures_clauses)
774 {
775 if(clause.is_false())
776 {
778 std::string("Attempt to assume false at ")
779 .append(clause.source_location().as_string())
780 .append(".\nPlease update ensures clause to avoid vacuity."));
781 }
782 source_locationt _location = clause.source_location();
783 _location.set_comment("Assume ensures clause");
784 _location.set_property_class(ID_assume);
785
789 converter,
790 clause,
791 mode,
792 [&is_fresh](goto_programt &ensures) { is_fresh.update_ensures(ensures); },
794 _location);
795 }
796
797 // Kill return value variable if fresh
799 {
801 log.warning(), [&target](messaget::mstreamt &mstream) {
802 target->output(mstream);
803 mstream << messaget::eom;
804 });
805 auto dead_inst =
807 function_body.insert_before_swap(target, dead_inst);
808 ++target;
809 }
810
811 is_fresh.add_memory_map_dead(new_program);
812
813 // Erase original function call
814 *target = goto_programt::make_skip();
815
816 // insert contract replacement instructions
818
819 // Add this function to the set of replaced functions.
820 summarized.insert(target_function);
821
822 // restore global goto_program consistency
824}
825
827 const irep_idt &function_name,
828 goto_functionst::goto_functiont &goto_function)
829{
830 const bool may_have_loops = std::any_of(
831 goto_function.body.instructions.begin(),
832 goto_function.body.instructions.end(),
833 [](const goto_programt::instructiont &instruction) {
834 return instruction.is_backwards_goto();
835 });
836
837 if(!may_have_loops)
838 return;
839
842
843 decorated.throw_on_recursive_calls(log, 0);
844
845 // restore internal invariants
847
848 local_may_aliast local_may_alias(goto_function);
849 natural_loops_mutablet natural_loops(goto_function.body);
850
851 // A graph node type that stores information about a loop.
852 // We create a DAG representing nesting of various loops in goto_function,
853 // sort them topologically, and instrument them in the top-sorted order.
854 //
855 // The goal here is not avoid explicit "subset checks" on nested write sets.
856 // When instrumenting in a top-sorted order,
857 // the outer loop would no longer observe the inner loop's write set,
858 // but only corresponding `havoc` statements,
859 // which can be instrumented in the usual way to achieve a "subset check".
860
861 struct loop_graph_nodet : public graph_nodet<empty_edget>
862 {
863 const typename natural_loops_mutablet::loopt &content;
866
868 const typename natural_loops_mutablet::loopt &loop,
869 const goto_programt::targett head,
870 const goto_programt::targett end,
871 const exprt &assigns,
872 const exprt &inv,
873 const exprt &decreases)
874 : content(loop),
875 head_target(head),
876 end_target(end),
877 assigns_clause(assigns),
878 invariant(inv),
879 decreases_clause(decreases)
880 {
881 }
882 };
884
885 std::list<size_t> to_check_contracts_on_children;
886
887 std::map<
889 std::pair<goto_programt::targett, natural_loops_mutablet::loopt>,
892
893 for(const auto &loop_head_and_content : natural_loops.loop_map)
894 {
895 const auto &loop_body = loop_head_and_content.second;
896 // Skip empty loops and self-looped node.
897 if(loop_body.size() <= 1)
898 continue;
899
900 auto loop_head = loop_head_and_content.first;
901 auto loop_end = loop_head;
902
903 // Find the last back edge to `loop_head`
904 for(const auto &t : loop_body)
905 {
906 if(
907 t->is_goto() && t->get_target() == loop_head &&
908 t->location_number > loop_end->location_number)
909 loop_end = t;
910 }
911
912 if(loop_end == loop_head)
913 {
914 log.error() << "Could not find end of the loop starting at: "
915 << loop_head->source_location() << messaget::eom;
916 throw 0;
917 }
918
919 // By definition the `loop_body` is a set of instructions computed
920 // by `natural_loops` based on the CFG.
921 // Since we perform assigns clause instrumentation by sequentially
922 // traversing instructions from `loop_head` to `loop_end`,
923 // here we ensure that all instructions in `loop_body` belong within
924 // the [loop_head, loop_end] target range.
925
926 // Check 1. (i \in loop_body) ==> loop_head <= i <= loop_end
927 for(const auto &i : loop_body)
928 {
929 if(
930 loop_head->location_number > i->location_number ||
931 i->location_number > loop_end->location_number)
932 {
934 log.error(), [&i, &loop_head](messaget::mstreamt &mstream) {
935 mstream << "Computed loop at " << loop_head->source_location()
936 << "contains an instruction beyond [loop_head, loop_end]:"
937 << messaget::eom;
938 i->output(mstream);
939 mstream << messaget::eom;
940 });
941 throw 0;
942 }
943 }
944
945 if(!loop_head_ends.emplace(loop_head, std::make_pair(loop_end, loop_body))
946 .second)
948 }
949
950 for(auto &loop_head_end : loop_head_ends)
951 {
952 auto loop_head = loop_head_end.first;
953 auto loop_end = loop_head_end.second.first;
954 // After loop-contract instrumentation, jumps to the `loop_head` will skip
955 // some instrumented instructions. So we want to make sure that there is
956 // only one jump targeting `loop_head` from `loop_end` before loop-contract
957 // instrumentation.
958 // Add a skip before `loop_head` and let all jumps (except for the
959 // `loop_end`) that target to the `loop_head` target to the skip
960 // instead.
962 goto_function.body, loop_head, goto_programt::make_skip());
963 loop_end->set_target(loop_head);
964
966 exprt invariant =
970
971 if(invariant.is_nil())
972 {
973 if(decreases_clause.is_not_nil() || assigns_clause.is_not_nil())
974 {
975 invariant = true_exprt{};
976 // assigns clause is missing; we will try to automatic inference
977 log.warning()
978 << "The loop at " << loop_head->source_location().as_string()
979 << " does not have an invariant in its contract.\n"
980 << "Hence, a default invariant ('true') is being used.\n"
981 << "This choice is sound, but verification may fail"
982 << " if it is be too weak to prove the desired properties."
983 << messaget::eom;
984 }
985 }
986 else
987 {
988 invariant = conjunction(invariant.operands());
989 if(decreases_clause.is_nil())
990 {
991 log.warning() << "The loop at "
992 << loop_head->source_location().as_string()
993 << " does not have a decreases clause in its contract.\n"
994 << "Termination of this loop will not be verified."
995 << messaget::eom;
996 }
997 }
998
999 const auto idx = loop_nesting_graph.add_node(
1000 loop_head_end.second.second,
1001 loop_head,
1002 loop_end,
1004 invariant,
1006
1007 if(
1008 assigns_clause.is_nil() && invariant.is_nil() &&
1009 decreases_clause.is_nil())
1010 continue;
1011
1012 to_check_contracts_on_children.push_back(idx);
1013 }
1014
1015 for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer)
1016 {
1017 for(size_t inner = 0; inner < loop_nesting_graph.size(); ++inner)
1018 {
1019 if(inner == outer)
1020 continue;
1021
1022 if(loop_nesting_graph[outer].content.contains(
1023 loop_nesting_graph[inner].head_target))
1024 {
1025 if(!loop_nesting_graph[outer].content.contains(
1026 loop_nesting_graph[inner].end_target))
1027 {
1028 log.error()
1029 << "Overlapping loops at:\n"
1030 << loop_nesting_graph[outer].head_target->source_location()
1031 << "\nand\n"
1032 << loop_nesting_graph[inner].head_target->source_location()
1033 << "\nLoops must be nested or sequential for contracts to be "
1034 "enforced."
1035 << messaget::eom;
1036 }
1037 loop_nesting_graph.add_edge(inner, outer);
1038 }
1039 }
1040 }
1041
1042 // make sure all children of a contractified loop also have contracts
1043 while(!to_check_contracts_on_children.empty())
1044 {
1045 const auto loop_idx = to_check_contracts_on_children.front();
1047
1048 const auto &loop_node = loop_nesting_graph[loop_idx];
1049 if(
1050 loop_node.assigns_clause.is_nil() && loop_node.invariant.is_nil() &&
1051 loop_node.decreases_clause.is_nil())
1052 {
1053 log.error()
1054 << "Inner loop at: " << loop_node.head_target->source_location()
1055 << " does not have contracts, but an enclosing loop does.\n"
1056 << "Please provide contracts for this loop, or unwind it first."
1057 << messaget::eom;
1058 throw 0;
1059 }
1060
1061 for(const auto child_idx : loop_nesting_graph.get_predecessors(loop_idx))
1063 }
1064
1065 // Iterate over the (natural) loops in the function, in topo-sorted order,
1066 // and apply any loop contracts that we find.
1067 for(const auto &idx : loop_nesting_graph.topsort())
1068 {
1069 const auto &loop_node = loop_nesting_graph[idx];
1070 if(
1071 loop_node.assigns_clause.is_nil() && loop_node.invariant.is_nil() &&
1072 loop_node.decreases_clause.is_nil())
1073 continue;
1074
1075 // Computed loop "contents" needs to be refreshed to include any newly
1076 // introduced instrumentation, e.g. havoc instructions for assigns clause,
1077 // on inner loops in to the outer loop's contents.
1078 // Else, during the outer loop instrumentation these instructions will be
1079 // "masked" just as any other instruction not within its "contents."
1080
1082 natural_loops_mutablet updated_loops(goto_function.body);
1083
1084 // We will unwind all transformed loops twice. Store the names of
1085 // to-unwind-loops here and perform the unwinding after transformation done.
1086 // As described in `check_apply_loop_contracts`, loops with loop contracts
1087 // will be transformed to a loop that execute exactly twice: one for base
1088 // case and one for step case. So we unwind them here to avoid users
1089 // incorrectly unwind them only once.
1090 std::string to_unwind = id2string(function_name) + "." +
1091 std::to_string(loop_node.end_target->loop_number) +
1092 ":2";
1093 loop_names.push_back(to_unwind);
1094
1096 function_name,
1097 goto_function,
1098 local_may_alias,
1099 loop_node.head_target,
1100 loop_node.end_target,
1101 updated_loops.loop_map[loop_node.head_target],
1102 loop_node.assigns_clause,
1103 loop_node.invariant,
1104 loop_node.decreases_clause,
1105 symbol_table.lookup_ref(function_name).mode);
1106 }
1107}
1108
1110{
1111 // Get the function object before instrumentation.
1112 auto function_obj = goto_functions.function_map.find(function);
1113
1114 INVARIANT(
1116 "Function '" + id2string(function) + "'must exist in the goto program");
1117
1118 const auto &goto_function = function_obj->second;
1119 auto &function_body = function_obj->second.body;
1120
1121 function_cfg_infot cfg_info(goto_function);
1122
1124 function,
1126 cfg_info,
1129
1130 // Detect and track static local variables before inlining
1133
1134 // Full inlining of the function body
1135 // Inlining is performed so that function calls to a same function
1136 // occurring under different write sets get instrumented specifically
1137 // for each write set
1140
1141 decorated.throw_on_recursive_calls(log, 0);
1142
1143 // Clean up possible fake loops that are due to `IF 0!=0 GOTO i` instructions
1145
1146 // Restore internal coherence in the programs
1148
1149 INVARIANT(
1151 "Loops remain in function '" + id2string(function) +
1152 "', assigns clause checking instrumentation cannot be applied.");
1153
1154 // Start instrumentation
1155 auto instruction_it = function_body.instructions.begin();
1156
1157 // Inject local static snapshots
1160
1161 // Track targets mentioned in the specification
1162 const symbolt &function_symbol = ns.lookup(function);
1163 const code_typet &function_type = to_code_type(function_symbol.type);
1165 // assigns clauses cannot refer to the return value, but we still need an
1166 // element in there to apply the lambda function consistently
1167 if(function_type.return_type() != empty_typet())
1168 instantiation_values.push_back(exprt{ID_nil, function_type.return_type()});
1169 for(const auto &param : function_type.parameters())
1170 {
1171 instantiation_values.push_back(
1172 ns.lookup(param.get_identifier()).symbol_expr());
1173 }
1174 for(auto &target : get_contract(function, ns).c_assigns())
1175 {
1177 instrument_spec_assigns.track_spec_target(
1178 to_lambda_expr(target).application(instantiation_values), payload);
1180 }
1181
1182 // Track formal parameters
1184 for(const auto &param : function_type.parameters())
1185 {
1187 instrument_spec_assigns.track_stack_allocated(
1188 ns.lookup(param.get_identifier()).symbol_expr(), payload);
1190 }
1191
1192 // Restore internal coherence in the programs
1194
1195 // Insert write set inclusion checks.
1196 instrument_spec_assigns.instrument_instructions(
1197 function_body, instruction_it, function_body.instructions.end());
1198}
1199
1201{
1202 // Add statements to the source function
1203 // to ensure assigns clause is respected.
1205
1206 // Rename source function
1207 std::stringstream ss;
1208 ss << CPROVER_PREFIX << "contracts_original_" << function;
1209 const irep_idt mangled(ss.str());
1210 const irep_idt original(function);
1211
1213 INVARIANT(
1215 "Function to replace must exist in the program.");
1216
1217 std::swap(goto_functions.function_map[mangled], old_function->second);
1219
1220 // Place a new symbol with the mangled name into the symbol table
1222 sl.set_file("instrumented for code contracts");
1223 sl.set_line("0");
1226 mangled_sym.name = mangled;
1227 mangled_sym.base_name = mangled;
1228 mangled_sym.location = sl;
1229 const auto mangled_found = symbol_table.insert(std::move(mangled_sym));
1230 INVARIANT(
1231 mangled_found.second,
1232 "There should be no existing function called " + ss.str() +
1233 " in the symbol table because that name is a mangled name");
1234
1235 // Insert wrapper function into goto_functions
1237 INVARIANT(
1239 "There should be no function called " + id2string(function) +
1240 " in the function map because that function should have had its"
1241 " name mangled");
1242
1244 INVARIANT(
1246 "There should be a function called " + ss.str() +
1247 " in the function map because we inserted a fresh goto-program"
1248 " with that mangled name");
1249
1251 wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers;
1254}
1255
1259 goto_programt &dest)
1260{
1261 PRECONDITION(!dest.instructions.empty());
1262
1263 // build:
1264 // decl ret
1265 // decl parameter1 ...
1266 // decl history_parameter1 ... [optional]
1267 // assume(requires) [optional]
1268 // ret=function(parameter1, ...)
1269 // assert(ensures)
1270
1271 const auto &code_type = get_contract(wrapper_function, ns);
1272 goto_programt check;
1273
1274 // prepare function call including all declarations
1275 const symbolt &function_symbol = ns.lookup(mangled_function);
1277
1278 // Prepare to instantiate expressions in the callee
1279 // with expressions from the call site (e.g. the return value).
1281
1282 source_locationt source_location = function_symbol.location;
1283 // Set function in source location to original function
1284 source_location.set_function(wrapper_function);
1285
1286 // decl ret
1287 std::optional<code_returnt> return_stmt;
1288 if(code_type.return_type() != empty_typet())
1289 {
1291 code_type.return_type(),
1292 id2string(source_location.get_function()),
1293 "tmp_cc",
1294 source_location,
1295 function_symbol.mode,
1297 .symbol_expr();
1298 check.add(goto_programt::make_decl(r, source_location));
1299
1300 call.lhs() = r;
1302
1303 instantiation_values.push_back(r);
1304 }
1305
1306 // decl parameter1 ...
1307 goto_functionst::function_mapt::iterator f_it =
1310
1311 const goto_functionst::goto_functiont &gf = f_it->second;
1312 for(const auto &parameter : gf.parameter_identifiers)
1313 {
1314 PRECONDITION(!parameter.empty());
1315 const symbolt &parameter_symbol = ns.lookup(parameter);
1317 parameter_symbol.type,
1318 id2string(source_location.get_function()),
1319 "tmp_cc",
1320 source_location,
1321 parameter_symbol.mode,
1323 .symbol_expr();
1324 check.add(goto_programt::make_decl(p, source_location));
1326 p, parameter_symbol.symbol_expr(), source_location));
1327
1328 call.arguments().push_back(p);
1329
1330 instantiation_values.push_back(p);
1331 }
1332
1335 visitor.create_declarations();
1336 visitor.add_memory_map_decl(check);
1337
1338 // Generate: assume(requires)
1339 for(const auto &clause : code_type.c_requires())
1340 {
1341 auto instantiated_clause =
1342 to_lambda_expr(clause).application(instantiation_values);
1343 if(instantiated_clause.is_false())
1344 {
1346 std::string("Attempt to assume false at ")
1347 .append(clause.source_location().as_string())
1348 .append(".\nPlease update requires clause to avoid vacuity."));
1349 }
1350 source_locationt _location = clause.source_location();
1351 _location.set_comment("Assume requires clause");
1352 _location.set_property_class(ID_assume);
1356 converter,
1358 function_symbol.mode,
1359 [&visitor](goto_programt &c_requires) {
1360 visitor.update_requires(c_requires);
1361 },
1362 check,
1363 _location);
1364 }
1365
1366 // Generate all the instructions required to initialize history variables
1368 for(auto clause : code_type.c_ensures())
1369 {
1370 auto instantiated_clause =
1371 to_lambda_expr(clause).application(instantiation_values);
1372 instantiated_clause.add_source_location() = clause.source_location();
1376 }
1377
1378 // ret=mangled_function(parameter1, ...)
1379 check.add(goto_programt::make_function_call(call, source_location));
1380
1381 // Generate: assert(ensures)
1382 for(auto &clause : instantiated_ensures_clauses)
1383 {
1384 source_locationt _location = clause.source_location();
1385 _location.set_comment("Check ensures clause");
1386 _location.set_property_class(ID_postcondition);
1390 converter,
1391 clause,
1392 function_symbol.mode,
1393 [&visitor](goto_programt &ensures) { visitor.update_ensures(ensures); },
1394 check,
1395 _location);
1396 }
1397
1398 if(code_type.return_type() != empty_typet())
1399 {
1401 return_stmt.value().return_value(), source_location));
1402 }
1403
1404 // kill the is_fresh memory map
1405 visitor.add_memory_map_dead(check);
1406
1407 // prepend the new code to dest
1408 dest.destructive_insert(dest.instructions.begin(), check);
1409
1410 // restore global goto_program consistency
1412}
1413
1415 const std::set<std::string> &functions) const
1416{
1417 for(const auto &function : functions)
1418 {
1419 if(
1420 goto_functions.function_map.find(function) ==
1422 {
1424 "Function '" + function + "' was not found in the GOTO program.");
1425 }
1426 }
1427}
1428
1429void code_contractst::replace_calls(const std::set<std::string> &to_replace)
1430{
1431 if(to_replace.empty())
1432 return;
1433
1434 log.status() << "Replacing function calls with contracts" << messaget::eom;
1435
1436 check_all_functions_found(to_replace);
1437
1438 for(auto &goto_function : goto_functions.function_map)
1439 {
1440 Forall_goto_program_instructions(ins, goto_function.second.body)
1441 {
1442 if(ins->is_function_call())
1443 {
1444 if(ins->call_function().id() != ID_symbol)
1445 continue;
1446
1447 const irep_idt &called_function =
1448 to_symbol_expr(ins->call_function()).get_identifier();
1449 auto found = std::find(
1450 to_replace.begin(), to_replace.end(), id2string(called_function));
1451 if(found == to_replace.end())
1452 continue;
1453
1455 goto_function.first,
1456 ins->source_location(),
1457 goto_function.second.body,
1458 ins);
1459 }
1460 }
1461 }
1462
1463 for(auto &goto_function : goto_functions.function_map)
1464 remove_skip(goto_function.second.body);
1465
1467}
1468
1470 const std::set<std::string> &to_exclude_from_nondet_init)
1471{
1472 for(auto &goto_function : goto_functions.function_map)
1473 apply_loop_contract(goto_function.first, goto_function.second);
1474
1475 log.status() << "Adding nondeterministic initialization "
1476 "of static/global variables."
1477 << messaget::eom;
1479
1480 // unwind all transformed loops twice.
1482 {
1483 unwindsett unwindset;
1484 unwindset.parse_unwindset(
1488 }
1489
1491
1492 // Record original loop number for some instrumented instructions.
1494 {
1495 auto &goto_function = goto_function_entry.second;
1496 bool is_in_loop_havoc_block = false;
1497
1498 unsigned loop_number_of_loop_havoc = 0;
1500 goto_function.body.instructions.begin();
1501 it_instr != goto_function.body.instructions.end();
1502 it_instr++)
1503 {
1504 // Don't override original loop numbers.
1505 if(original_loop_number_map.count(it_instr) != 0)
1506 continue;
1507
1508 // Store loop number for two type of instrumented instructions.
1509 // ASSIGN ENTERED_LOOP = false --- head of transformed loops.
1510 // ASSIGN ENTERED_LOOP = true --- end of transformed loops.
1511 if(
1513 {
1514 const auto &assign_lhs =
1517 id2string(assign_lhs->get_identifier()),
1518 std::string(ENTERED_LOOP) + "__");
1519 continue;
1520 }
1521
1522 // Loop havocs are assignments between
1523 // ASSIGN IN_LOOP_HAVOC_BLOCK = true
1524 // and
1525 // ASSIGN IN_LOOP_HAVOC_BLOCK = false
1526
1527 // Entering the loop-havoc block.
1529 {
1530 is_in_loop_havoc_block = it_instr->assign_rhs() == true_exprt();
1531 const auto &assign_lhs =
1534 id2string(assign_lhs->get_identifier()),
1535 std::string(IN_LOOP_HAVOC_BLOCK) + "__");
1536 continue;
1537 }
1538
1539 // Assignments in loop-havoc block are loop havocs.
1540 if(is_in_loop_havoc_block && it_instr->is_assign())
1541 {
1542 loop_havoc_set.emplace(it_instr);
1543
1544 // Store loop number for loop havoc.
1546 }
1547 }
1548 }
1549}
1550
1552 const std::set<std::string> &to_enforce,
1553 const std::set<std::string> &to_exclude_from_nondet_init)
1554{
1555 if(to_enforce.empty())
1556 return;
1557
1558 log.status() << "Enforcing contracts" << messaget ::eom;
1559
1561
1562 for(const auto &function : to_enforce)
1563 enforce_contract(function);
1564
1565 log.status() << "Adding nondeterministic initialization "
1566 "of static/global variables."
1567 << messaget::eom;
1569}
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:562
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
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:153
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:39
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:157
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:154
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:159
const namespacet ns
Definition contracts.h:150
std::unordered_set< goto_programt::const_targett, const_target_hash > loop_havoc_set
Loop havoc instructions instrumented during applying loop contracts.
Definition contracts.h:173
loop_contract_configt loop_contract_config
Definition contracts.h:176
std::list< std::string > loop_names
Name of loops we are going to unwind.
Definition contracts.h:162
goto_functionst & goto_functions
Definition contracts.h:155
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:169
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...
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:583
const parameterst & parameters() const
Definition std_types.h:699
const typet & return_type() const
Definition std_types.h:689
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
const char * c_str() const
Definition dstring.h:116
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:236
The Boolean constant false.
Definition std_expr.h:3200
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:90
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:434
bool is_nil() const
Definition irep.h:368
loop_mapt loop_map
void erase_locals(std::set< exprt > &exprs)
Definition cfg_info.h:171
mstreamt & error() const
Definition message.h:391
mstreamt & debug() const
Definition message.h:421
message_handlert & get_message_handler()
Definition message.h:183
mstreamt & warning() const
Definition message.h:396
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:289
mstreamt & status() const
Definition message.h:406
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:2459
Boolean OR.
Definition std_expr.h:2275
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:131
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:3191
void parse_unwindset(const std::list< std::string > &unwindset, abstract_goto_modelt &goto_model, message_handlert &message_handler)
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 std::map< dfcc_funt, int > to_unwind
set of functions that need to be unwound to assigns clause size with corresponding loop identifiers.
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition expr_util.cpp:98
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 ...
#define Forall_goto_program_instructions(it, program)
Havoc function assigns clauses.
std::set< exprt > assignst
Definition havoc_utils.h:24
std::optional< 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:44
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_modelt &goto_model, 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 UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#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(exprt a, exprt b)
Conjunction of two expressions.
Definition std_expr.cpp:83
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
A total order over targett and const_targett.
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:494
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:524
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:247
void infer_loop_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
Infer loop assigns using alias analysis result local_may_alias.
Definition utils.cpp:344
bool is_loop_free(const goto_programt &goto_program, const namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.
Definition utils.cpp:271
exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
Extract loop assigns from annotated loop end.
Definition utils.cpp:683
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:475
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:508
void insert_before_swap_and_advance(goto_programt &destination, goto_programt::targett &target, goto_programt &payload)
Insert a goto program before a target instruction iterator and advance the iterator.
Definition utils.cpp:237
void widen_assigns(assignst &assigns, const namespacet &ns)
Widen expressions in assigns with the following strategy.
Definition utils.cpp:360
void simplify_gotos(goto_programt &goto_program, const namespacet &ns)
Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SK...
Definition utils.cpp:260
exprt get_loop_invariants(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop invariants from annotated loop end.
Definition utils.cpp:666
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:516
exprt get_loop_decreases(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop decreases from annotated loop end.
Definition utils.cpp:688
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:546
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:193
#define ENTERED_LOOP
Definition utils.h:24
#define INIT_INVARIANT
Definition utils.h:26
#define IN_LOOP_HAVOC_BLOCK
Definition utils.h:25