Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (7 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/SimplifyCasts.ma

    r2103 r2176  
    719719#castee_val #src_sz #src_sg #cast_sz #cast_sg #m #result
    720720elim castee_val
    721 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
     721[ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ]
    722722[ 2: | *: whd in ⊢ ((??%?) → ?); #Habsurd destruct ]
    723723whd in ⊢ ((??%?) → ?);
     
    750750#sz #sg #v1 #v2 #m #r
    751751elim v1
    752 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
     752[ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ]
    753753whd in ⊢ ((??%?) → ?); normalize nodelta
    754754>classify_add_int normalize nodelta #H destruct
    755755elim v2 in H;
    756 [ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ]
     756[ 1: | 2: #sz'' #i' | 3: #f' | 4: | 5: #ptr' ]
    757757whd in ⊢ ((??%?) → ?); #H destruct
    758758elim (sz_eq_dec sz' sz'')
     
    766766#sz #sg #v1 #v2 #m #r
    767767elim v1
    768 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
     768[ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ]
    769769whd in ⊢ ((??%?) → ?); normalize nodelta
    770770>classify_sub_int normalize nodelta #H destruct
    771771elim v2 in H;
    772 [ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ]
     772[ 1: | 2: #sz'' #i' | 3: #f' | 4: | 5: #ptr' ]
    773773whd in ⊢ ((??%?) → ?); #H destruct
    774774elim (sz_eq_dec sz' sz'')
     
    789789#sz #sg #v1 #v2 #m
    790790elim v1
    791 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
     791[ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ]
    792792[ 2: | *: #_ %1 %1 % #H @H ]
    793793elim v2
    794 [ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ]
     794[ 1: | 2: #sz'' #i' | 3: #f' | 4: | 5: #ptr' ]
    795795[ 2: | *: #_ %1 %2 % #H @H ]
    796796whd in ⊢ ((??%?) → ?); normalize nodelta
     
    808808#sz #sg #v1 #v2 #m
    809809elim v1
    810 [ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
     810[ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ]
    811811[ 2: | *: #_ %1 %1 % #H @H ]
    812812elim v2
    813 [ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ]
     813[ 1: | 2: #sz'' #i' | 3: #f' | 4: | 5: #ptr' ]
    814814[ 2: | *: #_ %1 %2 % #H @H ]
    815815whd in ⊢ ((??%?) → ?); normalize nodelta
     
    827827elim op normalize in match (binop_simplifiable ?); #H destruct
    828828elim v1 in H;
    829 [ 1,6: | 2,7: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I)) | 3,8: #f | 4,9: #r | 5,10: #ptr ]
     829[ 1,6: | 2,7: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I)) | 3,8: #f | 4,9: | 5,10: #ptr ]
    830830#_
    831831whd in match (sem_binary_operation ??????); normalize nodelta
     
    11861186      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
    11871187        #Hsim %1 * #val #trace whd in match (exec_expr ????); #Hstep
    1188         cut (∃block,offset,r,ptype,pc. (exec_lvalue ge en m e1 = OK ? 〈block, offset, trace〉) ∧
    1189                                  (pointer_compat_dec block r = inl ?? pc) ∧
    1190                                  (ty = Tpointer r ptype) ∧
    1191                                   val = Vptr (mk_pointer r block pc offset))
     1188        cut (∃block,offset,ptype. (exec_lvalue ge en m e1 = OK ? 〈block, offset, trace〉) ∧
     1189                                 (ty = Tpointer ptype) ∧
     1190                                  val = Vptr (mk_pointer block offset))
    11921191        [ 1: lapply Hstep -Hstep
    11931192             cases (exec_lvalue ge en m e1)
    11941193             [ 1: * * #block #offset #trace' normalize nodelta
    11951194                  cases ty
    1196                   [ 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
    1197                   | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
     1195                  [ 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     1196                  | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
    11981197                  normalize nodelta try (#Heq destruct)
    1199                   @(ex_intro … block) @(ex_intro … offset) @(ex_intro … rg) @(ex_intro … ptr_ty)
    1200                   cases (pointer_compat_dec block rg) in Heq; normalize
    1201                   [ 2: #Hnotcompat #Hcontr destruct
    1202                   | 1: #compat #Heq @(ex_intro … compat) try @conj try @conj try @conj destruct // ]
     1198                  @(ex_intro … block) @(ex_intro … offset) @(ex_intro … ptr_ty)
     1199                  try @conj try @conj destruct //
    12031200             | 2: normalize nodelta #errmesg #Hcontr destruct
    12041201             ]
    1205         | 2: * #block * #offset * #region * #ptype * #pc * * * #Hexec_lvalue #Hptr_compat #Hty_eq #Hval_eq
     1202        | 2: * #block * #offset * #ptype * * #Hexec_lvalue #Hty_eq #Hval_eq
    12061203             whd in match (exec_expr ????); >(Hsim … Hexec_lvalue) normalize nodelta destruct normalize nodelta
    1207              >Hptr_compat //
     1204             //
    12081205        ]
    12091206     ]
     
    16441641           >Htype_eq
    16451642           cases (typeof rec_expr1) normalize nodelta
    1646            [ 2: #sz #sg | 3: #fl | 4: #rg #ty | 5: #rg #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #rg #ty ]
     1643           [ 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
    16471644           [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/
    16481645           | 6,7: cases Hsim_lvalue
     
    16591656           >Htype_eq
    16601657           cases (typeof rec_expr1) normalize nodelta
    1661            [ 2: #sz #sg | 3: #fl | 4: #rg #ty | 5: #rg #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #rg #ty ]
     1658           [ 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
    16621659           [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/
    16631660           | 6,7: cases Hsim_lvalue
     
    19311928   whd in match (exec_lvalue' ??? (Efield rec_expr1 f) ty); 
    19321929   [ 1: >Htype_eq cases (typeof rec_expr1) normalize nodelta
    1933        [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
    1934        | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
     1930       [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty'
     1931       | 7: #id #fl | 8: #id #fl | 9: #id ]
    19351932       try (@SimFail /2 by ex_intro/)
    19361933       cases Hsim_lvalue
     
    19431940   | 2: (* Note: identical to previous case. Too lazy to merge and manually shift indices. *)
    19441941       >Htype_eq cases (typeof rec_expr1) normalize nodelta
    1945        [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
    1946        | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
     1942       [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty'
     1943       | 7: #id #fl | 8: #id #fl | 9: #id ]
    19471944       try (@SimFail /2 by ex_intro/)
    19481945       cases Hsim_lvalue
     
    22042201      normalize in match (typeof (Expr ??));
    22052202      cases ty' in Hsim_lvalue; normalize nodelta
    2206       [ 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
    2207       | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
     2203      [ 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
     2204      | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
    22082205      #Hsim_lvalue
    22092206      try (@SimFail /2 by ex_intro/)
     
    26092606                    | 3: #res #k0 #k0' #m0 #Hcont_cast #Habsurd destruct (Habsurd)
    26102607                    | 4: #r #Habsurd destruct (Habsurd) ]                   
    2611                | 3: #irrelevant #Habsurd destruct
    2612                | 5: #irrelevant1 #irrelevant2 #irrelevant3 #Habsurd destruct
     2608               | 3,4,9: #irrelevant #Habsurd destruct
    26132609               | *: #irrelevant1 #irrelevant2 #Habsurd destruct ]
    26142610          | 2: (* Kseq stm' k' *)
     
    26752671                                  (free_list m (blocks_of_env en)))} @conj
    26762672                    [ 1: // | 2: %3 @cc_call // ]                                 
    2677                | 3: #irrelevant #Habsurd destruct (Habsurd)
    2678                | 5: #irrelevant1 #irrelevant2 #irrelevant3 #Habsurd destruct (Habsurd)
     2673               | 3,4,9: #irrelevant #Habsurd destruct (Habsurd)
    26792674               | *: #irrelevant1 #irrelevant2 #Habsurd destruct (Habsurd) ]
    26802675           ]
     
    29042899          [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta
    29052900               whd in match (ret ??) in ⊢ (% → %);
    2906                [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
    2907                | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
     2901               [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty'
     2902               | 7: #id #fl | 8: #id #fl | 9: #id ]
    29082903               #H destruct (H)
    29092904               %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env en)))}
Note: See TracChangeset for help on using the changeset viewer.