From 696c1103a27fb24e8516488467b6d080a73134af Mon Sep 17 00:00:00 2001
From: iC4rl0s <93283755+iC4rl0s@users.noreply.github.com>
Date: Mon, 4 Nov 2024 15:37:50 +0100
Subject: [PATCH 01/15] Draft of incredibly messy impls of bitfield shift
 operations that need some revision. Possible side-effects and runtime in
 O(n^2) while O(n) should be possible.

---
 src/cdomain/value/cdomains/intDomain.ml | 112 ++++++++++++++++++------
 1 file changed, 84 insertions(+), 28 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 45c718849f..2debf55b8f 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1197,7 +1197,13 @@ module BitFieldArith (Ints_t : IntOps.IntOps) = struct
   let zero_mask = Ints_t.zero
   let one_mask = Ints_t.lognot zero_mask
 
+  let is_const (z,o) = (Ints_t.logxor z o) = one_mask
+
   let of_int v = (Ints_t.lognot v, v)
+  let to_int (z, o) = if is_const (z,o) then Some o else None
+
+  let zero = of_int (Ints_t.of_int 0)
+  let one = of_int (Ints_t.of_int 1)
 
   let lognot (z,o) = (o,z)
 
@@ -1208,11 +1214,56 @@ module BitFieldArith (Ints_t : IntOps.IntOps) = struct
   let logxor (z1,o1)  (z2,o2) = (Ints_t.logor (Ints_t.logand z1 z2) (Ints_t.logand o1 o2), 
                                  Ints_t.logor (Ints_t.logand z1 o2) (Ints_t.logand o1 z2))
 
-  let shift_left (z1,o1) (z2,o2) = failwith "Not implemented"
+  let join (z1,o1) (z2,o2) = (Ints_t.logor z1 z2, Ints_t.logor o1 o2)
 
-  let shift_right (z1,o1) (z2,o2) = failwith "Not implemented"
+  let get_bit mask pos = ((Ints_t.to_int mask) lsr pos) land 1 = 1
+  let set_bit ?(zero=true) mask pos =
+    let one_mask = Ints_t.shift_left Ints_t.one pos in
+    if zero then
+      let zero_mask = Ints_t.lognot one_mask in
+      Ints_t.logand mask zero_mask
+    else
+      Ints_t.logor mask one_mask
 
-  let join (z1,o1) (z2,o2) = (Ints_t.logor z1 z2, Ints_t.logor o1 o2)
+  let break_down ikind_size (z, o) : Ints_t.t list option =
+    (* check if the abstract bitfield has undefined bits i.e. at some pos i the bit is neither 1 or 0 *)
+    if Ints_t.compare (Ints_t.lognot @@ Ints_t.logor (Ints_t.lognot z) o) Ints_t.zero = 0
+      then None
+      else
+        let result = ref [o] in
+        for i = ikind_size - 1 downto 0 do
+          if get_bit z i = get_bit o i then
+            let with_one = !result in
+            let with_zero = List.map (fun elm -> set_bit elm i) with_one in
+            result := with_one @ with_zero
+        done;
+        Some (!result)
+
+  let shift_left ikind_size (z1,o1) (z2,o2) =
+    let shift_by n (z, o) =
+      let z_or_mask = Ints_t.sub (Ints_t.shift_left Ints_t.one n) Ints_t.one in
+      (Ints_t.logor (Ints_t.shift_left z n) z_or_mask, Ints_t.shift_left o n)
+    in
+    if is_const (z2, o2) then shift_by (Ints_t.to_int o2) (z1, o1) |> Option.some
+    else
+      (* naive impl in O(n^2) *)
+      match break_down ikind_size (z2, o2) with None -> None
+      | Some c_lst ->
+        List.map (fun c -> shift_by (Ints_t.to_int c) (z1, o1)) c_lst
+      |> List.fold_left join zero
+      |> Option.some
+
+  let shift_right ikind_size (z1,o1) (z2,o2) =
+    let shift_by n (z, o) = (Ints_t.shift_right z n, Ints_t.shift_right o n) 
+    in
+    if is_const (z2, o2) then shift_by (Ints_t.to_int o2) (z1, o1) |> Option.some
+    else
+      (* naive impl in O(n^2) *)
+      match break_down ikind_size (z2, o2) with None -> None
+      | Some c_lst ->
+        List.map (fun c -> shift_by (Ints_t.to_int c) (z1, o1)) c_lst
+      |> List.fold_left join zero
+      |> Option.some
 
   let meet (z1,o1) (z2,o2) = (Ints_t.logand z1 z2, Ints_t.logand o1 o2)
 
@@ -1220,18 +1271,13 @@ module BitFieldArith (Ints_t : IntOps.IntOps) = struct
 
   let widen (z1,o1) (z2,o2) = (nabla z1 z2, nabla o1 o2)
 
-  let zero = of_int (Ints_t.of_int 0)
-  let one = of_int (Ints_t.of_int 1)
-  
-  let topbool = join zero one
+  let top_bool = join zero one
 
   let eq (z1,o1) (z2,o2) = (Ints_t.equal z1 z2 && Ints_t.equal o1 o2)
 
   let includes (z1,o1) (z2,o2) = (Ints_t.logor (Ints_t.lognot z1 ) z2 = one_mask) && 
                                  (Ints_t.logor (Ints_t.lognot o1 ) o2 = one_mask)
 
-  let is_constant (z,o) = (Ints_t.logxor z o) = one_mask
-
 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
@@ -1250,7 +1296,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)
@@ -1268,7 +1314,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     ((z,o), {underflow=false; overflow=false})
 
   let to_int (z,o) = if is_bot (z,o) then None else
-      if BArith.is_constant (z,o) then Some o
+      if BArith.is_const (z,o) then Some o
       else None
 
   let equal_to i (u,l) = 
@@ -1338,11 +1384,21 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
 
   let shift_right ik a b = 
     M.trace "bitfield" "shift_right";
-    failwith "Not implemented"
+    failwith "TODO"
+    (*
+    match BArith.shift_right ik a b with
+    | None -> (bot (), {underflow=false; overflow=false}) (*TODO*)
+    | Some x -> (x, {underflow=false; overflow=false}) (*TODO*)
+    *)
 
   let shift_left ik a b =
     M.trace "bitfield" "shift_left";
-    failwith "Not implemented"
+    failwith "TODO"
+    (*
+    match BArith.shift_left ik a b with
+    | None -> (bot (), {underflow=false; overflow=false}) (*TODO*)
+    | Some x -> (x, {underflow=false; overflow=false}) (*TODO*)
+    *)
 
   let add ?no_ov ik x y=(top_of ik,{underflow=false; overflow=false})
   let mul ?no_ov ik x y=(top_of ik,{underflow=false; overflow=false})
@@ -1359,14 +1415,14 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
 
   let eq ik x y =
     M.trace "bitfield" "eq";
-    if BArith.is_constant x && BArith.is_constant y then of_bool ik (BArith.eq x y) 
+    if BArith.is_const x && BArith.is_const y then of_bool ik (BArith.eq x y) 
                 else if not (BArith.includes x y || (BArith.includes y x)) then of_bool ik false
-                else BArith.topbool
+                else BArith.top_bool
 
     let ne ik x y =
-      if BArith.is_constant x && BArith.is_constant y then of_bool ik (not (BArith.eq x y)) 
+      if BArith.is_const x && BArith.is_const y then of_bool ik (not (BArith.eq x y)) 
       else if not (BArith.includes x y || (BArith.includes y x)) then of_bool ik true
-      else BArith.topbool
+      else BArith.top_bool
 
 
   let leq (x:t) (y:t) = BArith.includes x y
@@ -1385,14 +1441,14 @@ let compare_bitfields ?(strict=true) ?(signed=false) (z1,o1) (z2,o2) =
   let result = ref Unknown in
 
   (* Helper function to check bits at each position *)
-  let get_bit mask pos = ((Ints_t.to_int mask) lsr pos) land 1 = 1 in
+  (* let get_bit mask pos = ((Ints_t.to_int mask) lsr pos) land 1 = 1 in *)
 
   (* Iterate from Most Significant Bit (MSB) to Least Significant Bit (LSB) *)
   for i = bit_length - 1 downto 0 do
-    let bit1_zero = get_bit z1 i in
-    let bit1_one = get_bit o1 i in
-    let bit2_zero = get_bit z2 i in
-    let bit2_one = get_bit o2 i in
+    let bit1_zero = BArith.get_bit z1 i in
+    let bit1_one = BArith.get_bit o1 i in
+    let bit2_zero = BArith.get_bit z2 i in
+    let bit2_one = BArith.get_bit o2 i in
 
     (* Check if bits at position i are both known *)
     if (bit1_zero || bit1_one) && (bit2_zero || bit2_one) then
@@ -1414,8 +1470,8 @@ let compare_bitfields ?(strict=true) ?(signed=false) (z1,o1) (z2,o2) =
   (* Handle sign bit adjustment if signed *)
   if signed && !result <> Unknown then
     match !result with
-    | Less when get_bit o1 sign_bit_position <> get_bit o2 sign_bit_position -> result := Greater
-    | Greater when get_bit o1 sign_bit_position <> get_bit o2 sign_bit_position -> result := Less
+    | Less when BArith.get_bit o1 sign_bit_position <> BArith.get_bit o2 sign_bit_position -> result := Greater
+    | Greater when BArith.get_bit o1 sign_bit_position <> BArith.get_bit o2 sign_bit_position -> result := Less
     | _ -> ();
   else ();
 
