cprover
Loading...
Searching...
No Matches
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 = sym;
71 new_sym.name = mangled;
72 new_sym.base_name = mangled;
73 if(new_sym.pretty_name.empty())
74 new_sym.pretty_name = sym.base_name;
75 new_sym.is_file_local = false;
76
77 new_syms.push_back(new_sym);
78 old_syms.push_back(sym_it);
79
80 rename.insert(sym.symbol_expr(), new_sym.symbol_expr());
81 renamed_funs.insert(std::make_pair(sym.name, mangled));
82
83 log.debug() << "Mangling: " << sym.name << " -> " << mangled << log.eom;
84 }
85
86 for(const auto &sym : new_syms)
87 model.symbol_table.insert(sym);
88 for(const auto &sym : old_syms)
89 model.symbol_table.erase(sym);
90
91 for(auto it = model.symbol_table.begin(); it != model.symbol_table.end();
92 ++it)
93 {
94 const symbolt &sym = it->second;
95
96 exprt e = sym.value;
97 typet t = sym.type;
98 if(rename(e) && rename(t))
99 continue;
100
101 symbolt &new_sym = it.get_writeable_symbol();
102 new_sym.value = e;
103 new_sym.type = t;
104 }
105
106 for(auto &fun : model.goto_functions.function_map)
107 {
108 if(!fun.second.body_available())
109 continue;
110 for(auto &ins : fun.second.body.instructions)
111 {
112 rename(ins.code_nonconst());
113 if(ins.has_condition())
114 rename(ins.condition_nonconst());
115 }
116 }
117
118 // Add goto-programs with new function names
119 for(const auto &pair : renamed_funs)
120 {
121 auto found = model.goto_functions.function_map.find(pair.first);
122 INVARIANT(
123 found != model.goto_functions.function_map.end(),
124 "There should exist an entry in the function_map for the original name "
125 "of the function that we renamed '" +
126 std::string(pair.first.c_str()) + "'");
127
128 auto inserted = model.goto_functions.function_map.emplace(
129 pair.second, std::move(found->second));
130 if(!inserted.second)
131 log.debug() << "Found a mangled name that already exists: "
132 << std::string(pair.second.c_str()) << log.eom;
133
134 model.goto_functions.function_map.erase(found);
135 }
136 }
137
138protected:
139 mutable messaget log;
141 MangleFun mangle_fun;
142 const std::string &extra_info;
143};
144
147{
148public:
150 : forbidden("[^\\w]", std::regex::ECMAScript),
151 multi_under("_+", std::regex::ECMAScript)
152 {
153 }
154 irep_idt operator()(const symbolt &, const std::string &);
155
156protected:
157 const std::regex forbidden;
158 const std::regex multi_under;
159};
160
166{
167public:
169 {
170 }
171 irep_idt operator()(const symbolt &, const std::string &);
172};
173
174#endif // CPROVER_GOTO_PROGRAMS_NAME_MANGLER_H
irep_idt operator()(const symbolt &, const std::string &)
bool empty() const
Definition dstring.h:89
Base class for all expressions.
Definition expr.h:56
irep_idt operator()(const symbolt &, const std::string &)
const std::regex multi_under
const std::regex forbidden
void mangle()
Mangle all file-local function symbols in the program.
const std::string & extra_info
function_name_manglert(message_handlert &mh, goto_modelt &gm, const std::string &extra_info)
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
void insert(const class symbol_exprt &old_expr, const class symbol_exprt &new_expr)
Symbol table entry.
Definition symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
bool is_file_local
Definition symbol.h:73
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
irep_idt pretty_name
Language-specific display name.
Definition symbol.h:52
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.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
dstringt irep_idt