Merge pull request #6403 from diffblue/code_frontend_returnt

kroening · web-flow · commit 8dfeb1afae7c · 2021-10-21T19:17:02.000+01:00
Introduce code_frontend_returnt
diff --git a/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp b/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp
@@ -75,7 +75,7 @@ codet create_array_with_type_body(
   code_blockt code_block;
 
   // Declare new_array temporary:
-  code_block.add(code_declt(new_array_symbol_expr));
+  code_block.add(code_frontend_declt(new_array_symbol_expr));
 
   // new_array = new Object[length];
   side_effect_exprt new_array_expr{
@@ -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
diff --git a/src/util/std_code.h b/src/util/std_code.h
diff --git a/src/util/std_code_base.h b/src/util/std_code_base.h
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
`@@ -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`
Original file line number	Diff line number	Diff line change
`@@ -637,7 +637,7 @@ void jsil_typecheckt::typecheck_code(codet &code)`
`637`	`637`	`if(statement==ID_function_call)`
`638`	`638`	`typecheck_function_call(to_code_function_call(code));`
`639`	`639`	`else if(statement==ID_return)`
`640`		`- typecheck_return(to_code_return(code));`
	`640`	`+ typecheck_return(to_code_frontend_return(code));`
`641`	`641`	`else if(statement==ID_expression)`
`642`	`642`	`{`
`643`	`643`	`if(code.operands().size()!=1)`
`@@ -678,7 +678,7 @@ void jsil_typecheckt::typecheck_code(codet &code)`
`678`	`678`	`}`
`679`	`679`	`}`
`680`	`680`
`681`		`-void jsil_typecheckt::typecheck_return(code_returnt &code)`
	`681`	`+void jsil_typecheckt::typecheck_return(code_frontend_returnt &code)`
`682`	`682`	`{`
`683`	`683`	`if(code.has_return_value())`
`684`	`684`	`typecheck_expr(code.return_value());`
Original file line number	Diff line number	Diff line change
`@@ -1582,12 +1582,9 @@ void value_sett::apply_code_rec(`
`1582`	`1582`	`{`
`1583`	`1583`	`const code_returnt &code_return = to_code_return(code);`
`1584`	`1584`	`// this is turned into an assignment`
`1585`		`- if(code_return.has_return_value())`
`1586`		`- {`
`1587`		`- symbol_exprt lhs(`
`1588`		`- "value_set::return_value", code_return.return_value().type());`
`1589`		`- assign(lhs, code_return.return_value(), ns, false, false);`
`1590`		`- }`
	`1585`	`+ symbol_exprt lhs(`
	`1586`	`+ "value_set::return_value", code_return.return_value().type());`
	`1587`	`+ assign(lhs, code_return.return_value(), ns, false, false);`
`1591`	`1588`	`}`
`1592`	`1589`	`else if(statement==ID_array_set)`
`1593`	`1590`	`{`
Original file line number	Diff line number	Diff line change
`@@ -1378,12 +1378,9 @@ void value_set_fit::apply_code(const codet &code, const namespacet &ns)`
`1378`	`1378`	`{`
`1379`	`1379`	`const code_returnt &code_return = to_code_return(code);`
`1380`	`1380`	`// this is turned into an assignment`
`1381`		`- if(code_return.has_return_value())`
`1382`		`- {`
`1383`		`- std::string rvs="value_set::return_value"+std::to_string(from_function);`
`1384`		`- symbol_exprt lhs(rvs, code_return.return_value().type());`
`1385`		`- assign(lhs, code_return.return_value(), ns);`
`1386`		`- }`
	`1381`	`+ std::string rvs = "value_set::return_value" + std::to_string(from_function);`
	`1382`	`+ symbol_exprt lhs(rvs, code_return.return_value().type());`
	`1383`	`+ assign(lhs, code_return.return_value(), ns);`
`1387`	`1384`	`}`
`1388`	`1385`	`else if(statement==ID_fence)`
`1389`	`1386`	`{`