cprover
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 <algorithm>
17 #include <map>
18 
21 
22 #include <ansi-c/c_expr.h>
23 
25 
29 
30 #include <langapi/language_util.h>
31 
32 #include <util/c_types.h>
33 #include <util/expr_util.h>
34 #include <util/find_symbols.h>
35 #include <util/format_expr.h>
36 #include <util/fresh_symbol.h>
37 #include <util/graph.h>
38 #include <util/mathematical_expr.h>
40 #include <util/message.h>
43 #include <util/replace_symbol.h>
44 #include <util/std_code.h>
45 
48 #include "memory_predicates.h"
49 #include "utils.h"
50 
60 {
61 private:
64 
65  void parse_message(const std::string &message)
66  {
67  if(message.find("recursion is ignored on call") != std::string::npos)
69  }
70 
71 public:
72  explicit inlining_decoratort(message_handlert &_wrapped) : wrapped(_wrapped)
73  {
74  }
75 
77  {
79  }
80 
81  void print(unsigned level, const std::string &message) override
82  {
83  parse_message(message);
84  wrapped.print(level, message);
85  }
86 
87  void print(unsigned level, const xmlt &xml) override
88  {
89  wrapped.print(level, xml);
90  }
91 
92  void print(unsigned level, const jsont &json) override
93  {
94  wrapped.print(level, json);
95  }
96 
97  void print(unsigned level, const structured_datat &data) override
98  {
99  wrapped.print(level, data);
100  }
101 
102  void print(
103  unsigned level,
104  const std::string &message,
105  const source_locationt &location) override
106  {
107  parse_message(message);
108  wrapped.print(level, message, location);
109  return;
110  }
111 
112  void flush(unsigned i) override
113  {
114  return wrapped.flush(i);
115  }
116 
117  void set_verbosity(unsigned _verbosity)
118  {
119  wrapped.set_verbosity(_verbosity);
120  }
121 
122  unsigned get_verbosity() const
123  {
124  return wrapped.get_verbosity();
125  }
126 
127  std::size_t get_message_count(unsigned level) const
128  {
129  return wrapped.get_message_count(level);
130  }
131 
132  std::string command(unsigned i) const override
133  {
134  return wrapped.command(i);
135  }
136 };
137 
139  const irep_idt &function_name,
140  goto_functionst::goto_functiont &goto_function,
141  const local_may_aliast &local_may_alias,
142  goto_programt::targett loop_head,
143  const loopt &loop,
144  const irep_idt &mode)
145 {
146  PRECONDITION(!loop.empty());
147 
148  // find the last back edge
149  goto_programt::targett loop_end = loop_head;
150  for(const auto &t : loop)
151  if(
152  t->is_goto() && t->get_target() == loop_head &&
153  t->location_number > loop_end->location_number)
154  loop_end = t;
155 
156  // check for assigns, invariant, and decreases clauses
157  auto assigns_clause = static_cast<const exprt &>(
158  loop_end->get_condition().find(ID_C_spec_assigns));
159  auto invariant = static_cast<const exprt &>(
160  loop_end->get_condition().find(ID_C_spec_loop_invariant));
161  auto decreases_clause = static_cast<const exprt &>(
162  loop_end->get_condition().find(ID_C_spec_decreases));
163 
164  if(invariant.is_nil())
165  {
166  if(decreases_clause.is_nil() && assigns_clause.is_nil())
167  return;
168  else
169  {
170  invariant = true_exprt();
171  log.warning()
172  << "The loop at " << loop_head->source_location().as_string()
173  << " does not have an invariant, but has other clauses"
174  << " specified in its contract.\n"
175  << "Hence, a default invariant ('true') is being used to prove those."
176  << messaget::eom;
177  }
178  }
179  else
180  {
181  // form the conjunction
182  invariant = conjunction(invariant.operands());
183  }
184 
185  // Vector representing a (possibly multidimensional) decreases clause
186  const auto &decreases_clause_exprs = decreases_clause.operands();
187 
188  // Temporary variables for storing the multidimensional decreases clause
189  // at the start of and end of a loop body
190  std::vector<symbol_exprt> old_decreases_vars;
191  std::vector<symbol_exprt> new_decreases_vars;
192 
193  // change
194  // H: loop;
195  // E: ...
196  // to
197  // initialize loop_entry variables;
198  // H: assert(invariant);
199  // snapshot(write_set);
200  // havoc;
201  // assume(invariant);
202  // if(guard) goto E:
203  // old_decreases_value = decreases_clause_expr;
204  // loop with optional write_set inclusion checks;
205  // new_decreases_value = decreases_clause_expr;
206  // assert(invariant);
207  // assert(new_decreases_value < old_decreases_value);
208  // assume(false);
209  // E: ...
210 
211  // an intermediate goto_program to store generated instructions
212  goto_programt generated_code;
213 
214  // process quantified variables correctly (introduce a fresh temporary)
215  // and return a copy of the invariant
216  const auto &invariant_expr = [&]() {
217  auto invariant_copy = invariant;
219  code_contractst::add_quantified_variable(invariant_copy, replace, mode);
220  replace(invariant_copy);
221  return invariant_copy;
222  };
223 
224  // Process "loop_entry" history variables
225  // Find and replace "loop_entry" expression in the "invariant" expression.
226  std::map<exprt, exprt> parameter2history;
228  invariant,
229  parameter2history,
230  loop_head->source_location(),
231  mode,
232  generated_code,
233  ID_loop_entry);
234 
235  // Generate: assert(invariant) just before the loop
236  // We use a block scope to create a temporary assertion,
237  // and immediately convert it to goto instructions.
238  {
239  code_assertt assertion{invariant_expr()};
240  assertion.add_source_location() = loop_head->source_location();
241  converter.goto_convert(assertion, generated_code, mode);
242  generated_code.instructions.back().source_location_nonconst().set_comment(
243  "Check loop invariant before entry");
244  }
245 
246  // Add 'loop_entry' history variables and base case assertion.
247  // These variables are local and thus
248  // need not be checked against the enclosing scope's write set.
250  goto_function.body,
251  loop_head,
252  add_pragma_disable_assigns_check(generated_code));
253 
254  instrument_spec_assignst instrument_spec_assigns(
256 
257  // assigns clause snapshots
258  goto_programt snapshot_instructions;
259 
260  instrument_spec_assigns.track_static_locals(snapshot_instructions);
261 
262  // ^^^ FIXME ^^^ we should only allow assignments to static locals
263  // declared in functions that are called in the loop body, not from the whole
264  // function...
265 
266  // set of targets to havoc
267  assignst to_havoc;
268 
269  if(assigns_clause.is_nil())
270  {
271  // No assigns clause was specified for this loop.
272  // Infer memory locations assigned by the loop from the loop instructions
273  // and the inferred aliasing relation.
274  try
275  {
276  get_assigns(local_may_alias, loop, to_havoc);
277  // TODO: if the set contains pairs (i, a[i]),
278  // we must at least widen them to (i, pointer_object(a))
279  log.debug() << "No loop assigns clause provided. Inferred targets {";
280  // Add inferred targets to the loop assigns clause.
281  bool ran_once = false;
282  for(const auto &target : to_havoc)
283  {
284  if(ran_once)
285  log.debug() << ", ";
286  ran_once = true;
287  log.debug() << format(target);
288  instrument_spec_assigns.track_spec_target(
289  target, snapshot_instructions);
290  }
291  log.debug()
292  << "}. Please specify an assigns clause if verification fails."
293  << messaget::eom;
294  }
295  catch(const analysis_exceptiont &exc)
296  {
297  log.error() << "Failed to infer variables being modified by the loop at "
298  << loop_head->source_location()
299  << ".\nPlease specify an assigns clause.\nReason:"
300  << messaget::eom;
301  throw exc;
302  }
303  }
304  else
305  {
306  // An assigns clause was specified for this loop.
307  // Add the targets to the set of expressions to havoc.
308  for(const auto &target : assigns_clause.operands())
309  {
310  to_havoc.insert(target);
311  instrument_spec_assigns.track_spec_target(target, snapshot_instructions);
312  }
313  }
314 
315  // Insert instrumentation
316  // This must be done before havocing the write set.
317  // ^^^ FIXME this is not true ^^^
319  goto_function.body, loop_head, snapshot_instructions);
320 
321  optionalt<cfg_infot> cfg_empty_info;
322 
323  // Perform write set instrumentation on the entire loop.
325  function_name,
326  goto_function.body,
327  loop_head,
328  loop_end,
329  instrument_spec_assigns,
330  // do not skip checks on function parameter assignments
332  // do not use CFG info for now
333  cfg_empty_info);
334 
335  // insert havocing code
336  havoc_assigns_targetst havoc_gen(to_havoc, ns);
337  havoc_gen.append_full_havoc_code(
338  loop_head->source_location(), generated_code);
339 
340  // Add the havocing code, but only check against the enclosing scope's
341  // write set if it was manually specified.
342  if(assigns_clause.is_nil())
344  goto_function.body,
345  loop_head,
346  add_pragma_disable_assigns_check(generated_code));
347  else
349  goto_function.body, loop_head, generated_code);
350 
351  // ^^^ FIXME ^^^
352  // comment by delmasrd: I did not reactivate this behaviour
353  // because I think we always want to check the loop assignments against
354  // the surrounding clause
355 
356  insert_before_swap_and_advance(goto_function.body, loop_head, generated_code);
357 
358  // Generate: assume(invariant) just after havocing
359  // We use a block scope to create a temporary assumption,
360  // and immediately convert it to goto instructions.
361  {
362  code_assumet assumption{invariant_expr()};
363  assumption.add_source_location() = loop_head->source_location();
364  converter.goto_convert(assumption, generated_code, mode);
365  }
366 
367  // Create fresh temporary variables that store the multidimensional
368  // decreases clause's value before and after the loop
369  for(const auto &clause : decreases_clause.operands())
370  {
371  const auto old_decreases_var =
373  clause.type(), loop_head->source_location(), mode, symbol_table)
374  .symbol_expr();
375  generated_code.add(goto_programt::make_decl(
376  old_decreases_var, loop_head->source_location()));
377  old_decreases_vars.push_back(old_decreases_var);
378 
379  const auto new_decreases_var =
381  clause.type(), loop_head->source_location(), mode, symbol_table)
382  .symbol_expr();
383  generated_code.add(goto_programt::make_decl(
384  new_decreases_var, loop_head->source_location()));
385  new_decreases_vars.push_back(new_decreases_var);
386  }
387 
388  // TODO: Fix loop contract handling for do/while loops.
389  if(loop_end->is_goto() && !loop_end->get_condition().is_true())
390  {
391  log.error() << "Loop contracts are unsupported on do/while loops: "
392  << loop_head->source_location() << messaget::eom;
393  throw 0;
394 
395  // non-deterministically skip the loop if it is a do-while loop.
396  generated_code.add(goto_programt::make_goto(
397  loop_end,
399  }
400 
401  // Assume invariant & decl the variant temporaries (just before loop guard).
402  // Use insert_before_swap to preserve jumps to loop head.
404  goto_function.body,
405  loop_head,
406  add_pragma_disable_assigns_check(generated_code));
407 
408  // Forward the loop_head iterator until the start of the body.
409  // This is necessary because complex C loop_head conditions could be
410  // converted to multiple GOTO instructions (e.g. temporaries are introduced).
411  // If the loop_head location shifts to a different function,
412  // assume that it's an inlined function and keep skipping.
413  // FIXME: This simple approach wouldn't work when
414  // the loop guard in the source file is split across multiple lines.
415  const auto head_loc = loop_head->source_location();
416  while(loop_head->source_location() == head_loc ||
417  loop_head->source_location().get_function() != head_loc.get_function())
418  loop_head++;
419 
420  // At this point, we are just past the loop head,
421  // so at the beginning of the loop body.
422  auto loop_body = loop_head;
423  loop_head--;
424 
425  // Generate: assignments to store the multidimensional decreases clause's
426  // value just before the loop body (but just after the loop guard)
427  if(!decreases_clause.is_nil())
428  {
429  for(size_t i = 0; i < old_decreases_vars.size(); i++)
430  {
431  code_assignt old_decreases_assignment{old_decreases_vars[i],
432  decreases_clause_exprs[i]};
433  old_decreases_assignment.add_source_location() =
434  loop_head->source_location();
435  converter.goto_convert(old_decreases_assignment, generated_code, mode);
436  }
437 
438  goto_function.body.destructive_insert(
439  loop_body, add_pragma_disable_assigns_check(generated_code));
440  }
441 
442  // Generate: assert(invariant) just after the loop exits
443  // We use a block scope to create a temporary assertion,
444  // and immediately convert it to goto instructions.
445  {
446  code_assertt assertion{invariant_expr()};
447  assertion.add_source_location() = loop_end->source_location();
448  converter.goto_convert(assertion, generated_code, mode);
449  generated_code.instructions.back().source_location_nonconst().set_comment(
450  "Check that loop invariant is preserved");
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{new_decreases_vars[i],
460  decreases_clause_exprs[i]};
461  new_decreases_assignment.add_source_location() =
462  loop_head->source_location();
463  converter.goto_convert(new_decreases_assignment, generated_code, mode);
464  }
465 
466  // Generate: assertion that the multidimensional decreases clause's value
467  // after the loop is smaller than the value before the loop.
468  // Here, we use the lexicographic order.
469  code_assertt monotonic_decreasing_assertion{
471  new_decreases_vars, old_decreases_vars)};
472  monotonic_decreasing_assertion.add_source_location() =
473  loop_head->source_location();
475  monotonic_decreasing_assertion, generated_code, mode);
476  generated_code.instructions.back().source_location_nonconst().set_comment(
477  "Check decreases clause on loop iteration");
478 
479  // Discard the temporary variables that store decreases clause's value
480  for(size_t i = 0; i < old_decreases_vars.size(); i++)
481  {
482  generated_code.add(goto_programt::make_dead(
483  old_decreases_vars[i], loop_head->source_location()));
484  generated_code.add(goto_programt::make_dead(
485  new_decreases_vars[i], loop_head->source_location()));
486  }
487  }
488 
490  goto_function.body,
491  loop_end,
492  add_pragma_disable_assigns_check(generated_code));
493 
494  // change the back edge into assume(false) or assume(guard)
495  loop_end->turn_into_assume();
496  loop_end->set_condition(boolean_negate(loop_end->get_condition()));
497 }
498 
500  const exprt &expression,
502  const irep_idt &mode)
503 {
504  if(expression.id() == ID_not || expression.id() == ID_typecast)
505  {
506  // For unary connectives, recursively check for
507  // nested quantified formulae in the term
508  const auto &unary_expression = to_unary_expr(expression);
509  add_quantified_variable(unary_expression.op(), replace, mode);
510  }
511  if(expression.id() == ID_notequal || expression.id() == ID_implies)
512  {
513  // For binary connectives, recursively check for
514  // nested quantified formulae in the left and right terms
515  const auto &binary_expression = to_binary_expr(expression);
516  add_quantified_variable(binary_expression.lhs(), replace, mode);
517  add_quantified_variable(binary_expression.rhs(), replace, mode);
518  }
519  if(expression.id() == ID_if)
520  {
521  // For ternary connectives, recursively check for
522  // nested quantified formulae in all three terms
523  const auto &if_expression = to_if_expr(expression);
524  add_quantified_variable(if_expression.cond(), replace, mode);
525  add_quantified_variable(if_expression.true_case(), replace, mode);
526  add_quantified_variable(if_expression.false_case(), replace, mode);
527  }
528  if(expression.id() == ID_and || expression.id() == ID_or)
529  {
530  // For multi-ary connectives, recursively check for
531  // nested quantified formulae in all terms
532  const auto &multi_ary_expression = to_multi_ary_expr(expression);
533  for(const auto &operand : multi_ary_expression.operands())
534  {
535  add_quantified_variable(operand, replace, mode);
536  }
537  }
538  else if(expression.id() == ID_exists || expression.id() == ID_forall)
539  {
540  // When a quantifier expression is found,
541  // for each quantified variable ...
542  const auto &quantifier_expression = to_quantifier_expr(expression);
543  for(const auto &quantified_variable : quantifier_expression.variables())
544  {
545  const auto &quantified_symbol = to_symbol_expr(quantified_variable);
546 
547  // 1. create fresh symbol
548  symbolt new_symbol = new_tmp_symbol(
549  quantified_symbol.type(),
550  quantified_symbol.source_location(),
551  mode,
552  symbol_table);
553 
554  // 2. add created fresh symbol to expression map
555  symbol_exprt q(
556  quantified_symbol.get_identifier(), quantified_symbol.type());
557  replace.insert(q, new_symbol.symbol_expr());
558 
559  // 3. recursively check for nested quantified formulae
560  add_quantified_variable(quantifier_expression.where(), replace, mode);
561  }
562  }
563 }
564 
566  exprt &expr,
567  std::map<exprt, exprt> &parameter2history,
568  source_locationt location,
569  const irep_idt &mode,
570  goto_programt &history,
571  const irep_idt &id)
572 {
573  for(auto &op : expr.operands())
574  {
576  op, parameter2history, location, mode, history, id);
577  }
578 
579  if(expr.id() == ID_old || expr.id() == ID_loop_entry)
580  {
581  const auto &parameter = to_history_expr(expr, id).expression();
582 
583  const auto &id = parameter.id();
584  if(
585  id == ID_dereference || id == ID_member || id == ID_symbol ||
586  id == ID_ptrmember || id == ID_constant || id == ID_typecast)
587  {
588  auto it = parameter2history.find(parameter);
589 
590  if(it == parameter2history.end())
591  {
592  // 0. Create a skip target to jump to, if the parameter is invalid
593  goto_programt skip_program;
594  const auto skip_target =
595  skip_program.add(goto_programt::make_skip(location));
596 
597  // 1. Create a temporary symbol expression that represents the
598  // history variable
599  symbol_exprt tmp_symbol =
600  new_tmp_symbol(parameter.type(), location, mode, symbol_table)
601  .symbol_expr();
602 
603  // 2. Associate the above temporary variable to it's corresponding
604  // expression
605  parameter2history[parameter] = tmp_symbol;
606 
607  // 3. Add the required instructions to the instructions list
608  // 3.1. Declare the newly created temporary variable
609  history.add(goto_programt::make_decl(tmp_symbol, location));
610 
611  // 3.2. Skip storing the history if the expression is invalid
613  skip_target,
615  location));
616 
617  // 3.3. Add an assignment such that the value pointed to by the new
618  // temporary variable is equal to the value of the corresponding
619  // parameter
620  history.add(
621  goto_programt::make_assignment(tmp_symbol, parameter, location));
622 
623  // 3.4. Add a skip target
624  history.destructive_append(skip_program);
625  }
626 
627  expr = parameter2history[parameter];
628  }
629  else
630  {
631  log.error() << "Tracking history of " << parameter.id()
632  << " expressions is not supported yet." << messaget::eom;
633  throw 0;
634  }
635  }
636 }
637 
638 std::pair<goto_programt, goto_programt>
640  codet &expression,
641  source_locationt location,
642  const irep_idt &mode)
643 {
644  std::map<exprt, exprt> parameter2history;
645  goto_programt history;
646 
647  // Find and replace "old" expression in the "expression" variable
649  expression, parameter2history, location, mode, history, ID_old);
650 
651  // Create instructions corresponding to the ensures clause
652  goto_programt ensures_program;
653  converter.goto_convert(expression, ensures_program, mode);
654 
655  // return a pair containing:
656  // 1. instructions corresponding to the ensures clause
657  // 2. instructions related to initializing the history variables
658  return std::make_pair(std::move(ensures_program), std::move(history));
659 }
660 
662  const irep_idt &function,
663  const source_locationt &location,
664  goto_programt &function_body,
665  goto_programt::targett &target)
666 {
667  const auto &const_target =
668  static_cast<const goto_programt::targett &>(target);
669  // Return if the function is not named in the call; currently we don't handle
670  // function pointers.
671  PRECONDITION(const_target->call_function().id() == ID_symbol);
672 
673  // Retrieve the function type, which is needed to extract the contract
674  // components.
675  const irep_idt &target_function =
676  to_symbol_expr(const_target->call_function()).get_identifier();
677  const symbolt &function_symbol = ns.lookup(target_function);
678  const auto &type = to_code_with_contract_type(function_symbol.type);
679 
680  // Isolate each component of the contract.
681  auto assigns_clause = type.assigns();
682  auto requires = conjunction(type.requires());
683  auto ensures = conjunction(type.ensures());
684 
685  // Create a replace_symbolt object, for replacing expressions in the callee
686  // with expressions from the call site (e.g. the return value).
687  // This object tracks replacements that are common to ENSURES and REQUIRES.
688  replace_symbolt common_replace;
689 
690  // keep track of the call's return expression to make it nondet later
691  optionalt<exprt> call_ret_opt = {};
692 
693  // if true, the call return variable variable was created during replacement
694  bool call_ret_is_fresh_var = false;
695 
696  if(type.return_type() != empty_typet())
697  {
698  // Check whether the function's return value is not disregarded.
699  if(target->call_lhs().is_not_nil())
700  {
701  // If so, have it replaced appropriately.
702  // For example, if foo() ensures that its return value is > 5, then
703  // rewrite calls to foo as follows:
704  // x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5)
705  auto &lhs_expr = const_target->call_lhs();
706  call_ret_opt = lhs_expr;
707  symbol_exprt ret_val(CPROVER_PREFIX "return_value", lhs_expr.type());
708  common_replace.insert(ret_val, lhs_expr);
709  }
710  else
711  {
712  // If the function does return a value, but the return value is
713  // disregarded, check if the postcondition includes the return value.
715  ensures.visit(v);
716  if(v.found_return_value())
717  {
718  // The postcondition does mention __CPROVER_return_value, so mint a
719  // fresh variable to replace __CPROVER_return_value with.
720  call_ret_is_fresh_var = true;
721  const symbolt &fresh = get_fresh_aux_symbol(
722  type.return_type(),
723  id2string(target_function),
724  "ignored_return_value",
725  const_target->source_location(),
726  symbol_table.lookup_ref(target_function).mode,
727  ns,
728  symbol_table);
729  symbol_exprt ret_val(CPROVER_PREFIX "return_value", type.return_type());
730  auto fresh_sym_expr = fresh.symbol_expr();
731  common_replace.insert(ret_val, fresh_sym_expr);
732  call_ret_opt = fresh_sym_expr;
733  }
734  }
735  }
736 
737  // Replace formal parameters
738  const auto &arguments = const_target->call_arguments();
739  auto a_it = arguments.begin();
740  for(auto p_it = type.parameters().begin();
741  p_it != type.parameters().end() && a_it != arguments.end();
742  ++p_it, ++a_it)
743  {
744  if(!p_it->get_identifier().empty())
745  {
746  symbol_exprt p(p_it->get_identifier(), p_it->type());
747  common_replace.insert(p, *a_it);
748  }
749  }
750 
751  const auto &mode = symbol_table.lookup_ref(target_function).mode;
752 
753  is_fresh_replacet is_fresh(*this, log, target_function);
754  is_fresh.create_declarations();
755 
756  // Insert assertion of the precondition immediately before the call site.
757  if(!requires.is_true())
758  {
759  replace_symbolt replace(common_replace);
761  replace(requires);
762 
763  goto_programt assertion;
765  code_assertt(requires),
766  assertion,
767  symbol_table.lookup_ref(target_function).mode);
768  assertion.instructions.back().source_location_nonconst() =
769  requires.source_location();
770  assertion.instructions.back().source_location_nonconst().set_comment(
771  "Check requires clause");
772  assertion.instructions.back().source_location_nonconst().set_property_class(
773  ID_precondition);
774  is_fresh.update_requires(assertion);
775  insert_before_swap_and_advance(function_body, target, assertion);
776  }
777 
778  // Gather all the instructions required to handle history variables
779  // as well as the ensures clause
780  std::pair<goto_programt, goto_programt> ensures_pair;
781  if(!ensures.is_false())
782  {
783  replace_symbolt replace(common_replace);
785  replace(ensures);
786 
787  auto assumption = code_assumet(ensures);
788  ensures_pair = create_ensures_instruction(
789  assumption,
790  ensures.source_location(),
791  symbol_table.lookup_ref(target_function).mode);
792 
793  // add all the history variable initialization instructions
794  // to the goto program
795  insert_before_swap_and_advance(function_body, target, ensures_pair.second);
796  }
797 
798  // ASSIGNS clause should not refer to any quantified variables,
799  // and only refer to the common symbols to be replaced.
800  exprt targets;
801  for(auto &target : assigns_clause)
802  targets.add_to_operands(std::move(target));
803  common_replace(targets);
804 
805  // Create a sequence of non-deterministic assignments...
806  goto_programt havoc_instructions;
807 
808  // ...for assigns clause targets
809  if(!assigns_clause.empty())
810  {
811  // Havoc all targets in the assigns clause
812  // TODO: handle local statics possibly touched by this function
814  target_function,
815  targets.operands(),
817  location,
818  symbol_table,
820  havocker.get_instructions(havoc_instructions);
821  }
822 
823  // ...for the return value
824  if(call_ret_opt.has_value())
825  {
826  auto &call_ret = call_ret_opt.value();
827  auto &loc = call_ret.source_location();
828  auto &type = call_ret.type();
829 
830  // Declare if fresh
831  if(call_ret_is_fresh_var)
832  havoc_instructions.add(
833  goto_programt::make_decl(to_symbol_expr(call_ret), loc));
834 
835  side_effect_expr_nondett expr(type, location);
836  auto target = havoc_instructions.add(
837  goto_programt::make_assignment(call_ret, expr, loc));
838  target->code_nonconst().add_source_location() = loc;
839  }
840 
841  // Insert havoc instructions immediately before the call site.
842  insert_before_swap_and_advance(function_body, target, havoc_instructions);
843 
844  // To remove the function call, insert statements related to the assumption.
845  // Then, replace the function call with a SKIP statement.
846  if(!ensures.is_false())
847  {
848  is_fresh.update_ensures(ensures_pair.first);
849  insert_before_swap_and_advance(function_body, target, ensures_pair.first);
850  }
851 
852  // Kill return value variable if fresh
853  if(call_ret_is_fresh_var)
854  {
855  function_body.output_instruction(ns, "", log.warning(), *target);
856  auto dead_inst =
857  goto_programt::make_dead(to_symbol_expr(call_ret_opt.value()), location);
858  function_body.insert_before_swap(target, dead_inst);
859  ++target;
860  }
861 
862  // Erase original function call
863  *target = goto_programt::make_skip();
864 
865  // Add this function to the set of replaced functions.
866  summarized.insert(target_function);
867  return false;
868 }
869 
871  const irep_idt &function_name,
872  goto_functionst::goto_functiont &goto_function)
873 {
874  const bool may_have_loops = std::any_of(
875  goto_function.body.instructions.begin(),
876  goto_function.body.instructions.end(),
877  [](const goto_programt::instructiont &instruction) {
878  return instruction.is_backwards_goto();
879  });
880 
881  if(!may_have_loops)
882  return;
883 
886  goto_functions, function_name, ns, log.get_message_handler());
887 
888  INVARIANT(
889  decorated.get_recursive_function_warnings_count() == 0,
890  "Recursive functions found during inlining");
891 
892  // restore internal invariants
894 
895  local_may_aliast local_may_alias(goto_function);
896  natural_loops_mutablet natural_loops(goto_function.body);
897 
898  // A graph node type that stores information about a loop.
899  // We create a DAG representing nesting of various loops in goto_function,
900  // sort them topologically, and instrument them in the top-sorted order.
901  //
902  // The goal here is not avoid explicit "subset checks" on nested write sets.
903  // When instrumenting in a top-sorted order,
904  // the outer loop would no longer observe the inner loop's write set,
905  // but only corresponding `havoc` statements,
906  // which can be instrumented in the usual way to achieve a "subset check".
907 
908  struct loop_graph_nodet : public graph_nodet<empty_edget>
909  {
910  typedef const goto_programt::targett &targett;
911  typedef const typename natural_loops_mutablet::loopt &loopt;
912 
913  targett target;
914  loopt loop;
915 
916  loop_graph_nodet(targett t, loopt l) : target(t), loop(l)
917  {
918  }
919  };
920  grapht<loop_graph_nodet> loop_nesting_graph;
921 
922  for(const auto &loop : natural_loops.loop_map)
923  loop_nesting_graph.add_node(loop.first, loop.second);
924 
925  for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer)
926  {
927  for(size_t inner = 0; inner < loop_nesting_graph.size(); ++inner)
928  {
929  if(inner == outer)
930  continue;
931 
932  if(loop_nesting_graph[outer].loop.contains(
933  loop_nesting_graph[inner].target))
934  loop_nesting_graph.add_edge(outer, inner);
935  }
936  }
937 
938  // Iterate over the (natural) loops in the function, in topo-sorted order,
939  // and apply any loop contracts that we find.
940  for(const auto &idx : loop_nesting_graph.topsort())
941  {
942  const auto &loop_node = loop_nesting_graph[idx];
944  function_name,
945  goto_function,
946  local_may_alias,
947  loop_node.target,
948  loop_node.loop,
949  symbol_table.lookup_ref(function_name).mode);
950  }
951 }
952 
954 {
955  return symbol_table;
956 }
957 
959 {
960  return goto_functions;
961 }
962 
964  goto_programt::targett &instruction_it,
965  goto_programt &program,
966  instrument_spec_assignst &instrument_spec_assigns,
967  optionalt<cfg_infot> &cfg_info_opt)
968 {
969  auto lhs = instruction_it->assign_lhs();
970  lhs.add_source_location() = instruction_it->source_location();
971  goto_programt payload;
972  instrument_spec_assigns.check_inclusion_assignment(
973  lhs, cfg_info_opt, payload);
974  insert_before_swap_and_advance(program, instruction_it, payload);
975 }
976 
978  goto_programt::targett &instruction_it,
979  const irep_idt &function,
980  goto_programt &body,
981  instrument_spec_assignst &instrument_spec_assigns,
982  optionalt<cfg_infot> &cfg_info_opt)
983 {
984  INVARIANT(
985  instruction_it->is_function_call(),
986  "The first argument of instrument_call_statement should always be "
987  "a function call");
988 
989  const auto &callee_name =
990  to_symbol_expr(instruction_it->call_function()).get_identifier();
991 
992  if(callee_name == "malloc")
993  {
994  const auto &function_call =
995  to_code_function_call(instruction_it->get_code());
996  if(function_call.lhs().is_not_nil())
997  {
998  // grab the returned pointer from malloc
999  auto object = pointer_object(function_call.lhs());
1000  object.add_source_location() = function_call.source_location();
1001  // move past the call and then insert the CAR
1002  instruction_it++;
1003  goto_programt payload;
1004  instrument_spec_assigns.track_heap_allocated(object, payload);
1005  insert_before_swap_and_advance(body, instruction_it, payload);
1006  // since CAR was inserted *after* the malloc call,
1007  // move the instruction pointer backward,
1008  // because the caller increments it in a `for` loop
1009  instruction_it--;
1010  }
1011  }
1012  else if(callee_name == "free")
1013  {
1014  const auto &ptr = instruction_it->call_arguments().front();
1015  auto object = pointer_object(ptr);
1016  object.add_source_location() = instruction_it->source_location();
1017  goto_programt payload;
1018  instrument_spec_assigns
1020  object, cfg_info_opt, payload);
1021  insert_before_swap_and_advance(body, instruction_it, payload);
1022  }
1023 }
1024 
1026 {
1027  // Collect all GOTOs and mallocs
1028  std::vector<goto_programt::instructiont> back_gotos;
1029  std::vector<goto_programt::instructiont> malloc_calls;
1030 
1031  int index = 0;
1032  for(goto_programt::instructiont instruction : program.instructions)
1033  {
1034  if(instruction.is_backwards_goto())
1035  {
1036  back_gotos.push_back(instruction);
1037  }
1038  if(instruction.is_function_call())
1039  {
1040  irep_idt called_name;
1041  if(instruction.call_function().id() == ID_dereference)
1042  {
1043  called_name =
1045  to_dereference_expr(instruction.call_function()).pointer())
1046  .get_identifier();
1047  }
1048  else
1049  {
1050  called_name =
1051  to_symbol_expr(instruction.call_function()).get_identifier();
1052  }
1053 
1054  if(called_name == "malloc")
1055  {
1056  malloc_calls.push_back(instruction);
1057  }
1058  }
1059  index++;
1060  }
1061  // Make sure there are no gotos that go back such that a malloc
1062  // is between the goto and its destination (possible loop).
1063  for(auto goto_entry : back_gotos)
1064  {
1065  for(const auto &target : goto_entry.targets)
1066  {
1067  for(auto malloc_entry : malloc_calls)
1068  {
1069  if(
1070  malloc_entry.location_number >= target->location_number &&
1071  malloc_entry.location_number < goto_entry.location_number)
1072  {
1073  log.error() << "Call to malloc at location "
1074  << malloc_entry.location_number << " falls between goto "
1075  << "source location " << goto_entry.location_number
1076  << " and it's destination at location "
1077  << target->location_number << ". "
1078  << "Unable to complete instrumentation, as this malloc "
1079  << "may be in a loop." << messaget::eom;
1080  throw 0;
1081  }
1082  }
1083  }
1084  }
1085  return false;
1086 }
1087 
1089 {
1090  // Get the function object before instrumentation.
1091  auto function_obj = goto_functions.function_map.find(function);
1092  if(function_obj == goto_functions.function_map.end())
1093  {
1094  log.error() << "Could not find function '" << function
1095  << "' in goto-program; not enforcing contracts."
1096  << messaget::eom;
1097  return true;
1098  }
1099 
1100  const auto &goto_function = function_obj->second;
1101  auto &function_body = function_obj->second.body;
1102 
1103  // Get assigns clause for function
1104  const symbolt &function_sybmol = ns.lookup(function);
1105  const auto &function_with_contract =
1106  to_code_with_contract_type(function_sybmol.type);
1107 
1108  instrument_spec_assignst instrument_spec_assigns(
1110 
1111  // Detect and track static local variables before inlining
1112  goto_programt snapshot_static_locals;
1113  instrument_spec_assigns.track_static_locals(snapshot_static_locals);
1114 
1115  // Full inlining of the function body
1116  // Inlining is performed so that function calls to a same function
1117  // occurring under different write sets get instrumented specifically
1118  // for each write set
1120  goto_function_inline(goto_functions, function, ns, decorated);
1121 
1122  INVARIANT(
1123  decorated.get_recursive_function_warnings_count() == 0,
1124  "Recursive functions found during inlining");
1125 
1126  // Clean up possible fake loops that are due to `IF 0!=0 GOTO i` instructions
1127  simplify_gotos(function_body, ns);
1128 
1129  // Restore internal coherence in the programs
1131 
1132  INVARIANT(
1133  is_loop_free(function_body, ns, log),
1134  "Loops remain in function '" + id2string(function) +
1135  "', assigns clause checking instrumentation cannot be applied.");
1136 
1137  // Create a deep copy of the inlined body before any instrumentation is added
1138  // and compute static control flow graph information
1139  goto_functiont goto_function_orig;
1140  goto_function_orig.copy_from(goto_function);
1141  cfg_infot cfg_info(ns, goto_function_orig);
1142  optionalt<cfg_infot> cfg_info_opt{cfg_info};
1143 
1144  // Start instrumentation
1145  auto instruction_it = function_body.instructions.begin();
1146 
1147  // Inject local static snapshots
1149  function_body, instruction_it, snapshot_static_locals);
1150 
1151  // Track targets mentionned in the specification
1152  for(auto &target : function_with_contract.assigns())
1153  {
1154  goto_programt payload;
1155  instrument_spec_assigns.track_spec_target(target, payload);
1156  insert_before_swap_and_advance(function_body, instruction_it, payload);
1157  }
1158 
1159  // Track formal parameters
1160  goto_programt snapshot_function_parameters;
1161  for(const auto &param : to_code_type(function_sybmol.type).parameters())
1162  {
1163  goto_programt payload;
1164  instrument_spec_assigns.track_stack_allocated(
1165  ns.lookup(param.get_identifier()).symbol_expr(), payload);
1166  insert_before_swap_and_advance(function_body, instruction_it, payload);
1167  }
1168 
1169  // Restore internal coherence in the programs
1171 
1172  // Insert write set inclusion checks.
1174  function,
1175  function_body,
1176  instruction_it,
1177  function_body.instructions.end(),
1178  instrument_spec_assigns,
1179  // skip checks on function parameter assignments
1180  skipt::Skip,
1181  cfg_info_opt);
1182 
1183  return false;
1184 }
1185 
1189  const goto_programt::const_targett &target)
1190 {
1191  const auto &pragmas = target->source_location().get_pragmas();
1192  return pragmas.find(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK) != pragmas.end();
1193 }
1194 
1197  const goto_programt::const_targett &target,
1198  code_contractst::skipt skip_parameter_assigns,
1199  const namespacet ns,
1200  const optionalt<cfg_infot> cfg_info_opt)
1201 {
1202  if(
1203  const auto &symbol_expr =
1204  expr_try_dynamic_cast<symbol_exprt>(target->assign_lhs()))
1205  {
1206  if(
1207  skip_parameter_assigns == code_contractst::skipt::DontSkip &&
1208  ns.lookup(symbol_expr->get_identifier()).is_parameter)
1209  return true;
1210 
1211  if(cfg_info_opt.has_value())
1212  return !cfg_info_opt.value().is_local(symbol_expr->get_identifier());
1213  }
1214 
1215  return true;
1216 }
1217 
1228  const goto_programt::const_targett &target,
1229  const optionalt<cfg_infot> &cfg_info_opt)
1230 {
1231  if(cfg_info_opt.has_value())
1232  return cfg_info_opt.value().is_not_local_or_dirty_local(
1233  target->decl_symbol().get_identifier());
1234 
1235  // Unless proved non-dirty by the CFG analysis we assume it is dirty.
1236  return true;
1237 }
1238 
1242  const goto_programt::const_targett &target,
1243  const optionalt<cfg_infot> &cfg_info_opt)
1244 {
1245  // Unless proved non-dirty by the CFG analysis we assume it is dirty.
1246  if(!cfg_info_opt.has_value())
1247  return true;
1248 
1249  return cfg_info_opt.value().is_not_local_or_dirty_local(
1250  target->dead_symbol().get_identifier());
1251 }
1252 
1254  const irep_idt &function,
1255  goto_programt &body,
1256  goto_programt::targett instruction_it,
1257  const goto_programt::targett &instruction_end,
1258  instrument_spec_assignst &instrument_spec_assigns,
1259  skipt skip_parameter_assigns,
1260  optionalt<cfg_infot> &cfg_info_opt)
1261 {
1262  while(instruction_it != instruction_end)
1263  {
1264  // Skip instructions marked as disabled for assigns clause checking
1265  if(has_disable_assigns_check_pragma(instruction_it))
1266  {
1267  instruction_it++;
1268  if(cfg_info_opt.has_value())
1269  cfg_info_opt.value().step();
1270  continue;
1271  }
1272 
1273  // Do not instrument this instruction again in the future,
1274  // since we are going to instrument it now below.
1275  add_pragma_disable_assigns_check(*instruction_it);
1276 
1277  if(
1278  instruction_it->is_decl() &&
1279  must_track_decl(instruction_it, cfg_info_opt))
1280  {
1281  // grab the declared symbol
1282  const auto &decl_symbol = instruction_it->decl_symbol();
1283  // move past the call and then insert the CAR
1284  instruction_it++;
1285  goto_programt payload;
1286  instrument_spec_assigns.track_stack_allocated(decl_symbol, payload);
1287  insert_before_swap_and_advance(body, instruction_it, payload);
1288  // since CAR was inserted *after* the DECL instruction,
1289  // move the instruction pointer backward,
1290  // because the loop step takes care of the increment
1291  instruction_it--;
1292  }
1293  else if(
1294  instruction_it->is_assign() &&
1296  instruction_it, skip_parameter_assigns, ns, cfg_info_opt))
1297  {
1299  instruction_it, body, instrument_spec_assigns, cfg_info_opt);
1300  }
1301  else if(instruction_it->is_function_call())
1302  {
1304  instruction_it, function, body, instrument_spec_assigns, cfg_info_opt);
1305  }
1306  else if(
1307  instruction_it->is_dead() &&
1308  must_track_dead(instruction_it, cfg_info_opt))
1309  {
1310  const auto &symbol = instruction_it->dead_symbol();
1311  if(instrument_spec_assigns.stack_allocated_is_tracked(symbol))
1312  {
1313  goto_programt payload;
1314  instrument_spec_assigns.invalidate_stack_allocated(symbol, payload);
1315  insert_before_swap_and_advance(body, instruction_it, payload);
1316  }
1317  else
1318  {
1319  // For loops, the loop_head appears after the DECL of counters,
1320  // and any other temporaries introduced during "initialization".
1321  // However, they go `DEAD` (possible conditionally) inside the loop,
1322  // in presence of return statements.
1323  // Notice that for them those variables be writable,
1324  // they must appear as assigns targets anyway,
1325  // but their DECL statements are outside of the loop.
1326  log.warning() << "Found a `DEAD` variable " << symbol.get_identifier()
1327  << " without corresponding `DECL`, at: "
1328  << instruction_it->source_location() << messaget::eom;
1329  }
1330  }
1331  else if(
1332  instruction_it->is_other() &&
1333  instruction_it->get_other().get_statement() == ID_havoc_object)
1334  {
1335  auto havoc_argument = instruction_it->get_other().operands().front();
1336  auto havoc_object = pointer_object(havoc_argument);
1337  havoc_object.add_source_location() = instruction_it->source_location();
1338  goto_programt payload;
1339  instrument_spec_assigns.check_inclusion_assignment(
1340  havoc_object, cfg_info_opt, payload);
1341  insert_before_swap_and_advance(body, instruction_it, payload);
1342  }
1343 
1344  // Move to the next instruction
1345  instruction_it++;
1346  if(cfg_info_opt.has_value())
1347  cfg_info_opt.value().step();
1348  }
1349 }
1350 
1352 {
1353  // Add statements to the source function
1354  // to ensure assigns clause is respected.
1356 
1357  // Rename source function
1358  std::stringstream ss;
1359  ss << CPROVER_PREFIX << "contracts_original_" << function;
1360  const irep_idt mangled(ss.str());
1361  const irep_idt original(function);
1362 
1363  auto old_function = goto_functions.function_map.find(original);
1364  if(old_function == goto_functions.function_map.end())
1365  {
1366  log.error() << "Could not find function '" << function
1367  << "' in goto-program; not enforcing contracts."
1368  << messaget::eom;
1369  return true;
1370  }
1371 
1372  std::swap(goto_functions.function_map[mangled], old_function->second);
1373  goto_functions.function_map.erase(old_function);
1374 
1375  // Place a new symbol with the mangled name into the symbol table
1376  source_locationt sl;
1377  sl.set_file("instrumented for code contracts");
1378  sl.set_line("0");
1379  symbolt mangled_sym;
1380  const symbolt *original_sym = symbol_table.lookup(original);
1381  mangled_sym = *original_sym;
1382  mangled_sym.name = mangled;
1383  mangled_sym.base_name = mangled;
1384  mangled_sym.location = sl;
1385  const auto mangled_found = symbol_table.insert(std::move(mangled_sym));
1386  INVARIANT(
1387  mangled_found.second,
1388  "There should be no existing function called " + ss.str() +
1389  " in the symbol table because that name is a mangled name");
1390 
1391  // Insert wrapper function into goto_functions
1392  auto nexist_old_function = goto_functions.function_map.find(original);
1393  INVARIANT(
1394  nexist_old_function == goto_functions.function_map.end(),
1395  "There should be no function called " + id2string(function) +
1396  " in the function map because that function should have had its"
1397  " name mangled");
1398 
1399  auto mangled_fun = goto_functions.function_map.find(mangled);
1400  INVARIANT(
1401  mangled_fun != goto_functions.function_map.end(),
1402  "There should be a function called " + ss.str() +
1403  " in the function map because we inserted a fresh goto-program"
1404  " with that mangled name");
1405 
1406  goto_functiont &wrapper = goto_functions.function_map[original];
1407  wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers;
1409  add_contract_check(original, mangled, wrapper.body);
1410 
1411  return false;
1412 }
1413 
1415  const irep_idt &wrapper_function,
1416  const irep_idt &mangled_function,
1417  goto_programt &dest)
1418 {
1419  PRECONDITION(!dest.instructions.empty());
1420 
1421  const symbolt &function_symbol = ns.lookup(mangled_function);
1422  const auto &code_type = to_code_with_contract_type(function_symbol.type);
1423 
1424  auto assigns = code_type.assigns();
1425  auto requires = conjunction(code_type.requires());
1426  auto ensures = conjunction(code_type.ensures());
1427 
1428  // build:
1429  // if(nondet)
1430  // decl ret
1431  // decl parameter1 ...
1432  // decl history_parameter1 ... [optional]
1433  // assume(requires) [optional]
1434  // ret=function(parameter1, ...)
1435  // assert(ensures)
1436  // skip: ...
1437 
1438  // build skip so that if(nondet) can refer to it
1439  goto_programt tmp_skip;
1440  goto_programt::targett skip =
1441  tmp_skip.add(goto_programt::make_skip(ensures.source_location()));
1442 
1443  goto_programt check;
1444 
1445  // prepare function call including all declarations
1446  code_function_callt call(function_symbol.symbol_expr());
1447 
1448  // Create a replace_symbolt object, for replacing expressions in the callee
1449  // with expressions from the call site (e.g. the return value).
1450  // This object tracks replacements that are common to ENSURES and REQUIRES.
1451  replace_symbolt common_replace;
1452 
1453  // decl ret
1454  optionalt<code_returnt> return_stmt;
1455  if(code_type.return_type() != empty_typet())
1456  {
1458  code_type.return_type(),
1459  skip->source_location(),
1460  function_symbol.mode,
1461  symbol_table)
1462  .symbol_expr();
1463  check.add(goto_programt::make_decl(r, skip->source_location()));
1464 
1465  call.lhs() = r;
1466  return_stmt = code_returnt(r);
1467 
1468  symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
1469  common_replace.insert(ret_val, r);
1470  }
1471 
1472  // decl parameter1 ...
1473  goto_functionst::function_mapt::iterator f_it =
1474  goto_functions.function_map.find(mangled_function);
1475  PRECONDITION(f_it != goto_functions.function_map.end());
1476 
1477  const goto_functionst::goto_functiont &gf = f_it->second;
1478  for(const auto &parameter : gf.parameter_identifiers)
1479  {
1480  PRECONDITION(!parameter.empty());
1481  const symbolt &parameter_symbol = ns.lookup(parameter);
1483  parameter_symbol.type,
1484  skip->source_location(),
1485  parameter_symbol.mode,
1486  symbol_table)
1487  .symbol_expr();
1488  check.add(goto_programt::make_decl(p, skip->source_location()));
1490  p, parameter_symbol.symbol_expr(), skip->source_location()));
1491 
1492  call.arguments().push_back(p);
1493 
1494  common_replace.insert(parameter_symbol.symbol_expr(), p);
1495  }
1496 
1497  is_fresh_enforcet visitor(*this, log, wrapper_function);
1498  visitor.create_declarations();
1499 
1500  // Generate: assume(requires)
1501  if(!requires.is_false())
1502  {
1503  // extend common_replace with quantified variables in REQUIRES,
1504  // and then do the replacement
1505  replace_symbolt replace(common_replace);
1507  requires, replace, function_symbol.mode);
1508  replace(requires);
1509 
1510  goto_programt assumption;
1512  code_assumet(requires), assumption, function_symbol.mode);
1513  visitor.update_requires(assumption);
1514  check.destructive_append(assumption);
1515  }
1516 
1517  // Prepare the history variables handling
1518  std::pair<goto_programt, goto_programt> ensures_pair;
1519 
1520  // Generate: copies for history variables
1521  if(!ensures.is_true())
1522  {
1523  // extend common_replace with quantified variables in ENSURES,
1524  // and then do the replacement
1525  replace_symbolt replace(common_replace);
1527  ensures, replace, function_symbol.mode);
1528  replace(ensures);
1529 
1530  // get all the relevant instructions related to history variables
1531  auto assertion = code_assertt(ensures);
1532  assertion.add_source_location() = ensures.source_location();
1533  ensures_pair = create_ensures_instruction(
1534  assertion, ensures.source_location(), function_symbol.mode);
1535  ensures_pair.first.instructions.back()
1536  .source_location_nonconst()
1537  .set_comment("Check ensures clause");
1538  ensures_pair.first.instructions.back()
1539  .source_location_nonconst()
1540  .set_property_class(ID_postcondition);
1541 
1542  // add all the history variable initializations
1543  visitor.update_ensures(ensures_pair.first);
1544  check.destructive_append(ensures_pair.second);
1545  }
1546 
1547  // ret=mangled_function(parameter1, ...)
1549 
1550  // Generate: assert(ensures)
1551  if(ensures.is_not_nil())
1552  {
1553  check.destructive_append(ensures_pair.first);
1554  }
1555 
1556  if(code_type.return_type() != empty_typet())
1557  {
1559  return_stmt.value().return_value(), skip->source_location()));
1560  }
1561 
1562  // prepend the new code to dest
1563  check.destructive_append(tmp_skip);
1564  dest.destructive_insert(dest.instructions.begin(), check);
1565 }
1566 
1567 bool code_contractst::replace_calls(const std::set<std::string> &to_replace)
1568 {
1569  if(to_replace.empty())
1570  return false;
1571 
1572  bool fail = false;
1573 
1574  for(auto &goto_function : goto_functions.function_map)
1575  {
1576  Forall_goto_program_instructions(ins, goto_function.second.body)
1577  {
1578  if(ins->is_function_call())
1579  {
1580  if(ins->call_function().id() != ID_symbol)
1581  continue;
1582 
1583  const irep_idt &called_function =
1584  to_symbol_expr(ins->call_function()).get_identifier();
1585  auto found = std::find(
1586  to_replace.begin(), to_replace.end(), id2string(called_function));
1587  if(found == to_replace.end())
1588  continue;
1589 
1590  fail |= apply_function_contract(
1591  goto_function.first,
1592  ins->source_location(),
1593  goto_function.second.body,
1594  ins);
1595  }
1596  }
1597  }
1598 
1599  if(fail)
1600  return true;
1601 
1602  for(auto &goto_function : goto_functions.function_map)
1603  remove_skip(goto_function.second.body);
1604 
1606 
1607  return false;
1608 }
1609 
1611 {
1612  for(auto &goto_function : goto_functions.function_map)
1613  apply_loop_contract(goto_function.first, goto_function.second);
1614 }
1615 
1616 bool code_contractst::enforce_contracts(const std::set<std::string> &to_enforce)
1617 {
1618  if(to_enforce.empty())
1619  return false;
1620 
1621  bool fail = false;
1622 
1623  for(const auto &function : to_enforce)
1624  {
1625  auto goto_function = goto_functions.function_map.find(function);
1626  if(goto_function == goto_functions.function_map.end())
1627  {
1628  fail = true;
1629  log.error() << "Could not find function '" << function
1630  << "' in goto-program; not enforcing contracts."
1631  << messaget::eom;
1632  continue;
1633  }
1634 
1635  if(!fail)
1636  fail = enforce_contract(function);
1637  }
1638  return fail;
1639 }
API to expression classes that are internal to the C frontend.
const history_exprt & to_history_expr(const exprt &expr, const irep_idt &id)
Definition: c_expr.h:219
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:418
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
Stores information about a goto function computed from its CFG, together with a target iterator into ...
Definition: utils.h:190
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:270
A 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:112
std::pair< goto_programt, goto_programt > create_ensures_instruction(codet &expression, source_locationt location, const irep_idt &mode)
This function creates and returns an instruction that corresponds to the ensures clause.
Definition: contracts.cpp:639
void replace_history_parameter(exprt &expr, std::map< exprt, exprt > &parameter2history, source_locationt location, const irep_idt &mode, goto_programt &history, const irep_idt &id)
This function recursively identifies the "old" expressions within expr and replaces them with corresp...
Definition: contracts.cpp:565
bool replace_calls(const std::set< std::string > &)
Replace all calls to each function in the list with that function's contract.
Definition: contracts.cpp:1567
bool 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:661
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:870
messaget & log
Definition: contracts.h:125
goto_functionst & get_goto_functions()
Definition: contracts.cpp:958
void apply_loop_contracts()
Definition: contracts.cpp:1610
symbol_tablet & symbol_table
Definition: contracts.h:122
void instrument_call_statement(goto_programt::targett &instruction_it, const irep_idt &function, goto_programt &body, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt)
Inserts an assertion into program immediately before the function call at instruction_it,...
Definition: contracts.cpp:977
void add_quantified_variable(const exprt &expression, replace_symbolt &replace, const irep_idt &mode)
This function recursively searches the expression to find nested or non-nested quantified expressions...
Definition: contracts.cpp:499
bool check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
Definition: contracts.cpp:1088
bool enforce_contract(const irep_idt &function)
Enforce contract of a single function.
Definition: contracts.cpp:1351
std::unordered_set< irep_idt > summarized
Definition: contracts.h:128
void check_frame_conditions(const irep_idt &function, goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, instrument_spec_assignst &instrument_spec_assigns, skipt skip_parameter_assigns, optionalt< cfg_infot > &cfg_info_opt)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
Definition: contracts.cpp:1253
bool check_for_looped_mallocs(const goto_programt &program)
Check if there are any malloc statements which may be repeated because of a goto statement that jumps...
Definition: contracts.cpp:1025
goto_convertt converter
Definition: contracts.h:126
void instrument_assign_statement(goto_programt::targett &instruction_it, goto_programt &program, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt)
Inserts an assertion into program immediately before the assignment instruction_it,...
Definition: contracts.cpp:963
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, const loopt &loop, const irep_idt &mode)
Definition: contracts.cpp:138
goto_functionst & goto_functions
Definition: contracts.h:123
skipt
Tells wether to skip or not skip an action.
Definition: contracts.h:116
bool enforce_contracts(const std::set< std::string > &functions)
Turn requires & ensures into assumptions and assertions for each of the named functions.
Definition: contracts.cpp:1616
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:1414
symbol_tablet & get_symbol_table()
Definition: contracts.cpp:953
codet representation of a function call statement.
codet representation of a "return from a function" statement.
const parameterst & parameters() const
Definition: std_types.h:655
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:54
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
A collection of goto functions.
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
void copy_from(const goto_functiont &other)
Definition: goto_function.h:76
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:271
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:550
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:598
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:863
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:956
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:619
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:706
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:986
instructionst::iterator targett
Definition: goto_program.h:592
instructionst::const_iterator const_targett
Definition: goto_program.h:593
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:698
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:880
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:715
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:949
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
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...
void get_instructions(goto_programt &dest)
Generates the assigns clause replacement instructions in dest.
A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_obje...
Definition: utils.h:57
void append_full_havoc_code(const source_locationt location, goto_programt &dest) const
Append goto instructions to havoc the full assigns set.
Definition: havoc_utils.cpp:21
const exprt & expression() const
Definition: c_expr.h:212
Decorator for message_handlert that keeps track of warnings occuring when inlining a function.
Definition: contracts.cpp:60
void print(unsigned level, const std::string &message) override
Definition: contracts.cpp:81
unsigned get_verbosity() const
Definition: contracts.cpp:122
void print(unsigned level, const jsont &json) override
Definition: contracts.cpp:92
void set_verbosity(unsigned _verbosity)
Definition: contracts.cpp:117
void print(unsigned level, const std::string &message, const source_locationt &location) override
Definition: contracts.cpp:102
void flush(unsigned i) override
Definition: contracts.cpp:112
void print(unsigned level, const xmlt &xml) override
Definition: contracts.cpp:87
inlining_decoratort(message_handlert &_wrapped)
Definition: contracts.cpp:72
unsigned int get_recursive_function_warnings_count()
Definition: contracts.cpp:76
message_handlert & wrapped
Definition: contracts.cpp:62
void print(unsigned level, const structured_datat &data) override
Definition: contracts.cpp:97
std::string command(unsigned i) const override
Create an ECMA-48 SGR (Select Graphic Rendition) command.
Definition: contracts.cpp:132
std::size_t get_message_count(unsigned level) const
Definition: contracts.cpp:127
unsigned int recursive_function_warnings_count
Definition: contracts.cpp:63
void parse_message(const std::string &message)
Definition: contracts.cpp:65
A class that generates instrumentation for assigns clause checking.
void invalidate_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest)
Generate instructions to invalidate a stack-allocated object that goes DEAD in dest.
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_heap_allocated(const exprt &expr, goto_programt &dest)
Track a whole heap-alloc object and generate snaphsot instructions in dest.
void track_static_locals(goto_programt &dest)
Search the call graph reachable from the instrumented function to identify local static variables use...
void check_inclusion_assignment(const exprt &lhs, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest)
Generates inclusion check instructions for an assignment, havoc or havoc_object instruction.
bool stack_allocated_is_tracked(const symbol_exprt &symbol_expr) const
Returns true if the expression is tracked.
void check_inclusion_heap_allocated_and_invalidate_aliases(const exprt &expr, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest)
Generates inclusion check instructions for an argument passed to free.
const irep_idt & id() const
Definition: irep.h:396
void update_requires(goto_programt &requires)
void update_ensures(goto_programt &ensures)
virtual void create_declarations()
virtual void create_declarations()
Definition: json.h:27
loop_mapt loop_map
Definition: loop_analysis.h:88
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
void set_verbosity(unsigned _verbosity)
Definition: message.h:53
virtual void print(unsigned level, const std::string &message)=0
Definition: message.cpp:60
std::size_t get_message_count(unsigned level) const
Definition: message.h:56
unsigned get_verbosity() const
Definition: message.h:54
virtual std::string command(unsigned) const
Create an ECMA-48 SGR (Select Graphic Rendition) command.
Definition: message.h:66
virtual void flush(unsigned)=0
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
mstreamt & warning() const
Definition: message.h:404
mstreamt & debug() const
Definition: message.h:429
message_handlert & get_message_handler()
Definition: message.h:184
static eomt eom
Definition: message.h:297
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().
Definition: namespace.cpp:138
Boolean negation.
Definition: std_expr.h:2181
Replace expression or type symbols by an expression or type, respectively.
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
Predicate to be used with the exprt::visit() function.
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
std::string as_string() const
void set_file(const irep_idt &file)
void set_line(const irep_idt &line)
A way of representing nested key/value data.
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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:2856
const source_locationt & source_location() const
Definition: type.h:74
Definition: xml.h:21
bool has_disable_assigns_check_pragma(const goto_programt::const_targett &target)
Returns true iff the target instruction is tagged with a 'CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK' prag...
Definition: contracts.cpp:1188
bool must_track_dead(const goto_programt::const_targett &target, const optionalt< cfg_infot > &cfg_info_opt)
Returns true iff a DEAD x must be processed to upate the local write set.
Definition: contracts.cpp:1241
bool must_check_assign(const goto_programt::const_targett &target, code_contractst::skipt skip_parameter_assigns, const namespacet ns, const optionalt< cfg_infot > cfg_info_opt)
Returns true iff an ASSIGN lhs := rhs instruction must be instrumented.
Definition: contracts.cpp:1196
bool must_track_decl(const goto_programt::const_targett &target, const optionalt< cfg_infot > &cfg_info_opt)
Returns true iff a DECL x must be added to the local write set.
Definition: contracts.cpp:1227
Verify and use annotated invariants and pre/post-conditions.
#define CPROVER_PREFIX
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:126
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 ...
const code_function_callt & to_code_function_call(const codet &code)
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:23
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 bitvector analysis.
Field-insensitive, location-sensitive may-alias analysis.
void get_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
Definition: loop_utils.cpp:72
natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Mathematical types.
Predicates to specify memory footprint in function contracts.
nonstd::optional< T > optionalt
Definition: optional.h:35
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
Pointer Logic.
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:117
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:108
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:88
Program Transformation.
#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:34
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: kdev_t.h:24
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:215
exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
Generate a validity check over all dereferences in an expression.
Definition: utils.cpp:122
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &location, const irep_idt &mode, symbol_table_baset &symtab, std::string suffix, bool is_auxiliary)
Adds a fresh and uniquely named symbol to the symbol table.
Definition: utils.cpp:190
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:180
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:204
void add_pragma_disable_assigns_check(source_locationt &location)
Adds a pragma on a source_locationt to disable inclusion checking.
Definition: utils.cpp:103
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:136
#define CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK
Definition: utils.h:27