Merge pull request #4167 from tautschnig/parameter-identifiers

Use goto_functiont::parameter_identifiers and remove goto_functiont::type

Author: tautschnig

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/goto-checker/symex_coverage.cpp

@@ -161,7 +161,7 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
   xml.set_attribute("name", id2string(gf_it->first));
 
   xml.set_attribute(
-    "signature", from_type(ns, gf_it->first, gf_it->second.type));
+    "signature", from_type(ns, gf_it->first, ns.lookup(gf_it->first).type));
 
   xml.set_attribute("line-rate", rate_detailed(lines_covered, lines_total));
   xml.set_attribute("branch-rate", rate(branches_covered, branches_total));

src/goto-harness/function_call_harness_generator.cpp

@@ -453,10 +453,6 @@ void function_call_harness_generatort::implt::
 
   symbol_table->insert(harness_function_symbol);
 
-  auto const &generated_harness =
-    symbol_table->lookup_ref(harness_function_name);
-  goto_functions->function_map[harness_function_name].type =
-    to_code_type(generated_harness.type);
   goto_convert(*symbol_table, *goto_functions, *message_handler);
 }
 

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -322,7 +322,6 @@ void memory_snapshot_harness_generatort::
   CHECK_RETURN(function_iterator_pair.second);
 
   goto_functiont &harness_function = function_iterator_pair.first->second;
-  harness_function.type = to_code_type(function.type);
 
   goto_convert(
     goto_model.symbol_table, goto_model.goto_functions, message_handler);

src/goto-harness/recursive_initialization.cpp

@@ -366,8 +366,6 @@ irep_idt recursive_initializationt::build_constructor(const exprt &expr)
     expr_name,
     is_nullable);
 
-  goto_model.goto_functions.function_map[function_symbol.name].type =
-    to_code_type(function_symbol.type);
   return type_constructor_names.at(key);
 }
 

src/goto-instrument/code_contracts.cpp

@@ -484,8 +484,8 @@ void code_contractst::instrument_call_statement(
       return;
     }
 
