CBMC
contracts.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Verify and use annotated loop and function contracts
4 
5 Author: Michael Tautschnig
6 
7 Date: February 2016
8 
9 \*******************************************************************/
10 
13 
14 #include "contracts.h"
15 
16 #include <util/c_types.h>
17 #include <util/exception_utils.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>
23 #include <util/mathematical_expr.h>
24 #include <util/message.h>
25 #include <util/std_code.h>
26 
30 
32 #include <ansi-c/c_expr.h>
35 #include <goto-instrument/unwind.h>
37 #include <langapi/language_util.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,
51  goto_functionst::goto_functiont &goto_function,
52  const local_may_aliast &local_may_alias,
53  goto_programt::targett loop_head,
54  goto_programt::targett loop_end,
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,
144  symbol_table)
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,
160  symbol_table)
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 
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,
186  symbol_table)
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(
191  goto_programt::make_assignment(in_base_case, true_exprt{}));
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,
203  symbol_table,
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;
292  assertion.add_source_location().set_comment(
293  "Check loop invariant before entry");
294 
296  converter.goto_convert(assertion, pre_loop_head_instrs, mode);
297  }
298 
299  // Insert the first block of pre_loop_head_instrs,
300  // with a pragma to disable assigns clause checking.
301  // All of the initialization code so far introduces local temporaries,
302  // which need not be checked against the enclosing scope's assigns clause.
303  goto_function.body.destructive_insert(
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,
317  symbol_table)
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 
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,
357  symbol_table)
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,
370  symbol_table)
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 
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(
428  goto_programt::make_assignment(entered_loop, true_exprt{}));
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;
446  assertion.add_source_location().set_comment(
447  "Check that loop invariant is preserved");
448 
450  converter.goto_convert(assertion, pre_loop_end_instrs, mode);
451  }
452 
453  // Generate: assignments to store the multidimensional decreases clause's
454  // value after one iteration of the loop
455  if(!decreases_clause.is_nil())
456  {
457  for(size_t i = 0; i < new_decreases_vars.size(); i++)
458  {
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 
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 
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 
543 static 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 
588 static const code_with_contract_typet &
589 get_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,
613  goto_programt::targett &target)
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,
674  symbol_table);
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);
717  symbol_table,
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,
757  symbol_table,
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(
772  goto_programt::make_decl(to_symbol_expr(call_ret), loc));
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 
798  symbol_table,
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  {
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
834 }
835 
837  const irep_idt &function_name,
838  goto_functionst::goto_functiont &goto_function)
839 {
840  const bool may_have_loops = std::any_of(
841  goto_function.body.instructions.begin(),
842  goto_function.body.instructions.end(),
843  [](const goto_programt::instructiont &instruction) {
844  return instruction.is_backwards_goto();
845  });
846 
847  if(!may_have_loops)
848  return;
849 
852  goto_functions, function_name, ns, log.get_message_handler());
853 
854  INVARIANT(
855  decorated.get_recursive_call_set().size() == 0,
856  "Recursive functions found during inlining");
857 
858  // restore internal invariants
860 
861  local_may_aliast local_may_alias(goto_function);
862  natural_loops_mutablet natural_loops(goto_function.body);
863 
864  // A graph node type that stores information about a loop.
865  // We create a DAG representing nesting of various loops in goto_function,
866  // sort them topologically, and instrument them in the top-sorted order.
867  //
868  // The goal here is not avoid explicit "subset checks" on nested write sets.
869  // When instrumenting in a top-sorted order,
870  // the outer loop would no longer observe the inner loop's write set,
871  // but only corresponding `havoc` statements,
872  // which can be instrumented in the usual way to achieve a "subset check".
873 
874  struct loop_graph_nodet : public graph_nodet<empty_edget>
875  {
876  const typename natural_loops_mutablet::loopt &content;
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  {
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)
960  UNREACHABLE;
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 =
981  exprt decreases_clause =
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 
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,
1140  symbol_table,
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
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
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
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
1234  source_locationt sl;
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,
1309  symbol_table)
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,
1335  symbol_table)
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);
1368  symbol_table,
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);
1402  symbol_table,
1403  converter,
1404  clause,
1405  function_symbol.mode,
1406  [&visitor](goto_programt &ensures) { visitor.update_ensures(ensures); },
1407  check,
1408  _location);
1409  }
1410 
1411  if(code_type.return_type() != empty_typet())
1412  {
1414  return_stmt.value().return_value(), source_location));
1415  }
1416 
1417  // kill the is_fresh memory map
1418  visitor.add_memory_map_dead(check);
1419 
1420  // prepend the new code to dest
1421  dest.destructive_insert(dest.instructions.begin(), check);
1422 
1423  // restore global goto_program consistency
1425 }
1426 
1428  const std::set<std::string> &functions) const
1429 {
1430  for(const auto &function : functions)
1431  {
1432  if(
1433  goto_functions.function_map.find(function) ==
1435  {
1437  "Function '" + function + "' was not found in the GOTO program.");
1438  }
1439  }
1440 }
1441 
1442 void code_contractst::replace_calls(const std::set<std::string> &to_replace)
1443 {
1444  if(to_replace.empty())
1445  return;
1446 
1447  log.status() << "Replacing function calls with contracts" << messaget::eom;
1448 
1449  check_all_functions_found(to_replace);
1450 
1451  for(auto &goto_function : goto_functions.function_map)
1452  {
1453  Forall_goto_program_instructions(ins, goto_function.second.body)
1454  {
1455  if(ins->is_function_call())
1456  {
1457  if(ins->call_function().id() != ID_symbol)
1458  continue;
1459 
1460  const irep_idt &called_function =
1461  to_symbol_expr(ins->call_function()).get_identifier();
1462  auto found = std::find(
1463  to_replace.begin(), to_replace.end(), id2string(called_function));
1464  if(found == to_replace.end())
1465  continue;
1466 
1468  goto_function.first,
1469  ins->source_location(),
1470  goto_function.second.body,
1471  ins);
1472  }
1473  }
1474  }
1475 
1476  for(auto &goto_function : goto_functions.function_map)
1477  remove_skip(goto_function.second.body);
1478 
1480 }
1481 
1483  const std::set<std::string> &to_exclude_from_nondet_init)
1484 {
1485  for(auto &goto_function : goto_functions.function_map)
1486  apply_loop_contract(goto_function.first, goto_function.second);
1487 
1488  log.status() << "Adding nondeterministic initialization "
1489  "of static/global variables."
1490  << messaget::eom;
1491  nondet_static(goto_model, to_exclude_from_nondet_init);
1492 
1493  // unwind all transformed loops twice.
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(
1524  is_transformed_loop_end(it_instr) || is_transformed_loop_head(it_instr))
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 ...
Definition: contracts.cpp:609
void enforce_contract(const irep_idt &function)
Enforce contract of a single function.
Definition: contracts.cpp:1213
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.
Definition: contracts.cpp:836
void check_all_functions_found(const std::set< std::string > &functions) const
Throws an exception if some function functions is found in the program.
Definition: contracts.cpp:1427
void check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
Definition: contracts.cpp:1122
messaget & log
Definition: contracts.h:157
void apply_loop_contracts(const std::set< std::string > &to_exclude_from_nondet_init={})
Applies loop contract transformations.
Definition: contracts.cpp:1482
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.
Definition: contracts.cpp:1563
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.
Definition: contracts.cpp:1442
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...
Definition: contracts.cpp:1269
goto_instruction_codet representation of a function call statement.
goto_instruction_codet representation of a "return from a function" statement.
Base type of functions.
Definition: std_types.h:583
const typet & return_type() const
Definition: std_types.h:689
const parameterst & parameters() const
Definition: std_types.h:699
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
const char * c_str() const
Definition: dstring.h:116
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
source_locationt & add_source_location()
Definition: expr.h:236
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
operandst & operands()
Definition: expr.h:94
The Boolean constant false.
Definition: std_expr.h:3072
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...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:874
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:971
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:643
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:730
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:722
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())
Definition: goto_program.h:891
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.
Definition: goto_program.h:739
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())
Definition: goto_program.h:964
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:933
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.
Definition: havoc_utils.cpp:21
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
Definition: loop_analysis.h:88
void erase_locals(std::set< exprt > &exprs)
Definition: cfg_info.h:171
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
source_locationt source_location
Definition: message.h:239
mstreamt & error() const
Definition: message.h:391
mstreamt & warning() const
Definition: message.h:396
mstreamt & status() const
Definition: message.h:406
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
mstreamt & debug() const
Definition: message.h:421
message_handlert & get_message_handler()
Definition: message.h:183
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:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
Boolean negation.
Definition: std_expr.h:2327
Boolean OR.
Definition: std_expr.h:2228
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
const irep_idt & get_function() const
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
const irep_idt & get_property_class() const
const irep_idt & get_line() const
std::string as_string() const
void set_file(const irep_idt &file)
void set_line(const irep_idt &line)
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Definition: symbol_table.h:14
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:3063
static const code_with_contract_typet & get_contract(const irep_idt &function, const namespacet &ns)
Definition: contracts.cpp:589
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...
Definition: contracts.cpp:561
static void throw_on_unsupported(const goto_programt &program)
Throws an exception if a contract uses unsupported constructs like:
Definition: contracts.cpp:543
Verify and use annotated invariants and pre/post-conditions.
#define CPROVER_PREFIX
static const std::map< dfcc_funt, int > to_unwind
set of functions that need to be unwound to assigns clause size with corresponding loop identifiers.
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:103
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:22
void add_pragma_disable_assigns_check(source_locationt &location)
Adds a pragma on a source_locationt to disable inclusion checking.
Specify write set in function contracts.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
static int8_t r
Definition: irep_hash.h:60
Field-insensitive, location-sensitive may-alias analysis.
natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
API to expression classes for 'mathematical' expressions.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
Predicates to specify memory footprint in function contracts.
static void nondet_static(const namespacet &ns, goto_modelt &goto_model, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:87
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
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:83
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
A total order over targett and const_targett.
Definition: goto_program.h:392
Loop unwinding.
Loop unwinding.
void generate_history_variables_initialization(symbol_table_baset &symbol_table, exprt &clause, const irep_idt &mode, goto_programt &program)
This function generates all the instructions required to initialize history variables.
Definition: utils.cpp:494
bool is_assignment_to_instrumented_variable(const goto_programt::const_targett &target, std::string var_name)
Return true if target is an assignment to an instrumented variable with name var_name.
Definition: utils.cpp:524
void insert_before_and_update_jumps(goto_programt &destination, goto_programt::targett &target, const goto_programt::instructiont &i)
Insert a goto instruction before a target instruction iterator and update targets of all jumps that p...
Definition: utils.cpp:247
void infer_loop_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
Infer loop assigns using alias analysis result local_may_alias.
Definition: utils.cpp:344
bool is_loop_free(const goto_programt &goto_program, const namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.
Definition: utils.cpp:271
exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
Extract loop assigns from annotated loop end.
Definition: utils.cpp:683
replace_history_parametert replace_history_loop_entry(symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode)
This function recursively identifies the "loop_entry" expressions within expr and replaces them with ...
Definition: utils.cpp:475
bool is_transformed_loop_head(const goto_programt::const_targett &target)
Return true if target is the head of some transformed loop.
Definition: utils.cpp:508
void insert_before_swap_and_advance(goto_programt &destination, goto_programt::targett &target, goto_programt &payload)
Insert a goto program before a target instruction iterator and advance the iterator.
Definition: utils.cpp:237
void widen_assigns(assignst &assigns, const namespacet &ns)
Widen expressions in assigns with the following strategy.
Definition: utils.cpp:360
void simplify_gotos(goto_programt &goto_program, const namespacet &ns)
Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SK...
Definition: utils.cpp:260
exprt get_loop_invariants(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop invariants from annotated loop end.
Definition: utils.cpp:666
bool is_transformed_loop_end(const goto_programt::const_targett &target)
Return true if target is the end of some transformed loop.
Definition: utils.cpp:516
exprt get_loop_decreases(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop decreases from annotated loop end.
Definition: utils.cpp:688
unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix)
Convert the suffix digits right after prefix of str into unsigned.
Definition: utils.cpp:546
exprt generate_lexicographic_less_than_check(const std::vector< symbol_exprt > &lhs, const std::vector< symbol_exprt > &rhs)
Generate a lexicographic less-than comparison over ordered tuples.
Definition: utils.cpp:193
#define ENTERED_LOOP
Definition: utils.h:26
#define INIT_INVARIANT
Definition: utils.h:28
#define IN_LOOP_HAVOC_BLOCK
Definition: utils.h:27