Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10

1 files changed, 54 insertions, 0 deletions

diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 8bb46f0b..2f8b5e7c 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -1094,6 +1094,60 @@ Definition incrdecr_type (ty: type) :=
   | _ => Tvoid
   end.
 
+(** ** Accessing bit fields *)
+
+Definition chunk_for_carrier (sz: intsize) : memory_chunk :=
+  match sz with
+  | I8 | IBool => Mint8unsigned
+  | I16 => Mint16unsigned
+  | I32 => Mint32
+  end.
+
+(** For bitfield accesses, bits are numbered differently on
+    little-endian and on big-endian machines: bit 0 is the least
+    significant bit in little-endian, and the most significant bit in
+    big-endian. *)
+
+Definition bitsize_carrier (sz: intsize) : Z :=
+  match sz with
+  | I8 | IBool => 8
+  | I16 => 16
+  | I32 => 32
+  end.
+
+Definition first_bit (sz: intsize) (pos width: Z) : Z :=
+  if Archi.big_endian
+  then bitsize_carrier sz - pos - width
+  else pos.
+
+Definition bitfield_extract (sz: intsize) (sg: signedness) (pos width: Z) (c: int) : int :=
+  if intsize_eq sz IBool || signedness_eq sg Unsigned
+  then Int.unsigned_bitfield_extract (first_bit sz pos width) width c
+  else Int.signed_bitfield_extract (first_bit sz pos width) width c.
+
+Definition bitfield_normalize (sz: intsize) (sg: signedness) (width: Z) (n: int) : int :=
+  if intsize_eq sz IBool || signedness_eq sg Unsigned
+  then Int.zero_ext width n
+  else Int.sign_ext width n.
+
+Inductive load_bitfield: type -> intsize -> signedness -> Z -> Z -> mem -> val -> val -> Prop :=
+  | load_bitfield_intro: forall sz sg1 attr sg pos width m addr c,
+      0 <= pos -> 0 < width <= bitsize_intsize sz -> pos + width <= bitsize_carrier sz ->
+      sg1 = (if zlt width (bitsize_intsize sz) then Signed else sg) ->
+      Mem.loadv (chunk_for_carrier sz) m addr = Some (Vint c) ->
+      load_bitfield (Tint sz sg1 attr) sz sg pos width m addr
+                    (Vint (bitfield_extract sz sg pos width c)).
+
+Inductive store_bitfield: type -> intsize -> signedness -> Z -> Z -> mem -> val -> val -> mem -> val -> Prop :=
+  | store_bitfield_intro: forall sz sg1 attr sg pos width m addr c n m',
+      0 <= pos -> 0 < width <= bitsize_intsize sz -> pos + width <= bitsize_carrier sz ->
+      sg1 = (if zlt width (bitsize_intsize sz) then Signed else sg) ->
+      Mem.loadv (chunk_for_carrier sz) m addr = Some (Vint c) ->
+      Mem.storev (chunk_for_carrier sz) m addr
+                 (Vint (Int.bitfield_insert (first_bit sz pos width) width c n)) = Some m' ->
+      store_bitfield (Tint sz sg1 attr) sz sg pos width m addr (Vint n)
+                     m' (Vint (bitfield_normalize sz sg width n)).
+
 (** * Compatibility with extensions and injections *)
 
 Section GENERIC_INJECTION.