cprover
name_mangler.h
Go to the documentation of this file.
1
4
5#ifndef CPROVER_GOTO_PROGRAMS_NAME_MANGLER_H
6#define CPROVER_GOTO_PROGRAMS_NAME_MANGLER_H
7
8#include <util/message.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
29template <class MangleFun>
31{
32public:
38 goto_modelt &gm,
39 const std::string &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_nonconst());
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
134protected:
135 mutable messaget log;
137 MangleFun mangle_fun;
138 const std::string &extra_info;
139};
140
143{
144public:
146 : forbidden("[^\\w]", std::regex::ECMAScript),
147 multi_under("_+", std::regex::ECMAScript)
148 {
149 }
150 irep_idt operator()(const symbolt &, const std::string &);
151
152protected:
153 const std::regex forbidden;
154 const std::regex multi_under;
155};
156
162{
163public:
165 {
166 }
167 irep_idt operator()(const symbolt &, const std::string &);
168};
169
170#endif // CPROVER_GOTO_PROGRAMS_NAME_MANGLER_H
Mangle identifiers by hashing their working directory with djb2 hash.
Definition: name_mangler.h:162
irep_idt operator()(const symbolt &, const std::string &)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
Mangle identifiers by including their filename.
Definition: name_mangler.h:143
irep_idt operator()(const symbolt &, const std::string &)
const std::regex multi_under
Definition: name_mangler.h:154
const std::regex forbidden
Definition: name_mangler.h:153
Mangles the names in an entire program and its symbol table.
Definition: name_mangler.h:31
void mangle()
Mangle all file-local function symbols in the program.
Definition: name_mangler.h:49
const std::string & extra_info
Definition: name_mangler.h:138
function_name_manglert(message_handlert &mh, goto_modelt &gm, const std::string &extra_info)
Definition: name_mangler.h:36
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & debug() const
Definition: message.h:429
static eomt eom
Definition: message.h:297
void insert(const class symbol_exprt &old_expr, const class symbol_exprt &new_expr)
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual void erase(const symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition: symbol.h:28
bool is_file_local
Definition: symbol.h:66
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt value
Initial value of symbol.
Definition: symbol.h:34
The type of an expression, extends irept.
Definition: type.h:29
Symbol Table + CFG.
STL namespace.