Merge pull request #6250 from diffblue/goto_program_return_output

kroening · web-flow · commit 9509685a3b7b · 2021-07-27T16:28:52.000+01:00
rename RETURN -&gt; SET_RETURN_VALUE
diff --git a/jbmc/src/java_bytecode/replace_java_nondet.cpp b/jbmc/src/java_bytecode/replace_java_nondet.cpp
@@ -160,7 +160,7 @@ static bool is_return_with_variable(
   const goto_programt::instructiont &instr,
   const irep_idt &identifier)
 {
-  if(!instr.is_return())
+  if(!instr.is_set_return_value())
   {
     return false;
   }
@@ -271,7 +271,7 @@ static goto_programt::targett check_and_replace_target(
       instr.turn_into_skip();
     });
 
-  if(target_instruction->is_return())
+  if(target_instruction->is_set_return_value())
   {
     const auto &nondet_var = target_instruction->return_value();
 
diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
@@ -45,7 +45,7 @@ void validate_nondet_method_removed(
       }
     }
 
-    if(inst.is_return())
+    if(inst.is_set_return_value())
     {
       const auto &return_value = inst.return_value();
       if(return_value.id() == ID_side_effect)
@@ -94,7 +94,7 @@ void validate_nondets_converted(
     exprt target_expression =
       (inst.is_assign()
          ? inst.get_assign().rhs()
-         : inst.is_return() ? inst.return_value() : inst.get_code());
+         : inst.is_set_return_value() ? inst.return_value() : inst.get_code());
 
     if(
       const auto side_effect =
diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
@@ -540,8 +540,8 @@ void custom_bitvector_domaint::transform(
   case THROW:
     DATA_INVARIANT(false, "Exceptions must be removed before analysis");
     break;
-  case RETURN:
-    DATA_INVARIANT(false, "Returns must be removed before analysis");
+  case SET_RETURN_VALUE:
+    DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
     break;
   case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
   case ATOMIC_END:   // Ignoring is a valid over-approximation
diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp
@@ -255,8 +255,8 @@ void escape_domaint::transform(
   case THROW:
     DATA_INVARIANT(false, "Exceptions must be removed before analysis");
     break;
-  case RETURN:
-    DATA_INVARIANT(false, "Returns must be removed before analysis");
+  case SET_RETURN_VALUE:
+    DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
     break;
   case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
   case ATOMIC_END:   // Ignoring is a valid over-approximation
diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp
@@ -134,8 +134,8 @@ void global_may_alias_domaint::transform(
   case THROW:
     DATA_INVARIANT(false, "Exceptions must be removed before analysis");
     break;
-  case RETURN:
-    DATA_INVARIANT(false, "Returns must be removed before analysis");
+  case SET_RETURN_VALUE:
+    DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
     break;
   case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
   case ATOMIC_END:   // Ignoring is a valid over-approximation
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
@@ -2032,7 +2032,7 @@ void goto_checkt::goto_check(
       // the call might invalidate any assertion
       assertions.clear();
     }
-    else if(i.is_return())
+    else if(i.is_set_return_value())
     {
       check(i.return_value());
       // the return value invalidate any assertion
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
@@ -771,7 +771,7 @@ void goto_rw(
       target->get_condition());
     break;
 
-  case RETURN:
+  case SET_RETURN_VALUE:
     rw_set.get_objects_rec(
       function, target, rw_range_sett::get_modet::READ, target->return_value());
     break;
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
@@ -115,8 +115,8 @@ void interval_domaint::transform(
   case THROW:
     DATA_INVARIANT(false, "Exceptions must be removed before analysis");
     break;
-  case RETURN:
-    DATA_INVARIANT(false, "Returns must be removed before analysis");
+  case SET_RETURN_VALUE:
+    DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
     break;
   case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
   case ATOMIC_END:   // Ignoring is a valid over-approximation
diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp
@@ -50,11 +50,11 @@ void invariant_set_domaint::transform(
     }
     break;
 
-  case RETURN:
-    // ignore
-    break;
+    case SET_RETURN_VALUE:
+      // ignore
+      break;
 
-  case ASSIGN:
+    case ASSIGN:
     {
       const code_assignt &assignment = from_l->get_assign();
       invariant_set.assignment(assignment.lhs(), assignment.rhs());
diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
@@ -307,9 +307,9 @@ void local_bitvector_analysist::build()
       DATA_INVARIANT(false, "Exceptions must be removed before analysis");
       break;
 #endif
-    case RETURN:
+    case SET_RETURN_VALUE:
 #if 0
-      DATA_INVARIANT(false, "Returns must be removed before analysis");
+      DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
       break;
 #endif
     case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
diff --git a/src/analyses/local_cfg.cpp b/src/analyses/local_cfg.cpp
@@ -61,7 +61,7 @@ void local_cfgt::build(const goto_programt &goto_program)
       break; // no successor
 
     case CATCH:
-    case RETURN:
+    case SET_RETURN_VALUE:
     case ATOMIC_BEGIN:
     case ATOMIC_END:
     case LOCATION:
diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
@@ -423,9 +423,9 @@ void local_may_aliast::build(const goto_functiont &goto_function)
     case THROW:
       DATA_INVARIANT(false, "Exceptions must be removed before analysis");
       break;
-    case RETURN:
+    case SET_RETURN_VALUE:
 #if 0
-      DATA_INVARIANT(false, "Returns must be removed before analysis");
+      DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
 #endif
       break;
     case GOTO:         // Ignoring the guard is a valid over-approximation
diff --git a/src/analyses/local_safe_pointers.cpp b/src/analyses/local_safe_pointers.cpp
@@ -116,7 +116,7 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
     case ASSERT:
     case SKIP:
     case LOCATION:
-    case RETURN:
+    case SET_RETURN_VALUE:
     case THROW:
     case CATCH:
     case END_FUNCTION:
diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp
@@ -132,7 +132,7 @@ void uncaught_exceptions_domaint::transform(
   case DEAD:   // Safe to ignore in this context
   case ASSIGN: // Safe to ignore in this context
     break;
-  case RETURN:
+  case SET_RETURN_VALUE:
 #if 0
     DATA_INVARIANT(false, "Returns must be removed before analysis");
 #endif
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp
@@ -140,8 +140,8 @@ void variable_sensitivity_domaint::transform(
     // Can ignore
     break;
 
-  case RETURN:
-    throw "return instructions should be removed first";
+  case SET_RETURN_VALUE:
+    throw "the SET_RETURN_VALUE instructions should be removed first";
 
   case START_THREAD:
   case END_THREAD:
diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp
@@ -155,10 +155,9 @@ void dott::write_dot_subgraph(
         function_calls.push_back(
           std::pair<std::string, exprt>(ss.str(), function_call.function()));
       }
-      else if(it->is_assign() ||
-              it->is_decl() ||
-              it->is_return() ||
-              it->is_other())
+      else if(
+        it->is_assign() || it->is_decl() || it->is_set_return_value() ||
+        it->is_other())
       {
         std::string t = from_expr(ns, function_id, it->get_code());
         while(t[ t.size()-1 ]=='\n')
diff --git a/src/goto-instrument/function.cpp b/src/goto-instrument/function.cpp
@@ -125,7 +125,7 @@ void function_exit(
 
     Forall_goto_program_instructions(i_it, body)
     {
-      if(i_it->is_return())
+      if(i_it->is_set_return_value())
       {
         goto_programt::instructiont call = goto_programt::make_function_call(
           function_to_call(goto_model.symbol_table, id, gf_entry.first));
@@ -142,17 +142,17 @@ void function_exit(
     assert(last->is_end_function());
 
     // is there already a return?
-    bool has_return=false;
+    bool has_set_return_value = false;
 
     if(last!=body.instructions.begin())
     {
       goto_programt::targett before_last=last;
       --before_last;
-      if(before_last->is_return())
-        has_return=true;
+      if(before_last->is_set_return_value())
+        has_set_return_value = true;
     }
 
-    if(!has_return)
+    if(!has_set_return_value)
     {
       goto_programt::instructiont call = goto_programt::make_function_call(
         function_to_call(goto_model.symbol_table, id, gf_entry.first));
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
@@ -180,8 +180,8 @@ goto_programt::const_targett goto_program2codet::convert_instruction(
     case ASSIGN:
       return convert_assign(target, upper_bound, dest);
 
-    case RETURN:
-      return convert_return(target, upper_bound, dest);
+    case SET_RETURN_VALUE:
+      return convert_set_return_value(target, upper_bound, dest);
 
     case DECL:
       return convert_decl(target, upper_bound, dest);
@@ -410,7 +410,7 @@ void goto_program2codet::convert_assign_rec(
     dest.add(assign);
 }
 
-goto_programt::const_targett goto_program2codet::convert_return(
+goto_programt::const_targett goto_program2codet::convert_set_return_value(
   goto_programt::const_targett target,
   goto_programt::const_targett upper_bound,
   code_blockt &dest)
diff --git a/src/goto-instrument/goto_program2code.h b/src/goto-instrument/goto_program2code.h
@@ -141,7 +141,7 @@ class goto_program2codet
 
   void convert_assign_rec(const code_assignt &assign, code_blockt &dest);
 
-  goto_programt::const_targett convert_return(
+  goto_programt::const_targett convert_set_return_value(
     goto_programt::const_targett target,
     goto_programt::const_targett upper_bound,
     code_blockt &dest);
diff --git a/src/goto-instrument/points_to.cpp b/src/goto-instrument/points_to.cpp
@@ -58,7 +58,7 @@ bool points_tot::transform(const cfgt::nodet &e)
 
   switch(instruction.type)
   {
-  case RETURN:
+  case SET_RETURN_VALUE:
     // TODO
     break;
 
diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp
@@ -260,7 +260,7 @@ void instrumentert::cfg_visitort::visit_cfg_function(
       ); // NOLINT(whitespace/parens)
     }
 #ifdef CONTEXT_INSENSITIVE
-    else if(instruction.is_return())
+    else if(instruction.is_set_return_value())
     {
       visit_cfg_propagate(i_it);
       add_all_pos(it, out_nodes[function_id], in_pos[i_it]);
@@ -1227,13 +1227,10 @@ void inline instrumentert::add_instr_to_interleaving(
   goto_programt::instructionst::iterator it,
   goto_programt &interleaving)
 {
-  if(it->is_return() ||
-     it->is_throw() ||
-     it->is_catch() ||
-     it->is_skip() ||
-     it->is_dead() ||
-     it->is_start_thread() ||
-     it->is_end_thread())
+  if(
+    it->is_set_return_value() || it->is_throw() || it->is_catch() ||
+    it->is_skip() || it->is_dead() || it->is_start_thread() ||
+    it->is_end_thread())
     return;
 
   if(it->is_atomic_begin() ||
diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h
@@ -507,7 +507,7 @@ void cfg_baset<T, P, I>::compute_edges(
   case ASSIGN:
   case ASSERT:
   case OTHER:
-  case RETURN:
+  case SET_RETURN_VALUE:
   case SKIP:
   case LOCATION:
   case ATOMIC_BEGIN:
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
@@ -119,7 +119,7 @@ void goto_convert_functionst::add_return(
       }
 
       // return?
-      if(last_instruction->is_return())
+      if(last_instruction->is_set_return_value())
         return;
 
       // advance if it's a 'dead' without branch target
diff --git a/src/goto-programs/goto_functions.cpp b/src/goto-programs/goto_functions.cpp
@@ -138,7 +138,7 @@ void goto_functionst::validate(const namespacet &ns, const validation_modet vm)
       {
         DATA_CHECK(
           vm,
-          !instruction.is_return(),
+          !instruction.is_set_return_value(),
           "void function should not return a value");
       }
     }
diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp
@@ -155,7 +155,7 @@ void goto_inlinet::replace_return(
       it!=dest.instructions.end();
       it++)
   {
-    if(it->is_return())
+    if(it->is_set_return_value())
     {
       if(lhs.is_not_nil())
       {
diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
diff --git a/src/goto-programs/validate_goto_model.cpp b/src/goto-programs/validate_goto_model.cpp
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp
diff --git a/src/pointer-analysis/value_set_domain.h b/src/pointer-analysis/value_set_domain.h
diff --git a/src/pointer-analysis/value_set_domain_fi.cpp b/src/pointer-analysis/value_set_domain_fi.cpp
diff --git a/src/solvers/solver_hardness.cpp b/src/solvers/solver_hardness.cpp

Original file line number	Diff line number	Diff line change
`@@ -160,7 +160,7 @@ static bool is_return_with_variable(`
`160`	`160`	`const goto_programt::instructiont &instr,`
`161`	`161`	`const irep_idt &identifier)`
`162`	`162`	`{`
`163`		`- if(!instr.is_return())`
	`163`	`+ if(!instr.is_set_return_value())`
`164`	`164`	`{`
`165`	`165`	`return false;`
`166`	`166`	`}`
`@@ -271,7 +271,7 @@ static goto_programt::targett check_and_replace_target(`
`271`	`271`	`instr.turn_into_skip();`
`272`	`272`	`});`
`273`	`273`
`274`		`- if(target_instruction->is_return())`
	`274`	`+ if(target_instruction->is_set_return_value())`
`275`	`275`	`{`
`276`	`276`	`const auto &nondet_var = target_instruction->return_value();`
`277`	`277`
Original file line number	Diff line number	Diff line change
`@@ -45,7 +45,7 @@ void validate_nondet_method_removed(`
`45`	`45`	`}`
`46`	`46`	`}`
`47`	`47`
`48`		`- if(inst.is_return())`
	`48`	`+ if(inst.is_set_return_value())`
`49`	`49`	`{`
`50`	`50`	`const auto &return_value = inst.return_value();`
`51`	`51`	`if(return_value.id() == ID_side_effect)`
`@@ -94,7 +94,7 @@ void validate_nondets_converted(`
`94`	`94`	`exprt target_expression =`
`95`	`95`	`(inst.is_assign()`
`96`	`96`	`? inst.get_assign().rhs()`
`97`		`- : inst.is_return() ? inst.return_value() : inst.get_code());`
	`97`	`+ : inst.is_set_return_value() ? inst.return_value() : inst.get_code());`
`98`	`98`
`99`	`99`	`if(`
`100`	`100`	`const auto side_effect =`
Original file line number	Diff line number	Diff line change
`@@ -2032,7 +2032,7 @@ void goto_checkt::goto_check(`
`2032`	`2032`	`// the call might invalidate any assertion`
`2033`	`2033`	`assertions.clear();`
`2034`	`2034`	`}`
`2035`		`- else if(i.is_return())`
	`2035`	`+ else if(i.is_set_return_value())`
`2036`	`2036`	`{`
`2037`	`2037`	`check(i.return_value());`
`2038`	`2038`	`// the return value invalidate any assertion`
Original file line number	Diff line number	Diff line change
`@@ -50,11 +50,11 @@ void invariant_set_domaint::transform(`
`50`	`50`	`}`
`51`	`51`	`break;`
`52`	`52`
`53`		`- case RETURN:`
`54`		`- // ignore`
`55`		`- break;`
	`53`	`+ case SET_RETURN_VALUE:`
	`54`	`+ // ignore`
	`55`	`+ break;`
`56`	`56`
`57`		`- case ASSIGN:`
	`57`	`+ case ASSIGN:`
`58`	`58`	`{`
`59`	`59`	`const code_assignt &assignment = from_l->get_assign();`
`60`	`60`	`invariant_set.assignment(assignment.lhs(), assignment.rhs());`