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

Make block type a little more abstract; remove knowledge about the old
representation for a pointer from the evaluation of lvalues.

File:
1 edited

Legend:

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

    r496 r498  
    177177theorem exec_expr_sound: ∀ge:genv. ∀en:env. ∀m:mem. ∀e:expr.
    178178(P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)).
    179 #ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e)
     179#ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e)
    180180(* XXX // fails [ 1,2: #ty #c whd //  *)
    181181[ #ty #c whd %
     
    194194    | #loc #eget @(eval_Evar_local … eget)
    195195    ]
    196 | #ty #e #He whd in ⊢ (???%);
    197     @bind2_OK #v cases v; //; #sp #l #ofs #tr #Hv whd;
    198     @eval_Ederef >Hv in He #He @He
     196| #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 ]
    199199| #ty #e'' #ty'' #He'' @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H
    200     whd; @eval_Eaddrof >H in He'' #He'' @He''
     200  cases ty // #r #pty
     201    whd @eval_Eaddrof >H in He'' #He'' @He''
    201202| #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1
    202203    @opt_bind_OK #v #ev
     
    259260] qed.
    260261
    261 lemma addrof_eval_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty.
    262 eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr sp loc off) tr →
    263 eval_lvalue ge en m e sp loc off tr.
    264 #ge #en #m #e #sp #loc #off #tr #ty #H inversion H;
     262lemma addrof_eval_lvalue: ∀ge,en,m,e,r,loc,off,tr,ty.
     263eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr r loc off) tr →
     264eval_lvalue ge en m e loc off tr.
     265#ge #en #m #e #r #loc #off #tr #ty #H inversion H;
    265266[ 1,2,5: #a #b #H @False_ind destruct (H);
    266 | #a #b #c #d #e #f #g #H1 #i #H2 <H2 in H1 #H1 @False_ind
     267| #a #b #c #d #e #f #H1 #g #H2 <H2 in H1 #H1 @False_ind
    267268    @(eval_lvalue_inv_ind … H1)
    268269    [ #a #b #c #d #bad destruct (bad);
    269     | #a #b #c #d #e #f #bad destruct (bad);
     270    | #a #b #c #d #e #bad destruct (bad);
    270271    | #a #b #c #d #e #f #g #bad destruct (bad);
    271     | #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad @False_ind destruct (bad);
    272     | #a #b #c #d #e #f #g #h #i #j #k #l #bad destruct (bad);
    273     ]
    274 | #e' #ty' #sp' #loc' #ofs' #tr' #H #e1 #e2 #e3 destruct (e1 e2 e3); @H
     272    | #a #b #c #d #e #f #g #h #i #j #k #l #m #bad @False_ind destruct (bad);
     273    | #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
     274    ]
     275| #e' #ty' #loc' #ofs' #v #tr' #H #e1 #e2 #e3 destruct (e1 e2 e3); @H
    275276| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
    276277| #a #b #c #d #e #f #g #h #i #j #k #l #k #l #bad destruct (bad);
     
    285286] qed.
    286287
    287 lemma addrof_exec_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty.
    288 exec_lvalue ge en m e = OK ? 〈〈〈sp,loc〉,off〉,tr〉 →
    289 exec_expr ge en m (Expr (Eaddrof e) ty) = OK ? 〈Vptr sp loc off, tr〉.
    290 #ge #en #m #e #sp #loc #off #tr #ty #H whd in ⊢ (??%?);
    291 >H //;
     288lemma addrof_exec_lvalue: ∀ge,en,m,e,r,loc,off,tr,ty.
     289exec_lvalue ge en m e = OK ? 〈〈loc,off〉,tr〉 →
     290exec_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 //
    292293qed.
    293294
    294295theorem exec_lvalue_sound: ∀ge,en,m,e.
    295 P_res ? (λr.eval_lvalue ge en m e (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) (exec_lvalue ge en m e).
     296P_res ? (λr.eval_lvalue ge en m e (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue ge en m e).
    296297#ge #en #m #e lapply (refl ? (exec_lvalue ge en m e));
    297298cases (exec_lvalue ge en m e) in ⊢ (???% → %);
    298 [ #x cases x; #y cases y; #z cases z; #sp #loc #off #tr #H whd;
    299     @(addrof_eval_lvalue … Tvoid)
    300     lapply (addrof_exec_lvalue … Tvoid H); #H'
    301     lapply (exec_expr_sound ge en m (Expr (Eaddrof e) Tvoid));
     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)))
    302303    >H' #H'' @H''
    303 | #_ whd; @I
     304| #_ whd @I
    304305] qed.
    305306
     
    310311  P_res_to_P ???? (exec_expr_sound ge en m e) H.
    311312
    312 definition exec_lvalue_sound' ≝ λge,en,m,e,sp,loc,off,tr.
    313   λH:exec_lvalue ge en m e = OK ? 〈〈〈sp,loc〉,off〉,tr〉.
     313definition exec_lvalue_sound' ≝ λge,en,m,e,loc,off,tr.
     314  λH:exec_lvalue ge en m e = OK ? 〈〈loc,off〉,tr〉.
    314315  P_res_to_P ???? (exec_lvalue_sound ge en m e) H.
    315316
Note: See TracChangeset for help on using the changeset viewer.