Support for Bit Vectors

benchmarks/BV/cegar2.sl

@@ -0,0 +1,19 @@
+(set-logic BV)
+
+(synth-inv inv-f ((x (_ BitVec 32))(n (_ BitVec 32))(m (_ BitVec 32)))
+ )
+
+(define-fun pre-f ((x (_ BitVec 32))(n (_ BitVec 32))(m (_ BitVec 32))) Bool
+    (and (= x #x00000000) (= m #x00000000))
+)
+
+(define-fun trans-f ((x (_ BitVec 32))(n (_ BitVec 32))(m (_ BitVec 32))(x! (_ BitVec 32))(n! (_ BitVec 32))(m! (_ BitVec 32))) Bool
+    (or (and (and (and (bvult x n) (= x! (bvadd x #x00000001))) (= n! n)) (= m! m)) (and (and (and (bvult x n) (= x! (bvadd x #x00000001))) (= n! n)) (= m! x)))
+)
+
+(define-fun post-f ((x (_ BitVec 32))(n (_ BitVec 32))(m (_ BitVec 32))) Bool
+    (not (and (and (bvuge x n) (bvugt n #x00000000)) (or (bvule n m) (bvult m #x00000000))))
+)
+
+(inv-constraint inv-f pre-f trans-f post-f)
+(check-synth)

src/BitVecComponents.ml

@@ -0,0 +1,95 @@
+open Base
+open Exceptions
+open Expr
+
+let all = [
+    {
+      name = "bv-eq";
+      codomain = Type.BOOL;
+      domain = [Type.BITVEC (-1); Type.BITVEC (-1)];
+      is_argument_valid = (function
+                           | _ -> true);
+      evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] ->
+                    Value.Bool ((BitarrayExt.compare v1 v2) = 0));
+      to_string = (fun [@warning "-8"] [v1;v2] -> "(= " ^ v1 ^ " " ^ v2 ^ ")");
+      global_constraints = (fun _ -> []);
+    } ;
+    {
+      name = "bvnot";
+      codomain = Type.BITVEC (-1);
+      domain = [Type.BITVEC (-1)];
+      is_argument_valid = (function
+                             | _ -> true);
+      evaluate = (function [@warning "-8"] [Value.BitVec v] -> Value.BitVec (BitarrayExt.bvnot v));
+      to_string = (fun [@warning "-8"] [a] -> "(bvnot " ^ a ^ ")");
+      global_constraints = (fun _ -> []);
+    } ;
+    {
+      name = "bvult";
+      codomain = Type.BOOL;
+      domain = [Type.BITVEC (-1); Type.BITVEC (-1)];
+      is_argument_valid = (function
+                           | _ -> true);
+      evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] ->
+                    Value.Bool (BitarrayExt.bvult v1 v2));
+      to_string = (fun [@warning "-8"] [a ; b] -> "(bvult " ^ a ^ " " ^ b ^ ")");
+      global_constraints = (fun _ -> []);
+    } ;
+    {
+      name = "bvadd";
+      codomain = Type.BITVEC (-1);
+      domain = [Type.BITVEC (-1); Type.BITVEC (-1)];
+      is_argument_valid = (function
+                           | _ -> true);
+      evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] ->
+                    Value.BitVec (BitarrayExt.add v1 v2));
+      to_string = (fun [@warning "-8"] [a ; b] -> "(bvadd " ^ a ^ " " ^ b ^ ")");
+      global_constraints = (fun _ -> []);
+    } ;
+    {
+      name = "bvuge";
+      codomain = Type.BOOL;
+      domain = [Type.BITVEC (-1); Type.BITVEC (-1)];
+      is_argument_valid = (function
+                           | _ -> true);
+      evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] ->
+                    Value.Bool (BitarrayExt.bvuge v1 v2));
+      to_string = (fun [@warning "-8"] [a ; b] -> "(bvuge " ^ a ^ " " ^ b ^ ")");
+      global_constraints = (fun _ -> []);
+    } ;
+    {
+      name = "bvugt";
+      codomain = Type.BOOL;
+      domain = [Type.BITVEC (-1); Type.BITVEC (-1)];
+      is_argument_valid = (function
+                           | _ -> true);
+      evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] ->
+                    Value.Bool (BitarrayExt.bvugt v1 v2));
+      to_string = (fun [@warning "-8"] [a ; b] -> "(bvugt " ^ a ^ " " ^ b ^ ")");
+      global_constraints = (fun _ -> []);
+    } ;
+    {
+      name = "bvule";
+      codomain = Type.BOOL;
+      domain = [Type.BITVEC (-1); Type.BITVEC (-1)];
+      is_argument_valid = (function
+                           | _ -> true);
+      evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] ->
+                    Value.Bool (BitarrayExt.bvule v1 v2));
+      to_string = (fun [@warning "-8"] [a ; b] -> "(bvule " ^ a ^ " " ^ b ^ ")");
+      global_constraints = (fun _ -> []);
+    } ;
+    {
+      name = "bvsub";
+      codomain = Type.BITVEC (-1);
+      domain = [Type.BITVEC (-1); Type.BITVEC (-1)];
+      is_argument_valid = (function
+                           | _ -> true);
+      evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] ->
+                    Value.BitVec (BitarrayExt.bvsub v1 v2));
+      to_string = (fun [@warning "-8"] [a ; b] -> "(bvsub " ^ a ^ " " ^ b ^ ")");
+      global_constraints = (fun _ -> []);
+    }
+  ]
+
+let levels = [| all |]

