Merge pull request #12 from ManuelLerchner/bitfield-shifts

Bitfield shifts

src/cdomain/value/cdomains/intDomain.ml

@@ -1189,16 +1189,29 @@ struct
   let project ik p t = t
 end
 
-module BitFieldArith (Ints_t : IntOps.IntOps) = struct
-  let zero_mask = Ints_t.zero
-  let one_mask = Ints_t.lognot zero_mask
+(* Bitfield arithmetic, without any overflow handling etc. *)
+module BitfieldArith (Ints_t : IntOps.IntOps) = struct
 
   let of_int x = (Ints_t.lognot x, x) 
-  let join (z1,o1) (z2,o2) = (Ints_t.logor z1 z2, Ints_t.logor o1 o2)
 
+  let one = of_int Ints_t.one
+  let zero = of_int Ints_t.zero
+
+  let zero_mask = Ints_t.zero
+  let one_mask = Ints_t.lognot zero_mask
+
+  let join (z1,o1) (z2,o2) = (Ints_t.logor z1 z2, Ints_t.logor o1 o2)
   let meet (z1,o1) (z2,o2) = (Ints_t.logand z1 z2, Ints_t.logand o1 o2)
 
-  let is_constant (z,o) = (Ints_t.logxor z o) = one_mask
+  let top_bool = join one zero
+
+  let bits_known (z,o) = Ints_t.logxor z o
+  let bits_unknown bf = Ints_t.lognot @@ bits_known bf
+  let bits_set bf = Ints_t.logand (snd bf) @@ bits_known bf
+  let bits_undef (z,o) = Ints_t.lognot (Ints_t.logxor z o)
+
+  let is_const (z,o) = (Ints_t.logxor z o) = one_mask
+  let is_undef (z,o) = Ints_t.compare (bits_undef (z,o)) Ints_t.zero != 0
 
   let nabla x y= if x = Ints_t.logor x y then x else one_mask
 
@@ -1213,55 +1226,115 @@ module BitFieldArith (Ints_t : IntOps.IntOps) = struct
 
   let logor (z1,o1)  (z2,o2) = (Ints_t.logand z1 z2, Ints_t.logor o1 o2)
 
-  let min ik (z,o) = 
-    let knownBitMask = Ints_t.logxor z o in
-    let unknownBitMask = Ints_t.lognot knownBitMask in
-    let impossibleBitMask = Ints_t.lognot (Ints_t.logor z o) in
-    let guaranteedBits = Ints_t.logand o knownBitMask in
+  let make_bitone_msk pos = Ints_t.shift_left Ints_t.one pos
+  let make_bitzero_msk pos = Ints_t.lognot @@ make_bitone_msk pos
+  let make_lsb_bitmask pos = Ints_t.sub (make_bitone_msk pos) Ints_t.one
+  let make_msb_bitmask pos = Ints_t.lognot @@ make_lsb_bitmask pos
 
-    if impossibleBitMask <> zero_mask then
-      failwith "Impossible bitfield"
+  let get_bit bf pos = Ints_t.logand Ints_t.one @@ Ints_t.shift_right bf (pos-1)
+  let set_bit ?(zero=false) bf pos =
+    if zero then
+      Ints_t.logand bf @@ make_bitzero_msk pos
     else
+      Ints_t.logor bf @@ make_bitone_msk pos
 
-    if isSigned ik then
-      let signBitMask = Ints_t.shift_left Ints_t.one (Size.bit ik - 1) in
-      let worstPossibleUnknownBits = Ints_t.logand unknownBitMask signBitMask in
-      Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits))
-    else
-      let worstPossibleUnknownBits = Ints_t.logand unknownBitMask zero_mask in
-      Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits))
-
-  let max ik (z,o) =
-    let knownBitMask = Ints_t.logxor z o in
-    let unknownBitMask = Ints_t.lognot knownBitMask in
-    let impossibleBitMask = Ints_t.lognot (Ints_t.logor z o) in
-    let guaranteedBits = Ints_t.logand o knownBitMask in
-
-    if impossibleBitMask <> zero_mask then
-      failwith "Impossible bitfield"
-    else
-
-    let (_,fullMask) = Size.range ik in
-    let worstPossibleUnknownBits = Ints_t.logand unknownBitMask (Ints_t.of_bigint fullMask) in
+  let log2_bitcnt ik =
+    let ilog2 n =
+      let rec aux n acc =
+        if n <= 1 then acc
+        else aux (n lsr 1) (acc + 1)
+      in aux n 0
+    in ilog2 (Size.bit ik)
 
