Computes natural loops, enforces normal form conditions, computes the nesting graph, tags each instruction of the function with the loop ID of the innermost loop and loop instruction type. More...

#include <dfcc_cfg_info.h>

Collaboration diagram for dfcc_cfg_infot:

Public Member Functions
	dfcc_cfg_infot (const irep_idt &function_id, goto_functiont &goto_function, const exprt &top_level_write_set, const dfcc_loop_contract_modet loop_contract_mode, symbol_table_baset &symbol_table, message_handlert &message_handler, dfcc_libraryt &library)

void	output (std::ostream &out) const

const dfcc_loop_infot &	get_loop_info (const std::size_t loop_id) const
	Returns the loop info for that loop_id. More...

const exprt &	get_write_set (goto_programt::const_targett target) const
	Returns the write set variable for that instruction. More...

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

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 that target instruction is found. More...

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 outer loop. More...

const std::vector< std::size_t > &	get_loops_toposorted () const

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 outer loop. More...

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

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

const exprt &	get_top_level_write_set () const

const std::unordered_set< irep_idt > &	get_top_level_tracked ()
	Returns the set of top level symbols that must be tracked explicitly in the top level write set of the function. More...

Private Member Functions
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. More...

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

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

Private Attributes
const irep_idt &	function_id

goto_functiont &	goto_function

const exprt &	top_level_write_set

const namespacet	ns

std::vector< std::size_t >	topsorted_loops
	Loop identifiers sorted from most deeply nested to less deeply nested. More...

std::vector< std::size_t >	top_level_loops
	Loop identifiers for top level loops (ie for loops that are not nested in in another loop). More...

std::unordered_set< irep_idt >	top_level_local
	Set of identifiers DECL at top level. More...

std::unordered_set< irep_idt >	top_level_tracked
	Set of identifiers DECL at top level. More...

std::map< std::size_t, dfcc_loop_infot >	loop_info_map
	Map from loop identifier to loop info struct. More...

Detailed Description

Computes natural loops, enforces normal form conditions, computes the nesting graph, tags each instruction of the function with the loop ID of the innermost loop and loop instruction type.

Loop identifiers range from 0 to nof_loops-1. Instructions that are not part of any loop are given nof_loop as id and the top-level instruction kind.

For example, the following function has three loops:

int foo(args, __write_set_ptr_t __write_set) __assigns(A)
{
  do_something();
  while (not_done1()) __assigns(A1) __invariant(I1) __decreases(D1)
  {
    do_something1();
    while (not_done2()) __assigns(A2) __invariant(I2) __decreases(D2)
    {
      do_something2();
    }
 
    if (must_break1())
    {
      while (not_done3()) __assigns(A3) __invariant(I3) __decreases(D3)
      {
        do_something3();
      }
      break;
    }
  }
}

Natural loops are computed at the GOTO instruction level and a loop nesting graph is generated:

foo(A)-------------+
 |                 |
loop1(A1, I1, D1) loop3(A3, I3, D3)
 |
loop2(A2, I2, D2)

GOTO instructions are tagged as follows:

