Merge pull request #4252 from tautschnig/use-parameter-identifiers

Use goto_functiont::parameter_identifiers instead of looking at the type [blocks: #4167]

Author: tautschnig

src/goto-instrument/code_contracts.cpp

@@ -324,24 +324,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 : gf.parameter_identifiers)
   {
-    symbol_exprt p =
-      new_tmp_symbol(
-        p_it->type(), skip->source_location, function, function_symbol.mode)
-        .symbol_expr();
+    PRECONDITION(!parameter.empty());
+    const symbolt &parameter_symbol = ns.lookup(parameter);
+
+    symbol_exprt p = new_tmp_symbol(
+                       parameter_symbol.type,
+                       skip->source_location,
+                       function,
+                       parameter_symbol.mode)
+                       .symbol_expr();
     check.add(goto_programt::make_decl(p, skip->source_location));
 
     call.arguments().push_back(p);
 
-    if(!p_it->get_identifier().empty())
-    {
-      symbol_exprt cur_p(p_it->get_identifier(), p_it->type());
-      replace.insert(cur_p, p);
-    }
+    replace.insert(parameter_symbol.symbol_expr(), p);
   }
 
   // assume(requires)

src/goto-instrument/generate_function_bodies.cpp

@@ -209,26 +209,24 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
       instruction->source_location = function_symbol.location;
       return instruction;
     };
+
     const namespacet ns(symbol_table);