@@ -1426,13 +1482,13 @@ let compare_bitfields ?(strict=true) ?(signed=false) (z1,o1) (z2,o2) =
   end;
   !result
 
-  let ge ik x y = if compare_bitfields x y = GreaterOrEqual then of_bool ik true else BArith.topbool
+  let ge ik x y = if compare_bitfields x y = GreaterOrEqual then of_bool ik true else BArith.top_bool
 
-  let le ik x y = if compare_bitfields x y = LessOrEqual then of_bool ik true else BArith.topbool
+  let le ik x y = if compare_bitfields x y = LessOrEqual then of_bool ik true else BArith.top_bool
 
-  let gt ik x y = if compare_bitfields x y = Greater then of_bool ik true else BArith.topbool
+  let gt ik x y = if compare_bitfields x y = Greater then of_bool ik true else BArith.top_bool
 
-  let lt ik x y = if compare_bitfields x y = Less then of_bool ik true else BArith.topbool
+  let lt ik x y = if compare_bitfields x y = Less then of_bool ik true else BArith.top_bool
 
   let invariant_ikind e ik = 
     M.trace "bitfield" "invariant_ikind";

From 5c0fdbbbfeed0e4c4d3cf0f76900eb41dc169279 Mon Sep 17 00:00:00 2001
From: ge58kuc <ge58kuc@mytum.de>
Date: Tue, 5 Nov 2024 22:17:08 +0100
Subject: [PATCH 02/15] optimized shifts that concretize the shifting constants
 from an abstract bitfield by eliminating constants that would result in a
 shift to zero beforehand

---
 src/cdomain/value/cdomains/intDomain.ml | 77 +++++++++++++------------
 1 file changed, 40 insertions(+), 37 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 2debf55b8f..7347156dbd 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1217,7 +1217,7 @@ module BitFieldArith (Ints_t : IntOps.IntOps) = struct
   let join (z1,o1) (z2,o2) = (Ints_t.logor z1 z2, Ints_t.logor o1 o2)
 
   let get_bit mask pos = ((Ints_t.to_int mask) lsr pos) land 1 = 1
-  let set_bit ?(zero=true) mask pos =
+  let set_bit ?(zero=false) mask pos =
     let one_mask = Ints_t.shift_left Ints_t.one pos in
     if zero then
       let zero_mask = Ints_t.lognot one_mask in
@@ -1225,43 +1225,50 @@ module BitFieldArith (Ints_t : IntOps.IntOps) = struct
     else
       Ints_t.logor mask one_mask
 
-  let break_down ikind_size (z, o) : Ints_t.t list option =
+  (* max number of (left or right) shifts on an ikind s.t. 0 results from it *)
+  (* TODO hard coded. Other impl? *)
+  let max_shift (ik: Cil.ikind) =
+    let ilog2 n =
+      let rec aux n acc =
+        if n = 1 then acc
+        else aux (n lsr 1) (acc + 1)
+  in
+    Cil.bytesSizeOfInt ik * 8 |> ilog2
+
+  (* concretizes an abstract bitfield into a set of minimal bitfields that represent concrete numbers
+      used for shifting bitfields for an ikind in WC O( 2^(log(n)) ) with n = ikind size *)
+  let break_down ik (z, o) : Ints_t.t list option =
     (* check if the abstract bitfield has undefined bits i.e. at some pos i the bit is neither 1 or 0 *)
-    if Ints_t.compare (Ints_t.lognot @@ Ints_t.logor (Ints_t.lognot z) o) Ints_t.zero = 0
+    if Ints_t.compare (Ints_t.lognot @@ Ints_t.logor z o) Ints_t.zero = 0
       then None
       else
-        let result = ref [o] in
-        for i = ikind_size - 1 downto 0 do
+        let n = max_shift ik in
+        let zero_extend_mask = Ints_t.shift_left Ints_t.one n
+        |> fun x -> Ints_t.sub x Ints_t.one
+        |> Ints_t.lognot in
+        let result = ref [Ints_t.logand o zero_extend_mask] in
+        for i = 0 to n - 1 do
           if get_bit z i = get_bit o i then
             let with_one = !result in
-            let with_zero = List.map (fun elm -> set_bit elm i) with_one in
+            let with_zero = List.map (fun elm -> set_bit ~zero:true elm i) with_one in
             result := with_one @ with_zero
         done;
         Some (!result)
 
-  let shift_left ikind_size (z1,o1) (z2,o2) =
+  let shift ?left ik a n =
     let shift_by n (z, o) =
-      let z_or_mask = Ints_t.sub (Ints_t.shift_left Ints_t.one n) Ints_t.one in
-      (Ints_t.logor (Ints_t.shift_left z n) z_or_mask, Ints_t.shift_left o n)
-    in
-    if is_const (z2, o2) then shift_by (Ints_t.to_int o2) (z1, o1) |> Option.some
-    else
-      (* naive impl in O(n^2) *)
-      match break_down ikind_size (z2, o2) with None -> None
-      | Some c_lst ->
-        List.map (fun c -> shift_by (Ints_t.to_int c) (z1, o1)) c_lst
-      |> List.fold_left join zero
-      |> Option.some
-
-  let shift_right ikind_size (z1,o1) (z2,o2) =
-    let shift_by n (z, o) = (Ints_t.shift_right z n, Ints_t.shift_right o n) 
+      if left then
+        let z_or_mask = Ints_t.sub (Ints_t.shift_left Ints_t.one n) Ints_t.one
+        in (Ints_t.logor (Ints_t.shift_left z n) z_or_mask, Ints_t.shift_left o n)
+      else
+        (Ints_t.shift_right z n, Ints_t.shift_right o n) in
+        if is_const (z2, o2) then shift_by (Ints_t.to_int o2) (z1, o1) |> Option.some
     in
-    if is_const (z2, o2) then shift_by (Ints_t.to_int o2) (z1, o1) |> Option.some
+    if is_const n then shift_by (Ints_t.to_int @@ snd n) a |> Option.some
     else
-      (* naive impl in O(n^2) *)
-      match break_down ikind_size (z2, o2) with None -> None
+      match break_down ik n with None -> None
       | Some c_lst ->
-        List.map (fun c -> shift_by (Ints_t.to_int c) (z1, o1)) c_lst
+        List.map (fun c -> shift_by (Ints_t.to_int @@ snd n) a) c_lst
       |> List.fold_left join zero
       |> Option.some
 
@@ -1382,23 +1389,19 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     M.trace "bitfield" "neg";
     failwith "Not implemented"
 
+  (*TODO no overflow handling for shifts?*)
+  (*TODO move shift impl here due to dependancy to ikind?*)
   let shift_right ik a b = 
     M.trace "bitfield" "shift_right";
-    failwith "TODO"
-    (*
-    match BArith.shift_right ik a b with
-    | None -> (bot (), {underflow=false; overflow=false}) (*TODO*)
-    | Some x -> (x, {underflow=false; overflow=false}) (*TODO*)
-    *)
+    match BArith.shift ~left:false ik a b with
+    | None -> (bot (), {underflow=false; overflow=false})
+    | Some x -> (x, {underflow=false; overflow=false})
 
   let shift_left ik a b =
     M.trace "bitfield" "shift_left";
-    failwith "TODO"
-    (*
-    match BArith.shift_left ik a b with
-    | None -> (bot (), {underflow=false; overflow=false}) (*TODO*)
-    | Some x -> (x, {underflow=false; overflow=false}) (*TODO*)
-    *)
+    match BArith.shift ~left:true ik a b with
+    | None -> (bot (), {underflow=false; overflow=false})
+    | Some x -> (x, {underflow=false; overflow=false})
 
   let add ?no_ov ik x y=(top_of ik,{underflow=false; overflow=false})
   let mul ?no_ov ik x y=(top_of ik,{underflow=false; overflow=false})

From 087d4a925213b3b0cec940be125aeeebfe976884 Mon Sep 17 00:00:00 2001
From: ge58kuc <ge58kuc@mytum.de>
Date: Tue, 5 Nov 2024 22:28:36 +0100
Subject: [PATCH 03/15] minor bug in max_shift

---
 src/cdomain/value/cdomains/intDomain.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 7347156dbd..b9981c461d 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1232,6 +1232,7 @@ module BitFieldArith (Ints_t : IntOps.IntOps) = struct
       let rec aux n acc =
         if n = 1 then acc
         else aux (n lsr 1) (acc + 1)
+      in aux n 0
   in
     Cil.bytesSizeOfInt ik * 8 |> ilog2
 

From 0116023ec192d55efff67402e9a1233e0d5391a3 Mon Sep 17 00:00:00 2001
From: ge58kuc <ge58kuc@mytum.de>
Date: Tue, 5 Nov 2024 22:32:03 +0100
Subject: [PATCH 04/15] comparison bug in max_shift

---
 src/cdomain/value/cdomains/intDomain.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index b9981c461d..f0711dda83 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1230,7 +1230,7 @@ module BitFieldArith (Ints_t : IntOps.IntOps) = struct
   let max_shift (ik: Cil.ikind) =
     let ilog2 n =
       let rec aux n acc =
-        if n = 1 then acc
+        if n <= 1 then acc
         else aux (n lsr 1) (acc + 1)
       in aux n 0
   in

