Partially support imaxabs for SV-COMP

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

@@ -785,7 +785,8 @@ struct
            | 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, _), _ -> inv_exp (Int (FD.to_int ik c)) e st (* TODO: is this cast refinement correct? *)
+           | t, fk -> fallback (fun () -> Pretty.dprintf "CastE: incompatible types %a and %a" CilType.Typ.pretty t CilType.Fkind.pretty fk) 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

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; // NOWARN
+    }
+    return 8;
+}