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