# Changeset 744

Ignore:
Timestamp:
Apr 7, 2011, 6:53:59 PM (10 years ago)
Message:

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

Location:
src
Files:
15 edited

Unmodified
Removed
• ## src/ASM/Arithmetic.ma

 r724 λb, c: BitVector n. addition_n n b (two_complement_negation n c). definition multiplication ≝ λn: nat. λb, c: BitVector n. let b_nat ≝ nat_of_bitvector ? b in let c_nat ≝ nat_of_bitvector ? c in let result ≝ b_nat * c_nat in bitvector_of_nat (n + n) result. definition division_u ≝ λn: nat. λb, c: BitVector n. let b_nat ≝ nat_of_bitvector ? b in let c_nat ≝ nat_of_bitvector ? c in match c_nat with [ O ⇒ None ? | _ ⇒ let result ≝ b_nat ÷ c_nat in Some ? (bitvector_of_nat n result) let rec mult_aux (m,n:nat) (b:BitVector m) (c:BitVector (S n)) (acc:BitVector (S n)) on b : BitVector (S n) ≝ match b with [ VEmpty ⇒ acc | VCons m' hd tl ⇒ let acc' ≝ if hd then addition_n ? c acc else acc in mult_aux m' n tl (shift_right_1 ?? c false) acc' ]. definition multiplication : ∀n:nat. BitVector n → BitVector n → BitVector (n + n) ≝ λn: nat. match n return λn.BitVector n → BitVector n → BitVector (n + n) with [ O ⇒ λ_.λ_.[[ ]] | S m ⇒ λb, c : BitVector (S m). let c' ≝ pad (S m) (S m) c in mult_aux ?? b (shift_left ?? m c' false) (zero ?) ]. (* Division:  001...000 divided by 000...010 Shift the divisor as far left as possible, 100...000 then try subtracting it at each bit position, shifting left as we go. 001...000 - 100...000 X ⇒ 0 001...000 - 010...000 X ⇒ 0 001...000 - 001...000 Y ⇒ 1 (use subtracted value as new quotient) ... Then pad out the remaining bits at the front 00..001... *) inductive fbs_diff : nat → Type[0] ≝ | fbs_diff' : ∀n,m. fbs_diff (S (n+m)). let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝ match b return λn.λ_. option (fbs_diff n) with [ VEmpty ⇒ None ? | VCons m h t ⇒ if h then Some ? (fbs_diff' O m) else match first_bit_set m t with [ None ⇒ None ? | Some o ⇒ match o return λx.λ_. option (fbs_diff (S x)) with [ fbs_diff' x y ⇒ Some ? (fbs_diff' (S x) y) ] ] ]. let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝ match m with [ O ⇒ 〈[[ ]], q〉 | S m' ⇒ let 〈q',flags〉 ≝ add_with_carries ? q (two_complement_negation ? d) false in let bit ≝ head' … flags in let q'' ≝ if bit then q' else q in let 〈tl, md〉 ≝ divmod_u_aux n m' q'' (shift_right_1 ?? d false) in 〈bit:::tl, md〉 ]. definition divmod_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n) × (BitVector (S n))) ≝ λn: nat. λb, c: BitVector (S n). match first_bit_set ? c with [ None ⇒ None ? | Some fbs' ⇒ match fbs' return λx.λ_.option (BitVector x × (BitVector (S n))) with [ fbs_diff' fbs m ⇒ let 〈d,m〉 ≝ (divmod_u_aux ? (S fbs) b (shift_left ?? fbs c false)) in Some ? 〈switch_bv_plus ??? (pad ?? d), m〉 ] ]. definition division_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝ λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\fst p) ]. definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝ let b_sign_bit ≝ get_index_v ? ? b O ? in let c_sign_bit ≝ get_index_v ? ? c O ? in let b_as_nat ≝ nat_of_bitvector ? b in let c_as_nat ≝ nat_of_bitvector ? c in match c_as_nat with [ O ⇒ None ? | S o ⇒ match b_sign_bit with match b_sign_bit with [ true ⇒ let neg_b ≝ two_complement_negation ? b in match c_sign_bit with [ true ⇒ let temp_b ≝ b_as_nat - (2^p) in match c_sign_bit with [ true ⇒ let temp_c ≝ c_as_nat - (2^p) in Some ? (bitvector_of_nat ? (temp_b ÷ temp_c)) | false ⇒ let result ≝ (temp_b ÷ c_as_nat) + (2^p) in Some ? (bitvector_of_nat ? result) ] (* I was worrying slightly about -2^(n-1), whose negation can't be represented in an n bit signed number.  However, it's negation comes out as 2^(n-1) as an n bit *unsigned* number, so it's fine. *) division_u ? neg_b (two_complement_negation ? c) | false ⇒ match c_sign_bit with [ true ⇒ let temp_c ≝ c_as_nat - (2^p) in let result ≝ (b_as_nat ÷ temp_c) + (2^p) in Some ? (bitvector_of_nat ? result) | false ⇒ Some ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat)) ] match division_u ? neg_b c with [ None ⇒ None ? | Some r ⇒ Some ? (two_complement_negation ? r) ] ] | false ⇒ match c_sign_bit with [ true ⇒ match division_u ? b (two_complement_negation ? c) with [ None ⇒ None ? | Some r ⇒ Some ? (two_complement_negation ? r) ] | false ⇒ division_u ? b c ] ] ]. ]. // qed. definition modulus_u ≝ λn. λb, c: BitVector n. let b_nat ≝ nat_of_bitvector ? b in let c_nat ≝ nat_of_bitvector ? c in match c_nat with [ O ⇒ None ? | _ ⇒ let result ≝ modulus b_nat c_nat in Some ? (bitvector_of_nat n result) ]. definition modulus_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝ λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\snd p) ]. definition modulus_s ≝
• ## src/ASM/BitVector.ma

 r726 definition pad ≝ λm, n: nat. λb: BitVector n. let padding ≝ replicate bool m false in append bool m n padding b. λb: BitVector n. pad_vector ? false m n b. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
• ## src/ASM/Vector.ma

 r726 include "arithmetics/nat.ma". include "utilities/extranat.ma". include "utilities/oldlib/eq.ma". qed. let rec split (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝ definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝ λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with [ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ]. definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝ λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with [ VEmpty ⇒ I | VCons m hd tl ⇒ tl ]. let rec split' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝ match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with [ O ⇒ λv. 〈[[ ]], v〉 | S m' ⇒ λv. match v return λl. λ_: Vector A l. l = S (plus m' n) → (Vector A (S m')) × (Vector A n) with [ VEmpty ⇒ λK. ⊥ | VCons o he tl ⇒ λK. match split A m' n (tl⌈Vector A o ↦ Vector A (m' + n)⌉) with [ pair v1 v2 ⇒ 〈he:::v1, v2〉 ] ] (?: (S (m' + n)) = S (m' + n))]. // [ destruct | lapply (injective_S … K) // ] qed. | S m' ⇒ λv. let 〈l,r〉 ≝ split' A m' n (tail ?? v) in 〈head' ?? v:::l, r〉 ]. (* Prevent undesirable unfolding. *) let rec split (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝ split' A m n v. definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝ (* At some points matita will attempt to reduce reverse with a known vector, which reduces the equality proof for the cast.  Normalising this proof needs to be fast enough to keep matita usable. *) let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝ match n return λn'.∀m.S(n'+m) = n'+S m with [ O ⇒ λm.refl ?? | S n' ⇒ λm. ? ]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed. to be fast enough to keep matita usable, so use plus_n_Sm_fast. *) let rec revapp (A: Type[0]) (n: nat) (m:nat) (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉. < plus_n_O @refl qed. let rec pad_vector (A:Type[0]) (a:A) (n,m:nat) (v:Vector A m) on n : Vector A (n+m) ≝ match n return λn.Vector A (n+m) with [ O ⇒ v | S n' ⇒ a:::(pad_vector A a n' m v) ]. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) qed. (* XXX this is horrible - but useful to ensure that we can normalise in the proof assistant. *) definition switch_bv_plus : ∀A:Type[0]. ∀n,m. Vector A (n+m) → Vector A (m+n) ≝ λA,n,m. match commutative_plus_faster n m with [ refl ⇒ λi.i ]. definition shift_right_1 ≝ λA: Type[0]. λv: Vector A (S n). λa: A. reverse … (shift_left_1 … (reverse … v) a). definition shift_left ≝ let 〈v',dropped〉 ≝ split ? n 1 (switch_bv_plus ? 1 n v) in a:::v'. (*    reverse … (shift_left_1 … (reverse … v) a).*) definition shift_left : ∀A:Type[0]. ∀n,m:nat. Vector A n → A → Vector A n ≝ λA: Type[0]. λn, m: nat. λv: Vector A (S n). λa: A. iterate … (λx. shift_left_1 … x a) v m. match nat_compare n m return λx,y.λ_. Vector A x → A → Vector A x with [ nat_lt _ _ ⇒ λv,a. replicate … a | nat_eq _   ⇒ λv,a. replicate … a | nat_gt d m ⇒ λv,a. let 〈v0,v'〉 ≝ split … v in switch_bv_plus … (v' @@ (replicate … a)) ]. (*    iterate … (λx. shift_left_1 … x a) v m.*) definition shift_right ≝ (* Decidable equality.                                                        *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝ λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with [ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ]. definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝ λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with [ VEmpty ⇒ I | VCons m hd tl ⇒ tl ]. let rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝
• ## src/Clight/AST.ma

 r738 #r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed. definition size_pointer : region → Z ≝ λsp. match sp return λ_.Z with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ]. definition size_pointer : region → nat ≝ λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ]. (* * The intermediate languages are weakly typed, using only three types: lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2). #t1 #t2 cases t1 try *; cases t2 try *; /2/ %2 @nmk #H destruct; qed. #t1 #t2 cases t1 try *; cases t2 try *; /2/ %2 @nmk #H destruct qed. lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2). [ %1 @refl | 2,3: #ty %2 % #H destruct | #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct /2/ | #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct cases E /2/ ] qed. | Init_float32: float → init_data | Init_float64: float → init_data | Init_space: Z → init_data | Init_space: nat → init_data | Init_null: region → init_data | Init_addrof: region → ident → int → init_data.   (*r address of symbol + offset *)
• ## src/Clight/Cexec.ma

 r731 #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed. definition eq_nat_dec : ∀n,m:nat. Sum (n=m) (n≠m). #n #m lapply (refl ? (eqb n m)) cases (eqb n m) in ⊢ (???% → ?) #E [ %1 | %2 ] @(eqb_elim … E) // #_ #H destruct qed. let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝ match t1 return λt'. (t' = t2) + (t' ≠ t2) with match eq_region_dec s s' with [ inl e1 ⇒ match type_eq_dec t t' with [ inl e2 ⇒ match decidable_eq_Z_Type n n' with [ inl e3 ⇒ inl ??? match eq_nat_dec n n' with [ inl e3 ⇒ inl ??? | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
• ## src/Clight/CexecSound.ma

 r708 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r). #v #ty #r cases v; [ | #i | #f | #r1 | #r #b #pc #of ] cases v; [ | #i | #f | #r1 | #r' #b #pc #of ] cases ty; [ 2,11,20,29,38: #sz #sg | 3,12,21,30,39: #sz | 4,13,22,31,40: #r #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ] #H whd in H:(??%?); destruct; [ lapply (eq_spec i zero); elim (eq i zero); [ #e >e @bool_of_val_false //; | #ne @bool_of_val_true /2/; | #ne (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vint i) (Tint sz sg)) normalize #H @H /2/; ] | elim (eq_dec f Fzero); [ #e >e >(Feq_zero_true …) @bool_of_val_false //; | #ne >(Feq_zero_false …) //; @bool_of_val_true /2/; | #ne >(Feq_zero_false …) //; (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vfloat f) (Tfloat sz)) normalize #H @H /2/; ] | @bool_of_val_false // | @bool_of_val_true // | (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vptr r' b pc of) (Tpointer r ty)) normalize #H @H // ] qed.
• ## src/Clight/Csem.ma

 r725 if eq_block b1 b2 then if eq (repr (sizeof ty)) zero then None ? else Some ? (Vint (divu (sub_offset ofs1 ofs2) (repr (sizeof ty)))) else match division_u ? (sub_offset ofs1 ofs2) (repr (sizeof ty)) with [ None ⇒ None ? | Some v ⇒ Some ? (Vint v) ] else None ? | _ ⇒ None ? ] match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (divu n1 n2)) (*        [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)*) [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2) | _ ⇒ None ? ] | _ ⇒ None ? ] match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint(divs n1 n2)) (*         [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)*) [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2) | _ ⇒ None ? ] | _ ⇒ None ? ] match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (modu n1 n2)) (*        [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)*) [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2) | _ ⇒ None ? ] | _ ⇒ None ? ] match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (mods n1 n2)) (*        [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)*) [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2) | _ ⇒ None ? ] | _ ⇒ None ? ]
