#include "dfcc_cfg_info.h"#include <util/c_types.h>#include <util/format_expr.h>#include <util/fresh_symbol.h>#include <util/pointer_expr.h>#include <analyses/local_may_alias.h>#include <analyses/natural_loops.h>#include <goto-instrument/contracts/utils.h>#include "dfcc_check_loop_normal_form.h"#include "dfcc_infer_loop_assigns.h"#include "dfcc_is_cprover_symbol.h"#include "dfcc_library.h"#include "dfcc_loop_nesting_graph.h"#include "dfcc_loop_tags.h"#include "dfcc_root_object.h"#include "dfcc_utils.h"#include <iostream>
Include dependency graph for dfcc_cfg_info.cpp:Go to the source code of this file.
Classes | |
| struct | contract_clausest |
Functions | |
| static const exprt::operandst & | get_assigns (const goto_programt::const_targett &latch_target) |
| Extracts the assigns clause expression from the latch condition. More... | |
| static const exprt::operandst & | get_invariants (const goto_programt::const_targett &latch_target) |
| Extracts the invariant clause expression from the latch condition. More... | |
| static const exprt::operandst & | get_decreases (const goto_programt::const_targett &latch_target) |
| Extracts the decreases clause expression from the latch condition. More... | |
| 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. More... | |
| 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 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 have contracts also have contracts. More... | |
| 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 it belongs to, and the loop instruction type : head, body, exiting or latch. More... | |
| 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). More... | |
| 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. More... | |
| 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 is defined. More... | |
| 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 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. More... | |
Function Documentation
◆ check_has_contract_rec()
|
static |
Definition at line 155 of file dfcc_cfg_info.cpp.
◆ check_inner_loops_have_contracts()
|
static |
Traverses the loop nesting graph from top level loops and checks if all loops nested in loops that have contracts also have contracts.
Return the head of the first offending loop if it exists, nothing otherwise.
Definition at line 177 of file dfcc_cfg_info.cpp.
◆ default_loop_contract_clauses()
|
static |
Generate defaults for all contract clauses of the loop with ID loop_id if at least one type of clause is defined.
Definition at line 308 of file dfcc_cfg_info.cpp.
◆ gen_dfcc_loop_info()
|
static |
Definition at line 431 of file dfcc_cfg_info.cpp.
◆ gen_loop_locals_set()
|
static |
Collect identifiers that are local to this loop only (excluding nested loop).
Definition at line 277 of file dfcc_cfg_info.cpp.
◆ gen_tracked_set()
|
static |
Compute subset of locals that must be tracked in the loop's write set.
A local must be tracked if it is dirty or if it may be assigned by one of the inner loops. To understand why, just consider what would happen in this situation: The loop-local must be declared in the assigns clause of the inner loop otherwise assigns clause checking for the inner loop would fail (from the point of view of the inner loop, that variable is non-local). Since write sets inclusion checks are performed between a loop and its immediately inner loops, if a loop-local variable that's dirty or that is assigned by an inner loop is not tracked in the loop's write set the inclusion check between the loop write set and inner loop would fail, because the inner loop contains a location that cannot be found in the outer loop's write set.
Definition at line 308 of file dfcc_cfg_info.cpp.
◆ get_assigns()
|
static |
Extracts the assigns clause expression from the latch condition.
Definition at line 34 of file dfcc_cfg_info.cpp.
◆ get_decreases()
|
static |
Extracts the decreases clause expression from the latch condition.
Definition at line 52 of file dfcc_cfg_info.cpp.
◆ get_invariants()
|
static |
Extracts the invariant clause expression from the latch condition.
Definition at line 43 of file dfcc_cfg_info.cpp.
◆ has_contract()
|
static |
Returns true iff some contract clause expression is attached to the latch condition of this loop.
Definition at line 61 of file dfcc_cfg_info.cpp.
◆ is_assigned()
Definition at line 246 of file dfcc_cfg_info.cpp.
◆ must_check_lhs_from_local_and_tracked()
|
static |
Returns true if the lhs to an assignment must be checked against its write set.
The set of locally declared identifiers and the subset of that that are tracked explicitly in the write set are used to make the decision. See comments inside the function for explanations.
Definition at line 764 of file dfcc_cfg_info.cpp.
◆ tag_loop_instructions()
|
static |
Tags instructions of loops found in loop_nesting_graph with the loop identifier of the innermost loop it belongs to, and the loop instruction type : head, body, exiting or latch.
Definition at line 195 of file dfcc_cfg_info.cpp.
