diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2022-07-28 17:57:37 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-09-03 09:55:55 +0200 |
| commit | 7c0df3799418b6044e448d6266a082b2fbd8ae1f (patch) | |
| tree | 92e12621ba1ac980dbf228ebfbbbe0da4ae9cb20 | |
| parent | a2c0973bc94babb3f1a5d166e0bdf6a7d8fff94f (diff) | |
| download | compcert-7c0df3799418b6044e448d6266a082b2fbd8ae1f.tar.gz compcert-7c0df3799418b6044e448d6266a082b2fbd8ae1f.zip | |
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`.
| -rw-r--r-- | cfrontend/Ctypes.v | 26 | ||||
| -rw-r--r-- | extraction/extraction.v | 3 |
2 files changed, 28 insertions, 1 deletions
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 |