Merge pull request #4312 from tautschnig/store_is_hidden

Store "is hidden" attribute of goto functions in the symbol table [blocks: #4167]

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

@@ -335,7 +335,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;
 }