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.

Author: tautschnig

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)

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;
 }

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");

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();

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)

src/goto-symex/symex_main.cpp

@@ -326,7 +326,8 @@ 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 = start_function->is_hidden();
+  state->call_stack().top().hidden_function =
+    ns.lookup(entry_point_id).is_hidden();
 
   state->symex_target = &target;
 

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;
 

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;
 }