From adff78985362961ee117138c5bc38404dd336a58 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 21 Aug 2023 14:39:17 +0000
Subject: [PATCH] Use extractbits to extract non-byte-fields from unions

Do not use byte_extract to extract members that aren't multiples of
bytes. Instead, use extractbits in that case.

Issue was found by CSmith (test generated with random seed 1692379469),
regression test generated via C-Reduce.
---
 regression/cbmc/Bitfields5/main.c    | 10 ++++++++++
 regression/cbmc/Bitfields5/test.desc |  8 ++++++++
 src/goto-programs/rewrite_union.cpp  | 18 ++++++++++++++++--
 src/goto-symex/field_sensitivity.cpp | 28 ++++++++++++++++++++--------
 src/util/format_type.cpp             |  2 ++
 5 files changed, 56 insertions(+), 10 deletions(-)
 create mode 100644 regression/cbmc/Bitfields5/main.c
 create mode 100644 regression/cbmc/Bitfields5/test.desc

diff --git a/regression/cbmc/Bitfields5/main.c b/regression/cbmc/Bitfields5/main.c
new file mode 100644
index 00000000000..612743f55ab
--- /dev/null
+++ b/regression/cbmc/Bitfields5/main.c
@@ -0,0 +1,10 @@
+union
+{
+  unsigned five : 5;
+  char *a;
+  unsigned one : 1;
+} b = {8};
+int main()
+{
+  __CPROVER_assert(0, "");
+}
diff --git a/regression/cbmc/Bitfields5/test.desc b/regression/cbmc/Bitfields5/test.desc
new file mode 100644
index 00000000000..6de79559914
--- /dev/null
+++ b/regression/cbmc/Bitfields5/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/src/goto-programs/rewrite_union.cpp b/src/goto-programs/rewrite_union.cpp
index f52dfe04f9f..e57993ea598 100644
--- a/src/goto-programs/rewrite_union.cpp
+++ b/src/goto-programs/rewrite_union.cpp
@@ -12,8 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "rewrite_union.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/std_code.h>
@@ -85,8 +87,20 @@ void rewrite_union(exprt &expr)
 
     if(op.type().id() == ID_union_tag || op.type().id() == ID_union)
     {
-      exprt offset = from_integer(0, c_index_type());
-      expr = make_byte_extract(op, offset, expr.type());
+      if(
+        expr.type().id() != ID_c_bit_field ||
+        to_c_bit_field_type(expr.type()).get_width() %
+            config.ansi_c.char_width ==
+          0)
+      {
+        exprt offset = from_integer(0, c_index_type());
+        expr = make_byte_extract(op, offset, expr.type());
+      }
+      else
+      {
+        const auto upper = to_c_bit_field_type(expr.type()).get_width() - 1;
+        expr = extractbits_exprt(op, upper, 0, expr.type());
+      }
     }
   }
   else if(expr.id()==ID_union)
diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp
index a0cb3e1658d..b50215f1082 100644
--- a/src/goto-symex/field_sensitivity.cpp
+++ b/src/goto-symex/field_sensitivity.cpp
@@ -9,8 +9,10 @@ Author: Michael Tautschnig
 #include "field_sensitivity.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 
@@ -419,14 +421,24 @@ void field_sensitivityt::field_assignments_rec(
     exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
     for(const auto &comp : components)
     {
-      const exprt member_rhs = apply(
-        ns,
-        state,
-        simplify_opt(
-          make_byte_extract(
-            ssa_rhs, from_integer(0, c_index_type()), comp.type()),
-          ns),
-        false);
+      exprt extract;
+      if(
+        comp.type().id() != ID_c_bit_field ||
+        to_c_bit_field_type(comp.type()).get_width() %
+            config.ansi_c.char_width ==
+          0)
+      {
+        extract = make_byte_extract(
+          ssa_rhs, from_integer(0, c_index_type()), comp.type());
+      }
+      else
+      {
+        const auto upper = to_c_bit_field_type(comp.type()).get_width() - 1;
+        extract = extractbits_exprt(ssa_rhs, upper, 0, comp.type());
+      }
+
+      const exprt member_rhs =
+        apply(ns, state, simplify_opt(extract, ns), false);
 
       const exprt &member_lhs = *fs_it;
       if(
diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp
index 11560c150ad..50f21126957 100644
--- a/src/util/format_type.cpp
+++ b/src/util/format_type.cpp
@@ -115,6 +115,8 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
     os << u8" \u2192 "; // → -- we don't use ⟶  since that doesn't render well
     return os << format(mathematical_function.codomain());
   }
+  else if(id == ID_c_bit_field)
+    return os << "c_bit_field[" << to_c_bit_field_type(type).get_width() << ']';
   else
     return os << id;
 }