cprover
renaming_level.h File Reference
#include <map>
#include <unordered_set>
#include <util/expr_iterator.h>
#include <util/irep.h>
#include <util/range.h>
#include <util/sharing_map.h>
#include <util/simplify_expr.h>
#include <util/ssa_expr.h>
#include "renamed.h"
+ Include dependency graph for renaming_level.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  symex_level1t
 Functor to set the level 1 renaming of SSA expressions. More...
 
struct  symex_level2t
 Functor to set the level 2 renaming of SSA expressions. More...
 

Typedefs

using symex_renaming_levelt = sharing_mapt< irep_idt, std::pair< ssa_exprt, std::size_t > >
 Wrapper for a current_names map, which maps each identifier to an SSA expression and a counter. More...
 

Functions

void get_variables (const symex_renaming_levelt &current_names, std::unordered_set< ssa_exprt, irep_hash > &vars)
 Add the ssa_exprt of current_names to vars. More...
 
renamedt< ssa_exprt, L0symex_level0 (ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr)
 Set the level 0 renaming of SSA expressions. More...
 
exprt get_original_name (exprt expr)
 Undo all levels of renaming. More...
 
typet get_original_name (typet type)
 Undo all levels of renaming. More...
 
bool check_renaming (const exprt &expr)
 Check that expr is correctly renamed to level 2 and return true in case an error is detected. More...
 
bool check_renaming_l1 (const exprt &expr)
 Check that expr is correctly renamed to level 1 and return true in case an error is detected. More...
 
bool check_renaming (const typet &type)
 Check that type is correctly renamed to level 2 and return true in case an error is detected. More...
 

Detailed Description

Renaming levels

Definition in file renaming_level.h.

Typedef Documentation

◆ symex_renaming_levelt

using symex_renaming_levelt = sharing_mapt<irep_idt, std::pair<ssa_exprt, std::size_t> >

Wrapper for a current_names map, which maps each identifier to an SSA expression and a counter.

This is extended by the different symex_level structures which are used during symex to ensure static single assignment (SSA) form.

Definition at line 32 of file renaming_level.h.

Function Documentation

◆ check_renaming() [1/2]

bool check_renaming ( const exprt expr)

Check that expr is correctly renamed to level 2 and return true in case an error is detected.

Definition at line 250 of file renaming_level.cpp.

◆ check_renaming() [2/2]

bool check_renaming ( const typet type)

Check that type is correctly renamed to level 2 and return true in case an error is detected.

Definition at line 209 of file renaming_level.cpp.

◆ check_renaming_l1()

bool check_renaming_l1 ( const exprt expr)

Check that expr is correctly renamed to level 1 and return true in case an error is detected.

Definition at line 225 of file renaming_level.cpp.

◆ get_original_name() [1/2]

exprt get_original_name ( exprt  expr)

Undo all levels of renaming.

Definition at line 169 of file renaming_level.cpp.

◆ get_original_name() [2/2]

typet get_original_name ( typet  type)

Undo all levels of renaming.

Definition at line 183 of file renaming_level.cpp.

◆ get_variables()

void get_variables ( const symex_renaming_levelt current_names,
std::unordered_set< ssa_exprt, irep_hash > &  vars 
)

Add the ssa_exprt of current_names to vars.

Deprecated:
SINCE(2019, 6, 5, "Unused")

◆ symex_level0()

renamedt<ssa_exprt, L0> symex_level0 ( ssa_exprt  ssa_expr,
const namespacet ns,
std::size_t  thread_nr 
)

Set the level 0 renaming of SSA expressions.

Level 0 corresponds to threads. The renaming is built for one particular interleaving. Rename ssa_expr using thread_nr as L0 tag, unless ssa_expr is a guard, a shared variable or a function. ns is queried to decide whether we are in one of these cases.

Definition at line 34 of file renaming_level.cpp.