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

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -141,7 +141,7 @@ static void monitor_exits(codet &code, const codet &monitorexit)
     // Replace the return with a monitor exit plus return block
     code_blockt return_block;
     return_block.add(monitorexit);
-    return_block.move_to_operands(code);
+    return_block.move(code);
     code = return_block;
   }
   else if(
@@ -262,11 +262,11 @@ static void instrument_synchronized_code(
 
   // 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);
+  try_block.move(monitorenter);
+  try_block.move(catch_push);
+  try_block.move(code);
+  try_block.move(catch_pop);
+  try_block.move(catch_label);
   code = try_block;
 }
 

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -856,7 +856,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     code_blockt clone_body;
 
     code_declt declare_cloned(local_symexpr);
-    clone_body.move_to_operands(declare_cloned);
+    clone_body.move(declare_cloned);
 
     source_locationt location;
     location.set_function(local_name);
@@ -868,7 +868,7 @@ 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);
+    clone_body.move(create_blank);
 
     member_exprt old_data(
       old_array, data_component.get_name(), data_component.type());
@@ -898,7 +898,7 @@ 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);
+    clone_body.move(declare_index);
 
     code_fort copy_loop;
 
@@ -921,13 +921,13 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     copy_loop.body()=copy_cell;
 
     // End for-loop
-    clone_body.move_to_operands(copy_loop);
+    clone_body.move(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);
+    clone_body.move(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.move(to_code(this_block_children[blockidx]));
 
   // Relabel the inner header:
   to_code_label(to_code(newblock.operands()[0])).set_label(new_label_irep);
@@ -1728,7 +1728,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);
           }
@@ -1744,7 +1744,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;
@@ -1753,7 +1753,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
@@ -1835,7 +1835,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.move(newlabel);
       root.branch.push_back(block_tree_nodet::get_leaf());
       assert((root.branch_addresses.empty() ||
               root.branch_addresses.back()<address) &&
@@ -1913,7 +1913,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
   }
 
   for(auto &block : root_block.operands())
-    code.move_to_operands(block);
+    code.move(to_code(block));
 
   return code;
 }
@@ -2258,8 +2258,8 @@ void java_bytecode_convert_methodt::convert_invoke(
     if(clinit_call.get_statement() != ID_skip)
     {
       code_blockt ret_block;
-      ret_block.move_to_operands(clinit_call);
-      ret_block.move_to_operands(c);
+      ret_block.move(clinit_call);
+      ret_block.move(c);
       c = std::move(ret_block);
     }
   }
@@ -2325,8 +2325,8 @@ void java_bytecode_convert_methodt::convert_athrow(
     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);
+    ret_block.move(assert_code);
+    ret_block.move(assume_code);
     c = ret_block;
   }
   else
@@ -2399,8 +2399,8 @@ codet &java_bytecode_convert_methodt::do_exception_handling(
       }
 
       code_blockt try_block;
-      try_block.move_to_operands(catch_push);
-      try_block.move_to_operands(c);
+      try_block.move(catch_push);
+      try_block.move(c);
       c = try_block;
     }
     else
@@ -2440,8 +2440,8 @@ codet &java_bytecode_convert_methodt::do_exception_handling(
         // 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);
+        end_try_block.move(c);
+        end_try_block.move(catch_pop);
         c = end_try_block;
       }
     }
@@ -2468,11 +2468,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.move(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;
 }
@@ -2525,10 +2525,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).move(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;
 }
 
@@ -2552,8 +2552,8 @@ void java_bytecode_convert_methodt::convert_new(
   if(clinit_call.get_statement() != ID_skip)
   {
     code_blockt ret_block;
-    ret_block.move_to_operands(clinit_call);
-    ret_block.move_to_operands(c);
+    ret_block.move(clinit_call);
+    ret_block.move(c);
     c = std::move(ret_block);
   }
   results[0] = tmp;
@@ -2579,15 +2579,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.move(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;
 }
 
@@ -2602,7 +2602,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;
 }
 
@@ -2744,7 +2744,7 @@ codet java_bytecode_convert_methodt::convert_iinc(
     arg1_int_type.make_typecast(java_int_type());
   code_assign.rhs() =
     plus_exprt(variable(arg0, 'i', address, CAST_AS_NEEDED), arg1_int_type);
-  block.copy_to_operands(code_assign);
+  block.add(code_assign);
   return block;
 }
 
@@ -2849,7 +2849,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.move(g);
     else
     {
       code_ifthenelset branch;
@@ -2860,7 +2860,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.move(branch);
     }
   }
   return c;
