cprover
|
Base class for tree-like data structures with sharing. More...
#include <irep.h>
Classes | |
class | dt |
Public Types | |
typedef std::vector< irept > | subt |
typedef std::map< irep_namet, irept > | named_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) | |
irept & | operator= (const irept &irep) |
irept & | operator= (irept &&irep) |
~irept () | |
const irep_idt & | id () const |
const std::string & | id_string () const |
void | id (const irep_idt &_data) |
const irept & | find (const irep_namet &name) const |
irept & | add (const irep_namet &name) |
irept & | add (const irep_namet &name, const irept &irep) |
const std::string & | get_string (const irep_namet &name) const |
const irep_idt & | get (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 () |
subt & | get_sub () |
const subt & | get_sub () const |
named_subt & | get_named_sub () |
const named_subt & | get_named_sub () const |
named_subt & | get_comments () |
const named_subt & | get_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 dt & | read () const |
dt & | write () |
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 | |
dt * | data |
Static Protected Attributes | |
static dt | empty_d |
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:
USE_STD_STRING
is set, this is actually a dstringt and thus an integer which is a reference into a string table.)irep_namet
(a string) to irept. This is used for named children, i.e. subexpressions, parameters, etc.irep_namet
to irept which is used for annotations and other ‘non-semantic’ information. Note that this map is ignored by the default operator==.The irept::pretty function outputs the explicit tree structure of an irept and can be used to understand and debug problems with irept
s.
On their own irept
s 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_idt
s 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 irept
s 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.
typedef std::map<irep_namet, irept> irept::named_subt |
typedef std::vector<irept> irept::subt |
irept & irept::add | ( | const irep_namet & | name | ) |
irept & irept::add | ( | const irep_namet & | name, |
const irept & | irep | ||
) |
int irept::compare | ( | const irept & | i | ) | const |
const irept & irept::find | ( | const irep_namet & | name | ) | const |
const irep_idt & irept::get | ( | const irep_namet & | name | ) | const |
bool irept::get_bool | ( | const irep_namet & | name | ) | const |
|
inline |
|
inline |
int irept::get_int | ( | const irep_namet & | name | ) | const |
long long irept::get_long_long | ( | const irep_namet & | name | ) | const |
|
inline |
|
inline |
std::size_t irept::get_size_t | ( | const irep_namet & | name | ) | const |
|
inline |
unsigned int irept::get_unsigned_int | ( | const irep_namet & | name | ) | const |
|
inlinestaticprotected |
void irept::move_to_named_sub | ( | const irep_namet & | name, |
irept & | irep | ||
) |
|
staticprotected |
bool irept::operator< | ( | const irept & | other | ) | const |
bool irept::ordering | ( | const irept & | other | ) | const |
std::string irept::pretty | ( | unsigned | indent = 0 , |
unsigned | max_indent = 0 |
||
) | const |
void irept::remove | ( | const irep_namet & | name | ) |
|
inline |
|
inline |
void irept::set | ( | const irep_namet & | name, |
const long long | value | ||
) |