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/CexecComplete.ma

    r2468 r2588  
    194194    >(yields_eq ??? H5)
    195195    @refl
    196 | #e1 #e2 #ty #v1 #tr #H1 #H2 #H3 whd in ⊢ (??%?);
     196| #e1 #e2 #ty #v1 #tr #vres #H1 #H2 #Hcast #H3 whd in ⊢ (??%?);
    197197    >(yields_eq ??? H3) whd in ⊢ (??%?);
    198198    >(yields_eq ??? (bool_of_true ?? H2))
    199     @refl
    200 | #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 #H6 whd in ⊢ (??%?);
     199    >Hcast @refl
     200| #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #vres #H1 #H2 #H3 #H4 #Hcast #H5 #H6 whd in ⊢ (??%?);
    201201    >(yields_eq ??? H5) whd in ⊢ (??%?);
    202202    >(yields_eq ??? (bool_of_false ?? H2))
     
    204204    elim (bool_of_val_3_complete … H4); #b *; #evb #Hb
    205205    >(yields_eq ??? Hb) whd in ⊢ (??%?); <evb
    206     @refl
    207 | #e1 #e2 #ty #v1 #tr #H1 #H2 #H3 whd in ⊢ (??%?);
     206    >Hcast
     207    @refl
     208| #e1 #e2 #ty #v1 #tr #vres #H1 #H2 #Hcast #H3 whd in ⊢ (??%?);
    208209    >(yields_eq ??? H3) whd in ⊢ (??%?);
    209210    >(yields_eq ??? (bool_of_false ?? H2))
    210     @refl
    211 | #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 #H6 whd in ⊢ (??%?);
     211    >Hcast
     212    @refl
     213| #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #vres #H1 #H2 #H3 #H4 #Hcast #H5 #H6 whd in ⊢ (??%?);
    212214    >(yields_eq ??? H5) whd in ⊢ (??%?);
    213215    >(yields_eq ??? (bool_of_true ?? H2))
     
    215217    elim (bool_of_val_3_complete … H4); #b *; #evb #Hb
    216218    >(yields_eq ??? Hb) whd in ⊢ (??%?); <evb
     219    >Hcast normalize
    217220    @refl
    218221| #e #ty #ty' #v1 #v #tr #H1 #H2 #H3 whd in ⊢ (??%?);
Note: See TracChangeset for help on using the changeset viewer.