Changeset 2176 for src/common/FrontEndOps.ma

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.

File:

• src/common/FrontEndOps.ma (modified) (16 diffs)

src/common/FrontEndOps.ma

@@ -23 +23 @@
   | Ointconst: ∀sz,sg. bvint sz → constant (ASTint sz sg)
   | Ofloatconst: ∀sz. float → constant (ASTfloat sz)
-  | Oaddrsymbol: ∀r. ident → nat → constant (ASTptr r) (**r address of the symbol plus the offset *)
-  | Oaddrstack: nat → constant (ASTptr Any).         (**r stack pointer plus the given offset *)
-
-definition boolsrc : typ → Prop ≝ λt. match t with [ ASTint _ _ ⇒ True | ASTptr _ ⇒ True | _ ⇒ False ].
+  | Oaddrsymbol: ident → nat → constant ASTptr (**r address of the symbol plus the offset *)
+  | Oaddrstack: nat → constant ASTptr.         (**r stack pointer plus the given offset *)
+
+definition boolsrc : typ → Prop ≝ λt. match t with [ ASTint _ _ ⇒ True | ASTptr ⇒ True | _ ⇒ False ].
 
 inductive unary_operation : typ → typ → Type[0] ≝
@@ -41 +41 @@
   | Ofloatofintu: ∀fsz,sz. unary_operation (ASTint sz Unsigned) (ASTfloat fsz) (**r float to unsigned integer *)
   | Oid: ∀t. unary_operation t t                                               (**r identity (used to move between registers *)
-  | Optrofint: ∀sz,sg,r. unary_operation (ASTint sz sg) (ASTptr r)             (**r int to pointer with given representation *)
-  | Ointofptr: ∀sz,sg,r. unary_operation (ASTptr r) (ASTint sz sg).            (**r pointer to int *)
+  | Optrofint: ∀sz,sg. unary_operation (ASTint sz sg) ASTptr                   (**r int to pointer with given representation *)
+  | Ointofptr: ∀sz,sg. unary_operation ASTptr (ASTint sz sg).                  (**r pointer to int *)
 
 inductive binary_operation : typ → typ → typ → Type[0] ≝
@@ -65 +65 @@
   | Ocmpu: ∀sz,sg'.   comparison -> binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint I8 sg') (**r integer unsigned comparison *)
   | Ocmpf: ∀sz,sg'.   comparison -> binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTint I8 sg') (**r float comparison *)
-  | Oaddp: ∀sz,r.  binary_operation (ASTptr r)           (ASTint sz Signed)   (ASTptr r)           (**r add an integer to a pointer *)
-  | Osubpi: ∀sz,r. binary_operation (ASTptr r)           (ASTint sz Signed)   (ASTptr r)           (**r subtract int from a pointers *)
-  | Osubpp: ∀sz,r1,r2. binary_operation (ASTptr r1)      (ASTptr r2)          (ASTint sz Signed)   (**r subtract two pointers *)
-  | Ocmpp: ∀r,sg'. comparison → binary_operation (ASTptr r) (ASTptr r) (ASTint I8 sg').  (**r compare pointers *)
+  | Oaddp: ∀sz.    binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r add an integer to a pointer *)
+  | Osubpi: ∀sz.   binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r subtract int from a pointers *)
+  | Osubpp: ∀sz.   binary_operation  ASTptr               ASTptr              (ASTint sz Signed)   (**r subtract two pointers *)
+  | Ocmpp: ∀sg'. comparison → binary_operation ASTptr     ASTptr              (ASTint I8 sg').  (**r compare pointers *)
 
 
@@ -76 +76 @@
 [ ASTint sz sg ⇒ ∀i.P (Vint sz i)
 | ASTfloat sz ⇒ ∀f.P (Vfloat f)
-| ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr (mk_pointer r b c o))
+| ASTptr ⇒ P Vnull ∧ ∀b,o. P (Vptr (mk_pointer b o))
 ] →
 P v.
 #v #t #P *
 [ 1,2: //
-| #r * //
-| #r #b #c #o * //
+| * //
+| #b #o * //
 ] qed.
 
@@ -95 +95 @@
   [ Ointconst sz sg n ⇒ Some ? (Vint sz n)
   | Ofloatconst sz n ⇒ Some ? (Vfloat n)
-  | Oaddrsymbol r s ofs ⇒
+  | Oaddrsymbol s ofs ⇒
       match find_symbol s with
       [ None ⇒ None ?
-      | Some b ⇒ match pointer_compat_dec b r with
+      | Some b ⇒ (*match pointer_compat_dec b r with
                  [ inl pc ⇒ Some ? (Vptr (mk_pointer r b pc (shift_offset ? zero_offset (repr I16 ofs))))
                  | inr _ ⇒ None ?
-                 ]
+                 ]*) Some ? (Vptr (mk_pointer b (shift_offset ? zero_offset (repr I16 ofs))))
       ]
   | Oaddrstack ofs ⇒
-      Some ? (Vptr (mk_pointer Any sp ? (shift_offset ? zero_offset (repr I16 ofs))))
-  ]. cases sp // qed.
+      Some ? (Vptr (mk_pointer sp (shift_offset ? zero_offset (repr I16 ofs))))
+  ]. (*cases sp // qed.*)
 
 lemma eval_constant_typ_correct : ∀t,f,sp,c,v.
@@ -113 +113 @@
 [ #sz #sg #i #v #E normalize in E; destruct //
 | #sz #f #v #E normalize in E; destruct //
-| #r #id #n #v whd in ⊢ (??%? → ?); cases (f id) [2:#b] #E whd in E:(??%?); destruct
-  cases (pointer_compat_dec b r) in E; #pc #E whd in E:(??%?); destruct 
+| #id #n #v whd in ⊢ (??%? → ?); cases (f id) [2:#b] #E whd in E:(??%?); destruct 
+(*  cases (pointer_compat_dec b r) in E; #pc #E whd in E:(??%?); destruct *)
   //
 | #n #v #E whd in E:(??%?); destruct //
@@ -132 +132 @@
       [ Vint sz1 n1 ⇒ Some ? (Vint sz (if (eq_bv ? n1 (zero ?)) then (repr ? 1) else (zero ?)))
       | Vptr _ ⇒ Some ? (Vint sz (zero ?))
-      | Vnull _ ⇒ Some ? (Vint sz (repr ? 1))
+      | Vnull ⇒ Some ? (Vint sz (repr ? 1))
       | _ ⇒ None ?
       ]
@@ -145 +145 @@
   | Oid t ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
   (* Only conversion of null pointers is specified. *)
-  | Optrofint sz sg r ⇒ match arg with [ Vint sz1 n1 ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
-  | Ointofptr sz sg r ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
+  | Optrofint sz sg ⇒ match arg with [ Vint sz1 n1 ⇒ if eq_bv ? n1 (zero ?) then Some ? Vnull else None ? | _ ⇒ None ? ]
+  | Ointofptr sz sg ⇒ match arg with [ Vnull ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
   ].
 
@@ -159 +159 @@
 | #t'' #sz #sg cases t''
   [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?); #E' destruct cases (eq_bv ???) whd in ⊢ (?%?); %
-  | #r #H #v #v' #H1 @(elim_val_typ … H1) whd %
+  | #H #v #v' #H1 @(elim_val_typ … H1) whd %
     [ whd in ⊢ (??%? → ?); #E' destruct; %
-    | #b #c #o whd in ⊢ (??%? → ?); #E' destruct %
+    | #b #o whd in ⊢ (??%? → ?); #E' destruct %
     ]
   | #f *
@@ -174 +174 @@
 | #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
 | #t'' #v #v' #H whd in ⊢ (??%? → ?); #E destruct @H
-| #sz #sg #r #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); cases (eq_bv ???)
+| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); cases (eq_bv ???)
   whd in ⊢ (??%? → ?); #E destruct //
-| #sz #sg #r #v #v' #H @(elim_val_typ … H) %
+| #sz #sg #v #v' #H @(elim_val_typ … H) %
   [ whd in ⊢ (??%? → ?); #E destruct %
-  | #b #c #o whd in ⊢ (??%? → ?); #E destruct
+  | #b #o whd in ⊢ (??%? → ?); #E destruct
   ]
 ] qed.
@@ -215 +215 @@
     [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer ? ptr1 n2))
     | _ ⇒ None ? ]
-  | Vnull r ⇒ match v2 with
-    [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
+  | Vnull ⇒ match v2 with
+    [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ?
     | _ ⇒ None ?
     ]
@@ -226 +226 @@
     [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer ? ptr1 n2))
     | _ ⇒ None ? ]
-  | Vnull r ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
+  | Vnull ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ? | _ ⇒ None ? ]
   | _ ⇒ None ? ].
 
@@ -237 +237 @@
           else None ?
     | _ ⇒ None ? ]
-  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
+  | Vnull  ⇒ match v2 with [ Vnull  ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
   | _ ⇒ None ? ].
 
@@ -411 +411 @@
         then Some ? (FE_of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
         else ev_cmp_mismatch c
-    | Vnull r2 ⇒ ev_cmp_mismatch c
-    | _ ⇒ None ? ]
-  | Vnull r1 ⇒ match v2 with
+    | Vnull  ⇒ ev_cmp_mismatch c
+    | _ ⇒ None ? ]
+  | Vnull  ⇒ match v2 with
     [ Vptr _ ⇒ ev_cmp_mismatch c
-    | Vnull r2 ⇒ ev_cmp_match c
+    | Vnull  ⇒ ev_cmp_match c
     | _ ⇒ None ?
     ]
@@ -460 +460 @@
   | Ocmpu _ _ c ⇒ ev_cmpu c
   | Ocmpf _ _ c ⇒ ev_cmpf c
-  | Oaddp _ _ ⇒ ev_addp
-  | Osubpi _ _ ⇒ ev_subpi
-  | Osubpp sz _ _ ⇒ ev_subpp sz
-  | Ocmpp _ _ c ⇒ ev_cmpp c
+  | Oaddp _ ⇒ ev_addp
+  | Osubpi _ ⇒ ev_subpi
+  | Osubpp sz ⇒ ev_subpp sz
+  | Ocmpp _ c ⇒ ev_cmpp c
   ].
 
@@ -496 +496 @@
   whd in ⊢ (??%? → ?); cases (Fcmp ???) #E destruct //
 (* pointers *)
-| 21,22: #sz #r #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #c #o ] @(elim_val_typ … V2) #i2
+| 21,22: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #o ] @(elim_val_typ … V2) #i2
   whd in ⊢ (??%? → ?); [ 3,4: cases (eq_bv ???) whd in ⊢ (??%? → ?); | ] #E destruct //
-| #sz #r1 #r2 #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ | #b1 #c1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #c2 #o2 ]
+| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ | #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ]
   whd in ⊢ (??%? → ?); [ 2: cases (eq_block ??) whd in ⊢ (??%? → ?); | ] #E destruct //
-| #r #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2: #b1 #c1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #c2 #o2 ]
+| #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2: #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ]
   whd in ⊢ (??%? → ?); [ cases (eq_block ??) cases (cmp_offset ???) ] cases c whd in ⊢ (??%? → ?); #E destruct //
 ] qed.