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  const irep_idt &function_id,
66  const irep_idt &mode);
67 };
68 
70  goto_functionst::goto_functiont &goto_function,
71  const local_may_aliast &local_may_alias,
72  const goto_programt::targett loop_head,
73  const loopt &loop)
74 {
75  assert(!loop.empty());
76 
77  // find the last back edge
78  goto_programt::targett loop_end=loop_head;
80  it=loop.begin();
81  it!=loop.end();
82  ++it)
83  if((*it)->is_goto() &&
84  (*it)->get_target()==loop_head &&
85  (*it)->location_number>loop_end->location_number)
86  loop_end=*it;
87 
88  // see whether we have an invariant
89  exprt invariant = static_cast<const exprt &>(
90  loop_end->get_condition().find(ID_C_spec_loop_invariant));
91  if(invariant.is_nil())
92  return;
93 
94  // change H: loop; E: ...
95  // to
96  // H: assert(invariant);
97  // havoc;
98  // assume(invariant);
99  // if(guard) goto E:
100  // loop;
101  // assert(invariant);
102  // assume(false);
103  // E: ...
104 
105  // find out what can get changed in the loop
106  modifiest modifies;
107  get_modifies(local_may_alias, loop, modifies);
108 
109  // build the havocking code
110  goto_programt havoc_code;
111 
112  // assert the invariant
113  {
114  goto_programt::targett a = havoc_code.add(
115  goto_programt::make_assertion(invariant, 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  havoc_code.add(
124  goto_programt::make_assumption(invariant, loop_head->source_location));
125 
126  // non-deterministically skip the loop if it is a do-while loop
127  if(!loop_head->is_goto())
128  {
129  havoc_code.add(goto_programt::make_goto(
130  loop_end,
132  }
133 
134  // Now havoc at the loop head. Use insert_swap to
135  // preserve jumps to loop head.
136  goto_function.body.insert_before_swap(loop_head, havoc_code);
137 
138  // assert the invariant at the end of the loop body
139  {
141  goto_programt::make_assertion(invariant, loop_end->source_location);
142  a.source_location.set_comment("Loop invariant not preserved");
143  goto_function.body.insert_before_swap(loop_end, a);
144  ++loop_end;
145  }
146 
147  // change the back edge into assume(false) or assume(guard)
148  loop_end->targets.clear();
149  loop_end->type=ASSUME;
150  if(loop_head->is_goto())
151  loop_end->set_condition(false_exprt());
152  else
153  loop_end->set_condition(boolean_negate(loop_end->get_condition()));
154 }
155 
157  goto_programt &goto_program,
158  goto_programt::targett target)
159 {
160  const code_function_callt &call = target->get_function_call();
161 
162  // we don't handle function pointers
163  if(call.function().id()!=ID_symbol)
164  return;
165 
166  const irep_idt &function=
168  const symbolt &f_sym=ns.lookup(function);
169  const code_typet &type=to_code_type(f_sym.type);
170 
171  exprt requires=
172  static_cast<const exprt&>(type.find(ID_C_spec_requires));
173  exprt ensures=
174  static_cast<const exprt&>(type.find(ID_C_spec_ensures));
175 
176  // is there a contract?
177  if(ensures.is_nil())
178  return;
179 
180  // replace formal parameters by arguments, replace return
182 
183  // TODO: return value could be nil
184  if(type.return_type()!=empty_typet())
185  {
186  symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
187  replace.insert(ret_val, call.lhs());
188  }
189 
190  // formal parameters
191  code_function_callt::argumentst::const_iterator a_it=
192  call.arguments().begin();
193  for(code_typet::parameterst::const_iterator
194  p_it=type.parameters().begin();
195  p_it!=type.parameters().end() &&
196  a_it!=call.arguments().end();
197  ++p_it, ++a_it)
198  if(!p_it->get_identifier().empty())
199  {
200  symbol_exprt p(p_it->get_identifier(), p_it->type());
201  replace.insert(p, *a_it);
202  }
203 
204  replace(requires);
205  replace(ensures);
206 
207  if(requires.is_not_nil())
208  {
211 
212  goto_program.insert_before_swap(target, a);
213  ++target;
214  }
215 
216  // overwrite the function call
217  *target = goto_programt::make_assumption(ensures, target->source_location);
218 
219  summarized.insert(function);
220 }
221 
223  goto_functionst::goto_functiont &goto_function)
224 {
225  local_may_aliast local_may_alias(goto_function);
226  natural_loops_mutablet natural_loops(goto_function.body);
227 
228  // iterate over the (natural) loops in the function
229  for(natural_loops_mutablet::loop_mapt::const_iterator
230  l_it=natural_loops.loop_map.begin();
231  l_it!=natural_loops.loop_map.end();
232  l_it++)
234  goto_function,
235  local_may_alias,
236  l_it->first,
237  l_it->second);
238 
239  // look at all function calls
240  Forall_goto_program_instructions(it, goto_function.body)
241  if(it->is_function_call())
242  apply_contract(goto_function.body, it);
243 }
244 
246  const typet &type,
247  const source_locationt &source_location,
248  const irep_idt &function_id,
249  const irep_idt &mode)
250 {
251  return get_fresh_aux_symbol(
252  type,
253  id2string(function_id) + "::tmp_cc",
254  "tmp_cc",
255  source_location,
256  mode,
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  tmp_skip.add(goto_programt::make_skip(ensures.source_location()));
292 
293  goto_programt check;
294 
295  // if(nondet)
297  skip,
299  skip->source_location));
300 
301  // prepare function call including all declarations
302  const symbolt &function_symbol = ns.lookup(function);
303  code_function_callt call(function_symbol.symbol_expr());
305 
306  // decl ret
307  if(gf.type.return_type()!=empty_typet())
308  {
310  gf.type.return_type(),
311  skip->source_location,
312  function,
313  function_symbol.mode)
314  .symbol_expr();
315  check.add(goto_programt::make_decl(r, skip->source_location));
316 
317  call.lhs()=r;
318 
319  symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
320  replace.insert(ret_val, r);
321  }
322 
323  // decl parameter1 ...
324  for(const auto &parameter : gf.parameter_identifiers)
325  {
326  PRECONDITION(!parameter.empty());
327  const symbolt &parameter_symbol = ns.lookup(parameter);
328 
330  parameter_symbol.type,
331  skip->source_location,
332  function,
333  parameter_symbol.mode)
334  .symbol_expr();
336 
337  call.arguments().push_back(p);
338 
339  replace.insert(parameter_symbol.symbol_expr(), p);
340  }
341 
342  // assume(requires)
343  if(requires.is_not_nil())
344  {
345  // rewrite any use of parameters
346  exprt requires_cond = requires;
347  replace(requires_cond);
348 
350  requires_cond, requires.source_location()));
351  }
352 
353  // ret=function(parameter1, ...)
355 
356  // rewrite any use of __CPROVER_return_value
357  exprt ensures_cond = ensures;
358  replace(ensures_cond);
359 
360  // assert(ensures)
361  check.add(
362  goto_programt::make_assertion(ensures_cond, ensures.source_location()));
363 
364  // assume(false)
365  check.add(
367 
368  // prepend the new code to dest
369  check.destructive_append(tmp_skip);
370  dest.destructive_insert(dest.instructions.begin(), check);
371 }
372 
374 {
376  code_contracts(it->second);
377 
378  goto_functionst::function_mapt::iterator i_it=
380  assert(i_it!=goto_functions.function_map.end());
381 
382  for(const auto &contract : summarized)
383  add_contract_check(contract, i_it->second.body);
384 
385  // remove skips
386  remove_skip(i_it->second.body);
387 
389 }
390 
391 void code_contracts(goto_modelt &goto_model)
392 {
393  code_contractst(goto_model.symbol_table, goto_model.goto_functions)();
394 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1177
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_contractst::code_contracts
void code_contracts(goto_functionst::goto_functiont &goto_function)
Definition: code_contracts.cpp:222
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:269
source_locationt::set_comment
void set_comment(const irep_idt &comment)
Definition: source_location.h:141
typet
The type of an expression, extends irept.
Definition: type.h:29
fresh_symbol.h
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:85
replace_symbol.h
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:67
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
loop_templatet::end
const_iterator end() const
Iterator over this loop's instructions.
Definition: loop_analysis.h:55
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
bool_typet
The Boolean type.
Definition: std_types.h:37
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:82
code_contractst::operator()
void operator()()
Definition: code_contracts.cpp:373
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:920
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:69
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1211
local_may_aliast
Definition: local_may_alias.h:26
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:998
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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:1049
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1186
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
loop_templatet::begin
const_iterator begin() const
Iterator over this loop's instructions.
Definition: loop_analysis.h:49
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
modifiest
std::set< exprt > modifiest
Definition: loop_utils.h:17
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
loop_templatet::const_iterator
loop_instructionst::const_iterator const_iterator
Definition: loop_analysis.h:46
empty_typet
The empty type.
Definition: std_types.h:46
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:677
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
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:851
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
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:111
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:122
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
code_contractst
Definition: code_contracts.cpp:29
loop_templatet
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
code_typet
Base type of functions.
Definition: std_types.h:736
code_contractst::add_contract_check
void add_contract_check(const irep_idt &function, goto_programt &dest)
Definition: code_contracts.cpp:260
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
code_contractst::ns
namespacet ns
Definition: code_contracts.cpp:44
false_exprt
The Boolean constant false.
Definition: std_expr.h:3993
code_contracts
void code_contracts(goto_modelt &goto_model)
Definition: code_contracts.cpp:391
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
natural_loops_templatet< goto_programt, goto_programt::targett >
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1231
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
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:669
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:1955
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
code_contractst::new_tmp_symbol
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &function_id, const irep_idt &mode)
Definition: code_contracts.cpp:245
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
expr_util.h
Deprecated expression utility functions.
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
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:33
symbolt
Symbol table entry.
Definition: symbol.h:28
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:87
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:81
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
code_contractst::summarized
std::unordered_set< irep_idt > summarized
Definition: code_contracts.cpp:50
loop_templatet::empty
bool empty() const
Returns true if this loop contains no instructions.
Definition: loop_analysis.h:67
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
code_contractst::apply_contract
void apply_contract(goto_programt &goto_program, goto_programt::targett target)
Definition: code_contracts.cpp:156
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:905
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:606
remove_skip.h
build_havoc_code
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition: loop_utils.cpp:37
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:252
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
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::targett
instructionst::iterator targett
Definition: goto_program.h:579
code_contractst::symbol_table
symbol_tablet & symbol_table
Definition: code_contracts.cpp:45
code_function_callt::function
exprt & function()
Definition: std_code.h:1221
code_contracts.h
loop_analysist::loop_map
loop_mapt loop_map
Definition: loop_analysis.h:88
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:25