foo /* foo *&zwj;/
   CALL do_something()                   // loop_id:3 tags:{top-level}
   SKIP; // prehead                      // loop_id:3 tags:{top-level}
1: DECL __not_done1 : signedbv[32]       // loop_id:0 tags:{head}
   CALL __not_done1 := not_done1()       // loop_id:0 tags:{body}
   IF ¬(__not_done1 ≠ 0) THEN GOTO 7     // loop_id:0 tags:{body,exiting}
   CALL do_something1()                  // loop_id:0 tags:{body}
   SKIP; // prehead                      // loop_id:0 tags:{body}
2: DECL __not_done2 : signedbv[32]       // loop_id:1 tags:{head}
   CALL __not_done2 := not_done2()       // loop_id:1 tags:{body}
   IF ¬(__not_done2 ≠ 0) THEN GOTO 3     // loop_id:1 tags:{body,exiting}
   CALL do_something2()                  // loop_id:1 tags:{body}
   GOTO 2                                // loop_id:1 tags:{latch}
3: SKIP                                  // loop_id:0 tags:{body}
   DECL __must_break1 : signedbv[32]     // loop_id:0 tags:{body}
   CALL __must_break1 := must_break1()   // loop_id:0 tags:{body}
   IF ¬(__must_break1 ≠ 0) THEN GOTO 6   // loop_id:0 tags:{body}
   SKIP // prehead                       // loop_id:0 tags:{body}
4: DECL __not_done3 : signedbv[32]       // loop_id:2 tags:{head}
   CALL __not_done3 := not_done3()       // loop_id:2 tags:{body}
   IF ¬(__not_done3 ≠ 0) THEN GOTO 5     // loop_id:2 tags:{body,exiting}
   CALL do_something3()                  // loop_id:2 tags:{body}
   GOTO 4                                // loop_id:2 tags:{latch}
5: SKIP                                  // loop_id:0 tags:{body}
   GOTO 7                                // loop_id:0 tags:{body,exiting}
6: SKIP                                  // loop_id:0 tags:{body}
   DEAD __must_break1                    // loop_id:0 tags:{body}
   DEAD __not_done2                      // loop_id:0 tags:{body}
   GOTO 1                                // loop_id:0 tags:{latch}
7: SKIP                                  // loop_id:3 tags:{top-level}
   DEAD __not_done1                      // loop_id:3 tags:{top-level}
   END_FUNCTION                          // loop_id:3 tags:{top-level}

The tags allow to the dynamic frames instrumentation pass to select the write set instance of the specific loop to instrument the instruction, and allow the loop contracts instrumentation pass to robustly locate head, exiting nodes and latch nodes when applying the loop contract transformation.

Definition at line 234 of file dfcc_cfg_info.h.

Constructor & Destructor Documentation

◆ dfcc_cfg_infot()

dfcc_cfg_infot::dfcc_cfg_infot	(	const irep_idt &	function_id,
		goto_functiont &	goto_function,
		const exprt &	top_level_write_set,
		const dfcc_loop_contract_modet	loop_contract_mode,
		symbol_table_baset &	symbol_table,
		message_handlert &	message_handler,
		dfcc_libraryt &	library
	)

Definition at line 505 of file dfcc_cfg_info.cpp.

Member Function Documentation

◆ get_local_set()

const std::unordered_set< irep_idt > & dfcc_cfg_infot::get_local_set ( goto_programt::const_targett target ) const

Returns the set of local variable for the scope where that target instruction is found.

Definition at line 680 of file dfcc_cfg_info.cpp.

◆ get_loop_info()

const dfcc_loop_infot & dfcc_cfg_infot::get_loop_info ( const std::size_t loop_id ) const

Returns the loop info for that loop_id.

Definition at line 707 of file dfcc_cfg_info.cpp.

◆ get_loops_toposorted()

const std::vector<std::size_t>& dfcc_cfg_infot::get_loops_toposorted ( ) const

inline

Definition at line 268 of file dfcc_cfg_info.h.

◆ get_outer_loop_identifier()

const std::optional< std::size_t > dfcc_cfg_infot::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 outer loop.

Definition at line 714 of file dfcc_cfg_info.cpp.

◆ get_outer_write_set()

const exprt & dfcc_cfg_infot::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 outer loop.

Definition at line 697 of file dfcc_cfg_info.cpp.

◆ get_top_level_tracked()

const std::unordered_set<irep_idt>& dfcc_cfg_infot::get_top_level_tracked ( )

inline

Returns the set of top level symbols that must be tracked explicitly in the top level write set of the function.

Definition at line 296 of file dfcc_cfg_info.h.

◆ get_top_level_write_set()

const exprt& dfcc_cfg_infot::get_top_level_write_set ( ) const

inline

Definition at line 289 of file dfcc_cfg_info.h.

◆ get_tracked_set()

const std::unordered_set< irep_idt > & dfcc_cfg_infot::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 that target instruction is found.

Definition at line 662 of file dfcc_cfg_info.cpp.

◆ get_write_set()

const exprt & dfcc_cfg_infot::get_write_set ( goto_programt::const_targett target ) const

Returns the write set variable for that instruction.

Definition at line 644 of file dfcc_cfg_info.cpp.

◆ is_top_level_id()

bool dfcc_cfg_infot::is_top_level_id ( const std::size_t id ) const

private

True iff id is in the valid range for a loop id for this function.

Definition at line 744 of file dfcc_cfg_info.cpp.

◆ is_valid_loop_id()

bool dfcc_cfg_infot::is_valid_loop_id ( const std::size_t id ) const

private

True iff id is in the valid range for a loop id for this function.

Definition at line 739 of file dfcc_cfg_info.cpp.

◆ is_valid_loop_or_top_level_id()

bool dfcc_cfg_infot::is_valid_loop_or_top_level_id ( const std::size_t id ) const

private

True iff id is in the valid range for a loop id or is equal to the top level id for this function.

Definition at line 734 of file dfcc_cfg_info.cpp.

◆ must_check_lhs()

bool dfcc_cfg_infot::must_check_lhs ( goto_programt::const_targett target ) const

True iff the lhs of an assignment must be checked against the ambient write set.

We say a lhs must be checked if

lhs is a non-local symbol; or
lhs depends on some non-local roots.

Definition at line 874 of file dfcc_cfg_info.cpp.

◆ must_track_decl_or_dead()

bool dfcc_cfg_infot::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.

Definition at line 749 of file dfcc_cfg_info.cpp.

◆ output()

void dfcc_cfg_infot::output ( std::ostream & out ) const

Definition at line 599 of file dfcc_cfg_info.cpp.

Member Data Documentation

◆ function_id

const irep_idt& dfcc_cfg_infot::function_id

private

Definition at line 302 of file dfcc_cfg_info.h.

◆ goto_function

goto_functiont& dfcc_cfg_infot::goto_function

private

Definition at line 303 of file dfcc_cfg_info.h.

◆ loop_info_map

std::map<std::size_t, dfcc_loop_infot> dfcc_cfg_infot::loop_info_map

private

Map from loop identifier to loop info struct.

Definition at line 331 of file dfcc_cfg_info.h.

◆ ns

const namespacet dfcc_cfg_infot::ns

private

Definition at line 305 of file dfcc_cfg_info.h.

◆ top_level_local

std::unordered_set<irep_idt> dfcc_cfg_infot::top_level_local

private

Set of identifiers DECL at top level.

Definition at line 325 of file dfcc_cfg_info.h.

◆ top_level_loops

std::vector<std::size_t> dfcc_cfg_infot::top_level_loops

private

Loop identifiers for top level loops (ie for loops that are not nested in in another loop).

Definition at line 322 of file dfcc_cfg_info.h.

◆ top_level_tracked

std::unordered_set<irep_idt> dfcc_cfg_infot::top_level_tracked

private

Set of identifiers DECL at top level.

Definition at line 328 of file dfcc_cfg_info.h.

◆ top_level_write_set

const exprt& dfcc_cfg_infot::top_level_write_set

private

Definition at line 304 of file dfcc_cfg_info.h.

◆ topsorted_loops

std::vector<std::size_t> dfcc_cfg_infot::topsorted_loops

private

Loop identifiers sorted from most deeply nested to less deeply nested.

Definition at line 318 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

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ dfcc_cfg_infot()

Member Function Documentation

◆ get_local_set()

◆ get_loop_info()

◆ get_loops_toposorted()

◆ get_outer_loop_identifier()

◆ get_outer_write_set()

◆ get_top_level_tracked()

◆ get_top_level_write_set()

◆ get_tracked_set()

◆ get_write_set()

◆ is_top_level_id()

◆ is_valid_loop_id()

◆ is_valid_loop_or_top_level_id()

◆ must_check_lhs()

◆ must_track_decl_or_dead()

◆ output()

Member Data Documentation

◆ function_id

◆ goto_function

◆ loop_info_map

◆ ns

◆ top_level_local

◆ top_level_loops

◆ top_level_tracked

◆ top_level_write_set

◆ topsorted_loops