From 7c0df3799418b6044e448d6266a082b2fbd8ae1f Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 28 Jul 2022 17:57:37 +0200
Subject: Introduce `struct_layout` function

The `struct_layout` function computes for each member, that is neither
padding nor zero-length, the same result as `field_offset`.
---
 cfrontend/Ctypes.v      | 26 ++++++++++++++++++++++++++
 extraction/extraction.v |  3 ++-
 2 files changed, 28 insertions(+), 1 deletion(-)

diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 504e8be1..39117959 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -696,6 +696,32 @@ Fixpoint field_offset_rec (env: composite_env) (id: ident) (ms: members) (pos: Z
 Definition field_offset (env: composite_env) (id: ident) (ms: members) : res (Z * bitfield) :=
   field_offset_rec env id ms 0.
 
+(* [field_zero_or_padding m] returns true if the field is a zero length bitfield
+   or does not have a name *)
+Definition field_zero_or_padding (m: member) : bool :=
+  match m with
+  | Member_plain _ _ => false
+  | Member_bitfield _ _ _ _ w p => orb (zle w 0) p
+  end.
+
+(** [layout_struct env ms accu pos] computes the layout of all fields of a struct that
+    are not unnamed or zero width bitfield members *)
+Fixpoint layout_struct_rec (env: composite_env) (ms: members)
+                           (accu: list (ident * Z * bitfield)) (pos: Z)
+                           {struct ms} : res (list (ident * Z * bitfield)) :=
+  match ms with
+  | nil => OK accu
+  | m :: ms =>
+      if field_zero_or_padding m then
+        layout_struct_rec env ms accu (next_field env pos m)
+      else
+        do (p, b) <- layout_field env pos m;
+        layout_struct_rec env ms (((name_member m), p ,b) :: accu) (next_field env pos m)
+  end.
+
+Definition layout_struct (env: composite_env) (ms: members) : res (list (ident * Z * bitfield)) :=
+  layout_struct_rec env ms nil 0.
+
 (** Some sanity checks about field offsets.  First, field offsets are
   within the range of acceptable offsets. *)
 
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 621298f8..e52a06ee 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -154,7 +154,8 @@ Cd "extraction".
 Separate Extraction
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
-   Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env
+   Ctypes.merge_attributes Ctypes.remove_attributes 
+   Ctypes.build_composite_env Ctypes.layout_struct
    Initializers.transl_init Initializers.constval
    Csyntax.Eindex Csyntax.Epreincr Csyntax.Eselection
    Ctyping.typecheck_program
-- 
cgit