Changeset 1135
 Timestamp:
 Aug 29, 2011, 5:45:04 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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