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

    r2578 r2588  
    464464qed.
    465465
     466lemma value_eq_int_inversion' :
     467  ∀E,sz,i,v. value_eq E v (Vint sz i) → v = (Vint sz i).
     468#E #sz #i #v #Heq inversion Heq
     469[ 1: #_ #Habsurd destruct (Habsurd)
     470| 2: #sz #i #Heq #Heq' #_ @refl
     471| 3: #_ #Habsurd destruct (Habsurd)
     472| 4: #p1 #p2 #Heq #Heqv #Heqv2 #_ destruct ]
     473qed.
     474
    466475lemma value_eq_null_inversion :
    467476  ∀E,v. value_eq E Vnull v → v = Vnull.
    468477#E #v #Heq inversion Heq //
    469478#p1 #p2 #Htranslate #Habsurd lapply (jmeq_to_eq ??? Habsurd)
     479#Habsurd' destruct
     480qed.
     481
     482lemma value_eq_null_inversion' :
     483  ∀E,v. value_eq E v Vnull → v = Vnull.
     484#E #v #Heq inversion Heq //
     485#p1 #p2 #Htranslate #_ #Habsurd lapply (jmeq_to_eq ??? Habsurd)
    470486#Habsurd' destruct
    471487qed.
     
    17331749(* value_eq lifts to subtraction *)
    17341750lemma sub_value_eq :
    1735   ∀E,v1,v2,v1',v2',ty1,ty2.
     1751  ∀E,v1,v2,v1',v2',ty1,ty2,target.
    17361752   value_eq E v1 v2 →
    17371753   value_eq E v1' v2' →
    1738    ∀r1. (sem_sub v1 ty1 v1' ty2=Some val r1→
    1739            ∃r2:val.sem_sub v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
    1740 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
     1754   ∀r1. (sem_sub v1 ty1 v1' ty2 target=Some val r1→
     1755           ∃r2:val.sem_sub v2 ty1 v2' ty2 target=Some val r2∧value_eq E r1 r2).
     1756#E #v1 #v2 #v1' #v2' #ty1 #ty2 #target #Hvalue_eq1 #Hvalue_eq2 #r1
    17411757@(value_eq_inversion E … Hvalue_eq1)
    17421758[  | #sz #i | 3: | 4: #p1 #p2 #Hembed ]
    1743 [ 1: whd in match (sem_sub ????); normalize nodelta
     1759[ 1: whd in match (sem_sub ?????); normalize nodelta
    17441760     cases (classify_sub ty1 ty2) normalize nodelta
    17451761     [ #sz #sg | #n #ty #sz #sg | #n #sz #sg #ty |#ty1' #ty2' ]
    17461762     #Habsurd destruct (Habsurd)
    1747 | 2: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
     1763| 2: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta
    17481764     cases (classify_sub ty1 ty2) normalize nodelta     
    17491765     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
     
    17561772      | 2: #Heq destruct (Heq) normalize nodelta
    17571773           #Heq destruct (Heq)
    1758           /3 by ex_intro, conj, vint_eq/           
     1774          /3 by ex_intro, conj, vint_eq/
    17591775      ]
    17601776(*| 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
     
    17671783     #Heq destruct (Heq)
    17681784     /3 by ex_intro, conj, vfloat_eq/ *)
    1769 | 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
     1785| 3: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta
    17701786     cases (classify_sub ty1 ty2) normalize nodelta
    17711787     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
     
    17761792     [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
    17771793                      | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
    1778      | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ]
    1779 | 4: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
     1794     | 2: cases target
     1795          [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     1796          | #structname #fieldspec | #unionname #fieldspec | #id ]
     1797          normalize nodelta
     1798          #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ]
     1799| 4: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta
    17801800     cases (classify_sub ty1 ty2) normalize nodelta
    17811801     [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ]
     
    18101830               cases (eqb (sizeof tsg) O) normalize nodelta
    18111831               [ 1: #Habsurd destruct (Habsurd)
    1812                | 2: >(sub_offset_translation 32 off1 off1' dest_off)
    1813                     cases (division_u 31
    1814                             (sub_offset 32 (offset_plus off1 dest_off) (offset_plus off1' dest_off))
    1815                             (repr (sizeof tsg)))
     1832               | 2: cases target
     1833                    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     1834                    | #structname #fieldspec | #unionname #fieldspec | #id ]
     1835                    normalize nodelta
     1836                    #Heq destruct (Heq)
     1837                    <(sub_offset_translation 32 off1 off1' dest_off)
     1838                    cases (division_u ?
     1839                            (sub_offset ? off1 off1')
     1840                            (repr (sizeof tsg))) in Heq;
    18161841                    [ 1: normalize nodelta #Habsurd destruct (Habsurd)
    1817                     | 2: #r1' normalize nodelta #Heq2 destruct (Heq2)
     1842                    | 2: #r1' cases sg normalize nodelta #Heq2 destruct (Heq2)
    18181843                         /3 by ex_intro, conj, vint_eq/ ]
    18191844    ] ] ]
    18201845] qed.
    1821 
    18221846
    18231847lemma mul_value_eq :
     
    20892113] qed.
    20902114
    2091 (* /!\ Warning TODO Warning /!\ *)
    2092 
    20932115(* Note that x and y are bounded below and above, similarly for the shifted offsets.
    20942116   This is enough to prove that there is no "wrap-around-the-end" problem,
    20952117   /provided we know that the block bounds are implementable by 2^16 bitvectors/.
    2096    We axiomatize it for now. Notice that this axiom is in fact not provable and implies False.
    2097    In order to be true, we need to prove that the (x+delta) and (y+delta) do not overflow.
    2098    This is provable from the fact that the original pointers in which the offsets reside are "valid".
    2099    This in turn is ensured by the memory injection.
    2100    /DO NOT USE IT ELSEWHERE, this is just a temporary stopgap./ *)
     2118   We axiomatize it for now. *)
    21012119axiom cmp_offset_translation :
    21022120  ∀op,delta,x,y.
Note: See TracChangeset for help on using the changeset viewer.