cprover
var_map.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Variable Numbering
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_PATH_SYMEX_VAR_MAP_H
13 #define CPROVER_PATH_SYMEX_VAR_MAP_H
14 
15 #include <iosfwd>
16 #include <map>
17 
18 #include <util/namespace.h>
19 #include <util/type.h>
20 #include <util/std_expr.h>
21 #include <util/symbol_table.h>
22 
23 class var_mapt
24 {
25 public:
26  explicit var_mapt(const namespacet &_ns):
27  ns(_ns.get_symbol_table(), new_symbols),
28  shared_count(0),
29  local_count(0),
30  nondet_count(0),
31  dynamic_count(0)
32  {
33  }
34 
35  struct var_infot
36  {
38 
39  bool is_shared() const
40  {
41  return kind==SHARED;
42  }
43 
44  // the variables are numbered
45  unsigned number;
46 
47  // full_identifier=symbol+suffix
49 
50  // the type of the identifier (struct member or array)
52 
53  unsigned ssa_counter;
54 
55  var_infot():kind(SHARED), number(0), ssa_counter(0)
56  {
57  }
58 
59  irep_idt ssa_identifier() const;
60 
62  {
64  s.set(ID_C_SSA_symbol, true);
65  s.set(ID_C_full_identifier, full_identifier);
66  return s;
67  }
68 
70  {
71  ++ssa_counter;
72  }
73 
74  void output(std::ostream &out) const;
75  };
76 
77  typedef std::map<irep_idt, var_infot> id_mapt;
78  id_mapt id_map;
79 
81  const irep_idt &symbol,
82  const irep_idt &suffix,
83  const typet &type);
84 
86  {
87  return id_map[full_identifier];
88  }
89 
90  void clear()
91  {
92  shared_count=0;
93  local_count=0;
94  nondet_count=0;
95  dynamic_count=0;
96  id_map.clear();
97  }
98 
99  void init(var_infot &var_info);
100 
101  const namespacet ns;
103 
104  void output(std::ostream &) const;
105 
106 protected:
108 
109 public:
110  unsigned nondet_count; // free inputs
111  unsigned dynamic_count; // memory allocation
112 };
113 
114 #endif // CPROVER_PATH_SYMEX_VAR_MAP_H
The type of an expression.
Definition: type.h:20
symbol_tablet new_symbols
Definition: var_map.h:102
irep_idt symbol
Definition: var_map.h:48
var_infot & operator[](const irep_idt &full_identifier)
Definition: var_map.h:85
var_mapt(const namespacet &_ns)
Definition: var_map.h:26
irep_idt ssa_identifier() const
Definition: var_map.cpp:111
void output(std::ostream &out) const
Definition: var_map.cpp:47
void clear()
Definition: var_map.h:90
void init(var_infot &var_info)
Definition: var_map.cpp:71
symbol_exprt ssa_symbol() const
Definition: var_map.h:61
unsigned shared_count
Definition: var_map.h:107
API to expression classes.
id_mapt id_map
Definition: var_map.h:78
The symbol table.
Definition: symbol_table.h:52
unsigned ssa_counter
Definition: var_map.h:53
TO_BE_DOCUMENTED.
Definition: namespace.h:62
unsigned local_count
Definition: var_map.h:107
enum var_mapt::var_infot::@18 kind
var_infot & operator()(const irep_idt &symbol, const irep_idt &suffix, const typet &type)
Definition: var_map.cpp:20
Symbol table.
unsigned number
Definition: var_map.h:45
void increment_ssa_counter()
Definition: var_map.h:69
unsigned nondet_count
Definition: var_map.h:110
std::map< irep_idt, var_infot > id_mapt
Definition: var_map.h:77
bool is_shared() const
Definition: var_map.h:39
Expression to hold a symbol (variable)
Definition: std_expr.h:82
const namespacet ns
Definition: var_map.h:101
unsigned dynamic_count
Definition: var_map.h:111
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
irep_idt full_identifier
Definition: var_map.h:48
irep_idt suffix
Definition: var_map.h:48