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

    r2510 r2588  
    21242124(* Conservation of the semantics of binary operators under memory extensions.
    21252125   Tried to factorise it a bit but the play with indexes just becomes too messy.  *)
    2126 lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2,writeable.
     2126lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2,target_type,writeable.
    21272127  ∀Hext:sr_memext m1 m2 writeable. ∀res.
    2128   sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m1 = Some ? res →
    2129   sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m2 = Some ? res.
    2130 #op #v1 #v2 #e1 #e2 #m1 #m2 #writeable #Hmemext #res cases op
    2131 whd in match (sem_binary_operation ??????);
     2128  sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m1 target_type = Some ? res →
     2129  sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m2 target_type = Some ? res.
     2130#op #v1 #v2 #e1 #e2 #m1 #m2 #target_type #writeable #Hmemext #res cases op
     2131whd in match (sem_binary_operation ???????);
    21322132try //
    2133 whd in match (sem_binary_operation ??????);
     2133whd in match (sem_binary_operation ???????);
    21342134lapply (me_valid_pointers … Hmemext)
    21352135lapply (me_not_writeable_ptr … Hmemext)
     
    22822282     >(Hsim2 ? (refl ??))
    22832283     whd in match (m_bind ?????);
    2284      lapply (sim_sem_binary_operation op v pval e1 e2 m1 m2 writeable Hext)
    2285      cases (sem_binary_operation op v (typeof e1) pval (typeof e2) m1)
     2284     lapply (sim_sem_binary_operation op v pval e1 e2 m1 m2 ty writeable Hext)
     2285     cases (sem_binary_operation op v (typeof e1) pval (typeof e2) m1 ty)
    22862286     [ 1: #_ // ] #val #H >(H val (refl ??))
    22872287     normalize destruct @conj @refl
     
    23192319     whd in match (m_bind ?????);
    23202320     whd in match (m_bind ?????);
    2321      [ 2,3: normalize @conj try @refl ]
     2321     [ 2,3: cases (cast_bool_to_target ty ?) normalize // #v @conj try @refl ]
    23222322     cases (exec_expr ge en1 m1 e2) in Hsim2;
    23232323     [ 2,4: #error #_ normalize @I ]
     
    23262326     cases (exec_bool_of_val v2 (typeof e2))
    23272327     [ 2,4: #error normalize @I ]
    2328      * normalize @conj @refl
     2328     *
     2329     whd in match (m_bind ?????);
     2330     cases (cast_bool_to_target ty ?) normalize // #v @conj try @refl
    23292331| 12: #ty #ty' cases ty
    23302332     [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ]
Note: See TracChangeset for help on using the changeset viewer.