source: src/Clight/CexecInd.ma @ 2468

Last change on this file since 2468 was 2468, checked in by garnier, 7 years ago

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File size: 4.6 KB
Line 
1
2include "Clight/Csyntax.ma".
3
4(* We define a special induction principle for Clight expressions that matches
5   their execution. *)
6
7definition is_not_lvalue: expr_descr → Prop ≝
8λe. match e with [ Evar _ ⇒ False | Ederef _ ⇒ False | Efield _ _ ⇒ False | _ ⇒ True ].
9
10definition Plvalue ≝ λP:(expr → Prop).λe,ty.
11match e return λ_.Prop with [ Evar _ ⇒ P (Expr e ty) | Ederef _ ⇒ P (Expr e ty) | Efield _ _ ⇒ P (Expr e ty) | _ ⇒ True ].
12
13let rec expr_lvalue_ind
14  (P:expr → Prop)
15  (Q:expr_descr → type → Prop)
16  (ci:∀sz,ty,i.P (Expr (Econst_int sz i) ty))
17(*  (cf:∀ty,f.P (Expr (Econst_float f) ty))*)
18  (lv:∀e,ty. Q e ty → Plvalue P e ty)
19  (vr:∀v,ty.Q (Evar v) ty)
20  (dr:∀e,ty.P e → Q (Ederef e) ty)
21  (ao:∀ty,e,ty'.Q e ty' → P (Expr (Eaddrof (Expr e ty')) ty))
22  (uo:∀ty,op,e.P e → P (Expr (Eunop op e) ty))
23  (bo:∀ty,op,e1,e2.P e1 → P e2 → P (Expr (Ebinop op e1 e2) ty))
24  (ca:∀ty,ty',e.P e → P (Expr (Ecast ty' e) ty))
25  (cd:∀ty,e1,e2,e3.P e1 → P e2 → P e3 → P (Expr (Econdition e1 e2 e3) ty))
26  (ab:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eandbool e1 e2) ty))
27  (ob:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eorbool e1 e2) ty))
28  (sz:∀ty,ty'. P (Expr (Esizeof ty') ty))
29  (fl:∀ty,e,ty',i. Q e ty' → Q (Efield (Expr e ty') i) ty)
30  (co:∀ty,l,e. P e → P (Expr (Ecost l e) ty))
31  (xx:∀e,ty. is_not_lvalue e → Q e ty)
32  (e:expr) on e : P e ≝
33match e with
34[ Expr e' ty ⇒
35  match e' with
36  [ Econst_int sz i ⇒ ci sz ty i
37(*  | Econst_float f ⇒ cf ty f*)
38  | Evar v ⇒ lv (Evar v) ty (vr v ty)
39  | Ederef e'' ⇒ lv (Ederef e'') ty (dr e'' ty (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e''))
40  | Eaddrof e'' ⇒ match e'' with [ Expr e0 ty0 ⇒ ao ty e0 ty0 (lvalue_expr_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e0 ty0) ]
41  | Eunop op e'' ⇒ uo ty op e'' (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
42  | Ebinop op e1 e2 ⇒ bo ty op e1 e2 (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
43  | Ecast ty' e'' ⇒ ca ty ty' e'' (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
44  | Econdition e1 e2 e3 ⇒ cd ty e1 e2 e3 (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e2) (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e3)
45  | Eandbool e1 e2 ⇒ ab ty e1 e2 (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
46  | Eorbool e1 e2 ⇒ ob ty e1 e2 (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
47  | Esizeof ty' ⇒ sz ty ty'
48  | 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 lv vr dr ao uo bo ca cd ab ob sz fl co xx ef tyf)) ]
49  | Ecost l e'' ⇒ co ty l e'' (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
50  ]
51]
52and lvalue_expr_ind
53  (P:expr → Prop)
54  (Q:expr_descr → type → Prop)
55  (ci:∀sz,ty,i.P (Expr (Econst_int sz i) ty))
56(*  (cf:∀ty,f.P (Expr (Econst_float f) ty))*)
57  (lv:∀e,ty. Q e ty → Plvalue P e ty)
58  (vr:∀v,ty.Q (Evar v) ty)
59  (dr:∀e,ty.P e → Q (Ederef e) ty)
60  (ao:∀ty,e,ty'.Q e ty' → P (Expr (Eaddrof (Expr e ty')) ty))
61  (uo:∀ty,op,e.P e → P (Expr (Eunop op e) ty))
62  (bo:∀ty,op,e1,e2.P e1 → P e2 → P (Expr (Ebinop op e1 e2) ty))
63  (ca:∀ty,ty',e.P e → P (Expr (Ecast ty' e) ty))
64  (cd:∀ty,e1,e2,e3.P e1 → P e2 → P e3 → P (Expr (Econdition e1 e2 e3) ty))
65  (ab:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eandbool e1 e2) ty))
66  (ob:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eorbool e1 e2) ty))
67  (sz:∀ty,ty'. P (Expr (Esizeof ty') ty))
68  (fl:∀ty,e,ty',i. Q e ty' → Q (Efield (Expr e ty') i) ty)
69  (co:∀ty,l,e. P e → P (Expr (Ecost l e) ty))
70  (xx:∀e,ty. is_not_lvalue e → Q e ty)
71  (e:expr_descr) (ty:type) on e : Q e ty ≝
72  match e return λe0. Q e0 ty with
73  [ Evar v ⇒ vr v ty
74  | Ederef e'' ⇒ dr e'' ty (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
75  | 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 lv vr dr ao uo bo ca cd ab ob sz fl co xx e'' ty'') ]
76  | _ ⇒ xx ? ty ?
77  ]. whd; @I qed.
78
79definition expr_lvalue_ind_combined ≝
80λP,Q,ci,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
81conj ??
82 (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx)
83 (lvalue_expr_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx).
Note: See TracBrowser for help on using the repository browser.