Skip to content

Move "is hidden" attribute of goto functions out of type #5575

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 2 commits into from
Nov 13, 2020
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
2 changes: 1 addition & 1 deletion src/goto-instrument/cover_filter.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ bool internal_functions_filtert::operator()(
if(function.name == INITIALIZE_FUNCTION)
return false;

if(function.is_hidden())
if(goto_function.is_hidden())
return false;

// ignore Java built-ins (synthetic functions)
Expand Down
3 changes: 0 additions & 3 deletions src/goto-programs/goto_convert_functions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -226,10 +226,7 @@ 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;
}
Expand Down
18 changes: 12 additions & 6 deletions src/goto-programs/goto_function.h
Original file line number Diff line number Diff line change
Expand Up @@ -60,19 +60,17 @@ class goto_functiont
return type.get_bool(ID_C_inlined);
}

DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead"))
bool is_hidden() const
{
return type.get_bool(ID_C_hide);
return function_is_hidden;
}

DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead"))
void make_hidden()
{
type.set(ID_C_hide, true);
function_is_hidden = true;
}

goto_functiont() : body(), type({}, empty_typet())
goto_functiont() : body(), type({}, empty_typet()), function_is_hidden(false)
{
}

Expand All @@ -81,20 +79,23 @@ class goto_functiont
body.clear();
type.clear();
parameter_identifiers.clear();
function_is_hidden = false;
}

void swap(goto_functiont &other)
{
body.swap(other.body);
type.swap(other.type);
parameter_identifiers.swap(other.parameter_identifiers);
std::swap(function_is_hidden, other.function_is_hidden);
}

void copy_from(const goto_functiont &other)
{
body.copy_from(other.body);
type = other.type;
parameter_identifiers = other.parameter_identifiers;
function_is_hidden = other.function_is_hidden;
}

goto_functiont(const goto_functiont &) = delete;
Expand All @@ -103,7 +104,8 @@ class goto_functiont
goto_functiont(goto_functiont &&other)
: body(std::move(other.body)),
type(std::move(other.type)),
parameter_identifiers(std::move(other.parameter_identifiers))
parameter_identifiers(std::move(other.parameter_identifiers)),
function_is_hidden(other.function_is_hidden)
{
}

Expand All @@ -112,6 +114,7 @@ class goto_functiont
body = std::move(other.body);
type = std::move(other.type);
parameter_identifiers = std::move(other.parameter_identifiers);
function_is_hidden = other.function_is_hidden;
return *this;
}

Expand All @@ -120,6 +123,9 @@ class goto_functiont
/// The validation mode indicates whether well-formedness check failures are
/// reported via DATA_INVARIANT violations or exceptions.
void validate(const namespacet &ns, const validation_modet vm) const;

protected:
bool function_is_hidden;
};

void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);
Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/goto_inline_class.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -256,7 +256,7 @@ void goto_inlinet::insert_function_body(
end.type=LOCATION;

// make sure the inlined function does not introduce hiding
if(ns.lookup(identifier).is_hidden())
if(goto_function.is_hidden())
{
for(auto &instruction : body.instructions)
instruction.labels.remove(CPROVER_PREFIX "HIDE");
Expand Down
12 changes: 2 additions & 10 deletions src/goto-programs/read_bin_goto_object.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -131,8 +131,8 @@ static bool read_bin_goto_object(
instruction.labels.push_back(label);
if(label == CPROVER_PREFIX "HIDE")
hidden=true;
// The above info is normally in the type of the goto_functiont object,
// which should likely be stored in the binary.
// The above info is also held in the goto_functiont object, and could
// be stored in the binary.
}
}

Expand Down Expand Up @@ -160,15 +160,7 @@ 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();
Expand Down
5 changes: 2 additions & 3 deletions src/goto-symex/symex_function_call.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -270,9 +270,8 @@ void goto_symext::symex_function_call_code(
[&](const exprt &a) { return state.rename(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 && callee_is_hidden;
state.call_stack().top().hidden_function && goto_function.is_hidden();

// record the call
target.function_call(
Expand Down Expand Up @@ -338,7 +337,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 = callee_is_hidden;
frame.hidden_function = goto_function.is_hidden();

const framet &p_frame = state.call_stack().previous_frame();
for(const auto &pair : p_frame.loop_iterations)
Expand Down
3 changes: 1 addition & 2 deletions src/goto-symex/symex_main.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -434,8 +434,7 @@ std::unique_ptr<goto_symext::statet> 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 =
ns.lookup(entry_point_id).is_hidden();
state->call_stack().top().hidden_function = start_function->is_hidden();

state->symex_target = &target;

Expand Down
1 change: 0 additions & 1 deletion src/util/irep_ids.def
Original file line number Diff line number Diff line change
Expand Up @@ -285,7 +285,6 @@ IREP_ID_ONE(signed_int128)
IREP_ID_ONE(unsigned_int128)
IREP_ID_ONE(case)
IREP_ID_TWO(C_inlined, #inlined)
IREP_ID_TWO(C_hide, #hide)
IREP_ID_ONE(hide)
IREP_ID_ONE(abs)
IREP_ID_ONE(sign)
Expand Down
13 changes: 0 additions & 13 deletions src/util/symbol.h
Original file line number Diff line number Diff line change
Expand Up @@ -117,19 +117,6 @@ 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;

Expand Down
1 change: 0 additions & 1 deletion unit/goto-instrument/cover/cover_only.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@ 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;
}
Expand Down