Skip to content

Return pointer from symbol table lookup #1462

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Oct 11, 2017
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions CODING_STANDARD.md
Original file line number Diff line number Diff line change
Expand Up @@ -182,6 +182,11 @@ Here a few minimalistic coding rules for the CPROVER source tree.
- Avoid `assert`. If the condition is an actual invariant, use INVARIANT,
PRECONDITION, POSTCONDITION, CHECK_RETURN, UNREACHABLE or DATA_INVARIANT. If
there are possible reasons why it might fail, throw an exception.
- All raw pointers (such as those returned by `symbol_tablet::lookup`) are
assumed to be non-owning, and should not be `delete`d. Raw pointers that
point to heap-allocated memory should be private data members of an object
which safely manages the pointer. As such, `new` should only be used in
constructors, and `delete` in destructors. Never use `malloc` or `free`.

# Architecture-specific code
- Avoid if possible.
Expand Down
6 changes: 3 additions & 3 deletions src/ansi-c/c_typecheck_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -208,7 +208,7 @@ void c_typecheck_baset::typecheck_type(typet &type)
{
const irep_idt &tag_name=
to_c_enum_tag_type(type.subtype()).get_identifier();
symbol_table.get_writeable(tag_name)->get().type.subtype()=result;
symbol_table.get_writeable_ref(tag_name).type.subtype()=result;
}

type=result;
Expand Down Expand Up @@ -782,7 +782,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
type.set(ID_tag, base_name);

typecheck_compound_body(type);
symbol_table.get_writeable(s_it->first)->get().type.swap(type);
symbol_table.get_writeable_ref(s_it->first).type.swap(type);
}
}
else if(have_body)
Expand Down Expand Up @@ -1220,7 +1220,7 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
{
// Ok, overwrite the type in the symbol table.
// This gives us the members and the subtype.
symbol_table.get_writeable(symbol.name)->get().type=enum_tag_symbol.type;
symbol_table.get_writeable_ref(symbol.name).type=enum_tag_symbol.type;
}
else if(symbol.type.id()==ID_c_enum)
{
Expand Down
4 changes: 2 additions & 2 deletions src/cpp/cpp_declarator_converter.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@ symbolt &cpp_declarator_convertert::convert(
}

// try static first
symbol_tablet::opt_symbol_reft maybe_symbol=
auto maybe_symbol=
cpp_typecheck.symbol_table.get_writeable(final_identifier);

if(!maybe_symbol)
Expand Down Expand Up @@ -191,7 +191,7 @@ symbolt &cpp_declarator_convertert::convert(
}

// already there?
symbol_tablet::opt_symbol_reft maybe_symbol=
const auto maybe_symbol=
cpp_typecheck.symbol_table.get_writeable(final_identifier);
if(!maybe_symbol)
return convert_new_symbol(storage_spec, member_spec, declarator);
Expand Down
6 changes: 3 additions & 3 deletions src/cpp/cpp_typecheck.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -178,7 +178,7 @@ void cpp_typecheckt::static_and_dynamic_initialization()

// Make it nil to get zero initialization by
// __CPROVER_initialize
symbol_table.get_writeable(d_it)->get().value.make_nil();
symbol_table.get_writeable_ref(d_it).value.make_nil();
}
else
{
Expand Down Expand Up @@ -260,7 +260,7 @@ void cpp_typecheckt::do_not_typechecked()
for(const auto &named_symbol : symbol_table.symbols)
{
if(named_symbol.second.value.id()=="cpp_not_typechecked")
symbol_table.get_writeable(named_symbol.first)->get().value.make_nil();
symbol_table.get_writeable_ref(named_symbol.first).value.make_nil();
}
}

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

const struct_union_typet::componentst &components=
struct_union_type.components();
Expand Down
6 changes: 2 additions & 4 deletions src/cpp/cpp_typecheck_compound_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -159,9 +159,7 @@ void cpp_typecheckt::typecheck_compound_type(

// check if we have it already

symbol_tablet::opt_const_symbol_reft maybe_symbol=
symbol_table.lookup(symbol_name);
if(maybe_symbol)
if(const auto maybe_symbol=symbol_table.lookup(symbol_name))
{
// we do!
const symbolt &symbol=*maybe_symbol;
Expand Down Expand Up @@ -553,7 +551,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
put_compound_into_scope(compo);
}

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

Expand Down
2 changes: 1 addition & 1 deletion src/cpp/cpp_typecheck_declaration.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ void cpp_typecheckt::convert_anonymous_union(
id.is_member=true;
}

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

code.swap(new_code);
Expand Down
11 changes: 5 additions & 6 deletions src/cpp/cpp_typecheck_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1244,8 +1244,7 @@ void cpp_typecheckt::typecheck_expr_member(
assert(it!=symbol_table.symbols.end());

if(it->second.value.id()=="cpp_not_typechecked")
symbol_table.get_writeable(component_name)->get()
.value.set("is_used", true);
symbol_table.get_writeable_ref(component_name).value.set("is_used", true);
}
}

