Changeset 2569
- Timestamp:
- Jan 4, 2013, 2:59:37 PM (8 years ago)
- Location:
- src
- Files:
-
- 3 added
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/Csem.ma
r2560 r2569 110 110 | _ ⇒ None ? ] 111 111 | _ ⇒ None ? ] 112 | add_case_pi _ ty _ _⇒ (**r pointer plus integer *)112 | add_case_pi _ ty _ sg ⇒ (**r pointer plus integer *) 113 113 match v1 with 114 114 [ Vptr ptr1 ⇒ match v2 with 115 [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr1 (sizeof ty) n2))115 [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr1 (sizeof ty) sg n2)) 116 116 | _ ⇒ None ? ] 117 117 | Vnull ⇒ match v2 with … … 119 119 | _ ⇒ None ? ] 120 120 | _ ⇒ None ? ] 121 | add_case_ip _ _ _ty ⇒ (**r integer plus pointer *)121 | add_case_ip _ _ sg ty ⇒ (**r integer plus pointer *) 122 122 match v1 with 123 123 [ Vint sz1 n1 ⇒ match v2 with 124 [ Vptr ptr2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr2 (sizeof ty) n1))124 [ Vptr ptr2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr2 (sizeof ty) sg n1)) 125 125 | Vnull ⇒ if eq_bv ? n1 (zero ?) then Some ? Vnull else None ? 126 126 | _ ⇒ None ? ] … … 138 138 | _ ⇒ None ? ] 139 139 | _ ⇒ None ? ] 140 | sub_case_pi _ ty _ _⇒ (**r pointer minus integer *)140 | sub_case_pi _ ty _ sg ⇒ (**r pointer minus integer *) 141 141 match v1 with 142 142 [ Vptr ptr1 ⇒ match v2 with 143 [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer_n ? ptr1 (sizeof ty) n2))143 [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer_n ? ptr1 (sizeof ty) sg n2)) 144 144 | _ ⇒ None ? ] 145 145 | Vnull ⇒ match v2 with -
src/Clight/memoryInjections.ma
r2565 r2569 1436 1436 | 3: #Heq destruct (Heq) 1437 1437 normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed 1438 %{(Vptr (shift_pointer_n (bitsize_of_intsize sz) p2' (sizeof ty) i))} @conj try @refl1438 @(ex_intro … (conj … (refl …) ?)) 1439 1439 @vptr_eq whd in match (pointer_translation ??); 1440 1440 cases (E b1') in Hembed; … … 1442 1442 | 2: * #block #offset normalize nodelta #Heq destruct (Heq) 1443 1443 whd in match (shift_pointer_n ????); 1444 cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) i) offset =1445 (shift_offset_n (bitsize_of_intsize sz) (mk_offset (addition_n ? (offv o1') (offv offset))) (sizeof ty) i))1444 cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) tsg i) offset = 1445 (shift_offset_n (bitsize_of_intsize sz) (mk_offset (addition_n ? (offv o1') (offv offset))) (sizeof ty) tsg i)) 1446 1446 [ 1: whd in match (offset_plus ??); 1447 1447 whd in match (shift_offset_n ????) in ⊢ (??%%); … … 1477 1477 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 1478 1478 #Heq destruct (Heq) 1479 %{(Vptr (shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl1479 @(ex_intro … (conj … (refl …) ?)) 1480 1480 @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %; 1481 1481 elim p1 in Hembed; #b1 #o1 normalize nodelta … … 1572 1572 [ 1,2,4,5,6,7: #Habsurd destruct (Habsurd) ] 1573 1573 #Heq destruct (Heq) 1574 [ 1: %{(Vptr (neg_shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl1574 [ 1: @(ex_intro … (conj … (refl …) ?)) 1575 1575 @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %; 1576 1576 elim p1 in Hembed; #b1 #o1 normalize nodelta … … 1579 1579 | 2: * #block #offset normalize nodelta #Heq destruct (Heq) 1580 1580 whd in match (offset_plus ??) in ⊢ (??%%); 1581 whd in match (neg_shift_pointer_n ???? ) in ⊢ (??%%);1582 whd in match (neg_shift_offset_n ???? ) in ⊢ (??%%);1581 whd in match (neg_shift_pointer_n ?????) in ⊢ (??%%); 1582 whd in match (neg_shift_offset_n ?????) in ⊢ (??%%); 1583 1583 whd in match (subtraction) in ⊢ (??%%); normalize nodelta 1584 1584 generalize in match (short_multiplication ???); #mult -
src/Clight/toCminorCorrectness.ma
r2568 r2569 608 608 sem_add v1 (Tint sz sg) v2 (ptr_type ty' optlen) = Some ? res → 609 609 ∃sz',i. v1 = Vint sz' i ∧ 610 ((∃p. v2 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') i)) ∨610 ((∃p. v2 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨ 611 611 (v2 = Vnull ∧ i = (zero ?) ∧ res = Vnull)). 612 612 #tsz #tsg #ty' * [ | #n ] … … 637 637 sem_add v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res → 638 638 ∃sz',i. v2 = Vint sz' i ∧ 639 ((∃p. v1 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') i)) ∨639 ((∃p. v1 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨ 640 640 (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)). 641 641 #tsz #tsg #ty' * [ | #n ] -
src/common/Pointers.ma
r2296 r2569 104 104 λn,o,i. mk_offset (addition_n ? (offv o) (sign_ext … i)). 105 105 (* A version of shift_offset_n for multiplied addresses which avoids overflow. *) 106 definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝107 λn,o,i, j. mk_offset (addition_n ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))).106 definition shift_offset_n : ∀n. offset → nat → signedness → BitVector n → offset ≝ 107 λn,o,i,sg,j. mk_offset (addition_n ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (match sg with [ Signed ⇒ sign_ext … j | _ ⇒ zero_ext … j]))). 108 108 definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝ 109 109 λn,o,i. mk_offset (subtraction ? (offv o) (sign_ext … i)). 110 definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝111 λn,o,i, j. mk_offset (subtraction ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))).110 definition neg_shift_offset_n : ∀n. offset → nat → signedness → BitVector n → offset ≝ 111 λn,o,i,sg,j. mk_offset (subtraction ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (match sg with [ Signed ⇒ sign_ext … j | _ ⇒ zero_ext … j]))). 112 112 definition sub_offset : ∀n. offset → offset → BitVector n ≝ 113 113 λn,x,y. sign_ext … (subtraction ? (offv x) (offv y)). … … 132 132 133 133 (* multiply shift by a nat (i.e., sizeof) without danger of overflow *) 134 definition shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝135 λn,p,i, j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset_n n (poff p) ij).134 definition shift_pointer_n: ∀n. pointer → nat → signedness → BitVector n → pointer ≝ 135 λn,p,i,sg,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset_n n (poff p) i sg j). 136 136 137 137 definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝ 138 138 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset n (poff p) i). 139 139 140 definition neg_shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝141 λn,p,i, j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset_n n (poff p) ij).140 definition neg_shift_pointer_n: ∀n. pointer → nat → signedness → BitVector n → pointer ≝ 141 λn,p,i,sg,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset_n n (poff p) i sg j). 142 142 143 143 definition eq_pointer: pointer → pointer → bool ≝
Note: See TracChangeset
for help on using the changeset viewer.