[751] | 1 | include "common/Events.ma". |
---|
[1993] | 2 | include "common/FrontEndMem.ma". |
---|
[751] | 3 | include "common/IO.ma". |
---|
| 4 | include "common/Globalenvs.ma". |
---|
| 5 | include "common/SmallstepExec.ma". |
---|
| 6 | |
---|
[2601] | 7 | include "Cminor/Cminor_syntax.ma". |
---|
[1352] | 8 | include alias "basics/logic.ma". |
---|
[751] | 9 | |
---|
| 10 | definition env ≝ identifier_map SymbolTag val. |
---|
[1986] | 11 | definition genv ≝ genv_t (fundef internal_function). |
---|
[751] | 12 | |
---|
[1316] | 13 | definition stmt_inv : internal_function → env → stmt → Prop ≝ λf,en,s. |
---|
[1626] | 14 | stmt_P (λs.stmt_vars (λid,ty. present ?? en id) s ∧ |
---|
[1316] | 15 | stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of (f_body f))) s) s. |
---|
| 16 | |
---|
| 17 | lemma stmt_inv_update : ∀f,en,s,l,v. |
---|
| 18 | stmt_inv f en s → |
---|
| 19 | ∀H:present ?? en l. |
---|
| 20 | stmt_inv f (update_present ?? en l H v) s. |
---|
| 21 | #f #en #s #l #v #Inv #H |
---|
| 22 | @(stmt_P_mp … Inv) |
---|
| 23 | #s * #H1 #H2 % |
---|
| 24 | [ @(stmt_vars_mp … H1) |
---|
[1626] | 25 | #l #ty #H @update_still_present @H |
---|
[1316] | 26 | | @H2 |
---|
| 27 | ] qed. |
---|
| 28 | |
---|
| 29 | (* continuations within a function. *) |
---|
[751] | 30 | inductive cont : Type[0] ≝ |
---|
[1316] | 31 | | Kend : cont |
---|
[751] | 32 | | Kseq : stmt → cont → cont |
---|
[1316] | 33 | | Kblock : cont → cont. |
---|
[751] | 34 | |
---|
[1316] | 35 | let rec cont_inv (f:internal_function) (en:env) (k:cont) on k : Prop ≝ |
---|
| 36 | match k with |
---|
| 37 | [ Kend ⇒ True |
---|
| 38 | | Kseq s k' ⇒ stmt_inv f en s ∧ cont_inv f en k' |
---|
| 39 | | Kblock k' ⇒ cont_inv f en k' |
---|
| 40 | ]. |
---|
| 41 | |
---|
| 42 | lemma cont_inv_update : ∀f,en,k,l,v. |
---|
| 43 | cont_inv f en k → |
---|
| 44 | ∀H:present ?? en l. |
---|
| 45 | cont_inv f (update_present ?? en l H v) k. |
---|
| 46 | #f #en #k elim k /2/ |
---|
| 47 | #s #k #IH #l #v #Inv #H whd % |
---|
| 48 | [ @stmt_inv_update @(π1 Inv) |
---|
| 49 | | @IH @(π2 Inv) |
---|
| 50 | ] qed. |
---|
| 51 | |
---|
| 52 | (* a stack of function calls *) |
---|
| 53 | inductive stack : Type[0] ≝ |
---|
| 54 | | SStop : stack |
---|
[1626] | 55 | | Scall : ∀dest:option (ident×typ). ∀f:internal_function. block (* sp *) → ∀en:env. match dest with [ None ⇒ True | Some idty ⇒ present ?? en (\fst idty)] → stmt_inv f en (f_body f) → ∀k:cont. cont_inv f en k → stack → stack. |
---|
[1316] | 56 | |
---|
[751] | 57 | inductive state : Type[0] ≝ |
---|
| 58 | | State: |
---|
| 59 | ∀ f: internal_function. |
---|
| 60 | ∀ s: stmt. |
---|
| 61 | ∀ en: env. |
---|
[1316] | 62 | ∀ fInv: stmt_inv f en (f_body f). |
---|
| 63 | ∀ Inv: stmt_inv f en s. |
---|
[751] | 64 | ∀ m: mem. |
---|
| 65 | ∀ sp: block. |
---|
| 66 | ∀ k: cont. |
---|
[1316] | 67 | ∀ kInv: cont_inv f en k. |
---|
| 68 | ∀ st: stack. |
---|
[751] | 69 | state |
---|
| 70 | | Callstate: |
---|
| 71 | ∀ fd: fundef internal_function. |
---|
| 72 | ∀ args: list val. |
---|
| 73 | ∀ m: mem. |
---|
[1316] | 74 | ∀ st: stack. |
---|
[751] | 75 | state |
---|
| 76 | | Returnstate: |
---|
| 77 | ∀ v: option val. |
---|
| 78 | ∀ m: mem. |
---|
[1316] | 79 | ∀ st: stack. |
---|
[1713] | 80 | state |
---|
| 81 | | Finalstate: |
---|
| 82 | ∀ r: int. |
---|
| 83 | state |
---|
| 84 | . |
---|
[751] | 85 | |
---|
[797] | 86 | axiom UnknownLocal : String. |
---|
| 87 | axiom FailedConstant : String. |
---|
| 88 | axiom FailedOp : String. |
---|
| 89 | axiom FailedLoad : String. |
---|
| 90 | |
---|
[1626] | 91 | let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (Env:expr_vars ty0 e (λid,ty. present ?? en id)) (sp:block) (m:mem) on e : res (trace × val) ≝ |
---|
| 92 | match e return λt,e.expr_vars t e (λid,ty. present ?? en id) → res (trace × val) with |
---|
[1316] | 93 | [ Id _ i ⇒ λEnv. |
---|
| 94 | let r ≝ lookup_present ?? en i ? in |
---|
[751] | 95 | OK ? 〈E0, r〉 |
---|
[1316] | 96 | | Cst _ c ⇒ λEnv. |
---|
[1878] | 97 | do r ← opt_to_res … (msg FailedConstant) (eval_constant ? (find_symbol … ge) sp c); |
---|
[751] | 98 | OK ? 〈E0, r〉 |
---|
[1316] | 99 | | Op1 ty ty' op e' ⇒ λEnv. |
---|
| 100 | do 〈tr,v〉 ← eval_expr ge ? e' en ? sp m; |
---|
[1369] | 101 | do r ← opt_to_res … (msg FailedOp) (eval_unop ?? op v); |
---|
[751] | 102 | OK ? 〈tr, r〉 |
---|
[1316] | 103 | | Op2 ty1 ty2 ty' op e1 e2 ⇒ λEnv. |
---|
| 104 | do 〈tr1,v1〉 ← eval_expr ge ? e1 en ? sp m; |
---|
| 105 | do 〈tr2,v2〉 ← eval_expr ge ? e2 en ? sp m; |
---|
[2395] | 106 | do r ← opt_to_res … (msg FailedOp) (eval_binop m ??? op v1 v2); |
---|
[751] | 107 | OK ? 〈tr1 ⧺ tr2, r〉 |
---|
[2176] | 108 | | Mem ty e ⇒ λEnv. |
---|
[1316] | 109 | do 〈tr,v〉 ← eval_expr ge ? e en ? sp m; |
---|
[1872] | 110 | do r ← opt_to_res … (msg FailedLoad) (loadv ty m v); |
---|
[751] | 111 | OK ? 〈tr, r〉 |
---|
[1316] | 112 | | Cond sz sg ty e' e1 e2 ⇒ λEnv. |
---|
| 113 | do 〈tr,v〉 ← eval_expr ge ? e' en ? sp m; |
---|
[751] | 114 | do b ← eval_bool_of_val v; |
---|
[1316] | 115 | do 〈tr',r〉 ← eval_expr ge ? (if b then e1 else e2) en ? sp m; |
---|
[751] | 116 | OK ? 〈tr ⧺ tr', r〉 |
---|
[1316] | 117 | | Ecost ty l e' ⇒ λEnv. |
---|
| 118 | do 〈tr,r〉 ← eval_expr ge ty e' en ? sp m; |
---|
[751] | 119 | OK ? 〈Echarge l ⧺ tr, r〉 |
---|
[1316] | 120 | ] Env. |
---|
| 121 | try @Env |
---|
| 122 | try @(π1 Env) |
---|
| 123 | try @(π2 Env) |
---|
| 124 | try @(π1 (π1 Env)) |
---|
| 125 | cases b |
---|
| 126 | try @(π2 (π1 Env)) |
---|
| 127 | try @(π2 Env) |
---|
| 128 | qed. |
---|
[751] | 129 | |
---|
[797] | 130 | axiom BadState : String. |
---|
| 131 | |
---|
[1316] | 132 | let rec k_exit (n:nat) (k:cont) f en (kInv:cont_inv f en k) on k : res (Σk':cont. cont_inv f en k') ≝ |
---|
| 133 | match k return λk.cont_inv f en k → ? with |
---|
| 134 | [ Kend ⇒ λ_. Error ? (msg BadState) |
---|
| 135 | | Kseq _ k' ⇒ λkInv. k_exit n k' f en ? |
---|
| 136 | | Kblock k' ⇒ λkInv. match n with [ O ⇒ OK ? «k',?» | S m ⇒ k_exit m k' f en ? ] |
---|
| 137 | ] kInv. |
---|
| 138 | [ @(π2 kInv) | @kInv | @kInv ] |
---|
| 139 | qed. |
---|
[751] | 140 | |
---|
[961] | 141 | let rec find_case (A:Type[0]) (sz:intsize) (i:bvint sz) (cs:list (bvint sz × A)) (default:A) on cs : A ≝ |
---|
[751] | 142 | match cs with |
---|
| 143 | [ nil ⇒ default |
---|
| 144 | | cons h t ⇒ |
---|
| 145 | let 〈hi,a〉 ≝ h in |
---|
[961] | 146 | if eq_bv ? i hi then a else find_case A sz i t default |
---|
[751] | 147 | ]. |
---|
| 148 | |
---|
[1316] | 149 | let rec find_label (l:identifier Label) (s:stmt) (k:cont) f en (Inv:stmt_inv f en s) (kInv:cont_inv f en k) on s : option (Σsk:(stmt × cont). stmt_inv f en (\fst sk) ∧ cont_inv f en (\snd sk)) ≝ |
---|
| 150 | match s return λs. stmt_inv f en s → ? with |
---|
| 151 | [ St_seq s1 s2 ⇒ λInv. |
---|
| 152 | match find_label l s1 (Kseq s2 k) f en ?? with |
---|
| 153 | [ None ⇒ find_label l s2 k f en ?? |
---|
[751] | 154 | | Some sk ⇒ Some ? sk |
---|
| 155 | ] |
---|
[1316] | 156 | | St_ifthenelse _ _ _ s1 s2 ⇒ λInv. |
---|
| 157 | match find_label l s1 k f en ?? with |
---|
| 158 | [ None ⇒ find_label l s2 k f en ?? |
---|
[751] | 159 | | Some sk ⇒ Some ? sk |
---|
| 160 | ] |
---|
[1316] | 161 | | St_label l' s' ⇒ λInv. |
---|
| 162 | match identifier_eq ? l l' with |
---|
[751] | 163 | [ inl _ ⇒ Some ? 〈s',k〉 |
---|
[1316] | 164 | | inr _ ⇒ find_label l s' k f en ?? |
---|
[751] | 165 | ] |
---|
[1316] | 166 | | St_cost _ s' ⇒ λInv. find_label l s' k f en ?? |
---|
| 167 | | _ ⇒ λ_. None ? |
---|
| 168 | ] Inv. |
---|
| 169 | // |
---|
| 170 | try @(π2 Inv) |
---|
[2254] | 171 | try @(π1 (π2 Inv)) |
---|
| 172 | try @(π2 (π2 Inv)) |
---|
| 173 | [ % [ @(π2 (π2 Inv)) | @kInv ] |
---|
[1316] | 174 | | % [ @(π2 Inv) | @kInv ] |
---|
| 175 | ] qed. |
---|
[751] | 176 | |
---|
[1316] | 177 | lemma find_label_none : ∀l,s,k,f,en,Inv,kInv. |
---|
| 178 | find_label l s k f en Inv kInv = None ? → |
---|
| 179 | ¬Exists ? (λl'.l' = l) (labels_of s). |
---|
| 180 | #l #s elim s |
---|
| 181 | try (try #a try #b try #c try #d try #e try #f try #g try #h try #i try #j try #m % * (* *) ) |
---|
[1516] | 182 | [ #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%)); |
---|
[2254] | 183 | lapply (IH1 (Kseq s2 k) f en (π1 (π2 Inv)) (conj ?? (π2 (π2 Inv)) kInv)) |
---|
[1316] | 184 | cases (find_label l s1 (Kseq s2 k) f en ??) |
---|
[1516] | 185 | [ #H1 whd in ⊢ (??%? → ?); |
---|
[2254] | 186 | lapply (IH2 k f en (π2 (π2 Inv)) kInv) cases (find_label l s2 k f en ??) |
---|
[1316] | 187 | [ #H2 #_ % #H cases (Exists_append … H) |
---|
| 188 | [ #H' cases (H1 (refl ??)) /2/ |
---|
| 189 | | #H' cases (H2 (refl ??)) /2/ |
---|
| 190 | ] |
---|
| 191 | | #sk #_ #E destruct |
---|
| 192 | ] |
---|
| 193 | | #sk #_ #E whd in E:(??%?); destruct |
---|
| 194 | ] |
---|
[1516] | 195 | | #sz #sg #e #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%)); |
---|
[2254] | 196 | lapply (IH1 k f en (π1 (π2 Inv)) kInv) |
---|
[1316] | 197 | cases (find_label l s1 k f en ??) |
---|
[1516] | 198 | [ #H1 whd in ⊢ (??%? → ?); |
---|
[2254] | 199 | lapply (IH2 k f en (π2 (π2 Inv)) kInv) cases (find_label l s2 k f en ??) |
---|
[1316] | 200 | [ #H2 #_ % #H cases (Exists_append … H) |
---|
| 201 | [ #H' cases (H1 (refl ??)) /2/ |
---|
| 202 | | #H' cases (H2 (refl ??)) /2/ |
---|
| 203 | ] |
---|
| 204 | | #sk #_ #E destruct |
---|
| 205 | ] |
---|
| 206 | | #sk #_ #E whd in E:(??%?); destruct |
---|
| 207 | ] |
---|
| 208 | | #E whd in i:(??%?); cases (identifier_eq Label l a) in i; |
---|
[1516] | 209 | whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct | *; #H cases (H (sym_eq … E)) ] |
---|
[1316] | 210 | | whd in i:(??%?); cases (identifier_eq Label l a) in i; |
---|
[1516] | 211 | whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct | #NE #E cases (c d e f ?? E) #H @H ] |
---|
[1316] | 212 | | #cl #s1 #IH #k #f #en #Inv #kInv @IH |
---|
| 213 | ] qed. |
---|
| 214 | |
---|
| 215 | definition find_label_always : ∀l,s,k. Exists ? (λl'.l' = l) (labels_of s) → |
---|
| 216 | ∀f,en. stmt_inv f en s → cont_inv f en k → |
---|
| 217 | Σsk:stmt × cont. stmt_inv f en (\fst sk) ∧ cont_inv f en (\snd sk) ≝ |
---|
| 218 | λl,s,k,H,f,en,Inv,kInv. |
---|
| 219 | match find_label l s k f en Inv kInv return λx.find_label l s k f en Inv kInv = x → ? with |
---|
| 220 | [ Some sk ⇒ λ_. sk |
---|
| 221 | | None ⇒ λE. ⊥ |
---|
| 222 | ] (refl ? (find_label l s k f en Inv kInv)). |
---|
| 223 | cases (find_label_none … E) |
---|
| 224 | #H1 @(H1 H) |
---|
| 225 | qed. |
---|
| 226 | |
---|
[797] | 227 | axiom WrongNumberOfParameters : String. |
---|
| 228 | |
---|
[886] | 229 | (* TODO: perhaps should do a little type checking? *) |
---|
[1605] | 230 | let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Σen:env. All ? (λit. present ?? en (\fst it)) ids) ≝ |
---|
[751] | 231 | match vs with |
---|
[1316] | 232 | [ nil ⇒ match ids return λids.res (Σen. All ?? ids) with [ nil ⇒ OK ? «empty_map ??, ?» | _ ⇒ Error ? (msg WrongNumberOfParameters) ] |
---|
[751] | 233 | | cons v vt ⇒ |
---|
[1316] | 234 | match ids return λids.res (Σen. All ?? ids) with |
---|
[797] | 235 | [ nil ⇒ Error ? (msg WrongNumberOfParameters) |
---|
[886] | 236 | | cons idh idt ⇒ |
---|
| 237 | let 〈id,ty〉 ≝ idh in |
---|
[751] | 238 | do en ← bind_params vt idt; |
---|
[1316] | 239 | OK ? «add ?? en (\fst idh) v, ?» |
---|
[751] | 240 | ] |
---|
| 241 | ]. |
---|
[1316] | 242 | [ @I |
---|
| 243 | | % [ whd >lookup_add_hit % #E destruct |
---|
[1603] | 244 | | @(All_mp … (pi2 ?? en)) #a #H whd @lookup_add_oblivious @H |
---|
[1316] | 245 | ] |
---|
| 246 | ] qed. |
---|
[751] | 247 | |
---|
[886] | 248 | (* TODO: perhaps should do a little type checking? *) |
---|
| 249 | definition init_locals : env → list (ident×typ) → env ≝ |
---|
| 250 | foldr ?? (λidty,en. add ?? en (\fst idty) Vundef). |
---|
[761] | 251 | |
---|
[1316] | 252 | lemma init_locals_preserves : ∀en,vars,l. |
---|
| 253 | present ?? en l → |
---|
| 254 | present ?? (init_locals en vars) l. |
---|
| 255 | #en #vars elim vars |
---|
| 256 | [ #l #H @H |
---|
| 257 | | #idt #tl #IH #l #H whd |
---|
| 258 | @lookup_add_oblivious @IH @H |
---|
| 259 | ] qed. |
---|
| 260 | |
---|
| 261 | lemma init_locals_env : ∀en,vars. |
---|
| 262 | All ? (λidt. present ?? (init_locals en vars) (\fst idt)) vars. |
---|
| 263 | #en #vars elim vars |
---|
| 264 | [ @I |
---|
| 265 | | #idt #tl #IH % |
---|
| 266 | [ whd >lookup_add_hit % #E destruct |
---|
| 267 | | @(All_mp … IH) #a #H @lookup_add_oblivious @H |
---|
| 268 | ] |
---|
| 269 | ] qed. |
---|
| 270 | |
---|
| 271 | let rec trace_map_inv (A,B:Type[0]) (P:A → Prop) (f:∀a. P a → res (trace × B)) |
---|
| 272 | (l:list A) (p:All A P l) on l : res (trace × (list B)) ≝ |
---|
| 273 | match l return λl. All A P l → ? with |
---|
| 274 | [ nil ⇒ λ_. OK ? 〈E0, [ ]〉 |
---|
| 275 | | cons h t ⇒ λp. |
---|
| 276 | do 〈tr,h'〉 ← f h ?; |
---|
| 277 | do 〈tr',t'〉 ← trace_map_inv … f t ?; |
---|
| 278 | OK ? 〈tr ⧺ tr',h'::t'〉 |
---|
| 279 | ] p. |
---|
| 280 | [ @(π1 p) | @(π2 p) ] qed. |
---|
| 281 | |
---|
[797] | 282 | axiom FailedStore : String. |
---|
| 283 | axiom BadFunctionValue : String. |
---|
| 284 | axiom ReturnMismatch : String. |
---|
| 285 | |
---|
[751] | 286 | definition eval_step : genv → state → IO io_out io_in (trace × state) ≝ |
---|
| 287 | λge,st. |
---|
[1655] | 288 | match st return λ_. IO ??? with |
---|
| 289 | [ State f s en fInv Inv m sp k kInv st ⇒ err_to_io ??? ( |
---|
| 290 | match s return λs. stmt_inv f en s → res (trace × state) with |
---|
[1316] | 291 | [ St_skip ⇒ λInv. |
---|
[1655] | 292 | match k return λk. cont_inv f en k → res ? with |
---|
| 293 | [ Kseq s' k' ⇒ λkInv. return 〈E0, State f s' en fInv ? m sp k' ? st〉 |
---|
| 294 | | Kblock k' ⇒ λkInv. return 〈E0, State f St_skip en fInv ? m sp k' ? st〉 |
---|
[751] | 295 | (* cminor allows functions without an explicit return statement *) |
---|
[1988] | 296 | | Kend ⇒ λkInv. return 〈E0, Returnstate (None ?) (free m sp) st〉 |
---|
[1316] | 297 | ] kInv |
---|
| 298 | | St_assign _ id e ⇒ λInv. |
---|
| 299 | ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m; |
---|
| 300 | let en' ≝ update_present ?? en id ? v in |
---|
[1655] | 301 | return 〈tr, State f St_skip en' ? ? m sp k ? st〉 |
---|
[2176] | 302 | | St_store ty edst e ⇒ λInv. |
---|
[1316] | 303 | ! 〈tr,vdst〉 ← eval_expr ge ? edst en ? sp m; |
---|
| 304 | ! 〈tr',v〉 ← eval_expr ge ? e en ? sp m; |
---|
[1872] | 305 | ! m' ← opt_to_res … (msg FailedStore) (storev ty m vdst v); |
---|
[1655] | 306 | return 〈tr ⧺ tr', State f St_skip en fInv ? m' sp k ? st〉 |
---|
[751] | 307 | |
---|
[1316] | 308 | | St_call dst ef args ⇒ λInv. |
---|
| 309 | ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m; |
---|
[1986] | 310 | ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct … ge vf); |
---|
[1603] | 311 | ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ mk_DPair _ _ ⇒ ? ] → ? with [ mk_DPair ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?; |
---|
[1655] | 312 | return 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉 |
---|
[1680] | 313 | (* |
---|
[1316] | 314 | | St_tailcall ef args ⇒ λInv. |
---|
| 315 | ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m; |
---|
[797] | 316 | ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf); |
---|
[1603] | 317 | ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ mk_DPair _ _ ⇒ ? ] → ? with [ mk_DPair ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?; |
---|
[1655] | 318 | return 〈tr ⧺ tr', Callstate fd vargs (free m sp) st〉 |
---|
[1680] | 319 | *) |
---|
[1655] | 320 | | St_seq s1 s2 ⇒ λInv. return 〈E0, State f s1 en fInv ? m sp (Kseq s2 k) ? st〉 |
---|
[1316] | 321 | | St_ifthenelse _ _ e strue sfalse ⇒ λInv. |
---|
| 322 | ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m; |
---|
[751] | 323 | ! b ← eval_bool_of_val v; |
---|
[1655] | 324 | return 〈tr, State f (if b then strue else sfalse) en fInv ? m sp k ? st〉 |
---|
[751] | 325 | | St_return eo ⇒ |
---|
[1316] | 326 | match eo return λeo. stmt_inv f en (St_return eo) → ? with |
---|
[1988] | 327 | [ None ⇒ λInv. return 〈E0, Returnstate (None ?) (free m sp) st〉 |
---|
[751] | 328 | | Some e ⇒ |
---|
[1603] | 329 | match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ mk_DPair ty e ⇒ λInv. |
---|
[1316] | 330 | ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m; |
---|
[1988] | 331 | return 〈tr, Returnstate (Some ? v) (free m sp) st〉 |
---|
[880] | 332 | ] |
---|
[751] | 333 | ] |
---|
[1655] | 334 | | St_label l s' ⇒ λInv. return 〈E0, State f s' en fInv ? m sp k ? st〉 |
---|
[1316] | 335 | | St_goto l ⇒ λInv. |
---|
[1603] | 336 | match find_label_always l (f_body f) Kend ? f en ?? with [ mk_Sig sk Inv' ⇒ |
---|
[1655] | 337 | return 〈E0, State f (\fst sk) en fInv ? m sp (\snd sk) ? st〉 |
---|
[1316] | 338 | ] |
---|
| 339 | | St_cost l s' ⇒ λInv. |
---|
[1655] | 340 | return 〈Echarge l, State f s' en fInv ? m sp k ? st〉 |
---|
| 341 | ] Inv) |
---|
[1316] | 342 | | Callstate fd args m st ⇒ |
---|
[751] | 343 | match fd with |
---|
[1655] | 344 | [ Internal f ⇒ err_to_io ?? (trace × state) ( |
---|
[2176] | 345 | let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) XData in |
---|
[751] | 346 | ! en ← bind_params args (f_params f); |
---|
[1655] | 347 | return 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉) |
---|
[751] | 348 | | External fn ⇒ |
---|
[1655] | 349 | ! evargs ← err_to_io ??? (check_eventval_list args (sig_args (ef_sig fn))); |
---|
[879] | 350 | ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); |
---|
[751] | 351 | let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in |
---|
[1655] | 352 | return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m st〉 |
---|
[751] | 353 | ] |
---|
[1655] | 354 | | Returnstate result m st ⇒ err_to_io ??? ( |
---|
[1316] | 355 | match st with |
---|
| 356 | [ Scall dst f sp en dstP fInv k Inv st' ⇒ |
---|
[1655] | 357 | match result with |
---|
[1316] | 358 | [ None ⇒ match dst with |
---|
[1655] | 359 | [ None ⇒ return 〈E0, State f St_skip en ? ? m sp k ? st'〉 |
---|
| 360 | | Some _ ⇒ Error ? (msg ReturnMismatch)] |
---|
| 361 | | Some v ⇒ match dst return λdst. match dst with [ None ⇒ True | Some idty ⇒ present ?? en (\fst idty) ] → res (trace × state) with |
---|
| 362 | [ None ⇒ λ_. Error ? (msg ReturnMismatch) |
---|
| 363 | | Some idty ⇒ λdstP. return 〈E0, State f St_skip (update_present ?? en (\fst idty) dstP v) ? ? m sp k ? st'〉 |
---|
[1316] | 364 | ] dstP |
---|
| 365 | ] |
---|
[1713] | 366 | | SStop ⇒ |
---|
| 367 | match result with |
---|
| 368 | [ None ⇒ Error ? (msg ReturnMismatch) |
---|
| 369 | | Some v ⇒ match v with |
---|
| 370 | [ Vint sz r ⇒ match sz return λsz. bvint sz → res ? with |
---|
| 371 | [ I32 ⇒ λr. return 〈E0, Finalstate r〉 |
---|
| 372 | | _ ⇒ λ_. Error ? (msg ReturnMismatch) ] r |
---|
| 373 | | _ ⇒ Error ? (msg ReturnMismatch) ] |
---|
| 374 | ] |
---|
[1655] | 375 | ]) |
---|
[1713] | 376 | | Finalstate r ⇒ Error ? (msg BadState) |
---|
[751] | 377 | ]. |
---|
[1316] | 378 | try @(π1 kInv) |
---|
| 379 | try @(π2 kInv) |
---|
| 380 | try @(conj ?? I I) |
---|
| 381 | try @kInv |
---|
| 382 | try @(π2 (π1 Inv)) |
---|
| 383 | try @kInv |
---|
| 384 | try @(π1 (π1 Inv)) |
---|
[2254] | 385 | try (@cont_inv_update @kInv) |
---|
| 386 | try @(π2 (π1 (π1 Inv))) |
---|
[1316] | 387 | try @(π1 (π1 (π1 Inv))) |
---|
| 388 | try @(π2 Inv) |
---|
[2254] | 389 | try @(π1 (π2 Inv)) |
---|
[1655] | 390 | [ @fInv |
---|
| 391 | | @(π2 Inv') |
---|
| 392 | | @(π1 Inv') |
---|
[2254] | 393 | | cases b [ @(π1 (π2 Inv)) | @(π2 (π2 Inv)) ] |
---|
| 394 | | % [ @(π2 (π2 Inv)) | @kInv ] |
---|
| 395 | | @(π1 (π1 (π1 (π1 Inv)))) |
---|
| 396 | | @(π2 (π1 (π1 (π1 Inv)))) |
---|
| 397 | | /3/ |
---|
[1655] | 398 | | @stmt_inv_update @fInv |
---|
[2254] | 399 | | /3/ |
---|
| 400 | | /3/ |
---|
| 401 | | 12,13: |
---|
[1316] | 402 | @(stmt_P_mp … (f_inv f)) |
---|
[2251] | 403 | #s * #V #L #R % |
---|
[1626] | 404 | [ 1,3: @(stmt_vars_mp … V) #id #ty #EX cases (Exists_append … EX) |
---|
[1603] | 405 | [ 1,3: #H @init_locals_preserves cases (Exists_All … H (pi2 … en)) |
---|
[1626] | 406 | * #id' #ty * #E1 destruct #H @H |
---|
[1316] | 407 | | *: #H cases (Exists_All … H (init_locals_env … en …)) |
---|
[1626] | 408 | * #id' #ty * #E1 destruct #H @H |
---|
[1316] | 409 | ] |
---|
| 410 | | 2,4: @L |
---|
| 411 | ] |
---|
[1655] | 412 | | @I |
---|
| 413 | | @cont_inv_update @Inv |
---|
[2254] | 414 | | /3/ |
---|
[1655] | 415 | | @stmt_inv_update @fInv |
---|
| 416 | | @Inv |
---|
[2254] | 417 | | /3/ |
---|
[1316] | 418 | | @fInv |
---|
| 419 | ] qed. |
---|
[751] | 420 | |
---|
| 421 | definition is_final : state → option int ≝ |
---|
| 422 | λs. match s with |
---|
[1713] | 423 | [ Finalstate r ⇒ Some ? r |
---|
[751] | 424 | | _ ⇒ None ? |
---|
| 425 | ]. |
---|
| 426 | |
---|
[1238] | 427 | definition Cminor_exec : trans_system io_out io_in ≝ |
---|
| 428 | mk_trans_system … ? (λ_.is_final) eval_step. |
---|
[751] | 429 | |
---|
[797] | 430 | axiom MainMissing : String. |
---|
| 431 | |
---|
[1238] | 432 | definition make_global : Cminor_program → genv ≝ |
---|
[1986] | 433 | λp. globalenv … (λx.x) p. |
---|
[1238] | 434 | |
---|
| 435 | definition make_initial_state : Cminor_program → res state ≝ |
---|
[751] | 436 | λp. |
---|
[1238] | 437 | let ge ≝ make_global p in |
---|
[1986] | 438 | do m ← init_mem … (λx.x) p; |
---|
| 439 | do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p)); |
---|
| 440 | do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b); |
---|
[1316] | 441 | OK ? (Callstate f (nil ?) m SStop). |
---|
[751] | 442 | |
---|
| 443 | definition Cminor_fullexec : fullexec io_out io_in ≝ |
---|
[1238] | 444 | mk_fullexec … Cminor_exec make_global make_initial_state. |
---|
[1139] | 445 | |
---|
[1238] | 446 | definition make_noinit_global : Cminor_noinit_program → genv ≝ |
---|
[1986] | 447 | λp. globalenv … (λx.[Init_space x]) p. |
---|
[1238] | 448 | |
---|
| 449 | definition make_initial_noinit_state : Cminor_noinit_program → res state ≝ |
---|
[1139] | 450 | λp. |
---|
[1238] | 451 | let ge ≝ make_noinit_global p in |
---|
[1986] | 452 | do m ← init_mem … (λx.[Init_space x]) p; |
---|
| 453 | do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p)); |
---|
| 454 | do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b); |
---|
[1316] | 455 | OK ? (Callstate f (nil ?) m SStop). |
---|
[1139] | 456 | |
---|
| 457 | definition Cminor_noinit_fullexec : fullexec io_out io_in ≝ |
---|
[1238] | 458 | mk_fullexec … Cminor_exec make_noinit_global make_initial_noinit_state. |
---|