Introduce complex_imag_exprt and complex_real_exprt

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,

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);
 

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)

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";

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)

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);

src/solvers/flattening/boolbv_complex.cpp

@@ -45,35 +45,29 @@ 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
 
   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);

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<const complex_real_exprt &>(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<complex_real_exprt &>(expr);
+}
+
+template <>
+inline bool can_cast_expr<complex_real_exprt>(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<const complex_imag_exprt &>(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<complex_imag_exprt &>(expr);
+}
+
+template <>
+inline bool can_cast_expr<complex_imag_exprt>(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;