cprover
Loading...
Searching...
No Matches
contracts.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Verify and use annotated loop and function contracts
4
5Author: Michael Tautschnig
6
7Date: February 2016
8
9\*******************************************************************/
10
13
14#include "contracts.h"
15
16#include <util/c_types.h>
18#include <util/expr_util.h>
19#include <util/find_symbols.h>
20#include <util/format_expr.h>
21#include <util/fresh_symbol.h>
22#include <util/graph.h>
24#include <util/message.h>
25#include <util/std_code.h>
26
30
32#include <ansi-c/c_expr.h>
38
39#include "cfg_info.h"
41#include "inlining_decorator.h"
43#include "memory_predicates.h"
44#include "utils.h"
45
46#include <algorithm>
47#include <map>
48
50 const irep_idt &function_name,
52 const local_may_aliast &local_may_alias,
53 goto_programt::targett loop_head,
55 const loopt &loop,
56 exprt assigns_clause,
57 exprt invariant,
58 exprt decreases_clause,
59 const irep_idt &mode)
60{
61 const auto loop_head_location = loop_head->source_location();
62 const auto loop_number = loop_end->loop_number;
63
64 // Vector representing a (possibly multidimensional) decreases clause
65 const auto &decreases_clause_exprs = decreases_clause.operands();
66
67 // Temporary variables for storing the multidimensional decreases clause
68 // at the start of and end of a loop body
69 std::vector<symbol_exprt> old_decreases_vars, new_decreases_vars;
70
71 // replace bound variables by fresh instances
72 if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall))
73 add_quantified_variable(symbol_table, invariant, mode);
74
75 // instrument
76 //
77 // ... preamble ...
78 // HEAD:
79 // ... eval guard ...
80 // if (!guard)
81 // goto EXIT;
82 // ... loop body ...
83 // goto HEAD;
84 // EXIT:
85 // ... postamble ...
86 //
87 // to
88 //
89 // ... preamble ...
90 // ,- initialize loop_entry history vars;
91 // | entered_loop = false
92 // loop assigns check | initial_invariant_val = invariant_expr;
93 // - unchecked, temps | in_base_case = true;
94 // func assigns check | snapshot (write_set);
95 // - disabled via pragma | goto HEAD;
96 // | STEP:
97 // --. | assert (initial_invariant_val);
98 // loop assigns check | | in_base_case = false;
99 // - not applicable >======= in_loop_havoc_block = true;
100 // func assigns check | | havoc (assigns_set);
101 // + deferred | | in_loop_havoc_block = false;
102 // --' | assume (invariant_expr);
103 // `- old_variant_val = decreases_clause_expr;
104 // * HEAD:
105 // loop assigns check ,- ... eval guard ...
106 // + assertions added | if (!guard)
107 // func assigns check | goto EXIT;
108 // - disabled via pragma `- ... loop body ...
109 // ,- entered_loop = true
110 // | if (in_base_case)
111 // | goto STEP;
112 // loop assigns check | assert (invariant_expr);
113 // - unchecked, temps | new_variant_val = decreases_clause_expr;
114 // func assigns check | assert (new_variant_val < old_variant_val);
115 // - disabled via pragma | dead old_variant_val, new_variant_val;
116 // | * assume (false);
117 // | * EXIT:
118 // To be inserted at ,~~~|~~~~ assert (entered_loop ==> !in_base_case);
119 // every unique EXIT | | dead loop_entry history vars, in_base_case;
120 // (break, goto etc.) `~~~`- ~~ dead initial_invariant_val, entered_loop;
121 // ... postamble ..
122 //
123 // Asterisks (*) denote anchor points (goto targets) for instrumentations.
124 // We insert generated code above and/below these targets.
125 //
126 // Assertions for assigns clause checking are inserted in the loop body.
127
128 // Process "loop_entry" history variables.
129 // We find and replace all "__CPROVER_loop_entry" subexpressions in invariant.
130 auto replace_history_result = replace_history_loop_entry(
131 symbol_table, invariant, loop_head_location, mode);
132 invariant.swap(replace_history_result.expression_after_replacement);
133 const auto &history_var_map = replace_history_result.parameter_to_history;
134 // an intermediate goto_program to store generated instructions
135 // to be inserted before the loop head
136 goto_programt &pre_loop_head_instrs =
137 replace_history_result.history_construction;
138
139 // Create a temporary to track if we entered the loop,
140 // i.e., the loop guard was satisfied.
141 const auto entered_loop =
143 bool_typet(),
144 id2string(loop_head_location.get_function()),
145 std::string(ENTERED_LOOP) + "__" + std::to_string(loop_number),
146 loop_head_location,
147 mode,
149 .symbol_expr();
150 pre_loop_head_instrs.add(
151 goto_programt::make_decl(entered_loop, loop_head_location));
152 pre_loop_head_instrs.add(
154
155 // Create a snapshot of the invariant so that we can check the base case,
156 // if the loop is not vacuous and must be abstracted with contracts.
157 const auto initial_invariant_val =
159 bool_typet(),
160 id2string(loop_head_location.get_function()),
162 loop_head_location,
163 mode,
165 .symbol_expr();
166 pre_loop_head_instrs.add(
167 goto_programt::make_decl(initial_invariant_val, loop_head_location));
168 {
169 // Although the invariant at this point will not have side effects,
170 // it is still a C expression, and needs to be "goto_convert"ed.
171 // Note that this conversion may emit many GOTO instructions.
172 code_assignt initial_invariant_value_assignment{
173 initial_invariant_val, invariant};
174 initial_invariant_value_assignment.add_source_location() =
175 loop_head_location;
176
178 converter.goto_convert(
179 initial_invariant_value_assignment, pre_loop_head_instrs, mode);
180 }
181
182 // Create a temporary variable to track base case vs inductive case
183 // instrumentation of the loop.
184 const auto in_base_case = get_fresh_aux_symbol(
185 bool_typet(),
186 id2string(loop_head_location.get_function()),
187 "__in_base_case",
188 loop_head_location,
189 mode,
191 .symbol_expr();
192 pre_loop_head_instrs.add(
193 goto_programt::make_decl(in_base_case, loop_head_location));
194 pre_loop_head_instrs.add(
196
197 // CAR snapshot instructions for checking assigns clause
198 goto_programt snapshot_instructions;
199
200 loop_cfg_infot cfg_info(goto_function, loop);
201
202 // track static local symbols
203 instrument_spec_assignst instrument_spec_assigns(
204 function_name,
206 cfg_info,
209
210 instrument_spec_assigns.track_static_locals_between(
211 loop_head, loop_end, snapshot_instructions);
212
213 // set of targets to havoc
214 assignst to_havoc;
215
216 if(assigns_clause.is_nil())
217 {
218 // No assigns clause was specified for this loop.
219 // Infer memory locations assigned by the loop from the loop instructions
220 // and the inferred aliasing relation.
221 try
222 {
223 infer_loop_assigns(local_may_alias, loop, to_havoc);
224
225 // remove loop-local symbols from the inferred set
226 cfg_info.erase_locals(to_havoc);
227
228 // If the set contains pairs (i, a[i]),
229 // we widen them to (i, __CPROVER_POINTER_OBJECT(a))
230 widen_assigns(to_havoc, ns);
231
232 log.debug() << "No loop assigns clause provided. Inferred targets: {";
233 // Add inferred targets to the loop assigns clause.
234 bool ran_once = false;
235 for(const auto &target : to_havoc)
236 {
237 if(ran_once)
238 log.debug() << ", ";
239 ran_once = true;
240 log.debug() << format(target);
241 instrument_spec_assigns.track_spec_target(
242 target, snapshot_instructions);
243 }
244 log.debug() << "}" << messaget::eom;
245
246 instrument_spec_assigns.get_static_locals(
247 std::inserter(to_havoc, to_havoc.end()));
248 }
249 catch(const analysis_exceptiont &exc)
250 {
251 log.error() << "Failed to infer variables being modified by the loop at "
252 << loop_head_location
253 << ".\nPlease specify an assigns clause.\nReason:"
254 << messaget::eom;
255 throw exc;
256 }
257 }
258 else
259 {
260 // An assigns clause was specified for this loop.
261 // Add the targets to the set of expressions to havoc.
262 for(const auto &target : assigns_clause.operands())
263 {
264 to_havoc.insert(target);
265 instrument_spec_assigns.track_spec_target(target, snapshot_instructions);
266 }
267 }
268
269 // Insert instrumentation
270 // This must be done before havocing the write set.
271 // FIXME: this is not true for write set targets that
272 // might depend on other write set targets.
273 pre_loop_head_instrs.destructive_append(snapshot_instructions);
274
275 // Insert a jump to the loop head
276 // (skipping over the step case initialization code below)
277 pre_loop_head_instrs.add(
278 goto_programt::make_goto(loop_head, true_exprt{}, loop_head_location));
279
280 // The STEP case instructions follow.
281 // We skip past it initially, because of the unconditional jump above,
282 // but jump back here if we get past the loop guard while in_base_case.
283
284 const auto step_case_target =
285 pre_loop_head_instrs.add(goto_programt::make_assignment(
286 in_base_case, false_exprt{}, loop_head_location));
287
288 // If we jump here, then the loop runs at least once,
289 // so add the base case assertion:
290 // assert(initial_invariant_val)
291 // We use a block scope for assertion, since it's immediately goto converted,
292 // and doesn't need to be kept around.
293 {
294 code_assertt assertion{initial_invariant_val};
295 assertion.add_source_location() = loop_head_location;
296 assertion.add_source_location().set_comment(
297 "Check loop invariant before entry");
298
300 converter.goto_convert(assertion, pre_loop_head_instrs, mode);
301 }
302
303 // Insert the first block of pre_loop_head_instrs,
304 // with a pragma to disable assigns clause checking.
305 // All of the initialization code so far introduces local temporaries,
306 // which need not be checked against the enclosing scope's assigns clause.
307 goto_function.body.destructive_insert(
308 loop_head, add_pragma_disable_assigns_check(pre_loop_head_instrs));
309
310 // Generate havocing code for assignment targets.
311 // ASSIGN in_loop_havoc_block = true;
312 // havoc (assigns_set);
313 // ASSIGN in_loop_havoc_block = false;
314 const auto in_loop_havoc_block =
316 bool_typet(),
317 id2string(loop_head_location.get_function()),
318 std::string(IN_LOOP_HAVOC_BLOCK) + +"__" + std::to_string(loop_number),
319 loop_head_location,
320 mode,
322 .symbol_expr();
323 pre_loop_head_instrs.add(
324 goto_programt::make_decl(in_loop_havoc_block, loop_head_location));
325 pre_loop_head_instrs.add(
326 goto_programt::make_assignment(in_loop_havoc_block, true_exprt{}));
327 havoc_assigns_targetst havoc_gen(
328 to_havoc, symbol_table, log.get_message_handler(), mode);
329 havoc_gen.append_full_havoc_code(loop_head_location, pre_loop_head_instrs);
330 pre_loop_head_instrs.add(
331 goto_programt::make_assignment(in_loop_havoc_block, false_exprt{}));
332
333 // Insert the second block of pre_loop_head_instrs: the havocing code.
334 // We do not `add_pragma_disable_assigns_check`,
335 // so that the enclosing scope's assigns clause instrumentation
336 // would pick these havocs up for inclusion (subset) checks.
337 goto_function.body.destructive_insert(loop_head, pre_loop_head_instrs);
338
339 // Generate: assume(invariant) just after havocing
340 // We use a block scope for assumption, since it's immediately goto converted,
341 // and doesn't need to be kept around.
342 {
343 code_assumet assumption{invariant};
344 assumption.add_source_location() = loop_head_location;
345
347 converter.goto_convert(assumption, pre_loop_head_instrs, mode);
348 }
349
350 // Create fresh temporary variables that store the multidimensional
351 // decreases clause's value before and after the loop
352 for(const auto &clause : decreases_clause.operands())
353 {
354 const auto old_decreases_var =
356 clause.type(),
357 id2string(loop_head_location.get_function()),
358 "tmp_cc",
359 loop_head_location,
360 mode,
362 .symbol_expr();
363 pre_loop_head_instrs.add(
364 goto_programt::make_decl(old_decreases_var, loop_head_location));
365 old_decreases_vars.push_back(old_decreases_var);
366
367 const auto new_decreases_var =
369 clause.type(),
370 id2string(loop_head_location.get_function()),
371 "tmp_cc",
372 loop_head_location,
373 mode,
375 .symbol_expr();
376 pre_loop_head_instrs.add(
377 goto_programt::make_decl(new_decreases_var, loop_head_location));
378 new_decreases_vars.push_back(new_decreases_var);
379 }
380
381 // TODO: Fix loop contract handling for do/while loops.
382 if(loop_end->is_goto() && !loop_end->condition().is_true())
383 {
384 log.error() << "Loop contracts are unsupported on do/while loops: "
385 << loop_head_location << messaget::eom;
386 throw 0;
387
388 // non-deterministically skip the loop if it is a do-while loop.
389 // pre_loop_head_instrs.add(goto_programt::make_goto(
390 // loop_end, side_effect_expr_nondett(bool_typet(), loop_head_location)));
391 }
392
393 // Generate: assignments to store the multidimensional decreases clause's
394 // value just before the loop_head
395 if(!decreases_clause.is_nil())
396 {
397 for(size_t i = 0; i < old_decreases_vars.size(); i++)
398 {
399 code_assignt old_decreases_assignment{
400 old_decreases_vars[i], decreases_clause_exprs[i]};
401 old_decreases_assignment.add_source_location() = loop_head_location;
402
404 converter.goto_convert(
405 old_decreases_assignment, pre_loop_head_instrs, mode);
406 }
407
408 goto_function.body.destructive_insert(
409 loop_head, add_pragma_disable_assigns_check(pre_loop_head_instrs));
410 }
411
412 // Insert the third and final block of pre_loop_head_instrs,
413 // with a pragma to disable assigns clause checking.
414 // The variables to store old variant value are local temporaries,
415 // which need not be checked against the enclosing scope's assigns clause.
416 goto_function.body.destructive_insert(
417 loop_head, add_pragma_disable_assigns_check(pre_loop_head_instrs));
418
419 // Perform write set instrumentation on the entire loop.
420 instrument_spec_assigns.instrument_instructions(
421 goto_function.body,
422 loop_head,
423 loop_end,
424 [&loop](const goto_programt::targett &t) { return loop.contains(t); });
425
426 // Now we begin instrumenting at the loop_end.
427 // `pre_loop_end_instrs` are to be inserted before `loop_end`.
428 goto_programt pre_loop_end_instrs;
429
430 // Record that we entered the loop.
431 pre_loop_end_instrs.add(
433
434 // Jump back to the step case to havoc the write set, assume the invariant,
435 // and execute an arbitrary iteration.
436 pre_loop_end_instrs.add(goto_programt::make_goto(
437 step_case_target, in_base_case, loop_head_location));
438
439 // The following code is only reachable in the step case,
440 // i.e., when in_base_case == false,
441 // because of the unconditional jump above.
442
443 // Generate the inductiveness check:
444 // assert(invariant)
445 // We use a block scope for assertion, since it's immediately goto converted,
446 // and doesn't need to be kept around.
447 {
448 code_assertt assertion{invariant};
449 assertion.add_source_location() = loop_head_location;
450 assertion.add_source_location().set_comment(
451 "Check that loop invariant is preserved");
452
454 converter.goto_convert(assertion, pre_loop_end_instrs, mode);
455 }
456
457 // Generate: assignments to store the multidimensional decreases clause's
458 // value after one iteration of the loop
459 if(!decreases_clause.is_nil())
460 {
461 for(size_t i = 0; i < new_decreases_vars.size(); i++)
462 {
463 code_assignt new_decreases_assignment{
464 new_decreases_vars[i], decreases_clause_exprs[i]};
465 new_decreases_assignment.add_source_location() = loop_head_location;
466
468 converter.goto_convert(
469 new_decreases_assignment, pre_loop_end_instrs, mode);
470 }
471
472 // Generate: assertion that the multidimensional decreases clause's value
473 // after the loop is lexicographically smaller than its initial value.
474 code_assertt monotonic_decreasing_assertion{
476 new_decreases_vars, old_decreases_vars)};
477 monotonic_decreasing_assertion.add_source_location() = loop_head_location;
478 monotonic_decreasing_assertion.add_source_location().set_comment(
479 "Check decreases clause on loop iteration");
480
482 converter.goto_convert(
483 monotonic_decreasing_assertion, pre_loop_end_instrs, mode);
484
485 // Discard the temporary variables that store decreases clause's value
486 for(size_t i = 0; i < old_decreases_vars.size(); i++)
487 {
488 pre_loop_end_instrs.add(
489 goto_programt::make_dead(old_decreases_vars[i], loop_head_location));
490 pre_loop_end_instrs.add(
491 goto_programt::make_dead(new_decreases_vars[i], loop_head_location));
492 }
493 }
494
496 goto_function.body,
497 loop_end,
498 add_pragma_disable_assigns_check(pre_loop_end_instrs));
499
500 // change the back edge into assume(false) or assume(guard)
501 loop_end->turn_into_assume();
502 loop_end->condition_nonconst() = boolean_negate(loop_end->condition());
503
504 std::set<goto_programt::targett, goto_programt::target_less_than>
505 seen_targets;
506 // Find all exit points of the loop, make temporary variables `DEAD`,
507 // and check that step case was checked for non-vacuous loops.
508 for(const auto &t : loop)
509 {
510 if(!t->is_goto())
511 continue;
512
513 auto exit_target = t->get_target();
514 if(
515 loop.contains(exit_target) ||
516 seen_targets.find(exit_target) != seen_targets.end())
517 continue;
518
519 seen_targets.insert(exit_target);
520
521 goto_programt pre_loop_exit_instrs;
522 // Assertion to check that step case was checked if we entered the loop.
523 source_locationt annotated_location = loop_head_location;
524 annotated_location.set_comment(
525 "Check that loop instrumentation was not truncated");
526 pre_loop_exit_instrs.add(goto_programt::make_assertion(
527 or_exprt{not_exprt{entered_loop}, not_exprt{in_base_case}},
528 annotated_location));
529 // Instructions to make all the temporaries go dead.
530 pre_loop_exit_instrs.add(
531 goto_programt::make_dead(in_base_case, loop_head_location));
532 pre_loop_exit_instrs.add(
533 goto_programt::make_dead(initial_invariant_val, loop_head_location));
534 for(const auto &v : history_var_map)
535 {
536 pre_loop_exit_instrs.add(
537 goto_programt::make_dead(to_symbol_expr(v.second), loop_head_location));
538 }
539 // Insert these instructions, preserving the loop end target.
541 goto_function.body, exit_target, pre_loop_exit_instrs);
542 }
543}
544
547static void throw_on_unsupported(const goto_programt &program)
548{
549 for(const auto &it : program.instructions)
550 {
551 if(
552 it.is_function_call() && it.call_function().id() == ID_symbol &&
553 to_symbol_expr(it.call_function()).get_identifier() == CPROVER_PREFIX
554 "obeys_contract")
555 {
557 CPROVER_PREFIX "obeys_contract is not supported in this version",
558 it.source_location());
559 }
560 }
561}
562
566 symbol_tablet &symbol_table,
567 goto_convertt &converter,
568 exprt &instantiated_clause,
569 const irep_idt &mode,
570 const std::function<void(goto_programt &)> &is_fresh_update,
571 goto_programt &program,
572 const source_locationt &location)
573{
574 if(
575 has_subexpr(instantiated_clause, ID_exists) ||
576 has_subexpr(instantiated_clause, ID_forall))
577 {
578 add_quantified_variable(symbol_table, instantiated_clause, mode);
579 }
580
581 goto_programt constraint;
582 if(location.get_property_class() == ID_assume)
583 {
584 code_assumet assumption(instantiated_clause);
585 assumption.add_source_location() = location;
586 converter.goto_convert(assumption, constraint, mode);
587 }
588 else
589 {
590 code_assertt assertion(instantiated_clause);
591 assertion.add_source_location() = location;
592 converter.goto_convert(assertion, constraint, mode);
593 }
594 is_fresh_update(constraint);
595 throw_on_unsupported(constraint);
596 program.destructive_append(constraint);
597}
598
599static const code_with_contract_typet &
600get_contract(const irep_idt &function, const namespacet &ns)
601{
602 const std::string &function_str = id2string(function);
603 const auto &function_symbol = ns.lookup(function);
604
605 const symbolt *contract_sym;
606 if(ns.lookup("contract::" + function_str, contract_sym))
607 {
608 // no contract provided in the source or just an empty assigns clause
609 return to_code_with_contract_type(function_symbol.type);
610 }
611
612 const auto &type = to_code_with_contract_type(contract_sym->type);
614 type == function_symbol.type,
615 "front-end should have rejected re-declarations with a different type");
616
617 return type;
618}
619
621 const irep_idt &function,
622 const source_locationt &location,
623 goto_programt &function_body,
625{
626 const auto &const_target =
627 static_cast<const goto_programt::targett &>(target);
628 // Return if the function is not named in the call; currently we don't handle
629 // function pointers.
630 PRECONDITION(const_target->call_function().id() == ID_symbol);
631
632 const irep_idt &target_function =
633 to_symbol_expr(const_target->call_function()).get_identifier();
634 const symbolt &function_symbol = ns.lookup(target_function);
635 const code_typet &function_type = to_code_type(function_symbol.type);
636
637 // Isolate each component of the contract.
638 const auto &type = get_contract(target_function, ns);
639
640 // Prepare to instantiate expressions in the callee
641 // with expressions from the call site (e.g. the return value).
642 exprt::operandst instantiation_values;
643
644 // keep track of the call's return expression to make it nondet later
645 std::optional<exprt> call_ret_opt = {};
646
647 // if true, the call return variable variable was created during replacement
648 bool call_ret_is_fresh_var = false;
649
650 if(function_type.return_type() != empty_typet())
651 {
652 // Check whether the function's return value is not disregarded.
653 if(target->call_lhs().is_not_nil())
654 {
655 // If so, have it replaced appropriately.
656 // For example, if foo() ensures that its return value is > 5, then
657 // rewrite calls to foo as follows:
658 // x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5)
659 auto &lhs_expr = const_target->call_lhs();
660 call_ret_opt = lhs_expr;
661 instantiation_values.push_back(lhs_expr);
662 }
663 else
664 {
665 // If the function does return a value, but the return value is
666 // disregarded, check if the postcondition includes the return value.
667 if(std::any_of(
668 type.c_ensures().begin(),
669 type.c_ensures().end(),
670 [](const exprt &e) {
671 return has_symbol_expr(
672 to_lambda_expr(e).where(), CPROVER_PREFIX "return_value", true);
673 }))
674 {
675 // The postcondition does mention __CPROVER_return_value, so mint a
676 // fresh variable to replace __CPROVER_return_value with.
677 call_ret_is_fresh_var = true;
678 const symbolt &fresh = get_fresh_aux_symbol(
679 function_type.return_type(),
680 id2string(target_function),
681 "ignored_return_value",
682 const_target->source_location(),
683 symbol_table.lookup_ref(target_function).mode,
684 ns,
686 auto fresh_sym_expr = fresh.symbol_expr();
687 call_ret_opt = fresh_sym_expr;
688 instantiation_values.push_back(fresh_sym_expr);
689 }
690 else
691 {
692 // unused, add a dummy with the right type
693 instantiation_values.push_back(
694 exprt{ID_nil, function_type.return_type()});
695 }
696 }
697 }
698
699 // Replace formal parameters
700 const auto &arguments = const_target->call_arguments();
701 instantiation_values.insert(
702 instantiation_values.end(), arguments.begin(), arguments.end());
703
704 const auto &mode = function_symbol.mode;
705
706 // new program where all contract-derived instructions are added
707 goto_programt new_program;
708
709 is_fresh_replacet is_fresh(
710 goto_model, log.get_message_handler(), target_function);
711 is_fresh.create_declarations();
712 is_fresh.add_memory_map_decl(new_program);
713
714 // Generate: assert(requires)
715 for(const auto &clause : type.c_requires())
716 {
717 auto instantiated_clause =
718 to_lambda_expr(clause).application(instantiation_values);
719 source_locationt _location = clause.source_location();
720 _location.set_line(location.get_line());
721 _location.set_comment(std::string("Check requires clause of ")
722 .append(target_function.c_str())
723 .append(" in ")
724 .append(function.c_str()));
725 _location.set_property_class(ID_precondition);
729 converter,
730 instantiated_clause,
731 mode,
732 [&is_fresh](goto_programt &c_requires) {
733 is_fresh.update_requires(c_requires);
734 },
735 new_program,
736 _location);
737 }
738
739 // Generate all the instructions required to initialize history variables
740 exprt::operandst instantiated_ensures_clauses;
741 for(auto clause : type.c_ensures())
742 {
743 auto instantiated_clause =
744 to_lambda_expr(clause).application(instantiation_values);
745 instantiated_clause.add_source_location() = clause.source_location();
747 symbol_table, instantiated_clause, mode, new_program);
748 instantiated_ensures_clauses.push_back(instantiated_clause);
749 }
750
751 // ASSIGNS clause should not refer to any quantified variables,
752 // and only refer to the common symbols to be replaced.
753 exprt::operandst targets;
754 for(auto &target : type.c_assigns())
755 targets.push_back(to_lambda_expr(target).application(instantiation_values));
756
757 // Create a sequence of non-deterministic assignments ...
758
759 // ... for the assigns clause targets and static locals
760 goto_programt havoc_instructions;
761 function_cfg_infot cfg_info({});
763 target_function,
764 targets,
766 cfg_info,
767 location,
770
771 havocker.get_instructions(havoc_instructions);
772
773 // ... for the return value
774 if(call_ret_opt.has_value())
775 {
776 auto &call_ret = call_ret_opt.value();
777 auto &loc = call_ret.source_location();
778 auto &type = call_ret.type();
779
780 // Declare if fresh
781 if(call_ret_is_fresh_var)
782 havoc_instructions.add(
784
785 side_effect_expr_nondett expr(type, location);
786 havoc_instructions.add(goto_programt::make_assignment(
787 code_assignt{call_ret, std::move(expr), loc}, loc));
788 }
789
790 // Insert havoc instructions immediately before the call site.
791 new_program.destructive_append(havoc_instructions);
792
793 // Generate: assume(ensures)
794 for(auto &clause : instantiated_ensures_clauses)
795 {
796 if(clause.is_false())
797 {
799 std::string("Attempt to assume false at ")
800 .append(clause.source_location().as_string())
801 .append(".\nPlease update ensures clause to avoid vacuity."));
802 }
803 source_locationt _location = clause.source_location();
804 _location.set_comment("Assume ensures clause");
805 _location.set_property_class(ID_assume);
806
810 converter,
811 clause,
812 mode,
813 [&is_fresh](goto_programt &ensures) { is_fresh.update_ensures(ensures); },
814 new_program,
815 _location);
816 }
817
818 // Kill return value variable if fresh
819 if(call_ret_is_fresh_var)
820 {
822 log.warning(), [&target](messaget::mstreamt &mstream) {
823 target->output(mstream);
824 mstream << messaget::eom;
825 });
826 auto dead_inst =
827 goto_programt::make_dead(to_symbol_expr(call_ret_opt.value()), location);
828 function_body.insert_before_swap(target, dead_inst);
829 ++target;
830 }
831
832 is_fresh.add_memory_map_dead(new_program);
833
834 // Erase original function call
835 *target = goto_programt::make_skip();
836
837 // insert contract replacement instructions
838 insert_before_swap_and_advance(function_body, target, new_program);
839
840 // Add this function to the set of replaced functions.
841 summarized.insert(target_function);
842
843 // restore global goto_program consistency
845}
846
848 const irep_idt &function_name,
849 goto_functionst::goto_functiont &goto_function)
850{
851 const bool may_have_loops = std::any_of(
852 goto_function.body.instructions.begin(),
853 goto_function.body.instructions.end(),
854 [](const goto_programt::instructiont &instruction) {
855 return instruction.is_backwards_goto();
856 });
857
858 if(!may_have_loops)
859 return;
860
863 goto_functions, function_name, ns, log.get_message_handler());
864
865 INVARIANT(
866 decorated.get_recursive_call_set().size() == 0,
867 "Recursive functions found during inlining");
868
869 // restore internal invariants
871
872 local_may_aliast local_may_alias(goto_function);
873 natural_loops_mutablet natural_loops(goto_function.body);
874
875 // A graph node type that stores information about a loop.
876 // We create a DAG representing nesting of various loops in goto_function,
877 // sort them topologically, and instrument them in the top-sorted order.
878 //
879 // The goal here is not avoid explicit "subset checks" on nested write sets.
880 // When instrumenting in a top-sorted order,
881 // the outer loop would no longer observe the inner loop's write set,
882 // but only corresponding `havoc` statements,
883 // which can be instrumented in the usual way to achieve a "subset check".
884
885 struct loop_graph_nodet : public graph_nodet<empty_edget>
886 {
887 const typename natural_loops_mutablet::loopt &content;
888 const goto_programt::targett head_target, end_target;
889 exprt assigns_clause, invariant, decreases_clause;
890
891 loop_graph_nodet(
892 const typename natural_loops_mutablet::loopt &loop,
893 const goto_programt::targett head,
894 const goto_programt::targett end,
895 const exprt &assigns,
896 const exprt &inv,
897 const exprt &decreases)
898 : content(loop),
899 head_target(head),
900 end_target(end),
901 assigns_clause(assigns),
902 invariant(inv),
903 decreases_clause(decreases)
904 {
905 }
906 };
907 grapht<loop_graph_nodet> loop_nesting_graph;
908
909 std::list<size_t> to_check_contracts_on_children;
910
911 std::map<
913 std::pair<goto_programt::targett, natural_loops_mutablet::loopt>,
915 loop_head_ends;
916
917 for(const auto &loop_head_and_content : natural_loops.loop_map)
918 {
919 const auto &loop_body = loop_head_and_content.second;
920 // Skip empty loops and self-looped node.
921 if(loop_body.size() <= 1)
922 continue;
923
924 auto loop_head = loop_head_and_content.first;
925 auto loop_end = loop_head;
926
927 // Find the last back edge to `loop_head`
928 for(const auto &t : loop_body)
929 {
930 if(
931 t->is_goto() && t->get_target() == loop_head &&
932 t->location_number > loop_end->location_number)
933 loop_end = t;
934 }
935
936 if(loop_end == loop_head)
937 {
938 log.error() << "Could not find end of the loop starting at: "
939 << loop_head->source_location() << messaget::eom;
940 throw 0;
941 }
942
943 // By definition the `loop_body` is a set of instructions computed
944 // by `natural_loops` based on the CFG.
945 // Since we perform assigns clause instrumentation by sequentially
946 // traversing instructions from `loop_head` to `loop_end`,
947 // here we ensure that all instructions in `loop_body` belong within
948 // the [loop_head, loop_end] target range.
949
950 // Check 1. (i \in loop_body) ==> loop_head <= i <= loop_end
951 for(const auto &i : loop_body)
952 {
953 if(
954 loop_head->location_number > i->location_number ||
955 i->location_number > loop_end->location_number)
956 {
958 log.error(), [&i, &loop_head](messaget::mstreamt &mstream) {
959 mstream << "Computed loop at " << loop_head->source_location()
960 << "contains an instruction beyond [loop_head, loop_end]:"
961 << messaget::eom;
962 i->output(mstream);
963 mstream << messaget::eom;
964 });
965 throw 0;
966 }
967 }
968
969 if(!loop_head_ends.emplace(loop_head, std::make_pair(loop_end, loop_body))
970 .second)
972 }
973
974 for(auto &loop_head_end : loop_head_ends)
975 {
976 auto loop_head = loop_head_end.first;
977 auto loop_end = loop_head_end.second.first;
978 // After loop-contract instrumentation, jumps to the `loop_head` will skip
979 // some instrumented instructions. So we want to make sure that there is
980 // only one jump targeting `loop_head` from `loop_end` before loop-contract
981 // instrumentation.
982 // Add a skip before `loop_head` and let all jumps (except for the
983 // `loop_end`) that target to the `loop_head` target to the skip
984 // instead.
986 goto_function.body, loop_head, goto_programt::make_skip());
987 loop_end->set_target(loop_head);
988
989 exprt assigns_clause = get_loop_assigns(loop_end);
990 exprt invariant =
992 exprt decreases_clause =
994
995 if(invariant.is_nil())
996 {
997 if(decreases_clause.is_not_nil() || assigns_clause.is_not_nil())
998 {
999 invariant = true_exprt{};
1000 // assigns clause is missing; we will try to automatic inference
1001 log.warning()
1002 << "The loop at " << loop_head->source_location().as_string()
1003 << " does not have an invariant in its contract.\n"
1004 << "Hence, a default invariant ('true') is being used.\n"
1005 << "This choice is sound, but verification may fail"
1006 << " if it is be too weak to prove the desired properties."
1007 << messaget::eom;
1008 }
1009 }
1010 else
1011 {
1012 invariant = conjunction(invariant.operands());
1013 if(decreases_clause.is_nil())
1014 {
1015 log.warning() << "The loop at "
1016 << loop_head->source_location().as_string()
1017 << " does not have a decreases clause in its contract.\n"
1018 << "Termination of this loop will not be verified."
1019 << messaget::eom;
1020 }
1021 }
1022
1023 const auto idx = loop_nesting_graph.add_node(
1024 loop_head_end.second.second,
1025 loop_head,
1026 loop_end,
1027 assigns_clause,
1028 invariant,
1029 decreases_clause);
1030
1031 if(
1032 assigns_clause.is_nil() && invariant.is_nil() &&
1033 decreases_clause.is_nil())
1034 continue;
1035
1036 to_check_contracts_on_children.push_back(idx);
1037 }
1038
1039 for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer)
1040 {
1041 for(size_t inner = 0; inner < loop_nesting_graph.size(); ++inner)
1042 {
1043 if(inner == outer)
1044 continue;
1045
1046 if(loop_nesting_graph[outer].content.contains(
1047 loop_nesting_graph[inner].head_target))
1048 {
1049 if(!loop_nesting_graph[outer].content.contains(
1050 loop_nesting_graph[inner].end_target))
1051 {
1052 log.error()
1053 << "Overlapping loops at:\n"
1054 << loop_nesting_graph[outer].head_target->source_location()
1055 << "\nand\n"
1056 << loop_nesting_graph[inner].head_target->source_location()
1057 << "\nLoops must be nested or sequential for contracts to be "
1058 "enforced."
1059 << messaget::eom;
1060 }
1061 loop_nesting_graph.add_edge(inner, outer);
1062 }
1063 }
1064 }
1065
1066 // make sure all children of a contractified loop also have contracts
1067 while(!to_check_contracts_on_children.empty())
1068 {
1069 const auto loop_idx = to_check_contracts_on_children.front();
1070 to_check_contracts_on_children.pop_front();
1071
1072 const auto &loop_node = loop_nesting_graph[loop_idx];
1073 if(
1074 loop_node.assigns_clause.is_nil() && loop_node.invariant.is_nil() &&
1075 loop_node.decreases_clause.is_nil())
1076 {
1077 log.error()
1078 << "Inner loop at: " << loop_node.head_target->source_location()
1079 << " does not have contracts, but an enclosing loop does.\n"
1080 << "Please provide contracts for this loop, or unwind it first."
1081 << messaget::eom;
1082 throw 0;
1083 }
1084
1085 for(const auto child_idx : loop_nesting_graph.get_predecessors(loop_idx))
1086 to_check_contracts_on_children.push_back(child_idx);
1087 }
1088
1089 // Iterate over the (natural) loops in the function, in topo-sorted order,
1090 // and apply any loop contracts that we find.
1091 for(const auto &idx : loop_nesting_graph.topsort())
1092 {
1093 const auto &loop_node = loop_nesting_graph[idx];
1094 if(
1095 loop_node.assigns_clause.is_nil() && loop_node.invariant.is_nil() &&
1096 loop_node.decreases_clause.is_nil())
1097 continue;
1098
1099 // Computed loop "contents" needs to be refreshed to include any newly
1100 // introduced instrumentation, e.g. havoc instructions for assigns clause,
1101 // on inner loops in to the outer loop's contents.
1102 // Else, during the outer loop instrumentation these instructions will be
1103 // "masked" just as any other instruction not within its "contents."
1104
1106 natural_loops_mutablet updated_loops(goto_function.body);
1107
1108 // We will unwind all transformed loops twice. Store the names of
1109 // to-unwind-loops here and perform the unwinding after transformation done.
1110 // As described in `check_apply_loop_contracts`, loops with loop contracts
1111 // will be transformed to a loop that execute exactly twice: one for base
1112 // case and one for step case. So we unwind them here to avoid users
1113 // incorrectly unwind them only once.
1114 std::string to_unwind = id2string(function_name) + "." +
1115 std::to_string(loop_node.end_target->loop_number) +
1116 ":2";
1117 loop_names.push_back(to_unwind);
1118
1120 function_name,
1121 goto_function,
1122 local_may_alias,
1123 loop_node.head_target,
1124 loop_node.end_target,
1125 updated_loops.loop_map[loop_node.head_target],
1126 loop_node.assigns_clause,
1127 loop_node.invariant,
1128 loop_node.decreases_clause,
1129 symbol_table.lookup_ref(function_name).mode);
1130 }
1131}
1132
1134{
1135 // Get the function object before instrumentation.
1136 auto function_obj = goto_functions.function_map.find(function);
1137
1138 INVARIANT(
1139 function_obj != goto_functions.function_map.end(),
1140 "Function '" + id2string(function) + "'must exist in the goto program");
1141
1142 const auto &goto_function = function_obj->second;
1143 auto &function_body = function_obj->second.body;
1144
1145 function_cfg_infot cfg_info(goto_function);
1146
1147 instrument_spec_assignst instrument_spec_assigns(
1148 function,
1150 cfg_info,
1153
1154 // Detect and track static local variables before inlining
1155 goto_programt snapshot_static_locals;
1156 instrument_spec_assigns.track_static_locals(snapshot_static_locals);
1157
1158 // Full inlining of the function body
1159 // Inlining is performed so that function calls to a same function
1160 // occurring under different write sets get instrumented specifically
1161 // for each write set
1163 goto_function_inline(goto_functions, function, ns, decorated);
1164
1165 decorated.throw_on_recursive_calls(log, 0);
1166
1167 // Clean up possible fake loops that are due to `IF 0!=0 GOTO i` instructions
1168 simplify_gotos(function_body, ns);
1169
1170 // Restore internal coherence in the programs
1172
1173 INVARIANT(
1174 is_loop_free(function_body, ns, log),
1175 "Loops remain in function '" + id2string(function) +
1176 "', assigns clause checking instrumentation cannot be applied.");
1177
1178 // Start instrumentation
1179 auto instruction_it = function_body.instructions.begin();
1180
1181 // Inject local static snapshots
1183 function_body, instruction_it, snapshot_static_locals);
1184
1185 // Track targets mentioned in the specification
1186 const symbolt &function_symbol = ns.lookup(function);
1187 const code_typet &function_type = to_code_type(function_symbol.type);
1188 exprt::operandst instantiation_values;
1189 // assigns clauses cannot refer to the return value, but we still need an
1190 // element in there to apply the lambda function consistently
1191 if(function_type.return_type() != empty_typet())
1192 instantiation_values.push_back(exprt{ID_nil, function_type.return_type()});
1193 for(const auto &param : function_type.parameters())
1194 {
1195 instantiation_values.push_back(
1196 ns.lookup(param.get_identifier()).symbol_expr());
1197 }
1198 for(auto &target : get_contract(function, ns).c_assigns())
1199 {
1200 goto_programt payload;
1201 instrument_spec_assigns.track_spec_target(
1202 to_lambda_expr(target).application(instantiation_values), payload);
1203 insert_before_swap_and_advance(function_body, instruction_it, payload);
1204 }
1205
1206 // Track formal parameters
1207 goto_programt snapshot_function_parameters;
1208 for(const auto &param : function_type.parameters())
1209 {
1210 goto_programt payload;
1211 instrument_spec_assigns.track_stack_allocated(
1212 ns.lookup(param.get_identifier()).symbol_expr(), payload);
1213 insert_before_swap_and_advance(function_body, instruction_it, payload);
1214 }
1215
1216 // Restore internal coherence in the programs
1218
1219 // Insert write set inclusion checks.
1220 instrument_spec_assigns.instrument_instructions(
1221 function_body, instruction_it, function_body.instructions.end());
1222}
1223
1225{
1226 // Add statements to the source function
1227 // to ensure assigns clause is respected.
1229
1230 // Rename source function
1231 std::stringstream ss;
1232 ss << CPROVER_PREFIX << "contracts_original_" << function;
1233 const irep_idt mangled(ss.str());
1234 const irep_idt original(function);
1235
1236 auto old_function = goto_functions.function_map.find(original);
1237 INVARIANT(
1238 old_function != goto_functions.function_map.end(),
1239 "Function to replace must exist in the program.");
1240
1241 std::swap(goto_functions.function_map[mangled], old_function->second);
1242 goto_functions.function_map.erase(old_function);
1243
1244 // Place a new symbol with the mangled name into the symbol table
1246 sl.set_file("instrumented for code contracts");
1247 sl.set_line("0");
1248 const symbolt *original_sym = symbol_table.lookup(original);
1249 symbolt mangled_sym = *original_sym;
1250 mangled_sym.name = mangled;
1251 mangled_sym.base_name = mangled;
1252 mangled_sym.location = sl;
1253 const auto mangled_found = symbol_table.insert(std::move(mangled_sym));
1254 INVARIANT(
1255 mangled_found.second,
1256 "There should be no existing function called " + ss.str() +
1257 " in the symbol table because that name is a mangled name");
1258
1259 // Insert wrapper function into goto_functions
1260 auto nexist_old_function = goto_functions.function_map.find(original);
1261 INVARIANT(
1262 nexist_old_function == goto_functions.function_map.end(),
1263 "There should be no function called " + id2string(function) +
1264 " in the function map because that function should have had its"
1265 " name mangled");
1266
1267 auto mangled_fun = goto_functions.function_map.find(mangled);
1268 INVARIANT(
1269 mangled_fun != goto_functions.function_map.end(),
1270 "There should be a function called " + ss.str() +
1271 " in the function map because we inserted a fresh goto-program"
1272 " with that mangled name");
1273
1274 goto_functiont &wrapper = goto_functions.function_map[original];
1275 wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers;
1277 add_contract_check(original, mangled, wrapper.body);
1278}
1279
1281 const irep_idt &wrapper_function,
1282 const irep_idt &mangled_function,
1283 goto_programt &dest)
1284{
1285 PRECONDITION(!dest.instructions.empty());
1286
1287 // build:
1288 // decl ret
1289 // decl parameter1 ...
1290 // decl history_parameter1 ... [optional]
1291 // assume(requires) [optional]
1292 // ret=function(parameter1, ...)
1293 // assert(ensures)
1294
1295 const auto &code_type = get_contract(wrapper_function, ns);
1296 goto_programt check;
1297
1298 // prepare function call including all declarations
1299 const symbolt &function_symbol = ns.lookup(mangled_function);
1300 code_function_callt call(function_symbol.symbol_expr());
1301
1302 // Prepare to instantiate expressions in the callee
1303 // with expressions from the call site (e.g. the return value).
1304 exprt::operandst instantiation_values;
1305
1306 source_locationt source_location = function_symbol.location;
1307 // Set function in source location to original function
1308 source_location.set_function(wrapper_function);
1309
1310 // decl ret
1311 std::optional<code_returnt> return_stmt;
1312 if(code_type.return_type() != empty_typet())
1313 {
1315 code_type.return_type(),
1316 id2string(source_location.get_function()),
1317 "tmp_cc",
1318 source_location,
1319 function_symbol.mode,
1321 .symbol_expr();
1322 check.add(goto_programt::make_decl(r, source_location));
1323
1324 call.lhs() = r;
1325 return_stmt = code_returnt(r);
1326
1327 instantiation_values.push_back(r);
1328 }
1329
1330 // decl parameter1 ...
1331 goto_functionst::function_mapt::iterator f_it =
1332 goto_functions.function_map.find(mangled_function);
1334
1335 const goto_functionst::goto_functiont &gf = f_it->second;
1336 for(const auto &parameter : gf.parameter_identifiers)
1337 {
1338 PRECONDITION(!parameter.empty());
1339 const symbolt &parameter_symbol = ns.lookup(parameter);
1341 parameter_symbol.type,
1342 id2string(source_location.get_function()),
1343 "tmp_cc",
1344 source_location,
1345 parameter_symbol.mode,
1347 .symbol_expr();
1348 check.add(goto_programt::make_decl(p, source_location));
1350 p, parameter_symbol.symbol_expr(), source_location));
1351
1352 call.arguments().push_back(p);
1353
1354 instantiation_values.push_back(p);
1355 }
1356
1357 is_fresh_enforcet visitor(
1358 goto_model, log.get_message_handler(), wrapper_function);
1359 visitor.create_declarations();
1360 visitor.add_memory_map_decl(check);
1361
1362 // Generate: assume(requires)
1363 for(const auto &clause : code_type.c_requires())
1364 {
1365 auto instantiated_clause =
1366 to_lambda_expr(clause).application(instantiation_values);
1367 if(instantiated_clause.is_false())
1368 {
1370 std::string("Attempt to assume false at ")
1371 .append(clause.source_location().as_string())
1372 .append(".\nPlease update requires clause to avoid vacuity."));
1373 }
1374 source_locationt _location = clause.source_location();
1375 _location.set_comment("Assume requires clause");
1376 _location.set_property_class(ID_assume);
1380 converter,
1381 instantiated_clause,
1382 function_symbol.mode,
1383 [&visitor](goto_programt &c_requires) {
1384 visitor.update_requires(c_requires);
1385 },
1386 check,
1387 _location);
1388 }
1389
1390 // Generate all the instructions required to initialize history variables
1391 exprt::operandst instantiated_ensures_clauses;
1392 for(auto clause : code_type.c_ensures())
1393 {
1394 auto instantiated_clause =
1395 to_lambda_expr(clause).application(instantiation_values);
1396 instantiated_clause.add_source_location() = clause.source_location();
1398 symbol_table, instantiated_clause, function_symbol.mode, check);
1399 instantiated_ensures_clauses.push_back(instantiated_clause);
1400 }
1401
1402 // ret=mangled_function(parameter1, ...)
1403 check.add(goto_programt::make_function_call(call, source_location));
1404
1405 // Generate: assert(ensures)
1406 for(auto &clause : instantiated_ensures_clauses)
1407 {
1408 source_locationt _location = clause.source_location();
1409 _location.set_comment("Check ensures clause");
1410 _location.set_property_class(ID_postcondition);
1414 converter,
1415 clause,
1416 function_symbol.mode,
1417 [&visitor](goto_programt &ensures) { visitor.update_ensures(ensures); },
1418 check,
1419 _location);
1420 }
1421
1422 if(code_type.return_type() != empty_typet())
1423 {
1425 return_stmt.value().return_value(), source_location));
1426 }
1427
1428 // kill the is_fresh memory map
1429 visitor.add_memory_map_dead(check);
1430
1431 // prepend the new code to dest
1432 dest.destructive_insert(dest.instructions.begin(), check);
1433
1434 // restore global goto_program consistency
1436}
1437
1439 const std::set<std::string> &functions) const
1440{
1441 for(const auto &function : functions)
1442 {
1443 if(
1444 goto_functions.function_map.find(function) ==
1446 {
1448 "Function '" + function + "' was not found in the GOTO program.");
1449 }
1450 }
1451}
1452
1453void code_contractst::replace_calls(const std::set<std::string> &to_replace)
1454{
1455 if(to_replace.empty())
1456 return;
1457
1458 log.status() << "Replacing function calls with contracts" << messaget::eom;
1459
1460 check_all_functions_found(to_replace);
1461
1462 for(auto &goto_function : goto_functions.function_map)
1463 {
1464 Forall_goto_program_instructions(ins, goto_function.second.body)
1465 {
1466 if(ins->is_function_call())
1467 {
1468 if(ins->call_function().id() != ID_symbol)
1469 continue;
1470
1471 const irep_idt &called_function =
1472 to_symbol_expr(ins->call_function()).get_identifier();
1473 auto found = std::find(
1474 to_replace.begin(), to_replace.end(), id2string(called_function));
1475 if(found == to_replace.end())
1476 continue;
1477
1479 goto_function.first,
1480 ins->source_location(),
1481 goto_function.second.body,
1482 ins);
1483 }
1484 }
1485 }
1486
1487 for(auto &goto_function : goto_functions.function_map)
1488 remove_skip(goto_function.second.body);
1489
1491}
1492
1494 const std::set<std::string> &to_exclude_from_nondet_init)
1495{
1496 for(auto &goto_function : goto_functions.function_map)
1497 apply_loop_contract(goto_function.first, goto_function.second);
1498
1499 log.status() << "Adding nondeterministic initialization "
1500 "of static/global variables."
1501 << messaget::eom;
1502 nondet_static(goto_model, to_exclude_from_nondet_init);
1503
1504 // unwind all transformed loops twice.
1506 {
1507 unwindsett unwindset{goto_model};
1509 goto_unwindt goto_unwind;
1510 goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME);
1511 }
1512
1514
1515 // Record original loop number for some instrumented instructions.
1516 for(auto &goto_function_entry : goto_functions.function_map)
1517 {
1518 auto &goto_function = goto_function_entry.second;
1519 bool is_in_loop_havoc_block = false;
1520
1521 unsigned loop_number_of_loop_havoc = 0;
1522 for(goto_programt::const_targett it_instr =
1523 goto_function.body.instructions.begin();
1524 it_instr != goto_function.body.instructions.end();
1525 it_instr++)
1526 {
1527 // Don't override original loop numbers.
1528 if(original_loop_number_map.count(it_instr) != 0)
1529 continue;
1530
1531 // Store loop number for two type of instrumented instructions.
1532 // ASSIGN ENTERED_LOOP = false --- head of transformed loops.
1533 // ASSIGN ENTERED_LOOP = true --- end of transformed loops.
1534 if(
1536 {
1537 const auto &assign_lhs =
1538 expr_try_dynamic_cast<symbol_exprt>(it_instr->assign_lhs());
1540 id2string(assign_lhs->get_identifier()),
1541 std::string(ENTERED_LOOP) + "__");
1542 continue;
1543 }
1544
1545 // Loop havocs are assignments between
1546 // ASSIGN IN_LOOP_HAVOC_BLOCK = true
1547 // and
1548 // ASSIGN IN_LOOP_HAVOC_BLOCK = false
1549
1550 // Entering the loop-havoc block.
1552 {
1553 is_in_loop_havoc_block = it_instr->assign_rhs() == true_exprt();
1554 const auto &assign_lhs =
1555 expr_try_dynamic_cast<symbol_exprt>(it_instr->assign_lhs());
1556 loop_number_of_loop_havoc = get_suffix_unsigned(
1557 id2string(assign_lhs->get_identifier()),
1558 std::string(IN_LOOP_HAVOC_BLOCK) + "__");
1559 continue;
1560 }
1561
1562 // Assignments in loop-havoc block are loop havocs.
1563 if(is_in_loop_havoc_block && it_instr->is_assign())
1564 {
1565 loop_havoc_set.emplace(it_instr);
1566
1567 // Store loop number for loop havoc.
1568 original_loop_number_map[it_instr] = loop_number_of_loop_havoc;
1569 }
1570 }
1571 }
1572}
1573
1575 const std::set<std::string> &to_enforce,
1576 const std::set<std::string> &to_exclude_from_nondet_init)
1577{
1578 if(to_enforce.empty())
1579 return;
1580
1581 log.status() << "Enforcing contracts" << messaget ::eom;
1582
1583 check_all_functions_found(to_enforce);
1584
1585 for(const auto &function : to_enforce)
1586 enforce_contract(function);
1587
1588 log.status() << "Adding nondeterministic initialization "
1589 "of static/global variables."
1590 << messaget::eom;
1591 nondet_static(goto_model, to_exclude_from_nondet_init);
1592}
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...
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
The Boolean type.
Definition std_types.h:36
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition std_code.h:270
A goto_instruction_codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
Definition std_code.h:217
namespacet ns
Definition contracts.h:150
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
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 afunction" 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
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
operandst & operands()
Definition expr.h:94
source_locationt & add_source_location()
Definition expr.h:236
The Boolean constant false.
Definition std_expr.h:3064
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...
goto_programt body
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
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 insert_before_swap(targett target)
Insertion that preserves jumps to "target".
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())
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.
instructionst::iterator targett
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
instructionst::const_iterator const_targett
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
A generic directed graph with a parametric node type.
Definition graph.h:167
std::vector< node_indext > get_predecessors(const node_indext &n) const
Definition graph.h:943
node_indext add_node(arguments &&... values)
Definition graph.h:180
void add_edge(node_indext a, node_indext b)
Definition graph.h:232
std::size_t size() const
Definition graph.h:212
std::list< node_indext > topsort() const
Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph.
Definition graph.h:879
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
void append_full_havoc_code(const source_locationt location, goto_programt &dest)
Append goto instructions to havoc the full assigns set.
Decorator for a message_handlert used during function inlining that collect names of GOTO functions c...
void throw_on_recursive_calls(messaget &log, const int error_code)
Throws the given error code if recursive call warnings happend during inlining.
const std::set< irep_idt > & get_recursive_call_set() const
A class that generates instrumentation for assigns clause checking.
void track_spec_target(const exprt &expr, goto_programt &dest)
Track an assigns clause target and generate snaphsot instructions and well-definedness assertions in ...
void track_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest)
Track a stack-allocated object and generate snaphsot instructions in dest.
void track_static_locals(goto_programt &dest)
Searches the goto instructions reachable from the start to the end of the instrumented function's ins...
void instrument_instructions(goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, const std::function< bool(const goto_programt::targett &)> &pred={})
Instruments a sequence of instructions with inclusion checks.
void track_static_locals_between(goto_programt::const_targett it, const goto_programt::const_targett end, goto_programt &dest)
Searches the goto instructions reachable between the given it and end target instructions to identify...
void get_static_locals(std::insert_iterator< C > inserter) const
Inserts the detected static local symbols into a target container.
Thrown when user-provided input cannot be processed.
Thrown when we can't handle something in an input source file.
bool is_not_nil() const
Definition irep.h:372
void swap(irept &irep)
Definition irep.h:434
bool is_nil() const
Definition irep.h:368
void add_memory_map_decl(goto_programt &program)
void update_requires(goto_programt &requires_)
void add_memory_map_dead(goto_programt &program)
void update_ensures(goto_programt &ensures)
virtual void create_declarations()
virtual void create_declarations()
exprt application(const operandst &arguments) const
loop_mapt loop_map
void erase_locals(std::set< exprt > &exprs)
Definition cfg_info.h:171
A loop, specified as a set of instructions.
source_locationt source_location
Definition message.h:239
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:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Boolean negation.
Definition std_expr.h:2327
Boolean OR.
Definition std_expr.h:2228
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
const irep_idt & get_function() const
const irep_idt & get_line() const
const irep_idt & get_property_class() const
std::string as_string() const
void set_file(const irep_idt &file)
void set_line(const irep_idt &line)
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
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
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt mode
Language mode.
Definition symbol.h:49
The Boolean constant true.
Definition std_expr.h:3055
void parse_unwindset(const std::list< std::string > &unwindset, 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.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
static format_containert< T > format(const T &o)
Definition format.h:37
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Transitively inline all function calls made from a particular function.
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
Concrete Goto Program.
#define Forall_goto_program_instructions(it, program)
A Template Class for Graphs.
Havoc function assigns clauses.
Utilities for building havoc code for expressions.
std::set< exprt > assignst
Definition havoc_utils.h:24
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:66
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:534
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:564
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:245
void add_quantified_variable(symbol_table_baset &symbol_table, exprt &expression, const irep_idt &mode)
This function recursively searches expression to find nested or non-nested quantified expressions.
Definition utils.cpp:384
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:342
bool is_loop_free(const goto_programt &goto_program, namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.
Definition utils.cpp:269
exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
Definition utils.cpp:723
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:515
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:548
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:235
void widen_assigns(assignst &assigns, const namespacet &ns)
Widen expressions in assigns with the following strategy.
Definition utils.cpp:358
exprt get_loop_invariants(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Definition utils.cpp:706
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:556
void simplify_gotos(goto_programt &goto_program, namespacet &ns)
Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SK...
Definition utils.cpp:258
exprt get_loop_decreases(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop invariants from annotated loop end.
Definition utils.cpp:728
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:586
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:191
#define ENTERED_LOOP
Definition utils.h:26
#define INIT_INVARIANT
Definition utils.h:28
#define IN_LOOP_HAVOC_BLOCK
Definition utils.h:27