Add operation names to integer overflow messages and checks

src/cdomain/value/cdomains/int/intDomTuple.ml

@@ -60,34 +60,31 @@ module IntDomTupleImpl = struct
   let create2 r x = (* use where values are introduced *)
     create2 r x (int_precision_from_node_or_config ())
 
-  let no_overflow ik = function
-    | Some(_, {underflow; overflow}) -> not (underflow || overflow)
-    | _ -> false
 
-  let check_ov ?(suppress_ovwarn = false) ~cast ik intv intv_set bf =
-    let no_ov = (no_overflow ik intv) || (no_overflow ik intv_set) || (no_overflow ik bf) in
-    if not suppress_ovwarn && (BatOption.is_some intv || BatOption.is_some intv_set || BatOption.is_some bf) then (
-      if not no_ov then (
-        let (_,{underflow=underflow_intv; overflow=overflow_intv}) = match intv with None -> (I2.bot (), {underflow= true; overflow = true}) | Some x -> x in
-        let (_,{underflow=underflow_intv_set; overflow=overflow_intv_set}) = match intv_set with None -> (I5.bot (), {underflow= true; overflow = true}) | Some x -> x in
-        let (_,{underflow=underflow_bf; overflow=overflow_bf}) = match bf with None -> (I6.bot (), {underflow= true; overflow = true}) | Some x -> x in
-        let underflow = underflow_intv && underflow_intv_set && underflow_bf in
-        let overflow = overflow_intv && overflow_intv_set && overflow_bf in
-        set_overflow_flag ~cast ~underflow ~overflow ik;
-      ) else if not !AnalysisState.executing_speculative_computations then (
-        Checks.safe_msg Checks.Category.IntegerOverflow "Cast: %B" cast
-      )
-    );
-    no_ov
+  let overflow_true = {underflow=true; overflow=true}
+  let get_overflow = function
+    | Some (_, overflow) -> overflow
+    | None -> overflow_true
+  let active_overflow = Option.is_some
+
+  let check_ov ?(suppress_ovwarn = false) ~op ik intv intv_set bf =
+    let {underflow=underflow_intv; overflow=overflow_intv} = get_overflow intv in
+    let {underflow=underflow_intv_set; overflow=overflow_intv_set} = get_overflow intv_set in
+    let {underflow=underflow_bf; overflow=overflow_bf} = get_overflow bf in
+    let underflow = underflow_intv && underflow_intv_set && underflow_bf in
+    let overflow = overflow_intv && overflow_intv_set && overflow_bf in
+    if not suppress_ovwarn && (active_overflow intv || active_overflow intv_set || active_overflow bf) then
+      add_overflow_check ~op ~underflow ~overflow ik;
+    not (underflow || overflow)
 
   let create2_ovc ?(suppress_ovwarn = false) ik r x ((p1, p2, p3, p4, p5, p6): int_precision) =
     let f b g = if b then Some (g x) else None in
     let map x = Option.map fst x in
     let intv =  f p2 @@ r.fi2_ovc (module I2) in
     let intv_set = f p5 @@ r.fi2_ovc (module I5) in
     let bf = f p6 @@ r.fi2_ovc (module I6) in
-    ignore (check_ov ~suppress_ovwarn ~cast:false ik intv intv_set bf);
-    map @@ f p1 @@ r.fi2_ovc (module I1), map @@ f p2 @@ r.fi2_ovc (module I2), map @@ f p3 @@ r.fi2_ovc (module I3), map @@ f p4 @@ r.fi2_ovc (module I4), map @@ f p5 @@ r.fi2_ovc (module I5) , map @@ f p6 @@ r.fi2_ovc (module I6)
+    ignore (check_ov ~suppress_ovwarn ~op:`Internal ik intv intv_set bf);
+    map @@ f p1 @@ r.fi2_ovc (module I1), map intv, map @@ f p3 @@ r.fi2_ovc (module I3), map @@ f p4 @@ r.fi2_ovc (module I4), map intv_set, map bf
 
   let create2_ovc ?(suppress_ovwarn = false) ik r x = (* use where values are introduced *)
     create2_ovc ~suppress_ovwarn ik r x (int_precision_from_node_or_config ())
@@ -304,12 +301,12 @@ module IntDomTupleImpl = struct
 
 
   (* map with overflow check *)
-  let mapovc ?(suppress_ovwarn=false) ?(cast=false) ik r (a, b, c, d, e, f) =
+  let mapovc ?(suppress_ovwarn=false) ~op ik r (a, b, c, d, e, f) =
     let map f ?no_ov = function Some x -> Some (f ?no_ov x) | _ -> None  in
     let intv = map (r.f1_ovc (module I2)) b in
     let intv_set = map (r.f1_ovc (module I5)) e in
     let bf = map (r.f1_ovc (module I6)) f in
-    let no_ov = check_ov ~suppress_ovwarn ~cast ik intv intv_set bf in
+    let no_ov = check_ov ~suppress_ovwarn ~op ik intv intv_set bf in
     let no_ov = no_ov || should_ignore_overflow ik in
     refine ik
       ( map (fun ?no_ov x -> r.f1_ovc ?no_ov (module I1) x |> fst) a
@@ -320,11 +317,11 @@ module IntDomTupleImpl = struct
       , BatOption.map fst bf)
 
   (* map2 with overflow check *)
-  let map2ovc ?(cast=false) ik r (xa, xb, xc, xd, xe, xf) (ya, yb, yc, yd, ye, yf) =
+  let map2ovc ~op ik r (xa, xb, xc, xd, xe, xf) (ya, yb, yc, yd, ye, yf) =
     let intv = opt_map2 (r.f2_ovc (module I2)) xb yb in
     let intv_set = opt_map2 (r.f2_ovc (module I5)) xe ye in
     let bf = opt_map2 (r.f2_ovc (module I6)) xf yf in
-    let no_ov = check_ov ~cast ik intv intv_set bf in
+    let no_ov = check_ov ~op ik intv intv_set bf in
     let no_ov = no_ov || should_ignore_overflow ik in
     refine ik
       ( opt_map2 (fun ?no_ov x y -> r.f2_ovc ?no_ov (module I1) x y |> fst) xa ya
@@ -358,7 +355,7 @@ module IntDomTupleImpl = struct
 
   (* f1: unary ops *)
   let neg ?no_ov ik =
-    mapovc ik {f1_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.neg ?no_ov ik)}
+    mapovc ~op:(`Unop Neg) ik {f1_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.neg ?no_ov ik)}
 
   let lognot ik =
     map ik {f1 = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.lognot ik)}
