Merge pull request #3504 from tautschnig/constructors-ifthenelse

Multi-operand constructor for code_ifthenelset

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2705,15 +2705,19 @@ code_ifthenelset java_bytecode_convert_methodt::convert_ifnull(
   const mp_integer &number,
   const source_locationt &location) const
 {
-  code_ifthenelset code_branch;
   const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
   const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
-  code_branch.cond() = binary_relation_exprt(lhs, ID_equal, rhs);
+
   const method_offsett label_number = numeric_cast_v<method_offsett>(number);
-  code_branch.then_case() = code_gotot(label(std::to_string(label_number)));
+
+  code_ifthenelset code_branch(
+    binary_relation_exprt(lhs, ID_equal, rhs),
+    code_gotot(label(std::to_string(label_number))));
+
   code_branch.then_case().add_source_location() =
     address_map.at(label_number).source->source_location;
   code_branch.add_source_location() = location;
+
   return code_branch;
 }
 
@@ -2723,15 +2727,19 @@ code_ifthenelset java_bytecode_convert_methodt::convert_ifnonull(
   const mp_integer &number,
   const source_locationt &location) const
 {
-  code_ifthenelset code_branch;
   const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
   const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
-  code_branch.cond() = binary_relation_exprt(lhs, ID_notequal, rhs);
+
   const method_offsett label_number = numeric_cast_v<method_offsett>(number);
-  code_branch.then_case() = code_gotot(label(std::to_string(label_number)));
+
+  code_ifthenelset code_branch(
+    binary_relation_exprt(lhs, ID_notequal, rhs),
+    code_gotot(label(std::to_string(label_number))));
+
   code_branch.then_case().add_source_location() =
     address_map.at(label_number).source->source_location;
   code_branch.add_source_location() = location;
+
   return code_branch;
 }
 
@@ -2742,18 +2750,20 @@ code_ifthenelset java_bytecode_convert_methodt::convert_if(
   const mp_integer &number,
   const source_locationt &location) const
 {
-  code_ifthenelset code_branch;
-  code_branch.cond() =
-    binary_relation_exprt(op[0], id, from_integer(0, op[0].type()));
+  const method_offsett label_number = numeric_cast_v<method_offsett>(number);
+
+  code_ifthenelset code_branch(
+    binary_relation_exprt(op[0], id, from_integer(0, op[0].type())),
+    code_gotot(label(std::to_string(label_number))));
+
   code_branch.cond().add_source_location() = location;
   code_branch.cond().add_source_location().set_function(method_id);
-  const method_offsett label_number = numeric_cast_v<method_offsett>(number);
-  code_branch.then_case() = code_gotot(label(std::to_string(label_number)));
   code_branch.then_case().add_source_location() =
     address_map.at(label_number).source->source_location;
   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 code_branch;
 }
 
@@ -2764,15 +2774,16 @@ code_ifthenelset java_bytecode_convert_methodt::convert_if_cmp(
   const mp_integer &number,
   const source_locationt &location) const
 {
-  code_ifthenelset code_branch;
   const irep_idt cmp_op = get_if_cmp_operator(statement);
   binary_relation_exprt condition(
     op[0], cmp_op, typecast_exprt::conditional_cast(op[1], op[0].type()));
   condition.add_source_location() = location;
 
-  code_branch.cond() = condition;
   const method_offsett label_number = numeric_cast_v<method_offsett>(number);
-  code_branch.then_case() = code_gotot(label(std::to_string(label_number)));
+
+  code_ifthenelset code_branch(
+    std::move(condition), code_gotot(label(std::to_string(label_number))));
+
   code_branch.then_case().add_source_location() =
     address_map.at(label_number).source->source_location;
   code_branch.add_source_location() = location;
@@ -2797,15 +2808,16 @@ code_blockt java_bytecode_convert_methodt::convert_ret(
       c.add(g);
     else
     {
-      code_ifthenelset branch;
       auto address_ptr =
         from_integer(jsr_ret_targets[idx], unsignedbv_typet(64));
       address_ptr.type() = pointer_type(void_typet());
-      branch.cond() = equal_exprt(retvar, address_ptr);
+
+      code_ifthenelset branch(equal_exprt(retvar, address_ptr), std::move(g));
+
       branch.cond().add_source_location() = location;
-      branch.then_case() = g;
       branch.add_source_location() = location;
-      c.add(branch);
+
+      c.add(std::move(branch));
     }
   }
   return c;

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -127,10 +127,10 @@ code_ifthenelset java_bytecode_instrumentt::throw_exception(
   side_effect_expr_throwt throw_expr(irept(), typet(), original_loc);
   throw_expr.copy_to_operands(new_symbol.symbol_expr());
 
-  code_ifthenelset if_code;
+  code_ifthenelset if_code(
+    cond, code_blockt({assign_new, code_expressiont(throw_expr)}));
+
   if_code.add_source_location()=original_loc;
-  if_code.cond()=cond;
-  if_code.then_case() = code_blockt({assign_new, code_expressiont(throw_expr)});
 
   return if_code;
 }
@@ -250,11 +250,9 @@ code_ifthenelset java_bytecode_instrumentt::check_class_cast(
     check_code=std::move(assert_class);
   }
 
-  code_ifthenelset conditional_check;
-  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 conditional_check;
+  return code_ifthenelset(
+    notequal_exprt(std::move(null_check_op), null_pointer_exprt(voidptr)),
+    std::move(check_code));
 }
 
 /// Checks whether \p expr is null and throws NullPointerException/

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -853,12 +853,12 @@ void java_object_factoryt::gen_nondet_pointer_init(
     //    <code from recursive call to gen_nondet_init() with
     //             tmp$<temporary_counter>>
     // }
-    code_ifthenelset null_check;
-    null_check.cond() = side_effect_expr_nondett(bool_typet(), location);
-    null_check.then_case()=set_null_inst;
-    null_check.else_case()=non_null_inst;
+    code_ifthenelset null_check(
+      side_effect_expr_nondett(bool_typet(), location),
+      std::move(set_null_inst),
+      std::move(non_null_inst));
 
-    new_object_assignments.add(null_check);
+    new_object_assignments.add(std::move(null_check));
   }
 
   // Similarly to above, maybe use a conditional if both the
