Merge pull request #1519 from goblint/imaxabs

Partially support `imaxabs` for SV-COMP

conf/svcomp-validate.json

@@ -10,7 +10,8 @@
       "interval": true
     },
     "float": {
-      "interval": true
+      "interval": true,
+      "evaluate_math_functions": true
     },
     "activated": [
       "base",

conf/svcomp.json

@@ -10,7 +10,8 @@
       "interval": true
     },
     "float": {
-      "interval": true
+      "interval": true,
+      "evaluate_math_functions": true
     },
     "activated": [
       "base",

conf/svcomp24-validate.json

@@ -10,7 +10,8 @@
       "interval": true
     },
     "float": {
-      "interval": true
+      "interval": true,
+      "evaluate_math_functions": true
     },
     "activated": [
       "base",

conf/svcomp24.json

@@ -10,7 +10,8 @@
       "interval": true
     },
     "float": {
-      "interval": true
+      "interval": true,
+      "evaluate_math_functions": true
     },
     "activated": [
       "base",

src/analyses/baseInvariant.ml

@@ -777,33 +777,37 @@ struct
             | _ -> assert false
           end
         | Const _ , _ -> st (* nothing to do *)
-        | CastE ((TFloat (_, _)), e), Float c ->
-          (match unrollType (Cilfacade.typeOf e), FD.get_fkind c with
-           | TFloat (FLongDouble as fk, _), FFloat
-           | TFloat (FDouble as fk, _), FFloat
-           | TFloat (FLongDouble as fk, _), FDouble
-           | TFloat (fk, _), FLongDouble
-           | TFloat (FDouble as fk, _), FDouble
-           | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st
-           | _ -> fallback (fun () -> Pretty.text "CastE: incompatible types") st)
-        | CastE ((TInt (ik, _)) as t, e), Int c
-        | 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 ->
-             (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)
+        | CastE (t, e), c_typed ->
+          begin match Cil.unrollType t, c_typed with
+            | TFloat (_, _), Float c ->
+              (match unrollType (Cilfacade.typeOf e), FD.get_fkind c with
+               | TFloat (FLongDouble as fk, _), FFloat
+               | TFloat (FDouble as fk, _), FFloat
+               | TFloat (FLongDouble as fk, _), FDouble
+               | TFloat (fk, _), FLongDouble
+               | TFloat (FDouble as fk, _), FDouble
+               | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st
+               | _ -> fallback (fun () -> Pretty.text "CastE: incompatible types") st)
+            | (TInt (ik, _) as t), Int c
+            | (TEnum ({ekind = ik; _ }, _) as t), 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 ->
+                 (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)
+            | _, _ -> fallback (fun () -> Pretty.dprintf "CastE: %a not implemented" d_plainexp (CastE (t, e))) st
+          end
         | e, _ -> fallback (fun () -> Pretty.dprintf "%a not implemented" d_plainexp e) st
     in
     if eval_bool exp st = Some (not tv) then contra st (* we already know that the branch is dead *)

src/util/library/libraryFunctions.ml

@@ -6,6 +6,16 @@ open GobConfig
 
 module M = Messages
 
+let intmax_t = lazy (
+  let res = ref None in
+  GoblintCil.iterGlobals !Cilfacade.current_file (function
+      | GType ({tname = "intmax_t"; ttype; _}, _) ->
+        res := Some ttype;
+      | _ -> ()
+    );
+  !res
+)
+
 (** C standard library functions.
     These are specified by the C standard. *)
 let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
@@ -139,7 +149,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("abs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (IInt, j)) });
     ("labs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILong, j)) });
     ("llabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILongLong, j)) });
-    ("imaxabs", unknown [drop "j" []]);
+    ("imaxabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (Cilfacade.get_ikind (Option.get (Lazy.force intmax_t)), j)) });
     ("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]);
     ("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]);
     ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)

tests/regression/39-signed-overflows/11-imaxabs.c

@@ -0,0 +1,24 @@
+//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial
+#include<stdlib.h>
+#include <stdint.h>
+#include <inttypes.h>
+int main() {
+    int64_t data;
+    if (data > (-0x7fffffffffffffff - 1))
+    {
+        if (imaxabs(data) < 100)
+        {
+            __goblint_check(data < 100);
+            __goblint_check(-100 < data);
+            int64_t result = data * data; // NOWARN
+        }
+
+        if(imaxabs(data) <= 100)
+        {
+            __goblint_check(data <= 100);
+            __goblint_check(-100 <= data);
+            int64_t result = data * data; // NOWARN
+        }
+    }
+    return 8;
+}

tests/regression/39-signed-overflows/12-imaxabs-sqrt.c

@@ -0,0 +1,12 @@
+//PARAM: --enable ana.int.interval --enable ana.float.interval --enable ana.float.evaluate_math_functions --set ana.activated[+] tmpSpecial
+#include<math.h>
+#include <stdint.h>
+#include <inttypes.h>
+int main() {
+    int64_t data;
+    if (data > (-0x7fffffffffffffff - 1) && imaxabs((intmax_t)data) <= sqrtl(0x7fffffffffffffffLL))
+    {
+        int64_t result = data * data; // TODO NOWARN
+    }
+    return 8;
+}

tests/regression/39-signed-overflows/13-imaxabs-macos.c

@@ -0,0 +1,25 @@
+//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial
+// 39-signed-overflows/11-imaxabs, but with long long as int64_t instead (https://github.com/goblint/analyzer/pull/1519#issuecomment-2417032186).
+#include<stdlib.h>
+#include <stdint.h>
+#include <inttypes.h>
+int main() {
+    long long data;
+    if (data > (-0x7fffffffffffffff - 1))
+    {
+        if (imaxabs(data) < 100)
+        {
+            __goblint_check(data < 100);
+            __goblint_check(-100 < data);
+            long long result = data * data; // NOWARN
+        }
+
+        if(imaxabs(data) <= 100)
+        {
+            __goblint_check(data <= 100);
+            __goblint_check(-100 <= data);
+            long long result = data * data; // NOWARN
+        }
+    }
+    return 8;
+}