Merge pull request #4228 from tautschnig/byte-op-complex_typet

byte_extract lowering for complex_typet [blocks: #2068]

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -351,6 +351,48 @@ static array_exprt unpack_array_vector(
     array_typet(unsignedbv_typet(8), from_integer(size, size_type())));
 }
 
+/// Rewrite a complex_exprt into its individual bytes.
+/// \param src: complex-typed expression to unpack
+/// \param little_endian: true, iff assumed endianness is little-endian
+/// \param ns: namespace for type lookups
+/// \return array_exprt holding unpacked elements
+static array_exprt
+unpack_complex(const exprt &src, bool little_endian, const namespacet &ns)
+{
+  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());
+  CHECK_RETURN(*subtype_bits % 8 == 0);
+
+  exprt sub_real = unpack_rec(
+    complex_real_exprt{src},
+    little_endian,
+    mp_integer{0},
+    *subtype_bits / 8,
+    ns,
+    true);
+  exprt::operandst byte_operands = std::move(sub_real.operands());
+
+  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(),
+    std::make_move_iterator(sub_imag.operands().begin()),
+    std::make_move_iterator(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())}};
+}
+
 /// Rewrite an object into its individual bytes.
 /// \param src: object to unpack
 /// \param little_endian: true, iff assumed endianness is little-endian
@@ -415,7 +457,11 @@ static exprt unpack_rec(
       max_bytes,
       ns);
   }
-  else if(ns.follow(src.type()).id()==ID_struct)
+  else if(src.type().id() == ID_complex)
+  {
+    return unpack_complex(src, little_endian, 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();
@@ -573,6 +619,43 @@ static exprt unpack_rec(
     {}, array_typet(unsignedbv_typet(8), from_integer(0, size_type())));
 }
 
+/// Rewrite a byte extraction of a complex-typed result to byte extraction of
+/// the individual components that make up a \ref complex_exprt.
+/// \param src: Original byte extract expression
+/// \param unpacked: Byte extraction with root operand expanded into array (via
+///   \ref unpack_rec)
+/// \param ns: Namespace
+/// \return An expression if the subtype size is known, else `nullopt` so that a
+/// fall-back to more generic code can be used.
+static optionalt<exprt> lower_byte_extract_complex(
+  const byte_extract_exprt &src,
+  const byte_extract_exprt &unpacked,
+  const namespacet &ns)
+{
+  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() || *subtype_bits % 8 != 0)
+    return {};
+
+  // offset remains unchanged
+  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);
+}
+
 /// rewrite byte extraction from an array to byte extraction from a
 /// concatenation of array index expressions
 exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
@@ -712,7 +795,15 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
       return simplify_expr(vector_exprt(std::move(operands), vector_type), ns);
     }
   }
-  else if(ns.follow(src.type()).id()==ID_struct)
+  else if(src.type().id() == ID_complex)
+  {
+    auto result = lower_byte_extract_complex(src, unpacked, ns);
+    if(result.has_value())
+      return std::move(*result);
+
+    // else fall back to generic lowering that uses bit masks, below
+  }
+  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();

src/util/simplify_expr.cpp

@@ -2303,6 +2303,32 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
   return true;
 }
 
+bool simplify_exprt::simplify_complex(exprt &expr)
+{
+  if(expr.id() == ID_complex_real)
+  {
+    complex_real_exprt &complex_real_expr = to_complex_real_expr(expr);
+
+    if(complex_real_expr.op().id() == ID_complex)
+    {
+      expr = to_complex_expr(complex_real_expr.op()).real();
+      return false;
+    }
+  }
+  else if(expr.id() == ID_complex_imag)
+  {
+    complex_imag_exprt &complex_imag_expr = to_complex_imag_expr(expr);
+
+    if(complex_imag_expr.op().id() == ID_complex)
+    {
+      expr = to_complex_expr(complex_imag_expr.op()).imag();
+      return false;
+    }
+  }
+
+  return true;
+}
+
 bool simplify_exprt::simplify_node_preorder(exprt &expr)
 {
   bool result=true;
@@ -2445,18 +2471,21 @@ bool simplify_exprt::simplify_node(exprt &expr)
     result = simplify_popcount(to_popcount_expr(expr)) && result;
   else if(expr.id() == ID_function_application)
     result = simplify_function_application(expr) && result;
+  else if(expr.id() == ID_complex_real || expr.id() == ID_complex_imag)
+    result = simplify_complex(expr) && result;
 
-  #ifdef DEBUGX
-  if(!result
-     #ifdef DEBUG_ON_DEMAND
-     && debug_on
-     #endif
-     )
+#ifdef DEBUGX
+  if(
+    !result
+#ifdef DEBUG_ON_DEMAND
+    && debug_on
+#endif
+  )
   {
     std::cout << "===== " << old.id() << ": " << format(old) << '\n'
               << " ---> " << format(expr) << '\n';
   }
-  #endif
+#endif
 
   return result;
 }

src/util/simplify_expr_class.h

@@ -113,6 +113,7 @@ class simplify_exprt
   bool simplify_abs(exprt &expr);
   bool simplify_sign(exprt &expr);
   bool simplify_popcount(popcount_exprt &expr);
+  bool simplify_complex(exprt &expr);
 
   /// Attempt to simplify mathematical function applications if we have
   /// enough information to do so. Currently focused on constant comparisons.

unit/solvers/lowering/byte_operators.cpp

@@ -158,8 +158,8 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
       // pointer_typet(u64, 64),
       vector_typet(u8, size),
       vector_typet(u64, size),
-      // complex_typet(s16),
-      // complex_typet(u64)
+      complex_typet(s16),
+      complex_typet(u64)
     };
 
     simplify_exprt simp(ns);