diff options
Diffstat (limited to 'cfrontend/Clight.v')
| -rw-r--r-- | cfrontend/Clight.v | 80 |
1 files changed, 46 insertions, 34 deletions
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 8ab29fe9..d15bc90a 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.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. *) (* *) (* *********************************************************************) @@ -196,36 +197,42 @@ Definition empty_env: env := (PTree.empty (block * type)). Definition temp_env := PTree.t val. -(** [deref_loc ty m b ofs v] computes the value of a datum - of type [ty] residing in memory [m] at block [b], offset [ofs]. +(** [deref_loc ty m b ofs bf v] computes the value of a datum + of type [ty] residing in memory [m] at block [b], offset [ofs], + and bitfield designation [bf]. If the type [ty] indicates an access by value, the corresponding memory load is performed. If the type [ty] indicates an access by reference or by copy, the pointer [Vptr b ofs] is returned. *) -Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: ptrofs) : val -> Prop := +Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: ptrofs) : + bitfield -> val -> Prop := | deref_loc_value: forall chunk v, access_mode ty = By_value chunk -> Mem.loadv chunk m (Vptr b ofs) = Some v -> - deref_loc ty m b ofs v + deref_loc ty m b ofs Full v | deref_loc_reference: access_mode ty = By_reference -> - deref_loc ty m b ofs (Vptr b ofs) + deref_loc ty m b ofs Full (Vptr b ofs) | deref_loc_copy: access_mode ty = By_copy -> - deref_loc ty m b ofs (Vptr b ofs). + deref_loc ty m b ofs Full (Vptr b ofs) + | deref_loc_bitfield: forall sz sg pos width v, + load_bitfield ty sz sg pos width m (Vptr b ofs) v -> + deref_loc ty m b ofs (Bits sz sg pos width) v. -(** Symmetrically, [assign_loc ty m b ofs v m'] returns the +(** Symmetrically, [assign_loc ty m b ofs bf v m'] returns the memory state after storing the value [v] in the datum - of type [ty] residing in memory [m] at block [b], offset [ofs]. + of type [ty] residing in memory [m] at block [b], offset [ofs], + bitfield designation [bf]. This is allowed only if [ty] indicates an access by value or by copy. [m'] is the updated memory state. *) Inductive assign_loc (ce: composite_env) (ty: type) (m: mem) (b: block) (ofs: ptrofs): - val -> mem -> Prop := + bitfield -> val -> mem -> Prop := | assign_loc_value: forall v chunk m', access_mode ty = By_value chunk -> Mem.storev chunk m (Vptr b ofs) v = Some m' -> - assign_loc ce ty m b ofs v m' + assign_loc ce ty m b ofs Full v m' | assign_loc_copy: forall b' ofs' bytes m', access_mode ty = By_copy -> (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Ptrofs.unsigned ofs')) -> @@ -235,7 +242,10 @@ Inductive assign_loc (ce: composite_env) (ty: type) (m: mem) (b: block) (ofs: pt \/ Ptrofs.unsigned ofs + sizeof ce ty <= Ptrofs.unsigned ofs' -> Mem.loadbytes m b' (Ptrofs.unsigned ofs') (sizeof ce ty) = Some bytes -> Mem.storebytes m b (Ptrofs.unsigned ofs) bytes = Some m' -> - assign_loc ce ty m b ofs (Vptr b' ofs') m'. + assign_loc ce ty m b ofs Full (Vptr b' ofs') m' + | assign_loc_bitfield: forall sz sg pos width v m' v', + store_bitfield ty sz sg pos width m (Vptr b ofs) v m' v' -> + assign_loc ce ty m b ofs (Bits sz sg pos width) v m'. Section SEMANTICS. @@ -274,7 +284,7 @@ Inductive bind_parameters (e: env): | bind_parameters_cons: forall m id ty params v1 vl b m1 m2, PTree.get id e = Some(b, ty) -> - assign_loc ge ty m b Ptrofs.zero v1 m1 -> + assign_loc ge ty m b Ptrofs.zero Full v1 m1 -> bind_parameters e m1 params vl m2 -> bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2. @@ -368,7 +378,7 @@ Inductive eval_expr: expr -> val -> Prop := le!id = Some v -> eval_expr (Etempvar id ty) v | eval_Eaddrof: forall a ty loc ofs, - eval_lvalue a loc ofs -> + eval_lvalue a loc ofs Full -> eval_expr (Eaddrof a ty) (Vptr loc ofs) | eval_Eunop: forall op a ty v1 v, eval_expr a v1 -> @@ -387,37 +397,39 @@ Inductive eval_expr: expr -> val -> Prop := eval_expr (Esizeof ty1 ty) (Vptrofs (Ptrofs.repr (sizeof ge ty1))) | eval_Ealignof: forall ty1 ty, eval_expr (Ealignof ty1 ty) (Vptrofs (Ptrofs.repr (alignof ge ty1))) - | eval_Elvalue: forall a loc ofs v, - eval_lvalue a loc ofs -> - deref_loc (typeof a) m loc ofs v -> + | eval_Elvalue: forall a loc ofs bf v, + eval_lvalue a loc ofs bf -> + deref_loc (typeof a) m loc ofs bf v -> eval_expr a v (** [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a] in l-value position. The result is the memory location [b, ofs] - that contains the value of the expression [a]. *) + that contains the value of the expression [a], and the bitfield [bf] + designation. *) -with eval_lvalue: expr -> block -> ptrofs -> Prop := +with eval_lvalue: expr -> block -> ptrofs -> bitfield -> Prop := | eval_Evar_local: forall id l ty, e!id = Some(l, ty) -> - eval_lvalue (Evar id ty) l Ptrofs.zero + eval_lvalue (Evar id ty) l Ptrofs.zero Full | eval_Evar_global: forall id l ty, e!id = None -> Genv.find_symbol ge id = Some l -> - eval_lvalue (Evar id ty) l Ptrofs.zero + eval_lvalue (Evar id ty) l Ptrofs.zero Full | eval_Ederef: forall a ty l ofs, eval_expr a (Vptr l ofs) -> - eval_lvalue (Ederef a ty) l ofs - | eval_Efield_struct: forall a i ty l ofs id co att delta, + eval_lvalue (Ederef a ty) l ofs Full + | eval_Efield_struct: forall a i ty l ofs id co att delta bf, eval_expr a (Vptr l ofs) -> typeof a = Tstruct id att -> ge.(genv_cenv)!id = Some co -> - field_offset ge i (co_members co) = OK delta -> - eval_lvalue (Efield a i ty) l (Ptrofs.add ofs (Ptrofs.repr delta)) - | eval_Efield_union: forall a i ty l ofs id co att, + field_offset ge i (co_members co) = OK (delta, bf) -> + eval_lvalue (Efield a i ty) l (Ptrofs.add ofs (Ptrofs.repr delta)) bf + | eval_Efield_union: forall a i ty l ofs id co att delta bf, eval_expr a (Vptr l ofs) -> typeof a = Tunion id att -> ge.(genv_cenv)!id = Some co -> - eval_lvalue (Efield a i ty) l ofs. + union_field_offset ge i (co_members co) = OK (delta, bf) -> + eval_lvalue (Efield a i ty) l (Ptrofs.add ofs (Ptrofs.repr delta)) bf. Scheme eval_expr_ind2 := Minimality for eval_expr Sort Prop with eval_lvalue_ind2 := Minimality for eval_lvalue Sort Prop. @@ -546,11 +558,11 @@ Variable function_entry: function -> list val -> mem -> env -> temp_env -> mem - Inductive step: state -> trace -> state -> Prop := - | step_assign: forall f a1 a2 k e le m loc ofs v2 v m', - eval_lvalue e le m a1 loc ofs -> + | step_assign: forall f a1 a2 k e le m loc ofs bf v2 v m', + eval_lvalue e le m a1 loc ofs bf -> eval_expr e le m a2 v2 -> sem_cast v2 (typeof a2) (typeof a1) m = Some v -> - assign_loc ge (typeof a1) m loc ofs v m' -> + assign_loc ge (typeof a1) m loc ofs bf v m' -> step (State f (Sassign a1 a2) k e le m) E0 (State f Sskip k e le m') @@ -739,7 +751,7 @@ Proof. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate vres2 k m2). econstructor; eauto. (* trace length *) - red; simpl; intros. inv H; simpl; try omega. + red; simpl; intros. inv H; simpl; try lia. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. Qed. |