Use goto_functiont::parameter_identifiers and remove goto_functiont::type

Having two function type definitions (one in the symbol table and one in
goto_functiont) is just prone to become inconsistent. Instead, always look at
the symbol table when we do need type information. If all we care about are the
identifiers we can still use goto_functiont::parameter_identifiers.

Author: tautschnig

src/analyses/goto_check.cpp

@@ -1653,7 +1653,7 @@ void goto_checkt::goto_check(
 
   if(enable_pointer_check)
     local_bitvector_analysis =
-      util_make_unique<local_bitvector_analysist>(goto_function);
+      util_make_unique<local_bitvector_analysist>(goto_function, ns);
 
   goto_programt &goto_program=goto_function.body;
 

src/analyses/local_bitvector_analysis.cpp

@@ -60,13 +60,9 @@ bool local_bitvector_analysist::merge(points_tot &a, points_tot &b)
 /// \return return 'true' iff we track the object with given identifier
 bool local_bitvector_analysist::is_tracked(const irep_idt &identifier)
 {
-  localst::locals_mapt::const_iterator it=locals.locals_map.find(identifier);
-  if(it==locals.locals_map.end() ||
-     it->second.type().id()!=ID_pointer ||
-     dirty(identifier))
-    return false;
-
-  return true;
+  localst::locals_sett::const_iterator it = locals.locals.find(identifier);
+  return it != locals.locals.end() && ns.lookup(*it).type.id() == ID_pointer &&
+         !dirty(identifier);
 }
 
 void local_bitvector_analysist::assign_lhs(
@@ -254,9 +250,9 @@ void local_bitvector_analysist::build()
   // Gather the objects we track, and
   // feed in sufficiently bad defaults for their value
   // in the entry location.
-  for(const auto &local : locals.locals_map)
-    if(is_tracked(local.first))
-      loc_infos[0][pointers.number(local.first)]=flagst::mk_unknown();
+  for(const auto &local : locals.locals)
+    if(is_tracked(local))
+      loc_infos[0][pointers.number(local)] = flagst::mk_unknown();
 
   while(!work_queue.empty())
   {

src/analyses/local_bitvector_analysis.h

@@ -25,11 +25,13 @@ class local_bitvector_analysist
 public:
   typedef goto_functionst::goto_functiont goto_functiont;
 
-  explicit local_bitvector_analysist(
-    const goto_functiont &_goto_function):
-    dirty(_goto_function),
-    locals(_goto_function),
-    cfg(_goto_function.body)
+  local_bitvector_analysist(
+    const goto_functiont &_goto_function,
+    const namespacet &ns)
+    : dirty(_goto_function),
+      locals(_goto_function),
+      cfg(_goto_function.body),
+      ns(ns)
   {
     build();
   }
@@ -176,6 +178,7 @@ class local_bitvector_analysist
     const exprt &src);
 
 protected:
+  const namespacet &ns;
   void build();
 
   typedef std::stack<unsigned> work_queuet;

src/analyses/locals.cpp

@@ -18,20 +18,18 @@ Date: March 2013
 void localst::build(const goto_functiont &goto_function)
 {
   forall_goto_program_instructions(it, goto_function.body)
+  {
     if(it->is_decl())
-    {
-      const code_declt &code_decl=to_code_decl(it->code);
-      locals_map.emplace(code_decl.get_identifier(), code_decl.symbol());
-    }
-
-  for(const auto &param : goto_function.type.parameters())
-    locals_map.emplace(
-      param.get_identifier(),
-      symbol_exprt(param.get_identifier(), param.type()));
+      locals.insert(it->get_decl().get_identifier());
+  }
+
+  locals.insert(
+    goto_function.parameter_identifiers.begin(),
+    goto_function.parameter_identifiers.end());
 }
 
 void localst::output(std::ostream &out) const
 {
-  for(const auto &local : locals_map)
-    out << local.first << "\n";
+  for(const auto &local : locals)
+    out << local << "\n";
 }

src/analyses/locals.h

@@ -31,11 +31,11 @@ class localst
   // but including the function parameters.
   bool is_local(const irep_idt &identifier) const
   {
-    return locals_map.find(identifier)!=locals_map.end();
+    return locals.find(identifier) != locals.end();
   }
 
-  typedef std::map<irep_idt, symbol_exprt> locals_mapt;
-  locals_mapt locals_map;
+  typedef std::unordered_set<irep_idt> locals_sett;
+  locals_sett locals;
 
 protected:
   void build(const goto_functiont &goto_function);

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/assembler/remove_asm.cpp

@@ -122,14 +122,14 @@ void remove_asmt::gcc_asm_function_call(
     symbol.mode = ID_C;
 
     symbol_table.add(symbol);
-  }
 
-  if(
-    goto_functions.function_map.find(function_identifier) ==
-    goto_functions.function_map.end())
+    goto_functions.function_map.emplace(function_identifier, goto_functiont());
+  }
+  else
   {
-    auto &f = goto_functions.function_map[function_identifier];
-    f.type = fkt_type;
+    DATA_INVARIANT(
+      symbol_table.lookup_ref(function_identifier).type == fkt_type,
+      "function types should match");
   }
 }
 
