Revert "WIP"

This reverts commit d39e00ea28937cd4cf7279edf4aad741dad50fae.

Author: tautschnig

src/assembler/remove_asm.cpp

@@ -123,11 +123,13 @@ void remove_asmt::gcc_asm_function_call(
 
     symbol_table.add(symbol);
   }
-  else
+
+  if(
+    goto_functions.function_map.find(function_identifier) ==
+    goto_functions.function_map.end())
   {
-    DATA_INVARIANT(
-      symbol_table.lookup_ref(function_identifier).type == fkt_type,
-      "function types should match");
+    auto &f = goto_functions.function_map[function_identifier];
+    f.type = fkt_type;
   }
 }
 
@@ -170,11 +172,13 @@ void remove_asmt::msc_asm_function_call(
 
     symbol_table.add(symbol);
   }
-  else
+
+  if(
+    goto_functions.function_map.find(function_identifier) ==
+    goto_functions.function_map.end())
   {
-    DATA_INVARIANT(
-      symbol_table.lookup_ref(function_identifier).type == fkt_type,
-      "function types should match");
+    auto &f = goto_functions.function_map[function_identifier];
+    f.type = fkt_type;
   }
 }
 

src/goto-programs/goto_convert_functions.cpp

@@ -86,7 +86,6 @@ bool goto_convert_functionst::hide(const goto_programt &goto_program)
 
 void goto_convert_functionst::add_return(
   goto_functionst::goto_functiont &f,
-  const typet &return_type,
   const source_locationt &source_location)
 {
   #if 0
@@ -130,7 +129,7 @@ void goto_convert_functionst::add_return(
 
   #endif
 
-  const side_effect_expr_nondett rhs(return_type, source_location);
+  const side_effect_expr_nondett rhs(f.type.return_type(), source_location);
 
   goto_programt::targett t=f.body.add_instruction();
   t->make_return();
@@ -151,10 +150,7 @@ void goto_convert_functionst::convert_function(
   // make tmp variables local to function
   tmp_symbol_prefix=id2string(symbol.name)+"::$tmp";
 
-  const code_typet &code_type = to_code_type(symbol.type);
-  f.parameter_identifiers.reserve(code_type.parameters().size());
-  for(const auto &parameter : code_type.parameters())
-    f.parameter_identifiers.push_back(parameter.get_identifier());
+  f.type=to_code_type(symbol.type);
 
   if(symbol.value.is_nil() ||
      symbol.is_compiled()) /* goto_inline may have removed the body */
@@ -181,15 +177,15 @@ void goto_convert_functionst::convert_function(
   targets=targetst();
   targets.set_return(end_function);
   targets.has_return_value=
-    code_type.return_type().id()!=ID_empty &&
-    code_type.return_type().id()!=ID_constructor &&
-    code_type.return_type().id()!=ID_destructor;
+    f.type.return_type().id()!=ID_empty &&
+    f.type.return_type().id()!=ID_constructor &&
+    f.type.return_type().id()!=ID_destructor;
 
   goto_convert_rec(code, f.body, mode);
 
   // add non-det return value, if needed
   if(targets.has_return_value)
-    add_return(f, code_type.return_type(), end_location);
+    add_return(f, end_location);
 
   // handle SV-COMP's __VERIFIER_atomic_
   if(!f.body.instructions.empty() &&
@@ -217,7 +213,7 @@ void goto_convert_functionst::convert_function(
   f.body.update();
 
   if(hide(f.body))
-    to_code_type(symbol_table.get_writeable_ref(identifier).type).make_hidden();
+    f.make_hidden();
 
   lifetime = parent_lifetime;
 }

src/goto-programs/goto_convert_functions.h

@@ -58,7 +58,6 @@ class goto_convert_functionst:public goto_convertt
   //
   void add_return(
     goto_functionst::goto_functiont &,
-    const typet &return_type,
     const source_locationt &);
 };
 

src/goto-programs/goto_function.h

@@ -28,32 +28,61 @@ class goto_functiont
 public:
   goto_programt body;
 
+  /// The type of the function, indicating the return type and parameter types
+  code_typet type;
+
   typedef std::vector<irep_idt> parameter_identifierst;
+
   /// The identifiers of the parameters of this function
+  ///
+  /// Note: This variable is currently unused and the vector is thus always
+  /// empty. In the future the code base may be refactored to fill in the
+  /// parameter identifiers here when creating a `goto_functiont`. For now the
+  /// parameter identifiers should be retrieved from the type (`code_typet`).
   parameter_identifierst parameter_identifiers;
 
   bool body_available() const
   {
     return !body.instructions.empty();
   }
 
-  goto_functiont() = default;
+  bool is_inlined() const
+  {
+    return type.get_bool(ID_C_inlined);
+  }
+
+  bool is_hidden() const
+  {
+    return type.get_bool(ID_C_hide);
+  }
+
+  void make_hidden()
+  {
+    type.set(ID_C_hide, true);
+  }
+
+  goto_functiont() : body(), type({}, empty_typet())
+  {
+  }
 
   void clear()
   {
     body.clear();
+    type.clear();
     parameter_identifiers.clear();
   }
 
   void swap(goto_functiont &other)
   {
     body.swap(other.body);
+    type.swap(other.type);
     parameter_identifiers.swap(other.parameter_identifiers);
   }
 
   void copy_from(const goto_functiont &other)
   {
     body.copy_from(other.body);
+    type = other.type;
     parameter_identifiers = other.parameter_identifiers;
   }
 
@@ -62,13 +91,15 @@ 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))
   {
   }
 
   goto_functiont &operator=(goto_functiont &&other)
   {
     body = std::move(other.body);
+    type = std::move(other.type);
     parameter_identifiers = std::move(other.parameter_identifiers);
     return *this;
   }

src/goto-programs/goto_functions.h

@@ -117,28 +117,13 @@ class goto_functionst
     {
       const goto_functiont &goto_function = entry.second;
       const auto &function_name = entry.first;
-      const symbolt &function_symbol = ns.lookup(function_name);
-      const code_typet::parameterst &parameters =
-        to_code_type(function_symbol.type).parameters();
 
       DATA_CHECK(
         vm,
-        goto_function.parameter_identifiers.size() == parameters.size(),
-        id2string(function_name) + " parameter count inconsistency\n" +
-          "goto program: " + std::to_string(goto_function.parameter_identifiers.size()) +
-          "\nsymbol table: " + std::to_string(parameters.size()));
-
-      auto it = goto_function.parameter_identifiers.begin();
-      for(const auto &parameter : parameters)
-      {
-        DATA_CHECK(
-          vm,
-          ns.lookup(*it).type == parameter.type(),
-          id2string(function_name) + " parameter type inconsistency\n" +
-            "goto program: " + ns.lookup(*it).type.id_string() +
-            "\nsymbol table: " + parameter.type().id_string());
-        ++it;
-      }
+        goto_function.type == ns.lookup(function_name).type,
+        id2string(function_name) + " type inconsistency\ngoto program type: " +
+          goto_function.type.id_string() +
+          "\nsymbol table type: " + ns.lookup(function_name).type.id_string());
 
       goto_function.validate(ns, vm);
     }

src/goto-programs/goto_inline.cpp

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

src/goto-programs/goto_inline_class.cpp

@@ -31,7 +31,7 @@ Author: Daniel Kroening, [email protected]
 void goto_inlinet::parameter_assignments(
   const goto_programt::targett target,
   const irep_idt &function_name, // name of called function
-  const goto_functiont::parameter_identifierst &parameter_identifiers,
+  const code_typet &code_type, // type of called function
   const exprt::operandst &arguments, // arguments of call
   goto_programt &dest)
 {
@@ -43,21 +43,28 @@ void goto_inlinet::parameter_assignments(
   // iterates over the operands
   exprt::operandst::const_iterator it1=arguments.begin();
 
-  // iterates over the parameters
-  for(const auto &identifier : parameter_identifiers)
+  const code_typet::parameterst &parameter_types=
+    code_type.parameters();
+
+  // iterates over the types of the parameters
+  for(const auto &parameter : parameter_types)
   {
+    // this is the type the n-th argument should be
+    const typet &par_type = parameter.type();
+
+    const irep_idt &identifier=parameter.get_identifier();
+
     DATA_INVARIANT(
       !identifier.empty(),
       source_location.as_string() + ": no identifier for function parameter");
 
-    const symbolt &symbol=ns.lookup(identifier);
-
-    // this is the type the n-th argument should be
-    const typet &par_type = symbol.type;
+    {
+      const symbolt &symbol=ns.lookup(identifier);
 
-    goto_programt::targett decl = dest.add(
-      goto_programt::make_decl(symbol.symbol_expr(), source_location));
-    decl->code.add_source_location()=source_location;
+      goto_programt::targett decl = dest.add(
+        goto_programt::make_decl(symbol.symbol_expr(), source_location));
+      decl->code.add_source_location()=source_location;
+    }
 
     // this is the actual parameter
     exprt actual;
@@ -133,16 +140,22 @@ void goto_inlinet::parameter_assignments(
 
 void goto_inlinet::parameter_destruction(
   const goto_programt::targett target,
-  const goto_functiont::parameter_identifierst &parameter_identifiers,
+  const code_typet &code_type, // type of called function
   goto_programt &dest)
 {
   PRECONDITION(target->is_function_call());
   PRECONDITION(dest.empty());
 
   const source_locationt &source_location=target->source_location;
 
-  for(const auto &identifier : parameter_identifiers)
+  const code_typet::parameterst &parameter_types=
+    code_type.parameters();
+
+  // iterates over the types of the parameters
+  for(const auto &parameter : parameter_types)
   {
+    const irep_idt &identifier=parameter.get_identifier();
+
     INVARIANT(
       !identifier.empty(),
       source_location.as_string() + ": no identifier for function parameter");
@@ -254,9 +267,8 @@ 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(to_code_type(function_symbol.type).is_hidden())
+  if(goto_function.is_hidden())
   {
     for(auto &instruction : body.instructions)
       instruction.labels.remove(CPROVER_PREFIX "HIDE");
@@ -268,12 +280,12 @@ void goto_inlinet::insert_function_body(
   parameter_assignments(
     target,
     identifier,
-    goto_function.parameter_identifiers,
+    goto_function.type,
     arguments,
     tmp1);
 
   goto_programt tmp2;
-  parameter_destruction(target, goto_function.parameter_identifiers, tmp2);
+  parameter_destruction(target, goto_function.type, tmp2);
 
   goto_programt tmp;
   tmp.destructive_append(tmp1); // par assignment

src/goto-programs/goto_inline_class.h

@@ -178,13 +178,13 @@ class goto_inlinet:public messaget
   void parameter_assignments(
     const goto_programt::targett target,
     const irep_idt &function_name,
-    const goto_functiont::parameter_identifierst &parameter_identifiers,
+    const code_typet &code_type,
     const exprt::operandst &arguments,
     goto_programt &dest);
 
   void parameter_destruction(
     const goto_programt::targett target,
-    const goto_functiont::parameter_identifierst &parameter_identifiers,
+    const code_typet &code_type,
     goto_programt &dest);
 
   // goto functions that were already inlined transitively

src/goto-programs/link_goto_model.cpp

@@ -27,14 +27,8 @@ static void rename_symbols_in_function(
   irep_idt &new_function_name,
   const rename_symbolt &rename_symbol)
 {
-  for(auto &identifier : function.parameter_identifiers)
-  {
-    auto entry = rename_symbol.expr_map.find(identifier);
-    if(entry != rename_symbol.expr_map.end())
-      identifier = entry->second;
-  }
-
   goto_programt &program=function.body;
+  rename_symbol(function.type);
 
   Forall_goto_program_instructions(iit, program)
   {

src/goto-programs/read_bin_goto_object.cpp

@@ -87,12 +87,6 @@ static bool read_bin_goto_object(
     irep_idt fname=irepconverter.read_gb_string(in);
     goto_functionst::goto_functiont &f = functions.function_map[fname];
 
-    // parameter identifiers
-    std::size_t param_count = irepconverter.read_gb_word(in);
-    f.parameter_identifiers.reserve(param_count);
-    while(param_count-- > 0)
-      f.parameter_identifiers.push_back(irepconverter.read_string_ref(in));
-
     typedef std::map<goto_programt::targett, std::list<unsigned> > target_mapt;
     target_mapt target_map;
     typedef std::map<unsigned, goto_programt::targett> rev_target_mapt;