Merge pull request #5252 from tautschnig/byte-extract-unbounded-union

Support byte-extracting from unions of non-fixed size

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -141,6 +141,53 @@ static struct_exprt bv_to_struct_expr(
   return struct_exprt{std::move(operands), struct_type};
 }
 
+/// Convert a bitvector-typed expression \p bitvector_expr to a union-typed
+/// expression. See \ref bv_to_expr for an overview.
+static union_exprt bv_to_union_expr(
+  const exprt &bitvector_expr,
+  const union_typet &union_type,
+  const endianness_mapt &endianness_map,
+  const namespacet &ns)
+{
+  const union_typet::componentst &components = union_type.components();
+
+  // empty union, handled the same way as done in expr_initializert
+  if(components.empty())
+    return union_exprt{irep_idt{}, nil_exprt{}, union_type};
+
+  const auto widest_member = find_widest_union_component(union_type, ns);
+
+  std::size_t component_bits;
+  if(widest_member.has_value())
+    component_bits = numeric_cast_v<std::size_t>(widest_member->second);
+  else
+    component_bits = to_bitvector_type(bitvector_expr.type()).get_width();
+
+  if(component_bits == 0)
+  {
+    return union_exprt{components.front().get_name(),
+                       constant_exprt{irep_idt{}, components.front().type()},
+                       union_type};
+  }
+
+  const auto bounds = map_bounds(endianness_map, 0, component_bits - 1);
+  bitvector_typet type{bitvector_expr.type().id(), component_bits};
+  const irep_idt &component_name = widest_member.has_value()
+                                     ? widest_member->first.get_name()
+                                     : components.front().get_name();
+  const typet &component_type = widest_member.has_value()
+                                  ? widest_member->first.type()
+                                  : components.front().type();
+  return union_exprt{
+    component_name,
+    bv_to_expr(
+      extractbits_exprt{bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
+      component_type,
+      endianness_map,
+      ns),
+    union_type};
+}
+
 /// Convert a bitvector-typed expression \p bitvector_expr to an array-typed
 /// expression. See \ref bv_to_expr for an overview.
 static array_exprt bv_to_array_expr(
@@ -329,6 +376,21 @@ static exprt bv_to_expr(
     result.type() = target_type;
     return std::move(result);
   }
+  else if(target_type.id() == ID_union)
+  {
+    return bv_to_union_expr(
+      bitvector_expr, to_union_type(target_type), endianness_map, ns);
+  }
+  else if(target_type.id() == ID_union_tag)
+  {
+    union_exprt result = bv_to_union_expr(
+      bitvector_expr,
+      ns.follow_tag(to_union_tag_type(target_type)),
+      endianness_map,
+      ns);
+    result.type() = target_type;
+    return std::move(result);
+  }
   else if(target_type.id() == ID_array)
   {
     return bv_to_array_expr(

unit/solvers/lowering/byte_operators.cpp

@@ -91,6 +91,59 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
     }
   }
 
+  GIVEN("A an unbounded union byte_extract over a bounded operand")
+  {
+    const exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32));
+    const byte_extract_exprt be1(
+      ID_byte_extract_little_endian,
+      deadbeef,
+      from_integer(1, index_type()),
+      union_typet(
+        {{"unbounded_array",
+          array_typet(
+            unsignedbv_typet(16), exprt(ID_infinity, size_type()))}}));
+
+    THEN("byte_extract lowering does not raise an exception")
+    {
+      const exprt lower_be1 = lower_byte_extract(be1, ns);
+
+      REQUIRE(!has_subexpr(lower_be1, ID_byte_extract_little_endian));
+      REQUIRE(lower_be1.type() == be1.type());
+
+      byte_extract_exprt be2 = be1;
+      be2.id(ID_byte_extract_big_endian);
+      const exprt lower_be2 = lower_byte_extract(be2, ns);
+
+      REQUIRE(!has_subexpr(lower_be2, ID_byte_extract_big_endian));
+      REQUIRE(lower_be2.type() == be2.type());
+    }
+  }
+
+  GIVEN("A an empty union byte_extract over a bounded operand")
+  {
+    const exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32));
+    const byte_extract_exprt be1(
+      ID_byte_extract_little_endian,
+      deadbeef,
+      from_integer(1, index_type()),
+      union_typet{});
+
+    THEN("byte_extract lowering does not raise an exception")
+    {
+      const exprt lower_be1 = lower_byte_extract(be1, ns);
+
+      REQUIRE(!has_subexpr(lower_be1, ID_byte_extract_little_endian));
+      REQUIRE(lower_be1.type() == be1.type());
+
+      byte_extract_exprt be2 = be1;
+      be2.id(ID_byte_extract_big_endian);
+      const exprt lower_be2 = lower_byte_extract(be2, ns);
+
+      REQUIRE(!has_subexpr(lower_be2, ID_byte_extract_big_endian));
+      REQUIRE(lower_be2.type() == be2.type());
+    }
+  }
+
   GIVEN("A a byte_extract from a string constant")
   {
     string_constantt s("ABCD");