diff --git a/conf/svcomp-validate.json b/conf/svcomp-validate.json index 8e11fee7f5..f0e99057d1 100644 --- a/conf/svcomp-validate.json +++ b/conf/svcomp-validate.json @@ -10,7 +10,8 @@ "interval": true }, "float": { - "interval": true + "interval": true, + "evaluate_math_functions": true }, "activated": [ "base", diff --git a/conf/svcomp.json b/conf/svcomp.json index 12740a00ce..7b8d58e790 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -10,7 +10,8 @@ "interval": true }, "float": { - "interval": true + "interval": true, + "evaluate_math_functions": true }, "activated": [ "base", diff --git a/conf/svcomp24-validate.json b/conf/svcomp24-validate.json index 7832ffa6af..d83b1767a4 100644 --- a/conf/svcomp24-validate.json +++ b/conf/svcomp24-validate.json @@ -10,7 +10,8 @@ "interval": true }, "float": { - "interval": true + "interval": true, + "evaluate_math_functions": true }, "activated": [ "base", diff --git a/conf/svcomp24.json b/conf/svcomp24.json index 7e30554ceb..1c60f84920 100644 --- a/conf/svcomp24.json +++ b/conf/svcomp24.json @@ -10,7 +10,8 @@ "interval": true }, "float": { - "interval": true + "interval": true, + "evaluate_math_functions": true }, "activated": [ "base", diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 51a27e19f8..52f0888d3f 100644 --- a/src/analyses/baseInvariant.ml +++ b/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 *) diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index 25a90da2d3..979876729d 100644 --- a/src/util/library/libraryFunctions.ml +++ b/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 *) diff --git a/tests/regression/39-signed-overflows/11-imaxabs.c b/tests/regression/39-signed-overflows/11-imaxabs.c new file mode 100644 index 0000000000..47bd26569f --- /dev/null +++ b/tests/regression/39-signed-overflows/11-imaxabs.c @@ -0,0 +1,24 @@ +//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial +#include +#include +#include +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; +} diff --git a/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c new file mode 100644 index 0000000000..b121645b27 --- /dev/null +++ b/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 +#include +#include +int main() { + int64_t data; + if (data > (-0x7fffffffffffffff - 1) && imaxabs((intmax_t)data) <= sqrtl(0x7fffffffffffffffLL)) + { + int64_t result = data * data; // TODO NOWARN + } + return 8; +} diff --git a/tests/regression/39-signed-overflows/13-imaxabs-macos.c b/tests/regression/39-signed-overflows/13-imaxabs-macos.c new file mode 100644 index 0000000000..745d5b74c4 --- /dev/null +++ b/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 +#include +#include +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; +}