Changeset 582 for Deliverables/D3.1


Ignore:
Timestamp:
Feb 22, 2011, 11:35:16 AM (9 years ago)
Author:
campbell
Message:

Use bit vector operations widely instead of round-trips through Z.
Implement more efficient addition, subtraction and comparison on bit vectors.

Location:
Deliverables/D3.1/C-semantics
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Csem.ma

    r502 r582  
    7474  [ Tint _ _ ⇒
    7575      match v with
    76       [ Vint n ⇒ Some ? (Vint (neg n))
     76      [ Vint n ⇒ Some ? (Vint (negation_bv wordsize n))
    7777      | _ => None ?
    7878      ]
     
    8787let rec sem_notint (v: val) : option val ≝
    8888  match v with
    89   [ Vint n ⇒ Some ? (Vint (xor n mone))
     89  [ Vint n ⇒ Some ? (Vint (xor n mone)) (* XXX *)
    9090  | _ ⇒ None ?
    9191  ].
     
    117117      match v1 with
    118118      [ Vint n1 ⇒ match v2 with
    119         [ Vint n2 ⇒ Some ? (Vint (add n1 n2))
     119        [ Vint n2 ⇒ Some ? (Vint (addition_n wordsize n1 n2))
    120120        | _ ⇒ None ? ]
    121121      | _ ⇒ None ? ]
     
    149149      match v1 with
    150150      [ Vint n1 ⇒ match v2 with
    151         [ Vint n2 ⇒ Some ? (Vint (sub n1 n2))
     151        [ Vint n2 ⇒ Some ? (Vint (subtraction wordsize n1 n2))
    152152        | _ ⇒ None ? ]
    153153      | _ ⇒ None ? ]
     
    183183      match v1 with
    184184      [ Vint n1 ⇒ match v2 with
    185         [ Vint n2 ⇒ Some ? (Vint (mul n1 n2))
     185        [ Vint n2 ⇒ Some ? (Vint (\snd (split ? wordsize wordsize (multiplication ? n1 n2))))
    186186        | _ ⇒ None ? ]
    187187      | _ ⇒ None ? ]
     
    201201      match v1 with
    202202      [ Vint n1 ⇒ match v2 with
    203         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (divu n1 n2))
     203        [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)
    204204        | _ ⇒ None ? ]
    205205      | _ ⇒ None ? ]
     
    207207      match v1 with
    208208       [ Vint n1 ⇒ match v2 with
    209          [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint(divs n1 n2))
     209         [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)
    210210         | _ ⇒ None ? ]
    211211      | _ ⇒ None ? ]
     
    225225      match v1 with
    226226      [ Vint n1 ⇒ match v2 with
    227         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (modu n1 n2))
     227        [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)
    228228        | _ ⇒ None ? ]
    229229      | _ ⇒ None ? ]
     
    231231      match v1 with
    232232      [ Vint n1 ⇒ match v2 with
    233         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (mods n1 n2))
     233        [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)
    234234        | _ ⇒ None ? ]
    235235      | _ ⇒ None ? ]
     
    241241  match v1 with
    242242  [ Vint n1 ⇒ match v2 with
    243     [ Vint n2 ⇒ Some ? (Vint(i_and n1 n2))
     243    [ Vint n2 ⇒ Some ? (Vint (conjunction_bv ? n1 n2))
    244244    | _ ⇒ None ? ]
    245245  | _ ⇒ None ?
     
    249249  match v1 with
    250250  [ Vint n1 ⇒ match v2 with
    251     [ Vint n2 ⇒ Some ? (Vint(or n1 n2))
     251    [ Vint n2 ⇒ Some ? (Vint (inclusive_disjunction_bv ? n1 n2))
    252252    | _ ⇒ None ? ]
    253253  | _ ⇒ None ?
     
    257257  match v1 with
    258258  [ Vint n1 ⇒ match v2 with
    259     [ Vint n2 ⇒ Some ? (Vint(xor n1 n2))
     259    [ Vint n2 ⇒ Some ? (Vint (exclusive_disjunction_bv ? n1 n2))
    260260    | _ ⇒ None ? ]
    261261  | _ ⇒ None ?
  • Deliverables/D3.1/C-semantics/Integers.ma

    r547 r582  
    131131
    132132definition eq : int → int → bool ≝ eq_bv wordsize.
    133 definition lt : int → int → bool ≝ λx,y:int.
    134   if Zltb (signed x) (signed y) then true else false.
    135 definition ltu : int → int → bool ≝ λx,y: int.
    136   if Zltb (unsigned x) (unsigned y) then true else false.
    137 
    138 definition neg : int → int ≝ λx. repr (- unsigned x).
     133definition lt : int → int → bool ≝ lt_s wordsize.
     134definition ltu : int → int → bool ≝ lt_u wordsize.
     135
     136definition neg : int → int ≝ negation_bv wordsize.
    139137
    140138let rec zero_ext (n:Z) (x:int) on x : int ≝
     
    145143        if Zltb y (two_p (n-1)) then y else y - p).
    146144
    147 definition add ≝ λx,y: int.
    148   repr (unsigned x + unsigned y).
    149 definition sub ≝ λx,y: int.
    150   repr (unsigned x - unsigned y).
    151 definition mul ≝ λx,y: int.
    152   repr (unsigned x * unsigned y).
     145definition add ≝ addition_n wordsize.
     146definition sub ≝ subtraction wordsize.
     147definition mul ≝ λx,y. \fst (split ? wordsize wordsize (multiplication wordsize x y)).
    153148definition Zdiv_round : Z → Z → Z ≝ λx,y: Z.
    154149  if Zltb x 0 then
     
    218213  repr (Z_of_bits wordsize (λi. f (fx i) (fy i))).
    219214
    220 definition i_and : int → int → int ≝ λx,y. bitwise_binop andb x y.
    221 definition or : int → int → int ≝ λx,y. bitwise_binop orb x y.
    222 definition xor : int → int → int ≝ λx,y. bitwise_binop xorb x y.
    223 
    224 definition not : int → int ≝ λx.xor x mone.
     215definition i_and : int → int → int ≝ conjunction_bv wordsize.
     216definition or : int → int → int ≝ inclusive_disjunction_bv wordsize.
     217definition xor : int → int → int ≝ exclusive_disjunction_bv wordsize.
     218
     219definition not : int → int ≝ negation_bv wordsize.
    225220
    226221(* * Shifts and rotates. *)
     
    490485Qed.
    491486*)
    492 axiom one_not_zero: one ≠ zero.
     487theorem one_not_zero: one ≠ zero.
     488% #H
     489lapply (refl ? (get_index' ? 31 0 one))
     490>H in ⊢ (???% → ?)
     491normalize #E destruct
     492qed.
     493
    493494(*
    494 Theorem one_not_zero: one <> zero.
    495 Proof.
    496   assert (unsigned one <> unsigned zero).
    497   rewrite unsigned_one; rewrite unsigned_zero; congruence.
    498   congruence.
    499 Qed.
    500 
    501495Theorem unsigned_repr_wordsize:
    502496  unsigned iwordsize = Z_of_nat wordsize.
  • Deliverables/D3.1/C-semantics/cerco/Arithmetic.ma

    r533 r582  
    88      | true ⇒ S O
    99      ].
     10
     11definition carry_of : bool → bool → bool → bool ≝
     12λa,b,c. match a with [ false ⇒ b ∧ c | true ⇒ b ∨ c ].
     13
     14definition add_with_carries : ∀n:nat. BitVector n → BitVector n → bool →
     15                                      BitVector n × (BitVector n) ≝
     16  λn,x,y,init_carry.
     17  fold_right2_i ???
     18   (λn,b,c,r.
     19     let 〈lower_bits, carries〉 ≝ r in
     20     let last_carry ≝ match carries with [ VEmpty ⇒ init_carry | VCons _ cy _ ⇒ cy ] in
     21     let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_carry in
     22     let carry ≝ carry_of b c last_carry in
     23       〈bit:::lower_bits, carry:::carries〉
     24   )
     25   〈[[ ]], [[ ]]〉 n x y.
     26
     27(* Essentially the only difference for subtraction. *)
     28definition borrow_of : bool → bool → bool → bool ≝
     29λa,b,c. match a with [ false ⇒ b ∨ c | true ⇒ b ∧ c ].
     30
     31definition sub_with_borrows : ∀n:nat. BitVector n → BitVector n → bool →
     32                                      BitVector n × (BitVector n) ≝
     33  λn,x,y,init_borrow.
     34  fold_right2_i ???
     35   (λn,b,c,r.
     36     let 〈lower_bits, borrows〉 ≝ r in
     37     let last_borrow ≝ match borrows with [ VEmpty ⇒ init_borrow | VCons _ bw _ ⇒ bw ] in
     38     let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_borrow in
     39     let borrow ≝ borrow_of b c last_borrow in
     40       〈bit:::lower_bits, borrow:::borrows〉
     41   )
     42   〈[[ ]], [[ ]]〉 n x y.
    1043   
    1144definition add_n_with_carry:
    12       ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝
     45      ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. n ≥ 5 →
     46      (BitVector n) × (BitVector 3) ≝
    1347  λn: nat.
    1448  λb: BitVector n.
    1549  λc: BitVector n.
    1650  λcarry: bool.
    17     let b_as_nat ≝ nat_of_bitvector n b in
    18     let c_as_nat ≝ nat_of_bitvector n c in
    19     let carry_as_nat ≝ nat_of_bool carry in
    20     let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in
    21     let ac_flag ≝ geb ((modulus b_as_nat (2 * n)) +
    22                   (modulus c_as_nat (2 * n)) +
    23                   c_as_nat) (2 * n) in
    24     let bit_xxx ≝ geb ((modulus b_as_nat (2^(n - 1))) +
    25                   (modulus c_as_nat (2^(n - 1))) +
    26                   c_as_nat) (2^(n - 1)) in
    27     let result ≝ modulus result_old (2^n) in
    28     let cy_flag ≝ geb result_old (2^n) in
    29     let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
    30       pair ? ? (bitvector_of_nat n result)
    31                        ([[ cy_flag ; ac_flag ; ov_flag ]]).
    32 
    33 definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝
     51  λpf:n ≥ 5.
     52 
     53    let 〈result, carries〉 ≝ add_with_carries n b c carry in
     54    let cy_flag ≝ get_index_v ?? carries 0 ? in
     55    let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in
     56    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
     57      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
     58// @(transitive_le  … pf) /2/
     59qed.
     60
     61definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. n ≥ 5 →
     62                                            (BitVector n) × (BitVector 3) ≝
    3463  λn: nat.
    3564  λb: BitVector n.
    3665  λc: BitVector n.
    3766  λcarry: bool.
    38      let b_as_nat ≝ nat_of_bitvector n b in
    39      let c_as_nat ≝ nat_of_bitvector n c in
    40      let carry_as_nat ≝ nat_of_bool carry in
    41      let temporary ≝ (b_as_nat mod (2 * n)) - (c_as_nat mod (2 * n)) in
    42      let ac_flag ≝ ltb (b_as_nat mod (2 * n)) ((c_as_nat mod (2 * n)) + carry_as_nat) in
    43      let bit_six ≝ ltb (b_as_nat mod (2^(n - 1))) ((c_as_nat mod (2^(n - 1))) + carry_as_nat) in
    44      let 〈b',cy_flag〉 ≝
    45        if geb b_as_nat (c_as_nat + carry_as_nat) then
    46          〈b_as_nat, false〉
    47        else
    48          〈b_as_nat + (2^n), true〉
    49      in
    50        let ov_flag ≝ exclusive_disjunction cy_flag bit_six in
    51          〈bitvector_of_nat n ((b' - c_as_nat) - carry_as_nat), [[ cy_flag; ac_flag; ov_flag ]]〉.         
    52          
     67  λpf:n ≥ 5.
     68 
     69    let 〈result, carries〉 ≝ sub_with_borrows n b c carry in
     70    let cy_flag ≝ get_index_v ?? carries 0 ? in
     71    let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in
     72    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
     73      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
     74// @(transitive_le  … pf) /2/
     75qed.
     76
    5377definition add_8_with_carry ≝ add_n_with_carry 8.
    5478definition add_16_with_carry ≝ add_n_with_carry 16.
     
    5983  λn: nat.
    6084  λb: BitVector n.
    61     let b_as_nat ≝ (nat_of_bitvector n b) + 1 in
    62     let overflow ≝ geb b_as_nat 2^n in
    63       match overflow with
    64         [ false ⇒ bitvector_of_nat n b_as_nat
    65         | true ⇒ zero n
    66         ].
     85    \fst (add_with_carries n b (zero n) true).
    6786       
    6887definition decrement ≝
    6988  λn: nat.
    7089  λb: BitVector n.
    71     let b_as_nat ≝ nat_of_bitvector n b in
    72       match b_as_nat with
    73         [ O ⇒ maximum n
    74         | S o ⇒ bitvector_of_nat n o
    75         ].
     90    \fst (sub_with_borrows n b (zero n) true).
    7691   
    7792definition two_complement_negation ≝
     
    8499  λn: nat.
    85100  λb, c: BitVector n.
    86     let 〈res,flags〉 ≝ add_n_with_carry n b c false in
     101    let 〈res,flags〉 ≝ add_with_carries n b c false in
    87102      res.
    88103   
     
    154169    let b_nat ≝ nat_of_bitvector ? b in
    155170    let c_nat ≝ nat_of_bitvector ? c in
    156     let result ≝ modulus b_nat c_nat in
    157       bitvector_of_nat (n + n) result.
     171    match c_nat with
     172    [ O ⇒ None ?
     173    | _ ⇒
     174      let result ≝ modulus b_nat c_nat in
     175      Some ? (bitvector_of_nat n result)
     176    ].
    158177           
    159178definition modulus_s ≝
     
    168187     
    169188definition lt_u ≝
    170   λn.
    171   λb, c: BitVector n.
    172     let b_nat ≝ nat_of_bitvector ? b in
    173     let c_nat ≝ nat_of_bitvector ? c in
    174       ltb b_nat c_nat.
     189  fold_right2_i ???
     190    (λ_.λa,b,r.
     191      match a with
     192      [ true ⇒ b ∧ r
     193      | false ⇒ b ∨ r
     194      ])
     195    false.
    175196     
    176197definition gt_u ≝ λn, b, c. lt_u n c b.
     
    179200
    180201definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
    181      
     202
    182203definition lt_s ≝
    183204  λn.
    184205  λb, c: BitVector n.
    185     let 〈result, flags〉 ≝ sub_n_with_carry n b c false in
    186     let ov_flag ≝ get_index_v ? ? flags 2 ? in
    187      if ov_flag then
    188        true
    189      else
    190        ((match n return λn'.BitVector n' → bool with
    191        [ O ⇒ λ_.false
    192        | S o ⇒
    193          λresult'.(get_index_v ? ? result' O ?)
    194        ]) result).
    195   //
    196 qed.
    197 
     206    let 〈result, borrows〉 ≝ sub_with_borrows n b c false in
     207    match borrows with
     208    [ VEmpty ⇒ false
     209    | VCons _ bwn tl ⇒
     210      match tl with
     211      [ VEmpty ⇒ false
     212      | VCons _ bwpn _ ⇒
     213        if exclusive_disjunction bwn bwpn then
     214          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
     215        else
     216          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
     217      ]
     218    ].
     219   
    198220definition gt_s ≝ λn,b,c. lt_s n c b.
    199221
Note: See TracChangeset for help on using the changeset viewer.