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>
28 #include <util/replace_symbol.h>
29 
30 #include "code_contracts.h"
31 #include "loop_utils.h"
32 
37 {
38 public:
40  {
41  }
42 
43  // \brief Has this object been passed to exprt::visit() on an exprt whose
44  // descendants contain __CPROVER_return_value?
46  {
47  return found;
48  }
49 
50  void operator()(const exprt &exp) override
51  {
52  if(exp.id() != ID_symbol)
53  return;
54  const symbol_exprt &sym = to_symbol_expr(exp);
55  found |= sym.get_identifier() == CPROVER_PREFIX "return_value";
56  }
57 
58 protected:
59  bool found;
60 };
61 
63  goto_functionst::goto_functiont &goto_function,
64  const local_may_aliast &local_may_alias,
65  const goto_programt::targett loop_head,
66  const loopt &loop)
67 {
68  PRECONDITION(!loop.empty());
69 
70  // find the last back edge
71  goto_programt::targett loop_end=loop_head;
73  it=loop.begin();
74  it!=loop.end();
75  ++it)
76  if((*it)->is_goto() &&
77  (*it)->get_target()==loop_head &&
78  (*it)->location_number>loop_end->location_number)
79  loop_end=*it;
80 
81  // see whether we have an invariant
82  exprt invariant = static_cast<const exprt &>(
83  loop_end->get_condition().find(ID_C_spec_loop_invariant));
84  if(invariant.is_nil())
85  return;
86 
87  // change H: loop; E: ...
88  // to
89  // H: assert(invariant);
90  // havoc;
91  // assume(invariant);
92  // if(guard) goto E:
93  // loop;
94  // assert(invariant);
95  // assume(false);
96  // E: ...
97 
98  // find out what can get changed in the loop
99  modifiest modifies;
100  get_modifies(local_may_alias, loop, modifies);
101 
102  // build the havocking code
103  goto_programt havoc_code;
104 
105  // assert the invariant
106  {
107  goto_programt::targett a = havoc_code.add(
108  goto_programt::make_assertion(invariant, loop_head->source_location));
109  a->source_location.set_comment("Loop invariant violated before entry");
110  }
111 
112  // havoc variables being written to
113  build_havoc_code(loop_head, modifies, havoc_code);
114 
115  // assume the invariant
116  havoc_code.add(
117  goto_programt::make_assumption(invariant, loop_head->source_location));
118 
119  // non-deterministically skip the loop if it is a do-while loop
120  if(!loop_head->is_goto())
121  {
122  havoc_code.add(goto_programt::make_goto(
123  loop_end,
125  }
126 
127  // Now havoc at the loop head. Use insert_swap to
128  // preserve jumps to loop head.
129  goto_function.body.insert_before_swap(loop_head, havoc_code);
130 
131  // assert the invariant at the end of the loop body
132  {
134  goto_programt::make_assertion(invariant, loop_end->source_location);
135  a.source_location.set_comment("Loop invariant not preserved");
136  goto_function.body.insert_before_swap(loop_end, a);
137  ++loop_end;
138  }
139 
140  // change the back edge into assume(false) or assume(guard)
141  loop_end->targets.clear();
142  loop_end->type=ASSUME;
143  if(loop_head->is_goto())
144  loop_end->set_condition(false_exprt());
145  else
146  loop_end->set_condition(boolean_negate(loop_end->get_condition()));
147 }
148 
150 {
151  const symbolt &function_symbol = ns.lookup(fun_name);
152  const code_typet &type = to_code_type(function_symbol.type);
153  if(type.find(ID_C_spec_assigns).is_not_nil())
154  return true;
155 
156  return type.find(ID_C_spec_requires).is_not_nil() ||
157  type.find(ID_C_spec_ensures).is_not_nil();
158 }
159 
161  goto_programt &goto_program,
162  goto_programt::targett target)
163 {
164  const code_function_callt &call = target->get_function_call();
165 
166  // Return if the function is not named in the call; currently we don't handle
167  // function pointers.
168  // TODO: handle function pointers.
169  if(call.function().id() != ID_symbol)
170  return false;
171 
172  // Retrieve the function type, which is needed to extract the contract
173  // components.
174  const irep_idt &function = to_symbol_expr(call.function()).get_identifier();
175  const symbolt &function_symbol = ns.lookup(function);
176  const code_typet &type = to_code_type(function_symbol.type);
177 
178  // Isolate each component of the contract.
179  exprt assigns = static_cast<const exprt &>(type.find(ID_C_spec_assigns));
180  exprt requires = static_cast<const exprt &>(type.find(ID_C_spec_requires));
181  exprt ensures = static_cast<const exprt &>(type.find(ID_C_spec_ensures));
182 
183  // Check to see if the function contract actually constrains its effect on
184  // the program state; if not, return.
185  if(ensures.is_nil() && assigns.is_nil())
186  return false;
187 
188  // Create a replace_symbolt object, for replacing expressions in the callee
189  // with expressions from the call site (e.g. the return value).
191  if(type.return_type() != empty_typet())
192  {
193  // Check whether the function's return value is not disregarded.
194  if(call.lhs().is_not_nil())
195  {
196  // If so, have it replaced appropriately.
197  // For example, if foo() ensures that its return value is > 5, then
198  // rewrite calls to foo as follows:
199  // x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5)
200  symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
201  replace.insert(ret_val, call.lhs());
202  }
203  else
204  {
205  // If the function does return a value, but the return value is
206  // disregarded, check if the postcondition includes the return value.
208  ensures.visit(v);
209  if(v.found_return_value())
210  {
211  // The postcondition does mention __CPROVER_return_value, so mint a
212  // fresh variable to replace __CPROVER_return_value with.
213  const symbolt &fresh = get_fresh_aux_symbol(
214  type.return_type(),
215  id2string(function),
216  "ignored_return_value",
217  call.source_location(),
218  symbol_table.lookup_ref(function).mode,
219  ns,
220  symbol_table);
221  symbol_exprt ret_val(CPROVER_PREFIX "return_value", type.return_type());
222  replace.insert(ret_val, fresh.symbol_expr());
223  }
224  }
225  }
226 
227  // Replace formal parameters
228  code_function_callt::argumentst::const_iterator a_it=
229  call.arguments().begin();
230  for(code_typet::parameterst::const_iterator p_it = type.parameters().begin();
231  p_it != type.parameters().end() && a_it != call.arguments().end();
232  ++p_it, ++a_it)
233  {
234  if(!p_it->get_identifier().empty())
235  {
236  symbol_exprt p(p_it->get_identifier(), p_it->type());
237  replace.insert(p, *a_it);
238  }
239  }
240 
241  // Replace expressions in the contract components.
242  replace(assigns);
243  replace(requires);
244  replace(ensures);
245 
246  // Insert assertion of the precondition immediately before the call site.
247  if(requires.is_not_nil())
248  {
251 
252  goto_program.insert_before_swap(target, a);
253  ++target;
254  }
255 
256  // Create a series of non-deterministic assignments to havoc the variables
257  // in the assigns clause.
258  if(assigns.is_not_nil())
259  {
260  goto_programt assigns_havoc;
261  modifiest assigns_tgts;
262  const exprt::operandst &targets = assigns.operands();
263  for(const exprt &curr_op : targets)
264  {
265  if(curr_op.id() == ID_symbol || curr_op.id() == ID_dereference)
266  {
267  assigns_tgts.insert(curr_op);
268  }
269  else
270  {
271  log.error() << "Unable to apply assigns clause for expression of type '"
272  << curr_op.id() << "'; not enforcing assigns clause."
273  << messaget::eom;
274  return true;
275  }
276  }
277  build_havoc_code(target, assigns_tgts, assigns_havoc);
278 
279  // Insert the non-deterministic assignment immediately before the call site.
280  goto_program.insert_before_swap(target, assigns_havoc);
281  std::advance(target, assigns_tgts.size());
282  }
283 
284  // To remove the function call, replace it with an assumption statement
285  // assuming the postcondition, if there is one. Otherwise, replace the
286  // function call with a SKIP statement.
287  if(ensures.is_not_nil())
288  {
289  *target = goto_programt::make_assumption(ensures, target->source_location);
290  }
291  else
292  {
293  *target = goto_programt::make_skip();
294  }
295 
296  // Add this function to the set of replaced functions.
297  summarized.insert(function);
298  return false;
299 }
300 
302  goto_functionst::goto_functiont &goto_function)
303 {
304  local_may_aliast local_may_alias(goto_function);
305  natural_loops_mutablet natural_loops(goto_function.body);
306 
307  // iterate over the (natural) loops in the function
308  for(natural_loops_mutablet::loop_mapt::const_iterator l_it =
309  natural_loops.loop_map.begin();
310  l_it != natural_loops.loop_map.end();
311  l_it++)
313  goto_function, local_may_alias, l_it->first, l_it->second);
314 
315  // look at all function calls
316  Forall_goto_program_instructions(ins, goto_function.body)
317  if(ins->is_function_call())
318  apply_contract(goto_function.body, ins);
319 }
320 
322  const typet &type,
323  const source_locationt &source_location,
324  const irep_idt &function_id,
325  const irep_idt &mode)
326 {
327  return get_fresh_aux_symbol(
328  type,
329  id2string(function_id) + "::tmp_cc",
330  "tmp_cc",
331  source_location,
332  mode,
333  symbol_table);
334 }
335 
337  const exprt &assigns,
338  const exprt &lhs,
339  std::vector<exprt> &aliasable_references)
340 {
341  bool first_iter = true;
342  exprt running = false_exprt();
343  for(auto aliasable : aliasable_references)
344  {
345  exprt left_ptr = address_of_exprt{lhs};
346  exprt right_ptr = aliasable;
347  exprt same = same_object(left_ptr, right_ptr);
348 
349  if(first_iter)
350  {
351  running = same;
352  first_iter = false;
353  }
354  else
355  {
356  exprt::operandst disjuncts;
357  disjuncts.push_back(same);
358  disjuncts.push_back(running);
359  running = disjunction(disjuncts);
360  }
361  }
362 
363  return running;
364 }
365 
367  const symbolt &function_symbol,
368  const irep_idt &function_id,
369  goto_programt &created_decls,
370  std::vector<exprt> &created_references)
371 {
372  const code_typet &type = to_code_type(function_symbol.type);
373  const exprt &assigns =
374  static_cast<const exprt &>(type.find(ID_C_spec_assigns));
375 
376  const exprt::operandst &targets = assigns.operands();
377  for(const exprt &curr_op : targets)
378  {
379  // Declare a new symbol to stand in for the reference
380  symbol_exprt standin = new_tmp_symbol(
381  pointer_type(curr_op.type()),
382  function_symbol.location,
383  function_id,
384  function_symbol.mode)
385  .symbol_expr();
386 
387  created_decls.add(
388  goto_programt::make_decl(standin, function_symbol.location));
389 
390  created_decls.add(goto_programt::make_assignment(
391  code_assignt(standin, std::move(address_of_exprt{curr_op})),
392  function_symbol.location));
393 
394  // Add a map entry from the original operand to the new symbol
395  created_references.push_back(standin);
396  }
397 }
398 
400  goto_programt::instructionst::iterator &instruction_iterator,
401  goto_programt &program,
402  exprt &assigns,
403  std::vector<exprt> &assigns_references,
404  std::set<exprt> &freely_assignable_exprs)
405 {
406  INVARIANT(
407  instruction_iterator->is_assign(),
408  "The first argument of instrument_assigns_statement should always be"
409  " an assignment");
410  const exprt &lhs = instruction_iterator->get_assign().lhs();
411  if(freely_assignable_exprs.find(lhs) != freely_assignable_exprs.end())
412  {
413  return;
414  }
415  exprt alias_expr = create_alias_expression(assigns, lhs, assigns_references);
416 
417  goto_programt alias_assertion;
418  alias_assertion.add(goto_programt::make_assertion(
419  alias_expr, instruction_iterator->source_location));
420  program.insert_before_swap(instruction_iterator, alias_assertion);
421  ++instruction_iterator;
422 }
423 
425  goto_programt::instructionst::iterator &instruction_iterator,
426  goto_programt &program,
427  exprt &assigns,
428  std::vector<exprt> &aliasable_references,
429  std::set<exprt> &freely_assignable_exprs)
430 {
431  INVARIANT(
432  instruction_iterator->is_function_call(),
433  "The first argument of instrument_call_statement should always be "
434  "a function call");
435  code_function_callt call = instruction_iterator->get_function_call();
436  const irep_idt &called_name =
438 
439  // Malloc allocates memory which is not part of the caller's memory
440  // frame, so we want to capture the newly-allocated memory and
441  // treat it as assignable.
442  if(called_name == "malloc")
443  {
444  aliasable_references.push_back(call.lhs());
445 
446  // Make the variable, where result of malloc is stored, freely assignable.
447  goto_programt::instructionst::iterator local_instruction_iterator =
448  instruction_iterator;
449  local_instruction_iterator++;
450  if(
451  local_instruction_iterator->is_assign() &&
452  local_instruction_iterator->get_assign().lhs().is_not_nil())
453  {
454  freely_assignable_exprs.insert(
455  local_instruction_iterator->get_assign().lhs());
456  }
457  return; // assume malloc edits no currently-existing memory objects.
458  }
459 
460  if(call.lhs().is_not_nil())
461  {
462  exprt alias_expr =
463  create_alias_expression(assigns, call.lhs(), aliasable_references);
464 
465  goto_programt alias_assertion;
466  alias_assertion.add(goto_programt::make_assertion(
467  alias_expr, instruction_iterator->source_location));
468  program.insert_before_swap(instruction_iterator, alias_assertion);
469  ++instruction_iterator;
470  }
471 
472  // TODO we don't handle function pointers
473  if(call.function().id() == ID_symbol)
474  {
475  const symbolt &called_sym = ns.lookup(called_name);
476  const code_typet &called_type = to_code_type(called_sym.type);
477 
478  auto called_func = goto_functions.function_map.find(called_name);
479  if(called_func == goto_functions.function_map.end())
480  {
481  log.error() << "Could not find function '" << called_name
482  << "' in goto-program; not enforcing assigns clause."
483  << messaget::eom;
484  return;
485  }
486 
487  exprt called_assigns = static_cast<const exprt &>(
488  called_func->second.type.find(ID_C_spec_assigns));
489  if(called_assigns.is_nil()) // Called function has no assigns clause
490  {
491  // Fail if called function has no assigns clause.
492  log.error() << "No assigns specification found for function '"
493  << called_name
494  << "' in goto-program; not enforcing assigns clause."
495  << messaget::eom;
496 
497  // Create a false assertion, so the analysis will fail if this function
498  // is called.
499  goto_programt failing_assertion;
500  failing_assertion.add(goto_programt::make_assertion(
501  false_exprt(), instruction_iterator->source_location));
502  program.insert_before_swap(instruction_iterator, failing_assertion);
503  ++instruction_iterator;
504 
505  return;
506  }
507  else // Called function has assigns clause
508  {
510  // Replace formal parameters
511  code_function_callt::argumentst::const_iterator a_it =
512  call.arguments().begin();
513  for(code_typet::parameterst::const_iterator p_it =
514  called_type.parameters().begin();
515  p_it != called_type.parameters().end() &&
516  a_it != call.arguments().end();
517  ++p_it, ++a_it)
518  {
519  if(!p_it->get_identifier().empty())
520  {
521  symbol_exprt p(p_it->get_identifier(), p_it->type());
522  replace.insert(p, *a_it);
523  }
524  }
525 
526  replace(called_assigns);
527  for(exprt::operandst::const_iterator called_op_it =
528  called_assigns.operands().begin();
529  called_op_it != called_assigns.operands().end();
530  called_op_it++)
531  {
532  if(
533  freely_assignable_exprs.find(*called_op_it) !=
534  freely_assignable_exprs.end())
535  {
536  continue;
537  }
538  exprt alias_expr =
539  create_alias_expression(assigns, *called_op_it, aliasable_references);
540 
541  goto_programt alias_assertion;
542  alias_assertion.add(goto_programt::make_assertion(
543  alias_expr, instruction_iterator->source_location));
544  program.insert_before_swap(instruction_iterator, alias_assertion);
545  ++instruction_iterator;
546  }
547  }
548  }
549 }
550 
552 {
553  // Collect all GOTOs and mallocs
554  std::vector<goto_programt::instructiont> back_gotos;
555  std::vector<goto_programt::instructiont> malloc_calls;
556 
557  int idx = 0;
558  for(goto_programt::instructiont instruction : program.instructions)
559  {
560  if(instruction.is_backwards_goto())
561  {
562  back_gotos.push_back(instruction);
563  }
564  if(instruction.is_function_call())
565  {
566  code_function_callt call = instruction.get_function_call();
567  const irep_idt &called_name =
569 
570  if(called_name == "malloc")
571  {
572  malloc_calls.push_back(instruction);
573  }
574  }
575  idx++;
576  }
577  // Make sure there are no gotos that go back such that a malloc is between
578  // the goto and its destination (possible loop).
579  for(auto goto_entry : back_gotos)
580  {
581  for(const auto &target : goto_entry.targets)
582  {
583  for(auto malloc_entry : malloc_calls)
584  {
585  if(
586  malloc_entry.location_number >= target->location_number &&
587  malloc_entry.location_number < goto_entry.location_number)
588  {
589  // In order to statically keep track of all the memory we should
590  // be able to assign, we need to create ghost variables to store
591  // references to that memory.
592  // If a malloc is in a loop, we can't generally determine how many
593  // times it will run in order to create an appropriate number of
594  // references for the assignable memory.
595  // So, if we have a malloc in a loop, we can't statically create the
596  // assertion statements needed to enforce the assigns clause.
597  log.error() << "Call to malloc at location "
598  << malloc_entry.location_number << " falls between goto "
599  << "source location " << goto_entry.location_number
600  << " and it's destination at location "
601  << target->location_number << ". "
602  << "Unable to complete instrumentation, as this malloc "
603  << "may be in a loop." << messaget::eom;
604  throw 0;
605  }
606  }
607  }
608  }
609  return false;
610 }
611 
612 bool code_contractst::add_pointer_checks(const std::string &function_name)
613 {
614  // Get the function object before instrumentation.
615  auto old_function = goto_functions.function_map.find(function_name);
616  if(old_function == goto_functions.function_map.end())
617  {
618  log.error() << "Could not find function '" << function_name
619  << "' in goto-program; not enforcing contracts."
620  << messaget::eom;
621  return true;
622  }
623  goto_programt &program = old_function->second.body;
624  if(program.instructions.empty()) // empty function body
625  {
626  return false;
627  }
628 
629  const irep_idt function_id(function_name);
630  const symbolt &function_symbol = ns.lookup(function_id);
631  const code_typet &type = to_code_type(function_symbol.type);
632 
633  exprt assigns = static_cast<const exprt &>(type.find(ID_C_spec_assigns));
634 
635  // Return if there are no reference checks to perform.
636  if(assigns.is_nil())
637  return false;
638 
639  goto_programt::instructionst::iterator instruction_iterator =
640  program.instructions.begin();
641 
642  // Create temporary variables to hold the assigns clause targets before
643  // they can be modified.
644  goto_programt standin_decls;
645  std::vector<exprt> original_references;
647  function_symbol, function_id, standin_decls, original_references);
648 
649  // Create a list of variables that are okay to assign.
650  std::set<exprt> freely_assignable_exprs;
651  for(code_typet::parametert param : type.parameters())
652  {
653  freely_assignable_exprs.insert(param);
654  }
655 
656  int lines_to_iterate = standin_decls.instructions.size();
657  program.insert_before_swap(instruction_iterator, standin_decls);
658  std::advance(instruction_iterator, lines_to_iterate);
659 
660  if(check_for_looped_mallocs(program))
661  {
662  return true;
663  }
664 
665  // Insert aliasing assertions
666  for(; instruction_iterator != program.instructions.end();
667  ++instruction_iterator)
668  {
669  if(instruction_iterator->is_decl())
670  {
671  freely_assignable_exprs.insert(instruction_iterator->get_decl().symbol());
672  }
673  else if(instruction_iterator->is_assign())
674  {
676  instruction_iterator,
677  program,
678  assigns,
679  original_references,
680  freely_assignable_exprs);
681  }
682  else if(instruction_iterator->is_function_call())
683  {
685  instruction_iterator,
686  program,
687  assigns,
688  original_references,
689  freely_assignable_exprs);
690  }
691  }
692  return false;
693 }
694 
695 bool code_contractst::enforce_contract(const std::string &fun_to_enforce)
696 {
697  // Add statements to the source function to ensure assigns clause is
698  // respected.
699  add_pointer_checks(fun_to_enforce);
700 
701  // Rename source function
702  std::stringstream ss;
703  ss << CPROVER_PREFIX << "contracts_original_" << fun_to_enforce;
704  const irep_idt mangled(ss.str());
705  const irep_idt original(fun_to_enforce);
706 
707  auto old_function = goto_functions.function_map.find(original);
708  if(old_function == goto_functions.function_map.end())
709  {
710  log.error() << "Could not find function '" << fun_to_enforce
711  << "' in goto-program; not enforcing contracts."
712  << messaget::eom;
713  return true;
714  }
715 
716  std::swap(goto_functions.function_map[mangled], old_function->second);
717  goto_functions.function_map.erase(old_function);
718 
719  // Place a new symbol with the mangled name into the symbol table
720  source_locationt sl;
721  sl.set_file("instrumented for code contracts");
722  sl.set_line("0");
723  symbolt mangled_sym;
724  const symbolt *original_sym = symbol_table.lookup(original);
725  mangled_sym = *original_sym;
726  mangled_sym.name = mangled;
727  mangled_sym.base_name = mangled;
728  mangled_sym.location = sl;
729  const auto mangled_found = symbol_table.insert(std::move(mangled_sym));
730  INVARIANT(
731  mangled_found.second,
732  "There should be no existing function called " + ss.str() +
733  " in the symbol table because that name is a mangled name");
734 
735  // Insert wrapper function into goto_functions
736  auto nexist_old_function = goto_functions.function_map.find(original);
737  INVARIANT(
738  nexist_old_function == goto_functions.function_map.end(),
739  "There should be no function called " + fun_to_enforce +
740  " in the function map because that function should have had its"
741  " name mangled");
742 
743  auto mangled_fun = goto_functions.function_map.find(mangled);
744  INVARIANT(
745  mangled_fun != goto_functions.function_map.end(),
746  "There should be a function called " + ss.str() +
747  " in the function map because we inserted a fresh goto-program"
748  " with that mangled name");
749 
750  goto_functiont &wrapper = goto_functions.function_map[original];
751  wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers;
752  if(mangled_fun->second.type.is_not_nil())
753  wrapper.type = mangled_fun->second.type;
755  add_contract_check(original, mangled, wrapper.body);
756  return false;
757 }
758 
760  const irep_idt &wrapper_fun,
761  const irep_idt &mangled_fun,
762  goto_programt &dest)
763 {
764  PRECONDITION(!dest.instructions.empty());
765 
766  goto_functionst::function_mapt::iterator f_it =
767  goto_functions.function_map.find(mangled_fun);
769 
770  const goto_functionst::goto_functiont &gf = f_it->second;
771 
772  const exprt &assigns =
773  static_cast<const exprt &>(gf.type.find(ID_C_spec_assigns));
774  const exprt &requires =
775  static_cast<const exprt &>(gf.type.find(ID_C_spec_requires));
776  const exprt &ensures =
777  static_cast<const exprt &>(gf.type.find(ID_C_spec_ensures));
778  INVARIANT(
779  ensures.is_not_nil() || assigns.is_not_nil(),
780  "Code contract enforcement is trivial without an ensures or assigns "
781  "clause.");
782 
783  // build:
784  // if(nondet)
785  // decl ret
786  // decl parameter1 ...
787  // assume(requires) [optional]
788  // ret=function(parameter1, ...)
789  // assert(ensures)
790  // skip: ...
791 
792  // build skip so that if(nondet) can refer to it
793  goto_programt tmp_skip;
795  tmp_skip.add(goto_programt::make_skip(ensures.source_location()));
796 
797  goto_programt check;
798 
799  // if(nondet)
801  skip,
803  skip->source_location));
804 
805  // prepare function call including all declarations
806  const symbolt &function_symbol = ns.lookup(mangled_fun);
807  code_function_callt call(function_symbol.symbol_expr());
809 
810  // decl ret
811  if(gf.type.return_type()!=empty_typet())
812  {
814  gf.type.return_type(),
815  skip->source_location,
816  wrapper_fun,
817  function_symbol.mode)
818  .symbol_expr();
819  check.add(goto_programt::make_decl(r, skip->source_location));
820 
821  call.lhs()=r;
822 
823  symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
824  replace.insert(ret_val, r);
825  }
826 
827  // decl parameter1 ...
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:1201
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:301
goto_functiont::body
goto_programt body
Definition: goto_function.h:30
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:269
code_contractst::add_contract_check
void add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest)
Definition: code_contracts.cpp:759
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:366
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:424
typet
The type of an expression, extends irept.
Definition: type.h:29
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:37
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:957
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
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:53
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:82
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:920
return_value_visitort::return_value_visitort
return_value_visitort()
Definition: code_contracts.cpp:39
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:321
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:62
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
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:1024
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:998
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:1049
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
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:1183
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
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:946
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:893
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:677
local_may_alias.h
Field-insensitive, location-sensitive may-alias analysis.
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:851
code_contractst::has_contract
bool has_contract(const irep_idt)
Does the named function have a contract?
Definition: code_contracts.cpp:149
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:111
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:127
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:399
goto_programt::instructiont::is_backwards_goto
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:537
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
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:241
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:551
code_contractst::apply_contract
bool apply_contract(goto_programt &goto_program, goto_programt::targett target)
Definition: code_contracts.cpp:160
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:612
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:398
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:177
code_typet
Base type of functions.
Definition: std_types.h:736
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
code_contractst::ns
namespacet ns
Definition: code_contracts.h:83
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
natural_loops_templatet< goto_programt, goto_programt::targett >
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
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:669
source_locationt
Definition: source_location.h:20
return_value_visitort::operator()
void operator()(const exprt &exp) override
Definition: code_contracts.cpp:50
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
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:321
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
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:35
get_modifies
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:87
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:753
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
create_alias_expression
static exprt create_alias_expression(const exprt &assigns, const exprt &lhs, std::vector< exprt > &aliasable_references)
Definition: code_contracts.cpp:336
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:847
goto_functiont::parameter_identifiers
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:42
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:905
exprt::operands
operandst & operands()
Definition: expr.h:95
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:695
goto_functiont::type
code_typet type
The type of the function, indicating the return type and parameter types.
Definition: goto_function.h:34
static_lifetime_init.h
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:606
return_value_visitort::found_return_value
bool found_return_value()
Definition: code_contracts.cpp:45
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:37
message.h
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:461
return_value_visitort::found
bool found
Definition: code_contracts.cpp:59
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
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:579
code_contractst::symbol_table
symbol_tablet & symbol_table
Definition: code_contracts.h:84
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
code_contracts.h
Verify and use annotated invariants and pre/post-conditions.
validation_modet::INVARIANT
@ INVARIANT
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