diff options
Diffstat (limited to 'cfrontend/Cop.v')
| -rw-r--r-- | cfrontend/Cop.v | 63 |
1 files changed, 59 insertions, 4 deletions
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 143e87a3..0d7bcc3a 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -1083,6 +1084,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. |