cprover
name_mangler.h
Go to the documentation of this file.
1 
5 #ifndef CPROVER_GOTO_PROGRAMS_NAME_MANGLER_H
6 #define CPROVER_GOTO_PROGRAMS_NAME_MANGLER_H
7 
8 #include <util/message.h>
9 #include <util/rename_symbol.h>
10 
11 #include "goto_model.h"
12 
13 #include <regex>
14 #include <vector>
15 
16 #define FILE_LOCAL_PREFIX CPROVER_PREFIX "file_local_"
17 
29 template <class MangleFun>
31 {
32 public:
37  message_handlert &mh,
38  goto_modelt &gm,
39  const std::string &extra_info)
40  : log(mh), model(gm), mangle_fun(), extra_info(extra_info)
41  {
42  }
43 
49  void mangle()
50  {
51  rename_symbolt rename;
52  std::map<irep_idt, irep_idt> renamed_funs;
53  std::vector<symbolt> new_syms;
54  std::vector<symbol_tablet::symbolst::const_iterator> old_syms;
55 
56  for(auto sym_it = model.symbol_table.symbols.begin();
57  sym_it != model.symbol_table.symbols.end();
58  ++sym_it)
59  {
60  const symbolt &sym = sym_it->second;
61 
62  if(sym.type.id() != ID_code) // is not a function
63  continue;
64  if(sym.value.is_nil()) // has no body
65  continue;
66  if(!sym.is_file_local)
67  continue;
68 
69  const irep_idt mangled = mangle_fun(sym, extra_info);
70  symbolt new_sym;
71  new_sym = sym;
72  new_sym.name = mangled;
73  new_sym.is_file_local = false;
74 
75  new_syms.push_back(new_sym);
76  old_syms.push_back(sym_it);
77 
78  rename.insert(sym.symbol_expr(), new_sym.symbol_expr());
79  renamed_funs.insert(std::make_pair(sym.name, mangled));
80 
81  log.debug() << "Mangling: " << sym.name << " -> " << mangled << log.eom;
82  }
83 
84  for(const auto &sym : new_syms)
86  for(const auto &sym : old_syms)
88 
89  for(const auto &sym_pair : model.symbol_table)
90  {
91  const symbolt &sym = sym_pair.second;
92 
93  exprt e = sym.value;
94  typet t = sym.type;
95  if(rename(e) && rename(t))
96  continue;
97 
99  new_sym.value = e;
100  new_sym.type = t;
101  }
102 
103  for(auto &fun : model.goto_functions.function_map)
104  {
105  if(!fun.second.body_available())
106  continue;
107  for(auto &ins : fun.second.body.instructions)
108  {
109  rename(ins.code);
110  rename(ins.guard);
111  }
112  }
113 
114  // Add goto-programs with new function names
115  for(const auto &pair : renamed_funs)
116  {
117  auto found = model.goto_functions.function_map.find(pair.first);
118  INVARIANT(
119  found != model.goto_functions.function_map.end(),
120  "There should exist an entry in the function_map for the original name "
121  "of the function that we renamed '" +
122  std::string(pair.first.c_str()) + "'");
123 
124  auto inserted = model.goto_functions.function_map.emplace(
125  pair.second, std::move(found->second));
126  if(!inserted.second)
127  log.debug() << "Found a mangled name that already exists: "
128  << std::string(pair.second.c_str()) << log.eom;
129 
130  model.goto_functions.function_map.erase(found);
131  }
132  }
133 
134 protected:
135  mutable messaget log;
137  MangleFun mangle_fun;
138  const std::string &extra_info;
139 };
140 
143 {
144 public:
146  : forbidden("[^\\w]", std::regex::ECMAScript),
147  multi_under("_+", std::regex::ECMAScript)
148  {
149  }
150  irep_idt operator()(const symbolt &, const std::string &);
151 
152 protected:
153  const std::regex forbidden;
154  const std::regex multi_under;
155 };
156 
162 {
163 public:
165  {
166  }
167  irep_idt operator()(const symbolt &, const std::string &);
168 };
169 
170 #endif // CPROVER_GOTO_PROGRAMS_NAME_MANGLER_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
file_name_manglert::forbidden
const std::regex forbidden
Definition: name_mangler.h:153
file_name_manglert::multi_under
const std::regex multi_under
Definition: name_mangler.h:154
djb_manglert::operator()
irep_idt operator()(const symbolt &, const std::string &)
Definition: name_mangler.cpp:34
typet
The type of an expression, extends irept.
Definition: type.h:29
function_name_manglert::model
goto_modelt & model
Definition: name_mangler.h:136
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
file_name_manglert::operator()
irep_idt operator()(const symbolt &, const std::string &)
Definition: name_mangler.cpp:17
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:53
file_name_manglert::file_name_manglert
file_name_manglert()
Definition: name_mangler.h:145
goto_modelt
Definition: goto_model.h:26
messaget::eom
static eomt eom
Definition: message.h:297
function_name_manglert::mangle
void mangle()
Mangle all file-local function symbols in the program.
Definition: name_mangler.h:49
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
rename_symbol.h
function_name_manglert
Mangles the names in an entire program and its symbol table.
Definition: name_mangler.h:31
function_name_manglert::mangle_fun
MangleFun mangle_fun
Definition: name_mangler.h:137
djb_manglert
Mangle identifiers by hashing their working directory with djb2 hash.
Definition: name_mangler.h:162
file_name_manglert
Mangle identifiers by including their filename.
Definition: name_mangler.h:143
function_name_manglert::log
messaget log
Definition: name_mangler.h:135
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
rename_symbolt::insert
void insert(const class symbol_exprt &old_expr, const class symbol_exprt &new_expr)
Definition: rename_symbol.cpp:23
function_name_manglert::extra_info
const std::string & extra_info
Definition: name_mangler.h:138
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:19
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
function_name_manglert::function_name_manglert
function_name_manglert(message_handlert &mh, goto_modelt &gm, const std::string &extra_info)
Definition: name_mangler.h:36
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
djb_manglert::djb_manglert
djb_manglert()
Definition: name_mangler.h:164
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
symbolt
Symbol table entry.
Definition: symbol.h:28
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
rename_symbolt
Definition: rename_symbol.h:26
symbol_tablet::erase
virtual void erase(const symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
Definition: symbol_table.cpp:92
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
messaget::debug
mstreamt & debug() const
Definition: message.h:429
message.h
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
validation_modet::INVARIANT
@ INVARIANT