goto_symex: implement SET_RETURN_VALUE

regression/cbmc-cover/block-coverage-report2/test.desc

@@ -4,7 +4,7 @@ main.c
 block 1 \(lines main.c:main:13,14\): SATISFIED
 block 2 \(lines main.c:main:15\): SATISFIED
 block 3 \(lines main.c:main:17,18\): SATISFIED
-block 4 \(lines main.c:main:18,19\): SATISFIED
+block 4 \(lines main.c:main:19\): SATISFIED
 block 5 \(lines main.c:main:20\): SATISFIED
 block 6 \(lines main.c:main:15,21,22\): SATISFIED
 block 7 \(lines main.c:main:24,25\): SATISFIED

regression/cbmc/reachability-slice-interproc3/test.desc

@@ -3,6 +3,6 @@ main.c
 --reachability-slice-fb --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-ASSIGN main#return_value := 1
+SET RETURN VALUE 1$
 --
 ^warning: ignoring

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/process_goto_program.h>
+#include <goto-programs/remove_returns.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/show_symbol_table.h>
@@ -388,6 +389,7 @@ int goto_analyzer_parse_optionst::doit()
   // Preserve backwards compatibility in processing
   options.set_option("partial-inline", true);
   options.set_option("rewrite-union", false);
+  options.set_option("remove-returns", true);
 
   if(process_goto_program(options))
     return CPROVER_EXIT_INTERNAL_ERROR;

src/goto-programs/mm_io.cpp

@@ -13,6 +13,7 @@ Date:   April 2017
 
 #include "mm_io.h"
 
+#include <util/fresh_symbol.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
@@ -35,6 +36,7 @@ void collect_deref_expr(
 
 void mm_io(
   const exprt &mm_io_r,
+  const exprt &mm_io_r_value,
   const exprt &mm_io_w,
   goto_functionst::goto_functiont &goto_function,
   const namespacet &ns)
@@ -60,21 +62,20 @@ void mm_io(
           source_locationt source_location = it->source_location();
           const code_typet &ct=to_code_type(mm_io_r.type());
 
-          irep_idt identifier=to_symbol_expr(mm_io_r).get_identifier();
-          auto return_value = return_value_symbol(identifier, ns);
-          if_exprt if_expr(integer_address(d.pointer()), return_value, d);
+          if_exprt if_expr(integer_address(d.pointer()), mm_io_r_value, d);
           replace_expr(d, if_expr, a_rhs);
 
           const typet &pt=ct.parameters()[0].type();
           const typet &st=ct.parameters()[1].type();
           auto size_opt = size_of_expr(d.type(), ns);
           CHECK_RETURN(size_opt.has_value());
-          const code_function_callt fc(
+          auto call = goto_programt::make_function_call(
+            mm_io_r_value,
             mm_io_r,
             {typecast_exprt(d.pointer(), pt),
-             typecast_exprt(size_opt.value(), st)});
-          goto_function.body.insert_before_swap(it);
-          *it = goto_programt::make_function_call(fc, source_location);
+             typecast_exprt(size_opt.value(), st)},
+            source_location);
+          goto_function.body.insert_before_swap(it, call);
           it++;
         }
       }
@@ -105,26 +106,37 @@ void mm_io(
   }
 }
 
-void mm_io(
-  const symbol_tablet &symbol_table,
-  goto_functionst &goto_functions)
+void mm_io(symbol_tablet &symbol_table, goto_functionst &goto_functions)
 {
   const namespacet ns(symbol_table);
-  exprt mm_io_r=nil_exprt(), mm_io_w=nil_exprt();
+  exprt mm_io_r = nil_exprt(), mm_io_r_value = nil_exprt(),
+        mm_io_w = nil_exprt();
 
   irep_idt id_r=CPROVER_PREFIX "mm_io_r";
   irep_idt id_w=CPROVER_PREFIX "mm_io_w";
 
   auto maybe_symbol=symbol_table.lookup(id_r);
   if(maybe_symbol)
+  {
     mm_io_r=maybe_symbol->symbol_expr();
 
+    const auto &value_symbol = get_fresh_aux_symbol(
+      to_code_type(mm_io_r.type()).return_type(),
+      id2string(id_r) + "$value",
+      id2string(id_r) + "$value",
+      maybe_symbol->location,
+      maybe_symbol->mode,
+      symbol_table);
+
+    mm_io_r_value = value_symbol.symbol_expr();
+  }
+
   maybe_symbol=symbol_table.lookup(id_w);
   if(maybe_symbol)
     mm_io_w=maybe_symbol->symbol_expr();
 
   for(auto & f : goto_functions.function_map)
-    mm_io(mm_io_r, mm_io_w, f.second, ns);
+    mm_io(mm_io_r, mm_io_r_value, mm_io_w, f.second, ns);
 }
 
 void mm_io(goto_modelt &model)

