Go to the documentation of this file.
15 #include <unordered_set>
52 if(exp.
id() != ID_symbol)
76 if((*it)->is_goto() &&
77 (*it)->get_target()==loop_head &&
78 (*it)->location_number>loop_end->location_number)
83 loop_end->get_condition().find(ID_C_spec_loop_invariant));
109 a->source_location.set_comment(
"Loop invariant violated before entry");
120 if(!loop_head->is_goto())
129 goto_function.body.insert_before_swap(loop_head, havoc_code);
136 goto_function.body.insert_before_swap(loop_end, a);
141 loop_end->targets.clear();
143 if(loop_head->is_goto())
146 loop_end->set_condition(
boolean_negate(loop_end->get_condition()));
179 exprt assigns =
static_cast<const exprt &
>(type.
find(ID_C_spec_assigns));
180 exprt requires =
static_cast<const exprt &
>(type.
find(ID_C_spec_requires));
181 exprt ensures =
static_cast<const exprt &
>(type.
find(ID_C_spec_ensures));
216 "ignored_return_value",
228 code_function_callt::argumentst::const_iterator a_it=
230 for(code_typet::parameterst::const_iterator p_it = type.
parameters().begin();
234 if(!p_it->get_identifier().empty())
263 for(
const exprt &curr_op : targets)
265 if(curr_op.id() == ID_symbol || curr_op.id() == ID_dereference)
267 assigns_tgts.insert(curr_op);
271 log.
error() <<
"Unable to apply assigns clause for expression of type '"
272 << curr_op.id() <<
"'; not enforcing assigns clause."
281 std::advance(target, assigns_tgts.size());
308 for(natural_loops_mutablet::loop_mapt::const_iterator l_it =
310 l_it != natural_loops.
loop_map.end();
313 goto_function, local_may_alias, l_it->first, l_it->second);
317 if(ins->is_function_call())
337 const exprt &assigns,
339 std::vector<exprt> &aliasable_references)
341 bool first_iter =
true;
343 for(
auto aliasable : aliasable_references)
346 exprt right_ptr = aliasable;
357 disjuncts.push_back(same);
358 disjuncts.push_back(running);
367 const symbolt &function_symbol,
370 std::vector<exprt> &created_references)
373 const exprt &assigns =
374 static_cast<const exprt &
>(type.
find(ID_C_spec_assigns));
377 for(
const exprt &curr_op : targets)
384 function_symbol.
mode)
395 created_references.push_back(standin);
400 goto_programt::instructionst::iterator &instruction_iterator,
403 std::vector<exprt> &assigns_references,
404 std::set<exprt> &freely_assignable_exprs)
407 instruction_iterator->is_assign(),
408 "The first argument of instrument_assigns_statement should always be"
410 const exprt &lhs = instruction_iterator->get_assign().lhs();
411 if(freely_assignable_exprs.find(lhs) != freely_assignable_exprs.end())
421 ++instruction_iterator;
425 goto_programt::instructionst::iterator &instruction_iterator,
428 std::vector<exprt> &aliasable_references,
429 std::set<exprt> &freely_assignable_exprs)
432 instruction_iterator->is_function_call(),
433 "The first argument of instrument_call_statement should always be "
442 if(called_name ==
"malloc")
444 aliasable_references.push_back(call.
lhs());
447 goto_programt::instructionst::iterator local_instruction_iterator =
448 instruction_iterator;
449 local_instruction_iterator++;
451 local_instruction_iterator->is_assign() &&
452 local_instruction_iterator->get_assign().lhs().is_not_nil())
454 freely_assignable_exprs.insert(
455 local_instruction_iterator->get_assign().lhs());
469 ++instruction_iterator;
481 log.
error() <<
"Could not find function '" << called_name
482 <<
"' in goto-program; not enforcing assigns clause."
487 exprt called_assigns =
static_cast<const exprt &
>(
488 called_func->second.type.find(ID_C_spec_assigns));
489 if(called_assigns.
is_nil())
492 log.
error() <<
"No assigns specification found for function '"
494 <<
"' in goto-program; not enforcing assigns clause."
503 ++instruction_iterator;
511 code_function_callt::argumentst::const_iterator a_it =
513 for(code_typet::parameterst::const_iterator p_it =
519 if(!p_it->get_identifier().empty())
527 for(exprt::operandst::const_iterator called_op_it =
529 called_op_it != called_assigns.
operands().end();
533 freely_assignable_exprs.find(*called_op_it) !=
534 freely_assignable_exprs.end())
545 ++instruction_iterator;
554 std::vector<goto_programt::instructiont> back_gotos;
555 std::vector<goto_programt::instructiont> malloc_calls;
562 back_gotos.push_back(instruction);
570 if(called_name ==
"malloc")
572 malloc_calls.push_back(instruction);
579 for(
auto goto_entry : back_gotos)
581 for(
const auto &target : goto_entry.targets)
583 for(
auto malloc_entry : malloc_calls)
586 malloc_entry.location_number >= target->location_number &&
587 malloc_entry.location_number < goto_entry.location_number)
597 log.
error() <<
"Call to malloc at location "
598 << malloc_entry.location_number <<
" falls between goto "
599 <<
"source location " << goto_entry.location_number
600 <<
" and it's destination at location "
601 << target->location_number <<
". "
602 <<
"Unable to complete instrumentation, as this malloc "
618 log.
error() <<
"Could not find function '" << function_name
619 <<
"' in goto-program; not enforcing contracts."
629 const irep_idt function_id(function_name);
633 exprt assigns =
static_cast<const exprt &
>(type.
find(ID_C_spec_assigns));
639 goto_programt::instructionst::iterator instruction_iterator =
645 std::vector<exprt> original_references;
647 function_symbol, function_id, standin_decls, original_references);
650 std::set<exprt> freely_assignable_exprs;
653 freely_assignable_exprs.insert(param);
656 int lines_to_iterate = standin_decls.
instructions.size();
658 std::advance(instruction_iterator, lines_to_iterate);
666 for(; instruction_iterator != program.
instructions.end();
667 ++instruction_iterator)
669 if(instruction_iterator->is_decl())
671 freely_assignable_exprs.insert(instruction_iterator->get_decl().symbol());
673 else if(instruction_iterator->is_assign())
676 instruction_iterator,
680 freely_assignable_exprs);
682 else if(instruction_iterator->is_function_call())
685 instruction_iterator,
689 freely_assignable_exprs);
702 std::stringstream ss;
705 const irep_idt original(fun_to_enforce);
710 log.
error() <<
"Could not find function '" << fun_to_enforce
711 <<
"' in goto-program; not enforcing contracts."
721 sl.
set_file(
"instrumented for code contracts");
725 mangled_sym = *original_sym;
726 mangled_sym.
name = mangled;
731 mangled_found.second,
732 "There should be no existing function called " + ss.str() +
733 " in the symbol table because that name is a mangled name");
739 "There should be no function called " + fun_to_enforce +
740 " in the function map because that function should have had its"
746 "There should be a function called " + ss.str() +
747 " in the function map because we inserted a fresh goto-program"
748 " with that mangled name");
752 if(mangled_fun->second.type.is_not_nil())
753 wrapper.
type = mangled_fun->second.type;
766 goto_functionst::function_mapt::iterator f_it =
772 const exprt &assigns =
773 static_cast<const exprt &
>(gf.type.find(ID_C_spec_assigns));
774 const exprt &requires =
775 static_cast<const exprt &
>(gf.type.find(ID_C_spec_requires));
776 const exprt &ensures =
777 static_cast<const exprt &
>(gf.type.find(ID_C_spec_ensures));
780 "Code contract enforcement is trivial without an ensures or assigns "
814 gf.type.return_type(),
815 skip->source_location,
817 function_symbol.
mode)
828 for(
const auto ¶meter : gf.parameter_identifiers)
834 parameter_symbol.
type,
837 parameter_symbol.
mode)
850 exprt requires_cond = requires;
861 exprt ensures_cond = ensures;
877 const std::set<std::string> &funs_to_replace)
880 for(
const auto &fun : funs_to_replace)
885 <<
"' does not have a contract; "
886 "not replacing calls with contract."
898 if(ins->is_function_call())
908 auto found = std::find(
909 funs_to_replace.begin(), funs_to_replace.end(),
id2string(fun_name));
910 if(found == funs_to_replace.end())
931 std::set<std::string> funs_to_replace;
935 funs_to_replace.insert(
id2string(goto_function.first));
942 std::set<std::string> funs_to_enforce;
946 funs_to_enforce.insert(
id2string(goto_function.first));
952 const std::set<std::string> &funs_to_enforce)
955 for(
const auto &fun : funs_to_enforce)
960 log.
error() <<
"Could not find function '" << fun
961 <<
"' in goto-program; not enforcing contracts."
#define Forall_goto_program_instructions(it, program)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void code_contracts(goto_functionst::goto_functiont &goto_function)
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
source_locationt source_location
The location of the instruction in the source file.
void add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest)
void set_comment(const irep_idt &comment)
void populate_assigns_references(const symbolt &f_sym, const irep_idt &func_id, goto_programt &created_decls, std::vector< exprt > &created_references)
Creates a local variable declaration for each expression in the assigns clause (of the function given...
void instrument_call_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, std::vector< exprt > &assigns_references, std::set< exprt > &freely_assignable_exprs)
Inserts an assertion statement into program before the function call at ins_it, to ensure that any me...
The type of an expression, extends irept.
Fresh auxiliary symbol creation.
typet type
Type of symbol.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Various predicates over pointers in programs.
const irept & find(const irep_namet &name) const
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Predicate to be used with the exprt::visit() function.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
const_iterator end() const
Iterator over this loop's instructions.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
function_mapt function_map
Expression to hold a symbol (variable)
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void visit(class expr_visitort &visitor)
These are pre-order traversal visitors, i.e., the visitor is executed on a node before its children h...
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)
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
void set_line(const irep_idt &line)
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
const_iterator begin() const
Iterator over this loop's instructions.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
std::set< exprt > modifiest
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
irep_idt mode
Language mode.
loop_instructionst::const_iterator const_iterator
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Field-insensitive, location-sensitive may-alias analysis.
const std::string & id2string(const irep_idt &d)
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
bool has_contract(const irep_idt)
Does the named function have a contract?
#define PRECONDITION(CONDITION)
const source_locationt & source_location() const
const irep_idt & get_identifier() const
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
void instrument_assigns_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, std::vector< exprt > &original_references, std::set< exprt > &freely_assignable_exprs)
Inserts an assertion statement into program before the assignment ins_it, to ensure that the left-han...
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
void set_file(const irep_idt &file)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
bool check_for_looped_mallocs(const goto_programt &)
Check if there are any malloc statements which may be repeated because of a goto statement that jumps...
bool apply_contract(goto_programt &goto_program, goto_programt::targett target)
bool add_pointer_checks(const std::string &)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
A loop, specified as a set of instructions.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
pointer_typet pointer_type(const typet &subtype)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
A goto function, consisting of function type (see type), function body (see body),...
std::vector< exprt > operandst
The Boolean constant false.
const parameterst & parameters() const
Helper functions for k-induction and loop invariants.
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
void operator()(const exprt &exp) override
A side_effect_exprt that returns a non-deterministically chosen value.
::goto_functiont goto_functiont
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &function_id, const irep_idt &mode)
instructionst instructions
The list of instructions in the goto program.
Deprecated expression utility functions.
bool enforce_contracts()
Call enforce_contracts() on all functions that have a contract.
goto_functionst & goto_functions
source_locationt location
Source code location of definition of symbol.
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
exprt same_object(const exprt &p1, const exprt &p2)
A generic container class for the GOTO intermediate representation of one function.
static exprt create_alias_expression(const exprt &assigns, const exprt &lhs, std::vector< exprt > &aliasable_references)
bool replace_calls()
Call replace_calls() on all calls to any function that has a contract.
std::unordered_set< irep_idt > summarized
bool empty() const
Returns true if this loop contains no instructions.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const typet & return_type() const
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
bool enforce_contract(const std::string &)
Enforce contract of a single function.
code_typet type
The type of the function, indicating the return type and parameter types.
Operator to return the address of an object.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
bool found_return_value()
A codet representing an assignment in the program.
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
bool is_function_call() const
This class represents an instruction in the GOTO intermediate representation.
const source_locationt & source_location() const
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 ...
irep_idt name
The unique identifier.
instructionst::iterator targett
symbol_tablet & symbol_table
Verify and use annotated invariants and pre/post-conditions.
Replace expression or type symbols by an expression or type, respectively.