• ## src/Clight/Csyntax.ma

 r725 | Tfloat: floatsize → type            (**r floating-point types *) | Tpointer: region → type → type      (**r pointer types ([*ty]) *) | Tarray: region → type → Z → type    (**r array types ([ty[len]]) *) | Tarray: region → type → nat → type  (**r array types ([ty[len]]) *) | Tfunction: typelist → type → type   (**r function types *) | Tstruct: ident → fieldlist → type   (**r struct types *) (* * Natural alignment of a type, in bytes. *) (* FIXME: these are old values for 32 bit machines *) let rec alignof (t: type) : Z ≝ match t return λ_.Z (* XXX appears to infer nat otherwise *) with let rec alignof (t: type) : nat ≝ match t with [ Tvoid ⇒ 1 | Tint sz _ ⇒ match sz return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ] | Tfloat sz ⇒ match sz return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ] | Tint sz _ ⇒ match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ] | Tfloat sz ⇒ match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ] | Tpointer _ _ ⇒ 4 | Tarray _ t' n ⇒ alignof t' ] and alignof_fields (f: fieldlist) : Z ≝ and alignof_fields (f: fieldlist) : nat ≝ match f with [ Fnil ⇒ 1 | Fcons id t f' ⇒ Zmax (alignof t) (alignof_fields f') | Fcons id t f' ⇒ max (alignof t) (alignof_fields f') ]. ∀f. alignof_fields f > 0. @fieldlist_ind //; #i #t #fs' #IH lapply (Zmax_r (alignof t) (alignof_fields fs')); @Zlt_to_Zle_to_Zlt //; qed. #i #t #fs' #IH @max_r @IH qed. lemma alignof_pos: ∀t. alignof t > 0. #t elim t; normalize; //; [ 1,2: #z cases z; //; [ 1,2: #z cases z; /2/; | 3,4: #i @alignof_fields_pos ] qed. (* * Size of a type, in bytes. *) let rec sizeof (t: type) : Z ≝ match t return λ_.Z with let rec sizeof (t: type) : nat ≝ match t with [ Tvoid ⇒ 1 | Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ] | Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ] | Tint i _ ⇒ match i with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ] | Tfloat f ⇒ match f with [ F32 ⇒ 4 | F64 ⇒ 8 ] | Tpointer r _ ⇒ size_pointer r | Tarray _ t' n ⇒ sizeof t' * Zmax 1 n | Tarray _ t' n ⇒ sizeof t' * max 1 n | Tfunction _ _ ⇒ 1 | Tstruct _ fld ⇒ align (Zmax 1 (sizeof_struct fld 0)) (alignof t) | Tunion _ fld ⇒ align (Zmax 1 (sizeof_union fld)) (alignof t) | Tstruct _ fld ⇒ align (max 1 (sizeof_struct fld 0)) (alignof t) | Tunion _ fld ⇒ align (max 1 (sizeof_union fld)) (alignof t) | Tcomp_ptr r _ ⇒ size_pointer r ] and sizeof_struct (fld: fieldlist) (pos: Z) on fld : Z ≝ and sizeof_struct (fld: fieldlist) (pos: nat) on fld : nat ≝ match fld with [ Fnil ⇒ pos ] and sizeof_union (fld: fieldlist) : Z ≝ and sizeof_union (fld: fieldlist) : nat ≝ match fld with [ Fnil ⇒ 0 | Fcons id t fld' ⇒ Zmax (sizeof t) (sizeof_union fld') | Fcons id t fld' ⇒ max (sizeof t) (sizeof_union fld') ]. (* TODO: needs some Z_times results Open Local Scope string_scope. *) let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: Z) on fld : res Z ≝ let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: nat) on fld : res nat ≝ match fld with [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
