cprover
code_contracts.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Verify and use annotated invariants and pre/post-conditions
4 
5 Author: Michael Tautschnig
6 
7 Date: February 2016
8 
9 \*******************************************************************/
10 
13 
14 #include <algorithm>
15 #include <unordered_set>
16 
18 
20 
22 
23 #include <util/c_types.h>
24 #include <util/expr_util.h>
25 #include <util/fresh_symbol.h>
26 #include <util/message.h>
27 #include <util/pointer_expr.h>
29 #include <util/replace_symbol.h>
30 
31 #include "code_contracts.h"
32 #include "loop_utils.h"
33 
38 {
39 public:
41  {
42  }
43 
44  // \brief Has this object been passed to exprt::visit() on an exprt whose
45  // descendants contain __CPROVER_return_value?
47  {
48  return found;
49  }
50 
51  void operator()(const exprt &exp) override
52  {
53  if(exp.id() != ID_symbol)
54  return;
55  const symbol_exprt &sym = to_symbol_expr(exp);
56  found |= sym.get_identifier() == CPROVER_PREFIX "return_value";
57  }
58 
59 protected:
60  bool found;
61 };
62 
64  goto_functionst::goto_functiont &goto_function,
65  const local_may_aliast &local_may_alias,
66  const goto_programt::targett loop_head,
67  const loopt &loop)
68 {
69  PRECONDITION(!loop.empty());
70 
71  // find the last back edge
72  goto_programt::targett loop_end=loop_head;
74  it=loop.begin();
75  it!=loop.end();
76  ++it)
77  if((*it)->is_goto() &&
78  (*it)->get_target()==loop_head &&
79  (*it)->location_number>loop_end->location_number)
80  loop_end=*it;
81 
82  // see whether we have an invariant
83  exprt invariant = static_cast<const exprt &>(
84  loop_end->get_condition().find(ID_C_spec_loop_invariant));
85  if(invariant.is_nil())
86  return;
87 
88  // change H: loop; E: ...
89  // to
90  // H: assert(invariant);
91  // havoc;
92  // assume(invariant);
93  // if(guard) goto E:
94  // loop;
95  // assert(invariant);
96  // assume(false);
97  // E: ...
98 
99  // find out what can get changed in the loop
100  modifiest modifies;
101  get_modifies(local_may_alias, loop, modifies);
102 
103  // build the havocking code
104  goto_programt havoc_code;
105 
106  // assert the invariant
107  {
108  goto_programt::targett a = havoc_code.add(
109  goto_programt::make_assertion(invariant, loop_head->source_location));
110  a->source_location.set_comment("Loop invariant violated before entry");
111  }
112 
113  // havoc variables being written to
114  build_havoc_code(loop_head, modifies, havoc_code);
115 
116  // assume the invariant
117  havoc_code.add(
118  goto_programt::make_assumption(invariant, loop_head->source_location));
119 
120  // non-deterministically skip the loop if it is a do-while loop
121  if(!loop_head->is_goto())
122  {
123  havoc_code.add(goto_programt::make_goto(
124  loop_end,
126  }
127 
128  // Now havoc at the loop head. Use insert_swap to
129  // preserve jumps to loop head.
130  goto_function.body.insert_before_swap(loop_head, havoc_code);
131 
132  // assert the invariant at the end of the loop body
133  {
135  goto_programt::make_assertion(invariant, loop_end->source_location);
136  a.source_location.set_comment("Loop invariant not preserved");
137  goto_function.body.insert_before_swap(loop_end, a);
138  ++loop_end;
139  }
140 
141  // change the back edge into assume(false) or assume(guard)
142  loop_end->targets.clear();
143  loop_end->type=ASSUME;
144  if(loop_head->is_goto())
145  loop_end->set_condition(false_exprt());
146  else
147  loop_end->set_condition(boolean_negate(loop_end->get_condition()));
148 }
149 
151 {
152  const symbolt &function_symbol = ns.lookup(fun_name);
153  const code_typet &type = to_code_type(function_symbol.type);
154  if(type.find(ID_C_spec_assigns).is_not_nil())
155  return true;
156 
157  return type.find(ID_C_spec_requires).is_not_nil() ||
158  type.find(ID_C_spec_ensures).is_not_nil();
159 }
160 
162  goto_programt &goto_program,
163  goto_programt::targett target)
164 {
165  const code_function_callt &call = target->get_function_call();
166 
167  // Return if the function is not named in the call; currently we don't handle
168  // function pointers.
169  // TODO: handle function pointers.
170  if(call.function().id() != ID_symbol)
171  return false;
172 
173  // Retrieve the function type, which is needed to extract the contract
174  // components.
175  const irep_idt &function = to_symbol_expr(call.function()).get_identifier();
176  const symbolt &function_symbol = ns.lookup(function);
177  const code_typet &type = to_code_type(function_symbol.type);
178 
179  // Isolate each component of the contract.
180  exprt assigns = static_cast<const exprt &>(type.find(ID_C_spec_assigns));
181  exprt requires = static_cast<const exprt &>(type.find(ID_C_spec_requires));
182  exprt ensures = static_cast<const exprt &>(type.find(ID_C_spec_ensures));
183 
184  // Check to see if the function contract actually constrains its effect on
185  // the program state; if not, return.
186  if(ensures.is_nil() && assigns.is_nil())
187  return false;
188 
189  // Create a replace_symbolt object, for replacing expressions in the callee
190  // with expressions from the call site (e.g. the return value).
192  if(type.return_type() != empty_typet())
193  {
194  // Check whether the function's return value is not disregarded.
195  if(call.lhs().is_not_nil())
196  {
197  // If so, have it replaced appropriately.
198  // For example, if foo() ensures that its return value is > 5, then
199  // rewrite calls to foo as follows:
200  // x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5)
201  symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
202  replace.insert(ret_val, call.lhs());
203  }
204  else
205  {
206  // If the function does return a value, but the return value is
207  // disregarded, check if the postcondition includes the return value.
209  ensures.visit(v);
210  if(v.found_return_value())
211  {
212  // The postcondition does mention __CPROVER_return_value, so mint a
213  // fresh variable to replace __CPROVER_return_value with.
214  const symbolt &fresh = get_fresh_aux_symbol(
215  type.return_type(),
216  id2string(function),
217  "ignored_return_value",
218  call.source_location(),
219  symbol_table.lookup_ref(function).mode,
220  ns,
221  symbol_table);
222  symbol_exprt ret_val(CPROVER_PREFIX "return_value", type.return_type());
223  replace.insert(ret_val, fresh.symbol_expr());
224  }
225  }
226  }
227 
228  // Replace formal parameters
229  code_function_callt::argumentst::const_iterator a_it=
230  call.arguments().begin();
231  for(code_typet::parameterst::const_iterator p_it = type.parameters().begin();
232  p_it != type.parameters().end() && a_it != call.arguments().end();
233  ++p_it, ++a_it)
234  {
235  if(!p_it->get_identifier().empty())
236  {
237  symbol_exprt p(p_it->get_identifier(), p_it->type());
238  replace.insert(p, *a_it);
239  }
240  }
241 
242  // Replace expressions in the contract components.
243  replace(assigns);
244  replace(requires);
245  replace(ensures);
246 
247  // Insert assertion of the precondition immediately before the call site.
248  if(requires.is_not_nil())
249  {
252 
253  goto_program.insert_before_swap(target, a);
254  ++target;
255  }
256 
257  // Create a series of non-deterministic assignments to havoc the variables
258  // in the assigns clause.
259  if(assigns.is_not_nil())
260  {
261  goto_programt assigns_havoc;
262  modifiest assigns_tgts;
263  const exprt::operandst &targets = assigns.operands();
264  for(const exprt &curr_op : targets)
265  {
266  if(curr_op.id() == ID_symbol || curr_op.id() == ID_dereference)
267  {
268  assigns_tgts.insert(curr_op);
269  }
270  else
271  {
272  log.error() << "Unable to apply assigns clause for expression of type '"
273  << curr_op.id() << "'; not enforcing assigns clause."
274  << messaget::eom;
275  return true;
276  }
277  }
278  build_havoc_code(target, assigns_tgts, assigns_havoc);
279 
280  // Insert the non-deterministic assignment immediately before the call site.
281  goto_program.insert_before_swap(target, assigns_havoc);
282  std::advance(target, assigns_tgts.size());
283  }
284 
285  // To remove the function call, replace it with an assumption statement
286  // assuming the postcondition, if there is one. Otherwise, replace the
287  // function call with a SKIP statement.
288  if(ensures.is_not_nil())
289  {
290  *target = goto_programt::make_assumption(ensures, target->source_location);
291  }
292  else
293  {
294  *target = goto_programt::make_skip();
295  }
296 
297  // Add this function to the set of replaced functions.
298  summarized.insert(function);
299  return false;
300 }
301 
303  goto_functionst::goto_functiont &goto_function)
304 {
305  local_may_aliast local_may_alias(goto_function);
306  natural_loops_mutablet natural_loops(goto_function.body);
307 
308  // iterate over the (natural) loops in the function
309  for(natural_loops_mutablet::loop_mapt::const_iterator l_it =
310  natural_loops.loop_map.begin();
311  l_it != natural_loops.loop_map.end();
312  l_it++)
314  goto_function, local_may_alias, l_it->first, l_it->second);
315 
316  // look at all function calls
317  Forall_goto_program_instructions(ins, goto_function.body)
318  if(ins->is_function_call())
319  apply_contract(goto_function.body, ins);
320 }
321 
323  const typet &type,
324  const source_locationt &source_location,
325  const irep_idt &function_id,
326  const irep_idt &mode)
327 {
328  return get_fresh_aux_symbol(
329  type,
330  id2string(function_id) + "::tmp_cc",
331  "tmp_cc",
332  source_location,
333  mode,
334  symbol_table);
335 }
336 
338  const exprt &assigns,
339  const exprt &lhs,
340  std::vector<exprt> &aliasable_references)
341 {
342  bool first_iter = true;
343  exprt running = false_exprt();
344  for(auto aliasable : aliasable_references)
345  {
346  exprt left_ptr = address_of_exprt{lhs};
347  exprt right_ptr = aliasable;
348  exprt same = same_object(left_ptr, right_ptr);
349 
350  if(first_iter)
351  {
352  running = same;
353  first_iter = false;
354  }
355  else
356  {
357  exprt::operandst disjuncts;
358  disjuncts.push_back(same);
359  disjuncts.push_back(running);
360  running = disjunction(disjuncts);
361  }
362  }
363 
364  return running;
365 }
366 
368  const symbolt &function_symbol,
369  const irep_idt &function_id,
370  goto_programt &created_decls,
371  std::vector<exprt> &created_references)
372 {
373  const code_typet &type = to_code_type(function_symbol.type);
374  const exprt &assigns =
375  static_cast<const exprt &>(type.find(ID_C_spec_assigns));
376 
377  const exprt::operandst &targets = assigns.operands();
378  for(const exprt &curr_op : targets)
379  {
380  // Declare a new symbol to stand in for the reference
381  symbol_exprt standin = new_tmp_symbol(
382  pointer_type(curr_op.type()),
383  function_symbol.location,
384  function_id,
385  function_symbol.mode)
386  .symbol_expr();
387 
388  created_decls.add(
389  goto_programt::make_decl(standin, function_symbol.location));
390 
391  created_decls.add(goto_programt::make_assignment(
392  code_assignt(standin, std::move(address_of_exprt{curr_op})),
393  function_symbol.location));
394 
395  // Add a map entry from the original operand to the new symbol
396  created_references.push_back(standin);
397  }
398 }
399 
401  goto_programt::instructionst::iterator &instruction_iterator,
402  goto_programt &program,
403  exprt &assigns,
404  std::vector<exprt> &assigns_references,
405  std::set<exprt> &freely_assignable_exprs)
406 {
407  INVARIANT(
408  instruction_iterator->is_assign(),
409  "The first argument of instrument_assigns_statement should always be"
410  " an assignment");
411  const exprt &lhs = instruction_iterator->get_assign().lhs();
412  if(freely_assignable_exprs.find(lhs) != freely_assignable_exprs.end())
413  {
414  return;
415  }
416  exprt alias_expr = create_alias_expression(assigns, lhs, assigns_references);
417 
418  goto_programt alias_assertion;
419  alias_assertion.add(goto_programt::make_assertion(
420  alias_expr, instruction_iterator->source_location));
421  program.insert_before_swap(instruction_iterator, alias_assertion);
422  ++instruction_iterator;
423 }
424 
426  goto_programt::instructionst::iterator &instruction_iterator,
427  goto_programt &program,
428  exprt &assigns,
429  std::vector<exprt> &aliasable_references,
430  std::set<exprt> &freely_assignable_exprs)
431 {
432  INVARIANT(
433  instruction_iterator->is_function_call(),
434  "The first argument of instrument_call_statement should always be "
435  "a function call");
436  code_function_callt call = instruction_iterator->get_function_call();
437  const irep_idt &called_name =
439 
440  // Malloc allocates memory which is not part of the caller's memory
441  // frame, so we want to capture the newly-allocated memory and
442  // treat it as assignable.
443  if(called_name == "malloc")
444  {
445  aliasable_references.push_back(call.lhs());
446 
447  // Make the variable, where result of malloc is stored, freely assignable.
448  goto_programt::instructionst::iterator local_instruction_iterator =
449  instruction_iterator;
450  local_instruction_iterator++;
451  if(
452  local_instruction_iterator->is_assign() &&
453  local_instruction_iterator->get_assign().lhs().is_not_nil())
454  {
455  freely_assignable_exprs.insert(
456  local_instruction_iterator->get_assign().lhs());
457  }
458  return; // assume malloc edits no currently-existing memory objects.
459  }
460 
461  if(call.lhs().is_not_nil())
462  {
463  exprt alias_expr =
464  create_alias_expression(assigns, call.lhs(), aliasable_references);
465 
466  goto_programt alias_assertion;
467  alias_assertion.add(goto_programt::make_assertion(
468  alias_expr, instruction_iterator->source_location));
469  program.insert_before_swap(instruction_iterator, alias_assertion);
470  ++instruction_iterator;
471  }
472 
473  // TODO we don't handle function pointers
474  if(call.function().id() == ID_symbol)
475  {
476  const symbolt &called_sym = ns.lookup(called_name);
477  const code_typet &called_type = to_code_type(called_sym.type);
478 
479  auto called_func = goto_functions.function_map.find(called_name);
480  if(called_func == goto_functions.function_map.end())
481  {
482  log.error() << "Could not find function '" << called_name
483  << "' in goto-program; not enforcing assigns clause."
484  << messaget::eom;
485  return;
486  }
487 
488  exprt called_assigns =
489  static_cast<const exprt &>(called_sym.type.find(ID_C_spec_assigns));
490  if(called_assigns.is_nil()) // Called function has no assigns clause
491  {
492  // Fail if called function has no assigns clause.
493  log.error() << "No assigns specification found for function '"
494  << called_name
495  << "' in goto-program; not enforcing assigns clause."
496  << messaget::eom;
497 
498  // Create a false assertion, so the analysis will fail if this function
499  // is called.
500  goto_programt failing_assertion;
501  failing_assertion.add(goto_programt::make_assertion(
502  false_exprt(), instruction_iterator->source_location));
503  program.insert_before_swap(instruction_iterator, failing_assertion);
504  ++instruction_iterator;
505 
506  return;
507  }
508  else // Called function has assigns clause
509  {
511  // Replace formal parameters
512  code_function_callt::argumentst::const_iterator a_it =
513  call.arguments().begin();
514  for(code_typet::parameterst::const_iterator p_it =
515  called_type.parameters().begin();
516  p_it != called_type.parameters().end() &&
517  a_it != call.arguments().end();
518  ++p_it, ++a_it)
519  {
520  if(!p_it->get_identifier().empty())
521  {
522  symbol_exprt p(p_it->get_identifier(), p_it->type());
523  replace.insert(p, *a_it);
524  }
525  }
526 
527  replace(called_assigns);
528  for(exprt::operandst::const_iterator called_op_it =
529  called_assigns.operands().begin();
530  called_op_it != called_assigns.operands().end();
531  called_op_it++)
532  {
533  if(
534  freely_assignable_exprs.find(*called_op_it) !=
535  freely_assignable_exprs.end())
536  {
537  continue;
538  }
539  exprt alias_expr =
540  create_alias_expression(assigns, *called_op_it, aliasable_references);
541 
542  goto_programt alias_assertion;
543  alias_assertion.add(goto_programt::make_assertion(
544  alias_expr, instruction_iterator->source_location));
545  program.insert_before_swap(instruction_iterator, alias_assertion);
546  ++instruction_iterator;
547  }
548  }
549  }
550 }
551 
553 {
554  // Collect all GOTOs and mallocs
555  std::vector<goto_programt::instructiont> back_gotos;
556  std::vector<goto_programt::instructiont> malloc_calls;
557 
558  int idx = 0;
559  for(goto_programt::instructiont instruction : program.instructions)
560  {
561  if(instruction.is_backwards_goto())
562  {
563  back_gotos.push_back(instruction);
564  }
565  if(instruction.is_function_call())
566  {
567  code_function_callt call = instruction.get_function_call();
568  const irep_idt &called_name =
570 
571  if(called_name == "malloc")
572  {
573  malloc_calls.push_back(instruction);
574  }
575  }
576  idx++;
577  }
578  // Make sure there are no gotos that go back such that a malloc is between
579  // the goto and its destination (possible loop).
580  for(auto goto_entry : back_gotos)
581  {
582  for(const auto &target : goto_entry.targets)
583  {
584  for(auto malloc_entry : malloc_calls)
585  {
586  if(
587  malloc_entry.location_number >= target->location_number &&
588  malloc_entry.location_number < goto_entry.location_number)
589  {
590  // In order to statically keep track of all the memory we should
591  // be able to assign, we need to create ghost variables to store
592  // references to that memory.
593  // If a malloc is in a loop, we can't generally determine how many
594  // times it will run in order to create an appropriate number of
595  // references for the assignable memory.
596  // So, if we have a malloc in a loop, we can't statically create the
597  // assertion statements needed to enforce the assigns clause.
598  log.error() << "Call to malloc at location "
599  << malloc_entry.location_number << " falls between goto "
600  << "source location " << goto_entry.location_number
601  << " and it's destination at location "
602  << target->location_number << ". "
603  << "Unable to complete instrumentation, as this malloc "
604  << "may be in a loop." << messaget::eom;
605  throw 0;
606  }
607  }
608  }
609  }
610  return false;
611 }
612 
613 bool code_contractst::add_pointer_checks(const std::string &function_name)
614 {
615  // Get the function object before instrumentation.
616  auto old_function = goto_functions.function_map.find(function_name);
617  if(old_function == goto_functions.function_map.end())
618  {
619  log.error() << "Could not find function '" << function_name
620  << "' in goto-program; not enforcing contracts."
621  << messaget::eom;
622  return true;
623  }
624  goto_programt &program = old_function->second.body;
625  if(program.instructions.empty()) // empty function body
626  {
627  return false;
628  }
629 
630  const irep_idt function_id(function_name);
631  const symbolt &function_symbol = ns.lookup(function_id);
632  const code_typet &type = to_code_type(function_symbol.type);
633 
634  exprt assigns = static_cast<const exprt &>(type.find(ID_C_spec_assigns));
635 
636  // Return if there are no reference checks to perform.
637  if(assigns.is_nil())
638  return false;
639 
640  goto_programt::instructionst::iterator instruction_iterator =
641  program.instructions.begin();
642 
643  // Create temporary variables to hold the assigns clause targets before
644  // they can be modified.
645  goto_programt standin_decls;
646  std::vector<exprt> original_references;
648  function_symbol, function_id, standin_decls, original_references);
649 
650  // Create a list of variables that are okay to assign.
651  std::set<exprt> freely_assignable_exprs;
652  for(code_typet::parametert param : type.parameters())
653  {
654  freely_assignable_exprs.insert(param);
655  }
656 
657  int lines_to_iterate = standin_decls.instructions.size();
658  program.insert_before_swap(instruction_iterator, standin_decls);
659  std::advance(instruction_iterator, lines_to_iterate);
660 
661  if(check_for_looped_mallocs(program))
662  {
663  return true;
664  }
665 
666  // Insert aliasing assertions
667  for(; instruction_iterator != program.instructions.end();
668  ++instruction_iterator)
669  {
670  if(instruction_iterator->is_decl())
671  {
672  freely_assignable_exprs.insert(instruction_iterator->decl_symbol());
673  }
674  else if(instruction_iterator->is_assign())
675  {
677  instruction_iterator,
678  program,
679  assigns,
680  original_references,
681  freely_assignable_exprs);
682  }
683  else if(instruction_iterator->is_function_call())
684  {
686  instruction_iterator,
687  program,
688  assigns,
689  original_references,
690  freely_assignable_exprs);
691  }
692  }
693  return false;
694 }
695 
696 bool code_contractst::enforce_contract(const std::string &fun_to_enforce)
697 {
698  // Add statements to the source function to ensure assigns clause is
699  // respected.
700  add_pointer_checks(fun_to_enforce);
701 
702  // Rename source function
703  std::stringstream ss;
704  ss << CPROVER_PREFIX << "contracts_original_" << fun_to_enforce;
705  const irep_idt mangled(ss.str());
706  const irep_idt original(fun_to_enforce);
707 
708  auto old_function = goto_functions.function_map.find(original);
709  if(old_function == goto_functions.function_map.end())
710  {
711  log.error() << "Could not find function '" << fun_to_enforce
712  << "' in goto-program; not enforcing contracts."
713  << messaget::eom;
714  return true;
715  }
716 
717  std::swap(goto_functions.function_map[mangled], old_function->second);
718  goto_functions.function_map.erase(old_function);
719 
720  // Place a new symbol with the mangled name into the symbol table
721  source_locationt sl;
722  sl.set_file("instrumented for code contracts");
723  sl.set_line("0");
724  symbolt mangled_sym;
725  const symbolt *original_sym = symbol_table.lookup(original);
726  mangled_sym = *original_sym;
727  mangled_sym.name = mangled;
728  mangled_sym.base_name = mangled;
729  mangled_sym.location = sl;
730  const auto mangled_found = symbol_table.insert(std::move(mangled_sym));
731  INVARIANT(
732  mangled_found.second,
733  "There should be no existing function called " + ss.str() +
734  " in the symbol table because that name is a mangled name");
735 
736  // Insert wrapper function into goto_functions
737  auto nexist_old_function = goto_functions.function_map.find(original);
738  INVARIANT(
739  nexist_old_function == goto_functions.function_map.end(),
740  "There should be no function called " + fun_to_enforce +
741  " in the function map because that function should have had its"
742  " name mangled");
743 
744  auto mangled_fun = goto_functions.function_map.find(mangled);
745  INVARIANT(
746  mangled_fun != goto_functions.function_map.end(),
747  "There should be a function called " + ss.str() +
748  " in the function map because we inserted a fresh goto-program"
749  " with that mangled name");
750 
751  goto_functiont &wrapper = goto_functions.function_map[original];
752  wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers;
754  add_contract_check(original, mangled, wrapper.body);
755  return false;
756 }
757 
759  const irep_idt &wrapper_fun,
760  const irep_idt &mangled_fun,
761  goto_programt &dest)
762 {
763  PRECONDITION(!dest.instructions.empty());
764 
765  const symbolt &function_symbol = ns.lookup(mangled_fun);
766  const code_typet &code_type = to_code_type(function_symbol.type);
767 
768  const exprt &assigns =
769  static_cast<const exprt &>(code_type.find(ID_C_spec_assigns));
770  const exprt &requires =
771  static_cast<const exprt &>(code_type.find(ID_C_spec_requires));
772  const exprt &ensures =
773  static_cast<const exprt &>(code_type.find(ID_C_spec_ensures));
774  INVARIANT(
775  ensures.is_not_nil() || assigns.is_not_nil(),
776  "Code contract enforcement is trivial without an ensures or assigns "
777  "clause.");
778 
779  // build:
780  // if(nondet)
781  // decl ret
782  // decl parameter1 ...
783  // assume(requires) [optional]
784  // ret=function(parameter1, ...)
785  // assert(ensures)
786  // skip: ...
787 
788  // build skip so that if(nondet) can refer to it
789  goto_programt tmp_skip;
791  tmp_skip.add(goto_programt::make_skip(ensures.source_location()));
792 
793  goto_programt check;
794 
795  // if(nondet)
797  skip,
799  skip->source_location));
800 
801  // prepare function call including all declarations
802  code_function_callt call(function_symbol.symbol_expr());
804 
805  // decl ret
806  if(code_type.return_type() != empty_typet())
807  {
809  code_type.return_type(),
810  skip->source_location,
811  wrapper_fun,
812  function_symbol.mode)
813  .symbol_expr();
814  check.add(goto_programt::make_decl(r, skip->source_location));
815 
816  call.lhs()=r;
817 
818  symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
819  replace.insert(ret_val, r);
820  }
821 
822  // decl parameter1 ...
823  goto_functionst::function_mapt::iterator f_it =
824  goto_functions.function_map.find(mangled_fun);
826 
827  const goto_functionst::goto_functiont &gf = f_it->second;
828  for(const auto &parameter : gf.parameter_identifiers)
829  {
830  PRECONDITION(!parameter.empty());
831  const symbolt &parameter_symbol = ns.lookup(parameter);
832 
834  parameter_symbol.type,
835  skip->source_location,
836  wrapper_fun,
837  parameter_symbol.mode)
838  .symbol_expr();
840 
841  call.arguments().push_back(p);
842 
843  replace.insert(parameter_symbol.symbol_expr(), p);
844  }
845 
846  // assume(requires)
847  if(requires.is_not_nil())
848  {
849  // rewrite any use of parameters
850  exprt requires_cond = requires;
851  replace(requires_cond);
852 
854  requires_cond, requires.source_location()));
855  }
856 
857  // ret=mangled_fun(parameter1, ...)
859 
860  // rewrite any use of __CPROVER_return_value
861  exprt ensures_cond = ensures;
862  replace(ensures_cond);
863 
864  // assert(ensures)
865  if(ensures.is_not_nil())
866  {
867  check.add(
868  goto_programt::make_assertion(ensures_cond, ensures.source_location()));
869  }
870 
871  // prepend the new code to dest
872  check.destructive_append(tmp_skip);
873  dest.destructive_insert(dest.instructions.begin(), check);
874 }
875 
877  const std::set<std::string> &funs_to_replace)
878 {
879  bool fail = false;
880  for(const auto &fun : funs_to_replace)
881  {
882  if(!has_contract(fun))
883  {
884  log.error() << "Function '" << fun
885  << "' does not have a contract; "
886  "not replacing calls with contract."
887  << messaget::eom;
888  fail = true;
889  }
890  }
891  if(fail)
892  return true;
893 
894  for(auto &goto_function : goto_functions.function_map)
895  {
896  Forall_goto_program_instructions(ins, goto_function.second.body)
897  {
898  if(ins->is_function_call())
899  {
900  const code_function_callt &call = ins->get_function_call();
901 
902  // TODO we don't handle function pointers
903  if(call.function().id() != ID_symbol)
904  continue;
905 
906  const irep_idt &fun_name =
908  auto found = std::find(
909  funs_to_replace.begin(), funs_to_replace.end(), id2string(fun_name));
910  if(found == funs_to_replace.end())
911  continue;
912 
913  fail |= apply_contract(goto_function.second.body, ins);
914  }
915  }
916  }
917 
918  if(fail)
919  return true;
920 
921  for(auto &goto_function : goto_functions.function_map)
922  remove_skip(goto_function.second.body);
923 
925 
926  return false;
927 }
928 
930 {
931  std::set<std::string> funs_to_replace;
932  for(auto &goto_function : goto_functions.function_map)
933  {
934  if(has_contract(goto_function.first))
935  funs_to_replace.insert(id2string(goto_function.first));
936  }
937  return replace_calls(funs_to_replace);
938 }
939 
941 {
942  std::set<std::string> funs_to_enforce;
943  for(auto &goto_function : goto_functions.function_map)
944  {
945  if(has_contract(goto_function.first))
946  funs_to_enforce.insert(id2string(goto_function.first));
947  }
948  return enforce_contracts(funs_to_enforce);
949 }
950 
952  const std::set<std::string> &funs_to_enforce)
953 {
954  bool fail = false;
955  for(const auto &fun : funs_to_enforce)
956  {
957  if(!has_contract(fun))
958  {
959  fail = true;
960  log.error() << "Could not find function '" << fun
961  << "' in goto-program; not enforcing contracts."
962  << messaget::eom;
963  continue;
964  }
965 
966  if(!fail)
967  fail |= enforce_contract(fun);
968  }
969  return fail;
970 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1172
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_contractst::code_contracts
void code_contracts(goto_functionst::goto_functiont &goto_function)
Definition: code_contracts.cpp:302
goto_functiont::body
goto_programt body
Definition: goto_function.h:29
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:334
code_contractst::add_contract_check
void add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest)
Definition: code_contracts.cpp:758
source_locationt::set_comment
void set_comment(const irep_idt &comment)
Definition: source_location.h:141
code_contractst::populate_assigns_references
void populate_assigns_references(const symbolt &f_sym, const irep_idt &func_id, goto_programt &created_decls, std::vector< exprt > &created_references)
Creates a local variable declaration for each expression in the assigns clause (of the function given...
Definition: code_contracts.cpp:367
code_contractst::instrument_call_statement
void instrument_call_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, std::vector< exprt > &assigns_references, std::set< exprt > &freely_assignable_exprs)
Inserts an assertion statement into program before the function call at ins_it, to ensure that any me...
Definition: code_contracts.cpp:425
typet
The type of an expression, extends irept.
Definition: type.h:28
fresh_symbol.h
Fresh auxiliary symbol creation.
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
replace_symbol.h
pointer_predicates.h
Various predicates over pointers in programs.
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:67
return_value_visitort
Predicate to be used with the exprt::visit() function.
Definition: code_contracts.cpp:38
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:928
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:657
loop_templatet::end
const_iterator end() const
Iterator over this loop's instructions.
Definition: loop_analysis.h:55
exprt
Base class for all expressions.
Definition: expr.h:54
code_contractst::log
messaget & log
Definition: code_contracts.h:88
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool_typet
The Boolean type.
Definition: std_types.h:37
messaget::eom
static eomt eom
Definition: message.h:297
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:891
return_value_visitort::return_value_visitort
return_value_visitort()
Definition: code_contracts.cpp:40
exprt::visit
void visit(class expr_visitort &visitor)
These are pre-order traversal visitors, i.e., the visitor is executed on a node before its children h...
Definition: expr.cpp:269
check_apply_invariants
static void check_apply_invariants(goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, const goto_programt::targett loop_head, const loopt &loop)
Definition: code_contracts.cpp:63
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1240
local_may_aliast
Definition: local_may_alias.h:26
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:995
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:969
source_locationt::set_line
void set_line(const irep_idt &line)
Definition: source_location.h:106
goto_programt::make_function_call
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition: goto_program.h:1020
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
loop_templatet::begin
const_iterator begin() const
Iterator over this loop's instructions.
Definition: loop_analysis.h:49
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
disjunction
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:29
modifiest
std::set< exprt > modifiest
Definition: loop_utils.h:17
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:864
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::error
mstreamt & error() const
Definition: message.h:399
loop_templatet::const_iterator
loop_instructionst::const_iterator const_iterator
Definition: loop_analysis.h:46
empty_typet
The empty type.
Definition: std_types.h:46
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:648
local_may_alias.h
Field-insensitive, location-sensitive may-alias analysis.
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:822
code_contractst::has_contract
bool has_contract(const irep_idt)
Does the named function have a contract?
Definition: code_contracts.cpp:150
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
boolean_negate
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:128
code_contractst::instrument_assigns_statement
void instrument_assigns_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, std::vector< exprt > &original_references, std::set< exprt > &freely_assignable_exprs)
Inserts an assertion statement into program before the assignment ins_it, to ensure that the left-han...
Definition: code_contracts.cpp:400
goto_programt::instructiont::is_backwards_goto
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:508
source_locationt::set_file
void set_file(const irep_idt &file)
Definition: source_location.h:96
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
pointer_expr.h
API to expression classes for Pointers.
goto_programt::instructiont::get_function_call
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
Definition: goto_program.h:306
code_contractst::check_for_looped_mallocs
bool check_for_looped_mallocs(const goto_programt &)
Check if there are any malloc statements which may be repeated because of a goto statement that jumps...
Definition: code_contracts.cpp:552
code_contractst::apply_contract
bool apply_contract(goto_programt &goto_program, goto_programt::targett target)
Definition: code_contracts.cpp:161
code_contractst::add_pointer_checks
bool add_pointer_checks(const std::string &)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
Definition: code_contracts.cpp:613
loop_templatet
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:19
const_expr_visitort
Definition: expr.h:377
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
code_typet
Base type of functions.
Definition: std_types.h:744
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
code_contractst::ns
namespacet ns
Definition: code_contracts.h:83
false_exprt
The Boolean constant false.
Definition: std_expr.h:2726
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:860
natural_loops_templatet< goto_programt, goto_programt::targett >
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
loop_utils.h
Helper functions for k-induction and loop invariants.
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:640
source_locationt
Definition: source_location.h:20
return_value_visitort::operator()
void operator()(const exprt &exp) override
Definition: code_contracts.cpp:51
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
code_contractst::new_tmp_symbol
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &function_id, const irep_idt &mode)
Definition: code_contracts.cpp:322
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
expr_util.h
Deprecated expression utility functions.
code_contractst::enforce_contracts
bool enforce_contracts()
Call enforce_contracts() on all functions that have a contract.
Definition: code_contracts.cpp:940
code_contractst::goto_functions
goto_functionst & goto_functions
Definition: code_contracts.h:85
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
ASSUME
@ ASSUME
Definition: goto_program.h:36
get_modifies
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:88
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_functionst::update
void update()
Definition: goto_functions.h:81
same_object
exprt same_object(const exprt &p1, const exprt &p2)
Definition: pointer_predicates.cpp:27
code_typet::parametert
Definition: std_types.h:761
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
create_alias_expression
static exprt create_alias_expression(const exprt &assigns, const exprt &lhs, std::vector< exprt > &aliasable_references)
Definition: code_contracts.cpp:337
code_contractst::replace_calls
bool replace_calls()
Call replace_calls() on all calls to any function that has a contract.
Definition: code_contracts.cpp:929
code_contractst::summarized
std::unordered_set< irep_idt > summarized
Definition: code_contracts.h:90
loop_templatet::empty
bool empty() const
Returns true if this loop contains no instructions.
Definition: loop_analysis.h:67
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:850
goto_functiont::parameter_identifiers
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:36
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:876
exprt::operands
operandst & operands()
Definition: expr.h:96
r
static int8_t r
Definition: irep_hash.h:59
code_contractst::enforce_contract
bool enforce_contract(const std::string &)
Enforce contract of a single function.
Definition: code_contracts.cpp:696
static_lifetime_init.h
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:200
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:577
return_value_visitort::found_return_value
bool found_return_value()
Definition: code_contracts.cpp:46
remove_skip.h
Program Transformation.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
build_havoc_code
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition: loop_utils.cpp:38
message.h
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:432
return_value_visitort::found
bool found
Definition: code_contracts.cpp:60
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:234
c_types.h
get_fresh_aux_symbol
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 ...
Definition: fresh_symbol.cpp:32
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:550
code_contractst::symbol_table
symbol_tablet & symbol_table
Definition: code_contracts.h:84
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
code_contracts.h
Verify and use annotated invariants and pre/post-conditions.
loop_analysist::loop_map
loop_mapt loop_map
Definition: loop_analysis.h:88
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:25