diff --git a/CODING_STANDARD.md b/CODING_STANDARD.md index 06c6bf53666..3b62c9b45e4 100644 --- a/CODING_STANDARD.md +++ b/CODING_STANDARD.md @@ -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. diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 1cc2ac95cc0..5cc151ffac9 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -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; @@ -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) @@ -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) { diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp index bdc977eff6f..8e3deb08872 100644 --- a/src/cpp/cpp_declarator_converter.cpp +++ b/src/cpp/cpp_declarator_converter.cpp @@ -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) @@ -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); diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 570acc0aa1a..549a5b6d77d 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -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 { @@ -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(); } } @@ -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(); diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 4796f5e3d76..9818be9176a 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -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; @@ -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); diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp index 988b4de3568..082b5fcbbab 100644 --- a/src/cpp/cpp_typecheck_declaration.cpp +++ b/src/cpp/cpp_typecheck_declaration.cpp @@ -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); diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index b0a4a450395..0142c44780f 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -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); } } @@ -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; } } @@ -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)); @@ -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); } } @@ -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); diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp index feecc6ea169..6654db1cf3f 100644 --- a/src/cpp/cpp_typecheck_template.cpp +++ b/src/cpp/cpp_typecheck_template.cpp @@ -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; @@ -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; } diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 530e074bd88..9ace2924747 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -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"); } } } diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index 8d683aa4418..874e51e0d97 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -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; @@ -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) diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 2384f225513..6bb3b3644f2 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -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 ¶meters=code_type.parameters(); for(code_typet::parameterst::iterator diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 99444893dfb..70c2cc243b0 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -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 ¶meters=code_type.parameters(); for(code_typet::parameterst::iterator diff --git a/src/goto-instrument/remove_function.cpp b/src/goto-instrument/remove_function.cpp index f9344f68238..6376b4a5512 100644 --- a/src/goto-instrument/remove_function.cpp +++ b/src/goto-instrument/remove_function.cpp @@ -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(); } } diff --git a/src/goto-instrument/wmm/shared_buffers.h b/src/goto-instrument/wmm/shared_buffers.h index a3b87a26d86..7f946522858 100644 --- a/src/goto-instrument/wmm/shared_buffers.h +++ b/src/goto-instrument/wmm/shared_buffers.h @@ -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()); diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index b3ba928bcca..b2542cbeee7 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -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; } @@ -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); diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index 56313c42201..2ff0ee9da12 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -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); diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index a2cfcc10947..a49dcb12a4e 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -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; @@ -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()))); @@ -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) @@ -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( diff --git a/src/goto-programs/remove_static_init_loops.cpp b/src/goto-programs/remove_static_init_loops.cpp index 794ec547fc4..e9411beeb5b 100644 --- a/src/goto-programs/remove_static_init_loops.cpp +++ b/src/goto-programs/remove_static_init_loops.cpp @@ -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) diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp index 240dafc0e29..b0fc17fb03b 100644 --- a/src/java_bytecode/ci_lazy_methods.cpp +++ b/src/java_bytecode/ci_lazy_methods.cpp @@ -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; } diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index f6d267ef087..c5076ec235d 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -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) { diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index 1b30f02d037..31c18fab721 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -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); } diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index ce053f25185..73200f1fee7 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -796,8 +796,8 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr( typet deref_type; if(rhs.type().subtype().id()==ID_symbol) - deref_type=symbol_table.lookup( - to_symbol_type(rhs.type().subtype()).get_identifier())->get().type; + deref_type=symbol_table.lookup_ref( + to_symbol_type(rhs.type().subtype()).get_identifier()).type; else deref_type=rhs.type().subtype(); @@ -1252,11 +1252,9 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object( // Check that the type of the object is in the symbol table, // otherwise there is no safe way of finding its value. - symbol_tablet::opt_const_symbol_reft maybe_symbol= - symbol_table.lookup(object_type.get_identifier()); - if(maybe_symbol) + if(const auto maybe_symbol=symbol_table.lookup(object_type.get_identifier())) { - struct_typet struct_type=to_struct_type(maybe_symbol->get().type); + struct_typet struct_type=to_struct_type(maybe_symbol->type); // Check that the type has a value field const struct_union_typet::componentt value_comp= struct_type.get_component("value"); @@ -1502,7 +1500,7 @@ codet java_string_library_preprocesst::make_object_get_class_code( // > Class class1; pointer_typet class_type= java_reference_type( - symbol_table.lookup("java::java.lang.Class")->get().type); + symbol_table.lookup_ref("java::java.lang.Class").type); symbolt class1_sym=get_fresh_aux_symbol( class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table); symbol_exprt class1=class1_sym.symbol_expr(); @@ -1539,7 +1537,7 @@ codet java_string_library_preprocesst::make_object_get_class_code( // string1 = (String*) string_expr pointer_typet string_ptr_type=java_reference_type( - symbol_table.lookup("java::java.lang.String")->get().type); + symbol_table.lookup_ref("java::java.lang.String").type); exprt string1=allocate_fresh_string(string_ptr_type, loc, symbol_table, code); code.add( code_assign_string_expr_to_new_java_string( diff --git a/src/jsil/jsil_convert.cpp b/src/jsil/jsil_convert.cpp index 3bc44fa41e1..e2f24aa99a7 100644 --- a/src/jsil/jsil_convert.cpp +++ b/src/jsil/jsil_convert.cpp @@ -48,9 +48,7 @@ bool jsil_convertt::operator()(const jsil_parse_treet &parse_tree) if(convert_code(new_symbol, to_code(new_symbol.value))) return true; - symbol_tablet::opt_const_symbol_reft maybe_symbol= - symbol_table.lookup(new_symbol.name); - if(maybe_symbol) + if(const auto maybe_symbol=symbol_table.lookup(new_symbol.name)) { const symbolt &s=*maybe_symbol; if(s.value.id()=="no-body-just-yet") diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp index ecc36288bae..c7a8dd97acc 100644 --- a/src/jsil/jsil_typecheck.cpp +++ b/src/jsil/jsil_typecheck.cpp @@ -42,8 +42,7 @@ void jsil_typecheckt::update_expr_type(exprt &expr, const typet &type) { const irep_idt &id=to_symbol_expr(expr).get_identifier(); - symbol_tablet::opt_symbol_reft maybe_symbol= - symbol_table.get_writeable(id); + const auto maybe_symbol=symbol_table.get_writeable(id); if(!maybe_symbol) { error() << "unexpected symbol: " << id << eom; @@ -749,8 +748,7 @@ void jsil_typecheckt::typecheck_function_call( { const irep_idt &id=to_symbol_expr(f).get_identifier(); - symbol_tablet::opt_const_symbol_reft maybe_symbol=symbol_table.lookup(id); - if(maybe_symbol) + if(const auto maybe_symbol=symbol_table.lookup(id)) { const symbolt &s=*maybe_symbol; diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index d71ad02768a..0f89277ff94 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -1290,7 +1290,7 @@ void linkingt::copy_symbols() named_symbol.second.value.is_not_nil()) { object_type_updates( - main_symbol_table.get_writeable(named_symbol.first)->get().value); + main_symbol_table.get_writeable_ref(named_symbol.first).value); } } } diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index 4d96670cafd..1b085098e8d 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -31,8 +31,7 @@ bool static_lifetime_init( { namespacet ns(symbol_table); - symbol_tablet::opt_symbol_reft maybe_symbol= - symbol_table.get_writeable(INITIALIZE_FUNCTION); + const auto maybe_symbol=symbol_table.get_writeable(INITIALIZE_FUNCTION); if(!maybe_symbol) return false; symbolt &init_symbol=*maybe_symbol; diff --git a/src/util/config.cpp b/src/util/config.cpp index 0e8f3d692c8..8b4a6177991 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1177,9 +1177,7 @@ void configt::set_object_bits_from_symbol_table( return; // set object_bits according to entry point language - symbol_tablet::opt_const_symbol_reft maybe_symbol= - symbol_table.lookup(CPROVER_PREFIX "_start"); - if(maybe_symbol) + if(const auto maybe_symbol=symbol_table.lookup(CPROVER_PREFIX "_start")) { const symbolt &entry_point_symbol=*maybe_symbol; diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index 0cf07f24683..ed8b67b1bb2 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -148,30 +148,6 @@ void symbol_tablet::show(std::ostream &out) const out << it->second; } -/// Find a symbol in the symbol table for read-only access. -/// \param identifier: The name of the symbol to look for -/// \return an optional reference, set if found, unset otherwise. -symbol_tablet::opt_const_symbol_reft symbol_tablet::lookup( - const irep_idt &identifier) const -{ - symbolst::const_iterator it=symbols.find(identifier); - if(it==symbols.end()) - return opt_const_symbol_reft(); - return std::ref(it->second); -} - -/// Find a symbol in the symbol table for read-write access. -/// \param identifier: The name of the symbol to look for -/// \return an optional reference, set if found, unset otherwise. -symbol_tablet::opt_symbol_reft symbol_tablet::get_writeable( - const irep_idt &identifier) -{ - symbolst::iterator it=internal_symbols.find(identifier); - if(it==symbols.end()) - return opt_symbol_reft(); - return std::ref(it->second); -} - /// Print the contents of the symbol table /// \param out: The ostream to direct output to /// \param symbol_table: The symbol table to print out diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index 4fb920a179d..42893a0882d 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -41,9 +41,6 @@ class symbol_tablet { public: typedef std::unordered_map symbolst; - typedef optionalt> - opt_const_symbol_reft; - typedef optionalt> opt_symbol_reft; private: symbolst internal_symbols; @@ -101,9 +98,29 @@ class symbol_tablet return symbols.find(name)!=symbols.end(); } - opt_const_symbol_reft lookup(const irep_idt &identifier) const; - - opt_symbol_reft get_writeable(const irep_idt &identifier); + /// Find a symbol in the symbol table for read-only access. + /// \param id: The name of the symbol to look for + /// \return an optional reference, set if found, nullptr otherwise. + const symbolt *lookup(const irep_idt &id) const { return lookup_impl(id); } + + /// Find a symbol in the symbol table for read-write access. + /// \param id: The name of the symbol to look for + /// \return an optional reference, set if found, unset otherwise. + symbolt *get_writeable(const irep_idt &id) { return lookup_impl(id); } + + /// Find a symbol in the symbol table for read-only access. + /// \param id: The name of the symbol to look for + /// \return A reference to the symbol + /// \throw `std::out_of_range` if no such symbol exists + const symbolt &lookup_ref(const irep_idt &id) const + { return internal_symbols.at(id); } + + /// Find a symbol in the symbol table for read-write access. + /// \param id: The name of the symbol to look for + /// \return A reference to the symbol + /// \throw `std::out_of_range` if no such symbol exists + symbolt &get_writeable_ref(const irep_idt &id) + { return internal_symbols.at(id); } bool add(const symbolt &symbol); @@ -130,6 +147,21 @@ class symbol_tablet internal_symbol_base_map.swap(other.internal_symbol_base_map); internal_symbol_module_map.swap(other.internal_symbol_module_map); } + +private: + const symbolt *lookup_impl(const irep_idt &id) const + { return lookup_impl(*this, id); } + + symbolt *lookup_impl(const irep_idt &id) + { return lookup_impl(*this, id); } + + template + static auto lookup_impl(T &t, const irep_idt &id) + -> decltype(std::declval().lookup_impl(id)) + { + const auto it=t.internal_symbols.find(id); + return it==t.internal_symbols.end()?nullptr:&it->second; + } }; std::ostream &operator << ( diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp index 1b2e6941bd7..0cab10c80e5 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp @@ -32,8 +32,7 @@ SCENARIO( std::string class_prefix="java::DerivedGeneric"; REQUIRE(new_symbol_table.has_symbol(class_prefix)); - const symbolt &derived_symbol=new_symbol_table.lookup(class_prefix).value - ().get(); + const symbolt &derived_symbol=new_symbol_table.lookup_ref(class_prefix); REQUIRE(derived_symbol.is_type); const typet &derived_type=derived_symbol.type; REQUIRE(derived_type.id()==ID_struct); diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp index 21665f7b523..6060c33c906 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp @@ -32,8 +32,7 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(class_prefix)); const struct_typet &type=to_struct_type( - new_symbol_table.lookup(class_prefix) - .value().get().type); + new_symbol_table.lookup_ref(class_prefix).type); THEN("There should be a component with name t") { @@ -48,8 +47,7 @@ SCENARIO( THEN("The t component is a valid java array") { const struct_typet &subtype_type=to_struct_type( - new_symbol_table.lookup(subtype.get_identifier()) - .value().get().type); + new_symbol_table.lookup_ref(subtype.get_identifier()).type); REQUIRE(is_valid_java_array(subtype_type)); }