diff --git a/src/cdomain/value/cdomains/intDomain0.ml b/src/cdomain/value/cdomains/intDomain0.ml index b65df111ed..eae0318231 100644 --- a/src/cdomain/value/cdomains/intDomain0.ml +++ b/src/cdomain/value/cdomains/intDomain0.ml @@ -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 - *) @@ -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 () = diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index ec112c5eca..2efdc341f8 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -34,7 +34,13 @@ module Category = struct | AssertionFailure | InvalidMemoryAccess | DivisionByZero - | IntegerOverflow + | SignedIntegerOverflowInArithmetic + | SignedIntegerOverflowInExplicitCast + | SignedIntegerOverflowInImplicitCast + | UnsignedIntegerOverflowInArithmetic + | UnsignedIntegerOverflowInExplicitCast + | UnsignedIntegerOverflowInImplicitCast + | InvalidShift | InvalidPointerComparison | InvalidPointerSubtraction | DoubleFree @@ -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" @@ -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