Merge remote-tracking branch 'upstream/master'

src/analyses/base.ml

@@ -755,7 +755,7 @@ struct
       let te1 = Cilfacade.typeOf e1 in
       let te2 = Cilfacade.typeOf e2 in
       let both_arith_type = isArithmeticType te1 && isArithmeticType te2 in
-      let is_safe = (extra_is_safe || VD.is_safe_cast t1 te1 && VD.is_safe_cast t2 te2) && not both_arith_type in
+      let is_safe = (extra_is_safe || VD.is_statically_safe_cast t1 te1 && VD.is_statically_safe_cast t2 te2) && not both_arith_type in
       if M.tracing then M.tracel "cast" "remove cast on both sides for %a? -> %b" d_exp exp is_safe;
       if is_safe then ( (* we can ignore the casts if the casts can't change the value *)
         let e1 = if isArithmeticType te1 then c1 else e1 in
@@ -1264,6 +1264,26 @@ struct
     let res = match Cilfacade.get_ikind_exp exp with
       | exception _ -> BoolDomain.MayBool.top ()
       | ik ->
+        let checkDiv e1 e2 =
+          let binop = (GobOption.map2 Z.div )in
+          match ctx.ask (EvalInt e1), ctx.ask (EvalInt e2) with
+          | `Bot, _ -> false
+          | _, `Bot -> false
+          | `Lifted i1, `Lifted i2 ->
+            ( let divisor_contains_zero = (ID.is_bot @@ ID.meet i2 (ID.of_int ik Z.zero))  in
+              if divisor_contains_zero then true else 
+                ( let (min_ik, max_ik) = IntDomain.Size.range ik in
+                  let (min_i1, max_i1) = (IntDomain.IntDomTuple.minimal i1, IntDomain.IntDomTuple.maximal i1) in
+                  let (min_i2, max_i2) = (IntDomain.IntDomTuple.minimal i2, IntDomain.IntDomTuple.maximal i2) in
+                  let (min_i2, max_i2) = (Option.map (fun x -> if (Z.zero=x) then Z.one else x) min_i2,
+                                          Option.map (fun x -> if (Z.zero=x) then Z.neg Z.one else x) max_i2) in
+                  let possible_combinations = [binop min_i1 min_i2; binop  min_i1 max_i2; binop max_i1 min_i2; binop max_i1 max_i2] in
+                  let min_exp = List.min possible_combinations in
+                  let max_exp = List.max possible_combinations in
+                  match min_exp, max_exp with
+                  | Some min, Some max when min >= min_ik && max <= max_ik -> false
+                  | _ -> true ))
+          | _   -> true in
         let checkBinop e1 e2 binop =
           match ctx.ask (EvalInt e1), ctx.ask (EvalInt e2) with
           | `Bot, _ -> false
@@ -1317,7 +1337,7 @@ struct
               | PlusA|PlusPI|IndexPI -> checkBinop e1 e2 (GobOption.map2 Z.(+))
               | MinusA|MinusPI|MinusPP -> checkBinop e1 e2 (GobOption.map2 Z.(-))
               | Mult -> checkBinop e1 e2 (GobOption.map2 Z.mul)
-              | Div -> checkBinop e1 e2 (GobOption.map2 Z.div)
+              | Div -> checkDiv e1 e2
               | Mod -> (* an overflow happens when the second operand is negative *)
                 checkPredicate e2 (fun interval_bound _ -> Z.gt interval_bound Z.zero)
               (* operations that do not result in overflow in C: *)

src/analyses/baseInvariant.ml

@@ -205,15 +205,12 @@ struct
       (* Since we handle not only equalities, the order is important *)
       | BinOp(op, Lval x, rval, typ) -> helper op x (VD.cast (Cilfacade.typeOfLval x) (eval_rv ~ctx st rval)) tv
       | BinOp(op, rval, Lval x, typ) -> derived_invariant (BinOp(switchedOp op, Lval x, rval, typ)) tv
-      | BinOp(op, CastE (t1, c1), CastE (t2, c2), t) when (op = Eq || op = Ne) && typeSig t1 = typeSig t2 && VD.is_safe_cast t1 (Cilfacade.typeOf c1) && VD.is_safe_cast t2 (Cilfacade.typeOf c2)
+      | BinOp(op, CastE (t1, c1), CastE (t2, c2), t) when (op = Eq || op = Ne) && typeSig t1 = typeSig t2 && VD.is_statically_safe_cast t1 (Cilfacade.typeOf c1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf c2)
         -> derived_invariant (BinOp (op, c1, c2, t)) tv
       | BinOp(op, CastE (TInt (ik, _) as t1, Lval x), rval, typ) ->
         begin match eval_rv ~ctx st (Lval x) with
           | Int v ->
-            (* This is tricky: It it is not sufficient to check that ID.cast_to_ik v = v
-               If there is one domain that knows this to be true and the other does not, we
-               should still impose the invariant. E.g. i -> ([1,5]; Not {0}[byte]) *)
-            if VD.is_safe_cast t1 (Cilfacade.typeOfLval x) then
+            if VD.is_dynamically_safe_cast t1 (Cilfacade.typeOfLval x) (Int v) then
               derived_invariant (BinOp (op, Lval x, rval, typ)) tv
             else
               `NotUnderstood
@@ -591,16 +588,16 @@ struct
           )
         | UnOp (Neg, e, _), Float c -> inv_exp (unop_FD Neg c) e st
         | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp (Int (unop_ID op c)) e st
-        (* no equivalent for Float, as VD.is_safe_cast fails for all float types anyways *)
-        | BinOp((Eq | Ne) as op, CastE (t1, e1), CastE (t2, e2), t), Int c when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_safe_cast t2 (Cilfacade.typeOf e2) ->
+        (* no equivalent for Float, as VD.is_statically_safe_cast fails for all float types anyways *)
+        | BinOp((Eq | Ne) as op, CastE (t1, e1), CastE (t2, e2), t), Int c when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_statically_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf e2) ->
           inv_exp (Int c) (BinOp (op, e1, e2, t)) st
         | BinOp (LOr, arg1, arg2, typ) as exp, Int c ->
           (* copied & modified from eval_rv_base... *)
           let (let*) = Option.bind in
           (* split nested LOr Eqs to equality pairs, if possible *)
           let rec split = function
             (* copied from above to support pointer equalities with implicit casts inserted *)