• ## src/RTLabs/RTLabs-sem.ma

 r736 match v with [ Vint i ⇒ ! l ← nth_opt ? (abs (unsigned i)) ls; ! l ← nth_opt ? (nat_of_bitvector ? i) ls; ret ? 〈E0, build_state f fs m l〉 | _ ⇒ Wrong ???
• ## src/common/FrontEndOps.ma

 r727 ]. (* FIXME: switch to alias, or rename, or … *) definition int_eq : int → int → bool ≝ eq. definition ev_notbool : val → option val ≝ λv. match v with ]. definition ev_zero_ext ≝ λnbits: Z. λv: val. definition ev_zero_ext ≝ λnbits: nat. λv: val. match v with [ Vint n ⇒ Some ? (Vint (zero_ext nbits n)) ]. definition ev_sign_ext ≝ λnbits:Z. λv:val. definition ev_sign_ext ≝ λnbits:nat. λv:val. match v with [ Vint i ⇒ Some ? (Vint (sign_ext nbits i)) match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ Some ? (Vint (add n1 n2)) [ Vint n2 ⇒ Some ? (Vint (addition_n ? n1 n2)) | Vptr r b2 p ofs2 ⇒ Some ? (Vptr r b2 p (shift_offset ofs2 n1)) | _ ⇒ None ? ] match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ Some ? (Vint (sub n1 n2)) [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2)) | _ ⇒ None ? ] | Vptr r1 b1 p1 ofs1 ⇒ match v2 with match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ Some ? (Vint (divs n1 n2)) [ Vint n2 ⇒ option_map ?? Vint (division_s ? n1 n2) | _ ⇒ None ? ] | _ ⇒ None ? ]. match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (mods n1 n2)) [ Vint n2 ⇒ option_map ?? Vint (modulus_s ? n1 n2) | _ ⇒ None ? ] match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (divu n1 n2)) [ Vint n2 ⇒ option_map ?? Vint (division_u ? n1 n2) | _ ⇒ None ? ] match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (modu n1 n2)) [ Vint n2 ⇒ option_map ?? Vint (modulus_u ? n1 n2) | _ ⇒ None ? ]
