[751] | 1 | include "common/Events.ma". |
---|
| 2 | include "common/Mem.ma". |
---|
| 3 | include "common/IO.ma". |
---|
| 4 | include "common/Globalenvs.ma". |
---|
| 5 | include "common/SmallstepExec.ma". |
---|
| 6 | |
---|
| 7 | include "Cminor/syntax.ma". |
---|
[1352] | 8 | include alias "basics/logic.ma". |
---|
[751] | 9 | |
---|
| 10 | definition env ≝ identifier_map SymbolTag val. |
---|
| 11 | definition genv ≝ (genv_t Genv) (fundef internal_function). |
---|
| 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. |
---|
[797] | 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; |
---|
[1872] | 106 | do r ← opt_to_res … (msg FailedOp) (eval_binop ??? op v1 v2); |
---|
[751] | 107 | OK ? 〈tr1 ⧺ tr2, r〉 |
---|
[1872] | 108 | | Mem ty rg 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_loop s' ⇒ λInv. find_label l s' (Kseq (St_loop s') k) f en ?? |
---|
| 162 | | St_block s' ⇒ λInv. find_label l s' (Kblock k) f en ?? |
---|
| 163 | | St_label l' s' ⇒ λInv. |
---|
| 164 | match identifier_eq ? l l' with |
---|
[751] | 165 | [ inl _ ⇒ Some ? 〈s',k〉 |
---|
[1316] | 166 | | inr _ ⇒ find_label l s' k f en ?? |
---|
[751] | 167 | ] |
---|
[1316] | 168 | | St_cost _ s' ⇒ λInv. find_label l s' k f en ?? |
---|
| 169 | | _ ⇒ λ_. None ? |
---|
| 170 | ] Inv. |
---|
| 171 | // |
---|
| 172 | try @(π2 Inv) |
---|
| 173 | try @(π2 (π1 Inv)) |
---|
| 174 | [ % [ @(π2 Inv) | @kInv ] |
---|
| 175 | | % [ @Inv | @kInv ] |
---|
| 176 | | % [ @(π2 Inv) | @kInv ] |
---|
| 177 | ] qed. |
---|
[751] | 178 | |
---|
[1316] | 179 | lemma find_label_none : ∀l,s,k,f,en,Inv,kInv. |
---|
| 180 | find_label l s k f en Inv kInv = None ? → |
---|
| 181 | ¬Exists ? (λl'.l' = l) (labels_of s). |
---|
| 182 | #l #s elim s |
---|
| 183 | try (try #a try #b try #c try #d try #e try #f try #g try #h try #i try #j try #m % * (* *) ) |
---|
[1516] | 184 | [ #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%)); |
---|
[1316] | 185 | lapply (IH1 (Kseq s2 k) f en (π2 (π1 Inv)) (conj ?? (π2 Inv) kInv)) |
---|
| 186 | cases (find_label l s1 (Kseq s2 k) f en ??) |
---|
[1516] | 187 | [ #H1 whd in ⊢ (??%? → ?); |
---|
[1316] | 188 | lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??) |
---|
| 189 | [ #H2 #_ % #H cases (Exists_append … H) |
---|
| 190 | [ #H' cases (H1 (refl ??)) /2/ |
---|
| 191 | | #H' cases (H2 (refl ??)) /2/ |
---|
| 192 | ] |
---|
| 193 | | #sk #_ #E destruct |
---|
| 194 | ] |
---|
| 195 | | #sk #_ #E whd in E:(??%?); destruct |
---|
| 196 | ] |
---|
[1516] | 197 | | #sz #sg #e #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%)); |
---|
[1316] | 198 | lapply (IH1 k f en (π2 (π1 Inv)) kInv) |
---|
| 199 | cases (find_label l s1 k f en ??) |
---|
[1516] | 200 | [ #H1 whd in ⊢ (??%? → ?); |
---|
[1316] | 201 | lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??) |
---|
| 202 | [ #H2 #_ % #H cases (Exists_append … H) |
---|
| 203 | [ #H' cases (H1 (refl ??)) /2/ |
---|
| 204 | | #H' cases (H2 (refl ??)) /2/ |
---|
| 205 | ] |
---|
| 206 | | #sk #_ #E destruct |
---|
| 207 | ] |
---|
| 208 | | #sk #_ #E whd in E:(??%?); destruct |
---|
| 209 | ] |
---|
| 210 | | #s1 #IH #k #f #en #Inv #kInv @IH |
---|
| 211 | | #s1 #IH #k #f #en #Inv #kInv @IH |
---|
| 212 | | #E whd in i:(??%?); cases (identifier_eq Label l a) in i; |
---|
[1516] | 213 | whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct | *; #H cases (H (sym_eq … E)) ] |
---|
[1316] | 214 | | whd in i:(??%?); cases (identifier_eq Label l a) in i; |
---|
[1516] | 215 | whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct | #NE #E cases (c d e f ?? E) #H @H ] |
---|
[1316] | 216 | | #cl #s1 #IH #k #f #en #Inv #kInv @IH |
---|
| 217 | ] qed. |
---|
| 218 | |
---|
| 219 | definition find_label_always : ∀l,s,k. Exists ? (λl'.l' = l) (labels_of s) → |
---|
| 220 | ∀f,en. stmt_inv f en s → cont_inv f en k → |
---|
| 221 | Σsk:stmt × cont. stmt_inv f en (\fst sk) ∧ cont_inv f en (\snd sk) ≝ |
---|
| 222 | λl,s,k,H,f,en,Inv,kInv. |
---|
| 223 | match find_label l s k f en Inv kInv return λx.find_label l s k f en Inv kInv = x → ? with |
---|
| 224 | [ Some sk ⇒ λ_. sk |
---|
| 225 | | None ⇒ λE. ⊥ |
---|
| 226 | ] (refl ? (find_label l s k f en Inv kInv)). |
---|
| 227 | cases (find_label_none … E) |
---|
| 228 | #H1 @(H1 H) |
---|
| 229 | qed. |
---|
| 230 | |
---|
[797] | 231 | axiom WrongNumberOfParameters : String. |
---|
| 232 | |
---|
[886] | 233 | (* TODO: perhaps should do a little type checking? *) |
---|
[1605] | 234 | let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Σen:env. All ? (λit. present ?? en (\fst it)) ids) ≝ |
---|
[751] | 235 | match vs with |
---|
[1316] | 236 | [ nil ⇒ match ids return λids.res (Σen. All ?? ids) with [ nil ⇒ OK ? «empty_map ??, ?» | _ ⇒ Error ? (msg WrongNumberOfParameters) ] |
---|
[751] | 237 | | cons v vt ⇒ |
---|
[1316] | 238 | match ids return λids.res (Σen. All ?? ids) with |
---|
[797] | 239 | [ nil ⇒ Error ? (msg WrongNumberOfParameters) |
---|
[886] | 240 | | cons idh idt ⇒ |
---|
| 241 | let 〈id,ty〉 ≝ idh in |
---|
[751] | 242 | do en ← bind_params vt idt; |
---|
[1316] | 243 | OK ? «add ?? en (\fst idh) v, ?» |
---|
[751] | 244 | ] |
---|
| 245 | ]. |
---|
[1316] | 246 | [ @I |
---|
| 247 | | % [ whd >lookup_add_hit % #E destruct |
---|
[1603] | 248 | | @(All_mp … (pi2 ?? en)) #a #H whd @lookup_add_oblivious @H |
---|
[1316] | 249 | ] |
---|
| 250 | ] qed. |
---|
[751] | 251 | |
---|
[886] | 252 | (* TODO: perhaps should do a little type checking? *) |
---|
| 253 | definition init_locals : env → list (ident×typ) → env ≝ |
---|
| 254 | foldr ?? (λidty,en. add ?? en (\fst idty) Vundef). |
---|
[761] | 255 | |
---|
[1316] | 256 | lemma init_locals_preserves : ∀en,vars,l. |
---|
| 257 | present ?? en l → |
---|
| 258 | present ?? (init_locals en vars) l. |
---|
| 259 | #en #vars elim vars |
---|
| 260 | [ #l #H @H |
---|
| 261 | | #idt #tl #IH #l #H whd |
---|
| 262 | @lookup_add_oblivious @IH @H |
---|
| 263 | ] qed. |
---|
| 264 | |
---|
| 265 | lemma init_locals_env : ∀en,vars. |
---|
| 266 | All ? (λidt. present ?? (init_locals en vars) (\fst idt)) vars. |
---|
| 267 | #en #vars elim vars |
---|
| 268 | [ @I |
---|
| 269 | | #idt #tl #IH % |
---|
| 270 | [ whd >lookup_add_hit % #E destruct |
---|
| 271 | | @(All_mp … IH) #a #H @lookup_add_oblivious @H |
---|
| 272 | ] |
---|
| 273 | ] qed. |
---|
| 274 | |
---|
| 275 | let rec trace_map_inv (A,B:Type[0]) (P:A → Prop) (f:∀a. P a → res (trace × B)) |
---|
| 276 | (l:list A) (p:All A P l) on l : res (trace × (list B)) ≝ |
---|
| 277 | match l return λl. All A P l → ? with |
---|
| 278 | [ nil ⇒ λ_. OK ? 〈E0, [ ]〉 |
---|
| 279 | | cons h t ⇒ λp. |
---|
| 280 | do 〈tr,h'〉 ← f h ?; |
---|
| 281 | do 〈tr',t'〉 ← trace_map_inv … f t ?; |
---|
| 282 | OK ? 〈tr ⧺ tr',h'::t'〉 |
---|
| 283 | ] p. |
---|
| 284 | [ @(π1 p) | @(π2 p) ] qed. |
---|
| 285 | |
---|
[797] | 286 | axiom FailedStore : String. |
---|
| 287 | axiom BadFunctionValue : String. |
---|
| 288 | axiom BadSwitchValue : String. |
---|
| 289 | axiom UnknownLabel : String. |
---|
| 290 | axiom ReturnMismatch : String. |
---|
| 291 | |
---|
[751] | 292 | definition eval_step : genv → state → IO io_out io_in (trace × state) ≝ |
---|
| 293 | λge,st. |
---|
[1655] | 294 | match st return λ_. IO ??? with |
---|
| 295 | [ State f s en fInv Inv m sp k kInv st ⇒ err_to_io ??? ( |
---|
| 296 | match s return λs. stmt_inv f en s → res (trace × state) with |
---|
[1316] | 297 | [ St_skip ⇒ λInv. |
---|
[1655] | 298 | match k return λk. cont_inv f en k → res ? with |
---|
| 299 | [ Kseq s' k' ⇒ λkInv. return 〈E0, State f s' en fInv ? m sp k' ? st〉 |
---|
| 300 | | Kblock k' ⇒ λkInv. return 〈E0, State f St_skip en fInv ? m sp k' ? st〉 |
---|
[751] | 301 | (* cminor allows functions without an explicit return statement *) |
---|
[1655] | 302 | | Kend ⇒ λkInv. return 〈E0, Returnstate (None ?) (free m sp) st〉 |
---|
[1316] | 303 | ] kInv |
---|
| 304 | | St_assign _ id e ⇒ λInv. |
---|
| 305 | ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m; |
---|
| 306 | let en' ≝ update_present ?? en id ? v in |
---|
[1655] | 307 | return 〈tr, State f St_skip en' ? ? m sp k ? st〉 |
---|
[1872] | 308 | | St_store ty _ edst e ⇒ λInv. |
---|
[1316] | 309 | ! 〈tr,vdst〉 ← eval_expr ge ? edst en ? sp m; |
---|
| 310 | ! 〈tr',v〉 ← eval_expr ge ? e en ? sp m; |
---|
[1872] | 311 | ! m' ← opt_to_res … (msg FailedStore) (storev ty m vdst v); |
---|
[1655] | 312 | return 〈tr ⧺ tr', State f St_skip en fInv ? m' sp k ? st〉 |
---|
[751] | 313 | |
---|
[1316] | 314 | | St_call dst 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 m (Scall dst f sp en ? fInv k ? st)〉 |
---|
[1680] | 319 | (* |
---|
[1316] | 320 | | St_tailcall ef args ⇒ λInv. |
---|
| 321 | ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m; |
---|
[797] | 322 | ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf); |
---|
[1603] | 323 | ! 〈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] | 324 | return 〈tr ⧺ tr', Callstate fd vargs (free m sp) st〉 |
---|
[1680] | 325 | *) |
---|
[1655] | 326 | | St_seq s1 s2 ⇒ λInv. return 〈E0, State f s1 en fInv ? m sp (Kseq s2 k) ? st〉 |
---|
[1316] | 327 | | St_ifthenelse _ _ e strue sfalse ⇒ λInv. |
---|
| 328 | ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m; |
---|
[751] | 329 | ! b ← eval_bool_of_val v; |
---|
[1655] | 330 | return 〈tr, State f (if b then strue else sfalse) en fInv ? m sp k ? st〉 |
---|
| 331 | | St_loop s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kseq (St_loop s) k) ? st〉 |
---|
| 332 | | St_block s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kblock k) ? st〉 |
---|
[1316] | 333 | | St_exit n ⇒ λInv. |
---|
| 334 | ! k' ← k_exit n k ?? kInv; |
---|
[1655] | 335 | return 〈E0, State f St_skip en fInv ? m sp k' ? st〉 |
---|
[1316] | 336 | | St_switch sz _ e cs default ⇒ λInv. |
---|
| 337 | ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m; |
---|
[751] | 338 | match v with |
---|
[961] | 339 | [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi. |
---|
[1316] | 340 | ! k' ← k_exit (find_case ?? i cs default) k ?? kInv; |
---|
[1655] | 341 | return 〈tr, State f St_skip en fInv ? m sp k' ? st〉) |
---|
| 342 | (Error ? (msg BadSwitchValue)) |
---|
| 343 | | _ ⇒ Error ? (msg BadSwitchValue) |
---|
[751] | 344 | ] |
---|
| 345 | | St_return eo ⇒ |
---|
[1316] | 346 | match eo return λeo. stmt_inv f en (St_return eo) → ? with |
---|
[1655] | 347 | [ None ⇒ λInv. return 〈E0, Returnstate (None ?) (free m sp) st〉 |
---|
[751] | 348 | | Some e ⇒ |
---|
[1603] | 349 | match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ mk_DPair ty e ⇒ λInv. |
---|
[1316] | 350 | ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m; |
---|
[1655] | 351 | return 〈tr, Returnstate (Some ? v) (free m sp) st〉 |
---|
[880] | 352 | ] |
---|
[751] | 353 | ] |
---|
[1655] | 354 | | St_label l s' ⇒ λInv. return 〈E0, State f s' en fInv ? m sp k ? st〉 |
---|
[1316] | 355 | | St_goto l ⇒ λInv. |
---|
[1603] | 356 | match find_label_always l (f_body f) Kend ? f en ?? with [ mk_Sig sk Inv' ⇒ |
---|
[1655] | 357 | return 〈E0, State f (\fst sk) en fInv ? m sp (\snd sk) ? st〉 |
---|
[1316] | 358 | ] |
---|
| 359 | | St_cost l s' ⇒ λInv. |
---|
[1655] | 360 | return 〈Echarge l, State f s' en fInv ? m sp k ? st〉 |
---|
| 361 | ] Inv) |
---|
[1316] | 362 | | Callstate fd args m st ⇒ |
---|
[751] | 363 | match fd with |
---|
[1655] | 364 | [ Internal f ⇒ err_to_io ?? (trace × state) ( |
---|
[751] | 365 | let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in |
---|
| 366 | ! en ← bind_params args (f_params f); |
---|
[1655] | 367 | return 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉) |
---|
[751] | 368 | | External fn ⇒ |
---|
[1655] | 369 | ! evargs ← err_to_io ??? (check_eventval_list args (sig_args (ef_sig fn))); |
---|
[879] | 370 | ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); |
---|
[751] | 371 | let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in |
---|
[1655] | 372 | return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m st〉 |
---|
[751] | 373 | ] |
---|
[1655] | 374 | | Returnstate result m st ⇒ err_to_io ??? ( |
---|
[1316] | 375 | match st with |
---|
| 376 | [ Scall dst f sp en dstP fInv k Inv st' ⇒ |
---|
[1655] | 377 | match result with |
---|
[1316] | 378 | [ None ⇒ match dst with |
---|
[1655] | 379 | [ None ⇒ return 〈E0, State f St_skip en ? ? m sp k ? st'〉 |
---|
| 380 | | Some _ ⇒ Error ? (msg ReturnMismatch)] |
---|
| 381 | | Some v ⇒ match dst return λdst. match dst with [ None ⇒ True | Some idty ⇒ present ?? en (\fst idty) ] → res (trace × state) with |
---|
| 382 | [ None ⇒ λ_. Error ? (msg ReturnMismatch) |
---|
| 383 | | Some idty ⇒ λdstP. return 〈E0, State f St_skip (update_present ?? en (\fst idty) dstP v) ? ? m sp k ? st'〉 |
---|
[1316] | 384 | ] dstP |
---|
| 385 | ] |
---|
[1713] | 386 | | SStop ⇒ |
---|
| 387 | match result with |
---|
| 388 | [ None ⇒ Error ? (msg ReturnMismatch) |
---|
| 389 | | Some v ⇒ match v with |
---|
| 390 | [ Vint sz r ⇒ match sz return λsz. bvint sz → res ? with |
---|
| 391 | [ I32 ⇒ λr. return 〈E0, Finalstate r〉 |
---|
| 392 | | _ ⇒ λ_. Error ? (msg ReturnMismatch) ] r |
---|
| 393 | | _ ⇒ Error ? (msg ReturnMismatch) ] |
---|
| 394 | ] |
---|
[1655] | 395 | ]) |
---|
[1713] | 396 | | Finalstate r ⇒ Error ? (msg BadState) |
---|
[751] | 397 | ]. |
---|
[1316] | 398 | try @(π1 kInv) |
---|
| 399 | try @(π2 kInv) |
---|
| 400 | try @(conj ?? I I) |
---|
| 401 | try @kInv |
---|
| 402 | try @(π2 (π1 Inv)) |
---|
| 403 | try @kInv |
---|
| 404 | try @(π1 (π1 Inv)) |
---|
| 405 | try (@cont_inv_update @kInv) |
---|
| 406 | try @(π2 (π1 (π1 Inv))) |
---|
| 407 | try @(π1 (π1 (π1 Inv))) |
---|
| 408 | try @(π1 Inv) |
---|
| 409 | try @(π2 Inv) |
---|
[1655] | 410 | [ @fInv |
---|
| 411 | | @(π2 Inv') |
---|
| 412 | | @(π1 Inv') |
---|
[1603] | 413 | | @(pi2 … k') |
---|
| 414 | | @(pi2 … k') |
---|
[1655] | 415 | | % [ @Inv | @kInv ] |
---|
| 416 | | cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ] |
---|
| 417 | | % [ @(π2 Inv) | @kInv ] |
---|
| 418 | | @stmt_inv_update @fInv |
---|
| 419 | | 10,11: |
---|
[1316] | 420 | @(stmt_P_mp … (f_inv f)) |
---|
| 421 | #s * #V #L % |
---|
[1626] | 422 | [ 1,3: @(stmt_vars_mp … V) #id #ty #EX cases (Exists_append … EX) |
---|
[1603] | 423 | [ 1,3: #H @init_locals_preserves cases (Exists_All … H (pi2 … en)) |
---|
[1626] | 424 | * #id' #ty * #E1 destruct #H @H |
---|
[1316] | 425 | | *: #H cases (Exists_All … H (init_locals_env … en …)) |
---|
[1626] | 426 | * #id' #ty * #E1 destruct #H @H |
---|
[1316] | 427 | ] |
---|
| 428 | | 2,4: @L |
---|
| 429 | ] |
---|
[1655] | 430 | | @I |
---|
| 431 | | @cont_inv_update @Inv |
---|
| 432 | | @stmt_inv_update @fInv |
---|
| 433 | | @Inv |
---|
[1316] | 434 | | @fInv |
---|
| 435 | ] qed. |
---|
[751] | 436 | |
---|
| 437 | definition is_final : state → option int ≝ |
---|
| 438 | λs. match s with |
---|
[1713] | 439 | [ Finalstate r ⇒ Some ? r |
---|
[751] | 440 | | _ ⇒ None ? |
---|
| 441 | ]. |
---|
| 442 | |
---|
[1238] | 443 | definition Cminor_exec : trans_system io_out io_in ≝ |
---|
| 444 | mk_trans_system … ? (λ_.is_final) eval_step. |
---|
[751] | 445 | |
---|
[797] | 446 | axiom MainMissing : String. |
---|
| 447 | |
---|
[1238] | 448 | definition make_global : Cminor_program → genv ≝ |
---|
| 449 | λp. globalenv Genv ?? (λx.x) p. |
---|
| 450 | |
---|
| 451 | definition make_initial_state : Cminor_program → res state ≝ |
---|
[751] | 452 | λp. |
---|
[1238] | 453 | let ge ≝ make_global p in |
---|
[1139] | 454 | do m ← init_mem Genv ?? (λx.x) p; |
---|
[797] | 455 | do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p)); |
---|
| 456 | do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b); |
---|
[1316] | 457 | OK ? (Callstate f (nil ?) m SStop). |
---|
[751] | 458 | |
---|
| 459 | definition Cminor_fullexec : fullexec io_out io_in ≝ |
---|
[1238] | 460 | mk_fullexec … Cminor_exec make_global make_initial_state. |
---|
[1139] | 461 | |
---|
[1238] | 462 | definition make_noinit_global : Cminor_noinit_program → genv ≝ |
---|
| 463 | λp. globalenv Genv ?? (λx.[Init_space x]) p. |
---|
| 464 | |
---|
| 465 | definition make_initial_noinit_state : Cminor_noinit_program → res state ≝ |
---|
[1139] | 466 | λp. |
---|
[1238] | 467 | let ge ≝ make_noinit_global p in |
---|
[1139] | 468 | do m ← init_mem Genv ?? (λx.[Init_space x]) p; |
---|
| 469 | do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p)); |
---|
| 470 | do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b); |
---|
[1316] | 471 | OK ? (Callstate f (nil ?) m SStop). |
---|
[1139] | 472 | |
---|
| 473 | definition Cminor_noinit_fullexec : fullexec io_out io_in ≝ |
---|
[1238] | 474 | mk_fullexec … Cminor_exec make_noinit_global make_initial_noinit_state. |
---|