42 const std::vector<symbol_exprt> &lhs,
43 const std::vector<symbol_exprt> &rhs)
60 for(
size_t i = 1; i < equality_conjunctions.size() - 1; i++)
63 equality_conjunctions[i] =
64 and_exprt(equality_conjunctions[i - 1], component_i_equality);
74 lexicographic_individual_comparisons[0] =
76 for(
size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
79 lexicographic_individual_comparisons[i] =
80 and_exprt(equality_conjunctions[i - 1], component_i_less_than);
82 return disjunction(lexicographic_individual_comparisons);
92 std::advance(target, offset);
106 for(
const auto &t : loop)
108 t->is_goto() && t->get_target() == loop_head &&
109 t->location_number > loop_end->location_number)
113 auto invariant =
static_cast<const exprt &
>(
114 loop_end->get_condition().find(ID_C_spec_loop_invariant));
115 auto decreases_clause =
static_cast<const exprt &
>(
116 loop_end->get_condition().find(ID_C_spec_decreases));
118 if(invariant.is_nil())
120 if(decreases_clause.is_nil())
127 <<
" does not have a loop invariant, but has a decreases clause. "
128 <<
"Hence, a default loop invariant ('true') is being used."
139 const auto &decreases_clause_exprs = decreases_clause.operands();
143 std::vector<symbol_exprt> old_decreases_vars;
144 std::vector<symbol_exprt> new_decreases_vars;
172 const auto &invariant_expr = [&]() {
173 auto invariant_copy = invariant;
177 return invariant_copy;
182 std::map<exprt, exprt> parameter2history;
186 loop_head->source_location,
201 havoc_code.
instructions.back().source_location.set_comment(
202 "Check loop invariant before entry");
219 for(
const auto &clause : decreases_clause.operands())
221 const auto old_decreases_var =
226 old_decreases_vars.push_back(old_decreases_var);
228 const auto new_decreases_var =
233 new_decreases_vars.push_back(new_decreases_var);
237 if(!loop_head->is_goto())
250 if(!decreases_clause.is_nil())
252 for(
size_t i = 0; i < old_decreases_vars.size(); i++)
254 code_assignt old_decreases_assignment{old_decreases_vars[i],
255 decreases_clause_exprs[i]};
257 loop_head->source_location;
261 goto_function.body.destructive_insert(std::next(loop_head), havoc_code);
271 havoc_code.
instructions.back().source_location.set_comment(
272 "Check that loop invariant is preserved");
277 if(!decreases_clause.is_nil())
279 for(
size_t i = 0; i < new_decreases_vars.size(); i++)
281 code_assignt new_decreases_assignment{new_decreases_vars[i],
282 decreases_clause_exprs[i]};
284 loop_head->source_location;
294 loop_head->source_location;
296 havoc_code.
instructions.back().source_location.set_comment(
297 "Check decreases clause on loop iteration");
300 for(
size_t i = 0; i < old_decreases_vars.size(); i++)
303 old_decreases_vars[i], loop_head->source_location));
305 new_decreases_vars[i], loop_head->source_location));
312 loop_end->targets.clear();
314 if(loop_head->is_goto())
317 loop_end->set_condition(
boolean_negate(loop_end->get_condition()));
324 return type.has_contract();
328 const exprt &expression,
332 if(expression.
id() == ID_not || expression.
id() == ID_typecast)
339 if(expression.
id() == ID_notequal || expression.
id() == ID_implies)
347 if(expression.
id() == ID_if)
351 const auto &if_expression =
to_if_expr(expression);
356 if(expression.
id() == ID_and || expression.
id() == ID_or)
361 for(
const auto &operand : multi_ary_expression.operands())
366 else if(expression.
id() == ID_exists || expression.
id() == ID_forall)
371 for(
const auto &quantified_variable : quantifier_expression.variables())
373 const auto &quantified_symbol =
to_symbol_expr(quantified_variable);
377 quantified_symbol.type(),
378 id2string(quantified_symbol.get_identifier()),
380 quantified_symbol.source_location(),
386 quantified_symbol.get_identifier(), quantified_symbol.type());
397 std::map<exprt, exprt> ¶meter2history,
406 op, parameter2history, location, mode, history,
id);
409 if(expr.
id() == ID_old || expr.
id() == ID_loop_entry)
414 parameter.id() == ID_dereference || parameter.id() == ID_member ||
415 parameter.id() == ID_symbol || parameter.id() == ID_ptrmember)
417 auto it = parameter2history.
find(parameter);
419 if(it == parameter2history.end())
428 parameter2history[parameter] = tmp_symbol;
441 expr = parameter2history[parameter];
445 log.
error() <<
"Tracking history of " << parameter.id()
452 std::pair<goto_programt, goto_programt>
458 std::map<exprt, exprt> parameter2history;
463 expression, parameter2history, location, mode, history, ID_old);
472 return std::make_pair(std::move(ensures_program), std::move(history));
491 auto assigns = type.assigns();
502 if(
as_const(*target).call_lhs().is_not_nil())
525 "ignored_return_value",
526 target->source_location,
537 const auto &arguments = target->call_arguments();
538 auto a_it = arguments.begin();
539 for(
auto p_it = type.parameters().begin();
540 p_it != type.parameters().end() && a_it != arguments.end();
543 if(!p_it->get_identifier().empty())
546 common_replace.
insert(p, *a_it);
552 common_replace(assigns);
560 if(!requires.is_true())
571 assertion.
instructions.back().source_location = requires.source_location();
572 assertion.
instructions.back().source_location.set_comment(
573 "Check requires clause");
574 assertion.
instructions.back().source_location.set_property_class(
582 std::pair<goto_programt, goto_programt> ensures_pair;
583 if(!ensures.is_false())
592 ensures.source_location(),
602 if(assigns.is_not_nil())
613 if(!ensures.is_false())
634 for(
const auto &loop : natural_loops.
loop_map)
671 std::vector<exprt> &aliasable_references)
674 operands.reserve(aliasable_references.size());
675 for(
auto aliasable : aliasable_references)
683 goto_programt::instructionst::iterator &instruction_iterator,
686 std::set<irep_idt> &freely_assignable_symbols,
690 instruction_iterator->is_assign(),
691 "The first instruction of instrument_assign_statement should always be"
694 const exprt &lhs = instruction_iterator->assign_lhs();
697 freely_assignable_symbols.find(lhs.
get(ID_identifier)) ==
698 freely_assignable_symbols.end())
704 alias_assertion.
instructions.back().source_location.set_comment(
705 "Check that " +
from_expr(
ns, lhs.
id(), lhs) +
" is assignable");
707 program, instruction_iterator, alias_assertion);
712 goto_programt::instructionst::iterator &instruction_iterator,
715 std::set<irep_idt> &freely_assignable_symbols,
719 instruction_iterator->is_function_call(),
720 "The first argument of instrument_call_statement should always be "
724 if(instruction_iterator->call_function().id() == ID_dereference)
737 if(called_name ==
"malloc")
742 instruction_iterator++;
743 if(instruction_iterator->is_assign())
745 const exprt &rhs = instruction_iterator->assign_rhs();
747 rhs.
id() == ID_typecast,
748 "malloc is called but the result is not cast. Excluding result from "
749 "the assignable memory frame.");
757 program, instruction_iterator, pointer_capture);
763 instruction_iterator->call_lhs().is_not_nil() &&
764 instruction_iterator->call_lhs().id() == ID_symbol &&
765 freely_assignable_symbols.find(
767 freely_assignable_symbols.end())
775 alias_assertion.
instructions.back().source_location.set_comment(
779 ++instruction_iterator;
784 const typet &called_symbol_type = (called_symbol.
type.
id() == ID_pointer)
786 : called_symbol.
type;
787 exprt called_assigns =
794 const auto &arguments = instruction_iterator->call_arguments();
795 auto a_it = arguments.begin();
796 for(
auto p_it = called_type.
parameters().begin();
797 p_it != called_type.
parameters().end() && a_it != arguments.end();
800 if(!p_it->get_identifier().empty())
803 replace_formal_params.
insert(p, *a_it);
806 replace_formal_params(called_assigns);
810 called_assigns, *
this, called_name,
log);
816 alias_assertion.
instructions.back().source_location.set_comment(
817 "Check compatibility of assigns clause with the called function");
819 ++instruction_iterator;
826 std::vector<goto_programt::instructiont> back_gotos;
827 std::vector<goto_programt::instructiont> malloc_calls;
834 back_gotos.push_back(instruction);
852 if(called_name ==
"malloc")
854 malloc_calls.push_back(instruction);
861 for(
auto goto_entry : back_gotos)
863 for(
const auto &target : goto_entry.targets)
865 for(
auto malloc_entry : malloc_calls)
868 malloc_entry.location_number >= target->location_number &&
869 malloc_entry.location_number < goto_entry.location_number)
871 log.
error() <<
"Call to malloc at location "
872 << malloc_entry.location_number <<
" falls between goto "
873 <<
"source location " << goto_entry.location_number
874 <<
" and it's destination at location "
875 << target->location_number <<
". "
876 <<
"Unable to complete instrumentation, as this malloc "
892 log.
error() <<
"Could not find function '" <<
function
893 <<
"' in goto-program; not enforcing contracts."
919 exprt assigns_expr = type.assigns();
924 std::set<irep_idt> freely_assignable_symbols;
936 for(; instruction_it != program.
instructions.end(); ++instruction_it)
938 if(instruction_it->is_decl())
941 freely_assignable_symbols.insert(
942 instruction_it->get_decl().symbol().get_identifier());
945 assigns.
add_target(instruction_it->get_decl().symbol());
954 else if(instruction_it->is_assign())
960 freely_assignable_symbols,
963 else if(instruction_it->is_function_call())
969 freely_assignable_symbols,
975 while(!instruction_it->is_end_function())
991 std::stringstream ss;
999 log.
error() <<
"Could not find function '" <<
function
1000 <<
"' in goto-program; not enforcing contracts."
1010 sl.
set_file(
"instrumented for code contracts");
1014 mangled_sym = *original_sym;
1015 mangled_sym.
name = mangled;
1020 mangled_found.second,
1021 "There should be no existing function called " + ss.str() +
1022 " in the symbol table because that name is a mangled name");
1028 "There should be no function called " +
id2string(
function) +
1029 " in the function map because that function should have had its"
1035 "There should be a function called " + ss.str() +
1036 " in the function map because we inserted a fresh goto-program"
1037 " with that mangled name");
1057 exprt assigns = code_type.assigns();
1091 code_type.return_type(),
1092 skip->source_location,
1093 function_symbol.
mode)
1101 common_replace.
insert(ret_val,
r);
1105 goto_functionst::function_mapt::iterator f_it =
1110 for(
const auto ¶meter : gf.parameter_identifiers)
1115 parameter_symbol.
type,
1117 parameter_symbol.
mode)
1149 std::pair<goto_programt, goto_programt> ensures_pair;
1166 ensures_pair.first.instructions.back().source_location.set_comment(
1167 "Check ensures clause");
1168 ensures_pair.first.instructions.back().source_location.set_property_class(
1198 for(
const auto &
function : functions)
1202 log.
error() <<
"Function '" <<
function
1203 <<
"' does not have a contract; "
1204 "not replacing calls with contract."
1216 if(ins->is_function_call())
1218 if(ins->call_function().id() != ID_symbol)
1223 auto found = std::find(
1224 functions.begin(), functions.end(),
id2string(called_function));
1225 if(found == functions.end())
1252 std::set<std::string> functions;
1256 functions.insert(
id2string(goto_function.first));
1263 std::set<std::string> functions;
1267 functions.insert(
id2string(goto_function.first));
1275 for(
const auto &
function : functions)
1281 log.
error() <<
"Could not find function '" <<
function
1282 <<
"' in goto-program; not enforcing contracts."
1290 log.
error() <<
"Could not find any contracts within function '"
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Specify write set in function contracts.
API to expression classes that are internal to the C frontend.
const history_exprt & to_history_expr(const exprt &expr, const irep_idt &id)
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
A base class for assigns clause targets.
goto_programt & get_init_block()
goto_programt havoc_code()
exprt alias_expression(const exprt &lhs)
goto_programt init_block()
assigns_clause_targett * add_target(exprt target)
exprt compatible_expression(const assigns_clauset &called_assigns)
goto_programt dead_stmts()
A base class for relations, i.e., binary predicates whose two operands have the same type.
A non-fatal assertion, which checks a condition then permits execution to continue.
A codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
bool enforce_contracts()
Call enforce_contracts() on all functions that have a contract.
std::pair< goto_programt, goto_programt > create_ensures_instruction(codet &expression, source_locationt location, const irep_idt &mode)
This function creates and returns an instruction that corresponds to the ensures clause.
void replace_history_parameter(exprt &expr, std::map< exprt, exprt > ¶meter2history, source_locationt location, const irep_idt &mode, goto_programt &history, const irep_idt &id)
This function recursively identifies the "old" expressions within expr and replaces them with corresp...
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &mode)
void instrument_call_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause)
Inserts an assertion statement into program before the function call at ins_it, to ensure that any me...
void apply_loop_contract(const irep_idt &function, goto_functionst::goto_functiont &goto_function)
Apply loop contracts, whenever available, to all loops in function.
goto_functionst & get_goto_functions()
void check_frame_conditions(goto_programt &program, const symbolt &target)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
void apply_loop_contracts()
symbol_tablet & symbol_table
exprt create_alias_expression(const exprt &lhs, std::vector< exprt > &aliasable_references)
Creates a boolean expression which is true when there exists an expression in aliasable_references wi...
void add_quantified_variable(const exprt &expression, replace_symbolt &replace, const irep_idt &mode)
This function recursively searches the expression to find nested or non-nested quantified expressions...
void check_apply_loop_contracts(goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, const loopt &loop, const irep_idt &mode)
bool check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
bool apply_function_contract(goto_programt &goto_program, goto_programt::targett target)
Replaces function calls with assertions based on requires clauses, non-deterministic assignments for ...
bool replace_calls()
Call replace_calls() on all calls to any function that has a contract.
bool enforce_contract(const irep_idt &function)
Enforce contract of a single function.
std::unordered_set< irep_idt > summarized
bool has_contract(const irep_idt)
Does the named function have a contract?
bool check_for_looped_mallocs(const goto_programt &program)
Check if there are any malloc statements which may be repeated because of a goto statement that jumps...
void instrument_assign_statement(goto_programt::instructionst::iterator &instruction_it, goto_programt &program, exprt &assigns, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause)
Inserts an assertion statement into program before the assignment instruction_it, to ensure that the ...
goto_functionst & goto_functions
void add_contract_check(const irep_idt &wrapper_function, const irep_idt &mangled_function, goto_programt &dest)
Instruments wrapper_function adding assumptions based on requires clauses and assertions based on ens...
symbol_tablet & get_symbol_table()
codet representation of a function call statement.
codet representation of a "return from a function" statement.
const parameterst & parameters() const
const exprt & assigns() const
Data structure for representing an arbitrary statement in a program.
Operator to dereference a pointer.
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
bool is_true() const
Return whether the expression is a constant representing true.
source_locationt & add_source_location()
const source_locationt & source_location() const
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
The Boolean constant false.
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
This class represents an instruction in the GOTO intermediate representation.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
bool is_function_call() const
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_return(code_returnt c, const source_locationt &l=source_locationt::nil())
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 insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
const exprt & expression() const
const irept & find(const irep_namet &name) const
const irep_idt & id() const
const irep_idt & get(const irep_namet &name) const
void update_requires(goto_programt &requires)
void update_ensures(goto_programt &ensures)
virtual void create_declarations()
virtual void create_declarations()
source_locationt source_location
mstreamt & warning() const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Replace expression or type symbols by an expression or type, respectively.
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...
Predicate to be used with the exprt::visit() function.
bool found_return_value()
A side_effect_exprt that returns a non-deterministically chosen value.
const irep_idt & get_function() const
std::string as_string() const
void set_file(const irep_idt &file)
void set_line(const irep_idt &line)
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
irep_idt base_name
Base (non-scoped) name.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt mode
Language mode.
The Boolean constant true.
Semantic type conversion.
The type of an expression, extends irept.
const source_locationt & source_location() const
const typet & subtype() const
static exprt create_lexicographic_less_than(const std::vector< symbol_exprt > &lhs, const std::vector< symbol_exprt > &rhs)
static void insert_before_swap_and_advance(goto_programt &program, goto_programt::targett &target, goto_programt &payload)
Verify and use annotated invariants and pre/post-conditions.
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
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 ...
Fresh auxiliary symbol creation.
#define Forall_goto_program_instructions(it, program)
void append_havoc_code(const source_locationt source_location, const modifiest &modifies, goto_programt &dest)
Utilities for building havoc code for expressions.
std::set< exprt > modifiest
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Field-insensitive, location-sensitive may-alias analysis.
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
natural_loops_mutablet::natural_loopt loopt
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Predicates to specify memory footprint in function contracts.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define PRECONDITION(CONDITION)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
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 if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_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 code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)