Byte-operator lowering: do not generate type casts to compound types

These aren't fully supported by the back-ends. Instead, bit-extract the
components and construct an expression.

Author: tautschnig

regression/cbmc/Pointer_byte_extract3/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Pointer_byte_extract7/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --big-endian
 ^EXIT=0$

src/solvers/lowering/byte_operators.cpp

@@ -19,6 +19,168 @@ Author: Daniel Kroening, [email protected]
 
 #include "flatten_byte_extract_exceptions.h"
 
+static exprt bv_to_expr(
+  const exprt &bitvector_expr,
+  const typet &target_type,
+  const namespacet &ns)
+{
+  if(
+    can_cast_type<bitvector_typet>(target_type) ||
+    target_type.id() == ID_c_enum || target_type.id() == ID_c_enum_tag)
+  {
+    return simplify_expr(
+      typecast_exprt::conditional_cast(bitvector_expr, target_type), ns);
+  }
+
+  if(target_type.id() == ID_struct || target_type.id() == ID_struct_tag)
+  {
+    const struct_typet &struct_type = to_struct_type(ns.follow(target_type));
+    const struct_typet::componentst &components = struct_type.components();
+
+    exprt::operandst operands;
+    operands.reserve(components.size());
+    std::size_t offset = 0;
+    for(const auto &comp : components)
+    {
+      auto component_bits = pointer_offset_bits(comp.type(), ns);
+      std::size_t bits;
+      if(component_bits.has_value())
+        bits = numeric_cast_v<std::size_t>(*component_bits);
+      else
+        bits = to_bitvector_type(bitvector_expr.type()).get_width() - offset;
+
+      if(bits == 0)
+      {
+        operands.push_back(constant_exprt(irep_idt(), comp.type()));
+        continue;
+      }
+
+      bitvector_typet type(bitvector_expr.type().id(), bits);
+      operands.push_back(bv_to_expr(
+        extractbits_exprt(bitvector_expr, offset + bits - 1, offset, type),
+        comp.type(),
+        ns));
+
+      if(component_bits.has_value())
+        offset += bits;
+    }
+
+    return struct_exprt(std::move(operands), target_type);
+  }
+  else if(target_type.id() == ID_array)
+  {
+    const array_typet &array_type = to_array_type(target_type);
+    auto num_elements = numeric_cast<std::size_t>(array_type.size());
+    auto subtype_bits = pointer_offset_bits(array_type.subtype(), ns);
+
+    const std::size_t total_width =
+      to_bitvector_type(bitvector_expr.type()).get_width();
+    if(!num_elements.has_value())
+    {
+      if(!subtype_bits.has_value() || *subtype_bits == 0)
+        num_elements = total_width;
+      else
+        num_elements = total_width / numeric_cast_v<std::size_t>(*subtype_bits);
+    }
+
+    exprt::operandst operands;
+    operands.reserve(*num_elements);
+    for(std::size_t i = 0; i < *num_elements; ++i)
+    {
+      if(subtype_bits.has_value())
+      {
+        const std::size_t subtype_bits_int =
+          numeric_cast_v<std::size_t>(*subtype_bits);
+        bitvector_typet type(bitvector_expr.type().id(), subtype_bits_int);
+        operands.push_back(bv_to_expr(
+          extractbits_exprt(
+            bitvector_expr,
+            (i + 1) * subtype_bits_int - 1,
+            i * subtype_bits_int,
+            type),
+          array_type.subtype(),
+          ns));
+      }
+      else
+      {
+        operands.push_back(
+          bv_to_expr(bitvector_expr, array_type.subtype(), ns));
+      }
+    }
+
+    return array_exprt(std::move(operands), array_type);
+  }
+  else if(target_type.id() == ID_vector)
+  {
+    const vector_typet &vector_type = to_vector_type(target_type);
+    const std::size_t num_elements =
+      numeric_cast_v<std::size_t>(vector_type.size());
+    auto subtype_bits = pointer_offset_bits(vector_type.subtype(), ns);
+
+    exprt::operandst operands;
+    operands.reserve(num_elements);
+    for(std::size_t i = 0; i < num_elements; ++i)
+    {
+      if(subtype_bits.has_value())
+      {
+        const std::size_t subtype_bits_int =
+          numeric_cast_v<std::size_t>(*subtype_bits);
+        bitvector_typet type(bitvector_expr.type().id(), subtype_bits_int);
+        operands.push_back(bv_to_expr(
+          extractbits_exprt(
+            bitvector_expr,
+            (i + 1) * subtype_bits_int - 1,
+            i * subtype_bits_int,
+            type),
+          vector_type.subtype(),
+          ns));
+      }
+      else
+      {
+        operands.push_back(
+          bv_to_expr(bitvector_expr, vector_type.subtype(), ns));
+      }
+    }
+
+    return vector_exprt(std::move(operands), vector_type);
+  }
+  else if(target_type.id() == ID_complex)
+  {
+    const complex_typet &complex_type = to_complex_type(target_type);
+    auto subtype_bits = pointer_offset_bits(complex_type.subtype(), ns);
+    std::size_t subtype_bits_int;
+    if(subtype_bits.has_value())
+      subtype_bits_int = numeric_cast_v<std::size_t>(*subtype_bits);
+    else
+      subtype_bits_int =
+        to_bitvector_type(bitvector_expr.type()).get_width() / 2;
+
+    bitvector_typet type(bitvector_expr.type().id(), subtype_bits_int);
+
+    return complex_exprt(
+      bv_to_expr(
+        extractbits_exprt(bitvector_expr, subtype_bits_int - 1, 0, type),
+        complex_type.subtype(),
+        ns),
+      bv_to_expr(
+        extractbits_exprt(
+          bitvector_expr, subtype_bits_int * 2 - 1, subtype_bits_int, type),
+        complex_type.subtype(),
+        ns),
+      complex_type);
+  }
+  else if(target_type.id() == ID_string)
+  {
+    // this works, but is somewhat questionable
+    return typecast_exprt(bitvector_expr, target_type);
+  }
+  else
+  {
+    PRECONDITION_WITH_DIAGNOSTICS(
+      false, "bv_to_expr does not yet support ", target_type.id_string());
+  }
+}
+
 static exprt unpack_rec(
   const exprt &src,
   bool little_endian,
@@ -501,7 +663,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
 
       plus_exprt new_offset(
         unpacked.offset(),
-        typecast_exprt(
+        typecast_exprt::conditional_cast(
           member_offset_expr(struct_type, comp.get_name(), ns),
           unpacked.offset().type()));
 
@@ -607,13 +769,14 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
   }
 
   if(width_bytes==1)
-    return simplify_expr(typecast_exprt(op.front(), src.type()), ns);
+    return simplify_expr(
+      typecast_exprt::conditional_cast(op.front(), src.type()), ns);
   else // width_bytes>=2
   {
     concatenation_exprt concatenation(
       std::move(op), bitvector_typet(subtype->id(), width_bytes * 8));
-    return simplify_expr(
-      typecast_exprt(std::move(concatenation), src.type()), ns);
+
+    return bv_to_expr(concatenation, src.type(), ns);
   }
 }