Ignore:
Timestamp:
Feb 11, 2011, 4:45:38 PM (9 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...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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
Note: See TracChangeset for help on using the changeset viewer.