31 auto contract_identifier =
"contract::" +
id2string(function_identifier);
33 if(ns.
lookup(contract_identifier, symbol_ptr))
41 return get_contract(function_identifier, ns).has_value();
46 auto text =
expr2c(src, ns);
48 return std::string(text, 0,
MAX_TEXT - 3) +
"...";
55 if(src.
id() == ID_dereference)
99 if(expr.
id() == ID_symbol)
101 else if(expr.
id() == ID_member)
112 if(lhs.
id() == ID_member)
117 else if(lhs.
id() == ID_index)
150 for(
auto &assigns_clause : assigns)
154 if(a.id() == ID_conditional_target_group)
158 for(
auto &target : targets.operands())
176 disjuncts.push_back(std::move(match));
186 if(lhs.
id() == ID_member)
189 else if(lhs.
id() == ID_index)
191 else if(lhs.
id() == ID_symbol)
204 if(lhs.
id() == ID_symbol)
215 const std::string &prefix,
216 std::vector<std::pair<symbol_exprt, exprt>> &old_exprs)
218 for(std::size_t i = 0; i < old_exprs.size(); i++)
220 if(old_exprs[i].second == src)
221 return old_exprs[i].first;
224 auto index = old_exprs.size();
225 irep_idt identifier = prefix + std::to_string(index);
228 return old_exprs.back().first;
233 const std::string &prefix,
234 std::vector<std::pair<symbol_exprt, exprt>> &old_exprs)
236 if(src.
id() == ID_old)
251 const std::vector<std::pair<symbol_exprt, exprt>> &old_exprs,
256 for(
const auto &old_expr : old_exprs)
258 auto lhs = old_expr.first;
260 auto assignment_instruction =
262 dest.
add(std::move(assignment_instruction));
269 goto_functionst::function_mapt::value_type &f,
273 auto contract_identifier =
"contract::" +
id2string(f.first);
275 if(ns.
lookup(contract_identifier, symbol_ptr))
280 auto &body = f.second.body;
282 if(body.instructions.empty())
289 if(!contract.c_requires().empty())
293 for(
auto &assumption : contract.c_requires())
296 auto fixed_assumption =
add_function(f.first, assumption_instance);
298 fixed_assumption, fixed_assumption.source_location()));
303 std::vector<std::pair<symbol_exprt, exprt>> old_exprs;
304 const auto old_prefix =
"old::" +
id2string(f.first);
307 if(!contract.c_ensures().empty())
310 auto last = body.instructions.end();
311 if(std::prev(last)->is_end_function())
312 last = std::prev(last);
314 for(
auto &assertion : contract.c_ensures())
318 std::string
comment =
"postcondition";
319 if(contract.c_ensures().size() >= 2)
322 auto location = assertion.source_location();
323 location.set_function(f.first);
324 location.set_property_class(ID_postcondition);
327 auto replaced_assertion =
328 replace_old(assertion_instance, old_prefix, old_exprs);
330 auto fixed_assertion =
add_function(f.first, replaced_assertion);
332 auto assertion_instruction =
335 body.insert_before_swap(last, assertion_instruction);
341 !contract.c_assigns().empty() || !contract.c_requires().empty() ||
342 !contract.c_ensures().empty())
344 for(
auto &instruction : body.instructions)
345 instruction.transform(
358 body.destructive_insert(body.instructions.begin(), add_at_beginning);
362 !contract.c_assigns().empty() || !contract.c_requires().empty() ||
363 !contract.c_ensures().empty())
365 for(
auto it = body.instructions.begin(); it != body.instructions.end();
370 const auto &lhs = it->assign_lhs();
380 auto assigns_assertion =
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);
395 goto_functionst::function_mapt::value_type &f,
398 auto &body = f.second.body;
401 std::size_t call_site_counter = 0;
403 for(
auto it = body.instructions.begin(); it != body.instructions.end(); it++)
405 if(it->is_function_call())
407 const auto &function = it->call_function();
408 if(function.id() == ID_symbol)
412 const auto contract_opt =
get_contract(symbol.name, ns);
414 if(!contract_opt.has_value())
417 auto &contract = contract_opt.value();
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) +
"::";
433 const auto &arguments = it->call_arguments();
435 for(std::size_t p = 0; p < f_it->second.parameter_identifiers.size();
439 f_it->second.parameter_identifiers[p], parameters[p].type());
440 replace_symbol.
insert(p_symbol, arguments[p]);
444 const auto &call_lhs = it->call_lhs();
454 auto instantiated_precondition =
457 auto location = it->source_location();
458 location.set_property_class(ID_precondition);
459 location.set_comment(
460 id2string(symbol.display_name()) +
" precondition " +
461 expr2text(instantiated_precondition, ns));
463 auto replaced_precondition = instantiated_precondition;
464 replace_symbol(replaced_precondition);
471 for(
auto &assigns_clause_lambda : contract.c_assigns())
473 auto location = it->source_location();
475 auto assigns_clause =
478 if(assigns_clause.id() == ID_conditional_target_group)
481 auto replaced_condition = condition;
482 replace_symbol(replaced_condition);
484 const auto &targets =
488 for(
auto &target : targets)
492 auto replaced_lhs = target;
493 replace_symbol(replaced_lhs);
495 auto goto_instruction =
497 not_exprt(replaced_condition), location));
502 auto skip_instruction =
505 goto_instruction->complete_goto(skip_instruction);
510 const auto &lhs = assigns_clause;
513 auto replaced_lhs = lhs;
514 replace_symbol(replaced_lhs);
524 auto &location = it->source_location();
526 auto replaced_postcondition1 =
528 replace_symbol(replaced_postcondition1);
530 auto replaced_postcondition2 =
531 replace_old(replaced_postcondition1, old_prefix, old_exprs);
545 it->turn_into_skip();
548 body.destructive_insert(std::next(it), dest);
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Operator to return the address of an object.
const parameterst & parameters() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
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.
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
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.
const irep_idt & get_file() const
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
source_locationt location
Source code location of definition of symbol.
typet type
Type of symbol.
The Boolean constant true.
static exprt conditional_cast(const exprt &expr, const typet &type)
bool has_prefix(const std::string &s, const std::string &prefix)
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
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)
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)
bool is_true(const literalt &l)
API to expression classes for 'mathematical' expressions.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
nonstd::optional< T > optionalt
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,...
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.