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 
27 template <class MangleFun>
29 {
30 public:
35  message_handlert &mh,
36  goto_modelt &gm,
37  const std::string &extra_info)
38  : log(mh), model(gm), mangle_fun(), extra_info(extra_info)
39  {
40  }
41 
47  void mangle()
48  {
49  rename_symbolt rename;
50  std::map<irep_idt, irep_idt> renamed_funs;
51  std::vector<symbolt> new_syms;
52  std::vector<symbol_tablet::symbolst::const_iterator> old_syms;
53 
54  for(auto sym_it = model.symbol_table.symbols.begin();
55  sym_it != model.symbol_table.symbols.end();
56  ++sym_it)
57  {
58  const symbolt &sym = sym_it->second;
59 
60  if(sym.type.id() != ID_code) // is not a function
61  continue;
62  if(sym.value.is_nil()) // has no body
63  continue;
64  if(!sym.is_file_local)
65  continue;
66 
67  const irep_idt mangled = mangle_fun(sym, extra_info);
68  symbolt new_sym;
69  new_sym = sym;
70  new_sym.name = mangled;
71  new_sym.is_file_local = false;
72 
73  new_syms.push_back(new_sym);
74  old_syms.push_back(sym_it);
75 
76  rename.insert(sym.symbol_expr(), new_sym.symbol_expr());
77  renamed_funs.insert(std::make_pair(sym.name, mangled));
78 
79  log.debug() << "Mangling: " << sym.name << " -> " << mangled << log.eom;
80  }
81 
82  for(const auto &sym : new_syms)
84  for(const auto &sym : old_syms)
86 
87  for(const auto &sym_pair : model.symbol_table)
88  {
89  const symbolt &sym = sym_pair.second;
90 
91  exprt e = sym.value;
92  typet t = sym.type;
93  if(rename(e) && rename(t))
94  continue;
95 
97  new_sym.value = e;
98  new_sym.type = t;
99  }
100 
101  for(auto &fun : model.goto_functions.function_map)
102  {
103  if(!fun.second.body_available())
104  continue;
105  for(auto &ins : fun.second.body.instructions)
106  {
107  rename(ins.code);
108  rename(ins.guard);
109  }
110  }
111 
112  // Add goto-programs with new function names
113  for(const auto &pair : renamed_funs)
114  {
115  auto found = model.goto_functions.function_map.find(pair.first);
116  INVARIANT(
117  found != model.goto_functions.function_map.end(),
118  "There should exist an entry in the function_map for the original name "
119  "of the function that we renamed '" +
120  std::string(pair.first.c_str()) + "'");
121 
122  auto inserted = model.goto_functions.function_map.emplace(
123  pair.second, std::move(found->second));
124  INVARIANT(
125  inserted.second,
126  "The mangled name '" + std::string(pair.second.c_str()) +
127  "' should not already exist in the codebase");
128 
129  model.goto_functions.function_map.erase(found);
130  }
131  }
132 
133 protected:
134  mutable messaget log;
136  MangleFun mangle_fun;
137  const std::string &extra_info;
138 };
139 
142 {
143 public:
145  : forbidden("[^\\w]", std::regex::ECMAScript),
146  multi_under("_+", std::regex::ECMAScript)
147  {
148  }
149  irep_idt operator()(const symbolt &, const std::string &);
150 
151 protected:
152  const std::regex forbidden;
153  const std::regex multi_under;
154 };
155 
161 {
162 public:
164  {
165  }
166  irep_idt operator()(const symbolt &, const std::string &);
167 };
168 
169 #endif // CPROVER_GOTO_PROGRAMS_NAME_MANGLER_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:152
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:152
file_name_manglert::multi_under
const std::regex multi_under
Definition: name_mangler.h:153
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:135
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
exprt
Base class for all expressions.
Definition: expr.h:53
file_name_manglert::file_name_manglert
file_name_manglert()
Definition: name_mangler.h:144
goto_modelt
Definition: goto_model.h:26
messaget::eom
static eomt eom
Definition: message.h:283
function_name_manglert::mangle
void mangle()
Mangle all file-local function symbols in the program.
Definition: name_mangler.h:47
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:29
function_name_manglert::mangle_fun
MangleFun mangle_fun
Definition: name_mangler.h:136
djb_manglert
Mangle identifiers by hashing their working directory with djb2 hash.
Definition: name_mangler.h:161
file_name_manglert
Mangle identifiers by including their filename.
Definition: name_mangler.h:142
function_name_manglert::log
messaget log
Definition: name_mangler.h:134
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:137
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:27
function_name_manglert::function_name_manglert
function_name_manglert(message_handlert &mh, goto_modelt &gm, const std::string &extra_info)
Definition: name_mangler.h:34
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
djb_manglert::djb_manglert
djb_manglert()
Definition: name_mangler.h:163
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:415
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