# Changeset 2565

Ignore:
Timestamp:
Dec 19, 2012, 6:11:23 PM (7 years ago)
Message:

Cl to Cm progress.

Location:
src/Clight
Files:
4 edited

Unmodified
Removed
• ## src/Clight/frontend_misc.ma

 r2510 | 2: * #Habsurd @(False_ind … (Habsurd … (refl ? i))) ] qed. lemma intsize_eq_inversion : ∀sz,sz'. ∀A:Type[0]. ∀ok,not_ok. intsize_eq_elim' sz sz' (λsz,sz'. res A) (OK ? ok) (Error ? not_ok) = (OK ? ok) → sz = sz'. * * try // normalize #A #ok #not_ok #Habsurd destruct qed. lemma intsize_eq_elim_dec : ∀sz1,sz2. ∀P: ∀sz1,sz2. Type[0]. ((∀ifok,iferr. intsize_eq_elim' sz1 sz1 P ifok iferr = ifok) ∧ sz1 = sz2) ∨ ((∀ifok,iferr. intsize_eq_elim' sz1 sz2 P ifok iferr = iferr) ∧ sz1 ≠ sz2). * * #P normalize try /3 by or_introl, conj, refl/ %2 @conj try // % #H destruct qed. lemma typ_eq_elim : ∀t1,t2. ∀(P: (t1=t2)+(t1≠t2) → Prop). (∀H:t1 = t2. P (inl ?? H)) → (∀H:t1 ≠ t2. P (inr ?? H)) → P (typ_eq t1 t2). #t1 #t2 #P #Hl #Hr @(match typ_eq t1 t2 with [ inl H ⇒ Hl H | inr H ⇒ Hr H ]) qed. lemma eq_nat_dec_true : ∀n. eq_nat_dec n n = inl ?? (refl ? n). #n elim n try // #n' #Hind whd in ⊢ (??%?); >Hind @refl qed. lemma type_eq_dec_true : ∀ty. type_eq_dec ty ty = inl ?? (refl ? ty). #ty cases (type_eq_dec ty ty) #H destruct (H) try @refl @False_ind cases H #J @J @refl qed. lemma typ_eq_refl : ∀t. typ_eq t t = inl ?? (refl ? t). * [ * * normalize @refl | @refl ] qed. lemma intsize_eq_elim_inversion : ∀A:Type[0]. ∀sz1,sz2. ∀elt1,f,errmsg,res. intsize_eq_elim ? sz1 sz2 bvint elt1 f (Error A errmsg) = OK ? res → ∃H:sz1 = sz2. OK ? res = (f (eq_rect_r ? sz1 sz2 (sym_eq ??? H) ? elt1)). #A * * #elt1 #f #errmsg #res normalize #H destruct (H) %{(refl ??)} normalize nodelta >H @refl qed. lemma inttyp_eq_elim_true' : ∀sz,sg,P,p1,p2. inttyp_eq_elim' sz sz sg sg P p1 p2 = p1. * * #P #p1 #p2 normalize try @refl qed. (* --------------------------------------------------------------------------- *) ] qed. axiom commutative_multiplication : ∀n. ∀v1,v2:BitVector n. multiplication ? v1 v2 = multiplication ? v2 v1. lemma commutative_short_multiplication : ∀n. ∀v1,v2:BitVector n. short_multiplication ? v1 v2 = short_multiplication ? v2 v1. #n #v1 #v2 whd in ⊢ (??%%); >commutative_multiplication @refl qed. lemma sign_ext_same_size : ∀n,v. sign_ext n n v = v. #n #v whd in match (sign_ext ???); >nat_compare_eq @refl qed. axiom sign_ext_zero : ∀sz1,sz2. sign_ext sz1 sz2 (zero sz1) = zero sz2. axiom zero_ext_zero : ∀sz1,sz2. zero_ext sz1 sz2 (zero sz1) = zero sz2. axiom multiplication_zero : ∀n:nat. ∀v : BitVector n. multiplication … (zero ?) v = (zero ?). axiom short_multiplication_zero : ∀n. ∀v:BitVector n. short_multiplication ? (zero ?) v = (zero ?).
• ## src/Clight/memoryInjections.ma

 r2554 (* End of the definitions on memory injections. Now, on to proving some lemmas. *) (* particulars inversion. *) (* particulars inversions. *) lemma value_eq_ptr_inversion : ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2. | 3: #Hv1 #Hv2 #_ destruct @H3 | 4: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H4 // ] qed. (* Avoids the use of cut in toCminorCorrectness *) lemma value_eq_triangle_diagram : ∀E,v1,v2,v3. value_eq E v1 v2 → v2 = v3 → value_eq E v1 v3. #H1 #H2 #H3 #H4 #H5 #H6 destruct // qed. (* If we succeed to load something by value from a 〈b,off〉 location, Zltb (block_id b) (nextblock m) = true ∧ Zleb (low_bound m b) (Z_of_unsigned_bitvector ? (offv off)) = true ∧ Zltb (Z_of_unsigned_bitvector ? (offv off)) (high_bound m b) = true. #ty #m * #brg #bid #off #v
• ## src/Clight/toCminor.ma

 r2554 match classify_add ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with [ add_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oadd ??) e1 e2) (*| add_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddf sz) e1 e2) *) (* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *) | add_case_pi n ty sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16) (fix_ptr_type … e2) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty)))))) | add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch) ]. ]. definition translate_sub ≝ match classify_sub ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with [ sub_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osub ??) e1 e2) (* | sub_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osubf sz) e1 e2) *) (* XXX could optimise cast as above *) | sub_case_pi n ty sz sg ⇒