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: {"
98std::optional<goto_programt::targett>
113std::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 &&
260 const std::size_t loop_id)
262 std::unordered_set<irep_idt> loop_locals;
263 for(
const auto &target : loop_nesting_graph[loop_id].instructions)
267 target->is_decl() && loop_id_opt.has_value() &&
268 loop_id_opt.value() == loop_id)
270 loop_locals.insert(target->decl_symbol().get_identifier());
290 const std::vector<std::size_t> &inner_loops_ids,
291 const std::unordered_set<irep_idt> &locals,
293 const std::map<std::size_t, dfcc_loop_infot> &loop_info_map)
295 std::unordered_set<irep_idt> tracked;
296 for(
const auto &ident : locals)
300 tracked.insert(ident);
305 for(
const auto inner_loop_id : inner_loops_ids)
307 if(
is_assigned(dirty, ident, loop_info_map.at(inner_loop_id).assigns))
308 tracked.insert(ident);
330 const std::size_t loop_id,
333 const bool check_side_effect,
338 const auto &loop = loop_nesting_graph[loop_id];
352 !assigns_clauses.empty())
354 if(invariant_clauses.empty())
357 result.invariant_expr = true_exprt{};
359 log.warning() <<
"No invariant provided for loop " << function_id <<
"."
360 << loop.latch->loop_number <<
" at "
361 << loop.head->source_location()
362 <<
". Using 'true' as a sound default invariant. Please "
363 "provide an invariant the default is too weak."
369 result.invariant_expr = conjunction(invariant_clauses);
373 if(!assigns_clauses.empty())
375 for(auto &operand : assigns_clauses)
377 result.assigns.insert(operand);
384 local_may_alias, loop.instructions, loop.head->source_location(), ns);
385 log.warning() <<
"No assigns clause provided for loop " << function_id
386 <<
"." << loop.latch->loop_number <<
" at "
387 << loop.head->source_location() <<
". The inferred set {";
389 for(
const auto &expr : inferred)
393 log.warning() <<
", ";
396 log.warning() <<
format(expr);
398 log.warning() <<
"} might be incomplete or imprecise, please provide an "
399 "assigns clause if the analysis fails."
401 result.assigns.swap(inferred);
404 if(result.decreases_clauses.empty())
406 log.warning() <<
"No decrease clause provided for loop " << function_id
407 <<
"." << loop.latch->loop_number <<
" at "
408 << loop.head->source_location()
409 <<
". Termination will not be checked." << messaget::eom;
417 const std::size_t loop_id,
419 const std::map<std::size_t, dfcc_loop_infot> &loop_info_map,
422 const bool check_side_effect,
427 std::unordered_set<irep_idt> loop_locals =
446 std::set<std::size_t> inner_loops;
449 inner_loops.insert(pred_idx);
452 std::set<std::size_t> outer_loops;
455 outer_loops.insert(succ_idx);
458 auto &loop = loop_nesting_graph[loop_id];
459 const auto cbmc_loop_number = loop.latch->loop_number;
466 "__write_set_loop_" + std::to_string(cbmc_loop_number),
467 loop.head->source_location());
474 "__address_of_write_set_loop_" + std::to_string(cbmc_loop_number),
475 loop.head->source_location());
488 addr_of_write_set_var};
494 const exprt &top_level_write_set,
499 : function_id(function_id),
500 goto_function(goto_function),
501 top_level_write_set(top_level_write_set),
508 messaget log(message_handler);
509 dfcc_check_loop_normal_form(goto_program, log);
510 loop_nesting_graph = build_loop_nesting_graph(goto_program);
512 const auto head = check_inner_loops_have_contracts(
513 loop_nesting_graph, loop_contract_config.check_side_effect);
516 throw invalid_source_file_exceptiont(
517 "Found loop without contract nested in a loop with a "
519 "provide a contract or unwind this loop before applying loop "
521 head.value()->source_location());
524 auto topsorted = loop_nesting_graph.
topsort();
526 for(
const auto idx : topsorted)
528 topsorted_loops.push_back(idx);
547 dirtyt dirty(goto_function);
550 for(
const auto &loop_id : topsorted_loops)
552 loop_info_map.insert(
561 loop_contract_config.check_side_effect,
566 if(loop_nesting_graph.get_successors(loop_id).empty())
567 top_level_loops.push_back(loop_id);
571 top_level_local.insert(
572 goto_function.parameter_identifiers.begin(),
573 goto_function.parameter_identifiers.end());
575 for(
auto target = goto_function.body.instructions.begin();
576 target != goto_function.body.instructions.end();
580 top_level_local.insert(target->decl_symbol().get_identifier());
584 gen_tracked_set(top_level_loops, top_level_local, dirty, loop_info_map);
589 out <<
"// dfcc_cfg_infot for: " <<
function_id <<
"\n";
590 out <<
"// top_level_local: {";
597 out <<
"// top_level_tracked: {";
607 out <<
"// dfcc-loop_id:" << loop.first <<
"\n";
611 head.value()->output(out);
612 out <<
"// latch:\n";
613 latch.value()->output(out);
614 loop.second.output(out);
616 out <<
"// program:\n";
620 out <<
" cbmc-loop-number:" << target->loop_number;
632 const std::size_t loop_id)
const
647 loop_id_opt.has_value() &&
660const std::unordered_set<irep_idt> &
665 loop_id_opt.has_value() &&
667 auto loop_id = loop_id_opt.value();
678const std::unordered_set<irep_idt> &
683 loop_id_opt.has_value() &&
685 auto loop_id = loop_id_opt.value();
700 return outer_loop_opt.has_value()
712const std::optional<std::size_t>
723 std::find(outer_loops.begin(), outer_loops.end(), idx) !=
757 auto &ident = target->is_decl() ? target->decl_symbol().get_identifier()
758 : target->dead_symbol().get_identifier();
760 return tracked.find(ident) != tracked.end();
769 const std::unordered_set<irep_idt> &local,
770 const std::unordered_set<irep_idt> &tracked)
775 std::unordered_set<irep_idt> root_idents;
776 for(
const auto &expr : root_objects)
778 if(expr.id() != ID_symbol)
798 if(root_objects.size() == 1)
807 "` in assignment refers to a cprover symbol and something else.");
810 root_idents.insert(
id);
815 bool some_non_local =
false;
817 bool some_local_not_tracked =
false;
819 bool all_local_not_tracked =
true;
821 bool all_local_tracked =
true;
822 for(
const auto &root_ident : root_idents)
824 bool loc = local.find(root_ident) != local.end();
825 bool tra = tracked.find(root_ident) != tracked.end();
826 bool local_tracked = loc && tra;
827 bool local_not_tracked = loc && !tra;
828 some_non_local |= !loc;
829 some_local_not_tracked |= local_not_tracked;
830 all_local_not_tracked &= local_not_tracked;
831 all_local_tracked &= local_tracked;
839 if(some_local_not_tracked)
843 "` in assignment mentions both explicitly and implicitly tracked "
844 "memory locations. DFCC does not yet handle that case, please "
845 "reformulate the assignment into separate assignments to either "
846 "memory locations.");
859 if(all_local_not_tracked || all_local_tracked)
869 "` in assignment mentions both explicitly and implicitly tracked "
870 "memory locations. DFCC does not yet handle that case, please "
871 "reformulate the assignment into separate assignments to either "
872 "memory locations.");
879 PRECONDITION(target->is_assign() || target->is_function_call());
881 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...
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::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
dfcc_cfg_infot(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)
const std::vector< std::size_t > & get_loops_toposorted() const
goto_functiont & goto_function
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.
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...
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.
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.
static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
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, 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 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 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 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 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 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, 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)
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
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.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
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)
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...
Loop contract configurations.
bool apply_loop_contracts
exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
exprt get_loop_invariants(const goto_programt::const_targett &loop_end, const bool check_side_effect)
exprt get_loop_decreases(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop invariants from annotated loop end.