Skip to content

Deprecate multi-argument variants of exprt::copy_to_operands #6671

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.

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
Show file tree
Hide file tree
Changes from all commits
Commits
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
3 changes: 1 addition & 2 deletions jbmc/src/java_bytecode/remove_java_new.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -280,8 +280,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
const auto zero_element =
zero_initializer(data.type().subtype(), location, ns);
CHECK_RETURN(zero_element.has_value());
codet array_set(ID_array_set);
array_set.copy_to_operands(new_array_data_symbol, *zero_element);
codet array_set{ID_array_set, {new_array_data_symbol, *zero_element}};
dest.insert_before(next, goto_programt::make_other(array_set, location));
}

Expand Down
8 changes: 4 additions & 4 deletions src/ansi-c/c_typecheck_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1035,8 +1035,8 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
// It is not obvious whether the type or 'e' should be evaluated
// first.

exprt comma_expr(ID_comma, expr.type());
comma_expr.copy_to_operands(side_effect_expr, expr);
binary_exprt comma_expr{
std::move(side_effect_expr), ID_comma, expr, expr.type()};
expr.swap(comma_expr);
}
}
Expand Down Expand Up @@ -1085,8 +1085,8 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
// It is not obvious whether the type or 'e' should be evaluated
// first.

exprt comma_expr(ID_comma, op.type());
comma_expr.copy_to_operands(side_effect_expr, op);
binary_exprt comma_expr{
std::move(side_effect_expr), ID_comma, op, op.type()};
op.swap(comma_expr);
}

Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/builtin_functions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ void goto_convertt::do_prob_uniform(
throw 0;
}

rhs.copy_to_operands(arguments[0], arguments[1]);
rhs.add_to_operands(exprt{arguments[0]}, exprt{arguments[1]});

code_assignt assignment(lhs, rhs);
assignment.add_source_location()=function.source_location();
Expand Down
44 changes: 13 additions & 31 deletions src/goto-programs/goto_convert_side_effect.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -112,29 +112,23 @@ void goto_convertt::remove_assignment(
UNREACHABLE;
}

exprt rhs;

const typet &op0_type = to_binary_expr(expr).op0().type();
const binary_exprt &binary_expr = to_binary_expr(expr);
const typet &op0_type = binary_expr.op0().type();

PRECONDITION(
op0_type.id() != ID_c_enum_tag && op0_type.id() != ID_c_enum &&
op0_type.id() != ID_c_bool && op0_type.id() != ID_bool);

rhs.id(new_id);
rhs.copy_to_operands(
to_binary_expr(expr).op0(), to_binary_expr(expr).op1());
rhs.type() = to_binary_expr(expr).op0().type();
exprt rhs = binary_exprt{binary_expr.op0(), new_id, binary_expr.op1()};
rhs.add_source_location() = expr.source_location();

if(
result_is_used && !address_taken &&
needs_cleaning(to_binary_expr(expr).op0()))
if(result_is_used && !address_taken && needs_cleaning(binary_expr.op0()))
{
make_temp_symbol(rhs, "assign", dest, mode);
replacement_expr_opt = rhs;
}

exprt new_lhs = skip_typecast(to_binary_expr(expr).op0());
exprt new_lhs = skip_typecast(binary_expr.op0());
rhs = typecast_exprt::conditional_cast(rhs, new_lhs.type());
rhs.add_source_location() = expr.source_location();
code_assignt assignment(new_lhs, rhs);
Expand Down Expand Up @@ -196,14 +190,6 @@ void goto_convertt::remove_pre(
statement == ID_preincrement || statement == ID_predecrement,
"expects preincrement or predecrement");

exprt rhs;
rhs.add_source_location()=expr.source_location();

if(statement==ID_preincrement)
rhs.id(ID_plus);
else
rhs.id(ID_minus);

const auto &op = to_unary_expr(expr).op();
const typet &op_type = op.type();

