From e14c38aa67f4d7c82e6ff13943ecd9679541c89e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 2 Sep 2024 17:05:43 +0200
Subject: [PATCH] [kernel] Cabs2cil: fixes the alignement computation on packed
 directives.

- uses the alignment of a field type instead of its size to compute
  the field alignement.
- removes incorrect special case for flexible array members, introduced to
  circumvent a crash when computing their size. As we now use the alignment
  instead of the size, the crash no longer occurs.
- merges the implementation of two similar cases (whether there are aligned
  field attributes or not).
---
 src/kernel_internals/typing/cabs2cil.ml    | 61 +++++++++-------------
 tests/misc/oracle/pragma-pack.1.res.oracle |  4 +-
 2 files changed, 26 insertions(+), 39 deletions(-)

diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index ad3a9f63d63..8317846aaa3 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -636,43 +636,30 @@ let process_pragmas_pack_align_field_attributes fi fattrs cattr =
   match !current_packing_pragma, align_pragma_for_struct fi.forig_name with
   | None, None -> check_aligned fattrs
   | Some n, apragma ->
-    begin
-      warn_incompatible_pragmas_attributes apragma (fattrs <> []);
-      match combine_aligned_attributes fattrs with
-      | None ->
-        (* No valid aligned attributes in this field.
-           – if the composite type has a packed attribute, nothing needs to be
-             done (the composite will have the "packed" attribute anyway);
-           – otherwise, align on min(n,sizeof(fi.ftyp)).
-           Drop existing "aligned" attributes, if there are invalid ones. *)
-        if Cil.hasAttribute "packed" cattr then (dropAttribute "aligned" fattrs)
-        else begin
-          let sizeof_type =
-            if Cil.isUnsizedArrayType fi.ftype
-            then
-              (* flexible array member: use size of pointer *)
-              Cil.bitsSizeOf (Machine.uintptr_type ())
-            else
-              Cil.bytesSizeOf fi.ftype
-          in
-          let align = Integer.(min n (of_int sizeof_type)) in
-          Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true
-            "adding aligned(%a) attribute to field '%s.%s' due to packing pragma"
-            Integer.pretty align fi.fcomp.cname fi.fname;
-          addAttribute (Attr("aligned",[AInt align])) (dropAttribute "aligned" fattrs)
-        end
-      | Some local ->
-        (* There is an alignment attribute in this field. This may be smaller
-           than the field type alignment, so we get the maximum of both.
-           Then, we apply the pragma pack: the final alignment will be the
-           minimum between what we had and [n]. *)
-        let align = Integer.min n (Integer.max (Integer.of_int (Cil.bytesSizeOf fi.ftype)) local) in
-        Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true
-          "setting aligned(%a) attribute to field '%s.%s' due to packing pragma"
-          Integer.pretty align fi.fcomp.cname fi.fname;
-        addAttribute (Attr("aligned",[AInt align]))
-          (dropAttribute "aligned" fattrs)
-    end
+    warn_incompatible_pragmas_attributes apragma (fattrs <> []);
+    let field_align = combine_aligned_attributes fattrs in
+    (* If this field has no valid aligned attributes and the composite type
+        has a packed attribute, nothing needs to be done: the composite will
+        have the "packed" attribute anyway. *)
+    if field_align = None && Cil.hasAttribute "packed" cattr then
+      dropAttribute "aligned" fattrs
+    else
+      (* Otherwise, align on min(n, max(field alignment, type alignment)):
+         the field alignment attribute (if there is one) may be smaller than
+         its type alignment, so we get the maximum of both. Then, we apply
+         the pragma pack: the final alignment will be the minimum between what
+         we had and [n]. *)
+      let type_align = Integer.of_int (Cil.bytesAlignOf fi.ftype) in
+      let existing_align =
+        Option.fold field_align ~none:type_align ~some:(Integer.max type_align)
+      in
+      let new_align = Integer.min n existing_align in
+      Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true
+        "%s aligned(%a) attribute to field '%s.%s' due to packing pragma"
+        (if Option.is_none field_align then "adding" else "setting")
+        Integer.pretty new_align fi.fcomp.cname fi.fname;
+      let new_attr = Attr ("aligned", [AInt new_align]) in
+      addAttribute new_attr (dropAttribute "aligned" fattrs)
   | None, Some true ->
     dropAttribute "aligned" fattrs
   | None, Some false ->
diff --git a/tests/misc/oracle/pragma-pack.1.res.oracle b/tests/misc/oracle/pragma-pack.1.res.oracle
index 07e33348981..ee68d85c878 100644
--- a/tests/misc/oracle/pragma-pack.1.res.oracle
+++ b/tests/misc/oracle/pragma-pack.1.res.oracle
@@ -21,8 +21,8 @@
   S_j ∈ {4}
   S_sizeof ∈ {16}
   PACK8_i ∈ {0}
-  PACK8_j ∈ {8}
-  PACK8_sizeof ∈ {24}
+  PACK8_j ∈ {4}
+  PACK8_sizeof ∈ {16}
   PACK1_i ∈ {0}
   PACK1_j ∈ {1}
   PACK1_sizeof ∈ {13}
-- 
GitLab