byte_extract lowering for complex_typet

It may have worked before via the fallback to flattening of the entire
expression to a bitvector, but let's be on the safe side and construct
appropriate expressions.

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -180,7 +180,46 @@ static exprt unpack_rec(
       max_bytes,
       ns);
   }
-  else if(ns.follow(src.type()).id()==ID_struct)
+  else if(src.type().id() == ID_complex)
+  {
+    const complex_typet &complex_type = to_complex_type(src.type());
+    const typet &subtype = complex_type.subtype();
+
+    auto subtype_bits = pointer_offset_bits(subtype, ns);
+    CHECK_RETURN(subtype_bits.has_value());
+
+    exprt::operandst byte_operands;
+
+    exprt sub_real = unpack_rec(
+      complex_real_exprt(src),
+      little_endian,
+      mp_integer{0},
+      *subtype_bits / 8,
+      ns,
+      true);
+    byte_operands.insert(
+      byte_operands.end(),
+      sub_real.operands().begin(),
+      sub_real.operands().end());
+
+    exprt sub_imag = unpack_rec(
+      complex_imag_exprt(src),
+      little_endian,
+      mp_integer{0},
+      *subtype_bits / 8,
+      ns,
+      true);
+    byte_operands.insert(
+      byte_operands.end(),
+      sub_imag.operands().begin(),
+      sub_imag.operands().end());
+
+    const std::size_t size = byte_operands.size();
+    return array_exprt(
+      std::move(byte_operands),
+      array_typet(unsignedbv_typet(8), from_integer(size, size_type())));
+  }
+  else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
   {
     const struct_typet &struct_type=to_struct_type(ns.follow(src.type()));
     const struct_typet::componentst &components=struct_type.components();
@@ -478,7 +517,33 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
       return simplify_expr(vector, ns);
     }
   }
-  else if(ns.follow(src.type()).id()==ID_struct)
+  else if(src.type().id() == ID_complex)
+  {
+    const complex_typet &complex_type = to_complex_type(src.type());
+    const typet &subtype = complex_type.subtype();
+
+    auto subtype_bits = pointer_offset_bits(subtype, ns);
+    if(subtype_bits.has_value())
+    {
+      byte_extract_exprt real(unpacked);
+      real.type() = subtype;
+
+      const plus_exprt new_offset(
+        unpacked.offset(),
+        from_integer(*subtype_bits / 8, unpacked.offset().type()));
+      byte_extract_exprt imag(unpacked);
+      imag.type() = subtype;
+      imag.offset() = simplify_expr(new_offset, ns);
+
+      return simplify_expr(
+        complex_exprt(
+          lower_byte_extract(real, ns),
+          lower_byte_extract(imag, ns),
+          complex_type),
+        ns);
+    }
+  }
+  else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
   {
     const struct_typet &struct_type=to_struct_type(ns.follow(src.type()));
     const struct_typet::componentst &components=struct_type.components();

unit/solvers/lowering/byte_operators.cpp

@@ -158,6 +158,8 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
       // pointer_typet(u64, 64),
       vector_typet(u8, size),
       vector_typet(u64, size),
+      // seems to generate the correct value, but the simplifier needs to learn
+      // about complex_exprt, complex_real_exprt, complex_imag_exprt
       // complex_typet(s16),
       // complex_typet(u64)
     };