Changeset 2176 for src/Cminor
- Timestamp:
- Jul 12, 2012, 1:28:28 PM (7 years ago)
- Location:
- src/Cminor
- Files:
-
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/initialisation.ma
r1878 r2176 15 15 | Init_float64 f ⇒ Some ? (mk_DPair ?? (ASTfloat F64) (Cst ? (Ofloatconst F64 f))) 16 16 | Init_space n ⇒ None ? 17 | Init_null r ⇒ Some ? (mk_DPair ?? (ASTptr r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 Unsigned (zero ?)))))18 | Init_addrof r id off ⇒ Some ? (mk_DPair ?? (ASTptr r) (Cst ? (Oaddrsymbol rid off)))17 | Init_null ⇒ Some ? (mk_DPair ?? ASTptr (Op1 (ASTint I8 Unsigned) ? (Optrofint ??) (Cst ? (Ointconst I8 Unsigned (zero ?))))) 18 | Init_addrof id off ⇒ Some ? (mk_DPair ?? ASTptr (Cst ? (Oaddrsymbol id off))) 19 19 ]. 20 20 … … 35 35 | Some x ⇒ 36 36 match x with [ mk_DPair t e ⇒ 37 St_store t r (Cst ? (Oaddrsymbol rid off)) e37 St_store t (Cst ? (Oaddrsymbol id off)) e 38 38 ] 39 39 ]. 40 40 % // 41 cases init in p; [ 8: #a #b ] #c#p normalize in p;41 cases init in p; [ 7: | 8: #a #b | *: #a ] #p normalize in p; 42 42 destruct;/2/ 43 43 qed. -
src/Cminor/semantics.ma
r1993 r2176 106 106 do r ← opt_to_res … (msg FailedOp) (eval_binop ??? op v1 v2); 107 107 OK ? 〈tr1 ⧺ tr2, r〉 108 | Mem ty rge ⇒ λEnv.108 | Mem ty e ⇒ λEnv. 109 109 do 〈tr,v〉 ← eval_expr ge ? e en ? sp m; 110 110 do r ← opt_to_res … (msg FailedLoad) (loadv ty m v); … … 306 306 let en' ≝ update_present ?? en id ? v in 307 307 return 〈tr, State f St_skip en' ? ? m sp k ? st〉 308 | St_store ty _edst e ⇒ λInv.308 | St_store ty edst e ⇒ λInv. 309 309 ! 〈tr,vdst〉 ← eval_expr ge ? edst en ? sp m; 310 310 ! 〈tr',v〉 ← eval_expr ge ? e en ? sp m; … … 363 363 match fd with 364 364 [ Internal f ⇒ err_to_io ?? (trace × state) ( 365 let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Anyin365 let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) XData in 366 366 ! en ← bind_params args (f_params f); 367 367 return 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉) -
src/Cminor/syntax.ma
r1878 r2176 9 9 | Op1 : ∀t,t'. unary_operation t t' → expr t → expr t' 10 10 | Op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → expr t1 → expr t2 → expr t' 11 | Mem : ∀t ,r. expr (ASTptr r)→ expr t11 | Mem : ∀t. expr ASTptr → expr t 12 12 | Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t 13 13 | Ecost : ∀t. costlabel → expr t → expr t. … … 20 20 | Op1 _ _ _ e ⇒ expr_vars ? e P 21 21 | Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P 22 | Mem _ _e ⇒ expr_vars ? e P22 | Mem _ e ⇒ expr_vars ? e P 23 23 | Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P 24 24 | Ecost _ _ e ⇒ expr_vars ? e P … … 38 38 | St_skip : stmt 39 39 | St_assign : ∀t. ident → expr t → stmt 40 | St_store : ∀t ,r. expr (ASTptr r)→ expr t → stmt40 | St_store : ∀t. expr ASTptr → expr t → stmt 41 41 (* ident for returned value, expression to identify fn, args. *) 42 | St_call : option (ident × typ) → expr (ASTptr Code)→ list (𝚺t. expr t) → stmt42 | St_call : option (ident × typ) → expr ASTptr → list (𝚺t. expr t) → stmt 43 43 (* We don't use these at the moment, and they're getting in the way. 44 | St_tailcall : expr (ASTptr Code)→ list (𝚺t. expr t) → stmt44 | St_tailcall : expr ASTptr → list (𝚺t. expr t) → stmt 45 45 *) 46 46 | St_seq : stmt → stmt → stmt … … 80 80 match s with 81 81 [ St_assign t i e ⇒ P i t ∧ expr_vars ? e P 82 | St_store _ _e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P82 | St_store _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P 83 83 | St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P (\fst i) (\snd i) ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es 84 84 (* … … 113 113 [ // 114 114 | #t #id #e * /4/ 115 | #t # r #e1 #e2 * /4/115 | #t #e1 #e2 * /4/ 116 116 | * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ] 117 117 (* -
src/Cminor/toRTLabs.ma
r2103 r2176 532 532 let f ≝ add_expr … env ? e1 (proj1 … Env) f «r1, ?» in 533 533 «pi1 … f, ?» 534 | Mem t _e' ⇒ λEnv,dst.534 | Mem t e' ⇒ λEnv,dst. 535 535 let ❬f,r❭ ≝ choose_reg … e' f Env in 536 536 let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in … … 686 686 let dst ≝ lookup_reg env x t (π1 (π1 Env)) in 687 687 OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?» 688 | St_store t _e1 e2 ⇒ λEnv.688 | St_store t e1 e2 ⇒ λEnv. 689 689 let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (π1 Env)) in 690 690 let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (π1 Env)) in
Note: See TracChangeset
for help on using the changeset viewer.