-    for(auto const &parameter : function.type.parameters())
+    for(auto const &parameter : function.parameter_identifiers)
     {
+      const symbolt &parameter_symbol = ns.lookup(parameter);
       if(
-        parameter.type().id() == ID_pointer &&
-        !parameter.type().subtype().get_bool(ID_C_constant) &&
+        parameter_symbol.type.id() == ID_pointer &&
+        !parameter_symbol.type.subtype().get_bool(ID_C_constant) &&
         std::regex_match(
-          id2string(parameter.get_base_name()), parameters_to_havoc))
+          id2string(parameter_symbol.base_name), parameters_to_havoc))
       {
         auto goto_instruction =
           add_instruction(goto_programt::make_incomplete_goto(equal_exprt(
-            symbol_exprt(parameter.get_identifier(), parameter.type()),
-            null_pointer_exprt(to_pointer_type(parameter.type())))));
-
-        const irep_idt base_name = parameter.get_base_name();
-        CHECK_RETURN(!base_name.empty());
+            parameter_symbol.symbol_expr(),
+            null_pointer_exprt(to_pointer_type(parameter_symbol.type)))));
 
         dereference_exprt dereference_expr(
-          symbol_exprt(parameter.get_identifier(), parameter.type()),
-          parameter.type().subtype());
+          parameter_symbol.symbol_expr(), parameter_symbol.type.subtype());
 
         goto_programt dest;
         havoc_expr_rec(

src/goto-programs/goto_function.cpp

@@ -21,12 +21,9 @@ void get_local_identifiers(
 {
   goto_function.body.get_decl_identifiers(dest);
 
-  const code_typet::parameterst &parameters = goto_function.type.parameters();
-
   // add parameters
-  for(const auto &param : parameters)
+  for(const auto &identifier : goto_function.parameter_identifiers)
   {
-    const irep_idt &identifier = param.get_identifier();
     if(identifier != "")
       dest.insert(identifier);
   }

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 code_typet &code_type, // type of called function
+  const goto_functiont::parameter_identifierst &parameter_identifiers,
   const exprt::operandst &arguments, // arguments of call
   goto_programt &dest)
 {
@@ -43,28 +43,21 @@ void goto_inlinet::parameter_assignments(
   // iterates over the operands
   exprt::operandst::const_iterator it1=arguments.begin();
 
-  const code_typet::parameterst &parameter_types=
-    code_type.parameters();
-
-  // iterates over the types of the parameters
-  for(const auto &parameter : parameter_types)
+  // iterates over the parameters
+  for(const auto &identifier : parameter_identifiers)
   {
-    // 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);
+    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;
-    }
+    // this is the type the n-th argument should have
+    const typet &parameter_type = symbol.type;
+
+    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;
@@ -77,7 +70,7 @@ void goto_inlinet::parameter_assignments(
                 << "not enough arguments, "
                 << "inserting non-deterministic value" << eom;
 
-      actual = side_effect_expr_nondett(par_type, source_location);
+      actual = side_effect_expr_nondett(parameter_type, source_location);
     }
     else
       actual=*it1;
@@ -90,9 +83,9 @@ void goto_inlinet::parameter_assignments(
     {
       // it should be the same exact type as the parameter,
       // subject to some exceptions
-      if(!base_type_eq(par_type, actual.type(), ns))
+      if(!base_type_eq(parameter_type, actual.type(), ns))
       {
-        const typet &f_partype = par_type;
+        const typet &f_partype = parameter_type;
         const typet &f_acttype = actual.type();
 
         // we are willing to do some conversion
@@ -102,7 +95,7 @@ void goto_inlinet::parameter_assignments(
             f_acttype.id()==ID_array &&
             f_partype.subtype()==f_acttype.subtype()))
         {
-          actual = typecast_exprt(actual, par_type);
+          actual = typecast_exprt(actual, f_partype);
         }
         else if((f_partype.id()==ID_signedbv ||
                  f_partype.id()==ID_unsignedbv ||
@@ -111,7 +104,7 @@ void goto_inlinet::parameter_assignments(
                  f_acttype.id()==ID_unsignedbv ||
                  f_acttype.id()==ID_bool))
         {
-          actual = typecast_exprt(actual, par_type);
+          actual = typecast_exprt(actual, f_partype);
         }
         else
         {
@@ -120,7 +113,7 @@ void goto_inlinet::parameter_assignments(
       }
 
       // adds an assignment of the actual parameter to the formal parameter
-      code_assignt assignment(symbol_exprt(identifier, par_type), actual);
+      code_assignt assignment(symbol_exprt(identifier, parameter_type), actual);
       assignment.add_source_location()=source_location;
 
       dest.add_instruction(ASSIGN);
@@ -140,22 +133,16 @@ void goto_inlinet::parameter_assignments(
 
 void goto_inlinet::parameter_destruction(
   const goto_programt::targett target,
-  const code_typet &code_type, // type of called function
+  const goto_functiont::parameter_identifierst &parameter_identifiers,
   goto_programt &dest)
 {
   PRECONDITION(target->is_function_call());
   PRECONDITION(dest.empty());
 
   const source_locationt &source_location=target->source_location;
 
-  const code_typet::parameterst &parameter_types=
-    code_type.parameters();
-
-  // iterates over the types of the parameters
-  for(const auto &parameter : parameter_types)
+  for(const auto &identifier : parameter_identifiers)
   {
-    const irep_idt &identifier=parameter.get_identifier();
-
     INVARIANT(
       !identifier.empty(),
       source_location.as_string() + ": no identifier for function parameter");
@@ -278,14 +265,10 @@ void goto_inlinet::insert_function_body(
 
   goto_programt tmp1;
   parameter_assignments(
-    target,
-    identifier,
-    goto_function.type,
-    arguments,
-    tmp1);
+    target, identifier, goto_function.parameter_identifiers, arguments, tmp1);
 
   goto_programt tmp2;
-  parameter_destruction(target, goto_function.type, tmp2);
+  parameter_destruction(target, goto_function.parameter_identifiers, 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 code_typet &code_type,
+    const goto_functiont::parameter_identifierst &parameter_identifiers,
     const exprt::operandst &arguments,
     goto_programt &dest);
 
   void parameter_destruction(
     const goto_programt::targett target,
-    const code_typet &code_type,
+    const goto_functiont::parameter_identifierst &parameter_identifiers,
     goto_programt &dest);
 
   // goto functions that were already inlined transitively

src/goto-programs/interpreter.cpp

@@ -811,16 +811,14 @@ void interpretert::execute_function_call()
     }
 
     // assign the arguments
-    const code_typet::parameterst &parameters=
-      to_code_type(f_it->second.type).parameters();
-
-    if(argument_values.size()<parameters.size())
+    const auto &parameter_identifiers = f_it->second.parameter_identifiers;
+    if(argument_values.size() < parameter_identifiers.size())
       throw "not enough arguments";
 
-    for(std::size_t i=0; i<parameters.size(); i++)
+    for(std::size_t i = 0; i < parameter_identifiers.size(); i++)
     {
-      const code_typet::parametert &a=parameters[i];
-      const symbol_exprt symbol_expr(a.get_identifier(), a.type());
+      const symbol_exprt symbol_expr =
+        ns.lookup(parameter_identifiers[i]).symbol_expr();
       assign(evaluate_address(symbol_expr), argument_values[i]);
     }
 

src/goto-symex/symex_function_call.cpp

@@ -41,30 +41,18 @@ void goto_symext::parameter_assignments(
   // iterates over the arguments
   exprt::operandst::const_iterator it1=arguments.begin();
 
-  // these are the types of the parameters
-  const code_typet::parameterst &parameter_types=
-    function_type.parameters();
-
   // iterates over the types of the parameters
-  for(code_typet::parameterst::const_iterator
-      it2=parameter_types.begin();
-      it2!=parameter_types.end();
-      it2++)
+  for(const auto &identifier : goto_function.parameter_identifiers)
   {
-    const code_typet::parametert &parameter=*it2;
-
-    // this is the type that the n-th argument should have
-    const typet &parameter_type=parameter.type();
-
-    const irep_idt &identifier=parameter.get_identifier();
-
     INVARIANT(
-      !identifier.empty(),
-      "function pointer parameter must have an identifier");
+      !identifier.empty(), "function parameter must have an identifier");
 
     const symbolt &symbol=ns.lookup(identifier);
     symbol_exprt lhs=symbol.symbol_expr();
 
+    // this is the type that the n-th argument should have
+    const typet &parameter_type = symbol.type;
+
     exprt rhs;
 
     // if you run out of actual arguments there was a mismatch