From d42b9895552a0e6072b445bdde1ada52dbef4371 Mon Sep 17 00:00:00 2001
From: ge58kuc <ge58kuc@mytum.de>
Date: Thu, 7 Nov 2024 15:41:21 +0100
Subject: [PATCH 05/15] separation of break_down into
 break_down_to_const_bitfields and break_down_to_consts

---
 src/cdomain/value/cdomains/intDomain.ml | 50 +++++++++++++------------
 1 file changed, 27 insertions(+), 23 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index f0711dda83..f540a5f72c 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1191,13 +1191,14 @@ end
 
 
 
-(* BitField arithmetic, without any overflow handling etc. *)
-module BitFieldArith (Ints_t : IntOps.IntOps) = struct
+(* Bitfield arithmetic, without any overflow handling etc. *)
+module BitfieldArith (Ints_t : IntOps.IntOps) = struct
 
   let zero_mask = Ints_t.zero
   let one_mask = Ints_t.lognot zero_mask
 
   let is_const (z,o) = (Ints_t.logxor z o) = one_mask
+  let is_undefined (z,o) = Ints_t.compare (Ints_t.lognot @@ Ints_t.logor z o) Ints_t.zero = 0
 
   let of_int v = (Ints_t.lognot v, v)
   let to_int (z, o) = if is_const (z,o) then Some o else None
@@ -1225,8 +1226,6 @@ module BitFieldArith (Ints_t : IntOps.IntOps) = struct
     else
       Ints_t.logor mask one_mask
 
-  (* max number of (left or right) shifts on an ikind s.t. 0 results from it *)
-  (* TODO hard coded. Other impl? *)
   let max_shift (ik: Cil.ikind) =
     let ilog2 n =
       let rec aux n acc =
@@ -1234,27 +1233,33 @@ module BitFieldArith (Ints_t : IntOps.IntOps) = struct
         else aux (n lsr 1) (acc + 1)
       in aux n 0
   in
-    Cil.bytesSizeOfInt ik * 8 |> ilog2
+    Size.bit ik |> ilog2
 
-  (* concretizes an abstract bitfield into a set of minimal bitfields that represent concrete numbers
-      used for shifting bitfields for an ikind in WC O( 2^(log(n)) ) with n = ikind size *)
-  let break_down ik (z, o) : Ints_t.t list option =
-    (* check if the abstract bitfield has undefined bits i.e. at some pos i the bit is neither 1 or 0 *)
-    if Ints_t.compare (Ints_t.lognot @@ Ints_t.logor z o) Ints_t.zero = 0
-      then None
+  let break_down_to_const_bitfields ik_size one_mask (z,o) : (Ints_t.t * Ints_t.t) list option =
+    if is_undefined (z,o)
+      then None (* cannot break down due to undefined bits *)
       else
-        let n = max_shift ik in
-        let zero_extend_mask = Ints_t.shift_left Ints_t.one n
-        |> fun x -> Ints_t.sub x Ints_t.one
-        |> Ints_t.lognot in
-        let result = ref [Ints_t.logand o zero_extend_mask] in
-        for i = 0 to n - 1 do
+        let z_masked = Int_t.logand z (Ints_t.lognot one_mask) in
+        let o_masked = Ints_t.logand o one_mask in
+        let result = ref [(z_masked, o_masked)] in
+        for i = 0 to ik_size - 1 do
           if get_bit z i = get_bit o i then
             let with_one = !result in
-            let with_zero = List.map (fun elm -> set_bit ~zero:true elm i) with_one in
+            let with_zero = List.map (fun (z,o) -> (set_bit ~zero:false z i, set_bit ~zero:true o i)) with_one in
             result := with_one @ with_zero
         done;
-        Some (!result)
+    Some (!result)
+
+  (* concretizes an abstract bitfield into a set of minimal bitfields that represent concrete numbers
+      used for shifting bitfields for an ikind in WC O( 2^(log(n)) ) with n = ikind size *)
+  let break_down_to_consts ik (z, o) : Ints_t.t list option =
+    let n = max_shift ik in
+    let zero_extend_mask = Ints_t.shift_left Ints_t.one n
+    |> fun x -> Ints_t.sub x Ints_t.one
+    |> Ints_t.lognot in
+    match break_down_to_const_bitfields n zero_extend_mask with
+    | None -> None
+    | Some c_bf_lst = List.map snd c_bf_lst
 
   let shift ?left ik a n =
     let shift_by n (z, o) =
@@ -1262,12 +1267,11 @@ module BitFieldArith (Ints_t : IntOps.IntOps) = struct
         let z_or_mask = Ints_t.sub (Ints_t.shift_left Ints_t.one n) Ints_t.one
         in (Ints_t.logor (Ints_t.shift_left z n) z_or_mask, Ints_t.shift_left o n)
       else
-        (Ints_t.shift_right z n, Ints_t.shift_right o n) in
-        if is_const (z2, o2) then shift_by (Ints_t.to_int o2) (z1, o1) |> Option.some
+        (Ints_t.shift_right z n, Ints_t.shift_right o n)
     in
     if is_const n then shift_by (Ints_t.to_int @@ snd n) a |> Option.some
     else
-      match break_down ik n with None -> None
+      match break_down_to_consts ik n with None -> None
       | Some c_lst ->
         List.map (fun c -> shift_by (Ints_t.to_int @@ snd n) a) c_lst
       |> List.fold_left join zero
@@ -1292,7 +1296,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
   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 () = (Ints_t.lognot (Ints_t.zero),  Ints_t.lognot (Ints_t.zero))

From 27c9876fd117a44e135f19c07ab7199d9f84c79b Mon Sep 17 00:00:00 2001
From: ge58kuc <ge58kuc@mytum.de>
Date: Fri, 8 Nov 2024 01:47:51 +0100
Subject: [PATCH 06/15] make it more functional. untested

---
 src/cdomain/value/cdomains/intDomain.ml | 55 +++++++++++--------------
 1 file changed, 24 insertions(+), 31 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index f540a5f72c..b581188c5b 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1217,49 +1217,45 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
 
   let join (z1,o1) (z2,o2) = (Ints_t.logor z1 z2, Ints_t.logor o1 o2)
 
-  let get_bit mask pos = ((Ints_t.to_int mask) lsr pos) land 1 = 1
-  let set_bit ?(zero=false) mask pos =
+  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 =
     let one_mask = Ints_t.shift_left Ints_t.one pos in
     if zero then
       let zero_mask = Ints_t.lognot one_mask in
-      Ints_t.logand mask zero_mask
+      Ints_t.logand bf zero_mask
     else
-      Ints_t.logor mask one_mask
+      Ints_t.logor bf one_mask
 
-  let max_shift (ik: Cil.ikind) =
+  let max_shift 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
+    in
     Size.bit ik |> ilog2
 
-  let break_down_to_const_bitfields ik_size one_mask (z,o) : (Ints_t.t * Ints_t.t) list option =
+  let break_down_to_const_bitfields ik_size one_mask (z,o) =
     if is_undefined (z,o)
-      then None (* cannot break down due to undefined bits *)
+      then None
       else
         let z_masked = Int_t.logand z (Ints_t.lognot one_mask) in
         let o_masked = Ints_t.logand o one_mask in
-        let result = ref [(z_masked, o_masked)] in
-        for i = 0 to ik_size - 1 do
-          if get_bit z i = get_bit o i then
-            let with_one = !result in
-            let with_zero = List.map (fun (z,o) -> (set_bit ~zero:false z i, set_bit ~zero:true o i)) with_one in
-            result := with_one @ with_zero
-        done;
-    Some (!result)
-
-  (* concretizes an abstract bitfield into a set of minimal bitfields that represent concrete numbers
-      used for shifting bitfields for an ikind in WC O( 2^(log(n)) ) with n = ikind size *)
-  let break_down_to_consts ik (z, o) : Ints_t.t list option =
+        let rec break_down c_lst i =
+          if i < ik_size then
+            if get_bit z i = get_bit o i then
+              with_zero = List.map (fun (z,o) -> (set_bit z i, set_bit ~zero:true o i)) c_lst in
+              break_down (c_lst @ with_zero) (i+1)
+            else
+              break_down c_lst (i+1)
+          else c_lst
+        in break_down [(z_masked, o_masked)] 0 |> Option.some
+
+  let break_down_to_consts ik (z, o) =
     let n = max_shift ik in
-    let zero_extend_mask = Ints_t.shift_left Ints_t.one n
-    |> fun x -> Ints_t.sub x Ints_t.one
-    |> Ints_t.lognot in
-    match break_down_to_const_bitfields n zero_extend_mask with
-    | None -> None
-    | Some c_bf_lst = List.map snd c_bf_lst
+    let zero_extend_mask = Ints_t.lognot @@ Ints_t.sub (Ints_t.shift_left Ints_t.one n) Ints_t.one
+    in
+    Option.map (List.map snd) (break_down_to_const_bitfields n zero_extend_mask)
 
   let shift ?left ik a n =
     let shift_by n (z, o) =
@@ -1271,11 +1267,8 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
     in
     if is_const n then shift_by (Ints_t.to_int @@ snd n) a |> Option.some
     else
-      match break_down_to_consts ik n with None -> None
-      | Some c_lst ->
-        List.map (fun c -> shift_by (Ints_t.to_int @@ snd n) a) c_lst
-      |> List.fold_left join zero
-      |> Option.some
+      break_down_to_consts ik n
+      |> Option.map (fun c_lst -> List.map (fun c -> shift_by c a) c_lst |> List.fold_left join zero)
 
   let meet (z1,o1) (z2,o2) = (Ints_t.logand z1 z2, Ints_t.logand o1 o2)
 

