Loading...

Searching...

No Matches

Public Member Functions | Public Attributes | List of all members

dfcc_loop_infot Class Reference

Describes a single loop for the purpose of DFCC loop contract instrumentation. More...

#include <dfcc_cfg_info.h>

+ Collaboration diagram for dfcc_loop_infot:

[フレーム]

[legend]

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.

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.

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.

Public Attributes

const std::size_t loop_id

Loop identifier assigned by DFCC to this loop.

const std::size_t cbmc_loop_id

Loop identifier assigned to this loop by traditional CBMC loop numbering.

const std::set< exprt > assigns

Set of targets assigned by the loop, either user-provided or inferred.

const exprt invariant

Loop invariant expression.

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 loops.

const std::unordered_set< irep_idt > tracked

Subset of locals that must be tracked in the loop's write set.

const std::set< std::size_t > inner_loops

Integer identifiers of inner loops of that loop.

const std::set< std::size_t > outer_loops

Integer identifier of the outer loop(s) if they exists.

const symbol_exprt write_set_var

Symbol representing the stack-allocated write set object for this loop.

const symbol_exprt addr_of_write_set_var

Symbol representing pointer to the stack allocated write set object for this loop.

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()

dfcc_loop_infot::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

)

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()

const bool dfcc_loop_infot::must_skip ( ) const

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