67 if(message.find(
"recursion is ignored on call") != std::string::npos)
81 void print(
unsigned level,
const std::string &message)
override
104 const std::string &message,
150 for(
const auto &t : loop)
152 t->is_goto() && t->get_target() ==
loop_head &&
153 t->location_number >
loop_end->location_number)
159 auto invariant =
static_cast<const exprt &
>(
164 if(invariant.is_nil())
172 <<
"The loop at " <<
loop_head->source_location().as_string()
173 <<
" does not have an invariant, but has other clauses"
174 <<
" specified in its contract.\n"
175 <<
"Hence, a default invariant ('true') is being used to prove those."
240 assertion.add_source_location() =
loop_head->source_location();
242 generated_code.instructions.back().source_location_nonconst().set_comment(
243 "Check loop invariant before entry");
279 log.
debug() <<
"No loop assigns clause provided. Inferred targets {";
292 <<
"}. Please specify an assigns clause if verification fails."
297 log.
error() <<
"Failed to infer variables being modified by the loop at "
299 <<
".\nPlease specify an assigns clause.\nReason:"
363 assumption.add_source_location() =
loop_head->source_location();
391 log.
error() <<
"Loop contracts are unsupported on do/while loops: "
438 goto_function.body.destructive_insert(
447 assertion.add_source_location() =
loop_end->source_location();
449 generated_code.instructions.back().source_location_nonconst().set_comment(
450 "Check that loop invariant is preserved");
476 generated_code.instructions.back().source_location_nonconst().set_comment(
477 "Check decreases clause on loop iteration");
500 const exprt &expression,
638std::pair<goto_programt, goto_programt>
699 if(target->call_lhs().is_not_nil())
724 "ignored_return_value",
739 auto a_it = arguments.begin();
740 for(
auto p_it = type.parameters().begin();
741 p_it != type.parameters().end() &&
a_it != arguments.end();
744 if(!
p_it->get_identifier().empty())
768 assertion.
instructions.back().source_location_nonconst() =
769 requires.source_location();
770 assertion.
instructions.back().source_location_nonconst().set_comment(
771 "Check requires clause");
772 assertion.
instructions.back().source_location_nonconst().set_property_class(
774 is_fresh.update_requires(assertion);
781 if(!ensures.is_false())
790 ensures.source_location(),
827 auto &loc =
call_ret.source_location();
838 target->code_nonconst().add_source_location() = loc;
846 if(!ensures.is_false())
875 goto_function.body.instructions.begin(),
876 goto_function.body.instructions.end(),
878 return instruction.is_backwards_goto();
889 decorated.get_recursive_function_warnings_count() == 0,
890 "Recursive functions found during inlining");
922 for(
const auto &loop : natural_loops.
loop_map)
986 "The first argument of instrument_call_statement should always be "
994 const auto &function_call =
996 if(function_call.lhs().is_not_nil())
1000 object.add_source_location() = function_call.source_location();
1016 object.add_source_location() =
instruction_it->source_location();
1019 .check_inclusion_heap_allocated_and_invalidate_aliases(
1028 std::vector<goto_programt::instructiont>
back_gotos;
1034 if(instruction.is_backwards_goto())
1038 if(instruction.is_function_call())
1070 malloc_entry.location_number >= target->location_number &&
1073 log.
error() <<
"Call to malloc at location "
1074 <<
malloc_entry.location_number <<
" falls between goto "
1075 <<
"source location " <<
goto_entry.location_number
1076 <<
" and it's destination at location "
1077 << target->location_number <<
". "
1078 <<
"Unable to complete instrumentation, as this malloc "
1094 log.
error() <<
"Could not find function '" << function
1095 <<
"' in goto-program; not enforcing contracts."
1123 decorated.get_recursive_function_warnings_count() == 0,
1124 "Recursive functions found during inlining");
1134 "Loops remain in function '" +
id2string(function) +
1135 "', assigns clause checking instrumentation cannot be applied.");
1191 const auto &
pragmas = target->source_location().get_pragmas();
1203 const auto &symbol_expr =
1208 ns.
lookup(symbol_expr->get_identifier()).is_parameter)
1212 return !
cfg_info_opt.value().is_local(symbol_expr->get_identifier());
1232 return cfg_info_opt.value().is_not_local_or_dirty_local(
1233 target->decl_symbol().get_identifier());
1249 return cfg_info_opt.value().is_not_local_or_dirty_local(
1250 target->dead_symbol().get_identifier());
1326 log.
warning() <<
"Found a `DEAD` variable " << symbol.get_identifier()
1327 <<
" without corresponding `DECL`, at: "
1358 std::stringstream
ss;
1366 log.
error() <<
"Could not find function '" << function
1367 <<
"' in goto-program; not enforcing contracts."
1377 sl.set_file(
"instrumented for code contracts");
1388 "There should be no existing function called " +
ss.str() +
1389 " in the symbol table because that name is a mangled name");
1395 "There should be no function called " +
id2string(function) +
1396 " in the function map because that function should have had its"
1402 "There should be a function called " +
ss.str() +
1403 " in the function map because we inserted a fresh goto-program"
1404 " with that mangled name");
1459 skip->source_location(),
1473 goto_functionst::function_mapt::iterator
f_it =
1478 for(
const auto &
parameter :
gf.parameter_identifiers)
1484 skip->source_location(),
1492 call.arguments().push_back(p);
1498 visitor.create_declarations();
1513 visitor.update_requires(assumption);
1521 if(!ensures.is_true())
1532 assertion.add_source_location() = ensures.source_location();
1536 .source_location_nonconst()
1537 .set_comment(
"Check ensures clause");
1539 .source_location_nonconst()
1551 if(ensures.is_not_nil())
1564 dest.destructive_insert(
dest.instructions.begin(), check);
1578 if(
ins->is_function_call())
1585 auto found = std::find(
1591 goto_function.first,
1592 ins->source_location(),
1593 goto_function.second.body,
1629 log.
error() <<
"Could not find function '" << function
1630 <<
"' in goto-program; not enforcing 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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Stores information about a goto function computed from its CFG, together with a target iterator into ...
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.
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...
bool replace_calls(const std::set< std::string > &)
Replace all calls to each function in the list with that function's contract.
bool apply_function_contract(const irep_idt &function, const source_locationt &location, goto_programt &function_body, goto_programt::targett &target)
Replaces function calls with assertions based on requires clauses, non-deterministic assignments for ...
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 apply_loop_contracts()
symbol_tablet & symbol_table
void instrument_call_statement(goto_programt::targett &instruction_it, const irep_idt &function, goto_programt &body, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt)
Inserts an assertion into program immediately before the function call at instruction_it,...
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...
bool check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
bool enforce_contract(const irep_idt &function)
Enforce contract of a single function.
std::unordered_set< irep_idt > summarized
void check_frame_conditions(const irep_idt &function, goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, instrument_spec_assignst &instrument_spec_assigns, skipt skip_parameter_assigns, optionalt< cfg_infot > &cfg_info_opt)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
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::targett &instruction_it, goto_programt &program, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt)
Inserts an assertion into program immediately before the assignment instruction_it,...
void check_apply_loop_contracts(const irep_idt &function_name, 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)
goto_functionst & goto_functions
skipt
Tells wether to skip or not skip an action.
bool enforce_contracts(const std::set< std::string > &functions)
Turn requires & ensures into assumptions and assertions for each of the named 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
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
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...
This class represents an instruction in the GOTO intermediate representation.
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_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
instructionst::const_iterator const_targett
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())
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())
This class represents a node in a directed graph.
Class to generate havocking instructions for target expressions of a function contract's assign claus...
A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_obje...
const exprt & expression() const
Decorator for message_handlert that keeps track of warnings occuring when inlining a function.
void print(unsigned level, const std::string &message) override
unsigned get_verbosity() const
void print(unsigned level, const jsont &json) override
void set_verbosity(unsigned _verbosity)
void print(unsigned level, const std::string &message, const source_locationt &location) override
void flush(unsigned i) override
void print(unsigned level, const xmlt &xml) override
inlining_decoratort(message_handlert &_wrapped)
unsigned int get_recursive_function_warnings_count()
message_handlert & wrapped
void print(unsigned level, const structured_datat &data) override
std::string command(unsigned i) const override
Create an ECMA-48 SGR (Select Graphic Rendition) command.
std::size_t get_message_count(unsigned level) const
unsigned int recursive_function_warnings_count
void parse_message(const std::string &message)
A class that generates instrumentation for assigns clause checking.
const irep_idt & id() const
void set_verbosity(unsigned _verbosity)
virtual void print(unsigned level, const std::string &message)=0
std::size_t get_message_count(unsigned level) const
unsigned get_verbosity() const
virtual std::string command(unsigned) const
Create an ECMA-48 SGR (Select Graphic Rendition) command.
virtual void flush(unsigned)=0
message_handlert & get_message_handler()
mstreamt & warning() 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 expression or type symbols by an expression or type, respectively.
Predicate to be used with the exprt::visit() function.
bool found_return_value()
A side_effect_exprt that returns a non-deterministically chosen value.
A way of representing nested key/value data.
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.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
irep_idt mode
Language mode.
The Boolean constant true.
bool has_disable_assigns_check_pragma(const goto_programt::const_targett &target)
Returns true iff the target instruction is tagged with a 'CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK' prag...
bool must_track_dead(const goto_programt::const_targett &target, const optionalt< cfg_infot > &cfg_info_opt)
Returns true iff a DEAD x must be processed to upate the local write set.
bool must_check_assign(const goto_programt::const_targett &target, code_contractst::skipt skip_parameter_assigns, const namespacet ns, const optionalt< cfg_infot > cfg_info_opt)
Returns true iff an ASSIGN lhs := rhs instruction must be instrumented.
bool must_track_decl(const goto_programt::const_targett &target, const optionalt< cfg_infot > &cfg_info_opt)
Returns true iff a DECL x must be added to the local write set.
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.
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Transitively inline all function calls made from a particular function.
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
const code_function_callt & to_code_function_call(const codet &code)
#define Forall_goto_program_instructions(it, program)
A Template Class for Graphs.
Havoc function assigns clauses.
Utilities for building havoc code for expressions.
std::set< exprt > assignst
Specify write set in function contracts.
const std::string & id2string(const irep_idt &d)
bool is_false(const literalt &l)
bool is_true(const literalt &l)
Field-insensitive, location-sensitive bitvector analysis.
Field-insensitive, location-sensitive may-alias analysis.
void get_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
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.
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
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 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 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)
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &location, const irep_idt &mode, symbol_table_baset &symtab, std::string suffix, bool is_auxiliary)
Adds a fresh and uniquely named symbol to the symbol table.
bool is_loop_free(const goto_programt &goto_program, namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.
exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
Generate a validity check over all dereferences in an expression.
void insert_before_swap_and_advance(goto_programt &destination, goto_programt::targett &target, goto_programt &payload)
Insert a goto program before a target instruction iterator and advance the iterator.
void simplify_gotos(goto_programt &goto_program, namespacet &ns)
Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SK...
void add_pragma_disable_assigns_check(source_locationt &location)
Adds a pragma on a source_locationt to disable inclusion checking.
exprt generate_lexicographic_less_than_check(const std::vector< symbol_exprt > &lhs, const std::vector< symbol_exprt > &rhs)
Generate a lexicographic less-than comparison over ordered tuples.
#define CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK