Skip to content

Commit 1614c2c

Browse files
smowtonsmowton
authored
Merge pull request #1462 from reuk/reuk/symbol-table-pointer
Return pointer from symbol table lookup
2 parents d19e737 + a9ba0f9 commit 1614c2c

31 files changed

+100
-111
lines changed

‎CODING_STANDARD.md

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -182,6 +182,11 @@ Here a few minimalistic coding rules for the CPROVER source tree.
182182
- Avoid `assert`. If the condition is an actual invariant, use INVARIANT,
183183
PRECONDITION, POSTCONDITION, CHECK_RETURN, UNREACHABLE or DATA_INVARIANT. If
184184
there are possible reasons why it might fail, throw an exception.
185+
- All raw pointers (such as those returned by `symbol_tablet::lookup`) are
186+
assumed to be non-owning, and should not be `delete`d. Raw pointers that
187+
point to heap-allocated memory should be private data members of an object
188+
which safely manages the pointer. As such, `new` should only be used in
189+
constructors, and `delete` in destructors. Never use `malloc` or `free`.
185190

186191
# Architecture-specific code
187192
- Avoid if possible.

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -208,7 +208,7 @@ void c_typecheck_baset::typecheck_type(typet &type)
208208
{
209209
const irep_idt &tag_name=
210210
to_c_enum_tag_type(type.subtype()).get_identifier();
211-
symbol_table.get_writeable(tag_name)->get().type.subtype()=result;
211+
symbol_table.get_writeable_ref(tag_name).type.subtype()=result;
212212
}
213213

214214
type=result;
@@ -782,7 +782,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
782782
type.set(ID_tag, base_name);
783783

784784
typecheck_compound_body(type);
785-
symbol_table.get_writeable(s_it->first)->get().type.swap(type);
785+
symbol_table.get_writeable_ref(s_it->first).type.swap(type);
786786
}
787787
}
788788
else if(have_body)
@@ -1220,7 +1220,7 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
12201220
{
12211221
// Ok, overwrite the type in the symbol table.
12221222
// This gives us the members and the subtype.
1223-
symbol_table.get_writeable(symbol.name)->get().type=enum_tag_symbol.type;
1223+
symbol_table.get_writeable_ref(symbol.name).type=enum_tag_symbol.type;
12241224
}
12251225
else if(symbol.type.id()==ID_c_enum)
12261226
{

‎src/cpp/cpp_declarator_converter.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -98,7 +98,7 @@ symbolt &cpp_declarator_convertert::convert(
9898
}
9999

100100
// try static first
101-
symbol_tablet::opt_symbol_reft maybe_symbol=
101+
auto maybe_symbol=
102102
cpp_typecheck.symbol_table.get_writeable(final_identifier);
103103

104104
if(!maybe_symbol)
@@ -191,7 +191,7 @@ symbolt &cpp_declarator_convertert::convert(
191191
}
192192

193193
// already there?
194-
symbol_tablet::opt_symbol_reft maybe_symbol=
194+
const auto maybe_symbol=
195195
cpp_typecheck.symbol_table.get_writeable(final_identifier);
196196
if(!maybe_symbol)
197197
return convert_new_symbol(storage_spec, member_spec, declarator);

‎src/cpp/cpp_typecheck.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,7 @@ void cpp_typecheckt::static_and_dynamic_initialization()
178178

179179
// Make it nil to get zero initialization by
180180
// __CPROVER_initialize
181-
symbol_table.get_writeable(d_it)->get().value.make_nil();
181+
symbol_table.get_writeable_ref(d_it).value.make_nil();
182182
}
183183
else
184184
{
@@ -260,7 +260,7 @@ void cpp_typecheckt::do_not_typechecked()
260260
for(const auto &named_symbol : symbol_table.symbols)
261261
{
262262
if(named_symbol.second.value.id()=="cpp_not_typechecked")
263-
symbol_table.get_writeable(named_symbol.first)->get().value.make_nil();
263+
symbol_table.get_writeable_ref(named_symbol.first).value.make_nil();
264264
}
265265
}
266266

@@ -286,7 +286,7 @@ void cpp_typecheckt::clean_up()
286286
{
287287
// remove methods from 'components'
288288
struct_union_typet &struct_union_type=to_struct_union_type(
289-
symbol_table.get_writeable(cur_it->first)->get().type);
289+
symbol_table.get_writeable_ref(cur_it->first).type);
290290

291291
const struct_union_typet::componentst &components=
292292
struct_union_type.components();

‎src/cpp/cpp_typecheck_compound_type.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -159,9 +159,7 @@ void cpp_typecheckt::typecheck_compound_type(
159159

160160
// check if we have it already
161161

162-
symbol_tablet::opt_const_symbol_reft maybe_symbol=
163-
symbol_table.lookup(symbol_name);
164-
if(maybe_symbol)
162+
if(const auto maybe_symbol=symbol_table.lookup(symbol_name))
165163
{
166164
// we do!
167165
const symbolt &symbol=*maybe_symbol;
@@ -553,7 +551,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
553551
put_compound_into_scope(compo);
554552
}
555553

556-
typet &vt=symbol_table.get_writeable(vt_name)->get().type;
554+
typet &vt=symbol_table.get_writeable_ref(vt_name).type;
557555
INVARIANT(vt.id()==ID_struct, "Virtual tables must be stored as struct");
558556
struct_typet &virtual_table=to_struct_type(vt);
559557

‎src/cpp/cpp_typecheck_declaration.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@ void cpp_typecheckt::convert_anonymous_union(
105105
id.is_member=true;
106106
}
107107

108-
symbol_table.get_writeable(union_symbol.name)->get().type.set(
108+
symbol_table.get_writeable_ref(union_symbol.name).type.set(
109109
"#unnamed_object", symbol.base_name);
110110

111111
code.swap(new_code);

‎src/cpp/cpp_typecheck_expr.cpp

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1244,8 +1244,7 @@ void cpp_typecheckt::typecheck_expr_member(
12441244
assert(it!=symbol_table.symbols.end());
12451245

12461246
if(it->second.value.id()=="cpp_not_typechecked")
1247-
symbol_table.get_writeable(component_name)->get()
1248-
.value.set("is_used", true);
1247+
symbol_table.get_writeable_ref(component_name).value.set("is_used", true);
12491248
}
12501249
}
12511250

@@ -2203,7 +2202,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
22032202
type.id()==ID_code &&
22042203
type.find(ID_return_type).id()==ID_destructor)
22052204
{
2206-
add_method_body(&symbol_table.get_writeable(it->get(ID_name))->get());
2205+
add_method_body(&symbol_table.get_writeable_ref(it->get(ID_name)));
22072206
break;
22082207
}
22092208
}
@@ -2372,7 +2371,7 @@ void cpp_typecheckt::typecheck_method_application(
23722371
member_expr.swap(expr.function());
23732372

23742373
const symbolt &symbol=lookup(member_expr.get(ID_component_name));
2375-
add_method_body(&symbol_table.get_writeable(symbol.name)->get());
2374+
add_method_body(&symbol_table.get_writeable_ref(symbol.name));
23762375

23772376
// build new function expression
23782377
exprt new_function(cpp_symbol_expr(symbol));
@@ -2414,7 +2413,7 @@ void cpp_typecheckt::typecheck_method_application(
24142413
if(symbol.value.id()=="cpp_not_typechecked" &&
24152414
!symbol.value.get_bool("is_used"))
24162415
{
2417-
symbol_table.get_writeable(symbol.name)->get().value.set("is_used", true);
2416+
symbol_table.get_writeable_ref(symbol.name).value.set("is_used", true);
24182417
}
24192418
}
24202419

@@ -2683,7 +2682,7 @@ void cpp_typecheckt::typecheck_expr_function_identifier(exprt &expr)
26832682
assert(it != symbol_table.symbols.end());
26842683

26852684
if(it->second.value.id()=="cpp_not_typechecked")
2686-
symbol_table.get_writeable(it->first)->get().value.set("is_used", true);
2685+
symbol_table.get_writeable_ref(it->first).value.set("is_used", true);
26872686
}
26882687

26892688
c_typecheck_baset::typecheck_expr_function_identifier(expr);

‎src/cpp/cpp_typecheck_template.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -107,9 +107,7 @@ void cpp_typecheckt::typecheck_class_template(
107107

108108
// check if we have it already
109109

110-
symbol_tablet::opt_symbol_reft maybe_symbol=
111-
symbol_table.get_writeable(symbol_name);
112-
if(maybe_symbol)
110+
if(const auto maybe_symbol=symbol_table.get_writeable(symbol_name))
113111
{
114112
// there already
115113
symbolt &previous_symbol=*maybe_symbol;
@@ -265,7 +263,7 @@ void cpp_typecheckt::typecheck_function_template(
265263

266264
if(has_value)
267265
{
268-
symbol_table.get_writeable(symbol_name)->get().type.swap(declaration);
266+
symbol_table.get_writeable_ref(symbol_name).type.swap(declaration);
269267
cpp_scopes.id_map[symbol_name]=&template_scope;
270268
}
271269

‎src/goto-cc/compile.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -725,7 +725,7 @@ void compilet::convert_symbols(goto_functionst &dest)
725725
{
726726
debug() << "Compiling " << s_it->first << eom;
727727
converter.convert_function(s_it->first);
728-
symbol_table.get_writeable(*it)->get().value=exprt("compiled");
728+
symbol_table.get_writeable_ref(*it).value=exprt("compiled");
729729
}
730730
}
731731
}

‎src/goto-cc/linker_script_merge.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -168,8 +168,7 @@ int linker_script_merget::pointerize_linker_defined_symbols(
168168
// First, pointerize the actual linker-defined symbols
169169
for(const auto &pair : linker_values)
170170
{
171-
symbol_tablet::opt_symbol_reft maybe_symbol=
172-
symbol_table.get_writeable(pair.first);
171+
const auto maybe_symbol=symbol_table.get_writeable(pair.first);
173172
if(!maybe_symbol)
174173
continue;
175174
symbolt &entry=*maybe_symbol;
@@ -190,7 +189,7 @@ int linker_script_merget::pointerize_linker_defined_symbols(
190189
debug() << "Pointerizing the symbol-table value of symbol " << pair.first
191190
<< eom;
192191
int fail=pointerize_subexprs_of(
193-
symbol_table.get_writeable(pair.first)->get().value,
192+
symbol_table.get_writeable_ref(pair.first).value,
194193
to_pointerize,
195194
linker_values);
196195
if(to_pointerize.empty() && fail==0)

‎src/goto-instrument/dump_c.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ void dump_ct::operator()(std::ostream &os)
5555
continue;
5656

5757
code_typet &code_type=to_code_type(
58-
copied_symbol_table.get_writeable(named_symbol.first)->get().type);
58+
copied_symbol_table.get_writeable_ref(named_symbol.first).type);
5959
code_typet::parameterst &parameters=code_type.parameters();
6060

6161
for(code_typet::parameterst::iterator

‎src/goto-instrument/goto_program2code.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -134,7 +134,7 @@ void goto_program2codet::scan_for_varargs()
134134
system_headers.insert("stdarg.h");
135135

136136
code_typet &code_type=
137-
to_code_type(symbol_table.get_writeable(func_name)->get().type);
137+
to_code_type(symbol_table.get_writeable_ref(func_name).type);
138138
code_typet::parameterst &parameters=code_type.parameters();
139139

140140
for(code_typet::parameterst::iterator

‎src/goto-instrument/remove_function.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ void remove_function(
5151
message.status() << "Removing body of " << identifier
5252
<< messaget::eom;
5353
entry->second.clear();
54-
goto_model.symbol_table.get_writeable(identifier)->get().value.make_nil();
54+
goto_model.symbol_table.get_writeable_ref(identifier).value.make_nil();
5555
}
5656
}
5757

‎src/goto-instrument/wmm/shared_buffers.h

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -158,11 +158,10 @@ class shared_bufferst
158158

159159
irep_idt choice(const irep_idt &function, const std::string &suffix)
160160
{
161-
symbol_tablet::opt_const_symbol_reft maybe_symbol=
162-
symbol_table.lookup(function);
161+
const auto maybe_symbol=symbol_table.lookup(function);
163162
const std::string function_base_name =
164163
maybe_symbol
165-
? id2string(maybe_symbol->get().base_name)
164+
? id2string(maybe_symbol->base_name)
166165
: "main";
167166
return add(function_base_name+"_weak_choice",
168167
function_base_name+"_weak_choice", suffix, bool_typet());

‎src/goto-programs/interpreter.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -444,7 +444,7 @@ typet interpretert::get_type(const irep_idt &id) const
444444
{
445445
dynamic_typest::const_iterator it=dynamic_types.find(id);
446446
if(it==dynamic_types.end())
447-
return symbol_table.lookup(id)->get().type;
447+
return symbol_table.lookup_ref(id).type;
448448
return it->second;
449449
}
450450

@@ -1041,7 +1041,7 @@ exprt interpretert::get_value(const irep_idt &id)
10411041
if(findit!=dynamic_types.end())
10421042
get_type=findit->second;
10431043
else
1044-
get_type=symbol_table.lookup(id)->get().type;
1044+
get_type=symbol_table.lookup_ref(id).type;
10451045

10461046
symbol_exprt symbol_expr(id, get_type);
10471047
mp_integer whole_lhs_object_address=evaluate_address(symbol_expr);

‎src/goto-programs/mm_io.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -118,13 +118,13 @@ void mm_io(
118118
irep_idt id_r=CPROVER_PREFIX "mm_io_r";
119119
irep_idt id_w=CPROVER_PREFIX "mm_io_w";
120120

121-
symbol_tablet::opt_const_symbol_reft maybe_symbol=symbol_table.lookup(id_r);
121+
auto maybe_symbol=symbol_table.lookup(id_r);
122122
if(maybe_symbol)
123-
mm_io_r=maybe_symbol->get().symbol_expr();
123+
mm_io_r=maybe_symbol->symbol_expr();
124124

125125
maybe_symbol=symbol_table.lookup(id_w);
126126
if(maybe_symbol)
127-
mm_io_w=maybe_symbol->get().symbol_expr();
127+
mm_io_w=maybe_symbol->symbol_expr();
128128

129129
for(auto & f : goto_functions.function_map)
130130
mm_io(mm_io_r, mm_io_w, f.second, ns);

‎src/goto-programs/remove_exceptions.cpp

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -134,8 +134,7 @@ void remove_exceptionst::add_exceptional_returns(
134134
const irep_idt &function_id=func_it->first;
135135
goto_programt &goto_program=func_it->second.body;
136136

137-
symbol_tablet::opt_const_symbol_reft maybe_symbol=
138-
symbol_table.lookup(function_id);
137+
auto maybe_symbol=symbol_table.lookup(function_id);
139138
INVARIANT(maybe_symbol, "functions should be recorded in the symbol table");
140139
const symbolt &function_symbol=*maybe_symbol;
141140

@@ -255,11 +254,9 @@ void remove_exceptionst::instrument_exception_handler(
255254
to_code_landingpad(instr_it->code).catch_expr();
256255
irep_idt thrown_exception_global=id2string(function_id)+EXC_SUFFIX;
257256

258-
symbol_tablet::opt_const_symbol_reft maybe_symbol=
259-
symbol_table.lookup(thrown_exception_global);
260-
if(maybe_symbol)
257+
if(const auto maybe_symbol=symbol_table.lookup(thrown_exception_global))
261258
{
262-
const symbol_exprt thrown_global_symbol=maybe_symbol->get().symbol_expr();
259+
const symbol_exprt thrown_global_symbol=maybe_symbol->symbol_expr();
263260
// next we reset the exceptional return to NULL
264261
null_pointer_exprt null_voidptr((pointer_type(empty_typet())));
265262

@@ -425,9 +422,9 @@ void remove_exceptionst::instrument_function_call(
425422
const irep_idt &callee_id=
426423
to_symbol_expr(function_call.function()).get_identifier();
427424

428-
symbol_tablet::opt_const_symbol_reft callee_inflight_exception=
425+
const auto callee_inflight_exception=
429426
symbol_table.lookup(id2string(callee_id)+EXC_SUFFIX);
430-
symbol_tablet::opt_const_symbol_reft local_inflight_exception=
427+
const auto local_inflight_exception=
431428
symbol_table.lookup(id2string(function_id)+EXC_SUFFIX);
432429

433430
if(callee_inflight_exception && local_inflight_exception)
@@ -436,9 +433,9 @@ void remove_exceptionst::instrument_function_call(
436433
func_it, instr_it, stack_catch, locals);
437434

438435
const symbol_exprt callee_inflight_exception_expr=
439-
callee_inflight_exception->get().symbol_expr();
436+
callee_inflight_exception->symbol_expr();
440437
const symbol_exprt local_inflight_exception_expr=
441-
local_inflight_exception->get().symbol_expr();
438+
local_inflight_exception->symbol_expr();
442439

443440
// add a null check (so that instanceof can be applied)
444441
equal_exprt eq_null(

‎src/goto-programs/remove_static_init_loops.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -58,8 +58,7 @@ void remove_static_init_loopst::unwind_enum_static(
5858
const std::string &fname=id2string(ins.function);
5959
size_t class_prefix_length=fname.find_last_of('.');
6060
// is the function symbol in the symbol table?
61-
symbol_tablet::opt_const_symbol_reft maybe_symbol=
62-
symbol_table.lookup(ins.function);
61+
const auto maybe_symbol=symbol_table.lookup(ins.function);
6362
if(!maybe_symbol)
6463
{
6564
message.warning() << "function `" << id2string(ins.function)

‎src/java_bytecode/ci_lazy_methods.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -144,7 +144,7 @@ bool ci_lazy_methodst::operator()(
144144
method_converter(
145145
*parsed_method.first, *parsed_method.second, new_lazy_methods);
146146
gather_virtual_callsites(
147-
symbol_table.lookup(mname)->get().value,
147+
symbol_table.lookup_ref(mname).value,
148148
virtual_callsites);
149149
any_new_methods=true;
150150
}

‎src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -893,8 +893,7 @@ bool java_bytecode_convert_methodt::class_needs_clinit(
893893
findit_any.first->second=true;
894894
return true;
895895
}
896-
symbol_tablet::opt_const_symbol_reft maybe_symbol=
897-
symbol_table.lookup(classname);
896+
const auto maybe_symbol=symbol_table.lookup(classname);
898897
// Stub class?
899898
if(!maybe_symbol)
900899
{

‎src/java_bytecode/java_bytecode_instrument.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -617,5 +617,5 @@ void java_bytecode_instrument(
617617
// instrument(...) can add symbols to the table, so it's
618618
// not safe to hold a reference to a symbol across a call.
619619
for(const auto &symbol : symbols_to_instrument)
620-
instrument(symbol_table.get_writeable(symbol)->get().value);
620+
instrument(symbol_table.get_writeable_ref(symbol).value);
621621
}

0 commit comments

Comments
 (0)