Expand Down Expand Up @@ -233,8 +219,9 @@ void goto_convertt::remove_pre(
else
constant = from_integer(1, constant_type);

rhs.add_to_operands(op, std::move(constant));
rhs.type() = op.type();
exprt rhs = binary_exprt{
op, statement == ID_preincrement ? ID_plus : ID_minus, std::move(constant)};
rhs.add_source_location() = expr.source_location();

const bool cannot_use_lhs =
result_is_used && !address_taken && needs_cleaning(op);
Expand Down Expand Up @@ -282,14 +269,6 @@ void goto_convertt::remove_post(
statement == ID_postincrement || statement == ID_postdecrement,
"expects postincrement or postdecrement");

exprt rhs;
rhs.add_source_location()=expr.source_location();

if(statement==ID_postincrement)
rhs.id(ID_plus);
else
rhs.id(ID_minus);

const auto &op = to_unary_expr(expr).op();
const typet &op_type = op.type();

Expand Down Expand Up @@ -319,8 +298,11 @@ void goto_convertt::remove_post(
else
constant = from_integer(1, constant_type);

rhs.add_to_operands(op, std::move(constant));
rhs.type() = op.type();
binary_exprt rhs{
op,
statement == ID_postincrement ? ID_plus : ID_minus,
std::move(constant)};
rhs.add_source_location() = expr.source_location();

code_assignt assignment(op, rhs);
assignment.add_source_location()=expr.find_source_location();
Expand Down
2 changes: 1 addition & 1 deletion src/jsil/jsil_convert.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ bool jsil_convertt::convert_code(const symbolt &symbol, codet &code)
code_try_catcht t_c(std::move(t));
// Adding empty symbol to catch decl
code_frontend_declt d(symbol_exprt::typeless("decl_symbol"));
t_c.add_catch(d, g);
t_c.add_catch(std::move(d), std::move(g));
t_c.add_source_location()=code.source_location();

code.swap(t_c);
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/flattening/boolbv_get.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -356,7 +356,7 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
it++)
{
exprt index=from_integer(it->first, size.type());
result.copy_to_operands(index, it->second);
result.add_to_operands(std::move(index), exprt{it->second});
}
}
else
Expand Down
6 changes: 3 additions & 3 deletions src/solvers/lowering/byte_operators.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1408,7 +1408,7 @@ static exprt lower_byte_update_byte_array_vector(
{
const exprt &element = value_as_byte_array.operands()[i];

const exprt where = simplify_expr(
exprt where = simplify_expr(
plus_exprt{src.offset(), from_integer(i, src.offset().type())}, ns);

// skip elements that wouldn't change (skip over typecasts as we might have
Expand Down Expand Up @@ -1437,9 +1437,9 @@ static exprt lower_byte_update_byte_array_vector(
update_value = typecast_exprt::conditional_cast(element, subtype);

if(result.id() != ID_with)
result = with_exprt{result, where, update_value};
result = with_exprt{result, std::move(where), std::move(update_value)};
else
result.add_to_operands(where, update_value);
result.add_to_operands(std::move(where), std::move(update_value));
}

return simplify_expr(std::move(result), ns);
Expand Down
5 changes: 5 additions & 0 deletions src/util/expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
#define CPROVER_UTIL_EXPR_H

#include "as_const.h"
#include "deprecate.h"
#include "type.h"
#include "validate_expressions.h"
#include "validate_types.h"
Expand Down Expand Up @@ -148,6 +149,7 @@ class exprt:public irept
/// Copy the given arguments to the end of `exprt`'s operands.
/// \param e1: first `exprt` to append to the operands
/// \param e2: second `exprt` to append to the operands
DEPRECATED(SINCE(2022, 2, 15, "use add_to_operands(&&, &&) instead"))
void copy_to_operands(const exprt &e1, const exprt &e2)
{
operandst &op = operands();
Expand All @@ -161,6 +163,7 @@ class exprt:public irept
/// Add the given arguments to the end of `exprt`'s operands.
/// \param e1: first `exprt` to append to the operands
/// \param e2: second `exprt` to append to the operands
DEPRECATED(SINCE(2022, 2, 15, "use add_to_operands(&&, &&) instead"))
void add_to_operands(const exprt &e1, const exprt &e2)
{
copy_to_operands(e1, e2);
Expand All @@ -183,6 +186,7 @@ class exprt:public irept
/// \param e1: first `exprt` to append to the operands
/// \param e2: second `exprt` to append to the operands
/// \param e3: third `exprt` to append to the operands
DEPRECATED(SINCE(2022, 2, 15, "use add_to_operands(&&, &&, &&) instead"))
void add_to_operands(const exprt &e1, const exprt &e2, const exprt &e3)
{
copy_to_operands(e1, e2, e3);
Expand All @@ -192,6 +196,7 @@ class exprt:public irept
/// \param e1: first `exprt` to append to the operands
/// \param e2: second `exprt` to append to the operands
/// \param e3: third `exprt` to append to the operands
DEPRECATED(SINCE(2022, 2, 15, "use add_to_operands(&&, &&, &&) instead"))
void copy_to_operands(const exprt &e1, const exprt &e2, const exprt &e3)
{
operandst &op = operands();
Expand Down
4 changes: 2 additions & 2 deletions src/util/std_code.h
Original file line number Diff line number Diff line change
Expand Up @@ -2025,9 +2025,9 @@ class code_try_catcht:public codet
return to_code(operands()[2*i+2]);
}

void add_catch(const code_frontend_declt &to_catch, const codet &code_catch)
void add_catch(code_frontend_declt &&to_catch, codet &&code_catch)
{
add_to_operands(to_catch, code_catch);
add_to_operands(std::move(to_catch), std::move(code_catch));
}

protected:
Expand Down