Changeset 2176 for src/Cminor

Timestamp:

Jul 12, 2012, 1:28:28 PM (7 years ago)

Author:

campbell

Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

Location:

src/Cminor

Files:

• initialisation.ma (modified) (2 diffs)
• semantics.ma (modified) (3 diffs)
• syntax.ma (modified) (5 diffs)
• toRTLabs.ma (modified) (2 diffs)

src/Cminor/initialisation.ma

@@ -15 +15 @@
 | Init_float64 f       ⇒ Some ? (mk_DPair ?? (ASTfloat F64) (Cst ? (Ofloatconst F64 f)))
 | Init_space n         ⇒ None ?
-| Init_null r          ⇒ Some ? (mk_DPair ?? (ASTptr r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 Unsigned (zero ?)))))
-| Init_addrof r id off ⇒ Some ? (mk_DPair ?? (ASTptr r) (Cst ? (Oaddrsymbol r id off)))
+| Init_null            ⇒ Some ? (mk_DPair ?? ASTptr (Op1 (ASTint I8 Unsigned) ? (Optrofint ??) (Cst ? (Ointconst I8 Unsigned (zero ?)))))
+| Init_addrof   id off ⇒ Some ? (mk_DPair ?? ASTptr (Cst ? (Oaddrsymbol id off)))
 ].
 
@@ -35 +35 @@
 | Some x ⇒
     match x with [ mk_DPair t e ⇒
-      St_store t r (Cst ? (Oaddrsymbol r id off)) e
+      St_store t (Cst ? (Oaddrsymbol id off)) e
     ]
 ].
 % //
-cases init in p; [ 8: #a #b ] #c #p normalize in p;
+cases init in p; [ 7: | 8: #a #b | *: #a ] #p normalize in p;
 destruct;/2/
 qed.

src/Cminor/semantics.ma

@@ -106 +106 @@
     do r ← opt_to_res … (msg FailedOp) (eval_binop ??? op v1 v2);
     OK ? 〈tr1 ⧺ tr2, r〉
-| Mem ty rg e ⇒ λEnv.
+| Mem ty e ⇒ λEnv.
     do 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
     do r ← opt_to_res … (msg FailedLoad) (loadv ty m v);
@@ -306 +306 @@
         let en' ≝ update_present ?? en id ? v in
         return 〈tr, State f St_skip en' ? ? m sp k ? st〉
-    | St_store ty _ edst e ⇒ λInv.
+    | St_store ty edst e ⇒ λInv.
         ! 〈tr,vdst〉 ← eval_expr ge ? edst en ? sp m;
         ! 〈tr',v〉 ← eval_expr ge ? e en ? sp m;
@@ -363 +363 @@
     match fd with
     [ Internal f ⇒ err_to_io ?? (trace × state) (
-        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
+        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) XData in
         ! en ← bind_params args (f_params f);
         return 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉)

src/Cminor/syntax.ma

@@ -9 +9 @@
 | Op1 : ∀t,t'. unary_operation t t' → expr t → expr t'
 | Op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → expr t1 → expr t2 → expr t'
-| Mem : ∀t,r. expr (ASTptr r) → expr t
+| Mem : ∀t. expr ASTptr → expr t
 | Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
 | Ecost : ∀t. costlabel → expr t → expr t.
@@ -20 +20 @@
 | Op1 _ _ _ e ⇒ expr_vars ? e P
 | Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
-| Mem _ _ e ⇒ expr_vars ? e P
+| Mem _ e ⇒ expr_vars ? e P
 | Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
 | Ecost _ _ e ⇒ expr_vars ? e P
@@ -38 +38 @@
 | St_skip : stmt
 | St_assign : ∀t. ident → expr t → stmt
-| St_store : ∀t,r. expr (ASTptr r) → expr t → stmt
+| St_store : ∀t. expr ASTptr → expr t → stmt
 (* ident for returned value, expression to identify fn, args. *)
-| St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
+| St_call : option (ident × typ) → expr ASTptr → list (𝚺t. expr t) → stmt
 (* We don't use these at the moment, and they're getting in the way.
-| St_tailcall : expr (ASTptr Code) → list (𝚺t. expr t) → stmt
+| St_tailcall : expr ASTptr → list (𝚺t. expr t) → stmt
 *)
 | St_seq : stmt → stmt → stmt
@@ -80 +80 @@
 match s with
 [ St_assign t i e ⇒ P i t ∧ expr_vars ? e P
-| St_store _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
+| St_store _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
 | 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
 (*
@@ -113 +113 @@
 [ //
 | #t #id #e * /4/
-| #t #r #e1 #e2 * /4/
+| #t #e1 #e2 * /4/
 | * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ] 
 (*

src/Cminor/toRTLabs.ma

@@ -532 +532 @@
     let f ≝ add_expr … env ? e1 (proj1 … Env) f «r1, ?» in
       «pi1 … f, ?»
-| Mem t _ e' ⇒ λEnv,dst.
+| Mem t e' ⇒ λEnv,dst.
     let ❬f,r❭ ≝ choose_reg … e' f Env in
     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
     OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?»
-| St_store t _ e1 e2 ⇒ λEnv.
+| St_store t e1 e2 ⇒ λEnv.
     let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (π1 Env)) in
     let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (π1 Env)) in