diff --git a/conf/svcomp.json b/conf/svcomp.json index 107c59994c..3c9c689334 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -72,6 +72,7 @@ "wideningThresholds", "loopUnrollHeuristic", "memsafetySpecification", + "tmpSpecialAnalysis", "termination" ] } diff --git a/src/analyses/base.ml b/src/analyses/base.ml index a8ad9af95b..84be8c7a19 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2328,6 +2328,24 @@ struct | _ -> failwith ("non-floating-point argument in call to function "^f.vname) end in + let apply_abs ik x = + let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in + begin match eval_x with + | Int int_x -> + let xcast = ID.cast_to ik int_x in + (* the absolute value of the most-negative value is out of range for 2'complement types *) + (match (ID.minimal xcast), (ID.minimal (ID.top_of ik)) with + | _, None + | None, _ -> ID.top_of ik + | Some mx, Some mm when Z.equal mx mm -> ID.top_of ik + | _, _ -> + let x1 = ID.neg (ID.meet (ID.ending ik Z.zero) xcast) in + let x2 = ID.meet (ID.starting ik Z.zero) xcast in + ID.join x1 x2 + ) + | _ -> failwith ("non-integer argument in call to function "^f.vname) + end + in let result:value = begin match fun_args with | Nan (fk, str) when Cil.isPointerType (Cilfacade.typeOf str) -> Float (FD.nan_of fk) @@ -2356,6 +2374,8 @@ struct | Isunordered (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.unordered x y)) | Fmax (fd, x ,y) -> Float (apply_binary fd FD.fmax x y) | Fmin (fd, x ,y) -> Float (apply_binary fd FD.fmin x y) + | Sqrt (fk, x) -> Float (apply_unary fk FD.sqrt x) + | Abs (ik, x) -> Int (ID.cast_to ik (apply_abs ik x)) end in begin match lv with diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 72e00efbb1..f391231628 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -821,4 +821,31 @@ struct FD.top_of fk in inv_exp (Float ftv) exp st + + let invariant ctx a gs st exp tv: D.t = + let refine0 = invariant ctx a gs st exp tv in + (* bodge for abs(...); To be removed once we have a clean solution *) + let refineAbs op absargexp valexp = + let flip op = match op with | Le -> Ge | Lt -> Gt | _ -> failwith "impossible" in + (* e.g. |arg| <= 40 *) + (* arg <= e (arg <= 40) *) + let le = BinOp (op, absargexp, valexp, intType) in + (* arg >= -e (arg >= -40) *) + let gt = BinOp(flip op, absargexp, UnOp (Neg, valexp, Cilfacade.typeOf valexp), intType) in + let one = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global refine0 le tv in + invariant ctx (Analyses.ask_of_ctx ctx) ctx.global one gt tv + in + match exp with + | BinOp ((Lt|Le) as op, CastE(t, Lval (Var v, NoOffset)), e,_) when tv -> + begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with + | `Lifted (Abs (ik, arg)) -> refineAbs op (CastE (t, arg)) e + | _ -> refine0 + end + | BinOp ((Lt|Le) as op, Lval (Var v, NoOffset), e, _) when tv -> + begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with + | `Lifted (Abs (ik, arg)) -> refineAbs op arg e + | _ -> refine0 + end + | _ -> refine0 + end diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 55da9f6635..4997b306a9 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -27,6 +27,7 @@ type math = | Islessequal of (Basetype.CilExp.t * Basetype.CilExp.t) | Islessgreater of (Basetype.CilExp.t * Basetype.CilExp.t) | Isunordered of (Basetype.CilExp.t * Basetype.CilExp.t) + | Abs of (CilType.Ikind.t * Basetype.CilExp.t) | Ceil of (CilType.Fkind.t * Basetype.CilExp.t) | Floor of (CilType.Fkind.t * Basetype.CilExp.t) | Fabs of (CilType.Fkind.t * Basetype.CilExp.t) @@ -38,7 +39,8 @@ type math = | Atan2 of (CilType.Fkind.t * Basetype.CilExp.t * Basetype.CilExp.t) | Cos of (CilType.Fkind.t * Basetype.CilExp.t) | Sin of (CilType.Fkind.t * Basetype.CilExp.t) - | Tan of (CilType.Fkind.t * Basetype.CilExp.t) [@@deriving eq, ord, hash] + | Tan of (CilType.Fkind.t * Basetype.CilExp.t) + | Sqrt of (CilType.Fkind.t * Basetype.CilExp.t) [@@deriving eq, ord, hash] (** Type of special function, or {!Unknown}. *) (* Use inline record if not single {!Cil.exp} argument. *) @@ -159,6 +161,7 @@ module MathPrintable = struct | Islessequal (exp1, exp2) -> Pretty.dprintf "isLessEqual(%a, %a)" d_exp exp1 d_exp exp2 | Islessgreater (exp1, exp2) -> Pretty.dprintf "isLessGreater(%a, %a)" d_exp exp1 d_exp exp2 | Isunordered (exp1, exp2) -> Pretty.dprintf "isUnordered(%a, %a)" d_exp exp1 d_exp exp2 + | Abs (ik, exp) -> Pretty.dprintf "(%a )abs(%a)" d_ikind ik d_exp exp | Ceil (fk, exp) -> Pretty.dprintf "(%a )ceil(%a)" d_fkind fk d_exp exp | Floor (fk, exp) -> Pretty.dprintf "(%a )floor(%a)" d_fkind fk d_exp exp | Fabs (fk, exp) -> Pretty.dprintf "(%a )fabs(%a)" d_fkind fk d_exp exp @@ -171,6 +174,7 @@ module MathPrintable = struct | Cos (fk, exp) -> Pretty.dprintf "(%a )cos(%a)" d_fkind fk d_exp exp | Sin (fk, exp) -> Pretty.dprintf "(%a )sin(%a)" d_fkind fk d_exp exp | Tan (fk, exp) -> Pretty.dprintf "(%a )tan(%a)" d_fkind fk d_exp exp + | Sqrt (fk, exp) -> Pretty.dprintf "(%a )sqrt(%a)" d_fkind fk d_exp exp include Printable.SimplePretty ( struct diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 0a9c03a32e..12eda8f728 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -130,7 +130,9 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("wcstombs", unknown ~attrs:[ThreadUnsafe] [drop "dst" [w]; drop "src" [r]; drop "size" []]); ("wcsrtombs", unknown ~attrs:[ThreadUnsafe] [drop "dst" [w]; drop "src" [r_deep; w]; drop "size" []; drop "ps" [r_deep; w_deep]]); ("mbstowcs", unknown [drop "dest" [w]; drop "src" [r]; drop "n" []]); - ("abs", unknown [drop "j" []]); + ("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)) }); ("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 *) @@ -945,9 +947,9 @@ let math_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("scalbln", unknown [drop "arg" []; drop "exp" []]); ("scalblnf", unknown [drop "arg" []; drop "exp" []]); ("scalblnl", unknown [drop "arg" []; drop "exp" []]); - ("sqrt", unknown [drop "x" []]); - ("sqrtf", unknown [drop "x" []]); - ("sqrtl", unknown [drop "x" []]); + ("sqrt", special [__ "x" []] @@ fun x -> Math { fun_args = (Sqrt (FDouble, x)) }); + ("sqrtf", special [__ "x" []] @@ fun x -> Math { fun_args = (Sqrt (FFloat, x)) }); + ("sqrtl", special [__ "x" []] @@ fun x -> Math { fun_args = (Sqrt (FLongDouble, x)) }); ("tgamma", unknown [drop "x" []]); ("tgammaf", unknown [drop "x" []]); ("tgammal", unknown [drop "x" []]); diff --git a/src/autoTune.ml b/src/autoTune.ml index 346e9d7b6f..fefdeb32fd 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -473,6 +473,18 @@ let wideningOption factors file = print_endline "Enabled widening thresholds"; } +let activateTmpSpecialAnalysis () = + let isMathFun = function + | LibraryDesc.Math _ -> true + | _ -> false + in + let hasMathFunctions = hasFunction isMathFun in + if hasMathFunctions then ( + print_endline @@ "math function -> enabling tmpSpecial analysis and floating-point domain"; + enableAnalyses ["tmpSpecial"]; + set_bool "ana.float.interval" true; + ) + let estimateComplexity factors file = let pathsEstimate = factors.loops + factors.controlFlowStatements / 90 in let operationEstimate = factors.instructions + (factors.expressions / 60) in @@ -540,6 +552,9 @@ let chooseConfig file = if isActivated "arrayDomain" then selectArrayDomains file; + if isActivated "tmpSpecialAnalysis" then + activateTmpSpecialAnalysis (); + let options = [] in let options = if isActivated "congruence" then (congruenceOption factors file)::options else options in (* Termination analysis uses apron in a different configuration. *) diff --git a/src/cdomains/floatDomain.ml b/src/cdomains/floatDomain.ml index f52c849111..39d3744401 100644 --- a/src/cdomains/floatDomain.ml +++ b/src/cdomains/floatDomain.ml @@ -40,6 +40,8 @@ module type FloatArith = sig (** sin(x) *) val tan : t -> t (** tan(x) *) + val sqrt : t -> t + (** sqrt(x) *) (** {inversions of unary functions}*) val inv_ceil : ?asPreciseAsConcrete:bool -> t -> t @@ -670,6 +672,14 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct | (l, h) when l = h && l = Float_t.zero -> of_const 0. (*tan(0) = 0*) | _ -> top () (**could be exact for intervals where l=h, or even for some intervals *) + let eval_sqrt = function + | (l, h) when l = Float_t.zero && h = Float_t.zero -> of_const 0. + | (l, h) when l >= Float_t.zero -> + let low = Float_t.sqrt Down l in + let high = Float_t.sqrt Up h in + Interval (low, high) + | _ -> top () + let eval_inv_ceil ?(asPreciseAsConcrete=false) = function | (l, h) -> if (Float_t.sub Up (Float_t.ceil l) (Float_t.sub Down (Float_t.ceil l) (Float_t.of_float Nearest 1.0)) = (Float_t.of_float Nearest 1.0)) then ( @@ -784,6 +794,7 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct let cos = eval_unop eval_cos let sin = eval_unop eval_sin let tan = eval_unop eval_tan + let sqrt = eval_unop eval_sqrt let inv_ceil ?(asPreciseAsConcrete=false) = eval_unop ~warn:false (eval_inv_ceil ~asPreciseAsConcrete:asPreciseAsConcrete) let inv_floor ?(asPreciseAsConcrete=false) = eval_unop ~warn:false (eval_inv_floor ~asPreciseAsConcrete:asPreciseAsConcrete) @@ -899,6 +910,7 @@ module FloatIntervalImplLifted = struct let cos = lift (F1.cos, F2.cos) let sin = lift (F1.sin, F2.sin) let tan = lift (F1.tan, F2.tan) + let sqrt = lift (F1.sqrt, F2.sqrt) let inv_ceil ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) = function | F32 a -> F32 (F1.inv_ceil ~asPreciseAsConcrete:true a) @@ -1159,6 +1171,8 @@ module FloatDomTupleImpl = struct map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.sin); } let tan = map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.tan); } + let sqrt = + map { f1= (fun (type a) (module F : FloatDomain with type t = a) -> F.sqrt); } (*"asPreciseAsConcrete" has no meaning here*) let inv_ceil ?(asPreciseAsConcrete=BoolDomain.MustBool.top ()) = diff --git a/src/cdomains/floatDomain.mli b/src/cdomains/floatDomain.mli index 06bca69aca..d958e1ee81 100644 --- a/src/cdomains/floatDomain.mli +++ b/src/cdomains/floatDomain.mli @@ -57,6 +57,9 @@ module type FloatArith = sig val tan : t -> t (** tan(x) *) + val sqrt : t -> t + (** sqrt(x) *) + (** {inversions of unary functions}*) val inv_ceil : ?asPreciseAsConcrete:bool -> t -> t (** (inv_ceil z -> x) if (z = ceil(x)) *) diff --git a/src/cdomains/floatOps/floatOps.ml b/src/cdomains/floatOps/floatOps.ml index a951ec08fe..a4e39d930e 100644 --- a/src/cdomains/floatOps/floatOps.ml +++ b/src/cdomains/floatOps/floatOps.ml @@ -35,6 +35,7 @@ module type CFloatType = sig val sub: round_mode -> t -> t -> t val mul: round_mode -> t -> t -> t val div: round_mode -> t -> t -> t + val sqrt: round_mode -> t -> t val atof: round_mode -> string -> t end @@ -74,6 +75,7 @@ module CDouble = struct external sub: round_mode -> t -> t -> t = "sub_double" external mul: round_mode -> t -> t -> t = "mul_double" external div: round_mode -> t -> t -> t = "div_double" + external sqrt: round_mode -> t -> t = "sqrt_double" external atof: round_mode -> string -> t = "atof_double" end @@ -107,6 +109,7 @@ module CFloat = struct external sub: round_mode -> t -> t -> t = "sub_float" external mul: round_mode -> t -> t -> t = "mul_float" external div: round_mode -> t -> t -> t = "div_float" + external sqrt: round_mode -> t -> t = "sqrt_float" external atof: round_mode -> string -> t = "atof_float" diff --git a/src/cdomains/floatOps/floatOps.mli b/src/cdomains/floatOps/floatOps.mli index 05bf363872..cf24f75ed5 100644 --- a/src/cdomains/floatOps/floatOps.mli +++ b/src/cdomains/floatOps/floatOps.mli @@ -38,6 +38,7 @@ module type CFloatType = sig val sub: round_mode -> t -> t -> t val mul: round_mode -> t -> t -> t val div: round_mode -> t -> t -> t + val sqrt: round_mode -> t -> t val atof: round_mode -> string -> t end diff --git a/src/cdomains/floatOps/stubs.c b/src/cdomains/floatOps/stubs.c index e0485883dd..50e4a2fb31 100644 --- a/src/cdomains/floatOps/stubs.c +++ b/src/cdomains/floatOps/stubs.c @@ -36,6 +36,20 @@ static void change_round_mode(int mode) } } +#define UNARY_OP(name, type, op) \ + CAMLprim value name##_##type(value mode, value x) \ + { \ + int old_roundingmode = fegetround(); \ + change_round_mode(Int_val(mode)); \ + volatile type r, x1 = Double_val(x); \ + r = op(x1); \ + fesetround(old_roundingmode); \ + return caml_copy_double(r); \ + } + +UNARY_OP(sqrt, double, sqrt); +UNARY_OP(sqrt, float, sqrtf); + #define BINARY_OP(name, type, op) \ CAMLprim value name##_##type(value mode, value x, value y) \ { \ diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index 9a6a66ee6b..bbca23cbe1 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -544,7 +544,7 @@ "type": "array", "items": { "type": "string" }, "default": [ - "congruence", "singleThreaded", "specification", "mallocWrappers", "noRecursiveIntervals", "enums", "loopUnrollHeuristic", "arrayDomain", "octagon", "wideningThresholds", "memsafetySpecification" + "congruence", "singleThreaded", "specification", "mallocWrappers", "noRecursiveIntervals", "enums", "loopUnrollHeuristic", "arrayDomain", "octagon", "wideningThresholds", "memsafetySpecification", "tmpSpecialAnalysis" ] } }, diff --git a/tests/regression/39-signed-overflows/06-abs.c b/tests/regression/39-signed-overflows/06-abs.c new file mode 100644 index 0000000000..e56cc9ff7d --- /dev/null +++ b/tests/regression/39-signed-overflows/06-abs.c @@ -0,0 +1,22 @@ +//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial +#include +int main() { + int data; + if (data > (-0x7fffffff - 1)) + { + if (abs(data) < 100) + { + __goblint_check(data < 100); + __goblint_check(-100 < data); + int result = data * data; //NOWARN + } + + if(abs(data) <= 100) + { + __goblint_check(data <= 100); + __goblint_check(-100 <= data); + int result = data * data; //NOWARN + } + } + return 8; +} \ No newline at end of file diff --git a/tests/regression/39-signed-overflows/07-abs-sqrt.c b/tests/regression/39-signed-overflows/07-abs-sqrt.c new file mode 100644 index 0000000000..13ed863e51 --- /dev/null +++ b/tests/regression/39-signed-overflows/07-abs-sqrt.c @@ -0,0 +1,10 @@ +//PARAM: --enable ana.int.interval --enable ana.float.interval --set ana.activated[+] tmpSpecial +#include +int main() { + int data; + if (data > (-0x7fffffff - 1) && abs(data) < (long)sqrt((double)0x7fffffff)) + { + int result = data * data; //NOWARN + } + return 8; +} \ No newline at end of file diff --git a/tests/regression/39-signed-overflows/08-labs.c b/tests/regression/39-signed-overflows/08-labs.c new file mode 100644 index 0000000000..a9c6773d11 --- /dev/null +++ b/tests/regression/39-signed-overflows/08-labs.c @@ -0,0 +1,22 @@ +//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial +#include +int main() { + long data; + if (data > (-0xffffffff - 1)) + { + if (labs(data) < 100) + { + __goblint_check(data < 100); + __goblint_check(-100 < data); + int result = data * data; //NOWARN + } + + if(labs(data) <= 100) + { + __goblint_check(data <= 100); + __goblint_check(-100 <= data); + int result = data * data; //NOWARN + } + } + return 8; +} diff --git a/tests/regression/39-signed-overflows/09-labs-sqrt.c b/tests/regression/39-signed-overflows/09-labs-sqrt.c new file mode 100644 index 0000000000..3a4b20a82b --- /dev/null +++ b/tests/regression/39-signed-overflows/09-labs-sqrt.c @@ -0,0 +1,10 @@ +//PARAM: --enable ana.int.interval --enable ana.float.interval --set ana.activated[+] tmpSpecial +#include +int main() { + int data; + if (data > (-0x7fffffff - 1) && llabs(data) < (long)sqrt((double)0x7fffffff)) + { + int result = data * data; //NOWARN + } + return 8; +} diff --git a/tests/regression/39-signed-overflows/06-shiftleft.c b/tests/regression/39-signed-overflows/10-shiftleft.c similarity index 100% rename from tests/regression/39-signed-overflows/06-shiftleft.c rename to tests/regression/39-signed-overflows/10-shiftleft.c