introduce code_frontend_returnt

kroening · kroening · commit 47a327718d50 · 2021-10-20T19:54:59.000+01:00
This splits the classes that represent return statements in the frontends
and the return instructions in goto instructions.

They differ in semantics and in the invariants that they maintain.  The goto
instruction variant always has a return value.  The constructors for
creating that class without return value are removed.
diff --git a/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp b/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp
@@ -105,7 +105,7 @@ codet create_array_with_type_body(
     new_array_element_classid, old_array_element_classid));
 
   // return new_array
-  code_block.add(code_returnt(new_array_symbol_expr));
+  code_block.add(code_frontend_returnt(new_array_symbol_expr));
 
   return std::move(code_block);
 }
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1361,7 +1361,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
     else if(bytecode == BC_return)
     {
       PRECONDITION(op.empty() && results.empty());
-      c=code_returnt();
+      c = code_frontend_returnt();
     }
     else if(bytecode == patternt("?return"))
     {
@@ -1370,7 +1370,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
       PRECONDITION(op.size() == 1 && results.empty());
       const exprt r =
         typecast_exprt::conditional_cast(op[0], method_return_type);
-      c=code_returnt(r);
+      c = code_frontend_returnt(r);
     }
     else if(bytecode == patternt("?astore"))
     {
diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp
@@ -590,7 +590,7 @@ code_blockt get_thread_safe_clinit_wrapper_body(
       gen_clinit_eqexpr(
         clinit_thread_local_state_sym.symbol_expr(),
         clinit_statest::INIT_COMPLETE),
-      code_returnt());
+      code_frontend_returnt());
     function_body.add(std::move(conditional));
   }
 
@@ -651,7 +651,8 @@ code_blockt get_thread_safe_clinit_wrapper_body(
 
   // if(init_complete) return;
   {
-    code_ifthenelset conditional(init_complete.symbol_expr(), code_returnt());
+    code_ifthenelset conditional(
+      init_complete.symbol_expr(), code_frontend_returnt());
     function_body.add(std::move(conditional));
   }
 
@@ -696,7 +697,7 @@ code_blockt get_thread_safe_clinit_wrapper_body(
       gen_clinit_assign(
         clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE));
     function_body.add(atomic_end);
-    function_body.add(code_returnt());
+    function_body.add(code_frontend_returnt());
   }
 
   return function_body;
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
@@ -139,7 +139,7 @@ class c_typecheck_baset:
   virtual void typecheck_gcc_computed_goto(codet &code);
   virtual void typecheck_gcc_switch_case_range(code_gcc_switch_case_ranget &);
   virtual void typecheck_gcc_local_label(codet &code);
-  virtual void typecheck_return(code_returnt &code);
+  virtual void typecheck_return(code_frontend_returnt &);
   virtual void typecheck_switch(codet &code);
   virtual void typecheck_while(code_whilet &code);
   virtual void typecheck_dowhile(code_dowhilet &code);
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
@@ -68,7 +68,7 @@ void c_typecheck_baset::typecheck_code(codet &code)
   else if(statement==ID_continue)
     typecheck_continue(code);
   else if(statement==ID_return)
-    typecheck_return(to_code_return(code));
+    typecheck_return(to_code_frontend_return(code));
   else if(statement==ID_decl)
     typecheck_decl(code);
   else if(statement==ID_assign)
@@ -643,7 +643,7 @@ void c_typecheck_baset::typecheck_start_thread(codet &code)
   typecheck_code(to_code(code.op0()));
 }
 
-void c_typecheck_baset::typecheck_return(code_returnt &code)
+void c_typecheck_baset::typecheck_return(code_frontend_returnt &code)
 {
   if(code.has_return_value())
   {
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -2680,7 +2680,7 @@ std::string expr2ct::convert_code_return(
   std::string dest=indent_str(indent);
   dest+="return";
 
-  if(to_code_return(src).has_return_value())
+  if(to_code_frontend_return(src).has_return_value())
     dest+=" "+convert(src.op0());
 
   dest+=';';
diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp
@@ -688,8 +688,8 @@ void cpp_typecheckt::typecheck_compound_declarator(
         {
           expr_call.type()=to_code_type(component.type()).return_type();
 
-          func_symb.value = code_blockt{
-            {code_returnt(already_typechecked_exprt{std::move(expr_call)})}};
+          func_symb.value = code_blockt{{code_frontend_returnt(
+            already_typechecked_exprt{std::move(expr_call)})}};
         }
         else
         {
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
@@ -7350,7 +7350,7 @@ optionalt<codet> Parser::rStatement()
 
     lex.get_token(tk1);
 
-    code_returnt statement;
+    code_frontend_returnt statement;
     set_location(statement, tk1);
 
     if(lex.LookAhead(0)==';')
diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp
@@ -239,7 +239,7 @@ code_blockt build_null_pointer(const symbol_exprt &result_symbol)
   const null_pointer_exprt nullptr_expr{to_pointer_type(type_to_construct)};
   const code_assignt assign_null{dereference_exprt{result_symbol},
                                  nullptr_expr};
-  return code_blockt{{assign_null, code_returnt{}}};
+  return code_blockt{{assign_null, code_frontend_returnt{}}};
 }
 
 code_blockt recursive_initializationt::build_constructor_body(
@@ -688,7 +688,7 @@ code_blockt recursive_initializationt::build_pointer_constructor(
 
   null_pointer_exprt nullptr_expr{pointer_type(type.subtype())};
   const code_assignt assign_null{dereference_exprt{result}, nullptr_expr};
-  code_blockt null_and_return{{assign_null, code_returnt{}}};
+  code_blockt null_and_return{{assign_null, code_frontend_returnt{}}};
   body.add(code_ifthenelset{conjunction(should_not_recurse), null_and_return});
 
   const auto should_recurse_nondet =
@@ -1034,7 +1034,7 @@ code_blockt recursive_initializationt::build_function_pointer_constructor(
       auto const condition = equal_exprt{
         function_pointer_selector,
         from_integer(function_pointer_index, function_pointer_selector.type())};
-      auto const then = code_blockt{{assign, code_returnt{}}};
+      auto const then = code_blockt{{assign, code_frontend_returnt{}}};
       body.add(code_ifthenelset{condition, then});
     }
     else
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
@@ -1074,7 +1074,7 @@ void code_contractst::add_contract_check(
   replace_symbolt common_replace;
 
   // decl ret
-  code_returnt return_stmt;
+  optionalt<code_returnt> return_stmt;
   if(code_type.return_type() != empty_typet())
   {
     symbol_exprt r = new_tmp_symbol(
@@ -1178,7 +1178,8 @@ void code_contractst::add_contract_check(
 
   if(code_type.return_type() != empty_typet())
   {
-    check.add(goto_programt::make_return(return_stmt, skip->source_location()));
+    check.add(
+      goto_programt::make_return(return_stmt.value(), skip->source_location()));
   }
 
   // prepend the new code to dest
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
@@ -470,7 +470,7 @@ void goto_convertt::convert(
   else if(statement==ID_break)
     convert_break(to_code_break(code), dest, mode);
   else if(statement==ID_return)
-    convert_return(to_code_return(code), dest, mode);
+    convert_return(to_code_frontend_return(code), dest, mode);
   else if(statement==ID_continue)
     convert_continue(to_code_continue(code), dest, mode);
   else if(statement==ID_goto)
@@ -1258,7 +1258,7 @@ void goto_convertt::convert_break(
 }
 
 void goto_convertt::convert_return(
-  const code_returnt &code,
+  const code_frontend_returnt &code,
   goto_programt &dest,
   const irep_idt &mode)
 {
@@ -1273,7 +1273,7 @@ void goto_convertt::convert_return(
     "return takes none or one operand",
     code.find_source_location());
 
-  code_returnt new_code(code);
+  code_frontend_returnt new_code(code);
 
   if(new_code.has_return_value())
   {
@@ -1297,7 +1297,8 @@ void goto_convertt::convert_return(
       new_code.find_source_location());
 
     // Now add a return node to set the return value.
-    dest.add(goto_programt::make_return(new_code, new_code.source_location()));
+    dest.add(goto_programt::make_return(
+      to_code_return(new_code), new_code.source_location()));
   }
   else
   {
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
@@ -267,7 +267,7 @@ class goto_convertt:public messaget
     goto_programt &dest,
     const irep_idt &mode);
   void convert_return(
-    const code_returnt &code,
+    const code_frontend_returnt &,
     goto_programt &dest,
     const irep_idt &mode);
   void convert_continue(
diff --git a/src/jsil/jsil_parse_tree.cpp b/src/jsil/jsil_parse_tree.cpp
@@ -66,7 +66,7 @@ void jsil_declarationt::to_symbol(symbolt &symbol) const
       static_cast<const codet&>(find(ID_value))));
 
   irept returns(find(ID_return));
-  code_returnt r(symbol_exprt::typeless(returns.get(ID_value)));
+  code_frontend_returnt r(symbol_exprt::typeless(returns.get(ID_value)));
 
   irept throws(find(ID_throw));
   side_effect_expr_throwt t(
diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp
@@ -637,7 +637,7 @@ void jsil_typecheckt::typecheck_code(codet &code)
   if(statement==ID_function_call)
     typecheck_function_call(to_code_function_call(code));
   else if(statement==ID_return)
-    typecheck_return(to_code_return(code));
+    typecheck_return(to_code_frontend_return(code));
   else if(statement==ID_expression)
   {
     if(code.operands().size()!=1)
@@ -678,7 +678,7 @@ void jsil_typecheckt::typecheck_code(codet &code)
   }
 }
 
-void jsil_typecheckt::typecheck_return(code_returnt &code)
+void jsil_typecheckt::typecheck_return(code_frontend_returnt &code)
 {
   if(code.has_return_value())
     typecheck_expr(code.return_value());
diff --git a/src/jsil/jsil_typecheck.h b/src/jsil/jsil_typecheck.h
@@ -20,7 +20,7 @@ Author: Michael Tautschnig, tautschn@amazon.com
 class code_assignt;
 class code_function_callt;
 class code_ifthenelset;
-class code_returnt;
+class code_frontend_returnt;
 class code_try_catcht;
 class codet;
 class message_handlert;
@@ -89,7 +89,7 @@ class jsil_typecheckt:public typecheckt
   void typecheck_expr_main(exprt &expr);
   void typecheck_code(codet &code);
   void typecheck_function_call(code_function_callt &function_call);
-  void typecheck_return(code_returnt &code);
+  void typecheck_return(code_frontend_returnt &);
   void typecheck_block(codet &code);
   void typecheck_ifthenelse(code_ifthenelset &code);
   void typecheck_assign(code_assignt &code);
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
@@ -1582,12 +1582,9 @@ void value_sett::apply_code_rec(
   {
     const code_returnt &code_return = to_code_return(code);
     // this is turned into an assignment
-    if(code_return.has_return_value())
-    {
-      symbol_exprt lhs(
-        "value_set::return_value", code_return.return_value().type());
-      assign(lhs, code_return.return_value(), ns, false, false);
-    }
+    symbol_exprt lhs(
+      "value_set::return_value", code_return.return_value().type());
+    assign(lhs, code_return.return_value(), ns, false, false);
   }
   else if(statement==ID_array_set)
   {
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
@@ -1378,12 +1378,9 @@ void value_set_fit::apply_code(const codet &code, const namespacet &ns)
   {
     const code_returnt &code_return = to_code_return(code);
     // this is turned into an assignment
-    if(code_return.has_return_value())
-    {
-      std::string rvs="value_set::return_value"+std::to_string(from_function);
-      symbol_exprt lhs(rvs, code_return.return_value().type());
-      assign(lhs, code_return.return_value(), ns);
-    }
+    std::string rvs = "value_set::return_value" + std::to_string(from_function);
+    symbol_exprt lhs(rvs, code_return.return_value().type());
+    assign(lhs, code_return.return_value(), ns);
   }
   else if(statement==ID_fence)
   {
diff --git a/src/util/goto_instruction_code.h b/src/util/goto_instruction_code.h
@@ -479,4 +479,61 @@ inline void validate_expr(const code_outputt &output)
   code_outputt::check(output);
 }
 
+/// \ref codet representation of a "return from a function" statement.
+class code_returnt : public codet
+{
+public:
+  explicit code_returnt(exprt _op) : codet(ID_return, {std::move(_op)})
+  {
+  }
+
+  const exprt &return_value() const
+  {
+    return op0();
+  }
+
+  exprt &return_value()
+  {
+    return op0();
+  }
+
+  static void check(
+    const codet &code,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");
+  }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
+};
+
+template <>
+inline bool can_cast_expr<code_returnt>(const exprt &base)
+{
+  return detail::can_cast_code_impl(base, ID_return);
+}
+
+inline void validate_expr(const code_returnt &x)
+{
+  code_returnt::check(x);
+}
+
+inline const code_returnt &to_code_return(const codet &code)
+{
+  PRECONDITION(code.get_statement() == ID_return);
+  code_returnt::check(code);
+  return static_cast<const code_returnt &>(code);
+}
+
+inline code_returnt &to_code_return(codet &code)
+{
+  PRECONDITION(code.get_statement() == ID_return);
+  code_returnt::check(code);
+  return static_cast<code_returnt &>(code);
+}
+
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_INSTRUCTION_CODE_H
diff --git a/src/util/std_code.h b/src/util/std_code.h
@@ -902,14 +902,14 @@ inline code_gotot &to_code_goto(codet &code)
 }
 
 /// \ref codet representation of a "return from a function" statement.
-class code_returnt:public codet
+class code_frontend_returnt : public codet
 {
 public:
-  code_returnt() : codet(ID_return, {nil_exprt()})
+  code_frontend_returnt() : codet(ID_return, {nil_exprt()})
   {
   }
 
-  explicit code_returnt(exprt _op) : codet(ID_return, {std::move(_op)})
+  explicit code_frontend_returnt(exprt _op) : codet(ID_return, {std::move(_op)})
   {
   }
 
@@ -942,28 +942,29 @@ class code_returnt:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
+template <>
+inline bool can_cast_expr<code_frontend_returnt>(const exprt &base)
 {
   return detail::can_cast_code_impl(base, ID_return);
 }
 
-inline void validate_expr(const code_returnt &x)
+inline void validate_expr(const code_frontend_returnt &x)
 {
-  code_returnt::check(x);
+  code_frontend_returnt::check(x);
 }
 
-inline const code_returnt &to_code_return(const codet &code)
+inline const code_frontend_returnt &to_code_frontend_return(const codet &code)
 {
   PRECONDITION(code.get_statement() == ID_return);
-  code_returnt::check(code);
-  return static_cast<const code_returnt &>(code);
+  code_frontend_returnt::check(code);
+  return static_cast<const code_frontend_returnt &>(code);
 }
 
-inline code_returnt &to_code_return(codet &code)
+inline code_frontend_returnt &to_code_frontend_return(codet &code)
 {
   PRECONDITION(code.get_statement() == ID_return);
-  code_returnt::check(code);
-  return static_cast<code_returnt &>(code);
+  code_frontend_returnt::check(code);
+  return static_cast<code_frontend_returnt &>(code);
 }
 
 /// \ref codet representation of a label for branch targets.
diff --git a/unit/goto-programs/goto_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp

Original file line number	Diff line number	Diff line change
`@@ -105,7 +105,7 @@ codet create_array_with_type_body(`
`105`	`105`	`new_array_element_classid, old_array_element_classid));`
`106`	`106`
`107`	`107`	`// return new_array`
`108`		`- code_block.add(code_returnt(new_array_symbol_expr));`
	`108`	`+ code_block.add(code_frontend_returnt(new_array_symbol_expr));`
`109`	`109`
`110`	`110`	`return std::move(code_block);`
`111`	`111`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1361,7 +1361,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)`
`1361`	`1361`	`else if(bytecode == BC_return)`
`1362`	`1362`	`{`
`1363`	`1363`	`PRECONDITION(op.empty() && results.empty());`
`1364`		`- c=code_returnt();`
	`1364`	`+ c = code_frontend_returnt();`
`1365`	`1365`	`}`
`1366`	`1366`	`else if(bytecode == patternt("?return"))`
`1367`	`1367`	`{`
`@@ -1370,7 +1370,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)`
`1370`	`1370`	`PRECONDITION(op.size() == 1 && results.empty());`
`1371`	`1371`	`const exprt r =`
`1372`	`1372`	`typecast_exprt::conditional_cast(op[0], method_return_type);`
`1373`		`- c=code_returnt(r);`
	`1373`	`+ c = code_frontend_returnt(r);`
`1374`	`1374`	`}`
`1375`	`1375`	`else if(bytecode == patternt("?astore"))`
`1376`	`1376`	`{`
Original file line number	Diff line number	Diff line change
`@@ -590,7 +590,7 @@ code_blockt get_thread_safe_clinit_wrapper_body(`
`590`	`590`	`gen_clinit_eqexpr(`
`591`	`591`	`clinit_thread_local_state_sym.symbol_expr(),`
`592`	`592`	`clinit_statest::INIT_COMPLETE),`
`593`		`- code_returnt());`
	`593`	`+ code_frontend_returnt());`
`594`	`594`	`function_body.add(std::move(conditional));`
`595`	`595`	`}`
`596`	`596`
`@@ -651,7 +651,8 @@ code_blockt get_thread_safe_clinit_wrapper_body(`
`651`	`651`
`652`	`652`	`// if(init_complete) return;`
`653`	`653`	`{`
`654`		`- code_ifthenelset conditional(init_complete.symbol_expr(), code_returnt());`
	`654`	`+ code_ifthenelset conditional(`
	`655`	`+ init_complete.symbol_expr(), code_frontend_returnt());`
`655`	`656`	`function_body.add(std::move(conditional));`
`656`	`657`	`}`
`657`	`658`
`@@ -696,7 +697,7 @@ code_blockt get_thread_safe_clinit_wrapper_body(`
`696`	`697`	`gen_clinit_assign(`
`697`	`698`	`clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE));`
`698`	`699`	`function_body.add(atomic_end);`
`699`		`- function_body.add(code_returnt());`
	`700`	`+ function_body.add(code_frontend_returnt());`
`700`	`701`	`}`
`701`	`702`
`702`	`703`	`return function_body;`
Original file line number	Diff line number	Diff line change
`@@ -68,7 +68,7 @@ void c_typecheck_baset::typecheck_code(codet &code)`
`68`	`68`	`else if(statement==ID_continue)`
`69`	`69`	`typecheck_continue(code);`
`70`	`70`	`else if(statement==ID_return)`
`71`		`- typecheck_return(to_code_return(code));`
	`71`	`+ typecheck_return(to_code_frontend_return(code));`
`72`	`72`	`else if(statement==ID_decl)`
`73`	`73`	`typecheck_decl(code);`
`74`	`74`	`else if(statement==ID_assign)`
`@@ -643,7 +643,7 @@ void c_typecheck_baset::typecheck_start_thread(codet &code)`
`643`	`643`	`typecheck_code(to_code(code.op0()));`
`644`	`644`	`}`
`645`	`645`
`646`		`-void c_typecheck_baset::typecheck_return(code_returnt &code)`
	`646`	`+void c_typecheck_baset::typecheck_return(code_frontend_returnt &code)`
`647`	`647`	`{`
`648`	`648`	`if(code.has_return_value())`
`649`	`649`	`{`
Original file line number	Diff line number	Diff line change
`@@ -688,8 +688,8 @@ void cpp_typecheckt::typecheck_compound_declarator(`
`688`	`688`	`{`
`689`	`689`	`expr_call.type()=to_code_type(component.type()).return_type();`
`690`	`690`
`691`		`- func_symb.value = code_blockt{`
`692`		`- {code_returnt(already_typechecked_exprt{std::move(expr_call)})}};`
	`691`	`+ func_symb.value = code_blockt{{code_frontend_returnt(`
	`692`	`+ already_typechecked_exprt{std::move(expr_call)})}};`
`693`	`693`	`}`
`694`	`694`	`else`
`695`	`695`	`{`
Original file line number	Diff line number	Diff line change
`@@ -1074,7 +1074,7 @@ void code_contractst::add_contract_check(`
`1074`	`1074`	`replace_symbolt common_replace;`
`1075`	`1075`
`1076`	`1076`	`// decl ret`
`1077`		`- code_returnt return_stmt;`
	`1077`	`+ optionalt<code_returnt> return_stmt;`
`1078`	`1078`	`if(code_type.return_type() != empty_typet())`
`1079`	`1079`	`{`
`1080`	`1080`	`symbol_exprt r = new_tmp_symbol(`
`@@ -1178,7 +1178,8 @@ void code_contractst::add_contract_check(`
`1178`	`1178`
`1179`	`1179`	`if(code_type.return_type() != empty_typet())`
`1180`	`1180`	`{`
`1181`		`- check.add(goto_programt::make_return(return_stmt, skip->source_location()));`
	`1181`	`+ check.add(`
	`1182`	`+ goto_programt::make_return(return_stmt.value(), skip->source_location()));`
`1182`	`1183`	`}`
`1183`	`1184`
`1184`	`1185`	`// prepend the new code to dest`