renaming + signature of symex_function_call_code

This both renames the method symex_function_call_code and changes its
signature, to better reflect the ordering of steps when executing function
calls.

Author: kroening

src/goto-symex/goto_symex.h

@@ -464,11 +464,15 @@ class goto_symext
   /// \param get_goto_function: The delegate to retrieve function bodies (see
   ///   \ref get_goto_functiont)
   /// \param state: Symbolic execution state for current instruction
-  /// \param call: The function call instruction
-  virtual void symex_function_call_code(
+  /// \param cleaned_lhs: nil or the lhs of the function call, cleaned
+  /// \param function: the symbol of the function to call
+  /// \param cleaned_arguments: the arguments of the function call, cleaned
+  virtual void symex_function_call_post_clean(
     const get_goto_functiont &get_goto_function,
     statet &state,
-    const code_function_callt &call);
+    const exprt &cleaned_lhs,
+    const symbol_exprt &function,
+    const exprt::operandst &cleaned_arguments);
 
   virtual bool get_unwind_recursion(
     const irep_idt &identifier,

src/goto-symex/symex_function_call.cpp

@@ -197,30 +197,34 @@ void goto_symext::symex_function_call_symbol(
   const symbol_exprt &function,
   const exprt::operandst &arguments)
 {
-  code_function_callt code(lhs, function, arguments);
+  exprt cleaned_lhs;
 
-  if(code.lhs().is_not_nil())
-    code.lhs() = clean_expr(std::move(code.lhs()), state, true);
+  if(lhs.is_nil())
+    cleaned_lhs = lhs;
+  else
+    cleaned_lhs = clean_expr(lhs, state, true);
 
-  code.function() = clean_expr(std::move(code.function()), state, false);
+  // no need to clean the function, which is a symbol only
 
-  for(auto &argument : code.arguments())
-    argument = clean_expr(std::move(argument), state, false);
+  exprt::operandst cleaned_arguments;
 
-  target.location(state.guard.as_expr(), state.source);
+  for(auto &argument : arguments)
+    cleaned_arguments.push_back(clean_expr(argument, state, false));
 
-  PRECONDITION(code.function().id() == ID_symbol);
+  target.location(state.guard.as_expr(), state.source);
 
-  symex_function_call_code(get_goto_function, state, code);
+  symex_function_call_post_clean(
+    get_goto_function, state, cleaned_lhs, function, cleaned_arguments);
 }
 
-void goto_symext::symex_function_call_code(
+void goto_symext::symex_function_call_post_clean(
   const get_goto_functiont &get_goto_function,
   statet &state,
-  const code_function_callt &call)
+  const exprt &cleaned_lhs,
+  const symbol_exprt &function,
+  const exprt::operandst &cleaned_arguments)
 {
-  const irep_idt &identifier=
-    to_symbol_expr(call.function()).get_identifier();
+  const irep_idt &identifier = function.get_identifier();
 
   const goto_functionst::goto_functiont &goto_function =
     get_goto_function(identifier);
@@ -258,10 +262,10 @@ void goto_symext::symex_function_call_code(
   }
 
   // read the arguments -- before the locality renaming
-  const exprt::operandst &arguments = call.arguments();
   const std::vector<renamedt<exprt, L2>> renamed_arguments =
-    make_range(arguments).map(
-      [&](const exprt &a) { return state.rename(a, ns); });
+    make_range(cleaned_arguments).map([&](const exprt &a) {
+      return state.rename(a, ns);
+    });
 
   // we hide the call if the caller and callee are both hidden
   const bool hidden =
@@ -279,18 +283,18 @@ void goto_symext::symex_function_call_code(
     target.function_return(
       state.guard.as_expr(), identifier, state.source, hidden);
 
-    if(call.lhs().is_not_nil())
+    if(cleaned_lhs.is_not_nil())
     {
-      const auto rhs =
-        side_effect_expr_nondett(call.lhs().type(), call.source_location());
-      symex_assign(state, call.lhs(), rhs);
+      const auto rhs = side_effect_expr_nondett(
+        cleaned_lhs.type(), state.source.pc->source_location());
+      symex_assign(state, cleaned_lhs, rhs);
     }
 
     if(symex_config.havoc_undefined_functions)
     {
       // assign non det to function arguments if pointers
       // are not const
-      for(const auto &arg : call.arguments())
+      for(const auto &arg : cleaned_arguments)
       {
         if(
           arg.type().id() == ID_pointer &&
@@ -325,10 +329,10 @@ void goto_symext::symex_function_call_code(
   locality(identifier, state, path_storage, goto_function, ns);
 
   // assign actuals to formal parameters
-  parameter_assignments(identifier, goto_function, state, arguments);
+  parameter_assignments(identifier, goto_function, state, cleaned_arguments);
 
   frame.end_of_function=--goto_function.body.instructions.end();
-  frame.return_value=call.lhs();
+  frame.return_value = cleaned_lhs;
   frame.function_identifier=identifier;
   frame.hidden_function = goto_function.is_hidden();