Merge pull request #3274 from tautschnig/precise_return_type

Use more specific return type instead of generic codet/exprt

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -991,7 +991,7 @@ static std::size_t get_bytecode_type_width(const typet &ty)
   return ty.get_size_t(ID_width);
 }
 
-codet java_bytecode_convert_methodt::convert_instructions(
+code_blockt java_bytecode_convert_methodt::convert_instructions(
   const methodt &method,
   const java_class_typet::java_lambda_method_handlest &lambda_method_handles)
 {
@@ -1913,7 +1913,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
   for(auto &block : root_block.statements())
     code.add(block);
 
-  return std::move(code);
+  return code;
 }
 
 codet java_bytecode_convert_methodt::convert_pop(
@@ -1932,7 +1932,7 @@ codet java_bytecode_convert_methodt::convert_pop(
   return c;
 }
 
-codet java_bytecode_convert_methodt::convert_switch(
+code_switcht java_bytecode_convert_methodt::convert_switch(
   java_bytecode_convert_methodt::address_mapt &address_map,
   const exprt::operandst &op,
   const java_bytecode_parse_treet::instructiont::argst &args,
@@ -1983,7 +1983,7 @@ codet java_bytecode_convert_methodt::convert_switch(
   }
 
   code_switch.body() = code_block;
-  return std::move(code_switch);
+  return code_switch;
 }
 
 codet java_bytecode_convert_methodt::convert_monitorenterexit(
@@ -2538,7 +2538,7 @@ void java_bytecode_convert_methodt::convert_new(
   results[0] = tmp;
 }
 
-codet java_bytecode_convert_methodt::convert_putstatic(
+code_blockt java_bytecode_convert_methodt::convert_putstatic(
   const source_locationt &location,
   const exprt &arg0,
   const exprt::operandst &op,
@@ -2567,10 +2567,10 @@ codet java_bytecode_convert_methodt::convert_putstatic(
     bytecode_write_typet::STATIC_FIELD,
     symbol_expr.get_identifier());
   block.add(code_assignt(symbol_expr, op[0]));
-  return std::move(block);
+  return block;
 }
 
-codet java_bytecode_convert_methodt::convert_putfield(
+code_blockt java_bytecode_convert_methodt::convert_putfield(
   const exprt &arg0,
   const exprt::operandst &op)
 {
@@ -2582,7 +2582,7 @@ codet java_bytecode_convert_methodt::convert_putfield(
     bytecode_write_typet::FIELD,
     arg0.get(ID_component_name));
   block.add(code_assignt(to_member(op[0], arg0), op[1]));
-  return std::move(block);
+  return block;
 }
 
 void java_bytecode_convert_methodt::convert_getstatic(
@@ -2699,7 +2699,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_ushr(
   return results;
 }
 
-codet java_bytecode_convert_methodt::convert_iinc(
+code_blockt java_bytecode_convert_methodt::convert_iinc(
   const exprt &arg0,
   const exprt &arg1,
   const source_locationt &location,
@@ -2723,10 +2723,10 @@ codet java_bytecode_convert_methodt::convert_iinc(
     plus_exprt(variable(arg0, 'i', address, CAST_AS_NEEDED), arg1_int_type));
   block.add(code_assign);
 
-  return std::move(block);
+  return block;
 }
 
-codet java_bytecode_convert_methodt::convert_ifnull(
+code_ifthenelset java_bytecode_convert_methodt::convert_ifnull(
   const java_bytecode_convert_methodt::address_mapt &address_map,
   const exprt::operandst &op,
   const mp_integer &number,
@@ -2741,10 +2741,10 @@ codet java_bytecode_convert_methodt::convert_ifnull(
   code_branch.then_case().add_source_location() =
     address_map.at(label_number).source->source_location;
   code_branch.add_source_location() = location;
-  return std::move(code_branch);
+  return code_branch;
 }
 
-codet java_bytecode_convert_methodt::convert_ifnonull(
+code_ifthenelset java_bytecode_convert_methodt::convert_ifnonull(
   const java_bytecode_convert_methodt::address_mapt &address_map,
   const exprt::operandst &op,
   const mp_integer &number,
@@ -2759,10 +2759,10 @@ codet java_bytecode_convert_methodt::convert_ifnonull(
   code_branch.then_case().add_source_location() =
     address_map.at(label_number).source->source_location;
   code_branch.add_source_location() = location;
-  return std::move(code_branch);
+  return code_branch;
 }
 
-codet java_bytecode_convert_methodt::convert_if(
+code_ifthenelset java_bytecode_convert_methodt::convert_if(
   const java_bytecode_convert_methodt::address_mapt &address_map,
   const exprt::operandst &op,
   const irep_idt &id,
@@ -2781,10 +2781,10 @@ codet java_bytecode_convert_methodt::convert_if(
   code_branch.then_case().add_source_location().set_function(method_id);
   code_branch.add_source_location() = location;
   code_branch.add_source_location().set_function(method_id);
-  return std::move(code_branch);
+  return code_branch;
 }
 
-codet java_bytecode_convert_methodt::convert_if_cmp(
+code_ifthenelset java_bytecode_convert_methodt::convert_if_cmp(
   const java_bytecode_convert_methodt::address_mapt &address_map,
   const irep_idt &statement,
   const exprt::operandst &op,
@@ -2810,7 +2810,7 @@ codet java_bytecode_convert_methodt::convert_if_cmp(
     address_map.at(label_number).source->source_location;
   code_branch.add_source_location() = location;
 
-  return std::move(code_branch);
+  return code_branch;
 }
 
 code_blockt java_bytecode_convert_methodt::convert_ret(
@@ -2865,7 +2865,7 @@ exprt java_bytecode_convert_methodt::convert_aload(
   return java_bytecode_promotion(element);
 }
 
-codet java_bytecode_convert_methodt::convert_store(
+code_blockt java_bytecode_convert_methodt::convert_store(
   const irep_idt &statement,
   const exprt &arg0,
   const exprt::operandst &op,
@@ -2890,10 +2890,10 @@ codet java_bytecode_convert_methodt::convert_store(
   code_assignt assign(var, toassign);
   assign.add_source_location() = location;
   block.add(assign);
-  return std::move(block);
+  return block;
 }
 
-codet java_bytecode_convert_methodt::convert_astore(
+code_blockt java_bytecode_convert_methodt::convert_astore(
   const irep_idt &statement,
   const exprt::operandst &op,
   const source_locationt &location)
@@ -2922,7 +2922,7 @@ codet java_bytecode_convert_methodt::convert_astore(
   code_assignt array_put(element, op[2]);
   array_put.add_source_location() = location;
   block.add(array_put);
-  return std::move(block);
+  return block;
 }
 
 optionalt<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -268,7 +268,7 @@ class java_bytecode_convert_methodt:public messaget
   // conversion
   void convert(const symbolt &class_symbol, const methodt &);
 
-  codet convert_instructions(
+  code_blockt convert_instructions(
     const methodt &,
     const java_class_typet::java_lambda_method_handlest &);
 
@@ -321,12 +321,12 @@ class java_bytecode_convert_methodt:public messaget
     const source_locationt &location,
     const exprt &arg0);
 
-  codet convert_astore(
+  code_blockt convert_astore(
     const irep_idt &statement,
     const exprt::operandst &op,
     const source_locationt &location);
 
-  codet convert_store(
+  code_blockt convert_store(
     const irep_idt &statement,
     const exprt &arg0,
     const exprt::operandst &op,
@@ -342,33 +342,33 @@ class java_bytecode_convert_methodt:public messaget
     const source_locationt &location,
     const method_offsett address);
 
-  codet convert_if_cmp(
+  code_ifthenelset convert_if_cmp(
     const java_bytecode_convert_methodt::address_mapt &address_map,
     const irep_idt &statement,
     const exprt::operandst &op,
     const mp_integer &number,
     const source_locationt &location) const;
 
-  codet convert_if(
+  code_ifthenelset convert_if(
     const java_bytecode_convert_methodt::address_mapt &address_map,
     const exprt::operandst &op,
     const irep_idt &id,
     const mp_integer &number,
     const source_locationt &location) const;
 
-  codet convert_ifnonull(
+  code_ifthenelset convert_ifnonull(
     const java_bytecode_convert_methodt::address_mapt &address_map,
     const exprt::operandst &op,
     const mp_integer &number,
     const source_locationt &location) const;
 
-  codet convert_ifnull(
+  code_ifthenelset convert_ifnull(
     const java_bytecode_convert_methodt::address_mapt &address_map,
     const exprt::operandst &op,
     const mp_integer &number,
     const source_locationt &location) const;
 
-  codet convert_iinc(
+  code_blockt convert_iinc(
     const exprt &arg0,
     const exprt &arg1,
     const source_locationt &location,
@@ -394,9 +394,9 @@ class java_bytecode_convert_methodt:public messaget
     codet &c,
     exprt::operandst &results);
 
-  codet convert_putfield(const exprt &arg0, const exprt::operandst &op);
+  code_blockt convert_putfield(const exprt &arg0, const exprt::operandst &op);
 
-  codet convert_putstatic(
+  code_blockt convert_putstatic(
     const source_locationt &location,
     const exprt &arg0,
     const exprt::operandst &op,
@@ -464,7 +464,7 @@ class java_bytecode_convert_methodt:public messaget
 
   void convert_dup2(exprt::operandst &op, exprt::operandst &results);
 
-  codet convert_switch(
+  code_switcht convert_switch(
     java_bytecode_convert_methodt::address_mapt &address_map,
     const exprt::operandst &op,
     const java_bytecode_parse_treet::instructiont::argst &args,

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -43,7 +43,7 @@ class java_bytecode_instrumentt:public messaget
   const bool throw_runtime_exceptions;
   message_handlert &message_handler;
 
-  codet throw_exception(
+  code_ifthenelset throw_exception(
     const exprt &cond,
     const source_locationt &original_loc,
     const irep_idt &exc_name);
@@ -61,7 +61,7 @@ class java_bytecode_instrumentt:public messaget
     const exprt &expr,
     const source_locationt &original_loc);
 
-  codet check_class_cast(
+  code_ifthenelset check_class_cast(
     const exprt &class1,
     const exprt &class2,
     const source_locationt &original_loc);
@@ -92,7 +92,7 @@ const std::vector<std::string> exception_needed_classes = {
 /// \param exc_name: the name of the exception to be thrown
 /// \return Returns the code initialising the throwing the
 /// exception
-codet java_bytecode_instrumentt::throw_exception(
+code_ifthenelset java_bytecode_instrumentt::throw_exception(
   const exprt &cond,
   const source_locationt &original_loc,
   const irep_idt &exc_name)
@@ -133,7 +133,7 @@ codet java_bytecode_instrumentt::throw_exception(
   if_code.cond()=cond;
   if_code.then_case() = code_blockt({assign_new, code_expressiont(throw_expr)});
 
-  return std::move(if_code);
+  return if_code;
 }
 
 
@@ -218,7 +218,7 @@ codet java_bytecode_instrumentt::check_array_access(
 /// \return Based on the value of the flag `throw_runtime_exceptions`,
 /// it returns code that either throws an ClassCastException or emits an
 /// assertion checking the subtype relation
-codet java_bytecode_instrumentt::check_class_cast(
+code_ifthenelset java_bytecode_instrumentt::check_class_cast(
   const exprt &class1,
   const exprt &class2,
   const source_locationt &original_loc)
@@ -255,7 +255,7 @@ codet java_bytecode_instrumentt::check_class_cast(
   notequal_exprt op_not_null(null_check_op, null_pointer_exprt(voidptr));
   conditional_check.cond()=std::move(op_not_null);
   conditional_check.then_case()=std::move(check_code);
-  return std::move(conditional_check);
+  return conditional_check;
 }
 
 /// Checks whether `expr` is null and throws NullPointerException/

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -445,7 +445,7 @@ static void create_clinit_wrapper_symbols(
 /// \param pointer_type_selector: used to choose concrete types for abstract-
 ///   typed globals and fields (only needed if nondet-static is true)
 /// \return the body of the static initializer wrapper
-codet get_thread_safe_clinit_wrapper_body(
+code_blockt get_thread_safe_clinit_wrapper_body(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   const bool nondet_static,
@@ -626,7 +626,7 @@ codet get_thread_safe_clinit_wrapper_body(
     function_body.add(code_returnt());
   }
 
-  return std::move(function_body);
+  return function_body;
 }
 
 /// Produces the static initializer wrapper body for the given function.
@@ -641,7 +641,7 @@ codet get_thread_safe_clinit_wrapper_body(
 /// \param pointer_type_selector: used to choose concrete types for abstract-
 ///   typed globals and fields (only needed if nondet-static is true)
 /// \return the body of the static initializer wrapper
-codet get_clinit_wrapper_body(
+code_ifthenelset get_clinit_wrapper_body(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   const bool nondet_static,
@@ -701,7 +701,7 @@ codet get_clinit_wrapper_body(
 
   wrapper_body.then_case() = init_body;
 
-  return std::move(wrapper_body);
+  return wrapper_body;
 }
 
 
@@ -841,7 +841,7 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
 /// \param pointer_type_selector: used to choose concrete types for abstract-
 ///   typed globals and fields.
 /// \return synthetic static initializer body.
-codet stub_global_initializer_factoryt::get_stub_initializer_body(
+code_blockt stub_global_initializer_factoryt::get_stub_initializer_body(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   const object_factory_parameterst &object_factory_parameters,
@@ -890,5 +890,5 @@ codet stub_global_initializer_factoryt::get_stub_initializer_body(
       update_in_placet::NO_UPDATE_IN_PLACE);
   }
 
-  return std::move(static_init_body);
+  return static_init_body;
 }

jbmc/src/java_bytecode/java_static_initializers.h

@@ -27,14 +27,14 @@ void create_static_initializer_wrappers(
   synthetic_methods_mapt &synthetic_methods,
   const bool thread_safe);
 
-codet get_thread_safe_clinit_wrapper_body(
+code_blockt get_thread_safe_clinit_wrapper_body(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   const bool nondet_static,
   const object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector);
 
-codet get_clinit_wrapper_body(
+code_ifthenelset get_clinit_wrapper_body(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   const bool nondet_static,
@@ -53,7 +53,7 @@ class stub_global_initializer_factoryt
     const std::unordered_set<irep_idt> &stub_globals_set,
     synthetic_methods_mapt &synthetic_methods);
 
-  codet get_stub_initializer_body(
+  code_blockt get_stub_initializer_body(
     const irep_idt &function_id,
     symbol_table_baset &symbol_table,
     const object_factory_parameterst &object_factory_parameters,