Shifts are tested and seem operational. Only missing arithmetic and inequalities at this point

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}

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]