@@ -367,7 +364,7 @@ module IntDomTupleImpl = struct
     map ik {f1 = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.c_lognot ik)}
 
   let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov t =
-    mapovc ~suppress_ovwarn ~cast:true t {f1_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.cast_to ?torg ?no_ov t)}
+    mapovc ~suppress_ovwarn ~op:`Cast t {f1_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.cast_to ?torg ?no_ov t)}
 
   (* fp: projections *)
   let equal_to i x =
@@ -435,19 +432,19 @@ module IntDomTupleImpl = struct
     map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.narrow ik)}
 
   let add ?no_ov ik =
-    map2ovc ik
+    map2ovc ~op:(`Binop PlusA) ik
       {f2_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.add ?no_ov ik)}
 
   let sub ?no_ov ik =
-    map2ovc ik
+    map2ovc ~op:(`Binop MinusA) ik
       {f2_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.sub ?no_ov ik)}
 
   let mul ?no_ov ik =
-    map2ovc ik
+    map2ovc ~op:(`Binop Mult) ik
       {f2_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.mul ?no_ov ik)}
 
   let div ?no_ov ik =
-    map2ovc ik
+    map2ovc ~op:(`Binop Div) ik
       {f2_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.div ?no_ov ik)}
 
   let rem ik =
@@ -481,10 +478,10 @@ module IntDomTupleImpl = struct
     map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.logxor ik)}
 
   let shift_left ik =
-    map2ovc ik {f2_ovc= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.shift_left ik)}
+    map2ovc ~op:(`Binop Shiftlt) ik {f2_ovc= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.shift_left ik)}
 
   let shift_right ik =
-    map2ovc ik {f2_ovc= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.shift_right ik)}
+    map2ovc ~op:(`Binop Shiftrt) ik {f2_ovc= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.shift_right ik)}
 
   let c_logand ik =
     map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.c_logand ik)}

src/cdomain/value/cdomains/intDomain0.ml

@@ -71,27 +71,38 @@ let should_wrap ik = not (Cil.isSigned ik) || get_string "sem.int.signed_overflo
 let should_ignore_overflow ik = Cil.isSigned ik && get_string "sem.int.signed_overflow" = "assume_none"
 
 type overflow_info = IntDomain_intf.overflow_info = { overflow: bool; underflow: bool;}
+type overflow_op = [`Binop of binop | `Unop of unop | `Cast | `Internal]
 
-let set_overflow_flag ~cast ~underflow ~overflow ik =
+let add_overflow_check ~(op:overflow_op) ~underflow ~overflow ik =
   if !AnalysisState.executing_speculative_computations then
     (* Do not produce warnings when the operations are not actually happening in code *)
     ()
   else
     let signed = Cil.isSigned ik in
-    if !AnalysisState.postsolving && signed && not cast then
+    if !AnalysisState.postsolving && signed && op <> `Cast && (underflow || overflow) then
       AnalysisState.svcomp_may_overflow := true;
     let sign = if signed then "Signed" else "Unsigned" in
+    let op =
+      match op with
+      | `Binop bop -> CilType.Binop.show bop
+      | `Unop uop -> CilType.Unop.show uop
+      | `Cast -> "cast"
+      | `Internal -> "internal operation"
+    in
     match underflow, overflow with
     | true, true ->
-      M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 190; CWE 191] "%s integer overflow and underflow" sign;
-      Checks.warn Checks.Category.IntegerOverflow "%s integer overflow and underflow" sign
+      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" sign;
-      Checks.warn Checks.Category.IntegerOverflow "%s integer underflow" sign
+      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
     | false, true ->
