cprover
irept Class Reference

Base class for tree-like data structures with sharing. More...

#include <irep.h>

+ Inheritance diagram for irept:
+ Collaboration diagram for irept:

Classes

class  dt
 

Public Types

typedef std::vector< ireptsubt
 
typedef std::map< irep_namet, ireptnamed_subt
 

Public Member Functions

bool is_nil () const
 
bool is_not_nil () const
 
 irept (const irep_idt &_id)
 
 irept ()
 
 irept (const irept &irep)
 
 irept (irept &&irep)
 
ireptoperator= (const irept &irep)
 
ireptoperator= (irept &&irep)
 
 ~irept ()
 
const irep_idtid () const
 
const std::string & id_string () const
 
void id (const irep_idt &_data)
 
const ireptfind (const irep_namet &name) const
 
ireptadd (const irep_namet &name)
 
ireptadd (const irep_namet &name, const irept &irep)
 
const std::string & get_string (const irep_namet &name) const
 
const irep_idtget (const irep_namet &name) const
 
bool get_bool (const irep_namet &name) const
 
signed int get_int (const irep_namet &name) const
 
unsigned int get_unsigned_int (const irep_namet &name) const
 
std::size_t get_size_t (const irep_namet &name) const
 
long long get_long_long (const irep_namet &name) const
 
void set (const irep_namet &name, const irep_idt &value)
 
void set (const irep_namet &name, const irept &irep)
 
void set (const irep_namet &name, const long long value)
 
void remove (const irep_namet &name)
 
void move_to_sub (irept &irep)
 
void move_to_named_sub (const irep_namet &name, irept &irep)
 
bool operator== (const irept &other) const
 
bool operator!= (const irept &other) const
 
void swap (irept &irep)
 
bool operator< (const irept &other) const
 defines ordering on the internal representation More...
 
bool ordering (const irept &other) const
 defines ordering on the internal representation More...
 
int compare (const irept &i) const
 defines ordering on the internal representation More...
 
void clear ()
 
void make_nil ()
 
subtget_sub ()
 
const subtget_sub () const
 
named_subtget_named_sub ()
 
const named_subtget_named_sub () const
 
named_subtget_comments ()
 
const named_subtget_comments () const
 
std::size_t hash () const
 
std::size_t full_hash () const
 
bool full_eq (const irept &other) const
 
std::string pretty (unsigned indent=0, unsigned max_indent=0) const
 
const dtread () const
 
dtwrite ()
 

Protected Member Functions

void detach ()
 

Static Protected Member Functions

static bool is_comment (const irep_namet &name)
 
static void remove_ref (dt *old_data)
 
static void nonrecursive_destructor (dt *old_data)
 Does the same as remove_ref, but using an explicit stack instead of recursion. More...
 

Protected Attributes

dtdata
 

Static Protected Attributes

static dt empty_d
 

Detailed Description

Base class for tree-like data structures with sharing.

There are a large number of kinds of tree structured or tree-like data in CPROVER. irept provides a single, unified representation for all of these, allowing structure sharing and reference counting of data. As such irept is the basic unit of data in CPROVER. Each irept contains (or references, if reference counted data sharing is enabled, as it is by default - see the SHARING macro) a basic unit of data (of type dt) which contains four things:

  • irept::dt::data : A string, which is returned when the id() function is used. (Unless USE_STD_STRING is set, this is actually a dstringt and thus an integer which is a reference into a string table.)
  • irept::dt::named_sub : A map from irep_namet (a string) to irept. This is used for named children, i.e. subexpressions, parameters, etc.
  • irept::dt::comments : Another map from irep_namet to irept which is used for annotations and other ‘non-semantic’ information. Note that this map is ignored by the default operator==.
  • irept::dt::sub : A vector of irept which is used to store ordered but unnamed children.

The irept::pretty function outputs the explicit tree structure of an irept and can be used to understand and debug problems with irepts.

On their own irepts do not "mean" anything; they are effectively generic tree nodes. Their interpretation depends on the contents of result of the id() function, i.e. the data field. util/irep_ids.def contains a list of id values. During the build process it is used to generate util/irep_ids.h which gives constants for each id (named ID_). You can also make irep_idts which do not come from util/irep_ids.def. An irep_idt can then be used to identify what kind of data the irept stores and thus what can be done with it.