• ## src/common/Globalenvs.ma

 r700 ]. definition size_init_data : init_data → Z ≝ definition size_init_data : init_data → nat ≝ λi_data.match i_data with [ Init_int8 _ ⇒ 1 | Init_float32 _ ⇒ 4 | Init_float64 _ ⇒ 8 | Init_space n ⇒ Zmax n 0 | Init_space n ⇒ max n 0 | Init_null r ⇒ size_pointer r | Init_addrof r _ _ ⇒ size_pointer r].
• ## src/common/Integers.ma

 r700 include "arithmetics/nat.ma". include "utilities/binary/Z.ma". include "utilities/extralib.ma". include "utilities/extranat.ma". include "ASM/BitVector.ma". include "ASM/BitVectorZ.ma". include "ASM/Arithmetic.ma". definition wordsize : nat ≝ 32. (* definition modulus : Z ≝ Z_two_power_nat wordsize. definition half_modulus : Z ≝ modulus / 2. modulus > 0. //; qed. *) (* * Representation of machine integers *) definition int : Type[0] ≝ BitVector wordsize. (* definition intval: int → Z ≝ Z_of_unsigned_bitvector ?. definition intrange: ∀i:int. 0 ≤ (intval i) ∧ (intval i) < modulus. then unsigned n else unsigned n - modulus. *) (* Conversely, [repr] takes a Coq integer and returns the corresponding machine integer.  The argument is treated modulo [modulus]. *) (* definition repr : Z → int ≝ λz. bitvector_of_Z wordsize z. *) definition repr : nat → int ≝ λn. bitvector_of_nat wordsize n. definition zero := repr 0. definition one  := repr 1. definition mone := repr (-1). definition iwordsize := repr (Z_of_nat wordsize). definition mone := subtraction ? zero one. definition iwordsize := repr wordsize. lemma eq_dec: ∀x,y: int. (x = y) + (x ≠ y). definition neg : int → int ≝ two_complement_negation wordsize. let rec zero_ext (n:Z) (x:int) on x : int ≝ repr (modZ (unsigned x) (two_p n)). let rec sign_ext (n:Z) (x:int) on x : int ≝ repr (let p ≝ two_p n in let y ≝ modZ (unsigned x) p in if Zltb y (two_p (n-1)) then y else y - p). definition add ≝ addition_n wordsize. definition sub ≝ subtraction wordsize. (*definition mul ≝ λx,y. \fst (split ? wordsize wordsize (multiplication wordsize x y)).*) definition mul ≝ λx,y. repr ((unsigned x) * (unsigned y)). definition Zdiv_round : Z → Z → Z ≝ λx,y: Z. if Zltb x 0 then if Zltb y 0 then (-x) / (-y) else - ((-x) / y) else if Zltb y 0 then -(x / (-y)) else x / y. definition Zmod_round : Z → Z → Z ≝ λx,y: Z. x - (Zdiv_round x y) * y. definition divs : int → int → int ≝ λx,y:int. repr (Zdiv_round (signed x) (signed y)). definition mods : int → int → int ≝ λx,y:int. repr (Zmod_round (signed x) (signed y)). definition divu : int → int → int ≝ λx,y. repr (unsigned x / unsigned y). definition modu : int → int → int ≝ λx,y. repr (unsigned x \mod unsigned y). (* * For bitwise operations, we need to convert between Coq integers [Z] and their bit-level representations.  Bit-level representations are represented as characteristic functions, that is, functions [f] of type [nat -> bool] such that [f i] is the value of the [i]-th bit of the number.  The values of characteristic functions for [i] greater than 32 are ignored. *) definition Z_shift_add ≝ λb: bool. λx: Z. if b then 2 * x + 1 else 2 * x. definition Z_bin_decomp : Z → bool × Z ≝ λx.match x with [ OZ ⇒ 〈false, OZ〉 | pos p ⇒ match p with [ p1 q ⇒ 〈true, pos q〉 | p0 q ⇒ 〈false, pos q〉 | one ⇒ 〈true, OZ〉 ] | neg p ⇒ match p return λ_.bool × Z with [ p1 q ⇒ 〈true, Zpred (neg q)〉 | p0 q ⇒ 〈false, neg q〉 | one ⇒ 〈true, neg one〉 ] ]. let rec bits_of_Z (n:nat) (x:Z) on n : Z → bool ≝ match n with [ O ⇒ λi:Z. false | S m ⇒ match Z_bin_decomp x with [ pair b y ⇒ let f ≝ bits_of_Z m y in λi:Z. if eqZb i 0 then b else f (Zpred i) ] ]. let rec Z_of_bits (n:nat) (f:Z → bool) on n : Z ≝ match n with [ O ⇒ OZ | S m ⇒ Z_shift_add (f OZ) (Z_of_bits m (λi. f (Zsucc i))) ]. definition mul ≝ λx,y. \snd (split ? wordsize wordsize (multiplication wordsize x y)). definition zero_ext_n : ∀w,n:nat. BitVector w → BitVector w ≝ λw,n. match nat_compare n w return λx,y.λ_. BitVector y → BitVector y with [ nat_lt n' w' ⇒ λi. let 〈h,l〉 ≝ split ? (S w') n' (switch_bv_plus ??? i) in switch_bv_plus ??? (pad ?? l) | _ ⇒ λi.i ]. definition zero_ext : nat → int → int ≝ zero_ext_n wordsize. definition sign_ext_n : ∀w,n:nat. BitVector w → BitVector w ≝ λw,n. match nat_compare n w return λx,y.λ_. BitVector y → BitVector y with [ nat_lt n' w' ⇒ λi. let 〈h,l〉 ≝ split ? (S w') n' (switch_bv_plus ??? i) in switch_bv_plus ??? (pad_vector ? (match l with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ]) ?? l) | _ ⇒ λi.i ]. definition sign_ext : nat → int → int ≝ sign_ext_n wordsize. (* * Bitwise logical ``and'', ``or'' and ``xor'' operations. *) definition bitwise_binop ≝ λf: bool -> bool -> bool. λx,y: int. let fx ≝ bits_of_Z wordsize (unsigned x) in let fy ≝ bits_of_Z wordsize (unsigned y) in repr (Z_of_bits wordsize (λi. f (fx i) (fy i))). definition i_and : int → int → int ≝ conjunction_bv wordsize. (* * Shifts and rotates. *) definition shl : int → int → int ≝ λx,y. let fx ≝ bits_of_Z wordsize (unsigned x) in let vy ≝ unsigned y in repr (Z_of_bits wordsize (λi. fx (i - vy))). definition shru : int → int → int ≝ λx,y. let fx ≝ bits_of_Z wordsize (unsigned x) in let vy ≝ unsigned y in repr (Z_of_bits wordsize (λi. fx (i + vy))). definition shl : int → int → int ≝ λx,y. shift_left ?? (nat_of_bitvector … y) x false. definition shru : int → int → int ≝ λx,y. shift_right ?? (nat_of_bitvector … y) x false. (* * Arithmetic right shift is defined as signed division by a power of two. [shrx] rounds towards zero. *) definition shr : int → int → int ≝ λx,y. repr (signed x / two_p (unsigned y)). definition shr : int → int → int ≝ λx,y. shift_right ?? (nat_of_bitvector … y) x (head' … x). definition shrx : int → int → int ≝ λx,y. divs x (shl one y). match division_s ? x (shl one y) with [ None ⇒ zero | Some i ⇒ i ]. definition shr_carry ≝ λx,y: int. sub (shrx x y) (shr x y). definition rol : int → int → int ≝ λx,y. let fx ≝ bits_of_Z wordsize (unsigned x) in let vy ≝ unsigned y in repr (Z_of_bits wordsize (λi. fx (i - vy \mod Z_of_nat wordsize))). definition ror : int → int → int ≝ λx,y. let fx := bits_of_Z wordsize (unsigned x) in let vy := unsigned y in repr (Z_of_bits wordsize (λi. fx (i + vy \mod Z_of_nat wordsize))). subtraction ? (shrx x y) (shr x y). definition rol : int → int → int ≝ λx,y. rotate_left ?? (nat_of_bitvector ? y) x. definition ror : int → int → int ≝ λx,y. rotate_right ?? (nat_of_bitvector ? y) x. definition rolm ≝ λx,a,m: int. i_and (rol x a) m. *) theorem one_not_zero: one ≠ zero. % #H lapply (refl ? (get_index' ? 31 0 one)) >H in ⊢ (???% → ?) normalize #E destruct % #H @(match eq_dec one zero return λx.match x with [ inl _ ⇒ True | inr _ ⇒ False ] with [ inl _ ⇒ I | inr p ⇒ ?]) normalize cases p #H' @(H' H) qed. Qed. *) (* theorem unsigned_range: ∀i. 0 ≤ unsigned i ∧ unsigned i < modulus. #i @intrange *)
• ## src/common/Mem.ma

 r718 ] ] %2 @nmk *; #Hval #Hlo' #Hhi' #Hal' #Hcl' @(absurd ???) // [ 2: @Hval | 3: @Hnext ] %2 @nmk *; #Hval #Hlo' #Hhi' #Hal' #Hcl' [ @(absurd ? Hcl' Hcl) | @(absurd ? Hal' Hal) | @(absurd ? Hhi' Hhi) | @(absurd ? Hlo' Hlo) | @(absurd ? Hval Hnext) ] qed.