-      M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 190] "%s integer overflow" sign;
-      Checks.warn Checks.Category.IntegerOverflow "%s integer overflow" sign
-    | false, false -> assert false
+      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
+    | 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
+
 
 let reset_lazy () =
   ana_int_config.interval_threshold_widening <- None;

tests/regression/29-svcomp/32-no-ov.t

@@ -1,10 +1,10 @@
   $ goblint --enable ana.int.interval --enable ana.sv-comp.enabled --enable ana.sv-comp.functions --set ana.specification "CHECK( init(main()), LTL(G ! overflow) )"  32-no-ov.c
   [Info] Setting "ana.int.interval" to true
   [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
-  [Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (32-no-ov.c:5:6-5:159)
-  [Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (32-no-ov.c:5:6-5:159)
-  [Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (32-no-ov.c:5:6-5:159)
-  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (32-no-ov.c:5:6-5:159)
+  [Warning][Integer > Overflow][CWE-190] Unsigned integer overflow in << (32-no-ov.c:5:6-5:159)
+  [Warning][Integer > Overflow][CWE-190] Unsigned integer overflow in << (32-no-ov.c:5:6-5:159)
+  [Warning][Integer > Overflow][CWE-191] Unsigned integer underflow in - (32-no-ov.c:5:6-5:159)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow in cast (32-no-ov.c:5:6-5:159)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 3
     dead: 0

tests/regression/29-svcomp/34-verifier-assert-def.t

@@ -1,5 +1,5 @@
   $ goblint --enable ana.sv-comp.functions --enable ana.int.interval 34-verifier-assert-def.c
-  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (34-verifier-assert-def.c:4:7-4:18)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow in << (34-verifier-assert-def.c:4:7-4:18)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 8
     dead: 0

tests/regression/29-svcomp/36-svcomp-arch.t

@@ -3,7 +3,7 @@ There should be overflow on ILP32:
   $ goblint --enable ana.sv-comp.enabled --set ana.specification "CHECK( init(main()), LTL(G ! overflow) )" --set exp.architecture 32bit 36-svcomp-arch.c
   [Info] Setting "ana.int.interval" to true
   [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
-  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (36-svcomp-arch.c:6:8-6:17)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow in * (36-svcomp-arch.c:6:8-6:17)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 4
     dead: 0

tests/regression/39-signed-overflows/15-div-minus-1.t

@@ -1,17 +1,17 @@
   $ goblint --enable warn.deterministic --enable ana.int.interval 15-div-minus-1.c
-  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (15-div-minus-1.c:5:9-5:26)
-  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (15-div-minus-1.c:7:5-7:16)
-  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (15-div-minus-1.c:9:9-9:20)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow in / (15-div-minus-1.c:5:9-5:26)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow in / (15-div-minus-1.c:7:5-7:16)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow in / (15-div-minus-1.c:9:9-9:20)
   [Warning][Integer > DivByZero][CWE-369] Second argument of division might be zero (15-div-minus-1.c:7:5-7:16)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 6
     dead: 0
     total lines: 6
 
   $ goblint --enable warn.deterministic --enable ana.int.interval_set 15-div-minus-1.c
-  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (15-div-minus-1.c:5:9-5:26)
-  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (15-div-minus-1.c:7:5-7:16)
-  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (15-div-minus-1.c:9:9-9:20)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow in / (15-div-minus-1.c:5:9-5:26)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow in / (15-div-minus-1.c:7:5-7:16)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow in / (15-div-minus-1.c:9:9-9:20)
   [Warning][Integer > DivByZero][CWE-369] Second argument of division might be zero (15-div-minus-1.c:7:5-7:16)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 6

tests/regression/cfg/foo.t/run.t

@@ -60,8 +60,8 @@
                                                         └───────────────────────────────┘
 
   $ goblint --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant", "loop_invariant"]' --set sem.int.signed_overflow assume_none foo.c
-  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (foo.c:4:5-4:8)
-  [Warning][Integer > Overflow][CWE-191] Signed integer underflow (foo.c:5:5-5:8)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow in + (foo.c:4:5-4:8)
+  [Warning][Integer > Overflow][CWE-191] Signed integer underflow in - (foo.c:5:5-5:8)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 6
     dead: 0

tests/regression/cfg/issue-1356.t/run.t

@@ -93,7 +93,7 @@
 
 
   $ goblint --enable ana.sv-comp.functions --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' issue-1356.c
-  [Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (issue-1356.c:11:10-11:15)
+  [Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow in - (issue-1356.c:11:10-11:15)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 13
     dead: 0