src/Bitarray.ml

@@ -6,11 +6,10 @@
  *  - https://discuss.ocaml.org/t/ann-v0-12-release-of-jane-street-packages/3499/7
  *  - https://github.com/janestreet/core_extended/issues/22
  *)
-
 open Core
 
-(* a single 63 bit chunk of the array, bounds checking is left to the main module.
-   We can only use 62 bits, because of the sign bit *)
+(* a single 63 bit chunk of the array, bounds checking is left to the main module. We can
+   only use 62 bits, because of the sign bit *)
 module Int63_chunk : sig
   type t
 
@@ -23,34 +22,37 @@ end = struct
   type t = Int63.t
 
   let empty = zero
-
   let get t i = bit_and t (shift_left one i) > zero
 
   let set t i v =
-    if v then bit_or t (shift_left one i)
+    if v
+    then bit_or t (shift_left one i)
     else bit_and t (bit_xor minus_one (shift_left one i))
+  ;;
 end
 
-type t = {
-  data: Int63_chunk.t Array.t;
-  length: int
-}
+type t =
+  { data : Int63_chunk.t Array.t
+  ; length : int
+  }
 
 (* We can't use the sign bit, so we only get to use 62 bits *)
 let bits_per_bucket = 62
 
 let create sz =
-  if sz < 0 || sz > (Array.max_length * bits_per_bucket) then
-    invalid_argf "invalid size" ();
-  { data = Array.create ~len:(1 + (sz / bits_per_bucket)) Int63_chunk.empty;
-    length = sz }
+  if sz < 0 || sz > Array.max_length * bits_per_bucket
+  then invalid_argf "invalid size" ();
+  { data = Array.create ~len:(1 + (sz / bits_per_bucket)) Int63_chunk.empty
+  ; length = sz
+  }
 ;;
 
+let length t = t.length
 let bucket i = i / bits_per_bucket
 let index i = i mod bits_per_bucket
+
 let bounds_check t i =
-  if i < 0 || i >= t.length then
-    invalid_argf "Bitarray: out of bounds" ();
+  if i < 0 || i >= t.length then invalid_argf "Bitarray: out of bounds" ()
 ;;
 
 let get t i =
@@ -64,25 +66,19 @@ let set t i v =
   t.data.(bucket) <- Int63_chunk.set t.data.(bucket) (index i) v
 ;;
 
-let clear t =
-  Array.fill t.data ~pos:0 ~len:(Array.length t.data) Int63_chunk.empty
-;;
+let clear t = Array.fill t.data ~pos:0 ~len:(Array.length t.data) Int63_chunk.empty
 
 let fold =
   let rec loop t n ~init ~f =
-    if n < t.length then
-      loop t (n + 1) ~init:(f init (get t n)) ~f
-    else
-      init
+    if n < t.length then loop t (n + 1) ~init:(f init (get t n)) ~f else init
   in
   fun t ~init ~f -> loop t 0 ~init ~f
 ;;
 
 let iter t ~f = fold t ~init:() ~f:(fun _ v -> f v)
 
 let sexp_of_t t =
-  Array.sexp_of_t Bool.sexp_of_t
-    (Array.init t.length ~f:(fun i -> get t i))
+  Array.sexp_of_t Bool.sexp_of_t (Array.init t.length ~f:(fun i -> get t i))
 ;;
 
 let t_of_sexp sexp =