diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 3d3fd80f1f1..4e94f865ac8 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -82,22 +82,29 @@ void rw_range_sett::output(std::ostream &out) const } } -void rw_range_sett::get_objects_complex( +void rw_range_sett::get_objects_complex_real( get_modet mode, - const exprt &expr, + const complex_real_exprt &expr, const range_spect &range_start, const range_spect &size) { - const exprt &op=expr.op0(); - assert(op.type().id()==ID_complex); + get_objects_rec(mode, expr.op(), range_start, size); +} - range_spect sub_size= +void rw_range_sett::get_objects_complex_imag( + get_modet mode, + const complex_imag_exprt &expr, + const range_spect &range_start, + const range_spect &size) +{ + const exprt &op = expr.op(); + + range_spect sub_size = to_range_spect(pointer_offset_bits(op.type().subtype(), ns)); assert(sub_size>0); - range_spect offset= - (range_start==-1 || expr.id()==ID_complex_real) ? 0 : sub_size; + range_spect offset = range_start == -1 ? 0 : sub_size; - get_objects_rec(mode, op, range_start+offset, size); + get_objects_rec(mode, op, range_start + offset, size); } void rw_range_sett::get_objects_if( @@ -487,9 +494,12 @@ void rw_range_sett::get_objects_rec( const range_spect &range_start, const range_spect &size) { - if(expr.id()==ID_complex_real || - expr.id()==ID_complex_imag) - get_objects_complex(mode, expr, range_start, size); + if(expr.id() == ID_complex_real) + get_objects_complex_real( + mode, to_complex_real_expr(expr), range_start, size); + else if(expr.id() == ID_complex_imag) + get_objects_complex_imag( + mode, to_complex_imag_expr(expr), range_start, size); else if(expr.id()==ID_typecast) get_objects_typecast( mode, diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h index dd6c9e63c33..d30d4cabc18 100644 --- a/src/analyses/goto_rw.h +++ b/src/analyses/goto_rw.h @@ -161,9 +161,15 @@ class rw_range_sett get_modet mode, const exprt &expr); - virtual void get_objects_complex( + virtual void get_objects_complex_real( get_modet mode, - const exprt &expr, + const complex_real_exprt &expr, + const range_spect &range_start, + const range_spect &size); + + virtual void get_objects_complex_imag( + get_modet mode, + const complex_imag_exprt &expr, const range_spect &range_start, const range_spect &size); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index dfb9032791c..27df86e07e1 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -320,36 +320,80 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr) // these should only exist as constants, // and should already be typed } - else if(expr.id()==ID_complex_real || - expr.id()==ID_complex_imag) + else if(expr.id() == ID_complex_real) { - // get the subtype - assert(expr.operands().size()==1); - const typet &op_type=follow(expr.op0().type()); - if(op_type.id()!=ID_complex) + INVARIANT( + expr.operands().size() == 1, + "real part retrieval operation should have one operand"); + + exprt op = expr.op0(); + op.type() = follow(op.type()); + + if(op.type().id() != ID_complex) { - if(!is_number(op_type)) + if(!is_number(op.type())) { - err_location(expr.op0()); - error() << "real/imag expect numerical operand, " - << "but got `" << to_string(op_type) << "'" << eom; + err_location(op); + error() << "real part retrieval expects numerical operand, " + << "but got `" << to_string(op.type()) << "'" << eom; throw 0; } - // we could compile away, I suppose - expr.type()=op_type; - expr.op0().make_typecast(complex_typet(op_type)); + typecast_exprt typecast_expr(op, complex_typet(op.type())); + complex_real_exprt complex_real_expr(typecast_expr); + + expr.swap(complex_real_expr); } else { - expr.type()=op_type.subtype(); + complex_real_exprt complex_real_expr(op); // these are lvalues if the operand is one - if(expr.op0().get_bool(ID_C_lvalue)) - expr.set(ID_C_lvalue, true); + if(op.get_bool(ID_C_lvalue)) + complex_real_expr.set(ID_C_lvalue, true); + + if(op.get_bool(ID_C_constant)) + complex_real_expr.set(ID_C_constant, true); + + expr.swap(complex_real_expr); + } + } + else if(expr.id() == ID_complex_imag) + { + INVARIANT( + expr.operands().size() == 1, + "imaginary part retrieval operation should have one operand"); + + exprt op = expr.op0(); + op.type() = follow(op.type()); + + if(op.type().id() != ID_complex) + { + if(!is_number(op.type())) + { + err_location(op); + error() << "real part retrieval expects numerical operand, " + << "but got `" << to_string(op.type()) << "'" << eom; + throw 0; + } + + typecast_exprt typecast_expr(op, complex_typet(op.type())); + complex_imag_exprt complex_imag_expr(typecast_expr); + + expr.swap(complex_imag_expr); + } + else + { + complex_imag_exprt complex_imag_expr(op); + + // these are lvalues if the operand is one + if(op.get_bool(ID_C_lvalue)) + complex_imag_expr.set(ID_C_lvalue, true); + + if(op.get_bool(ID_C_constant)) + complex_imag_expr.set(ID_C_constant, true); - if(expr.op0().get_bool(ID_C_constant)) - expr.set(ID_C_constant, true); + expr.swap(complex_imag_expr); } } else if(expr.id()==ID_generic_selection) diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index ce5d7ee0775..03ab8f10b0a 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -168,28 +168,29 @@ void goto_symext::symex_assign_rec( symex_assign_byte_extract( state, to_byte_extract_expr(lhs), full_lhs, rhs, guard, assignment_type); } - else if(lhs.id()==ID_complex_real || - lhs.id()==ID_complex_imag) + else if(lhs.id() == ID_complex_real) { - // this is stuff like __real__ x = 1; - assert(lhs.operands().size()==1); + const complex_real_exprt &complex_real_expr = to_complex_real_expr(lhs); - exprt new_rhs=exprt(ID_complex, lhs.op0().type()); - new_rhs.operands().resize(2); + const complex_imag_exprt complex_imag_expr(complex_real_expr.op()); - if(lhs.id()==ID_complex_real) - { - new_rhs.op0()=rhs; - new_rhs.op1()=unary_exprt(ID_complex_imag, lhs.op0(), lhs.type()); - } - else - { - new_rhs.op0()=unary_exprt(ID_complex_real, lhs.op0(), lhs.type()); - new_rhs.op1()=rhs; - } + complex_exprt new_rhs( + rhs, complex_imag_expr, to_complex_type(complex_real_expr.op().type())); + + symex_assign_rec( + state, complex_real_expr.op(), full_lhs, new_rhs, guard, assignment_type); + } + else if(lhs.id() == ID_complex_imag) + { + const complex_imag_exprt &complex_imag_expr = to_complex_imag_expr(lhs); + + const complex_real_exprt complex_real_expr(complex_imag_expr.op()); + + complex_exprt new_rhs( + complex_real_expr, rhs, to_complex_type(complex_imag_expr.op().type())); symex_assign_rec( - state, lhs.op0(), full_lhs, new_rhs, guard, assignment_type); + state, complex_imag_expr.op(), full_lhs, new_rhs, guard, assignment_type); } else throw "assignment to `"+lhs.id_string()+"' not handled"; diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 3c5cb3856d8..bcdd6d7e53a 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -279,9 +279,9 @@ bvt boolbvt::convert_bitvector(const exprt &expr) else if(expr.id()==ID_complex) return convert_complex(expr); else if(expr.id()==ID_complex_real) - return convert_complex_real(expr); + return convert_complex_real(to_complex_real_expr(expr)); else if(expr.id()==ID_complex_imag) - return convert_complex_imag(expr); + return convert_complex_imag(to_complex_imag_expr(expr)); else if(expr.id()==ID_lambda) return convert_lambda(expr); else if(expr.id()==ID_array_of) diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 7c166dd2213..640d2764005 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -142,8 +142,8 @@ class boolbvt:public arrayst virtual bvt convert_array(const exprt &expr); virtual bvt convert_vector(const exprt &expr); virtual bvt convert_complex(const exprt &expr); - virtual bvt convert_complex_real(const exprt &expr); - virtual bvt convert_complex_imag(const exprt &expr); + virtual bvt convert_complex_real(const complex_real_exprt &expr); + virtual bvt convert_complex_imag(const complex_imag_exprt &expr); virtual bvt convert_lambda(const exprt &expr); virtual bvt convert_let(const let_exprt &); virtual bvt convert_array_of(const array_of_exprt &expr); diff --git a/src/solvers/flattening/boolbv_complex.cpp b/src/solvers/flattening/boolbv_complex.cpp index 833795be842..daf931cd98d 100644 --- a/src/solvers/flattening/boolbv_complex.cpp +++ b/src/solvers/flattening/boolbv_complex.cpp @@ -45,17 +45,14 @@ bvt boolbvt::convert_complex(const exprt &expr) return conversion_failed(expr); } -bvt boolbvt::convert_complex_real(const exprt &expr) +bvt boolbvt::convert_complex_real(const complex_real_exprt &expr) { std::size_t width=boolbv_width(expr.type()); if(width==0) return conversion_failed(expr); - if(expr.operands().size()!=1) - return conversion_failed(expr); - - bvt bv=convert_bv(expr.op0()); + bvt bv = convert_bv(expr.op()); assert(bv.size()==width*2); bv.resize(width); // chop @@ -63,17 +60,14 @@ bvt boolbvt::convert_complex_real(const exprt &expr) return bv; } -bvt boolbvt::convert_complex_imag(const exprt &expr) +bvt boolbvt::convert_complex_imag(const complex_imag_exprt &expr) { std::size_t width=boolbv_width(expr.type()); if(width==0) return conversion_failed(expr); - if(expr.operands().size()!=1) - return conversion_failed(expr); - - bvt bv=convert_bv(expr.op0()); + bvt bv = convert_bv(expr.op()); assert(bv.size()==width*2); bv.erase(bv.begin(), bv.begin()+width); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 85ca4a6b3a2..6d654de0f61 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -1730,6 +1730,99 @@ inline void validate_expr(const complex_exprt &value) validate_operands(value, 2, "Complex constructor must have two operands"); } +/// \brief Real part of the expression describing a complex number. +class complex_real_exprt : public unary_exprt +{ +public: + explicit complex_real_exprt(const exprt &op) + : unary_exprt(ID_complex_real, op, to_complex_type(op.type()).subtype()) + { + } +}; + +/// \brief Cast an exprt to a \ref complex_real_exprt +/// +/// \a expr must be known to be a \ref complex_real_exprt. +/// +/// \param expr: Source expression +/// \return Object of type \ref complex_real_exprt +inline const complex_real_exprt &to_complex_real_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_complex_real); + DATA_INVARIANT( + expr.operands().size() == 1, + "real part retrieval operation must have one operand"); + return static_cast(expr); +} + +/// \copydoc to_complex_real_expr(const exprt &) +inline complex_real_exprt &to_complex_real_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_complex_real); + DATA_INVARIANT( + expr.operands().size() == 1, + "real part retrieval operation must have one operand"); + return static_cast(expr); +} + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_complex_real; +} + +inline void validate_expr(const complex_real_exprt &expr) +{ + validate_operands( + expr, 1, "real part retrieval operation must have one operand"); +} + +/// \brief Imaginary part of the expression describing a complex number. +class complex_imag_exprt : public unary_exprt +{ +public: + explicit complex_imag_exprt(const exprt &op) + : unary_exprt(ID_complex_imag, op, to_complex_type(op.type()).subtype()) + { + } +}; + +/// \brief Cast an exprt to a \ref complex_imag_exprt +/// +/// \a expr must be known to be a \ref complex_imag_exprt. +/// +/// \param expr: Source expression +/// \return Object of type \ref complex_imag_exprt +inline const complex_imag_exprt &to_complex_imag_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_complex_imag); + DATA_INVARIANT( + expr.operands().size() == 1, + "imaginary part retrieval operation must have one operand"); + return static_cast(expr); +} + +/// \copydoc to_complex_imag_expr(const exprt &) +inline complex_imag_exprt &to_complex_imag_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_complex_imag); + DATA_INVARIANT( + expr.operands().size() == 1, + "imaginary part retrieval operation must have one operand"); + return static_cast(expr); +} + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_complex_imag; +} + +inline void validate_expr(const complex_imag_exprt &expr) +{ + validate_operands( + expr, 1, "imaginary part retrieval operation must have one operand"); +} class namespacet;