From ca7c04059b9bc977b49ac86a820599bd4b652dcb Mon Sep 17 00:00:00 2001
From: ge58kuc <ge58kuc@mytum.de>
Date: Fri, 8 Nov 2024 04:23:10 +0100
Subject: [PATCH 07/15] bug fix: Bitfields with z set to zero missed

---
 src/cdomain/value/cdomains/intDomain.ml | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index b581188c5b..37a19d1791 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1235,21 +1235,23 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
     in
     Size.bit ik |> ilog2
 
-  let break_down_to_const_bitfields ik_size one_mask (z,o) =
+  let break_down_to_const_bitfields ik_size suffix_mask (z,o) =
     if is_undefined (z,o)
       then None
       else
-        let z_masked = Int_t.logand z (Ints_t.lognot one_mask) in
-        let o_masked = Ints_t.logand o one_mask in
+        let z_prefix = Int_t.logand z (Ints_t.lognot suffix_mask) in
+        let o_suffix = Ints_t.logand o suffix_mask in
         let rec break_down c_lst i =
           if i < ik_size then
             if get_bit z i = get_bit o i then
-              with_zero = List.map (fun (z,o) -> (set_bit z i, set_bit ~zero:true o i)) c_lst in
-              break_down (c_lst @ with_zero) (i+1)
+              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)
           else c_lst
-        in break_down [(z_masked, o_masked)] 0 |> Option.some
+        in break_down [(z_prefix, o_suffix)] 0 |> Option.some
 
   let break_down_to_consts ik (z, o) =
     let n = max_shift ik in
@@ -1257,7 +1259,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
     in
     Option.map (List.map snd) (break_down_to_const_bitfields n zero_extend_mask)
 
-  let shift ?left ik a n =
+  let shift ?left ik bf n =
     let shift_by n (z, o) =
       if left then
         let z_or_mask = Ints_t.sub (Ints_t.shift_left Ints_t.one n) Ints_t.one
@@ -1265,10 +1267,10 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
       else
         (Ints_t.shift_right z n, Ints_t.shift_right o n)
     in
-    if is_const n then shift_by (Ints_t.to_int @@ snd n) a |> Option.some
+    if is_const n then shift_by (Ints_t.to_int @@ snd n) bf |> Option.some
     else
       break_down_to_consts ik n
-      |> Option.map (fun c_lst -> List.map (fun c -> shift_by c a) c_lst |> List.fold_left join zero)
+      |> Option.map (fun c_lst -> List.map (fun c -> shift_by c bf) c_lst |> List.fold_left join zero)
 
   let meet (z1,o1) (z2,o2) = (Ints_t.logand z1 z2, Ints_t.logand o1 o2)
 
@@ -1387,14 +1389,14 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     M.trace "bitfield" "neg";
     failwith "Not implemented"
 
-  (*TODO no overflow handling for shifts?*)
-  (*TODO move shift impl here due to dependancy to ikind?*)
+  (*TODO norming*)
   let shift_right ik a b = 
     M.trace "bitfield" "shift_right";
     match BArith.shift ~left:false ik a b with
     | None -> (bot (), {underflow=false; overflow=false})
     | Some x -> (x, {underflow=false; overflow=false})
 
+  (*TODO norming*)
   let shift_left ik a b =
     M.trace "bitfield" "shift_left";
     match BArith.shift ~left:true ik a b with

From 897d6a2970debdc16761f11b40ad66e80353a07c Mon Sep 17 00:00:00 2001
From: Giancarlo Calvache <giancarlo.calvache-valladares@tum.de>
Date: Tue, 12 Nov 2024 17:28:14 +0100
Subject: [PATCH 08/15] bitfield shifts pr ready

---
 src/cdomain/value/cdomains/intDomain.ml | 22 ++++++++--------------
 1 file changed, 8 insertions(+), 14 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 37a19d1791..57a9cbd755 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1235,14 +1235,16 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
     in
     Size.bit ik |> ilog2
 
-  let break_down_to_const_bitfields ik_size suffix_mask (z,o) =
+  let break_down_log ik (z,o) =
     if is_undefined (z,o)
       then None
       else
+        let n = max_shift ik in
+        let suffix_mask = Ints_t.lognot @@ Ints_t.sub (Ints_t.shift_left Ints_t.one n) Ints_t.one in
         let z_prefix = Int_t.logand z (Ints_t.lognot suffix_mask) in
         let o_suffix = Ints_t.logand o suffix_mask in
         let rec break_down c_lst i =
-          if i < ik_size then
+          if i < n then
             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
@@ -1253,11 +1255,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
           else c_lst
         in break_down [(z_prefix, o_suffix)] 0 |> Option.some
 
-  let break_down_to_consts ik (z, o) =
-    let n = max_shift ik in
-    let zero_extend_mask = Ints_t.lognot @@ Ints_t.sub (Ints_t.shift_left Ints_t.one n) Ints_t.one
-    in
-    Option.map (List.map snd) (break_down_to_const_bitfields n zero_extend_mask)
+  let break_down ik bf = Option.map (List.map snd) (break_down_log ik bf)
 
   let shift ?left ik bf n =
     let shift_by n (z, o) =
@@ -1269,7 +1267,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
     in
     if is_const n then shift_by (Ints_t.to_int @@ snd n) bf |> Option.some
     else
-      break_down_to_consts ik n
+      break_down ik n
       |> Option.map (fun c_lst -> List.map (fun c -> shift_by c bf) c_lst |> List.fold_left join zero)
 
   let meet (z1,o1) (z2,o2) = (Ints_t.logand z1 z2, Ints_t.logand o1 o2)
@@ -1392,16 +1390,12 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
   (*TODO norming*)
   let shift_right ik a b = 
     M.trace "bitfield" "shift_right";
-    match BArith.shift ~left:false ik a b with
-    | None -> (bot (), {underflow=false; overflow=false})
-    | Some x -> (x, {underflow=false; overflow=false})
+    norm ik @@ BArith.shift ~left:false ik a b |> Option.value ~default: (bot ())
 
   (*TODO norming*)
   let shift_left ik a b =
     M.trace "bitfield" "shift_left";
-    match BArith.shift ~left:true ik a b with
-    | None -> (bot (), {underflow=false; overflow=false})
-    | Some x -> (x, {underflow=false; overflow=false})
+    norm ik @@ BArith.shift ~left:true ik a b |> Option.value ~default: (bot ())
 
   let add ?no_ov ik x y=(top_of ik,{underflow=false; overflow=false})
   let mul ?no_ov ik x y=(top_of ik,{underflow=false; overflow=false})

From cbfbf28c38ee8cd619dca12861cd5572346e3226 Mon Sep 17 00:00:00 2001
From: Giancarlo Calvache <giancarlo.calvache-valladares@tum.de>
Date: Tue, 12 Nov 2024 20:48:51 +0100
Subject: [PATCH 09/15] bug fix: signedness with right shift considered

---
 src/cdomain/value/cdomains/intDomain.ml | 67 +++++++++++++------------
 1 file changed, 34 insertions(+), 33 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 57a9cbd755..74afd885d5 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1198,7 +1198,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
   let one_mask = Ints_t.lognot zero_mask
 
   let is_const (z,o) = (Ints_t.logxor z o) = one_mask
-  let is_undefined (z,o) = Ints_t.compare (Ints_t.lognot @@ Ints_t.logor z o) Ints_t.zero = 0
+  let is_undef (z,o) = Ints_t.compare (Ints_t.lognot @@ Ints_t.logor z o) Ints_t.zero = 0
 
   let of_int v = (Ints_t.lognot v, v)
   let to_int (z, o) = if is_const (z,o) then Some o else None
@@ -1232,43 +1232,46 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
         if n <= 1 then acc
         else aux (n lsr 1) (acc + 1)
       in aux n 0
-    in
-    Size.bit ik |> ilog2
+    in ilog2 (Size.bit ik)
 
-  let break_down_log ik (z,o) =
-    if is_undefined (z,o)
-      then None
+  let break_down_log ik (z,o) = if is_undef (z,o) then None
+    else
+      let n = max_shift ik in
+      let rec break_down c_lst i = if i >= n then c_lst
       else
-        let n = max_shift ik in
-        let suffix_mask = Ints_t.lognot @@ Ints_t.sub (Ints_t.shift_left Ints_t.one n) Ints_t.one in
-        let z_prefix = Int_t.logand z (Ints_t.lognot suffix_mask) in
-        let o_suffix = Ints_t.logand o suffix_mask in
-        let rec break_down c_lst i =
-          if i < n then
-            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)
-          else c_lst
-        in break_down [(z_prefix, o_suffix)] 0 |> Option.some
+        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 sfx_mask = Ints_t.lognot @@ Ints_t.sub (Ints_t.shift_left Ints_t.one n) Ints_t.one in
+      break_down [(Ints_t.logand z (Ints_t.lognot sfx_msk), Ints_t.logand o sfx_msk)] 0 |> Option.some
 
   let break_down ik bf = Option.map (List.map snd) (break_down_log ik bf)
 
