Merge pull request #4080 from romainbrenguier/doc/symex-function-call

Clean-up and document symex_function_call [DOC-150]

Author: romainbrenguier

src/goto-symex/goto_symex.h

@@ -275,27 +275,37 @@ class goto_symext
 
   virtual void loop_bound_exceeded(statet &, const exprt &guard);
 
-  // function calls
-
-  void pop_frame(statet &);
-  void return_assignment(statet &);
-
   virtual void no_body(const irep_idt &)
   {
   }
 
+  /// Symbolic execution of a function call.
+  /// Only functions that are symbols are supported, see
+  /// \ref goto_symext::symex_function_call_symbol
   virtual void symex_function_call(
     const get_goto_functiont &,
     statet &,
     const code_function_callt &);
 
   virtual void symex_end_of_function(statet &);
 
+  /// Symbolic execution of a call to a function call.
+  /// For functions \c CBMC_trace and functions starting with \c __CPROVER_fkt
+  /// see \ref goto_symext::symex_trace and
+  /// \ref goto_symext::symex_fkt
+  /// For non-special functions see
+  /// \ref goto_symext::symex_function_call_code
   virtual void symex_function_call_symbol(
     const get_goto_functiont &,
     statet &,
     const code_function_callt &);
 
+  /// Symbolic execution of a function call by inlining.
+  /// Records the call in \p target by appending a function call step and:
+  ///   - if the body is available create a new frame, assigns the parameters,
+  ///    and proceed to executing the code of the function.
+  ///   - otherwise assign a nondetministic value to the left-hand-side of the
+  ///     call when there is one
   virtual void symex_function_call_code(
     const get_goto_functiont &,
     statet &,
@@ -306,17 +316,18 @@ class goto_symext
     unsigned thread_nr,
     unsigned unwind);
 
+  /// Iterates over \p arguments and assigns them to the parameters, which are
+  /// symbols whose name and type are deduced from the type of \p goto_function.
+  /// \param function_identifier: name of the function
+  /// \param goto_function: function whose parameters we want to assign
+  /// \param [out] state: state of the goto program
+  /// \param arguments: arguments that are passed to the function
   void parameter_assignments(
     const irep_idt &function_identifier,
     const goto_functionst::goto_functiont &,
     statet &,
     const exprt::operandst &arguments);
 
-  void locality(
-    const irep_idt &function_identifier,
-    statet &,
-    const goto_functionst::goto_functiont &);
-
   // exceptions
   void symex_throw(statet &);
   void symex_catch(statet &);

src/goto-symex/symex_function_call.cpp

@@ -18,6 +18,12 @@ Author: Daniel Kroening, [email protected]
 #include <util/exception_utils.h>
 #include <util/invariant.h>
 
+static void locality(
+  const irep_idt &function_identifier,
+  goto_symext::statet &state,
+  const goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns);
+
 bool goto_symext::get_unwind_recursion(const irep_idt &, unsigned, unsigned)
 {
   return false;
@@ -220,7 +226,6 @@ void goto_symext::symex_function_call_symbol(
     symex_function_call_code(get_goto_function, state, code);
 }
 
-/// do function call by inlining
 void goto_symext::symex_function_call_code(
   const get_goto_functiont &get_goto_function,
   statet &state,
@@ -300,7 +305,7 @@ void goto_symext::symex_function_call_code(
   framet &frame = state.new_frame();
 
   // preserve locality of local variables
-  locality(identifier, state, goto_function);
+  locality(identifier, state, goto_function, ns);
 
   // assign actuals to formal parameters
   parameter_assignments(identifier, goto_function, state, arguments);
@@ -327,7 +332,7 @@ void goto_symext::symex_function_call_code(
 }
 
 /// pop one call frame
-void goto_symext::pop_frame(statet &state)
+static void pop_frame(goto_symext::statet &state)
 {
   PRECONDITION(!state.call_stack().empty());
 
@@ -378,10 +383,11 @@ void goto_symext::symex_end_of_function(statet &state)
 
 /// preserves locality of local variables of a given function by applying L1
 /// renaming to the local identifiers
-void goto_symext::locality(
+static void locality(
   const irep_idt &function_identifier,
-  statet &state,
-  const goto_functionst::goto_functiont &goto_function)
+  goto_symext::statet &state,
+  const goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns)
 {
   unsigned &frame_nr=
     state.threads[state.source.thread_nr].function_frame[function_identifier];
@@ -441,28 +447,3 @@ void goto_symext::locality(
   }
 }
 
-void goto_symext::return_assignment(statet &state)
-{
-  framet &frame = state.top();
-
-  const goto_programt::instructiont &instruction=*state.source.pc;
-  PRECONDITION(instruction.is_return());
-  const code_returnt &code = instruction.get_return();
-
-  target.location(state.guard.as_expr(), state.source);
-
-  PRECONDITION(code.operands().size() == 1 || frame.return_value.is_nil());
-
-  exprt value = code.return_value();
-
-  if(frame.return_value.is_not_nil())
-  {
-    code_assignt assignment(frame.return_value, value);
-
-    INVARIANT(
-      base_type_eq(assignment.lhs().type(), assignment.rhs().type(), ns),
-      "goto_symext::return_assignment type mismatch");
-
-    symex_assign(state, assignment);
-  }
-}

src/goto-symex/symex_main.cpp

@@ -441,10 +441,8 @@ void goto_symext::symex_step(
     break;
 
   case RETURN:
-    if(!state.guard.is_false())
-      return_assignment(state);
-
-    symex_transition(state);
+    // This case should have been removed by return-value removal
+    UNREACHABLE;
     break;
 
   case ASSIGN: