Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r2032 r2176  
    2323  | Ointconst: ∀sz,sg. bvint sz → constant (ASTint sz sg)
    2424  | Ofloatconst: ∀sz. float → constant (ASTfloat sz)
    25   | Oaddrsymbol: ∀r. ident → nat → constant (ASTptr r) (**r address of the symbol plus the offset *)
    26   | Oaddrstack: nat → constant (ASTptr Any).         (**r stack pointer plus the given offset *)
    27 
    28 definition boolsrc : typ → Prop ≝ λt. match t with [ ASTint _ _ ⇒ True | ASTptr _ ⇒ True | _ ⇒ False ].
     25  | Oaddrsymbol: ident → nat → constant ASTptr (**r address of the symbol plus the offset *)
     26  | Oaddrstack: nat → constant ASTptr.         (**r stack pointer plus the given offset *)
     27
     28definition boolsrc : typ → Prop ≝ λt. match t with [ ASTint _ _ ⇒ True | ASTptr ⇒ True | _ ⇒ False ].
    2929
    3030inductive unary_operation : typ → typ → Type[0] ≝
     
    4141  | Ofloatofintu: ∀fsz,sz. unary_operation (ASTint sz Unsigned) (ASTfloat fsz) (**r float to unsigned integer *)
    4242  | Oid: ∀t. unary_operation t t                                               (**r identity (used to move between registers *)
    43   | Optrofint: ∀sz,sg,r. unary_operation (ASTint sz sg) (ASTptr r)             (**r int to pointer with given representation *)
    44   | Ointofptr: ∀sz,sg,r. unary_operation (ASTptr r) (ASTint sz sg).            (**r pointer to int *)
     43  | Optrofint: ∀sz,sg. unary_operation (ASTint sz sg) ASTptr                   (**r int to pointer with given representation *)
     44  | Ointofptr: ∀sz,sg. unary_operation ASTptr (ASTint sz sg).                  (**r pointer to int *)
    4545
    4646inductive binary_operation : typ → typ → typ → Type[0] ≝
     
    6565  | Ocmpu: ∀sz,sg'.   comparison -> binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint I8 sg') (**r integer unsigned comparison *)
    6666  | Ocmpf: ∀sz,sg'.   comparison -> binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTint I8 sg') (**r float comparison *)
    67   | Oaddp: ∀sz,r.  binary_operation (ASTptr r)           (ASTint sz Signed)   (ASTptr r)           (**r add an integer to a pointer *)
    68   | Osubpi: ∀sz,r. binary_operation (ASTptr r)           (ASTint sz Signed)   (ASTptr r)           (**r subtract int from a pointers *)
    69   | Osubpp: ∀sz,r1,r2. binary_operation (ASTptr r1)      (ASTptr r2)          (ASTint sz Signed)   (**r subtract two pointers *)
    70   | Ocmpp: ∀r,sg'. comparison → binary_operation (ASTptr r) (ASTptr r) (ASTint I8 sg').  (**r compare pointers *)
     67  | Oaddp: ∀sz.    binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r add an integer to a pointer *)
     68  | Osubpi: ∀sz.   binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r subtract int from a pointers *)
     69  | Osubpp: ∀sz.   binary_operation  ASTptr               ASTptr              (ASTint sz Signed)   (**r subtract two pointers *)
     70  | Ocmpp: ∀sg'. comparison → binary_operation ASTptr     ASTptr              (ASTint I8 sg').  (**r compare pointers *)
    7171
    7272
     
    7676[ ASTint sz sg ⇒ ∀i.P (Vint sz i)
    7777| ASTfloat sz ⇒ ∀f.P (Vfloat f)
    78 | ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr (mk_pointer r b c o))
     78| ASTptr ⇒ P Vnull ∧ ∀b,o. P (Vptr (mk_pointer b o))
    7979] →
    8080P v.
    8181#v #t #P *
    8282[ 1,2: //
    83 | #r * //
    84 | #r #b #c #o * //
     83| * //
     84| #b #o * //
    8585] qed.
    8686
     
    9595  [ Ointconst sz sg n ⇒ Some ? (Vint sz n)
    9696  | Ofloatconst sz n ⇒ Some ? (Vfloat n)
    97   | Oaddrsymbol r s ofs ⇒
     97  | Oaddrsymbol s ofs ⇒
    9898      match find_symbol s with
    9999      [ None ⇒ None ?
    100       | Some b ⇒ match pointer_compat_dec b r with
     100      | Some b ⇒ (*match pointer_compat_dec b r with
    101101                 [ inl pc ⇒ Some ? (Vptr (mk_pointer r b pc (shift_offset ? zero_offset (repr I16 ofs))))
    102102                 | inr _ ⇒ None ?
    103                  ]
     103                 ]*) Some ? (Vptr (mk_pointer b (shift_offset ? zero_offset (repr I16 ofs))))
    104104      ]
    105105  | Oaddrstack ofs ⇒
    106       Some ? (Vptr (mk_pointer Any sp ? (shift_offset ? zero_offset (repr I16 ofs))))
    107   ]. cases sp // qed.
     106      Some ? (Vptr (mk_pointer sp (shift_offset ? zero_offset (repr I16 ofs))))
     107  ]. (*cases sp // qed.*)
    108108
    109109lemma eval_constant_typ_correct : ∀t,f,sp,c,v.
     
    113113[ #sz #sg #i #v #E normalize in E; destruct //
    114114| #sz #f #v #E normalize in E; destruct //
    115 | #r #id #n #v whd in ⊢ (??%? → ?); cases (f id) [2:#b] #E whd in E:(??%?); destruct
    116   cases (pointer_compat_dec b r) in E; #pc #E whd in E:(??%?); destruct
     115| #id #n #v whd in ⊢ (??%? → ?); cases (f id) [2:#b] #E whd in E:(??%?); destruct
     116(*  cases (pointer_compat_dec b r) in E; #pc #E whd in E:(??%?); destruct *)
    117117  //
    118118| #n #v #E whd in E:(??%?); destruct //
     
    132132      [ Vint sz1 n1 ⇒ Some ? (Vint sz (if (eq_bv ? n1 (zero ?)) then (repr ? 1) else (zero ?)))
    133133      | Vptr _ ⇒ Some ? (Vint sz (zero ?))
    134       | Vnull _ ⇒ Some ? (Vint sz (repr ? 1))
     134      | Vnull ⇒ Some ? (Vint sz (repr ? 1))
    135135      | _ ⇒ None ?
    136136      ]
     
    145145  | Oid t ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
    146146  (* Only conversion of null pointers is specified. *)
    147   | Optrofint sz sg r ⇒ match arg with [ Vint sz1 n1 ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
    148   | Ointofptr sz sg r ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
     147  | Optrofint sz sg ⇒ match arg with [ Vint sz1 n1 ⇒ if eq_bv ? n1 (zero ?) then Some ? Vnull else None ? | _ ⇒ None ? ]
     148  | Ointofptr sz sg ⇒ match arg with [ Vnull ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
    149149  ].
    150150
     
    159159| #t'' #sz #sg cases t''
    160160  [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?); #E' destruct cases (eq_bv ???) whd in ⊢ (?%?); %
    161   | #r #H #v #v' #H1 @(elim_val_typ … H1) whd %
     161  | #H #v #v' #H1 @(elim_val_typ … H1) whd %
    162162    [ whd in ⊢ (??%? → ?); #E' destruct; %
    163     | #b #c #o whd in ⊢ (??%? → ?); #E' destruct %
     163    | #b #o whd in ⊢ (??%? → ?); #E' destruct %
    164164    ]
    165165  | #f *
     
    174174| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
    175175| #t'' #v #v' #H whd in ⊢ (??%? → ?); #E destruct @H
    176 | #sz #sg #r #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); cases (eq_bv ???)
     176| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); cases (eq_bv ???)
    177177  whd in ⊢ (??%? → ?); #E destruct //
    178 | #sz #sg #r #v #v' #H @(elim_val_typ … H) %
     178| #sz #sg #v #v' #H @(elim_val_typ … H) %
    179179  [ whd in ⊢ (??%? → ?); #E destruct %
    180   | #b #c #o whd in ⊢ (??%? → ?); #E destruct
     180  | #b #o whd in ⊢ (??%? → ?); #E destruct
    181181  ]
    182182] qed.
     
    215215    [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer ? ptr1 n2))
    216216    | _ ⇒ None ? ]
    217   | Vnull r ⇒ match v2 with
    218     [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
     217  | Vnull ⇒ match v2 with
     218    [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ?
    219219    | _ ⇒ None ?
    220220    ]
     
    226226    [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer ? ptr1 n2))
    227227    | _ ⇒ None ? ]
    228   | Vnull r ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
     228  | Vnull ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ? | _ ⇒ None ? ]
    229229  | _ ⇒ None ? ].
    230230
     
    237237          else None ?
    238238    | _ ⇒ None ? ]
    239   | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
     239  | Vnull  ⇒ match v2 with [ Vnull ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
    240240  | _ ⇒ None ? ].
    241241
     
    411411        then Some ? (FE_of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
    412412        else ev_cmp_mismatch c
    413     | Vnull r2 ⇒ ev_cmp_mismatch c
    414     | _ ⇒ None ? ]
    415   | Vnull r1 ⇒ match v2 with
     413    | Vnull ⇒ ev_cmp_mismatch c
     414    | _ ⇒ None ? ]
     415  | Vnull ⇒ match v2 with
    416416    [ Vptr _ ⇒ ev_cmp_mismatch c
    417     | Vnull r2 ⇒ ev_cmp_match c
     417    | Vnull ⇒ ev_cmp_match c
    418418    | _ ⇒ None ?
    419419    ]
     
    460460  | Ocmpu _ _ c ⇒ ev_cmpu c
    461461  | Ocmpf _ _ c ⇒ ev_cmpf c
    462   | Oaddp _ _ ⇒ ev_addp
    463   | Osubpi _ _ ⇒ ev_subpi
    464   | Osubpp sz _ _ ⇒ ev_subpp sz
    465   | Ocmpp _ _ c ⇒ ev_cmpp c
     462  | Oaddp _ ⇒ ev_addp
     463  | Osubpi _ ⇒ ev_subpi
     464  | Osubpp sz ⇒ ev_subpp sz
     465  | Ocmpp _ c ⇒ ev_cmpp c
    466466  ].
    467467
     
    496496  whd in ⊢ (??%? → ?); cases (Fcmp ???) #E destruct //
    497497(* pointers *)
    498 | 21,22: #sz #r #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #c #o ] @(elim_val_typ … V2) #i2
     498| 21,22: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #o ] @(elim_val_typ … V2) #i2
    499499  whd in ⊢ (??%? → ?); [ 3,4: cases (eq_bv ???) whd in ⊢ (??%? → ?); | ] #E destruct //
    500 | #sz #r1 #r2 #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ | #b1 #c1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #c2 #o2 ]
     500| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ | #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ]
    501501  whd in ⊢ (??%? → ?); [ 2: cases (eq_block ??) whd in ⊢ (??%? → ?); | ] #E destruct //
    502 | #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 ]
     502| #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2: #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ]
    503503  whd in ⊢ (??%? → ?); [ cases (eq_block ??) cases (cmp_offset ???) ] cases c whd in ⊢ (??%? → ?); #E destruct //
    504504] qed.
Note: See TracChangeset for help on using the changeset viewer.