From bb985c0d6d84b7c5e2e6a3e4d6c916ef02b5bfab Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Sat, 16 Nov 2019 19:00:14 -0800 Subject: [PATCH 01/18] Parsing of bitvector types. --- src/SyGuS.ml | 1 + src/Type.ml | 7 +++++++ src/Value.ml | 10 ++++++++-- 3 files changed, 16 insertions(+), 2 deletions(-) diff --git a/src/SyGuS.ml b/src/SyGuS.ml index 5b5de94..ad9737b 100644 --- a/src/SyGuS.ml +++ b/src/SyGuS.ml @@ -60,6 +60,7 @@ let rec extract_consts : Sexp.t -> Value.t list = function let parse_variable_declaration : Sexp.t -> var = function | List [ Atom v ; Atom t ] -> (v, (Type.of_string t)) + | List [ Atom v ; List [Atom "_"; Atom "BitVec"; Atom n]] -> (v, (Type.of_params ("BitVec", (int_of_string n)))) | sexp -> raise (Parse_Exn ("Invalid variable usage: " ^ (Sexp.to_string_hum sexp))) let parse_define_fun : Sexp.t list -> func * Value.t list = function diff --git a/src/Type.ml b/src/Type.ml index 02d3024..fbbe675 100644 --- a/src/Type.ml +++ b/src/Type.ml @@ -1,3 +1,4 @@ +open Base open Exceptions type t = INT @@ -5,6 +6,7 @@ type t = INT | CHAR | STRING | LIST + | BITVEC of int [@@deriving sexp] let of_string : string -> t = function @@ -13,11 +15,16 @@ let of_string : string -> t = function | "Char" -> CHAR | "String" -> STRING | "List" -> LIST + (* | "BitVec" -> BITVEC *) | s -> raise (Parse_Exn ("Could not parse type `" ^ s ^ "`.")) +let of_params : string * int -> t = function + | "BitVec", n -> BITVEC n + let to_string : t -> string = function | INT -> "Int" | BOOL -> "Bool" | CHAR -> "Char" | STRING -> "String" | LIST -> "List" + | BITVEC n -> "(_ BitVec " ^ (Int.to_string_hum n) ^ ")" diff --git a/src/Value.ml b/src/Value.ml index 3f219ee..18bade9 100644 --- a/src/Value.ml +++ b/src/Value.ml @@ -8,6 +8,7 @@ module T = struct | Char of char | String of string | List of t list + | BitVec of int*int [@@deriving compare,sexp] end @@ -20,6 +21,7 @@ let typeof : t -> Type.t = function | Char _ -> Type.CHAR | String _ -> Type.STRING | List _ -> Type.LIST + | BitVec (n, _) -> Type.BITVEC n let to_string : t -> string = function | Int i -> Int.to_string i @@ -27,6 +29,7 @@ let to_string : t -> string = function | Char c -> "\'" ^ (Char.to_string c) ^ "\'" | String s -> "\"" ^ s ^ "\"" | List _ -> raise (Internal_Exn "List type (de/)serialization not implemented!") + | BitVec _ -> raise (Internal_Exn "BitVec type (de/)serialization not implemented!") let of_string (s : string) : t = try @@ -37,6 +40,9 @@ let of_string (s : string) : t = Char (Char.of_string (String.(chop_suffix_exn ~suffix:"\'" (chop_prefix_exn ~prefix:"\'" s)))) with Invalid_argument _ -> try - String String.(chop_suffix_exn ~suffix:"\"" (chop_prefix_exn ~prefix:"\"" s)) + String String.(chop_suffix_exn ~suffix:"\"" (chop_prefix_exn ~prefix:"\"" s)) + with Invalid_argument _ -> try + String s with Invalid_argument _ -> - raise (Parse_Exn ("Failed to parse value `" ^ s ^ "`.")) \ No newline at end of file + raise (Parse_Exn ("Failed to parse value `" ^ s ^ "`.")) + (* TODO: Implement BitVec from string. *) From 65216ba65e5b801f2be2f047a5fa52fa46f32ef8 Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Sun, 17 Nov 2019 13:29:54 -0800 Subject: [PATCH 02/18] Add the Bitvector type to functions which accept Type.t as input --- src/TestGen.ml | 1 + src/Type.ml | 2 +- src/Value.ml | 2 +- 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/TestGen.ml b/src/TestGen.ml index 6dec2e2..77c15e4 100644 --- a/src/TestGen.ml +++ b/src/TestGen.ml @@ -13,3 +13,4 @@ let for_type (t : Type.t) : Value.t Generator.t = >>= fun len -> (String.gen_with_length len (Char.gen_print) >>= fun s -> singleton (Value.String s)) | Type.LIST -> raise (Exceptions.Internal_Exn "Generators for List type not implemented!") + | Type.BITVEC _ -> raise (Exceptions.Internal_Exn "Generators for BitVec type not implemented!") diff --git a/src/Type.ml b/src/Type.ml index fbbe675..bc81941 100644 --- a/src/Type.ml +++ b/src/Type.ml @@ -21,7 +21,7 @@ let of_string : string -> t = function let of_params : string * int -> t = function | "BitVec", n -> BITVEC n -let to_string : t -> string = function +let to_string : t -> string = function [@warning "-8"] | INT -> "Int" | BOOL -> "Bool" | CHAR -> "Char" diff --git a/src/Value.ml b/src/Value.ml index 18bade9..8d57dd6 100644 --- a/src/Value.ml +++ b/src/Value.ml @@ -8,7 +8,7 @@ module T = struct | Char of char | String of string | List of t list - | BitVec of int*int + | BitVec of int*string [@@deriving compare,sexp] end From df78d32f97596755d300c0047d4f8ffb8f9a21af Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Tue, 26 Nov 2019 12:14:58 -0800 Subject: [PATCH 03/18] Use the Bitarray module instead of a string for bit vectors --- src/Value.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Value.ml b/src/Value.ml index 8d57dd6..7fb7955 100644 --- a/src/Value.ml +++ b/src/Value.ml @@ -8,7 +8,7 @@ module T = struct | Char of char | String of string | List of t list - | BitVec of int*string + | BitVec of int * BitArray.t [@@deriving compare,sexp] end From 2ccc228fcc0b2b46816232849a0679a806c2970e Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Mon, 16 Dec 2019 11:25:50 -0800 Subject: [PATCH 04/18] Add BitVecComponents.ml which implements bvadd, bvult, and bvnot, and add QF_BV to the supported logics --- src/BitVecComponents.ml | 45 ++++++++++++ src/Bitarray.ml | 159 +++++++++++++++++++++++++++++++++++++++- src/Logic.ml | 13 +++- src/Value.ml | 24 +++--- 4 files changed, 229 insertions(+), 12 deletions(-) create mode 100644 src/BitVecComponents.ml diff --git a/src/BitVecComponents.ml b/src/BitVecComponents.ml new file mode 100644 index 0000000..721eb9f --- /dev/null +++ b/src/BitVecComponents.ml @@ -0,0 +1,45 @@ +open Base +open Exceptions +open Expr + +let all = [ + { + name = "bv-eq"; + codomain = Type.BOOL; + domain = [Type.BITVEC _; Type.BITVEC _]; + is_argument_valid = (fun _ -> true); + evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> + Value.Bool ((not (Bitarray.bvult v1 v2)) && (not (Bitarray.bvult v2 v1)))); + to_string = (fun [@warning "-8"] [v1;v2] -> "(= " ^ v1 ^ " " ^ v2 ^ ")"); + global_constraints = (fun _ -> []); + } ; + { + name = "bvnot"; + codomain = Type.BITVEC _; + domain = [Type.BITVEC _]; + is_argument_valid = (fun _ -> true); + evaluate = (function [@warning "-8"] [Value.BitVec v] -> Value.BitVec (Bitarray.bvnot v)); + to_string = (fun [@warning "-8"] [a] -> "(bvnot " ^ a ^ ")"); + global_constraints = (fun _ -> []); + } ; + { + name = "bvult"; + codomain = Type.BOOL; + domain = [Type.BITVEC _; Type.BITVEC _]; + is_argument_valid = (fun _ -> true); + evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> + Value.Bool (Bitarray.bvult v1 v2)); + to_string = (fun [@warning "-8"] [a ; b] -> "(bvult " ^ a ^ " " ^ b ^ ")"); + global_constraints = (fun _ -> []); + } ; + { + name = "bvadd"; + codomain = Type.BITVEC _; + domain = [Type.BITVEC _; Type.BITVEC _]; + is_argument_valid = (fun _ -> true); + evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> + Value.BitVec (Bitarray.add v1 v2)); + to_string = (fun [@warning "-8"] [a ; b] -> "(bvadd " ^ a ^ " " ^ b ^ ")"); + global_constraints = (fun _ -> []); + } + ] diff --git a/src/Bitarray.ml b/src/Bitarray.ml index b18b400..795f94f 100644 --- a/src/Bitarray.ml +++ b/src/Bitarray.ml @@ -78,6 +78,16 @@ let fold = fun t ~init ~f -> loop t 0 ~init ~f ;; +let foldl2 = + let rec loop t1 t2 n ~init ~f = + if n < t1.length && n >= 0 then + loop t1 t2 (n + 1) ~init:(f init (get t1 n) (get t2 n)) ~f + else + init + in + fun t1 t2 ~init ~f -> loop t1 t2 0 ~init ~f +;; + let iter t ~f = fold t ~init:() ~f:(fun _ v -> f v) let sexp_of_t t = @@ -90,4 +100,151 @@ let t_of_sexp sexp = let t = create (Array.length a) in Array.iteri a ~f:(fun i v -> set t i v); t -;; \ No newline at end of file +;; + +(* Currently only supporting binary to bits *) +let of_string s = match String.prefix s 2 with + | "#b" -> + let bv = create (String.length (String.drop_prefix s 2)) in + let rec loop s bv i = if i >= 0 + then match s with + | '0'::t -> set bv i false; loop t bv (i - 1) + | '1'::t -> set bv i true; loop t bv (i - 1) + else + bv in + loop (String.to_list (String.drop_prefix s 2)) bv ((String.length (String.drop_prefix s 2)) - 1) + | "#x" -> + let bv = create ((String.length (String.drop_prefix s 2)) * 4) in + let n = ((String.length (String.drop_prefix s 2)) - 1) in + let rec loop s bv i = if i <= n + then match s with + | '0'::t -> set bv (i * 4) false; + set bv ((i * 4) + 1) false; + set bv ((i * 4) + 2) false; + set bv ((i * 4) + 3) false; + loop t bv (i + 1) + | '1'::t -> set bv (i * 4) true; + set bv ((i * 4) + 1) false; + set bv ((i * 4) + 2) false; + set bv ((i * 4) + 3) false; + loop t bv (i + 1) + | '2'::t -> set bv (i * 4) false; + set bv ((i * 4) + 1) true; + set bv ((i * 4) + 2) false; + set bv ((i * 4) + 3) false; + loop t bv (i + 1) + | '3'::t -> set bv (i * 4) true; + set bv ((i * 4) + 1) true; + set bv ((i * 4) + 2) false; + set bv ((i * 4) + 3) false; + loop t bv (i + 1) + | '4'::t -> set bv (i * 4) false; + set bv ((i * 4) + 1) false; + set bv ((i * 4) + 2) true; + set bv ((i * 4) + 3) false; + loop t bv (i + 1) + | '5'::t -> set bv (i * 4) true; + set bv ((i * 4) + 1) false; + set bv ((i * 4) + 2) true; + set bv ((i * 4) + 3) false; + loop t bv (i + 1) + | '6'::t -> set bv (i * 4) false; + set bv ((i * 4) + 1) true; + set bv ((i * 4) + 2) true; + set bv ((i * 4) + 3) false; + loop t bv (i + 1) + | '7'::t -> set bv (i * 4) true; + set bv ((i * 4) + 1) true; + set bv ((i * 4) + 2) true; + set bv ((i * 4) + 3) false; + loop t bv (i + 1) + | '8'::t -> set bv (i * 4) false; + set bv ((i * 4) + 1) false; + set bv ((i * 4) + 2) false; + set bv ((i * 4) + 3) true; + loop t bv (i + 1) + | '9'::t -> set bv (i * 4) true; + set bv ((i * 4) + 1) false; + set bv ((i * 4) + 2) false; + set bv ((i * 4) + 3) true; + loop t bv (i + 1) + | 'a'::t -> set bv (i * 4) false; + set bv ((i * 4) + 1) true; + set bv ((i * 4) + 2) false; + set bv ((i * 4) + 3) true; + loop t bv (i + 1) + | 'b'::t -> set bv (i * 4) true; + set bv ((i * 4) + 1) true; + set bv ((i * 4) + 2) false; + set bv ((i * 4) + 3) true; + loop t bv (i + 1) + | 'c'::t -> set bv (i * 4) false; + set bv ((i * 4) + 1) false; + set bv ((i * 4) + 2) true; + set bv ((i * 4) + 3) true; + loop t bv (i + 1) + | 'd'::t -> set bv (i * 4) true; + set bv ((i * 4) + 1) false; + set bv ((i * 4) + 2) true; + set bv ((i * 4) + 3) true; + loop t bv (i + 1) + | 'e'::t -> set bv (i * 4) false; + set bv ((i * 4) + 1) true; + set bv ((i * 4) + 2) true; + set bv ((i * 4) + 3) true; + loop t bv (i + 1) + | 'f'::t -> set bv (i * 4) true; + set bv ((i * 4) + 1) true; + set bv ((i * 4) + 2) true; + set bv ((i * 4) + 3) true; + loop t bv (i + 1) + else + bv in + loop (String.to_list (String.rev (String.drop_prefix s 2))) bv 0 + + +;; + +let to_string bv = "#b" ^ (fold bv ~init:"" ~f:(fun acc -> function + | false -> "0" ^ acc + | true -> "1" ^ acc)) +;; + +(* Does not support adding different sizes. *) +let rec add bv1 bv2 = + let sum = create bv1.length in + let s, _, _ = foldl2 bv1 bv2 ~init:(sum, 0, 0) ~f:(fun (sum, carry, ind) v1 v2 -> + match v1, v2 with + | true, true -> if phys_equal carry 1 then (set sum ind true; (sum, 1, ind + 1)) + else (set sum ind false; (sum, 1, ind + 1)) + | false, true | true, false -> if phys_equal carry 1 then (set sum ind false; (sum, 1, ind + 1)) + else (set sum ind true; (sum, 0, ind + 1)) + | false, false -> if phys_equal carry 1 then (set sum ind true; (sum, 0, ind + 1)) + else (set sum ind false; (sum, 0, ind + 1))) in + s +;; + +let bvnot bv = + let bv_new, _ = fold bv ~init:(bv, 0) ~f:(fun (bv, i) v -> + if phys_equal v true then (set bv i false; (bv, i + 1)) + else (set bv i true; (bv, i + 1))) in + bv_new + +;; + +let compare bv1 bv2 = + let rec helper ind bv1 bv2 = + if ind >= 0 then + let v1 = get bv1 ind in + let v2 = get bv2 ind in + if phys_equal v1 v2 then helper (ind - 1) bv1 bv2 + else if phys_equal v1 false then -1 else 1 + else + 0 + in + helper (bv1.length - 1) bv1 bv2 +;; + +let bvult bv1 bv2 = + let c = compare bv1 bv2 in + if c > 0 then false else true diff --git a/src/Logic.ml b/src/Logic.ml index 84149aa..7a81b35 100644 --- a/src/Logic.ml +++ b/src/Logic.ml @@ -29,7 +29,18 @@ let all_supported = (BooleanComponents.all @ IntegerComponents.peano) ; |] ; sample_set_size_multiplier = 8 - }] + } ; { + name = "QF_BV" ; + components_per_level = [| + (BitVecComponents.all @ BooleanComponents.all @ IntegerComponents.equality) ; + (BitVecComponents.all @ BooleanComponents.all @ IntegerComponents.intervals) ; + (BitVecComponents.all @ BooleanComponents.all @ IntegerComponents.octagons) ; + (BitVecComponents.all @ BooleanComponents.all @ IntegerComponents.polyhedra) ; + (BitVecComponents.all @ BooleanComponents.all @ IntegerComponents.polynomials) ; + (BitVecComponents.all @ BooleanComponents.all @ IntegerComponents.peano) ; + |] ; + sample_set_size_multiplier = 8 + }] ; table let of_string name = String.Table.find_exn all_supported name diff --git a/src/Value.ml b/src/Value.ml index 7fb7955..9cc7d35 100644 --- a/src/Value.ml +++ b/src/Value.ml @@ -2,13 +2,15 @@ open Base open Exceptions +module Bitarray = Bitarray + module T = struct type t = Int of int | Bool of bool | Char of char | String of string | List of t list - | BitVec of int * BitArray.t + | BitVec of Bitarray.t [@@deriving compare,sexp] end @@ -21,7 +23,7 @@ let typeof : t -> Type.t = function | Char _ -> Type.CHAR | String _ -> Type.STRING | List _ -> Type.LIST - | BitVec (n, _) -> Type.BITVEC n + | BitVec bv -> Type.BITVEC bv.length let to_string : t -> string = function | Int i -> Int.to_string i @@ -29,20 +31,22 @@ let to_string : t -> string = function | Char c -> "\'" ^ (Char.to_string c) ^ "\'" | String s -> "\"" ^ s ^ "\"" | List _ -> raise (Internal_Exn "List type (de/)serialization not implemented!") - | BitVec _ -> raise (Internal_Exn "BitVec type (de/)serialization not implemented!") + | BitVec bv -> Bitarray.to_string bv let of_string (s : string) : t = try Int (Int.of_string s) with Failure _ -> try - Bool (Bool.of_string s) + Bool (Bool.of_string s) + with Invalid_argument _ -> try + Char (Char.of_string (String.(chop_suffix_exn ~suffix:"\'" + (chop_prefix_exn ~prefix:"\'" s)))) with Invalid_argument _ -> try - Char (Char.of_string (String.(chop_suffix_exn ~suffix:"\'" - (chop_prefix_exn ~prefix:"\'" s)))) + BitVec (Bitarray.of_string s) with Invalid_argument _ -> try String String.(chop_suffix_exn ~suffix:"\"" (chop_prefix_exn ~prefix:"\"" s)) - with Invalid_argument _ -> try - String s - with Invalid_argument _ -> + with Invalid_argument _ -> try + String s + with Invalid_argument _ -> raise (Parse_Exn ("Failed to parse value `" ^ s ^ "`.")) - (* TODO: Implement BitVec from string. *) + From 828e319e921a560e12dff8e1493d808807a52117 Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Mon, 16 Dec 2019 11:31:42 -0800 Subject: [PATCH 05/18] Remove unnecessary comment --- src/Bitarray.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Bitarray.ml b/src/Bitarray.ml index 795f94f..dfcd716 100644 --- a/src/Bitarray.ml +++ b/src/Bitarray.ml @@ -102,7 +102,6 @@ let t_of_sexp sexp = t ;; -(* Currently only supporting binary to bits *) let of_string s = match String.prefix s 2 with | "#b" -> let bv = create (String.length (String.drop_prefix s 2)) in From 4ac1c2a95fe8266aaa4d431979b1adb55a0a945e Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Tue, 17 Dec 2019 12:53:10 -0800 Subject: [PATCH 06/18] Add the is_argument_valid functions for bitvectors --- src/BitVecComponents.ml | 16 ++++++++---- src/Bitarray.ml | 58 ++++++++++++++++++++++++++++------------- 2 files changed, 51 insertions(+), 23 deletions(-) diff --git a/src/BitVecComponents.ml b/src/BitVecComponents.ml index 721eb9f..df27c3f 100644 --- a/src/BitVecComponents.ml +++ b/src/BitVecComponents.ml @@ -1,13 +1,15 @@ open Base open Exceptions -open Expr - +open Expr + let all = [ { name = "bv-eq"; codomain = Type.BOOL; domain = [Type.BITVEC _; Type.BITVEC _]; - is_argument_valid = (fun _ -> true); + is_argument_valid = (function + | [a ; b] -> a.length = b.length + | _ -> false); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> Value.Bool ((not (Bitarray.bvult v1 v2)) && (not (Bitarray.bvult v2 v1)))); to_string = (fun [@warning "-8"] [v1;v2] -> "(= " ^ v1 ^ " " ^ v2 ^ ")"); @@ -26,7 +28,9 @@ let all = [ name = "bvult"; codomain = Type.BOOL; domain = [Type.BITVEC _; Type.BITVEC _]; - is_argument_valid = (fun _ -> true); + is_argument_valid = (function + | [a ; b] -> a.length = b.length + | _ -> false); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> Value.Bool (Bitarray.bvult v1 v2)); to_string = (fun [@warning "-8"] [a ; b] -> "(bvult " ^ a ^ " " ^ b ^ ")"); @@ -36,7 +40,9 @@ let all = [ name = "bvadd"; codomain = Type.BITVEC _; domain = [Type.BITVEC _; Type.BITVEC _]; - is_argument_valid = (fun _ -> true); + is_argument_valid = (function + | [a ; b] -> a.length = b.length + | _ -> false); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> Value.BitVec (Bitarray.add v1 v2)); to_string = (fun [@warning "-8"] [a ; b] -> "(bvadd " ^ a ^ " " ^ b ^ ")"); diff --git a/src/Bitarray.ml b/src/Bitarray.ml index dfcd716..5489003 100644 --- a/src/Bitarray.ml +++ b/src/Bitarray.ml @@ -68,6 +68,7 @@ let clear t = Array.fill t.data ~pos:0 ~len:(Array.length t.data) Int63_chunk.empty ;; +(* Applies f to index 0, then index 1, ...*) let fold = let rec loop t n ~init ~f = if n < t.length then @@ -78,9 +79,9 @@ let fold = fun t ~init ~f -> loop t 0 ~init ~f ;; -let foldl2 = +let fold2 = let rec loop t1 t2 n ~init ~f = - if n < t1.length && n >= 0 then + if n < t1.length then loop t1 t2 (n + 1) ~init:(f init (get t1 n) (get t2 n)) ~f else init @@ -102,19 +103,26 @@ let t_of_sexp sexp = t ;; -let of_string s = match String.prefix s 2 with +(* A bitarray created from the string "#b00011" will be represented by + the bitarray with index 0 set to true, index 1 to true, index 2 to + false, etc.*) +let of_string s = + let prefix = String.prefix s 2 in + let numeral = String.drop_prefix s 2 in + let bvsize = String.length numeral in + match prefix with | "#b" -> - let bv = create (String.length (String.drop_prefix s 2)) in + let bv = create bvsize in let rec loop s bv i = if i >= 0 then match s with | '0'::t -> set bv i false; loop t bv (i - 1) | '1'::t -> set bv i true; loop t bv (i - 1) else bv in - loop (String.to_list (String.drop_prefix s 2)) bv ((String.length (String.drop_prefix s 2)) - 1) + loop (String.to_list numeral) bv (bvsize - 1) | "#x" -> - let bv = create ((String.length (String.drop_prefix s 2)) * 4) in - let n = ((String.length (String.drop_prefix s 2)) - 1) in + let bv = create (bvsize * 4) in + let n = (bvsize - 1) in let rec loop s bv i = if i <= n then match s with | '0'::t -> set bv (i * 4) false; @@ -199,26 +207,28 @@ let of_string s = match String.prefix s 2 with loop t bv (i + 1) else bv in - loop (String.to_list (String.rev (String.drop_prefix s 2))) bv 0 - - + loop (String.to_list (String.rev numeral)) bv 0 ;; +(* TODO: If the length of the bitvector is a multiple of 4, represent with hex.*) let to_string bv = "#b" ^ (fold bv ~init:"" ~f:(fun acc -> function - | false -> "0" ^ acc - | true -> "1" ^ acc)) + | false -> "0" ^ acc + | true -> "1" ^ acc)) ;; -(* Does not support adding different sizes. *) let rec add bv1 bv2 = let sum = create bv1.length in - let s, _, _ = foldl2 bv1 bv2 ~init:(sum, 0, 0) ~f:(fun (sum, carry, ind) v1 v2 -> + let s, _, _ = fold2 bv1 bv2 ~init:(sum, 0, 0) ~f:(fun (sum, carry, ind) v1 v2 -> match v1, v2 with - | true, true -> if phys_equal carry 1 then (set sum ind true; (sum, 1, ind + 1)) + | true, true -> if phys_equal carry 1 + then (set sum ind true; (sum, 1, ind + 1)) else (set sum ind false; (sum, 1, ind + 1)) - | false, true | true, false -> if phys_equal carry 1 then (set sum ind false; (sum, 1, ind + 1)) - else (set sum ind true; (sum, 0, ind + 1)) - | false, false -> if phys_equal carry 1 then (set sum ind true; (sum, 0, ind + 1)) + | false, true + | true, false -> if phys_equal carry 1 + then (set sum ind false; (sum, 1, ind + 1)) + else (set sum ind true; (sum, 0, ind + 1)) + | false, false -> if phys_equal carry 1 + then (set sum ind true; (sum, 0, ind + 1)) else (set sum ind false; (sum, 0, ind + 1))) in s ;; @@ -247,3 +257,15 @@ let compare bv1 bv2 = let bvult bv1 bv2 = let c = compare bv1 bv2 in if c > 0 then false else true +;; + +let concat bv1 bv2 = + let bv3 = create (bv1.length + bv2.length) in + let bv1_, _ = fold bv1 ~init:(bv3, bv2.length) ~f:(fun (bv, i) v -> + set bv i v; (bv, i+1)) in + let bv12, _ = fold bv2 ~init:(bv1_, 0) ~f:(fun (bv, i) v -> + set bv i v; (bv, i+1)) in + bv12 +;; + + From e8eaf73388b31c307c8ad8af276feb28b7cc89cd Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Sat, 18 Jan 2020 14:08:38 -0800 Subject: [PATCH 07/18] Change BITVEC type to use TVAR for its size and correctly unify + The TVAR type stores the string representation of the bitvector's size. Two bitvectors will unify if they have the same size. + More operations on bitvectors were added to BitVecComponents.ml and to Bitarray.ml. --- src/BitVecComponents.ml | 60 +++++++++++++++++++++++++++++++++++------ src/Bitarray.ml | 32 ++++++++++++++++++---- src/Synthesizer.ml | 14 +++++++--- src/Type.ml | 8 +++--- src/Value.ml | 2 +- 5 files changed, 95 insertions(+), 21 deletions(-) diff --git a/src/BitVecComponents.ml b/src/BitVecComponents.ml index 5e33d50..1d7b957 100644 --- a/src/BitVecComponents.ml +++ b/src/BitVecComponents.ml @@ -6,18 +6,18 @@ let all = [ { name = "bv-eq"; codomain = Type.BOOL; - domain = [Type.TVAR "T1"; Type.TVAR "T1"]; + domain = [Type.BITVEC (Type.TVAR "T1"); Type.BITVEC (Type.TVAR "T1")]; is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> - Value.Bool ((not (Bitarray.bvult v1 v2)) && (not (Bitarray.bvult v2 v1)))); + Value.Bool ((Bitarray.compare v1 v2) = 0)); to_string = (fun [@warning "-8"] [v1;v2] -> "(= " ^ v1 ^ " " ^ v2 ^ ")"); global_constraints = (fun _ -> []); } ; { name = "bvnot"; - codomain = Type.TVAR "T1"; - domain = [Type.TVAR "T1"]; + codomain = Type.BITVEC (Type.TVAR "T1"); + domain = [Type.BITVEC (Type.TVAR "T1")]; is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v] -> Value.BitVec (Bitarray.bvnot v)); @@ -27,7 +27,7 @@ let all = [ { name = "bvult"; codomain = Type.BOOL; - domain = [Type.TVAR "T1"; Type.TVAR "T1"]; + domain = [Type.BITVEC (Type.TVAR "T1"); Type.BITVEC (Type.TVAR "T1")]; is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> @@ -37,15 +37,59 @@ let all = [ } ; { name = "bvadd"; - codomain = Type.TVAR "T1"; - domain = [Type.TVAR "T1"; Type.TVAR "T1"]; + codomain = Type.BITVEC (Type.TVAR "T1"); + domain = [Type.BITVEC (Type.TVAR "T1"); Type.BITVEC (Type.TVAR "T1")]; is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> Value.BitVec (Bitarray.add v1 v2)); to_string = (fun [@warning "-8"] [a ; b] -> "(bvadd " ^ a ^ " " ^ b ^ ")"); global_constraints = (fun _ -> []); - } + } ; + { + name = "bvuge"; + codomain = Type.BOOL; + domain = [Type.BITVEC (Type.TVAR "T1"); Type.BITVEC (Type.TVAR "T1")]; + is_argument_valid = (function + | _ -> true); + evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> + Value.Bool (Bitarray.bvuge v1 v2)); + to_string = (fun [@warning "-8"] [a ; b] -> "(bvuge " ^ a ^ " " ^ b ^ ")"); + global_constraints = (fun _ -> []); + } ; + { + name = "bvugt"; + codomain = Type.BOOL; + domain = [Type.BITVEC (Type.TVAR "T1"); Type.BITVEC (Type.TVAR "T1")]; + is_argument_valid = (function + | _ -> true); + evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> + Value.Bool (Bitarray.bvugt v1 v2)); + to_string = (fun [@warning "-8"] [a ; b] -> "(bvugt " ^ a ^ " " ^ b ^ ")"); + global_constraints = (fun _ -> []); + } ; + { + name = "bvule"; + codomain = Type.BOOL; + domain = [Type.BITVEC (Type.TVAR "T1"); Type.BITVEC (Type.TVAR "T1")]; + is_argument_valid = (function + | _ -> true); + evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> + Value.Bool (Bitarray.bvule v1 v2)); + to_string = (fun [@warning "-8"] [a ; b] -> "(bvule " ^ a ^ " " ^ b ^ ")"); + global_constraints = (fun _ -> []); + } ; + { + name = "bvsub"; + codomain = Type.BITVEC (Type.TVAR "T1"); + domain = [Type.BITVEC (Type.TVAR "T1"); Type.BITVEC (Type.TVAR "T1")]; + is_argument_valid = (function + | _ -> true); + evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> + Value.BitVec (Bitarray.bvsub v1 v2)); + to_string = (fun [@warning "-8"] [a ; b] -> "(bvsub " ^ a ^ " " ^ b ^ ")"); + global_constraints = (fun _ -> []); + } ] let levels = [| all |] diff --git a/src/Bitarray.ml b/src/Bitarray.ml index 5489003..ec908d9 100644 --- a/src/Bitarray.ml +++ b/src/Bitarray.ml @@ -17,6 +17,8 @@ module Int63_chunk : sig val empty : t val get : t -> int -> bool val set : t -> int -> bool -> t + val gen_incl : Int63.t -> Int63.t -> t Core_kernel.Quickcheck.Generator.t + end = struct open Int63 @@ -29,6 +31,8 @@ end = struct let set t i v = if v then bit_or t (shift_left one i) else bit_and t (bit_xor minus_one (shift_left one i)) + + let gen_incl h l = Int63.gen_incl h l end type t = { @@ -234,10 +238,12 @@ let rec add bv1 bv2 = ;; let bvnot bv = - let bv_new, _ = fold bv ~init:(bv, 0) ~f:(fun (bv, i) v -> - if phys_equal v true then (set bv i false; (bv, i + 1)) - else (set bv i true; (bv, i + 1))) in - bv_new + let bv_new = create bv.length in + fold bv ~init:(bv, 0) ~f:(fun (bv, i) v -> + if phys_equal v true then (set bv_new i false; (bv, i + 1)) + else (set bv_new i true; (bv, i + 1))) + ; + bv_new ;; @@ -256,7 +262,11 @@ let compare bv1 bv2 = let bvult bv1 bv2 = let c = compare bv1 bv2 in - if c > 0 then false else true + if c >= 0 then false else true +;; + +let bvule bv1 bv2 = + (bvult bv1 bv2) || ((compare bv1 bv2) = 0) ;; let concat bv1 bv2 = @@ -268,4 +278,16 @@ let concat bv1 bv2 = bv12 ;; +let bvuge bv1 bv2 = + (bvult bv2 bv1) || ((compare bv1 bv2) = 0) +;; + +let bvugt bv1 bv2 = + bvult bv2 bv1 +;; +let bvsub bv1 bv2 = + let const_one = create bv2.length in + set const_one 0 true; + (add bv1 (add (bvnot bv2) const_one)) +;; diff --git a/src/Synthesizer.ml b/src/Synthesizer.ml index 129675d..a92a81f 100644 --- a/src/Synthesizer.ml +++ b/src/Synthesizer.ml @@ -170,6 +170,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) = let string_components = typed_components Type.STRING in let poly_list_components = typed_components Type.(LIST (TVAR "_")) in let poly_array_components = typed_components Type.(ARRAY (TVAR "_", TVAR "_")) in + let bitvec_components = typed_components Type.(BITVEC (TVAR "_")) in let empty_candidates () = Array.(init ((length config.logic.components_per_level) + 1) @@ -182,6 +183,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) = let string_candidates = empty_candidates () in let list_candidates = empty_candidates () in let array_candidates = empty_candidates () in + let bitvec_candidates = empty_candidates () in let typed_candidates ?(no_tvar = false) = function | Type.INT -> int_candidates @@ -189,12 +191,14 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) = | Type.CHAR -> char_candidates | Type.STRING -> string_candidates | Type.LIST _ -> list_candidates + | Type.BITVEC _ -> bitvec_candidates | Type.ARRAY _ -> array_candidates | Type.TVAR _ when no_tvar = false -> raise (Internal_Exn "No candidates for TVAR") | Type.TVAR _ -> let (@) = Array.append in int_candidates @ bool_candidates @ char_candidates - @ string_candidates @ list_candidates @ array_candidates + @ string_candidates @ list_candidates @ array_candidates + @ bitvec_candidates in let seen_outputs = ref (Set.empty (module Output)) in @@ -311,13 +315,15 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) = ; (CHAR, char_candidates) ; (STRING, string_candidates) ; (LIST (TVAR "_"), list_candidates) - ; (ARRAY (TVAR "_", TVAR "_"), array_candidates) ] + ; (ARRAY (TVAR "_", TVAR "_"), array_candidates) + ; (BITVEC (TVAR "_"), bitvec_candidates) ] [ bool_components.(l) ; int_components.(l) ; char_components.(l) ; string_components.(l) ; poly_list_components.(l) - ; poly_array_components.(l) ] + ; poly_array_components.(l) + ; bitvec_components.(l) ] ~f:(fun (cand_type, cands) comps -> List.iter comps ~f:(expand_component l level cost cands cand_type)))) @@ -344,4 +350,4 @@ let solve ?(config = Config.default) (task : task) : result = ; func = Expr.to_function solution ; constraints = solution_constraints ; stats = stats - } \ No newline at end of file + } diff --git a/src/Type.ml b/src/Type.ml index 2706157..ab1f2ce 100644 --- a/src/Type.ml +++ b/src/Type.ml @@ -10,7 +10,7 @@ module T = struct | TVAR of string | LIST of t | ARRAY of (t * t) - | BITVEC of string + | BITVEC of t [@@deriving compare,sexp] end @@ -29,7 +29,7 @@ let rec of_sexp (sexp: Sexp.t) : t = | List [Atom "Array" ; index ; value] -> ARRAY ((of_sexp index) , (of_sexp value)) | List [Atom "_"; Atom "BitVec"; Atom n] - -> BITVEC n + -> BITVEC (TVAR n) | s -> raise (Parse_Exn ("Could not parse type `" ^ (Sexp.to_string_hum s) ^ "`.")) let rec to_string : t -> string = function @@ -39,7 +39,7 @@ let rec to_string : t -> string = function | STRING -> "String" | LIST t -> "(List " ^ (to_string t) ^ ")" | ARRAY (k,v) -> "(Array " ^ (to_string k) ^ " " ^ (to_string v) ^ ")" - | BITVEC n -> "(_ BitVec " ^ n ^ ")" + | BITVEC (TVAR n) -> "(_ BitVec " ^ n ^ ")" | TVAR n -> n (* TODO: We may want to detect cases when a TVAR should never occur in a type, and throw exceptions in those cases *) @@ -60,6 +60,7 @@ module Unification = struct | LIST typ -> LIST (substitute_with_exn env typ) | ARRAY (key,value) -> ARRAY ((substitute_with_exn env key), (substitute_with_exn env value)) + | BITVEC len -> BITVEC (substitute_with_exn env len) | t -> t let substitute (env : (string * t) list) (t : t) : t option = @@ -99,6 +100,7 @@ module Unification = struct | ARRAY (lhs_key,lhs_value), ARRAY (rhs_key,rhs_value) -> let env = env @ (of_type ~env lhs_key rhs_key) in (of_type lhs_value rhs_value ~env) + | BITVEC (TVAR llen), BITVEC (TVAR rlen) -> (rlen, (TVAR llen)) :: env | lhs , rhs -> if equal lhs rhs then env else raise (Unification_Exn "Circular dependency!") diff --git a/src/Value.ml b/src/Value.ml index 02f92bf..c737a08 100644 --- a/src/Value.ml +++ b/src/Value.ml @@ -27,7 +27,7 @@ let rec typeof : t -> Type.t = function | List (typ, _) -> Type.LIST typ | Array (key_type, value_type, _, _) -> Type.ARRAY (key_type,value_type) - | BitVec bv -> Type.BITVEC (Int.to_string bv.length) + | BitVec bv -> Type.BITVEC (Type.TVAR (Int.to_string bv.length)) let rec to_string : t -> string = function | Int i -> Int.to_string i From 810a48162dd74ab8a2c84ead2e33056a547770c5 Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Sat, 18 Jan 2020 14:18:47 -0800 Subject: [PATCH 08/18] Add random bitvector generation --- src/TestGen.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/TestGen.ml b/src/TestGen.ml index c3cc1a8..dc74620 100644 --- a/src/TestGen.ml +++ b/src/TestGen.ml @@ -15,5 +15,9 @@ let rec for_type (t : Type.t) : Value.t Generator.t = | Type.ARRAY (key,value) -> (Int.gen_incl 0 64) >>= fun len -> ((tuple2 (List.gen_with_length len (tuple2 (for_type key) (for_type value))) (for_type value)) >>= fun (arr, def) -> singleton (Value.Array (key, value, arr, def))) - | Type.LIST _ | Type.TVAR _ | Type.BITVEC _ + | Type.BITVEC (TVAR n) -> let bv = Bitarray.create (Int.of_string n) in let open Bitarray in + (Int63_chunk.gen_incl Int63.min_value Int63.max_value) >>= fun i -> + singleton (Value.BitVec {data = (Array.map bv.data ~f:(fun x -> i)); + length = (Int.of_string n)}) + | Type.LIST _ | Type.TVAR _ -> raise (Exceptions.Internal_Exn "Generator not implemented!") From efae245bca9c3dea64a2ef485dfa4fef9aea8f8d Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Sat, 25 Jan 2020 16:19:11 -0800 Subject: [PATCH 09/18] Add unit tests for operations on BitVec and Bitarray --- src/TestGen.ml | 11 +-- test/Test_BitVecComponents.ml | 130 ++++++++++++++++++++++++++++++++++ 2 files changed, 137 insertions(+), 4 deletions(-) create mode 100644 test/Test_BitVecComponents.ml diff --git a/src/TestGen.ml b/src/TestGen.ml index dc74620..ef04ffa 100644 --- a/src/TestGen.ml +++ b/src/TestGen.ml @@ -15,9 +15,12 @@ let rec for_type (t : Type.t) : Value.t Generator.t = | Type.ARRAY (key,value) -> (Int.gen_incl 0 64) >>= fun len -> ((tuple2 (List.gen_with_length len (tuple2 (for_type key) (for_type value))) (for_type value)) >>= fun (arr, def) -> singleton (Value.Array (key, value, arr, def))) - | Type.BITVEC (TVAR n) -> let bv = Bitarray.create (Int.of_string n) in let open Bitarray in - (Int63_chunk.gen_incl Int63.min_value Int63.max_value) >>= fun i -> - singleton (Value.BitVec {data = (Array.map bv.data ~f:(fun x -> i)); - length = (Int.of_string n)}) + (* Any BitVector with size greater than 63 bits will have bits number 64 = 0, + 65 = 1, ... *) + | Type.BITVEC (TVAR n) -> let bv = Bitarray.create (Int.of_string n) in + let open Bitarray in + (Int63_chunk.gen_incl Int63.min_value Int63.max_value) >>= fun i -> + singleton (Value.BitVec {data = (Array.map bv.data ~f:(fun x -> i)); + length = (Int.of_string n)}) | Type.LIST _ | Type.TVAR _ -> raise (Exceptions.Internal_Exn "Generator not implemented!") diff --git a/test/Test_BitVecComponents.ml b/test/Test_BitVecComponents.ml new file mode 100644 index 0000000..63cf36c --- /dev/null +++ b/test/Test_BitVecComponents.ml @@ -0,0 +1,130 @@ +open Base + +open LoopInvGen + +let bveq_eval = (List.find_exn BitVecComponents.all + ~f:(fun comp -> String.equal comp.name "bv-eq")).evaluate +let bvadd_eval = (List.find_exn BitVecComponents.all + ~f:(fun comp -> String.equal comp.name "bvadd")).evaluate +let bvnot_eval = (List.find_exn BitVecComponents.all + ~f:(fun comp -> String.equal comp.name "bvnot")).evaluate +let bvult_eval = (List.find_exn BitVecComponents.all + ~f:(fun comp -> String.equal comp.name "bvult")).evaluate +let bvuge_eval = (List.find_exn BitVecComponents.all + ~f:(fun comp -> String.equal comp.name "bvuge")).evaluate +let bvugt_eval = (List.find_exn BitVecComponents.all + ~f:(fun comp -> String.equal comp.name "bvugt")).evaluate +let bvule_eval = (List.find_exn BitVecComponents.all + ~f:(fun comp -> String.equal comp.name "bvule")).evaluate +let bvsub_eval = (List.find_exn BitVecComponents.all + ~f:(fun comp -> String.equal comp.name "bvsub")).evaluate + + +let equal_hex_bin () = + let bv1 = Value.BitVec (Bitarray.of_string "#x1010") in + let bv2 = Value.BitVec (Bitarray.of_string "#b0001000000010000") in + let eq_ret = bveq_eval [bv1; bv2] in + let ret = Value.equal (Value.Bool true) eq_ret in + Alcotest.(check bool) "identical" true ret + +let bvadd () = + let bv1 = Value.BitVec (Bitarray.of_string "#b10101010101010101") in + let bv2 = Value.BitVec (Bitarray.of_string "#b01010101010101010") in + let add_ret = bvadd_eval [bv1; bv2] in + let ret = Value.equal (Value.BitVec (Bitarray.of_string "#b11111111111111111")) add_ret in + Alcotest.(check bool) "identical" true ret + +let bvadd_ovf () = + let bv1 = Value.BitVec (Bitarray.of_string "#b10101010101010101") in + let bv2 = Value.BitVec (Bitarray.of_string "#b01010101010101011") in + let add_ret = bvadd_eval [bv1; bv2] in + let ret = Value.equal (Value.BitVec (Bitarray.of_string "#b00000000000000000")) add_ret in + Alcotest.(check bool) "identical" true ret + +let bvnot () = + let bv = Value.BitVec (Bitarray.of_string "#xa482ad9301") in + let bvnot_ret = bvnot_eval [bv] in + let ret = Value.equal (Value.BitVec (Bitarray.of_string "#x5b7d526cfe")) bvnot_ret in + Alcotest.(check bool) "identical" true ret + +let bvult_same () = + let bv1 = Value.BitVec (Bitarray.of_string "#x00000000") in + let bvult_ret = bvult_eval [bv1; bv1] in + let ret = Value.equal (Value.Bool false) bvult_ret in + Alcotest.(check bool) "identical" true ret + +let bvult_ovf () = + (* bv1 is a bitvector which has a 63bit Bitarray *) + let bv1 = Value.BitVec + (Bitarray.of_string + "#b111111111111111111111111111111111111111111111111111111111111111") in + let bvult_ret = bvult_eval [bv1; bv1] in + let ret = Value.equal (Value.Bool false) bvult_ret in + Alcotest.(check bool) "identical" true ret + +let bvult_onegreater () = + let bv1 = Value.BitVec (Bitarray.of_string "#x1") in + let bv2 = Value.BitVec (Bitarray.of_string "#x0") in + let bvult_ret = bvult_eval [bv2; bv1] in + let ret = Value.equal (Value.Bool true) bvult_ret in + Alcotest.(check bool) "identical" true ret + +let bvuge () = + let bv1 = Value.BitVec (Bitarray.of_string "#xff") in + let bv2 = Value.BitVec (Bitarray.of_string "#b11111111") in + let bvuge_ret = bvuge_eval [bv2; bv1] in + let ret = Value.equal (Value.Bool true) bvuge_ret in + Alcotest.(check bool) "identical" true ret + +let bvugt () = + let bv1 = Value.BitVec (Bitarray.of_string "#xa") in + let bv2 = Value.BitVec (Bitarray.of_string "#b1000") in + let bvugt_ret = bvugt_eval [bv1; bv2] in + let ret = Value.equal (Value.Bool true) bvugt_ret in + Alcotest.(check bool) "identical" true ret + +let bvule () = + let bv1 = Value.BitVec (Bitarray.of_string "#x1") in + let bv2 = Value.BitVec (Bitarray.of_string "#xb") in + let bvule_ret = bvult_eval [bv1; bv2] in + let ret = Value.equal (Value.Bool true) bvule_ret in + Alcotest.(check bool) "identical" true ret + +let bvsub () = + let bv1 = Value.BitVec (Bitarray.of_string "#b00") in + let bv2 = Value.BitVec (Bitarray.of_string "#b01") in + let bvsub_ret = bvsub_eval [bv1; bv2] in + (* We should get the representation for -1 *) + let ret = Value.equal (Value.BitVec (Bitarray.of_string "#b11")) bvsub_ret in + Alcotest.(check bool) "identical" true ret + + +let bv_pp f p = match p with + | Value.BitVec ba -> Format.fprintf f "%s\n" (Bitarray.to_string ba) + | _ -> Format.fprintf f "Error with pretty printing the BitVector\n" + +let bitvec_testable = Alcotest.testable bv_pp (fun x y -> Value.equal (Value.Bool true) (bveq_eval [x; y])) + +let gen () = + let bvgen1 = TestGen.for_type (Type.BITVEC (Type.TVAR "32")) in + let bvgen2 = TestGen.for_type (Type.BITVEC (Type.TVAR "32")) in + Alcotest.(check (neg bitvec_testable)) "identical" + (Core.Quickcheck.Generator.generate bvgen1 ~size:1 ~random:(Splittable_random.State.of_int 1)) + (Core.Quickcheck.Generator.generate bvgen2 ~size:1 ~random:(Splittable_random.State.of_int 2)) + + +let all = [ + "equal hex and binary", `Quick, equal_hex_bin ; + "bvadd", `Quick, bvadd ; + "bvadd_ovf", `Quick, bvadd_ovf ; + "bvnot", `Quick, bvnot ; + "bvult_same", `Quick, bvult_same ; + "bvult_ovf", `Quick, bvult_ovf ; + "bvult_onegreater", `Quick, bvult_onegreater ; + "bvuge", `Quick, bvuge ; + "bvugt", `Quick, bvugt ; + "bvule", `Quick, bvule ; + "bvsub", `Quick, bvsub ; + "gen", `Quick, gen + ] + From 99ea8c4e4e79b663daf640f60655bd34fb293173 Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Tue, 11 Feb 2020 19:33:09 -0800 Subject: [PATCH 10/18] Change the BITVEC type to be of int and perform BitVec generation per bit The unification routines try to match a BitVec of negative size to one of positive size. The negative size is treated as a variable, so all BitVecs of size -1 will be matched to the same length BitVec. There is still int to string conversions because the length is parsed as a string and the unification routines use an environment, env, of type (string * t). --- src/BitVecComponents.ml | 22 +++++++++++----------- src/Logic.ml | 4 ++-- src/Synthesizer.ml | 4 ++-- src/TestGen.ml | 13 ++++++++----- src/Type.ml | 12 +++++++----- src/Value.ml | 16 +++++++--------- test/Test_BitVecComponents.ml | 8 ++++---- 7 files changed, 41 insertions(+), 38 deletions(-) diff --git a/src/BitVecComponents.ml b/src/BitVecComponents.ml index 1d7b957..d9b3514 100644 --- a/src/BitVecComponents.ml +++ b/src/BitVecComponents.ml @@ -6,7 +6,7 @@ let all = [ { name = "bv-eq"; codomain = Type.BOOL; - domain = [Type.BITVEC (Type.TVAR "T1"); Type.BITVEC (Type.TVAR "T1")]; + domain = [Type.BITVEC (-1); Type.BITVEC (-1)]; is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> @@ -16,8 +16,8 @@ let all = [ } ; { name = "bvnot"; - codomain = Type.BITVEC (Type.TVAR "T1"); - domain = [Type.BITVEC (Type.TVAR "T1")]; + codomain = Type.BITVEC (-1); + domain = [Type.BITVEC (-1)]; is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v] -> Value.BitVec (Bitarray.bvnot v)); @@ -27,7 +27,7 @@ let all = [ { name = "bvult"; codomain = Type.BOOL; - domain = [Type.BITVEC (Type.TVAR "T1"); Type.BITVEC (Type.TVAR "T1")]; + domain = [Type.BITVEC (-1); Type.BITVEC (-1)]; is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> @@ -37,8 +37,8 @@ let all = [ } ; { name = "bvadd"; - codomain = Type.BITVEC (Type.TVAR "T1"); - domain = [Type.BITVEC (Type.TVAR "T1"); Type.BITVEC (Type.TVAR "T1")]; + 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] -> @@ -49,7 +49,7 @@ let all = [ { name = "bvuge"; codomain = Type.BOOL; - domain = [Type.BITVEC (Type.TVAR "T1"); Type.BITVEC (Type.TVAR "T1")]; + domain = [Type.BITVEC (-1); Type.BITVEC (-1)]; is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> @@ -60,7 +60,7 @@ let all = [ { name = "bvugt"; codomain = Type.BOOL; - domain = [Type.BITVEC (Type.TVAR "T1"); Type.BITVEC (Type.TVAR "T1")]; + domain = [Type.BITVEC (-1); Type.BITVEC (-1)]; is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> @@ -71,7 +71,7 @@ let all = [ { name = "bvule"; codomain = Type.BOOL; - domain = [Type.BITVEC (Type.TVAR "T1"); Type.BITVEC (Type.TVAR "T1")]; + domain = [Type.BITVEC (-1); Type.BITVEC (-1)]; is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> @@ -81,8 +81,8 @@ let all = [ } ; { name = "bvsub"; - codomain = Type.BITVEC (Type.TVAR "T1"); - domain = [Type.BITVEC (Type.TVAR "T1"); Type.BITVEC (Type.TVAR "T1")]; + 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] -> diff --git a/src/Logic.ml b/src/Logic.ml index 657b312..066a89f 100644 --- a/src/Logic.ml +++ b/src/Logic.ml @@ -37,8 +37,8 @@ let all_supported = components_per_level = ArrayComponents.levels ++ BooleanComponents.levels ++ IntegerComponents.non_linear_levels ; sample_set_size_multiplier = 8 } ; { - name = "QF_BV"; - components_per_level = BitVecComponents.levels ++ BooleanComponents.levels; + name = "BV"; + components_per_level = BooleanComponents.levels ++ BitVecComponents.levels; sample_set_size_multiplier = 1 } ; { name = "ALL" ; diff --git a/src/Synthesizer.ml b/src/Synthesizer.ml index a92a81f..3ee4494 100644 --- a/src/Synthesizer.ml +++ b/src/Synthesizer.ml @@ -170,7 +170,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) = let string_components = typed_components Type.STRING in let poly_list_components = typed_components Type.(LIST (TVAR "_")) in let poly_array_components = typed_components Type.(ARRAY (TVAR "_", TVAR "_")) in - let bitvec_components = typed_components Type.(BITVEC (TVAR "_")) in + let bitvec_components = typed_components Type.(BITVEC (-2)) in let empty_candidates () = Array.(init ((length config.logic.components_per_level) + 1) @@ -316,7 +316,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) = ; (STRING, string_candidates) ; (LIST (TVAR "_"), list_candidates) ; (ARRAY (TVAR "_", TVAR "_"), array_candidates) - ; (BITVEC (TVAR "_"), bitvec_candidates) ] + ; (BITVEC (-2), bitvec_candidates) ] [ bool_components.(l) ; int_components.(l) ; char_components.(l) diff --git a/src/TestGen.ml b/src/TestGen.ml index ef04ffa..644e3c3 100644 --- a/src/TestGen.ml +++ b/src/TestGen.ml @@ -17,10 +17,13 @@ let rec for_type (t : Type.t) : Value.t Generator.t = >>= fun (arr, def) -> singleton (Value.Array (key, value, arr, def))) (* Any BitVector with size greater than 63 bits will have bits number 64 = 0, 65 = 1, ... *) - | Type.BITVEC (TVAR n) -> let bv = Bitarray.create (Int.of_string n) in - let open Bitarray in - (Int63_chunk.gen_incl Int63.min_value Int63.max_value) >>= fun i -> - singleton (Value.BitVec {data = (Array.map bv.data ~f:(fun x -> i)); - length = (Int.of_string n)}) + | Type.BITVEC n -> let bv = Bitarray.create n in + let randarray = Bitarray.fold bv ~init:((singleton bv), 0) + ~f:(fun (sbv, i) _ -> + (sbv >>= fun bitarr -> bool >>= fun b -> + Bitarray.set bitarr i b; singleton bitarr), i+1) in + (match randarray with + | sbv, i -> sbv >>= fun bv -> singleton (Value.BitVec bv)) + | Type.LIST _ | Type.TVAR _ -> raise (Exceptions.Internal_Exn "Generator not implemented!") diff --git a/src/Type.ml b/src/Type.ml index ab1f2ce..83dd5b3 100644 --- a/src/Type.ml +++ b/src/Type.ml @@ -10,7 +10,7 @@ module T = struct | TVAR of string | LIST of t | ARRAY of (t * t) - | BITVEC of t + | BITVEC of int [@@deriving compare,sexp] end @@ -29,7 +29,7 @@ let rec of_sexp (sexp: Sexp.t) : t = | List [Atom "Array" ; index ; value] -> ARRAY ((of_sexp index) , (of_sexp value)) | List [Atom "_"; Atom "BitVec"; Atom n] - -> BITVEC (TVAR n) + -> BITVEC (Int.of_string n) | s -> raise (Parse_Exn ("Could not parse type `" ^ (Sexp.to_string_hum s) ^ "`.")) let rec to_string : t -> string = function @@ -39,7 +39,7 @@ let rec to_string : t -> string = function | STRING -> "String" | LIST t -> "(List " ^ (to_string t) ^ ")" | ARRAY (k,v) -> "(Array " ^ (to_string k) ^ " " ^ (to_string v) ^ ")" - | BITVEC (TVAR n) -> "(_ BitVec " ^ n ^ ")" + | BITVEC n -> "(_ BitVec " ^ (Int.to_string n) ^ ")" | TVAR n -> n (* TODO: We may want to detect cases when a TVAR should never occur in a type, and throw exceptions in those cases *) @@ -60,7 +60,9 @@ module Unification = struct | LIST typ -> LIST (substitute_with_exn env typ) | ARRAY (key,value) -> ARRAY ((substitute_with_exn env key), (substitute_with_exn env value)) - | BITVEC len -> BITVEC (substitute_with_exn env len) + | BITVEC len -> (match List.find ~f:(fun (id,_) -> String.equal id (Int.to_string len)) env with + | Some (_, value) -> value + | _ -> raise (Unification_Exn ("Could not find a binding for " ^ (to_string (BITVEC len))))) | t -> t let substitute (env : (string * t) list) (t : t) : t option = @@ -100,7 +102,7 @@ module Unification = struct | ARRAY (lhs_key,lhs_value), ARRAY (rhs_key,rhs_value) -> let env = env @ (of_type ~env lhs_key rhs_key) in (of_type lhs_value rhs_value ~env) - | BITVEC (TVAR llen), BITVEC (TVAR rlen) -> (rlen, (TVAR llen)) :: env + | BITVEC llen, BITVEC rlen -> ((Int.to_string rlen), BITVEC llen) :: env | lhs , rhs -> if equal lhs rhs then env else raise (Unification_Exn "Circular dependency!") diff --git a/src/Value.ml b/src/Value.ml index c737a08..35688b3 100644 --- a/src/Value.ml +++ b/src/Value.ml @@ -2,8 +2,6 @@ open Base open Exceptions -module Bitarray = Bitarray - module T = struct type t = Int of int | Bool of bool @@ -27,7 +25,7 @@ let rec typeof : t -> Type.t = function | List (typ, _) -> Type.LIST typ | Array (key_type, value_type, _, _) -> Type.ARRAY (key_type,value_type) - | BitVec bv -> Type.BITVEC (Type.TVAR (Int.to_string bv.length)) + | BitVec bv -> Type.BITVEC bv.length let rec to_string : t -> string = function | Int i -> Int.to_string i @@ -45,15 +43,15 @@ let of_atomic_string (s : string) : t = try Int (Int.of_string s) with Failure _ -> try - Bool (Bool.of_string s) + Bool (Bool.of_string s) with Invalid_argument _ -> try - Char (Char.of_string (String.(chop_suffix_exn ~suffix:"\'" - (chop_prefix_exn ~prefix:"\'" s)))) + Char (Char.of_string (String.(chop_suffix_exn ~suffix:"\'" + (chop_prefix_exn ~prefix:"\'" s)))) with Invalid_argument _ -> try - BitVec (Bitarray.of_string s) + BitVec (Bitarray.of_string s) with Invalid_argument _ -> try - String String.(chop_suffix_exn ~suffix:"\"" (chop_prefix_exn ~prefix:"\"" s)) - with Invalid_argument _ -> + String String.(chop_suffix_exn ~suffix:"\"" (chop_prefix_exn ~prefix:"\"" s)) + with Invalid_argument _ -> raise (Parse_Exn ("Failed to parse value `" ^ s ^ "`.")) diff --git a/test/Test_BitVecComponents.ml b/test/Test_BitVecComponents.ml index 63cf36c..7d01374 100644 --- a/test/Test_BitVecComponents.ml +++ b/test/Test_BitVecComponents.ml @@ -106,13 +106,13 @@ let bv_pp f p = match p with let bitvec_testable = Alcotest.testable bv_pp (fun x y -> Value.equal (Value.Bool true) (bveq_eval [x; y])) let gen () = - let bvgen1 = TestGen.for_type (Type.BITVEC (Type.TVAR "32")) in - let bvgen2 = TestGen.for_type (Type.BITVEC (Type.TVAR "32")) in + let bvgen1 = TestGen.for_type (Type.BITVEC 32) in + let bvgen2 = TestGen.for_type (Type.BITVEC 32) in Alcotest.(check (neg bitvec_testable)) "identical" (Core.Quickcheck.Generator.generate bvgen1 ~size:1 ~random:(Splittable_random.State.of_int 1)) (Core.Quickcheck.Generator.generate bvgen2 ~size:1 ~random:(Splittable_random.State.of_int 2)) - - + + let all = [ "equal hex and binary", `Quick, equal_hex_bin ; "bvadd", `Quick, bvadd ; From 0a6caf907a1a9b3209d12010badbb4b9790d0484 Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Thu, 27 Feb 2020 19:59:31 -0800 Subject: [PATCH 11/18] Remove all integer to string conversions from bitvec unification --- src/Type.ml | 62 +++++++++++++++++++++++++--------------- test/Test_Unification.ml | 15 ++++++---- 2 files changed, 48 insertions(+), 29 deletions(-) diff --git a/src/Type.ml b/src/Type.ml index 83dd5b3..36906cc 100644 --- a/src/Type.ml +++ b/src/Type.ml @@ -50,44 +50,60 @@ module Unification = struct * TODO: The algorithm below is simple but not efficient. * See: https://eli.thegreenplace.net/2018/unification#efficiency *) + type id = + | STR of string + | NUM of int - let rec substitute_with_exn (env : (string * t) list) = function + let rec substitute_with_exn (env : (id * t) list) = function | TVAR name -> begin - match List.find ~f:(fun (id,_) -> String.equal id name) env with + match List.find ~f:(fun (id,_) -> match id with + | STR idstr -> String.equal idstr name + | _ -> false) env with | Some (_,value) -> value | _ -> raise (Unification_Exn ("Could not find a binding for " ^ name)) end | LIST typ -> LIST (substitute_with_exn env typ) | ARRAY (key,value) -> ARRAY ((substitute_with_exn env key), (substitute_with_exn env value)) - | BITVEC len -> (match List.find ~f:(fun (id,_) -> String.equal id (Int.to_string len)) env with - | Some (_, value) -> value - | _ -> raise (Unification_Exn ("Could not find a binding for " ^ (to_string (BITVEC len))))) + | BITVEC len -> (match List.find ~f:(fun (id,_) -> (match id with + | NUM idnum -> Int.equal idnum len + | _ -> false)) env with + | Some (_, value) -> value + | _ -> raise (Unification_Exn ("Could not find a binding for " ^ (to_string (BITVEC len))))) | t -> t - let substitute (env : (string * t) list) (t : t) : t option = + let substitute (env : (id * t) list) (t : t) : t option = try Some (substitute_with_exn env t) with _ -> None let rec resolve_var ?(env = []) = function - | lhs, TVAR rhs -> if String.equal lhs rhs - then raise (Unification_Exn "Circular dependency!") - else begin - match List.find env ~f:(fun (e,_) -> String.equal e rhs) with - | None -> (lhs, TVAR rhs) - | Some (_, (TVAR x)) -> resolve_var ~env (lhs, (TVAR x)) - | Some (_, rhs) -> (lhs, rhs) - end + | STR lhs, TVAR rhs -> if String.equal lhs rhs + then raise (Unification_Exn "Circular dependency!") + else begin + match List.find env ~f:(fun (e,_) -> match e with + | STR idstr -> String.equal idstr rhs + | _ -> false) with + | None -> (STR lhs, TVAR rhs) + | Some (_, (TVAR x)) -> resolve_var ~env (STR lhs, (TVAR x)) + | Some (_, rhs) -> (STR lhs, rhs) + end | pair -> pair - let rec of_var ?(env = []) (var : string) (rhs : t) = - match List.Assoc.find env ~equal:String.equal var with + let rec of_var ?(env = []) (var : id) (rhs : t) = + match List.Assoc.find env ~equal:(fun idquery idenv -> (match (idenv, idquery) with + | (STR id1), (STR id2) -> String.equal id1 id2 + | (NUM id1), (NUM id2) -> Int.equal id1 id2 + | _ -> false)) var with | None -> begin match rhs with | TVAR var_rhs -> begin - match List.Assoc.find env ~equal:String.equal var_rhs with + match List.Assoc.find env ~equal:(fun _ idvar -> match idvar with + | STR idstr -> String.equal idstr var_rhs + | _ -> false) (STR var_rhs) with | None -> List.fold ((var,rhs) :: env) ~init:[] ~f:(fun acc elem -> (resolve_var elem ~env:(((var,rhs) :: env)) :: acc)) - | Some value -> of_type ~env (TVAR var) value + | Some value -> (match var with + | STR varstr -> of_type ~env (TVAR varstr) value + | _ -> raise (Unification_Exn ("Type variable was as integer but should be a string"))) end | _ -> List.fold ((var,rhs) :: env) ~init:[] ~f:(fun acc elem -> (resolve_var elem ~env:(((var,rhs)::env)) :: acc)) @@ -95,22 +111,22 @@ module Unification = struct | Some value -> of_type ~env value rhs and of_type ?(env = []) (lhs : t) (rhs : t) = match lhs, rhs with - | TVAR x , _ -> of_var ~env x rhs - | _ , TVAR y -> of_var ~env y lhs + | TVAR x , _ -> of_var ~env (STR x) rhs + | _ , TVAR y -> of_var ~env (STR y) lhs | LIST lhs_type, LIST rhs_type -> of_type lhs_type rhs_type ~env | ARRAY (lhs_key,lhs_value), ARRAY (rhs_key,rhs_value) -> let env = env @ (of_type ~env lhs_key rhs_key) in (of_type lhs_value rhs_value ~env) - | BITVEC llen, BITVEC rlen -> ((Int.to_string rlen), BITVEC llen) :: env + | BITVEC llen, BITVEC rlen -> of_var ~env (NUM llen) rhs (* (NUM rlen, BITVEC llen) :: env *) | lhs , rhs -> if equal lhs rhs then env else raise (Unification_Exn "Circular dependency!") - let rec of_types_exn ?(env = []) (lhs : t list) (rhs : t list) : (string * t) list = + let rec of_types_exn ?(env = []) (lhs : t list) (rhs : t list) : (id * t) list = match lhs , rhs with | (x :: tx, y :: ty) -> of_types_exn ~env:(of_type ~env x y) tx ty | _ -> env - let of_types ?(env = []) (t1 : t list) (t2 : t list) : (string * t) list option = + let of_types ?(env = []) (t1 : t list) (t2 : t list) : (id * t) list option = try Some (of_types_exn t1 t2) with _ -> None end diff --git a/test/Test_Unification.ml b/test/Test_Unification.ml index fbad637..0e6033e 100644 --- a/test/Test_Unification.ml +++ b/test/Test_Unification.ml @@ -6,7 +6,10 @@ open Exceptions open Type let are_bindings_equal = - List.equal (Tuple.T2.equal ~eq1:String.equal ~eq2:equal) + List.equal (Tuple.T2.equal ~eq1:(fun var1 var2 -> match var1, var2 with + | Unification.STR var1str, Unification.STR var2str -> String.equal var1str var2str + | Unification.NUM var1num, Unification.NUM var2num -> Int.equal var1num var2num + | _ -> false) ~eq2:equal) let monomorphic () = let domain1 = [ INT ; STRING ] in @@ -20,7 +23,7 @@ let without_dependencies () = let domain1 = [ ARRAY (TVAR "a", TVAR "b") ; INT ; STRING ] in let domain2 = [ ARRAY (INT,BOOL) ; INT ; STRING ] in let bindings = Unification.of_types_exn domain1 domain2 in - let bindings_correct = [("a", INT); ("b", BOOL)] in + let bindings_correct = [(Unification.STR "a", INT); (Unification.STR "b", BOOL)] in let res = are_bindings_equal bindings bindings_correct in Alcotest.(check bool) "identical" true res @@ -28,7 +31,7 @@ let with_dependencies () = let domain1 = [ ARRAY (TVAR "a", TVAR "b") ; LIST(TVAR "a") ] in let domain2 = [ ARRAY (STRING,INT) ; LIST STRING ] in let bindings = Unification.of_types_exn domain1 domain2 in - let correct_bindings = [("a", STRING) ; ("b", INT)] in + let correct_bindings = [(Unification.STR "a", STRING) ; (Unification.STR "b", INT)] in let res = are_bindings_equal bindings correct_bindings in Alcotest.(check bool) "identical" true res @@ -45,7 +48,7 @@ let direct_circular () = in Alcotest.check_raises "cannot unify" (Unification_Exn "Circular dependency!") test let substitution () = - let env = [("a",STRING) ; ("b",INT)] in + let env = [(Unification.STR "a",STRING) ; (Unification.STR "b",INT)] in let codomain = ARRAY(TVAR "b" , TVAR "a") in let resolved_codomain = ARRAY(INT,STRING) in let res = match Unification.substitute env codomain with @@ -54,7 +57,7 @@ let substitution () = in Alcotest.(check bool) "correct application of env" true res let incomplete_substitution () = - let env = [("a",INT)] in + let env = [(Unification.STR "a",INT)] in let codomain = ARRAY(TVAR "a" , TVAR "b") in let resolved_codomain = ARRAY (INT ,INT) in let res = match Unification.substitute env codomain with @@ -70,4 +73,4 @@ let all = [ "Indirect circular dependency", `Quick, indirect_circular ; "Substitution", `Quick, substitution ; "Incomplete substitution", `Quick, incomplete_substitution ; -] \ No newline at end of file +] From 6c15ad6a3420891680556cdeb12a114566218398 Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Thu, 27 Feb 2020 21:34:14 -0800 Subject: [PATCH 12/18] Fix Bitvec unification bug with ordering of arguments --- src/Type.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/Type.ml b/src/Type.ml index 36906cc..64d1a36 100644 --- a/src/Type.ml +++ b/src/Type.ml @@ -65,9 +65,9 @@ module Unification = struct | LIST typ -> LIST (substitute_with_exn env typ) | ARRAY (key,value) -> ARRAY ((substitute_with_exn env key), (substitute_with_exn env value)) - | BITVEC len -> (match List.find ~f:(fun (id,_) -> (match id with - | NUM idnum -> Int.equal idnum len - | _ -> false)) env with + | BITVEC len -> (match List.find env ~f:(fun (id,_) -> (match id with + | NUM idnum -> Int.equal idnum len + | _ -> false)) with | Some (_, value) -> value | _ -> raise (Unification_Exn ("Could not find a binding for " ^ (to_string (BITVEC len))))) | t -> t @@ -118,7 +118,10 @@ module Unification = struct | ARRAY (lhs_key,lhs_value), ARRAY (rhs_key,rhs_value) -> let env = env @ (of_type ~env lhs_key rhs_key) in (of_type lhs_value rhs_value ~env) - | BITVEC llen, BITVEC rlen -> of_var ~env (NUM llen) rhs (* (NUM rlen, BITVEC llen) :: env *) + | BITVEC llen, BITVEC rlen -> (match llen, rlen with + | _ when Int.(<) llen 0 -> of_var ~env (NUM llen) rhs + | _ when Int.(<) rlen 0 -> of_var ~env (NUM rlen) lhs + | _ -> env) | lhs , rhs -> if equal lhs rhs then env else raise (Unification_Exn "Circular dependency!") From dc41d5a01ee8d91b19b38cfd8b8a3f0d4aff4f56 Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Sat, 4 Apr 2020 21:16:15 -0700 Subject: [PATCH 13/18] Add tests for BitVec synthesis and unification --- src/Synthesizer.ml | 6 ++++-- test/Runner.ml | 3 ++- test/Test_Synthesizer.ml | 26 +++++++++++++++++++++++++- test/Test_Unification.ml | 19 +++++++++++++++++++ 4 files changed, 50 insertions(+), 4 deletions(-) diff --git a/src/Synthesizer.ml b/src/Synthesizer.ml index 3ee4494..6577948 100644 --- a/src/Synthesizer.ml +++ b/src/Synthesizer.ml @@ -153,6 +153,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) = | ARRAY _ , ARRAY _ -> true | LIST _ , LIST _ -> true | TVAR _, _ -> true + | BITVEC _, BITVEC _ -> true | cod, t_type -> equal cod t_type) in Array.(append (create ~len:1 []) @@ -170,7 +171,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) = let string_components = typed_components Type.STRING in let poly_list_components = typed_components Type.(LIST (TVAR "_")) in let poly_array_components = typed_components Type.(ARRAY (TVAR "_", TVAR "_")) in - let bitvec_components = typed_components Type.(BITVEC (-2)) in + let bitvec_components = typed_components Type.(BITVEC (-1)) in let empty_candidates () = Array.(init ((length config.logic.components_per_level) + 1) @@ -266,6 +267,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) = let cod = Type.(match unified_component.codomain with | ARRAY _ -> ARRAY (TVAR "_" , TVAR "_") | LIST _ -> LIST (TVAR "_") + | BITVEC _ -> BITVEC (-1) | cod -> cod) in if not (Type.equal cod cand_type) then Log.debug (lazy (" > The candidate type " ^ (Type.to_string cand_type) ^ @@ -316,7 +318,7 @@ let solve_impl (config : Config.t) (task : task) (stats : stats) = ; (STRING, string_candidates) ; (LIST (TVAR "_"), list_candidates) ; (ARRAY (TVAR "_", TVAR "_"), array_candidates) - ; (BITVEC (-2), bitvec_candidates) ] + ; (BITVEC (-1), bitvec_candidates) ] [ bool_components.(l) ; int_components.(l) ; char_components.(l) diff --git a/test/Runner.ml b/test/Runner.ml index 2b4a2f7..26d20e9 100644 --- a/test/Runner.ml +++ b/test/Runner.ml @@ -10,4 +10,5 @@ let () = ; "Test_Unification", Test_Unification.all ; "Test_Expr", Test_Expr.all ; "Test_ArrayComponents", Test_ArrayComponents.all - ]) \ No newline at end of file + ; "Test_BitVecComponents", Test_BitVecComponents.all + ]) diff --git a/test/Test_Synthesizer.ml b/test/Test_Synthesizer.ml index 43c77a4..65208f5 100644 --- a/test/Test_Synthesizer.ml +++ b/test/Test_Synthesizer.ml @@ -180,6 +180,28 @@ let all_mapR_ge_l_0 () = constants = [] } in Alcotest.(check string) "identical" "(all (map-fixR-int-geq l 0))" result.string +let bvadd_a_b () = + let result = solve ~config:{ Config.default with logic = Logic.of_string "BV" } { + arg_names = ["a"; "b"]; + inputs = List.map ~f:(fun a -> Array.map ~f:(fun x -> Value.BitVec (Bitarray.of_string x)) a) + [ [| "#b00"; "#b01" ; "#b10" ; "#b11" |] ; + [| "#b01"; "#b10" ; "#b11" ; "#b00"|]]; + outputs = Array.map ~f:(fun x -> Value.BitVec (Bitarray.of_string x)) + [| "#b01"; "#b11"; "#b01" ; "#b11" |]; + constants = [] + } in Alcotest.(check string) "identical" "(bvadd a b)" result.string + +let bvult_a_b () = + let result = solve ~config:{ Config.default with logic = Logic.of_string "BV" } { + arg_names = ["a"; "b"]; + inputs = List.map ~f:(fun a -> Array.map ~f:(fun x -> Value.BitVec (Bitarray.of_string x)) a) + [ [| "#b00"; "#b01" ; "#b10" ; "#b11"|] ; + [| "#b01"; "#b10" ; "#b11" ; "#b00"|]]; + outputs = Array.map ~f:(fun b -> Value.Bool b) + [|true; true; true; false|]; + constants = [] + } in Alcotest.(check string) "identical" "(bvult a b)" result.string + let all = [ "(+ x y)", `Quick, plus_x_y ; "(>= (+ x z) y)", `Quick, ge_plus_x_z_y ; @@ -191,4 +213,6 @@ let all = [ "(store a k v) ; with duplicates", `Quick, store_a_k_v__with_duplicates ; "(>= y (len x))", `Quick, ge_y_len_x ; "(all (map-fixR-int-geq l 0))", `Quick, all_mapR_ge_l_0 ; -] \ No newline at end of file + "(bvadd a b)", `Quick, bvadd_a_b ; + "(bvult a b)", `Quick, bvult_a_b ; +] diff --git a/test/Test_Unification.ml b/test/Test_Unification.ml index 0e6033e..5658728 100644 --- a/test/Test_Unification.ml +++ b/test/Test_Unification.ml @@ -65,6 +65,23 @@ let incomplete_substitution () = | None -> false in Alcotest.(check bool) "incorrect application of env" false res +let bitvec () = + let domain1 = [BITVEC (-2); BITVEC (-1) ; BITVEC (-2)] in + let domain2 = [BITVEC (32); BITVEC (32) ; BITVEC (32)] in + let bindings = Unification.of_types_exn domain1 domain2 in + let bindings_correct = [(Unification.NUM (-2), BITVEC (32)) ; (Unification.NUM (-1), BITVEC (32))] in + let res = are_bindings_equal bindings bindings_correct + in Alcotest.(check bool) "identical" true res + +let bitvec_sub () = + let env = [(Unification.NUM (-1), BITVEC (32))] in + let codomain = BITVEC (-1) in + let resolved_codomain = BITVEC (32) in + let res = match Unification.substitute env codomain with + | Some res -> equal res resolved_codomain + | None -> false in + Alcotest.(check bool) "incorrect application of env" true res + let all = [ "Unif. of monomorphic types", `Quick, monomorphic ; "Unif. without dependencies", `Quick, without_dependencies ; @@ -73,4 +90,6 @@ let all = [ "Indirect circular dependency", `Quick, indirect_circular ; "Substitution", `Quick, substitution ; "Incomplete substitution", `Quick, incomplete_substitution ; + "Bitvec", `Quick, bitvec ; + "Bitvec substitution", `Quick, bitvec_sub ; ] From d2af30bad55b722f7f390fed19166867a9ea27f3 Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Mon, 6 Apr 2020 20:58:37 -0700 Subject: [PATCH 14/18] Add more complex BitVec synthesis test --- test/Test_Synthesizer.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/test/Test_Synthesizer.ml b/test/Test_Synthesizer.ml index 65208f5..b300b1a 100644 --- a/test/Test_Synthesizer.ml +++ b/test/Test_Synthesizer.ml @@ -202,6 +202,17 @@ let bvult_a_b () = constants = [] } in Alcotest.(check string) "identical" "(bvult a b)" result.string +let bvnot_bvsub_a_b () = + let result = solve ~config:{ Config.default with logic = Logic.of_string "BV" } { + arg_names = ["a"; "b"]; + inputs = List.map ~f:(fun a -> Array.map ~f:(fun x -> Value.BitVec (Bitarray.of_string x)) a) + [ [| "#b0000"; "#b0010" ; "#b1000" ; "#b1100"|] ; + [| "#b0100"; "#b1000" ; "#b1100" ; "#b0000"|]]; + outputs = Array.map ~f:(fun x -> Value.BitVec (Bitarray.of_string x)) + [|"#b0011"; "#b0101"; "#b0011"; "#b0011"|]; + constants = [] + } in Alcotest.(check string) "identical" "(bvnot (bvsub a b))" result.string + let all = [ "(+ x y)", `Quick, plus_x_y ; "(>= (+ x z) y)", `Quick, ge_plus_x_z_y ; @@ -215,4 +226,5 @@ let all = [ "(all (map-fixR-int-geq l 0))", `Quick, all_mapR_ge_l_0 ; "(bvadd a b)", `Quick, bvadd_a_b ; "(bvult a b)", `Quick, bvult_a_b ; + "(bvnot (bvsub a b))", `Quick, bvnot_bvsub_a_b ; ] From e4a27d51cfbcb2bebce9ea244c26d9c33fd3a10e Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Mon, 6 Apr 2020 20:59:35 -0700 Subject: [PATCH 15/18] Remove unnecessary code and comments --- src/Bitarray.ml | 3 --- src/TestGen.ml | 2 -- src/Value.ml | 1 - 3 files changed, 6 deletions(-) diff --git a/src/Bitarray.ml b/src/Bitarray.ml index ec908d9..80bb055 100644 --- a/src/Bitarray.ml +++ b/src/Bitarray.ml @@ -17,7 +17,6 @@ module Int63_chunk : sig val empty : t val get : t -> int -> bool val set : t -> int -> bool -> t - val gen_incl : Int63.t -> Int63.t -> t Core_kernel.Quickcheck.Generator.t end = struct open Int63 @@ -31,8 +30,6 @@ end = struct let set t i v = if v then bit_or t (shift_left one i) else bit_and t (bit_xor minus_one (shift_left one i)) - - let gen_incl h l = Int63.gen_incl h l end type t = { diff --git a/src/TestGen.ml b/src/TestGen.ml index 644e3c3..bf71b4d 100644 --- a/src/TestGen.ml +++ b/src/TestGen.ml @@ -15,8 +15,6 @@ let rec for_type (t : Type.t) : Value.t Generator.t = | Type.ARRAY (key,value) -> (Int.gen_incl 0 64) >>= fun len -> ((tuple2 (List.gen_with_length len (tuple2 (for_type key) (for_type value))) (for_type value)) >>= fun (arr, def) -> singleton (Value.Array (key, value, arr, def))) - (* Any BitVector with size greater than 63 bits will have bits number 64 = 0, - 65 = 1, ... *) | Type.BITVEC n -> let bv = Bitarray.create n in let randarray = Bitarray.fold bv ~init:((singleton bv), 0) ~f:(fun (sbv, i) _ -> diff --git a/src/Value.ml b/src/Value.ml index 35688b3..94b47cc 100644 --- a/src/Value.ml +++ b/src/Value.ml @@ -54,7 +54,6 @@ let of_atomic_string (s : string) : t = with Invalid_argument _ -> raise (Parse_Exn ("Failed to parse value `" ^ s ^ "`.")) - (* We assume that an array serialization provides explicit (k,v) pairs -- * either using nested `store` calls, or if-then-else constructs. * The different array formats are described in more details here: From 26154cc52876ce4ba9729cdbfa8417383f551cdc Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Fri, 19 Jun 2020 15:53:46 -0700 Subject: [PATCH 16/18] Remove newline at end of files --- src/BitVecComponents.ml | 2 +- src/Bitarray.ml | 2 +- src/Logic.ml | 2 +- src/SyGuS.ml | 2 +- src/Synthesizer.ml | 2 +- src/TestGen.ml | 2 +- src/Type.ml | 2 +- src/Value.ml | 2 +- test/Runner.ml | 2 +- test/Test_BitVecComponents.ml | 3 +-- test/Test_Synthesizer.ml | 2 +- test/Test_Unification.ml | 2 +- 12 files changed, 12 insertions(+), 13 deletions(-) diff --git a/src/BitVecComponents.ml b/src/BitVecComponents.ml index d9b3514..e5b7839 100644 --- a/src/BitVecComponents.ml +++ b/src/BitVecComponents.ml @@ -92,4 +92,4 @@ let all = [ } ] -let levels = [| all |] +let levels = [| all |] \ No newline at end of file diff --git a/src/Bitarray.ml b/src/Bitarray.ml index 80bb055..747b7e0 100644 --- a/src/Bitarray.ml +++ b/src/Bitarray.ml @@ -287,4 +287,4 @@ let bvsub bv1 bv2 = let const_one = create bv2.length in set const_one 0 true; (add bv1 (add (bvnot bv2) const_one)) -;; +;; \ No newline at end of file diff --git a/src/Logic.ml b/src/Logic.ml index 066a89f..81f0ec9 100644 --- a/src/Logic.ml +++ b/src/Logic.ml @@ -50,4 +50,4 @@ let all_supported = }] ; table -let of_string name = String.Table.find_exn all_supported name +let of_string name = String.Table.find_exn all_supported name \ No newline at end of file diff --git a/src/SyGuS.ml b/src/SyGuS.ml index efae292..b63bd7a 100644 --- a/src/SyGuS.ml +++ b/src/SyGuS.ml @@ -171,4 +171,4 @@ let translate_smtlib_expr (expr : string) : string = | sexp -> sexp in match Sexplib.Sexp.parse expr with | Done (sexp, _) -> Sexp.to_string_hum (helper (sexp)) - | _ -> expr (* TODO: parse does not work on single atoms *) + | _ -> expr (* TODO: parse does not work on single atoms *) \ No newline at end of file diff --git a/src/Synthesizer.ml b/src/Synthesizer.ml index 95a0c35..6244563 100644 --- a/src/Synthesizer.ml +++ b/src/Synthesizer.ml @@ -352,4 +352,4 @@ let solve ?(config = Config.default) (task : task) : result = ; func = Expr.to_function solution ; constraints = solution_constraints ; stats = stats - } + } \ No newline at end of file diff --git a/src/TestGen.ml b/src/TestGen.ml index bf71b4d..057acbf 100644 --- a/src/TestGen.ml +++ b/src/TestGen.ml @@ -24,4 +24,4 @@ let rec for_type (t : Type.t) : Value.t Generator.t = | sbv, i -> sbv >>= fun bv -> singleton (Value.BitVec bv)) | Type.LIST _ | Type.TVAR _ - -> raise (Exceptions.Internal_Exn "Generator not implemented!") + -> raise (Exceptions.Internal_Exn "Generator not implemented!") \ No newline at end of file diff --git a/src/Type.ml b/src/Type.ml index 64d1a36..2894e96 100644 --- a/src/Type.ml +++ b/src/Type.ml @@ -132,4 +132,4 @@ module Unification = struct let of_types ?(env = []) (t1 : t list) (t2 : t list) : (id * t) list option = try Some (of_types_exn t1 t2) with _ -> None -end +end \ No newline at end of file diff --git a/src/Value.ml b/src/Value.ml index 94b47cc..a067bbc 100644 --- a/src/Value.ml +++ b/src/Value.ml @@ -97,4 +97,4 @@ and of_sexp (sexp : Sexp.t) : t = ^ (to_string_hum sexp))) let of_string (s : string) : t = - (of_sexp (Core.Sexp.of_string s)) + (of_sexp (Core.Sexp.of_string s)) \ No newline at end of file diff --git a/test/Runner.ml b/test/Runner.ml index cc950bd..6cea918 100644 --- a/test/Runner.ml +++ b/test/Runner.ml @@ -12,4 +12,4 @@ let () = ; "Test_Unification", Test_Unification.all ; "Test_VPIE", (Test_VPIE.all ~zpath) ; "Test_ZProc", (Test_ZProc.all ~zpath) - ]) + ]) \ No newline at end of file diff --git a/test/Test_BitVecComponents.ml b/test/Test_BitVecComponents.ml index 7d01374..7a2e4a5 100644 --- a/test/Test_BitVecComponents.ml +++ b/test/Test_BitVecComponents.ml @@ -126,5 +126,4 @@ let all = [ "bvule", `Quick, bvule ; "bvsub", `Quick, bvsub ; "gen", `Quick, gen - ] - + ] \ No newline at end of file diff --git a/test/Test_Synthesizer.ml b/test/Test_Synthesizer.ml index b300b1a..ed8e39f 100644 --- a/test/Test_Synthesizer.ml +++ b/test/Test_Synthesizer.ml @@ -227,4 +227,4 @@ let all = [ "(bvadd a b)", `Quick, bvadd_a_b ; "(bvult a b)", `Quick, bvult_a_b ; "(bvnot (bvsub a b))", `Quick, bvnot_bvsub_a_b ; -] +] \ No newline at end of file diff --git a/test/Test_Unification.ml b/test/Test_Unification.ml index 5658728..612bb27 100644 --- a/test/Test_Unification.ml +++ b/test/Test_Unification.ml @@ -92,4 +92,4 @@ let all = [ "Incomplete substitution", `Quick, incomplete_substitution ; "Bitvec", `Quick, bitvec ; "Bitvec substitution", `Quick, bitvec_sub ; -] +] \ No newline at end of file From 7b14015d820569ecf0266eb97261c89a22df0ed0 Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Sun, 21 Jun 2020 18:36:50 -0700 Subject: [PATCH 17/18] Refactor bitarray to separate module Bitarray.ml is taken from v0.14.0 of core_extended and included into the extended BitarrayExt module. A bitvector benchmark is included adapted from [cegar2.sl](https://github.com/SyGuS-Org/benchmarks/blob/master/lib-nonconforming/Inv_Track/cegist-cav18/cegar2.sl) in the SyGuS benchmarks repository. This benchmark currently passes. --- benchmarks/BV/cegar2.sl | 19 ++++ src/BitVecComponents.ml | 16 +-- src/Bitarray.ml | 241 ++++------------------------------------ src/BitarrayExt.ml | 196 ++++++++++++++++++++++++++++++++ src/Value.ml | 6 +- 5 files changed, 246 insertions(+), 232 deletions(-) create mode 100644 benchmarks/BV/cegar2.sl create mode 100644 src/BitarrayExt.ml diff --git a/benchmarks/BV/cegar2.sl b/benchmarks/BV/cegar2.sl new file mode 100644 index 0000000..aac3326 --- /dev/null +++ b/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) diff --git a/src/BitVecComponents.ml b/src/BitVecComponents.ml index e5b7839..fb5b640 100644 --- a/src/BitVecComponents.ml +++ b/src/BitVecComponents.ml @@ -10,7 +10,7 @@ let all = [ is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> - Value.Bool ((Bitarray.compare v1 v2) = 0)); + Value.Bool ((BitarrayExt.compare v1 v2) = 0)); to_string = (fun [@warning "-8"] [v1;v2] -> "(= " ^ v1 ^ " " ^ v2 ^ ")"); global_constraints = (fun _ -> []); } ; @@ -20,7 +20,7 @@ let all = [ domain = [Type.BITVEC (-1)]; is_argument_valid = (function | _ -> true); - evaluate = (function [@warning "-8"] [Value.BitVec v] -> Value.BitVec (Bitarray.bvnot v)); + evaluate = (function [@warning "-8"] [Value.BitVec v] -> Value.BitVec (BitarrayExt.bvnot v)); to_string = (fun [@warning "-8"] [a] -> "(bvnot " ^ a ^ ")"); global_constraints = (fun _ -> []); } ; @@ -31,7 +31,7 @@ let all = [ is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> - Value.Bool (Bitarray.bvult v1 v2)); + Value.Bool (BitarrayExt.bvult v1 v2)); to_string = (fun [@warning "-8"] [a ; b] -> "(bvult " ^ a ^ " " ^ b ^ ")"); global_constraints = (fun _ -> []); } ; @@ -42,7 +42,7 @@ let all = [ is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> - Value.BitVec (Bitarray.add v1 v2)); + Value.BitVec (BitarrayExt.add v1 v2)); to_string = (fun [@warning "-8"] [a ; b] -> "(bvadd " ^ a ^ " " ^ b ^ ")"); global_constraints = (fun _ -> []); } ; @@ -53,7 +53,7 @@ let all = [ is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> - Value.Bool (Bitarray.bvuge v1 v2)); + Value.Bool (BitarrayExt.bvuge v1 v2)); to_string = (fun [@warning "-8"] [a ; b] -> "(bvuge " ^ a ^ " " ^ b ^ ")"); global_constraints = (fun _ -> []); } ; @@ -64,7 +64,7 @@ let all = [ is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> - Value.Bool (Bitarray.bvugt v1 v2)); + Value.Bool (BitarrayExt.bvugt v1 v2)); to_string = (fun [@warning "-8"] [a ; b] -> "(bvugt " ^ a ^ " " ^ b ^ ")"); global_constraints = (fun _ -> []); } ; @@ -75,7 +75,7 @@ let all = [ is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> - Value.Bool (Bitarray.bvule v1 v2)); + Value.Bool (BitarrayExt.bvule v1 v2)); to_string = (fun [@warning "-8"] [a ; b] -> "(bvule " ^ a ^ " " ^ b ^ ")"); global_constraints = (fun _ -> []); } ; @@ -86,7 +86,7 @@ let all = [ is_argument_valid = (function | _ -> true); evaluate = (function [@warning "-8"] [Value.BitVec v1; Value.BitVec v2] -> - Value.BitVec (Bitarray.bvsub v1 v2)); + Value.BitVec (BitarrayExt.bvsub v1 v2)); to_string = (fun [@warning "-8"] [a ; b] -> "(bvsub " ^ a ^ " " ^ b ^ ")"); global_constraints = (fun _ -> []); } diff --git a/src/Bitarray.ml b/src/Bitarray.ml index 747b7e0..990a5a8 100644 --- a/src/Bitarray.ml +++ b/src/Bitarray.ml @@ -6,52 +6,53 @@ * - 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 val empty : t val get : t -> int -> bool val set : t -> int -> bool -> t - end = struct open Int63 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 = @@ -65,36 +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 -(* Applies f to index 0, then index 1, ...*) 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 fold2 = - let rec loop t1 t2 n ~init ~f = - if n < t1.length then - loop t1 t2 (n + 1) ~init:(f init (get t1 n) (get t2 n)) ~f - else - init - in - fun t1 t2 ~init ~f -> loop t1 t2 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 = @@ -102,189 +86,4 @@ let t_of_sexp sexp = let t = create (Array.length a) in Array.iteri a ~f:(fun i v -> set t i v); t -;; - -(* A bitarray created from the string "#b00011" will be represented by - the bitarray with index 0 set to true, index 1 to true, index 2 to - false, etc.*) -let of_string s = - let prefix = String.prefix s 2 in - let numeral = String.drop_prefix s 2 in - let bvsize = String.length numeral in - match prefix with - | "#b" -> - let bv = create bvsize in - let rec loop s bv i = if i >= 0 - then match s with - | '0'::t -> set bv i false; loop t bv (i - 1) - | '1'::t -> set bv i true; loop t bv (i - 1) - else - bv in - loop (String.to_list numeral) bv (bvsize - 1) - | "#x" -> - let bv = create (bvsize * 4) in - let n = (bvsize - 1) in - let rec loop s bv i = if i <= n - then match s with - | '0'::t -> set bv (i * 4) false; - set bv ((i * 4) + 1) false; - set bv ((i * 4) + 2) false; - set bv ((i * 4) + 3) false; - loop t bv (i + 1) - | '1'::t -> set bv (i * 4) true; - set bv ((i * 4) + 1) false; - set bv ((i * 4) + 2) false; - set bv ((i * 4) + 3) false; - loop t bv (i + 1) - | '2'::t -> set bv (i * 4) false; - set bv ((i * 4) + 1) true; - set bv ((i * 4) + 2) false; - set bv ((i * 4) + 3) false; - loop t bv (i + 1) - | '3'::t -> set bv (i * 4) true; - set bv ((i * 4) + 1) true; - set bv ((i * 4) + 2) false; - set bv ((i * 4) + 3) false; - loop t bv (i + 1) - | '4'::t -> set bv (i * 4) false; - set bv ((i * 4) + 1) false; - set bv ((i * 4) + 2) true; - set bv ((i * 4) + 3) false; - loop t bv (i + 1) - | '5'::t -> set bv (i * 4) true; - set bv ((i * 4) + 1) false; - set bv ((i * 4) + 2) true; - set bv ((i * 4) + 3) false; - loop t bv (i + 1) - | '6'::t -> set bv (i * 4) false; - set bv ((i * 4) + 1) true; - set bv ((i * 4) + 2) true; - set bv ((i * 4) + 3) false; - loop t bv (i + 1) - | '7'::t -> set bv (i * 4) true; - set bv ((i * 4) + 1) true; - set bv ((i * 4) + 2) true; - set bv ((i * 4) + 3) false; - loop t bv (i + 1) - | '8'::t -> set bv (i * 4) false; - set bv ((i * 4) + 1) false; - set bv ((i * 4) + 2) false; - set bv ((i * 4) + 3) true; - loop t bv (i + 1) - | '9'::t -> set bv (i * 4) true; - set bv ((i * 4) + 1) false; - set bv ((i * 4) + 2) false; - set bv ((i * 4) + 3) true; - loop t bv (i + 1) - | 'a'::t -> set bv (i * 4) false; - set bv ((i * 4) + 1) true; - set bv ((i * 4) + 2) false; - set bv ((i * 4) + 3) true; - loop t bv (i + 1) - | 'b'::t -> set bv (i * 4) true; - set bv ((i * 4) + 1) true; - set bv ((i * 4) + 2) false; - set bv ((i * 4) + 3) true; - loop t bv (i + 1) - | 'c'::t -> set bv (i * 4) false; - set bv ((i * 4) + 1) false; - set bv ((i * 4) + 2) true; - set bv ((i * 4) + 3) true; - loop t bv (i + 1) - | 'd'::t -> set bv (i * 4) true; - set bv ((i * 4) + 1) false; - set bv ((i * 4) + 2) true; - set bv ((i * 4) + 3) true; - loop t bv (i + 1) - | 'e'::t -> set bv (i * 4) false; - set bv ((i * 4) + 1) true; - set bv ((i * 4) + 2) true; - set bv ((i * 4) + 3) true; - loop t bv (i + 1) - | 'f'::t -> set bv (i * 4) true; - set bv ((i * 4) + 1) true; - set bv ((i * 4) + 2) true; - set bv ((i * 4) + 3) true; - loop t bv (i + 1) - else - bv in - loop (String.to_list (String.rev numeral)) bv 0 -;; - -(* TODO: If the length of the bitvector is a multiple of 4, represent with hex.*) -let to_string bv = "#b" ^ (fold bv ~init:"" ~f:(fun acc -> function - | false -> "0" ^ acc - | true -> "1" ^ acc)) -;; - -let rec add bv1 bv2 = - let sum = create bv1.length in - let s, _, _ = fold2 bv1 bv2 ~init:(sum, 0, 0) ~f:(fun (sum, carry, ind) v1 v2 -> - match v1, v2 with - | true, true -> if phys_equal carry 1 - then (set sum ind true; (sum, 1, ind + 1)) - else (set sum ind false; (sum, 1, ind + 1)) - | false, true - | true, false -> if phys_equal carry 1 - then (set sum ind false; (sum, 1, ind + 1)) - else (set sum ind true; (sum, 0, ind + 1)) - | false, false -> if phys_equal carry 1 - then (set sum ind true; (sum, 0, ind + 1)) - else (set sum ind false; (sum, 0, ind + 1))) in - s -;; - -let bvnot bv = - let bv_new = create bv.length in - fold bv ~init:(bv, 0) ~f:(fun (bv, i) v -> - if phys_equal v true then (set bv_new i false; (bv, i + 1)) - else (set bv_new i true; (bv, i + 1))) - ; - bv_new - -;; - -let compare bv1 bv2 = - let rec helper ind bv1 bv2 = - if ind >= 0 then - let v1 = get bv1 ind in - let v2 = get bv2 ind in - if phys_equal v1 v2 then helper (ind - 1) bv1 bv2 - else if phys_equal v1 false then -1 else 1 - else - 0 - in - helper (bv1.length - 1) bv1 bv2 -;; - -let bvult bv1 bv2 = - let c = compare bv1 bv2 in - if c >= 0 then false else true -;; - -let bvule bv1 bv2 = - (bvult bv1 bv2) || ((compare bv1 bv2) = 0) -;; - -let concat bv1 bv2 = - let bv3 = create (bv1.length + bv2.length) in - let bv1_, _ = fold bv1 ~init:(bv3, bv2.length) ~f:(fun (bv, i) v -> - set bv i v; (bv, i+1)) in - let bv12, _ = fold bv2 ~init:(bv1_, 0) ~f:(fun (bv, i) v -> - set bv i v; (bv, i+1)) in - bv12 -;; - -let bvuge bv1 bv2 = - (bvult bv2 bv1) || ((compare bv1 bv2) = 0) -;; - -let bvugt bv1 bv2 = - bvult bv2 bv1 -;; - -let bvsub bv1 bv2 = - let const_one = create bv2.length in - set const_one 0 true; - (add bv1 (add (bvnot bv2) const_one)) ;; \ No newline at end of file diff --git a/src/BitarrayExt.ml b/src/BitarrayExt.ml new file mode 100644 index 0000000..757cb55 --- /dev/null +++ b/src/BitarrayExt.ml @@ -0,0 +1,196 @@ +open Core +include Bitarray + +let fold2 = + let rec loop t1 t2 n ~init ~f = + if n < (Bitarray.length t1) then + loop t1 t2 (n + 1) ~init:(f init (get t1 n) (get t2 n)) ~f + else + init + in + fun t1 t2 ~init ~f -> loop t1 t2 0 ~init ~f +;; + +(* A bitarray created from the string "#b00011" will be represented by + the bitarray with index 0 set to true, index 1 to true, index 2 to + false, etc.*) +let of_string s = + let prefix = String.prefix s 2 in + let numeral = String.drop_prefix s 2 in + let bvsize = String.length numeral in + match prefix with + | "#b" -> + let bv = create bvsize in + let rec loop s bv i = if i >= 0 + then match s with + | '0'::t -> set bv i false; loop t bv (i - 1) + | '1'::t -> set bv i true; loop t bv (i - 1) + else + bv in + loop (String.to_list numeral) bv (bvsize - 1) + | "#x" -> + let bv = create (bvsize * 4) in + let n = (bvsize - 1) in + let rec loop s bv i = if i <= n + then match s with + | '0'::t -> set bv (i * 4) false; + set bv ((i * 4) + 1) false; + set bv ((i * 4) + 2) false; + set bv ((i * 4) + 3) false; + loop t bv (i + 1) + | '1'::t -> set bv (i * 4) true; + set bv ((i * 4) + 1) false; + set bv ((i * 4) + 2) false; + set bv ((i * 4) + 3) false; + loop t bv (i + 1) + | '2'::t -> set bv (i * 4) false; + set bv ((i * 4) + 1) true; + set bv ((i * 4) + 2) false; + set bv ((i * 4) + 3) false; + loop t bv (i + 1) + | '3'::t -> set bv (i * 4) true; + set bv ((i * 4) + 1) true; + set bv ((i * 4) + 2) false; + set bv ((i * 4) + 3) false; + loop t bv (i + 1) + | '4'::t -> set bv (i * 4) false; + set bv ((i * 4) + 1) false; + set bv ((i * 4) + 2) true; + set bv ((i * 4) + 3) false; + loop t bv (i + 1) + | '5'::t -> set bv (i * 4) true; + set bv ((i * 4) + 1) false; + set bv ((i * 4) + 2) true; + set bv ((i * 4) + 3) false; + loop t bv (i + 1) + | '6'::t -> set bv (i * 4) false; + set bv ((i * 4) + 1) true; + set bv ((i * 4) + 2) true; + set bv ((i * 4) + 3) false; + loop t bv (i + 1) + | '7'::t -> set bv (i * 4) true; + set bv ((i * 4) + 1) true; + set bv ((i * 4) + 2) true; + set bv ((i * 4) + 3) false; + loop t bv (i + 1) + | '8'::t -> set bv (i * 4) false; + set bv ((i * 4) + 1) false; + set bv ((i * 4) + 2) false; + set bv ((i * 4) + 3) true; + loop t bv (i + 1) + | '9'::t -> set bv (i * 4) true; + set bv ((i * 4) + 1) false; + set bv ((i * 4) + 2) false; + set bv ((i * 4) + 3) true; + loop t bv (i + 1) + | 'a'::t -> set bv (i * 4) false; + set bv ((i * 4) + 1) true; + set bv ((i * 4) + 2) false; + set bv ((i * 4) + 3) true; + loop t bv (i + 1) + | 'b'::t -> set bv (i * 4) true; + set bv ((i * 4) + 1) true; + set bv ((i * 4) + 2) false; + set bv ((i * 4) + 3) true; + loop t bv (i + 1) + | 'c'::t -> set bv (i * 4) false; + set bv ((i * 4) + 1) false; + set bv ((i * 4) + 2) true; + set bv ((i * 4) + 3) true; + loop t bv (i + 1) + | 'd'::t -> set bv (i * 4) true; + set bv ((i * 4) + 1) false; + set bv ((i * 4) + 2) true; + set bv ((i * 4) + 3) true; + loop t bv (i + 1) + | 'e'::t -> set bv (i * 4) false; + set bv ((i * 4) + 1) true; + set bv ((i * 4) + 2) true; + set bv ((i * 4) + 3) true; + loop t bv (i + 1) + | 'f'::t -> set bv (i * 4) true; + set bv ((i * 4) + 1) true; + set bv ((i * 4) + 2) true; + set bv ((i * 4) + 3) true; + loop t bv (i + 1) + else + bv in + loop (String.to_list (String.rev numeral)) bv 0 +;; + +(* TODO: If the length of the bitvector is a multiple of 4, represent with hex.*) +let to_string bv = "#b" ^ (fold bv ~init:"" ~f:(fun acc -> function + | false -> "0" ^ acc + | true -> "1" ^ acc)) +;; + +let rec add bv1 bv2 = + let sum = create bv1.length in + let s, _, _ = fold2 bv1 bv2 ~init:(sum, 0, 0) ~f:(fun (sum, carry, ind) v1 v2 -> + match v1, v2 with + | true, true -> if phys_equal carry 1 + then (set sum ind true; (sum, 1, ind + 1)) + else (set sum ind false; (sum, 1, ind + 1)) + | false, true + | true, false -> if phys_equal carry 1 + then (set sum ind false; (sum, 1, ind + 1)) + else (set sum ind true; (sum, 0, ind + 1)) + | false, false -> if phys_equal carry 1 + then (set sum ind true; (sum, 0, ind + 1)) + else (set sum ind false; (sum, 0, ind + 1))) in + s +;; + +let bvnot bv = + let bv_new = create bv.length in + fold bv ~init:(bv, 0) ~f:(fun (bv, i) v -> + if phys_equal v true then (set bv_new i false; (bv, i + 1)) + else (set bv_new i true; (bv, i + 1))) + ; + bv_new +;; + +let compare bv1 bv2 = + let rec helper ind bv1 bv2 = + if ind >= 0 then + let v1 = get bv1 ind in + let v2 = get bv2 ind in + if phys_equal v1 v2 then helper (ind - 1) bv1 bv2 + else if phys_equal v1 false then -1 else 1 + else + 0 + in + helper (bv1.length - 1) bv1 bv2 +;; + +let bvult bv1 bv2 = + let c = compare bv1 bv2 in + if c >= 0 then false else true +;; + +let bvule bv1 bv2 = + (bvult bv1 bv2) || ((compare bv1 bv2) = 0) +;; + +let concat bv1 bv2 = + let bv3 = create (bv1.length + bv2.length) in + let bv1_, _ = fold bv1 ~init:(bv3, bv2.length) ~f:(fun (bv, i) v -> + set bv i v; (bv, i+1)) in + let bv12, _ = fold bv2 ~init:(bv1_, 0) ~f:(fun (bv, i) v -> + set bv i v; (bv, i+1)) in + bv12 +;; + +let bvuge bv1 bv2 = + (bvult bv2 bv1) || ((compare bv1 bv2) = 0) +;; + +let bvugt bv1 bv2 = + bvult bv2 bv1 +;; + +let bvsub bv1 bv2 = + let const_one = create bv2.length in + set const_one 0 true; + (add bv1 (add (bvnot bv2) const_one)) +;; \ No newline at end of file diff --git a/src/Value.ml b/src/Value.ml index a067bbc..ba1e937 100644 --- a/src/Value.ml +++ b/src/Value.ml @@ -7,7 +7,7 @@ module T = struct | Bool of bool | Char of char | String of string - | BitVec of Bitarray.t + | BitVec of BitarrayExt.t | List of Type.t * t list | Array of Type.t * Type.t * (t * t) list * t (* FIXME: Use HashTable instead of List *) @@ -33,7 +33,7 @@ let rec to_string : t -> string = function | Char c -> "\'" ^ (Char.to_string c) ^ "\'" | String s -> "\"" ^ s ^ "\"" | List _ -> raise (Internal_Exn "List type (de/)serialization not implemented!") - | BitVec bv -> Bitarray.to_string bv + | BitVec bv -> BitarrayExt.to_string bv | Array (key_type, val_type, value, default_v) -> let default_string = "((as const (Array " ^ (Type.to_string key_type) ^ " " ^ (Type.to_string val_type) ^ ")) " ^ (to_string default_v) ^ ")" in List.fold_left ~init:default_string value @@ -48,7 +48,7 @@ let of_atomic_string (s : string) : t = Char (Char.of_string (String.(chop_suffix_exn ~suffix:"\'" (chop_prefix_exn ~prefix:"\'" s)))) with Invalid_argument _ -> try - BitVec (Bitarray.of_string s) + BitVec (BitarrayExt.of_string s) with Invalid_argument _ -> try String String.(chop_suffix_exn ~suffix:"\"" (chop_prefix_exn ~prefix:"\"" s)) with Invalid_argument _ -> From ec8fbd4ad95eb71f6af66ed3f51c9d5e1bfe4a73 Mon Sep 17 00:00:00 2001 From: Adam Stein Date: Mon, 22 Jun 2020 15:10:47 -0700 Subject: [PATCH 18/18] Fix failing build --- test/Test_BitVecComponents.ml | 52 +++++++++++++++++------------------ test/Test_Synthesizer.ml | 10 +++---- 2 files changed, 31 insertions(+), 31 deletions(-) diff --git a/test/Test_BitVecComponents.ml b/test/Test_BitVecComponents.ml index 7a2e4a5..a0a7eca 100644 --- a/test/Test_BitVecComponents.ml +++ b/test/Test_BitVecComponents.ml @@ -21,91 +21,91 @@ let bvsub_eval = (List.find_exn BitVecComponents.all let equal_hex_bin () = - let bv1 = Value.BitVec (Bitarray.of_string "#x1010") in - let bv2 = Value.BitVec (Bitarray.of_string "#b0001000000010000") in + let bv1 = Value.BitVec (BitarrayExt.of_string "#x1010") in + let bv2 = Value.BitVec (BitarrayExt.of_string "#b0001000000010000") in let eq_ret = bveq_eval [bv1; bv2] in let ret = Value.equal (Value.Bool true) eq_ret in Alcotest.(check bool) "identical" true ret let bvadd () = - let bv1 = Value.BitVec (Bitarray.of_string "#b10101010101010101") in - let bv2 = Value.BitVec (Bitarray.of_string "#b01010101010101010") in + let bv1 = Value.BitVec (BitarrayExt.of_string "#b10101010101010101") in + let bv2 = Value.BitVec (BitarrayExt.of_string "#b01010101010101010") in let add_ret = bvadd_eval [bv1; bv2] in - let ret = Value.equal (Value.BitVec (Bitarray.of_string "#b11111111111111111")) add_ret in + let ret = Value.equal (Value.BitVec (BitarrayExt.of_string "#b11111111111111111")) add_ret in Alcotest.(check bool) "identical" true ret let bvadd_ovf () = - let bv1 = Value.BitVec (Bitarray.of_string "#b10101010101010101") in - let bv2 = Value.BitVec (Bitarray.of_string "#b01010101010101011") in + let bv1 = Value.BitVec (BitarrayExt.of_string "#b10101010101010101") in + let bv2 = Value.BitVec (BitarrayExt.of_string "#b01010101010101011") in let add_ret = bvadd_eval [bv1; bv2] in - let ret = Value.equal (Value.BitVec (Bitarray.of_string "#b00000000000000000")) add_ret in + let ret = Value.equal (Value.BitVec (BitarrayExt.of_string "#b00000000000000000")) add_ret in Alcotest.(check bool) "identical" true ret let bvnot () = - let bv = Value.BitVec (Bitarray.of_string "#xa482ad9301") in + let bv = Value.BitVec (BitarrayExt.of_string "#xa482ad9301") in let bvnot_ret = bvnot_eval [bv] in - let ret = Value.equal (Value.BitVec (Bitarray.of_string "#x5b7d526cfe")) bvnot_ret in + let ret = Value.equal (Value.BitVec (BitarrayExt.of_string "#x5b7d526cfe")) bvnot_ret in Alcotest.(check bool) "identical" true ret let bvult_same () = - let bv1 = Value.BitVec (Bitarray.of_string "#x00000000") in + let bv1 = Value.BitVec (BitarrayExt.of_string "#x00000000") in let bvult_ret = bvult_eval [bv1; bv1] in let ret = Value.equal (Value.Bool false) bvult_ret in Alcotest.(check bool) "identical" true ret let bvult_ovf () = - (* bv1 is a bitvector which has a 63bit Bitarray *) + (* bv1 is a bitvector which has a 63bit BitarrayExt *) let bv1 = Value.BitVec - (Bitarray.of_string + (BitarrayExt.of_string "#b111111111111111111111111111111111111111111111111111111111111111") in let bvult_ret = bvult_eval [bv1; bv1] in let ret = Value.equal (Value.Bool false) bvult_ret in Alcotest.(check bool) "identical" true ret let bvult_onegreater () = - let bv1 = Value.BitVec (Bitarray.of_string "#x1") in - let bv2 = Value.BitVec (Bitarray.of_string "#x0") in + let bv1 = Value.BitVec (BitarrayExt.of_string "#x1") in + let bv2 = Value.BitVec (BitarrayExt.of_string "#x0") in let bvult_ret = bvult_eval [bv2; bv1] in let ret = Value.equal (Value.Bool true) bvult_ret in Alcotest.(check bool) "identical" true ret let bvuge () = - let bv1 = Value.BitVec (Bitarray.of_string "#xff") in - let bv2 = Value.BitVec (Bitarray.of_string "#b11111111") in + let bv1 = Value.BitVec (BitarrayExt.of_string "#xff") in + let bv2 = Value.BitVec (BitarrayExt.of_string "#b11111111") in let bvuge_ret = bvuge_eval [bv2; bv1] in let ret = Value.equal (Value.Bool true) bvuge_ret in Alcotest.(check bool) "identical" true ret let bvugt () = - let bv1 = Value.BitVec (Bitarray.of_string "#xa") in - let bv2 = Value.BitVec (Bitarray.of_string "#b1000") in + let bv1 = Value.BitVec (BitarrayExt.of_string "#xa") in + let bv2 = Value.BitVec (BitarrayExt.of_string "#b1000") in let bvugt_ret = bvugt_eval [bv1; bv2] in let ret = Value.equal (Value.Bool true) bvugt_ret in Alcotest.(check bool) "identical" true ret let bvule () = - let bv1 = Value.BitVec (Bitarray.of_string "#x1") in - let bv2 = Value.BitVec (Bitarray.of_string "#xb") in + let bv1 = Value.BitVec (BitarrayExt.of_string "#x1") in + let bv2 = Value.BitVec (BitarrayExt.of_string "#xb") in let bvule_ret = bvult_eval [bv1; bv2] in let ret = Value.equal (Value.Bool true) bvule_ret in Alcotest.(check bool) "identical" true ret let bvsub () = - let bv1 = Value.BitVec (Bitarray.of_string "#b00") in - let bv2 = Value.BitVec (Bitarray.of_string "#b01") in + let bv1 = Value.BitVec (BitarrayExt.of_string "#b00") in + let bv2 = Value.BitVec (BitarrayExt.of_string "#b01") in let bvsub_ret = bvsub_eval [bv1; bv2] in (* We should get the representation for -1 *) - let ret = Value.equal (Value.BitVec (Bitarray.of_string "#b11")) bvsub_ret in + let ret = Value.equal (Value.BitVec (BitarrayExt.of_string "#b11")) bvsub_ret in Alcotest.(check bool) "identical" true ret let bv_pp f p = match p with - | Value.BitVec ba -> Format.fprintf f "%s\n" (Bitarray.to_string ba) + | Value.BitVec ba -> Format.fprintf f "%s\n" (BitarrayExt.to_string ba) | _ -> Format.fprintf f "Error with pretty printing the BitVector\n" let bitvec_testable = Alcotest.testable bv_pp (fun x y -> Value.equal (Value.Bool true) (bveq_eval [x; y])) -let gen () = +let gen () = let bvgen1 = TestGen.for_type (Type.BITVEC 32) in let bvgen2 = TestGen.for_type (Type.BITVEC 32) in Alcotest.(check (neg bitvec_testable)) "identical" diff --git a/test/Test_Synthesizer.ml b/test/Test_Synthesizer.ml index ed8e39f..2d19fd9 100644 --- a/test/Test_Synthesizer.ml +++ b/test/Test_Synthesizer.ml @@ -183,10 +183,10 @@ let all_mapR_ge_l_0 () = let bvadd_a_b () = let result = solve ~config:{ Config.default with logic = Logic.of_string "BV" } { arg_names = ["a"; "b"]; - inputs = List.map ~f:(fun a -> Array.map ~f:(fun x -> Value.BitVec (Bitarray.of_string x)) a) + inputs = List.map ~f:(fun a -> Array.map ~f:(fun x -> Value.BitVec (BitarrayExt.of_string x)) a) [ [| "#b00"; "#b01" ; "#b10" ; "#b11" |] ; [| "#b01"; "#b10" ; "#b11" ; "#b00"|]]; - outputs = Array.map ~f:(fun x -> Value.BitVec (Bitarray.of_string x)) + outputs = Array.map ~f:(fun x -> Value.BitVec (BitarrayExt.of_string x)) [| "#b01"; "#b11"; "#b01" ; "#b11" |]; constants = [] } in Alcotest.(check string) "identical" "(bvadd a b)" result.string @@ -194,7 +194,7 @@ let bvadd_a_b () = let bvult_a_b () = let result = solve ~config:{ Config.default with logic = Logic.of_string "BV" } { arg_names = ["a"; "b"]; - inputs = List.map ~f:(fun a -> Array.map ~f:(fun x -> Value.BitVec (Bitarray.of_string x)) a) + inputs = List.map ~f:(fun a -> Array.map ~f:(fun x -> Value.BitVec (BitarrayExt.of_string x)) a) [ [| "#b00"; "#b01" ; "#b10" ; "#b11"|] ; [| "#b01"; "#b10" ; "#b11" ; "#b00"|]]; outputs = Array.map ~f:(fun b -> Value.Bool b) @@ -205,10 +205,10 @@ let bvult_a_b () = let bvnot_bvsub_a_b () = let result = solve ~config:{ Config.default with logic = Logic.of_string "BV" } { arg_names = ["a"; "b"]; - inputs = List.map ~f:(fun a -> Array.map ~f:(fun x -> Value.BitVec (Bitarray.of_string x)) a) + inputs = List.map ~f:(fun a -> Array.map ~f:(fun x -> Value.BitVec (BitarrayExt.of_string x)) a) [ [| "#b0000"; "#b0010" ; "#b1000" ; "#b1100"|] ; [| "#b0100"; "#b1000" ; "#b1100" ; "#b0000"|]]; - outputs = Array.map ~f:(fun x -> Value.BitVec (Bitarray.of_string x)) + outputs = Array.map ~f:(fun x -> Value.BitVec (BitarrayExt.of_string x)) [|"#b0011"; "#b0101"; "#b0011"; "#b0011"|]; constants = [] } in Alcotest.(check string) "identical" "(bvnot (bvsub a b))" result.string