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=
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 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
code_contractst::code_contracts
void code_contracts(goto_functionst::goto_functiont &goto_function)
Definition: code_contracts.cpp:231
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:57
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:187
source_locationt::set_comment
void set_comment(const irep_idt &comment)
Definition: source_location.h:137
typet
The type of an expression, extends irept.
Definition: type.h:27
fresh_symbol.h
get_fresh_aux_symbol
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
Definition: fresh_symbol.cpp:30
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
replace_symbol.h
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:65
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:352
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:24
bool_typet
The Boolean type.
Definition: std_types.h:28
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
code_contractst::operator()
void operator()()
Definition: code_contracts.cpp:394
check_apply_invariants
static void check_apply_invariants(goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, const goto_programt::targett loop_head, const loopt &loop)
Definition: code_contracts.cpp:67
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1089
local_may_aliast
Definition: local_may_alias.h:25
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
GOTO
@ GOTO
Definition: goto_program.h:34
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
modifiest
std::set< exprt > modifiest
Definition: loop_utils.h:17
empty_typet
The empty type.
Definition: std_types.h:48
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:532
local_may_alias.h
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
code_contractst::temporary_counter
unsigned temporary_counter
Definition: code_contracts.cpp:48
typet::source_location
const source_locationt & source_location() const
Definition: type.h:62
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
boolean_negate
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:127
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
code_contractst
Definition: code_contracts.cpp:28
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
code_typet
Base type of functions.
Definition: std_types.h:751
code_contractst::add_contract_check
void add_contract_check(const irep_idt &function, goto_programt &dest)
Definition: code_contracts.cpp:267
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
code_contractst::ns
namespacet ns
Definition: code_contracts.cpp:44
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
code_contracts
void code_contracts(goto_modelt &goto_model)
Definition: code_contracts.cpp:412
code_contractst::new_tmp_symbol
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location)
Definition: code_contracts.cpp:254
SKIP
@ SKIP
Definition: goto_program.h:38
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:893
natural_loops_templatet< goto_programt, goto_programt::targett >
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1109
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:144
loop_utils.h
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:524
source_locationt
Definition: source_location.h:20
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
expr_util.h
Deprecated expression utility functions.
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
code_contractst::goto_functions
goto_functionst & goto_functions
Definition: code_contracts.cpp:46
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
DECL
@ DECL
Definition: goto_program.h:47
goto_programt::instructiont::function
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:184
symbolt
Symbol table entry.
Definition: symbol.h:27
ASSUME
@ ASSUME
Definition: goto_program.h:35
get_modifies
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:89
goto_programt::instructiont::guard
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:193
code_contractst::code_contractst
code_contractst(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
Definition: code_contracts.cpp:31
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_functionst::update
void update()
Definition: goto_functions.h:91
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
code_contractst::summarized
std::unordered_set< irep_idt > summarized
Definition: code_contracts.cpp:50
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:883
code_contractst::apply_contract
void apply_contract(goto_programt &goto_program, goto_programt::targett target)
Definition: code_contracts.cpp:165
r
static int8_t r
Definition: irep_hash.h:59
static_lifetime_init.h
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:477
remove_skip.h
loopt
const typedef natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
build_havoc_code
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition: loop_utils.cpp:37
ASSERT
@ ASSERT
Definition: goto_program.h:36
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
natural_loops_templatet::loop_map
loop_mapt loop_map
Definition: natural_loops.h:54
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
code_contractst::symbol_table
symbol_tablet & symbol_table
Definition: code_contracts.cpp:45
code_function_callt::function
exprt & function()
Definition: std_code.h:1099
code_contracts.h
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:24