Skip to content

Use constructors with fewer parameters if possible, for dereference_exprt and plus_exprt #4524

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
Apr 13, 2019
Merged

Use constructors with fewer parameters if possible, for dereference_exprt and plus_exprt #4524

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
fda5ca0
Use single-parameter dereference_exprt constructor if possible
antlechner Apr 12, 2019
cdb0133
Use plus_exprt constructor that does not take a type
antlechner Apr 12, 2019
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
4 changes: 2 additions & 2 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 @@ -867,8 +867,8 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
location.set_function(local_name);
side_effect_exprt java_new_array(
ID_java_new_array, java_reference_type(struct_tag_type), location);
dereference_exprt old_array(this_symbol.symbol_expr(), struct_tag_type);
dereference_exprt new_array(local_symexpr, struct_tag_type);
dereference_exprt old_array{this_symbol.symbol_expr()};
dereference_exprt new_array{local_symexpr};
Copy link
Collaborator

Choose a reason for hiding this comment

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

So in order to confirm that this is correct I had to read some more code, and the same is happening below: apologies that I'll come up with (almost) unrelated requests for fixes. For this one: local_symexpr is declared as a const reference, but .symbol_expr returns by value, so that's a reference to a temporary. Can you please remove the reference from local_symexpr?

member_exprt old_length(
old_array, length_component.get_name(), length_component.type());
java_new_array.copy_to_operands(old_length);
Expand Down
16 changes: 7 additions & 9 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 @@ -1623,7 +1623,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(

const typecast_exprt pointer(op[0], java_array_type(statement[0]));

dereference_exprt array(pointer, pointer.type().subtype());
dereference_exprt array{pointer};
Copy link
Collaborator

Choose a reason for hiding this comment

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

We should actually use either std::move(pointer) (and get rid of the const) or just do array{typecast_exprt{op[0], java_array_type(statement[0])}}. Applies here and in several other places.

PRECONDITION(pointer.type().subtype().id() == ID_struct_tag);
Copy link
Collaborator

Choose a reason for hiding this comment

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

I have no idea why this PRECONDITION is important right here, but if it for some reason needs to be enforced: PRECONDITION(array.type().id() == ID_struct_tag) would be less opaque - but actually makes me wonder whether the name array is a particularly good choice?

array.set(ID_java_member_access, true);

Expand Down Expand Up @@ -2832,17 +2832,16 @@ exprt java_bytecode_convert_methodt::convert_aload(
const char &type_char = statement[0];
const typecast_exprt pointer(op[0], java_array_type(type_char));

dereference_exprt deref(pointer, pointer.type().subtype());
dereference_exprt deref{pointer};
deref.set(ID_java_member_access, true);

const member_exprt data_ptr(
deref, "data", pointer_type(java_type_from_char(type_char)));

plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type());
plus_exprt data_plus_offset{data_ptr, op[1]};
// tag it so it's easy to identify during instrumentation
data_plus_offset.set(ID_java_array_access, true);
const typet &element_type = data_ptr.type().subtype();
const dereference_exprt element(data_plus_offset, element_type);
const dereference_exprt element{data_plus_offset};
return java_bytecode_promotion(element);
}

Expand Down Expand Up @@ -2881,17 +2880,16 @@ code_blockt java_bytecode_convert_methodt::convert_astore(
const char type_char = statement[0];
const typecast_exprt pointer(op[0], java_array_type(type_char));

dereference_exprt deref(pointer, pointer.type().subtype());
dereference_exprt deref{pointer};
deref.set(ID_java_member_access, true);

const member_exprt data_ptr(
deref, "data", pointer_type(java_type_from_char(type_char)));

plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type());
plus_exprt data_plus_offset{data_ptr, op[1]};
// tag it so it's easy to identify during instrumentation
data_plus_offset.set(ID_java_array_access, true);
const typet &element_type = data_ptr.type().subtype();
const dereference_exprt element(data_plus_offset, element_type);
const dereference_exprt element{data_plus_offset};

