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
31
33#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 // 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.
126 auto replace_history_result = replace_history_loop_entry(
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
132 goto_programt &pre_loop_head_instrs =
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),
142 loop_head_location,
143 mode,
145 .symbol_expr();
146 pre_loop_head_instrs.add(
147 goto_programt::make_decl(entered_loop, loop_head_location));
148 pre_loop_head_instrs.add(
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()),
158 loop_head_location,
159 mode,
161 .symbol_expr();
162 pre_loop_head_instrs.add(
163 goto_programt::make_decl(initial_invariant_val, loop_head_location));
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.
168 code_assignt initial_invariant_value_assignment{
169 initial_invariant_val, invariant};
170 initial_invariant_value_assignment.add_source_location() =
171 loop_head_location;
172
173 goto_convertt converter(symbol_table, log.get_message_handler());
174 converter.goto_convert(
175 initial_invariant_value_assignment, pre_loop_head_instrs, mode);
176 }
177
178 // Create a temporary variable to track base case vs inductive case
179 // instrumentation of the loop.
180 const auto in_base_case = get_fresh_aux_symbol(
181 bool_typet(),
182 id2string(loop_head_location.get_function()),
183 "__in_base_case",
184 loop_head_location,
185 mode,
187 .symbol_expr();
188 pre_loop_head_instrs.add(
189 goto_programt::make_decl(in_base_case, loop_head_location));
190 pre_loop_head_instrs.add(
192
193 // CAR snapshot instructions for checking assigns clause
194 goto_programt snapshot_instructions;
195
196 loop_cfg_infot cfg_info(goto_function, loop);
197
198 // track static local symbols
199 instrument_spec_assignst instrument_spec_assigns(
200 function_name,
202 cfg_info,
204 log.get_message_handler());
205
206 instrument_spec_assigns.track_static_locals_between(
207 loop_head, loop_end, snapshot_instructions);
208
209 // set of targets to havoc
210 assignst 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))
226 widen_assigns(to_havoc, ns);
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 "
248 << loop_head_location
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.
269 pre_loop_head_instrs.destructive_append(snapshot_instructions);
270
271 // Insert a jump to the loop head
272 // (skipping over the step case initialization code below)
273 pre_loop_head_instrs.add(
274 goto_programt::make_goto(loop_head, true_exprt{}, loop_head_location));
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 =
281 pre_loop_head_instrs.add(goto_programt::make_assignment(
282 in_base_case, false_exprt{}, loop_head_location));
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 {
290 code_assertt assertion{initial_invariant_val};
291 assertion.add_source_location() = loop_head_location;
293 "Check loop invariant before entry");
294
295 goto_convertt converter(symbol_table, log.get_message_handler());
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(
304 loop_head, add_pragma_disable_assigns_check(pre_loop_head_instrs));
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),
315 loop_head_location,
316 mode,
318 .symbol_expr();
319 pre_loop_head_instrs.add(
320 goto_programt::make_decl(in_loop_havoc_block, loop_head_location));
321 pre_loop_head_instrs.add(
322 goto_programt::make_assignment(in_loop_havoc_block, true_exprt{}));
323 havoc_assigns_targetst havoc_gen(
324 to_havoc, symbol_table, log.get_message_handler(), mode);
325 havoc_gen.append_full_havoc_code(loop_head_location, pre_loop_head_instrs);
326 pre_loop_head_instrs.add(
327 goto_programt::make_assignment(in_loop_havoc_block, false_exprt{}));
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};
340 assumption.add_source_location() = loop_head_location;
341
342 goto_convertt converter(symbol_table, log.get_message_handler());
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",
355 loop_head_location,
356 mode,
358 .symbol_expr();
359 pre_loop_head_instrs.add(
360 goto_programt::make_decl(old_decreases_var, loop_head_location));
361 old_decreases_vars.push_back(old_decreases_var);
362
363 const auto new_decreases_var =
365 clause.type(),
366 id2string(loop_head_location.get_function()),
367 "tmp_cc",
368 loop_head_location,
369 mode,
371 .symbol_expr();
372 pre_loop_head_instrs.add(
373 goto_programt::make_decl(new_decreases_var, loop_head_location));
374 new_decreases_vars.push_back(new_decreases_var);
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: "
381 << loop_head_location << messaget::eom;
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 {
395 code_assignt old_decreases_assignment{
396 old_decreases_vars[i], decreases_clause_exprs[i]};
397 old_decreases_assignment.add_source_location() = loop_head_location;
398
399 goto_convertt converter(symbol_table, log.get_message_handler());
400 converter.goto_convert(
401 old_decreases_assignment, pre_loop_head_instrs, mode);
402 }
403
404 goto_function.body.destructive_insert(
405 loop_head, add_pragma_disable_assigns_check(pre_loop_head_instrs));
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(
413 loop_head, add_pragma_disable_assigns_check(pre_loop_head_instrs));
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`.
424 goto_programt pre_loop_end_instrs;
425
426 // Record that we entered the loop.
427 pre_loop_end_instrs.add(
429
430 // Jump back to the step case to havoc the write set, assume the invariant,
431 // and execute an arbitrary iteration.
432 pre_loop_end_instrs.add(goto_programt::make_goto(
433 step_case_target, in_base_case, loop_head_location));
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};
445 assertion.add_source_location() = loop_head_location;
447 "Check that loop invariant is preserved");
448
449 goto_convertt converter(symbol_table, log.get_message_handler());
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 {
459 code_assignt new_decreases_assignment{
460 new_decreases_vars[i], decreases_clause_exprs[i]};
461 new_decreases_assignment.add_source_location() = loop_head_location;
462
463 goto_convertt converter(symbol_table, log.get_message_handler());
464 converter.goto_convert(
465 new_decreases_assignment, pre_loop_end_instrs, mode);
466 }
467
468 // Generate: assertion that the multidimensional decreases clause's value
469 // after the loop is lexicographically smaller than its initial value.
470 code_assertt monotonic_decreasing_assertion{
472 new_decreases_vars, old_decreases_vars)};
473 monotonic_decreasing_assertion.add_source_location() = loop_head_location;
474 monotonic_decreasing_assertion.add_source_location().set_comment(
475 "Check decreases clause on loop iteration");
476
477 goto_convertt converter(symbol_table, log.get_message_handler());
478 converter.goto_convert(
479 monotonic_decreasing_assertion, pre_loop_end_instrs, mode);
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 {
484 pre_loop_end_instrs.add(
485 goto_programt::make_dead(old_decreases_vars[i], loop_head_location));
486 pre_loop_end_instrs.add(
487 goto_programt::make_dead(new_decreases_vars[i], loop_head_location));
488 }
489 }
490
492 goto_function.body,
493 loop_end,
494 add_pragma_disable_assigns_check(pre_loop_end_instrs));
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>
501 seen_targets;
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) ||
512 seen_targets.find(exit_target) != seen_targets.end())
513 continue;
514
515 seen_targets.insert(exit_target);
516
517 goto_programt pre_loop_exit_instrs;
518 // Assertion to check that step case was checked if we entered the loop.
519 source_locationt annotated_location = loop_head_location;
520 annotated_location.set_comment(
521 "Check that loop instrumentation was not truncated");
522 pre_loop_exit_instrs.add(goto_programt::make_assertion(
523 or_exprt{not_exprt{entered_loop}, not_exprt{in_base_case}},
524 annotated_location));
525 // Instructions to make all the temporaries go dead.
526 pre_loop_exit_instrs.add(
527 goto_programt::make_dead(in_base_case, loop_head_location));
528 pre_loop_exit_instrs.add(
529 goto_programt::make_dead(initial_invariant_val, loop_head_location));
530 for(const auto &v : history_var_map)
531 {
532 pre_loop_exit_instrs.add(
533 goto_programt::make_dead(to_symbol_expr(v.second), loop_head_location));
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,
564 exprt &instantiated_clause,
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 {
573 code_assumet assumption(instantiated_clause);
574 assumption.add_source_location() = location;
575 converter.goto_convert(assumption, constraint, mode);
576 }
577 else
578 {
579 code_assertt assertion(instantiated_clause);
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
598 return to_code_with_contract_type(function_symbol.type);
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,
612 goto_programt &function_body,
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).
631 exprt::operandst instantiation_values;
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();
649 call_ret_opt = lhs_expr;
650 instantiation_values.push_back(lhs_expr);
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.
666 call_ret_is_fresh_var = true;
667 const symbolt &fresh = get_fresh_aux_symbol(
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();
676 call_ret_opt = fresh_sym_expr;
677 instantiation_values.push_back(fresh_sym_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();
690 instantiation_values.insert(
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
696 goto_programt new_program;
697
698 is_fresh_replacet is_fresh(
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 {
706 auto instantiated_clause =
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);
715 goto_convertt converter(symbol_table, log.get_message_handler());
718 converter,
719 instantiated_clause,
720 mode,
721 [&is_fresh](goto_programt &c_requires) {
722 is_fresh.update_requires(c_requires);
723 },
724 new_program,
725 _location);
726 }
727
728 // Generate all the instructions required to initialize history variables
729 exprt::operandst instantiated_ensures_clauses;
730 for(auto clause : type.c_ensures())
731 {
732 auto instantiated_clause =
733 to_lambda_expr(clause).application(instantiation_values);
734 instantiated_clause.add_source_location() = clause.source_location();
736 symbol_table, instantiated_clause, mode, new_program);
737 instantiated_ensures_clauses.push_back(instantiated_clause);
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
749 goto_programt havoc_instructions;
750 function_cfg_infot cfg_info({});
752 target_function,
753 targets,
755 cfg_info,
756 location,
758 log.get_message_handler());
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
770 if(call_ret_is_fresh_var)
771 havoc_instructions.add(
773
774 side_effect_expr_nondett expr(type, location);
775 havoc_instructions.add(goto_programt::make_assignment(
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
796 goto_convertt converter(symbol_table, log.get_message_handler());
799 converter,
800 clause,
801 mode,
802 [&is_fresh](goto_programt &ensures) { is_fresh.update_ensures(ensures); },
803 new_program,
804 _location);
805 }
806
807 // Kill return value variable if fresh
808 if(call_ret_is_fresh_var)
809 {
810 log.conditional_output(
811 log.warning(), [&target](messaget::mstreamt &mstream) {
812 target->output(mstream);
813 mstream << messaget::eom;
814 });
815 auto dead_inst =
816 goto_programt::make_dead(to_symbol_expr(call_ret_opt.value()), location);
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
827 insert_before_swap_and_advance(function_body, target, new_program);
828
829 // Add this function to the set of replaced functions.
830 summarized.insert(target_function);
831
832 // restore global goto_program consistency
833 goto_functions.update();
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
850 inlining_decoratort decorated(log.get_message_handler());
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
859 goto_functions.update();
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;
877 const goto_programt::targett head_target, end_target;
878 exprt assigns_clause, invariant, decreases_clause;
879
880 loop_graph_nodet(
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 };
896 grapht<loop_graph_nodet> loop_nesting_graph;
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>,
904 loop_head_ends;
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 {
946 log.conditional_output(
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
978 exprt assigns_clause = get_loop_assigns(loop_end);
979 exprt invariant =
980 get_loop_invariants(loop_end, loop_contract_config.check_side_effect);
981 exprt decreases_clause =
982 get_loop_decreases(loop_end, loop_contract_config.check_side_effect);
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,
1016 assigns_clause,
1017 invariant,
1018 decreases_clause);
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();
1059 to_check_contracts_on_children.pop_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))
1075 to_check_contracts_on_children.push_back(child_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
1094 goto_functions.update();
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(
1128 function_obj != goto_functions.function_map.end(),
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
1136 instrument_spec_assignst instrument_spec_assigns(
1137 function,
1139 cfg_info,
1141 log.get_message_handler());
1142
1143 // Detect and track static local variables before inlining
1144 goto_programt snapshot_static_locals;
1145 instrument_spec_assigns.track_static_locals(snapshot_static_locals);
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
1151 inlining_decoratort decorated(log.get_message_handler());
1152 goto_function_inline(goto_functions, function, ns, decorated);
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
1157 simplify_gotos(function_body, ns);
1158
1159 // Restore internal coherence in the programs
1160 goto_functions.update();
1161
1162 INVARIANT(
1163 is_loop_free(function_body, ns, log),
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
1172 function_body, instruction_it, snapshot_static_locals);
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);
1177 exprt::operandst instantiation_values;
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 {
1189 goto_programt payload;
1190 instrument_spec_assigns.track_spec_target(
1191 to_lambda_expr(target).application(instantiation_values), payload);
1192 insert_before_swap_and_advance(function_body, instruction_it, payload);
1193 }
1194
1195 // Track formal parameters
1196 goto_programt snapshot_function_parameters;
1197 for(const auto &param : function_type.parameters())
1198 {
1199 goto_programt payload;
1200 instrument_spec_assigns.track_stack_allocated(
1201 ns.lookup(param.get_identifier()).symbol_expr(), payload);
1202 insert_before_swap_and_advance(function_body, instruction_it, payload);
1203 }
1204
1205 // Restore internal coherence in the programs
1206 goto_functions.update();
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
1225 auto old_function = goto_functions.function_map.find(original);
1226 INVARIANT(
1227 old_function != goto_functions.function_map.end(),
1228 "Function to replace must exist in the program.");
1229
1230 std::swap(goto_functions.function_map[mangled], old_function->second);
1231 goto_functions.function_map.erase(old_function);
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");
1237 const symbolt *original_sym = symbol_table.lookup(original);
1238 symbolt mangled_sym = *original_sym;
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
1249 auto nexist_old_function = goto_functions.function_map.find(original);
1250 INVARIANT(
1251 nexist_old_function == goto_functions.function_map.end(),
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
1256 auto mangled_fun = goto_functions.function_map.find(mangled);
1257 INVARIANT(
1258 mangled_fun != goto_functions.function_map.end(),
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
1263 goto_functiont &wrapper = goto_functions.function_map[original];
1264 wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers;
1266 add_contract_check(original, mangled, wrapper.body);
1267}
1268
1270 const irep_idt &wrapper_function,
1271 const irep_idt &mangled_function,
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);
1289 code_function_callt call(function_symbol.symbol_expr());
1290
1291 // Prepare to instantiate expressions in the callee
1292 // with expressions from the call site (e.g. the return value).
1293 exprt::operandst instantiation_values;
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;
1314 return_stmt = code_returnt(r);
1315
1316 instantiation_values.push_back(r);
1317 }
1318
1319 // decl parameter1 ...
1320 goto_functionst::function_mapt::iterator f_it =
1321 goto_functions.function_map.find(mangled_function);
1322 PRECONDITION(f_it != goto_functions.function_map.end());
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
1346 is_fresh_enforcet visitor(
1347 goto_model, log.get_message_handler(), wrapper_function);
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);
1366 goto_convertt converter(symbol_table, log.get_message_handler());
1369 converter,
1370 instantiated_clause,
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
1380 exprt::operandst instantiated_ensures_clauses;
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();
1387 symbol_table, instantiated_clause, function_symbol.mode, check);
1388 instantiated_ensures_clauses.push_back(instantiated_clause);
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);
1400 goto_convertt converter(symbol_table, log.get_message_handler());
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
1424 goto_functions.update();
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) ==
1434 goto_functions.function_map.end())
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
1479 goto_functions.update();
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;
1491 nondet_static(goto_model, to_exclude_from_nondet_init);
1492
1493 // unwind all transformed loops twice.
1494 if(loop_contract_config.unwind_transformed_loops)
1495 {
1496 unwindsett unwindset{goto_model};
1497 unwindset.parse_unwindset(loop_names, log.get_message_handler());
1498 goto_unwindt goto_unwind;
1499 goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME);
1500 }
1501
1503
1504 // Record original loop number for some instrumented instructions.
1505 for(auto &goto_function_entry : goto_functions.function_map)
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;
1511 for(goto_programt::const_targett it_instr =
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 =
1527 expr_try_dynamic_cast<symbol_exprt>(it_instr->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 =
1544 expr_try_dynamic_cast<symbol_exprt>(it_instr->assign_lhs());
1545 loop_number_of_loop_havoc = get_suffix_unsigned(
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.
1557 original_loop_number_map[it_instr] = loop_number_of_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
1572 check_all_functions_found(to_enforce);
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;
1580 nondet_static(goto_model, to_exclude_from_nondet_init);
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...
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 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
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:3200
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
::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())
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.
instructiont::target_less_than target_less_than
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
loop_templatet< T, C > loopt
void erase_locals(std::set< exprt > &exprs)
Definition cfg_info.h:171
static eomt eom
Definition message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Boolean negation.
Definition std_expr.h:2459
Boolean OR.
Definition std_expr.h:2275
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
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
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
The symbol table.
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:3191
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
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition expr_util.cpp:98
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.
natural_loops_templatet< goto_programt, goto_programt::targett, goto_programt::target_less_than > natural_loops_mutablet
static void nondet_static(const namespacet &ns, goto_modelt &goto_model, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
Definition std_expr.cpp:83
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
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)
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)
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 invariants 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
dstringt irep_idt