Expand Down Expand Up @@ -2203,7 +2202,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
type.id()==ID_code &&
type.find(ID_return_type).id()==ID_destructor)
{
add_method_body(&symbol_table.get_writeable(it->get(ID_name))->get());
add_method_body(&symbol_table.get_writeable_ref(it->get(ID_name)));
break;
}
}
Expand Down Expand Up @@ -2372,7 +2371,7 @@ void cpp_typecheckt::typecheck_method_application(
member_expr.swap(expr.function());

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

// build new function expression
exprt new_function(cpp_symbol_expr(symbol));
Expand Down Expand Up @@ -2414,7 +2413,7 @@ void cpp_typecheckt::typecheck_method_application(
if(symbol.value.id()=="cpp_not_typechecked" &&
!symbol.value.get_bool("is_used"))
{
symbol_table.get_writeable(symbol.name)->get().value.set("is_used", true);
symbol_table.get_writeable_ref(symbol.name).value.set("is_used", true);
}
}

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

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

c_typecheck_baset::typecheck_expr_function_identifier(expr);
Expand Down
6 changes: 2 additions & 4 deletions src/cpp/cpp_typecheck_template.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -107,9 +107,7 @@ void cpp_typecheckt::typecheck_class_template(

// check if we have it already

symbol_tablet::opt_symbol_reft maybe_symbol=
symbol_table.get_writeable(symbol_name);
if(maybe_symbol)
if(const auto maybe_symbol=symbol_table.get_writeable(symbol_name))
{
// there already
symbolt &previous_symbol=*maybe_symbol;
Expand Down Expand Up @@ -265,7 +263,7 @@ void cpp_typecheckt::typecheck_function_template(

if(has_value)
{
symbol_table.get_writeable(symbol_name)->get().type.swap(declaration);
symbol_table.get_writeable_ref(symbol_name).type.swap(declaration);
cpp_scopes.id_map[symbol_name]=&template_scope;
}

Expand Down
2 changes: 1 addition & 1 deletion src/goto-cc/compile.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -725,7 +725,7 @@ void compilet::convert_symbols(goto_functionst &dest)
{
debug() << "Compiling " << s_it->first << eom;
converter.convert_function(s_it->first);
symbol_table.get_writeable(*it)->get().value=exprt("compiled");
symbol_table.get_writeable_ref(*it).value=exprt("compiled");
}
}
}
Expand Down
5 changes: 2 additions & 3 deletions src/goto-cc/linker_script_merge.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -168,8 +168,7 @@ int linker_script_merget::pointerize_linker_defined_symbols(
// First, pointerize the actual linker-defined symbols
for(const auto &pair : linker_values)
{
symbol_tablet::opt_symbol_reft maybe_symbol=
symbol_table.get_writeable(pair.first);
const auto maybe_symbol=symbol_table.get_writeable(pair.first);
if(!maybe_symbol)
continue;
symbolt &entry=*maybe_symbol;
Expand All @@ -190,7 +189,7 @@ int linker_script_merget::pointerize_linker_defined_symbols(
debug() << "Pointerizing the symbol-table value of symbol " << pair.first
<< eom;
int fail=pointerize_subexprs_of(
symbol_table.get_writeable(pair.first)->get().value,
symbol_table.get_writeable_ref(pair.first).value,
to_pointerize,
linker_values);
if(to_pointerize.empty() && fail==0)
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/dump_c.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ void dump_ct::operator()(std::ostream &os)
continue;

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

for(code_typet::parameterst::iterator
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/goto_program2code.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,7 @@ void goto_program2codet::scan_for_varargs()
system_headers.insert("stdarg.h");

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

for(code_typet::parameterst::iterator
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/remove_function.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ void remove_function(
message.status() << "Removing body of " << identifier
<< messaget::eom;
entry->second.clear();
goto_model.symbol_table.get_writeable(identifier)->get().value.make_nil();
goto_model.symbol_table.get_writeable_ref(identifier).value.make_nil();
}
}

Expand Down
5 changes: 2 additions & 3 deletions src/goto-instrument/wmm/shared_buffers.h
Original file line number Diff line number Diff line change
Expand Up @@ -158,11 +158,10 @@ class shared_bufferst

irep_idt choice(const irep_idt &function, const std::string &suffix)
{
symbol_tablet::opt_const_symbol_reft maybe_symbol=
symbol_table.lookup(function);
const auto maybe_symbol=symbol_table.lookup(function);
const std::string function_base_name =
maybe_symbol
? id2string(maybe_symbol->get().base_name)
? id2string(maybe_symbol->base_name)
: "main";
return add(function_base_name+"_weak_choice",
function_base_name+"_weak_choice", suffix, bool_typet());
Expand Down
4 changes: 2 additions & 2 deletions src/goto-programs/interpreter.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -444,7 +444,7 @@ typet interpretert::get_type(const irep_idt &id) const
{
dynamic_typest::const_iterator it=dynamic_types.find(id);
if(it==dynamic_types.end())
return symbol_table.lookup(id)->get().type;
return symbol_table.lookup_ref(id).type;
return it->second;
}

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

symbol_exprt symbol_expr(id, get_type);
mp_integer whole_lhs_object_address=evaluate_address(symbol_expr);
Expand Down
6 changes: 3 additions & 3 deletions src/goto-programs/mm_io.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -118,13 +118,13 @@ void mm_io(
irep_idt id_r=CPROVER_PREFIX "mm_io_r";
irep_idt id_w=CPROVER_PREFIX "mm_io_w";

symbol_tablet::opt_const_symbol_reft maybe_symbol=symbol_table.lookup(id_r);
auto maybe_symbol=symbol_table.lookup(id_r);
if(maybe_symbol)
mm_io_r=maybe_symbol->get().symbol_expr();
mm_io_r=maybe_symbol->symbol_expr();

maybe_symbol=symbol_table.lookup(id_w);
if(maybe_symbol)
mm_io_w=maybe_symbol->get().symbol_expr();
mm_io_w=maybe_symbol->symbol_expr();

for(auto & f : goto_functions.function_map)
mm_io(mm_io_r, mm_io_w, f.second, ns);
Expand Down
17 changes: 7 additions & 10 deletions src/goto-programs/remove_exceptions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -134,8 +134,7 @@ void remove_exceptionst::add_exceptional_returns(
const irep_idt &function_id=func_it->first;
goto_programt &goto_program=func_it->second.body;

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

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

symbol_tablet::opt_const_symbol_reft maybe_symbol=
symbol_table.lookup(thrown_exception_global);
if(maybe_symbol)
if(const auto maybe_symbol=symbol_table.lookup(thrown_exception_global))
{
const symbol_exprt thrown_global_symbol=maybe_symbol->get().symbol_expr();
const symbol_exprt thrown_global_symbol=maybe_symbol->symbol_expr();
// next we reset the exceptional return to NULL
null_pointer_exprt null_voidptr((pointer_type(empty_typet())));

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

symbol_tablet::opt_const_symbol_reft callee_inflight_exception=
const auto callee_inflight_exception=
symbol_table.lookup(id2string(callee_id)+EXC_SUFFIX);
symbol_tablet::opt_const_symbol_reft local_inflight_exception=
const auto local_inflight_exception=
symbol_table.lookup(id2string(function_id)+EXC_SUFFIX);

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

const symbol_exprt callee_inflight_exception_expr=
callee_inflight_exception->get().symbol_expr();
callee_inflight_exception->symbol_expr();
const symbol_exprt local_inflight_exception_expr=
local_inflight_exception->get().symbol_expr();
local_inflight_exception->symbol_expr();

// add a null check (so that instanceof can be applied)
equal_exprt eq_null(
Expand Down
3 changes: 1 addition & 2 deletions src/goto-programs/remove_static_init_loops.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -58,8 +58,7 @@ void remove_static_init_loopst::unwind_enum_static(
const std::string &fname=id2string(ins.function);
size_t class_prefix_length=fname.find_last_of('.');
// is the function symbol in the symbol table?
symbol_tablet::opt_const_symbol_reft maybe_symbol=
symbol_table.lookup(ins.function);
const auto maybe_symbol=symbol_table.lookup(ins.function);
if(!maybe_symbol)
{
message.warning() << "function `" << id2string(ins.function)
Expand Down
2 changes: 1 addition & 1 deletion src/java_bytecode/ci_lazy_methods.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,7 @@ bool ci_lazy_methodst::operator()(
method_converter(
*parsed_method.first, *parsed_method.second, new_lazy_methods);
gather_virtual_callsites(
symbol_table.lookup(mname)->get().value,
symbol_table.lookup_ref(mname).value,
virtual_callsites);
any_new_methods=true;
}
Expand Down
3 changes: 1 addition & 2 deletions src/java_bytecode/java_bytecode_convert_method.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -893,8 +893,7 @@ bool java_bytecode_convert_methodt::class_needs_clinit(
findit_any.first->second=true;
return true;
}
symbol_tablet::opt_const_symbol_reft maybe_symbol=
symbol_table.lookup(classname);
const auto maybe_symbol=symbol_table.lookup(classname);
// Stub class?
if(!maybe_symbol)
{
Expand Down
2 changes: 1 addition & 1 deletion src/java_bytecode/java_bytecode_instrument.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -617,5 +617,5 @@ void java_bytecode_instrument(
// instrument(...) can add symbols to the table, so it's
// not safe to hold a reference to a symbol across a call.
for(const auto &symbol : symbols_to_instrument)
instrument(symbol_table.get_writeable(symbol)->get().value);
instrument(symbol_table.get_writeable_ref(symbol).value);
}
Loading