-  let shift ?left ik bf n =
-    let shift_by n (z, o) =
-      if left then
-        let z_or_mask = Ints_t.sub (Ints_t.shift_left Ints_t.one n) Ints_t.one
-        in (Ints_t.logor (Ints_t.shift_left z n) z_or_mask, Ints_t.shift_left o n)
+  let shift_right ik bf n_bf =
+    let shift_right bf (z,o) =
+      let sign_msk = Ints_t.shift_left one_mask (Size.bit ik - n) in
+      if isSigned ik then
+        (Ints_t.shift_right z n, Ints_t.logor (Ints_t.shift_right o n) sign_msk)
       else
-        (Ints_t.shift_right z n, Ints_t.shift_right o n)
-    in
-    if is_const n then shift_by (Ints_t.to_int @@ snd n) bf |> Option.some
+        (Ints_t.logor (Ints_t.shift_right z n) sign_msk, Ints_t.shift_right o n)
+      in
+    if is_const n_bf then Some (shift_right bf (Ints_t.to_int @@ snd n_bf))
     else
-      break_down ik n
-      |> Option.map (fun c_lst -> List.map (fun c -> shift_by c bf) c_lst |> List.fold_left join zero)
+      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 bf (z,o) =
+        let z_msk = Ints_t.sub (Ints_t.shift_left Ints_t.one n) Ints_t.one
+        in (Ints_t.logor (Ints_t.shift_left z n) z_msk, Ints_t.shift_left o n)
+      in
+    if is_const n 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 meet (z1,o1) (z2,o2) = (Ints_t.logand z1 z2, Ints_t.logand o1 o2)
 
@@ -1401,8 +1404,6 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
   let mul ?no_ov ik x y=(top_of ik,{underflow=false; overflow=false})
   let sub ?no_ov ik x y=(top_of ik,{underflow=false; overflow=false})
 
-  let shift_left ik a b =(top_of ik,{underflow=false; overflow=false})
-
   let rem ik x y = 
     M.trace "bitfield" "rem";
     top_of ik

From a31dc674d6016917e5208dc8fa75617cd15de411 Mon Sep 17 00:00:00 2001
From: ge58kuc <ge58kuc@mytum.de>
Date: Fri, 15 Nov 2024 18:39:28 +0100
Subject: [PATCH 10/15] intDomain.ml is compilable

---
 src/cdomain/value/cdomains/intDomain.ml | 47 ++++++++++++-------------
 1 file changed, 23 insertions(+), 24 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 1f64aec377..badde25b55 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1190,19 +1190,21 @@ struct
 end
 
 (* Bitfield arithmetic, without any overflow handling etc. *)
-module BitFieldArith (Ints_t : IntOps.IntOps) = struct
+module BitfieldArith (Ints_t : IntOps.IntOps) = struct
+
+  let of_int x = (Ints_t.lognot x, x) 
+
   let one = of_int Ints_t.one
   let zero = of_int Ints_t.zero
-  let top_bool = join one zero
 
   let zero_mask = Ints_t.zero
   let one_mask = Ints_t.lognot zero_mask
-
-  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 meet (z1,o1) (z2,o2) = (Ints_t.logand z1 z2, Ints_t.logand o1 o2)
 
+  let top_bool = join one zero
+
   let is_const (z,o) = (Ints_t.logxor z o) = one_mask
   let is_undef (z,o) = Ints_t.compare (Ints_t.lognot @@ Ints_t.logor z o) Ints_t.zero = 0
 
@@ -1240,7 +1242,7 @@ module BitFieldArith (Ints_t : IntOps.IntOps) = struct
       in aux n 0
     in ilog2 (Size.bit ik)
 
-  let break_down_log ik (z,o) = if is_undef (z,o) then None
+  let break_down_log ik (z,o) : (Ints_t.t * Ints_t.t) list option = if is_undef (z,o) then None
     else
       let n = max_shift ik in
       let rec break_down c_lst i = if i >= n then c_lst
@@ -1253,29 +1255,29 @@ module BitFieldArith (Ints_t : IntOps.IntOps) = struct
         else
           break_down c_lst (i+1)
       in
-      let sfx_mask = Ints_t.lognot @@ Ints_t.sub (Ints_t.shift_left Ints_t.one n) Ints_t.one in
-      break_down [(Ints_t.logand z (Ints_t.lognot sfx_msk), Ints_t.logand o sfx_msk)] 0 |> Option.some
+      let sufx_msk = Ints_t.lognot @@ Ints_t.sub (Ints_t.shift_left Ints_t.one n) Ints_t.one in
+      break_down [(Ints_t.logand z (Ints_t.lognot sufx_msk), Ints_t.logand o sufx_msk)] 0 |> Option.some
 
-  let break_down ik bf = Option.map (List.map snd) (break_down_log ik bf)
+  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_log ik bf)
 
   let shift_right ik bf n_bf =
-    let shift_right bf (z,o) =
-      let sign_msk = Ints_t.shift_left one_mask (Size.bit ik - n) in
+    let shift_right (z,o) c =
+      let sign_msk = Ints_t.shift_left one_mask (Size.bit ik - c) in
       if isSigned ik then
-        (Ints_t.shift_right z n, Ints_t.logor (Ints_t.shift_right o n) sign_msk)
+        (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 n) sign_msk, Ints_t.shift_right o n)
+        (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 bf (z,o) =
-        let z_msk = Ints_t.sub (Ints_t.shift_left Ints_t.one n) Ints_t.one
-        in (Ints_t.logor (Ints_t.shift_left z n) z_msk, Ints_t.shift_left o n)
+    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 then Some (shift_left bf (Ints_t.to_int @@ snd n_bf))
+    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)
 
@@ -1434,11 +1436,11 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
 
   let shift_right ik a b = 
     M.trace "bitfield" "shift_right";
-    norm ik @@ BArith.shift ~left:false ik a b |> Option.value ~default: (bot ())
+    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:true ik a b |> Option.value ~default: (bot ())
+    norm ik @@ (BArith.shift_left ik a b |> Option.value ~default: (bot ()))
 
   (* Arith *)
 
@@ -1594,16 +1596,13 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     failwith "Not implemented"
 
   let refine_with_congruence ik (intv : t) (cong : (int_t * int_t ) option) : t =
-    M.trace "bitfield" "refine_with_congruence";
-    t
+    M.trace "bitfield" "refine_with_congruence"; bot ()
   
   let refine_with_interval ik a b = 
-    M.trace "bitfield" "refine_with_interval";
-    t
+    M.trace "bitfield" "refine_with_interval"; bot ()
 
   let refine_with_excl_list ik (intv : t) (excl : (int_t list * (int64 * int64)) option) : t = 
-    M.trace "bitfield" "refine_with_excl_list";
-    t
+    M.trace "bitfield" "refine_with_excl_list"; bot ()
 
   let refine_with_incl_list ik t (incl : (int_t list) option) : t =
     (* loop over all included ints *)

From 28d9db084a31578ef8dca3f403ef7ccde5b0c6e6 Mon Sep 17 00:00:00 2001
From: ge58kuc <ge58kuc@mytum.de>
Date: Sun, 17 Nov 2024 00:38:28 +0100
Subject: [PATCH 11/15] Avoiding unnecessary computation when min{b} >
 ceil(log2 max{a}) in shift a b since in that case shift a b = zero always.

---
 src/cdomain/value/cdomains/intDomain.ml | 89 +++++++++++++------------
 1 file changed, 45 insertions(+), 44 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index badde25b55..5fdb29350e 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1205,8 +1205,13 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
 
   let top_bool = join one zero
 
+  let bits_known (z,o) = Ints_t.logxor z o
+  let bits_unknown bf = Ints_t.lognot @@ known_bits bf
+  let bits_set bf = Ints_t.logand (snd bf) @@ known_bits 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 (Ints_t.lognot @@ Ints_t.logor z o) Ints_t.zero = 0
+  let is_undef (z,o) = Ints_t.compare (bits_undef (z,o)) Ints_t.zero != 0
 
   let eq (z1,o1) (z2,o2) = (Ints_t.equal z1 z2) && (Ints_t.equal o1 o2)
 
@@ -1225,16 +1230,19 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
 
   let join (z1,o1) (z2,o2) = (Ints_t.logor z1 z2, Ints_t.logor o1 o2)
 
+  let make_bitone_msk pos = Ints_t.shift_left 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
+
   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 =
-    let one_mask = Ints_t.shift_left Ints_t.one pos in
     if zero then
-      let zero_mask = Ints_t.lognot one_mask in
-      Ints_t.logand bf zero_mask
+      Ints_t.logand bf @@ make_bitzero_msk pos
     else
-      Ints_t.logor bf one_mask
+      Ints_t.logor bf @@ make_bitone_msk pos
 
-  let max_shift ik =
+  let log2_bitcnt ik =
     let ilog2 n =
       let rec aux n acc =
         if n <= 1 then acc
@@ -1242,23 +1250,27 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
       in aux n 0
     in ilog2 (Size.bit ik)
 
-  let break_down_log ik (z,o) : (Ints_t.t * Ints_t.t) list option = if is_undef (z,o) then None
+  let break_down_lsb ik (z,o) : (Ints_t.t * Ints_t.t) list option = if is_undef (z,o) then None
     else
-      let n = max_shift ik in
-      let rec break_down c_lst i = if i >= n then c_lst
+      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)
+          |> fun c_lst -> break_down c_lst (i-1)
         else
-          break_down c_lst (i+1)
+          break_down c_lst (i-1)
       in