code_blockt block;
block.add_source_location() = location;
Expand Down
10 changes: 4 additions & 6 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 @@ -1102,8 +1102,7 @@ void java_object_factoryt::array_primitive_init_code(

// *array_data_init = NONDET(TYPE [max_length_expr]);
side_effect_expr_nondett nondet_data(array_type, location);
const dereference_exprt data_pointer_deref(
tmp_finite_array_pointer, array_type);
const dereference_exprt data_pointer_deref{tmp_finite_array_pointer};
Copy link
Collaborator

@tautschnig tautschnig Apr 12, 2019 •
edited
Loading

Choose a reason for hiding this comment

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

Get rid of const and use std::move(data_pointer_deref) below.

assignments.add(code_assignt(data_pointer_deref, std::move(nondet_data)));
assignments.statements().back().add_source_location() = location;

Expand Down Expand Up @@ -1201,9 +1200,8 @@ void java_object_factoryt::array_loop_init_code(
assignments.add(std::move(max_test));
}

const dereference_exprt arraycellref(
plus_exprt(array_init_symexpr, counter_expr, array_init_symexpr.type()),
array_init_symexpr.type().subtype());
const dereference_exprt arraycellref{
plus_exprt{array_init_symexpr, counter_expr}};

bool new_item_is_primitive = arraycellref.type().id() != ID_pointer;

Expand Down Expand Up @@ -1303,7 +1301,7 @@ void java_object_factoryt::gen_nondet_array_init(
is_valid_java_array(struct_type),
"Java struct array does not conform to expectations");

dereference_exprt deref_expr(expr, expr.type().subtype());
dereference_exprt deref_expr(expr);
Copy link
Collaborator

Choose a reason for hiding this comment

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

Braces (as introduced in all the other places)

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I knew I would forget them somewhere!

const auto &comps = struct_type.components();
const member_exprt length_expr(deref_expr, "length", comps[1].type());
exprt init_array_expr = member_exprt(deref_expr, "data", comps[2].type());
Expand Down
4 changes: 1 addition & 3 deletions jbmc/src/java_bytecode/java_pointer_casts.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,9 +21,7 @@ Author: Daniel Kroening, [email protected]
/// \return dereferenced pointer
static exprt clean_deref(const exprt &ptr)
{
return ptr.id()==ID_address_of
? ptr.op0()
: dereference_exprt(ptr, ptr.type().subtype());
return ptr.id() == ID_address_of ? ptr.op0() : dereference_exprt{ptr};
}

/// \par parameters: pointer
Expand Down
2 changes: 1 addition & 1 deletion 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 @@ -602,7 +602,7 @@ exprt make_nondet_infinite_char_array(
code.add(code_declt(data_pointer));
code.add(make_allocate_code(data_pointer, array_type.size()));
const exprt nondet_data = side_effect_expr_nondett(array_type, loc);
const exprt data = dereference_exprt(data_pointer, array_type);
const exprt data = dereference_exprt{data_pointer};
code.add(code_assignt(data, nondet_data), loc);
return data;
}
Expand Down
4 changes: 2 additions & 2 deletions src/analyses/goto_check.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1106,7 +1106,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)

binary_relation_exprt lb_check(a.first, ID_le, int_ptr);

plus_exprt ub(int_ptr, size, int_ptr.type());
plus_exprt ub{int_ptr, size};

binary_relation_exprt ub_check(ub, ID_le, plus_exprt(a.first, a.second));

Expand Down Expand Up @@ -1576,7 +1576,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
const exprt new_address_casted =
typecast_exprt::conditional_cast(new_address, new_pointer_type);

