Skip to content

Commit 6178774

Browse files
sim642sim642
authored
Merge pull request #1929 from goblint/checks-integer-overflow
Split integer overflow category in dashboard checks
2 parents 94c3632 + 73baa12 commit 6178774

File tree

2 files changed

+61
-14
lines changed

2 files changed

+61
-14
lines changed

‎src/cdomain/value/cdomains/intDomain0.ml‎

Lines changed: 40 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -85,7 +85,17 @@ let add_overflow_check ~(op:overflow_op) ~underflow ~overflow ik =
8585
let signed = Cil.isSigned ik in
8686
if !AnalysisState.postsolving && signed && (match op with Cast _ -> false | _ -> true) && (underflow || overflow) then
8787
AnalysisState.svcomp_may_overflow := true;
88-
let sign = if signed then "Signed" else "Unsigned" in
88+
let check: Checks.Category.t option =
89+
match signed, op with
90+
| true, (Unop Neg | Binop (PlusA | MinusA | Mult | Div | Mod)) -> Some SignedIntegerOverflowInArithmetic
91+
| true, Cast Explicit -> Some SignedIntegerOverflowInExplicitCast
92+
| true, Cast (IntegerPromotion | DefaultArgumentPromotion | ArithmeticConversion | ConditionalConversion | PointerConversion | Implicit) -> Some SignedIntegerOverflowInImplicitCast
93+
| false, (Unop Neg | Binop (PlusA | MinusA | Mult | Div | Mod)) -> Some UnsignedIntegerOverflowInArithmetic
94+
| false, Cast Explicit -> Some UnsignedIntegerOverflowInExplicitCast
95+
| false, Cast (IntegerPromotion | DefaultArgumentPromotion | ArithmeticConversion | ConditionalConversion | PointerConversion | Implicit) -> Some UnsignedIntegerOverflowInImplicitCast
96+
| _, Binop Shiftlt -> Some InvalidShift
97+
| _, _ -> None
98+
in
8999
let op =
90100
match op with
91101
(* explicitly distinguish binary and unary - *)
@@ -103,19 +113,38 @@ let add_overflow_check ~(op:overflow_op) ~underflow ~overflow ik =
103113
| Cast Internal -> "internal cast"
104114
| Internal -> "internal operation"
105115
in
116+
let message =
117+
let sign = if signed then "Signed" else "Unsigned" in
118+
match underflow, overflow with
119+
| true, true ->
120+
Printf.sprintf "%s integer overflow and underflow in %s" sign op
121+
| true, false ->
122+
Printf.sprintf "%s integer underflow in %s" sign op
123+
| false, true ->
124+
Printf.sprintf "%s integer overflow in %s" sign op
125+
| false, false ->
126+
let sign = if signed then "signed" else "unsigned" in (* lowercase constants *)
127+
Printf.sprintf "No %s integer overflow or underflow in %s" sign op
128+
in
129+
let tags: M.Tag.t list =
130+
match underflow, overflow with
131+
| true, true -> [CWE 190; CWE 191]
132+
| true, false -> [CWE 191]
133+
| false, true -> [CWE 190]
134+
| false, false -> []
135+
in
106136
match underflow, overflow with
107-
| true, true ->
108-
M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 190; CWE 191] "%s integer overflow and underflow in %s" sign op;
109-
Checks.warn Checks.Category.IntegerOverflow "%s integer overflow and underflow in %s" sign op
110-
| true, false ->
111-
M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 191] "%s integer underflow in %s" sign op;
112-
Checks.warn Checks.Category.IntegerOverflow "%s integer underflow in %s" sign op
137+
| true, true
138+
| true, false
113139
| false, true ->
114-
M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 190] "%s integer overflow in %s" sign op;
115-
Checks.warn Checks.Category.IntegerOverflow "%s integer overflow in %s" sign op
140+
M.warn ~category:M.Category.Integer.overflow ~tags "%s" message;
141+
Option.iter (fun check ->
142+
Checks.warn check "%s" message
143+
) check
116144
| false, false ->
117-
let sign = if signed then "signed" else "unsigned" in (* lowercase constants *)
118-
Checks.safe_msg Checks.Category.IntegerOverflow "No %s integer overflow or underflow in %s" sign op
145+
Option.iter (fun check ->
146+
Checks.safe_msg check "%s" message
147+
) check
119148

120149

121150
let reset_lazy () =

‎src/common/util/checks.ml‎

Lines changed: 21 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,13 @@ module Category = struct
3434
| AssertionFailure
3535
| InvalidMemoryAccess
3636
| DivisionByZero
37-
| IntegerOverflow
37+
| SignedIntegerOverflowInArithmetic
38+
| SignedIntegerOverflowInExplicitCast
39+
| SignedIntegerOverflowInImplicitCast
40+
| UnsignedIntegerOverflowInArithmetic
41+
| UnsignedIntegerOverflowInExplicitCast
42+
| UnsignedIntegerOverflowInImplicitCast
43+
| InvalidShift
3844
| InvalidPointerComparison
3945
| InvalidPointerSubtraction
4046
| DoubleFree
@@ -46,7 +52,13 @@ module Category = struct
4652
| AssertionFailure -> "Assertion failure"
4753
| InvalidMemoryAccess -> "Invalid memory access"
4854
| DivisionByZero -> "Division by zero"
49-
| IntegerOverflow -> "Integer overflow"
55+
| SignedIntegerOverflowInArithmetic -> "Signed integer overflow in arithmetic operator"
56+
| SignedIntegerOverflowInExplicitCast -> "Signed integer overflow in explicit cast"
57+
| SignedIntegerOverflowInImplicitCast -> "Signed integer overflow in implicit cast"
58+
| UnsignedIntegerOverflowInArithmetic -> "Unsigned integer overflow in arithmetic operator"
59+
| UnsignedIntegerOverflowInExplicitCast -> "Unsigned integer overflow in explicit cast"
60+
| UnsignedIntegerOverflowInImplicitCast -> "Unsigned integer overflow in implicit cast"
61+
| InvalidShift -> "Invalid shift"
5062
| InvalidPointerComparison -> "Invalid pointer comparison"
5163
| InvalidPointerSubtraction -> "Invalid pointer subtraction"
5264
| DoubleFree -> "Double free"
@@ -57,7 +69,13 @@ module Category = struct
5769
| `String "Assertion failure" -> Ok AssertionFailure
5870
| `String "Invalid memory access" -> Ok InvalidMemoryAccess
5971
| `String "Division by zero" -> Ok DivisionByZero
60-
| `String "Integer overflow" -> Ok IntegerOverflow
72+
| `String "Signed integer overflow in arithmetic operator" -> Ok SignedIntegerOverflowInArithmetic
73+
| `String "Signed integer overflow in explicit cast" -> Ok SignedIntegerOverflowInExplicitCast
74+
| `String "Signed integer overflow in implicit cast" -> Ok SignedIntegerOverflowInImplicitCast
75+
| `String "Unsigned integer overflow in arithmetic operator" -> Ok UnsignedIntegerOverflowInArithmetic
76+
| `String "Unsigned integer overflow in explicit cast" -> Ok UnsignedIntegerOverflowInExplicitCast
77+
| `String "Unsigned integer overflow in implicit cast" -> Ok UnsignedIntegerOverflowInImplicitCast
78+
| `String "Invalid shift" -> Ok InvalidShift
6179
| `String "Invalid pointer comparison" -> Ok InvalidPointerComparison
6280
| `String "Invalid pointer subtraction" -> Ok InvalidPointerSubtraction
6381
| `String "Double free" -> Ok DoubleFree

0 commit comments

Comments
 (0)