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>
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 // instrument
72 //
73 // ... preamble ...
74 // HEAD:
75 // ... eval guard ...
76 // if (!guard)
77 // goto EXIT;
78 // ... loop body ...
79 // goto HEAD;
80 // EXIT:
81 // ... postamble ...
82 //
83 // to
84 //
85 // ... preamble ...
86 // ,- initialize loop_entry history vars;
87 // | entered_loop = false
88 // loop assigns check | initial_invariant_val = invariant_expr;
89 // - unchecked, temps | in_base_case = true;
90 // func assigns check | snapshot (write_set);
91 // - disabled via pragma | goto HEAD;
92 // | STEP:
93 // --. | assert (initial_invariant_val);
94 // loop assigns check | | in_base_case = false;
95 // - not applicable >======= in_loop_havoc_block = true;
96 // func assigns check | | havoc (assigns_set);
97 // + deferred | | in_loop_havoc_block = false;
98 // --' | assume (invariant_expr);
99 // `- old_variant_val = decreases_clause_expr;
100 // * HEAD:
101 // loop assigns check ,- ... eval guard ...
102 // + assertions added | if (!guard)
103 // func assigns check | goto EXIT;
104 // - disabled via pragma `- ... loop body ...
105 // ,- entered_loop = true
106 // | if (in_base_case)
107 // | goto STEP;
108 // loop assigns check | assert (invariant_expr);
109 // - unchecked, temps | new_variant_val = decreases_clause_expr;
110 // func assigns check | assert (new_variant_val < old_variant_val);
111 // - disabled via pragma | dead old_variant_val, new_variant_val;
112 // | * assume (false);
113 // | * EXIT:
114 // To be inserted at ,~~~|~~~~ assert (entered_loop ==> !in_base_case);
115 // every unique EXIT | | dead loop_entry history vars, in_base_case;
116 // (break, goto etc.) `~~~`- ~~ dead initial_invariant_val, entered_loop;
117 // ... postamble ..
118 //
119 // Asterisks (*) denote anchor points (goto targets) for instrumentations.
120 // We insert generated code above and/below these targets.
121 //
122 // Assertions for assigns clause checking are inserted in the loop body.
123
124 // Process "loop_entry" history variables.
125 // We find and replace all "__CPROVER_loop_entry" subexpressions in invariant.
127 symbol_table, invariant, loop_head_location, mode);
128 invariant.swap(replace_history_result.expression_after_replacement);
129 const auto &history_var_map = replace_history_result.parameter_to_history;
130 // an intermediate goto_program to store generated instructions
131 // to be inserted before the loop head
133 replace_history_result.history_construction;
134
135 // Create a temporary to track if we entered the loop,
136 // i.e., the loop guard was satisfied.
137 const auto entered_loop =
139 bool_typet(),
140 id2string(loop_head_location.get_function()),
141 std::string(ENTERED_LOOP) + "__" + std::to_string(loop_number),
143 mode,
145 .symbol_expr();
150
151 // Create a snapshot of the invariant so that we can check the base case,
152 // if the loop is not vacuous and must be abstracted with contracts.
153 const auto initial_invariant_val =
155 bool_typet(),
156 id2string(loop_head_location.get_function()),
159 mode,
161 .symbol_expr();
164 {
165 // Although the invariant at this point will not have side effects,
166 // it is still a C expression, and needs to be "goto_convert"ed.
167 // Note that this conversion may emit many GOTO instructions.
169 initial_invariant_val, invariant};
170 initial_invariant_value_assignment.add_source_location() =
172
174 converter.goto_convert(
176 }
177
178 // Create a temporary variable to track base case vs inductive case
179 // instrumentation of the loop.
181 bool_typet(),
182 id2string(loop_head_location.get_function()),
183 "__in_base_case",
185 mode,
187 .symbol_expr();
192
193 // CAR snapshot instructions for checking assigns clause
195
196 loop_cfg_infot cfg_info(goto_function, loop);
197
198 // track static local symbols
200 function_name,
202 cfg_info,
205
206 instrument_spec_assigns.track_static_locals_between(
208
209 // set of targets to havoc
211
212 if(assigns_clause.is_nil())
213 {
214 // No assigns clause was specified for this loop.
215 // Infer memory locations assigned by the loop from the loop instructions
216 // and the inferred aliasing relation.
217 try
218 {
219 infer_loop_assigns(local_may_alias, loop, to_havoc);
220
221 // remove loop-local symbols from the inferred set
222 cfg_info.erase_locals(to_havoc);
223
224 // If the set contains pairs (i, a[i]),
225 // we widen them to (i, __CPROVER_POINTER_OBJECT(a))
227
228 log.debug() << "No loop assigns clause provided. Inferred targets: {";
229 // Add inferred targets to the loop assigns clause.
230 bool ran_once = false;
231 for(const auto &target : to_havoc)
232 {
233 if(ran_once)
234 log.debug() << ", ";
235 ran_once = true;
236 log.debug() << format(target);
237 instrument_spec_assigns.track_spec_target(
238 target, snapshot_instructions);
239 }
240 log.debug() << "}" << messaget::eom;
241
242 instrument_spec_assigns.get_static_locals(
243 std::inserter(to_havoc, to_havoc.end()));
244 }
245 catch(const analysis_exceptiont &exc)
246 {
247 log.error() << "Failed to infer variables being modified by the loop at "
249 << ".\nPlease specify an assigns clause.\nReason:"
250 << messaget::eom;
251 throw exc;
252 }
253 }
254 else
255 {
256 // An assigns clause was specified for this loop.
257 // Add the targets to the set of expressions to havoc.
258 for(const auto &target : assigns_clause.operands())
259 {
260 to_havoc.insert(target);
261 instrument_spec_assigns.track_spec_target(target, snapshot_instructions);
262 }
263 }
264
265 // Insert instrumentation
266 // This must be done before havocing the write set.
267 // FIXME: this is not true for write set targets that
268 // might depend on other write set targets.
270
271 // Insert a jump to the loop head
272 // (skipping over the step case initialization code below)
275
276 // The STEP case instructions follow.
277 // We skip past it initially, because of the unconditional jump above,
278 // but jump back here if we get past the loop guard while in_base_case.
279
280 const auto step_case_target =
283
284 // If we jump here, then the loop runs at least once,
285 // so add the base case assertion:
286 // assert(initial_invariant_val)
287 // We use a block scope for assertion, since it's immediately goto converted,
288 // and doesn't need to be kept around.
289 {
291 assertion.add_source_location() = loop_head_location;
292 assertion.add_source_location().set_comment(
293 "Check loop invariant before entry");
294
296 converter.goto_convert(assertion, pre_loop_head_instrs, mode);
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};
341
343 converter.goto_convert(assumption, pre_loop_head_instrs, mode);
344 }
345
346 // Create fresh temporary variables that store the multidimensional
347 // decreases clause's value before and after the loop
348 for(const auto &clause : decreases_clause.operands())
349 {
350 const auto old_decreases_var =
352 clause.type(),
353 id2string(loop_head_location.get_function()),
354 "tmp_cc",
356 mode,
358 .symbol_expr();
362
363 const auto new_decreases_var =
365 clause.type(),
366 id2string(loop_head_location.get_function()),
367 "tmp_cc",
369 mode,
371 .symbol_expr();
375 }
376
377 // TODO: Fix loop contract handling for do/while loops.
378 if(loop_end->is_goto() && !loop_end->condition().is_true())
379 {
380 log.error() << "Loop contracts are unsupported on do/while loops: "
382 throw 0;
383
384 // non-deterministically skip the loop if it is a do-while loop.
385 // pre_loop_head_instrs.add(goto_programt::make_goto(
386 // loop_end, side_effect_expr_nondett(bool_typet(), loop_head_location)));
387 }
388
389 // Generate: assignments to store the multidimensional decreases clause's
390 // value just before the loop_head
391 if(!decreases_clause.is_nil())
392 {
393 for(size_t i = 0; i < old_decreases_vars.size(); i++)
394 {
397 old_decreases_assignment.add_source_location() = loop_head_location;
398
400 converter.goto_convert(
402 }
403
404 goto_function.body.destructive_insert(
406 }
407
408 // Insert the third and final block of pre_loop_head_instrs,
409 // with a pragma to disable assigns clause checking.
410 // The variables to store old variant value are local temporaries,
411 // which need not be checked against the enclosing scope's assigns clause.
412 goto_function.body.destructive_insert(
414
415 // Perform write set instrumentation on the entire loop.
416 instrument_spec_assigns.instrument_instructions(
417 goto_function.body,
418 loop_head,
419 loop_end,
420 [&loop](const goto_programt::targett &t) { return loop.contains(t); });
421
422 // Now we begin instrumenting at the loop_end.
423 // `pre_loop_end_instrs` are to be inserted before `loop_end`.
425
426 // Record that we entered the loop.
429
430 // Jump back to the step case to havoc the write set, assume the invariant,
431 // and execute an arbitrary iteration.
434
435 // The following code is only reachable in the step case,
436 // i.e., when in_base_case == false,
437 // because of the unconditional jump above.
438
439 // Generate the inductiveness check:
440 // assert(invariant)
441 // We use a block scope for assertion, since it's immediately goto converted,
442 // and doesn't need to be kept around.
443 {
444 code_assertt assertion{invariant};
446 assertion.add_source_location().set_comment(
447 "Check that loop invariant is preserved");
448
450 converter.goto_convert(assertion, pre_loop_end_instrs, mode);
451 }
452
453 // Generate: assignments to store the multidimensional decreases clause's
454 // value after one iteration of the loop
455 if(!decreases_clause.is_nil())
456 {
457 for(size_t i = 0; i < new_decreases_vars.size(); i++)
458 {
461 new_decreases_assignment.add_source_location() = loop_head_location;
462
464 converter.goto_convert(
466 }
467
468 // Generate: assertion that the multidimensional decreases clause's value
469 // after the loop is lexicographically smaller than its initial value.
474 monotonic_decreasing_assertion.add_source_location().set_comment(
475 "Check decreases clause on loop iteration");
476
478 converter.goto_convert(
480
481 // Discard the temporary variables that store decreases clause's value
482 for(size_t i = 0; i < old_decreases_vars.size(); i++)
483 {
488 }
489 }
490
492 goto_function.body,
493 loop_end,
495
496 // change the back edge into assume(false) or assume(guard)
497 loop_end->turn_into_assume();
498 loop_end->condition_nonconst() = boolean_negate(loop_end->condition());
499
500 std::set<goto_programt::targett, goto_programt::target_less_than>
502 // Find all exit points of the loop, make temporary variables `DEAD`,
503 // and check that step case was checked for non-vacuous loops.
504 for(const auto &t : loop)
505 {
506 if(!t->is_goto())
507 continue;
508
509 auto exit_target = t->get_target();
510 if(
511 loop.contains(exit_target) ||
513 continue;
514
516
518 // Assertion to check that step case was checked if we entered the loop.
520 annotated_location.set_comment(
521 "Check that loop instrumentation was not truncated");
525 // Instructions to make all the temporaries go dead.
530 for(const auto &v : history_var_map)
531 {
534 }
535 // Insert these instructions, preserving the loop end target.
537 goto_function.body, exit_target, pre_loop_exit_instrs);
538 }
539}
540
543static void throw_on_unsupported(const goto_programt &program)
544{
545 for(const auto &it : program.instructions)
546 {
547 if(
548 it.is_function_call() && it.call_function().id() == ID_symbol &&
549 to_symbol_expr(it.call_function()).get_identifier() == CPROVER_PREFIX
550 "obeys_contract")
551 {
553 CPROVER_PREFIX "obeys_contract is not supported in this version",
554 it.source_location());
555 }
556 }
557}
558
562 symbol_tablet &symbol_table,
563 goto_convertt &converter,
565 const irep_idt &mode,
566 const std::function<void(goto_programt &)> &is_fresh_update,
567 goto_programt &program,
568 const source_locationt &location)
569{
570 goto_programt constraint;
571 if(location.get_property_class() == ID_assume)
572 {
574 assumption.add_source_location() = location;
575 converter.goto_convert(assumption, constraint, mode);
576 }
577 else
578 {
580 assertion.add_source_location() = location;
581 converter.goto_convert(assertion, constraint, mode);
582 }
583 is_fresh_update(constraint);
584 throw_on_unsupported(constraint);
585 program.destructive_append(constraint);
586}
587
588static const code_with_contract_typet &
589get_contract(const irep_idt &function, const namespacet &ns)
590{
591 const std::string &function_str = id2string(function);
592 const auto &function_symbol = ns.lookup(function);
593
594 const symbolt *contract_sym;
595 if(ns.lookup("contract::" + function_str, contract_sym))
596 {
597 // no contract provided in the source or just an empty assigns clause
599 }
600
601 const auto &type = to_code_with_contract_type(contract_sym->type);
603 type == function_symbol.type,
604 "front-end should have rejected re-declarations with a different type");
605
606 return type;
607}
608
610 const irep_idt &function,
611 const source_locationt &location,
614{
615 const auto &const_target =
616 static_cast<const goto_programt::targett &>(target);
617 // Return if the function is not named in the call; currently we don't handle
618 // function pointers.
619 PRECONDITION(const_target->call_function().id() == ID_symbol);
620
621 const irep_idt &target_function =
622 to_symbol_expr(const_target->call_function()).get_identifier();
623 const symbolt &function_symbol = ns.lookup(target_function);
624 const code_typet &function_type = to_code_type(function_symbol.type);
625
626 // Isolate each component of the contract.
627 const auto &type = get_contract(target_function, ns);
628
629 // Prepare to instantiate expressions in the callee
630 // with expressions from the call site (e.g. the return value).
632
633 // keep track of the call's return expression to make it nondet later
634 std::optional<exprt> call_ret_opt = {};
635
636 // if true, the call return variable variable was created during replacement
637 bool call_ret_is_fresh_var = false;
638
639 if(function_type.return_type() != empty_typet())
640 {
641 // Check whether the function's return value is not disregarded.
642 if(target->call_lhs().is_not_nil())
643 {
644 // If so, have it replaced appropriately.
645 // For example, if foo() ensures that its return value is > 5, then
646 // rewrite calls to foo as follows:
647 // x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5)
648 auto &lhs_expr = const_target->call_lhs();
651 }
652 else
653 {
654 // If the function does return a value, but the return value is
655 // disregarded, check if the postcondition includes the return value.
656 if(std::any_of(
657 type.c_ensures().begin(),
658 type.c_ensures().end(),
659 [](const exprt &e) {
660 return has_symbol_expr(
661 to_lambda_expr(e).where(), CPROVER_PREFIX "return_value", true);
662 }))
663 {
664 // The postcondition does mention __CPROVER_return_value, so mint a
665 // fresh variable to replace __CPROVER_return_value with.
668 function_type.return_type(),
669 id2string(target_function),
670 "ignored_return_value",
671 const_target->source_location(),
672 symbol_table.lookup_ref(target_function).mode,
673 ns,
675 auto fresh_sym_expr = fresh.symbol_expr();
678 }
679 else
680 {
681 // unused, add a dummy with the right type
682 instantiation_values.push_back(
683 exprt{ID_nil, function_type.return_type()});
684 }
685 }
686 }
687
688 // Replace formal parameters
689 const auto &arguments = const_target->call_arguments();
691 instantiation_values.end(), arguments.begin(), arguments.end());
692
693 const auto &mode = function_symbol.mode;
694
695 // new program where all contract-derived instructions are added
697
699 goto_model, log.get_message_handler(), target_function);
700 is_fresh.create_declarations();
701 is_fresh.add_memory_map_decl(new_program);
702
703 // Generate: assert(requires)
704 for(const auto &clause : type.c_requires())
705 {
707 to_lambda_expr(clause).application(instantiation_values);
708 source_locationt _location = clause.source_location();
709 _location.set_line(location.get_line());
710 _location.set_comment(std::string("Check requires clause of ")
711 .append(target_function.c_str())
712 .append(" in ")
713 .append(function.c_str()));
714 _location.set_property_class(ID_precondition);
718 converter,
720 mode,
721 [&is_fresh](goto_programt &c_requires) {
722 is_fresh.update_requires(c_requires);
723 },
725 _location);
726 }
727
728 // Generate all the instructions required to initialize history variables
730 for(auto clause : type.c_ensures())
731 {
733 to_lambda_expr(clause).application(instantiation_values);
734 instantiated_clause.add_source_location() = clause.source_location();
738 }
739
740 // ASSIGNS clause should not refer to any quantified variables,
741 // and only refer to the common symbols to be replaced.
742 exprt::operandst targets;
743 for(auto &target : type.c_assigns())
744 targets.push_back(to_lambda_expr(target).application(instantiation_values));
745
746 // Create a sequence of non-deterministic assignments ...
747
748 // ... for the assigns clause targets and static locals
750 function_cfg_infot cfg_info({});
752 target_function,
753 targets,
755 cfg_info,
756 location,
759
760 havocker.get_instructions(havoc_instructions);
761
762 // ... for the return value
763 if(call_ret_opt.has_value())
764 {
765 auto &call_ret = call_ret_opt.value();
766 auto &loc = call_ret.source_location();
767 auto &type = call_ret.type();
768
769 // Declare if fresh
773
774 side_effect_expr_nondett expr(type, location);
776 code_assignt{call_ret, std::move(expr), loc}, loc));
777 }
778
779 // Insert havoc instructions immediately before the call site.
780 new_program.destructive_append(havoc_instructions);
781
782 // Generate: assume(ensures)
783 for(auto &clause : instantiated_ensures_clauses)
784 {
785 if(clause.is_false())
786 {
788 std::string("Attempt to assume false at ")
789 .append(clause.source_location().as_string())
790 .append(".\nPlease update ensures clause to avoid vacuity."));
791 }
792 source_locationt _location = clause.source_location();
793 _location.set_comment("Assume ensures clause");
794 _location.set_property_class(ID_assume);
795
799 converter,
800 clause,
801 mode,
802 [&is_fresh](goto_programt &ensures) { is_fresh.update_ensures(ensures); },
804 _location);
805 }
806
807 // Kill return value variable if fresh
809 {
811 log.warning(), [&target](messaget::mstreamt &mstream) {
812 target->output(mstream);
813 mstream << messaget::eom;
814 });
815 auto dead_inst =
817 function_body.insert_before_swap(target, dead_inst);
818 ++target;
819 }
820
821 is_fresh.add_memory_map_dead(new_program);
822
823 // Erase original function call
824 *target = goto_programt::make_skip();
825
826 // insert contract replacement instructions
828
829 // Add this function to the set of replaced functions.
830 summarized.insert(target_function);
831
832 // restore global goto_program consistency
834}
835
837 const irep_idt &function_name,
838 goto_functionst::goto_functiont &goto_function)
839{
840 const bool may_have_loops = std::any_of(
841 goto_function.body.instructions.begin(),
842 goto_function.body.instructions.end(),
843 [](const goto_programt::instructiont &instruction) {
844 return instruction.is_backwards_goto();
845 });
846
847 if(!may_have_loops)
848 return;
849
852 goto_functions, function_name, ns, log.get_message_handler());
853
854 INVARIANT(
855 decorated.get_recursive_call_set().size() == 0,
856 "Recursive functions found during inlining");
857
858 // restore internal invariants
860
861 local_may_aliast local_may_alias(goto_function);
862 natural_loops_mutablet natural_loops(goto_function.body);
863
864 // A graph node type that stores information about a loop.
865 // We create a DAG representing nesting of various loops in goto_function,
866 // sort them topologically, and instrument them in the top-sorted order.
867 //
868 // The goal here is not avoid explicit "subset checks" on nested write sets.
869 // When instrumenting in a top-sorted order,
870 // the outer loop would no longer observe the inner loop's write set,
871 // but only corresponding `havoc` statements,
872 // which can be instrumented in the usual way to achieve a "subset check".
873
874 struct loop_graph_nodet : public graph_nodet<empty_edget>
875 {
876 const typename natural_loops_mutablet::loopt &content;
879
881 const typename natural_loops_mutablet::loopt &loop,
882 const goto_programt::targett head,
883 const goto_programt::targett end,
884 const exprt &assigns,
885 const exprt &inv,
886 const exprt &decreases)
887 : content(loop),
888 head_target(head),
889 end_target(end),
890 assigns_clause(assigns),
891 invariant(inv),
892 decreases_clause(decreases)
893 {
894 }
895 };
897
898 std::list<size_t> to_check_contracts_on_children;
899
900 std::map<
902 std::pair<goto_programt::targett, natural_loops_mutablet::loopt>,
905
906 for(const auto &loop_head_and_content : natural_loops.loop_map)
907 {
908 const auto &loop_body = loop_head_and_content.second;
909 // Skip empty loops and self-looped node.
910 if(loop_body.size() <= 1)
911 continue;
912
913 auto loop_head = loop_head_and_content.first;
914 auto loop_end = loop_head;
915
916 // Find the last back edge to `loop_head`
917 for(const auto &t : loop_body)
918 {
919 if(
920 t->is_goto() && t->get_target() == loop_head &&
921 t->location_number > loop_end->location_number)
922 loop_end = t;
923 }
924
925 if(loop_end == loop_head)
926 {
927 log.error() << "Could not find end of the loop starting at: "
928 << loop_head->source_location() << messaget::eom;
929 throw 0;
930 }
931
932 // By definition the `loop_body` is a set of instructions computed
933 // by `natural_loops` based on the CFG.
934 // Since we perform assigns clause instrumentation by sequentially
935 // traversing instructions from `loop_head` to `loop_end`,
936 // here we ensure that all instructions in `loop_body` belong within
937 // the [loop_head, loop_end] target range.
938
939 // Check 1. (i \in loop_body) ==> loop_head <= i <= loop_end
940 for(const auto &i : loop_body)
941 {
942 if(
943 loop_head->location_number > i->location_number ||
944 i->location_number > loop_end->location_number)
945 {
947 log.error(), [&i, &loop_head](messaget::mstreamt &mstream) {
948 mstream << "Computed loop at " << loop_head->source_location()
949 << "contains an instruction beyond [loop_head, loop_end]:"
950 << messaget::eom;
951 i->output(mstream);
952 mstream << messaget::eom;
953 });
954 throw 0;
955 }
956 }
957
958 if(!loop_head_ends.emplace(loop_head, std::make_pair(loop_end, loop_body))
959 .second)
961 }
962
963 for(auto &loop_head_end : loop_head_ends)
964 {
965 auto loop_head = loop_head_end.first;
966 auto loop_end = loop_head_end.second.first;
967 // After loop-contract instrumentation, jumps to the `loop_head` will skip
968 // some instrumented instructions. So we want to make sure that there is
969 // only one jump targeting `loop_head` from `loop_end` before loop-contract
970 // instrumentation.
971 // Add a skip before `loop_head` and let all jumps (except for the
972 // `loop_end`) that target to the `loop_head` target to the skip
973 // instead.
975 goto_function.body, loop_head, goto_programt::make_skip());
976 loop_end->set_target(loop_head);
977
979 exprt invariant =
983
984 if(invariant.is_nil())
985 {
986 if(decreases_clause.is_not_nil() || assigns_clause.is_not_nil())
987 {
988 invariant = true_exprt{};
989 // assigns clause is missing; we will try to automatic inference
990 log.warning()
991 << "The loop at " << loop_head->source_location().as_string()
992 << " does not have an invariant in its contract.\n"
993 << "Hence, a default invariant ('true') is being used.\n"
994 << "This choice is sound, but verification may fail"
995 << " if it is be too weak to prove the desired properties."
996 << messaget::eom;
997 }
998 }
999 else
1000 {
1001 invariant = conjunction(invariant.operands());
1002 if(decreases_clause.is_nil())
1003 {
1004 log.warning() << "The loop at "
1005 << loop_head->source_location().as_string()
1006 << " does not have a decreases clause in its contract.\n"
1007 << "Termination of this loop will not be verified."
1008 << messaget::eom;
1009 }
1010 }
1011
1012 const auto idx = loop_nesting_graph.add_node(
1013 loop_head_end.second.second,
1014 loop_head,
1015 loop_end,
1017 invariant,
1019
1020 if(
1021 assigns_clause.is_nil() && invariant.is_nil() &&
1022 decreases_clause.is_nil())
1023 continue;
1024
1025 to_check_contracts_on_children.push_back(idx);
1026 }
1027
1028 for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer)
1029 {
1030 for(size_t inner = 0; inner < loop_nesting_graph.size(); ++inner)
1031 {
1032 if(inner == outer)
1033 continue;
1034
1035 if(loop_nesting_graph[outer].content.contains(
1036 loop_nesting_graph[inner].head_target))
1037 {
1038 if(!loop_nesting_graph[outer].content.contains(
1039 loop_nesting_graph[inner].end_target))
1040 {
1041 log.error()
1042 << "Overlapping loops at:\n"
1043 << loop_nesting_graph[outer].head_target->source_location()
1044 << "\nand\n"
1045 << loop_nesting_graph[inner].head_target->source_location()
1046 << "\nLoops must be nested or sequential for contracts to be "
1047 "enforced."
1048 << messaget::eom;
1049 }
1050 loop_nesting_graph.add_edge(inner, outer);
1051 }
1052 }
1053 }
1054
1055 // make sure all children of a contractified loop also have contracts
1056 while(!to_check_contracts_on_children.empty())
1057 {
1058 const auto loop_idx = to_check_contracts_on_children.front();
1060
1061 const auto &loop_node = loop_nesting_graph[loop_idx];
1062 if(
1063 loop_node.assigns_clause.is_nil() && loop_node.invariant.is_nil() &&
1064 loop_node.decreases_clause.is_nil())
1065 {
1066 log.error()
1067 << "Inner loop at: " << loop_node.head_target->source_location()
1068 << " does not have contracts, but an enclosing loop does.\n"
1069 << "Please provide contracts for this loop, or unwind it first."
1070 << messaget::eom;
1071 throw 0;
1072 }
1073
1074 for(const auto child_idx : loop_nesting_graph.get_predecessors(loop_idx))
1076 }
1077
1078 // Iterate over the (natural) loops in the function, in topo-sorted order,
1079 // and apply any loop contracts that we find.
1080 for(const auto &idx : loop_nesting_graph.topsort())
1081 {
1082 const auto &loop_node = loop_nesting_graph[idx];
1083 if(
1084 loop_node.assigns_clause.is_nil() && loop_node.invariant.is_nil() &&
1085 loop_node.decreases_clause.is_nil())
1086 continue;
1087
1088 // Computed loop "contents" needs to be refreshed to include any newly
1089 // introduced instrumentation, e.g. havoc instructions for assigns clause,
1090 // on inner loops in to the outer loop's contents.
1091 // Else, during the outer loop instrumentation these instructions will be
1092 // "masked" just as any other instruction not within its "contents."
1093
1095 natural_loops_mutablet updated_loops(goto_function.body);
1096
1097 // We will unwind all transformed loops twice. Store the names of
1098 // to-unwind-loops here and perform the unwinding after transformation done.
1099 // As described in `check_apply_loop_contracts`, loops with loop contracts
1100 // will be transformed to a loop that execute exactly twice: one for base
1101 // case and one for step case. So we unwind them here to avoid users
1102 // incorrectly unwind them only once.
1103 std::string to_unwind = id2string(function_name) + "." +
1104 std::to_string(loop_node.end_target->loop_number) +
1105 ":2";
1106 loop_names.push_back(to_unwind);
1107
1109 function_name,
1110 goto_function,
1111 local_may_alias,
1112 loop_node.head_target,
1113 loop_node.end_target,
1114 updated_loops.loop_map[loop_node.head_target],
1115 loop_node.assigns_clause,
1116 loop_node.invariant,
1117 loop_node.decreases_clause,
1118 symbol_table.lookup_ref(function_name).mode);
1119 }
1120}
1121
1123{
1124 // Get the function object before instrumentation.
1125 auto function_obj = goto_functions.function_map.find(function);
1126
1127 INVARIANT(
1129 "Function '" + id2string(function) + "'must exist in the goto program");
1130
1131 const auto &goto_function = function_obj->second;
1132 auto &function_body = function_obj->second.body;
1133
1134 function_cfg_infot cfg_info(goto_function);
1135
1137 function,
1139 cfg_info,
1142
1143 // Detect and track static local variables before inlining
1146
1147 // Full inlining of the function body
1148 // Inlining is performed so that function calls to a same function
1149 // occurring under different write sets get instrumented specifically
1150 // for each write set
1153
1154 decorated.throw_on_recursive_calls(log, 0);
1155
1156 // Clean up possible fake loops that are due to `IF 0!=0 GOTO i` instructions
1158
1159 // Restore internal coherence in the programs
1161
1162 INVARIANT(
1164 "Loops remain in function '" + id2string(function) +
1165 "', assigns clause checking instrumentation cannot be applied.");
1166
1167 // Start instrumentation
1168 auto instruction_it = function_body.instructions.begin();
1169
1170 // Inject local static snapshots
1173
1174 // Track targets mentioned in the specification
1175 const symbolt &function_symbol = ns.lookup(function);
1176 const code_typet &function_type = to_code_type(function_symbol.type);
1178 // assigns clauses cannot refer to the return value, but we still need an
1179 // element in there to apply the lambda function consistently
1180 if(function_type.return_type() != empty_typet())
1181 instantiation_values.push_back(exprt{ID_nil, function_type.return_type()});
1182 for(const auto &param : function_type.parameters())
1183 {
1184 instantiation_values.push_back(
1185 ns.lookup(param.get_identifier()).symbol_expr());
1186 }
1187 for(auto &target : get_contract(function, ns).c_assigns())
1188 {
1190 instrument_spec_assigns.track_spec_target(
1191 to_lambda_expr(target).application(instantiation_values), payload);
1193 }
1194
1195 // Track formal parameters
1197 for(const auto &param : function_type.parameters())
1198 {
1200 instrument_spec_assigns.track_stack_allocated(
1201 ns.lookup(param.get_identifier()).symbol_expr(), payload);
1203 }
1204
1205 // Restore internal coherence in the programs
1207
1208 // Insert write set inclusion checks.
1209 instrument_spec_assigns.instrument_instructions(
1210 function_body, instruction_it, function_body.instructions.end());
1211}
1212
1214{
1215 // Add statements to the source function
1216 // to ensure assigns clause is respected.
1218
1219 // Rename source function
1220 std::stringstream ss;
1221 ss << CPROVER_PREFIX << "contracts_original_" << function;
1222 const irep_idt mangled(ss.str());
1223 const irep_idt original(function);
1224
1226 INVARIANT(
1228 "Function to replace must exist in the program.");
1229
1230 std::swap(goto_functions.function_map[mangled], old_function->second);
1232
1233 // Place a new symbol with the mangled name into the symbol table
1235 sl.set_file("instrumented for code contracts");
1236 sl.set_line("0");
1239 mangled_sym.name = mangled;
1240 mangled_sym.base_name = mangled;
1241 mangled_sym.location = sl;
1242 const auto mangled_found = symbol_table.insert(std::move(mangled_sym));
1243 INVARIANT(
1244 mangled_found.second,
1245 "There should be no existing function called " + ss.str() +
1246 " in the symbol table because that name is a mangled name");
1247
1248 // Insert wrapper function into goto_functions
1250 INVARIANT(
1252 "There should be no function called " + id2string(function) +
1253 " in the function map because that function should have had its"
1254 " name mangled");
1255
1257 INVARIANT(
1259 "There should be a function called " + ss.str() +
1260 " in the function map because we inserted a fresh goto-program"
1261 " with that mangled name");
1262
1264 wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers;
1267}
1268
1272 goto_programt &dest)
1273{
1274 PRECONDITION(!dest.instructions.empty());
1275
1276 // build:
1277 // decl ret
1278 // decl parameter1 ...
1279 // decl history_parameter1 ... [optional]
1280 // assume(requires) [optional]
1281 // ret=function(parameter1, ...)
1282 // assert(ensures)
1283
1284 const auto &code_type = get_contract(wrapper_function, ns);
1285 goto_programt check;
1286
1287 // prepare function call including all declarations
1288 const symbolt &function_symbol = ns.lookup(mangled_function);
1290
1291 // Prepare to instantiate expressions in the callee
1292 // with expressions from the call site (e.g. the return value).
1294
1295 source_locationt source_location = function_symbol.location;
1296 // Set function in source location to original function
1297 source_location.set_function(wrapper_function);
1298
1299 // decl ret
1300 std::optional<code_returnt> return_stmt;
1301 if(code_type.return_type() != empty_typet())
1302 {
1304 code_type.return_type(),
1305 id2string(source_location.get_function()),
1306 "tmp_cc",
1307 source_location,
1308 function_symbol.mode,
1310 .symbol_expr();
1311 check.add(goto_programt::make_decl(r, source_location));
1312
1313 call.lhs() = r;
1315
1316 instantiation_values.push_back(r);
1317 }
1318
1319 // decl parameter1 ...
1320 goto_functionst::function_mapt::iterator f_it =
1323
1324 const goto_functionst::goto_functiont &gf = f_it->second;
1325 for(const auto &parameter : gf.parameter_identifiers)
1326 {
1327 PRECONDITION(!parameter.empty());
1328 const symbolt &parameter_symbol = ns.lookup(parameter);
1330 parameter_symbol.type,
1331 id2string(source_location.get_function()),
1332 "tmp_cc",
1333 source_location,
1334 parameter_symbol.mode,
1336 .symbol_expr();
1337 check.add(goto_programt::make_decl(p, source_location));
1339 p, parameter_symbol.symbol_expr(), source_location));
1340
1341 call.arguments().push_back(p);
1342
1343 instantiation_values.push_back(p);
1344 }
1345
1348 visitor.create_declarations();
1349 visitor.add_memory_map_decl(check);
1350
1351 // Generate: assume(requires)
1352 for(const auto &clause : code_type.c_requires())
1353 {
1354 auto instantiated_clause =
1355 to_lambda_expr(clause).application(instantiation_values);
1356 if(instantiated_clause.is_false())
1357 {
1359 std::string("Attempt to assume false at ")
1360 .append(clause.source_location().as_string())
1361 .append(".\nPlease update requires clause to avoid vacuity."));
1362 }
1363 source_locationt _location = clause.source_location();
1364 _location.set_comment("Assume requires clause");
1365 _location.set_property_class(ID_assume);
1369 converter,
1371 function_symbol.mode,
1372 [&visitor](goto_programt &c_requires) {
1373 visitor.update_requires(c_requires);
1374 },
1375 check,
1376 _location);
1377 }
1378
1379 // Generate all the instructions required to initialize history variables
1381 for(auto clause : code_type.c_ensures())
1382 {
1383 auto instantiated_clause =
1384 to_lambda_expr(clause).application(instantiation_values);
1385 instantiated_clause.add_source_location() = clause.source_location();
1389 }
1390
1391 // ret=mangled_function(parameter1, ...)
1392 check.add(goto_programt::make_function_call(call, source_location));
1393
1394 // Generate: assert(ensures)
1395 for(auto &clause : instantiated_ensures_clauses)
1396 {
1397 source_locationt _location = clause.source_location();
1398 _location.set_comment("Check ensures clause");
1399 _location.set_property_class(ID_postcondition);
1403 converter,
1404 clause,
1405 function_symbol.mode,
1406 [&visitor](goto_programt &ensures) { visitor.update_ensures(ensures); },
1407 check,
1408 _location);
1409 }
1410
1411 if(code_type.return_type() != empty_typet())
1412 {
1414 return_stmt.value().return_value(), source_location));
1415 }
1416
1417 // kill the is_fresh memory map
1418 visitor.add_memory_map_dead(check);
1419
1420 // prepend the new code to dest
1421 dest.destructive_insert(dest.instructions.begin(), check);
1422
1423 // restore global goto_program consistency
1425}
1426
1428 const std::set<std::string> &functions) const
1429{
1430 for(const auto &function : functions)
1431 {
1432 if(
1433 goto_functions.function_map.find(function) ==
1435 {
1437 "Function '" + function + "' was not found in the GOTO program.");
1438 }
1439 }
1440}
1441
1442void code_contractst::replace_calls(const std::set<std::string> &to_replace)
1443{
1444 if(to_replace.empty())
1445 return;
1446
1447 log.status() << "Replacing function calls with contracts" << messaget::eom;
1448
1449 check_all_functions_found(to_replace);
1450
1451 for(auto &goto_function : goto_functions.function_map)
1452 {
1453 Forall_goto_program_instructions(ins, goto_function.second.body)
1454 {
1455 if(ins->is_function_call())
1456 {
1457 if(ins->call_function().id() != ID_symbol)
1458 continue;
1459
1460 const irep_idt &called_function =
1461 to_symbol_expr(ins->call_function()).get_identifier();
1462 auto found = std::find(
1463 to_replace.begin(), to_replace.end(), id2string(called_function));
1464 if(found == to_replace.end())
1465 continue;
1466
1468 goto_function.first,
1469 ins->source_location(),
1470 goto_function.second.body,
1471 ins);
1472 }
1473 }
1474 }
1475
1476 for(auto &goto_function : goto_functions.function_map)
1477 remove_skip(goto_function.second.body);
1478
1480}
1481
1483 const std::set<std::string> &to_exclude_from_nondet_init)
1484{
1485 for(auto &goto_function : goto_functions.function_map)
1486 apply_loop_contract(goto_function.first, goto_function.second);
1487
1488 log.status() << "Adding nondeterministic initialization "
1489 "of static/global variables."
1490 << messaget::eom;
1492
1493 // unwind all transformed loops twice.
1495 {
1496 unwindsett unwindset{goto_model};
1497 unwindset.parse_unwindset(loop_names, log.get_message_handler());
1500 }
1501
1503
1504 // Record original loop number for some instrumented instructions.
1506 {
1507 auto &goto_function = goto_function_entry.second;
1508 bool is_in_loop_havoc_block = false;
1509
1510 unsigned loop_number_of_loop_havoc = 0;
1512 goto_function.body.instructions.begin();
1513 it_instr != goto_function.body.instructions.end();
1514 it_instr++)
1515 {
1516 // Don't override original loop numbers.
1517 if(original_loop_number_map.count(it_instr) != 0)
1518 continue;
1519
1520 // Store loop number for two type of instrumented instructions.
1521 // ASSIGN ENTERED_LOOP = false --- head of transformed loops.
1522 // ASSIGN ENTERED_LOOP = true --- end of transformed loops.
1523 if(
1525 {
1526 const auto &assign_lhs =
1529 id2string(assign_lhs->get_identifier()),
1530 std::string(ENTERED_LOOP) + "__");
1531 continue;
1532 }
1533
1534 // Loop havocs are assignments between
1535 // ASSIGN IN_LOOP_HAVOC_BLOCK = true
1536 // and
1537 // ASSIGN IN_LOOP_HAVOC_BLOCK = false
1538
1539 // Entering the loop-havoc block.
1541 {
1542 is_in_loop_havoc_block = it_instr->assign_rhs() == true_exprt();
1543 const auto &assign_lhs =
1546 id2string(assign_lhs->get_identifier()),
1547 std::string(IN_LOOP_HAVOC_BLOCK) + "__");
1548 continue;
1549 }
1550
1551 // Assignments in loop-havoc block are loop havocs.
1552 if(is_in_loop_havoc_block && it_instr->is_assign())
1553 {
1554 loop_havoc_set.emplace(it_instr);
1555
1556 // Store loop number for loop havoc.
1558 }
1559 }
1560 }
1561}
1562
1564 const std::set<std::string> &to_enforce,
1565 const std::set<std::string> &to_exclude_from_nondet_init)
1566{
1567 if(to_enforce.empty())
1568 return;
1569
1570 log.status() << "Enforcing contracts" << messaget ::eom;
1571
1573
1574 for(const auto &function : to_enforce)
1575 enforce_contract(function);
1576
1577 log.status() << "Adding nondeterministic initialization "
1578 "of static/global variables."
1579 << messaget::eom;
1581}
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: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: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: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:3199
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:92
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:2454
Boolean OR.
Definition std_expr.h:2270
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:3190
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
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
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(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: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:26
#define INIT_INVARIANT
Definition utils.h:28
#define IN_LOOP_HAVOC_BLOCK
Definition utils.h:27