cprover
Loading...
Searching...
No Matches
instrument_contracts.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Instrument Contracts
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
13
14#include <util/c_types.h>
17#include <util/prefix.h>
18#include <util/replace_symbol.h>
19#include <util/std_code.h>
20
22
23#include <ansi-c/expr2c.h>
24
25#define MAX_TEXT 20
26
28get_contract(const irep_idt &function_identifier, const namespacet &ns)
29{
30 // contracts are in a separate symbol, with prefix "contract::"
31 auto contract_identifier = "contract::" + id2string(function_identifier);
32 const symbolt *symbol_ptr;
34 return {}; // symbol not found
35 else
37}
38
39bool has_contract(const irep_idt &function_identifier, const namespacet &ns)
40{
41 return get_contract(function_identifier, ns).has_value();
42}
43
44static std::string expr2text(const exprt &src, const namespacet &ns)
45{
46 auto text = expr2c(src, ns);
47 if(text.size() >= MAX_TEXT)
48 return std::string(text, 0, MAX_TEXT - 3) + "...";
49 else
50 return text;
51}
52
54{
55 if(src.id() == ID_dereference)
56 {
57 return to_dereference_expr(src).pointer();
58 }
59 else
60 return address_of_exprt(src);
61}
62
63// add the function to the source location
65add_function(irep_idt function_identifier, source_locationt src)
66{
67 if(!src.get_file().empty())
68 src.set_function(function_identifier);
69
70 return src;
71}
72
73// add the function to the source location
74exprt add_function(irep_idt function_identifier, exprt src)
75{
76 for(auto &op : src.operands())
77 op = add_function(function_identifier, op);
78
79 if(!src.source_location().get_file().empty())
80 src.add_source_location().set_function(function_identifier);
81
82 return src;
83}
84
86 exprt src,
87 const source_locationt &source_location)
88{
89 for(auto &op : src.operands())
90 op = replace_source_location(op, source_location);
91
92 src.add_source_location() = source_location;
93
94 return src;
95}
96
97static bool is_symbol_member(const exprt &expr)
98{
99 if(expr.id() == ID_symbol)
100 return true;
101 else if(expr.id() == ID_member)
102 return is_symbol_member(to_member_expr(expr).struct_op());
103 else
104 return false;
105}
106
107exprt assigns_match(const exprt &assigns, const exprt &lhs)
108{
109 if(is_symbol_member(lhs) && assigns == lhs)
110 return true_exprt(); // trivial match
111
112 if(lhs.id() == ID_member)
113 {
114 if(assigns_match(assigns, to_member_expr(lhs).struct_op()).is_true())
115 return true_exprt();
116 }
117 else if(lhs.id() == ID_index)
118 {
119 if(assigns_match(assigns, to_index_expr(lhs).array()).is_true())
120 return true_exprt();
121 }
122
123 auto assigns_address = make_address(assigns);
124 auto lhs_address = make_address(lhs);
125
126 if(lhs.type() == assigns.type())
127 {
129 }
130 else
131 {
132 // need to compare offset ranges
134 return same_object;
135 }
136}
137
139{
140 return src.id() == ID_lambda ? to_lambda_expr(src).where() : src;
141}
142
144 irep_idt function_identifier,
145 const exprt::operandst &assigns,
146 const exprt &lhs)
147{
149
150 for(auto &assigns_clause : assigns)
151 {
153
155 {
156 auto &condition = to_binary_expr(a).op0();
157 auto &targets = to_multi_ary_expr(to_binary_expr(a).op1());
158 for(auto &target : targets.operands())
159 {
160 auto target_address = make_address(target);
161 auto lhs_address = make_address(lhs);
164 disjuncts.push_back(
166 }
167 }
168 else
169 {
170 auto match = assigns_match(a, lhs);
171
172 // trivial?
173 if(match.is_true())
174 return true_exprt();
175
176 disjuncts.push_back(std::move(match));
177 }
178 }
179
180 return disjunction(disjuncts);
181}
182
183static bool
184is_procedure_local(const irep_idt &function_identifier, const exprt &lhs)
185{
186 if(lhs.id() == ID_member)
187 return is_procedure_local(
188 function_identifier, to_member_expr(lhs).struct_op());
189 else if(lhs.id() == ID_index)
190 return is_procedure_local(function_identifier, to_index_expr(lhs).array());
191 else if(lhs.id() == ID_symbol)
192 {
193 const auto &symbol_expr = to_symbol_expr(lhs);
194 return has_prefix(
195 id2string(symbol_expr.get_identifier()),
196 id2string(function_identifier) + "::");
197 }
198 else
199 return false;
200}
201
202static bool is_old(const exprt &lhs)
203{
204 if(lhs.id() == ID_symbol)
205 {
206 const auto &symbol_expr = to_symbol_expr(lhs);
207 return has_prefix(id2string(symbol_expr.get_identifier()), "old::");
208 }
209 else
210 return false;
211}
212
214 const exprt &src,
215 const std::string &prefix,
216 std::vector<std::pair<symbol_exprt, exprt>> &old_exprs)
217{
218 for(std::size_t i = 0; i < old_exprs.size(); i++)
219 {
220 if(old_exprs[i].second == src)
221 return old_exprs[i].first;
222 }
223
224 auto index = old_exprs.size();
225 irep_idt identifier = prefix + std::to_string(index);
226 old_exprs.emplace_back(symbol_exprt(identifier, src.type()), src);
227
228 return old_exprs.back().first;
229}
230
232 exprt src,
233 const std::string &prefix,
234 std::vector<std::pair<symbol_exprt, exprt>> &old_exprs)
235{
236 if(src.id() == ID_old)
237 {
238 const auto &old_expr = to_unary_expr(src);
239 return find_old_expr(old_expr.op(), prefix, old_exprs);
240 }
241 else
242 {
243 // rec. call
244 for(auto &op : src.operands())
245 op = replace_old(op, prefix, old_exprs);
246 return src;
247 }
248}
249
251 const std::vector<std::pair<symbol_exprt, exprt>> &old_exprs,
252 const source_locationt &source_location)
253{
254 goto_programt dest;
255
256 for(const auto &old_expr : old_exprs)
257 {
258 auto lhs = old_expr.first;
259 auto fixed_rhs = replace_source_location(old_expr.second, source_location);
261 goto_programt::make_assignment(lhs, fixed_rhs, source_location);
262 dest.add(std::move(assignment_instruction));
263 }
264
265 return dest;
266}
267
269 goto_functionst::function_mapt::value_type &f,
270 const namespacet &ns)
271{
272 // contracts are in a separate symbol, with prefix "contract::"
273 auto contract_identifier = "contract::" + id2string(f.first);
274 const symbolt *symbol_ptr;
276 return; // nothing to check
277
279
280 auto &body = f.second.body;
281
282 if(body.instructions.empty())
283 return; // nothing to check
284
285 // new instructions to add at the beginning of the function
287
288 // precondition?
289 if(!contract.c_requires().empty())
290 {
291 // stick these in as assumptions, preserving the ordering
292 goto_programt dest;
293 for(auto &assumption : contract.c_requires())
294 {
298 fixed_assumption, fixed_assumption.source_location()));
299 }
300 }
301
302 // record "old(...)" expressions.
303 std::vector<std::pair<symbol_exprt, exprt>> old_exprs;
304 const auto old_prefix = "old::" + id2string(f.first);
305
306 // postcondition?
307 if(!contract.c_ensures().empty())
308 {
309 // Stick the postconditions in as assertions at the end
310 auto last = body.instructions.end();
311 if(std::prev(last)->is_end_function())
312 last = std::prev(last);
313
314 for(auto &assertion : contract.c_ensures())
315 {
317
318 std::string comment = "postcondition";
319 if(contract.c_ensures().size() >= 2)
321
322 auto location = assertion.source_location();
323 location.set_function(f.first); // seems to be missing
324 location.set_property_class(ID_postcondition);
325 location.set_comment(comment);
326
327 auto replaced_assertion =
329
331
334
335 body.insert_before_swap(last, assertion_instruction);
336 }
337 }
338
339 // do 'old' in the body
340 if(
341 !contract.c_assigns().empty() || !contract.c_requires().empty() ||
342 !contract.c_ensures().empty())
343 {
344 for(auto &instruction : body.instructions)
345 instruction.transform(
347 return replace_old(expr, old_prefix, old_exprs);
348 });
349 }
350
351 // Add assignments to 'old' symbols at the beginning of the function.
352 {
353 auto tmp =
354 old_assignments(old_exprs, add_function(f.first, symbol_ptr->location));
355 add_at_beginning.destructive_append(tmp);
356 }
357
358 body.destructive_insert(body.instructions.begin(), add_at_beginning);
359
360 // assigns?
361 if(
362 !contract.c_assigns().empty() || !contract.c_requires().empty() ||
363 !contract.c_ensures().empty())
364 {
365 for(auto it = body.instructions.begin(); it != body.instructions.end();
366 it++)
367 {
368 if(it->is_assign())
369 {
370 const auto &lhs = it->assign_lhs();
371
372 // Parameter or local or old? Ignore.
373 if(is_procedure_local(f.first, lhs))
374 continue; // ok
375
376 if(is_old(lhs))
377 continue; // ok
378
379 // maybe not ok
380 auto assigns_assertion =
381 make_assigns_assertion(f.first, contract.c_assigns(), lhs);
382 auto location = it->source_location();
383 location.set_property_class("assigns");
384 location.set_comment("assigns clause");
386 std::move(assigns_assertion), std::move(location));
387 body.insert_before_swap(it, assertion_instruction);
388 it++; // skip over the assertion we have just generated
389 }
390 }
391 }
392}
393
395 goto_functionst::function_mapt::value_type &f,
396 const goto_modelt &goto_model)
397{
398 auto &body = f.second.body;
399 const namespacet ns(goto_model.symbol_table);
400
401 std::size_t call_site_counter = 0;
402
403 for(auto it = body.instructions.begin(); it != body.instructions.end(); it++)
404 {
405 if(it->is_function_call())
406 {
407 const auto &function = it->call_function();
408 if(function.id() == ID_symbol)
409 {
410 const auto &symbol = ns.lookup(to_symbol_expr(function));
411
412 const auto contract_opt = get_contract(symbol.name, ns);
413
414 if(!contract_opt.has_value())
415 continue;
416
417 auto &contract = contract_opt.value();
418
419 // record "old(...)" expressions.
420 std::vector<std::pair<symbol_exprt, exprt>> old_exprs;
421 const auto old_prefix = "old::" + id2string(f.first) + "::call-site-" +
422 std::to_string(++call_site_counter) + "::";
423
424 // need to substitute parameters
425 const auto f_it =
426 goto_model.goto_functions.function_map.find(symbol.name);
427
428 if(f_it == goto_model.goto_functions.function_map.end())
429 DATA_INVARIANT(false, "failed to find function in function_map");
430
431 replace_symbolt replace_symbol;
432 const auto &parameters = to_code_type(symbol.type).parameters();
433 const auto &arguments = it->call_arguments();
434
435 for(std::size_t p = 0; p < f_it->second.parameter_identifiers.size();
436 p++)
437 {
438 auto p_symbol = symbol_exprt(
439 f_it->second.parameter_identifiers[p], parameters[p].type());
440 replace_symbol.insert(p_symbol, arguments[p]);
441 }
442
443 // replace __CPROVER_return_value by the lhs of the call
444 const auto &call_lhs = it->call_lhs();
445 replace_symbol.insert(
446 symbol_exprt(CPROVER_PREFIX "return_value", call_lhs.type()),
447 call_lhs);
448
449 goto_programt dest;
450
451 // assert the preconditions
452 for(auto &precondition : contract.c_requires())
453 {
456
457 auto location = it->source_location();
458 location.set_property_class(ID_precondition);
459 location.set_comment(
460 id2string(symbol.display_name()) + " precondition " +
462
464 replace_symbol(replaced_precondition);
465
466 dest.add(
468 }
469
470 // havoc the 'assigned' variables
471 for(auto &assigns_clause_lambda : contract.c_assigns())
472 {
473 auto location = it->source_location();
474
475 auto assigns_clause =
477
479 {
480 const auto &condition = to_binary_expr(assigns_clause).op0();
481 auto replaced_condition = condition;
482 replace_symbol(replaced_condition);
483
484 const auto &targets =
486 .operands();
487
488 for(auto &target : targets)
489 {
490 auto rhs = side_effect_expr_nondett(target.type(), location);
491
492 auto replaced_lhs = target;
493 replace_symbol(replaced_lhs);
494
495 auto goto_instruction =
497 not_exprt(replaced_condition), location));
498
499 dest.add(
501
502 auto skip_instruction =
503 dest.add(goto_programt::make_skip(location));
504
505 goto_instruction->complete_goto(skip_instruction);
506 }
507 }
508 else
509 {
510 const auto &lhs = assigns_clause;
511 auto rhs = side_effect_expr_nondett(lhs.type(), location);
512
513 auto replaced_lhs = lhs;
514 replace_symbol(replaced_lhs);
516
517 dest.add(goto_programt::make_assignment(fixed_lhs, rhs, location));
518 }
519 }
520
521 // assume the postconditions
522 for(auto &postcondition : contract.c_ensures())
523 {
524 auto &location = it->source_location();
525
528 replace_symbol(replaced_postcondition1);
529
532
533 dest.add(
535 }
536
537 // now insert the assignents to old::... at the beginning
538 // of 'dest'
539 {
540 auto tmp = old_assignments(old_exprs, it->source_location());
541 dest.destructive_insert(dest.instructions.begin(), tmp);
542 }
543
544 // remove the function call
545 it->turn_into_skip();
546
547 // insert after 'it' to preserve branches to the call
548 body.destructive_insert(std::next(it), dest);
549 }
550 }
551 }
552}
553
555{
556 const namespacet ns(goto_model.symbol_table);
557
558 for(auto &f : goto_model.goto_functions.function_map)
559 {
562 }
563}
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Definition c_types.h:467
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Boolean AND.
Definition std_expr.h:2071
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:223
source_locationt & add_source_location()
Definition expr.h:228
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
const irep_idt & id() const
Definition irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Boolean negation.
Definition std_expr.h:2278
Replace a symbol expression by a given expression.
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
const irep_idt & get_file() const
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
Definition std_expr.h:113
Symbol table entry.
Definition symbol.h:28
The Boolean constant true.
Definition std_expr.h:3008
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4144
Symbol Table + CFG.
static std::string expr2text(const exprt &src, const namespacet &ns)
static bool is_symbol_member(const exprt &expr)
static bool is_procedure_local(const irep_idt &function_identifier, const exprt &lhs)
void replace_function_calls_by_contracts(goto_functionst::function_mapt::value_type &f, const goto_modelt &goto_model)
goto_programt old_assignments(const std::vector< std::pair< symbol_exprt, exprt > > &old_exprs, const source_locationt &source_location)
static bool is_old(const exprt &lhs)
static exprt make_address(exprt src)
exprt replace_old(exprt src, const std::string &prefix, std::vector< std::pair< symbol_exprt, exprt > > &old_exprs)
static exprt instantiate_contract_lambda(exprt src)
source_locationt add_function(irep_idt function_identifier, source_locationt src)
exprt assigns_match(const exprt &assigns, const exprt &lhs)
#define MAX_TEXT
optionalt< code_with_contract_typet > get_contract(const irep_idt &function_identifier, const namespacet &ns)
void instrument_contracts(goto_modelt &goto_model)
static exprt make_assigns_assertion(irep_idt function_identifier, const exprt::operandst &assigns, const exprt &lhs)
void instrument_contract_checks(goto_functionst::function_mapt::value_type &f, const namespacet &ns)
symbol_exprt find_old_expr(const exprt &src, const std::string &prefix, std::vector< std::pair< symbol_exprt, exprt > > &old_exprs)
bool has_contract(const irep_idt &function_identifier, const namespacet &ns)
exprt replace_source_location(exprt src, const source_locationt &source_location)
Instrument Given Invariants.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
bool is_true(const literalt &l)
Definition literal.h:198
API to expression classes for 'mathematical' expressions.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
exprt same_object(const exprt &p1, const exprt &p2)
Various predicates over pointers in programs.
void postcondition(const namespacet &ns, const value_sett &value_set, const symex_target_equationt &equation, const goto_symex_statet &s, exprt &dest)
void precondition(const namespacet &ns, value_setst &value_sets, const goto_programt::const_targett target, const symex_target_equationt &equation, const goto_symex_statet &s, exprt &dest)
static std::string comment(const rw_set_baset::entryt &entry, bool write)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:51
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:660
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:932
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744