From 0e7a2e9415e16f217ccf0568860612ce5a0763ae Mon Sep 17 00:00:00 2001
From: Alina Weber <alina.weber@aisec.fraunhofer.de>
Date: Thu, 1 Feb 2024 13:09:34 +0100
Subject: [PATCH] unfinished adjustment of maySignedOverflow

---
 src/analyses/base.ml                          | 72 +++++++++++--------
 .../77-lin2vareq/28-narrowing-on-steroids.c   |  2 +-
 2 files changed, 42 insertions(+), 32 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 35a80bad5b..e9b257893b 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1233,36 +1233,46 @@ struct
       Invariant.none
 
   let rec exp_may_signed_overflow ctx exp =
-    match Cilfacade.get_ikind_exp exp with
-    | exception _ -> BoolDomain.MayBool.top ()
-    | ik ->
-      let exp_is_top = match eval_rv_ask_evalint ~ctx:ctx ctx.local exp with
-        | Int i ->Queries.ID.is_top_of ik (`Lifted i)
-        | _   -> true
-        | exception (IntDomain.ArithmeticOnIntegerBot _) -> true in
-      match exp with
-      | Const _
-      | SizeOf _
-      | SizeOfStr _
-      | AlignOf _
-      | AddrOfLabel _ -> false
-      | Real e
-      | Imag e
-      | SizeOfE e
-      | AlignOfE e
-      | CastE (_, e) -> exp_may_signed_overflow ctx e
-      | UnOp (_, e, _) ->
-        if Cil.isSigned ik && exp_is_top then true
-        (** if EvalInt returns top, there was probably an overflow.
-                Otherwise, to be sure that there is no overflow, we need to check each subexpression *)
-        else exp_may_signed_overflow ctx e
-      | BinOp (_, e1, e2, _) -> if Cil.isSigned ik && exp_is_top then true else
-          exp_may_signed_overflow ctx e1 || exp_may_signed_overflow ctx e2
-      | Question (e1, e2, e3, _) ->
-        exp_may_signed_overflow ctx e1 || exp_may_signed_overflow ctx e2 || exp_may_signed_overflow ctx e3
-      | Lval lval
-      | AddrOf lval
-      | StartOf lval -> lval_may_signed_overflow ctx lval
+    let res = match Cilfacade.get_ikind_exp exp with
+      | exception _ -> BoolDomain.MayBool.top ()
+      | ik ->
+        let check e =  
+          let res = match (Analyses.ask_of_ctx ctx).f (EvalInt e) with
+            | `Bot -> true (* TODO AWE: Throw exception? But which one? This should never happen according to Michael Schwarz *)
+            | `Lifted i -> if Queries.ID.is_top_of ik (`Lifted i) then true 
+              else (
+                let (minimal, maximal) = IntDomain.Size.range ik in
+                match IntDomain.IntDomTuple.minimal i, IntDomain.IntDomTuple.maximal i with
+                | Some min, Some max when  min > minimal && max < maximal -> false
+                | _ -> true )
+            | _   -> true in
+          if M.tracing then M.trace "signed_overflow" "may_signed_overflow-check: %a. Result = %b\n" d_plainexp e res; res
+        in
+        match exp with
+        | Const _
+        | SizeOf _
+        | SizeOfStr _
+        | AlignOf _
+        | AddrOfLabel _ -> false
+        | Real e
+        | Imag e
+        | SizeOfE e
+        | AlignOfE e
+        | CastE (_, e) -> exp_may_signed_overflow ctx e
+        | UnOp (_, e, _) ->
+          if Cil.isSigned ik && check exp then true
+          (** if EvalInt returns top, there was probably an overflow.
+                  Otherwise, to be sure that there is no overflow, we need to check each subexpression *)
+          else exp_may_signed_overflow ctx e
+        | BinOp (_, e1, e2, _) -> 
+          check e1 || check e2 ||exp_may_signed_overflow ctx e1 || exp_may_signed_overflow ctx e2 || (Cil.isSigned ik && check exp)
+        | Question (e1, e2, e3, _) ->
+          exp_may_signed_overflow ctx e1 || exp_may_signed_overflow ctx e2 || exp_may_signed_overflow ctx e3
+        | Lval lval
+        | AddrOf lval
+        | StartOf lval -> lval_may_signed_overflow ctx lval
+    in
+    if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b\n" d_plainexp exp res; res
   and lval_may_signed_overflow ctx (lval : lval) =
     let (host, offset) = lval in
     let host_may_signed_overflow = function
@@ -1442,7 +1452,7 @@ struct
       let g: V.t = Obj.obj g in
       query_invariant_global ctx g
     | Q.MaySignedOverflow e -> (let res = exp_may_signed_overflow ctx e in
-                                if M.tracing then M.traceli "signed_overflow" "base exp_may_signed_overflow %a. Result = %b\n" d_plainexp e res; res
+                                if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b\n" d_plainexp e res; res
                                )
     | _ -> Q.Result.top q
 
diff --git a/tests/regression/77-lin2vareq/28-narrowing-on-steroids.c b/tests/regression/77-lin2vareq/28-narrowing-on-steroids.c
index d2017086d9..0548021b92 100644
--- a/tests/regression/77-lin2vareq/28-narrowing-on-steroids.c
+++ b/tests/regression/77-lin2vareq/28-narrowing-on-steroids.c
@@ -2,7 +2,7 @@
 #include <assert.h>
 
 int main() {
-  int a;
+  short a;
   a = a % 10;
   int b;
   int c;