Changeset 500


Ignore:
Timestamp:
Feb 11, 2011, 4:45:38 PM (6 years ago)
Author:
campbell
Message:

Use dependent pointer type to ensure that the representation is always
compatible with the memory region used.
Add a couple of missing checks as a result...

Location:
Deliverables/D3.1/C-semantics
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Cexec.ma

    r499 r500  
    5252    | _ ⇒ Error ?
    5353    ]
    54   | Vptr _ _ _ ⇒ match ty with
     54  | Vptr _ _ _ _ ⇒ match ty with
    5555    [ Tpointer _ _ ⇒ OK ? true
    5656    | _ ⇒ Error ?
     
    6666#v #ty #r #H elim H; #v #t #H' elim H';
    6767  [ #i #is #s #ne %{ true} % //; whd in ⊢ (??%?); >(eq_false … ne) //;
    68   | #p #b #i #i0 #s %{ true} % //
     68  | #r #b #pc #i #i0 #s %{ true} % //
    6969  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //;
    7070  | #i #s %{ false} % //;
     
    164164  | _ ⇒ Error ?
    165165  ]
    166 | Vptr p b ofs ⇒
     166| Vptr r b _ ofs ⇒
    167167    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];
    168     do u ← match eq_region_dec p s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? ];
     168    do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? ];
    169169    do s' ← match ty' with
    170170         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
    171171         | _ ⇒ Error ? ];
    172     if is_pointer_compat b s'
    173     then OK ? (Vptr s' b ofs)
    174     else Error ?
     172    match pointer_compat_dec b s' with
     173    [ inl p' ⇒ OK ? (Vptr s' b p' ofs)
     174    | inr _ ⇒ Error ?
     175    ]
    175176| Vnull r ⇒
    176177    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];
     
    211212      do 〈lo,tr〉 ← exec_lvalue ge en m a;
    212213      match ty with
    213       [ Tpointer r _ ⇒ OK ? 〈match lo with [ pair loc ofs ⇒  Vptr r loc ofs ], tr〉
     214      [ Tpointer r _ ⇒
     215        match lo with [ pair loc ofs ⇒
     216          match pointer_compat_dec loc r with
     217          [ inl pc ⇒ OK ? 〈Vptr r loc pc ofs, tr〉
     218          | inr _ ⇒ Error ?
     219          ]
     220        ]
    214221      | _ ⇒ Error ?
    215222      ]
     
    266273      do 〈v,tr〉 ← exec_expr ge en m a;
    267274      match v with
    268       [ Vptr _ l ofs ⇒ OK ? 〈〈l,ofs〉,tr〉
     275      [ Vptr _ l _ ofs ⇒ OK ? 〈〈l,ofs〉,tr〉
    269276      | _ ⇒ Error ?
    270277      ]
     
    669676    | #f %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    670677    | #r %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    671     | #r #b #of %2 ; % *;   #r #H inversion H; #i #m #e destruct;
     678    | #r #b #pc #of %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    672679    ]
    673680  | #a #b %2 ; % *; #r #H inversion H; #i #m #e destruct;
     
    754761  | #fd #args #k #mem
    755762  | #v #k #mem (* for final state check *) cases k;
    756     [ cases v; [ 2,3: #v' | 4: #r | 5: #sp #loc #off ]
     763    [ cases v; [ 2,3: #v' | 4: #r | 5: #r #loc #pc #off ]
    757764    | #s' #k' | 3,4: #e #s' #k' | 5,6: #e #s' #s'' #k' | #k' | #a #b #c #d ]
    758765  ]
  • Deliverables/D3.1/C-semantics/CexecComplete.ma

    r499 r500  
    4848] qed.
    4949
    50 lemma eq_region_dec_true: ∀s. eq_region_dec s s = inl ???.
    51 [ #s cases s; @refl
    52 | skip
     50lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inl ?? p')) → Q f.
     51#P #f #p #Q #H cases f;
     52[ @H
     53| #np cut False [ @(absurd ? p np) | * ]
     54] qed.
     55
     56lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inr ?? p')) → Q f.
     57#P #f #p #Q #H cases f;
     58[ #np cut False [ @(absurd ? np p) | * ]
     59| @H
    5360] qed.
    5461
     
    105112| #m #i #sz #sz' #sg @refl
    106113| #m #f #sz #sz' @refl
    107 | #m #sp #sp' #ty #ty' #b #ofs #H1 #H2 #H3
    108     elim H1; [ #sp1 #ty1 | #sp1 #ty1 #n1 | #tys1 #ty1 letin sp1 ≝ Code ]
    109     whd in ⊢ (??%?);
    110     [ 1,2: >(eq_region_dec_true …) whd in ⊢ (??%?); ]
    111     elim H2 in H3 ⊢ %; [ 1,4,7: #sp2 #ty2 | 2,5,8: #sp2 #ty2 #n2 | 3,6,9: #tys2 #ty2 letin sp2 ≝ Code ]
    112     #H3 whd in ⊢ (??%?);
    113     >(is_pointer_compat_true …) //;
     114| #m #r #r' #ty #ty' #b #pc #ofs #H1 #H2 #pc'
     115    elim H1 in pc ⊢ % [ #r1 #ty1 #pc | #r1 #ty1 #n1 #pc | #tys1 #ty1 #pc letin r1 ≝ Code ]
     116    whd in ⊢ (??%?)
     117    [ 1,2: @(dec_true ? (eq_region_dec r1 r1) (refl ??) …) #H0 whd in ⊢ (??%?) ]
     118    elim H2 in pc' ⊢ %; [ 1,4,7: #sp2 #ty2 | 2,5,8: #sp2 #ty2 #n2 | 3,6,9: #tys2 #ty2 letin sp2 ≝ Code ]
     119    #pc' whd in ⊢ (??%?)
     120    @(dec_true ? (pointer_compat_dec b sp2) pc') //
    114121| #m #sz #si #ty'' #r #H cases H; //;
    115122| #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f
    116     whd in ⊢ (??%?); try @refl >eq_region_dec_true @refl
     123    whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl
    117124] qed.
    118125
     
    133140#v #ty #r #H elim H; #v #t #H' elim H';
    134141  [ #i #is #s #ne %{ true} % //; whd; >(eq_false … ne) //;
    135   | #p #b #i #i0 #s %{ true} % //
     142  | #r #b #pc #i #i0 #s %{ true} % //
    136143  | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;
    137144  | #i #s %{ false} % //;
     
    171178    >(yields_eq ??? H3)
    172179    whd in ⊢ (??%?); >H2 @refl
    173 | #e #ty #sp #l #off #tr #H1 #H2 whd in ⊢ (??%?);
    174     >(yields_eq ??? H2)
     180| #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?);
     181    >(yields_eq ??? H2) whd in ⊢ (??%?)
     182    @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd
    175183    @refl
    176184| #ty' #ty @refl
     
    226234| #id #l #ty #e1 #e2 whd in ⊢ (??%?); >e1
    227235    >e2 @refl
    228 | #e #ty #r #l #ofs #tr #H1 #H2 whd in ⊢ (??%?);
     236| #e #ty #r #l #pc #ofs #tr #H1 #H2 whd in ⊢ (??%?);
    229237    >(yields_eq ??? H2)
    230238    @refl
     
    348356] qed.
    349357
    350 lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Prop. (∀p'.Q (inl ?? p')) → Q f.
    351 #P #f #p #Q #H cases f;
    352 [ @H
    353 | #np @False_ind @(absurd ? p np)
    354 ] qed.
    355 
    356 lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Prop. (∀p'.Q (inr ?? p')) → Q f.
    357 #P #f #p #Q #H cases f;
    358 [ #np @False_ind @(absurd ? np p)
    359 | @H
    360 ] qed.
    361 
    362358theorem step_complete: ∀ge,s,tr,s'.
    363359  step ge s tr s' → yieldsIO ? (exec_step ge s) 〈tr,s'〉.
  • Deliverables/D3.1/C-semantics/CexecSound.ma

    r499 r500  
    66 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
    77#v #ty #r
    8 cases v; [ | #i | #f | #r1 | #r #b #of ]
     8cases v; [ | #i | #f | #r1 | #r #b #pc #of ]
    99cases ty; [ 2,11,20,29,38: #sz #sg | 3,12,21,30,39: #sz | 4,13,22,31,40: #r #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ]
    1010#H whd in H:(??%?); destruct;
     
    8787    cases ty' in H2; normalize; try #a try #b try #c try #d destruct;
    8888    @cast_pp_z //;
    89 | #sp #b #of whd in ⊢ (??%? → ?); #e
    90     elim (bind_inversion ????? e); #s *; #es #e'
    91     elim (bind_inversion ????? e'); #u *; #eu #e''
    92     elim (bind_inversion ????? e''); #s' *; #es' #e'''
     89| #r #b #pc #of whd in ⊢ (??%? → ?) #e
     90    elim (bind_inversion ????? e) #s * #es #e'
     91    elim (bind_inversion ????? e') #u * #eu #e'' -e';
     92    elim (bind_inversion ????? e'') #s' * #es' #e'''; -e'';
    9393    cut (type_region ty s);
    9494    [ cases ty in es:(??%?) ⊢ %; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ]
     
    9999            whd in e:(??%?); destruct; //;
    100100        | #Hty'
    101             cut (s = sp). elim (eq_region_dec sp s) in eu; //; normalize; #_ #e destruct.
    102             #e <e
    103             whd in match (is_pointer_compat ??) in e''';
    104             cases (pointer_compat_dec b s') in e'''; #Hcompat #e'''
    105             whd in e''':(??%?); destruct (e'''); /2/
     101            cut (s = r). elim (eq_region_dec r s) in eu; //; normalize; #_ #e destruct.
     102            #e >e in Hty #Hty
     103            cases (pointer_compat_dec b s') in e'''
     104            #Hcompat #e''' whd in e''':(??%?); destruct (e'''); /2/
    106105        ]
    107106    ]
     
    195194    ]
    196195| #ty #e #He whd in ⊢ (???%)
    197     @bind2_OK #v cases v // #r #l #ofs #tr #Hv whd
    198     @eval_Ederef [ 2: >Hv in He #He @He | skip ]
    199 | #ty #e'' #ty'' #He'' @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H
    200   cases ty // #r #pty
    201     whd @eval_Eaddrof >H in He'' #He'' @He''
     196    @bind2_OK #v cases v // #r #l #pc #ofs #tr #Hv whd
     197    @eval_Ederef [ 3: >Hv in He #He @He | *: skip ]
     198| #ty #e'' #ty'' #He'' @bind2_OK #x cases x #loc #ofs #tr #H
     199  cases ty // *#pty
     200  cases loc in H ⊢ % * #loc' #H
     201  whd try @I
     202  @eval_Eaddrof >H in He'' #He'' @He''
    202203| #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1
    203204    @opt_bind_OK #v #ev
     
    260261] qed.
    261262
    262 lemma addrof_eval_lvalue: ∀ge,en,m,e,r,loc,off,tr,ty.
    263 eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr r loc off) tr →
     263lemma addrof_eval_lvalue: ∀ge,en,m,e,r,loc,pc,off,tr,ty.
     264eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr r loc pc off) tr →
    264265eval_lvalue ge en m e loc off tr.
    265 #ge #en #m #e #r #loc #off #tr #ty #H inversion H;
     266#ge #en #m #e #r #loc #pc #off #tr #ty #H inversion H;
    266267[ 1,2,5: #a #b #H @False_ind destruct (H);
    267268| #a #b #c #d #e #f #H1 #g #H2 <H2 in H1 #H1 @False_ind
     
    269270    [ #a #b #c #d #bad destruct (bad);
    270271    | #a #b #c #d #e #bad destruct (bad);
    271     | #a #b #c #d #e #f #g #bad destruct (bad);
     272    | #a #b #c #d #e #f #g #h #bad destruct (bad);
    272273    | #a #b #c #d #e #f #g #h #i #j #k #l #m #bad @False_ind destruct (bad);
    273274    | #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
    274275    ]
    275 | #e' #ty' #loc' #ofs' #v #tr' #H #e1 #e2 #e3 destruct (e1 e2 e3); @H
     276| #e' #ty' #r' #loc' #ofs' #tr' #H' #pc' #e1 #e2 #e3 destruct (e1 e2 e3); @H'
    276277| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
    277278| #a #b #c #d #e #f #g #h #i #j #k #l #k #l #bad destruct (bad);
     
    286287] qed.
    287288
    288 lemma addrof_exec_lvalue: ∀ge,en,m,e,r,loc,off,tr,ty.
    289 exec_lvalue ge en m e = OK ? 〈〈loc,off〉,tr〉 →
    290 exec_expr ge en m (Expr (Eaddrof e) (Tpointer r ty)) = OK ? 〈Vptr r loc off, tr〉.
    291 #ge #en #m #e #r #loc #off #tr #ty #H whd in ⊢ (??%?)
    292 >H //
     289lemma addrof_exec_lvalue: ∀ge,en,m,e,r,loc,off,tr.
     290exec_lvalue ge en m e = OK ? 〈〈mk_block r loc,off〉,tr〉 →
     291exec_expr ge en m (Expr (Eaddrof e) (Tpointer r Tvoid)) = OK ? 〈Vptr r (mk_block r loc) (same_compat ??) off, tr〉.
     292#ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?)
     293>H whd in ⊢ (??%?) cases r @refl
    293294qed.
    294295
     
    297298#ge #en #m #e lapply (refl ? (exec_lvalue ge en m e));
    298299cases (exec_lvalue ge en m e) in ⊢ (???% → %);
    299 [ #x cases x #y cases y #loc #off #tr #H whd
    300     @(addrof_eval_lvalue … Any … (Tpointer Any Tvoid))
    301     lapply (addrof_exec_lvalue … Any … (Tpointer Any Tvoid) H) #H'
    302     lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer Any Tvoid)))
     300[ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ % #locr #loci #H
     301    @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ /2/ ]
     302    lapply (addrof_exec_lvalue … H) #H'
     303    lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer locr Tvoid)))
    303304    >H' #H'' @H''
    304305| #_ whd @I
  • Deliverables/D3.1/C-semantics/Csem.ma

    r499 r500  
    4848      n ≠ zero →
    4949      is_true (Vint n) (Tint sz sg)
    50   | is_true_pointer_pointer: ∀psp,b,ofs,s,t.
    51       is_true (Vptr psp b ofs) (Tpointer s t)
     50  | is_true_pointer_pointer: ∀r,b,pc,ofs,s,t.
     51      is_true (Vptr r b pc ofs) (Tpointer s t)
    5252  | is_true_float: ∀f,sz.
    5353      f ≠ Fzero →
     
    9696      match v with
    9797      [ Vint n ⇒ Some ? (of_bool (eq n zero))
    98       | Vptr _ _ _ ⇒ Some ? Vfalse
     98      | Vptr _ _ _ _ ⇒ Some ? Vfalse
    9999      | _ ⇒ None ?
    100100      ]
     
    102102      match v with
    103103      [ Vint n ⇒ Some ? (of_bool (eq n zero))
    104       | Vptr _ _ _ ⇒ Some ? Vfalse
     104      | Vptr _ _ _ _ ⇒ Some ? Vfalse
    105105      | _ ⇒ None ?
    106106      ]
     
    129129  | add_case_pi ty ⇒                    (**r pointer plus integer *)
    130130      match v1 with
    131       [ Vptr pcl1 b1 ofs1 ⇒ match v2 with
    132         [ Vint n2 ⇒ Some ? (Vptr pcl1 b1 (add ofs1 (mul (repr (sizeof ty)) n2)))
     131      [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     132        [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (add ofs1 (mul (repr (sizeof ty)) n2)))
    133133        | _ ⇒ None ? ]
    134134      | Vnull r ⇒ match v2 with
     
    139139      match v1 with
    140140      [ Vint n1 ⇒ match v2 with
    141         [ Vptr pcl2 b2 ofs2 ⇒ Some ? (Vptr pcl2 b2 (add ofs2 (mul (repr (sizeof ty)) n1)))
     141        [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (add ofs2 (mul (repr (sizeof ty)) n1)))
    142142        | _ ⇒ None ? ]
    143143      | _ ⇒ None ? ]
     
    161161  | sub_case_pi ty ⇒             (**r pointer minus integer *)
    162162      match v1 with
    163       [ Vptr pcl1 b1 ofs1 ⇒ match v2 with
    164         [ Vint n2 ⇒ Some ? (Vptr pcl1 b1 (sub ofs1 (mul (repr (sizeof ty)) n2)))
     163      [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     164        [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (sub ofs1 (mul (repr (sizeof ty)) n2)))
    165165        | _ ⇒ None ? ]
    166166      | _ ⇒ None ? ]
    167167  | sub_case_pp ty ⇒             (**r pointer minus pointer *)
    168168      match v1 with
    169       [ Vptr pcl1 b1 ofs1 ⇒ match v2 with
    170         [ Vptr pcl2 b2 ofs2 ⇒
     169      [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     170        [ Vptr r2 b2 p2 ofs2 ⇒
    171171          if eq_block b1 b2 then
    172172            if eq (repr (sizeof ty)) zero then None ?
     
    321321         | _ ⇒ None ?
    322322         ]
    323       | Vptr r1 b1 ofs1 ⇒
     323      | Vptr r1 b1 p1 ofs1 ⇒
    324324        match v2 with
    325         [ Vptr r2 b2 ofs2 ⇒
     325        [ Vptr r2 b2 p2 ofs2 ⇒
    326326          if valid_pointer m r1 b1 (signed ofs1)
    327327          ∧ valid_pointer m r2 b2 (signed ofs2) then
     
    334334      | Vnull r1 ⇒
    335335        match v2 with
    336         [ Vptr r2 b2 ofs2 ⇒ sem_cmp_mismatch c
     336        [ Vptr r2 b2 p2 ofs2 ⇒ sem_cmp_mismatch c
    337337        | Vnull r2 ⇒ sem_cmp_match c
    338338        | _ ⇒ None ?
     
    429429      cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
    430430           (Vfloat (cast_float_float sz2 f))
    431   | cast_pp: ∀m,r,r',ty,ty',b,ofs.
     431  | cast_pp: ∀m,r,r',ty,ty',b,pc,ofs.
    432432      type_region ty r →
    433433      type_region ty' r' →
    434       pointer_compat b r' →
    435       cast m (Vptr r b ofs) ty ty' (Vptr r' b ofs)
     434      ∀pc':pointer_compat b r'.
     435      cast m (Vptr r b pc ofs) ty ty' (Vptr r' b pc' ofs)
    436436  | cast_ip_z: ∀m,sz,sg,ty',r.
    437437      type_region ty' r →
     
    466466let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: int) : option val ≝
    467467  match access_mode ty with
    468   [ By_value chunk ⇒ loadv chunk m (Vptr Any b ofs)
    469   | By_reference r ⇒ Some ? (Vptr r b ofs)
     468  [ By_value chunk ⇒ loadv chunk m (Vptr Any b ? ofs)
     469  | By_reference r ⇒
     470    match pointer_compat_dec b r with
     471    [ inl p ⇒ Some ? (Vptr r b p ofs)
     472    | inr _ ⇒ None ?
     473    ]
    470474  | By_nothing ⇒ None ?
    471475  ].
     476cases b //
     477qed.
    472478
    473479(* * Symmetrically, [store_value_of_type ty m b ofs v] returns the
     
    478484let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: int) (v: val) : option mem ≝
    479485  match access_mode ty_dest with
    480   [ By_value chunk ⇒ storev chunk m (Vptr Any loc ofs) v
     486  [ By_value chunk ⇒ storev chunk m (Vptr Any loc ? ofs) v
    481487  | By_reference _ ⇒ None ?
    482488  | By_nothing ⇒ None ?
    483489  ].
     490cases loc //
     491qed.
    484492
    485493(* * Allocation of function-local variables.
     
    570578  | eval_Eaddrof: ∀a,ty,r,loc,ofs,tr.
    571579      eval_lvalue ge e m a loc ofs tr →
    572       eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr r loc ofs) tr
     580      ∀pc:pointer_compat loc r.
     581      eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr r loc pc ofs) tr
    573582  | eval_Esizeof: ∀ty',ty.
    574583      eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) E0
     
    633642      find_symbol ?? ge id = Some ? l →
    634643      eval_lvalue ge e m (Expr (Evar id) ty) l zero E0
    635   | eval_Ederef: ∀a,ty,r,l,ofs,tr.
    636       eval_expr ge e m a (Vptr r l ofs) tr →
     644  | eval_Ederef: ∀a,ty,r,l,p,ofs,tr.
     645      eval_expr ge e m a (Vptr r l p ofs) tr →
    637646      eval_lvalue ge e m (Expr (Ederef a) ty) l ofs tr
    638647    (* Aside: note that each block of memory is entirely contained within one
     
    654663  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    655664  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
    656   (ead:∀a,ty,psp,loc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))
     665  (ead:∀a,ty,r,loc,pc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty r loc pc ofs tr H))
    657666  (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
    658667  (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2))
     
    671680  | eval_Econst_float f ty ⇒ ecF f ty
    672681  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2
    673   | eval_Eaddrof a ty psp loc ofs tr H ⇒ ead a ty psp loc ofs tr H
     682  | eval_Eaddrof a ty r loc pc ofs tr H ⇒ ead a ty r loc pc ofs tr H
    674683  | eval_Esizeof ty' ty ⇒ esz ty' ty
    675684  | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1)
     
    691700  (lvl:∀id,l,ty,H. P ???? (eval_Evar_local ge e m id l ty H))
    692701  (lvg:∀id,l,ty,H1,H2. P ???? (eval_Evar_global ge e m id l ty H1 H2))
    693   (lde:∀a,ty,psp,l,ofs,tr,H. P ???? (eval_Ederef ge e m a ty psp l ofs tr H))
     702  (lde:∀a,ty,r,l,pc,ofs,tr,H. P ???? (eval_Ederef ge e m a ty r l pc ofs tr H))
    694703  (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. P a l ofs tr H1 → P ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3))
    695704  (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. P a l ofs tr H1 → P ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2))
     
    698707  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
    699708  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
    700   | eval_Ederef a ty psp l ofs tr H ⇒ lde a ty psp l ofs tr H
     709  | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc ofs tr H
    701710  | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1)
    702711  | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1)
     
    762771  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    763772  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
    764   (ead:∀a,ty,psp,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))
     773  (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc))
    765774  (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
    766775  (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2))
     
    776785  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
    777786  (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2))
    778   (lde:∀a,ty,psp,l,ofs,tr,H. P a (Vptr psp l ofs) tr H → Q ???? (eval_Ederef ge e m a ty psp l ofs tr H))
     787  (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr r l pc ofs) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H))
    779788  (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3))
    780789  (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2))
     
    785794  | eval_Econst_float f ty ⇒ ecF f ty
    786795  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu (Expr a ty) loc ofs tr H1)
    787   | eval_Eaddrof a ty psp loc ofs tr H ⇒ ead a ty psp loc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H)
     796  | eval_Eaddrof a ty r loc ofs tr H pc ⇒ ead a ty r loc pc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H)
    788797  | eval_Esizeof ty' ty ⇒ esz ty' ty
    789798  | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1)
     
    804813  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    805814  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
    806   (ead:∀a,ty,psp,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))
     815  (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc))
    807816  (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
    808817  (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2))
     
    818827  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
    819828  (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2))
    820   (lde:∀a,ty,psp,l,ofs,tr,H. P a (Vptr psp l ofs) tr H → Q ???? (eval_Ederef ge e m a ty psp l ofs tr H))
     829  (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr r l pc ofs) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H))
    821830  (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3))
    822831  (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2))
     
    825834  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
    826835  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
    827   | eval_Ederef a ty psp l ofs tr H ⇒ lde a ty psp l ofs tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a (Vptr psp l ofs) tr H)
     836  | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc ofs tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a (Vptr r l pc ofs) tr H)
    828837  | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1)
    829838  | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1)
  • Deliverables/D3.1/C-semantics/Globalenvs.ma

    r498 r500  
    414414      match (*find_symbol ge symb*) symbols ? ge symb with
    415415      [ None ⇒ None ?
    416       | Some b' ⇒ store (Mpointer r') m r b p (Vptr r' b' ofs)
     416      | Some b' ⇒
     417        match pointer_compat_dec b' r' with
     418        [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc ofs)
     419        | inr _ ⇒ None ?
     420        ]
    417421      ]
    418422  | Init_space n ⇒ Some ? m
     
    519523  init_mem_
    520524  (λF,ge. functions ? ge) (* find_funct_ptr *)
    521   (λF,ge,v. match v with [ Vptr _ b o ⇒ if eq o zero then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
     525  (λF,ge,v. match v with [ Vptr _ b _ o ⇒ if eq o zero then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
    522526  (λF,ge. symbols ? ge) (* find_symbol *)
    523527(*  ?
  • Deliverables/D3.1/C-semantics/Mem.ma

    r499 r500  
    588588qed.
    589589*)
    590 (* pointer_compat block_region pointer_region *)
    591 
    592 inductive pointer_compat : block → region → Prop ≝
    593 |        same_compat : ∀s,id. pointer_compat (mk_block s id) s
    594 |      pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData
    595 |   universal_compat : ∀r,id. pointer_compat (mk_block r id) Any.
    596 
    597 lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
    598 * * #id *
    599 try ( %1 // )
    600 %2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
    601 qed.
    602 
    603 definition is_pointer_compat : block → region → bool ≝
    604 λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
    605590
    606591(* [valid_access m chunk r b ofs] holds if a memory access (load or store)
     
    695680let rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝
    696681  match addr with
    697   [ Vptr r b ofs ⇒ load chunk m r b (signed ofs)
     682  [ Vptr r b p ofs ⇒ load chunk m r b (signed ofs)
    698683  | _ ⇒ None ? ].
    699684
     
    742727λchunk,m,addr,v.
    743728  match addr with
    744   [ Vptr r b ofs ⇒ store chunk m r b (signed ofs) v
     729  [ Vptr r b p ofs ⇒ store chunk m r b (signed ofs) v
    745730  | _ ⇒ None ? ].
    746731
     
    35303515  ∀m,a,v.
    35313516  storev Mint8signed m a v = storev Mint8unsigned m a v.
    3532 #m #a #v whd in ⊢ (??%%); elim a; //;
    3533 #r #b #ofs whd in ⊢ (??%%);
    3534 >(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) //;
     3517#m #a #v whd in ⊢ (??%%) elim a //
     3518#r #b #p #ofs whd in ⊢ (??%%)
     3519>(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) //
    35353520qed.
    35363521
     
    35383523  ∀m,a,v.
    35393524  storev Mint16signed m a v = storev Mint16unsigned m a v.
    3540 #m #a #v whd in ⊢ (??%%); elim a; //;
    3541 #r #b #ofs whd in ⊢ (??%%);
    3542 >(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) //;
     3525#m #a #v whd in ⊢ (??%%) elim a //
     3526#r #b #p #ofs whd in ⊢ (??%%)
     3527>(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) //
    35433528qed.
    35443529
  • Deliverables/D3.1/C-semantics/Values.ma

    r498 r500  
    4444] qed.
    4545
     46(* pointer_compat block_region pointer_region *)
     47
     48inductive pointer_compat : block → region → Prop ≝
     49|        same_compat : ∀s,id. pointer_compat (mk_block s id) s
     50|      pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData
     51|   universal_compat : ∀r,id. pointer_compat (mk_block r id) Any.
     52
     53lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
     54* * #id *;
     55try ( %1 // )
     56%2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
     57qed.
     58
     59definition is_pointer_compat : block → region → bool ≝
     60λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
     61
    4662(* * A value is either:
    4763- a machine integer;
     
    6076  | Vfloat: float → val
    6177  | Vnull: region → val
    62   | Vptr: region → block → int → val.
     78  | Vptr: ∀r:region. ∀b:block. pointer_compat b r → int → val.
    6379
    6480definition Vzero: val ≝ Vint zero.
     
    101117  match v with
    102118  [ Vint n ⇒ n ≠ zero
    103   | Vptr _ b ofs ⇒ True
     119  | Vptr _ b _ ofs ⇒ True
    104120  | _ ⇒ False
    105121  ].
     
    118134      bool_of_val (Vint zero) false
    119135  | bool_of_val_ptr:
    120       ∀r,b,ofs. bool_of_val (Vptr r b ofs) true
     136      ∀r,b,p,ofs. bool_of_val (Vptr r b p ofs) true
    121137  | bool_of_val_null:
    122138      ∀r. bool_of_val (Vnull r) true.
     
    175191  match v with
    176192  [ Vint n ⇒ of_bool (int_eq n zero)
    177   | Vptr _ b ofs ⇒ Vfalse
     193  | Vptr _ b _ ofs ⇒ Vfalse
    178194  | Vnull _ ⇒ Vtrue
    179195  | _ ⇒ Vundef
     
    203219  [ Vint n1 ⇒ match v2 with
    204220    [ Vint n2 ⇒ Vint (add n1 n2)
    205     | Vptr pty b2 ofs2 ⇒ Vptr pty b2 (add ofs2 n1)
    206     | _ ⇒ Vundef ]
    207   | Vptr pty b1 ofs1 ⇒ match v2 with
    208     [ Vint n2 ⇒ Vptr pty b1 (add ofs1 n2)
     221    | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (add ofs2 n1)
     222    | _ ⇒ Vundef ]
     223  | Vptr r b1 p ofs1 ⇒ match v2 with
     224    [ Vint n2 ⇒ Vptr r b1 p (add ofs1 n2)
    209225    | _ ⇒ Vundef ]
    210226  | _ ⇒ Vundef ].
     
    215231    [ Vint n2 ⇒ Vint (sub n1 n2)
    216232    | _ ⇒ Vundef ]
    217   | Vptr pty1 b1 ofs1 ⇒ match v2 with
    218     [ Vint n2 ⇒ Vptr pty1 b1 (sub ofs1 n2)
    219     | Vptr pty2 b2 ofs2 ⇒
     233  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     234    [ Vint n2 ⇒ Vptr r1 b1 p1 (sub ofs1 n2)
     235    | Vptr r2 b2 p2 ofs2 ⇒
    220236        if eq_block b1 b2 then Vint (sub ofs1 ofs2) else Vundef
    221237    | _ ⇒ Vundef ]
     
    387403    [ Vint n2 ⇒ of_bool (cmp c n1 n2)
    388404    | _ ⇒ Vundef ]
    389   | Vptr r1 b1 ofs1 ⇒ match v2 with
    390     [ Vptr r2 b2 ofs2 ⇒
     405  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     406    [ Vptr r2 b2 p2 ofs2 ⇒
    391407        if eq_block b1 b2
    392408        then of_bool (cmp c ofs1 ofs2)
     
    395411    | _ ⇒ Vundef ]
    396412  | Vnull r1 ⇒ match v2 with
    397     [ Vptr _ _ _ ⇒ cmp_mismatch c
     413    [ Vptr _ _ _ _ ⇒ cmp_mismatch c
    398414    | Vnull r2 ⇒ cmp_match c
    399415    | _ ⇒ Vundef
     
    406422    [ Vint n2 ⇒ of_bool (cmpu c n1 n2)
    407423    | _ ⇒ Vundef ]
    408   | Vptr r1 b1 ofs1 ⇒ match v2 with
    409     [ Vptr r2 b2 ofs2 ⇒
     424  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     425    [ Vptr r2 b2 p2 ofs2 ⇒
    410426        if eq_block b1 b2
    411427        then of_bool (cmpu c ofs1 ofs2)
     
    414430    | _ ⇒ Vundef ]
    415431  | Vnull r1 ⇒ match v2 with
    416     [ Vptr _ _ _ ⇒ cmp_mismatch c
     432    [ Vptr _ _ _ _ ⇒ cmp_mismatch c
    417433    | Vnull r2 ⇒ cmp_match c
    418434    | _ ⇒ Vundef
     
    447463    | _ ⇒ Vundef
    448464    ]
    449   | Vptr r b ofs ⇒
     465  | Vptr r b p ofs ⇒
    450466    match chunk with
    451     [ Mpointer r' ⇒ if eq_region r r' then Vptr r b ofs else Vundef
     467    [ Mpointer r' ⇒ if eq_region r r' then Vptr r b p ofs else Vundef
    452468    | _ ⇒ Vundef
    453469    ]
Note: See TracChangeset for help on using the changeset viewer.