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 (goto_modelt &goto_model, const irep_idt &function_id, goto_functiont &goto_function, const exprt &top_level_write_set, const loop_contract_configt &loop_contract_config, 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 to use for the given instruction Returns the write set for the loop, or one of the outer loops, or top level, passing through all loops that are [must_skip]. 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

std::size_t	get_first_id_not_skipped_or_top_level_id (const std::size_t loop_id) const
	Returns the id of the first outer loop (including this one) that is not skipped, or the top level id. More...

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

size_t	top_level_id () const
	Returns the top level ID. 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 242 of file dfcc_cfg_info.h.

Constructor & Destructor Documentation

◆ dfcc_cfg_infot()

dfcc_cfg_infot::dfcc_cfg_infot	(	goto_modelt &	goto_model,
		const irep_idt &	function_id,
		goto_functiont &	goto_function,
		const exprt &	top_level_write_set,
		const loop_contract_configt &	loop_contract_config,
		symbol_table_baset &	symbol_table,
		message_handlert &	message_handler,
		dfcc_libraryt &	library
	)

Definition at line 486 of file dfcc_cfg_info.cpp.

Member Function Documentation

◆ get_first_id_not_skipped_or_top_level_id()

std::size_t dfcc_cfg_infot::get_first_id_not_skipped_or_top_level_id ( const std::size_t loop_id ) const

Returns the id of the first outer loop (including this one) that is not skipped, or the top level id.

Definition at line 650 of file dfcc_cfg_info.cpp.

◆ 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 698 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 725 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 279 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 732 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 715 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 312 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 305 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 680 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 to use for the given instruction Returns the write set for the loop, or one of the outer loops, or top level, passing through all loops that are [must_skip].

Definition at line 662 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 762 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 757 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 752 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 896 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 772 of file dfcc_cfg_info.cpp.

◆ output()

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

Definition at line 606 of file dfcc_cfg_info.cpp.

◆ top_level_id()

size_t dfcc_cfg_infot::top_level_id ( ) const

private

Returns the top level ID.

Definition at line 767 of file dfcc_cfg_info.cpp.

Member Data Documentation

◆ function_id

const irep_idt& dfcc_cfg_infot::function_id

private

Definition at line 318 of file dfcc_cfg_info.h.

◆ goto_function

goto_functiont& dfcc_cfg_infot::goto_function

private

Definition at line 319 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 350 of file dfcc_cfg_info.h.

◆ ns

const namespacet dfcc_cfg_infot::ns

private

Definition at line 321 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 344 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 341 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 347 of file dfcc_cfg_info.h.

◆ top_level_write_set

const exprt& dfcc_cfg_infot::top_level_write_set

private

Definition at line 320 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 337 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_first_id_not_skipped_or_top_level_id()

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

◆ top_level_id()

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