Describes a single loop for the purpose of DFCC loop contract instrumentation. More...
#include <dfcc_cfg_info.h>
Collaboration diagram for dfcc_loop_infot:Public Member Functions | |
| dfcc_loop_infot (std::size_t loop_id, std::size_t cbmc_loop_id, const std::set< exprt > &assigns, exprt invariant, exprt::operandst decreases, const std::unordered_set< irep_idt > &local, const std::unordered_set< irep_idt > &tracked, std::set< std::size_t > inner_loops, std::set< std::size_t > outer_loops, symbol_exprt write_set_var, symbol_exprt addr_of_write_set_var) | |
| void | output (std::ostream &out) const |
Prints a textual representation of the struct to out. More... | |
| 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 the given program. More... | |
| std::optional< goto_programt::targett > | find_latch (goto_programt &goto_program) const |
| const bool | must_skip () const |
| Returns true if the loop has no invariant and no decreases clause and its instrumentation must be skipped. More... | |
Public Attributes | |
| const std::size_t | loop_id |
| Loop identifier assigned by DFCC to this loop. More... | |
| const std::size_t | cbmc_loop_id |
| Loop identifier assigned to this loop by traditional CBMC loop numbering. More... | |
| const std::set< exprt > | assigns |
| Set of targets assigned by the loop, either user-provided or inferred. More... | |
| const exprt | invariant |
| Loop invariant expression. More... | |
| const exprt::operandst | decreases |
| Decreases clause expression. More... | |
| const std::unordered_set< irep_idt > | local |
| Set of local identifiers locally DECL in loop instructions, excluding identifiers declared in nested loops. More... | |
| const std::unordered_set< irep_idt > | tracked |
| Subset of locals that must be tracked in the loop's write set. More... | |
| const std::set< std::size_t > | inner_loops |
| Integer identifiers of inner loops of that loop. More... | |
| const std::set< std::size_t > | outer_loops |
| Integer identifier of the outer loop(s) if they exists. More... | |
| const symbol_exprt | write_set_var |
| Symbol representing the stack-allocated write set object for this loop. More... | |
| const symbol_exprt | addr_of_write_set_var |
| Symbol representing pointer to the stack allocated write set object for this loop. More... | |
Detailed Description
Describes a single loop for the purpose of DFCC loop contract instrumentation.
Definition at line 39 of file dfcc_cfg_info.h.
Constructor & Destructor Documentation
◆ dfcc_loop_infot()
|
inline |
Definition at line 42 of file dfcc_cfg_info.h.
Member Function Documentation
◆ find_head()
| std::optional< goto_programt::targett > dfcc_loop_infot::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 the given program.
The goto program passed as argument to this method must be the program from which that instance was initially generated. Technically it will not be the exact same program because the whole point of contract instrumentation is to turn the program into a different program by adding new instructions and turning loops into non-loops. However, when the program given as argument is the one obtained from the initial program through DFCC instrumentation steps then the first instruction from the start of the program that has the head tag for the same loop id corresponds to the head instruction of the loop that initially had this loop id in the not-yet instrumented program. This is because since the tags are attached to the instruction's source locations and instrumenting instructions after or before the original head instruction does not affect the head instruction itself and preserves the structure of the goto program's CFG that is relevant for dominator properties, which is what loop heads are (the loop head dominates ther nodes of the loop when looking from outside of the loop). If the instruction itself was instrumented by adding instructions right before or right after it while copying its source location to the inserted instructions then it is not the head instruction anymore, however the first instruction found from the start of the goto program that carries this same head tag is head instruction of the loop. If the program was instrumented in any other manner that might not maintain or copy the source location tags properly then nothing of the argument above is expected to hold anymore and you then use this method at your own risk.
Definition at line 99 of file dfcc_cfg_info.cpp.
◆ find_latch()
| std::optional< goto_programt::targett > dfcc_loop_infot::find_latch | ( | goto_programt & | goto_program | ) | const |
Definition at line 114 of file dfcc_cfg_info.cpp.
◆ must_skip()
|
inline |
Returns true if the loop has no invariant and no decreases clause and its instrumentation must be skipped.
Definition at line 151 of file dfcc_cfg_info.h.
◆ output()
| void dfcc_loop_infot::output | ( | std::ostream & | out | ) | const |
Prints a textual representation of the struct to out.
Definition at line 43 of file dfcc_cfg_info.cpp.
Member Data Documentation
◆ addr_of_write_set_var
| const symbol_exprt dfcc_loop_infot::addr_of_write_set_var |
Symbol representing pointer to the stack allocated write set object for this loop.
This is the one that must be passed as argument to write set functions.
Definition at line 147 of file dfcc_cfg_info.h.
◆ assigns
| const std::set<exprt> dfcc_loop_infot::assigns |
Set of targets assigned by the loop, either user-provided or inferred.
Definition at line 118 of file dfcc_cfg_info.h.
◆ cbmc_loop_id
| const std::size_t dfcc_loop_infot::cbmc_loop_id |
Loop identifier assigned to this loop by traditional CBMC loop numbering.
Definition at line 115 of file dfcc_cfg_info.h.
◆ decreases
| const exprt::operandst dfcc_loop_infot::decreases |
Decreases clause expression.
Definition at line 124 of file dfcc_cfg_info.h.
◆ inner_loops
| const std::set<std::size_t> dfcc_loop_infot::inner_loops |
Integer identifiers of inner loops of that loop.
Definition at line 136 of file dfcc_cfg_info.h.
◆ invariant
| const exprt dfcc_loop_infot::invariant |
Loop invariant expression.
Definition at line 121 of file dfcc_cfg_info.h.
◆ local
| const std::unordered_set<irep_idt> dfcc_loop_infot::local |
Set of local identifiers locally DECL in loop instructions, excluding identifiers declared in nested loops.
Definition at line 128 of file dfcc_cfg_info.h.
◆ loop_id
| const std::size_t dfcc_loop_infot::loop_id |
Loop identifier assigned by DFCC to this loop.
Definition at line 112 of file dfcc_cfg_info.h.
◆ outer_loops
| const std::set<std::size_t> dfcc_loop_infot::outer_loops |
Integer identifier of the outer loop(s) if they exists.
Definition at line 139 of file dfcc_cfg_info.h.
◆ tracked
| const std::unordered_set<irep_idt> dfcc_loop_infot::tracked |
Subset of locals that must be tracked in the loop's write set.
A local must be tracked if it is dirty or might be assigned by one of the inner loops of that loop.
Definition at line 133 of file dfcc_cfg_info.h.
◆ write_set_var
| const symbol_exprt dfcc_loop_infot::write_set_var |
Symbol representing the stack-allocated write set object for this loop.
Definition at line 142 of file dfcc_cfg_info.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h
- /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp
