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/cprover_prefix.h>
17 #include <util/fresh_symbol.h>
18 #include <util/replace_symbol.h>
19 
21 
23 
24 #include "loop_utils.h"
25 
27 {
28 public:
30  symbol_tablet &_symbol_table,
31  goto_functionst &_goto_functions):
32  ns(_symbol_table),
33  symbol_table(_symbol_table),
34  goto_functions(_goto_functions),
36  {
37  }
38 
39  void operator()();
40 
41 protected:
45 
47 
48  typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
50 
52 
53  void apply_contract(
54  goto_programt &goto_program,
55  goto_programt::targett target);
56 
57  void add_contract_check(
58  const irep_idt &function,
59  goto_programt &dest);
60 
61  const symbolt &new_tmp_symbol(
62  const typet &type,
63  const source_locationt &source_location);
64 };
65 
67  goto_functionst::goto_functiont &goto_function,
68  const local_may_aliast &local_may_alias,
69  const goto_programt::targett loop_head,
70  const loopt &loop)
71 {
72  assert(!loop.empty());
73 
74  // find the last back edge
75  goto_programt::targett loop_end=loop_head;
76  for(loopt::const_iterator
77  it=loop.begin();
78  it!=loop.end();
79  ++it)
80  if((*it)->is_goto() &&
81  (*it)->get_target()==loop_head &&
82  (*it)->location_number>loop_end->location_number)
83  loop_end=*it;
84 
85  // see whether we have an invariant
86  exprt invariant=
87  static_cast<const exprt&>(
88  loop_end->guard.find(ID_C_spec_loop_invariant));
89  if(invariant.is_nil())
90  return;
91 
92  // change H: loop; E: ...
93  // to
94  // H: assert(invariant);
95  // havoc;
96  // assume(invariant);
97  // if(guard) goto E:
98  // loop;
99  // assert(invariant);
100  // assume(false);
101  // E: ...
102 
103  // find out what can get changed in the loop
104  modifiest modifies;
105  get_modifies(local_may_alias, loop, modifies);
106 
107  // build the havocking code
108  goto_programt havoc_code;
109 
110  // assert the invariant
111  {
113  a->guard=invariant;
114  a->function=loop_head->function;
115  a->source_location=loop_head->source_location;
116  a->source_location.set_comment("Loop invariant violated before entry");
117  }
118 
119  // havoc variables being written to
120  build_havoc_code(loop_head, modifies, havoc_code);
121 
122  // assume the invariant
123  {
124  goto_programt::targett assume=havoc_code.add_instruction(ASSUME);
125  assume->guard=invariant;
126  assume->function=loop_head->function;
127  assume->source_location=loop_head->source_location;
128  }
129 
130  // non-deterministically skip the loop if it is a do-while loop
131  if(!loop_head->is_goto())
132  {
134  jump->guard=side_effect_expr_nondett(bool_typet());
135  jump->targets.push_back(loop_end);
136  jump->function=loop_head->function;
137  jump->source_location=loop_head->source_location;
138  }
139 
140  // Now havoc at the loop head. Use insert_swap to
141  // preserve jumps to loop head.
142  goto_function.body.insert_before_swap(loop_head, havoc_code);
143 
144  // assert the invariant at the end of the loop body
145  {
146  goto_programt::instructiont a(ASSERT);
147  a.guard=invariant;
148  a.function=loop_end->function;
149  a.source_location=loop_end->source_location;
150  a.source_location.set_comment("Loop invariant not preserved");
151  goto_function.body.insert_before_swap(loop_end, a);
152  ++loop_end;
153  }
154 
155  // change the back edge into assume(false) or assume(guard)
156  loop_end->targets.clear();
157  loop_end->type=ASSUME;
158  if(loop_head->is_goto())
159  loop_end->guard.make_false();
160  else
161  loop_end->guard.make_not();
162 }
163 
165  goto_programt &goto_program,
166  goto_programt::targett target)
167 {
168  const code_function_callt &call=to_code_function_call(target->code);
169  // we don't handle function pointers
170  if(call.function().id()!=ID_symbol)
171  return;
172 
173  const irep_idt &function=
174  to_symbol_expr(call.function()).get_identifier();
175  const symbolt &f_sym=ns.lookup(function);
176  const code_typet &type=to_code_type(f_sym.type);
177 
178  exprt requires=
179  static_cast<const exprt&>(type.find(ID_C_spec_requires));
180  exprt ensures=
181  static_cast<const exprt&>(type.find(ID_C_spec_ensures));
182 
183  // is there a contract?
184  if(ensures.is_nil())
185  return;
186 
187  // replace formal parameters by arguments, replace return
188  replace_symbolt replace;
189 
190  // TODO: return value could be nil
191  if(type.return_type()!=empty_typet())
192  replace.insert("__CPROVER_return_value", call.lhs());
193 
194  // formal parameters
195  code_function_callt::argumentst::const_iterator a_it=
196  call.arguments().begin();
197  for(code_typet::parameterst::const_iterator
198  p_it=type.parameters().begin();
199  p_it!=type.parameters().end() &&
200  a_it!=call.arguments().end();
201  ++p_it, ++a_it)
202  if(!p_it->get_identifier().empty())
203  replace.insert(p_it->get_identifier(), *a_it);
204 
205  replace(requires);
206  replace(ensures);
207 
208  if(requires.is_not_nil())
209  {
210  goto_programt::instructiont a(ASSERT);
211  a.guard=requires;
212  a.function=target->function;
213  a.source_location=target->source_location;
214 
215  goto_program.insert_before_swap(target, a);
216  ++target;
217  }
218 
219  target->make_assumption(ensures);
220 
221  summarized.insert(function);
222 }
223 
225  goto_functionst::goto_functiont &goto_function)
226 {
227  local_may_aliast local_may_alias(goto_function);
228  natural_loops_mutablet natural_loops(goto_function.body);
229 
230  // iterate over the (natural) loops in the function
231  for(natural_loops_mutablet::loop_mapt::const_iterator
232  l_it=natural_loops.loop_map.begin();
233  l_it!=natural_loops.loop_map.end();
234  l_it++)
236  goto_function,
237  local_may_alias,
238  l_it->first,
239  l_it->second);
240 
241  // look at all function calls
242  Forall_goto_program_instructions(it, goto_function.body)
243  if(it->is_function_call())
244  apply_contract(goto_function.body, it);
245 }
246 
248  const typet &type,
249  const source_locationt &source_location)
250 {
251  return get_fresh_aux_symbol(
252  type,
253  "",
254  "tmp_cc",
255  source_location,
256  irep_idt(),
257  symbol_table);
258 }
259 
261  const irep_idt &function,
262  goto_programt &dest)
263 {
264  assert(!dest.instructions.empty());
265 
266  goto_functionst::function_mapt::iterator f_it=
267  goto_functions.function_map.find(function);
268  assert(f_it!=goto_functions.function_map.end());
269 
270  const goto_functionst::goto_functiont &gf=f_it->second;
271 
272  const exprt &requires=
273  static_cast<const exprt&>(gf.type.find(ID_C_spec_requires));
274  const exprt &ensures=
275  static_cast<const exprt&>(gf.type.find(ID_C_spec_ensures));
276  assert(ensures.is_not_nil());
277 
278  // build:
279  // if(nondet)
280  // decl ret
281  // decl parameter1 ...
282  // assume(requires) [optional]
283  // ret=function(parameter1, ...)
284  // assert(ensures)
285  // assume(false)
286  // skip: ...
287 
288  // build skip so that if(nondet) can refer to it
289  goto_programt tmp_skip;
290  goto_programt::targett skip=tmp_skip.add_instruction(SKIP);
291  skip->function=dest.instructions.front().function;
292  skip->source_location=ensures.source_location();
293 
294  goto_programt check;
295 
296  // if(nondet)
298  g->make_goto(skip, side_effect_expr_nondett(bool_typet()));
299  g->function=skip->function;
300  g->source_location=skip->source_location;
301 
302  // prepare function call including all declarations
303  code_function_callt call;
304  call.function()=ns.lookup(function).symbol_expr();
305  replace_symbolt replace;
306 
307  // decl ret
308  if(gf.type.return_type()!=empty_typet())
309  {
311  d->function=skip->function;
312  d->source_location=skip->source_location;
313 
314  symbol_exprt r=
315  new_tmp_symbol(gf.type.return_type(),
316  d->source_location).symbol_expr();
317  d->code=code_declt(r);
318 
319  call.lhs()=r;
320 
321  replace.insert("__CPROVER_return_value", r);
322  }
323 
324  // decl parameter1 ...
325  for(code_typet::parameterst::const_iterator
326  p_it=gf.type.parameters().begin();
327  p_it!=gf.type.parameters().end();
328  ++p_it)
329  {
331  d->function=skip->function;
332  d->source_location=skip->source_location;
333 
334  symbol_exprt p=
335  new_tmp_symbol(p_it->type(),
336  d->source_location).symbol_expr();
337  d->code=code_declt(p);
338 
339  call.arguments().push_back(p);
340 
341  if(!p_it->get_identifier().empty())
342  replace.insert(p_it->get_identifier(), p);
343  }
344 
345  // assume(requires)
346  if(requires.is_not_nil())
347  {
349  a->make_assumption(requires);
350  a->function=skip->function;
351  a->source_location=requires.source_location();
352 
353  // rewrite any use of parameters
354  replace(a->guard);
355  }
356 
357  // ret=function(parameter1, ...)
359  f->make_function_call(call);
360  f->function=skip->function;
361  f->source_location=skip->source_location;
362 
363  // assert(ensures)
365  a->make_assertion(ensures);
366  a->function=skip->function;
367  a->source_location=ensures.source_location();
368 
369  // rewrite any use of __CPROVER_return_value
370  replace(a->guard);
371 
372  // assume(false)
374  af->make_assumption(false_exprt());
375  af->function=skip->function;
376  af->source_location=ensures.source_location();
377 
378  // prepend the new code to dest
379  check.destructive_append(tmp_skip);
380  dest.destructive_insert(dest.instructions.begin(), check);
381 }
382 
384 {
386  code_contracts(it->second);
387 
388  goto_functionst::function_mapt::iterator i_it=
389  goto_functions.function_map.find(CPROVER_PREFIX "initialize");
390  assert(i_it!=goto_functions.function_map.end());
391 
392  for(id_sett::const_iterator it=summarized.begin();
393  it!=summarized.end();
394  ++it)
395  add_contract_check(*it, i_it->second.body);
396 
397  // remove skips
398  remove_skip(i_it->second.body);
399 
401 }
402 
404  symbol_tablet &symbol_table,
405  goto_functionst &goto_functions)
406 {
407  code_contractst(symbol_table, goto_functions)();
408 }
The type of an expression.
Definition: type.h:20
std::unordered_set< irep_idt, irep_id_hash > id_sett
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
static int8_t r
Definition: irep_hash.h:59
targett add_instruction()
Adds an instruction at the end.
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
bool is_not_nil() const
Definition: irep.h:104
goto_functionst & goto_functions
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_tablet &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
#define CPROVER_PREFIX
void add_contract_check(const irep_idt &function, goto_programt &dest)
instructionst instructions
The list of instructions in the goto program.
void set_comment(const irep_idt &comment)
Fresh auxiliary symbol creation.
void apply_contract(goto_programt &goto_program, goto_programt::targett target)
const natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
void code_contracts(symbol_tablet &symbol_table, goto_functionst &goto_functions)
The proper Booleans.
Definition: std_types.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
symbol_tablet & symbol_table
void code_contracts(goto_functionst::goto_functiont &goto_function)
const irep_idt & id() const
Definition: irep.h:189
argumentst & arguments()
Definition: std_code.h:689
A declaration of a local variable.
Definition: std_code.h:192
code_contractst(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
The empty type.
Definition: std_types.h:53
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::set< exprt > modifiest
Definition: loop_utils.h:17
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1037
A function call.
Definition: std_code.h:657
goto_function_templatet< goto_programt > goto_functiont
Helper functions for k-induction and loop invariants.
The boolean constant false.
Definition: std_expr.h:3753
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
Verify and use annotated invariants and pre/post-conditions.
typet type
Type of symbol.
Definition: symbol.h:37
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
Definition: remove_skip.cpp:71
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:88
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:142
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
unsigned temporary_counter
void insert(const irep_idt &identifier, const exprt &expr)
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition: loop_utils.cpp:37
void destructive_insert(const_targett target, goto_program_templatet< codeT, guardT > &p)
Inserts the given program at the given location.
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
dstringt irep_idt
Definition: irep.h:32
Program Transformation.
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const typet & return_type() const
Definition: std_types.h:831
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:700