Merge pull request #5863 from diffblue/goto_instruction_return

introduce instructiont::return_value()

Author: kroening

jbmc/src/java_bytecode/replace_java_nondet.cpp

@@ -165,7 +165,7 @@ static bool is_return_with_variable(
   {
     return false;
   }
-  const auto &rhs = to_code_return(instr.code).return_value();
+  const auto &rhs = instr.return_value();
   return is_symbol_with_id(rhs, identifier) ||
          is_typecast_with_id(rhs, identifier);
 }
@@ -276,8 +276,7 @@ static goto_programt::targett check_and_replace_target(
 
   if(target_instruction->is_return())
   {
-    const auto &nondet_var =
-      to_code_return(target_instruction->code).return_value();
+    const auto &nondet_var = target_instruction->return_value();
 
     side_effect_expr_nondett inserted_expr(
       nondet_var.type(), target_instruction->source_location);

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

@@ -54,11 +54,10 @@ void validate_nondet_method_removed(
 
     if(inst.is_return())
     {
-      const code_returnt &ret_expr = to_code_return(inst.code);
-      if(ret_expr.return_value().id() == ID_side_effect)
+      const auto &return_value = inst.return_value();
+      if(return_value.id() == ID_side_effect)
       {
-        const side_effect_exprt &see =
-          to_side_effect_expr(ret_expr.return_value());
+        const side_effect_exprt &see = to_side_effect_expr(return_value);
         if(see.get_statement() == ID_nondet)
         {
           replacement_nondet_exists = true;

src/analyses/goto_check.cpp

@@ -1998,22 +1998,18 @@ void goto_checkt::goto_check(
     }
     else if(i.is_return())
     {
-      if(i.code.operands().size()==1)
+      check(i.return_value());
+      // the return value invalidate any assertion
+      invalidate(i.return_value());
+
+      if(has_subexpr(i.return_value(), [](const exprt &expr) {
+           return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
+         }))
       {
-        const code_returnt &code_return = to_code_return(i.code);
-        check(code_return.return_value());
-        // the return value invalidate any assertion
-        invalidate(code_return.return_value());
-
-        if(has_subexpr(code_return.return_value(), [](const exprt &expr) {
-             return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
-           }))
-        {
-          exprt &return_value = to_code_return(i.code).return_value();
-          auto rw_ok_cond = rw_ok_check(return_value);
-          if(rw_ok_cond.has_value())
-            return_value = *rw_ok_cond;
-        }
+        exprt &return_value = i.return_value();
+        auto rw_ok_cond = rw_ok_check(return_value);
+        if(rw_ok_cond.has_value())
+          return_value = *rw_ok_cond;
       }
     }
     else if(i.is_throw())

src/analyses/goto_rw.cpp

@@ -775,16 +775,8 @@ void goto_rw(
     break;
 
   case RETURN:
-    {
-      const code_returnt &code_return=
-        to_code_return(target->code);
-      if(code_return.has_return_value())
-        rw_set.get_objects_rec(
-          function,
-          target,
-          rw_range_sett::get_modet::READ,
-          code_return.return_value());
-    }
+    rw_set.get_objects_rec(
+      function, target, rw_range_sett::get_modet::READ, target->return_value());
     break;
 
   case OTHER:

src/goto-instrument/goto_program2code.cpp

@@ -418,14 +418,12 @@ goto_programt::const_targett goto_program2codet::convert_return(
   goto_programt::const_targett upper_bound,
   code_blockt &dest)
 {
-  const code_returnt &ret = target->get_return();
-
   // add return instruction unless original code was missing a return
-  if(!ret.has_return_value() ||
-     ret.return_value().id()!=ID_side_effect ||
-     to_side_effect_expr(ret.return_value()).get_statement()!=ID_nondet)
+  if(
+    target->return_value().id() != ID_side_effect ||
+    to_side_effect_expr(target->return_value()).get_statement() != ID_nondet)
   {
-    dest.add(ret);
+    dest.add(code_returnt{target->return_value()});
   }
 
   // all v3 (or later) goto programs have an explicit GOTO after return

src/goto-programs/goto_inline_class.cpp

@@ -165,31 +165,20 @@ void goto_inlinet::replace_return(
   {
     if(it->is_return())
     {
-      const auto &code_return = it->get_return();
-
       if(lhs.is_not_nil())
       {
-        if(!code_return.has_return_value())
-        {
-          log.warning().source_location = it->code.find_source_location();
-          log.warning() << "return expects one operand!\n"
-                        << it->code.pretty() << messaget::eom;
-          continue;
-        }
-
         // a typecast may be necessary if the declared return type at the call
         // site differs from the defined return type
         it->code = code_assignt(
           lhs,
-          typecast_exprt::conditional_cast(
-            code_return.return_value(), lhs.type()));
+          typecast_exprt::conditional_cast(it->return_value(), lhs.type()));
         it->type=ASSIGN;
 
         it++;
       }
-      else if(code_return.has_return_value())
+      else
       {
-        it->code = code_expressiont(code_return.return_value());
+        it->code = code_expressiont(it->return_value());
         it->type=OTHER;
         it++;
       }

src/goto-programs/goto_program.cpp

@@ -285,8 +285,7 @@ std::list<exprt> expressions_read(
     break;
 
   case RETURN:
-    if(instruction.get_return().return_value().is_not_nil())
-      dest.push_back(instruction.get_return().return_value());
+    dest.push_back(instruction.return_value());
     break;
 
   case FUNCTION_CALL:
@@ -928,13 +927,9 @@ void goto_programt::instructiont::transform(
 
   case RETURN:
   {
-    auto new_return_value = f(get_return().return_value());
+    auto new_return_value = f(return_value());
     if(new_return_value.has_value())
-    {
-      auto new_return = get_return();
-      new_return.return_value() = *new_return_value;
-      set_return(new_return);
-    }
+      return_value() = *new_return_value;
   }
   break;
 
@@ -1037,7 +1032,7 @@ void goto_programt::instructiont::apply(
     break;
 
   case RETURN:
-    f(get_return().return_value());
+    f(return_value());
     break;
 
   case ASSIGN:

src/goto-programs/goto_program.h

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <sstream>
 #include <string>
 
+#include <util/deprecate.h>
 #include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/source_location.h>
@@ -232,13 +233,29 @@ class goto_programt
     }
 
     /// Get the return statement for READ
+    DEPRECATED(SINCE(2021, 2, 24, "Use return_value instead"))
     const code_returnt &get_return() const
     {
       PRECONDITION(is_return());
       return to_code_return(code);
     }
 
+    /// Get the return value of a RETURN instruction
+    const exprt &return_value() const
+    {
+      PRECONDITION(is_return());
+      return to_code_return(code).return_value();
+    }
+
+    /// Get the return value of a RETURN instruction
+    exprt &return_value()
+    {
+      PRECONDITION(is_return());
+      return to_code_return(code).return_value();
+    }
+
     /// Set the return statement for READ
+    DEPRECATED(SINCE(2021, 2, 24, "Use return_value instead"))
     void set_return(code_returnt c)
     {
       PRECONDITION(is_return());

src/goto-programs/interpreter.cpp

@@ -300,11 +300,10 @@ void interpretert::step()
     if(call_stack.empty())
       throw "RETURN without call"; // NOLINT(readability/throw)
 
-    if(pc->code.operands().size()==1 &&
-       call_stack.top().return_value_address!=0)
+    if(call_stack.top().return_value_address != 0)
     {
       mp_vectort rhs;
-      evaluate(pc->code.op0(), rhs);
+      evaluate(pc->return_value(), rhs);
       assign(call_stack.top().return_value_address, rhs);
     }
 

src/pointer-analysis/goto_program_dereference.cpp

@@ -228,13 +228,7 @@ void goto_program_dereferencet::dereference_instruction(
   }
   else if(i.is_return())
   {
-    auto r = i.get_return();
-
-    if(r.return_value().is_not_nil())
-    {
-      dereference_expr(r.return_value(), checks_only);
-      i.set_return(r);
-    }
+    dereference_expr(i.return_value(), checks_only);
   }
   else if(i.is_other())
   {