Merge pull request #5575 from tautschnig/goto_functiont-is_hidden

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

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(function.is_hidden())
+  if(goto_function.is_hidden())
     return false;
 
   // ignore Java built-ins (synthetic functions)

src/goto-programs/goto_convert_functions.cpp

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

src/goto-programs/goto_function.h

@@ -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)
   {
   }
 
@@ -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;
@@ -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)
   {
   }
 
@@ -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;
   }
 
@@ -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);

src/goto-programs/goto_inline_class.cpp

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

src/goto-programs/read_bin_goto_object.cpp

@@ -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.
       }
     }
 
@@ -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();

src/goto-symex/symex_function_call.cpp

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

src/goto-symex/symex_main.cpp

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

src/util/irep_ids.def

@@ -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)

src/util/symbol.h

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

unit/goto-instrument/cover/cover_only.cpp

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