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/fresh_symbol.h>
17 #include <util/replace_symbol.h>
18 
20 
22 
24 
25 #include "loop_utils.h"
26 
28 {
29 public:
31  symbol_tablet &_symbol_table,
32  goto_functionst &_goto_functions):
33  ns(_symbol_table),
34  symbol_table(_symbol_table),
35  goto_functions(_goto_functions),
37  {
38  }
39 
40  void operator()();
41 
42 protected:
46 
48 
49  std::unordered_set<irep_idt> summarized;
50 
52 
53  void apply_contract(
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 =
136  jump->targets.push_back(loop_end);
137  jump->function=loop_head->function;
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  {
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 
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  {
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  id2string(source_location.get_function()),
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;
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(
300  g->function=skip->function;
301  g->source_location=skip->source_location;
302 
303  // prepare function call including all declarations
304  code_function_callt call;
305  call.function()=ns.lookup(function).symbol_expr();
306  replace_symbolt replace;
307 
308  // decl ret
309  if(gf.type.return_type()!=empty_typet())
310  {
312  d->function=skip->function;
313  d->source_location=skip->source_location;
314 
315  symbol_exprt r=
316  new_tmp_symbol(gf.type.return_type(),
317  d->source_location).symbol_expr();
318  d->code=code_declt(r);
319 
320  call.lhs()=r;
321 
322  replace.insert("__CPROVER_return_value", r);
323  }
324 
325  // decl parameter1 ...
326  for(code_typet::parameterst::const_iterator
327  p_it=gf.type.parameters().begin();
328  p_it!=gf.type.parameters().end();
329  ++p_it)
330  {
332  d->function=skip->function;
333  d->source_location=skip->source_location;
334 
335  symbol_exprt p=
336  new_tmp_symbol(p_it->type(),
337  d->source_location).symbol_expr();
338  d->code=code_declt(p);
339 
340  call.arguments().push_back(p);
341 
342  if(!p_it->get_identifier().empty())
343  replace.insert(p_it->get_identifier(), p);
344  }
345 
346  // assume(requires)
347  if(requires.is_not_nil())
348  {
350  a->make_assumption(requires);
351  a->function=skip->function;
352  a->source_location=requires.source_location();
353 
354  // rewrite any use of parameters
355  replace(a->guard);
356  }
357 
358  // ret=function(parameter1, ...)
360  f->make_function_call(call);
361  f->function=skip->function;
362  f->source_location=skip->source_location;
363 
364  // assert(ensures)
366  a->make_assertion(ensures);
367  a->function=skip->function;
368  a->source_location=ensures.source_location();
369 
370  // rewrite any use of __CPROVER_return_value
371  replace(a->guard);
372 
373  // assume(false)
375  af->make_assumption(false_exprt());
376  af->function=skip->function;
377  af->source_location=ensures.source_location();
378 
379  // prepend the new code to dest
380  check.destructive_append(tmp_skip);
381  dest.destructive_insert(dest.instructions.begin(), check);
382 }
383 
385 {
387  code_contracts(it->second);
388 
389  goto_functionst::function_mapt::iterator i_it=
391  assert(i_it!=goto_functions.function_map.end());
392 
393  for(const auto &contract : summarized)
394  add_contract_check(contract, i_it->second.body);
395 
396  // remove skips
397  remove_skip(i_it->second.body);
398 
400 }
401 
402 void code_contracts(goto_modelt &goto_model)
403 {
404  code_contractst(goto_model.symbol_table, goto_model.goto_functions)();
405 }
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:188
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:179
The type of an expression.
Definition: type.h:22
static int8_t r
Definition: irep_hash.h:59
Base type of functions.
Definition: std_types.h:764
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:441
goto_functionst & goto_functions
void add_contract_check(const irep_idt &function, goto_programt &dest)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:993
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, which is destroyed.
Definition: goto_program.h:486
const natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
function_mapt function_map
The proper Booleans.
Definition: std_types.h:34
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
symbol_tablet & symbol_table
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
void code_contracts(goto_functionst::goto_functiont &goto_function)
const irep_idt & id() const
Definition: irep.h:259
argumentst & arguments()
Definition: std_code.h:890
instructionst::iterator targett
Definition: goto_program.h:397
A declaration of a local variable.
Definition: std_code.h:254
code_contractst(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
The empty type.
Definition: std_types.h:54
#define INITIALIZE_FUNCTION
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
std::set< exprt > modifiest
Definition: loop_utils.h:17
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1340
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
Definition: goto_program.h:495
A function call.
Definition: std_code.h:858
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Helper functions for k-induction and loop invariants.
The boolean constant false.
Definition: std_expr.h:4497
const source_locationt & source_location() const
Definition: type.h:97
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
Verify and use annotated invariants and pre/post-conditions.
typet type
Type of symbol.
Definition: symbol.h:34
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:878
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:182
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
const parameterst & parameters() const
Definition: std_types.h:905
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:125
unsigned temporary_counter
goto_programt & goto_program
Definition: cover.cpp:63
void insert(const irep_idt &identifier, const exprt &expr)
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
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:90
void code_contracts(goto_modelt &goto_model)
dstringt irep_idt
Definition: irep.h:32
Program Transformation.
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
const typet & return_type() const
Definition: std_types.h:895
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
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:909