From 8f65bf639b79dc0553e586a59ea5c09cb7e85506 Mon Sep 17 00:00:00 2001 From: Fardale Date: Sat, 22 May 2021 21:38:36 +0200 Subject: [PATCH 01/26] use bytes instead of int array for CCBV --- src/data/CCBV.ml | 167 +++++++++++++++++++++++++--------------------- src/data/CCBV.mli | 2 +- 2 files changed, 92 insertions(+), 77 deletions(-) diff --git a/src/data/CCBV.ml b/src/data/CCBV.ml index 50191da5..3b8142b3 100644 --- a/src/data/CCBV.ml +++ b/src/data/CCBV.ml @@ -8,20 +8,35 @@ let ppli = CCFormat.(Dump.list int) *) -let width_ = Sys.word_size - 1 +let width_ = 8 -(** We use OCamls ints to store the bits. We index them from the +(* Helper functions *) +let[@inline] get_ b i = Char.code (Bytes.get b i) +let[@inline] unsafe_get_ b i = Char.code (Bytes.unsafe_get b i) + +let[@inline] set_ b i v = Bytes.set b i (Char.unsafe_chr v) +let[@inline] unsafe_set_ b i v = Bytes.unsafe_set b i (Char.unsafe_chr v) + +let[@inline] mod_ n = (n lsl (Sys.word_size - 4)) lsr (Sys.word_size - 4) + +let[@inline] div_ n = n lsr 3 + +let[@inline] mul_ n = n lsl 3 + +let zero = Char.unsafe_chr 0 + +(** We use OCamls chars to store the bits. We index them from the least significant bit. We create masks to zero out the most significant bits that aren't used to store values. This is necessary when we are constructing or negating a bit vector. *) let lsb_masks_ = - let a = Array.make (width_ + 1) 0 in + let b = Bytes.make (width_ + 1) zero in for i = 1 to width_ do - a.(i) <- a.(i-1) lor (1 lsl (i - 1)) + set_ b i (get_ b (i-1) lor (1 lsl (i - 1))) done; - a + b -let all_ones_ = lsb_masks_.(width_) +let all_ones_ = Bytes.get lsb_masks_ width_ (* count the 1 bits in [n]. See https://en.wikipedia.org/wiki/Hamming_weight *) let count_bits_ n = @@ -35,31 +50,31 @@ let count_bits_ n = *) type t = { - mutable a : int array; + mutable b : bytes; mutable size : int; } let length t = t.size -let empty () = { a = [| |] ; size = 0 } +let empty () = { b = Bytes.empty ; size = 0 } -let array_length_of_size size = - if size mod width_ = 0 then size / width_ else (size / width_) + 1 +let bytes_length_of_size size = + if mod_ size = 0 then div_ size else (div_ size) + 1 let create ~size default = - if size = 0 then { a = [| |]; size } + if size = 0 then empty () else ( - let n = array_length_of_size size in - let a = if default - then Array.make n all_ones_ - else Array.make n 0 + let n = bytes_length_of_size size in + let b = if default + then Bytes.make n all_ones_ + else Bytes.make n zero in (* adjust last bits *) - let r = size mod width_ in + let r = mod_ size in if default && r <> 0 then ( - Array.unsafe_set a (n-1) lsb_masks_.(r); + Bytes.unsafe_set b (n-1) (Bytes.unsafe_get lsb_masks_ r); ); - { a; size } + { b; size } ) (*$Q @@ -74,21 +89,21 @@ let create ~size default = create ~size:29 true |> to_sorted_list = CCList.range 0 28 *) -let copy bv = { bv with a = Array.copy bv.a } +let copy bv = { bv with b = Bytes.copy bv.b } (*$Q (Q.list Q.small_int) (fun l -> \ let bv = of_list l in to_list bv = to_list (copy bv)) *) -let capacity bv = width_ * Array.length bv.a +let capacity bv = mul_ (Bytes.length bv.b) let cardinal bv = if bv.size = 0 then 0 else ( let n = ref 0 in - for i = 0 to Array.length bv.a - 1 do - n := !n + count_bits_ bv.a.(i) (* MSB of last element are all 0 *) + for i = 0 to Bytes.length bv.b - 1 do + n := !n + count_bits_ (get_ bv.b i) (* MSB of last element are all 0 *) done; !n ) @@ -98,9 +113,9 @@ let cardinal bv = *) let really_resize_ bv ~desired ~current size = - let a' = Array.make desired 0 in - Array.blit bv.a 0 a' 0 current; - bv.a <- a'; + let b = Bytes.make desired zero in + Bytes.blit bv.b 0 b 0 current; + bv.b <- b; bv.size <- size let grow_ bv size = @@ -108,15 +123,15 @@ let grow_ bv size = then bv.size <- size else ( (* beyond capacity *) - let desired = array_length_of_size size in - let current = Array.length bv.a in + let desired = bytes_length_of_size size in + let current = Bytes.length bv.b in assert (desired > current); really_resize_ bv ~desired ~current size ) let shrink_ bv size = - let desired = array_length_of_size size in - let current = Array.length bv.a in + let desired = bytes_length_of_size size in + let current = Bytes.length bv.b in really_resize_ bv ~desired ~current size let resize bv size = @@ -138,8 +153,8 @@ let resize bv size = let is_empty bv = try - for i = 0 to Array.length bv.a - 1 do - if bv.a.(i) <> 0 then raise Exit (* MSB of last element are all 0 *) + for i = 0 to Bytes.length bv.b - 1 do + if get_ bv.b i <> 0 then raise Exit (* MSB of last element are all 0 *) done; true with Exit -> @@ -147,10 +162,10 @@ let is_empty bv = let get bv i = if i < 0 then invalid_arg "get: negative index"; - let n = i / width_ in - let i = i mod width_ in - if n < Array.length bv.a - then (Array.unsafe_get bv.a n) land (1 lsl i) <> 0 + let n = div_ i in + let i = mod_ i in + if n < Bytes.length bv.b + then (unsafe_get_ bv.b n) land (1 lsl i) <> 0 else false (*$R @@ -172,10 +187,10 @@ let get bv i = let set bv i = if i < 0 then invalid_arg "set: negative index" else ( - let n = i / width_ in - let j = i mod width_ in + let n = div_ i in + let j = mod_ i in if i >= bv.size then grow_ bv (i+1); - Array.unsafe_set bv.a n ((Array.unsafe_get bv.a n) lor (1 lsl j)) + unsafe_set_ bv.b n ((unsafe_get_ bv.b n) lor (1 lsl j)) ) (*$T @@ -186,10 +201,10 @@ let set bv i = let reset bv i = if i < 0 then invalid_arg "reset: negative index" else ( - let n = i / width_ in - let j = i mod width_ in + let n = div_ i in + let j = mod_ i in if i >= bv.size then grow_ bv (i+1); - Array.unsafe_set bv.a n ((Array.unsafe_get bv.a n) land (lnot (1 lsl j))) + unsafe_set_ bv.b n ((unsafe_get_ bv.b n) land (lnot (1 lsl j))) ) (*$T @@ -199,10 +214,10 @@ let reset bv i = let flip bv i = if i < 0 then invalid_arg "reset: negative index" else ( - let n = i / width_ in - let j = i mod width_ in + let n = div_ i in + let j = mod_ i in if i >= bv.size then grow_ bv (i+1); - Array.unsafe_set bv.a n ((Array.unsafe_get bv.a n) lxor (1 lsl j)) + unsafe_set_ bv.b n ((unsafe_get_ bv.b n) lxor (1 lsl j)) ) (*$R @@ -221,7 +236,7 @@ let flip bv i = *) let clear bv = - Array.fill bv.a 0 (Array.length bv.a) 0 + Bytes.fill bv.b 0 (Bytes.length bv.b) zero (*$T let bv = create ~size:37 true in cardinal bv = 37 && (clear bv; cardinal bv= 0) @@ -237,7 +252,7 @@ let clear bv = let equal x y : bool = x.size = y.size && - x.a = y.a + x.b = y.b (*$T equal (of_list [1; 3; 4]) (of_list [1; 3; 4]) @@ -248,20 +263,20 @@ let equal x y : bool = *) let iter bv f = - let len = array_length_of_size bv.size in - assert (len <= Array.length bv.a); + let len = bytes_length_of_size bv.size in + assert (len <= Bytes.length bv.b); for n = 0 to len - 2 do - let j = width_ * n in - let word_n = Array.unsafe_get bv.a n in + let j = mul_ n in + let word_n = unsafe_get_ bv.b n in for i = 0 to width_ - 1 do f (j+i) ((word_n land (1 lsl i)) <> 0) done done; if bv.size > 0 then ( - let j = width_ * (len - 1) in - let r = bv.size mod width_ in + let j = mul_ (len - 1) in + let r = mod_ bv.size in let final_length = if r = 0 then width_ else r in - let final_word = Array.unsafe_get bv.a (len-1) in + let final_word = unsafe_get_ bv.b (len-1) in for i = 0 to final_length - 1 do f (j + i) ((final_word land (1 lsl i)) <> 0) done @@ -399,37 +414,37 @@ let filter bv p = *) let negate_self b = - let len = Array.length b.a in + let len = Bytes.length b.b in for n = 0 to len - 1 do - Array.unsafe_set b.a n (lnot (Array.unsafe_get b.a n)) + unsafe_set_ b.b n (lnot (unsafe_get_ b.b n)) done; - let r = b.size mod width_ in + let r = mod_ b.size in if r <> 0 then - let l = Array.length b.a - 1 in - Array.unsafe_set b.a l (lsb_masks_.(r) land (Array.unsafe_get b.a l)) + let l = Bytes.length b.b - 1 in + unsafe_set_ b.b l (unsafe_get_ lsb_masks_ r land (unsafe_get_ b.b l)) (*$= & ~printer:(CCFormat.to_string ppli) [0;3;4;6] (let v = of_list [1;2;5;7;] in negate_self v; to_sorted_list v) *) -let negate b = - let a = Array.map (lnot) b.a in - let r = b.size mod width_ in +let negate a = + let b = Bytes.map (fun c -> Char.unsafe_chr (lnot (Char.code c))) a.b in + let r = mod_ a.size in if r <> 0 then ( - let l = Array.length b.a - 1 in - Array.unsafe_set a l (lsb_masks_.(r) land (Array.unsafe_get a l)) + let l = Bytes.length a.b - 1 in + unsafe_set_ b l (unsafe_get_ lsb_masks_ r land (unsafe_get_ b l)) ); - { a ; size = b.size } + { b ; size = a.size } (*$Q Q.small_int (fun size -> create ~size false |> negate |> cardinal = size) *) let union_into_no_resize_ ~into bv = - assert (Array.length into.a >= Array.length bv.a); - for i = 0 to Array.length bv.a - 1 do - Array.unsafe_set into.a i - ((Array.unsafe_get into.a i) lor (Array.unsafe_get bv.a i)) + assert (Bytes.length into.b >= Bytes.length bv.b); + for i = 0 to Bytes.length bv.b - 1 do + unsafe_set_ into.b i + ((unsafe_get_ into.b i) lor (unsafe_get_ bv.b i)) done (* Underlying size grows for union. *) @@ -494,10 +509,10 @@ let union b1 b2 = let inter_into_no_resize_ ~into bv = - assert (Array.length into.a <= Array.length bv.a); - for i = 0 to (Array.length into.a) - 1 do - Array.unsafe_set into.a i - ((Array.unsafe_get into.a i) land (Array.unsafe_get bv.a i)) + assert (Bytes.length into.b <= Bytes.length bv.b); + for i = 0 to (Bytes.length into.b) - 1 do + unsafe_set_ into.b i + ((unsafe_get_ into.b i) land (unsafe_get_ bv.b i)) done (* Underlying size shrinks for inter. *) @@ -543,10 +558,10 @@ let inter b1 b2 = (* Underlying size depends on the 'in_' set for diff, so we don't change it's size! *) let diff_into ~into bv = - let n = min (Array.length into.a) (Array.length bv.a) in + let n = min (Bytes.length into.b) (Bytes.length bv.b) in for i = 0 to n - 1 do - Array.unsafe_set into.a i - ((Array.unsafe_get into.a i) land (lnot (Array.unsafe_get bv.a i))) + unsafe_set_ into.b i + ((unsafe_get_ into.b i) land (lnot (unsafe_get_ bv.b i))) done let diff in_ not_in = @@ -647,4 +662,4 @@ let pp out bv = "bv {00001}" (CCFormat.to_string pp (of_list [4])) *) -let __to_word_l bv = Array.to_list bv.a +let __to_word_l bv = CCString.to_list (Bytes.unsafe_to_string bv.b) diff --git a/src/data/CCBV.mli b/src/data/CCBV.mli index 7829c6ad..3a6bec70 100644 --- a/src/data/CCBV.mli +++ b/src/data/CCBV.mli @@ -151,5 +151,5 @@ val pp : Format.formatter -> t -> unit (**/**) -val __to_word_l : t -> int list +val __to_word_l : t -> char list (**/**) From 8ff253f18de08c06974855be18127b33cf50077b Mon Sep 17 00:00:00 2001 From: Fardale Date: Sat, 22 May 2021 22:09:24 +0200 Subject: [PATCH 02/26] chore(CCBV): clean comments --- src/data/CCBV.ml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/data/CCBV.ml b/src/data/CCBV.ml index 3b8142b3..8f7b478f 100644 --- a/src/data/CCBV.ml +++ b/src/data/CCBV.ml @@ -1,9 +1,6 @@ (** {2 Imperative Bitvectors} *) -(* TODO: move to [bytes] and replace all [mod] and [/] with bitshifts - because width_=8 *) - (*$inject let ppli = CCFormat.(Dump.list int) *) @@ -154,7 +151,7 @@ let resize bv size = let is_empty bv = try for i = 0 to Bytes.length bv.b - 1 do - if get_ bv.b i <> 0 then raise Exit (* MSB of last element are all 0 *) + if get_ bv.b i <> 0 then raise Exit done; true with Exit -> From 6a3e446d277d609829921e9c0133fc7c3d6ddbe4 Mon Sep 17 00:00:00 2001 From: Fardale Date: Sun, 23 May 2021 14:49:31 +0200 Subject: [PATCH 03/26] use precomputed table for count_bits_ --- src/data/CCBV.ml | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/src/data/CCBV.ml b/src/data/CCBV.ml index 8f7b478f..53410171 100644 --- a/src/data/CCBV.ml +++ b/src/data/CCBV.ml @@ -35,12 +35,19 @@ let lsb_masks_ = let all_ones_ = Bytes.get lsb_masks_ width_ -(* count the 1 bits in [n]. See https://en.wikipedia.org/wiki/Hamming_weight *) let count_bits_ n = - let rec recurse count n = - if n = 0 then count else recurse (count+1) (n land (n-1)) - in - recurse 0 n + let table = [| 0; 1; 1; 2; 1; 2; 2; 3; 1; 2; 2; 3; 2; 3; 3; 4; 1; 2; 2; 3; 2; 3; 3; 4; + 2; 3; 3; 4; 3; 4; 4; 5; 1; 2; 2; 3; 2; 3; 3; 4; 2; 3; 3; 4; 3; 4; 4; 5; + 2; 3; 3; 4; 3; 4; 4; 5; 3; 4; 4; 5; 4; 5; 5; 6; 1; 2; 2; 3; 2; 3; 3; 4; + 2; 3; 3; 4; 3; 4; 4; 5; 2; 3; 3; 4; 3; 4; 4; 5; 3; 4; 4; 5; 4; 5; 5; 6; + 2; 3; 3; 4; 3; 4; 4; 5; 3; 4; 4; 5; 4; 5; 5; 6; 3; 4; 4; 5; 4; 5; 5; 6; + 4; 5; 5; 6; 5; 6; 6; 7; 1; 2; 2; 3; 2; 3; 3; 4; 2; 3; 3; 4; 3; 4; 4; 5; + 2; 3; 3; 4; 3; 4; 4; 5; 3; 4; 4; 5; 4; 5; 5; 6; 2; 3; 3; 4; 3; 4; 4; 5; + 3; 4; 4; 5; 4; 5; 5; 6; 3; 4; 4; 5; 4; 5; 5; 6; 4; 5; 5; 6; 5; 6; 6; 7; + 2; 3; 3; 4; 3; 4; 4; 5; 3; 4; 4; 5; 4; 5; 5; 6; 3; 4; 4; 5; 4; 5; 5; 6; + 4; 5; 5; 6; 5; 6; 6; 7; 3; 4; 4; 5; 4; 5; 5; 6; 4; 5; 5; 6; 5; 6; 6; 7; + 4; 5; 5; 6; 5; 6; 6; 7; 5; 6; 6; 7; 6; 7; 7; 8; |] in + Array.unsafe_get table n (* Can I access the "private" members in testing? $Q (Q.int_bound (Sys.word_size - 1)) (fun i -> count_bits_ lsb_masks_.(i) = i) From 19c65b5472eb583e2a5a92e2a165a457febe0b4c Mon Sep 17 00:00:00 2001 From: Fardale Date: Sun, 23 May 2021 15:01:36 +0200 Subject: [PATCH 04/26] apply comments from the review --- src/data/CCBV.ml | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) diff --git a/src/data/CCBV.ml b/src/data/CCBV.ml index 53410171..f355203f 100644 --- a/src/data/CCBV.ml +++ b/src/data/CCBV.ml @@ -14,7 +14,7 @@ let[@inline] unsafe_get_ b i = Char.code (Bytes.unsafe_get b i) let[@inline] set_ b i v = Bytes.set b i (Char.unsafe_chr v) let[@inline] unsafe_set_ b i v = Bytes.unsafe_set b i (Char.unsafe_chr v) -let[@inline] mod_ n = (n lsl (Sys.word_size - 4)) lsr (Sys.word_size - 4) +let[@inline] mod_ n = (n land 0b111) let[@inline] div_ n = n lsr 3 @@ -26,14 +26,9 @@ let zero = Char.unsafe_chr 0 least significant bit. We create masks to zero out the most significant bits that aren't used to store values. This is necessary when we are constructing or negating a bit vector. *) -let lsb_masks_ = - let b = Bytes.make (width_ + 1) zero in - for i = 1 to width_ do - set_ b i (get_ b (i-1) lor (1 lsl (i - 1))) - done; - b +let[@inline] lsb_masks_ n = (1 lsl n) - 1 -let all_ones_ = Bytes.get lsb_masks_ width_ +let all_ones_ = Char.unsafe_chr (lsb_masks_ width_) let count_bits_ n = let table = [| 0; 1; 1; 2; 1; 2; 2; 3; 1; 2; 2; 3; 2; 3; 3; 4; 1; 2; 2; 3; 2; 3; 3; 4; @@ -76,7 +71,7 @@ let create ~size default = (* adjust last bits *) let r = mod_ size in if default && r <> 0 then ( - Bytes.unsafe_set b (n-1) (Bytes.unsafe_get lsb_masks_ r); + Bytes.unsafe_set b (n-1) (Char.unsafe_chr (lsb_masks_ r)); ); { b; size } ) @@ -425,7 +420,7 @@ let negate_self b = let r = mod_ b.size in if r <> 0 then let l = Bytes.length b.b - 1 in - unsafe_set_ b.b l (unsafe_get_ lsb_masks_ r land (unsafe_get_ b.b l)) + unsafe_set_ b.b l (lsb_masks_ r land (unsafe_get_ b.b l)) (*$= & ~printer:(CCFormat.to_string ppli) [0;3;4;6] (let v = of_list [1;2;5;7;] in negate_self v; to_sorted_list v) @@ -436,7 +431,7 @@ let negate a = let r = mod_ a.size in if r <> 0 then ( let l = Bytes.length a.b - 1 in - unsafe_set_ b l (unsafe_get_ lsb_masks_ r land (unsafe_get_ b l)) + unsafe_set_ b l (lsb_masks_ r land (unsafe_get_ b l)) ); { b ; size = a.size } @@ -666,4 +661,7 @@ let pp out bv = "bv {00001}" (CCFormat.to_string pp (of_list [4])) *) -let __to_word_l bv = CCString.to_list (Bytes.unsafe_to_string bv.b) +let __to_word_l bv = + let l = ref [] in + Bytes.iter (fun c -> l := c :: !l) bv.b; + List.rev !l From 22bbe23c5a16494030000d72f27739f5624ef2cd Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 2 Jan 2022 21:16:45 -0500 Subject: [PATCH 05/26] feat(CCInt64): add `popcount` operation adapted from CCInt, but directly on int64, so it works for Int64.{min_int/max_int}. --- src/core/CCInt64.ml | 24 ++++++++++++++++++++++++ src/core/CCInt64.mli | 4 ++++ 2 files changed, 28 insertions(+) diff --git a/src/core/CCInt64.ml b/src/core/CCInt64.ml index ab290798..bb32d24c 100644 --- a/src/core/CCInt64.ml +++ b/src/core/CCInt64.ml @@ -11,6 +11,30 @@ let hash x = Stdlib.abs (to_int x) let sign i = compare i zero +(* see {!CCInt.popcount} for more details *) +let[@inline] popcount (b:t) : int = + let m1 = 0x5555555555555555L in + let m2 = 0x3333333333333333L in + let m4 = 0x0f0f0f0f0f0f0f0fL in + + let b = sub b (logand (shift_right_logical b 1) m1) in + let b = add (logand b m2) (logand (shift_right_logical b 2) m2) in + let b = logand (add b (shift_right_logical b 4)) m4 in + let b = add b (shift_right_logical b 8) in + let b = add b (shift_right_logical b 16) in + let b = add b (shift_right_logical b 32) in + let b = logand b 0x7fL in + to_int b + +(*$= & ~printer:CCInt.to_string + 0 (popcount 0L) + 1 (popcount 1L) + 63 (popcount max_int) + 1 (popcount min_int) + 10 (popcount 0b1110010110110001010L) + 5 (popcount 0b1101110000000000L) +*) + let pow a b = let rec aux acc = function | 1L -> acc diff --git a/src/core/CCInt64.mli b/src/core/CCInt64.mli index 3a55f996..39ccbeec 100644 --- a/src/core/CCInt64.mli +++ b/src/core/CCInt64.mli @@ -30,6 +30,10 @@ val hash : t -> int (** [hash x] computes the hash of [x]. Like {!Stdlib.abs (to_int x)}. *) +val popcount : t -> int +(** Number of bits set to 1. + @since NEXT_RELEASE *) + val sign : t -> int (** [sign x] return [0] if [x = 0], [-1] if [x < 0] and [1] if [x > 0]. Same as [compare x zero]. From b8c93f42fab2fd0ee006c9f699a14200b9a9c3ce Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 2 Jan 2022 21:42:59 -0500 Subject: [PATCH 06/26] feat(CCInt32): add popcount function --- src/core/CCInt32.ml | 30 ++++++++++++++++++++++++++++++ src/core/CCInt32.mli | 4 ++++ 2 files changed, 34 insertions(+) diff --git a/src/core/CCInt32.ml b/src/core/CCInt32.ml index 2abe36cd..642b6daa 100644 --- a/src/core/CCInt32.ml +++ b/src/core/CCInt32.ml @@ -32,6 +32,36 @@ let pow a b = pow 0l 1l = 0l *) +(* see {!CCInt.popcount} for more details *) +let[@inline] popcount (b:t) : int = + let m1 = 0x55555555l in + let m2 = 0x33333333l in + let m4 = 0x0f0f0f0fl in + + let b = sub b (logand (shift_right_logical b 1) m1) in + let b = add (logand b m2) (logand (shift_right_logical b 2) m2) in + let b = logand (add b (shift_right_logical b 4)) m4 in + let b = add b (shift_right_logical b 8) in + let b = add b (shift_right_logical b 16) in + let b = logand b 0x7fl in + to_int b + +(*$Q + Q.(0 -- (Int32.max_int |> Int32.to_int)) (fun i -> \ + let n1 = CCInt.popcount i in \ + let n2 = CCInt32.popcount (Int32.of_int i) in \ + CCInt.(n1 = n2)) + *) + +(*$= & ~printer:CCInt.to_string + 0 (popcount 0l) + 1 (popcount 1l) + 31 (popcount max_int) + 1 (popcount min_int) + 10 (popcount 0b1110010110110001010l) + 5 (popcount 0b1101110000000000l) +*) + let floor_div a n = if compare a 0l < 0 && compare n 0l >= 0 then sub (div (add a 1l) n) 1l diff --git a/src/core/CCInt32.mli b/src/core/CCInt32.mli index 3dd383cb..95efe38b 100644 --- a/src/core/CCInt32.mli +++ b/src/core/CCInt32.mli @@ -41,6 +41,10 @@ val pow : t -> t -> t Raises [Invalid_argument] if [x = y = 0] or [y] < 0. @since 0.11 *) +val popcount : t -> int +(** Number of bits set to 1. + @since NEXT_RELEASE *) + val floor_div : t -> t -> t (** [floor_div x n] is integer division rounding towards negative infinity. It satisfies [x = m * floor_div x n + rem x n]. From ced66a76e177df9ee860d362ff599fc42a1984b5 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 2 Jan 2022 21:45:26 -0500 Subject: [PATCH 07/26] perf(CCBV): better bitwise operations - a 8-bit popcount - simpler logic for LSB masks --- src/data/CCBV.ml | 99 ++++++++++++++++++++++++++++++++++++----------- src/data/CCBV.mli | 2 + 2 files changed, 78 insertions(+), 23 deletions(-) diff --git a/src/data/CCBV.ml b/src/data/CCBV.ml index f355203f..170bc367 100644 --- a/src/data/CCBV.ml +++ b/src/data/CCBV.ml @@ -22,27 +22,80 @@ let[@inline] mul_ n = n lsl 3 let zero = Char.unsafe_chr 0 -(** We use OCamls chars to store the bits. We index them from the - least significant bit. We create masks to zero out the most significant - bits that aren't used to store values. This is necessary when we are - constructing or negating a bit vector. *) -let[@inline] lsb_masks_ n = (1 lsl n) - 1 +(* 0b11111111 *) +let all_ones_ = Char.unsafe_chr ((1 lsl width_) - 1) -let all_ones_ = Char.unsafe_chr (lsb_masks_ width_) +let() = assert (all_ones_ = Char.chr 0b1111_1111) -let count_bits_ n = - let table = [| 0; 1; 1; 2; 1; 2; 2; 3; 1; 2; 2; 3; 2; 3; 3; 4; 1; 2; 2; 3; 2; 3; 3; 4; - 2; 3; 3; 4; 3; 4; 4; 5; 1; 2; 2; 3; 2; 3; 3; 4; 2; 3; 3; 4; 3; 4; 4; 5; - 2; 3; 3; 4; 3; 4; 4; 5; 3; 4; 4; 5; 4; 5; 5; 6; 1; 2; 2; 3; 2; 3; 3; 4; - 2; 3; 3; 4; 3; 4; 4; 5; 2; 3; 3; 4; 3; 4; 4; 5; 3; 4; 4; 5; 4; 5; 5; 6; - 2; 3; 3; 4; 3; 4; 4; 5; 3; 4; 4; 5; 4; 5; 5; 6; 3; 4; 4; 5; 4; 5; 5; 6; - 4; 5; 5; 6; 5; 6; 6; 7; 1; 2; 2; 3; 2; 3; 3; 4; 2; 3; 3; 4; 3; 4; 4; 5; - 2; 3; 3; 4; 3; 4; 4; 5; 3; 4; 4; 5; 4; 5; 5; 6; 2; 3; 3; 4; 3; 4; 4; 5; - 3; 4; 4; 5; 4; 5; 5; 6; 3; 4; 4; 5; 4; 5; 5; 6; 4; 5; 5; 6; 5; 6; 6; 7; - 2; 3; 3; 4; 3; 4; 4; 5; 3; 4; 4; 5; 4; 5; 5; 6; 3; 4; 4; 5; 4; 5; 5; 6; - 4; 5; 5; 6; 5; 6; 6; 7; 3; 4; 4; 5; 4; 5; 5; 6; 4; 5; 5; 6; 5; 6; 6; 7; - 4; 5; 5; 6; 5; 6; 6; 7; 5; 6; 6; 7; 6; 7; 7; 8; |] in - Array.unsafe_get table n +(* [lsb_mask_ n] is [0b111111] with [n] ones. *) +let[@inline] __lsb_mask n = (1 lsl n) - 1 + +(*$= & ~printer:CCInt.to_string + 0b0 (__lsb_mask 0) + 0b1 (__lsb_mask 1) + 0b11 (__lsb_mask 2) + 0b111 (__lsb_mask 3) + 0b1111 (__lsb_mask 4) + 0b1_1111 (__lsb_mask 5) + 0b11_1111 (__lsb_mask 6) + 0b111_1111 (__lsb_mask 7) + 0b1111_1111 (__lsb_mask 8) +*) + +(* + from https://en.wikipedia.org/wiki/Hamming_weight + + //This uses fewer arithmetic operations than any other known + //implementation on machines with slow multiplication. + //It uses 17 arithmetic operations. + int popcount_2(uint64_t x) { + x -= (x >> 1) & m1; //put count of each 2 bits into those 2 bits + x = (x & m2) + ((x >> 2) & m2); //put count of each 4 bits into those 4 bits + x = (x + (x >> 4)) & m4; //put count of each 8 bits into those 8 bits + + // not necessary for int8 + // x += x >> 8; //put count of each 16 bits into their lowest 8 bits + // x += x >> 16; //put count of each 32 bits into their lowest 8 bits + // x += x >> 32; //put count of each 64 bits into their lowest 8 bits + + return x & 0x7f; + } + + m1 = 0x5555555555555555 + m2 = 0x3333333333333333 + m4 = 0x0f0f0f0f0f0f0f0f +*) +let[@inline] __popcount8 (b:int) : int = + let m1 = 0x55 in + let m2 = 0x33 in + let m4 = 0x0f in + + let b = b - ((b lsr 1) land m1) in + let b = (b land m2) + ((b lsr 2) land m2) in + let b = (b + (b lsr 4)) land m4 in + b land 0x7f + +(*$inject + let popcount8_ref n = + let rec loop n = + if n=0 then 0 + else if (n land 1) = 0 then loop (n lsr 1) + else 1 + loop (n lsr 1) + in + loop n +*) + +(* test __popcount8 just to be sure. *) +(*$R + for i=0 to 255 do + let n = __popcount8 i in + let n2 = popcount8_ref i in + if n<>n2 then ( + Printf.printf "bad: i=%d => %d,%d\n" i n n2; + assert false + ); + done +*) (* Can I access the "private" members in testing? $Q (Q.int_bound (Sys.word_size - 1)) (fun i -> count_bits_ lsb_masks_.(i) = i) @@ -71,7 +124,7 @@ let create ~size default = (* adjust last bits *) let r = mod_ size in if default && r <> 0 then ( - Bytes.unsafe_set b (n-1) (Char.unsafe_chr (lsb_masks_ r)); + Bytes.unsafe_set b (n-1) (Char.unsafe_chr (__lsb_mask r)); ); { b; size } ) @@ -102,7 +155,7 @@ let cardinal bv = else ( let n = ref 0 in for i = 0 to Bytes.length bv.b - 1 do - n := !n + count_bits_ (get_ bv.b i) (* MSB of last element are all 0 *) + n := !n + __popcount8 (get_ bv.b i) (* MSB of last element are all 0 *) done; !n ) @@ -420,7 +473,7 @@ let negate_self b = let r = mod_ b.size in if r <> 0 then let l = Bytes.length b.b - 1 in - unsafe_set_ b.b l (lsb_masks_ r land (unsafe_get_ b.b l)) + unsafe_set_ b.b l (__lsb_mask r land (unsafe_get_ b.b l)) (*$= & ~printer:(CCFormat.to_string ppli) [0;3;4;6] (let v = of_list [1;2;5;7;] in negate_self v; to_sorted_list v) @@ -431,7 +484,7 @@ let negate a = let r = mod_ a.size in if r <> 0 then ( let l = Bytes.length a.b - 1 in - unsafe_set_ b l (lsb_masks_ r land (unsafe_get_ b l)) + unsafe_set_ b l (__lsb_mask r land (unsafe_get_ b l)) ); { b ; size = a.size } diff --git a/src/data/CCBV.mli b/src/data/CCBV.mli index 3a6bec70..e466b12b 100644 --- a/src/data/CCBV.mli +++ b/src/data/CCBV.mli @@ -152,4 +152,6 @@ val pp : Format.formatter -> t -> unit (**/**) val __to_word_l : t -> char list +val __popcount8 : int -> int +val __lsb_mask : int -> int (**/**) From 92463d33c50d1724e2fced20f025b25d9314b220 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 2 Jan 2022 21:56:33 -0500 Subject: [PATCH 08/26] perf(BV): make more functions inline, use raise_notrace --- src/data/CCBV.ml | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/src/data/CCBV.ml b/src/data/CCBV.ml index 170bc367..c3a13979 100644 --- a/src/data/CCBV.ml +++ b/src/data/CCBV.ml @@ -141,14 +141,14 @@ let create ~size default = create ~size:29 true |> to_sorted_list = CCList.range 0 28 *) -let copy bv = { bv with b = Bytes.copy bv.b } +let[@inline] copy bv = { bv with b = Bytes.copy bv.b } (*$Q (Q.list Q.small_int) (fun l -> \ let bv = of_list l in to_list bv = to_list (copy bv)) *) -let capacity bv = mul_ (Bytes.length bv.b) +let[@inline] capacity bv = mul_ (Bytes.length bv.b) let cardinal bv = if bv.size = 0 then 0 @@ -206,18 +206,18 @@ let resize bv size = let is_empty bv = try for i = 0 to Bytes.length bv.b - 1 do - if get_ bv.b i <> 0 then raise Exit + if get_ bv.b i <> 0 then raise_notrace Exit done; true with Exit -> false -let get bv i = +let[@inline] get bv i = if i < 0 then invalid_arg "get: negative index"; - let n = div_ i in - let i = mod_ i in - if n < Bytes.length bv.b - then (unsafe_get_ bv.b n) land (1 lsl i) <> 0 + let idx_bucket = div_ i in + let idx_in_byte = mod_ i in + if idx_bucket < Bytes.length bv.b + then (unsafe_get_ bv.b idx_bucket) land (1 lsl idx_in_byte) <> 0 else false (*$R @@ -236,13 +236,13 @@ let get bv i = assert_bool "1 must be false" (not (CCBV.get bv 1)); *) -let set bv i = +let[@inline] set bv i = if i < 0 then invalid_arg "set: negative index" else ( - let n = div_ i in - let j = mod_ i in + let idx_bucket = div_ i in + let idx_in_byte = mod_ i in if i >= bv.size then grow_ bv (i+1); - unsafe_set_ bv.b n ((unsafe_get_ bv.b n) lor (1 lsl j)) + unsafe_set_ bv.b idx_bucket ((unsafe_get_ bv.b idx_bucket) lor (1 lsl idx_in_byte)) ) (*$T @@ -250,7 +250,7 @@ let set bv i = let bv = create ~size:3 false in set bv 1; not (get bv 0) *) -let reset bv i = +let[@inline] reset bv i = if i < 0 then invalid_arg "reset: negative index" else ( let n = div_ i in @@ -443,7 +443,7 @@ exception FoundFirst of int let first_exn bv = try - iter_true bv (fun i -> raise (FoundFirst i)); + iter_true bv (fun i -> raise_notrace (FoundFirst i)); raise Not_found with FoundFirst i -> i @@ -607,8 +607,8 @@ let inter b1 b2 = assert_equal [3;4] l; *) -(* Underlying size depends on the 'in_' set for diff, so we don't change - it's size! *) +(* Underlying size depends on the [in_] set for diff, so we don't change + its size! *) let diff_into ~into bv = let n = min (Bytes.length into.b) (Bytes.length bv.b) in for i = 0 to n - 1 do @@ -642,7 +642,7 @@ let select bv arr = iter_true bv (fun i -> if i >= Array.length arr - then raise Exit + then raise_notrace Exit else l := arr.(i) :: !l) with Exit -> () end; @@ -661,7 +661,7 @@ let selecti bv arr = iter_true bv (fun i -> if i >= Array.length arr - then raise Exit + then raise_notrace Exit else l := (arr.(i), i) :: !l) with Exit -> () end; From 3d57a5c86eddc14dd6da5fcbc469d48e206c4833 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 2 Jan 2022 21:57:53 -0500 Subject: [PATCH 09/26] feat(CCBV): prevent `resize` from shrinking underlying array also add `BV.resize_minimize_memory` to force shrinking. This shouldn't be the default because it can allocate a lot in case of repeated shrinkings. --- src/data/CCBV.ml | 50 +++++++++++++++++++++++++++++++---------------- src/data/CCBV.mli | 12 +++++++++--- 2 files changed, 42 insertions(+), 20 deletions(-) diff --git a/src/data/CCBV.ml b/src/data/CCBV.ml index c3a13979..2215e60b 100644 --- a/src/data/CCBV.ml +++ b/src/data/CCBV.ml @@ -165,20 +165,28 @@ let cardinal bv = *) let really_resize_ bv ~desired ~current size = - let b = Bytes.make desired zero in - Bytes.blit bv.b 0 b 0 current; - bv.b <- b; - bv.size <- size + bv.size <- size; + if desired <> current then ( + let b = Bytes.make desired zero in + Bytes.blit bv.b 0 b 0 current; + bv.b <- b; + ) + +let[@inline never] grow_real_ bv size = + (* beyond capacity *) + let desired = bytes_length_of_size size in + let current = Bytes.length bv.b in + assert (desired > current); + really_resize_ bv ~desired ~current size let grow_ bv size = - if size <= capacity bv (* within capacity *) - then bv.size <- size - else ( - (* beyond capacity *) - let desired = bytes_length_of_size size in - let current = Bytes.length bv.b in - assert (desired > current); - really_resize_ bv ~desired ~current size + if size <= capacity bv then ( + (* within capacity *) + bv.size <- size + ) else ( + (* resize. This is a separate function so it's easier to + inline the happy path. *) + grow_real_ bv size ) let shrink_ bv size = @@ -188,11 +196,19 @@ let shrink_ bv size = let resize bv size = if size < 0 then invalid_arg "resize: negative size"; - if size < bv.size (* shrink *) - then shrink_ bv size - else if size = bv.size - then () - else grow_ bv size + if size < bv.size then ( + bv.size <- size; + ) else if size > bv.size then ( + grow_ bv size + ) + +let resize_minimize_memory bv size = + if size < 0 then invalid_arg "resize: negative size"; + if size < bv.size then ( + shrink_ bv size + ) else if size > bv.size then ( + grow_ bv size + ) (*$R let bv1 = CCBV.create ~size:87 true in diff --git a/src/data/CCBV.mli b/src/data/CCBV.mli index e466b12b..d00747c2 100644 --- a/src/data/CCBV.mli +++ b/src/data/CCBV.mli @@ -39,10 +39,16 @@ val capacity : t -> int @since 1.2 *) val resize : t -> int -> unit -(** Resize the BV so that it has the specified length. This can grow or shrink - the underlying bitvector. +(** Resize the BV so that it has the specified length. This can grow + the underlying array, but it will not shrink it, to minimize + memory traffic. + @raise Invalid_argument on negative sizes. *) - @raise Invalid_arg on negative sizes. *) +val resize_minimize_memory : t -> int -> unit +(** Same as {!resize}, but this can also shrink the underlying + array if this reduces the size. + @raise Invalid_argument on negative sizes. + @since NEXT_RELEASE *) val is_empty : t -> bool (** Are there any true bits? *) From 3960ea379205c724fe1855aafb56e64238902bd2 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 2 Jan 2022 21:58:45 -0500 Subject: [PATCH 10/26] feat(BV): add `set_bool` --- src/data/CCBV.ml | 3 +++ src/data/CCBV.mli | 4 ++++ 2 files changed, 7 insertions(+) diff --git a/src/data/CCBV.ml b/src/data/CCBV.ml index 2215e60b..9b89f201 100644 --- a/src/data/CCBV.ml +++ b/src/data/CCBV.ml @@ -279,6 +279,9 @@ let[@inline] reset bv i = let bv = create ~size:3 false in set bv 0; reset bv 0; not (get bv 0) *) +let[@inline] set_bool bv i b = + if b then set bv i else reset bv i + let flip bv i = if i < 0 then invalid_arg "reset: negative index" else ( diff --git a/src/data/CCBV.mli b/src/data/CCBV.mli index d00747c2..ba3864c3 100644 --- a/src/data/CCBV.mli +++ b/src/data/CCBV.mli @@ -62,6 +62,10 @@ val get : t -> int -> bool val reset : t -> int -> unit (** Set i-th bit to 0, extending the bitvector if needed. *) +val set_bool : t -> int -> bool -> unit +(** Set or reset [i]-th bit. + @since NEXT_RELEASE *) + val flip : t -> int -> unit (** Flip i-th bit, extending the bitvector if needed. *) From 2b5b2a0e02fcc000e66463ec620bbb1e88913c70 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 4 Jul 2022 14:35:32 -0400 Subject: [PATCH 11/26] chore: have `make test` be quiet --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index f70f36e6..600c94ca 100644 --- a/Makefile +++ b/Makefile @@ -6,7 +6,7 @@ build: dune build @install -p $(PACKAGES) test: build - dune runtest --cache=disabled --no-buffer --force + dune runtest --display=quiet --cache=disabled --no-buffer --force clean: dune clean From 856e73d2b2f5c279a2303fbfa576e5a17ef76903 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 4 Jul 2022 14:37:24 -0400 Subject: [PATCH 12/26] fix --- src/data/CCBV.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/CCBV.ml b/src/data/CCBV.ml index 47c29352..1ded6faa 100644 --- a/src/data/CCBV.ml +++ b/src/data/CCBV.ml @@ -144,7 +144,7 @@ let resize_minimize_memory bv size = let is_empty bv = try for i = 0 to Bytes.length bv.b - 1 do - if get_ bv.b i <> 1 then raise_notrace Exit + if get_ bv.b i <> 0 then raise_notrace Exit done; true with Exit -> false From cc55e4cdfb1592049810ab0066e9daa2e451fb8b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 4 Jul 2022 16:07:58 -0400 Subject: [PATCH 13/26] feat(testlib): optional name for all tests --- src/testlib/containers_testlib.ml | 62 ++++++++++++++++++------------ src/testlib/containers_testlib.mli | 11 ++++-- 2 files changed, 46 insertions(+), 27 deletions(-) diff --git a/src/testlib/containers_testlib.ml b/src/testlib/containers_testlib.ml index 12914132..be673507 100644 --- a/src/testlib/containers_testlib.ml +++ b/src/testlib/containers_testlib.ml @@ -7,7 +7,7 @@ type 'a print = 'a -> string module Test = struct type run = - | T of (unit -> bool) + | T of { prop: unit -> bool } | Eq : { eq: 'a eq option; print: 'a print option; lhs: 'a; rhs: 'a } -> run | Q : { count: int option; @@ -17,11 +17,16 @@ module Test = struct } -> run - type t = { run: run; __FILE__: string; n: int } + type t = { name: string option; run: run; __FILE__: string; n: int } (** Location for this test *) let str_loc (self : t) : string = - Printf.sprintf "(test :file '%s' :n %d)" self.__FILE__ self.n + let what = + match self.name with + | None -> "" + | Some f -> spf " :name %S" f + in + Printf.sprintf "(test :file '%s'%s :n %d)" self.__FILE__ what self.n [@@@ifge 4.08] @@ -38,12 +43,15 @@ module Test = struct let run ~seed (self : t) : _ result = match + let what = CCOption.map_or ~default:"" (fun s -> s ^ " ") self.name in match self.run with - | T f -> - if f () then - Ok () - else - Error "failed: returns false" + | T { prop } -> + let fail msg = Error (spf "%sfailed: %s" what msg) in + + (match prop () with + | exception e -> fail (spf "raised %s" (Printexc.to_string e)) + | true -> Ok () + | false -> fail "returns false") | Eq { eq; print; lhs; rhs } -> let eq = match eq with @@ -55,8 +63,9 @@ module Test = struct else ( let msg = match print with - | None -> "failed: not equal" - | Some p -> spf "failed: not equal:\nlhs=%s\nrhs=%s" (p lhs) (p rhs) + | None -> spf "%sfailed: not equal" what + | Some p -> + spf "%s failed: not equal:\nlhs=%s\nrhs=%s" what (p lhs) (p rhs) in Error msg ) @@ -97,18 +106,18 @@ module Test = struct | QCheck.TestResult.Success -> Ok () | QCheck.TestResult.Failed { instances } -> let msg = - Format.asprintf "@[failed on instances:@ %a@]" + Format.asprintf "@[%sfailed on instances:@ %a@]" what (Fmt.list ~sep:(Fmt.return ";@ ") pp_cex) instances in Error msg | QCheck.TestResult.Failed_other { msg } -> - let msg = spf "failed: %s" msg in + let msg = spf "%sfailed: %s" what msg in Error msg | QCheck.TestResult.Error { instance; exn; backtrace } -> let msg = - Format.asprintf "@[raised %s@ on instance %a@ :backtrace %s@]" - (Printexc.to_string exn) pp_cex instance backtrace + Format.asprintf "@[%sraised %s@ on instance %a@ :backtrace %s@]" + what (Printexc.to_string exn) pp_cex instance backtrace in Error msg) with @@ -119,11 +128,16 @@ end module type S = sig module Q = QCheck - val t : (unit -> bool) -> unit - val eq : ?cmp:'a eq -> ?printer:'a print -> 'a -> 'a -> unit + val t : ?name:string -> (unit -> bool) -> unit + val eq : ?name:string -> ?cmp:'a eq -> ?printer:'a print -> 'a -> 'a -> unit val q : - ?count:int -> ?long_factor:int -> 'a Q.arbitrary -> ('a -> bool) -> unit + ?name:string -> + ?count:int -> + ?long_factor:int -> + 'a Q.arbitrary -> + ('a -> bool) -> + unit val assert_equal : ?printer:('a -> string) -> ?cmp:('a -> 'a -> bool) -> 'a -> 'a -> unit @@ -144,18 +158,18 @@ struct let add_ t = all_ := t :: !all_ let n_ = ref 0 - let mk run : Test.t = + let mk ?name run : Test.t = let n = !n_ in incr n_; - { __FILE__ = X.file; n; run } + { __FILE__ = X.file; name; n; run } - let t f : unit = add_ @@ mk @@ Test.T f + let t ?name f : unit = add_ @@ mk ?name @@ Test.T { prop = f } - let eq ?cmp ?printer lhs rhs : unit = - add_ @@ mk @@ Test.Eq { eq = cmp; print = printer; lhs; rhs } + let eq ?name ?cmp ?printer lhs rhs : unit = + add_ @@ mk ?name @@ Test.Eq { eq = cmp; print = printer; lhs; rhs } - let q ?count ?long_factor arb prop : unit = - add_ @@ mk @@ Test.Q { arb; prop; count; long_factor } + let q ?name ?count ?long_factor arb prop : unit = + add_ @@ mk ?name @@ Test.Q { arb; prop; count; long_factor } let assert_equal ?printer ?(cmp = ( = )) x y : unit = if not @@ cmp x y then ( diff --git a/src/testlib/containers_testlib.mli b/src/testlib/containers_testlib.mli index 0e6aeff9..f910714e 100644 --- a/src/testlib/containers_testlib.mli +++ b/src/testlib/containers_testlib.mli @@ -8,11 +8,16 @@ end module type S = sig module Q = QCheck - val t : (unit -> bool) -> unit - val eq : ?cmp:'a eq -> ?printer:'a print -> 'a -> 'a -> unit + val t : ?name:string -> (unit -> bool) -> unit + val eq : ?name:string -> ?cmp:'a eq -> ?printer:'a print -> 'a -> 'a -> unit val q : - ?count:int -> ?long_factor:int -> 'a Q.arbitrary -> ('a -> bool) -> unit + ?name:string -> + ?count:int -> + ?long_factor:int -> + 'a Q.arbitrary -> + ('a -> bool) -> + unit val assert_equal : ?printer:('a -> string) -> ?cmp:('a -> 'a -> bool) -> 'a -> 'a -> unit From 090945c3f8383fe78bea37c276953cb38fe7e57a Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 4 Jul 2022 16:08:17 -0400 Subject: [PATCH 14/26] fix(BV): equal function --- src/data/CCBV.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/data/CCBV.ml b/src/data/CCBV.ml index 1ded6faa..ffcaecb1 100644 --- a/src/data/CCBV.ml +++ b/src/data/CCBV.ml @@ -196,7 +196,16 @@ let flip bv i = ) let clear bv = Bytes.fill bv.b 0 (Bytes.length bv.b) zero -let equal x y : bool = x.size = y.size && x.b = y.b + +let equal_bytes_ size b1 b2 = + try + for i = 0 to bytes_length_of_size size - 1 do + if Bytes.get b1 i <> Bytes.get b2 i then raise_notrace Exit + done; + true + with Exit -> false + +let equal x y : bool = x.size = y.size && equal_bytes_ x.size x.b y.b let iter bv f = let len = bytes_length_of_size bv.size in From 75fe196d3a40753e6115931dd9f23cfab31e61f0 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 4 Jul 2022 21:47:24 -0400 Subject: [PATCH 15/26] feat(testlib): optional arguments for `q` --- src/testlib/containers_testlib.ml | 35 ++++++++++++++++++++++++++---- src/testlib/containers_testlib.mli | 3 +++ 2 files changed, 34 insertions(+), 4 deletions(-) diff --git a/src/testlib/containers_testlib.ml b/src/testlib/containers_testlib.ml index be673507..f21d6644 100644 --- a/src/testlib/containers_testlib.ml +++ b/src/testlib/containers_testlib.ml @@ -14,6 +14,9 @@ module Test = struct arb: 'a Q.arbitrary; prop: 'a -> bool; long_factor: int option; + max_gen: int option; + max_fail: int option; + if_assumptions_fail: ([ `Fatal | `Warning ] * float) option; } -> run @@ -69,7 +72,16 @@ module Test = struct in Error msg ) - | Q { count; arb; prop; long_factor } -> + | Q + { + count; + arb; + prop; + long_factor; + max_fail; + max_gen; + if_assumptions_fail; + } -> (* create a random state from the seed *) let rand = let bits = @@ -80,7 +92,8 @@ module Test = struct let module Fmt = CCFormat in let cell = - Q.Test.make_cell ?count ?long_factor ~name:(str_loc self) arb prop + Q.Test.make_cell ?if_assumptions_fail ?max_gen ?max_fail ?count + ?long_factor ~name:(str_loc self) arb prop in let pp_cex out (cx : _ Q.TestResult.counter_ex) = @@ -135,6 +148,9 @@ module type S = sig ?name:string -> ?count:int -> ?long_factor:int -> + ?max_gen:int -> + ?max_fail:int -> + ?if_assumptions_fail:[ `Fatal | `Warning ] * float -> 'a Q.arbitrary -> ('a -> bool) -> unit @@ -168,8 +184,19 @@ struct let eq ?name ?cmp ?printer lhs rhs : unit = add_ @@ mk ?name @@ Test.Eq { eq = cmp; print = printer; lhs; rhs } - let q ?name ?count ?long_factor arb prop : unit = - add_ @@ mk ?name @@ Test.Q { arb; prop; count; long_factor } + let q ?name ?count ?long_factor ?max_gen ?max_fail ?if_assumptions_fail arb + prop : unit = + add_ @@ mk ?name + @@ Test.Q + { + arb; + prop; + count; + long_factor; + max_gen; + max_fail; + if_assumptions_fail; + } let assert_equal ?printer ?(cmp = ( = )) x y : unit = if not @@ cmp x y then ( diff --git a/src/testlib/containers_testlib.mli b/src/testlib/containers_testlib.mli index f910714e..d6211b64 100644 --- a/src/testlib/containers_testlib.mli +++ b/src/testlib/containers_testlib.mli @@ -15,6 +15,9 @@ module type S = sig ?name:string -> ?count:int -> ?long_factor:int -> + ?max_gen:int -> + ?max_fail:int -> + ?if_assumptions_fail:[ `Fatal | `Warning ] * float -> 'a Q.arbitrary -> ('a -> bool) -> unit From 60b9ece69eef3e9bdc8b644c8fa75c8b979f06a8 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 4 Jul 2022 21:47:39 -0400 Subject: [PATCH 16/26] feat(BV): correct many bugs, clarify parts of the API --- src/data/CCBV.ml | 148 +++++++++++++++++++++++++++------------------- src/data/CCBV.mli | 14 ++++- 2 files changed, 99 insertions(+), 63 deletions(-) diff --git a/src/data/CCBV.ml b/src/data/CCBV.ml index ffcaecb1..01cb632b 100644 --- a/src/data/CCBV.ml +++ b/src/data/CCBV.ml @@ -1,5 +1,3 @@ -(** {2 Imperative Bitvectors} *) - let width_ = 8 (* Helper functions *) @@ -52,6 +50,12 @@ let[@inline] __popcount8 (b : int) : int = let b = (b + (b lsr 4)) land m4 in b land 0x7f +(* + invariants for [v:t]: + + - [Bytes.length v.b >= div_ v.size] (enough storage) + - all bits above [size] are 0 in [v.b] +*) type t = { mutable b: bytes; mutable size: int } let length t = t.size @@ -76,22 +80,43 @@ let create ~size default = in (* adjust last bits *) let r = mod_ size in - if default && r <> 0 then - Bytes.unsafe_set b (n - 1) (Char.unsafe_chr (__lsb_mask r)); + if default && r <> 0 then unsafe_set_ b (n - 1) (__lsb_mask r); { b; size } ) -let[@inline] copy bv = { bv with b = Bytes.copy bv.b } +let copy bv = { bv with b = Bytes.sub bv.b 0 (bytes_length_of_size bv.size) } let[@inline] capacity bv = mul_ (Bytes.length bv.b) +(* call [f i width(byte[i]) (byte[i])] on each byte. + The last byte might have a width of less than 8. *) +let iter_bytes_ (b : t) ~f : unit = + for n = 0 to div_ b.size - 1 do + f (mul_ n) width_ (unsafe_get_ b.b n) + done; + let r = mod_ b.size in + if r <> 0 then ( + let last = div_ b.size in + f (mul_ last) r (__lsb_mask r land unsafe_get_ b.b last) + ) + +(* set [byte[i]] to [f(byte[i])] *) +let map_bytes_ (b : t) ~f : unit = + for n = 0 to div_ b.size - 1 do + unsafe_set_ b.b n (f (unsafe_get_ b.b n)) + done; + let r = mod_ b.size in + if r <> 0 then ( + let last = div_ b.size in + let mask = __lsb_mask r in + unsafe_set_ b.b last (mask land f (mask land unsafe_get_ b.b last)) + ) + let cardinal bv = if bv.size = 0 then 0 else ( let n = ref 0 in - for i = 0 to Bytes.length bv.b - 1 do - n := !n + __popcount8 (get_ bv.b i) (* MSB of last element are all 0 *) - done; + iter_bytes_ bv ~f:(fun _ _ b -> n := !n + __popcount8 b); !n ) @@ -99,10 +124,19 @@ let really_resize_ bv ~desired ~current size = bv.size <- size; if desired <> current then ( let b = Bytes.make desired zero in - Bytes.blit bv.b 0 b 0 current; + Bytes.blit bv.b 0 b 0 (min desired current); bv.b <- b ) +(* set bits above [n] to 0 *) +let[@inline never] clear_bits_above_ bv top = + let n = div_ top in + let j = mod_ top in + Bytes.fill bv.b (n + 1) + (bytes_length_of_size bv.size - n - 1) + (Char.unsafe_chr 0); + unsafe_set_ bv.b n (unsafe_get_ bv.b n land __lsb_mask j) + let[@inline never] grow_to_at_least_real_ bv size = (* beyond capacity *) let current = Bytes.length bv.b in @@ -123,15 +157,20 @@ let grow_to_at_least_ bv size = grow_to_at_least_real_ bv size let shrink_ bv size = - let desired = bytes_length_of_size size in - let current = Bytes.length bv.b in - really_resize_ bv ~desired ~current size + assert (size <= bv.size); + if size < bv.size then ( + let desired = bytes_length_of_size size in + let current = Bytes.length bv.b in + if desired = current then clear_bits_above_ bv size; + really_resize_ bv ~desired ~current size + ) let resize bv size = if size < 0 then invalid_arg "resize: negative size"; - if size < bv.size then + if size < bv.size then ( + clear_bits_above_ bv size; bv.size <- size - else if size > bv.size then + ) else if size > bv.size then grow_to_at_least_ bv size let resize_minimize_memory bv size = @@ -197,6 +236,10 @@ let flip bv i = let clear bv = Bytes.fill bv.b 0 (Bytes.length bv.b) zero +let clear_and_shrink bv = + clear bv; + bv.size <- 0 + let equal_bytes_ size b1 b2 = try for i = 0 to bytes_length_of_size size - 1 do @@ -208,31 +251,12 @@ let equal_bytes_ size b1 b2 = let equal x y : bool = x.size = y.size && equal_bytes_ x.size x.b y.b let iter bv f = - let len = bytes_length_of_size bv.size in - assert (len <= Bytes.length bv.b); - for n = 0 to len - 2 do - let j = mul_ n in - let word_n = unsafe_get_ bv.b n in - for i = 0 to width_ - 1 do - f (j + i) (word_n land (1 lsl i) <> 0) - done - done; - if bv.size > 0 then ( - let j = mul_ (len - 1) in - let r = mod_ bv.size in - let final_length = - if r = 0 then - width_ - else - r - in - let final_word = unsafe_get_ bv.b (len - 1) in - for i = 0 to final_length - 1 do - f (j + i) (final_word land (1 lsl i) <> 0) - done - ) + iter_bytes_ bv ~f:(fun off width_n word_n -> + for i = 0 to width_n - 1 do + f (off + i) (word_n land (1 lsl i) <> 0) + done) -let[@inline] iter_true bv f = +let iter_true bv f = iter bv (fun i b -> if b then f i @@ -248,7 +272,11 @@ let to_sorted_list bv = List.rev (to_list bv) (* Interpret these as indices. *) let of_list l = - let size = List.fold_left max 0 l + 1 in + let size = + match l with + | [] -> 0 + | _ -> List.fold_left max 0 l + 1 + in let bv = create ~size false in List.iter (fun i -> set bv i) l; bv @@ -263,30 +291,16 @@ let first_exn bv = let first bv = try Some (first_exn bv) with Not_found -> None let filter bv p = iter_true bv (fun i -> if not (p i) then reset bv i) - -let negate_self b = - let len = Bytes.length b.b in - for n = 0 to len - 1 do - unsafe_set_ b.b n (lnot (unsafe_get_ b.b n)) - done; - let r = mod_ b.size in - if r <> 0 then ( - let l = Bytes.length b.b - 1 in - unsafe_set_ b.b l (__lsb_mask r land unsafe_get_ b.b l) - ) +let negate_self bv = map_bytes_ bv ~f:(fun b -> lnot b) let negate a = - let b = Bytes.map (fun c -> Char.unsafe_chr (lnot (Char.code c))) a.b in - let r = mod_ a.size in - if r <> 0 then ( - let l = Bytes.length a.b - 1 in - unsafe_set_ b l (__lsb_mask r land unsafe_get_ b l) - ); - { b; size = a.size } + let b = copy a in + negate_self b; + b let union_into_no_resize_ ~into bv = - assert (Bytes.length into.b >= Bytes.length bv.b); - for i = 0 to Bytes.length bv.b - 1 do + assert (Bytes.length into.b >= bytes_length_of_size bv.size); + for i = 0 to bytes_length_of_size bv.size - 1 do unsafe_set_ into.b i (unsafe_get_ into.b i lor unsafe_get_ bv.b i) done @@ -308,8 +322,8 @@ let union b1 b2 = ) let inter_into_no_resize_ ~into bv = - assert (Bytes.length into.b <= Bytes.length bv.b); - for i = 0 to Bytes.length into.b - 1 do + assert (into.size <= bv.size); + for i = 0 to bytes_length_of_size into.size - 1 do unsafe_set_ into.b i (unsafe_get_ into.b i land unsafe_get_ bv.b i) done @@ -395,4 +409,16 @@ module Internal_ = struct let __popcount8 = __popcount8 let __lsb_mask = __lsb_mask + + let __check_invariant self = + let n = div_ self.size in + let j = mod_ self.size in + assert (Bytes.length self.b >= n); + if j > 0 then + assert ( + let c = get_ self.b n in + c land __lsb_mask j = c); + for i = n + 1 to Bytes.length self.b - 1 do + assert (get_ self.b i = 0) + done end diff --git a/src/data/CCBV.mli b/src/data/CCBV.mli index 1018d177..f49992e0 100644 --- a/src/data/CCBV.mli +++ b/src/data/CCBV.mli @@ -71,7 +71,11 @@ val flip : t -> int -> unit (** Flip i-th bit, extending the bitvector if needed. *) val clear : t -> unit -(** Set every bit to 0. *) +(** Set every bit to 0. Does not change the length. *) + +val clear_and_shrink : t -> unit +(** Set every bit to 0, and set length to 0. + @since NEXT_RELEASE *) val iter : t -> (int -> bool -> unit) -> unit (** Iterate on all bits. *) @@ -120,7 +124,12 @@ val union_into : into:t -> t -> unit val inter_into : into:t -> t -> unit (** [inter_into ~into bv] sets [into] to the intersection of itself and [bv]. - Also updates the length of [into] to be at most [length bv]. *) + Also updates the length of [into] to be at most [length bv]. + + After executing: + - [length ~into' = min (length into) (length bv)]. + - [for all i: get into' ==> get into i /\ get bv i] + *) val union : t -> t -> t (** [union bv1 bv2] returns the union of the two sets. *) @@ -166,6 +175,7 @@ module Internal_ : sig val __to_word_l : t -> char list val __popcount8 : int -> int val __lsb_mask : int -> int + val __check_invariant : t -> unit end (**/**) From 30cb40c71f5898a2c8bb5d052a15ef57d1335b24 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 4 Jul 2022 21:50:01 -0400 Subject: [PATCH 17/26] test: add strong tests for BV we use the classic QCheck construction with a random list of operations, and test: - internal invariant after each operation - same cardinal and content as reference implementation after each operation --- tests/data/t_bv.ml | 492 ++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 438 insertions(+), 54 deletions(-) diff --git a/tests/data/t_bv.ml b/tests/data/t_bv.ml index 979172ef..08026d13 100644 --- a/tests/data/t_bv.ml +++ b/tests/data/t_bv.ml @@ -3,15 +3,33 @@ open Test open CCBV open Internal_ -let ppli = CCFormat.(Dump.list int);; +let spf = Printf.sprintf +let ppli = CCFormat.(Dump.list int) + +module Intset = CCSet.Make (CCInt);; q (Q.pair Q.small_int Q.bool) (fun (size, b) -> create ~size b |> length = size) ;; -t @@ fun () -> create ~size:17 true |> cardinal = 17;; -t @@ fun () -> create ~size:32 true |> cardinal = 32;; -t @@ fun () -> create ~size:132 true |> cardinal = 132;; -t @@ fun () -> create ~size:200 false |> cardinal = 0;; -t @@ fun () -> create ~size:29 true |> to_sorted_list = CCList.range 0 28;; + +t ~name:(spf "line %d" __LINE__) @@ fun () -> +create ~size:17 true |> cardinal = 17 +;; + +t ~name:(spf "line %d" __LINE__) @@ fun () -> +create ~size:32 true |> cardinal = 32 +;; + +t ~name:(spf "line %d" __LINE__) @@ fun () -> +create ~size:132 true |> cardinal = 132 +;; + +t ~name:(spf "line %d" __LINE__) @@ fun () -> +create ~size:200 false |> cardinal = 0 +;; + +t ~name:(spf "line %d" __LINE__) @@ fun () -> +create ~size:29 true |> to_sorted_list = CCList.range 0 28 +;; q (Q.list Q.small_int) (fun l -> let bv = of_list l in @@ -20,7 +38,7 @@ q (Q.list Q.small_int) (fun l -> q Q.small_int (fun size -> create ~size true |> cardinal = size);; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv1 = CCBV.create ~size:87 true in assert_equal ~printer:string_of_int 87 (CCBV.cardinal bv1); true @@ -28,7 +46,7 @@ true q Q.small_int (fun n -> CCBV.cardinal (CCBV.create ~size:n true) = n);; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv = CCBV.create ~size:99 false in assert_bool "32 must be false" (not (CCBV.get bv 32)); assert_bool "88 must be false" (not (CCBV.get bv 88)); @@ -45,26 +63,26 @@ assert_bool "1 must be false" (not (CCBV.get bv 1)); true ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv = create ~size:3 false in set bv 0; get bv 0 ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv = create ~size:3 false in set bv 1; not (get bv 0) ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv = create ~size:3 false in set bv 0; reset bv 0; not (get bv 0) ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv = of_list [ 1; 10; 11; 30 ] in flip bv 10; assert_equal ~printer:Q.Print.(list int) [ 1; 11; 30 ] (to_sorted_list bv); @@ -84,7 +102,7 @@ assert_equal ~printer:Q.Print.bool true (get bv 100); true ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv = create ~size:37 true in cardinal bv = 37 && @@ -92,7 +110,7 @@ cardinal bv = 37 cardinal bv = 0) ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv = CCBV.of_list [ 1; 5; 200 ] in assert_equal ~printer:string_of_int 3 (CCBV.cardinal bv); CCBV.clear bv; @@ -101,13 +119,25 @@ assert_bool "must be empty" (CCBV.is_empty bv); true ;; -t @@ fun () -> equal (of_list [ 1; 3; 4 ]) (of_list [ 1; 3; 4 ]);; -t @@ fun () -> equal (empty ()) (empty ());; -t @@ fun () -> not (equal (empty ()) (of_list [ 1 ]));; -t @@ fun () -> not (equal (empty ()) (of_list [ 2; 5 ]));; -t @@ fun () -> not (equal (of_list [ 1; 3 ]) (of_list [ 2; 3 ]));; +t ~name:(spf "line %d" __LINE__) @@ fun () -> +equal (of_list [ 1; 3; 4 ]) (of_list [ 1; 3; 4 ]) +;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> equal (empty ()) (empty ());; + +t ~name:(spf "line %d" __LINE__) @@ fun () -> +not (equal (empty ()) (of_list [ 1 ])) +;; + +t ~name:(spf "line %d" __LINE__) @@ fun () -> +not (equal (empty ()) (of_list [ 2; 5 ])) +;; + +t ~name:(spf "line %d" __LINE__) @@ fun () -> +not (equal (of_list [ 1; 3 ]) (of_list [ 2; 3 ])) +;; + +t ~name:(spf "line %d" __LINE__) @@ fun () -> List.iter (fun size -> let bv = create ~size false in @@ -143,7 +173,7 @@ q List.length l = n && List.for_all (fun (_, b) -> b) l) ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> of_list [ 1; 5; 7 ] |> iter_true |> Iter.to_list |> List.sort CCOrd.poly = [ 1; 5; 7 ] @@ -158,7 +188,7 @@ q gen_bv (fun bv -> CCBV.cardinal bv = CCBV.cardinal bv') ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv = CCBV.of_list [ 1; 5; 156; 0; 222 ] in assert_equal ~printer:string_of_int 5 (CCBV.cardinal bv); CCBV.set bv 201; @@ -209,12 +239,23 @@ eq ~cmp:equal ~printer:(CCFormat.to_string pp) bv) ;; -t @@ fun () -> of_list [ 1; 32; 64 ] |> CCFun.flip get 64;; -t @@ fun () -> of_list [ 1; 32; 64 ] |> CCFun.flip get 32;; -t @@ fun () -> of_list [ 1; 31; 63 ] |> CCFun.flip get 63;; -t @@ fun () -> of_list [ 50; 10; 17; 22; 3; 12 ] |> first = Some 3;; +t ~name:(spf "line %d" __LINE__) @@ fun () -> +of_list [ 1; 32; 64 ] |> CCFun.flip get 64 +;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> +of_list [ 1; 32; 64 ] |> CCFun.flip get 32 +;; + +t ~name:(spf "line %d" __LINE__) @@ fun () -> +of_list [ 1; 31; 63 ] |> CCFun.flip get 63 +;; + +t ~name:(spf "line %d" __LINE__) @@ fun () -> +of_list [ 50; 10; 17; 22; 3; 12 ] |> first = Some 3 +;; + +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv = of_list [ 1; 2; 3; 4; 5; 6; 7 ] in filter bv (fun x -> x mod 2 = 0); to_sorted_list bv = [ 2; 4; 6 ] @@ -228,7 +269,7 @@ eq ~printer:(CCFormat.to_string ppli) [ 0; 3; 4; 6 ] q Q.small_int (fun size -> create ~size false |> negate |> cardinal = size);; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv1 = CCBV.of_list [ 1; 2; 3; 4 ] in let bv2 = CCBV.of_list [ 4; 200; 3 ] in let bv = CCBV.union bv1 bv2 in @@ -237,7 +278,20 @@ assert_equal ~printer:CCFormat.(to_string (Dump.list int)) [ 1; 2; 3; 4; 200 ] l true ;; -t @@ fun () -> +q ~name:"union" + Q.(pair (small_list small_nat) (small_list small_nat)) + (fun (l1, l2) -> + let bv1 = of_list l1 in + let bv2 = of_list l2 in + let l' = CCList.sort_uniq ~cmp:CCInt.compare (l1 @ l2) in + let bv = union bv1 bv2 in + let bv' = of_list l' in + if not (equal bv bv') then + Q.Test.fail_reportf "union (%a, %a) <> %a" ppli l1 ppli l2 ppli l'; + true) +;; + +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv1 = CCBV.of_list [ 1; 2; 3; 4; 64; 130 ] in let bv2 = CCBV.of_list [ 4; 64; 3; 120 ] in let bv = CCBV.union bv1 bv2 in @@ -247,7 +301,7 @@ assert_equal ~cmp:equal ~printer:(CCFormat.to_string pp) true ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv1 = CCBV.of_list [ 1; 2; 3; 4 ] in let bv2 = CCBV.of_list [ 4; 200; 3 ] in let bv = CCBV.union bv1 bv2 in @@ -257,7 +311,7 @@ assert_equal ~cmp:equal ~printer:(CCFormat.to_string pp) true ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> let v1 = CCBV.empty () in let () = CCBV.set v1 64 in let v2 = CCBV.diff (CCBV.empty ()) (CCBV.empty ()) in @@ -266,17 +320,17 @@ assert_equal ~printer:(CCFormat.to_string pp) ~cmp:CCBV.equal v1 v3; true ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> union (of_list [ 1; 2; 3; 4; 5 ]) (of_list [ 7; 3; 5; 6 ]) |> to_sorted_list = CCList.range 1 7 ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> inter (of_list [ 1; 2; 3; 4 ]) (of_list [ 2; 4; 6; 1 ]) |> to_sorted_list = [ 1; 2; 4 ] ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv1 = CCBV.of_list [ 1; 2; 3; 4; 200; 201 ] in let bv2 = CCBV.of_list [ 4; 200; 3 ] in let bv = CCBV.inter bv1 bv2 in @@ -285,7 +339,25 @@ assert_equal ~printer:CCFormat.(to_string (Dump.list int)) [ 3; 4; 200 ] l; true ;; -t @@ fun () -> +q ~name:"inter" ~count:10_000 + Q.(pair (small_list small_nat) (small_list small_nat)) + (fun (l1, l2) -> + let bv1 = of_list l1 in + let bv2 = of_list l2 in + let l' = CCList.inter ~eq:CCInt.equal l1 l2 in + let bv = inter bv1 bv2 in + let bv' = of_list l' in + (* make sure both are of the same length before comparing *) + let len = max (length bv) (length bv') in + resize bv len; + resize bv' len; + if not (equal bv bv') then + Q.Test.fail_reportf "inter (%a, %a) <> %a@ (@[bv= %a,@ bv'=%a@])" ppli + l1 ppli l2 ppli l' pp bv pp bv'; + true) +;; + +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv1 = CCBV.of_list [ 1; 2; 3; 4 ] in let bv2 = CCBV.of_list [ 4; 200; 3 ] in CCBV.inter_into ~into:bv1 bv2; @@ -294,33 +366,52 @@ assert_equal [ 3; 4 ] l; true ;; -t @@ fun () -> diff (of_list [ 1; 2; 3 ]) (of_list [ 1; 2; 3 ]) |> to_list = [] +t ~name:(spf "line %d" __LINE__) @@ fun () -> +diff (of_list [ 1; 2; 3 ]) (of_list [ 1; 2; 3 ]) |> to_list = [] ;; -t @@ fun () -> +q ~name:"diff" ~count:10_000 + Q.(pair (small_list small_nat) (small_list small_nat)) + (fun (l1, l2) -> + let bv1 = of_list l1 in + let bv2 = of_list l2 in + let bv = diff bv1 bv2 in + let l' = Intset.(diff (of_list l1) (of_list l2) |> to_list) in + let bv' = of_list l' in + (* make sure both are of the same length before comparing *) + let len = max (length bv) (length bv') in + resize bv len; + resize bv' len; + if not (equal bv bv') then + Q.Test.fail_reportf "idff (%a, %a) <> %a@ (@[bv= %a,@ bv'=%a@])" ppli + l1 ppli l2 ppli l' pp bv pp bv'; + true) +;; + +t ~name:(spf "line %d" __LINE__) @@ fun () -> diff (of_list [ 1; 2; 3 ]) (of_list [ 1; 2; 3; 4 ]) |> to_list = [] ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> diff (of_list [ 1; 2; 3; 4 ]) (of_list [ 1; 2; 3 ]) |> to_list = [ 4 ] ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> diff (of_list [ 1; 2; 3 ]) (of_list [ 1; 2; 3; 400 ]) |> to_list = [] ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> diff (of_list [ 1; 2; 3; 400 ]) (of_list [ 1; 2; 3 ]) |> to_list = [ 400 ] ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> let v1 = CCBV.empty () in set v1 65; let v2 = CCBV.diff v1 v1 in CCBV.is_empty v2 ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv = CCBV.of_list [ 1; 2; 5; 400 ] in let arr = [| "a"; "b"; "c"; "d"; "e"; "f" |] in let l = List.sort compare (CCBV.select bv arr) in @@ -328,7 +419,7 @@ assert_equal [ "b"; "c"; "f" ] l; true ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv = CCBV.of_list [ 1; 2; 5; 400 ] in let arr = [| "a"; "b"; "c"; "d"; "e"; "f" |] in let l = List.sort compare (CCBV.selecti bv arr) in @@ -351,7 +442,7 @@ q i = (to_iter bv |> Iter.length)) ;; -t @@ fun () -> +t ~name:(spf "line %d" __LINE__) @@ fun () -> CCList.range 0 10 |> CCList.to_iter |> of_iter |> to_iter |> CCList.of_iter |> List.sort CCOrd.poly = CCList.range 0 10 ;; @@ -383,13 +474,306 @@ let popcount8_ref n = ;; (* test __popcount8 just to be sure. *) -t @@ fun () -> -for i = 0 to 255 do - let n = __popcount8 i in - let n2 = popcount8_ref i in - if n <> n2 then ( - Printf.printf "bad: i=%d => %d,%d\n" i n n2; - assert false - ) -done; -true +t ~name:(spf "line %d" __LINE__) (fun () -> + for i = 0 to 255 do + let n = __popcount8 i in + let n2 = popcount8_ref i in + if n <> n2 then ( + Printf.printf "bad: i=%d => %d,%d\n" i n n2; + assert false + ) + done; + true) +;; + +t ~name:(spf "line %d" __LINE__) (fun () -> + let b = create ~size:10 false in + assert_equal 10 (length b); + set b 9; + for i = 0 to 9 do + assert (i = 9 || not (get b i)) + done; + + resize b 42; + assert_equal 42 (length b); + for i = 0 to 41 do + assert (i = 9 || not (get b i)) + done; + resize b 11; + assert_equal 11 (length b); + for i = 0 to 11 do + assert (i = 9 || not (get b i)) + done; + + true) +;; + +t ~name:(spf "line %d" __LINE__) (fun () -> + let v = empty () in + resize v 9; + inter_into ~into:v (of_list []); + true) +;; + +t ~name:(spf "line %d" __LINE__) (fun () -> + let bv = empty () in + flip bv 0; + resize bv 0; + negate_self bv; + union_into ~into:bv (of_list [ 2 ]); + assert_equal ~printer:(CCFormat.to_string ppli) [ 2 ] (to_list bv); + true) +;; + +t ~name:(spf "line %d" __LINE__) (fun () -> + let bv = empty () in + flip bv 0; + inter_into ~into:bv (of_list []); + negate_self bv; + assert_equal ~printer:(CCFormat.to_string ppli) [] (to_list bv); + true) + +module Op = struct + type t = + | Resize of int + | Set of int + | Reset of int + | Set_bool of int * bool + | Flip of int + | Clear + | Clear_and_shrink + | Filter_is_odd + | Negate + | Inter of int list + | Union of int list + + let apply (self : CCBV.t) (op : t) : unit = + match op with + | Resize n -> resize self n + | Set i -> set self i + | Reset i -> reset self i + | Set_bool (i, b) -> set_bool self i b + | Flip i -> flip self i + | Clear -> clear self + | Clear_and_shrink -> clear_and_shrink self + | Filter_is_odd -> filter self (fun i -> i mod 2 = 1) + | Negate -> negate_self self + | Inter l -> + let bv' = of_list l in + inter_into ~into:self bv' + | Union l -> + let bv' = of_list l in + union_into ~into:self bv' + + let post_size sz (self : t) = + match self with + | Resize i -> i + | Set j | Reset j | Set_bool (j, _) | Flip j -> max sz (j + 1) + | Clear -> sz + | Clear_and_shrink -> 0 + | Filter_is_odd | Negate -> sz + | Inter l | Union l -> List.fold_left max sz l + + let gen_ size : t Q.Gen.t = + let open Q.Gen in + let nonzero = + [ + (3, 0 -- size >|= fun x -> Set x); + (3, 0 -- size >|= fun x -> Reset x); + ( 3, + 0 -- size >>= fun x -> + bool >|= fun y -> Set_bool (x, y) ); + (3, 0 -- size >|= fun x -> Flip x); + ] + in + + (* random list of integers *) + let rand_list = + 0 -- 200 >>= fun n st -> + List.init n (fun i -> + if bool st then + Some i + else + None) + |> CCList.keep_some + in + + frequency + @@ List.flatten + [ + (if size > 0 then + nonzero + else + []); + [ + 1, return Clear; + 1, return Negate; + 1, return Filter_is_odd; + (1, rand_list >|= fun l -> Inter l); + (1, rand_list >|= fun l -> Union l); + (1, 0 -- 100 >|= fun x -> Resize x); + ]; + ] + + let shrink = + let open Q.Iter in + let module S = Q.Shrink in + function + | Resize i -> S.int i >|= fun i -> Resize i + | Set i -> S.int i >|= fun i -> Resize i + | Reset i -> S.int i >|= fun i -> Resize i + | Set_bool (i, b) -> + S.int i + >|= (fun i -> Set_bool (i, b)) + <+> + if b then + return @@ Set_bool (i, b) + else + empty + | Flip i -> S.int i >|= fun i -> Flip i + | Clear | Clear_and_shrink | Filter_is_odd | Negate -> empty + | Inter l -> S.list ~shrink:S.int l >|= fun l -> Inter l + | Union l -> S.list ~shrink:S.int l >|= fun l -> Union l + + let pp out = + let fpf = Format.fprintf in + function + | Resize i -> fpf out "resize %d" i + | Set i -> fpf out "set %d" i + | Reset i -> fpf out "reset %d" i + | Set_bool (i, b) -> fpf out "set_bool(%d,%b)" i b + | Flip i -> fpf out "flip %d" i + | Clear -> fpf out "clear" + | Clear_and_shrink -> fpf out "clear_and_shrink" + | Filter_is_odd -> fpf out "filter_is_odd" + | Negate -> fpf out "negate" + | Inter l -> fpf out "inter %a" CCFormat.(Dump.list int) l + | Union l -> fpf out "union %a" CCFormat.(Dump.list int) l + + let arb_l = + let rec gen_l sz n = + let open Q.Gen in + if n = 0 then + return [] + else + gen_ sz >>= fun op -> + let sz' = post_size sz op in + gen_l sz' (n - 1) >|= fun tl -> op :: tl + in + + Q.make + ~print:CCFormat.(to_string @@ Dump.list pp) + ~shrink:(Q.Shrink.list ~shrink) + Q.Gen.(0 -- 30 >>= fun len -> gen_l 0 len) +end + +module Ref_ = struct + type t = { mutable set: Intset.t; mutable size: int } + + let empty () = { size = 0; set = Intset.empty } + + let to_list self = + Intset.to_list self.set |> List.filter (fun x -> x < self.size) + + let pp out (self : t) = ppli out (to_list self) + + let equal_to_bv (self : t) (bv : CCBV.t) : bool = + to_list self = CCBV.to_sorted_list bv + + let cardinal self : int = + Intset.filter (fun x -> x < self.size) self.set |> Intset.cardinal + + let get (self : t) i = Intset.mem i self.set + + let rec apply_op (self : t) (op : Op.t) = + match op with + | Resize n -> + self.set <- Intset.filter (fun x -> x < n) self.set; + self.size <- n + | Set i -> + self.size <- max self.size (i + 1); + self.set <- Intset.add i self.set + | Reset i -> + self.size <- max self.size (i + 1); + self.set <- Intset.remove i self.set + | Set_bool (i, b) -> + apply_op self + (if b then + Set i + else + Reset i) + | Flip i -> + self.size <- max self.size (i + 1); + apply_op self + (if Intset.mem i self.set then + Reset i + else + Set i) + | Clear -> self.set <- Intset.empty + | Clear_and_shrink -> + self.set <- Intset.empty; + self.size <- 0 + | Filter_is_odd -> self.set <- Intset.filter (fun x -> x mod 2 = 1) self.set + | Negate -> + let l' = + List.init self.size (fun x -> x) + |> List.filter (fun x -> not (Intset.mem x self.set)) + in + self.set <- Intset.of_list l' + | Inter l -> + let s' = Intset.of_list l in + let sz' = List.fold_left (fun s x -> max s (x + 1)) 0 l in + self.size <- min self.size sz'; + self.set <- Intset.inter self.set s' + | Union l -> + let s' = Intset.of_list l in + self.size <- List.fold_left (fun s x -> max s (x + 1)) self.size l; + self.set <- Intset.union self.set s' +end +;; + +q ~name:"list ops: invariant" ~max_fail:1 ~count:20_000 Op.arb_l (fun ops -> + let bv = empty () in + + Internal_.__check_invariant bv; + List.iter + (fun op -> + Op.apply bv op; + Internal_.__check_invariant bv) + ops; + true) +;; + +q ~name:"list ops: compare to ref" ~max_fail:1 ~count:2_000 Op.arb_l (fun ops -> + let bv = empty () in + let bv' = Ref_.empty () in + + List.iter + (fun op -> + Op.apply bv op; + Ref_.apply_op bv' op; + + if cardinal bv <> Ref_.cardinal bv' then + Q.Test.fail_reportf + "@[different cardinal:@ actual=%a@ ref=%a@ @[actual.card \ + %d@]@ @[ref.cardinal %d@]@]" + pp bv Ref_.pp bv' (cardinal bv) (Ref_.cardinal bv'); + + let bad_idx = + Iter.(0 -- CCBV.length bv) + |> Iter.find_pred (fun i -> get bv i <> Ref_.get bv' i) + in + (match bad_idx with + | None -> () + | Some idx -> + Q.Test.fail_reportf + "at idx %d, not same `get`@ actual.get=%b,@ ref.get=%b" idx + (get bv idx) (Ref_.get bv' idx)); + + if not (Ref_.equal_to_bv bv' bv) then + Q.Test.fail_reportf + "@[not equal:@ actual=%a@ ref=%a@ @[actual.to_list@ %a@]@ \ + @[ref.to_list@ %a@]@]" + pp bv Ref_.pp bv' ppli (to_sorted_list bv) ppli (Ref_.to_list bv')) + ops; + true) From d9717095efeaf047d4c860ab77ce7040500b7f5b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 4 Jul 2022 22:04:40 -0400 Subject: [PATCH 18/26] improve doc for BV --- src/data/CCBV.ml | 6 ++++-- src/data/CCBV.mli | 22 +++++++++++++++------- 2 files changed, 19 insertions(+), 9 deletions(-) diff --git a/src/data/CCBV.ml b/src/data/CCBV.ml index 01cb632b..5b650f60 100644 --- a/src/data/CCBV.ml +++ b/src/data/CCBV.ml @@ -181,9 +181,11 @@ let resize_minimize_memory bv size = grow_to_at_least_ bv size let is_empty bv = + bv.size = 0 + || try - for i = 0 to Bytes.length bv.b - 1 do - if get_ bv.b i <> 0 then raise_notrace Exit + for i = 0 to bytes_length_of_size bv.size - 1 do + if unsafe_get_ bv.b i <> 0 then raise_notrace Exit done; true with Exit -> false diff --git a/src/data/CCBV.mli b/src/data/CCBV.mli index f49992e0..47dd4982 100644 --- a/src/data/CCBV.mli +++ b/src/data/CCBV.mli @@ -17,10 +17,11 @@ type t (** A resizable bitvector *) val empty : unit -> t -(** Empty bitvector. *) +(** Empty bitvector. Length is 0. *) val create : size:int -> bool -> t -(** Create a bitvector of given size, with given default value. *) +(** Create a bitvector of given size, with given default value. + Length of result is [size]. *) val copy : t -> t (** Copy of bitvector. *) @@ -108,15 +109,17 @@ val first_exn : t -> int val filter : t -> (int -> bool) -> unit (** [filter bv p] only keeps the true bits of [bv] whose [index] - satisfies [p index]. *) + satisfies [p index]. + Length is unchanged. *) val negate_self : t -> unit -(** [negate_self t] flips all of the bits in [t]. +(** [negate_self t] flips all of the bits in [t]. Length is unchanged. @since 1.2 *) val negate : t -> t -(** [negate t] returns a copy of [t] with all of the bits flipped. *) +(** [negate t] returns a copy of [t] with all of the bits flipped. + Length is unchanged. *) val union_into : into:t -> t -> unit (** [union_into ~into bv] sets [into] to the union of itself and [bv]. @@ -132,10 +135,12 @@ val inter_into : into:t -> t -> unit *) val union : t -> t -> t -(** [union bv1 bv2] returns the union of the two sets. *) +(** [union bv1 bv2] returns the union of the two sets. The length + of the result is the max of the inputs' lengths. *) val inter : t -> t -> t -(** [inter bv1 bv2] returns the intersection of the two sets. *) +(** [inter bv1 bv2] returns the intersection of the two sets. The length + of the result is the min of the inputs' lengths. *) val diff_into : into:t -> t -> unit (** [diff_into ~into t] modifies [into] with only the bits set but not in [t]. @@ -163,7 +168,10 @@ val equal : t -> t -> bool type 'a iter = ('a -> unit) -> unit val to_iter : t -> int iter +(** Iterate over the true bits. *) + val of_iter : int iter -> t +(** Build from true bits. *) val pp : Format.formatter -> t -> unit (** Print the bitvector as a string of bits. From e01b758de88bb7ab76222b3a7c3dc1f1ab2194cd Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 4 Jul 2022 22:04:50 -0400 Subject: [PATCH 19/26] more tests --- tests/data/t_bv.ml | 29 +++++++++++++++++++++++++---- 1 file changed, 25 insertions(+), 4 deletions(-) diff --git a/tests/data/t_bv.ml b/tests/data/t_bv.ml index 08026d13..ec0072d6 100644 --- a/tests/data/t_bv.ml +++ b/tests/data/t_bv.ml @@ -38,6 +38,10 @@ q (Q.list Q.small_int) (fun l -> q Q.small_int (fun size -> create ~size true |> cardinal = size);; +q Q.small_int (fun size -> + create ~size true |> to_sorted_list = List.init size CCFun.id) +;; + t ~name:(spf "line %d" __LINE__) @@ fun () -> let bv1 = CCBV.create ~size:87 true in assert_equal ~printer:string_of_int 87 (CCBV.cardinal bv1); @@ -536,6 +540,7 @@ t ~name:(spf "line %d" __LINE__) (fun () -> module Op = struct type t = | Resize of int + | Resize_min_mem of int | Set of int | Reset of int | Set_bool of int * bool @@ -546,10 +551,12 @@ module Op = struct | Negate | Inter of int list | Union of int list + | Diff of int list let apply (self : CCBV.t) (op : t) : unit = match op with | Resize n -> resize self n + | Resize_min_mem n -> resize_minimize_memory self n | Set i -> set self i | Reset i -> reset self i | Set_bool (i, b) -> set_bool self i b @@ -564,15 +571,22 @@ module Op = struct | Union l -> let bv' = of_list l in union_into ~into:self bv' + | Diff l -> + let bv' = of_list l in + diff_into ~into:self bv' let post_size sz (self : t) = match self with | Resize i -> i + | Resize_min_mem i -> i | Set j | Reset j | Set_bool (j, _) | Flip j -> max sz (j + 1) | Clear -> sz | Clear_and_shrink -> 0 | Filter_is_odd | Negate -> sz - | Inter l | Union l -> List.fold_left max sz l + | Diff _ -> sz + | Inter [] | Union [] -> sz + | Union l -> max sz (succ (List.fold_left max 0 l)) + | Inter l -> min sz (succ (List.fold_left max 0 l)) let gen_ size : t Q.Gen.t = let open Q.Gen in @@ -620,6 +634,7 @@ module Op = struct let module S = Q.Shrink in function | Resize i -> S.int i >|= fun i -> Resize i + | Resize_min_mem i -> S.int i >|= fun i -> Resize_min_mem i | Set i -> S.int i >|= fun i -> Resize i | Reset i -> S.int i >|= fun i -> Resize i | Set_bool (i, b) -> @@ -634,11 +649,13 @@ module Op = struct | Clear | Clear_and_shrink | Filter_is_odd | Negate -> empty | Inter l -> S.list ~shrink:S.int l >|= fun l -> Inter l | Union l -> S.list ~shrink:S.int l >|= fun l -> Union l + | Diff l -> S.list ~shrink:S.int l >|= fun l -> Diff l let pp out = let fpf = Format.fprintf in function | Resize i -> fpf out "resize %d" i + | Resize_min_mem i -> fpf out "resize_minimize_memory %d" i | Set i -> fpf out "set %d" i | Reset i -> fpf out "reset %d" i | Set_bool (i, b) -> fpf out "set_bool(%d,%b)" i b @@ -647,8 +664,9 @@ module Op = struct | Clear_and_shrink -> fpf out "clear_and_shrink" | Filter_is_odd -> fpf out "filter_is_odd" | Negate -> fpf out "negate" - | Inter l -> fpf out "inter %a" CCFormat.(Dump.list int) l - | Union l -> fpf out "union %a" CCFormat.(Dump.list int) l + | Inter l -> fpf out "inter %a" ppli l + | Union l -> fpf out "union %a" ppli l + | Diff l -> fpf out "diff %a" ppli l let arb_l = let rec gen_l sz n = @@ -687,7 +705,7 @@ module Ref_ = struct let rec apply_op (self : t) (op : Op.t) = match op with - | Resize n -> + | Resize n | Resize_min_mem n -> self.set <- Intset.filter (fun x -> x < n) self.set; self.size <- n | Set i -> @@ -729,6 +747,9 @@ module Ref_ = struct let s' = Intset.of_list l in self.size <- List.fold_left (fun s x -> max s (x + 1)) self.size l; self.set <- Intset.union self.set s' + | Diff l -> + let s' = Intset.of_list l in + self.set <- Intset.diff self.set s' end ;; From 36eb87db21089d7d89478c469205aaab493b7cd1 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 4 Jul 2022 22:09:14 -0400 Subject: [PATCH 20/26] fix(BV): clear bits properly --- src/data/CCBV.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/CCBV.ml b/src/data/CCBV.ml index 5b650f60..08b71c5f 100644 --- a/src/data/CCBV.ml +++ b/src/data/CCBV.ml @@ -161,7 +161,7 @@ let shrink_ bv size = if size < bv.size then ( let desired = bytes_length_of_size size in let current = Bytes.length bv.b in - if desired = current then clear_bits_above_ bv size; + clear_bits_above_ bv size; really_resize_ bv ~desired ~current size ) From b24feaf2d644d242a8709e270145d104f40148d2 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 4 Jul 2022 22:09:25 -0400 Subject: [PATCH 21/26] strong BV test --- tests/data/t_bv.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/tests/data/t_bv.ml b/tests/data/t_bv.ml index ec0072d6..6cf555e1 100644 --- a/tests/data/t_bv.ml +++ b/tests/data/t_bv.ml @@ -536,6 +536,14 @@ t ~name:(spf "line %d" __LINE__) (fun () -> negate_self bv; assert_equal ~printer:(CCFormat.to_string ppli) [] (to_list bv); true) +;; + +t ~name:(spf "line %d" __LINE__) (fun () -> + let v = empty () in + union_into ~into:v (of_list [ 9; 16 ]); + resize_minimize_memory v 9; + Internal_.__check_invariant v; + is_empty v) module Op = struct type t = @@ -621,11 +629,14 @@ module Op = struct []); [ 1, return Clear; + 1, return Clear_and_shrink; 1, return Negate; 1, return Filter_is_odd; (1, rand_list >|= fun l -> Inter l); (1, rand_list >|= fun l -> Union l); + (1, rand_list >|= fun l -> Diff l); (1, 0 -- 100 >|= fun x -> Resize x); + (1, 0 -- 100 >|= fun x -> Resize_min_mem x); ]; ] From e15971934d4a62be768483c4d50e2f6629c3918f Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 4 Jul 2022 22:15:06 -0400 Subject: [PATCH 22/26] feat(BV): add `init` --- src/data/CCBV.ml | 9 ++++++++- src/data/CCBV.mli | 5 +++++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/src/data/CCBV.ml b/src/data/CCBV.ml index 08b71c5f..2f624271 100644 --- a/src/data/CCBV.ml +++ b/src/data/CCBV.ml @@ -67,7 +67,7 @@ let bytes_length_of_size size = else div_ size + 1 -let create ~size default = +let create ~size default : t = if size = 0 then empty () else ( @@ -210,6 +210,13 @@ let[@inline] set bv i = (unsafe_get_ bv.b idx_bucket lor (1 lsl idx_in_byte)) ) +let init size f : t = + let v = create ~size false in + for i = 0 to size - 1 do + if f i then set v i + done; + v + let[@inline] reset bv i = if i < 0 then invalid_arg "reset: negative index" diff --git a/src/data/CCBV.mli b/src/data/CCBV.mli index 47dd4982..af726dd8 100644 --- a/src/data/CCBV.mli +++ b/src/data/CCBV.mli @@ -23,6 +23,11 @@ val create : size:int -> bool -> t (** Create a bitvector of given size, with given default value. Length of result is [size]. *) +val init : int -> (int -> bool) -> t +(** [init len f] initializes a bitvector of length [len], where bit [i] + is true iff [f i] is. + @since NEXT_RELEASE *) + val copy : t -> t (** Copy of bitvector. *) From feaa8ecf7dd6f4a680cfa7fe08e4a5eaf880003e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 4 Jul 2022 22:15:13 -0400 Subject: [PATCH 23/26] test BV.init --- tests/data/t_bv.ml | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/tests/data/t_bv.ml b/tests/data/t_bv.ml index 6cf555e1..f83433f7 100644 --- a/tests/data/t_bv.ml +++ b/tests/data/t_bv.ml @@ -519,6 +519,23 @@ t ~name:(spf "line %d" __LINE__) (fun () -> true) ;; +t ~name:(spf "line %d" __LINE__) (fun () -> + let l = [ 1; 3; 10; 29; 55 ] in + let v = init 120 (fun i -> List.mem i l) in + assert_equal ~printer:(CCFormat.to_string ppli) l (to_sorted_list v); + true) +;; + +q ~name:(spf "line %d" __LINE__) + Q.(small_list small_nat) + (fun l -> + let l = CCList.sort_uniq ~cmp:CCInt.compare l in + let max = 1 + List.fold_left max 0 l in + let v = init max (fun i -> List.mem i l) in + assert_equal ~printer:(CCFormat.to_string ppli) l (to_sorted_list v); + true) +;; + t ~name:(spf "line %d" __LINE__) (fun () -> let bv = empty () in flip bv 0; From 8b751754ba8e034fd3bafc6378c53bcf9fa07ac1 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 4 Jul 2022 22:16:46 -0400 Subject: [PATCH 24/26] test: compat 4.03 --- tests/data/t_bv.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/data/t_bv.ml b/tests/data/t_bv.ml index f83433f7..a37b0dad 100644 --- a/tests/data/t_bv.ml +++ b/tests/data/t_bv.ml @@ -39,7 +39,7 @@ q (Q.list Q.small_int) (fun l -> q Q.small_int (fun size -> create ~size true |> cardinal = size);; q Q.small_int (fun size -> - create ~size true |> to_sorted_list = List.init size CCFun.id) + create ~size true |> to_sorted_list = CCList.init size CCFun.id) ;; t ~name:(spf "line %d" __LINE__) @@ fun () -> @@ -225,7 +225,7 @@ q let l1 = bv |> to_sorted_list in let l2 = CCList.init (length bv) (get bv) - |> List.mapi (fun i b -> i, b) + |> CCList.mapi (fun i b -> i, b) |> CCList.filter_map (function | i, true -> Some i | _ -> None) @@ -629,7 +629,7 @@ module Op = struct (* random list of integers *) let rand_list = 0 -- 200 >>= fun n st -> - List.init n (fun i -> + CCList.init n (fun i -> if bool st then Some i else @@ -762,7 +762,7 @@ module Ref_ = struct | Filter_is_odd -> self.set <- Intset.filter (fun x -> x mod 2 = 1) self.set | Negate -> let l' = - List.init self.size (fun x -> x) + CCList.init self.size (fun x -> x) |> List.filter (fun x -> not (Intset.mem x self.set)) in self.set <- Intset.of_list l' From af77f371fd7cd8ea04b99d5e07c89d31a3740fae Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 5 Jul 2022 21:28:54 -0400 Subject: [PATCH 25/26] feat(testlib): allow ?long arg --- src/testlib/containers_testlib.ml | 13 +++++++++---- src/testlib/containers_testlib.mli | 4 +++- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/src/testlib/containers_testlib.ml b/src/testlib/containers_testlib.ml index f21d6644..63a7264f 100644 --- a/src/testlib/containers_testlib.ml +++ b/src/testlib/containers_testlib.ml @@ -44,7 +44,7 @@ module Test = struct [@@@endif] - let run ~seed (self : t) : _ result = + let run ?(long = false) ~seed (self : t) : _ result = match let what = CCOption.map_or ~default:"" (fun s -> s ^ " ") self.name in match self.run with @@ -113,7 +113,7 @@ module Test = struct in (* TODO: if verbose, print stats, etc. *) - let res = Q.Test.check_cell ~rand cell in + let res = Q.Test.check_cell ~long ~rand cell in (match get_state res with | QCheck.TestResult.Success -> Ok () @@ -229,7 +229,12 @@ let make ~__FILE__ () : (module S) = let getenv_opt s = try Some (Sys.getenv s) with _ -> None -let run_all ?seed:seed_hex ~descr (l : Test.t list list) : unit = +let long = + match getenv_opt "LONG" with + | Some ("true" | "1") -> true + | _ -> false + +let run_all ?seed:seed_hex ?(long = long) ~descr (l : Test.t list list) : unit = let start = Unix.gettimeofday () in (* generate or parse seed *) @@ -264,7 +269,7 @@ let run_all ?seed:seed_hex ~descr (l : Test.t list list) : unit = NOTE: we probably want this to be silent? Format.printf "> run %s@." (Test.str_loc t); *) - match Test.run ~seed t with + match Test.run ~long ~seed t with | Ok () -> () | Error msg -> Format.printf "FAILED: %s@." (Test.str_loc t); diff --git a/src/testlib/containers_testlib.mli b/src/testlib/containers_testlib.mli index d6211b64..adebb0c7 100644 --- a/src/testlib/containers_testlib.mli +++ b/src/testlib/containers_testlib.mli @@ -32,4 +32,6 @@ module type S = sig end val make : __FILE__:string -> unit -> (module S) -val run_all : ?seed:string -> descr:string -> Test.t list list -> unit + +val run_all : + ?seed:string -> ?long:bool -> descr:string -> Test.t list list -> unit From b7d19e9dc575a94f1ca53a5cab2dc22c61a70b2d Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 5 Jul 2022 21:29:03 -0400 Subject: [PATCH 26/26] test --- tests/data/t_bv.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/tests/data/t_bv.ml b/tests/data/t_bv.ml index a37b0dad..1d0428c9 100644 --- a/tests/data/t_bv.ml +++ b/tests/data/t_bv.ml @@ -781,7 +781,8 @@ module Ref_ = struct end ;; -q ~name:"list ops: invariant" ~max_fail:1 ~count:20_000 Op.arb_l (fun ops -> +q ~name:"list ops: invariant" ~max_fail:1 ~long_factor:10 ~count:20_000 Op.arb_l + (fun ops -> let bv = empty () in Internal_.__check_invariant bv; @@ -793,7 +794,8 @@ q ~name:"list ops: invariant" ~max_fail:1 ~count:20_000 Op.arb_l (fun ops -> true) ;; -q ~name:"list ops: compare to ref" ~max_fail:1 ~count:2_000 Op.arb_l (fun ops -> +q ~name:"list ops: compare to ref" ~max_fail:1 ~long_factor:10 ~count:2_000 + Op.arb_l (fun ops -> let bv = empty () in let bv' = Ref_.empty () in