Ignore:
Timestamp:
Feb 6, 2013, 1:01:34 PM (7 years ago)
Author:
garnier
Message:

Regions are no more stored in blocks. block_region now tests the id, it being below 0 implying Code region, XData otherwise.
Changes propagated through the front-end and common. Some more work might be required in the back-end, but it should be
trivial to fix related problems.

Motivation: no way to /elegantly/ prove that two blocks with the same id but different regions are non-sensical.
Prevented some proofs to go through in memory injections.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r2588 r2608  
    138138(* expressions that are lvalues *)
    139139| #e' #ty cases e'; //; [ #i #He' | #e #He' | #e #i #He' ] whd in He' ⊢ %;
    140     @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H
     140    @bind2_OK *  (* #x cases x; #y cases y; #sp *) #loc #ofs #tr #H
    141141    @opt_bind_OK #vl #evl whd in evl:(??%?); @(eval_Elvalue … evl)
    142142    >H in He'; #He' @He'
     
    145145    lapply (refl ? (lookup SymbolTag block en v))
    146146    cases (lookup SymbolTag block en v) in ⊢ (???% → %);
    147     [ #eget @opt_bind_OK #sploc cases sploc; #sp #loc #efind
     147    [ #eget @opt_bind_OK #sploc cases sploc; #sp (* #loc *) #efind
    148148        whd; @(eval_Evar_global … eget efind)
    149149    | #loc #eget @(eval_Evar_local … eget)
     
    257257] qed.
    258258
    259 lemma addrof_exec_lvalue: ∀ge,en,m,e,r,loc,off,tr.
    260 exec_lvalue ge en m e = OK ? 〈〈mk_block r loc,off〉,tr〉 →
    261 exec_expr ge en m (Expr (Eaddrof e) (Tpointer Tvoid)) = OK ? 〈Vptr (mk_pointer (mk_block r loc) off), tr〉.
    262 #ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?);
    263 >H whd in ⊢ (??%?); cases r @refl
     259lemma addrof_exec_lvalue: ∀ge,en,m,e(*,r*),loc,off,tr.
     260exec_lvalue ge en m e = OK ? 〈〈mk_block (*r*) loc,off〉,tr〉 →
     261exec_expr ge en m (Expr (Eaddrof e) (Tpointer Tvoid)) = OK ? 〈Vptr (mk_pointer (mk_block (*r*) loc) off), tr〉.
     262#ge #en #m #e (* #r *) #loc #off #tr #H whd in ⊢ (??%?);
     263>H whd in ⊢ (??%?); (* cases r *) @refl
    264264qed.
    265265
     
    268268#ge #en #m #e lapply (refl ? (exec_lvalue ge en m e));
    269269cases (exec_lvalue ge en m e) in ⊢ (???% → %);
    270 [ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ %; #locr #loci #H
     270[ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ %; #loci #H (* #locr #loci #H *)
    271271    @(addrof_eval_lvalue … (Tpointer Tvoid))
    272272    lapply (addrof_exec_lvalue … H) #H'
     
    305305[ #en #m #en' #m' #EXEC whd in EXEC:(??%?); destruct %
    306306| * #id #ty #t #IH #en #m #en' #m'
    307   lapply (refl ? (alloc m O (sizeof ty) XData)) whd in ⊢ (? → ??%? → ?);
    308   cases (alloc ????) in ⊢ (???% → %); #m'' #b #ALLOC #EXEC
     307  lapply (refl ? (alloc m O (sizeof ty) (*XData*))) whd in ⊢ (? → ??%? → ?);
     308  cases (alloc ??? (*?*)) in ⊢ (???% → %); #m'' #b #ALLOC #EXEC
    309309 @(alloc_variables_cons … ALLOC)
    310310 @IH @EXEC
     
    378378    ]
    379379  | #ex1 #ex2
    380     @res_bindIO2_OK #x cases x; #y cases y; #pcl #loc #ofs #tr1 #Hlval
     380    @res_bindIO2_OK #x cases x; (*#y cases y; *) #pcl (* #loc *) #ofs #tr1 #Hlval
    381381    @res_bindIO2_OK #v2 #tr2 #Hv2
    382382    @opt_bindIO_OK #m' #em'
     
    390390    [ @(step_call_none … Hvf Hvargs efd ety)
    391391    | #lhs'
    392         @res_bindIO2_OK #x cases x; #y cases y; #pcl #loc #ofs #tr3 #Hlocofs
     392        @res_bindIO2_OK #x cases x; (* #y cases y; *) #pcl (* #loc *) #ofs #tr3 #Hlocofs
    393393        whd; @(step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety)
    394394    ]
     
    483483whd in ⊢ (???%);
    484484@bind_OK #m #Em
    485 @opt_bind_OK #x cases x; #sp #b #esb
     485@opt_bind_OK #x cases x; #sp #esb (* #b #esb *)
    486486@opt_bind_OK #f #ef
    487487@(initial_state_intro … Em esb ef) @refl
Note: See TracChangeset for help on using the changeset viewer.