Merge pull request #1411 from goblint/issue_1296_warnings

Add flag `AnalysisState.executing_speculative_computations` to avoid flagging overflows during `invariant`

src/analyses/baseInvariant.ml

@@ -830,4 +830,10 @@ struct
             FD.top_of fk
         in
         inv_exp (Float ftv) exp st
+
+  let invariant ctx st exp tv =
+    (* The computations that happen here are not computations that happen in the programs *)
+    (* Any overflow during the forward evaluation will already have been flagged here *)
+    GobRef.wrap AnalysisState.executing_speculative_computations true
+    @@ fun () -> invariant ctx st exp tv
 end

src/cdomain/value/cdomains/intDomain.ml

@@ -75,18 +75,22 @@ let widening_thresholds_desc = ResettableLazy.from_fun (List.rev % WideningThres
 type overflow_info = { overflow: bool; underflow: bool;}
 
 let set_overflow_flag ~cast ~underflow ~overflow ik =
-  let signed = Cil.isSigned ik in
-  if !AnalysisState.postsolving && signed && not cast then
-    AnalysisState.svcomp_may_overflow := true;
-  let sign = if signed then "Signed" else "Unsigned" 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
-  | true, false ->
-    M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 191] "%s integer underflow" sign
-  | false, true ->
-    M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 190] "%s integer overflow" sign
-  | false, false -> assert false
+  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
+      AnalysisState.svcomp_may_overflow := true;
+    let sign = if signed then "Signed" else "Unsigned" 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
+    | true, false ->
+      M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 191] "%s integer underflow" sign
+    | false, true ->
+      M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 190] "%s integer overflow" sign
+    | false, false -> assert false
 
 let reset_lazy () =
   ResettableLazy.reset widening_thresholds;

src/common/framework/analysisState.ml

@@ -4,6 +4,12 @@
     This is set to true in control.ml before we verify the result (or already before solving if warn = 'early') *)
 let should_warn = ref false
 
+(** If this is true, any overflows happening in IntDomains will not lead to warnings being produced or
+    {!svcomp_may_overflow} being set to true. This is useful when, e.g., {!BaseInvariant.Make.invariant} executes computations that
+    are not in the actual program
+*)
+let executing_speculative_computations = ref false
+
 (** Whether signed overflow or underflow happened *)
 let svcomp_may_overflow = ref false
 

tests/regression/27-inv_invariants/20-warns-unsigned.c

@@ -19,4 +19,22 @@ int main() {
     __goblint_check(i <= 8);
     i = 8;
   }
+
+  length = 20;
+  unsigned int blub = 5;
+
+  if(top) {
+    blub = 10;
+  }
+
+  for (int i1 = 0; i1 < length; i1++) {
+    // Previously, we would warn as the inverse would make a substraction that becomes negative and is
+    // outside the range of unsigned int.
+    if (i1 < blub + 3) //NOWARN
+    {
+
+    }
+  }
+  return 0;
+
 }

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

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