@@ -872,13 +872,12 @@ void java_object_factoryt::gen_nondet_pointer_init(
     INVARIANT(update_in_place==update_in_placet::MAY_UPDATE_IN_PLACE,
       "No-update and must-update should have already been resolved");
 
-    code_ifthenelset update_check;
-    update_check.cond() =
-      side_effect_expr_nondett(bool_typet(), expr.source_location());
-    update_check.then_case()=update_in_place_assignments;
-    update_check.else_case()=new_object_assignments;
+    code_ifthenelset update_check(
+      side_effect_expr_nondett(bool_typet(), expr.source_location()),
+      std::move(update_in_place_assignments),
+      std::move(new_object_assignments));
 
-    assignments.add(update_check);
+    assignments.add(std::move(update_check));
   }
 }
 
@@ -1461,19 +1460,17 @@ void java_object_factoryt::gen_nondet_array_init(
   code_labelt init_done_label(done_name, code_skipt());
   code_gotot goto_done(done_name);
 
-  code_ifthenelset done_test;
-  done_test.cond()=equal_exprt(counter_expr, length_expr);
-  done_test.then_case()=goto_done;
+  const code_ifthenelset done_test(
+    equal_exprt(counter_expr, length_expr), goto_done);
 
   assignments.add(std::move(done_test));
 
   if(update_in_place!=update_in_placet::MUST_UPDATE_IN_PLACE)
   {
     // Add a redundant if(counter == max_length) break
     // that is easier for the unwinder to understand.
-    code_ifthenelset max_test;
-    max_test.cond()=equal_exprt(counter_expr, max_length_expr);
-    max_test.then_case()=goto_done;
+    code_ifthenelset max_test(
+      equal_exprt(counter_expr, max_length_expr), std::move(goto_done));
 
     assignments.add(std::move(max_test));
   }

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -510,12 +510,12 @@ code_blockt get_thread_safe_clinit_wrapper_body(
 
   // if(C::__CPROVER_PREFIX_clinit_thread_local_state == INIT_COMPLETE) return;
   {
-    code_ifthenelset conditional;
-    conditional.cond() = gen_clinit_eqexpr(
-      clinit_thread_local_state_sym.symbol_expr(),
-      clinit_statest::INIT_COMPLETE);
-    conditional.then_case() = code_returnt();
-    function_body.add(conditional);
+    code_ifthenelset conditional(
+      gen_clinit_eqexpr(
+        clinit_thread_local_state_sym.symbol_expr(),
+        clinit_statest::INIT_COMPLETE),
+      code_returnt());
+    function_body.add(std::move(conditional));
   }
 
   // C::__CPROVER_PREFIX_clinit_thread_local_state = INIT_COMPLETE;
@@ -550,25 +550,21 @@ code_blockt get_thread_safe_clinit_wrapper_body(
   //   init_complete = true;
   // }
   {
-    code_ifthenelset not_init_conditional;
-    code_blockt then_block;
-    not_init_conditional.cond() = gen_clinit_eqexpr(
-      clinit_state_sym.symbol_expr(), clinit_statest::NOT_INIT);
-    then_block.add(
-      gen_clinit_assign(
-        clinit_state_sym.symbol_expr(), clinit_statest::IN_PROGRESS));
-    then_block.add(code_assignt(init_complete.symbol_expr(), false_exprt()));
-    not_init_conditional.then_case() = then_block;
-
-    code_ifthenelset init_conditional;
-    code_blockt init_conditional_body;
-    init_conditional.cond() = gen_clinit_eqexpr(
-      clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE);
-    init_conditional_body.add(
-      code_assignt(init_complete.symbol_expr(), true_exprt()));
-    init_conditional.then_case() = init_conditional_body;
-    not_init_conditional.else_case() = init_conditional;
-    function_body.add(not_init_conditional);
+    code_ifthenelset init_conditional(
+      gen_clinit_eqexpr(
+        clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE),
+      code_blockt({code_assignt(init_complete.symbol_expr(), true_exprt())}));
+
+    code_ifthenelset not_init_conditional(
+      gen_clinit_eqexpr(
+        clinit_state_sym.symbol_expr(), clinit_statest::NOT_INIT),
+      code_blockt(
+        {gen_clinit_assign(
+           clinit_state_sym.symbol_expr(), clinit_statest::IN_PROGRESS),
+         code_assignt(init_complete.symbol_expr(), false_exprt())}),
+      std::move(init_conditional));
+
+    function_body.add(std::move(not_init_conditional));
   }
 
   // ATOMIC_END
@@ -578,10 +574,8 @@ code_blockt get_thread_safe_clinit_wrapper_body(
 
   // if(init_complete) return;
   {
-    code_ifthenelset conditional;
-    conditional.cond() = init_complete.symbol_expr();
-    conditional.then_case() = code_returnt();
-    function_body.add(conditional);
+    code_ifthenelset conditional(init_complete.symbol_expr(), code_returnt());
+    function_body.add(std::move(conditional));
   }
 
   // Initialize the super-class C' and
@@ -680,12 +674,6 @@ code_ifthenelset get_clinit_wrapper_body(
     already_run_symbol.symbol_expr(),
     false_exprt());
 
-  // the entire body of the function is an if-then-else
-  code_ifthenelset wrapper_body;
-
-  // add the condition to the if
-  wrapper_body.cond() = check_already_run;
-
   // add the "already-run = false" statement
   code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt());
   code_blockt init_body({set_already_run});
@@ -698,9 +686,8 @@ code_ifthenelset get_clinit_wrapper_body(
     object_factory_parameters,
     pointer_type_selector);
 
-  wrapper_body.then_case() = init_body;
-
-  return wrapper_body;
+  // the entire body of the function is an if-then-else
+  return code_ifthenelset(std::move(check_already_run), std::move(init_body));
 }
 
 

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -1065,12 +1065,11 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
     str, string_expr_list[0], symbol_table, true);
   for(std::size_t i=1; i<condition_list.size(); i++)
   {
-    code_ifthenelset ife;
-    ife.cond()=condition_list[i];
-    ife.then_case() = code_assign_string_expr_to_java_string(
-      str, string_expr_list[i], symbol_table, true);
-    ife.else_case()=tmp_code;
-    tmp_code=ife;
+    tmp_code = code_ifthenelset(
+      condition_list[i],
+      code_assign_string_expr_to_java_string(
+        str, string_expr_list[i], symbol_table, true),
+      tmp_code);
   }
   code.add(tmp_code, loc);
 

jbmc/src/java_bytecode/remove_instanceof.cpp

@@ -134,13 +134,6 @@ bool remove_instanceoft::lower_instanceof(
   // possible values of T.
   // (http://docs.oracle.com/javase/specs/jls/se7/html/jls-15.html#jls-15.20.2)
 
-  code_ifthenelset is_null_branch;
-  is_null_branch.cond() =
-    equal_exprt(
-      check_ptr, null_pointer_exprt(to_pointer_type(check_ptr.type())));
-  is_null_branch.then_case() =
-    code_assignt(instanceof_result_sym.symbol_expr(), false_exprt());
-
   code_blockt else_block;
   else_block.add(code_declt(clsid_tmp_sym.symbol_expr()));
   else_block.add(code_assignt(clsid_tmp_sym.symbol_expr(), object_clsid));
@@ -155,7 +148,11 @@ bool remove_instanceoft::lower_instanceof(
   else_block.add(
     code_assignt(instanceof_result_sym.symbol_expr(), disjunction(or_ops)));
 
-  is_null_branch.else_case() = std::move(else_block);
+  const code_ifthenelset is_null_branch(
+    equal_exprt(
+      check_ptr, null_pointer_exprt(to_pointer_type(check_ptr.type()))),
+    code_assignt(instanceof_result_sym.symbol_expr(), false_exprt()),
+    std::move(else_block));
 
   // Replace the instanceof construct with instanceof_result:
   expr = instanceof_result_sym.symbol_expr();

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -187,10 +187,10 @@ void symbol_factoryt::gen_nondet_init(
       auto set_null_inst=code_assignt(expr, null_pointer_exprt(pointer_type));
       set_null_inst.add_source_location()=loc;
 
-      code_ifthenelset null_check;
-      null_check.cond() = side_effect_expr_nondett(bool_typet(), loc);
-      null_check.then_case()=set_null_inst;
-      null_check.else_case()=non_null_inst;
+      code_ifthenelset null_check(
+        side_effect_expr_nondett(bool_typet(), loc),
+        std::move(set_null_inst),
+        std::move(non_null_inst));
 
       assignments.add(std::move(null_check));
     }