-            | BinOp (Eq, CastE (t1, e1), CastE (t2, e2), typ) when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_safe_cast t2 (Cilfacade.typeOf e2) -> (* slightly different from eval_rv_base... *)
+            | BinOp (Eq, CastE (t1, e1), CastE (t2, e2), typ) when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_statically_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf e2) -> (* slightly different from eval_rv_base... *)
               Some [(e1, e2)]
             | BinOp (Eq, arg1, arg2, _) ->
               Some [(arg1, arg2)]
@@ -793,19 +790,19 @@ struct
         | CastE ((TEnum ({ekind = ik; _ }, _)) as t, e), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *)
           (match eval e st with
            | Int i ->
-             if ID.leq i (ID.cast_to ik i) then
-               match unrollType (Cilfacade.typeOf e) with
-               | TInt(ik_e, _)
-               | TEnum ({ekind = ik_e; _ }, _) ->
-                 (* let c' = ID.cast_to ik_e c in *)
-                 (* Suppressing overflow warnings as this is not a computation that comes from the program *)
-                 let res_range = (ID.cast_to ~suppress_ovwarn:true ik (ID.top_of ik_e)) in
-                 let c' = ID.cast_to ik_e (ID.meet c res_range) in (* TODO: cast without overflow, is this right for normal invariant? *)
-                 if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c';
-                 inv_exp (Int c') e st
-               | x -> fallback (fun () -> Pretty.dprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st
-             else
-               fallback (fun () -> Pretty.dprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st
+             (match unrollType (Cilfacade.typeOf e) with
+              | (TInt(ik_e, _) as t')
+              | (TEnum ({ekind = ik_e; _ }, _) as t') ->
+                if VD.is_dynamically_safe_cast t t' (Int i) then
+                  (* let c' = ID.cast_to ik_e c in *)
+                  (* Suppressing overflow warnings as this is not a computation that comes from the program *)
+                  let res_range = (ID.cast_to ~suppress_ovwarn:true ik (ID.top_of ik_e)) in
+                  let c' = ID.cast_to ik_e (ID.meet c res_range) in (* TODO: cast without overflow, is this right for normal invariant? *)
+                  if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c';
+                  inv_exp (Int c') e st
+                else
+                  fallback (fun () -> Pretty.dprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st
+              | x -> fallback (fun () -> Pretty.dprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st)
            | v -> fallback (fun () -> Pretty.dprintf "CastE: e did not evaluate to Int, but %a" VD.pretty v) st)
         | e, _ -> fallback (fun () -> Pretty.dprintf "%a not implemented" d_plainexp e) st
     in
@@ -833,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;
@@ -2063,7 +2067,6 @@ struct
     | _ -> None
 
   let from_excl ikind (s: S.t) = norm ikind @@ `Excluded (s, size ikind)
-  let not_zero ikind = from_excl ikind (S.singleton Z.zero)
 
   let of_bool_cmp ik x = of_int ik (if x then Z.one else Z.zero)
   let of_bool = of_bool_cmp

src/cdomain/value/cdomains/valueDomain.ml

@@ -24,7 +24,8 @@ sig
   val affecting_vars: t -> varinfo list
   val invalidate_value: VDQ.t -> typ -> t -> t
   val invalidate_abstract_value: t -> t
-  val is_safe_cast: typ -> typ -> bool
+  val is_statically_safe_cast: typ -> typ -> bool
+  val is_dynamically_safe_cast: typ -> typ -> t -> bool
   val cast: ?torg:typ -> typ -> t -> t
   val smart_join: (exp -> Z.t option) -> (exp -> Z.t option) -> t -> t ->  t
   val smart_widen: (exp -> Z.t option) -> (exp -> Z.t option) ->  t -> t -> t
@@ -334,8 +335,8 @@ struct
    * Functions for getting state out of a compound:
    ************************************************************)
 
-  (* is a cast t1 to t2 invertible, i.e., content-preserving? TODO also use abstract value? *)
-  let is_safe_cast t2 t1 = match t2, t1 with
+  (* is a cast t1 to t2 invertible, i.e., content-preserving in general? *)
+  let is_statically_safe_cast t2 t1 = match t2, t1 with
     (*| TPtr _, t -> bitsSizeOf t <= bitsSizeOf !upointType
       | t, TPtr _ -> bitsSizeOf t >= bitsSizeOf !upointType*)
     | TFloat (fk1,_), TFloat (fk2,_) when fk1 = fk2 -> true
@@ -353,6 +354,21 @@ struct
       IntDomain.Size.is_cast_injective ~from_type:t1 ~to_type:t2 && bitsSizeOf t2 >= bitsSizeOf t1
     | _ -> false
 
+  (* is a cast t1 to t2 invertible, i.e., content-preserving for the given value of v? *)
+  let is_dynamically_safe_cast t2 t1 v =
+    if is_statically_safe_cast t2 t1 then
+      true
+    else
+      match t2, t1, v with
+      | (TInt (ik2,_) | TEnum ({ekind=ik2; _},_)) , (TInt (ik1,_) | TEnum ({ekind=ik1; _},_)), Int v ->
+        let cl, cu = IntDomain.Size.range ik2 in
+        let l, u = ID.minimal v, ID.maximal v in
+        (match l, u with
+         | Some l, Some u when Z.leq cl l && Z.leq u cu -> true
+         | _ -> false)
+      | _ -> false
+
+
   exception CastError of string
 
   let typ_eq t1 t2 = match typeSig t1, typeSig t2 with

src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml

@@ -19,7 +19,7 @@ module Mpqf = SharedFunctions.Mpqf
 module Equality = struct
   (* (Some i, k) represents a sum of a variable with index i and the number k.
      (None, k) represents the number k. *)
-  type t = (int option * (Z.t [@printer Z.pp_print])) [@@deriving eq, ord, hash, show]
+  type t = (int option * GobZ.t) [@@deriving eq, ord, hash, show]
   let zero = (None, Z.zero)
   let var_zero i = (Some i, Z.zero)
   let to_int x = Z.to_int @@ snd x

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
 

src/util/std/gobZ.ml

@@ -1,4 +1,4 @@
-type t = Z.t
+type t = Z.t [@@deriving eq, ord, hash]
 
 let to_yojson z =
   `Intlit (Z.to_string z)
@@ -10,3 +10,5 @@ let rec for_all_range f (a, b) =
     f a && for_all_range f (Z.succ a, b)
 
 let pretty () x = GoblintCil.Pretty.text (Z.to_string x)
+
+let pp = Z.pp_print

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/27-inv_invariants/21-unsigned.c

@@ -0,0 +1,18 @@
+//PARAM:  --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <time.h>
+
+
+int main() {
+   int i = 0;
+   unsigned int length = 5;
+
+   while(i < length) {
+      i = i+1;
+   }
+
+   __goblint_check(i == 5);
+
+   return 0;
+}

tests/regression/77-lin2vareq/32-divbzero-in-overflow.c

@@ -0,0 +1,16 @@
+// SKIP PARAM: --set ana.activated[+] lin2vareq
+
+/**
+ * This test shows an instance where MaySignedOverflow raised
+ * an uncaught division by zero in the treatment of main's sole statement
+ * 
+ * Fixed in #1419
+ */
+int a;
+char b;
+int main()
+{
+     0 == a && 1 / b;
+    __goblint_check(1); // (reachable)
+    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