Merge pull request #3067 from diffblue/code_block_move_add_partial

use code_blockt::add and ::move for adding a statement

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -135,10 +135,7 @@ static void monitor_exits(codet &code, const codet &monitorexit)
   if(statement == ID_return)
   {
     // Replace the return with a monitor exit plus return block
-    code_blockt return_block;
-    return_block.add(monitorexit);
-    return_block.move_to_operands(code);
-    code = return_block;
+    code = code_blockt({monitorexit, code});
   }
   else if(
     statement == ID_label || statement == ID_block ||
@@ -257,13 +254,7 @@ static void instrument_synchronized_code(
   monitor_exits(code, monitorexit);
 
   // Wrap the code into a try finally
-  code_blockt try_block;
-  try_block.move_to_operands(monitorenter);
-  try_block.move_to_operands(catch_push);
-  try_block.move_to_operands(code);
-  try_block.move_to_operands(catch_pop);
-  try_block.move_to_operands(catch_label);
-  code = try_block;
+  code = code_blockt({monitorenter, catch_push, code, catch_pop, catch_label});
 }
 
 /// Transforms the codet stored in in \p f_code, which is a call to function
@@ -326,17 +317,14 @@ static void instrument_start_thread(
   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);
-  block.add(tmp_b);
-  block.add(tmp_c);
-  block.add(codet(ID_atomic_begin));
-  block.add(tmp_d);
-  block.add(tmp_e);
-  block.add(codet(ID_atomic_end));
-  block.add_source_location() = f_code.source_location();
-
-  code = block;
+  code = code_blockt({tmp_a,
+                      tmp_b,
+                      tmp_c,
+                      codet(ID_atomic_begin),
+                      tmp_d,
+                      tmp_e,
+                      codet(ID_atomic_end)});
+  code.add_source_location() = f_code.source_location();
 }
 
 /// Transforms the codet stored in in \p f_code, which is a call to function
@@ -367,12 +355,9 @@ static void instrument_end_thread(
   codet tmp_a(ID_end_thread);
   const code_labelt tmp_b(lbl2, code_skipt());
 
-  code_blockt block;
-  block.add(tmp_a);
-  block.add(tmp_b);
-  block.add_source_location() = code.source_location();
-
-  code = block;
+  const auto location = code.source_location();
+  code = code_blockt({tmp_a, tmp_b});
+  code.add_source_location() = location;
 }
 
 /// Transforms the codet stored in in \p f_code, which is a call to function

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -853,10 +853,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     symbol_table.add(local_symbol);
     const auto &local_symexpr=local_symbol.symbol_expr();
 
-    code_blockt clone_body;
-
     code_declt declare_cloned(local_symexpr);
-    clone_body.move_to_operands(declare_cloned);
 
     source_locationt location;
     location.set_function(local_name);
@@ -868,7 +865,6 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
       old_array, length_component.get_name(), length_component.type());
     java_new_array.copy_to_operands(old_length);
     code_assignt create_blank(local_symexpr, java_new_array);
-    clone_body.move_to_operands(create_blank);
 
     member_exprt old_data(
       old_array, data_component.get_name(), data_component.type());
@@ -898,7 +894,6 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     const auto &index_symexpr=index_symbol.symbol_expr();
 
     code_declt declare_index(index_symexpr);
-    clone_body.move_to_operands(declare_index);
 
     code_fort copy_loop;
 
@@ -920,14 +915,13 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     code_assignt copy_cell(new_cell, old_cell);
     copy_loop.body()=copy_cell;
 
-    // End for-loop
-    clone_body.move_to_operands(copy_loop);
-
     member_exprt new_base_class(
       new_array, base_class_component.get_name(), base_class_component.type());
     address_of_exprt retval(new_base_class);
     code_returnt return_inst(retval);
