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