Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (8 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r2106 r2176  
    55 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
    66#v #ty #r
    7 cases v; [ | #sz #i | #f | #r1 | #ptr ]
    8 cases ty; [ 2,11,20,29,38: #sz' #sg | 3,12,21,30,39: #sz' | 4,13,22,31,40: #rg #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 ]
     7cases v; [ | #sz #i | #f | | #ptr ]
     8cases ty; [ 2,11,20,29,38: #sz' #sg | 3,12,21,30,39: #sz' | 4,13,22,31,40: (*#rg*) #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 ]
    99whd in ⊢ (??%? → ?);
    1010[ 2: @intsize_eq_elim_elim
     
    3939@eq_bv_elim
    4040[ #e >e
    41     cases ty; [ | #sz' #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ]
     41    cases ty; [ | #sz' #sg | #fs | (*#sp*) #ty | (*#sp*) #ty #n | #args #rty | #id #fs | #id #fs | (*#r*) #id ]
    4242    whd in ⊢ (??%? → ?); #H [ 2: | *: destruct ]
    43     cases ty' in H ⊢ %; [ | #sz'' #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ]
     43    cases ty' in H ⊢ %; [ | #sz'' #sg | #fs | (*#sp*) #ty | (*#sp*) #ty #n | #args #rty | #id #fs | #id #fs | (*#r*) #id ]
    4444    try (@eq_intsize_elim #E) whd in ⊢ (??%? → ?); #H destruct @cast_ip_z //
    4545| #_ whd in ⊢ (??%? → ?); #H destruct
     
    5454  [ #H whd in H:(??%?); destruct;
    5555  | 3: #a #H whd in H:(??%?); destruct;
    56   | 7,8,9: #a #b #H whd in H:(??%?); destruct;
     56  | 7,8,9: #a [ 1,2: #b ] #H whd in H:(??%?); destruct;
    5757  | #sz1 #si1 cases ty';
    5858    [ whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
     
    6464      | *; whd #H whd in H:(??%?); destruct; @cast_if
    6565      ]
    66     | 2,7,8,9: #a #b whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
     66    | 2,7,8,9: #a [1,2,3: #b] whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    6767      [ 1,3,5,7: #NE #H destruct
    6868      | *: *; whd #H whd in H:(??%?); destruct; //
    6969      ]
    70     | 4,5,6: [ #sp #ty'' letin t ≝ (Tpointer sp ty'')
    71                  | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n)
    72                  | #args #rty letin t ≝ (Tfunction args rty) ]
     70    | 4,5,6: [ #ty'' letin t ≝ (Tpointer ty'')
     71             | #ty'' #n letin t ≝ (Tarray ty'' n)
     72             | #args #rty letin t ≝ (Tfunction args rty) ]
    7373        whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    7474        [ 1,3,5: #NE #H destruct
     
    8181        ]
    8282    ]
    83   | *: [ #sp #ty'' letin t ≝ (Tpointer sp ty'')
    84            | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n)
    85            | #args #rty letin t ≝ (Tfunction args rty) ]
     83  | *: [ #ty'' letin t ≝ (Tpointer ty'')
     84       | #ty'' #n letin t ≝ (Tarray ty'' n)
     85       | #args #rty letin t ≝ (Tfunction args rty) ]
    8686        whd in ⊢ (??%? → ?);
    8787        lapply (try_cast_null_sound m sz i t ty' v');
     
    9191        ]
    9292  ]
    93 | #f cases ty;  [ 3: #x | 2,4,6,7,8,9: #x #y | 5: #x #y #z ]
    94                     [ cases ty'; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ]
     93| #f cases ty;  [ 3,4,9: #x | 2,5,6,7,8: #x #y ]
     94                    [ cases ty'; [ #e | 3,4,9: #a #e | 2,6,7,8: #a #b #e | #a #b #e ]
    9595                        whd in e:(??%?); destruct; //;
    9696                    | *: #e whd in e:(??%?); destruct
    9797                    ]
    98 | #r cases ty; [ 3: #x | 2,4,6,7,8,9: #x #y | 5: #x #y #z ]
    99     whd in ⊢ (??%? → ?); #H destruct; cases (eq_region_dec r ?) in H;
    100     whd in ⊢ (? → ??%? → ?); #H1 #H2 destruct;
    101     cases ty' in H2; normalize; try #a try #b try #c try #d destruct;
     98| cases ty; [ 3,4,9: #x | 2,5,6,7,8: #x #y ]
     99    whd in ⊢ (??%? → ?); #H destruct
     100    cases ty' in H; normalize; try #a try #b try #c try #d destruct;
    102101    @cast_pp_z //;
     102(*
    103103| #ptr whd in ⊢ (??%? → ?); #e
    104104    elim (bind_inversion ????? e) #s * #es #e'
     
    119119        ]
    120120    ]
     121*)
     122| #ptr
     123  cases ty; [ 3,4,9: #x | 2,5,6,7,8: #x #y ]
     124  #E whd in E:(??%?); destruct
     125  cases ty' in E ⊢ %; normalize #A try #B try #C try #D destruct /2/
    121126] qed.
    122127
     
    142147    ]
    143148| #ty #e #He whd in ⊢ (???%);
    144     @bind2_OK #v cases v / by / * #r #l #pc #ofs #tr #Hv whd
     149    @bind2_OK #v cases v / by / * #l #ofs #tr #Hv whd
    145150    >Hv in He; #He
    146     @eval_Ederef [ 3: @He | *: skip ]
     151    @eval_Ederef @He
    147152| #ty #e'' #ty'' #He'' @bind2_OK * #loc #ofs #tr #H
    148   cases ty try (try #a try #b try #c @I) * #pty
    149   cases loc in H ⊢ %; * #loc' #H
    150   whd try @I
     153  cases ty try (try #a try #b try #c @I)
     154  #ty' whd
    151155  @eval_Eaddrof whd in H:(??%?); >H in He''; #He'' @He''
    152156| #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1
     
    210214] qed.
    211215
    212 lemma addrof_eval_lvalue: ∀ge,en,m,e,r,loc,pc,off,tr,ty.
    213 eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr (mk_pointer r loc pc off)) tr →
     216lemma addrof_eval_lvalue: ∀ge,en,m,e,loc,off,tr,ty.
     217eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr (mk_pointer loc off)) tr →
    214218eval_lvalue ge en m e loc off tr.
    215 #ge #en #m #e #r #loc #pc #off #tr #ty #H inversion H;
     219#ge #en #m #e #loc #off #tr #ty #H inversion H;
    216220[ 1,2,5: #a #b #c #H @False_ind destruct (H);
    217221| #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1; #H1 @False_ind
     
    219223    [ #a #b #c #d #bad destruct (bad);
    220224    | #a #b #c #d #e #bad destruct (bad);
    221     | #a #b #c #d #e #f #g #h #bad destruct (bad);
     225    | #a #b #c #d #e #f #bad destruct (bad);
    222226    | #a #b #c #d #e #f #g #h #i #j #k #l #bad @False_ind destruct (bad);
    223227    | #a #b #c #d #e #f #g #h #i #j #bad destruct (bad);
    224228    ]
    225 | #e' #ty' #r' #loc' #ofs' #tr' #H' #pc' #e1 #e2 #e3 destruct (e1 e2 e3); #E @H'
     229| #e' #ty' #loc' #ofs' #tr' #H' #e1 #e2 #e3 destruct (e1 e2 e3); #E @H'
    226230| #a #b #c #d #e #f #g #h #bad destruct (bad);
    227231| #a #b #c #d #e #f #g #h #i #j #k #l #bad destruct (bad);
     
    238242lemma addrof_exec_lvalue: ∀ge,en,m,e,r,loc,off,tr.
    239243exec_lvalue ge en m e = OK ? 〈〈mk_block r loc,off〉,tr〉 →
    240 exec_expr ge en m (Expr (Eaddrof e) (Tpointer r Tvoid)) = OK ? 〈Vptr (mk_pointer r (mk_block r loc) (same_compat ??) off), tr〉.
     244exec_expr ge en m (Expr (Eaddrof e) (Tpointer Tvoid)) = OK ? 〈Vptr (mk_pointer (mk_block r loc) off), tr〉.
    241245#ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?);
    242246>H whd in ⊢ (??%?); cases r @refl
     
    248252cases (exec_lvalue ge en m e) in ⊢ (???% → %);
    249253[ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ %; #locr #loci #H
    250     @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ @same_compat ]
     254    @(addrof_eval_lvalue … (Tpointer Tvoid))
    251255    lapply (addrof_exec_lvalue … H) #H'
    252     lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer locr Tvoid)))
     256    lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer Tvoid)))
    253257    >H' #H'' @H''
    254258| #msg #_ whd @I
     
    284288[ #en #m #en' #m' #EXEC whd in EXEC:(??%?); destruct %
    285289| * #id #ty #t #IH #en #m #en' #m'
    286   lapply (refl ? (alloc m O (sizeof ty) Any)) whd in ⊢ (? → ??%? → ?);
     290  lapply (refl ? (alloc m O (sizeof ty) XData)) whd in ⊢ (? → ??%? → ?);
    287291  cases (alloc ????) in ⊢ (???% → %); #m'' #b #ALLOC #EXEC
    288292 @(alloc_variables_cons … ALLOC)
     
    314318  [ //
    315319  | #ty #tys whd in ⊢ (???%);
    316     cases ty [ #sz #sg | #sz | #r ] cases v //
     320    cases ty [ #sz #sg | | #sz ] cases v //
    317321    [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?);
    318322      @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct
Note: See TracChangeset for help on using the changeset viewer.