-    clone_body.move_to_operands(return_inst);
+
+    const code_blockt clone_body(
+      {declare_cloned, create_blank, declare_index, copy_loop, return_inst});
 
     symbolt clone_symbol;
     clone_symbol.name=clone_name;

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -873,7 +873,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
   for(auto blockidx=child_offset, blocklim=child_offset+nblocks;
       blockidx!=blocklim;
       ++blockidx)
-    newblock.move_to_operands(this_block_children[blockidx]);
+    newblock.add(this_block_children[blockidx]);
 
   // Relabel the inner header:
   to_code_label(newblock.statements()[0]).set_label(new_label_irep);
@@ -1727,7 +1727,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
           {
             symbol_exprt lhs=tmp_variable("$stack", s_it->type());
             code_assignt a(lhs, *s_it);
-            more_code.copy_to_operands(a);
+            more_code.add(a);
 
             s_it->swap(lhs);
           }
@@ -1743,7 +1743,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
             assert(has_prefix(os_it->get_string(ID_C_base_name), "$stack"));
             symbol_exprt lhs=to_symbol_expr(*os_it);
             code_assignt a(lhs, expr);
-            more_code.copy_to_operands(a);
+            more_code.add(a);
 
             expr.swap(lhs);
             ++os_it;
@@ -1752,7 +1752,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
 
         if(results.empty())
         {
-          more_code.copy_to_operands(c);
+          more_code.add(c);
           c.swap(more_code);
         }
         else
@@ -1834,7 +1834,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     if(start_new_block)
     {
       code_labelt newlabel(label(std::to_string(address)), code_blockt());
-      root_block.move_to_operands(newlabel);
+      root_block.add(newlabel);
       root.branch.push_back(block_tree_nodet::get_leaf());
       assert((root.branch_addresses.empty() ||
               root.branch_addresses.back()<address) &&
@@ -1912,7 +1912,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
   }
 
   for(auto &block : root_block.statements())
-    code.move_to_operands(block);
+    code.add(block);
 
   return code;
 }
@@ -2252,12 +2252,7 @@ void java_bytecode_convert_methodt::convert_invoke(
   {
     codet clinit_call = get_clinit_call(arg0.get(ID_C_class));
     if(clinit_call.get_statement() != ID_skip)
-    {
-      code_blockt ret_block;
-      ret_block.move_to_operands(clinit_call);
-      ret_block.move_to_operands(c);
-      c = std::move(ret_block);
-    }
+      c = code_blockt({clinit_call, c});
   }
 }
 
@@ -2320,10 +2315,7 @@ void java_bytecode_convert_methodt::convert_athrow(
     assume_location.set("user-provided", true);
     assume_code.add_source_location() = assume_location;
 
-    code_blockt ret_block;
-    ret_block.move_to_operands(assert_code);
-    ret_block.move_to_operands(assume_code);
-    c = ret_block;
+    c = code_blockt({assert_code, assume_code});
   }
   else
   {
@@ -2394,10 +2386,7 @@ codet &java_bytecode_convert_methodt::do_exception_handling(
             exception_ids[i], handler_labels[i]));
       }
 
-      code_blockt try_block;
-      try_block.move_to_operands(catch_push);
-      try_block.move_to_operands(c);
-      c = try_block;
+      c = code_blockt({catch_push, c});
     }
     else
     {
@@ -2435,10 +2424,7 @@ codet &java_bytecode_convert_methodt::do_exception_handling(
         start_pc = exception_row.start_pc;
         // add CATCH_POP instruction
         code_pop_catcht catch_pop;
-        code_blockt end_try_block;
-        end_try_block.move_to_operands(c);
-        end_try_block.move_to_operands(catch_pop);
-        c = end_try_block;
+        c = code_blockt({c, catch_pop});
       }
     }
   }
@@ -2464,11 +2450,11 @@ void java_bytecode_convert_methodt::convert_multianewarray(
     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);
-    create.move_to_operands(assume_le_max_size);
+    create.add(assume_le_max_size);
   }
 
   const exprt tmp = tmp_variable("newarray", ref_type);
