Skip to content
This repository has been archived by the owner on Mar 16, 2024. It is now read-only.

Support for Bit Vectors #13

Open
wants to merge 20 commits into
base: master
Choose a base branch
from
Open

Support for Bit Vectors #13

Show file tree
Hide file tree
Changes from 9 commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
bb985c0
Parsing of bitvector types.
adaminsky Nov 17, 2019
65216ba
Add the Bitvector type to functions which accept Type.t as input
adaminsky Nov 17, 2019
df78d32
Use the Bitarray module instead of a string for bit vectors
adaminsky Nov 26, 2019
2ccc228
Add BitVecComponents.ml which implements bvadd, bvult, and bvnot, and…
adaminsky Dec 16, 2019
828e319
Remove unnecessary comment
adaminsky Dec 16, 2019
4ac1c2a
Add the is_argument_valid functions for bitvectors
adaminsky Dec 17, 2019
581440a
Merge upstream changes and make BITVEC type hold the length as a string
adaminsky Dec 18, 2019
e8eaf73
Change BITVEC type to use TVAR for its size and correctly unify
adaminsky Jan 18, 2020
810a481
Add random bitvector generation
adaminsky Jan 18, 2020
efae245
Add unit tests for operations on BitVec and Bitarray
adaminsky Jan 26, 2020
99ea8c4
Change the BITVEC type to be of int and perform BitVec generation per…
adaminsky Feb 12, 2020
0a6caf9
Remove all integer to string conversions from bitvec unification
adaminsky Feb 28, 2020
6c15ad6
Fix Bitvec unification bug with ordering of arguments
adaminsky Feb 28, 2020
dc41d5a
Add tests for BitVec synthesis and unification
adaminsky Apr 5, 2020
d2af30b
Add more complex BitVec synthesis test
adaminsky Apr 7, 2020
e4a27d5
Remove unnecessary code and comments
adaminsky Apr 7, 2020
f83bf06
Merge branch 'master' into BitVectors
SaswatPadhi Apr 23, 2020
26154cc
Remove newline at end of files
adaminsky Jun 19, 2020
7b14015
Refactor bitarray to separate module
adaminsky Jun 22, 2020
ec8fbd4
Fix failing build
adaminsky Jun 22, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
95 changes: 95 additions & 0 deletions src/BitVecComponents.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,95 @@
open Base
open Exceptions
open Expr

let all = [
{
name = "bv-eq";
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.compare v1 v2) = 0));
to_string = (fun [@warning "-8"] [v1;v2] -> "(= " ^ v1 ^ " " ^ v2 ^ ")");
global_constraints = (fun _ -> []);
} ;
{
name = "bvnot";
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));
to_string = (fun [@warning "-8"] [a] -> "(bvnot " ^ a ^ ")");
global_constraints = (fun _ -> []);
} ;
{
name = "bvult";
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.bvult v1 v2));
to_string = (fun [@warning "-8"] [a ; b] -> "(bvult " ^ a ^ " " ^ b ^ ")");
global_constraints = (fun _ -> []);
} ;
{
name = "bvadd";
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 |]
202 changes: 201 additions & 1 deletion src/Bitarray.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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 = {
Expand Down Expand Up @@ -68,6 +72,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
Expand All @@ -78,6 +83,16 @@ let fold =
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 =
Expand All @@ -90,4 +105,189 @@ 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))
;;
6 changes: 5 additions & 1 deletion src/Logic.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,10 @@ 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;
sample_set_size_multiplier = 1
} ; {
name = "ALL" ;
(* FIXME: The verification side for lists, especially with transformed components,
doesn't work as of now -- we need to emit valid SMTLIB expressions for them *)
Expand All @@ -46,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
2 changes: 1 addition & 1 deletion src/SyGuS.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -166,4 +166,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 *)
Loading