-    if isSigned ik then
-      Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits))
+  let break_down_lsb ik (z,o) : (Ints_t.t * Ints_t.t) list option = if is_undef (z,o) then None
     else
-      Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits))
-
-
-  let one = of_int Ints_t.one
-  let zero = of_int Ints_t.zero
-  let top_bool = join one zero
+      let rec break_down c_lst i = if i < 0 then c_lst
+      else
+        if get_bit z i = get_bit o i then
+          List.fold_left2 (
+            fun acc (z1,o1) (z2,o2) -> (set_bit z1 i, set_bit ~zero:true o1 i) :: (set_bit ~zero:true z2 i, o2) :: acc
+          ) [] c_lst c_lst
+          |> fun c_lst -> break_down c_lst (i-1)
+        else
+          break_down c_lst (i-1)
+      in
+      let lsb_bitcnt_log_ik = log2_bitcnt ik + 1 in (* ilog2 bitcnt of ik ceiled *)
+      let pfx_msk = make_msb_bitmask lsb_bitcnt_log_ik in
+      let sufx_msk = make_lsb_bitmask lsb_bitcnt_log_ik in
+      let msb_msk = Ints_t.logand (bits_set (z,o)) pfx_msk in (* shift a b = zero when min{b} > ceil(ilog2 a) *)
+      if Ints_t.compare msb_msk Ints_t.zero = 0
+        then break_down [(Ints_t.logand z pfx_msk, Ints_t.logand o sufx_msk)] (lsb_bitcnt_log_ik - 1) |> Option.some
+        else Some ([of_int @@ Ints_t.of_int (lsb_bitcnt_log_ik)])
+
+  let break_down ik bf = Option.map (fun c_bf_lst -> List.map snd c_bf_lst |> List.map Ints_t.to_int) (break_down_lsb ik bf)
+
+  let shift_right ik bf n_bf =
+    let shift_right (z,o) c =
+      let sign_msk = Ints_t.shift_left one_mask (Size.bit ik - c) in
+      if (isSigned ik) && ((Ints_t.to_int o) < 0) then
+        (Ints_t.shift_right z c, Ints_t.logor (Ints_t.shift_right o c) sign_msk)
+      else
+        (Ints_t.logor (Ints_t.shift_right z c) sign_msk, Ints_t.shift_right o c)
+    in
+    if is_const n_bf then Some (shift_right bf (Ints_t.to_int @@ snd n_bf))
+    else Option.map (fun c_lst -> List.map (shift_right bf) c_lst |> List.fold_left join zero) (break_down ik n_bf)
 
+  let shift_left ik bf n_bf =
+    let shift_left (z,o) c =
+        let z_msk = Ints_t.sub (Ints_t.shift_left Ints_t.one c) Ints_t.one in
+        (Ints_t.logor (Ints_t.shift_left z c) z_msk, Ints_t.shift_left o c)
+    in
+    if is_const n_bf then Some (shift_left bf (Ints_t.to_int @@ snd n_bf))
+    else Option.map (fun c_lst -> List.map (shift_left bf) c_lst |> List.fold_left join zero) (break_down ik n_bf)
+
+    let min ik (z,o) = 
+      let knownBitMask = Ints_t.logxor z o in
+      let unknownBitMask = Ints_t.lognot knownBitMask in
+      let impossibleBitMask = Ints_t.lognot (Ints_t.logor z o) in
+      let guaranteedBits = Ints_t.logand o knownBitMask in
+
+      if impossibleBitMask <> zero_mask then
+        failwith "Impossible bitfield"
+      else
+
+      if isSigned ik then
+        let signBitMask = Ints_t.shift_left Ints_t.one (Size.bit ik - 1) in
+        let worstPossibleUnknownBits = Ints_t.logand unknownBitMask signBitMask in
+        Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits))
+      else
+        let worstPossibleUnknownBits = Ints_t.logand unknownBitMask zero_mask in
+        Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits))
+
+    let max ik (z,o) =
+      let knownBitMask = Ints_t.logxor z o in
+      let unknownBitMask = Ints_t.lognot knownBitMask in
+      let impossibleBitMask = Ints_t.lognot (Ints_t.logor z o) in
+      let guaranteedBits = Ints_t.logand o knownBitMask in
+
+      if impossibleBitMask <> zero_mask then
+        failwith "Impossible bitfield"
+      else
+
+      let (_,fullMask) = Size.range ik in
+      let worstPossibleUnknownBits = Ints_t.logand unknownBitMask (Ints_t.of_bigint fullMask) in
+
+      if isSigned ik then
+        Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits))
+      else
+        Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits))
+
+
+    let one = of_int Ints_t.one
+    let zero = of_int Ints_t.zero
+    let top_bool = join one zero
+
 end
 
 module BitFieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) = struct
   let name () = "bitfield"
   type int_t = Ints_t.t
   type t = (Ints_t.t * Ints_t.t) [@@deriving eq, ord, hash]
-
-  module BArith = BitFieldArith (Ints_t)
+  module BArith = BitfieldArith (Ints_t)
 
   let top () = (BArith.one_mask, BArith.one_mask)
   let bot () = (BArith.zero_mask, BArith.zero_mask)
@@ -1270,8 +1343,6 @@ module BitFieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
 
   let range ik bf = (BArith.min ik bf, BArith.max ik bf)
 
-  let get_bit n i = (Ints_t.logand (Ints_t.shift_right n (i-1)) Ints_t.one) 
-
   let norm ?(suppress_ovwarn=false) ik (z,o) = 
     let (min_ik, max_ik) = Size.range ik in
 