-  create.copy_to_operands(code_assignt(tmp, java_new_array));
+  create.add(code_assignt(tmp, java_new_array));
   c = std::move(create);
   results[0] = tmp;
 }
@@ -2521,10 +2507,10 @@ void 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);
-    c.move_to_operands(assume_le_max_size);
+    to_code_block(c).add(assume_le_max_size);
   }
   const exprt tmp = tmp_variable("newarray", ref_type);
-  c.copy_to_operands(code_assignt(tmp, java_new_array));
+  to_code_block(c).add(code_assignt(tmp, java_new_array));
   results[0] = tmp;
 }
 
@@ -2547,10 +2533,7 @@ void java_bytecode_convert_methodt::convert_new(
     get_clinit_call(to_symbol_type(arg0.type()).get_identifier());
   if(clinit_call.get_statement() != ID_skip)
   {
-    code_blockt ret_block;
-    ret_block.move_to_operands(clinit_call);
-    ret_block.move_to_operands(c);
-    c = std::move(ret_block);
+    c = code_blockt({clinit_call, c});
   }
   results[0] = tmp;
 }
@@ -2575,15 +2558,15 @@ codet java_bytecode_convert_methodt::convert_putstatic(
   // the field.
   codet clinit_call = get_clinit_call(arg0.get_string(ID_class));
   if(clinit_call.get_statement() != ID_skip)
-    block.move_to_operands(clinit_call);
+    block.add(clinit_call);
 
   save_stack_entries(
     "stack_static_field",
     symbol_expr.type(),
     block,
     bytecode_write_typet::STATIC_FIELD,
     symbol_expr.get_identifier());
-  block.copy_to_operands(code_assignt(symbol_expr, op[0]));
+  block.add(code_assignt(symbol_expr, op[0]));
   return block;
 }
 
@@ -2598,7 +2581,7 @@ codet java_bytecode_convert_methodt::convert_putfield(
     block,
     bytecode_write_typet::FIELD,
     arg0.get(ID_component_name));
-  block.copy_to_operands(code_assignt(to_member(op[0], arg0), op[1]));
+  block.add(code_assignt(to_member(op[0], arg0), op[1]));
   return block;
 }
 
@@ -2738,7 +2721,8 @@ codet java_bytecode_convert_methodt::convert_iinc(
   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);
+  block.add(code_assign);
+
   return block;
 }
 
@@ -2843,7 +2827,7 @@ code_blockt java_bytecode_convert_methodt::convert_ret(
     code_gotot g(label(number));
     g.add_source_location() = location;
     if(idx == idxlim - 1)
-      c.move_to_operands(g);
+      c.add(g);
     else
     {
       code_ifthenelset branch;
@@ -2854,7 +2838,7 @@ code_blockt java_bytecode_convert_methodt::convert_ret(
       branch.cond().add_source_location() = location;
       branch.then_case() = g;
       branch.add_source_location() = location;
-      c.move_to_operands(branch);
+      c.add(branch);
     }
   }
   return c;
@@ -2905,7 +2889,7 @@ codet java_bytecode_convert_methodt::convert_store(
     var_name);
   code_assignt assign(var, toassign);
   assign.add_source_location() = location;
-  block.move(assign);
+  block.add(assign);
   return block;
 }
 
@@ -2937,7 +2921,7 @@ codet java_bytecode_convert_methodt::convert_astore(
 
   code_assignt array_put(element, op[2]);
   array_put.add_source_location() = location;
-  block.move(array_put);
+  block.add(array_put);
   return block;
 }
 
@@ -3268,6 +3252,6 @@ void java_bytecode_convert_methodt::create_stack_tmp_var(
 {
   const exprt tmp_var=
     tmp_variable(tmp_var_prefix, tmp_var_type);
-  block.copy_to_operands(code_assignt(tmp_var, stack_entry));
+  block.add(code_assignt(tmp_var, stack_entry));
   stack_entry=tmp_var;
 }