@@ -171,14 +171,14 @@ void remove_asmt::msc_asm_function_call(
     symbol.mode = ID_C;
 
     symbol_table.add(symbol);
-  }
 
-  if(
-    goto_functions.function_map.find(function_identifier) ==
-    goto_functions.function_map.end())
+    goto_functions.function_map.emplace(function_identifier, goto_functiont());
+  }
+  else
   {
-    auto &f = goto_functions.function_map[function_identifier];
-    f.type = fkt_type;
+    DATA_INVARIANT(
+      symbol_table.lookup_ref(function_identifier).type == fkt_type,
+      "function types should match");
   }
 }
 

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-harness/function_call_harness_generator.cpp

@@ -112,8 +112,6 @@ void function_call_harness_generatort::generate(
 
   symbol_table.insert(harness_function_symbol);
 
-  goto_model.goto_functions.function_map[harness_function_name].type =
-    to_code_type(harness_function_symbol.type);
   auto &body =
     goto_model.goto_functions.function_map[harness_function_name].body;
   goto_convert(

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/code_contracts.cpp

@@ -269,16 +269,13 @@ void code_contractst::add_contract_check(
 {
   assert(!dest.instructions.empty());
 
-  goto_functionst::function_mapt::iterator f_it=
-    goto_functions.function_map.find(function);
-  assert(f_it!=goto_functions.function_map.end());
-
-  const goto_functionst::goto_functiont &gf=f_it->second;
+  const symbolt &function_symbol = ns.lookup(function);
+  const code_typet &code_type = to_code_type(function_symbol.type);
 
-  const exprt &requires=
-    static_cast<const exprt&>(gf.type.find(ID_C_spec_requires));
-  const exprt &ensures=
-    static_cast<const exprt&>(gf.type.find(ID_C_spec_ensures));
+  const exprt &requires =
+    static_cast<const exprt &>(code_type.find(ID_C_spec_requires));
+  const exprt &ensures =
+    static_cast<const exprt &>(code_type.find(ID_C_spec_ensures));
   assert(ensures.is_not_nil());
 
   // build:
@@ -305,18 +302,17 @@ void code_contractst::add_contract_check(
   g->source_location=skip->source_location;
 
   // prepare function call including all declarations
-  const symbolt &function_symbol = ns.lookup(function);
   code_function_callt call(function_symbol.symbol_expr());
   replace_symbolt replace;
 
   // decl ret
-  if(gf.type.return_type()!=empty_typet())
+  if(code_type.return_type() != empty_typet())
   {
     goto_programt::targett d=check.add_instruction(DECL);
     d->source_location=skip->source_location;
 
     symbol_exprt r = new_tmp_symbol(
-                       gf.type.return_type(),
+                       code_type.return_type(),
                        d->source_location,
                        function,
                        function_symbol.mode)
@@ -330,25 +326,22 @@ void code_contractst::add_contract_check(
   }
 
   // decl parameter1 ...
-  for(code_typet::parameterst::const_iterator
-      p_it=gf.type.parameters().begin();
-      p_it!=gf.type.parameters().end();
-      ++p_it)
+  for(const auto &parameter : code_type.parameters())
   {
     goto_programt::targett d=check.add_instruction(DECL);
     d->source_location=skip->source_location;
 
     symbol_exprt p =
       new_tmp_symbol(
-        p_it->type(), d->source_location, function, function_symbol.mode)
+        parameter.type(), d->source_location, function, function_symbol.mode)
         .symbol_expr();
     d->code=code_declt(p);
 
     call.arguments().push_back(p);
 
-    if(!p_it->get_identifier().empty())
+    if(!parameter.get_identifier().empty())
     {
-      symbol_exprt cur_p(p_it->get_identifier(), p_it->type());
+      symbol_exprt cur_p(parameter.get_identifier(), parameter.type());
       replace.insert(cur_p, p);
     }
   }

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)
@@ -283,7 +285,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,
@@ -309,16 +311,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();
@@ -353,11 +358,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();