diff --git a/src/bv.ml b/src/bv.ml
index b29e8817065bada5c9e427af451b8956683a0e12..ce32f5cfdcce2553bf1d19ed8e24707e32d1b75d 100644
--- a/src/bv.ml
+++ b/src/bv.ml
@@ -26,6 +26,8 @@ open Solver
let lazy_propagation = false
+
+
let debug = Debug.register_info_flag
~desc:"for bit-vectors theory"
"bv"
@@ -53,15 +55,25 @@ type bvdom = {aun : Z.t; azer : Z.t}
(* end *)
let dom : bvdom dom = Dom.create_key "bvdom"
+let domlen x = max (Z.numbits x.aun) (Z.numbits x.azer)
let bvmeet x y = Z.({aun = logor x.aun y.aun ; azer = logand x.azer y.azer})
let bneg x = Z.({aun = lognot x.azer ; azer = lognot x.aun})
let bveqdom x y = Z.equal x.aun y.aun && Z.equal x.azer y.azer
let bvconflict x = not (Z.equal Z.(logand (lognot x.azer) x.aun) Z.zero)
let normalshift shift_op x n =
Z.({aun = shift_op x.aun n; azer = shift_op x.azer n})
-let unknownshift shift_op x n=
+
+let shifted_ones shift_op x n =
+if (shift_op Z.one 1 == (Z.of_int 2)) then (* it's << *)
+ Z.lognot (shift_op Z.minus_one n)
+else (* it's >>, so use << *)
+ let len = domlen x in
+ Z.shift_left Z.minus_one (len - n)
+
+let unknownshift shift_op x n =
+ let ones = shifted_ones shift_op x n in
Z.({aun = shift_op x.aun n;
- azer = logor (shift_op x.azer n) (lognot (shift_op one n)) })
+ azer = logor (shift_op x.azer n) ones })
let bvfixed x = if Z.equal x.aun x.azer then Some x.aun else None
@@ -108,8 +120,7 @@ module D = struct
Format.pp_print_string fmt to_print
let print fmt interval =
- let len = 1 + max (Z.numbits interval.aun) (Z.numbits interval.azer) in
- let len = max len 1 in
+ let len = 1 + domlen interval in
(** Here we print most significant bit first *)
let to_print =
"["^ String.init len
@@ -132,6 +143,16 @@ end
module DE = RegisterDom(D)
+(* Useful utils: removable *)
+let simpleprint var env str=
+ let xd = D.get_dom_bv env dom var in
+ Format.print_string ("\n"^ str);
+ D.print Format.std_formatter xd;
+ Format.print_string "\n"
+let simpledomprint xd str=
+ Format.print_string ("\n"^ str);
+ D.print Format.std_formatter xd;
+ Format.print_string "\n"
module T = struct
type t = bvexp
@@ -152,8 +173,8 @@ module T = struct
| Band (a,b) -> 11 * (Cl.hash a) + 13 * (Cl.hash b)
| Bnot a -> 17 * Cl.hash a
| Cst i -> Z.hash i
- | Bsr (a,n) -> 19 * (Cl.hash a) + Cl.hash n
- | Bsl (a,n) -> 23 * (Cl.hash a) + Cl.hash n
+ | Bsr (a,n) -> 19 * (Cl.hash a) + 31 * (Cl.hash n)
+ | Bsl (a,n) -> 23 * (Cl.hash a) + 33 * (Cl.hash n)
let compare n m =
match n, m with
@@ -304,16 +325,20 @@ module DaemonPropa = struct
let dom_set_or_merge ds exp c domc =
match bvfixed domc with
|None -> D.set_dom_bv ds exp c domc
- |Some def ->
- let cst = index_aux (Cst def) in
+ |Some i ->
+ let cst = index_aux (Cst i) in
+ Solver.Delayed.register ds cst;
+ Solver.Delayed.flush ds;
+ (* let pexp = Explanation.pexpfact in *)
+ (* D.set_dom_bv ds pexp cst {aun = i; azer = i}; *)
Delayed.merge ds exp c cst
let generic_shift d sh_op inv_op clsem c off =
let offset = D.get_dom_bv d dom off in
match bvfixed offset with
| None -> ()
- | Some n ->
- let n = Z.to_int n in
+ | Some nn ->
+ let n = Z.to_int nn in
let cl = ThE.cl clsem in
let dc = D.get_dom_bv d dom c in
let dcl = D.get_dom_bv d dom cl in
@@ -326,8 +351,8 @@ module DaemonPropa = struct
let pexp1 = Delayed.mk_pexp d expprop (ExpInvBV (clsem, Left)) in
(* I also want an explanation that says
"it's because the offset became fixed" *)
- dom_set_or_merge d pexp c ndc;
- dom_set_or_merge d pexp1 cl ndcl
+ dom_set_or_merge d pexp1 c ndc;
+ dom_set_or_merge d pexp cl ndcl
let generic_prop d prop_fun clsem c1 c2 =
let cl = ThE.cl clsem in
@@ -367,8 +392,8 @@ module DaemonPropa = struct
| Bor (c1, c2) -> generic_prop d or_prop clsem c1 c2
| Band (c1, c2) -> generic_prop d and_prop clsem c1 c2
| Bxor (c1, c2) -> generic_prop d xor_prop clsem c1 c2
- | Bsr (c, off) -> generic_shift d (Z.shift_left) (Z.shift_right) clsem c off
- | Bsl (c, off) -> generic_shift d (Z.shift_right) (Z.shift_left) clsem c off
+ | Bsl (c, off) -> generic_shift d (Z.shift_left) (Z.shift_right) clsem c off
+ | Bsr (c, off) -> generic_shift d (Z.shift_right) (Z.shift_left) clsem c off
| _ -> failwith "should be impossible"
end
| _ -> raise UnwaitedEvent
@@ -378,10 +403,10 @@ module DaemonPropa = struct
let ctxt = ThE.cl clsem in
match v with
| Bor (c1,c2)
-| Band (c1, c2)
-| Bxor (c1,c2)
-| Bsr (c1,c2)
-| Bsl (c1,c2) ->
+ | Band (c1, c2)
+ | Bxor (c1,c2)
+ | Bsr (c1,c2)
+ | Bsl (c1,c2) ->
let events = [Demon.Create.EventDom (c1,dom,clsem);
Demon.Create.EventDom (c2,dom,clsem);
Demon.Create.EventDom (ctxt,dom,clsem)] in
@@ -391,7 +416,7 @@ module DaemonPropa = struct
let events = [Demon.Create.EventDom (c,dom,clsem);
Demon.Create.EventDom (ctxt,dom,clsem)] in
Demon.Fast.attach d key events;
- wakeup d (Events.Fired.EventDom(c, dom, clsem))
+ wakeup d (Events.Fired.EventDom(ctxt, dom, clsem))
| Cst i ->
let pexp = Explanation.pexpfact in
D.set_dom_bv d pexp ctxt {aun = i; azer = i}
diff --git a/tests/tests_bv.ml b/tests/tests_bv.ml
index 492fa3d7cbc6442ea4a0c3ec6ea6b0de6e8b77ac..bc2de26424b5086835bd5c1d248bd859cc5057c4 100644
--- a/tests/tests_bv.ml
+++ b/tests/tests_bv.ml
@@ -41,7 +41,7 @@ let tests_pretty_print () =
test "[0??????]" Z.zero _63;
test "[0XXXXX0]" _62 Z.zero
-let simpleprint var env str=
+let simpleprint var env str =
let xd = Bv.D.get_dom_bv env Bv.dom var in
Format.print_string str;
Bv.D.print Format.std_formatter xd;
@@ -52,6 +52,8 @@ type bvtestexp =
|Tand of bvtestexp * bvtestexp
|Txor of bvtestexp * bvtestexp
|Tnot of bvtestexp
+|Tsl of bvtestexp * bvtestexp
+|Tsr of bvtestexp * bvtestexp
|Tcst of int
|Tvar of string
|Tcl of Popop.Types.Cl.t
@@ -79,6 +81,16 @@ let rec testexp_to_test (e: bvtestexp) env =
let cc = testexp_to_test c env in
propagate_all env [bb;cc];
Bv._bxor bb cc
+ | Tsl (b,c) ->
+ let bb = testexp_to_test b env in
+ let cc = testexp_to_test c env in
+ propagate_all env [bb;cc];
+ Bv._bsl bb cc
+ | Tsr(b,c) ->
+ let bb = testexp_to_test b env in
+ let cc = testexp_to_test c env in
+ propagate_all env [bb;cc];
+ Bv._bsr bb cc
| Tnot c ->
let cc = testexp_to_test c env in
register env cc;
@@ -104,47 +116,46 @@ let simple_tests num () =
let y = Variable.fresh Bv.ty "y" in
let t = Variable.fresh Bv.ty "t" in
let z = Variable.fresh Bv.ty "z" in
+ let r = Variable.fresh Bv.ty "r" in
let cl_one = Bv._cnst (-1) in
let cl_zero = Bv._cnst 0 in
- propagate_all env [cl_one; cl_zero;x;y];
+ propagate_all env [cl_one; cl_zero;x;y;t;z;r];
match num with
- | 1 -> (* x = Cst 1 [Passed]*)
+ | 1 -> (* x = Cst 1 *)
merge env x cl_one;
assert_bool "x=1(Cl)" (is_equal env x cl_one)
- | 2 -> (* x|y = 0 [Passed]*)
+ | 2 -> (* x|y = 0 *)
let lside = Bv._bor x y in
propagate_all env [lside];
merge env lside cl_zero ;
assert_bool "x|y = 0" (is_equal env lside cl_zero);
assert_bool "x=0" (is_equal env x cl_zero);
- assert_bool "y=0" (is_equal env y cl_zero);
+ assert_bool "y=0" (is_equal env y cl_zero)
- | 3 -> (* x & y = 1 [Passed]*)
+ | 3 -> (* x & y = 1 *)
let lside = Bv._band x y in
propagate_all env [lside];
merge env lside cl_one;
assert_bool "x&y = 1" (is_equal env lside cl_one);
assert_bool "x=1" (is_equal env x cl_one);
- assert_bool "y=1" (is_equal env y cl_one);
-
+ assert_bool "y=1" (is_equal env y cl_one)
- | 4 -> (* x & 1 = 0 [Passed] *)
+ | 4 -> (* x & 1 = 0 *)
let lside = Bv._band x cl_one in
propagate_all env [lside];
merge env lside cl_zero;
assert_bool "x & 1 = 0" (is_equal env lside cl_zero);
- assert_bool "x=0" (is_equal env x cl_zero);
-
+ assert_bool "x=0" (is_equal env x cl_zero)
- | 5 -> (* x | 0 = 1 [Passed] *)
+ | 5 -> (* x | 0 = 1 *)
let lside = Bv._bor x cl_zero in
propagate_all env [lside];
merge env lside cl_one;
assert_bool "x | 0 = 1" (is_equal env lside cl_one);
assert_bool "x = 1" (is_equal env x cl_one)
- | 6 -> (* x = not 0 [PASSED]*)
+ | 6 -> (* x = not 0 *)
let rside = Bv._bnot cl_zero in
register env rside;
register env cl_zero;
@@ -163,10 +174,10 @@ let simple_tests num () =
| 9 ->
(*
- a- z ⊕ 101 = (x & y) | (t & y)
- b- y ⊕ x = 110
- c- t & x = 100
- d- z ⊕ t = 010
+ a- z ⊕ 101 = (x & y) | (t & y)
+ b- y ⊕ x = 110
+ c- t & x = 100
+ d- z ⊕ t = 010
e- t = 100
*)
let exmp =
@@ -192,10 +203,29 @@ let simple_tests num () =
assert_bool "y = 011" (is_equal env y (Bv._cnst 3));
assert_bool "z = 100" (is_equal env z (Bv._cnst 7));
assert_bool "t = 100" (is_equal env t (Bv._cnst 4));
- (* simpleprint x env "\nx="; *)
- (* simpleprint y env "y="; *)
- (* simpleprint z env "z="; *)
- (* simpleprint t env "t=" *)
+ (* simpleprint x env "\nx="; *)
+ (* simpleprint y env "y="; *)
+ (* simpleprint z env "z="; *)
+ (* simpleprint t env "t=" *)
+
+ | 10 -> (* 100 >> 2 = r *)
+ let exmp = [ Tsr (Tcst 4, Tcst 2), Tcl r] in
+ constraint_list exmp env;
+ assert_bool "r = 01" (is_equal env r (Bv._cnst 1));
+
+ | 11 -> (* x << 1 = 1010 ==> x = ?101*)
+ let exmp =
+ [(Tsl (Tcl x, Tcst 1), Tcst 10);
+ (Tand (Tcl x, Tcl cl_one), Tcst 5)] in
+ constraint_list exmp env;
+ assert_bool "x = 101" (is_equal env x (Bv._cnst 5));
+
+ | 12 -> (* x >> 1 = 1010 ==> x = 01010?*)
+ let exmp =
+ [(Tsr (Tcl x, Tcst 1), Tcst 10);
+ (Tor (Tcl x, Tcl cl_zero), Tcst 20)] in
+ constraint_list exmp env;
+ assert_bool "x = 10100" (is_equal env x (Bv._cnst 20));
| _ -> failwith "No test by that number in tests_bv.ml"
@@ -215,6 +245,6 @@ let rec gen_tests = function
(simple_tests x)) :: gen_tests rest
let basic = "Bv.Basic" >::: ((
- "pretty print" >:: tests_pretty_print) :: (gen_tests (gen_list 1 (incr 9))) )
+ "pretty print" >:: tests_pretty_print) :: (gen_tests (gen_list 1 (incr 12))) )
let tests = TestList[basic]