Changeset 744


Ignore:
Timestamp:
Apr 7, 2011, 6:53:59 PM (9 years ago)
Author:
campbell
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:
1 added
15 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r724 r744  
    149149  λb, c: BitVector n.
    150150    addition_n n b (two_complement_negation n c).
    151    
    152 definition multiplication ≝
    153   λn: nat.
    154   λb, c: BitVector n.
    155     let b_nat ≝ nat_of_bitvector ? b in
    156     let c_nat ≝ nat_of_bitvector ? c in
    157     let result ≝ b_nat * c_nat in
    158       bitvector_of_nat (n + n) result.
    159      
    160 definition division_u ≝
    161   λn: nat.
    162   λb, c: BitVector n.
    163     let b_nat ≝ nat_of_bitvector ? b in
    164     let c_nat ≝ nat_of_bitvector ? c in
    165     match c_nat with
    166     [ O ⇒ None ?
    167     | _ ⇒
    168       let result ≝ b_nat ÷ c_nat in
    169         Some ? (bitvector_of_nat n result)
     151
     152let rec mult_aux (m,n:nat) (b:BitVector m) (c:BitVector (S n)) (acc:BitVector (S n)) on b : BitVector (S n) ≝
     153match b with
     154[ VEmpty ⇒ acc
     155| VCons m' hd tl ⇒
     156    let acc' ≝ if hd then addition_n ? c acc else acc in
     157    mult_aux m' n tl (shift_right_1 ?? c false) acc'
     158].
     159
     160definition multiplication : ∀n:nat. BitVector n → BitVector n → BitVector (n + n) ≝
     161  λn: nat.
     162  match n return λn.BitVector n → BitVector n → BitVector (n + n) with
     163  [ O ⇒ λ_.λ_.[[ ]]
     164  | S m ⇒
     165    λb, c : BitVector (S m).
     166    let c' ≝ pad (S m) (S m) c in
     167      mult_aux ?? b (shift_left ?? m c' false) (zero ?)
     168  ].
     169
     170(* Division:  001...000 divided by 000...010
     171     Shift the divisor as far left as possible,
     172                                  100...000
     173      then try subtracting it at each
     174      bit position, shifting left as we go.
     175              001...000 - 100...000 X ⇒ 0
     176              001...000 - 010...000 X ⇒ 0
     177              001...000 - 001...000 Y ⇒ 1 (use subtracted value as new quotient)
     178              ...
     179      Then pad out the remaining bits at the front
     180         00..001...
     181*)
     182inductive fbs_diff : nat → Type[0] ≝
     183| fbs_diff' : ∀n,m. fbs_diff (S (n+m)).
     184
     185let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝
     186match b return λn.λ_. option (fbs_diff n) with
     187[ VEmpty ⇒ None ?
     188| VCons m h t ⇒
     189    if h then Some ? (fbs_diff' O m)
     190    else match first_bit_set m t with
     191         [ None ⇒ None ?
     192         | Some o ⇒ match o return λx.λ_. option (fbs_diff (S x)) with [ fbs_diff' x y ⇒ Some ? (fbs_diff' (S x) y) ]
     193         ]
     194].
     195
     196let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝
     197match m with
     198[ O ⇒ 〈[[ ]], q〉
     199| S m' ⇒
     200    let 〈q',flags〉 ≝ add_with_carries ? q (two_complement_negation ? d) false in
     201    let bit ≝ head' … flags in
     202    let q'' ≝ if bit then q' else q in
     203    let 〈tl, md〉 ≝ divmod_u_aux n m' q'' (shift_right_1 ?? d false) in
     204    〈bit:::tl, md〉
     205].
     206
     207definition divmod_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n) × (BitVector (S n))) ≝
     208  λn: nat.
     209  λb, c: BitVector (S n).
     210
     211    match first_bit_set ? c with
     212    [ None ⇒ None ?
     213    | Some fbs' ⇒
     214        match fbs' return λx.λ_.option (BitVector x × (BitVector (S n))) with [ fbs_diff' fbs m ⇒
     215          let 〈d,m〉 ≝ (divmod_u_aux ? (S fbs) b (shift_left ?? fbs c false)) in
     216          Some ? 〈switch_bv_plus ??? (pad ?? d), m〉
     217        ]
    170218    ].
     219
     220definition division_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
     221λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\fst p) ].
    171222     
    172223definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
     
    177228        let b_sign_bit ≝ get_index_v ? ? b O ? in
    178229        let c_sign_bit ≝ get_index_v ? ? c O ? in
    179         let b_as_nat ≝ nat_of_bitvector ? b in
    180         let c_as_nat ≝ nat_of_bitvector ? c in
    181         match c_as_nat with
    182         [ O ⇒ None ?
    183         | S o ⇒
    184           match b_sign_bit with
     230        match b_sign_bit with
     231        [ true ⇒
     232          let neg_b ≝ two_complement_negation ? b in
     233          match c_sign_bit with
    185234          [ true ⇒
    186             let temp_b ≝ b_as_nat - (2^p) in
    187             match c_sign_bit with
    188             [ true ⇒
    189               let temp_c ≝ c_as_nat - (2^p) in
    190                 Some ? (bitvector_of_nat ? (temp_b ÷ temp_c))
    191             | false ⇒
    192               let result ≝ (temp_b ÷ c_as_nat) + (2^p) in
    193                 Some ? (bitvector_of_nat ? result)
    194             ]
     235              (* I was worrying slightly about -2^(n-1), whose negation can't
     236                 be represented in an n bit signed number.  However, it's
     237                 negation comes out as 2^(n-1) as an n bit *unsigned* number,
     238                 so it's fine. *)
     239              division_u ? neg_b (two_complement_negation ? c)
    195240          | false ⇒
    196             match c_sign_bit with
    197             [ true ⇒
    198               let temp_c ≝ c_as_nat - (2^p) in
    199               let result ≝ (b_as_nat ÷ temp_c) + (2^p) in
    200                 Some ? (bitvector_of_nat ? result)
    201             | false ⇒ Some ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat))
    202             ]
     241              match division_u ? neg_b c with
     242              [ None ⇒ None ?
     243              | Some r ⇒ Some ? (two_complement_negation ? r)
     244              ]
     245          ]
     246        | false ⇒
     247          match c_sign_bit with
     248          [ true ⇒
     249              match division_u ? b (two_complement_negation ? c) with
     250              [ None ⇒ None ?
     251              | Some r ⇒ Some ? (two_complement_negation ? r)
     252              ]
     253          | false ⇒ division_u ? b c
    203254          ]
    204255        ]
    205     ].
     256   ].
    206257    //
    207258qed.
    208259
    209 definition modulus_u ≝
    210   λn.
    211   λb, c: BitVector n.
    212     let b_nat ≝ nat_of_bitvector ? b in
    213     let c_nat ≝ nat_of_bitvector ? c in
    214     match c_nat with
    215     [ O ⇒ None ?
    216     | _ ⇒
    217       let result ≝ modulus b_nat c_nat in
    218       Some ? (bitvector_of_nat n result)
    219     ].
     260definition modulus_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
     261λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\snd p) ].
    220262           
    221263definition modulus_s ≝
  • src/ASM/BitVector.ma

    r726 r744  
    4040definition pad ≝
    4141  λm, n: nat.
    42   λb: BitVector n.
    43     let padding ≝ replicate bool m false in
    44       append bool m n padding b.
     42  λb: BitVector n. pad_vector ? false m n b.
    4543     
    4644(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • src/ASM/Vector.ma

    r726 r744  
    1212include "arithmetics/nat.ma".
    1313
     14include "utilities/extranat.ma".
    1415include "utilities/oldlib/eq.ma".
    1516
     
    152153qed.
    153154
    154 let rec split (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
     155definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝
     156λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with
     157[ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ].
     158
     159definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝
     160λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with
     161[ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].
     162
     163let rec split' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
    155164 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
    156165  [ O ⇒ λv. 〈[[ ]], v〉
    157   | S m' ⇒ λv.
    158     match v return λl. λ_: Vector A l. l = S (plus m' n) → (Vector A (S m')) × (Vector A n) with
    159       [ VEmpty ⇒ λK. ⊥
    160       | VCons o he tl ⇒ λK.
    161         match split A m' n (tl⌈Vector A o ↦ Vector A (m' + n)⌉) with
    162         [ pair v1 v2 ⇒ 〈he:::v1, v2〉
    163         ]
    164       ] (?: (S (m' + n)) = S (m' + n))].
    165       //
    166       [ destruct
    167       | lapply (injective_S … K)
    168         //
    169       ]
    170 qed.
     166  | S m' ⇒ λv. let 〈l,r〉 ≝ split' A m' n (tail ?? v) in 〈head' ?? v:::l, r〉
     167  ].
     168(* Prevent undesirable unfolding. *)
     169let rec split (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝
     170 split' A m n v.
     171
    171172
    172173definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
     
    329330(* At some points matita will attempt to reduce reverse with a known vector,
    330331   which reduces the equality proof for the cast.  Normalising this proof needs
    331    to be fast enough to keep matita usable. *)
    332 let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝
    333 match n return λn'.∀m.S(n'+m) = n'+S m with
    334 [ O ⇒ λm.refl ??
    335 | S n' ⇒ λm. ?
    336 ]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed.
     332   to be fast enough to keep matita usable, so use plus_n_Sm_fast. *)
    337333
    338334let rec revapp (A: Type[0]) (n: nat) (m:nat)
     
    347343  (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉.
    348344< plus_n_O @refl qed.
     345
     346let rec pad_vector (A:Type[0]) (a:A) (n,m:nat) (v:Vector A m) on n : Vector A (n+m) ≝
     347match n return λn.Vector A (n+m) with
     348[ O ⇒ v
     349| S n' ⇒ a:::(pad_vector A a n' m v)
     350].
    349351
    350352(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    404406qed.
    405407
     408
     409(* XXX this is horrible - but useful to ensure that we can normalise in the proof assistant. *)
     410definition switch_bv_plus : ∀A:Type[0]. ∀n,m. Vector A (n+m) → Vector A (m+n) ≝
     411λA,n,m. match commutative_plus_faster n m with [ refl ⇒ λi.i ].
     412
    406413definition shift_right_1 ≝
    407414  λA: Type[0].
     
    409416  λv: Vector A (S n).
    410417  λa: A.
    411     reverse … (shift_left_1 … (reverse … v) a).
    412    
    413 definition shift_left ≝
     418    let 〈v',dropped〉 ≝ split ? n 1 (switch_bv_plus ? 1 n v) in a:::v'.
     419(*    reverse … (shift_left_1 … (reverse … v) a).*)
     420
     421definition shift_left : ∀A:Type[0]. ∀n,m:nat. Vector A n → A → Vector A n ≝
    414422  λA: Type[0].
    415423  λn, m: nat.
    416   λv: Vector A (S n).
    417   λa: A.
    418     iterate … (λx. shift_left_1 … x a) v m.
     424    match nat_compare n m return λx,y.λ_. Vector A x → A → Vector A x with
     425    [ nat_lt _ _ ⇒ λv,a. replicate … a
     426    | nat_eq _   ⇒ λv,a. replicate … a
     427    | nat_gt d m ⇒ λv,a. let 〈v0,v'〉 ≝ split … v in switch_bv_plus … (v' @@ (replicate … a))
     428    ].
     429
     430(*    iterate … (λx. shift_left_1 … x a) v m.*)
    419431   
    420432definition shift_right ≝
     
    428440(* Decidable equality.                                                        *)
    429441(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    430 
    431 definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝
    432 λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with
    433 [ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ].
    434 
    435 definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝
    436 λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with
    437 [ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].
    438442
    439443let 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 r744  
    7070#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.
    7171
    72 definition size_pointer : region → Z
    73 λsp. match sp return λ_.Z with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
     72definition size_pointer : region → nat
     73λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
    7474
    7575(* * The intermediate languages are weakly typed, using only three types:
     
    9090
    9191lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
    92 #t1 #t2 cases t1 try *; cases t2 try *; /2/ %2 @nmk #H destruct; qed.
     92#t1 #t2 cases t1 try *; cases t2 try *; /2/ %2 @nmk #H destruct qed.
    9393
    9494lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
     
    9696[ %1 @refl
    9797| 2,3: #ty %2 % #H destruct
    98 | #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct /2/
     98| #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct cases E /2/
    9999]
    100100qed.
     
    139139  | Init_float32: float → init_data
    140140  | Init_float64: float → init_data
    141   | Init_space: Z → init_data
     141  | Init_space: nat → init_data
    142142  | Init_null: region → init_data
    143143  | Init_addrof: region → ident → int → init_data.   (*r address of symbol + offset *)
  • src/Clight/Cexec.ma

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

    r708 r744  
    66 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
    77#v #ty #r
    8 cases v; [ | #i | #f | #r1 | #r #b #pc #of ]
     8cases v; [ | #i | #f | #r1 | #r' #b #pc #of ]
    99cases 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 ]
    1010#H whd in H:(??%?); destruct;
    1111[ lapply (eq_spec i zero); elim (eq i zero);
    1212  [ #e >e @bool_of_val_false //;
    13   | #ne @bool_of_val_true /2/;
     13  | #ne (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vint i) (Tint sz sg)) normalize #H @H /2/;
    1414  ]
    1515| elim (eq_dec f Fzero);
    1616  [ #e >e >(Feq_zero_true …) @bool_of_val_false //;
    17   | #ne >(Feq_zero_false …) //; @bool_of_val_true /2/;
     17  | #ne >(Feq_zero_false …) //; (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vfloat f) (Tfloat sz)) normalize #H @H /2/;
    1818  ]
    1919| @bool_of_val_false //
    20 | @bool_of_val_true //
     20| (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vptr r' b pc of) (Tpointer r ty)) normalize #H @H //
    2121] qed.
    2222
  • src/Clight/Csem.ma

    r725 r744  
    170170          if eq_block b1 b2 then
    171171            if eq (repr (sizeof ty)) zero then None ?
    172             else Some ? (Vint (divu (sub_offset ofs1 ofs2) (repr (sizeof ty))))
     172            else match division_u ? (sub_offset ofs1 ofs2) (repr (sizeof ty)) with
     173                 [ None ⇒ None ?
     174                 | Some v ⇒ Some ? (Vint v)
     175                 ]
    173176          else None ?
    174177        | _ ⇒ None ? ]
     
    202205      match v1 with
    203206      [ Vint n1 ⇒ match v2 with
    204         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (divu n1 n2))
    205 (*        [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)*)
     207        [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)
    206208        | _ ⇒ None ? ]
    207209      | _ ⇒ None ? ]
     
    209211      match v1 with
    210212       [ Vint n1 ⇒ match v2 with
    211          [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint(divs n1 n2))
    212 (*         [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)*)
     213         [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)
    213214         | _ ⇒ None ? ]
    214215      | _ ⇒ None ? ]
     
    228229      match v1 with
    229230      [ Vint n1 ⇒ match v2 with
    230         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (modu n1 n2))
    231 (*        [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)*)
     231        [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)
    232232        | _ ⇒ None ? ]
    233233      | _ ⇒ None ? ]
     
    235235      match v1 with
    236236      [ Vint n1 ⇒ match v2 with
    237         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (mods n1 n2))
    238 (*        [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)*)
     237        [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)
    239238        | _ ⇒ None ? ]
    240239      | _ ⇒ None ? ]
  • src/Clight/Csyntax.ma

    r725 r744  
    8888  | Tfloat: floatsize → type            (**r floating-point types *)
    8989  | Tpointer: region → type → type      (**r pointer types ([*ty]) *)
    90   | Tarray: region → type → Z → type    (**r array types ([ty[len]]) *)
     90  | Tarray: region → type → nat → type  (**r array types ([ty[len]]) *)
    9191  | Tfunction: typelist → type → type   (**r function types *)
    9292  | Tstruct: ident → fieldlist → type   (**r struct types *)
     
    363363(* * Natural alignment of a type, in bytes. *)
    364364(* FIXME: these are old values for 32 bit machines *)
    365 let rec alignof (t: type) : Z
    366   match t return λ_.Z (* XXX appears to infer nat otherwise *) with
     365let rec alignof (t: type) : nat
     366  match t with
    367367  [ Tvoid ⇒ 1
    368   | Tint sz _ ⇒ match sz return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    369   | Tfloat sz ⇒ match sz return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
     368  | Tint sz _ ⇒ match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
     369  | Tfloat sz ⇒ match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    370370  | Tpointer _ _ ⇒ 4
    371371  | Tarray _ t' n ⇒ alignof t'
     
    376376  ]
    377377
    378 and alignof_fields (f: fieldlist) : Z
     378and alignof_fields (f: fieldlist) : nat
    379379  match f with
    380380  [ Fnil ⇒ 1
    381   | Fcons id t f' ⇒ Zmax (alignof t) (alignof_fields f')
     381  | Fcons id t f' ⇒ max (alignof t) (alignof_fields f')
    382382  ].
    383383
     
    436436  ∀f. alignof_fields f > 0.
    437437@fieldlist_ind //;
    438 #i #t #fs' #IH lapply (Zmax_r (alignof t) (alignof_fields fs'));
    439 @Zlt_to_Zle_to_Zlt //; qed.
     438#i #t #fs' #IH @max_r @IH qed.
    440439
    441440lemma alignof_pos:
    442441  ∀t. alignof t > 0.
    443442#t elim t; normalize; //;
    444 [ 1,2: #z cases z; //;
     443[ 1,2: #z cases z; /2/;
    445444| 3,4: #i @alignof_fields_pos
    446445] qed.
     
    448447(* * Size of a type, in bytes. *)
    449448
    450 let rec sizeof (t: type) : Z
    451   match t return λ_.Z with
     449let rec sizeof (t: type) : nat
     450  match t with
    452451  [ Tvoid ⇒ 1
    453   | Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    454   | Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
     452  | Tint i _ ⇒ match i with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
     453  | Tfloat f ⇒ match f with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    455454  | Tpointer r _ ⇒ size_pointer r
    456   | Tarray _ t' n ⇒ sizeof t' * Zmax 1 n
     455  | Tarray _ t' n ⇒ sizeof t' * max 1 n
    457456  | Tfunction _ _ ⇒ 1
    458   | Tstruct _ fld ⇒ align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
    459   | Tunion _ fld ⇒ align (Zmax 1 (sizeof_union fld)) (alignof t)
     457  | Tstruct _ fld ⇒ align (max 1 (sizeof_struct fld 0)) (alignof t)
     458  | Tunion _ fld ⇒ align (max 1 (sizeof_union fld)) (alignof t)
    460459  | Tcomp_ptr r _ ⇒ size_pointer r
    461460  ]
    462461
    463 and sizeof_struct (fld: fieldlist) (pos: Z) on fld : Z
     462and sizeof_struct (fld: fieldlist) (pos: nat) on fld : nat
    464463  match fld with
    465464  [ Fnil ⇒ pos
     
    467466  ]
    468467
    469 and sizeof_union (fld: fieldlist) : Z
     468and sizeof_union (fld: fieldlist) : nat
    470469  match fld with
    471470  [ Fnil ⇒ 0
    472   | Fcons id t fld' ⇒ Zmax (sizeof t) (sizeof_union fld')
     471  | Fcons id t fld' ⇒ max (sizeof t) (sizeof_union fld')
    473472  ].
    474473(* TODO: needs some Z_times results
     
    518517Open Local Scope string_scope.
    519518*)
    520 let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)
    521                               on fld : res Z
     519let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: nat)
     520                              on fld : res nat
    522521  match fld with
    523522  [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
  • src/RTLabs/RTLabs-sem.ma

    r736 r744  
    182182      match v with
    183183      [ Vint i ⇒
    184           ! l ← nth_opt ? (abs (unsigned i)) ls;
     184          ! l ← nth_opt ? (nat_of_bitvector ? i) ls;
    185185          ret ? 〈E0, build_state f fs m l〉
    186186      | _ ⇒ Wrong ???
  • src/common/FrontEndOps.ma

    r727 r744  
    171171  ].
    172172 
    173 (* FIXME: switch to alias, or rename, or … *)
    174 definition int_eq : int → int → bool ≝ eq.
    175173definition ev_notbool : val → option val ≝ λv.
    176174  match v with
     
    181179  ].
    182180
    183 definition ev_zero_ext ≝ λnbits: Z. λv: val.
     181definition ev_zero_ext ≝ λnbits: nat. λv: val.
    184182  match v with
    185183  [ Vint n ⇒ Some ? (Vint (zero_ext nbits n))
     
    187185  ].
    188186
    189 definition ev_sign_ext ≝ λnbits:Z. λv:val.
     187definition ev_sign_ext ≝ λnbits:nat. λv:val.
    190188  match v with
    191189  [ Vint i ⇒ Some ? (Vint (sign_ext nbits i))
     
    203201  match v1 with
    204202  [ Vint n1 ⇒ match v2 with
    205     [ Vint n2 ⇒ Some ? (Vint (add n1 n2))
     203    [ Vint n2 ⇒ Some ? (Vint (addition_n ? n1 n2))
    206204    | Vptr r b2 p ofs2 ⇒ Some ? (Vptr r b2 p (shift_offset ofs2 n1))
    207205    | _ ⇒ None ? ]
     
    214212  match v1 with
    215213  [ Vint n1 ⇒ match v2 with
    216     [ Vint n2 ⇒ Some ? (Vint (sub n1 n2))
     214    [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2))
    217215    | _ ⇒ None ? ]
    218216  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     
    234232  match v1 with
    235233  [ Vint n1 ⇒ match v2 with
    236     [ Vint n2 ⇒ Some ? (Vint (divs n1 n2))
     234    [ Vint n2 ⇒ option_map ?? Vint (division_s ? n1 n2)
    237235    | _ ⇒ None ? ]
    238236  | _ ⇒ None ? ].
     
    241239  match v1 with
    242240  [ Vint n1 ⇒ match v2 with
    243     [ Vint n2 ⇒
    244        if eq n2 zero then None ? else Some ? (Vint (mods n1 n2))
     241    [ Vint n2 ⇒ option_map ?? Vint (modulus_s ? n1 n2)
    245242    | _ ⇒ None ?
    246243    ]
     
    251248  match v1 with
    252249  [ Vint n1 ⇒ match v2 with
    253     [ Vint n2 ⇒
    254         if eq n2 zero then None ? else Some ? (Vint (divu n1 n2))
     250    [ Vint n2 ⇒ option_map ?? Vint (division_u ? n1 n2)
    255251    | _ ⇒ None ?
    256252    ]
     
    261257  match v1 with
    262258  [ Vint n1 ⇒ match v2 with
    263     [ Vint n2 ⇒
    264       if eq n2 zero then None ? else Some ? (Vint (modu n1 n2))
     259    [ Vint n2 ⇒ option_map ?? Vint (modulus_u ? n1 n2)
    265260    | _ ⇒ None ?
    266261    ]
  • src/common/Globalenvs.ma

    r700 r744  
    424424  ].
    425425
    426 definition size_init_data : init_data → Z
     426definition size_init_data : init_data → nat
    427427 λi_data.match i_data with
    428428  [ Init_int8 _ ⇒ 1
     
    431431  | Init_float32 _ ⇒ 4
    432432  | Init_float64 _ ⇒ 8
    433   | Init_space n ⇒ Zmax n 0
     433  | Init_space n ⇒ max n 0
    434434  | Init_null r ⇒ size_pointer r
    435435  | Init_addrof r _ _ ⇒ size_pointer r].
  • src/common/Integers.ma

    r700 r744  
    1717
    1818include "arithmetics/nat.ma".
    19 include "utilities/binary/Z.ma".
    20 include "utilities/extralib.ma".
     19include "utilities/extranat.ma".
    2120
    2221include "ASM/BitVector.ma".
    23 include "ASM/BitVectorZ.ma".
    2422include "ASM/Arithmetic.ma".
    2523
     
    6866
    6967definition wordsize : nat ≝ 32.
     68(*
    7069definition modulus : Z ≝ Z_two_power_nat wordsize.
    7170definition half_modulus : Z ≝ modulus / 2.
     
    8584  modulus > 0.
    8685//; qed.
    87 
     86*)
    8887(* * Representation of machine integers *)
    8988
     
    9392
    9493definition int : Type[0] ≝ BitVector wordsize.
    95 
     94(*
    9695definition intval: int → Z ≝ Z_of_unsigned_bitvector ?.
    9796definition intrange: ∀i:int. 0 ≤ (intval i) ∧ (intval i) < modulus.
     
    111110  then unsigned n
    112111  else unsigned n - modulus.
    113 
     112*)
    114113(* Conversely, [repr] takes a Coq integer and returns the corresponding
    115114  machine integer.  The argument is treated modulo [modulus]. *)
    116 
     115(*
    117116definition repr : Z → int ≝ λz. bitvector_of_Z wordsize z.
     117*)
     118definition repr : nat → int ≝ λn. bitvector_of_nat wordsize n.
    118119
    119120definition zero := repr 0.
    120121definition one  := repr 1.
    121 definition mone := repr (-1).
    122 definition iwordsize := repr (Z_of_nat wordsize).
     122definition mone := subtraction ? zero one.
     123definition iwordsize := repr wordsize.
    123124
    124125lemma eq_dec: ∀x,y: int. (x = y) + (x ≠ y).
     
    135136
    136137definition neg : int → int ≝ two_complement_negation wordsize.
    137 
    138 let rec zero_ext (n:Z) (x:int) on x : int ≝
    139   repr (modZ (unsigned x) (two_p n)).
    140 let rec sign_ext (n:Z) (x:int) on x : int ≝
    141   repr (let p ≝ two_p n in
    142         let y ≝ modZ (unsigned x) p in
    143         if Zltb y (two_p (n-1)) then y else y - p).
    144 
    145 definition add ≝ addition_n wordsize.
    146 definition sub ≝ subtraction wordsize.
    147 (*definition mul ≝ λx,y. \fst (split ? wordsize wordsize (multiplication wordsize x y)).*)
    148 definition mul ≝ λx,y. repr ((unsigned x) * (unsigned y)).
    149 definition Zdiv_round : Z → Z → Z ≝ λx,y: Z.
    150   if Zltb x 0 then
    151     if Zltb y 0 then (-x) / (-y) else - ((-x) / y)
    152   else
    153     if Zltb y 0 then -(x / (-y)) else x / y.
    154 
    155 definition Zmod_round : Z → Z → Z ≝ λx,y: Z.
    156   x - (Zdiv_round x y) * y.
    157 
    158 definition divs : int → int → int ≝ λx,y:int.
    159   repr (Zdiv_round (signed x) (signed y)).
    160 definition mods : int → int → int ≝ λx,y:int.
    161   repr (Zmod_round (signed x) (signed y)).
    162 definition divu : int → int → int ≝ λx,y.
    163   repr (unsigned x / unsigned y).
    164 definition modu : int → int → int ≝ λx,y.
    165   repr (unsigned x \mod unsigned y).
    166 
    167 (* * For bitwise operations, we need to convert between Coq integers [Z]
    168   and their bit-level representations.  Bit-level representations are
    169   represented as characteristic functions, that is, functions [f]
    170   of type [nat -> bool] such that [f i] is the value of the [i]-th bit
    171   of the number.  The values of characteristic functions for [i] greater
    172   than 32 are ignored. *)
    173 
    174 definition Z_shift_add ≝ λb: bool. λx: Z.
    175   if b then 2 * x + 1 else 2 * x.
    176 
    177 definition Z_bin_decomp : Z → bool × Z ≝
    178 λx.match x with
    179 [ OZ ⇒ 〈false, OZ〉
    180 | pos p ⇒
    181   match p with
    182   [ p1 q ⇒ 〈true, pos q〉
    183   | p0 q ⇒ 〈false, pos q〉
    184   | one ⇒ 〈true, OZ〉
    185   ]
    186 | neg p ⇒
    187   match p return λ_.bool × Z with
    188   [ p1 q ⇒ 〈true, Zpred (neg q)〉
    189   | p0 q ⇒ 〈false, neg q〉
    190   | one ⇒ 〈true, neg one〉
    191   ]
    192 ].
    193 
    194 let rec bits_of_Z (n:nat) (x:Z) on n : Z → bool ≝
    195 match n with
    196 [ O ⇒ λi:Z. false
    197 | S m ⇒
    198     match Z_bin_decomp x with [ pair b y ⇒
    199       let f ≝ bits_of_Z m y in
    200       λi:Z. if eqZb i 0 then b else f (Zpred i) ]
    201 ].
    202 
    203 let rec Z_of_bits (n:nat) (f:Z → bool) on n : Z ≝
    204 match n with
    205 [ O ⇒ OZ
    206 | S m ⇒ Z_shift_add (f OZ) (Z_of_bits m (λi. f (Zsucc i)))
    207 ].
     138definition mul ≝ λx,y. \snd (split ? wordsize wordsize (multiplication wordsize x y)).
     139
     140definition zero_ext_n : ∀w,n:nat. BitVector w → BitVector w ≝
     141λw,n.
     142  match nat_compare n w return λx,y.λ_. BitVector y → BitVector y with
     143  [ nat_lt n' w' ⇒ λi.
     144      let 〈h,l〉 ≝ split ? (S w') n' (switch_bv_plus ??? i) in
     145      switch_bv_plus ??? (pad ?? l)
     146  | _ ⇒ λi.i
     147  ].
     148
     149definition zero_ext : nat → int → int ≝ zero_ext_n wordsize.
     150
     151definition sign_ext_n : ∀w,n:nat. BitVector w → BitVector w ≝
     152λw,n.
     153  match nat_compare n w return λx,y.λ_. BitVector y → BitVector y with
     154  [ nat_lt n' w' ⇒ λi.
     155      let 〈h,l〉 ≝ split ? (S w') n' (switch_bv_plus ??? i) in
     156      switch_bv_plus ??? (pad_vector ? (match l with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ]) ?? l)
     157  | _ ⇒ λi.i
     158  ].
     159
     160definition sign_ext : nat → int → int ≝ sign_ext_n wordsize.
    208161
    209162(* * Bitwise logical ``and'', ``or'' and ``xor'' operations. *)
    210163
    211 definition bitwise_binop ≝ λf: bool -> bool -> bool. λx,y: int.
    212   let fx ≝ bits_of_Z wordsize (unsigned x) in
    213   let fy ≝ bits_of_Z wordsize (unsigned y) in
    214   repr (Z_of_bits wordsize (λi. f (fx i) (fy i))).
    215164
    216165definition i_and : int → int → int ≝ conjunction_bv wordsize.
     
    222171(* * Shifts and rotates. *)
    223172
    224 definition shl : int → int → int ≝ λx,y.
    225   let fx ≝ bits_of_Z wordsize (unsigned x) in
    226   let vy ≝ unsigned y in
    227   repr (Z_of_bits wordsize (λi. fx (i - vy))).
    228 
    229 definition shru : int → int → int ≝ λx,y.
    230   let fx ≝ bits_of_Z wordsize (unsigned x) in
    231   let vy ≝ unsigned y in
    232   repr (Z_of_bits wordsize (λi. fx (i + vy))).
     173definition shl : int → int → int ≝ λx,y. shift_left ?? (nat_of_bitvector … y) x false.
     174definition shru : int → int → int ≝ λx,y. shift_right ?? (nat_of_bitvector … y) x false.
    233175
    234176(* * Arithmetic right shift is defined as signed division by a power of two.
     
    237179  [shrx] rounds towards zero. *)
    238180
    239 definition shr : int → int → int ≝ λx,y.
    240   repr (signed x / two_p (unsigned y)).
    241 
     181definition shr : int → int → int ≝ λx,y. shift_right ?? (nat_of_bitvector … y) x (head' … x).
    242182definition shrx : int → int → int ≝ λx,y.
    243   divs x (shl one y).
     183  match division_s ? x (shl one y) with [ None ⇒ zero | Some i ⇒ i ].
    244184
    245185definition shr_carry ≝ λx,y: int.
    246   sub (shrx x y) (shr x y).
    247 
    248 definition rol : int → int → int ≝ λx,y.
    249   let fx ≝ bits_of_Z wordsize (unsigned x) in
    250   let vy ≝ unsigned y in
    251   repr (Z_of_bits wordsize
    252          (λi. fx (i - vy \mod Z_of_nat wordsize))).
    253 
    254 definition ror : int → int → int ≝ λx,y.
    255   let fx := bits_of_Z wordsize (unsigned x) in
    256   let vy := unsigned y in
    257   repr (Z_of_bits wordsize
    258          (λi. fx (i + vy \mod Z_of_nat wordsize))).
     186  subtraction ? (shrx x y) (shr x y).
     187
     188definition rol : int → int → int ≝ λx,y. rotate_left ?? (nat_of_bitvector ? y) x.
     189definition ror : int → int → int ≝ λx,y. rotate_right ?? (nat_of_bitvector ? y) x.
    259190
    260191definition rolm ≝ λx,a,m: int. i_and (rol x a) m.
     
    487418*)
    488419theorem one_not_zero: one ≠ zero.
    489 % #H
    490 lapply (refl ? (get_index' ? 31 0 one))
    491 >H in ⊢ (???% → ?)
    492 normalize #E destruct
     420% #H @(match eq_dec one zero return λx.match x with [ inl _ ⇒ True | inr _ ⇒ False ] with [ inl _ ⇒ I | inr p ⇒ ?]) normalize
     421cases p #H' @(H' H)
    493422qed.
    494423
     
    705634Qed.
    706635*)
    707 
     636(*
    708637theorem unsigned_range: ∀i. 0 ≤ unsigned i ∧ unsigned i < modulus.
    709638#i @intrange
     
    27102639
    27112640
     2641*)
  • src/common/Mem.ma

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

    r718 r744  
    2323include "common/Errors.ma".
    2424
    25 include "ASM/Vector.ma".
     25include "ASM/BitVectorZ.ma".
    2626
    2727include "basics/logic.ma".
     28
     29include "utilities/binary/Z.ma".
    2830
    2931(* To define pointers we need a few details about the memory model.
     
    8890definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
    8991definition shift_offset : offset → int → offset ≝
    90   λo,i. mk_offset (offv o + signed i).
     92  λo,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
    9193definition neg_shift_offset : offset → int → offset ≝
    92   λo,i. mk_offset (offv o - signed i).
     94  λo,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
    9395definition sub_offset : offset → offset → int ≝
    94   λx,y. repr (offv x - offv y).
     96  λx,y. bitvector_of_Z ? (offv x - offv y).
    9597definition zero_offset ≝ mk_offset OZ.
    9698definition lt_offset : offset → offset → bool ≝
     
    321323  ].
    322324
    323 definition zero_ext ≝ λnbits: Z. λv: val.
     325definition zero_ext ≝ λnbits: nat. λv: val.
    324326  match v with
    325327  [ Vint n ⇒ Vint (zero_ext nbits n)
     
    327329  ].
    328330
    329 definition sign_ext ≝ λnbits:Z. λv:val.
     331definition sign_ext ≝ λnbits:nat. λv:val.
    330332  match v with
    331333  [ Vint i ⇒ Vint (sign_ext nbits i)
     
    343345  match v1 with
    344346  [ Vint n1 ⇒ match v2 with
    345     [ Vint n2 ⇒ Vint (add n1 n2)
     347    [ Vint n2 ⇒ Vint (addition_n ? n1 n2)
    346348    | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1)
    347349    | _ ⇒ Vundef ]
     
    354356  match v1 with
    355357  [ Vint n1 ⇒ match v2 with
    356     [ Vint n2 ⇒ Vint (sub n1 n2)
     358    [ Vint n2 ⇒ Vint (subtraction ? n1 n2)
    357359    | _ ⇒ Vundef ]
    358360  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
     
    12051207qed.
    12061208
    1207 (*
    1208 Lemma zero_ext_lessdef:
    1209   forall n v1 v2, lessdef v1 v2 -> lessdef (zero_ext n v1) (zero_ext n v2).
    1210 Proof.
    1211   intros; inv H; simpl; auto.
    1212 Qed.
    1213 *)
     1209lemma zero_ext_lessdef:
     1210  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (zero_ext n v1) (zero_ext n v2).
     1211#n #v1 #v2 #H inversion H // #v #E1 #E2 destruct //
     1212qed.
     1213
    12141214lemma sign_ext_lessdef:
    12151215  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2).
  • src/utilities/Coqlib.ma

    r697 r744  
    2323
    2424include "utilities/extralib.ma".
     25include "ASM/Util.ma".
    2526
    2627(*
     
    576577(*naxiom align : Z → Z → Z.*)
    577578
    578 definition align ≝ λn: Z. λamount: Z.
    579   ((n + amount - 1) / amount) * amount.
     579definition align : nat → nat → nat ≝ λn: nat. λamount: nat.
     580  ((minus (n + amount) 1) ÷ amount) * amount.
    580581(*
    581582Lemma align_le: forall x y, y > 0 -> x <= align x y.
Note: See TracChangeset for help on using the changeset viewer.