dereference_exprt new_deref(new_address_casted, expr.type());
dereference_exprt new_deref{new_address_casted};
new_deref.add_source_location() = deref.source_location();
pointer_validity_check(new_deref, guard);

Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/c_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2009,7 +2009,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
}
else
{
dereference_exprt tmp(f_op, f_op_type.subtype());
dereference_exprt tmp{f_op};
tmp.set(ID_C_implicit, true);
tmp.add_source_location()=f_op.source_location();
f_op.swap(tmp);
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/wmm/shared_buffers.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1214,7 +1214,7 @@ void shared_bufferst::cfg_visitort::weak_memory(
read_delayed_expr,
if_exprt(
choice1_expr,
dereference_exprt(new_read_expr, vars.type),
dereference_exprt{new_read_expr},
to_replace_expr),
to_replace_expr); // original_instruction.code.op1());

Expand Down
12 changes: 6 additions & 6 deletions src/goto-programs/builtin_functions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -299,7 +299,7 @@ void goto_convertt::do_scanf(
copy(array_copy_statement, OTHER, dest);
#else
const index_exprt new_lhs(
dereference_exprt(ptr, *type), from_integer(0, index_type()));
dereference_exprt{ptr}, from_integer(0, index_type()));
const side_effect_expr_nondett rhs(
type->subtype(), function.source_location());
code_assignt assign(new_lhs, rhs);
Expand All @@ -310,7 +310,7 @@ void goto_convertt::do_scanf(
else
{
// make it nondet for now
const dereference_exprt new_lhs(ptr, *type);
const dereference_exprt new_lhs{ptr};
const side_effect_expr_nondett rhs(
*type, function.source_location());
code_assignt assign(new_lhs, rhs);
Expand Down Expand Up @@ -1222,7 +1222,7 @@ void goto_convertt::do_function_call_symbol(
}

// build *ptr
dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
dereference_exprt deref_ptr{arguments[0]};

dest.add(goto_programt::make_atomic_begin(function.source_location()));

Expand Down Expand Up @@ -1287,7 +1287,7 @@ void goto_convertt::do_function_call_symbol(
}

// build *ptr
dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
dereference_exprt deref_ptr{arguments[0]};

dest.add(goto_programt::make_atomic_begin(function.source_location()));

Expand Down Expand Up @@ -1356,7 +1356,7 @@ void goto_convertt::do_function_call_symbol(
}

// build *ptr
dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
dereference_exprt deref_ptr{arguments[0]};

dest.add(goto_programt::make_atomic_begin(function.source_location()));

Expand Down Expand Up @@ -1412,7 +1412,7 @@ void goto_convertt::do_function_call_symbol(
}

// build *ptr
dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
dereference_exprt deref_ptr{arguments[0]};

dest.add(goto_programt::make_atomic_begin(function.source_location()));

Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/class_identifier.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ exprt get_class_identifier_field(
const auto &points_to=this_expr.type().subtype();
if(points_to==empty_typet())
this_expr=typecast_exprt(this_expr, pointer_type(suggested_type));
const dereference_exprt deref(this_expr, this_expr.type().subtype());
const dereference_exprt deref{this_expr};
return build_class_identifier(deref, ns);
}

Expand Down
9 changes: 4 additions & 5 deletions src/goto-programs/string_abstraction.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -964,7 +964,7 @@ bool string_abstractiont::build_symbol(const symbol_exprt &sym, exprt &dest)
dest=str_symbol.symbol_expr();
if(current_args.find(symbol.name)!=current_args.end() &&
!is_ptr_argument(abstract_type))
dest=dereference_exprt(dest, dest.type().subtype());
dest = dereference_exprt{dest};

return false;
}
Expand Down Expand Up @@ -1218,10 +1218,9 @@ goto_programt::targett string_abstractiont::value_assignments(
index_exprt(lhs, from_integer(i, a_size.type())),
index_exprt(rhs, from_integer(i, a_size.type())));
}
else if(lhs.type().id()==ID_pointer)
return value_assignments(dest, target,
dereference_exprt(lhs, lhs.type().subtype()),
dereference_exprt(rhs, rhs.type().subtype()));
else if(lhs.type().id() == ID_pointer)
return value_assignments(
dest, target, dereference_exprt{lhs}, dereference_exprt{rhs});
Copy link
Collaborator

Choose a reason for hiding this comment

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

Please add braces as this is (always was) a multi-line statement in the body of an if.

else if(lhs.type()==string_struct)
return value_assignments_string_struct(dest, target, lhs, rhs);
else if(lhs.type().id()==ID_struct || lhs.type().id()==ID_union)
Expand Down
6 changes: 2 additions & 4 deletions src/goto-programs/string_instrumentation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -552,9 +552,7 @@ void string_instrumentationt::do_format_string_write(
default: // everything else
{
const exprt &argument=arguments[argument_start_inx+args];
const typet &arg_type = argument.type();

const dereference_exprt lhs(argument, arg_type.subtype());
const dereference_exprt lhs{argument};

side_effect_expr_nondett rhs(lhs.type(), target->source_location);

Expand Down Expand Up @@ -594,7 +592,7 @@ void string_instrumentationt::do_format_string_write(
}
else
{
dereference_exprt lhs(arguments[i], arg_type.subtype());
dereference_exprt lhs{arguments[i]};

side_effect_expr_nondett rhs(lhs.type(), target->source_location);

Expand Down
3 changes: 1 addition & 2 deletions src/goto-symex/symex_dereference.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -255,8 +255,7 @@ void goto_symext::dereference_rec(exprt &expr, statet &state)
address_of_exprt address_of_expr(index_expr.array());
address_of_expr.type()=pointer_type(expr.type());

dereference_exprt tmp(
plus_exprt(address_of_expr, index_expr.index()), expr.type());
dereference_exprt tmp{plus_exprt{address_of_expr, index_expr.index()}};
tmp.add_source_location()=expr.source_location();

// recursive call
Expand Down
2 changes: 1 addition & 1 deletion src/pointer-analysis/value_set_dereference.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -306,7 +306,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
result.pointer_guard = dynamic_object(pointer_expr);

// can't remove here, turn into *p
result.value=dereference_exprt(pointer_expr, dereference_type);
result.value = dereference_exprt{pointer_expr};
}
else if(root_object.id()==ID_integer_address)
{
Expand Down
5 changes: 1 addition & 4 deletions src/solvers/smt2/smt2_conv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -561,10 +561,7 @@ void smt2_convt::convert_address_of_rec(
new_index_expr,
pointer_type(array.type().subtype()));

plus_exprt plus_expr(
address_of_expr,
index,
address_of_expr.type());
plus_exprt plus_expr{address_of_expr, index};

convert_expr(plus_expr);
}
Expand Down
4 changes: 2 additions & 2 deletions src/util/simplify_expr_pointer.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ bool simplify_exprt::simplify_address_of_arg(exprt &expr)
from_integer((*step_size) * (*index) + address, index_type()),
pointer_type);

expr = dereference_exprt(typecast_expr, expr.type());
expr = dereference_exprt{typecast_expr};
result = true;
}
}
Expand Down Expand Up @@ -124,7 +124,7 @@ bool simplify_exprt::simplify_address_of_arg(exprt &expr)
pointer_type.subtype()=expr.type();
typecast_exprt typecast_expr(
from_integer(address + *offset, index_type()), pointer_type);
expr = dereference_exprt(typecast_expr, expr.type());
expr = dereference_exprt{typecast_expr};
result=true;
}
}
Expand Down