Skip to content

Split integer overflow category in dashboard checks #1929

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

Merged
sim642 merged 4 commits into from
Jan 23, 2026
Merged

Split integer overflow category in dashboard checks #1929

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
4acfe14
Split integer overflow category in dashboard checks
sim642 Jan 21, 2026
5a399b4
Deduplicate cases in IntDomain0.add_overflow_check
sim642 Jan 21, 2026
d0e54b2
Add left shift overflows as invalid shift checks in dashboard
sim642 Jan 21, 2026
73baa12
Add word "operator" after "arithmetic" to checks as in Mopsa and dash…
karoliineh Jan 22, 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
51 changes: 40 additions & 11 deletions src/cdomain/value/cdomains/intDomain0.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,17 @@ let add_overflow_check ~(op:overflow_op) ~underflow ~overflow ik =
let signed = Cil.isSigned ik in
if !AnalysisState.postsolving && signed && (match op with Cast _ -> false | _ -> true) && (underflow || overflow) then
AnalysisState.svcomp_may_overflow := true;
let sign = if signed then "Signed" else "Unsigned" in
let check: Checks.Category.t option =
match signed, op with
| true, (Unop Neg | Binop (PlusA | MinusA | Mult | Div | Mod)) -> Some SignedIntegerOverflowInArithmetic
| true, Cast Explicit -> Some SignedIntegerOverflowInExplicitCast
| true, Cast (IntegerPromotion | DefaultArgumentPromotion | ArithmeticConversion | ConditionalConversion | PointerConversion | Implicit) -> Some SignedIntegerOverflowInImplicitCast
| false, (Unop Neg | Binop (PlusA | MinusA | Mult | Div | Mod)) -> Some UnsignedIntegerOverflowInArithmetic
| false, Cast Explicit -> Some UnsignedIntegerOverflowInExplicitCast
| false, Cast (IntegerPromotion | DefaultArgumentPromotion | ArithmeticConversion | ConditionalConversion | PointerConversion | Implicit) -> Some UnsignedIntegerOverflowInImplicitCast
| _, Binop Shiftlt -> Some InvalidShift
| _, _ -> None
in
let op =
match op with
(* explicitly distinguish binary and unary - *)
Expand All @@ -103,19 +113,38 @@ let add_overflow_check ~(op:overflow_op) ~underflow ~overflow ik =
| Cast Internal -> "internal cast"
| Internal -> "internal operation"
in
let message =
let sign = if signed then "Signed" else "Unsigned" in
match underflow, overflow with
| true, true ->
Printf.sprintf "%s integer overflow and underflow in %s" sign op
| true, false ->
Printf.sprintf "%s integer underflow in %s" sign op
| false, true ->
Printf.sprintf "%s integer overflow in %s" sign op
| false, false ->
let sign = if signed then "signed" else "unsigned" in (* lowercase constants *)
Printf.sprintf "No %s integer overflow or underflow in %s" sign op
in
let tags: M.Tag.t list =
match underflow, overflow with
| true, true -> [CWE 190; CWE 191]
| true, false -> [CWE 191]
| false, true -> [CWE 190]
| false, false -> []
in
match underflow, overflow with
| true, true ->
M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 190; CWE 191] "%s integer overflow and underflow in %s" sign op;
Checks.warn Checks.Category.IntegerOverflow "%s integer overflow and underflow in %s" sign op
| true, false ->
M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 191] "%s integer underflow in %s" sign op;
Checks.warn Checks.Category.IntegerOverflow "%s integer underflow in %s" sign op
| true, true
| true, false
| false, true ->
M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 190] "%s integer overflow in %s" sign op;
Checks.warn Checks.Category.IntegerOverflow "%s integer overflow in %s" sign op
M.warn ~category:M.Category.Integer.overflow ~tags "%s" message;
Option.iter (fun check ->
Checks.warn check "%s" message
) check
| false, false ->
let sign = if signed then "signed" else "unsigned" in (* lowercase constants *)
Checks.safe_msg Checks.Category.IntegerOverflow "No %s integer overflow or underflow in %s" sign op
Option.iter (fun check ->
Checks.safe_msg check "%s" message
) check


let reset_lazy () =
Expand Down
24 changes: 21 additions & 3 deletions src/common/util/checks.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,13 @@ module Category = struct
| AssertionFailure
| InvalidMemoryAccess
| DivisionByZero
| IntegerOverflow
| SignedIntegerOverflowInArithmetic
| SignedIntegerOverflowInExplicitCast
| SignedIntegerOverflowInImplicitCast
| UnsignedIntegerOverflowInArithmetic
| UnsignedIntegerOverflowInExplicitCast
| UnsignedIntegerOverflowInImplicitCast
| InvalidShift
| InvalidPointerComparison
| InvalidPointerSubtraction
| DoubleFree
Expand All @@ -46,7 +52,13 @@ module Category = struct
| AssertionFailure -> "Assertion failure"
| InvalidMemoryAccess -> "Invalid memory access"
| DivisionByZero -> "Division by zero"
| IntegerOverflow -> "Integer overflow"
| SignedIntegerOverflowInArithmetic -> "Signed integer overflow in arithmetic operator"
| SignedIntegerOverflowInExplicitCast -> "Signed integer overflow in explicit cast"
| SignedIntegerOverflowInImplicitCast -> "Signed integer overflow in implicit cast"
| UnsignedIntegerOverflowInArithmetic -> "Unsigned integer overflow in arithmetic operator"
| UnsignedIntegerOverflowInExplicitCast -> "Unsigned integer overflow in explicit cast"
| UnsignedIntegerOverflowInImplicitCast -> "Unsigned integer overflow in implicit cast"
| InvalidShift -> "Invalid shift"
| InvalidPointerComparison -> "Invalid pointer comparison"
| InvalidPointerSubtraction -> "Invalid pointer subtraction"
| DoubleFree -> "Double free"
Expand All @@ -57,7 +69,13 @@ module Category = struct
| `String "Assertion failure" -> Ok AssertionFailure
| `String "Invalid memory access" -> Ok InvalidMemoryAccess
| `String "Division by zero" -> Ok DivisionByZero
| `String "Integer overflow" -> Ok IntegerOverflow
| `String "Signed integer overflow in arithmetic operator" -> Ok SignedIntegerOverflowInArithmetic
| `String "Signed integer overflow in explicit cast" -> Ok SignedIntegerOverflowInExplicitCast
| `String "Signed integer overflow in implicit cast" -> Ok SignedIntegerOverflowInImplicitCast
| `String "Unsigned integer overflow in arithmetic operator" -> Ok UnsignedIntegerOverflowInArithmetic
| `String "Unsigned integer overflow in explicit cast" -> Ok UnsignedIntegerOverflowInExplicitCast
| `String "Unsigned integer overflow in implicit cast" -> Ok UnsignedIntegerOverflowInImplicitCast
| `String "Invalid shift" -> Ok InvalidShift
| `String "Invalid pointer comparison" -> Ok InvalidPointerComparison
| `String "Invalid pointer subtraction" -> Ok InvalidPointerSubtraction
| `String "Double free" -> Ok DoubleFree
Expand Down
Loading