62 const auto loop_number =
loop_end->loop_number;
141 std::string(
ENTERED_LOOP) +
"__" + std::to_string(loop_number),
228 log.
debug() <<
"No loop assigns clause provided. Inferred targets: {";
247 log.
error() <<
"Failed to infer variables being modified by the loop at "
249 <<
".\nPlease specify an assigns clause.\nReason:"
292 assertion.add_source_location().set_comment(
293 "Check loop invariant before entry");
303 goto_function.body.destructive_insert(
380 log.
error() <<
"Loop contracts are unsupported on do/while loops: "
404 goto_function.body.destructive_insert(
412 goto_function.body.destructive_insert(
446 assertion.add_source_location().set_comment(
447 "Check that loop invariant is preserved");
475 "Check decreases clause on loop iteration");
500 std::set<goto_programt::targett, goto_programt::target_less_than>
504 for(
const auto &t : loop)
521 "Check that loop instrumentation was not truncated");
548 it.is_function_call() && it.call_function().id() ==
ID_symbol &&
554 it.source_location());
604 "front-end should have rejected re-declarations with a different type");
642 if(target->call_lhs().is_not_nil())
657 type.c_ensures().begin(),
658 type.c_ensures().end(),
660 return has_symbol_expr(
661 to_lambda_expr(e).where(), CPROVER_PREFIX
"return_value", true);
670 "ignored_return_value",
704 for(
const auto &clause : type.c_requires())
710 _location.set_comment(std::string(
"Check requires clause of ")
711 .append(target_function.
c_str())
713 .append(function.
c_str()));
722 is_fresh.update_requires(c_requires);
730 for(
auto clause : type.c_ensures())
743 for(
auto &target : type.c_assigns())
766 auto &loc =
call_ret.source_location();
785 if(clause.is_false())
788 std::string(
"Attempt to assume false at ")
789 .append(clause.source_location().as_string())
790 .append(
".\nPlease update ensures clause to avoid vacuity."));
793 _location.set_comment(
"Assume ensures clause");
812 target->output(mstream);
813 mstream << messaget::eom;
841 goto_function.body.instructions.begin(),
842 goto_function.body.instructions.end(),
844 return instruction.is_backwards_goto();
855 decorated.get_recursive_call_set().size() == 0,
856 "Recursive functions found during inlining");
884 const exprt &assigns,
886 const exprt &decreases)
902 std::pair<goto_programt::targett, natural_loops_mutablet::loopt>,
920 t->is_goto() && t->get_target() ==
loop_head &&
921 t->location_number >
loop_end->location_number)
927 log.
error() <<
"Could not find end of the loop starting at: "
943 loop_head->location_number > i->location_number ||
944 i->location_number >
loop_end->location_number)
948 mstream <<
"Computed loop at " <<
loop_head->source_location()
949 <<
"contains an instruction beyond [loop_head, loop_end]:"
991 <<
"The loop at " <<
loop_head->source_location().as_string()
992 <<
" does not have an invariant in its contract.\n"
993 <<
"Hence, a default invariant ('true') is being used.\n"
994 <<
"This choice is sound, but verification may fail"
995 <<
" if it is be too weak to prove the desired properties."
1005 <<
loop_head->source_location().as_string()
1006 <<
" does not have a decreases clause in its contract.\n"
1007 <<
"Termination of this loop will not be verified."
1042 <<
"Overlapping loops at:\n"
1046 <<
"\nLoops must be nested or sequential for contracts to be "
1067 <<
"Inner loop at: " <<
loop_node.head_target->source_location()
1068 <<
" does not have contracts, but an enclosing loop does.\n"
1069 <<
"Please provide contracts for this loop, or unwind it first."
1104 std::to_string(
loop_node.end_target->loop_number) +
1129 "Function '" +
id2string(function) +
"'must exist in the goto program");
1164 "Loops remain in function '" +
id2string(function) +
1165 "', assigns clause checking instrumentation cannot be applied.");
1185 ns.lookup(
param.get_identifier()).symbol_expr());
1220 std::stringstream
ss;
1228 "Function to replace must exist in the program.");
1235 sl.set_file(
"instrumented for code contracts");
1245 "There should be no existing function called " +
ss.str() +
1246 " in the symbol table because that name is a mangled name");
1252 "There should be no function called " +
id2string(function) +
1253 " in the function map because that function should have had its"
1259 "There should be a function called " +
ss.str() +
1260 " in the function map because we inserted a fresh goto-program"
1261 " with that mangled name");
1320 goto_functionst::function_mapt::iterator
f_it =
1325 for(
const auto &
parameter :
gf.parameter_identifiers)
1341 call.arguments().push_back(p);
1348 visitor.create_declarations();
1349 visitor.add_memory_map_decl(check);
1352 for(
const auto &clause :
code_type.c_requires())
1359 std::string(
"Attempt to assume false at ")
1360 .append(clause.source_location().as_string())
1361 .append(
".\nPlease update requires clause to avoid vacuity."));
1364 _location.set_comment(
"Assume requires clause");
1373 visitor.update_requires(c_requires);
1381 for(
auto clause :
code_type.c_ensures())
1398 _location.set_comment(
"Check ensures clause");
1414 return_stmt.value().return_value(), source_location));
1418 visitor.add_memory_map_dead(check);
1428 const std::set<std::string> &functions)
const
1430 for(
const auto &function : functions)
1437 "Function '" + function +
"' was not found in the GOTO program.");
1444 if(to_replace.empty())
1455 if(
ins->is_function_call())
1462 auto found = std::find(
1463 to_replace.begin(), to_replace.end(),
id2string(called_function));
1464 if(
found == to_replace.end())
1468 goto_function.first,
1469 ins->source_location(),
1470 goto_function.second.body,
1488 log.
status() <<
"Adding nondeterministic initialization "
1489 "of static/global variables."
1512 goto_function.body.instructions.begin();
1513 it_instr != goto_function.body.instructions.end();
1526 const auto &assign_lhs =
1529 id2string(assign_lhs->get_identifier()),
1543 const auto &assign_lhs =
1546 id2string(assign_lhs->get_identifier()),
1570 log.
status() <<
"Enforcing contracts" << messaget ::eom;
1577 log.
status() <<
"Adding nondeterministic initialization "
1578 "of static/global variables."
API to expression classes that are internal to the C frontend.
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Classes providing CFG-based information about symbols to guide simplifications in function and loop a...
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
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...
A non-fatal assertion, which checks a condition then permits execution to continue.
A goto_instruction_codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
void 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 enforce_contract(const irep_idt &function)
Enforce contract of a single function.
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, goto_programt::targett loop_end, const loopt &loop, exprt assigns_clause, exprt invariant, exprt decreases_clause, const irep_idt &mode)
void apply_loop_contract(const irep_idt &function, goto_functionst::goto_functiont &goto_function)
Apply loop contracts, whenever available, to all loops in function.
void check_all_functions_found(const std::set< std::string > &functions) const
Throws an exception if some function functions is found in the program.
void check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
void apply_loop_contracts(const std::set< std::string > &to_exclude_from_nondet_init={})
Applies loop contract transformations.
symbol_tablet & symbol_table
void enforce_contracts(const std::set< std::string > &to_enforce, const std::set< std::string > &to_exclude_from_nondet_init={})
Turn requires & ensures into assumptions and assertions for each of the named functions.
void replace_calls(const std::set< std::string > &to_replace)
Replace all calls to each function in the to_replace set with that function's contract.
std::unordered_set< irep_idt > summarized
std::unordered_set< goto_programt::const_targett, const_target_hash > loop_havoc_set
Loop havoc instructions instrumented during applying loop contracts.
loop_contract_configt loop_contract_config
std::list< std::string > loop_names
Name of loops we are going to unwind.
goto_functionst & goto_functions
std::unordered_map< goto_programt::const_targett, unsigned, const_target_hash > original_loop_number_map
Store the map from instrumented instructions for loop contracts to their original loop numbers.
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...
goto_instruction_codet representation of a function call statement.
goto_instruction_codet representation of a "return from a function" statement.
const parameterst & parameters() const
const typet & return_type() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const char * c_str() const
Base class for all expressions.
std::vector< exprt > operandst
source_locationt & add_source_location()
The Boolean constant false.
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
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())
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
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())
static instructiont make_assertion(const exprt &g, 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...
Decorator for a message_handlert used during function inlining that collect names of GOTO functions c...
A class that generates instrumentation for assigns clause checking.
Thrown when we can't handle something in an input source file.
void erase_locals(std::set< exprt > &exprs)
message_handlert & get_message_handler()
mstreamt & warning() const
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
mstreamt & status() 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().
A side_effect_exprt that returns a non-deterministically chosen value.
const irep_idt & get_function() const
const irep_idt & get_line() const
const irep_idt & get_property_class() const
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
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.
The Boolean constant true.
static void generate_contract_constraints(symbol_tablet &symbol_table, goto_convertt &converter, exprt &instantiated_clause, const irep_idt &mode, const std::function< void(goto_programt &)> &is_fresh_update, goto_programt &program, const source_locationt &location)
This function generates instructions for all contract constraint, i.e., assumptions and assertions ba...
static const code_with_contract_typet & get_contract(const irep_idt &function, const namespacet &ns)
static void throw_on_unsupported(const goto_programt &program)
Throws an exception if a contract uses unsupported constructs like:
Verify and use annotated invariants and pre/post-conditions.
static const std::map< dfcc_funt, int > to_unwind
set of functions that need to be unwound to assigns clause size with corresponding loop identifiers.
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 ...
#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
std::optional< code_with_contract_typet > get_contract(const irep_idt &function_identifier, const namespacet &ns)
void add_pragma_disable_assigns_check(source_locationt &location)
Adds a pragma on a source_locationt to disable inclusion checking.
Specify write set in function contracts.
const std::string & id2string(const irep_idt &d)
Field-insensitive, location-sensitive may-alias analysis.
natural_loops_mutablet::natural_loopt loopt
API to expression classes for 'mathematical' expressions.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
Predicates to specify memory footprint in function contracts.
static void nondet_static(const namespacet &ns, goto_modelt &goto_model, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#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 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.
A total order over targett and const_targett.
bool unwind_transformed_loops
void generate_history_variables_initialization(symbol_table_baset &symbol_table, exprt &clause, const irep_idt &mode, goto_programt &program)
This function generates all the instructions required to initialize history variables.
bool is_assignment_to_instrumented_variable(const goto_programt::const_targett &target, std::string var_name)
Return true if target is an assignment to an instrumented variable with name var_name.
void insert_before_and_update_jumps(goto_programt &destination, goto_programt::targett &target, const goto_programt::instructiont &i)
Insert a goto instruction before a target instruction iterator and update targets of all jumps that p...
void infer_loop_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
Infer loop assigns using alias analysis result local_may_alias.
bool is_loop_free(const goto_programt &goto_program, const namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.
exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
Extract loop assigns from annotated loop end.
replace_history_parametert replace_history_loop_entry(symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode)
This function recursively identifies the "loop_entry" expressions within expr and replaces them with ...
bool is_transformed_loop_head(const goto_programt::const_targett &target)
Return true if target is the head of some transformed loop.
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 widen_assigns(assignst &assigns, const namespacet &ns)
Widen expressions in assigns with the following strategy.
void simplify_gotos(goto_programt &goto_program, const namespacet &ns)
Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SK...
exprt get_loop_invariants(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop invariants from annotated loop end.
bool is_transformed_loop_end(const goto_programt::const_targett &target)
Return true if target is the end of some transformed loop.
exprt get_loop_decreases(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop decreases from annotated loop end.
unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix)
Convert the suffix digits right after prefix of str into unsigned.
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 IN_LOOP_HAVOC_BLOCK