36 const bool check_side_effect)
45 out <<
"dfcc_loop_id: " <<
loop_id <<
"\n";
68 out <<
format(expr) <<
", ";
74 out <<
"decreases: {";
77 out <<
format(expr) <<
", ";
81 out <<
"inner loops: {"
89 out <<
"outer loops: {"
98 std::optional<goto_programt::targett>
113 std::optional<goto_programt::targett>
116 std::optional<goto_programt::targett> result = std::nullopt;
132 const std::size_t loop_idx,
133 const bool must_have_contract,
134 const bool check_side_effect)
136 const auto &node = loop_nesting_graph[loop_idx];
137 if(must_have_contract && !
has_contract(node.latch, check_side_effect))
147 if(result.has_value())
158 const bool check_side_effect)
160 for(std::size_t idx = 0; idx < loop_nesting_graph.
size(); idx++)
165 loop_nesting_graph, idx,
false, check_side_effect);
166 if(result.has_value())
180 for(
const auto &idx : loop_nesting_graph.
topsort())
182 auto &node = loop_nesting_graph[idx];
183 auto &head = node.head;
184 auto &latch = node.latch;
185 auto &instruction_iterators = node.instructions;
194 if(loop_id_opt.has_value())
199 if(t != head && t != latch)
202 if(t->is_goto() && !instruction_iterators.contains(t->get_target()))
209 auto top_level_id = loop_nesting_graph.
size();
218 if(loop_id_opt.has_value())
231 for(
const auto &expr : assigns)
234 for(
const auto &root_object : root_objects)
237 root_object.id() == ID_symbol &&
238 expr_try_dynamic_cast<symbol_exprt>(root_object)->get_identifier() ==
270 const std::vector<std::size_t> &inner_loops_ids,
271 const std::unordered_set<irep_idt> &locals,
273 const std::map<std::size_t, dfcc_loop_infot> &loop_info_map)
275 std::unordered_set<irep_idt> tracked;
276 for(
const auto &ident : locals)
280 tracked.insert(ident);
285 for(
const auto inner_loop_id : inner_loops_ids)
287 if(
is_assigned(dirty, ident, loop_info_map.at(inner_loop_id).assigns))
288 tracked.insert(ident);
310 const std::size_t loop_id,
313 const bool check_side_effect,
318 const auto &loop = loop_nesting_graph[loop_id];
332 !assigns_clauses.empty())
334 if(invariant_clauses.empty())
339 log.warning() <<
"No invariant provided for loop " << function_id <<
"."
340 << loop.latch->loop_number <<
" at "
341 << loop.head->source_location()
342 <<
". Using 'true' as a sound default invariant. Please "
343 "provide an invariant the default is too weak."
353 if(!assigns_clauses.empty())
355 for(
auto &operand : assigns_clauses)
357 result.
assigns.insert(operand);
363 log.warning() <<
"No assigns clause provided for loop " << function_id
364 <<
"." << loop.latch->loop_number <<
" at "
365 << loop.head->source_location() <<
". The inferred set {";
367 for(
const auto &expr : inferred_assigns)
371 log.warning() <<
", ";
376 log.warning() <<
"} might be incomplete or imprecise, please provide an "
377 "assigns clause if the analysis fails."
379 result.
assigns = inferred_assigns;
384 log.warning() <<
"No decrease clause provided for loop " << function_id
385 <<
"." << loop.latch->loop_number <<
" at "
386 << loop.head->source_location()
395 const std::size_t loop_id,
398 const std::map<std::size_t, dfcc_loop_infot> &loop_info_map,
401 const bool check_side_effect,
410 loop_nesting_graph[loop_id],
418 loop_info_map.find(inner_loop) != loop_info_map.end(),
419 "DFCC should gen_dfcc_loop_info for inner loops first.");
420 for(
const auto &inner_local : loop_info_map.at(inner_loop).local)
422 loop_locals.erase(inner_local);
441 std::set<std::size_t> inner_loops;
444 inner_loops.insert(pred_idx);
447 std::set<std::size_t> outer_loops;
450 outer_loops.insert(succ_idx);
453 auto &loop = loop_nesting_graph[loop_id];
454 const auto cbmc_loop_number = loop.latch->loop_number;
462 loop.head->source_location());
469 "__address_of_write_set_loop_" +
std::to_string(cbmc_loop_number),
470 loop.head->source_location());
483 addr_of_write_set_var};
490 const exprt &top_level_write_set,
495 : function_id(function_id),
496 goto_function(goto_function),
497 top_level_write_set(top_level_write_set),
507 std::map<std::size_t, assignst> inferred_loop_assigns_map;
520 "Found loop without contract nested in a loop with a "
522 "provide a contract or unwind this loop before applying loop "
524 head.value()->source_location());
527 auto topsorted = loop_nesting_graph.
topsort();
529 bool has_loops_with_contracts =
false;
530 for(
const auto idx : topsorted)
538 if(has_loops_with_contracts)
541 inferred_loop_assigns_map,
568 auto inferred_loop_assigns =
569 inferred_loop_assigns_map[loop_nesting_graph[loop_id].latch->loop_number];
579 inferred_loop_assigns,
585 if(loop_nesting_graph.get_successors(loop_id).empty())
608 out <<
"// dfcc_cfg_infot for: " <<
function_id <<
"\n";
609 out <<
"// top_level_local: {";
616 out <<
"// top_level_tracked: {";
626 out <<
"// dfcc-loop_id:" << loop.first <<
"\n";
630 head.value()->output(out);
631 out <<
"// latch:\n";
632 latch.value()->output(out);
633 loop.second.output(out);
635 out <<
"// program:\n";
639 out <<
" cbmc-loop-number:" << target->loop_number;
651 const std::size_t loop_id)
const
666 loop_id_opt.has_value() &&
679 const std::unordered_set<irep_idt> &
684 loop_id_opt.has_value() &&
686 auto loop_id = loop_id_opt.value();
697 const std::unordered_set<irep_idt> &
702 loop_id_opt.has_value() &&
704 auto loop_id = loop_id_opt.value();
719 return outer_loop_opt.has_value()
731 const std::optional<std::size_t>
742 std::find(outer_loops.begin(), outer_loops.end(), idx) !=
776 auto &ident = target->is_decl() ? target->decl_symbol().get_identifier()
777 : target->dead_symbol().get_identifier();
779 return tracked.find(ident) != tracked.end();
788 const std::unordered_set<irep_idt> &local,
789 const std::unordered_set<irep_idt> &tracked)
794 std::unordered_set<irep_idt> root_idents;
795 for(
const auto &expr : root_objects)
797 if(expr.id() != ID_symbol)
817 if(root_objects.size() == 1)
826 "` in assignment refers to a cprover symbol and something else.");
829 root_idents.insert(
id);
834 bool some_non_local =
false;
836 bool some_local_not_tracked =
false;
838 bool all_local_not_tracked =
true;
840 bool all_local_tracked =
true;
841 for(
const auto &root_ident : root_idents)
843 bool loc = local.find(root_ident) != local.end();
844 bool tra = tracked.find(root_ident) != tracked.end();
845 bool local_tracked = loc && tra;
846 bool local_not_tracked = loc && !tra;
847 some_non_local |= !loc;
848 some_local_not_tracked |= local_not_tracked;
849 all_local_not_tracked &= local_not_tracked;
850 all_local_tracked &= local_tracked;
858 if(some_local_not_tracked)
862 "` in assignment mentions both explicitly and implicitly tracked "
863 "memory locations. DFCC does not yet handle that case, please "
864 "reformulate the assignment into separate assignments to either "
865 "memory locations.");
878 if(all_local_not_tracked || all_local_tracked)
888 "` in assignment mentions both explicitly and implicitly tracked "
889 "memory locations. DFCC does not yet handle that case, please "
890 "reformulate the assignment into separate assignments to either "
891 "memory locations.");
898 PRECONDITION(target->is_assign() || target->is_function_call());
900 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::size_t get_first_id_not_skipped_or_top_level_id(const std::size_t loop_id) const
Returns the id of the first outer loop (including this one) that is not skipped, or the top level id.
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...
dfcc_cfg_infot(goto_modelt &goto_model, const irep_idt &function_id, goto_functiont &goto_function, const exprt &top_level_write_set, const loop_contract_configt &loop_contract_config, symbol_table_baset &symbol_table, message_handlert &message_handler, dfcc_libraryt &library)
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.
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 to use for the given instruction Returns the write set for the loop,...
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.
size_t top_level_id() const
Returns the top level ID.
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.
goto_functionst goto_functions
GOTO functions.
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 bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
static std::optional< goto_programt::targett > check_inner_loops_have_contracts(const dfcc_loop_nesting_grapht &loop_nesting_graph, const bool check_side_effect)
Traverses the loop nesting graph from top level loops and checks if all loops nested in loops that ha...
static bool has_contract(const goto_programt::const_targett &latch_target, const bool check_side_effect)
Returns true iff some contract clause expression is attached to the latch condition of this 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 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, const assignst &inferred_assigns, const bool check_side_effect, 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::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 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, goto_functiont &goto_function, const std::map< std::size_t, dfcc_loop_infot > &loop_info_map, dirtyt &dirty, const assignst &inferred_assigns, const bool check_side_effect, message_handlert &message_handler, dfcc_libraryt &library, symbol_table_baset &symbol_table)
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, const bool check_side_effect)
Class that computes CFG information about the loop structure of a GOTO function for the purpose of dy...
std::unordered_set< irep_idt > gen_loop_locals_set(const irep_idt &function_id, goto_functiont &goto_function, const dfcc_loop_nesting_graph_nodet &loop_node, message_handlert &message_handler, const namespacet &ns)
Collect identifiers that are local to this loop.
void dfcc_infer_loop_assigns_for_function(std::map< std::size_t, assignst > &inferred_loop_assigns_map, goto_functionst &goto_functions, const goto_functiont &goto_function, message_handlert &message_handler, const namespacet &ns)
Infer assigns clause targets for loops in goto_function from their instructions and an alias analysis...
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_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...
Loop contract configurations.
bool apply_loop_contracts
exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
Extract loop assigns from annotated loop end.
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.
exprt get_loop_decreases(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop decreases from annotated loop end.