fixed edge case where shift with 0 was done without zero in shifting bf

goblint · Dec 3, 2024 · 9bcd884 · 9bcd884
1 parent 3e4928a
commit 9bcd884
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 11 deletions.
diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
@@ -1187,12 +1187,16 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
       ((z >>: c) |: sign_msk, o >>: c)
 
   let shift_right ik (z1, o1) (z2, o2) = 
-    if is_const (z2, o2) then shift_right_action ik (z1, o1) (Ints_t.to_int o2)
+    if is_const (z2, o2) 
+      then 
+        shift_right_action ik (z1, o1) (Ints_t.to_int o2)
     else
       let max_bit = Z.log2up (Z.of_int (Size.bit ik)) in
-      let mask = !:(one_mask<<:max_bit) in
-      let concrete_values = concretize ((z2 &: mask), (o2 &: mask)) in
-      if (List.length concrete_values) == 0 then (one_mask, zero_mask)
+      let mask_usefull_bits = !:(one_mask<<:max_bit) in
+      let concrete_values = concretize ((z2 &: mask_usefull_bits), (o2 &: mask_usefull_bits)) in
+      if (((o2 &: mask_usefull_bits) == Ints_t.of_int 0) && (z2 != one_mask)) || (List.length concrete_values) == 0 
+        then 
+          (one_mask, zero_mask)
       else 
         let (v1, v2) = (ref zero_mask, ref zero_mask) in
         List.iter (fun x -> let (a, b) = (shift_right_action ik (z1, o1) x) in
@@ -1207,12 +1211,16 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
 
   let shift_left ik (z1, o1) (z2, o2) = 
     (* (one_mask, Ints_t.of_int (Size.bit ik)) *)
-    if is_const (z2, o2) then shift_left_action ik (z1, o1) (Ints_t.to_int o2)
+    if is_const (z2, o2) 
+      then 
+        shift_left_action ik (z1, o1) (Ints_t.to_int o2)
     else
       let max_bit = Z.log2up (Z.of_int (Size.bit ik)) in
-      let mask = !:(one_mask<<:max_bit) in
-      let concrete_values = concretize ((z2 &: mask), (o2 &: mask)) in
-      if (List.length concrete_values) == 0 then (one_mask, zero_mask)
+      let mask_usefull_bits = !:(one_mask <<: max_bit) in
+      let concrete_values = concretize ((z2 &: mask_usefull_bits), (o2 &: mask_usefull_bits)) in
+      if (((o2 &: mask_usefull_bits) == Ints_t.of_int 0) && (z2 != one_mask)) || (List.length concrete_values) == 0 
+      then 
+        (one_mask, zero_mask)
       else 
         let (v1, v2) = (ref zero_mask, ref zero_mask) in
         List.iter (fun x -> let (a, b) = (shift_left_action ik (z1, o1) x) in

diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml
@@ -492,15 +492,18 @@ struct
     assert_shift_left ik [-1] [2] [-4];
     assert_shift_left ik [-1] [3] [-8];
     assert_shift_left ik [-2] [1; 2] [-2; -4; -8; -16];
-    assert_shift_left ik [-1] [1; 2] [-1; -2; -4; -8]
-
+    assert_shift_left ik [-1] [1; 2] [-1; -2; -4; -8];
+    assert_shift_left ik [1073741824] [128; 384] [0];
+    assert_shift_left ik [1073741824] [0; 128; 384] [1073741824]
 
   let test_shift_right _ =
     assert_shift_right ik [4] [1] [2];
     assert_shift_right ik [-4] [1] [-2];
     assert_shift_right ik [1] [1] [0];
     assert_shift_right ik [1] [1; 2] [0; 1];
-    assert_shift_right ik [1; 2] [1; 2] [0; 1; 2; 3]
+    assert_shift_right ik [1; 2] [1; 2] [0; 1; 2; 3];
+    assert_shift_right ik [32] [64; 2] [8; 32];
+    assert_shift_right ik [32] [128; 384] [0]
 
 
   (* Arith *)