loopst Class Reference

#include <loopst.h>

Public Types
typedef std::unordered_set< expr2tc, irep2_hash >	loop_varst

Public Member Functions
	loopst ()
const loop_varst &	get_modified_loop_vars () const
const loop_varst &	get_unmodified_loop_vars () const
const goto_programt::targett	get_original_loop_exit () const
void	set_original_loop_exit (goto_programt::targett _loop_exit)
const goto_programt::targett	get_original_loop_head () const
void	set_original_loop_head (goto_programt::targett _loop_head)
goto_programt::targett	effective_loop_head () const
	Effective loop head: the first non-inert instruction at-or-after original_loop_head.
void	add_modified_var_to_loop (const expr2tc &expr)
void	add_unmodified_var_to_loop (const expr2tc &expr)
void	add_pointer_array_write_ptr (const expr2tc &ptr)
	Record a pointer the loop writes through, or a pointer argument of a callee that does ((*dest)[i] = ... records dest, p[i] = ... records p).
const loop_varst &	get_pointer_array_write_ptrs () const
void	set_pointer_array_write_unresolvable ()
	Record a write that havocking through the recorded pointers cannot cover: an element a callee writes past its argument, or a write whose pointer could not be extracted.
bool	pointer_array_write_unresolvable () const
void	set_writes_through_pointer ()
	Record that the loop, or a function it calls, writes through a dereference (*p = ..., p->f = ..., p->e[i] = ...).
bool	writes_through_pointer () const
void	add_written_pointer (const expr2tc &ptr)
	Record a pointer the loop, or a function it calls, writes through, in the scope of the function holding the dereference.
const loop_varst &	get_written_pointers () const
void	add_written_pointee (const expr2tc &pointee)
	Record *p for a write that stays inside it (*p = ..., p->f = ...).
const loop_varst &	get_written_pointees () const
void	set_unnamed_pointer_write ()
	Record a write through a pointer that neither add_written_pointer nor add_written_pointee can name: a conditional l-value, or a call through a function pointer.
bool	unnamed_pointer_write () const
void	dump () const
void	dump_loop_vars () const
void	output_to (std::ostream &oss) const
void	output_loop_vars_to (std::ostream &oss) const
void	set_size (std::size_t size)

Protected Attributes
loop_varst	modified_loop_vars
loop_varst	unmodified_loop_vars
goto_programt::targett	original_loop_head
goto_programt::targett	original_loop_exit
std::size_t	size
bool	pointer_array_write_unresolvable_ = false
bool	writes_through_pointer_ = false
loop_varst	pointer_array_write_ptrs_
loop_varst	written_pointers_
loop_varst	written_pointees_
bool	unnamed_pointer_write_ = false

Member Typedef Documentation

loop_varst

typedef std::unordered_set<expr2tc, irep2_hash> loopst::loop_varst

Constructor & Destructor Documentation

loopst()

loopst::loopst ( )

inline

Member Function Documentation

add_modified_var_to_loop()

void loopst::add_modified_var_to_loop

(

const expr2tc &

expr

)

add_pointer_array_write_ptr()

void loopst::add_pointer_array_write_ptr ( const expr2tc & ptr )

inline

Record a pointer the loop writes through, or a pointer argument of a callee that does ((*dest)[i] = ... records dest, p[i] = ... records p).

