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

    r2582 r2588  
    259259λty1,ty2,P,p.
    260260  do E ← assert_type_eq ty1 ty2;
    261   OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p). 
     261  OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p).
     262 
     263(* associated reasoning principle *)
     264lemma type_should_eq_inversion :
     265  ∀ty1,ty2,P,f,res.
     266    type_should_eq ty1 ty2 P f = OK ? res →
     267    ty1 = ty2 ∧ f ≃ res.
     268#ty1 #ty2 #P #f #res normalize
     269cases (type_eq_dec ty1 ty2) normalize nodelta
     270[ 2: #Hneq #Habsurd destruct ]
     271#Heq #Heq2 @conj try assumption
     272destruct (Heq2) cases Heq normalize nodelta
     273@eq_to_jmeq @refl
     274qed. 
    262275
    263276(* same gig for regions *)
     
    274287  ].
    275288destruct %
     289qed.
     290
     291(* associated reasoning principle *)
     292lemma typ_should_eq_inversion :
     293  ∀ty1,ty2,P,a,x.
     294    typ_should_eq ty1 ty2 P a = OK ? x →
     295    ty1 = ty2 ∧ a ≃ x.
     296* [ #sz #sg ] * [ 1,3: #sz2 #sg2 ]
     297[ 4: #P #a #x normalize #H destruct (H) @conj try @refl @refl_jmeq
     298| 3: cases sz cases sg #P #A #x normalize #H destruct
     299| 2: cases sz2 cases sg2 #P #a #x normalize #H destruct ]
     300cases sz cases sz2 cases sg cases sg2
     301#P #a #x #H normalize in H:(??%?); destruct (H)
     302try @conj try @refl try @refl_jmeq
    276303qed.
    277304
     
    340367    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddip I16) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))) (fix_ptr_type … e2))
    341368| add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch)
    342 ].
    343 
     369].
     370
     371
     372(* XXX Clight pointer/int subtraction uses neg_shift_pointer_n, which boils down to (sub32 lhs (mul32 (const32 sizeof_ty) (sext32/zext32 rhs))),
     373 * whereas Cminor uses neg_shift_pointer, which translates into (sub32 lhs (sext32 rhs)). We have to translate the multiplication as actual
     374 * Cminor code, yielding something like (sub32 lhs (sext32 (mulXX (constXX sizeof_ty) (sextXX/zextXX rhs)))). In the original translate_sub,
     375 * XX=16, which we can't prove equivalent in general. Moreover, Osubpi expects a /signed/ integer argument, whereas Clight does not care and
     376 * casesplits on the sign to select either a zero extension or a sign extension.
     377 * λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I16) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
     378      corresponding cl value: Some ? (Vptr (shift_pointer_n ? ptr1 (sizeof ty) sg n2))  =
     379      mk_offset (sub32 lhs (mult32 (const32 (sizeof ty)) (sext32/zext32 rhs)))
     380
     381      cminor
     382      mk_offset (sub32 lhs (sext32 ))
     383 *)
    344384definition translate_sub ≝
    345385λty1,ty2,ty'.
     
    350390(* XXX could optimise cast as above *)
    351391| sub_case_pi n ty sz sg ⇒
    352     λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I16) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
     392    (* XXX This is so ugly. *)
     393    λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I32) (fix_ptr_type … e1)
     394                                                    (Op1 ?? (Ocastint ?? I32 Signed) (Op2 ??? (Omul I16 sg) (Op1 ?? (Ocastint ??? sg) e2)
     395                                                                                     (Cst ? (Ointconst I16 sg (repr I16 (sizeof ty)))))))
    353396(* XXX check in detail? *)
    354397| sub_case_pp n1 n2 ty1 ty2 ⇒
    355398    λe1,e2. match ty' return λty'. res (CMexpr (typ_of_type ty')) with
    356399    [ Tint sz sg ⇒
    357       (* XXX we make the constant unsigned to match CL semantics. *)
     400      (* XXX we make the constant unsigned to match CL semantics. We also use 32 bits, still for CL semantics. Documented in Csem.ma@sem_sub *)
    358401      (* OK ? (Op1 ?? (Ocastint I16 Signed sz sg) (Op2 ??? (Odiv I16) (Op2 ??? (Osubpp I16) (fix_ptr_type … e1) (fix_ptr_type ?? e2)) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty2)))))) *)
    359          OK ? (Op1 ?? (Ocastint I16 Unsigned sz sg) (Op2 ??? (Odivu I16) (Op2 ??? (Osubpp I16) (fix_ptr_type … e1) (fix_ptr_type ?? e2)) (Cst ? (Ointconst I16 Unsigned (repr ? (sizeof ty2))))))     
     402         OK ? (Op1 ?? (Ocastint I32 Unsigned sz sg) (Op2 ??? (Odivu I32) (Op2 ??? (Osubpp I32) (fix_ptr_type … e1) (fix_ptr_type ?? e2)) (Cst ? (Ointconst I32 Unsigned (repr ? (sizeof ty1))))))
    360403    | _ ⇒ Error ? (msg TypeMismatch)
    361404    ]
     
    599642]. whd normalize nodelta @pi2
    600643qed.
     644
     645definition cm_zero ≝ λsz,sg. Cst ? (Ointconst sz sg (zero ?)).
     646definition cm_one  ≝ λsz,sg. Cst ? (Ointconst sz sg (repr sz 1)).
    601647
    602648(* Translate Clight exprs into Cminor ones.
     
    740786          with
    741787          [ ASTint sz1 _ ⇒ λe1'.
    742             OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz sg (zero ?))), ?»
     788            (* Producing a nested comparison to match CL. *)
     789            OK ? «Cond ??? e1' (Cond ??? e2' (cm_one sz sg) (cm_zero sz sg)) (cm_zero sz sg), ?»
    743790          | _ ⇒ λ_. Error ? (msg TypeMismatch)
    744791          ] e1'
    745792      | _ ⇒ Error ? (msg TypeMismatch)
    746793      ]
    747 (*  | Eandbool e1 e2 ⇒
    748       do e1' ← translate_expr vars e1;
    749       do e2' ← translate_expr vars e2;
    750       match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
    751       [ Tint sz sg ⇒
    752         match sz
    753         return λsz'. (sz = sz') → res (Σe':CMexpr (typ_of_type ?). ?)
    754         with
    755         [ I32 ⇒ λHsz_eq.
    756           do e2' ← type_should_eq ? (Tint I32 sg) (λx.Σe:CMexpr (typ_of_type x).?) e2';
    757           match typ_of_type (typeof e1)
    758           return λx.
    759             (Σe:CMexpr x. expr_vars ? e (local_id vars)) → (res ?)
    760           with
    761           [ ASTint sz1 _ ⇒ λe1'.
    762             OK ? «Cond ??? e1' e2' (Cst ? (Ointconst I32 sg (zero ?))), ?»
    763           | _ ⇒ λ_. Error ? (msg TypeMismatch)
    764           ] e1'
    765         | _ ⇒ λ_. Error ? (msg TypeMismatch)
    766         ] (refl ? sz)
    767       | _ ⇒ Error ? (msg TypeMismatch)
    768       ]*)
    769794  | Eorbool e1 e2 ⇒
    770795      do e1' ← translate_expr vars e1;
     
    775800        match typ_of_type (typeof e1)
    776801        return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with
    777         [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz sg (repr ? 1))) e2', ?»
     802        [ ASTint _ _ ⇒ λe1'.
     803          OK ? «Cond ??? e1' (cm_one sz sg) (Cond ??? e2' (cm_one sz sg) (cm_zero sz sg)), ?»
    778804        | _ ⇒ λ_. Error ? (msg TypeMismatch)
    779805        ] e1'
     
    858884| @(translate_binop_vars … E) @pi2
    859885| % [ % ] @pi2
    860 | % [ % @pi2 ] whd @I
    861 | % [ % [ @pi2 | @I ] | @pi2 ]
     886| % [ % try @pi2 whd @conj try @conj try // @pi2 ] whd @I
     887| % [ % [ @pi2 | @I ] | % try @conj try // @pi2 ]
    862888| % [ @pi2 | @I ]
    863889| % [ @pi2 | @I ]
Note: See TracChangeset for help on using the changeset viewer.