Changeset 2019


Ignore:
Timestamp:
Jun 6, 2012, 6:24:43 PM (5 years ago)
Author:
campbell
Message:

Split out special induction principle for Clight from soundness file.
Put cast simplification into compiler.ma.

Location:
src
Files:
1 added
5 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1988 r2019  
    269269lemma P_res_to_P: ∀A,P,e,v.  P_res A P e → e = OK A v → P v.
    270270#A #P #e #v #H1 #H2 >H2 in H1; whd in ⊢ (% → ?); //; qed.
    271 
    272 (* We define a special induction principle tailored to the recursive definition
    273    above. *)
    274 
    275 definition is_not_lvalue: expr_descr → Prop ≝
    276 λe. match e with [ Evar _ ⇒ False | Ederef _ ⇒ False | Efield _ _ ⇒ False | _ ⇒ True ].
    277 
    278 definition Plvalue ≝ λP:(expr → Prop).λe,ty.
    279 match e return λ_.Prop with [ Evar _ ⇒ P (Expr e ty) | Ederef _ ⇒ P (Expr e ty) | Efield _ _ ⇒ P (Expr e ty) | _ ⇒ True ].
    280271
    281272(* TODO: Can we do this sensibly with a map combinator? *)
  • src/Clight/CexecSound.ma

    r1988 r2019  
    11include "Clight/Cexec.ma".
     2include "Clight/CexecInd.ma".
    23
    34lemma exec_bool_of_val_sound: ∀v,ty,r.
     
    120121] qed.
    121122
    122 let rec expr_lvalue_ind
    123   (P:expr → Prop)
    124   (Q:expr_descr → type → Prop)
    125   (ci:∀sz,ty,i.P (Expr (Econst_int sz i) ty))
    126   (cf:∀ty,f.P (Expr (Econst_float f) ty))
    127   (lv:∀e,ty. Q e ty → Plvalue P e ty)
    128   (vr:∀v,ty.Q (Evar v) ty)
    129   (dr:∀e,ty.P e → Q (Ederef e) ty)
    130   (ao:∀ty,e,ty'.Q e ty' → P (Expr (Eaddrof (Expr e ty')) ty))
    131   (uo:∀ty,op,e.P e → P (Expr (Eunop op e) ty))
    132   (bo:∀ty,op,e1,e2.P e1 → P e2 → P (Expr (Ebinop op e1 e2) ty))
    133   (ca:∀ty,ty',e.P e → P (Expr (Ecast ty' e) ty))
    134   (cd:∀ty,e1,e2,e3.P e1 → P e2 → P e3 → P (Expr (Econdition e1 e2 e3) ty))
    135   (ab:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eandbool e1 e2) ty))
    136   (ob:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eorbool e1 e2) ty))
    137   (sz:∀ty,ty'. P (Expr (Esizeof ty') ty))
    138   (fl:∀ty,e,ty',i. Q e ty' → Q (Efield (Expr e ty') i) ty)
    139   (co:∀ty,l,e. P e → P (Expr (Ecost l e) ty))
    140   (xx:∀e,ty. is_not_lvalue e → Q e ty)
    141   (e:expr) on e : P e ≝
    142 match e with
    143 [ Expr e' ty ⇒
    144   match e' with
    145   [ Econst_int sz i ⇒ ci sz ty i
    146   | Econst_float f ⇒ cf ty f
    147   | Evar v ⇒ lv (Evar v) ty (vr v ty)
    148   | Ederef e'' ⇒ lv (Ederef e'') ty (dr e'' ty (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e''))
    149   | Eaddrof e'' ⇒ match e'' with [ Expr e0 ty0 ⇒ ao ty e0 ty0 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e0 ty0) ]
    150   | Eunop op e'' ⇒ uo ty op e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
    151   | Ebinop op e1 e2 ⇒ bo ty op e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
    152   | Ecast ty' e'' ⇒ ca ty ty' e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
    153   | Econdition e1 e2 e3 ⇒ cd ty e1 e2 e3 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e3)
    154   | Eandbool e1 e2 ⇒ ab ty e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
    155   | Eorbool e1 e2 ⇒ ob ty e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
    156   | Esizeof ty' ⇒ sz ty ty'
    157   | Efield e'' i ⇒ match e'' with [ Expr ef tyf ⇒ lv (Efield (Expr ef tyf) i) ty (fl ty ef tyf i (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx ef tyf)) ]
    158   | Ecost l e'' ⇒ co ty l e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
    159   ]
    160 ]
    161 and lvalue_expr_ind
    162   (P:expr → Prop)
    163   (Q:expr_descr → type → Prop)
    164   (ci:∀sz,ty,i.P (Expr (Econst_int sz i) ty))
    165   (cf:∀ty,f.P (Expr (Econst_float f) ty))
    166   (lv:∀e,ty. Q e ty → Plvalue P e ty)
    167   (vr:∀v,ty.Q (Evar v) ty)
    168   (dr:∀e,ty.P e → Q (Ederef e) ty)
    169   (ao:∀ty,e,ty'.Q e ty' → P (Expr (Eaddrof (Expr e ty')) ty))
    170   (uo:∀ty,op,e.P e → P (Expr (Eunop op e) ty))
    171   (bo:∀ty,op,e1,e2.P e1 → P e2 → P (Expr (Ebinop op e1 e2) ty))
    172   (ca:∀ty,ty',e.P e → P (Expr (Ecast ty' e) ty))
    173   (cd:∀ty,e1,e2,e3.P e1 → P e2 → P e3 → P (Expr (Econdition e1 e2 e3) ty))
    174   (ab:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eandbool e1 e2) ty))
    175   (ob:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eorbool e1 e2) ty))
    176   (sz:∀ty,ty'. P (Expr (Esizeof ty') ty))
    177   (fl:∀ty,e,ty',i. Q e ty' → Q (Efield (Expr e ty') i) ty)
    178   (co:∀ty,l,e. P e → P (Expr (Ecost l e) ty))
    179   (xx:∀e,ty. is_not_lvalue e → Q e ty)
    180   (e:expr_descr) (ty:type) on e : Q e ty ≝
    181   match e return λe0. Q e0 ty with
    182   [ Evar v ⇒ vr v ty
    183   | Ederef e'' ⇒ dr e'' ty (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
    184   | Efield e' i ⇒ match e' return λe1.Q (Efield e1 i) ty with [ Expr e'' ty'' ⇒ fl ty e'' ty'' i (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'' ty'') ]
    185   | _ ⇒ xx ? ty ?
    186   ]. whd; @I qed.
    187 
    188123
    189124theorem exec_expr_sound: ∀ge:genv. ∀en:env. ∀m:mem. ∀e:expr.
  • src/Clight/SimplifyCasts.ma

    r2011 r2019  
    20462046// qed.
    20472047
    2048 include "CexecSound.ma".
    2049 
    2050 definition expr_lvalue_ind_combined ≝
    2051 λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
    2052 conj ??
    2053  (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
    2054  (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
     2048include "Clight/CexecInd.ma".
    20552049 
    20562050lemma simulation_transitive : ∀A,r0,r1,r2. simulate A r0 r1 → simulate A r1 r2 → simulate A r0 r2.
  • src/Clight/labelSimulation.ma

    r2011 r2019  
    22include "Clight/label.ma".
    33include "Clight/Cexec.ma".
    4 
    5 (* for the induction principle *)
    6 include "Clight/CexecSound.ma".
     4include "Clight/CexecInd.ma".
    75
    86(* TODO: make something general that can live in common/Globalenvs.ma. *)
     
    8482#tr1 #tr2 #tr1' #tr2' #twel1 elim twel1 /3/
    8583qed. 
    86 
    87 definition expr_lvalue_ind_combined ≝
    88 λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
    89 conj ??
    90  (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
    91  (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
    9284
    9385theorem label_expr_ok : ∀ge,ge',en,m.
  • src/compiler.ma

    r2001 r2019  
    11
    22include "Clight/label.ma".
    3 (* include "Clight/SimplifyCasts.ma". *)  definition simplify_program : clight_program → clight_program ≝ λp.p.
     3include "Clight/SimplifyCasts.ma".
    44include "Clight/switchRemoval.ma".
    55include "Clight/toCminor.ma".
Note: See TracChangeset for help on using the changeset viewer.