From b2ab5f4460ed2c47e68b3820749886e0aeafd503 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 11 Nov 2021 13:58:22 +0200 Subject: [PATCH 1/3] Add tests where assume_none for signed_overflow is unsound --- .../39-signed-overflows/03-cast-return-void-ptr.c | 15 +++++++++++++++ .../04-cast-unsigned-to-signed.c | 9 +++++++++ 2 files changed, 24 insertions(+) create mode 100644 tests/regression/39-signed-overflows/03-cast-return-void-ptr.c create mode 100644 tests/regression/39-signed-overflows/04-cast-unsigned-to-signed.c diff --git a/tests/regression/39-signed-overflows/03-cast-return-void-ptr.c b/tests/regression/39-signed-overflows/03-cast-return-void-ptr.c new file mode 100644 index 0000000000..463a6f8359 --- /dev/null +++ b/tests/regression/39-signed-overflows/03-cast-return-void-ptr.c @@ -0,0 +1,15 @@ +// PARAM: --enable ana.int.interval --set sem.int.signed_overflow assume_none +#include + +int empty() { + return -1; // return shouldn't cast to void* generally, but just for thread return +} + +int main(void) { + if (!empty()==-1) { // if -1 is cast to void*, it makes both branches dead! + assert(1); // NOWARN (unreachable) + } + + assert(1); // reachable + return 0; +} diff --git a/tests/regression/39-signed-overflows/04-cast-unsigned-to-signed.c b/tests/regression/39-signed-overflows/04-cast-unsigned-to-signed.c new file mode 100644 index 0000000000..63f1f8ef30 --- /dev/null +++ b/tests/regression/39-signed-overflows/04-cast-unsigned-to-signed.c @@ -0,0 +1,9 @@ +// PARAM: --enable ana.int.interval --set sem.int.signed_overflow assume_none +#include + +int main(void) { + unsigned long x; + long y = x; + assert(y >= 0); // UNKNOWN! + return 0; +} From 827a52783da341c85c0fc4985b05b1d5e1b068fb Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 10 Nov 2021 14:55:11 +0200 Subject: [PATCH 2/3] Fix base return cast regression from #225 Only thread return value needs to be case, but not the function return value. --- src/analyses/base.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index c9fd4c504f..dd95ce9c59 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1826,12 +1826,14 @@ struct | TVoid _ -> M.warn "Returning a value from a void function"; assert false | ret -> ret in - (* Evaluate exp and cast the resulting value to the void-pointer-type. - Casting to the right type here avoids precision loss on joins. *) - let rv = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp |> VD.cast ~torg:(Cilfacade.typeOf exp) Cil.voidPtrType in + let rv = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp in let nst: store = match ThreadId.get_current (Analyses.ask_of_ctx ctx) with - | `Lifted tid when ThreadReturn.is_current (Analyses.ask_of_ctx ctx) -> { nst with cpa = CPA.add (ThreadIdDomain.Thread.to_varinfo tid) rv nst.cpa} + | `Lifted tid when ThreadReturn.is_current (Analyses.ask_of_ctx ctx) -> + (* Evaluate exp and cast the resulting value to the void-pointer-type. + Casting to the right type here avoids precision loss on joins. *) + let rv = VD.cast ~torg:(Cilfacade.typeOf exp) Cil.voidPtrType rv in + { nst with cpa = CPA.add (ThreadIdDomain.Thread.to_varinfo tid) rv nst.cpa} | _ -> nst in set ~ctx:(Some ctx) ~t_override (Analyses.ask_of_ctx ctx) ctx.global nst (return_var ()) t_override rv From 86dea61c911138e6bfd7844f0850fefd601bb24c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 11 Nov 2021 14:14:08 +0200 Subject: [PATCH 3/3] Fix unsound cast handling with assume_none Casts are conversions where signed overflow is not actually undefined behavior. --- src/cdomains/intDomain.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml index 5c5f7b9189..40e675ac5e 100644 --- a/src/cdomains/intDomain.ml +++ b/src/cdomains/intDomain.ml @@ -531,9 +531,9 @@ struct | Some (a, b) -> if a = b && b = i then `Eq else if Ints_t.compare a i <= 0 && Ints_t.compare i b <=0 then `Top else `Neq - let set_overflow_flag ~underflow ~overflow ik = + let set_overflow_flag ~cast ~underflow ~overflow ik = let signed = Cil.isSigned ik in - if !GU.postsolving && signed then + if !GU.postsolving && signed && not cast then Goblintutil.svcomp_may_overflow := true; let sign = if signed then "Signed" else "Unsigned" in @@ -546,7 +546,7 @@ struct M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 190] "%s integer overflow" sign | false, false -> assert false - let norm ik = function None -> None | Some (x,y) -> + let norm ?(cast=false) ik = function None -> None | Some (x,y) -> if Ints_t.compare x y > 0 then None else ( let min_ik = min_int ik in @@ -554,8 +554,8 @@ struct let underflow = Ints_t.compare min_ik x > 0 in let overflow = Ints_t.compare max_ik y < 0 in if underflow || overflow then ( - set_overflow_flag ~underflow ~overflow ik; - if should_wrap ik then + set_overflow_flag ~cast ~underflow ~overflow ik; + if should_wrap ik then (* could add [|| cast], but that's GCC implementation-defined behavior: https://gcc.gnu.org/onlinedocs/gcc/Integers-implementation.html#Integers-implementation *) (* We can only soundly wrap if at most one overflow occurred, otherwise the minimal and maximal values of the interval *) (* on Z will not safely contain the minimal and maximal elements after the cast *) let diff = Ints_t.abs (Ints_t.sub max_ik min_ik) in @@ -570,7 +570,7 @@ struct else (* Interval that wraps around (begins to the right of its end). We can not represent such intervals *) top_of ik - else if should_ignore_overflow ik then + else if not cast && should_ignore_overflow ik then let tl, tu = BatOption.get @@ top_of ik in Some (max tl x, min tu y) else @@ -630,7 +630,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 t (* norm does all overflow handling *) + let cast_to ?torg ?no_ov t = norm ~cast:true t (* norm does all overflow handling *) let widen ik x y = match x, y with @@ -694,7 +694,7 @@ struct | _ -> match to_int i1, to_int i2 with | Some x, Some y -> (try norm ik (of_int ik (f ik x y)) with Division_by_zero | Invalid_argument _ -> top_of ik) - | _ -> (set_overflow_flag ~underflow:true ~overflow:true ik; top_of ik) + | _ -> (set_overflow_flag ~cast:false ~underflow:true ~overflow:true ik; top_of ik) let bitxor = bit (fun _ik -> Ints_t.bitxor) let bitand = bit (fun _ik -> Ints_t.bitand)