Skip to content

Multi-operand constructor for code_ifthenelset #3504

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Dec 18, 2018
Merged

Multi-operand constructor for code_ifthenelset #3504

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
73ae7a3
Multi-operand constructor for code_ifthenelset
tautschnig Dec 2, 2018
8427934
Use code_ifthenelset constructor
tautschnig Dec 2, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
48 changes: 30 additions & 18 deletions jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

Expand All @@ -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;
}

Expand All @@ -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;
}

Expand All @@ -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;
Expand All @@ -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;
Expand Down
14 changes: 6 additions & 8 deletions jbmc/src/java_bytecode/java_bytecode_instrument.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down Expand Up @@ -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/
Expand Down
31 changes: 14 additions & 17 deletions jbmc/src/java_bytecode/java_object_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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));
}
}

Expand Down Expand Up @@ -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));
}
Expand Down
63 changes: 25 additions & 38 deletions jbmc/src/java_bytecode/java_static_initializers.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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
Expand All @@ -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));
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No need for the temporary conditional any longer?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

True, but I still left it in place as the line otherwise got long-ish. But if anyone thinks it should rather be removed then I'll happily do so.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BTW, the combination of 'const' and std::move won't do anything.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed.

}

// Initialize the super-class C' and
Expand Down Expand Up @@ -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});
Expand All @@ -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));
}


Expand Down
11 changes: 5 additions & 6 deletions jbmc/src/java_bytecode/java_string_library_preprocess.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);

Expand Down
13 changes: 5 additions & 8 deletions jbmc/src/java_bytecode/remove_instanceof.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand All @@ -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();
Expand Down
8 changes: 4 additions & 4 deletions src/ansi-c/c_nondet_symbol_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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));
}
Expand Down
Loading