-      let sufx_msk = Ints_t.lognot @@ Ints_t.sub (Ints_t.shift_left Ints_t.one n) Ints_t.one in
-      break_down [(Ints_t.logand z (Ints_t.lognot sufx_msk), Ints_t.logand o sufx_msk)] 0 |> Option.some
+      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_log ik bf)
+  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 =
@@ -1267,55 +1279,46 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
         (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
+    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)
+    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
+        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)
-
+    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
+    let unknownBitMask = bits_unknown (z,o) in
+    let impossibleBitMask = bits_undef in
+    let guaranteedBits = bits_set (z,o) 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 signBitMask = make_bitone_msk (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))
+      Size.cast ik (Ints_t.to_bigint guaranteedBits)
 
   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
+    let unknownBitMask = bits_unknown (z,o) in
+    let impossibleBitMask = bits_undef (z,o) in
+    let guaranteedBits = bits_set (z,o) 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 worstPossibleUnknownBits = Ints_t.logand unknownBitMask (Ints_t.of_bigint fullMask) in (* Necessary? *)
+    Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits))
 
 end
 
@@ -1332,8 +1335,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
 
@@ -1343,8 +1344,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

From 8e8b9cba7e4f4aee5deb9634fe4838d154074b29 Mon Sep 17 00:00:00 2001
From: leon <leonunterberger@gmx.at>
Date: Mon, 18 Nov 2024 23:48:28 +0100
Subject: [PATCH 12/15] add simple shift unit tests

---
 tests/unit/cdomains/intDomainTest.ml | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml
index 25087069a9..0a9a8dfd97 100644
--- a/tests/unit/cdomains/intDomainTest.ml
+++ b/tests/unit/cdomains/intDomainTest.ml
@@ -461,10 +461,18 @@ 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
+    
+    assert_bool "2 << 1 = 4" (I.equal_to (of_int (4)) (I.shift_left ik stat1 stat2) = `Top)
+
 
   let test_shift_right _ =
-    ()
+    let stat1 = I.of_int ik (of_int 4) in
+    let stat2 = I.of_int ik (of_int 1) in
+
+    assert_bool "4 >> 1 = 2" (I.equal_to (of_int (2)) (I.shift_left ik stat1 stat2) = `Top)
+
 
   (* Arith *)
 

From 9ae2b8f65d2266be3f60483927204525bf916785 Mon Sep 17 00:00:00 2001
From: leon <leonunterberger@gmx.at>
Date: Tue, 19 Nov 2024 12:01:19 +0100
Subject: [PATCH 13/15] base test impl

---
 src/cdomain/value/cdomains/intDomain.ml  |   8 +-
 src/cdomain/value/cdomains/intDomain.mli |   4 +
 tests/unit/cdomains/intDomainTest.ml     | 420 +++++++++++++++++++++++
 3 files changed, 428 insertions(+), 4 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 87ee6df60f..2bd88836d8 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1206,8 +1206,8 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
   let top_bool = join one zero
 
   let bits_known (z,o) = Ints_t.logxor z o
-  let bits_unknown bf = Ints_t.lognot @@ known_bits bf
-  let bits_set bf = Ints_t.logand (snd bf) @@ known_bits bf
+  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
@@ -1230,7 +1230,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
 
   let join (z1,o1) (z2,o2) = (Ints_t.logor z1 z2, Ints_t.logor o1 o2)
 
-  let make_bitone_msk pos = Ints_t.shift_left one pos
+  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
@@ -1293,7 +1293,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
     
   let min ik (z,o) = 
     let unknownBitMask = bits_unknown (z,o) in
-    let impossibleBitMask = bits_undef in
+    let impossibleBitMask = bits_undef (z,o) in
     let guaranteedBits = bits_set (z,o) in
 
     if impossibleBitMask <> zero_mask then
diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli
index e7667c9b14..3c7fb21c23 100644
--- a/src/cdomain/value/cdomains/intDomain.mli
+++ b/src/cdomain/value/cdomains/intDomain.mli
@@ -402,12 +402,16 @@ module Lifted : IkindUnawareS with type t = [`Top | `Lifted of int64 | `Bot] and
 
 module IntervalFunctor(Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option
 
+module BitFieldFunctor(Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t)
+
 module IntervalSetFunctor(Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) list
 
 module Interval32 :Y with (* type t = (IntOps.Int64Ops.t * IntOps.Int64Ops.t) option and *) type int_t = IntOps.Int64Ops.t
 
 module Interval : SOverflow with type int_t = Z.t
 
+module BitField : SOverflow with type int_t = Z.t
+
 module IntervalSet : SOverflow with type int_t = Z.t
 
 module Congruence : S with type int_t = Z.t
diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml
index a60b7a6cb1..0a9a8dfd97 100644
--- a/tests/unit/cdomains/intDomainTest.ml
+++ b/tests/unit/cdomains/intDomainTest.ml
@@ -250,7 +250,426 @@ struct
   ]
 end
 
+module BitFieldTest (I : IntDomain.SOverflow with type int_t = Z.t) =
+struct
+module I = IntDomain.SOverflowUnlifter (I)
+
+  let ik = Cil.IInt
+
+  let assert_equal x y =
+    OUnit.assert_equal ~printer:I.show x y
+
+
+  let test_of_int_to_int _ =
+    let b1 = I.of_int ik (of_int 17) in
+    OUnit.assert_equal 17 (I.to_int b1 |> Option.get |> to_int)
+
+  let test_to_int_of_int _ =
+    OUnit.assert_equal None (I.to_int (I.bot_of ik));
+    OUnit.assert_equal (of_int 13) (I.to_int (I.of_int ik (of_int 13)) |> Option.get);
+    OUnit.assert_equal None (I.to_int (I.top_of ik));
+    OUnit.assert_equal None (I.to_int (I.join ik (I.of_int ik (of_int 13)) (I.of_int ik (of_int 14))))
+
+  let test_equal_to _ =
+    let b1 = I.join ik (I.of_int ik (of_int 4)) (I.of_int ik (of_int 2)) in
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 4) b1);
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 2) b1);
+
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 0) b1);
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 6) b1);
+
+    OUnit.assert_equal `Neq (I.equal_to (Z.of_int 1) b1);
+    OUnit.assert_equal `Neq (I.equal_to (Z.of_int 3) b1);
+    OUnit.assert_equal `Neq (I.equal_to (Z.of_int 5) b1);
+
+    let b2 =I.of_int ik (of_int 123) in
+    OUnit.assert_equal `Eq (I.equal_to (Z.of_int 123) b2)
+
+  let test_join _ =
+    let b1 = I.of_int ik (of_int 9) in
+    let b2 = I.of_int ik (of_int 2) in
+    let bjoin = I.join ik b1 b2 in
+    assert_bool "num1 leq join" (I.leq b1 bjoin);
+    assert_bool "num2 leq join" (I.leq b2 bjoin);
+
+
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 9) bjoin);
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 2) bjoin);
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 11) bjoin)
+
+  let test_meet _ =
+    let b1 = I.of_int ik (of_int 5) in
+    let b2 = I.of_int ik (of_int 3) in
+    let bf12 = I.join ik b1 b2 in
+
+    let b3 = I.of_int ik (of_int 7) in
+    let b4 = I.of_int ik (of_int 4) in
+    let bf34 = I.join ik b3 b4 in
+
+    let bmeet2 = I.meet ik bf12 bf34 in
+
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 5) bmeet2);
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 7) bmeet2)
+
+  let test_leq_1 _ =
+    let b1 = I.of_int ik (of_int 13) in
+    let b2 = I.of_int ik (of_int 5) in
+
+    let bjoin = I.join ik b1 b2 in
+
+    OUnit.assert_bool "13 leq 13" (I.leq b1 b1);
+    OUnit.assert_bool "5 leq 5" (I.leq b2 b2);
+
+    OUnit.assert_bool "5 leq 13" (I.leq b2 bjoin);
+    OUnit.assert_bool "not 13 leq 5" (not (I.leq bjoin b2))
+
+  let test_leq_2 _ =
+    let b1 = I.of_int ik (of_int 7) in
+
+    OUnit.assert_bool "bot leq 7" (I.leq (I.bot_of ik) b1);
+    OUnit.assert_bool "7 leq top" (I.leq b1 (I.top_of ik))
+
+  let test_wrap_1 _ =
+    let z = of_int 31376 in
+    let b_uint8 = I.of_int IChar z in
+    let b_sint8 = I.of_int ISChar z in
+    let b_uint16 = I.of_int IUShort z in
+    let b_sint16 = I.of_int IShort z in
+
+    (* See https://www.simonv.fr/TypesConvert/?integers *)
+    assert_equal (I.of_int IChar (of_int 144)) b_uint8;
+    assert_equal (I.of_int ISChar (of_int (-112))) b_sint8;
+    assert_equal (I.of_int IUShort (of_int 31376)) b_uint16;
+    assert_equal (I.of_int IShort (of_int 31376)) b_sint16
+
+  let test_wrap_2 _ =
+    let z1 = of_int 30867 in
+    let z2 = of_int 30870 in
+    let join_cast_unsigned = I.join IChar (I.of_int IChar z1) (I.of_int IChar z2) in
+
+    let expected_unsigned = I.join IChar (I.of_int IChar (of_int 147)) (I.of_int IChar (of_int 150)) in
+
+    let expected_signed = I.join IChar (I.of_int IChar (of_int (-106))) (I.of_int IChar (of_int (-109))) in
+
+    assert_equal expected_unsigned join_cast_unsigned;
+    assert_equal expected_signed join_cast_unsigned
+
+  let test_widen_1 _ =
+    let b1 = I.of_int ik (of_int 3) in
+    let b2 = I.of_int ik (of_int 17) in
+
+    (* widen both masks *)
+    assert_equal (I.top_of ik) (I.widen ik b1 b2);
+
+    (* no widening *)
+    let bjoin = I.join ik b1 b2 in
+    assert_equal bjoin (I.widen ik bjoin b1)
+
+
+  let test_widen_2 _ =
+    let b1 = I.of_int ik (of_int 123613) in
+    let b2 = I.of_int ik (of_int 613261) in
+
+    (* no widening needed *)
+    assert_bool "join leq widen" (I.leq (I.join ik b1 b2) (I.widen ik b1 b2))
+
+  let test_of_interval _ =
+    let intvl= (of_int 3, of_int 17) in
+    let b1 = I.of_interval ik intvl in
+
+    for i = 3 to 17 do
+      assert_bool (string_of_int i) (I.equal_to (of_int i) b1 = `Top)
+    done
+
+  let test_of_bool _ =
+    let b1 = I.of_bool ik true in
+    let b2 = I.of_bool ik false in
+
+    assert_bool "true" (I.equal_to (of_int 1) b1 = `Eq);
+    assert_bool "false" (I.equal_to (of_int 0) b2 = `Eq)
+
+  let test_to_bool _ =
+    let b1 = I.of_int ik (of_int 3) in
+    let b2 = I.of_int ik (of_int (-6)) in
+    let b3 = I.of_int ik (of_int 0) in
+
+    let b12 = I.join ik b1 b2 in
+    let b13 = I.join ik b1 b3 in
+    let b23 = I.join ik b2 b3 in
+
+    assert_bool "3" (I.to_bool b1 = Some true);
+    assert_bool "-6" (I.to_bool b2 = Some true);
+    assert_bool "0" (I.to_bool b3 = Some false);
+
+    assert_bool "3 | -6" (I.to_bool b12 = Some true);
+    assert_bool "3 | 0" (I.to_bool b13 = None);
+    assert_bool "-6 | 0" (I.to_bool b23 = None)
+
+  let test_cast_to _ =
+    let b1 = I.of_int ik (of_int 1234) in
+    
+    assert_equal (I.of_int IChar (of_int (210))) (I.cast_to IChar b1);
+    assert_equal (I.of_int ISChar (of_int (-46))) (I.cast_to ISChar b1);
+
+    assert_equal (I.of_int IUInt128 (of_int 1234)) (I.cast_to IUInt128 b1)
+
+  (* Bitwise  *)
+
+  let test_logxor _ =
+    let b1 = I.of_int ik (of_int 5) in
+    let b2 = I.of_int ik (of_int 17) in
+
+    assert_equal (I.of_int ik (of_int 20)) (I.logxor ik b1 b2);
+
+    let b12 = I.join ik b1 b2 in
+    let b3 = I.of_int ik (of_int 13) in
+    assert_bool "8 ?= 13 xor (5 | 17)" (I.equal_to (of_int 8) (I.logxor ik b12 b3) = `Top);
+    assert_bool "28 ?= 13 xor (5 | 17)" (I.equal_to (of_int 28) (I.logxor ik b12 b3) = `Top)
+
+  let test_logand _ =
+    let b1 = I.of_int ik (of_int 7) in
+    let b2 = I.of_int ik (of_int 13) in
+
+    assert_equal (I.of_int ik (of_int 5)) (I.logand ik b1 b2);
+
+    let b12 = I.join ik b1 b2 in
+    let b3 = I.of_int ik (of_int 12) in
+    assert_bool "4 ?= 12 and (7 | 12)" (I.equal_to (of_int 4) (I.logand ik b12 b3) = `Top);
+    assert_bool "12 ?= 12 and (7 | 12)" (I.equal_to (of_int 12) (I.logand ik b12 b3) = `Top)
+
+
+  let test_logor _ =
+    let b1 = I.of_int ik (of_int 5) in
+    let b2 = I.of_int ik (of_int 17) in
+
+    assert_equal (I.of_int ik (of_int 21)) (I.logor ik b1 b2);
+
+    let b12 = I.join ik b1 b2 in
+    let b3 = I.of_int ik (of_int 13) in
+    assert_bool "13 ?= 13 or (5 | 17)" (I.equal_to (of_int 13) (I.logor ik b12 b3) = `Top);
+    assert_bool "29 ?= 13 or (5 | 17)" (I.equal_to (of_int 29) (I.logor ik b12 b3) = `Top)
+
+ let test_lognot _ =
+    let b1 = I.of_int ik (of_int 4) in
+    let b2 = I.of_int ik (of_int 12) in
+
+    (* assumes two's complement *)
+    assert_equal (I.of_int ik (of_int (-5))) (I.lognot ik b1);
+
+    let b12= I.join ik b1 b2 in
+    assert_bool "-13 ?= not (4 | 12)" (I.equal_to (of_int (-13)) (I.lognot ik b12) = `Top);
+    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
+    
+    assert_bool "2 << 1 = 4" (I.equal_to (of_int (4)) (I.shift_left ik stat1 stat2) = `Top)
+
+
+  let test_shift_right _ =
+    let stat1 = I.of_int ik (of_int 4) in
+    let stat2 = I.of_int ik (of_int 1) in
+
+    assert_bool "4 >> 1 = 2" (I.equal_to (of_int (2)) (I.shift_left ik stat1 stat2) = `Top)
+
+
+  (* Arith *)
+
+
+  (* Comparisons *)
+
+  let test_eq _ =
+    let b1 = I.of_int ik (of_int 5) in
+    let b2 = I.of_int ik (of_int 17) in
+
+    assert_bool "5 == 5" (I.eq ik b1 b1 = I.of_bool ik true);
+    assert_bool "5 == 17" (I.eq ik b1 b2 = I.of_bool ik false);
+
+    let b12 = I.join ik b1 b2 in
+    assert_bool "5 == (5 | 17)" (I.eq ik b1 b12 = (I.join ik (I.of_bool ik true) (I.of_bool ik false)))
+
+  let test_ne _ =
+    let b1 = I.of_int ik (of_int 5) in
+    let b2 = I.of_int ik (of_int 17) in
+
+    assert_bool "5 != 5" (I.ne ik b1 b1 = I.of_bool ik false);
+    assert_bool "5 != 17" (I.ne ik b1 b2 = I.of_bool ik true);
+
+    let b12 = I.join ik b1 b2 in
+    assert_bool "5 != (5 | 17)" (I.ne ik b1 b12 = (I.join ik (I.of_bool ik false) (I.of_bool ik true)))
+
+  let test_le _ =
+    let b1 = I.of_int ik (of_int 5) in
+    let b2 = I.of_int ik (of_int 14) in
+
+    assert_bool "5 <= 5" (I.le ik b1 b1 = I.of_bool ik true);
+    assert_bool "5 <= 14" (I.le ik b1 b2 = I.of_bool ik true);
+    assert_bool "14 <= 5" (I.le ik b2 b1 = I.of_bool ik false);
+
+    let b12 = I.join ik b1 b2 in
+
+    let b3 = I.of_int ik (of_int 17) in
+    assert_bool "17 <= (5 | 14)" (I.le ik b3 b12 = I.of_bool ik false);
+
+    let b4 = I.of_int ik (of_int 13) in
+    assert_bool "13 <= (5 | 14)" (I.le ik b4 b12 = (I.join ik (I.of_bool ik false) (I.of_bool ik true)));
+
+    let b5 = I.of_int ik (of_int 5) in
+    assert_bool "5 <= (5 | 14)" (I.le ik b5 b12 = I.join ik (I.of_bool ik true) (I.of_bool ik false));
+
+    let b6 = I.of_int ik (of_int 4) in
+    assert_bool "4 <= (5 | 14)" (I.le ik b6 b12 = I.of_bool ik true)
+
+    
+  let test_ge _ =
+    let b1 = I.of_int ik (of_int 5) in
+    let b2 = I.of_int ik (of_int 14) in
+
+    assert_bool "5 >= 5" (I.ge ik b1 b1 = I.of_bool ik true);
+    assert_bool "5 >= 14" (I.ge ik b1 b2 = I.of_bool ik false);
+    assert_bool "14 >= 5" (I.ge ik b2 b1 = I.of_bool ik true);
+
+    let b12 = I.join ik b1 b2 in
+
+    let b3 = I.of_int ik (of_int 2) in
+    assert_bool "2 >= (5 | 14)" (I.ge ik b3 b12 = I.of_bool ik false);
+
+    let b4 = I.of_int ik (of_int 13) in
+    assert_bool "13 >= (5 | 14)" (I.ge ik b4 b12 = (I.join ik (I.of_bool ik true) (I.of_bool ik false)));
+
+    let b6 = I.of_int ik (of_int 15) in
+    assert_bool "15 >= (5 | 14)" (I.ge ik b6 b12 = I.of_bool ik true)
+
+  let test_lt _ =
+    let b1 = I.of_int ik (of_int 7) in
+    let b2 = I.of_int ik (of_int 13) in
+
+    assert_bool "7 < 7" (I.lt ik b1 b1 = I.of_bool ik false);
+    assert_bool "7 < 13" (I.lt ik b1 b2 = I.of_bool ik true);
+
+    let b12 = I.join ik b1 b2 in
+    let b3 = I.of_int ik (of_int 4) in
+    assert_bool "4 < (7 | 13)" (I.lt ik b3 b12 = I.of_bool ik true);
+
+    let b4 = I.of_int ik (of_int 8) in
+    assert_bool "8 < (7 | 13)" (I.lt ik b4 b12 = I.join ik (I.of_bool ik false) (I.of_bool ik true))
+
+  let test_gt _ =
+    let b1 = I.of_int ik (of_int 5) in
+    let b2 = I.of_int ik (of_int 14) in
+
+
+    assert_bool "5 > 5" (I.gt ik b1 b1 = I.of_bool ik false);
+    assert_bool "5 > 14" (I.gt ik b1 b2 = I.of_bool ik false);
+    assert_bool "14 > 5" (I.gt ik b2 b1 = I.of_bool ik true);
+
+    let b12 = I.join ik b1 b2 in
+
+    let b3 = I.of_int ik (of_int 2) in
+    assert_bool "2 > (5 | 14)" (I.gt ik b3 b12 = I.of_bool ik false);
+
+    let b4 = I.of_int ik (of_int 13) in
+    assert_bool "13 > (5 | 14)" (I.gt ik b4 b12 = (I.join ik (I.of_bool ik false) (I.of_bool ik true)));
+
+    let b5 = I.of_int ik (of_int 5) in
+    assert_bool "5 > (5 | 14)" (I.gt ik b5 b12 = I.join ik (I.of_bool ik false) (I.of_bool ik true));
+
+    let b6 = I.of_int ik (of_int 4) in
+    assert_bool "4 > (5 | 14)" (I.gt ik b6 b12 = (I.of_bool ik false) )
+
+  let test_starting _ =
+    let bf1 = I.starting ik (of_int 17) in
+
+    assert_bool "17" (I.equal_to (of_int 17) bf1 = `Top);
+    assert_bool "18" (I.equal_to (of_int 18) bf1 = `Top);
+
+    assert_bool "-3" (I.equal_to (of_int (-3)) bf1 = `Neq);
+
+    let bf2 = I.starting ik (of_int (-17)) in
+
+    assert_bool "-16" (I.equal_to (of_int (-16)) bf2 = `Top);
+    assert_bool "-17" (I.equal_to (of_int (-17)) bf2 = `Top)
+
+
+  let test_ending _ =
+    let bf = I.ending ik (of_int 17) in
+
+    assert_bool "-4" (I.equal_to (of_int (-4)) bf = `Top);
+    assert_bool "16" (I.equal_to (of_int 16) bf = `Top);
+
+    let bf2 = I.ending ik (of_int (-17)) in
+
+    assert_bool "-16" (I.equal_to (of_int (-16)) bf2 = `Top);
+    assert_bool "-18" (I.equal_to (of_int (-18)) bf2 = `Top);
+
+    assert_bool "17" (I.equal_to (of_int 17) bf2 = `Neq)
+
+  let test_refine_with_congruence _ =
+    let bf = I.top_of ik in
+
+    let bf_refined1= I.refine_with_congruence ik bf (Some (Z.of_int 3, Z.of_int 4)) in
+    assert_bool "3" (I.equal_to (of_int 3) bf_refined1 = `Top);
+    let bf_refined2= I.refine_with_congruence ik bf_refined1 (Some (Z.of_int 1, Z.of_int 1)) in
+    assert_bool "1" (I.equal_to (of_int 1) bf_refined2 = `Eq);
+    let bf_refined3= I.refine_with_congruence ik bf_refined2 (Some (Z.of_int 5, Z.of_int 0)) in
+    assert_bool "5" (I.equal_to (of_int 5) bf_refined3 = `Eq)
+
+  let test_refine_with_inclusion_list _ =
+    let bf = I.top_of ik in
+
+    let list = List.map of_int [-2;3;23; 26] in
+    let bf_refined = I.refine_with_incl_list ik bf (Some list) in
+
+    List.iter (fun i -> assert_bool (Z.to_string i) (I.equal_to i bf_refined = `Top)) list
+
+  let test () =[
+    "test_of_int_to_int" >:: test_of_int_to_int;
+    "test_to_int_of_int" >:: test_to_int_of_int;
+    "test_equal_to" >:: test_equal_to;
+
+    "test_join" >:: test_join;
+    "test_meet" >:: test_meet;
+
+    "test_leq_1" >:: test_leq_1;
+    "test_leq_2" >:: test_leq_2;
+
+    "test_wrap_1" >:: test_wrap_1;
+    "test_wrap_2" >:: test_wrap_2;
+
+    "test_widen_1" >:: test_widen_1;
+    "test_widen_2" >:: test_widen_2;
+
+    "test_of_interval" >:: test_of_interval;
+    "test_of_bool" >:: test_of_bool;
+    "test_to_bool" >:: test_to_bool;
+    "test_cast_to" >:: test_cast_to;
+
+    "test_logxor" >:: test_logxor;
+    "test_logand" >:: test_logand;
+    "test_logor" >:: test_logor;
+    "test_lognot" >:: test_lognot;
+    "test_shift_left" >:: test_shift_left;
+    "test_shift_right" >:: test_shift_right;
+
+    "test_eq" >:: test_eq;
+    "test_ne" >:: test_ne;
+    "test_le" >:: test_le;
+    "test_ge" >:: test_ge;
+    "test_lt" >:: test_lt;
+    "test_gt" >:: test_gt;
+
+    "test_starting" >:: test_starting;
+    "test_ending" >:: test_ending;
+
+    "test_refine_with_congruence" >:: test_refine_with_congruence;
+    "test_refine_with_inclusion_list" >:: test_refine_with_inclusion_list;
+    ]
+
+end
+
 module Interval    = IntervalTest (IntDomain.Interval)
+module BitField    = BitFieldTest (IntDomain.BitField)
 module IntervalSet = IntervalTest (IntDomain.IntervalSet)
 
 module Congruence =
@@ -330,6 +749,7 @@ let test () =
     "test_meet"     >::  test_meet;
     "test_excl_list">::  test_ex_set;
     "interval" >::: Interval.test ();
+    "bitField" >::: BitField.test ();
     "intervalSet" >::: IntervalSet.test ();
     "congruence" >::: Congruence.test ();
     "intDomTuple" >::: IntDomTuple.test ();

From 5ce8db7742c88c12e8ca5de8c0edf015d890ba49 Mon Sep 17 00:00:00 2001
From: leon <leonunterberger@gmx.at>
Date: Tue, 19 Nov 2024 13:58:41 +0100
Subject: [PATCH 14/15] add simple tests

---
 src/cdomain/value/cdomains/intDomain.ml | 72 ++++++++++++++-----------
 tests/unit/cdomains/intDomainTest.ml    | 22 ++++++--
 2 files changed, 59 insertions(+), 35 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 6a5226a3bd..dfe5b8da8c 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1226,8 +1226,6 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
 
   let logor (z1,o1)  (z2,o2) = (Ints_t.logand z1 z2, Ints_t.logor o1 o2)
 
-  let join (z1,o1) (z2,o2) = (Ints_t.logor z1 z2, Ints_t.logor o1 o2)
-
   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
@@ -1289,35 +1287,47 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
     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 unknownBitMask = bits_unknown (z,o) in
-    let impossibleBitMask = bits_undef (z,o) in
-    let guaranteedBits = bits_set (z,o) in
-
-    if impossibleBitMask <> zero_mask then
-      failwith "Impossible bitfield"
-    else
-
-    if isSigned ik then
-      let signBitMask = make_bitone_msk (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
-      Size.cast ik (Ints_t.to_bigint guaranteedBits)
-
-  let max ik (z,o) =
-    let unknownBitMask = bits_unknown (z,o) in
-    let impossibleBitMask = bits_undef (z,o) in
-    let guaranteedBits = bits_set (z,o) 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 (* Necessary? *)
-    Size.cast ik (Ints_t.to_bigint (Ints_t.logor guaranteedBits worstPossibleUnknownBits))
-
+    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
diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml
index 0a9a8dfd97..5e49252aae 100644
--- a/tests/unit/cdomains/intDomainTest.ml
+++ b/tests/unit/cdomains/intDomainTest.ml
@@ -463,15 +463,29 @@ module I = IntDomain.SOverflowUnlifter (I)
   let test_shift_left _ =
     let stat1 = I.of_int ik (of_int 2) in
     let stat2 = I.of_int ik (of_int 1) in
-    
-    assert_bool "2 << 1 = 4" (I.equal_to (of_int (4)) (I.shift_left ik stat1 stat2) = `Top)
+    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 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);
 
-    assert_bool "4 >> 1 = 2" (I.equal_to (of_int (2)) (I.shift_left ik stat1 stat2) = `Top)
+    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 *)

From 4170f7fc526b8f787d5ad3ba26de5c7111a9d7b9 Mon Sep 17 00:00:00 2001
From: leon <leonunterberger@gmx.at>
Date: Tue, 19 Nov 2024 14:39:53 +0100
Subject: [PATCH 15/15] fix small bug in constant shifting expecting isSigned
 ik to check if the value is signed

---
 src/cdomain/value/cdomains/intDomain.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index dfe5b8da8c..823007475f 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1271,7 +1271,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
   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 then
+      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)