Changeset 2569 for src/Clight


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/Clight
Files:
3 added
3 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 ]
Note: See TracChangeset for help on using the changeset viewer.