cprover
var_map.cpp
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 #include "var_map.h"
13 
14 #include <ostream>
15 
16 #include <util/symbol.h>
17 #include <util/std_expr.h>
18 #include <util/prefix.h>
19 
21  const irep_idt &symbol,
22  const irep_idt &suffix,
23  const typet &type)
24 {
25  assert(!symbol.empty());
26 
27  std::string full_identifier=
28  id2string(symbol)+id2string(suffix);
29 
30  std::pair<id_mapt::iterator, bool> result;
31 
32  result=id_map.insert(std::pair<irep_idt, var_infot>(
33  full_identifier, var_infot()));
34 
35  if(result.second) // inserted?
36  {
37  result.first->second.full_identifier=full_identifier;
38  result.first->second.symbol=symbol;
39  result.first->second.suffix=suffix;
40  result.first->second.type=type;
41  init(result.first->second);
42  }
43 
44  return result.first->second;
45 }
46 
47 void var_mapt::var_infot::output(std::ostream &out) const
48 {
49  out << "full_identifier: " << full_identifier << "\n";
50  out << "symbol: " << symbol << "\n";
51  out << "suffix: " << suffix << "\n";
52 
53  out << "kind: ";
54 
55  switch(kind)
56  {
57  case PROCEDURE_LOCAL: out << "PROCEDURE_LOCAL"; break;
58  case THREAD_LOCAL: out << "THREAD_LOCAL"; break;
59  case SHARED: out << "SHARED"; break;
60  }
61 
62  out << "\n";
63 
64  out << "number: " << number << "\n";
65 
66  out << "type: " << type.pretty() << "\n";
67 
68  out << "\n";
69 }
70 
71 void var_mapt::init(var_infot &var_info)
72 {
73  if(has_prefix(id2string(var_info.symbol), "symex_dynamic::"))
74  {
75  var_info.kind=var_infot::SHARED;
76  }
77  else
78  {
79  // Check for the presence of va_args
80  std::size_t found=id2string(var_info.symbol).find("::va_arg");
81  if(found != std::string::npos)
82  {
84  }
85  else
86  {
87  const symbolt *symbol=nullptr;
88  if(ns.lookup(var_info.symbol, symbol))
89  throw "var_mapt::init identifier \""
90  +id2string(var_info.full_identifier)
91  +"\" lookup in ns failed";
92 
93  if(symbol->is_static_lifetime)
94  {
95  if(symbol->is_thread_local)
97  else
98  var_info.kind=var_infot::SHARED;
99  }
100  else
102  }
103  }
104 
105  if(var_info.is_shared())
106  var_info.number=shared_count++;
107  else
108  var_info.number=local_count++;
109 }
110 
112 {
113  return id2string(full_identifier)+
114  "#"+std::to_string(ssa_counter);
115 }
116 
117 void var_mapt::output(std::ostream &out) const
118 {
119  for(id_mapt::const_iterator
120  it=id_map.begin();
121  it!=id_map.end();
122  it++)
123  {
124  out << it->first << ":\n";
125  it->second.output(out);
126  }
127 }
The type of an expression.
Definition: type.h:20
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
irep_idt symbol
Definition: var_map.h:48
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_thread_local
Definition: symbol.h:70
Symbol table entry.
irep_idt ssa_identifier() const
Definition: var_map.cpp:111
void output(std::ostream &out) const
Definition: var_map.cpp:47
void init(var_infot &var_info)
Definition: var_map.cpp:71
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
bool is_static_lifetime
Definition: symbol.h:70
unsigned shared_count
Definition: var_map.h:107
API to expression classes.
id_mapt id_map
Definition: var_map.h:78
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
unsigned number
Definition: var_map.h:45
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
Variable Numbering.
void output(std::ostream &) const
Definition: var_map.cpp:117
bool is_shared() const
Definition: var_map.h:39
const namespacet ns
Definition: var_map.h:101
bool empty() const
Definition: dstring.h:61
irep_idt full_identifier
Definition: var_map.h:48