src/goto-programs/process_goto_program.cpp

@@ -58,9 +58,16 @@ bool process_goto_program(
   }
 
   // remove returns, gcc vectors, complex
-  remove_returns(goto_model);
+  if(
+    options.get_bool_option("remove-returns") ||
+    options.get_bool_option("string-abstraction"))
+  {
+    remove_returns(goto_model);
+  }
+
   remove_vector(goto_model);
   remove_complex(goto_model);
+
   if(options.get_bool_option("rewrite-union"))
     rewrite_union(goto_model);
 

src/goto-programs/validate_goto_model.cpp

@@ -14,7 +14,6 @@ Date: Oct 2018
 #include <util/pointer_expr.h>
 
 #include "goto_functions.h"
-#include "remove_returns.h"
 
 namespace
 {
@@ -38,18 +37,6 @@ class validate_goto_modelt
   /// Check that no function calls via function pointer are present
   void function_pointer_calls_removed();
 
-  /// Check returns have been removed
-  ///
-  /// Calls via function pointer must have been removed already when
-  /// removing returns, thus enabling this check also enables the check
-  /// that all calls via function pointer have been removed
-  ///
-  /// Sub-checks are:
-  /// - no return statements in any of the functions
-  /// - lhs of every \ref code_function_callt instruction is nil
-  /// - all return types are void (of both calls and functions themselves)
-  void check_returns_removed();
-
   /// Check that for all:
   /// -# functions that are called or
   /// -# functions of which the address is taken
@@ -74,19 +61,11 @@ validate_goto_modelt::validate_goto_modelt(
   if(validation_options.entry_point_exists)
     entry_point_exists();
 
-  /// NB function pointer calls must have been removed before removing
-  /// returns - so 'check_returns_removed' also enables
-  // 'function_pointer_calls_removed'
-  if(
-    validation_options.function_pointer_calls_removed ||
-    validation_options.check_returns_removed)
+  if(validation_options.function_pointer_calls_removed)
   {
     function_pointer_calls_removed();
   }
 
-  if(validation_options.check_returns_removed)
-    check_returns_removed();
-
   if(validation_options.check_called_functions)
     check_called_functions();
 }
@@ -116,30 +95,6 @@ void validate_goto_modelt::function_pointer_calls_removed()
   }
 }
 
