Warn about bitwise shift with negative shift amount (UB in C) (#1989)

* Initial plan

* Add warnings for bitwise shift with negative shift amount (UB in C)

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/c81d432d-7783-4469-9c48-85d6bb3d1531

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Flatten nested match in shift_amount_negcheck for readability

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/c81d432d-7783-4469-9c48-85d6bb3d1531

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Use Behavior.Undefined.other category for shift-by-negative warnings

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/c81d432d-7783-4469-9c48-85d6bb3d1531

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Refactor shift neg check to deduplicate code; fix test to use unsigned int

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/1dec7b36-67b9-4835-abab-afb1ff9c852e

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Fix test: use bounded non-negative interval [0,5] instead of unsigned int top

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/daf39d5f-96e8-4887-9ade-7004d5fcc994

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

* Use ID.ge/ID.lt instead of ID.minimal/ID.maximal in check_shift_neg

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/fd400683-08ae-4a0a-b4ff-458d87ba80f8

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>

Author: Copilot

src/analyses/base.ml

@@ -223,7 +223,23 @@ struct
     | Bot -> Bot
     | _ -> VD.top ()
 
-  let binop_ID (result_ik: Cil.ikind) = function
+  let binop_ID (result_ik: Cil.ikind) =
+    (* Check the shift amount for negative values (undefined behavior in C), emitting
+       appropriate warnings/errors based on bounds analysis. *)
+    let check_shift_neg dir y =
+      let ik = ID.ikind y in
+      let zero = ID.of_int ik Z.zero in
+      match ID.ge y zero, ID.lt y zero with
+      | Some true, _ ->
+        Checks.safe Checks.Category.InvalidShift
+      | _, Some true ->
+        M.error ~category:M.Category.Behavior.Undefined.other ~tags:[CWE 758] "Shift-%s by negative amount is undefined behavior" dir;
+        Checks.error Checks.Category.InvalidShift "Shift-%s by negative amount is undefined behavior" dir
+      | _ ->
+        M.warn ~category:M.Category.Behavior.Undefined.other ~tags:[CWE 758] "Shift-%s by possibly negative amount may be undefined behavior" dir;
+        Checks.warn Checks.Category.InvalidShift "Shift-%s by possibly negative amount may be undefined behavior" dir
+    in
+    function
     | PlusA -> ID.add
     | MinusA -> ID.sub
     | Mult -> ID.mul
@@ -265,8 +281,14 @@ struct
     | BAnd -> ID.logand
     | BOr -> ID.logor
     | BXor -> ID.logxor
-    | Shiftlt -> ID.shift_left
-    | Shiftrt -> ID.shift_right
+    | Shiftlt ->
+      fun x y ->
+        check_shift_neg "left" y;
+        ID.shift_left x y
+    | Shiftrt ->
+      fun x y ->
+        check_shift_neg "right" y;
+        ID.shift_right x y
     | LAnd -> id_binary_log (&&) ~annihilator:false result_ik
     | LOr -> id_binary_log (||) ~annihilator:true result_ik
     | b -> (fun x y -> (ID.top_of result_ik))

tests/regression/98-bitwise-operations/09-shift-neg.c

@@ -0,0 +1,37 @@
+// PARAM: --enable ana.int.interval
+#include <goblint.h>
+
+int main() {
+  int res;
+  int top;
+  int neg;
+
+  // Definitely negative shift amount: error
+  res = 8 << -2; //WARN
+
+  // Definitely negative shift amount in right shift: error
+  res = 8 >> -1; //WARN
+
+  // Non-negative shift amount: no warning
+  res = 8 << 2; //NOWARN
+  res = 8 >> 2; //NOWARN
+
+  // Zero shift amount: no warning
+  res = 8 << 0; //NOWARN
+  res = 8 >> 0; //NOWARN
+
+  // Possibly negative shift amount: warn
+  // (top is uninitialized, representing a non-deterministic value — a common convention in goblint tests)
+  if (top) { neg = -1; } else { neg = 1; }
+  res = 8 << neg; //WARN
+  res = 8 >> neg; //WARN
+
+  // Provably non-negative, bounded interval: no warning
+  // (pos_shift is [0,5] — non-negative and within valid shift range)
+  int pos_shift = 0;
+  if (top) { pos_shift = 5; }
+  res = 8 << pos_shift; //NOWARN
+  res = 8 >> pos_shift; //NOWARN
+
+  return 0;
+}