Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (7 years ago)
Author:
garnier
Message:

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r2428 r2468  
    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 |  | #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,10,18,26: #sz' #sg | 3,11,19,27: #ty' | 4,12,20,28: (*#r*) #ty #n
     9           | 5,13,21,29: #args #rty | 6,7,14,15,22,23,30,31: #id #fs | 8,16,24,32: (*#r*) #id ]
    910whd in ⊢ (??%? → ?);
    1011[ 2: @intsize_eq_elim_elim
     
    1516    ]
    1617  ]
    17 | 8: #H cases (eq_dec f Fzero)
     18(*| 8: #H cases (eq_dec f Fzero)
    1819  [ #e >e in H ⊢ %; >Feq_zero_true #E destruct @bool_of_val_false @is_false_float
    1920  | #ne >Feq_zero_false in H; // #E destruct @bool_of_val_true @is_true_float @ne
    20   ]
    21 | 14: #H destruct @bool_of_val_false @is_false_pointer
    22 | 15: #H destruct @bool_of_val_true @is_true_pointer_pointer
     21  ]*)
     22| 7: #H destruct @bool_of_val_false @is_false_pointer
     23| 8: #H destruct @bool_of_val_true @is_true_pointer_pointer
    2324| *: #H destruct
    2425] qed.
     
    3940@eq_bv_elim
    4041[ #e >e
    41     cases ty; [ | #sz' #sg | #fs | (*#sp*) #ty | (*#sp*) #ty #n | #args #rty | #id #fs | #id #fs | (*#r*) #id ]
     42    cases ty; [ | #sz' #sg (* | #fs *) | (*#sp*) #ty | (*#sp*) #ty #n | #args #rty | #id #fs | #id #fs | (*#r*) #id ]
    4243    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 ]
     44    cases ty' in H ⊢ %; [ | #sz'' #sg (* | #fs*) | (*#sp*) #ty | (*#sp*) #ty #n | #args #rty | #id #fs | #id #fs | (*#r*) #id ]
    4445    try (@eq_intsize_elim #E) whd in ⊢ (??%? → ?); #H destruct @cast_ip_z //
    4546| #_ whd in ⊢ (??%? → ?); #H destruct
    4647]
    47 qed. 
     48qed.
    4849
    4950lemma exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'.
     
    5354| #sz #i cases ty;
    5455  [ #H whd in H:(??%?); destruct;
    55   | 3: #a #H whd in H:(??%?); destruct;
    56   | 7,8,9: #a [ 1,2: #b ] #H whd in H:(??%?); destruct;
     56(* | 3: #a #H whd in H:(??%?); destruct; *)
     57  | 6,7,8: #a [ 1,2: #b ] #H whd in H:(??%?); destruct;
    5758  | #sz1 #si1 cases ty';
    5859    [ whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
     
    6061      | *; whd #H whd in H:(??%?); destruct;
    6162      ]
    62     | 3: #a whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
     63     (* | 3: #a whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    6364      [ #E #H whd in H:(??%?); destruct
    6465      | *; whd #H whd in H:(??%?); destruct; @cast_if
    65       ]
    66     | 2,7,8,9: #a [1,2,3: #b] whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
     66      ] *)
     67    | 2,6,7,8: #a [1,2,3: #b] whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    6768      [ 1,3,5,7: #NE #H destruct
    6869      | *: *; whd #H whd in H:(??%?); destruct; //
    6970      ]
    70     | 4,5,6: [ #ty'' letin t ≝ (Tpointer ty'')
     71    | 3,4,5: [ #ty'' letin t ≝ (Tpointer ty'')
    7172             | #ty'' #n letin t ≝ (Tarray ty'' n)
    7273             | #args #rty letin t ≝ (Tfunction args rty) ]
     
    9192        ]
    9293  ]
    93 | #f cases ty;  [ 3,4,9: #x | 2,5,6,7,8: #x #y ]
     94(*| #f cases ty;  [ 3,4,9: #x | 2,5,6,7,8: #x #y ]
    9495                    [ cases ty'; [ #e | 3,4,9: #a #e | 2,6,7,8: #a #b #e | #a #b #e ]
    9596                        whd in e:(??%?); destruct; //;
    9697                    | *: #e whd in e:(??%?); destruct
    97                     ]
    98 | cases ty; [ 3,4,9: #x | 2,5,6,7,8: #x #y ]
     98                    ] *)
     99| cases ty; [ 3,8: #x | 2,4,5,6,7: #x #y ]
    99100    whd in ⊢ (??%? → ?); #H destruct
    100101    cases ty' in H; normalize; try #a try #b try #c try #d destruct;
     
    121122*)
    122123| #ptr
    123   cases ty; [ 3,4,9: #x | 2,5,6,7,8: #x #y ]
     124  cases ty;  [ 3,8: #x | 2,4,5,6,7: #x #y ]
    124125  #E whd in E:(??%?); destruct
    125126  cases ty' in E ⊢ %; normalize #A try #B try #C try #D destruct /2/
    126127] qed.
     128
     129
    127130
    128131
     
    132135[ #sz #ty #c whd in ⊢ (???%); cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%);
    133136  @eq_intsize_elim #E try @I <E whd %
    134 | #ty #c whd //
     137(*| #ty #c whd //*)
    135138(* expressions that are lvalues *)
    136139| #e' #ty cases e'; //; [ #i #He' | #e #He' | #e #i #He' ] whd in He' ⊢ %;
     
    210213(* exec_lvalue fails on non-lvalues. *)
    211214| #e' #ty cases e';
    212     [ 2,5,12: #a #H | 3,4: #a * | 13,14: #a #b * | 1,6,8,10,11: #a #b #H | 7,9: #a #b #c #H ]
    213     @I
     215    [ 2,4,11: #a #H try @I @(False_ind … H) | 3: #a * | 12,13: #a #b * | 1,5,7,9,10: #a #b #H @I | 6,8: #a #b #c #H @I ]
     216    try @I
    214217] qed.
    215218
     
    218221eval_lvalue ge en m e loc off tr.
    219222#ge #en #m #e #loc #off #tr #ty #H inversion H;
    220 [ 1,2,5: #a #b #c #H @False_ind destruct (H);
     223[ 1,4: #a #b #c #H @False_ind destruct (H);
    221224| #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1; #H1 @False_ind
    222225    @(eval_lvalue_inv_ind … H1)
     
    318321  [ //
    319322  | #ty #tys whd in ⊢ (???%);
    320     cases ty [ #sz #sg | | #sz ] cases v //
    321     [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?);
    322       @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct
    323     | #v ] @bind_OK #evs #CHECKevs
     323    cases ty [ #sz #sg | ] cases v //
     324    #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?);
     325    @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct
     326    @bind_OK #evs #CHECKevs
    324327      @(evl_match_cons ??????? (P_res_to_P ???? (IH ?) CHECKevs))
    325328      //
Note: See TracChangeset for help on using the changeset viewer.