-void validate_goto_modelt::check_returns_removed()
-{
-  for(const auto &fun : function_map)
-  {
-    const goto_functiont &goto_function = fun.second;
-
-    for(const auto &instr : goto_function.body.instructions)
-    {
-      DATA_CHECK(
-        vm,
-        !instr.is_set_return_value(),
-        "no SET_RETURN_VALUE instructions should be present");
-
-      if(instr.is_function_call())
-      {
-        DATA_CHECK(
-          vm,
-          !does_function_call_return(instr),
-          "function call lhs return should be nil");
-      }
-    }
-  }
-}
-
 void validate_goto_modelt::check_called_functions()
 {
   auto test_for_function_address =

src/goto-symex/Makefile

@@ -31,6 +31,7 @@ SRC = auto_objects.cpp \
       symex_goto.cpp \
       symex_main.cpp \
       symex_other.cpp \
+      symex_set_return_value.cpp \
       symex_start_thread.cpp \
       symex_target.cpp \
       symex_target_equation.cpp \

src/goto-symex/frame.h

@@ -14,6 +14,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 
 #include "goto_state.h"
 #include "symex_target.h"
+
 #include <analyses/lexical_loops.h>
 
 /// Stack frames -- these are used for function calls and for exceptions
@@ -30,7 +31,8 @@ struct framet
   std::vector<irep_idt> parameter_names;
   guardt guard_at_function_start;
   goto_programt::const_targett end_of_function;
-  exprt return_value = nil_exprt();
+  exprt call_lhs = nil_exprt();                // cleaned, but not renamed
+  optionalt<symbol_exprt> return_value_symbol; // not renamed
   bool hidden_function = false;
 
   symex_level1t old_level1;

src/goto-symex/goto_symex.h

@@ -303,6 +303,10 @@ class goto_symext
   /// Symbolically execute a GOTO instruction in the context of unreachable code
   /// \param state: Symbolic execution state for current instruction
   void symex_unreachable_goto(statet &state);
+  /// Symbolically execute a SET_RETURN_VALUE instruction
+  /// \param state: Symbolic execution state for current instruction
+  /// \param return_value: The value to be returned
+  void symex_set_return_value(statet &state, const exprt &return_value);
   /// Symbolically execute a START_THREAD instruction
   /// \param state: Symbolic execution state for current instruction
   virtual void symex_start_thread(statet &state);

src/goto-symex/symex_function_call.cpp

@@ -332,11 +332,33 @@ void goto_symext::symex_function_call_post_clean(
   // assign actuals to formal parameters
   parameter_assignments(identifier, goto_function, state, cleaned_arguments);
 
-  frame.end_of_function=--goto_function.body.instructions.end();
-  frame.return_value = cleaned_lhs;
+  frame.call_lhs = cleaned_lhs;
+  frame.end_of_function = --goto_function.body.instructions.end();
   frame.function_identifier=identifier;
   frame.hidden_function = goto_function.is_hidden();
 
+  // set up the 'return value symbol' when needed
+  if(frame.call_lhs.is_not_nil())
+  {
+    irep_idt return_value_symbol_identifier =
+      "goto_symex::return_value::" + id2string(identifier);
+
+    if(!state.symbol_table.has_symbol(return_value_symbol_identifier))
+    {
+      const symbolt &function_symbol = ns.lookup(identifier);
+      auxiliary_symbolt
+        new_symbol; // these are thread-local and have dynamic lifetime
+      new_symbol.base_name = "return_value";
+      new_symbol.name = return_value_symbol_identifier;
+      new_symbol.type = to_code_type(function_symbol.type).return_type();
+      new_symbol.mode = function_symbol.mode;
+      state.symbol_table.add(new_symbol);
+    }
+
+    frame.return_value_symbol =
+      ns.lookup(return_value_symbol_identifier).symbol_expr();
+  }
+
   const framet &p_frame = state.call_stack().previous_frame();
   for(const auto &pair : p_frame.loop_iterations)
   {
@@ -405,14 +427,33 @@ static void pop_frame(
 /// do function call by inlining
 void goto_symext::symex_end_of_function(statet &state)
 {
+  PRECONDITION(!state.call_stack().empty());
+
   const bool hidden = state.call_stack().top().hidden_function;
 
   // first record the return
   target.function_return(
     state.guard.as_expr(), state.source.function_id, state.source, hidden);
 
-  // then get rid of the frame
+  // before we drop the frame, remember the call LHS
+  // and the return value symbol, if any
+  auto call_lhs = state.call_stack().top().call_lhs;
+  auto return_value_symbol = state.call_stack().top().return_value_symbol;
+
+  // now get rid of the frame
   pop_frame(state, path_storage, symex_config.doing_path_exploration);
+
+  // after dropping the frame, assign the return value, if any
+  if(state.reachable && call_lhs.is_not_nil())
+  {
+    DATA_INVARIANT(
+      return_value_symbol.has_value(),
+      "must have return value symbol when assigning call lhs");
+    // the type of the call lhs and the return type might not match
+    auto casted_return_value = typecast_exprt::conditional_cast(
+      return_value_symbol.value(), call_lhs.type());
+    symex_assign(state, call_lhs, casted_return_value);
+  }
 }
 
 /// Preserves locality of parameters of a given function by applying L1

src/goto-symex/symex_main.cpp

@@ -661,8 +661,9 @@ void goto_symext::execute_next_instruction(
     break;
 
   case SET_RETURN_VALUE:
-    // This case should have been removed by return-value removal
-    UNREACHABLE;
+    if(state.reachable)
+      symex_set_return_value(state, instruction.return_value());
+    symex_transition(state);
     break;
 
   case ASSIGN:

src/goto-symex/symex_set_return_value.cpp

@@ -0,0 +1,26 @@
+/*******************************************************************\
+
+Module: Symbolic Execution of ANSI-C
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// Symbolic Execution of ANSI-C
+
+#include "goto_symex.h"
+
+void goto_symext::symex_set_return_value(
+  statet &state,
+  const exprt &return_value)
+{
+  // we must be inside a function that was called
+  PRECONDITION(!state.call_stack().empty());
+
+  framet &frame = state.call_stack().top();
+  if(frame.return_value_symbol.has_value())
+  {
+    symex_assign(state, frame.return_value_symbol.value(), return_value);
+  }
+}