Merge pull request diffblue#4532 from tautschnig/4524-follow-up

Java bytecode conversion: inline or move temporaries

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -859,7 +859,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     local_symbol.type = java_reference_type(struct_tag_type);
     local_symbol.mode=ID_java;
     symbol_table.add(local_symbol);
-    const auto &local_symexpr=local_symbol.symbol_expr();
+    const auto local_symexpr = local_symbol.symbol_expr();
 
     code_declt declare_cloned(local_symexpr);
 

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1621,15 +1621,12 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     {
       PRECONDITION(op.size() == 1 && results.size() == 1);
 
-      const typecast_exprt pointer(op[0], java_array_type(statement[0]));
-
-      dereference_exprt array{pointer};
-      PRECONDITION(pointer.type().subtype().id() == ID_struct_tag);
+      dereference_exprt array{
+        typecast_exprt{op[0], java_array_type(statement[0])}};
+      PRECONDITION(array.type().id() == ID_struct_tag);
       array.set(ID_java_member_access, true);
 
-      const member_exprt length(array, "length", java_int_type());
-
-      results[0]=length;
+      results[0] = member_exprt{std::move(array), "length", java_int_type()};
     }
     else if(statement=="tableswitch" ||
             statement=="lookupswitch")
@@ -1823,8 +1820,8 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
 
     if(start_new_block)
     {
-      code_labelt newlabel(label(std::to_string(address)), code_blockt());
-      root_block.add(newlabel);
+      root_block.add(
+        code_labelt{label(std::to_string(address)), code_blockt{}});
       root.branch.push_back(block_tree_nodet::get_leaf());
       assert((root.branch_addresses.empty() ||
               root.branch_addresses.back()<address) &&
@@ -1952,10 +1949,9 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
       if(a_it == args.begin())
       {
         code_switch_caset code_case(nil_exprt(), std::move(code));
-        code_case.add_source_location() = location;
         code_case.set_default();
 
-        code_block.add(std::move(code_case));
+        code_block.add(std::move(code_case), location);
       }
       else
       {
@@ -1964,9 +1960,7 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
         case_op.add_source_location() = location;
 
         code_switch_caset code_case(std::move(case_op), std::move(code));
-        code_case.add_source_location() = location;
-
-        code_block.add(std::move(code_case));
+        code_block.add(std::move(code_case), location);
       }
     }
   }
@@ -2490,7 +2484,7 @@ code_blockt java_bytecode_convert_methodt::convert_newarray(
     constant_exprt size_limit = from_integer(max_array_length, java_int_type());
     binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
     code_assumet assume_le_max_size(le_max_size);
-    block.add(assume_le_max_size);
+    block.add(std::move(assume_le_max_size));
   }
   const exprt tmp = tmp_variable("newarray", ref_type);
   block.add(code_assignt(tmp, java_new_array));
