Ignore:
Timestamp:
Jan 23, 2013, 2:38:06 PM (7 years ago)
Author:
garnier
Message:

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r2468 r2588  
    185185    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1
    186186    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
     187    normalize nodelta
    187188    [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2
    188         @bind_OK #b2 #eb2
    189         @(eval_Eandbool_2 … He1 … He2)
    190         [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ]
    191     | @(eval_Eandbool_1 … He1) @(bool_of … Hb1)
     189        @bind_OK #b2 #eb2 whd in match (cast_bool_to_target ??);
     190        cases ty
     191        [ | #sz #sg | #ptr_ty | #arr_ty #arr_sz | #dom #codom | #sname #flspc | #uname #flspc | #id ]
     192        try @I normalize nodelta
     193        @(eval_Eandbool_2 … (of_bool b2) … He1 … He2)
     194        [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) | @refl ]
     195    | cases ty
     196      [ | #sz #sg | #ptr_ty | #arr_ty #arr_sz | #dom #codom | #sname #flspc | #uname #flspc | #id ]
     197      try @I
     198      @(eval_Eandbool_1 … He1) [ @(bool_of … Hb1) | @refl ]
    192199    ]
    193200| #ty #e1 #e2 #He1 #He2
    194201    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1
    195202    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
    196     [ @(eval_Eorbool_1 … He1) @(bool_of … Hb1)
     203    normalize nodelta
     204    [ cases ty
     205      [ | #sz #sg | #ptr_ty | #arr_ty #arr_sz | #dom #codom | #sname #flspc | #uname #flspc | #id ]
     206      try @I
     207      @(eval_Eorbool_1 … He1) [ @(bool_of … Hb1) | @refl ]
    197208    | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2
    198209        @bind_OK #b2 #eb2
    199         @(eval_Eorbool_2 … He1 … He2)
    200         [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ]
     210        cases ty
     211        [ | #sz #sg | #ptr_ty | #arr_ty #arr_sz | #dom #codom | #sname #flspc | #uname #flspc | #id ]
     212        try @I
     213        @(eval_Eorbool_2 … (of_bool b2) … He1 … He2)
     214        [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) | @refl ]
    201215    ]
    202216| #ty #ty' cases ty try #sz try #sg try #x //
     
    235249| #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
    236250| #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
    237 | #a #b #c #d #e #f #g #bad destruct (bad);
    238 | #a #b #c #d #e #f #g #h #i #j #k #l #bad destruct (bad);
    239 | #a #b #c #d #e #f #g #bad destruct (bad);
    240 | #a #b #c #d #e #f #g #h #i #j #k #l #bad  destruct (bad);
     251| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
     252| #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad destruct (bad);
     253| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
     254| #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad  destruct (bad);
    241255| #a #b #c #d #e #f #g #h #bad destruct (bad);
    242256| #a #b #c #d #e #f #bad destruct (bad);
Note: See TracChangeset for help on using the changeset viewer.