Changeset 2569


Ignore:
Timestamp:
Jan 4, 2013, 2:59:37 PM (7 years ago)
Author:
campbell
Message:

Fix Clight semantics for ptr + char. (Compiler works anyway.)

Location:
src
Files:
3 added
4 edited

Legend:

Unmodified
Added
Removed

  • src/Clight/Csem.ma

    r2560 r2569  
    110110        | _ ⇒ None ? ]
    111111      | _ ⇒ None ? ]
    112   | add_case_pi _ ty _ _ ⇒                    (**r pointer plus integer *)
     112  | add_case_pi _ ty _ sg ⇒                    (**r pointer plus integer *)
    113113      match v1 with
    114114      [ 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))
    116116        | _ ⇒ None ? ]
    117117      | Vnull ⇒ match v2 with
    … …  
    119119        | _ ⇒ None ? ]
    120120      | _ ⇒ None ? ]
    121   | add_case_ip _ _ _ ty ⇒                    (**r integer plus pointer *)
     121  | add_case_ip _ _ sg ty ⇒                    (**r integer plus pointer *)
    122122      match v1 with
    123123      [ 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))
    125125        | Vnull ⇒ if eq_bv ? n1 (zero ?) then Some ? Vnull else None ?
    126126        | _ ⇒ None ? ]
    … …  
    138138        | _ ⇒ None ? ]
    139139      | _ ⇒ None ? ]
    140   | sub_case_pi _ ty _ _ ⇒             (**r pointer minus integer *)
     140  | sub_case_pi _ ty _ sg ⇒             (**r pointer minus integer *)
    141141      match v1 with
    142142      [ 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))
    144144        | _ ⇒ None ? ]
    145145      | Vnull ⇒ match v2 with

  • src/Clight/memoryInjections.ma

    r2565 r2569  
    14361436     | 3: #Heq destruct (Heq)
    14371437          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 @refl
     1438          @(ex_intro … (conj … (refl …) ?))
    14391439          @vptr_eq whd in match (pointer_translation ??);
    14401440          cases (E b1') in Hembed;
    … …  
    14421442          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
    14431443               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))
    14461446               [ 1: whd in match (offset_plus ??);
    14471447                    whd in match (shift_offset_n ????) in ⊢ (??%%);
    … …  
    14771477     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
    14781478     #Heq destruct (Heq)
    1479      %{(Vptr (shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
     1479     @(ex_intro … (conj … (refl …) ?))
    14801480     @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
    14811481     elim p1 in Hembed; #b1 #o1 normalize nodelta
    … …  
    15721572     [ 1,2,4,5,6,7: #Habsurd destruct (Habsurd) ]
    15731573     #Heq destruct (Heq)
    1574      [ 1: %{(Vptr (neg_shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
     1574     [ 1: @(ex_intro … (conj … (refl …) ?))
    15751575          @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
    15761576          elim p1 in Hembed; #b1 #o1 normalize nodelta
    … …  
    15791579          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
    15801580               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 ⊢ (??%%);
    15831583               whd in match (subtraction) in ⊢ (??%%); normalize nodelta
    15841584               generalize in match (short_multiplication ???); #mult

  • src/Clight/toCminorCorrectness.ma

    r2568 r2569  
    608608  sem_add v1 (Tint sz sg) v2 (ptr_type ty' optlen) = Some ? res →
    609609  ∃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)) ∨
    611611       (v2 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
    612612#tsz #tsg #ty' * [ | #n ]
    … …  
    637637  sem_add v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res →
    638638  ∃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)) ∨
    640640       (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
    641641#tsz #tsg #ty' * [ | #n ]

  • src/common/Pointers.ma

    r2296 r2569  
    104104  λn,o,i. mk_offset (addition_n ? (offv o) (sign_ext … i)).
    105105(* 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))).
     106definition 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]))).
    108108definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
    109109  λ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))).
     110definition 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]))).
    112112definition sub_offset : ∀n. offset → offset → BitVector n ≝
    113113  λn,x,y. sign_ext … (subtraction ? (offv x) (offv y)).
    … …  
    132132
    133133(* 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) i j).
     134definition 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).
    136136
    137137definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝
    138138 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset n (poff p) i).
    139139
    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) i j).
     140definition 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).
    142142
    143143definition eq_pointer: pointer → pointer → bool ≝
Note: See TracChangeset for help on using the changeset viewer.