@@ -2693,10 +2687,10 @@ code_blockt java_bytecode_convert_methodt::convert_iinc(
 
   const exprt arg1_int_type =
     typecast_exprt::conditional_cast(arg1, java_int_type());
-  const code_assignt code_assign(
+  code_assignt code_assign(
     variable(arg0, 'i', address, NO_CAST),
     plus_exprt(variable(arg0, 'i', address, CAST_AS_NEEDED), arg1_int_type));
-  block.add(code_assign);
+  block.add(std::move(code_assign));
 
   return block;
 }
@@ -2829,20 +2823,16 @@ exprt java_bytecode_convert_methodt::convert_aload(
   const irep_idt &statement,
   const exprt::operandst &op) const
 {
-  const char &type_char = statement[0];
-  const typecast_exprt pointer(op[0], java_array_type(type_char));
-
-  dereference_exprt deref{pointer};
+  const char type_char = statement[0];
+  dereference_exprt deref{typecast_exprt{op[0], java_array_type(type_char)}};
   deref.set(ID_java_member_access, true);
 
-  const member_exprt data_ptr(
+  member_exprt data_ptr(
     deref, "data", pointer_type(java_type_from_char(type_char)));
-
-  plus_exprt data_plus_offset{data_ptr, op[1]};
+  plus_exprt data_plus_offset{std::move(data_ptr), op[1]};
   // tag it so it's easy to identify during instrumentation
   data_plus_offset.set(ID_java_array_access, true);
-  const dereference_exprt element{data_plus_offset};
-  return java_bytecode_promotion(element);
+  return java_bytecode_promotion(dereference_exprt{data_plus_offset});
 }
 
 code_blockt java_bytecode_convert_methodt::convert_store(
@@ -2860,15 +2850,15 @@ code_blockt java_bytecode_convert_methodt::convert_store(
     toassign = typecast_exprt::conditional_cast(toassign, var.type());
 
   code_blockt block;
+  block.add_source_location() = location;
 
   save_stack_entries(
     "stack_store",
     block,
     bytecode_write_typet::VARIABLE,
     var_name);
-  code_assignt assign(var, toassign);
-  assign.add_source_location() = location;
-  block.add(assign);
+
+  block.add(code_assignt{var, toassign}, location);
   return block;
 }
 
@@ -2878,28 +2868,23 @@ code_blockt java_bytecode_convert_methodt::convert_astore(
   const source_locationt &location)
 {
   const char type_char = statement[0];
-  const typecast_exprt pointer(op[0], java_array_type(type_char));
-
-  dereference_exprt deref{pointer};
+  dereference_exprt deref{typecast_exprt{op[0], java_array_type(type_char)}};
   deref.set(ID_java_member_access, true);
 
-  const member_exprt data_ptr(
+  member_exprt data_ptr(
     deref, "data", pointer_type(java_type_from_char(type_char)));
-
-  plus_exprt data_plus_offset{data_ptr, op[1]};
+  plus_exprt data_plus_offset{std::move(data_ptr), op[1]};
   // tag it so it's easy to identify during instrumentation
   data_plus_offset.set(ID_java_array_access, true);
-  const dereference_exprt element{data_plus_offset};
 
   code_blockt block;
   block.add_source_location() = location;
 
   save_stack_entries(
     "stack_astore", block, bytecode_write_typet::ARRAY_REF, "");
 
-  code_assignt array_put(element, op[2]);
-  array_put.add_source_location() = location;
-  block.add(array_put);
+  code_assignt array_put{dereference_exprt{data_plus_offset}, op[2]};
+  block.add(std::move(array_put), location);
   return block;
 }
 

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -468,10 +468,8 @@ refined_string_exprt java_string_library_preprocesst::decl_string_expr(
     array_type, "cprover_string_content", loc, function_id, symbol_table);
   const symbol_exprt content_field = sym_content.symbol_expr();
   code.add(code_declt(content_field), loc);
-  const refined_string_exprt str{
-    length_field, content_field, refined_string_type};
-  code.add(code_declt(length_field), loc);
-  return str;
+  code.add(code_declt{length_field}, loc);
+  return refined_string_exprt{length_field, content_field, refined_string_type};
 }
 
 /// add symbols with prefix cprover_string_length and cprover_string_data and
@@ -601,10 +599,10 @@ exprt make_nondet_infinite_char_array(
   const symbol_exprt data_pointer = data_sym.symbol_expr();
   code.add(code_declt(data_pointer));
   code.add(make_allocate_code(data_pointer, array_type.size()));
-  const exprt nondet_data = side_effect_expr_nondett(array_type, loc);
-  const exprt data = dereference_exprt{data_pointer};
-  code.add(code_assignt(data, nondet_data), loc);
-  return data;
+  side_effect_expr_nondett nondet_data{array_type, loc};
+  dereference_exprt data{data_pointer};
+  code.add(code_assignt{data, std::move(nondet_data)}, loc);
+  return std::move(data);
 }
 
 /// Add a call to a primitive of the string solver, letting it know that
@@ -847,8 +845,8 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
 
   // Assignments
   code.add(code_assignt(lhs.length(), rhs_length), loc);
-  const exprt data_as_array = get_data(deref, symbol_table);
-  code.add(code_assignt(lhs.content(), data_as_array), loc);
+  exprt data_as_array = get_data(deref, symbol_table);
+  code.add(code_assignt{lhs.content(), std::move(data_as_array)}, loc);
 }
 
 /// Create a string expression whose value is given by a literal
@@ -868,9 +866,12 @@ java_string_library_preprocesst::string_literal_to_string_expr(
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
-  const constant_exprt expr(s, string_typet());
   return string_expr_of_function(
-    ID_cprover_string_literal_func, {expr}, loc, symbol_table, code);
+    ID_cprover_string_literal_func,
+    {constant_exprt{s, string_typet{}}},
+    loc,
+    symbol_table,
+    code);
 }
 
 /// Provide code for the String.valueOf(F) function.