Changeset 2176 for src/common/FrontEndOps.ma
- Timestamp:
- Jul 12, 2012, 1:28:28 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/FrontEndOps.ma
r2032 r2176 23 23 | Ointconst: ∀sz,sg. bvint sz → constant (ASTint sz sg) 24 24 | 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 28 definition boolsrc : typ → Prop ≝ λt. match t with [ ASTint _ _ ⇒ True | ASTptr ⇒ True | _ ⇒ False ]. 29 29 30 30 inductive unary_operation : typ → typ → Type[0] ≝ … … 41 41 | Ofloatofintu: ∀fsz,sz. unary_operation (ASTint sz Unsigned) (ASTfloat fsz) (**r float to unsigned integer *) 42 42 | 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 *) 45 45 46 46 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 *) 66 66 | 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 *) 71 71 72 72 … … 76 76 [ ASTint sz sg ⇒ ∀i.P (Vint sz i) 77 77 | ASTfloat sz ⇒ ∀f.P (Vfloat f) 78 | ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr (mk_pointer r b co))78 | ASTptr ⇒ P Vnull ∧ ∀b,o. P (Vptr (mk_pointer b o)) 79 79 ] → 80 80 P v. 81 81 #v #t #P * 82 82 [ 1,2: // 83 | #r* //84 | # r #b #c#o * //83 | * // 84 | #b #o * // 85 85 ] qed. 86 86 … … 95 95 [ Ointconst sz sg n ⇒ Some ? (Vint sz n) 96 96 | Ofloatconst sz n ⇒ Some ? (Vfloat n) 97 | Oaddrsymbol rs ofs ⇒97 | Oaddrsymbol s ofs ⇒ 98 98 match find_symbol s with 99 99 [ None ⇒ None ? 100 | Some b ⇒ match pointer_compat_dec b r with100 | Some b ⇒ (*match pointer_compat_dec b r with 101 101 [ inl pc ⇒ Some ? (Vptr (mk_pointer r b pc (shift_offset ? zero_offset (repr I16 ofs)))) 102 102 | inr _ ⇒ None ? 103 ] 103 ]*) Some ? (Vptr (mk_pointer b (shift_offset ? zero_offset (repr I16 ofs)))) 104 104 ] 105 105 | 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.*) 108 108 109 109 lemma eval_constant_typ_correct : ∀t,f,sp,c,v. … … 113 113 [ #sz #sg #i #v #E normalize in E; destruct // 114 114 | #sz #f #v #E normalize in E; destruct // 115 | # r #id #n #v whd in ⊢ (??%? → ?); cases (f id) [2:#b] #E whd in E:(??%?); destruct116 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 *) 117 117 // 118 118 | #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 ?))) 133 133 | Vptr _ ⇒ Some ? (Vint sz (zero ?)) 134 | Vnull _⇒ Some ? (Vint sz (repr ? 1))134 | Vnull ⇒ Some ? (Vint sz (repr ? 1)) 135 135 | _ ⇒ None ? 136 136 ] … … 145 145 | Oid t ⇒ Some ? arg (* XXX should we restricted the values allowed? *) 146 146 (* 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 ? ] 149 149 ]. 150 150 … … 159 159 | #t'' #sz #sg cases t'' 160 160 [ #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 % 162 162 [ whd in ⊢ (??%? → ?); #E' destruct; % 163 | #b # c #o whd in ⊢ (??%? → ?); #E' destruct %163 | #b #o whd in ⊢ (??%? → ?); #E' destruct % 164 164 ] 165 165 | #f * … … 174 174 | #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2 175 175 | #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 ???) 177 177 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) % 179 179 [ whd in ⊢ (??%? → ?); #E destruct % 180 | #b # c #o whd in ⊢ (??%? → ?); #E destruct180 | #b #o whd in ⊢ (??%? → ?); #E destruct 181 181 ] 182 182 ] qed. … … 215 215 [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer ? ptr1 n2)) 216 216 | _ ⇒ None ? ] 217 | Vnull r⇒ match v2 with218 [ 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 ? 219 219 | _ ⇒ None ? 220 220 ] … … 226 226 [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer ? ptr1 n2)) 227 227 | _ ⇒ 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 ? ] 229 229 | _ ⇒ None ? ]. 230 230 … … 237 237 else None ? 238 238 | _ ⇒ 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 ? ] 240 240 | _ ⇒ None ? ]. 241 241 … … 411 411 then Some ? (FE_of_bool (cmp_offset c (poff ptr1) (poff ptr2))) 412 412 else ev_cmp_mismatch c 413 | Vnull r2⇒ ev_cmp_mismatch c414 | _ ⇒ None ? ] 415 | Vnull r1⇒ match v2 with413 | Vnull ⇒ ev_cmp_mismatch c 414 | _ ⇒ None ? ] 415 | Vnull ⇒ match v2 with 416 416 [ Vptr _ ⇒ ev_cmp_mismatch c 417 | Vnull r2⇒ ev_cmp_match c417 | Vnull ⇒ ev_cmp_match c 418 418 | _ ⇒ None ? 419 419 ] … … 460 460 | Ocmpu _ _ c ⇒ ev_cmpu c 461 461 | Ocmpf _ _ c ⇒ ev_cmpf c 462 | Oaddp _ _⇒ ev_addp463 | Osubpi _ _⇒ ev_subpi464 | Osubpp sz _ _⇒ ev_subpp sz465 | Ocmpp _ _c ⇒ ev_cmpp c462 | Oaddp _ ⇒ ev_addp 463 | Osubpi _ ⇒ ev_subpi 464 | Osubpp sz ⇒ ev_subpp sz 465 | Ocmpp _ c ⇒ ev_cmpp c 466 466 ]. 467 467 … … 496 496 whd in ⊢ (??%? → ?); cases (Fcmp ???) #E destruct // 497 497 (* pointers *) 498 | 21,22: #sz # r #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #c#o ] @(elim_val_typ … V2) #i2498 | 21,22: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #o ] @(elim_val_typ … V2) #i2 499 499 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 ] 501 501 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 ] 503 503 whd in ⊢ (??%? → ?); [ cases (eq_block ??) cases (cmp_offset ???) ] cases c whd in ⊢ (??%? → ?); #E destruct // 504 504 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.