To simplify this process, there are a variety of classes that inherit from irept, roughly corresponding to the ids listed (i.e. ID_or (the string "or”) corresponds to the class or_exprt). These give semantically relevant accessor functions for the data; effectively different APIs for the same underlying data structure. None of these classes add fields (only methods) and so static casting can be used. The inheritance graph of the subclasses of irept is a useful starting point for working out how to manipulate data.

There are three main groups of classes (or APIs); those derived from typet, codet and exprt respectively. Although all of these inherit from irept, these are the most abstract level that code should handle data. If code is manipulating plain irepts then something is wrong with the architecture of the code.

Many of the key descendants of exprt are declared in std_expr.h. All expressions have a named subexpression with ID "type", which gives the type of the expression (slightly simplified from C/C++ as unsignedbv_typet, signedbv_typet, floatbv_typet, etc.). All type conversions are explicit with a typecast_exprt. One key descendant of exprt is symbol_exprt which creates irept instances with ID “symbol”. These are used to represent variables; the name of which can be found using the get_identifier accessor function.

codet inherits from exprt and is defined in std_code.h. It represents executable code; statements in a C-like language rather than expressions. In the front-end there are versions of these that hold whole code blocks, but in goto-programs these have been flattened so that each irept represents one sequence point (almost one line of code / one semi-colon). The most common descendant of codet is code_assignt so a common pattern is to cast the codet to an assignment and then recurse on the expression on either side.

Definition at line 156 of file irep.h.

Member Typedef Documentation

◆ named_subt

typedef std::map<irep_namet, irept> irept::named_subt

Definition at line 169 of file irep.h.

◆ subt

typedef std::vector<irept> irept::subt

Definition at line 160 of file irep.h.

Constructor & Destructor Documentation

◆ irept() [1/4]

irept::irept ( const irep_idt _id)
inlineexplicit

Definition at line 175 of file irep.h.

◆ irept() [2/4]

irept::irept ( )
inline

Definition at line 185 of file irep.h.

◆ irept() [3/4]

irept::irept ( const irept irep)
inline

Definition at line 190 of file irep.h.

◆ irept() [4/4]

irept::irept ( irept &&  irep)
inline

Definition at line 207 of file irep.h.

◆ ~irept()

irept::~irept ( )
inline

Definition at line 248 of file irep.h.

Member Function Documentation

◆ add() [1/2]

irept & irept::add ( const irep_namet name)

Definition at line 305 of file irep.cpp.

◆ add() [2/2]

irept & irept::add ( const irep_namet name,
const irept irep 
)

Definition at line 323 of file irep.cpp.

◆ clear()

void irept::clear ( void  )
inline

Definition at line 313 of file irep.h.

◆ compare()

int irept::compare ( const irept i) const

defines ordering on the internal representation

Definition at line 497 of file irep.cpp.

◆ detach()

void irept::detach ( )
protected

Definition at line 63 of file irep.cpp.

◆ find()

const irept & irept::find ( const irep_namet name) const

Definition at line 284 of file irep.cpp.

◆ full_eq()

bool irept::full_eq ( const irept other) const

Definition at line 379 of file irep.cpp.

◆ full_hash()

std::size_t irept::full_hash ( ) const

Definition at line 605 of file irep.cpp.

◆ get()

const irep_idt & irept::get ( const irep_namet name) const

Definition at line 212 of file irep.cpp.

◆ get_bool()

bool irept::get_bool ( const irep_namet name) const

Definition at line 239 of file irep.cpp.

◆ get_comments() [1/2]

named_subt& irept::get_comments ( )
inline

Definition at line 321 of file irep.h.

◆ get_comments() [2/2]

const named_subt& irept::get_comments ( ) const
inline

Definition at line 322 of file irep.h.

◆ get_int()

int irept::get_int ( const irep_namet name) const

Definition at line 244 of file irep.cpp.

◆ get_long_long()

long long irept::get_long_long ( const irep_namet name) const

Definition at line 259 of file irep.cpp.

◆ get_named_sub() [1/2]

named_subt& irept::get_named_sub ( )
inline

Definition at line 319 of file irep.h.

◆ get_named_sub() [2/2]

const named_subt& irept::get_named_sub ( ) const
inline

Definition at line 320 of file irep.h.

◆ get_size_t()

std::size_t irept::get_size_t ( const irep_namet name) const

Definition at line 254 of file irep.cpp.

◆ get_string()

const std::string& irept::get_string ( const irep_namet name) const
inline

Definition at line 272 of file irep.h.

◆ get_sub() [1/2]

subt& irept::get_sub ( )
inline

Definition at line 317 of file irep.h.

◆ get_sub() [2/2]

const subt& irept::get_sub ( ) const
inline

Definition at line 318 of file irep.h.

◆ get_unsigned_int()

unsigned int irept::get_unsigned_int ( const irep_namet name) const
Deprecated:
use get_size_t instead

Definition at line 249 of file irep.cpp.

◆ hash()

std::size_t irept::hash ( ) const

Definition at line 574 of file irep.cpp.

◆ id() [1/2]

const irep_idt& irept::id ( ) const
inline

Definition at line 259 of file irep.h.

◆ id() [2/2]

void irept::id ( const irep_idt _data)
inline

Definition at line 265 of file irep.h.

◆ id_string()

const std::string& irept::id_string ( ) const
inline

Definition at line 262 of file irep.h.

◆ is_comment()

static bool irept::is_comment ( const irep_namet name)
inlinestaticprotected

Definition at line 332 of file irep.h.

◆ is_nil()

bool irept::is_nil ( ) const
inline

Definition at line 172 of file irep.h.

◆ is_not_nil()

bool irept::is_not_nil ( ) const
inline

Definition at line 173 of file irep.h.

◆ make_nil()

void irept::make_nil ( )
inline

Definition at line 315 of file irep.h.

◆ move_to_named_sub()

void irept::move_to_named_sub ( const irep_namet name,
irept irep 
)

Definition at line 194 of file irep.cpp.

◆ move_to_sub()

void irept::move_to_sub ( irept irep)

Definition at line 203 of file irep.cpp.

◆ nonrecursive_destructor()

void irept::nonrecursive_destructor ( dt old_data)
staticprotected

Does the same as remove_ref, but using an explicit stack instead of recursion.

Definition at line 139 of file irep.cpp.

◆ operator!=()

bool irept::operator!= ( const irept other) const
inline

Definition at line 298 of file irep.h.

◆ operator<()

bool irept::operator< ( const irept other) const

defines ordering on the internal representation

Definition at line 565 of file irep.cpp.

◆ operator=() [1/2]

irept& irept::operator= ( const irept irep)
inline

Definition at line 216 of file irep.h.

◆ operator=() [2/2]

irept& irept::operator= ( irept &&  irep)
inline

Definition at line 237 of file irep.h.

◆ operator==()

bool irept::operator== ( const irept other) const

Definition at line 354 of file irep.cpp.

◆ ordering()

bool irept::ordering ( const irept other) const

defines ordering on the internal representation

Definition at line 429 of file irep.cpp.

◆ pretty()

std::string irept::pretty ( unsigned  indent = 0,
unsigned  max_indent = 0 
) const

Definition at line 640 of file irep.cpp.

◆ read()

const dt& irept::read ( ) const
inline

Definition at line 406 of file irep.h.

◆ remove()

void irept::remove ( const irep_namet name)

Definition at line 269 of file irep.cpp.

◆ remove_ref()

void irept::remove_ref ( dt old_data)
staticprotected

Definition at line 99 of file irep.cpp.

◆ set() [1/3]

void irept::set ( const irep_namet name,
const irep_idt value 
)
inline

Definition at line 286 of file irep.h.

◆ set() [2/3]

void irept::set ( const irep_namet name,
const irept irep 
)
inline

Definition at line 288 of file irep.h.

◆ set() [3/3]

void irept::set ( const irep_namet name,
const long long  value 
)

Definition at line 264 of file irep.cpp.

◆ swap()

void irept::swap ( irept irep)
inline

Definition at line 303 of file irep.h.

◆ write()

dt& irept::write ( )
inline

Definition at line 411 of file irep.h.

Member Data Documentation

◆ data

dt* irept::data
protected

Definition at line 398 of file irep.h.

◆ empty_d

irept::dt irept::empty_d
staticprotected

Definition at line 399 of file irep.h.


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