@@ -1281,8 +1352,8 @@ module BitFieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
 
     let new_bitfield=
       (if isSigned ik then
-         let newz = Ints_t.logor (Ints_t.logand z (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (get_bit z (Size.bit ik))) in
-         let newo = Ints_t.logor (Ints_t.logand o (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (get_bit o (Size.bit ik))) in
+         let newz = Ints_t.logor (Ints_t.logand z (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (BArith.get_bit z (Size.bit ik))) in
+         let newo = Ints_t.logor (Ints_t.logand o (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (BArith.get_bit o (Size.bit ik))) in
          (newz,newo)
        else
          let newz = Ints_t.logor z (Ints_t.neg (Ints_t.of_bigint max_ik)) in
@@ -1296,7 +1367,7 @@ module BitFieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     if t = bot () then "bot" else
     if t = top () then "top" else
       let (z,o) = t in
-      if BArith.is_constant t then 
+      if BArith.is_const t then 
         Format.sprintf "[%08X, %08X] (unique: %d)" (Ints_t.to_int z) (Ints_t.to_int o) (Ints_t.to_int o)
       else 
         Format.sprintf "[%08X, %08X]" (Ints_t.to_int z) (Ints_t.to_int o)
@@ -1315,8 +1386,8 @@ module BitFieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
   let of_int ik (x: int_t) = (norm ik @@ BArith.of_int x) 
 
   let to_int (z,o) = if is_bot (z,o) then None else
-    if BArith.is_constant (z,o) then Some o
-    else None
+      if BArith.is_const (z,o) then Some o
+      else None
 
   let equal_to i bf = 
     if BArith.of_int i = bf then `Eq
@@ -1371,10 +1442,13 @@ module BitFieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
 
   let lognot ik i1 = BArith.lognot i1
 
-  let shift_right ik a b = (top_of ik,{underflow=false; overflow=false})
-
-  let shift_left ik a b = (top_of ik,{underflow=false; overflow=false})
+  let shift_right ik a b = 
+    M.trace "bitfield" "shift_right";
+    norm ik @@ (BArith.shift_right ik a b |> Option.value ~default: (bot ()))
 
+  let shift_left ik a b =
+    M.trace "bitfield" "shift_left";
+    norm ik @@ (BArith.shift_left ik a b |> Option.value ~default: (bot ()))
 
   (* Arith *)
 
@@ -1446,12 +1520,12 @@ module BitFieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     ((!z3, !o3),{underflow=false; overflow=false})
 
   let rec div ?no_ov ik (z1, o1) (z2, o2) =
-    if BArith.is_constant (z1, o1) && BArith.is_constant (z2, o2) then (let res = Ints_t.div z1 z2 in ((res, Ints_t.lognot res),{underflow=false; overflow=false}))
+    if BArith.is_const (z1, o1) && BArith.is_const (z2, o2) then (let res = Ints_t.div z1 z2 in ((res, Ints_t.lognot res),{underflow=false; overflow=false}))
     else (top_of ik,{underflow=false; overflow=false})
 
   let rem ik x y = 
     M.trace "bitfield" "rem";
-    if BArith.is_constant x && BArith.is_constant y then (
+    if BArith.is_const x && BArith.is_const y then (
     (* x % y = x - (x / y) * y *)
     let tmp = fst (div ik x y) in
     let tmp = fst (mul ik tmp y) in 
@@ -1479,6 +1553,7 @@ module BitFieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     else if (BArith.min ik x) >= (BArith.max ik y) then of_bool ik false 
     else BArith.top_bool
 
+
   let gt ik x y = lt ik y x
 
   let invariant_ikind e ik (z,o) = 

tests/unit/cdomains/intDomainTest.ml

@@ -461,10 +461,32 @@ module I = IntDomain.SOverflowUnlifter (I)
     assert_bool "-5 ?= not (4 | 12)" (I.equal_to (of_int (-5)) (I.lognot ik b12) = `Top)
 
   let test_shift_left _ =
-    ()
+    let stat1 = I.of_int ik (of_int 2) in
+    let stat2 = I.of_int ik (of_int 1) in
+    let eval = (I.shift_left ik stat1 stat2) in
+    let eq = (of_int(4)) in
+    assert_bool ("2 << 1 should be: \"4\" but was: \"" ^ I.show eval ^ "\"") (I.equal_to eq eval = `Eq);
+
+    let stat1 = I.of_int ik (of_int (-2)) in
+    let stat2 = I.of_int ik (of_int 1) in
+    let eval = (I.shift_left ik stat1 stat2) in
+    let eq = (of_int(-4)) in
+    assert_bool ("2 << 1 should be: \"4\" but was: \"" ^ I.show eval ^ "\"") (I.equal_to eq eval = `Eq)
+
 
   let test_shift_right _ =
-    ()
+    let stat1 = I.of_int ik (of_int (4)) in
+    let stat2 = I.of_int ik (of_int 1) in
+    let eval = (I.shift_right ik stat1 stat2) in
+    let eq = (of_int (2)) in
+    assert_bool ("4 >> 1 should be: \"2\" but was: \"" ^ I.show eval ^ "\"" ^ I.show stat1) (I.equal_to eq eval = `Eq);
+
+    let stat1 = I.of_int ik (of_int (-4)) in
+    let stat2 = I.of_int ik (of_int 1) in
+    let eval = (I.shift_right ik stat1 stat2) in
+    let eq = (of_int (-2)) in
+    assert_bool ("4 >> 1 should be: \"2\" but was: \"" ^ I.show eval ^ "\"" ^ I.show stat1) (I.equal_to eq eval = `Eq)
+
 
   (* Arith *)