#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 dependency graph for dfcc_cfg_info.cpp:Go to the source code of this file.
Classes | |
| struct | contract_clausest |
Functions | |
| 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. 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, const bool check_side_effect) |
| 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 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_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, 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 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, 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 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 130 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 156 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 269 of file dfcc_cfg_info.cpp.
◆ gen_dfcc_loop_info()
|
static |
Definition at line 393 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 269 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 34 of file dfcc_cfg_info.cpp.
◆ is_assigned()
Definition at line 227 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 786 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 176 of file dfcc_cfg_info.cpp.
