diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 5c1b8223b6..4cf4f11be2 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -798,7 +798,9 @@ struct | TInt(ik_e, _) | TEnum ({ekind = ik_e; _ }, _) -> (* let c' = ID.cast_to ik_e c in *) - let c' = ID.cast_to ik_e (ID.meet c (ID.cast_to ik (ID.top_of ik_e))) in (* TODO: cast without overflow, is this right for normal invariant? *) + (* 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 diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index e79bc86bef..6c67279044 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -179,7 +179,7 @@ sig val maximal : t -> int_t option val minimal : t -> int_t option - val cast_to: ?torg:Cil.typ -> Cil.ikind -> t -> t + val cast_to: ?suppress_ovwarn:bool -> ?torg:Cil.typ -> Cil.ikind -> t -> t end (** Interface of IntDomain implementations that do not take ikinds for arithmetic operations yet. TODO: Should be ported to S in the future. *) @@ -208,7 +208,7 @@ sig val mul : ?no_ov:bool -> Cil.ikind -> t -> t -> t val div : ?no_ov:bool -> Cil.ikind -> t -> t -> t val neg : ?no_ov:bool -> Cil.ikind -> t -> t - val cast_to : ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t + val cast_to : ?suppress_ovwarn:bool -> ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t val join: Cil.ikind -> t -> t -> t val meet: Cil.ikind -> t -> t -> t @@ -247,7 +247,7 @@ sig val neg : ?no_ov:bool -> Cil.ikind -> t -> t * overflow_info - val cast_to : ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t * overflow_info + val cast_to : ?suppress_ovwarn:bool -> ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t * overflow_info val of_int : Cil.ikind -> int_t -> t * overflow_info @@ -375,7 +375,7 @@ struct let c_logand = lift2 I.c_logand let c_logor = lift2 I.c_logor - let cast_to ?torg ikind x = {v = I.cast_to ~torg:(TInt(x.ikind,[])) ikind x.v; ikind} + let cast_to ?(suppress_ovwarn=false) ?torg ikind x = {v = I.cast_to ~suppress_ovwarn ~torg:(TInt(x.ikind,[])) ikind x.v; ikind} let is_top_of ik x = ik = x.ikind && I.is_top_of ik x.v @@ -656,7 +656,7 @@ struct let maximal = function None -> None | Some (x,y) -> Some y let minimal = function None -> None | Some (x,y) -> Some x - let cast_to ?torg ?no_ov t = norm ~cast:true t (* norm does all overflow handling *) + let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov t = norm ~cast:true t (* norm does all overflow handling *) let widen ik x y = match x, y with @@ -1358,7 +1358,7 @@ struct in binop x y interval_rem - let cast_to ?torg ?no_ov ik x = norm_intvs ~cast:true ik x + let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov ik x = norm_intvs ~cast:true ik x (* narrows down the extremeties of xs if they are equal to boundary values of the ikind with (possibly) narrower values from ys @@ -1542,7 +1542,7 @@ module SOverflowUnlifter (D : SOverflow) : S with type int_t = D.int_t and type let neg ?no_ov ik x = fst @@ D.neg ?no_ov ik x - let cast_to ?torg ?no_ov ik x = fst @@ D.cast_to ?torg ?no_ov ik x + let cast_to ?suppress_ovwarn ?torg ?no_ov ik x = fst @@ D.cast_to ?suppress_ovwarn ?torg ?no_ov ik x let of_int ik x = fst @@ D.of_int ik x @@ -1612,7 +1612,7 @@ struct let c_lognot n1 = of_bool (not (to_bool' n1)) let c_logand n1 n2 = of_bool ((to_bool' n1) && (to_bool' n2)) let c_logor n1 n2 = of_bool ((to_bool' n1) || (to_bool' n2)) - let cast_to ?torg t x = failwith @@ "Cast_to not implemented for " ^ (name ()) ^ "." + let cast_to ?(suppress_ovwarn=false) ?torg t x = failwith @@ "Cast_to not implemented for " ^ (name ()) ^ "." let arbitrary ik = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 (* TODO: use ikind *) let invariant _ _ = Invariant.none (* TODO *) end @@ -1642,7 +1642,7 @@ struct let name () = "flat integers" - let cast_to ?torg t = function + let cast_to ?(suppress_ovwarn=false) ?torg t = function | `Lifted x -> `Lifted (Base.cast_to t x) | x -> x @@ -1722,7 +1722,7 @@ struct include StdTop (struct type nonrec t = t let top_of = top_of end) let name () = "lifted integers" - let cast_to ?torg t = function + let cast_to ?(suppress_ovwarn=false) ?torg t = function | `Lifted x -> `Lifted (Base.cast_to t x) | x -> x @@ -1907,7 +1907,7 @@ struct | `Excluded (s,r) -> if S.mem i s then `Neq else `Top let top_of ik = `Excluded (S.empty (), size ik) - let cast_to ?torg ?no_ov ik = function + let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov ik = function | `Excluded (s,r) -> let r' = size ik in if R.leq r r' then (* upcast -> no change *) @@ -2347,7 +2347,7 @@ struct let is_top x = x (* override Std *) let equal_to i x = if x then `Top else failwith "unsupported: equal_to with bottom" - let cast_to ?torg _ x = x (* ok since there's no smaller ikind to cast to *) + let cast_to ?(suppress_ovwarn=false) ?torg _ x = x (* ok since there's no smaller ikind to cast to *) let leq x y = not x || y let join = (||) @@ -2471,7 +2471,7 @@ module Enums : S with type int_t = Z.t = struct if BISet.mem i x then `Neq else `Top - let cast_to ?torg ?no_ov ik v = norm ik @@ match v with + let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov ik v = norm ik @@ match v with | Exc (s,r) -> let r' = size ik in if R.leq r r' then (* upcast -> no change *) @@ -2892,7 +2892,7 @@ struct | _ -> None (* cast from original type to ikind, set to top if the value doesn't fit into the new type *) - let cast_to ?torg ?(no_ov=false) t x = + let cast_to ?(suppress_ovwarn=false) ?torg ?(no_ov=false) t x = match x with | None -> None | Some (c, m) when m =: Z.zero -> @@ -2916,7 +2916,7 @@ struct | _ -> top () - let cast_to ?torg ?no_ov (t : Cil.ikind) x = + let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov (t : Cil.ikind) x = let pretty_bool _ x = Pretty.text (string_of_bool x) in let res = cast_to ?torg ?no_ov t x in if M.tracing then M.trace "cong-cast" "Cast %a to %a (no_ov: %a) = %a" pretty x Cil.d_ikind t (Pretty.docOpt (pretty_bool ())) no_ov pretty res; @@ -3258,7 +3258,7 @@ module SOverflowLifter (D : S) : SOverflow with type int_t = D.int_t and type t let neg ?no_ov ik x = lift @@ D.neg ?no_ov ik x - let cast_to ?torg ?no_ov ik x = lift @@ D.cast_to ?torg ?no_ov ik x + let cast_to ?suppress_ovwarn ?torg ?no_ov ik x = lift @@ D.cast_to ?suppress_ovwarn ?torg ?no_ov ik x let of_int ik x = lift @@ D.of_int ik x @@ -3329,9 +3329,9 @@ module IntDomTupleImpl = struct | Some(_, {underflow; overflow}) -> not (underflow || overflow) | _ -> false - let check_ov ~cast ik intv intv_set = + let check_ov ?(suppress_ovwarn = false) ~cast ik intv intv_set = let no_ov = (no_overflow ik intv) || (no_overflow ik intv_set) in - if not no_ov && ( BatOption.is_some intv || BatOption.is_some intv_set) then ( + if not no_ov && not suppress_ovwarn && ( BatOption.is_some intv || BatOption.is_some intv_set) 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_intv && underflow_intv_set in @@ -3540,11 +3540,11 @@ module IntDomTupleImpl = struct (* map with overflow check *) - let mapovc ?(cast=false) ik r (a, b, c, d, e) = + let mapovc ?(suppress_ovwarn=false) ?(cast=false) ik r (a, b, c, d, e) = 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 no_ov = check_ov ~cast ik intv intv_set in + let no_ov = check_ov ~suppress_ovwarn ~cast ik intv intv_set 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 @@ -3596,8 +3596,8 @@ module IntDomTupleImpl = struct let c_lognot ik = map ik {f1 = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.c_lognot ik)} - let cast_to ?torg ?no_ov t = - mapovc ~cast:true t {f1_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.cast_to ?torg ?no_ov t)} + 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)} (* fp: projections *) let equal_to i x = diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli index 63aa47d868..ca64692290 100644 --- a/src/cdomain/value/cdomains/intDomain.mli +++ b/src/cdomain/value/cdomains/intDomain.mli @@ -204,7 +204,7 @@ sig (** {b Cast} *) - val cast_to: ?torg:Cil.typ -> Cil.ikind -> t -> t + val cast_to: ?suppress_ovwarn:bool -> ?torg:Cil.typ -> Cil.ikind -> t -> t (** Cast from original type [torg] to integer type [Cil.ikind]. Currently, [torg] is only present for actual casts. The function is also called to handle overflows/wrap around after operations. In these cases (where the type stays the same) [torg] is None. *) end @@ -244,7 +244,7 @@ sig val mul : ?no_ov:bool -> Cil.ikind -> t -> t -> t val div : ?no_ov:bool -> Cil.ikind -> t -> t -> t val neg : ?no_ov:bool -> Cil.ikind -> t -> t - val cast_to : ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t + val cast_to : ?suppress_ovwarn:bool -> ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t (** @param no_ov If true, assume no overflow can occur. *) val join: Cil.ikind -> t -> t -> t @@ -290,7 +290,7 @@ sig val neg : ?no_ov:bool -> Cil.ikind -> t -> t * overflow_info - val cast_to : ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t * overflow_info + val cast_to : ?suppress_ovwarn:bool -> ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t * overflow_info val of_int : Cil.ikind -> int_t -> t * overflow_info diff --git a/tests/regression/27-inv_invariants/20-warns-unsigned.c b/tests/regression/27-inv_invariants/20-warns-unsigned.c new file mode 100644 index 0000000000..25da5e1ada --- /dev/null +++ b/tests/regression/27-inv_invariants/20-warns-unsigned.c @@ -0,0 +1,22 @@ +// PARAM: --enable ana.int.interval +#include +#include +#include + + +int main() { + unsigned int length = 5; + int i = 0; + int top; + + if(top) { + i = 10; + } + + // Previously, we would warn as invariant internally casts an artificially created top between types. + if(i < length + 3) //NOWARN + { + __goblint_check(i <= 8); + i = 8; + } +}