Use constructors to construct objects

This is some drive-by cleanup resulting from reviewing #3067. Instead of
incrementally constructing objects do RAII.

Author: tautschnig

jbmc/lib/java-models-library

@@ -122,11 +122,7 @@ static codet get_monitor_call(
     return code_skipt();
 
   // Otherwise we create a function call
-  code_function_callt call;
-  call.function() = symbol_exprt(symbol, it->second.type);
-  call.lhs().make_nil();
-  call.arguments().push_back(object);
-  return call;
+  return code_function_callt(symbol_exprt(symbol, it->second.type), {object});
 }
 
 /// Introduces a monitorexit before every return recursively.
@@ -288,11 +284,15 @@ static void instrument_start_thread(
 
   // Create global variable __CPROVER__next_thread_id. Used as a counter
   // in-order to to assign ids to new threads.
-  const symbolt &next_symbol =
-    add_or_get_symbol(
-        symbol_table, next_thread_id, next_thread_id,
-        java_int_type(),
-        from_integer(0, java_int_type()), false, true);
+  const symbol_exprt next_symbol_expr = add_or_get_symbol(
+                                          symbol_table,
+                                          next_thread_id,
+                                          next_thread_id,
+                                          java_int_type(),
+                                          from_integer(0, java_int_type()),
+                                          false,
+                                          true)
+                                          .symbol_expr();
 
   // Create thread-local variable __CPROVER__thread_id. Holds the id of
   // the thread.
@@ -320,14 +320,11 @@ static void instrument_start_thread(
   codet tmp_a(ID_start_thread);
   tmp_a.set(ID_destination, lbl1);
   code_gotot tmp_b(lbl2);
-  code_labelt tmp_c(lbl1);
-  tmp_c.op0() = codet(ID_skip);
+  const code_labelt tmp_c(lbl1, code_skipt());
 
-  exprt plus(ID_plus, java_int_type());
-  plus.copy_to_operands(next_symbol.symbol_expr());
-  plus.copy_to_operands(from_integer(1, java_int_type()));
-  code_assignt tmp_d(next_symbol.symbol_expr(), plus);
-  code_assignt tmp_e(current_symbol.symbol_expr(), next_symbol.symbol_expr());
+  const plus_exprt plus(next_symbol_expr, from_integer(1, java_int_type()));
+  const code_assignt tmp_d(next_symbol_expr, plus);
+  const code_assignt tmp_e(current_symbol.symbol_expr(), next_symbol_expr);
 
   code_blockt block;
   block.add(tmp_a);
@@ -368,8 +365,7 @@ static void instrument_end_thread(
   // A: codet(id=ID_end_thread)
   // B: codet(id=ID_label,label= __CPROVER_THREAD_EXIT_<ID>)
   codet tmp_a(ID_end_thread);
-  code_labelt tmp_b(lbl2);
-  tmp_b.op0() = codet(ID_skip);
+  const code_labelt tmp_b(lbl2, code_skipt());
 
   code_blockt block;
   block.add(tmp_a);

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -973,8 +973,7 @@ codet java_bytecode_convert_methodt::get_clinit_call(
     return code_skipt();
   else
   {
-    code_function_callt ret;
-    ret.function() = findit->second.symbol_expr();
+    const code_function_callt ret(findit->second.symbol_expr());
     if(needed_lazy_methods)
       needed_lazy_methods->add_needed_method(findit->second.name);
     return ret;
@@ -2004,10 +2003,7 @@ codet java_bytecode_convert_methodt::convert_monitorenterexit(
   java_method_typet type(
     {java_method_typet::parametert(java_reference_type(void_typet()))},
     void_typet());
-  code_function_callt call;
-  call.function() = symbol_exprt(descriptor, type);
-  call.lhs().make_nil();
-  call.arguments().push_back(op[0]);
+  code_function_callt call(symbol_exprt(descriptor, type), {op[0]});
   call.add_source_location() = source_location;
   if(needed_lazy_methods && symbol_table.has_symbol(descriptor))
     needed_lazy_methods->add_needed_method(descriptor);
@@ -2737,13 +2733,11 @@ codet java_bytecode_convert_methodt::convert_iinc(
     bytecode_write_typet::VARIABLE,
     to_symbol_expr(locvar).get_identifier());
 
-  code_assignt code_assign;
-  code_assign.lhs() = variable(arg0, 'i', address, NO_CAST);
-  exprt arg1_int_type = arg1;
-  if(arg1.type() != java_int_type())
-    arg1_int_type.make_typecast(java_int_type());
-  code_assign.rhs() =
-    plus_exprt(variable(arg0, 'i', address, CAST_AS_NEEDED), arg1_int_type);
+  const exprt arg1_int_type =
+    typecast_exprt::conditional_cast(arg1, java_int_type());
+  const code_assignt code_assign(
+    variable(arg0, 'i', address, NO_CAST),
+    plus_exprt(variable(arg0, 'i', address, CAST_AS_NEEDED), arg1_int_type));
   block.copy_to_operands(code_assign);
   return block;
 }

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -169,33 +169,26 @@ static void java_static_lifetime_init(
         // Argument order is: name, isAnnotation, isArray, isInterface,
         // isSynthetic, isLocalClass, isMemberClass, isEnum
 
-        code_function_callt initializer_call;
-        initializer_call.function() = class_literal_init_method->symbol_expr();
-
-        code_function_callt::argumentst &args = initializer_call.arguments();
-
-        // this:
-        args.push_back(address_of_exprt(sym.symbol_expr()));
-        // name:
-        args.push_back(address_of_exprt(class_name_literal));
-        // isAnnotation:
-        args.push_back(
-          constant_bool(class_symbol.type.get_bool(ID_is_annotation)));
-        // isArray:
-        args.push_back(constant_bool(class_is_array));
-        // isInterface:
-        args.push_back(
-          constant_bool(class_symbol.type.get_bool(ID_interface)));
-        // isSynthetic:
-        args.push_back(
-          constant_bool(class_symbol.type.get_bool(ID_synthetic)));
-        // isLocalClass:
-        args.push_back(nondet_bool);
-        // isMemberClass:
-        args.push_back(nondet_bool);
-        // isEnum:
-        args.push_back(
-          constant_bool(class_symbol.type.get_bool(ID_enumeration)));
+        code_function_callt initializer_call(
+          class_literal_init_method->symbol_expr(),
+          {// this:
+           address_of_exprt(sym.symbol_expr()),
+           // name:
+           address_of_exprt(class_name_literal),
+           // isAnnotation:
+           constant_bool(class_symbol.type.get_bool(ID_is_annotation)),
+           // isArray:
+           constant_bool(class_is_array),
+           // isInterface:
+           constant_bool(class_symbol.type.get_bool(ID_interface)),
+           // isSynthetic:
+           constant_bool(class_symbol.type.get_bool(ID_synthetic)),
+           // isLocalClass:
+           nondet_bool,
+           // isMemberClass:
+           nondet_bool,
+           // isEnum:
+           constant_bool(class_symbol.type.get_bool(ID_enumeration))});
 
         // First initialize the object as prior to a constructor:
         namespacet ns(symbol_table);
@@ -676,10 +669,8 @@ bool generate_java_start_function(
       return true; // give up with error
     }
 
-    code_function_callt call_init;
-    call_init.lhs().make_nil();
+    code_function_callt call_init(init_it->second.symbol_expr());
     call_init.add_source_location()=symbol.location;
-    call_init.function()=init_it->second.symbol_expr();
 
     init_code.move_to_operands(call_init);
   }
@@ -689,15 +680,13 @@ bool generate_java_start_function(
   // where return is a new variable
   // and arg1 ... argn are constructed below as well
 
-  code_function_callt call_main;
-
   source_locationt loc=symbol.location;
   loc.set_function(symbol.name);
   source_locationt &dloc=loc;
 
   // function to call
+  code_function_callt call_main(symbol.symbol_expr());
   call_main.add_source_location()=dloc;
-  call_main.function()=symbol.symbol_expr();
   call_main.function().add_source_location()=dloc;
 
   // if the method return type is not void, store return value in a new variable

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -213,7 +213,7 @@ exprt allocate_dynamic_object(
       ID_java,
       symbol_table);
     symbols_created.push_back(&malloc_sym);
-    code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr);
+    code_assignt assign(malloc_sym.symbol_expr(), malloc_expr);
     assign.add_source_location()=loc;
     output_code.copy_to_operands(assign);
     exprt malloc_symbol_expr=malloc_sym.symbol_expr();
@@ -1391,7 +1391,7 @@ void java_object_factoryt::gen_nondet_array_init(
     symbol_table);
   symbols_created.push_back(&array_init_symbol);
   const auto &array_init_symexpr=array_init_symbol.symbol_expr();
-  codet data_assign=code_assignt(array_init_symexpr, init_array_expr);
+  code_assignt data_assign(array_init_symexpr, init_array_expr);
   data_assign.add_source_location()=loc;
   assignments.copy_to_operands(data_assign);
 
@@ -1738,8 +1738,7 @@ void java_object_factoryt::gen_method_call_if_present(
   if(const auto func = symbol_table.lookup(method_name))
   {
     const java_method_typet &type = to_java_method_type(func->type);
-    code_function_callt fun_call;
-    fun_call.function() = func->symbol_expr();
+    code_function_callt fun_call(func->symbol_expr());
     if(type.has_this())
       fun_call.arguments().push_back(address_of_exprt(instance_expr));
     assignments.add(fun_call);

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -208,18 +208,16 @@ static void clinit_wrapper_do_recursive_calls(
     auto findit = symbol_table.symbols.find(base_init_routine);
     if(findit == symbol_table.symbols.end())
       continue;
-    code_function_callt call_base;
-    call_base.function() = findit->second.symbol_expr();
-    init_body.move_to_operands(call_base);
+    const code_function_callt call_base(findit->second.symbol_expr());
+    init_body.add(call_base);
   }
 
   const irep_idt &real_clinit_name = clinit_function_name(class_name);
   auto find_sym_it = symbol_table.symbols.find(real_clinit_name);
   if(find_sym_it != symbol_table.symbols.end())
   {
-    code_function_callt call_real_init;
-    call_real_init.function() = find_sym_it->second.symbol_expr();
-    init_body.move_to_operands(call_real_init);
+    const code_function_callt call_real_init(find_sym_it->second.symbol_expr());
+    init_body.add(call_real_init);
   }
 
   // If nondet-static option is given, add a standard nondet initialization for

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -1552,11 +1552,11 @@ codet java_string_library_preprocesst::make_object_get_class_code(
     loc);
 
   // > class1 = Class.forName(string1)
-  code_function_callt fun_call;
-  fun_call.function()=symbol_exprt(
-    "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;");
-  fun_call.lhs()=class1;
-  fun_call.arguments().push_back(string1);
+  code_function_callt fun_call(
+    class1,
+    symbol_exprt(
+      "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;"),
+    {string1});
   const java_method_typet fun_type(
     {java_method_typet::parametert(string_ptr_type)}, class_type);
   fun_call.function().type()=fun_type;

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -129,13 +129,12 @@ SCENARIO(
   callee.set(ID_C_class, "java::VirtualFunctionsTestParent");
   callee.set(ID_component_name, "f:()V");
 
-  code_function_callt call;
-  call.function() = callee;
-  // Specific argument doesn't matter, so just pass an appropriately typed
-  // null pointer:
-  call.arguments().push_back(
-    null_pointer_exprt(
-      to_pointer_type(to_code_type(callee.type()).parameters()[0].type())));
+  const code_function_callt call(
+    callee,
+    // Specific argument doesn't matter, so just pass an appropriately typed
+    // null pointer:
+    {null_pointer_exprt(
+      to_pointer_type(to_code_type(callee.type()).parameters()[0].type()))});
   virtual_call_inst->code = call;
 
   test_program.add_instruction(END_FUNCTION);

jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp

@@ -32,7 +32,7 @@ void check_function_call(
   for(const auto &target : targets)
   {
     REQUIRE(target->type == goto_program_instruction_typet::FUNCTION_CALL);
-    const code_function_callt call = to_code_function_call(target->code);
+    const code_function_callt &call = to_code_function_call(target->code);
     REQUIRE(call.function().id() == ID_symbol);
     REQUIRE(to_symbol_expr(call.function()).get_identifier() == function_name);
   }

jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

@@ -334,7 +334,7 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code)
         else
         {
           auto source_location = code.source_location();
-          code = codet(ID_skip);
+          code = code_skipt();
           code.add_source_location() = source_location;
         }
       }