36 return static_cast<const exprt &
>(
45 return static_cast<const exprt &
>(
54 return static_cast<const exprt &
>(
70 out <<
"dfcc_loop_id: " <<
loop_id <<
"\n";
93 out <<
format(expr) <<
", ";
99 out <<
"decreases: {";
102 out <<
format(expr) <<
", ";
106 out <<
"inner loops: {"
114 out <<
"outer loops: {"
168 if(result.has_value())
185 if(result.has_value())
202 auto &head = node.head;
203 auto &latch = node.latch;
218 if(t != head && t != latch)
250 for(
const auto &expr : assigns)
279 const std::size_t loop_id)
289 loop_locals.insert(target->decl_symbol().get_identifier());
310 const std::unordered_set<irep_idt> &locals,
312 const std::map<std::size_t, dfcc_loop_infot> &loop_info_map)
314 std::unordered_set<irep_idt> tracked;
315 for(
const auto &
ident : locals)
319 tracked.insert(
ident);
327 tracked.insert(
ident);
349 const std::size_t loop_id,
375 log.
warning() <<
"No invariant provided for loop " << function_id <<
"."
376 << loop.latch->loop_number <<
" at "
377 << loop.head->source_location()
378 <<
". Using 'true' as a sound default invariant. Please "
379 "provide an invariant the default is too weak."
400 local_may_alias, loop.instructions, loop.head->source_location(), ns);
401 log.
warning() <<
"No assigns clause provided for loop " << function_id
402 <<
"." << loop.latch->loop_number <<
" at "
403 << loop.head->source_location() <<
". The inferred set {";
414 log.
warning() <<
"} might be incomplete or imprecise, please provide an "
415 "assigns clause if the analysis fails."
422 log.
warning() <<
"No decrease clause provided for loop " << function_id
423 <<
"." << loop.latch->loop_number <<
" at "
424 << loop.head->source_location()
433 const std::size_t loop_id,
435 const std::map<std::size_t, dfcc_loop_infot> &loop_info_map,
460 std::set<std::size_t> inner_loops;
466 std::set<std::size_t> outer_loops;
481 loop.head->source_location());
489 loop.head->source_location());
502 addr_of_write_set_var};
508 const exprt &top_level_write_set,
513 : function_id(function_id),
514 goto_function(goto_function),
515 top_level_write_set(top_level_write_set),
530 "Found loop without contract nested in a loop with a "
532 "provide a contract or unwind this loop before applying loop "
534 head.value()->source_location());
601 out <<
"// dfcc_cfg_infot for: " <<
function_id <<
"\n";
602 out <<
"// top_level_local: {";
609 out <<
"// top_level_tracked: {";
619 out <<
"// dfcc-loop_id:" << loop.first <<
"\n";
623 head.value()->output(out);
624 out <<
"// latch:\n";
625 latch.value()->output(out);
626 loop.second.output(out);
628 out <<
"// program:\n";
632 out <<
" cbmc-loop-number:" << target->loop_number;
661const std::unordered_set<irep_idt> &
679const std::unordered_set<irep_idt> &
724 std::find(outer_loops.begin(), outer_loops.end(), idx) !=
753 auto &
ident = target->is_decl() ? target->decl_symbol().get_identifier()
754 : target->dead_symbol().get_identifier();
756 return tracked.find(
ident) != tracked.end();
766 const std::unordered_set<irep_idt> &local,
767 const std::unordered_set<irep_idt> &tracked)
804 "` in assignment refers to a cprover symbol and something else.");
821 bool loc = local.find(
root_ident) != local.end();
840 "` in assignment mentions both explicitly and implicitly tracked "
841 "memory locations. DFCC does not yet handle that case, please "
842 "reformulate the assignment into separate assignments to either "
843 "memory locations.");
866 "` in assignment mentions both explicitly and implicitly tracked "
867 "memory locations. DFCC does not yet handle that case, please "
868 "reformulate the assignment into separate assignments to either "
869 "memory locations.");
876 PRECONDITION(target->is_assign() || target->is_function_call());
878 target->is_assign() ? target->assign_lhs() : target->call_lhs();
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...
std::unordered_set< irep_idt > top_level_local
Set of identifiers DECL at top level.
const exprt & top_level_write_set
std::vector< std::size_t > topsorted_loops
Loop identifiers sorted from most deeply nested to less deeply nested.
std::unordered_set< irep_idt > top_level_tracked
Set of identifiers DECL at top level.
bool is_top_level_id(const std::size_t id) const
True iff id is in the valid range for a loop id for this function.
const dfcc_loop_infot & get_loop_info(const std::size_t loop_id) const
Returns the loop info for that loop_id.
void output(std::ostream &out) const
const std::vector< std::size_t > & get_loops_toposorted() const
const optionalt< std::size_t > get_outer_loop_identifier(const std::size_t loop_id) const
Finds the DFCC id of the loop that contains the given loop, returns nullopt when the loop has no oute...
goto_functiont & goto_function
std::vector< std::size_t > top_level_loops
Loop identifiers for top level loops (ie for loops that are not nested in in another loop).
const std::unordered_set< irep_idt > & get_tracked_set(goto_programt::const_targett target) const
Returns the subset of local variable that are explicitly tracked in the write set for the scope where...
bool must_check_lhs(goto_programt::const_targett target) const
True iff the lhs of an assignment must be checked against the ambient write set.
dfcc_cfg_infot(const irep_idt &function_id, goto_functiont &goto_function, const exprt &top_level_write_set, const dfcc_loop_contract_modet loop_contract_mode, symbol_table_baset &symbol_table, message_handlert &message_handler, dfcc_libraryt &library)
const std::unordered_set< irep_idt > & get_local_set(goto_programt::const_targett target) const
Returns the set of local variable for the scope where that target instruction is found.
const exprt & get_outer_write_set(std::size_t loop_id) const
Returns the write set of the outer loop of that loop or the top level write set if that loop has no o...
const exprt & get_write_set(goto_programt::const_targett target) const
Returns the write set variable for that instruction.
bool must_track_decl_or_dead(goto_programt::const_targett target) const
True iff a DECL ident must be tracked in the write set of the loop that contains the DECL.
bool is_valid_loop_id(const std::size_t id) const
True iff id is in the valid range for a loop id for this function.
const irep_idt & function_id
std::map< std::size_t, dfcc_loop_infot > loop_info_map
Map from loop identifier to loop info struct.
bool is_valid_loop_or_top_level_id(const std::size_t id) const
True iff id is in the valid range for a loop id or is equal to the top level id for this function.
Class interface to library types and functions defined in cprover_contracts.c.
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
Describes a single loop for the purpose of DFCC loop contract instrumentation.
const symbol_exprt addr_of_write_set_var
Symbol representing pointer to the stack allocated write set object for this loop.
optionalt< goto_programt::targett > find_head(goto_programt &goto_program) const
Finds the first instruction tagged as loop head and having the same loop identifier as this struct in...
void output(std::ostream &out) const
Prints a textual representation of the struct to out.
const exprt::operandst decreases
Decreases clause expression.
const std::unordered_set< irep_idt > local
Set of local identifiers locally DECL in loop instructions, excluding identifiers declared in nested ...
const std::set< exprt > assigns
Set of targets assigned by the loop, either user-provided or inferred.
const std::size_t cbmc_loop_id
Loop identifier assigned to this loop by traditional CBMC loop numbering.
const std::unordered_set< irep_idt > tracked
Subset of locals that must be tracked in the loop's write set.
const std::size_t loop_id
Loop identifier assigned by DFCC to this loop.
const exprt invariant
Loop invariant expression.
const std::set< std::size_t > outer_loops
Integer identifier of the outer loop(s) if they exists.
const std::set< std::size_t > inner_loops
Integer identifiers of inner loops of that loop.
optionalt< goto_programt::targett > find_latch(goto_programt &goto_program) const
const symbol_exprt write_set_var
Symbol representing the stack-allocated write set object for this loop.
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
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
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.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::iterator targett
instructionst::const_iterator const_targett
Thrown when we can't handle something in an input source file.
Class that provides messages with a built-in verbosity 'level'.
mstreamt & warning() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The symbol table base class interface.
The Boolean constant true.
static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
static std::unordered_set< irep_idt > gen_loop_locals_set(const dfcc_loop_nesting_grapht &loop_nesting_graph, const std::size_t loop_id)
Collect identifiers that are local to this loop only (excluding nested loop).
static void tag_loop_instructions(goto_programt &goto_program, dfcc_loop_nesting_grapht &loop_nesting_graph)
Tags instructions of loops found in loop_nesting_graph with the loop identifier of the innermost loop...
static bool must_check_lhs_from_local_and_tracked(const exprt &lhs, const std::unordered_set< irep_idt > &local, const std::unordered_set< irep_idt > &tracked)
Returns true if the lhs to an assignment must be checked against its write set.
static optionalt< goto_programt::targett > check_has_contract_rec(const dfcc_loop_nesting_grapht &loop_nesting_graph, const std::size_t loop_idx, const bool must_have_contract)
static bool has_contract(const goto_programt::const_targett &latch_target)
Returns true iff some contract clause expression is attached to the latch condition of this loop.
static const exprt::operandst & get_invariants(const goto_programt::const_targett &latch_target)
Extracts the invariant clause expression from the latch condition.
static struct contract_clausest default_loop_contract_clauses(const dfcc_loop_nesting_grapht &loop_nesting_graph, const std::size_t loop_id, const irep_idt &function_id, local_may_aliast &local_may_alias, message_handlert &message_handler, const namespacet &ns)
Generate defaults for all contract clauses of the loop with ID loop_id if at least one type of clause...
static optionalt< goto_programt::targett > check_inner_loops_have_contracts(const dfcc_loop_nesting_grapht &loop_nesting_graph)
Traverses the loop nesting graph from top level loops and checks if all loops nested in loops that ha...
static dfcc_loop_infot gen_dfcc_loop_info(const dfcc_loop_nesting_grapht &loop_nesting_graph, const std::size_t loop_id, const irep_idt &function_id, const std::map< std::size_t, dfcc_loop_infot > &loop_info_map, dirtyt &dirty, local_may_aliast &local_may_alias, message_handlert &message_handler, dfcc_libraryt &library, symbol_table_baset &symbol_table)
static const exprt::operandst & get_assigns(const goto_programt::const_targett &latch_target)
Extracts the assigns clause expression from the latch condition.
static const exprt::operandst & get_decreases(const goto_programt::const_targett &latch_target)
Extracts the decreases clause expression from the latch condition.
static std::unordered_set< irep_idt > gen_tracked_set(const std::vector< std::size_t > &inner_loops_ids, const std::unordered_set< irep_idt > &locals, dirtyt &dirty, const std::map< std::size_t, dfcc_loop_infot > &loop_info_map)
Compute subset of locals that must be tracked in the loop's write set.
Class that computes CFG information about the loop structure of a GOTO function for the purpose of dy...
assignst dfcc_infer_loop_assigns(const local_may_aliast &local_may_alias, const loopt &loop_instructions, const source_locationt &loop_head_location, const namespacet &ns)
Infer a set of assigns clause targets for a natural loop.
bool dfcc_is_cprover_static_symbol(const irep_idt &id)
Returns true iff the symbol is one of the known CPROVER static instrumentation variables or ends with...
Dynamic frame condition checking library loading.
@ WRITE_SET
type of descriptors of assignable/freeable sets of locations
@ WRITE_SET_PTR
type of pointers to descriptors of assignable/freeable sets of locations
dfcc_loop_contract_modet
Enumeration representing the instrumentation mode for loop contracts.
@ NONE
Do not apply loop contracts.
dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program)
Builds a graph instance describing the nesting structure of natural loops in the given goto_program.
Builds a graph describing how loops are nested in a GOTO program.
std::unordered_set< exprt, irep_hash > dfcc_root_objects(const exprt &expr)
Computes a set of root object expressions from an lvalue or assigns clause target expression.
Utility functions that compute root object expressions for assigns clause targets and LHS expressions...
Dynamic frame condition checking utility functions.
Fresh auxiliary symbol creation.
#define Forall_goto_program_instructions(it, program)
std::set< exprt > assignst
Field-insensitive, location-sensitive may-alias analysis.
Compute natural loops in a goto_function.
API to expression classes for Pointers.
#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...
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
exprt::operandst decreases_clauses
contract_clausest(const exprt::operandst &decreases)
static symbol_exprt create_symbol(symbol_table_baset &, const typet &type, const irep_idt &function_id, const std::string &base_name, const source_locationt &source_location)
Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table...