• ## src/common/Values.ma

 r718 include "common/Errors.ma". include "ASM/Vector.ma". include "ASM/BitVectorZ.ma". include "basics/logic.ma". include "utilities/binary/Z.ma". (* To define pointers we need a few details about the memory model. definition eq_offset ≝ λx,y. eqZb (offv x) (offv y). definition shift_offset : offset → int → offset ≝ λo,i. mk_offset (offv o + signed i). λo,i. mk_offset (offv o + Z_of_signed_bitvector ? i). definition neg_shift_offset : offset → int → offset ≝ λo,i. mk_offset (offv o - signed i). λo,i. mk_offset (offv o - Z_of_signed_bitvector ? i). definition sub_offset : offset → offset → int ≝ λx,y. repr (offv x - offv y). λx,y. bitvector_of_Z ? (offv x - offv y). definition zero_offset ≝ mk_offset OZ. definition lt_offset : offset → offset → bool ≝ ]. definition zero_ext ≝ λnbits: Z. λv: val. definition zero_ext ≝ λnbits: nat. λv: val. match v with [ Vint n ⇒ Vint (zero_ext nbits n) ]. definition sign_ext ≝ λnbits:Z. λv:val. definition sign_ext ≝ λnbits:nat. λv:val. match v with [ Vint i ⇒ Vint (sign_ext nbits i) match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ Vint (add n1 n2) [ Vint n2 ⇒ Vint (addition_n ? n1 n2) | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1) | _ ⇒ Vundef ] match v1 with [ Vint n1 ⇒ match v2 with [ Vint n2 ⇒ Vint (sub n1 n2) [ Vint n2 ⇒ Vint (subtraction ? n1 n2) | _ ⇒ Vundef ] | Vptr r1 b1 p1 ofs1 ⇒ match v2 with qed. (* Lemma zero_ext_lessdef: forall n v1 v2, lessdef v1 v2 -> lessdef (zero_ext n v1) (zero_ext n v2). Proof. intros; inv H; simpl; auto. Qed. *) lemma zero_ext_lessdef: ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (zero_ext n v1) (zero_ext n v2). #n #v1 #v2 #H inversion H // #v #E1 #E2 destruct // qed. lemma sign_ext_lessdef: ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2).
• ## src/utilities/Coqlib.ma

 r697 include "utilities/extralib.ma". include "ASM/Util.ma". (* (*naxiom align : Z → Z → Z.*) definition align ≝ λn: Z. λamount: Z. ((n + amount - 1) / amount) * amount. definition align : nat → nat → nat ≝ λn: nat. λamount: nat. ((minus (n + amount) 1) ÷ amount) * amount. (* Lemma align_le: forall x y, y > 0 -> x <= align x y.
Note: See TracChangeset for help on using the changeset viewer.