The loop-invariant schema havocs through these (#7478).

add_unmodified_var_to_loop()

void loopst::add_unmodified_var_to_loop

(

const expr2tc &

expr

)

add_written_pointee()

void loopst::add_written_pointee ( const expr2tc & pointee )

inline

Record *p for a write that stays inside it (*p = ..., p->f = ...).

While the loop leaves p alone, havocking *p covers the write even when p reaches memory with no name, such as the heap.

add_written_pointer()

void loopst::add_written_pointer ( const expr2tc & ptr )

inline

Record a pointer the loop, or a function it calls, writes through, in the scope of the function holding the dereference.

A whole-program points-to analysis resolves these to the objects the inductive step must havoc.

dump()

void loopst::dump

(

)

const

dump_loop_vars()

void loopst::dump_loop_vars

(

)

const

effective_loop_head()

goto_programt::targett loopst::effective_loop_head

(

)

const

Effective loop head: the first non-inert instruction at-or-after original_loop_head.

Inert here means an instruction that does not change control flow and that a structural recogniser would otherwise reject — SKIP, LOCATION, DECL, DEAD, and ASSUME.

Motivation: --interval-analysis (and other passes that use insert_swap) insert ASSUME(bounds) instructions at the back- edge target. The back-edge then lands on the ASSUME, and get_original_loop_head() returns that ASSUME rather than the loop's IF. Structural recognisers (eca's recognize_eca_main_loop, the ranking certifier's recognize_loop, etc.) need to find the actual control-flow instruction; calling this helper instead of get_original_loop_head() does the right skip in one place.

Returns original_loop_exit if every instruction in [original_loop_head, original_loop_exit) is inert (degenerate loop with no body besides the back-edge); callers should handle that case explicitly.

get_modified_loop_vars()

const loopst::loop_varst & loopst::get_modified_loop_vars

(

)

const

get_original_loop_exit()

const goto_programt::targett loopst::get_original_loop_exit

(

)

const

get_original_loop_head()

const goto_programt::targett loopst::get_original_loop_head

(

)

const

get_pointer_array_write_ptrs()

const loop_varst & loopst::get_pointer_array_write_ptrs ( ) const

inline

get_unmodified_loop_vars()

const loopst::loop_varst & loopst::get_unmodified_loop_vars

(

)

const

get_written_pointees()

const loop_varst & loopst::get_written_pointees ( ) const

inline

get_written_pointers()

const loop_varst & loopst::get_written_pointers ( ) const

inline

output_loop_vars_to()

void loopst::output_loop_vars_to

(

std::ostream &

oss

)

const

output_to()

void loopst::output_to

(

std::ostream &

oss

)

const

pointer_array_write_unresolvable()

bool loopst::pointer_array_write_unresolvable ( ) const

inline

set_original_loop_exit()

void loopst::set_original_loop_exit

(

goto_programt::targett

_loop_exit

)

set_original_loop_head()

void loopst::set_original_loop_head

(

goto_programt::targett

_loop_head

)

set_pointer_array_write_unresolvable()

void loopst::set_pointer_array_write_unresolvable ( )

inline

Record a write that havocking through the recorded pointers cannot cover: an element a callee writes past its argument, or a write whose pointer could not be extracted.

The loop-invariant schema declines.

set_size()

void loopst::set_size ( std::size_t size )

inline

set_unnamed_pointer_write()

void loopst::set_unnamed_pointer_write ( )

inline

Record a write through a pointer that neither add_written_pointer nor add_written_pointee can name: a conditional l-value, or a call through a function pointer.

set_writes_through_pointer()

void loopst::set_writes_through_pointer ( )

inline

Record that the loop, or a function it calls, writes through a dereference (*p = ..., p->f = ..., p->e[i] = ...).

The pointee is not a named symbol, so a schema that havocs named symbols cannot cover it: k-induction havocs the objects the written pointers resolve to, and the loop-invariant schema declines a loop whose guard the havoc cannot reach (issue #7478).

unnamed_pointer_write()

bool loopst::unnamed_pointer_write ( ) const

inline

writes_through_pointer()

bool loopst::writes_through_pointer ( ) const

inline

Member Data Documentation

modified_loop_vars

loop_varst loopst::modified_loop_vars

protected

original_loop_exit

goto_programt::targett loopst::original_loop_exit

protected

original_loop_head

goto_programt::targett loopst::original_loop_head

protected

pointer_array_write_ptrs_

loop_varst loopst::pointer_array_write_ptrs_

protected

pointer_array_write_unresolvable_

bool loopst::pointer_array_write_unresolvable_ = false

protected

size

std::size_t loopst::size

protected

unmodified_loop_vars

loop_varst loopst::unmodified_loop_vars

protected

unnamed_pointer_write_

bool loopst::unnamed_pointer_write_ = false

protected

writes_through_pointer_

bool loopst::writes_through_pointer_ = false

protected

written_pointees_

loop_varst loopst::written_pointees_

protected

written_pointers_

loop_varst loopst::written_pointers_

protected

---

The documentation for this class was generated from the following files:

• src/goto-programs/loopst.h
• src/goto-programs/loopst.cpp