36 return static_cast<const exprt &
>(
37 latch_target->condition().find(ID_C_spec_assigns))
45 return static_cast<const exprt &
>(
46 latch_target->condition().find(ID_C_spec_loop_invariant))
54 return static_cast<const exprt &
>(
55 latch_target->condition().find(ID_C_spec_decreases))
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: {"
123 std::optional<goto_programt::targett>
138 std::optional<goto_programt::targett>
141 std::optional<goto_programt::targett> result = std::nullopt;
157 const std::size_t loop_idx,
158 const bool must_have_contract)
160 const auto &node = loop_nesting_graph[loop_idx];
167 loop_nesting_graph, pred_idx,
has_contract(node.latch));
168 if(result.has_value())
180 for(std::size_t idx = 0; idx < loop_nesting_graph.
size(); idx++)
185 if(result.has_value())
199 for(
const auto &idx : loop_nesting_graph.
topsort())
201 auto &node = loop_nesting_graph[idx];
202 auto &head = node.head;
203 auto &latch = node.latch;
204 auto &instruction_iterators = node.instructions;
213 if(loop_id_opt.has_value())
218 if(t != head && t != latch)
221 if(t->is_goto() && !instruction_iterators.contains(t->get_target()))
228 auto top_level_id = loop_nesting_graph.
size();
237 if(loop_id_opt.has_value())
250 for(
const auto &expr : assigns)
253 for(
const auto &root_object : root_objects)
256 root_object.id() == ID_symbol &&
257 expr_try_dynamic_cast<symbol_exprt>(root_object)->get_identifier() ==
279 const std::size_t loop_id)
281 std::unordered_set<irep_idt> loop_locals;
282 for(
const auto &target : loop_nesting_graph[loop_id].instructions)
286 target->is_decl() && loop_id_opt.has_value() &&
287 loop_id_opt.value() == loop_id)
289 loop_locals.insert(target->decl_symbol().get_identifier());
309 const std::vector<std::size_t> &inner_loops_ids,
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);
324 for(
const auto inner_loop_id : inner_loops_ids)
326 if(
is_assigned(dirty, ident, loop_info_map.at(inner_loop_id).assigns))
327 tracked.insert(ident);
349 const std::size_t loop_id,
356 const auto &loop = loop_nesting_graph[loop_id];
368 !assigns_clauses.empty())
370 if(invariant_clauses.empty())
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."
389 if(!assigns_clauses.empty())
391 for(
auto &operand : assigns_clauses)
393 result.
assigns.insert(operand);
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 {";
405 for(
const auto &expr : inferred)
409 log.warning() <<
", ";
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,
442 std::unordered_set<irep_idt> loop_locals =
460 std::set<std::size_t> inner_loops;
463 inner_loops.insert(pred_idx);
466 std::set<std::size_t> outer_loops;
469 outer_loops.insert(succ_idx);
472 auto &loop = loop_nesting_graph[loop_id];
473 const auto cbmc_loop_number = loop.latch->loop_number;
481 loop.head->source_location());
488 "__address_of_write_set_loop_" +
std::to_string(cbmc_loop_number),
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());
537 auto topsorted = loop_nesting_graph.
topsort();
539 for(
const auto idx : topsorted)
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;
648 loop_id_opt.has_value() &&
650 auto loop_id = loop_id_opt.value();
661 const std::unordered_set<irep_idt> &
666 loop_id_opt.has_value() &&
668 auto loop_id = loop_id_opt.value();
679 const std::unordered_set<irep_idt> &
684 loop_id_opt.has_value() &&
686 auto loop_id = loop_id_opt.value();
701 return outer_loop_opt.has_value()
713 const std::optional<std::size_t>
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)
772 std::unordered_set<irep_idt> root_idents;
773 for(
const auto &expr : root_objects)
775 if(expr.id() != ID_symbol)
795 if(root_objects.size() == 1)
804 "` in assignment refers to a cprover symbol and something else.");
807 root_idents.insert(
id);
812 bool some_non_local =
false;
814 bool some_local_not_tracked =
false;
816 bool all_local_not_tracked =
true;
818 bool all_local_tracked =
true;
819 for(
const auto &root_ident : root_idents)
821 bool loc = local.find(root_ident) != local.end();
822 bool tra = tracked.find(root_ident) != tracked.end();
823 bool local_tracked = loc && tra;
824 bool local_not_tracked = loc && !tra;
825 some_non_local |= !loc;
826 some_local_not_tracked |= local_not_tracked;
827 all_local_not_tracked &= local_not_tracked;
828 all_local_tracked &= local_tracked;
836 if(some_local_not_tracked)
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.");
856 if(all_local_not_tracked || all_local_tracked)
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();
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
const std::optional< 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...
const std::vector< std::size_t > & get_loops_toposorted() const
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
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.
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.
std::optional< goto_programt::targett > find_latch(goto_programt &goto_program) const
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.
std::optional< 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...
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
A generic directed graph with a parametric node type.
std::vector< node_indext > get_predecessors(const node_indext &n) const
std::vector< node_indext > get_successors(const node_indext &n) const
std::list< node_indext > topsort() const
Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph.
Thrown when we can't handle something in an input source file.
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const irep_idt & get_identifier() const
The symbol table base class interface.
The Boolean constant true.
static std::optional< 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 is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
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 const exprt::operandst & get_decreases(const goto_programt::const_targett &latch_target)
Extracts the decreases clause expression from the latch condition.
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_invariants(const goto_programt::const_targett &latch_target)
Extracts the invariant 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.
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 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 std::optional< 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 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).
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.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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...