[700] | 1 | include "Clight/Cexec.ma". |
---|
[399] | 2 | |
---|
[487] | 3 | lemma exec_bool_of_val_sound: ∀v,ty,r. |
---|
[399] | 4 | exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r). |
---|
[487] | 5 | #v #ty #r |
---|
[961] | 6 | cases v; [ | #sz #i | #f | #r1 | #r' #b #pc #of ] |
---|
| 7 | cases ty; [ 2,11,20,29,38: #sz' #sg | 3,12,21,30,39: #sz' | 4,13,22,31,40: #rg #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ] |
---|
[1516] | 8 | whd in ⊢ (??%? → ?); |
---|
[961] | 9 | [ 2: @intsize_eq_elim_elim |
---|
| 10 | [ #NE #H destruct |
---|
| 11 | | *; whd @eq_bv_elim |
---|
| 12 | [ #E1 #E2 destruct @bool_of_val_false @is_false_int |
---|
[1410] | 13 | | #E1 #E2 destruct @bool_of_val_true @is_true_int_int @E1 |
---|
[961] | 14 | ] |
---|
[487] | 15 | ] |
---|
[961] | 16 | | 8: #H cases (eq_dec f Fzero) |
---|
[1516] | 17 | [ #e >e in H ⊢ %; >Feq_zero_true #E destruct @bool_of_val_false @is_false_float |
---|
| 18 | | #ne >Feq_zero_false in H; // #E destruct @bool_of_val_true @is_true_float @ne |
---|
[487] | 19 | ] |
---|
[1410] | 20 | | 14: #H destruct @bool_of_val_false @is_false_pointer |
---|
| 21 | | 15: #H destruct @bool_of_val_true @is_true_pointer_pointer |
---|
[961] | 22 | | *: #H destruct |
---|
[487] | 23 | ] qed. |
---|
[399] | 24 | |
---|
[487] | 25 | lemma bool_val_distinct: Vtrue ≠ Vfalse. |
---|
[1410] | 26 | % normalize #H destruct |
---|
[487] | 27 | qed. |
---|
[399] | 28 | |
---|
[487] | 29 | lemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) → |
---|
[399] | 30 | if b then is_true v ty else is_false v ty. |
---|
[1336] | 31 | #v #ty #b cases b; #H inversion H; #v' #ty' #H' #ev #et #ev' //; |
---|
| 32 | @⊥ cases (bool_val_distinct) #X @X [2: @sym_eq] @ev' |
---|
[487] | 33 | qed. |
---|
[399] | 34 | |
---|
[961] | 35 | lemma try_cast_null_sound: ∀m,sz,i,ty,ty',v'. try_cast_null m sz i ty ty' = OK ? v' → cast m (Vint sz i) ty ty' v'. |
---|
| 36 | #m #sz #i #ty #ty' #v' |
---|
[1516] | 37 | whd in ⊢ (??%? → ?); |
---|
[961] | 38 | @eq_bv_elim |
---|
[487] | 39 | [ #e >e |
---|
[961] | 40 | cases ty; [ | #sz' #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ] |
---|
| 41 | whd in ⊢ (??%? → ?); #H [ 2: | *: destruct ] |
---|
| 42 | cases ty' in H ⊢ %; [ | #sz'' #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ] |
---|
| 43 | try (@eq_intsize_elim #E) whd in ⊢ (??%? → ?); #H destruct @cast_ip_z // |
---|
[487] | 44 | | #_ whd in ⊢ (??%? → ?); #H destruct |
---|
| 45 | ] |
---|
| 46 | qed. |
---|
[399] | 47 | |
---|
[1410] | 48 | lemma exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'. |
---|
| 49 | #m #v #ty #ty' #v' |
---|
[487] | 50 | cases v; |
---|
| 51 | [ #H whd in H:(??%?); destruct; |
---|
[961] | 52 | | #sz #i cases ty; |
---|
[487] | 53 | [ #H whd in H:(??%?); destruct; |
---|
| 54 | | 3: #a #H whd in H:(??%?); destruct; |
---|
| 55 | | 7,8,9: #a #b #H whd in H:(??%?); destruct; |
---|
| 56 | | #sz1 #si1 cases ty'; |
---|
[1516] | 57 | [ whd in ⊢ (??%? → ?); @intsize_eq_elim_elim |
---|
[961] | 58 | [ #NE #H destruct |
---|
| 59 | | *; whd #H whd in H:(??%?); destruct; |
---|
| 60 | ] |
---|
[1516] | 61 | | 3: #a whd in ⊢ (??%? → ?); @intsize_eq_elim_elim |
---|
[961] | 62 | [ #E #H whd in H:(??%?); destruct |
---|
| 63 | | *; whd #H whd in H:(??%?); destruct; @cast_if |
---|
| 64 | ] |
---|
[1516] | 65 | | 2,7,8,9: #a #b whd in ⊢ (??%? → ?); @intsize_eq_elim_elim |
---|
[961] | 66 | [ 1,3,5,7: #NE #H destruct |
---|
| 67 | | *: *; whd #H whd in H:(??%?); destruct; // |
---|
| 68 | ] |
---|
[487] | 69 | | 4,5,6: [ #sp #ty'' letin t ≝ (Tpointer sp ty'') |
---|
| 70 | | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n) |
---|
| 71 | | #args #rty letin t ≝ (Tfunction args rty) ] |
---|
[1516] | 72 | whd in ⊢ (??%? → ?); @intsize_eq_elim_elim |
---|
[961] | 73 | [ 1,3,5: #NE #H destruct |
---|
| 74 | | *: *; whd |
---|
| 75 | lapply (try_cast_null_sound m sz i (Tint sz si1) t v'); |
---|
| 76 | cases (try_cast_null m sz i (Tint sz si1) t); |
---|
| 77 | [ 1,3,5: #v'' #H' #e @H' @e |
---|
| 78 | | *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H); |
---|
| 79 | ] |
---|
[487] | 80 | ] |
---|
| 81 | ] |
---|
| 82 | | *: [ #sp #ty'' letin t ≝ (Tpointer sp ty'') |
---|
| 83 | | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n) |
---|
| 84 | | #args #rty letin t ≝ (Tfunction args rty) ] |
---|
| 85 | whd in ⊢ (??%? → ?); |
---|
[961] | 86 | lapply (try_cast_null_sound m sz i t ty' v'); |
---|
| 87 | cases (try_cast_null m sz i t ty'); |
---|
[487] | 88 | [ 1,3,5: #v'' #H' #e @H' @e |
---|
[797] | 89 | | *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H); |
---|
[487] | 90 | ] |
---|
| 91 | ] |
---|
| 92 | | #f cases ty; [ 3: #x | 2,4,6,7,8,9: #x #y | 5: #x #y #z ] |
---|
| 93 | [ cases ty'; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ] |
---|
| 94 | whd in e:(??%?); destruct; //; |
---|
| 95 | | *: #e whd in e:(??%?); destruct |
---|
| 96 | ] |
---|
| 97 | | #r cases ty; [ 3: #x | 2,4,6,7,8,9: #x #y | 5: #x #y #z ] |
---|
| 98 | whd in ⊢ (??%? → ?); #H destruct; cases (eq_region_dec r ?) in H; |
---|
| 99 | whd in ⊢ (? → ??%? → ?); #H1 #H2 destruct; |
---|
| 100 | cases ty' in H2; normalize; try #a try #b try #c try #d destruct; |
---|
| 101 | @cast_pp_z //; |
---|
[1516] | 102 | | #r #b #pc #of whd in ⊢ (??%? → ?); #e |
---|
[500] | 103 | elim (bind_inversion ????? e) #s * #es #e' |
---|
| 104 | elim (bind_inversion ????? e') #u * #eu #e'' -e'; |
---|
| 105 | elim (bind_inversion ????? e'') #s' * #es' #e'''; -e''; |
---|
[487] | 106 | cut (type_region ty s); |
---|
| 107 | [ cases ty in es:(??%?) ⊢ %; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ] |
---|
| 108 | whd in e:(??%?); destruct; //; |
---|
| 109 | | #Hty |
---|
| 110 | cut (type_region ty' s'); |
---|
| 111 | [ cases ty' in es' ⊢ %; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ] |
---|
| 112 | whd in e:(??%?); destruct; //; |
---|
| 113 | | #Hty' |
---|
[500] | 114 | cut (s = r). elim (eq_region_dec r s) in eu; //; normalize; #_ #e destruct. |
---|
[1516] | 115 | #e >e in Hty; #Hty |
---|
| 116 | cases (pointer_compat_dec b s') in e'''; |
---|
[500] | 117 | #Hcompat #e''' whd in e''':(??%?); destruct (e'''); /2/ |
---|
[487] | 118 | ] |
---|
| 119 | ] |
---|
[1410] | 120 | ] qed. |
---|
[399] | 121 | |
---|
[487] | 122 | let rec expr_lvalue_ind |
---|
[399] | 123 | (P:expr → Prop) |
---|
| 124 | (Q:expr_descr → type → Prop) |
---|
[961] | 125 | (ci:∀sz,ty,i.P (Expr (Econst_int sz i) ty)) |
---|
[399] | 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 |
---|
[961] | 145 | [ Econst_int sz i ⇒ ci sz ty i |
---|
[399] | 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) |
---|
[961] | 164 | (ci:∀sz,ty,i.P (Expr (Econst_int sz i) ty)) |
---|
[399] | 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 ? |
---|
[487] | 186 | ]. whd; @I qed. |
---|
[399] | 187 | |
---|
| 188 | |
---|
[487] | 189 | theorem exec_expr_sound: ∀ge:genv. ∀en:env. ∀m:mem. ∀e:expr. |
---|
[399] | 190 | (P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)). |
---|
[498] | 191 | #ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e) |
---|
[1516] | 192 | [ #sz #ty #c whd in ⊢ (???%); cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%); |
---|
[961] | 193 | @eq_intsize_elim #E try @I <E whd % |
---|
[1410] | 194 | | #ty #c whd // |
---|
[399] | 195 | (* expressions that are lvalues *) |
---|
[487] | 196 | | #e' #ty cases e'; //; [ #i #He' | #e #He' | #e #i #He' ] whd in He' ⊢ %; |
---|
| 197 | @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H |
---|
| 198 | @opt_bind_OK #vl #evl whd in evl:(??%?); @(eval_Elvalue … evl) |
---|
[1516] | 199 | >H in He'; #He' @He' |
---|
[487] | 200 | | #v #ty |
---|
| 201 | whd in ⊢ (???%); |
---|
[1058] | 202 | lapply (refl ? (lookup SymbolTag block en v)) |
---|
[1516] | 203 | cases (lookup SymbolTag block en v) in ⊢ (???% → %); |
---|
[487] | 204 | [ #eget @opt_bind_OK #sploc cases sploc; #sp #loc #efind |
---|
| 205 | whd; @(eval_Evar_global … eget efind) |
---|
| 206 | | #loc #eget @(eval_Evar_local … eget) |
---|
| 207 | ] |
---|
[1516] | 208 | | #ty #e #He whd in ⊢ (???%); |
---|
[500] | 209 | @bind2_OK #v cases v // #r #l #pc #ofs #tr #Hv whd |
---|
[1516] | 210 | >Hv in He; #He |
---|
[882] | 211 | @eval_Ederef [ 3: @He | *: skip ] |
---|
[891] | 212 | | #ty #e'' #ty'' #He'' @bind2_OK * #loc #ofs #tr #H |
---|
| 213 | cases ty // * #pty |
---|
[1516] | 214 | cases loc in H ⊢ %; * #loc' #H |
---|
[500] | 215 | whd try @I |
---|
[1516] | 216 | @eval_Eaddrof whd in H:(??%?); >H in He''; #He'' @He'' |
---|
[487] | 217 | | #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1 |
---|
| 218 | @opt_bind_OK #v #ev |
---|
| 219 | @(eval_Eunop … ev) |
---|
[1516] | 220 | >Hv1 in He1; #He1 @He1 |
---|
[487] | 221 | | #ty #op #e1 #e2 #He1 #He2 |
---|
[1516] | 222 | @bind2_OK #v1 #tr1 #ev1 >ev1 in He1; #He1 |
---|
| 223 | @bind2_OK #v2 #tr2 #ev2 >ev2 in He2; #He2 |
---|
[487] | 224 | @opt_bind_OK #v #ev whd in He1 He2; whd; |
---|
| 225 | @(eval_Ebinop … He1 He2 ev) |
---|
| 226 | | #ty #ty' #e' #He' |
---|
[1516] | 227 | @bind2_OK #v #tr #Hv >Hv in He'; #He' |
---|
[487] | 228 | @bind_OK #v' #ev' |
---|
| 229 | @(eval_Ecast … He' ?) |
---|
| 230 | (* XXX /2/; *) |
---|
| 231 | @(exec_cast_sound … ev') |
---|
| 232 | | #ty #e1 #e2 #e3 #He1 #He2 #He3 |
---|
[1516] | 233 | @bind2_OK #vb #tr1 #Hvb >Hvb in He1; #He1 |
---|
[487] | 234 | @bind_OK #b |
---|
| 235 | cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb |
---|
[1516] | 236 | @bind2_OK #v #tr #Hv whd in Hv:(??%?); |
---|
| 237 | [ >Hv in He2; #He2 whd in He2 Hv:(??%?) ⊢%; |
---|
[487] | 238 | @(eval_Econdition_true … He1 ? He2) @(bool_of ??? Hb) |
---|
[1516] | 239 | | >Hv in He3; #He3 whd in He3 Hv:(??%?) ⊢%; |
---|
[487] | 240 | @(eval_Econdition_false … He1 ? He3) @(bool_of ??? Hb) |
---|
| 241 | ] |
---|
| 242 | | #ty #e1 #e2 #He1 #He2 |
---|
[1516] | 243 | @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1 |
---|
[487] | 244 | @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1 |
---|
[1516] | 245 | [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2 |
---|
[487] | 246 | @bind_OK #b2 #eb2 |
---|
| 247 | @(eval_Eandbool_2 … He1 … He2) |
---|
| 248 | [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ] |
---|
| 249 | | @(eval_Eandbool_1 … He1) @(bool_of … Hb1) |
---|
| 250 | ] |
---|
| 251 | | #ty #e1 #e2 #He1 #He2 |
---|
[1516] | 252 | @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1 |
---|
[487] | 253 | @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1 |
---|
| 254 | [ @(eval_Eorbool_1 … He1) @(bool_of … Hb1) |
---|
[1516] | 255 | | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2 |
---|
[487] | 256 | @bind_OK #b2 #eb2 |
---|
| 257 | @(eval_Eorbool_2 … He1 … He2) |
---|
| 258 | [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ] |
---|
| 259 | ] |
---|
[1410] | 260 | | #ty #ty' cases ty try #sz try #sg try #x // |
---|
[487] | 261 | | #ty #e' #ty' #i cases ty'; //; |
---|
| 262 | [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H |
---|
[1516] | 263 | @bind_OK #delta #Hdelta whd in H:(??%?); >H in He'; #He' |
---|
[487] | 264 | @(eval_Efield_struct … He' (refl ??) Hdelta) |
---|
[1516] | 265 | | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H whd in H:(??%?); |
---|
| 266 | >H in He'; #He' |
---|
[487] | 267 | @(eval_Efield_union … He' (refl ??)) |
---|
| 268 | ] |
---|
[1516] | 269 | | #ty #l #e' #He' @bind2_OK #v #tr1 #H >H in He'; #He' |
---|
[487] | 270 | @(eval_Ecost … He') |
---|
[399] | 271 | (* exec_lvalue fails on non-lvalues. *) |
---|
[487] | 272 | | #e' #ty cases e'; |
---|
[961] | 273 | [ 2,5,12: #a #H | 3,4: #a * | 13,14: #a #b * | 1,6,8,10,11: #a #b #H | 7,9: #a #b #c #H ] |
---|
[487] | 274 | @I |
---|
| 275 | ] qed. |
---|
[399] | 276 | |
---|
[500] | 277 | lemma addrof_eval_lvalue: ∀ge,en,m,e,r,loc,pc,off,tr,ty. |
---|
| 278 | eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr r loc pc off) tr → |
---|
[498] | 279 | eval_lvalue ge en m e loc off tr. |
---|
[500] | 280 | #ge #en #m #e #r #loc #pc #off #tr #ty #H inversion H; |
---|
[961] | 281 | [ 1,2,5: #a #b #c #H @False_ind destruct (H); |
---|
[1516] | 282 | | #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1; #H1 @False_ind |
---|
[487] | 283 | @(eval_lvalue_inv_ind … H1) |
---|
| 284 | [ #a #b #c #d #bad destruct (bad); |
---|
[498] | 285 | | #a #b #c #d #e #bad destruct (bad); |
---|
[500] | 286 | | #a #b #c #d #e #f #g #h #bad destruct (bad); |
---|
[498] | 287 | | #a #b #c #d #e #f #g #h #i #j #k #l #m #bad @False_ind destruct (bad); |
---|
| 288 | | #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad); |
---|
[487] | 289 | ] |
---|
[1510] | 290 | | #e' #ty' #r' #loc' #ofs' #tr' #H' #pc' #e1 #e2 #e3 destruct (e1 e2 e3); #E @H' |
---|
[487] | 291 | | #a #b #c #d #e #f #g #h #i #bad destruct (bad); |
---|
| 292 | | #a #b #c #d #e #f #g #h #i #j #k #l #k #l #bad destruct (bad); |
---|
| 293 | | #a #b #c #d #e #f #g #h #i #j #k #l #m #bad destruct (bad); |
---|
| 294 | | #a #b #c #d #e #f #g #h #i #j #k #l #m #bad destruct (bad); |
---|
| 295 | | #a #b #c #d #e #f #g #h #bad destruct (bad); |
---|
| 296 | | #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad destruct (bad); |
---|
| 297 | | #a #b #c #d #e #f #g #h #bad destruct (bad); |
---|
| 298 | | #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad destruct (bad); |
---|
| 299 | | #a #b #c #d #e #f #g #h #i #bad destruct (bad); |
---|
| 300 | | #a #b #c #d #e #f #g #bad destruct (bad); |
---|
| 301 | ] qed. |
---|
[399] | 302 | |
---|
[500] | 303 | lemma addrof_exec_lvalue: ∀ge,en,m,e,r,loc,off,tr. |
---|
| 304 | exec_lvalue ge en m e = OK ? 〈〈mk_block r loc,off〉,tr〉 → |
---|
| 305 | exec_expr ge en m (Expr (Eaddrof e) (Tpointer r Tvoid)) = OK ? 〈Vptr r (mk_block r loc) (same_compat ??) off, tr〉. |
---|
[1516] | 306 | #ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?); |
---|
| 307 | >H whd in ⊢ (??%?); cases r @refl |
---|
[487] | 308 | qed. |
---|
[399] | 309 | |
---|
[487] | 310 | theorem exec_lvalue_sound: ∀ge,en,m,e. |
---|
[498] | 311 | P_res ? (λr.eval_lvalue ge en m e (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue ge en m e). |
---|
[487] | 312 | #ge #en #m #e lapply (refl ? (exec_lvalue ge en m e)); |
---|
| 313 | cases (exec_lvalue ge en m e) in ⊢ (???% → %); |
---|
[1516] | 314 | [ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ %; #locr #loci #H |
---|
[891] | 315 | @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ @same_compat ] |
---|
[500] | 316 | lapply (addrof_exec_lvalue … H) #H' |
---|
| 317 | lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer locr Tvoid))) |
---|
[487] | 318 | >H' #H'' @H'' |
---|
[797] | 319 | | #msg #_ whd @I |
---|
[487] | 320 | ] qed. |
---|
[399] | 321 | |
---|
| 322 | (* Plain equality versions of the above *) |
---|
| 323 | |
---|
[487] | 324 | definition exec_expr_sound' ≝ λge,en,m,e,v. |
---|
[399] | 325 | λH:exec_expr ge en m e = OK ? v. |
---|
| 326 | P_res_to_P ???? (exec_expr_sound ge en m e) H. |
---|
| 327 | |
---|
[498] | 328 | definition exec_lvalue_sound' ≝ λge,en,m,e,loc,off,tr. |
---|
| 329 | λH:exec_lvalue ge en m e = OK ? 〈〈loc,off〉,tr〉. |
---|
[399] | 330 | P_res_to_P ???? (exec_lvalue_sound ge en m e) H. |
---|
| 331 | |
---|
[487] | 332 | lemma exec_exprlist_sound: ∀ge,e,m,l. P_res ? (λvltr:list val×trace. eval_exprlist ge e m l (\fst vltr) (\snd vltr)) (exec_exprlist ge e m l). |
---|
| 333 | #ge #e #m #l elim l; |
---|
[1410] | 334 | whd |
---|
[487] | 335 | [ % |
---|
| 336 | | #e1 #es #IH |
---|
| 337 | @bind2_OK #v #tr1 #Hv |
---|
| 338 | @bind2_OK #vs #tr2 #Hvs |
---|
| 339 | whd; @eval_Econs |
---|
| 340 | [ @(P_res_to_P … (exec_expr_sound ge e m e1) Hv) |
---|
| 341 | | @(P_res_to_P … IH Hvs) |
---|
| 342 | ] |
---|
| 343 | ] qed. |
---|
[399] | 344 | |
---|
[487] | 345 | lemma exec_alloc_variables_sound : ∀l,en,m,en',m'. |
---|
| 346 | exec_alloc_variables en m l = 〈en',m'〉 → |
---|
| 347 | alloc_variables en m l en' m'. |
---|
| 348 | #l elim l |
---|
| 349 | [ #en #m #en' #m' #EXEC whd in EXEC:(??%?); destruct % |
---|
| 350 | | * #id #ty #t #IH #en #m #en' #m' |
---|
| 351 | lapply (refl ? (alloc m O (sizeof ty) Any)) #ALLOC #EXEC |
---|
[1516] | 352 | whd in EXEC:(??%?) ALLOC:(???%); |
---|
[487] | 353 | @(alloc_variables_cons … ALLOC) |
---|
| 354 | @IH @EXEC |
---|
| 355 | qed. |
---|
| 356 | |
---|
| 357 | lemma exec_bind_parameters_sound : ∀ps,vs,en,m. |
---|
| 358 | P_res ? (λm'. bind_parameters en m ps vs m') (exec_bind_parameters en m ps vs). |
---|
| 359 | #ps elim ps |
---|
| 360 | [ * // |
---|
| 361 | | * #id #ty #ps' #IH * |
---|
| 362 | [ // |
---|
| 363 | | #v #vs #en #m |
---|
| 364 | @opt_bind_OK #b #GET |
---|
| 365 | @opt_bind_OK #m' #STORE |
---|
| 366 | lapply (refl ? (exec_bind_parameters en m' ps' vs)) |
---|
[1516] | 367 | cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %); [2: #msg #_ %] |
---|
[487] | 368 | #m'' #BIND |
---|
| 369 | @(bind_parameters_cons … GET STORE) |
---|
[1516] | 370 | lapply (IH vs en m') whd in ⊢ (% → ?); >BIND // |
---|
[487] | 371 | ] |
---|
| 372 | ] qed. |
---|
| 373 | |
---|
| 374 | lemma check_eventval_list_sound : ∀vs,tys. |
---|
| 375 | P_res ? (λevs. eventval_list_match evs tys vs) (check_eventval_list vs tys). |
---|
| 376 | #vs0 elim vs0 |
---|
| 377 | [ * // |
---|
| 378 | | #v #vs #IH * |
---|
| 379 | [ // |
---|
[1516] | 380 | | #ty #tys whd in ⊢ (???%); |
---|
[961] | 381 | cases ty [ #sz #sg | #sz | #r ] cases v // |
---|
[1516] | 382 | [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?); |
---|
[961] | 383 | @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct |
---|
| 384 | | #v ] @bind_OK #evs #CHECKevs |
---|
| 385 | @(evl_match_cons ??????? (P_res_to_P ???? (IH ?) CHECKevs)) |
---|
| 386 | // |
---|
[487] | 387 | ] |
---|
| 388 | ] qed. |
---|
| 389 | |
---|
| 390 | theorem exec_step_sound: ∀ge,st. |
---|
[399] | 391 | P_io ??? (λr. step ge st (\fst r) (\snd r)) (exec_step ge st). |
---|
[487] | 392 | #ge #st cases st; |
---|
| 393 | [ #f #s #k #e #m cases s; |
---|
| 394 | [ cases k; |
---|
| 395 | [ whd in ⊢ (?????%); |
---|
| 396 | lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %); |
---|
| 397 | //; #H whd; |
---|
| 398 | @step_skip_call //; |
---|
[1410] | 399 | | #s' #k' whd; // |
---|
[487] | 400 | | #ex #s' #k' @step_skip_or_continue_while % //; |
---|
| 401 | | #ex #s' #k' |
---|
| 402 | @res_bindIO2_OK #v #tr #Hv |
---|
| 403 | letin bexpr ≝ (exec_bool_of_val v (typeof ex)); |
---|
| 404 | lapply (refl ? bexpr); |
---|
| 405 | cases bexpr in ⊢ (???% → %); |
---|
| 406 | [ #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb |
---|
| 407 | whd in ⊢ (?????%); |
---|
| 408 | [ @(step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv)) |
---|
| 409 | [ % // | @(bool_of … Hb) ] |
---|
| 410 | | @(step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv)) |
---|
| 411 | [ % // | @(bool_of … Hb) ] |
---|
| 412 | ] |
---|
[797] | 413 | | #msg #_ //; |
---|
[487] | 414 | ] |
---|
| 415 | | #ex #s1 #s2 #k' @step_skip_or_continue_for2 % //; |
---|
| 416 | | #ex #s1 #s2 #k' @step_skip_for3 |
---|
| 417 | | #k' @step_skip_break_switch % //; |
---|
| 418 | | #r #f' #e' #k' whd in ⊢ (?????%); |
---|
| 419 | lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %); |
---|
| 420 | //; #H whd; |
---|
| 421 | @step_skip_call //; |
---|
| 422 | ] |
---|
| 423 | | #ex1 #ex2 |
---|
| 424 | @res_bindIO2_OK #x cases x; #y cases y; #pcl #loc #ofs #tr1 #Hlval |
---|
| 425 | @res_bindIO2_OK #v2 #tr2 #Hv2 |
---|
| 426 | @opt_bindIO_OK #m' #em' |
---|
| 427 | whd; @(step_assign … (exec_lvalue_sound' … Hlval) (exec_expr_sound' … Hv2) em') |
---|
| 428 | | #lex #fex #args |
---|
| 429 | @res_bindIO2_OK #vf #tr1 #Hvf0 lapply (exec_expr_sound' … Hvf0); #Hvf |
---|
| 430 | @res_bindIO2_OK #vargs #tr2 #Hvargs0 lapply (P_res_to_P ???? (exec_exprlist_sound …) Hvargs0); #Hvargs |
---|
| 431 | @opt_bindIO_OK #fd #efd |
---|
| 432 | @bindIO_OK #ety |
---|
| 433 | cases lex; whd; |
---|
| 434 | [ @(step_call_none … Hvf Hvargs efd ety) |
---|
| 435 | | #lhs' |
---|
| 436 | @res_bindIO2_OK #x cases x; #y cases y; #pcl #loc #ofs #tr3 #Hlocofs |
---|
| 437 | whd; @(step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety) |
---|
| 438 | ] |
---|
[1410] | 439 | | #s1 #s2 // |
---|
[487] | 440 | | #ex #s1 #s2 |
---|
| 441 | @res_bindIO2_OK #v #tr #Hv |
---|
| 442 | letin bexpr ≝ (exec_bool_of_val v (typeof ex)); |
---|
| 443 | lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //; |
---|
| 444 | #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb |
---|
| 445 | [ @(step_ifthenelse_true … (exec_expr_sound' … Hv)) @(bool_of … Hb) |
---|
| 446 | | @(step_ifthenelse_false … (exec_expr_sound' … Hv)) @(bool_of … Hb) |
---|
| 447 | ] |
---|
| 448 | | #ex #s' |
---|
| 449 | @res_bindIO2_OK #v #tr #Hv |
---|
| 450 | letin bexpr ≝ (exec_bool_of_val v (typeof ex)); |
---|
| 451 | lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //; |
---|
| 452 | #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb |
---|
| 453 | [ @(step_while_true … (exec_expr_sound' … Hv)) @(bool_of … Hb) |
---|
| 454 | | @(step_while_false … (exec_expr_sound' … Hv)) @(bool_of … Hb) |
---|
| 455 | ] |
---|
[1410] | 456 | | #ex #s' // |
---|
[487] | 457 | | #s1 #ex #s2 #s3 whd in ⊢ (?????%); elim (is_Sskip s1); #Hs1 whd in ⊢ (?????%); |
---|
| 458 | [ >Hs1 |
---|
| 459 | @res_bindIO2_OK #v #tr #Hv |
---|
| 460 | letin bexpr ≝ (exec_bool_of_val v (typeof ex)); |
---|
| 461 | lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //; |
---|
| 462 | #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb |
---|
| 463 | [ @(step_for_true … (exec_expr_sound' … Hv)) @(bool_of … Hb) |
---|
| 464 | | @(step_for_false … (exec_expr_sound' … Hv)) @(bool_of … Hb) |
---|
| 465 | ] |
---|
| 466 | | @step_for_start //; |
---|
| 467 | ] |
---|
[1342] | 468 | | whd in ⊢ (?????%); cases k; // #k' @step_skip_break_switch %2 // |
---|
[487] | 469 | | whd in ⊢ (?????%); cases k; //; |
---|
[1342] | 470 | [ #ex #s' #k' whd; @step_skip_or_continue_while %2 ; //; |
---|
[487] | 471 | | #ex #s' #k' whd; |
---|
| 472 | @res_bindIO2_OK #v #tr #Hv |
---|
| 473 | letin bexpr ≝ (exec_bool_of_val v (typeof ex)); |
---|
| 474 | lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //; |
---|
| 475 | #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb |
---|
| 476 | [ @(step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv)) |
---|
| 477 | [ %2 ; // | @(bool_of … Hb) ] |
---|
| 478 | | @(step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv)) |
---|
| 479 | [ %2 ; // | @(bool_of … Hb) ] |
---|
| 480 | ] |
---|
| 481 | | #ex #s1 #s2 #k' whd; @step_skip_or_continue_for2 %2 ; // |
---|
| 482 | ] |
---|
| 483 | | #r whd in ⊢ (?????%); cases r; |
---|
| 484 | [ whd; lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %); //; #H |
---|
| 485 | @step_return_0 @H |
---|
| 486 | | #ex cases (type_eq_dec (fn_return f) Tvoid); //; whd in ⊢ (% → ?????%); #Hnotvoid |
---|
| 487 | @res_bindIO2_OK #v #tr #Hv |
---|
| 488 | whd; @(step_return_1 … Hnotvoid (exec_expr_sound' … Hv)) |
---|
| 489 | ] |
---|
[961] | 490 | | #ex #ls @res_bindIO2_OK * // #sz #n #tr #Hv |
---|
[487] | 491 | @step_switch @(exec_expr_sound' … Hv) |
---|
[1410] | 492 | | #l #s' // |
---|
[487] | 493 | | #l whd in ⊢ (?????%); lapply (refl ? (find_label l (fn_body f) (call_cont k))); |
---|
| 494 | cases (find_label l (fn_body f) (call_cont k)) in ⊢ (???% → %); //; |
---|
| 495 | #sk cases sk; #s' #k' #H |
---|
| 496 | @(step_goto … H) |
---|
[1410] | 497 | | #l #s' // |
---|
[487] | 498 | ] |
---|
| 499 | | #f0 #vargs #k #m whd in ⊢ (?????%); cases f0; |
---|
[1516] | 500 | [ #fn whd in ⊢ (?????%); |
---|
[487] | 501 | lapply (refl ? (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn))) |
---|
[1516] | 502 | cases (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)) in ⊢ (???% → %); |
---|
| 503 | #en' #m' #ALLOC whd in ⊢ (?????%); |
---|
[487] | 504 | @res_bindIO_OK #m2 #BIND |
---|
| 505 | whd; @(step_internal_function … (exec_alloc_variables_sound … ALLOC)) |
---|
| 506 | @(P_res_to_P … (exec_bind_parameters_sound …) BIND) |
---|
| 507 | | #id #argtys #rty @res_bindIO_OK #evs #Hevs |
---|
| 508 | @bindIO_OK #eres whd; |
---|
| 509 | @step_external_function % [ @(P_res_to_P … (check_eventval_list_sound …) Hevs) |
---|
| 510 | | @mk_val_correct ] |
---|
| 511 | ] |
---|
| 512 | | #v #k' #m' whd in ⊢ (?????%); cases k'; //; |
---|
| 513 | #r #f #e #k whd in ⊢ (?????%); cases r; |
---|
| 514 | [ whd; @step_returnstate_0 |
---|
| 515 | | #x cases x; #y cases y; #z cases z; #pcl #b #ofs #ty |
---|
| 516 | @opt_bindIO_OK #m' #em' @step_returnstate_1 whd in em':(??%?); //; |
---|
| 517 | ] |
---|
| 518 | ] |
---|
| 519 | qed. |
---|
[399] | 520 | |
---|
[1244] | 521 | lemma make_initial_state_sound : ∀p. P_res ? (initial_state p) (make_initial_state p). |
---|
[487] | 522 | #p cases p; #fns #main #vars |
---|
| 523 | whd in ⊢ (???%); |
---|
| 524 | @bind_OK #m #Em |
---|
| 525 | @opt_bind_OK #x cases x; #sp #b #esb |
---|
| 526 | @opt_bind_OK #f #ef |
---|
[1244] | 527 | @(initial_state_intro … Em esb ef) @refl |
---|
[487] | 528 | qed. |
---|
[399] | 529 | |
---|
[487] | 530 | theorem exec_steps_sound: ∀ge,n,st. |
---|
[399] | 531 | P_io ??? (λts:trace×state. star (mk_transrel ?? step) ge st (\fst ts) (\snd ts)) |
---|
| 532 | (exec_steps n ge st). |
---|
[487] | 533 | #ge #n elim n; |
---|
| 534 | [ #st whd in ⊢ (?????%); elim (is_final_state st); #H whd; % |
---|
| 535 | | #n' #IH #st whd in ⊢ (?????%); elim (is_final_state st); #H |
---|
| 536 | [ whd; % |
---|
| 537 | | @(P_bindIO2_OK ????????? (exec_step_sound …)) #t #s' cases s'; |
---|
| 538 | [ #f #s #k #e #m | #fd #args #k #m | #r #k #m ] |
---|
| 539 | whd in ⊢ (? → ?????(??????%?)); |
---|
| 540 | cases m; #mc #mn #mp #Hstep |
---|
| 541 | whd in ⊢ (?????(??????%?)); |
---|
| 542 | @(P_bindIO2_OK ????????? (IH …)) #t' #s'' #Hsteps |
---|
| 543 | whd; @(star_step ????????? Hsteps) [ 2,5,8: @Hstep | 3,6,9: // ] |
---|
| 544 | ] |
---|
| 545 | qed. |
---|
[708] | 546 | |
---|
| 547 | lemma is_final_sound: ∀s,r. is_final s = Some ? r → final_state s r. |
---|
[961] | 548 | * [ 3: #v * [ #m #r cases v [ 2: * #r' #E normalize in E; destruct % |
---|
[708] | 549 | | *: normalize #x1 try #x2 try #x3 try #x4 try #x5 destruct |
---|
| 550 | ] |
---|
| 551 | | *: normalize #x1 try #x2 try #x3 try #x4 try #x5 try #x6 try #x7 destruct |
---|
| 552 | ] |
---|
| 553 | | *: normalize #x1 #x2 #x3 #x4 #x5 #x6 try #x7 destruct |
---|
[1350] | 554 | ] qed. |
---|