-    exprt called_assigns = static_cast<const exprt &>(
-      called_func->second.type.find(ID_C_spec_assigns));
+    exprt called_assigns =
+      static_cast<const exprt &>(called_sym.type.find(ID_C_spec_assigns));
     if(called_assigns.is_nil()) // Called function has no assigns clause
     {
       // Fail if called function has no assigns clause.
@@ -749,8 +749,6 @@ bool code_contractst::enforce_contract(const std::string &fun_to_enforce)
 
   goto_functiont &wrapper = goto_functions.function_map[original];
   wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers;
-  if(mangled_fun->second.type.is_not_nil())
-    wrapper.type = mangled_fun->second.type;
   wrapper.body.add(goto_programt::make_end_function(sl));
   add_contract_check(original, mangled, wrapper.body);
   return false;
@@ -763,18 +761,15 @@ void code_contractst::add_contract_check(
 {
   PRECONDITION(!dest.instructions.empty());
 
-  goto_functionst::function_mapt::iterator f_it =
-    goto_functions.function_map.find(mangled_fun);
-  PRECONDITION(f_it != goto_functions.function_map.end());
-
-  const goto_functionst::goto_functiont &gf = f_it->second;
+  const symbolt &function_symbol = ns.lookup(mangled_fun);
+  const code_typet &code_type = to_code_type(function_symbol.type);
 
   const exprt &assigns =
-    static_cast<const exprt &>(gf.type.find(ID_C_spec_assigns));
+    static_cast<const exprt &>(code_type.find(ID_C_spec_assigns));
   const exprt &requires =
-    static_cast<const exprt &>(gf.type.find(ID_C_spec_requires));
+    static_cast<const exprt &>(code_type.find(ID_C_spec_requires));
   const exprt &ensures =
-    static_cast<const exprt &>(gf.type.find(ID_C_spec_ensures));
+    static_cast<const exprt &>(code_type.find(ID_C_spec_ensures));
   INVARIANT(
     ensures.is_not_nil() || assigns.is_not_nil(),
     "Code contract enforcement is trivial without an ensures or assigns "
@@ -803,15 +798,14 @@ void code_contractst::add_contract_check(
     skip->source_location));
 
   // prepare function call including all declarations
-  const symbolt &function_symbol = ns.lookup(mangled_fun);
   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())
   {
     symbol_exprt r = new_tmp_symbol(
-                       gf.type.return_type(),
+                       code_type.return_type(),
                        skip->source_location,
                        wrapper_fun,
                        function_symbol.mode)
@@ -825,6 +819,11 @@ void code_contractst::add_contract_check(
   }
 
   // decl parameter1 ...
+  goto_functionst::function_mapt::iterator f_it =
+    goto_functions.function_map.find(mangled_fun);
+  PRECONDITION(f_it != goto_functions.function_map.end());
+
+  const goto_functionst::goto_functiont &gf = f_it->second;
   for(const auto &parameter : gf.parameter_identifiers)
   {
     PRECONDITION(!parameter.empty());

src/goto-instrument/generate_function_bodies.cpp

@@ -64,7 +64,6 @@ void generate_function_bodiest::generate_parameter_names(
       symbol_table.add(new_param_sym);
     }
   }
-  function.type = to_code_type(function_symbol.type);
   function.set_parameter_identifiers(to_code_type(function_symbol.type));
 }
 
@@ -321,9 +320,10 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
       function.body.destructive_append(dest);
     }
 
-    if(function.type.return_type() != empty_typet())
+    const typet &return_type = to_code_type(function_symbol.type).return_type();
+    if(return_type != empty_typet())
     {
-      typet type(function.type.return_type());
+      typet type(return_type);
       type.remove(ID_C_constant);
 
       symbolt &aux_symbol = get_fresh_aux_symbol(
@@ -350,8 +350,8 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
 
       function.body.destructive_append(dest);
 
-      exprt return_expr = typecast_exprt::conditional_cast(
-        aux_symbol.symbol_expr(), function.type.return_type());
+      exprt return_expr =
+        typecast_exprt::conditional_cast(aux_symbol.symbol_expr(), return_type);
 
       add_instruction(goto_programt::make_return(code_returnt(return_expr)));
 
@@ -590,8 +590,6 @@ void generate_function_bodies(
     model.symbol_table.lookup_ref(havoc_function_symbol.name);
 
   // convert to get the function stub to goto-model
-  model.goto_functions.function_map[havoc_function_symbol.name].type =
-    to_code_type(generated_havoc.type);
   goto_convert(model.symbol_table, model.goto_functions, message_handler);
 
   // now generate body as above

src/goto-instrument/replace_calls.cpp

@@ -94,10 +94,8 @@ void replace_callst::operator()(
     auto f_it2 = goto_functions.function_map.find(new_id);
     PRECONDITION(f_it2 != goto_functions.function_map.end());
 
-    PRECONDITION(base_type_eq(f_it1->second.type, f_it2->second.type, ns));
-
     // check that returns have not been removed
-    if(to_code_type(f_it1->second.type).return_type().id() != ID_empty)
+    if(to_code_type(function.type()).return_type().id() != ID_empty)
     {
       goto_programt::const_targett next_it = std::next(it);
       if(next_it != goto_program.instructions.end() && next_it->is_assign())
@@ -112,7 +110,7 @@ void replace_callst::operator()(
     }
 
     // Finally modify the call
-    function.type() = f_it2->second.type;
+    function.type() = ns.lookup(f_it2->first).type;
     se.set_identifier(new_id);
 
     ins.set_function_call(cfc);
@@ -167,7 +165,8 @@ void replace_callst::check_replacement_map(
     auto it1 = goto_functions.function_map.find(p.first);
     if(it1 != goto_functions.function_map.end())
     {
-      if(!base_type_eq(it1->second.type, it2->second.type, ns))
+      if(!base_type_eq(
+           ns.lookup(it1->first).type, ns.lookup(it2->first).type, ns))
         throw invalid_command_line_argument_exceptiont(
           "functions " + id2string(p.first) + " and " + id2string(p.second) +
             " are not type-compatible",

src/goto-programs/goto_convert_functions.cpp

@@ -87,6 +87,7 @@ 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
@@ -133,7 +134,7 @@ void goto_convert_functionst::add_return(
 
 #endif
 
-  side_effect_expr_nondett rhs(f.type.return_type(), source_location);
+  side_effect_expr_nondett rhs(return_type, source_location);
 
   f.body.add(
     goto_programt::make_return(code_returnt(std::move(rhs)), source_location));
@@ -154,7 +155,6 @@ void goto_convert_functionst::convert_function(
 
   // store the parameter identifiers in the goto functions
   const code_typet &code_type = to_code_type(symbol.type);
-  f.type = code_type;
   f.set_parameter_identifiers(code_type);
 
   if(
@@ -190,15 +190,15 @@ void goto_convert_functionst::convert_function(
 
   targets = targetst();
   targets.set_return(end_function);
-  targets.has_return_value = f.type.return_type().id() != ID_empty &&
-                             f.type.return_type().id() != ID_constructor &&
-                             f.type.return_type().id() != ID_destructor;
+  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;
 
   goto_convert_rec(code, f.body, mode);
 
   // add non-det return value, if needed
   if(targets.has_return_value)
-    add_return(f, end_location);
+    add_return(f, code_type.return_type(), end_location);
 
   // handle SV-COMP's __VERIFIER_atomic_
   if(

src/goto-programs/goto_convert_functions.h

@@ -58,6 +58,7 @@ 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.cpp

@@ -46,27 +46,4 @@ void goto_functiont::validate(const namespacet &ns, const validation_modet vm)
   }
 
   body.validate(ns, vm);
-
-  find_symbols_sett typetags;
-  find_type_symbols(type, typetags);
-  const symbolt *symbol;
-  for(const auto &identifier : typetags)
-  {
-    DATA_CHECK(
-      vm, !ns.lookup(identifier, symbol), id2string(identifier) + " not found");
-  }
-
-  // Check that a void function does not contain any RETURN instructions
-  if(to_code_type(type).return_type().id() == ID_empty)
-  {
-    forall_goto_program_instructions(instruction, body)
-    {
-      DATA_CHECK(
-        vm,
-        !instruction->is_return(),
-        "void function should not return a value");
-    }
-  }
-
-  validate_full_type(type, ns, vm);
 }

src/goto-programs/goto_function.h

@@ -16,25 +16,19 @@ Date: May 2018
 
 #include <iosfwd>
 
-#include <util/deprecate.h>
 #include <util/find_symbols.h>
 #include <util/std_types.h>
 
 #include "goto_program.h"
 
-/// A goto function, consisting of function type (see #type), function body (see
-/// #body), and parameter identifiers (see #parameter_identifiers).
+/// A goto function, consisting of function body (see #body) and parameter
+/// identifiers (see #parameter_identifiers).
 class goto_functiont
 {
 public:
   goto_programt body;
 
-  /// The type of the function, indicating the return type and parameter types
-  DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead"))
-  code_typet type;
-
   typedef std::vector<irep_idt> parameter_identifierst;
-
   /// The identifiers of the parameters of this function
   ///
   /// Note: This is now the preferred way of getting the identifiers of the
@@ -54,12 +48,6 @@ class goto_functiont
       parameter_identifiers.push_back(parameter.get_identifier());
   }
 
-  DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead"))
-  bool is_inlined() const
-  {
-    return type.get_bool(ID_C_inlined);
-  }
-
   bool is_hidden() const
   {
     return function_is_hidden;
@@ -70,30 +58,27 @@ class goto_functiont
     function_is_hidden = true;
   }
 
-  goto_functiont() : body(), type({}, empty_typet()), function_is_hidden(false)
+  goto_functiont() : body(), function_is_hidden(false)
   {
   }
 
   void clear()
   {
     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;
   }
@@ -103,7 +88,6 @@ 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)),
       function_is_hidden(other.function_is_hidden)
   {
@@ -112,7 +96,6 @@ class goto_functiont
   goto_functiont &operator=(goto_functiont &&other)
   {
     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;