Store inlined/hidden attributes of code-typed symbols in the symbol table

There should only be a single place to hold type information, including
attributes, to ensure consistency.

Author: tautschnig

src/ansi-c/ansi_c_declaration.cpp

@@ -150,7 +150,7 @@ void ansi_c_declarationt::to_symbol(
     symbol.is_file_local=get_is_static();
 
     if(get_is_inline())
-      symbol.type.set(ID_C_inlined, true);
+      to_code_type(symbol.type).set_inlined(true);
 
     if(
       config.ansi_c.mode == configt::ansi_ct::flavourt::GCC ||

src/ansi-c/c_typecheck_base.cpp

@@ -309,10 +309,6 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
 
   if(final_new.id()==ID_code)
   {
-    bool inlined=
-       (new_symbol.type.get_bool(ID_C_inlined) ||
-        old_symbol.type.get_bool(ID_C_inlined));
-
     if(final_old.id()!=ID_code)
     {
       error().source_location=new_symbol.location;
@@ -327,15 +323,17 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
     code_typet &old_ct=to_code_type(old_symbol.type);
     code_typet &new_ct=to_code_type(new_symbol.type);
 
+    const bool inlined = old_ct.get_inlined() || new_ct.get_inlined();
+
     if(old_ct.has_ellipsis() && !new_ct.has_ellipsis())
       old_ct=new_ct;
     else if(!old_ct.has_ellipsis() && new_ct.has_ellipsis())
       new_ct=old_ct;
 
     if(inlined)
     {
-      old_symbol.type.set(ID_C_inlined, true);
-      new_symbol.type.set(ID_C_inlined, true);
+      old_ct.set_inlined(true);
+      new_ct.set_inlined(true);
     }
 
     // do body
@@ -348,7 +346,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
         // definition is marked as "extern inline"
 
         if(
-          old_symbol.type.get_bool(ID_C_inlined) &&
+          old_ct.get_inlined() &&
           (config.ansi_c.mode == configt::ansi_ct::flavourt::GCC ||
            config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG ||
            config.ansi_c.mode == configt::ansi_ct::flavourt::ARM ||

src/cpp/cpp_declarator_converter.cpp

@@ -433,7 +433,7 @@ symbolt &cpp_declarator_convertert::convert_new_symbol(
     symbol.is_macro=true;
 
   if(member_spec.is_inline())
-    symbol.type.set(ID_C_inlined, true);
+    to_code_type(symbol.type).set_inlined(true);
 
   if(!symbol.is_type)
   {

src/cpp/cpp_typecheck_compound_type.cpp

@@ -1308,7 +1308,7 @@ void cpp_typecheckt::typecheck_member_function(
   component.set(ID_prefix, id2string(identifier) + "::");
 
   if(value.is_not_nil())
-    type.set(ID_C_inlined, true);
+    to_code_type(type).set_inlined(true);
 
   symbol.name=identifier;
   symbol.base_name=component.get_base_name();

src/goto-analyzer/unreachable_instructions.cpp

@@ -173,8 +173,9 @@ void unreachable_instructions(
 
     // f_it->first may be a link-time renamed version, use the
     // base_name instead; do not list inlined functions
-    if(called.find(decl.base_name)!=called.end() ||
-       f_it->second.is_inlined())
+    if(
+      called.find(decl.base_name) != called.end() ||
+      to_code_type(decl.type).get_inlined())
       unreachable_instructions(goto_program, dead_map);
     else
       all_unreachable(goto_program, dead_map);
@@ -295,9 +296,9 @@ static void list_functions(
 
     // f_it->first may be a link-time renamed version, use the
     // base_name instead; do not list inlined functions
-    if(unreachable ==
-       (called.find(decl.base_name)!=called.end() ||
-        f_it->second.is_inlined()))
+    if(
+      unreachable == (called.find(decl.base_name) != called.end() ||
+                      to_code_type(decl.type).get_inlined()))
       continue;
 
     source_locationt first_location=decl.location;

src/goto-instrument/aggressive_slicer.cpp

@@ -39,9 +39,11 @@ void aggressive_slicert::note_functions_to_keep(
 
 void aggressive_slicert::get_all_functions_containing_properties()
 {
+  const namespacet ns(goto_model.symbol_table);
+
   for(const auto &fct : goto_model.goto_functions.function_map)
   {
-    if(!fct.second.is_inlined())
+    if(!to_code_type(ns.lookup(fct.first).type).get_inlined())
     {
       for(const auto &ins : fct.second.body.instructions)
         if(ins.is_assert())

src/goto-instrument/cover.cpp

@@ -255,11 +255,13 @@ std::unique_ptr<cover_configt> get_cover_config(
 /// \param cover_config: configuration, produced using get_cover_config
 /// \param function_id: function name
 /// \param function: function to instrument
+/// \param ns: namespace
 /// \param message_handler: log output
 static void instrument_cover_goals(
   const cover_configt &cover_config,
   const irep_idt &function_id,
   goto_functionst::goto_functiont &function,
+  const namespacet &ns,
   message_handlert &message_handler)
 {
   if(!cover_config.keep_assertions)
@@ -284,7 +286,7 @@ static void instrument_cover_goals(
 
   bool changed = false;
 
-  if(cover_config.function_filters(function_id, function))
+  if(cover_config.function_filters(function_id, function, ns))
   {
     instrument_cover_goals(
       function_id,
@@ -310,16 +312,19 @@ static void instrument_cover_goals(
 /// Instruments a single goto program based on the given configuration
 /// \param cover_config: configuration, produced using get_cover_config
 /// \param function: goto program to instrument
+/// \param ns: namespace
 /// \param message_handler: log output
 void instrument_cover_goals(
   const cover_configt &cover_config,
   goto_model_functiont &function,
+  const namespacet &ns,
   message_handlert &message_handler)
 {
   instrument_cover_goals(
     cover_config,
     function.get_function_id(),
     function.get_goto_function(),
+    ns,
     message_handler);
 
   function.compute_location_numbers();
@@ -354,11 +359,12 @@ bool instrument_cover_goals(
     return true;
   }
 
+  const namespacet ns(symbol_table);
   Forall_goto_functions(f_it, goto_functions)
   {
     cover_config->mode = symbol_table.lookup(f_it->first)->mode;
     instrument_cover_goals(
-      *cover_config, f_it->first, f_it->second, message_handler);
+      *cover_config, f_it->first, f_it->second, ns, message_handler);
   }
   goto_functions.compute_location_numbers();
 

src/goto-instrument/cover.h

@@ -62,6 +62,7 @@ std::unique_ptr<cover_configt> get_cover_config(
 void instrument_cover_goals(
   const cover_configt &,
   goto_model_functiont &,
+  const namespacet &ns,
   message_handlert &);
 
 void parse_cover_options(const cmdlinet &, optionst &);

src/goto-instrument/cover_filter.cpp

@@ -16,18 +16,20 @@ Author: Peter Schrammel
 /// Filter out functions that are not considered provided by the user
 /// \param function_id: a function name
 /// \param goto_function: a goto function
+/// \param ns: a namespace
 /// \return returns true if function is considered user-provided
 bool internal_functions_filtert::operator()(
   const irep_idt &function_id,
-  const goto_functionst::goto_functiont &goto_function) const
+  const goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns) const
 {
   if(function_id == goto_functionst::entry_point())
     return false;
 
   if(function_id == INITIALIZE_FUNCTION)
     return false;
 
-  if(goto_function.is_hidden())
+  if(to_code_type(ns.lookup(function_id).type).is_hidden())
     return false;
 
   // ignore Java built-ins (synthetic functions)
@@ -46,12 +48,15 @@ bool internal_functions_filtert::operator()(
 /// Filter functions whose name match the regex
 /// \param function_id: a function name
 /// \param goto_function: a goto function
+/// \param ns: a namespace
 /// \return returns true if the function name matches
 bool include_pattern_filtert::operator()(
   const irep_idt &function_id,
-  const goto_functionst::goto_functiont &goto_function) const
+  const goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns) const
 {
   (void)goto_function; // unused parameter
+  (void)ns;            // unused parameter
   std::smatch string_matcher;
   return std::regex_match(
     id2string(function_id), string_matcher, regex_matcher);
@@ -64,12 +69,15 @@ bool include_pattern_filtert::operator()(
 /// These criteria are arbitrarily chosen.
 /// \param function_id: name of \p goto_function
 /// \param goto_function: a goto function
+/// \param ns: a namespace
 /// \return returns true if non-trivial
 bool trivial_functions_filtert::operator()(
   const irep_idt &function_id,
-  const goto_functionst::goto_functiont &goto_function) const
+  const goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns) const
 {
   (void)function_id; // unused parameter
+  (void)ns;          // unused parameter
   unsigned long count_assignments = 0, count_goto = 0;
   forall_goto_program_instructions(i_it, goto_function.body)
   {

src/goto-instrument/cover_filter.h

@@ -36,7 +36,8 @@ class function_filter_baset : public messaget
   /// Returns true if the function passes the filter criteria
   virtual bool operator()(
     const irep_idt &identifier,
-    const goto_functionst::goto_functiont &goto_function) const = 0;
+    const goto_functionst::goto_functiont &goto_function,
+    const namespacet &) const = 0;
 
   /// Can be called after final filter application to report
   /// on unexpected situations encountered
@@ -84,12 +85,14 @@ class function_filterst
   /// Applies the filters to the given function
   /// \param identifier: function name
   /// \param goto_function: goto function
+  /// \param ns: a namespace
   bool operator()(
     const irep_idt &identifier,
-    const goto_functionst::goto_functiont &goto_function) const
+    const goto_functionst::goto_functiont &goto_function,
+    const namespacet &ns) const
   {
     for(const auto &filter : filters)
-      if(!(*filter)(identifier, goto_function))
+      if(!(*filter)(identifier, goto_function, ns))
         return false;
 
     return true;
@@ -152,7 +155,8 @@ class internal_functions_filtert : public function_filter_baset
 
   bool operator()(
     const irep_idt &identifier,
-    const goto_functionst::goto_functiont &goto_function) const override;
+    const goto_functionst::goto_functiont &goto_function,
+    const namespacet &ns) const override;
 };
 
 /// Filters functions that match the provided pattern
@@ -169,7 +173,8 @@ class include_pattern_filtert : public function_filter_baset
 
   bool operator()(
     const irep_idt &identifier,
-    const goto_functionst::goto_functiont &goto_function) const override;
+    const goto_functionst::goto_functiont &goto_function,
+    const namespacet &) const override;
 
 private:
   std::regex regex_matcher;
@@ -186,7 +191,8 @@ class trivial_functions_filtert : public function_filter_baset
 
   bool operator()(
     const irep_idt &identifier,
-    const goto_functionst::goto_functiont &goto_function) const override;
+    const goto_functionst::goto_functiont &goto_function,
+    const namespacet &) const override;
 };
 
 /// Filters out goals with source locations considered internal

src/goto-instrument/remove_function.cpp

@@ -39,7 +39,8 @@ void remove_function(
                     << " in goto program" << messaget::eom;
     return;
   }
-  else if(entry->second.is_inlined())
+  else if(to_code_type(goto_model.symbol_table.lookup_ref(identifier).type)
+            .get_inlined())
   {
     message.warning() << "Function " << identifier << " is inlined, "
                       << "instantiations will not be removed"

src/goto-programs/goto_convert_functions.cpp

@@ -219,7 +219,7 @@ void goto_convert_functionst::convert_function(
   f.body.update();
 
   if(hide(f.body))
-    f.make_hidden();
+    to_code_type(symbol_table.get_writeable_ref(identifier).type).make_hidden();
 
   lifetime = parent_lifetime;
 }

src/goto-programs/goto_inline.cpp

@@ -195,7 +195,7 @@ void goto_partial_inline(
         continue;
 
       if(
-        called_function.is_inlined() ||
+        to_code_type(ns.lookup(id).type).get_inlined() ||
         called_function.body.instructions.size() <= smallfunc_limit)
       {
         PRECONDITION(i_it->is_function_call());

src/goto-programs/goto_inline_class.cpp

@@ -267,8 +267,9 @@ void goto_inlinet::insert_function_body(
     "final instruction of a function must be an END_FUNCTION");
   end.type=LOCATION;
 
+  const symbolt &function_symbol = ns.lookup(identifier);
   // make sure the inlined function does not introduce hiding
-  if(goto_function.is_hidden())
+  if(to_code_type(function_symbol.type).is_hidden())
   {
     for(auto &instruction : body.instructions)
       instruction.labels.remove(CPROVER_PREFIX "HIDE");

src/goto-programs/link_goto_model.cpp

@@ -104,7 +104,7 @@ static bool link_functions(
       {
         // just keep the old one in dest
       }
-      else if(in_dest_symbol_table.type.get_bool(ID_C_inlined))
+      else if(to_code_type(ns.lookup(final_id).type).get_inlined())
       {
         // ok, we silently ignore
       }

src/goto-programs/property_checker.cpp

@@ -30,12 +30,14 @@ property_checkert::property_checkert(
 {
 }
 
-void property_checkert::initialize_property_map(
-  const goto_functionst &goto_functions)
+void property_checkert::initialize_property_map(const goto_modelt &goto_model)
 {
-  forall_goto_functions(it, goto_functions)
-    if(!it->second.is_inlined() ||
-       it->first==goto_functions.entry_point())
+  const namespacet ns(goto_model.symbol_table);
+
+  forall_goto_functions(it, goto_model.goto_functions)
+    if(
+      !to_code_type(ns.lookup(it->first).type).get_inlined() ||
+      it->first == goto_functionst::entry_point())
     {
       const goto_programt &goto_program=it->second.body;
 

src/goto-programs/property_checker.h

@@ -49,7 +49,7 @@ class property_checkert:public messaget
   property_mapt property_map;
 
 protected:
-  void initialize_property_map(const goto_functionst &);
+  void initialize_property_map(const goto_modelt &);
 };
 
 #endif // CPROVER_GOTO_PROGRAMS_PROPERTY_CHECKER_H

src/goto-programs/read_bin_goto_object.cpp

@@ -164,7 +164,7 @@ static bool read_bin_goto_object(
     f.body.update();
 
     if(hidden)
-      f.make_hidden();
+      to_code_type(symbol_table.get_writeable_ref(fname).type).make_hidden();
   }
 
   functions.compute_location_numbers();

src/goto-programs/set_properties.cpp

@@ -97,19 +97,14 @@ void set_properties(
   goto_modelt &goto_model,
   const std::list<std::string> &properties)
 {
-  set_properties(goto_model.goto_functions, properties);
-}
+  const namespacet ns(goto_model.symbol_table);
 
-void set_properties(
-  goto_functionst &goto_functions,
-  const std::list<std::string> &properties)
-{
   std::unordered_set<irep_idt> property_set;
 
   property_set.insert(properties.begin(), properties.end());
 
-  Forall_goto_functions(it, goto_functions)
-    if(!it->second.is_inlined())
+  Forall_goto_functions(it, goto_model.goto_functions)
+    if(!to_code_type(ns.lookup(it->first).type).get_inlined())
       set_properties(it->second.body, property_set);
 
   if(!property_set.empty())