@@ -3274,6 +3274,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;
 }

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -129,8 +129,8 @@ codet java_bytecode_instrumentt::throw_exception(
   throw_expr.copy_to_operands(new_symbol.symbol_expr());
 
   code_blockt throw_code;
-  throw_code.move_to_operands(assign_new);
-  throw_code.copy_to_operands(code_expressiont(throw_expr));
+  throw_code.move(assign_new);
+  throw_code.add(code_expressiont(throw_expr));
 
   code_ifthenelset if_code;
   if_code.add_source_location()=original_loc;
@@ -333,7 +333,7 @@ void java_bytecode_instrumentt::add_expr_instrumentation(
     if(expr_instrumentation->get_statement() == ID_block)
       block.append(to_code_block(*expr_instrumentation));
     else
-      block.move_to_operands(*expr_instrumentation);
+      block.move(*expr_instrumentation);
   }
 }
 
@@ -350,7 +350,7 @@ void java_bytecode_instrumentt::prepend_instrumentation(
     if(code.get_statement()==ID_block)
       instrumentation.append(to_code_block(code));
     else
-      instrumentation.copy_to_operands(code);
+      instrumentation.add(code);
     code=instrumentation;
   }
 }
@@ -452,10 +452,9 @@ void java_bytecode_instrumentt::instrument_code(codet &code)
     // Check for a null this-argument of a virtual call:
     if(function_type.has_this())
     {
-      block.copy_to_operands(
-        check_null_dereference(
-          code_function_call.arguments()[0],
-          code_function_call.source_location()));
+      block.add(check_null_dereference(
+        code_function_call.arguments()[0],
+        code_function_call.source_location()));
     }
 
     for(const auto &arg : code_function_call.arguments())
@@ -481,7 +480,7 @@ optionalt<codet> java_bytecode_instrumentt::instrument_expr(const exprt &expr)
   forall_operands(it, expr)
   {
     if(optionalt<codet> op_result = instrument_expr(*it))
-      result.move_to_operands(*op_result);
+      result.move(*op_result);
   }
 
   // Add any check due at this node:
@@ -503,7 +502,7 @@ optionalt<codet> java_bytecode_instrumentt::instrument_expr(const exprt &expr)
             dereference_expr,
             plus_expr.op1(),
             expr.source_location());
-        result.move_to_operands(bounds_check);
+        result.move(bounds_check);
       }
     }
   }
@@ -515,29 +514,20 @@ optionalt<codet> java_bytecode_instrumentt::instrument_expr(const exprt &expr)
     {
       // this corresponds to a throw and so we check that
       // we don't throw null
-      result.copy_to_operands(
-        check_null_dereference(
-          expr.op0(),
-          expr.source_location()));
+      result.add(check_null_dereference(expr.op0(), expr.source_location()));
     }
     else if(statement==ID_java_new_array)
     {
       // this corresponds to new array so we check that
       // length is >=0
-      result.copy_to_operands(
-        check_array_length(
-          expr.op0(),
-          expr.source_location()));
+      result.add(check_array_length(expr.op0(), expr.source_location()));
     }
   }
   else if((expr.id()==ID_div || expr.id()==ID_mod) &&
           expr.type().id()==ID_signedbv)
   {
     // check division by zero (for integer types only)
-    result.copy_to_operands(
-      check_arithmetic_exception(
-        expr.op1(),
-        expr.source_location()));
+    result.add(check_arithmetic_exception(expr.op1(), expr.source_location()));
   }
   else if(expr.id()==ID_dereference &&
           expr.get_bool(ID_java_member_access))
@@ -548,7 +538,7 @@ optionalt<codet> java_bytecode_instrumentt::instrument_expr(const exprt &expr)
       check_null_dereference(
         dereference_expr.op0(),
         dereference_expr.source_location());
-    result.move_to_operands(null_dereference_check);
+    result.move(null_dereference_check);
   }
 
   if(result==code_blockt())
@@ -599,7 +589,7 @@ void java_bytecode_instrument_symbol(
 /// \param exc_symbol: the top-level exception symbol
 /// \param source_location: the source location to attach to the assertion
 void java_bytecode_instrument_uncaught_exceptions(
-  codet &init_code,
+  code_blockt &init_code,
   const symbolt &exc_symbol,
   const source_locationt &source_location)
 {
@@ -612,7 +602,7 @@ void java_bytecode_instrument_uncaught_exceptions(
   assert_location.set_comment("no uncaught exception");
   assert_no_exception.add_source_location() = assert_location;
 
-  init_code.move_to_operands(assert_no_exception);
+  init_code.move(assert_no_exception);
 }
 
 /// Instruments all the code in the symbol_table with