From ebfab8d2c1b5b064828f0f3498cecb6f19a24cac Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 2 Mar 2019 10:51:03 +0000 Subject: [PATCH] Store "is hidden" attribute of goto functions in the symbol table There should only be a single place to hold type information, including attributes, to ensure consistency. Future changes will remove the "type" member of goto_functiont, making the type information stored in the symbol table the single, authoritative source of information. With this commit the information will remain available in both places, but all read accesses only use the information in the symbol table. --- src/goto-instrument/cover_filter.cpp | 2 +- src/goto-programs/goto_convert_functions.cpp | 3 +++ src/goto-programs/goto_inline_class.cpp | 2 +- src/goto-programs/read_bin_goto_object.cpp | 8 ++++++++ src/goto-symex/symex_function_call.cpp | 5 +++-- src/goto-symex/symex_main.cpp | 3 ++- src/util/symbol.h | 13 +++++++++++++ unit/goto-instrument/cover/cover_only.cpp | 1 + 8 files changed, 32 insertions(+), 5 deletions(-) diff --git a/src/goto-instrument/cover_filter.cpp b/src/goto-instrument/cover_filter.cpp index 03f6b1e2f9e..60c6ecf8d1a 100644 --- a/src/goto-instrument/cover_filter.cpp +++ b/src/goto-instrument/cover_filter.cpp @@ -29,7 +29,7 @@ bool internal_functions_filtert::operator()( if(function.name == INITIALIZE_FUNCTION) return false; - if(goto_function.is_hidden()) + if(function.is_hidden()) return false; // ignore Java built-ins (synthetic functions) diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 3512b84a3fa..24f515685e5 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -215,7 +215,10 @@ void goto_convert_functionst::convert_function( f.body.update(); if(hide(f.body)) + { f.make_hidden(); + symbol_table.get_writeable_ref(identifier).set_hidden(); + } lifetime = parent_lifetime; } diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index 96dbd04eef4..fdb8fd9c287 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -253,7 +253,7 @@ void goto_inlinet::insert_function_body( end.type=LOCATION; // make sure the inlined function does not introduce hiding - if(goto_function.is_hidden()) + if(ns.lookup(identifier).is_hidden()) { for(auto &instruction : body.instructions) instruction.labels.remove(CPROVER_PREFIX "HIDE"); diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index 775d0f4c545..09fbebd9a53 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -160,7 +160,15 @@ static bool read_bin_goto_object( f.body.update(); if(hidden) + { f.make_hidden(); + // can be removed with the next goto-binary version update as the + // information is guaranteed to be stored in the symbol table +#if GOTO_BINARY_VERSION > 5 +#error This code should be removed +#endif + symbol_table.get_writeable_ref(fname).set_hidden(); + } } functions.compute_location_numbers(); diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index add84eae5ba..36a27757a40 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -274,8 +274,9 @@ void goto_symext::symex_function_call_code( a = state.rename(std::move(a), ns); // we hide the call if the caller and callee are both hidden + const bool callee_is_hidden = ns.lookup(identifier).is_hidden(); const bool hidden = - state.call_stack().top().hidden_function && goto_function.is_hidden(); + state.call_stack().top().hidden_function && callee_is_hidden; // record the call target.function_call( @@ -314,7 +315,7 @@ void goto_symext::symex_function_call_code( frame.end_of_function=--goto_function.body.instructions.end(); frame.return_value=call.lhs(); frame.function_identifier=identifier; - frame.hidden_function=goto_function.is_hidden(); + frame.hidden_function = callee_is_hidden; const framet &p_frame = state.call_stack().previous_frame(); for(const auto &pair : p_frame.loop_iterations) diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 82233ed2406..7f34603829f 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -326,7 +326,8 @@ std::unique_ptr goto_symext::initialize_entry_point_state( state->call_stack().top().end_of_function = limit; state->call_stack().top().calling_location.pc = state->call_stack().top().end_of_function; - state->call_stack().top().hidden_function = start_function->is_hidden(); + state->call_stack().top().hidden_function = + ns.lookup(entry_point_id).is_hidden(); state->symex_target = ⌖ diff --git a/src/util/symbol.h b/src/util/symbol.h index d34c8351c43..d83e7581418 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -117,6 +117,19 @@ class symbolt value = exprt(ID_compiled); } + /// Returns true iff the symbol is marked for internal use. + bool is_hidden() const + { + return is_auxiliary; + } + + /// Mark a symbol for internal use. This is advisory and may be utilized, + /// e.g., to filter output. + void set_hidden() + { + is_auxiliary = true; + } + /// Check that a symbol is well formed. bool is_well_formed() const; diff --git a/unit/goto-instrument/cover/cover_only.cpp b/unit/goto-instrument/cover/cover_only.cpp index 68c413f7253..c6083206108 100644 --- a/unit/goto-instrument/cover/cover_only.cpp +++ b/unit/goto-instrument/cover/cover_only.cpp @@ -22,6 +22,7 @@ symbolt create_new_symbol(const irep_idt &name, const irep_idt &file_name) source_locationt location; location.set_file(file_name); symbol.location = location; + symbol.type = code_typet{{}, empty_typet{}}; return symbol; }