Skip to content

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

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 4 commits into from
Oct 7, 2018
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
b032b00
rvalue variants of exprt::copy_to_operands
Oct 3, 2018
16d6934
rvalue variant of code_blockt::add
Oct 3, 2018
1b4c3ac
new constructors for code_blockt
Oct 2, 2018
46232f0
use code_blockt::add and code_blockt constructor for adding a statement
Sep 30, 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
41 changes: 13 additions & 28 deletions jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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});
Copy link
Contributor

Choose a reason for hiding this comment

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

If you're going for this style, could I recommend replacing the constructor for code_blockt that takes a std::list<const codet &> with one taking a std::initializer_list? The former means a bunch of heap allocates and deallocates, whereas the latter is basically a type-safe layer atop varargs.

Copy link
Contributor

Choose a reason for hiding this comment

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

(It could also take universal references, permitting {monitorexit, std::move(code)})

Copy link
Contributor

Choose a reason for hiding this comment

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

(Correction, it's not a wrapper on <stdarg> style varargs as I'd thought, but it is a fixed-size array, probably stack-allocated, which still avoids much of the pointless back-and-forth of a temporary linked list)

Copy link
Contributor

Choose a reason for hiding this comment

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

(You could also use a variadic template... but that's probably more fuss than it's worth when the initializers are monovariant)

Copy link
Member Author

@kroening kroening Oct 2, 2018 •
edited
Loading

Choose a reason for hiding this comment

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

Indeed, there is unnecessary copying going on in the constructor. How about these:

  explicit code_blockt(const std::vector<codet> &_statements):codet(ID_block)
  {
    operands()=(const std::vector<exprt> &)_statements;
  }

  explicit code_blockt(std::vector<codet> &&_statements):codet(ID_block)
  {
    operands()=std::move((std::vector<exprt> &&)_statements);
  }

Copy link
Contributor

Choose a reason for hiding this comment

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

Why not std::initializer_list<codet>? Should be just like vector, except without the heap alloc; plus it's (one of the) new standard ways to do varargs

Copy link
Member Author

Choose a reason for hiding this comment

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

Does that add anything over offering the vector interface? Note that the vector offers a constructor from std::initializer_list, and that the vector needs to exist eventually.

Copy link
Contributor

Choose a reason for hiding this comment

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

I think marginally, but the difference is small so let's go with this. It's definitely much better than std::list for this purpose.

}
else if(
statement == ID_label || statement == ID_block ||
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
12 changes: 3 additions & 9 deletions jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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());
Expand Down Expand Up @@ -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;

Expand All @@ -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;
Expand Down
66 changes: 25 additions & 41 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 @@ -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);
Expand Down Expand Up @@ -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);
}
Expand All @@ -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;
Expand All @@ -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
Expand Down Expand Up @@ -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) &&
Expand Down Expand Up @@ -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;
}
Expand Down Expand Up @@ -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});
}
}

Expand Down Expand Up @@ -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
{
Expand Down Expand Up @@ -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
{
Expand Down Expand Up @@ -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});
}
}
}
Expand All @@ -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;
}
Expand Down Expand Up @@ -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;
}

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

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

Expand Down Expand Up @@ -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);
Copy link
Member

Choose a reason for hiding this comment

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

move?


return block;
}

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

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

Expand Down Expand Up @@ -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;
}
Loading