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 "code_contracts.h"
15 
16 #include <util/expr_util.h>
17 #include <util/fresh_symbol.h>
18 #include <util/replace_symbol.h>
19 
21 
23 
25 
26 #include "loop_utils.h"
27 
29 {
30 public:
32  symbol_tablet &_symbol_table,
33  goto_functionst &_goto_functions):
34  ns(_symbol_table),
35  symbol_table(_symbol_table),
36  goto_functions(_goto_functions),
38  {
39  }
40 
41  void operator()();
42 
43 protected:
47 
49 
50  std::unordered_set<irep_idt> summarized;
51 
53 
54  void apply_contract(
55  goto_programt &goto_program,
56  goto_programt::targett target);
57 
58  void add_contract_check(
59  const irep_idt &function,
60  goto_programt &dest);
61 
62  const symbolt &new_tmp_symbol(
63  const typet &type,
64  const source_locationt &source_location);
65 };
66 
68  goto_functionst::goto_functiont &goto_function,
69  const local_may_aliast &local_may_alias,
70  const goto_programt::targett loop_head,
71  const loopt &loop)
72 {
73  assert(!loop.empty());
74 
75  // find the last back edge
76  goto_programt::targett loop_end=loop_head;
77  for(loopt::const_iterator
78  it=loop.begin();
79  it!=loop.end();
80  ++it)
81  if((*it)->is_goto() &&
82  (*it)->get_target()==loop_head &&
83  (*it)->location_number>loop_end->location_number)
84  loop_end=*it;
85 
86  // see whether we have an invariant
87  exprt invariant=
88  static_cast<const exprt&>(
89  loop_end->guard.find(ID_C_spec_loop_invariant));
90  if(invariant.is_nil())
91  return;
92 
93  // change H: loop; E: ...
94  // to
95  // H: assert(invariant);
96  // havoc;
97  // assume(invariant);
98  // if(guard) goto E:
99  // loop;
100  // assert(invariant);
101  // assume(false);
102  // E: ...
103 
104  // find out what can get changed in the loop
105  modifiest modifies;
106  get_modifies(local_may_alias, loop, modifies);
107 
108  // build the havocking code
109  goto_programt havoc_code;
110 
111  // assert the invariant
112  {
114  a->guard=invariant;
115  a->function=loop_head->function;
116  a->source_location=loop_head->source_location;
117  a->source_location.set_comment("Loop invariant violated before entry");
118  }
119 
120  // havoc variables being written to
121  build_havoc_code(loop_head, modifies, havoc_code);
122 
123  // assume the invariant
124  {
125  goto_programt::targett assume=havoc_code.add_instruction(ASSUME);
126  assume->guard=invariant;
127  assume->function=loop_head->function;
128  assume->source_location=loop_head->source_location;
129  }
130 
131  // non-deterministically skip the loop if it is a do-while loop
132  if(!loop_head->is_goto())
133  {
135  jump->guard =
137  jump->targets.push_back(loop_end);
138  jump->function=loop_head->function;
139  }
140 
141  // Now havoc at the loop head. Use insert_swap to
142  // preserve jumps to loop head.
143  goto_function.body.insert_before_swap(loop_head, havoc_code);
144 
145  // assert the invariant at the end of the loop body
146  {
148  a.guard=invariant;
149  a.function=loop_end->function;
150  a.source_location=loop_end->source_location;
151  a.source_location.set_comment("Loop invariant not preserved");
152  goto_function.body.insert_before_swap(loop_end, a);
153  ++loop_end;
154  }
155 
156  // change the back edge into assume(false) or assume(guard)
157  loop_end->targets.clear();
158  loop_end->type=ASSUME;
159  if(loop_head->is_goto())
160  loop_end->guard = false_exprt();
161  else
162  loop_end->guard = boolean_negate(loop_end->guard);
163 }
164 
166  goto_programt &goto_program,
167  goto_programt::targett target)
168 {
169  const code_function_callt &call=to_code_function_call(target->code);
170  // we don't handle function pointers
171  if(call.function().id()!=ID_symbol)
172  return;
173 
174  const irep_idt &function=
175  to_symbol_expr(call.function()).get_identifier();
176  const symbolt &f_sym=ns.lookup(function);
177  const code_typet &type=to_code_type(f_sym.type);
178 
179  exprt requires=
180  static_cast<const exprt&>(type.find(ID_C_spec_requires));
181  exprt ensures=
182  static_cast<const exprt&>(type.find(ID_C_spec_ensures));
183 
184  // is there a contract?
185  if(ensures.is_nil())
186  return;
187 
188  // replace formal parameters by arguments, replace return
190 
191  // TODO: return value could be nil
192  if(type.return_type()!=empty_typet())
193  {
194  symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
195  replace.insert(ret_val, call.lhs());
196  }
197 
198  // formal parameters
199  code_function_callt::argumentst::const_iterator a_it=
200  call.arguments().begin();
201  for(code_typet::parameterst::const_iterator
202  p_it=type.parameters().begin();
203  p_it!=type.parameters().end() &&
204  a_it!=call.arguments().end();
205  ++p_it, ++a_it)
206  if(!p_it->get_identifier().empty())
207  {
208  symbol_exprt p(p_it->get_identifier(), p_it->type());
209  replace.insert(p, *a_it);
210  }
211 
212  replace(requires);
213  replace(ensures);
214 
215  if(requires.is_not_nil())
216  {
218  a.guard=requires;
219  a.function=target->function;
220  a.source_location=target->source_location;
221 
222  goto_program.insert_before_swap(target, a);
223  ++target;
224  }
225 
226  target->make_assumption(ensures);
227 
228  summarized.insert(function);
229 }
230 
232  goto_functionst::goto_functiont &goto_function)
233 {
234  local_may_aliast local_may_alias(goto_function);
235  natural_loops_mutablet natural_loops(goto_function.body);
236 
237  // iterate over the (natural) loops in the function
238  for(natural_loops_mutablet::loop_mapt::const_iterator
239  l_it=natural_loops.loop_map.begin();
240  l_it!=natural_loops.loop_map.end();
241  l_it++)
243  goto_function,
244  local_may_alias,
245  l_it->first,
246  l_it->second);
247 
248  // look at all function calls
249  Forall_goto_program_instructions(it, goto_function.body)
250  if(it->is_function_call())
251  apply_contract(goto_function.body, it);
252 }
253 
255  const typet &type,
256  const source_locationt &source_location)
257 {
258  return get_fresh_aux_symbol(
259  type,
260  id2string(source_location.get_function()),
261  "tmp_cc",
262  source_location,
263  irep_idt(),
264  symbol_table);
265 }
266 
268  const irep_idt &function,
269  goto_programt &dest)
270 {
271  assert(!dest.instructions.empty());
272 
273  goto_functionst::function_mapt::iterator f_it=
274  goto_functions.function_map.find(function);
275  assert(f_it!=goto_functions.function_map.end());
276 
277  const goto_functionst::goto_functiont &gf=f_it->second;
278 
279  const exprt &requires=
280  static_cast<const exprt&>(gf.type.find(ID_C_spec_requires));
281  const exprt &ensures=
282  static_cast<const exprt&>(gf.type.find(ID_C_spec_ensures));
283  assert(ensures.is_not_nil());
284 
285  // build:
286  // if(nondet)
287  // decl ret
288  // decl parameter1 ...
289  // assume(requires) [optional]
290  // ret=function(parameter1, ...)
291  // assert(ensures)
292  // assume(false)
293  // skip: ...
294 
295  // build skip so that if(nondet) can refer to it
296  goto_programt tmp_skip;
298  skip->function=dest.instructions.front().function;
299  skip->source_location=ensures.source_location();
300 
301  goto_programt check;
302 
303  // if(nondet)
305  g->make_goto(
307  g->function=skip->function;
308  g->source_location=skip->source_location;
309 
310  // prepare function call including all declarations
311  code_function_callt call(ns.lookup(function).symbol_expr());
313 
314  // decl ret
315  if(gf.type.return_type()!=empty_typet())
316  {
318  d->function=skip->function;
319  d->source_location=skip->source_location;
320 
321  symbol_exprt r=
322  new_tmp_symbol(gf.type.return_type(),
323  d->source_location).symbol_expr();
324  d->code=code_declt(r);
325 
326  call.lhs()=r;
327 
328  symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
329  replace.insert(ret_val, r);
330  }
331 
332  // decl parameter1 ...
333  for(code_typet::parameterst::const_iterator
334  p_it=gf.type.parameters().begin();
335  p_it!=gf.type.parameters().end();
336  ++p_it)
337  {
339  d->function=skip->function;
340  d->source_location=skip->source_location;
341 
342  symbol_exprt p=
343  new_tmp_symbol(p_it->type(),
344  d->source_location).symbol_expr();
345  d->code=code_declt(p);
346 
347  call.arguments().push_back(p);
348 
349  if(!p_it->get_identifier().empty())
350  {
351  symbol_exprt cur_p(p_it->get_identifier(), p_it->type());
352  replace.insert(cur_p, p);
353  }
354  }
355 
356  // assume(requires)
357  if(requires.is_not_nil())
358  {
360  a->make_assumption(requires);
361  a->function=skip->function;
362  a->source_location=requires.source_location();
363 
364  // rewrite any use of parameters
365  replace(a->guard);
366  }
367 
368  // ret=function(parameter1, ...)
370  f->make_function_call(call);
371  f->function=skip->function;
372  f->source_location=skip->source_location;
373 
374  // assert(ensures)
376  a->make_assertion(ensures);
377  a->function=skip->function;
378  a->source_location=ensures.source_location();
379 
380  // rewrite any use of __CPROVER_return_value
381  replace(a->guard);
382 
383  // assume(false)
385  af->make_assumption(false_exprt());
386  af->function=skip->function;
387  af->source_location=ensures.source_location();
388 
389  // prepend the new code to dest
390  check.destructive_append(tmp_skip);
391  dest.destructive_insert(dest.instructions.begin(), check);
392 }
393 
395 {
397  code_contracts(it->second);
398 
399  goto_functionst::function_mapt::iterator i_it=
401  assert(i_it!=goto_functions.function_map.end());
402 
403  for(const auto &contract : summarized)
404  add_contract_check(contract, i_it->second.body);
405 
406  // remove skips
407  remove_skip(i_it->second.body);
408 
410 }
411 
412 void code_contracts(goto_modelt &goto_model)
413 {
414  code_contractst(goto_model.symbol_table, goto_model.goto_functions)();
415 }
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:193
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:184
The type of an expression, extends irept.
Definition: type.h:27
static int8_t r
Definition: irep_hash.h:59
Base type of functions.
Definition: std_types.h:751
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:477
goto_functionst & goto_functions
#define CPROVER_PREFIX
void add_contract_check(const irep_idt &function, goto_programt &dest)
Deprecated expression utility functions.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
void set_comment(const irep_idt &comment)
const irep_idt & get_function() const
std::unordered_set< irep_idt > summarized
Fresh auxiliary symbol creation.
void apply_contract(goto_programt &goto_program, goto_programt::targett target)
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:524
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
const natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
function_mapt function_map
typet & type()
Return the type of the expression.
Definition: expr.h:68
The Boolean type.
Definition: std_types.h:28
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.
Definition: symbol.h:27
symbol_tablet & symbol_table
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
void code_contracts(goto_functionst::goto_functiont &goto_function)
const irep_idt & id() const
Definition: irep.h:259
argumentst & arguments()
Definition: std_code.h:1109
instructionst::iterator targett
Definition: goto_program.h:414
Replace expression or type symbols by an expression or type, respectively.
A codet representing the declaration of a local variable.
Definition: std_code.h:352
code_contractst(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
The empty type.
Definition: std_types.h:48
#define INITIALIZE_FUNCTION
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
The symbol table.
Definition: symbol_table.h:19
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
::goto_functiont goto_functiont
std::set< exprt > modifiest
Definition: loop_utils.h:17
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:532
codet representation of a function call statement.
Definition: std_code.h:1036
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
Helper functions for k-induction and loop invariants.
The Boolean constant false.
Definition: std_expr.h:4452
const source_locationt & source_location() const
Definition: type.h:62
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
Verify and use annotated invariants and pre/post-conditions.
typet type
Type of symbol.
Definition: symbol.h:31
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:89
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, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
exprt & function()
Definition: std_code.h:1099
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:187
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
Base class for all expressions.
Definition: expr.h:54
const parameterst & parameters() const
Definition: std_types.h:893
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:228
unsigned temporary_counter
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition: loop_utils.cpp:37
Expression to hold a symbol (variable)
Definition: std_expr.h:143
void code_contracts(goto_modelt &goto_model)
dstringt irep_idt
Definition: irep.h:32
Program Transformation.
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
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
const typet & return_type() const
Definition: std_types.h:883
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location)
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)
Field-insensitive, location-sensitive may-alias analysis.
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173