Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
Copilot wants to merge 7 commits into
base: master
Choose a base branch
from
+60 −3
Draft

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

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
ee780c5
Initial plan
Copilot Apr 12, 2026
5ee0617
Add warnings for bitwise shift with negative shift amount (UB in C)
Copilot Apr 12, 2026
fad313c
Flatten nested match in shift_amount_negcheck for readability
Copilot Apr 12, 2026
5d9e460
Use Behavior.Undefined.other category for shift-by-negative warnings
Copilot Apr 12, 2026
67be8c5
Refactor shift neg check to deduplicate code; fix test to use unsigne…
Copilot Apr 23, 2026
5dd9a2e
Fix test: use bounded non-negative interval [0,5] instead of unsigned…
Copilot Apr 23, 2026
9292a45
Merge branch 'master' into copilot/warn-bitwise-shift-misuse
michael-schwarz Apr 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
37 changes: 34 additions & 3 deletions src/analyses/base.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -223,7 +223,16 @@ struct
| Bot -> Bot
| _ -> VD.top ()

let binop_ID (result_ik: Cil.ikind) = function
let binop_ID (result_ik: Cil.ikind) =
(* Classify the shift amount as definitely non-negative, definitely negative,
or possibly negative, to check for undefined behavior. *)
let shift_amount_negcheck y =
match ID.minimal y, ID.maximal y with
| Some min_y, _ when Z.geq min_y Z.zero -> `NonNeg
| _, Some max_y when Z.lt max_y Z.zero -> `Neg
| _ -> `MayNeg
in
function
| PlusA -> ID.add
| MinusA -> ID.sub
| Mult -> ID.mul
Expand Down Expand Up @@ -265,8 +274,30 @@ struct
| BAnd -> ID.logand
| BOr -> ID.logor
| BXor -> ID.logxor
| Shiftlt -> ID.shift_left
| Shiftrt -> ID.shift_right
| Shiftlt ->
fun x y ->
(* If the shift amount is negative, the result is undefined behavior in C *)
(match shift_amount_negcheck y with
| `NonNeg -> Checks.safe Checks.Category.InvalidShift
| `Neg ->
M.error ~category:M.Category.Behavior.Undefined.other ~tags:[CWE 758] "Shift-left by negative amount is undefined behavior";
Copy link
Copy Markdown
Member

@sim642 sim642 Apr 17, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems like all of these duplicated messages and checks could be deduplicated in shift_amount_negcheck.

Copy link
Copy Markdown
Contributor Author

Copilot AI Apr 23, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done in commit 67be8c5. Renamed shift_amount_negcheck to check_shift_neg dir y which now performs the M.error/M.warn/Checks.* calls directly with the direction embedded in the message. The Shiftlt and Shiftrt cases are now just:

| 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

Also fixed the failing test — the int nonneg case (which relied on interval analysis propagating lower bounds through the combined def_exc+interval tuple) was replaced with unsigned int u_shift, which is always non-negative by type.

Checks.error Checks.Category.InvalidShift "Shift-left by negative amount is undefined behavior"
| `MayNeg ->
M.warn ~category:M.Category.Behavior.Undefined.other ~tags:[CWE 758] "Shift-left by possibly negative amount may be undefined behavior";
Checks.warn Checks.Category.InvalidShift "Shift-left by possibly negative amount may be undefined behavior");
ID.shift_left x y
| Shiftrt ->
fun x y ->
(* If the shift amount is negative, the result is undefined behavior in C *)
(match shift_amount_negcheck y with
| `NonNeg -> Checks.safe Checks.Category.InvalidShift
| `Neg ->
M.error ~category:M.Category.Behavior.Undefined.other ~tags:[CWE 758] "Shift-right by negative amount is undefined behavior";
Checks.error Checks.Category.InvalidShift "Shift-right by negative amount is undefined behavior"
| `MayNeg ->
M.warn ~category:M.Category.Behavior.Undefined.other ~tags:[CWE 758] "Shift-right by possibly negative amount may be undefined behavior";
Checks.warn Checks.Category.InvalidShift "Shift-right by possibly negative amount may be undefined behavior");
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))
Expand Down
36 changes: 36 additions & 0 deletions tests/regression/98-bitwise-operations/09-shift-neg.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
// 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

// Definitely non-negative interval: no warning
int nonneg;
if (nonneg < 0) { nonneg = 0; }
res = 8 << nonneg; //NOWARN
res = 8 >> nonneg; //NOWARN

return 0;
}
Loading