Merge pull request #6406 from diffblue/symex_function_call

clean up goto_symex function calls

Author: kroening

src/goto-symex/goto_symex.h

@@ -431,29 +431,29 @@ 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 code: The function call instruction
+  /// \param instruction: The function call instruction
   virtual void symex_function_call(
     const get_goto_functiont &get_goto_function,
     statet &state,
-    const code_function_callt &code);
+    const goto_programt::instructiont &instruction);
 
   /// Symbolically execute a END_FUNCTION instruction.
   /// \param state: Symbolic execution state for current instruction
   virtual void symex_end_of_function(statet &);
 
   /// Symbolic execution of a call to a function call.
-  /// For functions starting with \c __CPROVER_fkt
-  /// \ref goto_symext::symex_fkt
-  /// For non-special functions see
-  /// \ref goto_symext::symex_function_call_code
   /// \param get_goto_function: The delegate to retrieve function bodies (see
   ///   \ref get_goto_functiont)
   /// \param state: Symbolic execution state for current instruction
-  /// \param code: The function call instruction
+  /// \param lhs: nil or the lhs of the function call instruction
+  /// \param function: the symbol of the function to call
+  /// \param arguments: the arguments of the function call
   virtual void symex_function_call_symbol(
     const get_goto_functiont &get_goto_function,
     statet &state,
-    const code_function_callt &code);
+    const exprt &lhs,
+    const symbol_exprt &function,
+    const exprt::operandst &arguments);
 
   /// Symbolic execution of a function call by inlining.
   /// Records the call in \p target by appending a function call step and:
@@ -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,
@@ -754,16 +758,7 @@ class goto_symext
   /// \param code: right-hand side containing side effect
   virtual void
   symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code);
-  /// Symbolically execute a FUNCTION_CALL instruction for a function whose
-  /// name starts with CPROVER_FKT_PREFIX
-  /// \remarks
-  /// While the name seems to imply that this would be called when symbolic
-  /// execution doesn't know what to do, it may actually be derived from a
-  /// German abbreviation for function.
-  /// This should not be called as these functions should already be removed
-  /// \param state: Symbolic execution state for current instruction
-  /// \param code: The function call instruction
-  virtual void symex_fkt(statet &state, const code_function_callt &code);
+
   /// Symbolically execute an OTHER instruction that does a CPP `printf`
   /// \param state: Symbolic execution state for current instruction
   /// \param rhs: The cleaned up CPP `printf` instruction

src/goto-symex/symex_builtin_functions.cpp

@@ -534,28 +534,3 @@ void goto_symext::symex_cpp_delete(
   bool do_array=code.get(ID_statement)==ID_cpp_delete_array;
   #endif
 }
-
-void goto_symext::symex_fkt(
-  statet &,
-  const code_function_callt &)
-{
-  // TODO: uncomment this line when TG-4667 is done
-  // UNREACHABLE;
-  #if 0
-  exprt new_fc(ID_function, fc.type());
-
-  new_fc.reserve_operands(fc.operands().size()-1);
-
-  bool first=true;
-
-  Forall_operands(it, fc)
-    if(first)
-      first=false;
-    else
-      new_fc.add_to_operands(std::move(*it));
-
-  new_fc.set(ID_identifier, fc.op0().get(ID_identifier));
-
-  fc.swap(new_fc);
-  #endif
-}

src/goto-symex/symex_function_call.cpp

@@ -173,54 +173,58 @@ void goto_symext::parameter_assignments(
 void goto_symext::symex_function_call(
   const get_goto_functiont &get_goto_function,
   statet &state,
-  const code_function_callt &code)
+  const goto_programt::instructiont &instruction)
 {
-  const exprt &function=code.function();
+  const exprt &function = instruction.call_function();
 
   // If at some point symex_function_call can support more
   // expression ids(), like ID_Dereference, please expand the
   // precondition appropriately.
   PRECONDITION(function.id() == ID_symbol);
-  symex_function_call_symbol(get_goto_function, state, code);
+
+  symex_function_call_symbol(
+    get_goto_function,
+    state,
+    instruction.call_lhs(),
+    to_symbol_expr(instruction.call_function()),
+    instruction.call_arguments());
 }
 
 void goto_symext::symex_function_call_symbol(
   const get_goto_functiont &get_goto_function,
   statet &state,
-  const code_function_callt &original_code)
+  const exprt &lhs,
+  const symbol_exprt &function,
+  const exprt::operandst &arguments)
 {
-  code_function_callt code = original_code;
-
-  if(code.lhs().is_not_nil())
-    code.lhs() = clean_expr(std::move(code.lhs()), state, true);
+  exprt cleaned_lhs;
 
-  code.function() = clean_expr(std::move(code.function()), state, false);
+  if(lhs.is_nil())
+    cleaned_lhs = lhs;
+  else
+    cleaned_lhs = clean_expr(lhs, state, true);
 
-  for(auto &argument : code.arguments())
-    argument = clean_expr(std::move(argument), state, false);
+  // no need to clean the function, which is a symbol only
 
-  target.location(state.guard.as_expr(), state.source);
+  exprt::operandst cleaned_arguments;
 
-  PRECONDITION(code.function().id() == ID_symbol);
+  for(auto &argument : arguments)
+    cleaned_arguments.push_back(clean_expr(argument, state, false));
 
-  const irep_idt &identifier=
-    to_symbol_expr(code.function()).get_identifier();
+  target.location(state.guard.as_expr(), state.source);
 
-  if(has_prefix(id2string(identifier), CPROVER_FKT_PREFIX))
-  {
-    symex_fkt(state, code);
-  }
-  else
-    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();
 

src/goto-symex/symex_main.cpp

@@ -674,13 +674,7 @@ void goto_symext::execute_next_instruction(
 
   case FUNCTION_CALL:
     if(state.reachable)
-    {
-      code_function_callt call(
-        instruction.call_lhs(),
-        instruction.call_function(),
-        instruction.call_arguments());
-      symex_function_call(get_goto_function, state, call);
-    }
+      symex_function_call(get_goto_function, state, instruction);
     else
       symex_transition(state);
     break;