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 
20 
21 #include <ansi-c/c_expr.h>
22 
24 
26 
27 #include <util/c_types.h>
28 #include <util/expr_util.h>
29 #include <util/fresh_symbol.h>
30 #include <util/mathematical_expr.h>
32 #include <util/message.h>
34 #include <util/replace_symbol.h>
35 
36 #include "assigns.h"
37 #include "memory_predicates.h"
38 
39 // Create a lexicographic less-than relation between two tuples of variables.
40 // This is used in the implementation of multidimensional decreases clauses.
42  const std::vector<symbol_exprt> &lhs,
43  const std::vector<symbol_exprt> &rhs)
44 {
45  PRECONDITION(lhs.size() == rhs.size());
46 
47  if(lhs.empty())
48  {
49  return false_exprt();
50  }
51 
52  // Store conjunctions of equalities.
53  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
54  // l2, l3>.
55  // Then this vector stores <s1 == l1, s1 == l1 && s2 == l2,
56  // s1 == l1 && s2 == l2 && s3 == l3>.
57  // In fact, the last element is unnecessary, so we do not create it.
58  exprt::operandst equality_conjunctions(lhs.size());
59  equality_conjunctions[0] = binary_relation_exprt(lhs[0], ID_equal, rhs[0]);
60  for(size_t i = 1; i < equality_conjunctions.size() - 1; i++)
61  {
62  binary_relation_exprt component_i_equality{lhs[i], ID_equal, rhs[i]};
63  equality_conjunctions[i] =
64  and_exprt(equality_conjunctions[i - 1], component_i_equality);
65  }
66 
67  // Store inequalities between the i-th components of the input vectors
68  // (i.e. lhs and rhs).
69  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
70  // l2, l3>.
71  // Then this vector stores <s1 < l1, s1 == l1 && s2 < l2, s1 == l1 &&
72  // s2 == l2 && s3 < l3>.
73  exprt::operandst lexicographic_individual_comparisons(lhs.size());
74  lexicographic_individual_comparisons[0] =
75  binary_relation_exprt(lhs[0], ID_lt, rhs[0]);
76  for(size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
77  {
78  binary_relation_exprt component_i_less_than{lhs[i], ID_lt, rhs[i]};
79  lexicographic_individual_comparisons[i] =
80  and_exprt(equality_conjunctions[i - 1], component_i_less_than);
81  }
82  return disjunction(lexicographic_individual_comparisons);
83 }
84 
86  goto_programt &program,
87  goto_programt::targett &target,
88  goto_programt &payload)
89 {
90  const auto offset = payload.instructions.size();
91  program.insert_before_swap(target, payload);
92  std::advance(target, offset);
93 }
94 
96  goto_functionst::goto_functiont &goto_function,
97  const local_may_aliast &local_may_alias,
98  goto_programt::targett loop_head,
99  const loopt &loop,
100  const irep_idt &mode)
101 {
102  PRECONDITION(!loop.empty());
103 
104  // find the last back edge
105  goto_programt::targett loop_end = loop_head;
106  for(const auto &t : loop)
107  if(
108  t->is_goto() && t->get_target() == loop_head &&
109  t->location_number > loop_end->location_number)
110  loop_end = t;
111 
112  // see whether we have an invariant and a decreases clause
113  auto invariant = static_cast<const exprt &>(
114  loop_end->get_condition().find(ID_C_spec_loop_invariant));
115  auto decreases_clause = static_cast<const exprt &>(
116  loop_end->get_condition().find(ID_C_spec_decreases));
117 
118  if(invariant.is_nil())
119  {
120  if(decreases_clause.is_nil())
121  return;
122  else
123  {
124  invariant = true_exprt();
125  log.warning()
126  << "The loop at " << loop_head->source_location.as_string()
127  << " does not have a loop invariant, but has a decreases clause. "
128  << "Hence, a default loop invariant ('true') is being used."
129  << messaget::eom;
130  }
131  }
132  else
133  {
134  // form the conjunction
135  invariant = conjunction(invariant.operands());
136  }
137 
138  // Vector representing a (possibly multidimensional) decreases clause
139  const auto &decreases_clause_exprs = decreases_clause.operands();
140 
141  // Temporary variables for storing the multidimensional decreases clause
142  // at the start of and end of a loop body
143  std::vector<symbol_exprt> old_decreases_vars;
144  std::vector<symbol_exprt> new_decreases_vars;
145 
146  // change
147  // H: loop;
148  // E: ...
149  // to
150  // initialize loop_entry variables;
151  // H: assert(invariant);
152  // havoc;
153  // assume(invariant);
154  // if(guard) goto E:
155  // old_decreases_value = decreases_clause(current_environment);
156  // loop;
157  // new_decreases_value = decreases_clause(current_environment);
158  // assert(invariant);
159  // assert(new_decreases_value < old_decreases_value);
160  // assume(false);
161  // E: ...
162 
163  // find out what can get changed in the loop
164  modifiest modifies;
165  get_modifies(local_may_alias, loop, modifies);
166 
167  // build the havocking code
168  goto_programt havoc_code;
169 
170  // process quantified variables correctly (introduce a fresh temporary)
171  // and return a copy of the invariant
172  const auto &invariant_expr = [&]() {
173  auto invariant_copy = invariant;
175  code_contractst::add_quantified_variable(invariant_copy, replace, mode);
176  replace(invariant_copy);
177  return invariant_copy;
178  };
179 
180  // Process "loop_entry" history variables
181  // Find and replace "loop_entry" expression in the "invariant" expression.
182  std::map<exprt, exprt> parameter2history;
184  invariant,
185  parameter2history,
186  loop_head->source_location,
187  mode,
188  havoc_code,
189  ID_loop_entry);
190 
191  // Create 'loop_entry' history variables
192  insert_before_swap_and_advance(goto_function.body, loop_head, havoc_code);
193 
194  // Generate: assert(invariant) just before the loop
195  // We use a block scope to create a temporary assertion,
196  // and immediately convert it to goto instructions.
197  {
198  code_assertt assertion{invariant_expr()};
199  assertion.add_source_location() = loop_head->source_location;
200  converter.goto_convert(assertion, havoc_code, mode);
201  havoc_code.instructions.back().source_location.set_comment(
202  "Check loop invariant before entry");
203  }
204 
205  // havoc the variables that may be modified
206  append_havoc_code(loop_head->source_location, modifies, havoc_code);
207 
208  // Generate: assume(invariant) just after havocing
209  // We use a block scope to create a temporary assumption,
210  // and immediately convert it to goto instructions.
211  {
212  code_assumet assumption{invariant_expr()};
213  assumption.add_source_location() = loop_head->source_location;
214  converter.goto_convert(assumption, havoc_code, mode);
215  }
216 
217  // Create fresh temporary variables that store the multidimensional
218  // decreases clause's value before and after the loop
219  for(const auto &clause : decreases_clause.operands())
220  {
221  const auto old_decreases_var =
222  new_tmp_symbol(clause.type(), loop_head->source_location, mode)
223  .symbol_expr();
224  havoc_code.add(
225  goto_programt::make_decl(old_decreases_var, loop_head->source_location));
226  old_decreases_vars.push_back(old_decreases_var);
227 
228  const auto new_decreases_var =
229  new_tmp_symbol(clause.type(), loop_head->source_location, mode)
230  .symbol_expr();
231  havoc_code.add(
232  goto_programt::make_decl(new_decreases_var, loop_head->source_location));
233  new_decreases_vars.push_back(new_decreases_var);
234  }
235 
236  // non-deterministically skip the loop if it is a do-while loop
237  if(!loop_head->is_goto())
238  {
239  havoc_code.add(goto_programt::make_goto(
240  loop_end,
242  }
243 
244  // Now havoc at the loop head.
245  // Use insert_before_swap to preserve jumps to loop head.
246  insert_before_swap_and_advance(goto_function.body, loop_head, havoc_code);
247 
248  // Generate: assignments to store the multidimensional decreases clause's
249  // value before the loop
250  if(!decreases_clause.is_nil())
251  {
252  for(size_t i = 0; i < old_decreases_vars.size(); i++)
253  {
254  code_assignt old_decreases_assignment{old_decreases_vars[i],
255  decreases_clause_exprs[i]};
256  old_decreases_assignment.add_source_location() =
257  loop_head->source_location;
258  converter.goto_convert(old_decreases_assignment, havoc_code, mode);
259  }
260 
261  goto_function.body.destructive_insert(std::next(loop_head), havoc_code);
262  }
263 
264  // Generate: assert(invariant) just after the loop exits
265  // We use a block scope to create a temporary assertion,
266  // and immediately convert it to goto instructions.
267  {
268  code_assertt assertion{invariant_expr()};
269  assertion.add_source_location() = loop_end->source_location;
270  converter.goto_convert(assertion, havoc_code, mode);
271  havoc_code.instructions.back().source_location.set_comment(
272  "Check that loop invariant is preserved");
273  }
274 
275  // Generate: assignments to store the multidimensional decreases clause's
276  // value after one iteration of the loop
277  if(!decreases_clause.is_nil())
278  {
279  for(size_t i = 0; i < new_decreases_vars.size(); i++)
280  {
281  code_assignt new_decreases_assignment{new_decreases_vars[i],
282  decreases_clause_exprs[i]};
283  new_decreases_assignment.add_source_location() =
284  loop_head->source_location;
285  converter.goto_convert(new_decreases_assignment, havoc_code, mode);
286  }
287 
288  // Generate: assertion that the multidimensional decreases clause's value
289  // after the loop is smaller than the value before the loop.
290  // Here, we use the lexicographic order.
291  code_assertt monotonic_decreasing_assertion{
292  create_lexicographic_less_than(new_decreases_vars, old_decreases_vars)};
293  monotonic_decreasing_assertion.add_source_location() =
294  loop_head->source_location;
295  converter.goto_convert(monotonic_decreasing_assertion, havoc_code, mode);
296  havoc_code.instructions.back().source_location.set_comment(
297  "Check decreases clause on loop iteration");
298 
299  // Discard the temporary variables that store decreases clause's value
300  for(size_t i = 0; i < old_decreases_vars.size(); i++)
301  {
302  havoc_code.add(goto_programt::make_dead(
303  old_decreases_vars[i], loop_head->source_location));
304  havoc_code.add(goto_programt::make_dead(
305  new_decreases_vars[i], loop_head->source_location));
306  }
307  }
308 
309  insert_before_swap_and_advance(goto_function.body, loop_end, havoc_code);
310 
311  // change the back edge into assume(false) or assume(guard)
312  loop_end->targets.clear();
313  loop_end->type = ASSUME;
314  if(loop_head->is_goto())
315  loop_end->set_condition(false_exprt());
316  else
317  loop_end->set_condition(boolean_negate(loop_end->get_condition()));
318 }
319 
321 {
322  const symbolt &function_symbol = ns.lookup(fun_name);
323  const auto &type = to_code_with_contract_type(function_symbol.type);
324  return type.has_contract();
325 }
326 
328  const exprt &expression,
330  const irep_idt &mode)
331 {
332  if(expression.id() == ID_not || expression.id() == ID_typecast)
333  {
334  // For unary connectives, recursively check for
335  // nested quantified formulae in the term
336  const auto &unary_expression = to_unary_expr(expression);
337  add_quantified_variable(unary_expression.op(), replace, mode);
338  }
339  if(expression.id() == ID_notequal || expression.id() == ID_implies)
340  {
341  // For binary connectives, recursively check for
342  // nested quantified formulae in the left and right terms
343  const auto &binary_expression = to_binary_expr(expression);
344  add_quantified_variable(binary_expression.lhs(), replace, mode);
345  add_quantified_variable(binary_expression.rhs(), replace, mode);
346  }
347  if(expression.id() == ID_if)
348  {
349  // For ternary connectives, recursively check for
350  // nested quantified formulae in all three terms
351  const auto &if_expression = to_if_expr(expression);
352  add_quantified_variable(if_expression.cond(), replace, mode);
353  add_quantified_variable(if_expression.true_case(), replace, mode);
354  add_quantified_variable(if_expression.false_case(), replace, mode);
355  }
356  if(expression.id() == ID_and || expression.id() == ID_or)
357  {
358  // For multi-ary connectives, recursively check for
359  // nested quantified formulae in all terms
360  const auto &multi_ary_expression = to_multi_ary_expr(expression);
361  for(const auto &operand : multi_ary_expression.operands())
362  {
363  add_quantified_variable(operand, replace, mode);
364  }
365  }
366  else if(expression.id() == ID_exists || expression.id() == ID_forall)
367  {
368  // When a quantifier expression is found,
369  // for each quantified variable ...
370  const auto &quantifier_expression = to_quantifier_expr(expression);
371  for(const auto &quantified_variable : quantifier_expression.variables())
372  {
373  const auto &quantified_symbol = to_symbol_expr(quantified_variable);
374 
375  // 1. create fresh symbol
376  symbolt new_symbol = get_fresh_aux_symbol(
377  quantified_symbol.type(),
378  id2string(quantified_symbol.get_identifier()),
379  "tmp",
380  quantified_symbol.source_location(),
381  mode,
382  symbol_table);
383 
384  // 2. add created fresh symbol to expression map
385  symbol_exprt q(
386  quantified_symbol.get_identifier(), quantified_symbol.type());
387  replace.insert(q, new_symbol.symbol_expr());
388 
389  // 3. recursively check for nested quantified formulae
390  add_quantified_variable(quantifier_expression.where(), replace, mode);
391  }
392  }
393 }
394 
396  exprt &expr,
397  std::map<exprt, exprt> &parameter2history,
398  source_locationt location,
399  const irep_idt &mode,
400  goto_programt &history,
401  const irep_idt &id)
402 {
403  for(auto &op : expr.operands())
404  {
406  op, parameter2history, location, mode, history, id);
407  }
408 
409  if(expr.id() == ID_old || expr.id() == ID_loop_entry)
410  {
411  const auto &parameter = to_history_expr(expr, id).expression();
412 
413  if(
414  parameter.id() == ID_dereference || parameter.id() == ID_member ||
415  parameter.id() == ID_symbol || parameter.id() == ID_ptrmember)
416  {
417  auto it = parameter2history.find(parameter);
418 
419  if(it == parameter2history.end())
420  {
421  // 1. Create a temporary symbol expression that represents the
422  // history variable
423  symbol_exprt tmp_symbol =
424  new_tmp_symbol(parameter.type(), location, mode).symbol_expr();
425 
426  // 2. Associate the above temporary variable to it's corresponding
427  // expression
428  parameter2history[parameter] = tmp_symbol;
429 
430  // 3. Add the required instructions to the instructions list
431  // 3.1 Declare the newly created temporary variable
432  history.add(goto_programt::make_decl(tmp_symbol, location));
433 
434  // 3.2 Add an assignment such that the value pointed to by the new
435  // temporary variable is equal to the value of the corresponding
436  // parameter
437  history.add(
438  goto_programt::make_assignment(tmp_symbol, parameter, location));
439  }
440 
441  expr = parameter2history[parameter];
442  }
443  else
444  {
445  log.error() << "Tracking history of " << parameter.id()
446  << " expressions is not supported yet." << messaget::eom;
447  throw 0;
448  }
449  }
450 }
451 
452 std::pair<goto_programt, goto_programt>
454  codet &expression,
455  source_locationt location,
456  const irep_idt &mode)
457 {
458  std::map<exprt, exprt> parameter2history;
459  goto_programt history;
460 
461  // Find and replace "old" expression in the "expression" variable
463  expression, parameter2history, location, mode, history, ID_old);
464 
465  // Create instructions corresponding to the ensures clause
466  goto_programt ensures_program;
467  converter.goto_convert(expression, ensures_program, mode);
468 
469  // return a pair containing:
470  // 1. instructions corresponding to the ensures clause
471  // 2. instructions related to initializing the history variables
472  return std::make_pair(std::move(ensures_program), std::move(history));
473 }
474 
476  goto_programt &goto_program,
477  goto_programt::targett target)
478 {
479  // Return if the function is not named in the call; currently we don't handle
480  // function pointers.
481  PRECONDITION(as_const(*target).call_function().id() == ID_symbol);
482 
483  // Retrieve the function type, which is needed to extract the contract
484  // components.
485  const irep_idt &function =
486  to_symbol_expr(as_const(*target).call_function()).get_identifier();
487  const symbolt &function_symbol = ns.lookup(function);
488  const auto &type = to_code_with_contract_type(function_symbol.type);
489 
490  // Isolate each component of the contract.
491  auto assigns = type.assigns();
492  auto requires = conjunction(type.requires());
493  auto ensures = conjunction(type.ensures());
494 
495  // Create a replace_symbolt object, for replacing expressions in the callee
496  // with expressions from the call site (e.g. the return value).
497  // This object tracks replacements that are common to ENSURES and REQUIRES.
498  replace_symbolt common_replace;
499  if(type.return_type() != empty_typet())
500  {
501  // Check whether the function's return value is not disregarded.
502  if(as_const(*target).call_lhs().is_not_nil())
503  {
504  // If so, have it replaced appropriately.
505  // For example, if foo() ensures that its return value is > 5, then
506  // rewrite calls to foo as follows:
507  // x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5)
508  symbol_exprt ret_val(
509  CPROVER_PREFIX "return_value", as_const(*target).call_lhs().type());
510  common_replace.insert(ret_val, as_const(*target).call_lhs());
511  }
512  else
513  {
514  // If the function does return a value, but the return value is
515  // disregarded, check if the postcondition includes the return value.
517  ensures.visit(v);
518  if(v.found_return_value())
519  {
520  // The postcondition does mention __CPROVER_return_value, so mint a
521  // fresh variable to replace __CPROVER_return_value with.
522  const symbolt &fresh = get_fresh_aux_symbol(
523  type.return_type(),
524  id2string(function),
525  "ignored_return_value",
526  target->source_location,
527  symbol_table.lookup_ref(function).mode,
528  ns,
529  symbol_table);
530  symbol_exprt ret_val(CPROVER_PREFIX "return_value", type.return_type());
531  common_replace.insert(ret_val, fresh.symbol_expr());
532  }
533  }
534  }
535 
536  // Replace formal parameters
537  const auto &arguments = target->call_arguments();
538  auto a_it = arguments.begin();
539  for(auto p_it = type.parameters().begin();
540  p_it != type.parameters().end() && a_it != arguments.end();
541  ++p_it, ++a_it)
542  {
543  if(!p_it->get_identifier().empty())
544  {
545  symbol_exprt p(p_it->get_identifier(), p_it->type());
546  common_replace.insert(p, *a_it);
547  }
548  }
549 
550  // ASSIGNS clause should not refer to any quantified variables,
551  // and only refer to the common symbols to be replaced.
552  common_replace(assigns);
553 
554  const auto &mode = symbol_table.lookup_ref(function).mode;
555 
556  is_fresh_replacet is_fresh(*this, log, function);
557  is_fresh.create_declarations();
558 
559  // Insert assertion of the precondition immediately before the call site.
560  if(!requires.is_true())
561  {
562  replace_symbolt replace(common_replace);
564  replace(requires);
565 
566  goto_programt assertion;
568  code_assertt(requires),
569  assertion,
570  symbol_table.lookup_ref(function).mode);
571  assertion.instructions.back().source_location = requires.source_location();
572  assertion.instructions.back().source_location.set_comment(
573  "Check requires clause");
574  assertion.instructions.back().source_location.set_property_class(
575  ID_precondition);
576  is_fresh.update_requires(assertion);
577  insert_before_swap_and_advance(goto_program, target, assertion);
578  }
579 
580  // Gather all the instructions required to handle history variables
581  // as well as the ensures clause
582  std::pair<goto_programt, goto_programt> ensures_pair;
583  if(!ensures.is_false())
584  {
585  replace_symbolt replace(common_replace);
587  replace(ensures);
588 
589  auto assumption = code_assumet(ensures);
590  ensures_pair = create_ensures_instruction(
591  assumption,
592  ensures.source_location(),
593  symbol_table.lookup_ref(function).mode);
594 
595  // add all the history variable initialization instructions
596  // to the goto program
597  insert_before_swap_and_advance(goto_program, target, ensures_pair.second);
598  }
599 
600  // Create a series of non-deterministic assignments to havoc the variables
601  // in the assigns clause.
602  if(assigns.is_not_nil())
603  {
604  assigns_clauset assigns_cause(assigns, *this, function, log);
605  goto_programt assigns_havoc = assigns_cause.havoc_code();
606 
607  // Insert the non-deterministic assignment immediately before the call site.
608  insert_before_swap_and_advance(goto_program, target, assigns_havoc);
609  }
610 
611  // To remove the function call, insert statements related to the assumption.
612  // Then, replace the function call with a SKIP statement.
613  if(!ensures.is_false())
614  {
615  is_fresh.update_ensures(ensures_pair.first);
616  insert_before_swap_and_advance(goto_program, target, ensures_pair.first);
617  }
618  *target = goto_programt::make_skip();
619 
620  // Add this function to the set of replaced functions.
621  summarized.insert(function);
622  return false;
623 }
624 
626  const irep_idt &function,
627  goto_functionst::goto_functiont &goto_function)
628 {
629  local_may_aliast local_may_alias(goto_function);
630  natural_loops_mutablet natural_loops(goto_function.body);
631 
632  // Iterate over the (natural) loops in the function,
633  // and apply any invariant annotations that we find.
634  for(const auto &loop : natural_loops.loop_map)
635  {
637  goto_function,
638  local_may_alias,
639  loop.first,
640  loop.second,
641  symbol_table.lookup_ref(function).mode);
642  }
643 }
644 
646  const typet &type,
647  const source_locationt &source_location,
648  const irep_idt &mode)
649 {
650  return get_fresh_aux_symbol(
651  type,
652  id2string(source_location.get_function()) + "::tmp_cc",
653  "tmp_cc",
654  source_location,
655  mode,
656  symbol_table);
657 }
658 
660 {
661  return symbol_table;
662 }
663 
665 {
666  return goto_functions;
667 }
668 
670  const exprt &lhs,
671  std::vector<exprt> &aliasable_references)
672 {
673  exprt::operandst operands;
674  operands.reserve(aliasable_references.size());
675  for(auto aliasable : aliasable_references)
676  {
677  operands.push_back(equal_exprt(lhs, typecast_exprt(aliasable, lhs.type())));
678  }
679  return disjunction(operands);
680 }
681 
683  goto_programt::instructionst::iterator &instruction_iterator,
684  goto_programt &program,
685  exprt &assigns,
686  std::set<irep_idt> &freely_assignable_symbols,
687  assigns_clauset &assigns_clause)
688 {
689  INVARIANT(
690  instruction_iterator->is_assign(),
691  "The first instruction of instrument_assign_statement should always be"
692  " an assignment");
693 
694  const exprt &lhs = instruction_iterator->assign_lhs();
695 
696  if(
697  freely_assignable_symbols.find(lhs.get(ID_identifier)) ==
698  freely_assignable_symbols.end())
699  {
700  goto_programt alias_assertion;
701  alias_assertion.add(goto_programt::make_assertion(
702  assigns_clause.alias_expression(lhs),
703  instruction_iterator->source_location));
704  alias_assertion.instructions.back().source_location.set_comment(
705  "Check that " + from_expr(ns, lhs.id(), lhs) + " is assignable");
707  program, instruction_iterator, alias_assertion);
708  }
709 }
710 
712  goto_programt::instructionst::iterator &instruction_iterator,
713  goto_programt &program,
714  exprt &assigns,
715  std::set<irep_idt> &freely_assignable_symbols,
716  assigns_clauset &assigns_clause)
717 {
718  INVARIANT(
719  instruction_iterator->is_function_call(),
720  "The first argument of instrument_call_statement should always be "
721  "a function call");
722 
723  irep_idt called_name;
724  if(instruction_iterator->call_function().id() == ID_dereference)
725  {
726  called_name =
728  to_dereference_expr(instruction_iterator->call_function()).pointer())
729  .get_identifier();
730  }
731  else
732  {
733  called_name =
734  to_symbol_expr(instruction_iterator->call_function()).get_identifier();
735  }
736 
737  if(called_name == "malloc")
738  {
739  // malloc statments return a void pointer, which is then cast and assigned
740  // to a result variable. We iterate one line forward to grab the result of
741  // the malloc once it is cast.
742  instruction_iterator++;
743  if(instruction_iterator->is_assign())
744  {
745  const exprt &rhs = instruction_iterator->assign_rhs();
746  INVARIANT(
747  rhs.id() == ID_typecast,
748  "malloc is called but the result is not cast. Excluding result from "
749  "the assignable memory frame.");
750  typet cast_type = rhs.type();
751 
752  // Make freshly allocated memory assignable, if we can determine its type.
753  assigns_clause_targett *new_target =
754  assigns_clause.add_target(dereference_exprt(rhs));
755  goto_programt &pointer_capture = new_target->get_init_block();
757  program, instruction_iterator, pointer_capture);
758  }
759  return; // assume malloc edits no pre-existing memory objects.
760  }
761 
762  if(
763  instruction_iterator->call_lhs().is_not_nil() &&
764  instruction_iterator->call_lhs().id() == ID_symbol &&
765  freely_assignable_symbols.find(
766  to_symbol_expr(instruction_iterator->call_lhs()).get_identifier()) ==
767  freely_assignable_symbols.end())
768  {
769  exprt alias_expr =
770  assigns_clause.alias_expression(instruction_iterator->call_lhs());
771 
772  goto_programt alias_assertion;
773  alias_assertion.add(goto_programt::make_assertion(
774  alias_expr, instruction_iterator->source_location));
775  alias_assertion.instructions.back().source_location.set_comment(
776  "Check that " + from_expr(ns, alias_expr.id(), alias_expr) +
777  " is assignable");
778  program.insert_before_swap(instruction_iterator, alias_assertion);
779  ++instruction_iterator;
780  }
781 
782  const symbolt &called_symbol = ns.lookup(called_name);
783  // Called symbol might be a function pointer.
784  const typet &called_symbol_type = (called_symbol.type.id() == ID_pointer)
785  ? called_symbol.type.subtype()
786  : called_symbol.type;
787  exprt called_assigns =
788  to_code_with_contract_type(called_symbol_type).assigns();
789  const code_typet &called_type = to_code_type(called_symbol_type);
790 
791  if(called_assigns.is_not_nil())
792  {
793  replace_symbolt replace_formal_params;
794  const auto &arguments = instruction_iterator->call_arguments();
795  auto a_it = arguments.begin();
796  for(auto p_it = called_type.parameters().begin();
797  p_it != called_type.parameters().end() && a_it != arguments.end();
798  ++p_it, ++a_it)
799  {
800  if(!p_it->get_identifier().empty())
801  {
802  symbol_exprt p(p_it->get_identifier(), p_it->type());
803  replace_formal_params.insert(p, *a_it);
804  }
805  }
806  replace_formal_params(called_assigns);
807 
808  // check compatibility of assigns clause with the called function
809  assigns_clauset called_assigns_clause(
810  called_assigns, *this, called_name, log);
811  exprt compatible =
812  assigns_clause.compatible_expression(called_assigns_clause);
813  goto_programt alias_assertion;
814  alias_assertion.add(goto_programt::make_assertion(
815  compatible, instruction_iterator->source_location));
816  alias_assertion.instructions.back().source_location.set_comment(
817  "Check compatibility of assigns clause with the called function");
818  program.insert_before_swap(instruction_iterator, alias_assertion);
819  ++instruction_iterator;
820  }
821 }
822 
824 {
825  // Collect all GOTOs and mallocs
826  std::vector<goto_programt::instructiont> back_gotos;
827  std::vector<goto_programt::instructiont> malloc_calls;
828 
829  int index = 0;
830  for(goto_programt::instructiont instruction : program.instructions)
831  {
832  if(instruction.is_backwards_goto())
833  {
834  back_gotos.push_back(instruction);
835  }
836  if(instruction.is_function_call())
837  {
838  irep_idt called_name;
839  if(instruction.call_function().id() == ID_dereference)
840  {
841  called_name =
843  to_dereference_expr(instruction.call_function()).pointer())
844  .get_identifier();
845  }
846  else
847  {
848  called_name =
850  }
851 
852  if(called_name == "malloc")
853  {
854  malloc_calls.push_back(instruction);
855  }
856  }
857  index++;
858  }
859  // Make sure there are no gotos that go back such that a malloc
860  // is between the goto and its destination (possible loop).
861  for(auto goto_entry : back_gotos)
862  {
863  for(const auto &target : goto_entry.targets)
864  {
865  for(auto malloc_entry : malloc_calls)
866  {
867  if(
868  malloc_entry.location_number >= target->location_number &&
869  malloc_entry.location_number < goto_entry.location_number)
870  {
871  log.error() << "Call to malloc at location "
872  << malloc_entry.location_number << " falls between goto "
873  << "source location " << goto_entry.location_number
874  << " and it's destination at location "
875  << target->location_number << ". "
876  << "Unable to complete instrumentation, as this malloc "
877  << "may be in a loop." << messaget::eom;
878  throw 0;
879  }
880  }
881  }
882  }
883  return false;
884 }
885 
887 {
888  // Get the function object before instrumentation.
889  auto old_function = goto_functions.function_map.find(function);
890  if(old_function == goto_functions.function_map.end())
891  {
892  log.error() << "Could not find function '" << function
893  << "' in goto-program; not enforcing contracts."
894  << messaget::eom;
895  return true;
896  }
897  goto_programt &program = old_function->second.body;
898  if(program.instructions.empty()) // empty function body
899  {
900  return false;
901  }
902 
903  if(check_for_looped_mallocs(program))
904  {
905  return true;
906  }
907 
908  // Insert aliasing assertions
909  check_frame_conditions(program, ns.lookup(function));
910 
911  return false;
912 }
913 
915  goto_programt &program,
916  const symbolt &target)
917 {
918  const auto &type = to_code_with_contract_type(target.type);
919  exprt assigns_expr = type.assigns();
920 
921  assigns_clauset assigns(assigns_expr, *this, target.name, log);
922 
923  // Create a list of variables that are okay to assign.
924  std::set<irep_idt> freely_assignable_symbols;
925 
926  // Create temporary variables to hold the assigns
927  // clause targets before they can be modified.
928  goto_programt standin_decls = assigns.init_block();
929  // Create dead statements for temporary variables
930  goto_programt mark_dead = assigns.dead_stmts();
931 
932  // Skip lines with temporary variable declarations
933  auto instruction_it = program.instructions.begin();
934  insert_before_swap_and_advance(program, instruction_it, standin_decls);
935 
936  for(; instruction_it != program.instructions.end(); ++instruction_it)
937  {
938  if(instruction_it->is_decl())
939  {
940  // Local variables are always freely assignable
941  freely_assignable_symbols.insert(
942  instruction_it->get_decl().symbol().get_identifier());
943 
944  assigns_clause_targett *new_target =
945  assigns.add_target(instruction_it->get_decl().symbol());
946  goto_programt &pointer_capture = new_target->get_init_block();
947 
948  for(auto in : pointer_capture.instructions)
949  {
950  program.insert_after(instruction_it, in);
951  ++instruction_it;
952  }
953  }
954  else if(instruction_it->is_assign())
955  {
957  instruction_it,
958  program,
959  assigns_expr,
960  freely_assignable_symbols,
961  assigns);
962  }
963  else if(instruction_it->is_function_call())
964  {
966  instruction_it,
967  program,
968  assigns_expr,
969  freely_assignable_symbols,
970  assigns);
971  }
972  }
973 
974  // Walk the iterator back to the last statement
975  while(!instruction_it->is_end_function())
976  {
977  --instruction_it;
978  }
979 
980  // Make sure the temporary symbols are marked dead
981  program.insert_before_swap(instruction_it, mark_dead);
982 }
983 
985 {
986  // Add statements to the source function
987  // to ensure assigns clause is respected.
989 
990  // Rename source function
991  std::stringstream ss;
992  ss << CPROVER_PREFIX << "contracts_original_" << function;
993  const irep_idt mangled(ss.str());
994  const irep_idt original(function);
995 
996  auto old_function = goto_functions.function_map.find(original);
997  if(old_function == goto_functions.function_map.end())
998  {
999  log.error() << "Could not find function '" << function
1000  << "' in goto-program; not enforcing contracts."
1001  << messaget::eom;
1002  return true;
1003  }
1004 
1005  std::swap(goto_functions.function_map[mangled], old_function->second);
1006  goto_functions.function_map.erase(old_function);
1007 
1008  // Place a new symbol with the mangled name into the symbol table
1009  source_locationt sl;
1010  sl.set_file("instrumented for code contracts");
1011  sl.set_line("0");
1012  symbolt mangled_sym;
1013  const symbolt *original_sym = symbol_table.lookup(original);
1014  mangled_sym = *original_sym;
1015  mangled_sym.name = mangled;
1016  mangled_sym.base_name = mangled;
1017  mangled_sym.location = sl;
1018  const auto mangled_found = symbol_table.insert(std::move(mangled_sym));
1019  INVARIANT(
1020  mangled_found.second,
1021  "There should be no existing function called " + ss.str() +
1022  " in the symbol table because that name is a mangled name");
1023 
1024  // Insert wrapper function into goto_functions
1025  auto nexist_old_function = goto_functions.function_map.find(original);
1026  INVARIANT(
1027  nexist_old_function == goto_functions.function_map.end(),
1028  "There should be no function called " + id2string(function) +
1029  " in the function map because that function should have had its"
1030  " name mangled");
1031 
1032  auto mangled_fun = goto_functions.function_map.find(mangled);
1033  INVARIANT(
1034  mangled_fun != goto_functions.function_map.end(),
1035  "There should be a function called " + ss.str() +
1036  " in the function map because we inserted a fresh goto-program"
1037  " with that mangled name");
1038 
1039  goto_functiont &wrapper = goto_functions.function_map[original];
1040  wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers;
1042  add_contract_check(original, mangled, wrapper.body);
1043 
1044  return false;
1045 }
1046 
1048  const irep_idt &wrapper_function,
1049  const irep_idt &mangled_function,
1050  goto_programt &dest)
1051 {
1052  PRECONDITION(!dest.instructions.empty());
1053 
1054  const symbolt &function_symbol = ns.lookup(mangled_function);
1055  const auto &code_type = to_code_with_contract_type(function_symbol.type);
1056 
1057  exprt assigns = code_type.assigns();
1058  exprt requires = conjunction(code_type.requires());
1059  exprt ensures = conjunction(code_type.ensures());
1060 
1061  // build:
1062  // if(nondet)
1063  // decl ret
1064  // decl parameter1 ...
1065  // decl history_parameter1 ... [optional]
1066  // assume(requires) [optional]
1067  // ret=function(parameter1, ...)
1068  // assert(ensures)
1069  // skip: ...
1070 
1071  // build skip so that if(nondet) can refer to it
1072  goto_programt tmp_skip;
1073  goto_programt::targett skip =
1074  tmp_skip.add(goto_programt::make_skip(ensures.source_location()));
1075 
1076  goto_programt check;
1077 
1078  // prepare function call including all declarations
1079  code_function_callt call(function_symbol.symbol_expr());
1080 
1081  // Create a replace_symbolt object, for replacing expressions in the callee
1082  // with expressions from the call site (e.g. the return value).
1083  // This object tracks replacements that are common to ENSURES and REQUIRES.
1084  replace_symbolt common_replace;
1085 
1086  // decl ret
1087  code_returnt return_stmt;
1088  if(code_type.return_type() != empty_typet())
1089  {
1091  code_type.return_type(),
1092  skip->source_location,
1093  function_symbol.mode)
1094  .symbol_expr();
1095  check.add(goto_programt::make_decl(r, skip->source_location));
1096 
1097  call.lhs() = r;
1098  return_stmt = code_returnt(r);
1099 
1100  symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
1101  common_replace.insert(ret_val, r);
1102  }
1103 
1104  // decl parameter1 ...
1105  goto_functionst::function_mapt::iterator f_it =
1106  goto_functions.function_map.find(mangled_function);
1107  PRECONDITION(f_it != goto_functions.function_map.end());
1108 
1109  const goto_functionst::goto_functiont &gf = f_it->second;
1110  for(const auto &parameter : gf.parameter_identifiers)
1111  {
1112  PRECONDITION(!parameter.empty());
1113  const symbolt &parameter_symbol = ns.lookup(parameter);
1115  parameter_symbol.type,
1116  skip->source_location,
1117  parameter_symbol.mode)
1118  .symbol_expr();
1119  check.add(goto_programt::make_decl(p, skip->source_location));
1121  p, parameter_symbol.symbol_expr(), skip->source_location));
1122 
1123  call.arguments().push_back(p);
1124 
1125  common_replace.insert(parameter_symbol.symbol_expr(), p);
1126  }
1127 
1128  is_fresh_enforcet visitor(*this, log, wrapper_function);
1129  visitor.create_declarations();
1130 
1131  // Generate: assume(requires)
1132  if(!requires.is_false())
1133  {
1134  // extend common_replace with quantified variables in REQUIRES,
1135  // and then do the replacement
1136  replace_symbolt replace(common_replace);
1138  requires, replace, function_symbol.mode);
1139  replace(requires);
1140 
1141  goto_programt assumption;
1143  code_assumet(requires), assumption, function_symbol.mode);
1144  visitor.update_requires(assumption);
1145  check.destructive_append(assumption);
1146  }
1147 
1148  // Prepare the history variables handling
1149  std::pair<goto_programt, goto_programt> ensures_pair;
1150 
1151  // Generate: copies for history variables
1152  if(!ensures.is_true())
1153  {
1154  // extend common_replace with quantified variables in ENSURES,
1155  // and then do the replacement
1156  replace_symbolt replace(common_replace);
1158  ensures, replace, function_symbol.mode);
1159  replace(ensures);
1160 
1161  // get all the relevant instructions related to history variables
1162  auto assertion = code_assertt(ensures);
1163  assertion.add_source_location() = ensures.source_location();
1164  ensures_pair = create_ensures_instruction(
1165  assertion, ensures.source_location(), function_symbol.mode);
1166  ensures_pair.first.instructions.back().source_location.set_comment(
1167  "Check ensures clause");
1168  ensures_pair.first.instructions.back().source_location.set_property_class(
1169  ID_postcondition);
1170 
1171  // add all the history variable initializations
1172  visitor.update_ensures(ensures_pair.first);
1173  check.destructive_append(ensures_pair.second);
1174  }
1175 
1176  // ret=mangled_function(parameter1, ...)
1178 
1179  // Generate: assert(ensures)
1180  if(ensures.is_not_nil())
1181  {
1182  check.destructive_append(ensures_pair.first);
1183  }
1184 
1185  if(code_type.return_type() != empty_typet())
1186  {
1187  check.add(goto_programt::make_return(return_stmt, skip->source_location));
1188  }
1189 
1190  // prepend the new code to dest
1191  check.destructive_append(tmp_skip);
1192  dest.destructive_insert(dest.instructions.begin(), check);
1193 }
1194 
1195 bool code_contractst::replace_calls(const std::set<std::string> &functions)
1196 {
1197  bool fail = false;
1198  for(const auto &function : functions)
1199  {
1200  if(!has_contract(function))
1201  {
1202  log.error() << "Function '" << function
1203  << "' does not have a contract; "
1204  "not replacing calls with contract."
1205  << messaget::eom;
1206  fail = true;
1207  }
1208  }
1209  if(fail)
1210  return true;
1211 
1212  for(auto &goto_function : goto_functions.function_map)
1213  {
1214  Forall_goto_program_instructions(ins, goto_function.second.body)
1215  {
1216  if(ins->is_function_call())
1217  {
1218  if(ins->call_function().id() != ID_symbol)
1219  continue;
1220 
1221  const irep_idt &called_function =
1222  to_symbol_expr(ins->call_function()).get_identifier();
1223  auto found = std::find(
1224  functions.begin(), functions.end(), id2string(called_function));
1225  if(found == functions.end())
1226  continue;
1227 
1228  fail |= apply_function_contract(goto_function.second.body, ins);
1229  }
1230  }
1231  }
1232 
1233  if(fail)
1234  return true;
1235 
1236  for(auto &goto_function : goto_functions.function_map)
1237  remove_skip(goto_function.second.body);
1238 
1240 
1241  return false;
1242 }
1243 
1245 {
1246  for(auto &goto_function : goto_functions.function_map)
1247  apply_loop_contract(goto_function.first, goto_function.second);
1248 }
1249 
1251 {
1252  std::set<std::string> functions;
1253  for(auto &goto_function : goto_functions.function_map)
1254  {
1255  if(has_contract(goto_function.first))
1256  functions.insert(id2string(goto_function.first));
1257  }
1258  return replace_calls(functions);
1259 }
1260 
1262 {
1263  std::set<std::string> functions;
1264  for(auto &goto_function : goto_functions.function_map)
1265  {
1266  if(has_contract(goto_function.first))
1267  functions.insert(id2string(goto_function.first));
1268  }
1269  return enforce_contracts(functions);
1270 }
1271 
1272 bool code_contractst::enforce_contracts(const std::set<std::string> &functions)
1273 {
1274  bool fail = false;
1275  for(const auto &function : functions)
1276  {
1277  auto goto_function = goto_functions.function_map.find(function);
1278  if(goto_function == goto_functions.function_map.end())
1279  {
1280  fail = true;
1281  log.error() << "Could not find function '" << function
1282  << "' in goto-program; not enforcing contracts."
1283  << messaget::eom;
1284  continue;
1285  }
1286 
1287  if(!has_contract(function))
1288  {
1289  fail = true;
1290  log.error() << "Could not find any contracts within function '"
1291  << function << "'; nothing to enforce." << messaget::eom;
1292  continue;
1293  }
1294 
1295  if(!fail)
1296  fail = enforce_contract(function);
1297  }
1298  return fail;
1299 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1260
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
goto_functiont::body
goto_programt body
Definition: goto_function.h:26
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:55
to_code_with_contract_type
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:399
is_fresh_enforcet
Definition: memory_predicates.h:56
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
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
typet::subtype
const typet & subtype() const
Definition: type.h:47
source_locationt::as_string
std::string as_string() const
Definition: source_location.h:25
conjunction
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
goto_programt::make_dead
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:985
to_history_expr
const history_exprt & to_history_expr(const exprt &expr, const irep_idt &id)
Definition: c_expr.h:219
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
typet
The type of an expression, extends irept.
Definition: type.h:28
fresh_symbol.h
Fresh auxiliary symbol creation.
code_contractst::add_contract_check
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:1047
code_contractst::check_frame_conditions
void check_frame_conditions(goto_programt &program, const symbolt &target)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
Definition: contracts.cpp:914
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
assigns_clause_targett::get_init_block
goto_programt & get_init_block()
Definition: assigns.cpp:114
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:628
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:86
replace_symbol.h
assigns_clauset::init_block
goto_programt init_block()
Definition: assigns.cpp:156
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:69
code_assertt
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:617
and_exprt
Boolean AND.
Definition: std_expr.h:1920
return_value_visitort
Predicate to be used with the exprt::visit() function.
Definition: memory_predicates.h:108
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1015
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:753
insert_before_swap_and_advance
static void insert_before_swap_and_advance(goto_programt &program, goto_programt::targett &target, goto_programt &payload)
Definition: contracts.cpp:85
assigns_clauset::alias_expression
exprt alias_expression(const exprt &lhs)
Definition: assigns.cpp:195
exprt
Base class for all expressions.
Definition: expr.h:54
code_contractst::log
messaget & log
Definition: contracts.h:140
havoc_utils.h
Utilities for building havoc code for expressions.
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
code_with_contract_typet::assigns
const exprt & assigns() const
Definition: c_types.h:347
bool_typet
The Boolean type.
Definition: std_types.h:36
messaget::eom
static eomt eom
Definition: message.h:297
goto_programt::make_return
static instructiont make_return(code_returnt c, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:901
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
code_contractst::instrument_call_statement
void instrument_call_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause)
Inserts an assertion statement into program before the function call at ins_it, to ensure that any me...
Definition: contracts.cpp:711
code_contractst::check_apply_loop_contracts
void check_apply_loop_contracts(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:95
assigns_clauset::add_target
assigns_clause_targett * add_target(exprt target)
Definition: assigns.cpp:143
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:978
equal_exprt
Equality.
Definition: std_expr.h:1225
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1238
loopt
natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
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:1082
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1056
modifiest
std::set< exprt > modifiest
Definition: havoc_utils.h:23
goto_convertt::goto_convert
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:278
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
is_fresh_baset::update_ensures
void update_ensures(goto_programt &ensures)
Definition: memory_predicates.cpp:128
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
code_contractst::instrument_assign_statement
void instrument_assign_statement(goto_programt::instructionst::iterator &instruction_it, goto_programt &program, exprt &assigns, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause)
Inserts an assertion statement into program before the assignment instruction_it, to ensure that the ...
Definition: contracts.cpp:682
mathematical_types.h
Mathematical types.
memory_predicates.h
Predicates to specify memory footprint in function contracts.
source_locationt::set_line
void set_line(const irep_idt &line)
Definition: source_location.h:105
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:1107
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:138
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1213
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
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:22
is_fresh_replacet
Definition: memory_predicates.h:71
code_contractst::converter
goto_convertt converter
Definition: contracts.h:141
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:951
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
as_const
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
messaget::error
mstreamt & error() const
Definition: message.h:399
create_lexicographic_less_than
static exprt create_lexicographic_less_than(const std::vector< symbol_exprt > &lhs, const std::vector< symbol_exprt > &rhs)
Definition: contracts.cpp:41
empty_typet
The empty type.
Definition: std_types.h:51
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:744
code_contractst::apply_loop_contracts
void apply_loop_contracts()
Definition: contracts.cpp:1244
local_may_alias.h
Field-insensitive, location-sensitive may-alias analysis.
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:909
code_contractst::has_contract
bool has_contract(const irep_idt)
Does the named function have a contract?
Definition: contracts.cpp:320
code_contractst::check_frame_conditions_function
bool check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
Definition: contracts.cpp:886
c_expr.h
API to expression classes that are internal to the C frontend.
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:109
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:641
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:125
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:565
goto_programt::instructiont::is_backwards_goto
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:604
source_locationt::set_file
void set_file(const irep_idt &file)
Definition: source_location.h:95
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
code_contractst::create_alias_expression
exprt create_alias_expression(const exprt &lhs, std::vector< exprt > &aliasable_references)
Creates a boolean expression which is true when there exists an expression in aliasable_references wi...
Definition: contracts.cpp:669
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:17
assigns_clauset
Definition: assigns.h:53
code_contractst::apply_loop_contract
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:625
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
code_typet
Base type of functions.
Definition: std_types.h:539
irept::id
const irep_idt & id() const
Definition: irep.h:407
assigns_clauset::compatible_expression
exprt compatible_expression(const assigns_clauset &called_assigns)
Definition: assigns.cpp:211
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
code_contractst::ns
namespacet ns
Definition: contracts.h:134
false_exprt
The Boolean constant false.
Definition: std_expr.h:2811
replace_symbolt::insert
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...
Definition: replace_symbol.cpp:24
code_contractst::check_for_looped_mallocs
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:823
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:655
natural_loops_templatet< goto_programt, goto_programt::targett >
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1258
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:736
source_locationt
Definition: source_location.h:19
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:27
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
expr_util.h
Deprecated expression utility functions.
contracts.h
Verify and use annotated invariants and pre/post-conditions.
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
assigns_clauset::havoc_code
goto_programt havoc_code()
Definition: assigns.cpp:184
code_contractst::enforce_contracts
bool enforce_contracts()
Call enforce_contracts() on all functions that have a contract.
Definition: contracts.cpp:1261
code_contractst::create_ensures_instruction
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:453
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1340
code_contractst::goto_functions
goto_functionst & goto_functions
Definition: contracts.h:138
to_quantifier_expr
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Definition: mathematical_expr.h:314
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
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:33
get_modifies
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:68
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
assigns.h
Specify write set in function contracts.
code_contractst::get_symbol_table
symbol_tablet & get_symbol_table()
Definition: contracts.cpp:659
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_functionst::update
void update()
Definition: goto_functions.h:83
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
code_contractst::replace_calls
bool replace_calls()
Call replace_calls() on all calls to any function that has a contract.
Definition: contracts.cpp:1250
goto_programt::insert_after
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:722
assigns_clauset::dead_stmts
goto_programt dead_stmts()
Definition: assigns.cpp:170
code_contractst::summarized
std::unordered_set< irep_idt > summarized
Definition: contracts.h:143
code_contractst::replace_history_parameter
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:395
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
goto_functiont::parameter_identifiers
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:33
exprt::operands
operandst & operands()
Definition: expr.h:92
r
static int8_t r
Definition: irep_hash.h:60
is_fresh_enforcet::create_declarations
virtual void create_declarations()
Definition: memory_predicates.cpp:245
append_havoc_code
void append_havoc_code(const source_locationt source_location, const modifiest &modifies, goto_programt &dest)
Definition: havoc_utils.cpp:73
code_contractst::apply_function_contract
bool apply_function_contract(goto_programt &goto_program, goto_programt::targett target)
Replaces function calls with assertions based on requires clauses, non-deterministic assignments for ...
Definition: contracts.cpp:475
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:235
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:673
is_fresh_replacet::create_declarations
virtual void create_declarations()
Definition: memory_predicates.cpp:315
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1866
return_value_visitort::found_return_value
bool found_return_value()
Definition: memory_predicates.cpp:24
remove_skip.h
Program Transformation.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:293
code_contractst::new_tmp_symbol
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &mode)
Definition: contracts.cpp:645
message.h
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
code_contractst::get_goto_functions
goto_functionst & get_goto_functions()
Definition: contracts.cpp:664
code_contractst::enforce_contract
bool enforce_contract(const irep_idt &function)
Enforce contract of a single function.
Definition: contracts.cpp:984
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:530
messaget::warning
mstreamt & warning() const
Definition: message.h:404
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
history_exprt::expression
const exprt & expression() const
Definition: c_expr.h:212
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:230
assigns_clause_targett
A base class for assigns clause targets.
Definition: assigns.h:23
code_contractst::add_quantified_variable
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:327
c_types.h
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
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
goto_programt::instructiont::call_function
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:361
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:646
code_contractst::symbol_table
symbol_tablet & symbol_table
Definition: contracts.h:137
loop_analysist::loop_map
loop_mapt loop_map
Definition: loop_analysis.h:88
is_fresh_baset::update_requires
void update_requires(goto_programt &requires)
Definition: memory_predicates.cpp:118
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:25
mathematical_expr.h
API to expression classes for 'mathematical' expressions.
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33