From 9420a089fcc1134f289d61f5eb8e45571ca47d23 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 16 Nov 2023 16:13:29 +0100 Subject: [PATCH 01/17] add sqrt handling in float domain --- src/analyses/base.ml | 1 + src/analyses/libraryDesc.ml | 4 +++- src/analyses/libraryFunctions.ml | 6 +++--- src/cdomains/floatDomain.ml | 14 ++++++++++++++ src/cdomains/floatDomain.mli | 3 +++ src/cdomains/floatOps/floatOps.ml | 3 +++ src/cdomains/floatOps/floatOps.mli | 1 + src/cdomains/floatOps/stubs.c | 14 ++++++++++++++ 8 files changed, 42 insertions(+), 4 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index a8ad9af95b..86951ab4a5 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2356,6 +2356,7 @@ 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) end in begin match lv with diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 72a4261cb5..5403612fae 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -38,7 +38,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. *) @@ -170,6 +171,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 117dcbd236..8f8a43cb29 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -944,9 +944,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/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) \ { \ From 0740491dcc290a8e41e693f0b8534af9540ebb37 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 16 Nov 2023 20:09:24 +0100 Subject: [PATCH 02/17] implement abs function for integers --- src/analyses/base.ml | 18 ++++++++++++++++++ src/analyses/libraryDesc.ml | 2 ++ src/analyses/libraryFunctions.ml | 2 +- 3 files changed, 21 insertions(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 86951ab4a5..bca3cb6588 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2328,6 +2328,23 @@ 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 + (* TODO cover case where x is the MIN value -> undefined *) + (match ID.le xcast (ID.of_int ik Z.zero) with + | d when d = ID.of_int ik Z.zero -> xcast (* x positive *) + | d when d = ID.of_int ik Z.one -> ID.neg xcast (* x negative *) + | _ -> (* both possible *) + 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) @@ -2357,6 +2374,7 @@ struct | 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 x -> Int (ID.cast_to IInt (apply_abs IInt x)) end in begin match lv with diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 5403612fae..8cd3dfa1ba 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 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) @@ -159,6 +160,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 exp -> Pretty.dprintf "abs(%a)" 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 diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 8f8a43cb29..ae33f57f70 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -130,7 +130,7 @@ 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 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 *) From b9ede51e83b64db87b6a2e0322d3c348c114c07c Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Fri, 17 Nov 2023 11:11:14 +0100 Subject: [PATCH 03/17] implement special case for most-negative value --- src/analyses/base.ml | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index bca3cb6588..f25f0a9693 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2333,14 +2333,19 @@ struct begin match eval_x with | Int int_x -> let xcast = ID.cast_to ik int_x in - (* TODO cover case where x is the MIN value -> undefined *) - (match ID.le xcast (ID.of_int ik Z.zero) with - | d when d = ID.of_int ik Z.zero -> xcast (* x positive *) - | d when d = ID.of_int ik Z.one -> ID.neg xcast (* x negative *) - | _ -> (* both possible *) - 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 + (* 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 + | _, _ -> + match ID.le xcast (ID.of_int ik Z.zero) with + | d when d = ID.of_int ik Z.zero -> xcast (* x positive *) + | d when d = ID.of_int ik Z.one -> ID.neg xcast (* x negative *) + | _ -> (* both possible *) + 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 From 566348216fff4b119559d907df9b8e2e005fa023 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Fri, 17 Nov 2023 16:14:36 +0100 Subject: [PATCH 04/17] improve values of parameters in abs call --- src/analyses/baseInvariant.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 72e00efbb1..73a41bcea1 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -726,6 +726,8 @@ struct | `Lifted (Isless (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st | `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st | `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st + | `Lifted (Abs xInt) -> + inv_exp (Int (ID.of_bool ik tv)) (BinOp (LAnd, (BinOp (Le, xInt, Lval x, TInt (IInt,[]))), (BinOp (Le, (UnOp (Neg, Lval x, (typeOf xInt))), xInt, TInt (IInt,[]))), (TInt (IInt, [])))) st | _ -> update_lval c x c' ID.pretty end | None -> update_lval c x c' ID.pretty From 688cff1c28936295f3c084dd5d60f36e70dbd5a1 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Sat, 18 Nov 2023 11:26:38 +0100 Subject: [PATCH 05/17] trying to fix that value is not improved for parameter of abs call --- src/analyses/baseInvariant.ml | 71 +++++++++++++++++++++-------------- 1 file changed, 42 insertions(+), 29 deletions(-) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 73a41bcea1..b82ab88806 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -562,7 +562,7 @@ struct | TFloat (fk, _) -> fk | _ -> failwith "value which was expected to be a float is of different type?!" in - let rec inv_exp c_typed exp (st:D.t): D.t = + let rec inv_exp ?(query_special=true) c_typed exp (st:D.t) : D.t = (* trying to improve variables in an expression so it is bottom means dead code *) if VD.is_bot_value c_typed then contra st else @@ -578,12 +578,12 @@ struct | Some false -> ID.of_bool ikind false | _ -> ID.top_of ikind in - inv_exp (Int c') e st - | UnOp (Neg, e, _), Float c -> inv_exp (Float (unop_FD Neg c)) e st - | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp (Int (unop_ID op c)) e st + inv_exp ~query_special (Int c') e st + | UnOp (Neg, e, _), Float c -> inv_exp ~query_special (Float (unop_FD Neg c)) e st + | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp ~query_special (Int (unop_ID op c)) e st (* no equivalent for Float, as VD.is_safe_cast fails for all float types anyways *) | BinOp((Eq | Ne) as op, CastE (t1, e1), CastE (t2, e2), t), Int c when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_safe_cast t2 (Cilfacade.typeOf e2) -> - inv_exp (Int c) (BinOp (op, e1, e2, t)) st + inv_exp ~query_special (Int c) (BinOp (op, e1, e2, t)) st | BinOp (LOr, arg1, arg2, typ) as exp, Int c -> (* copied & modified from eval_rv_base... *) let (let*) = Option.bind in @@ -631,7 +631,7 @@ struct in let definite_ad = to_definite_ad vs in let c' = VD.Address definite_ad in - Some (inv_exp c' e st) + Some (inv_exp ~query_special c' e st) | Int i -> let ik = ID.ikind i in let module BISet = IntDomain.BISet in @@ -648,20 +648,20 @@ struct in let int_id = to_int_id vs in let c' = VD.Int int_id in - Some (inv_exp c' e st) + Some (inv_exp ~query_special c' e st) | _ -> None in begin match eqs_st with | Some st -> st | None when ID.to_bool c = Some true -> - begin match inv_exp (Int c) arg1 st with + begin match inv_exp ~query_special (Int c) arg1 st with | st1 -> - begin match inv_exp (Int c) arg2 st with + begin match inv_exp ~query_special (Int c) arg2 st with | st2 -> D.join st1 st2 | exception Analyses.Deadcode -> st1 end - | exception Analyses.Deadcode -> inv_exp (Int c) arg2 st (* Deadcode falls through *) + | exception Analyses.Deadcode -> inv_exp ~query_special (Int c) arg2 st (* Deadcode falls through *) end | None -> st (* TODO: not bothering to fall back, no other case can refine LOr anyway *) @@ -676,15 +676,15 @@ struct let ikres = Cilfacade.get_ikind_exp e in (* might be different from argument types, e.g. for LT, GT, EQ, ... *) let a', b' = inv_bin_int (a, b) ikind (c_int ikres) op in if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a\n" d_exp e ID.pretty (c_int ikind) ID.pretty a' ID.pretty b'; - let st' = inv_exp (Int a') e1 st in - let st'' = inv_exp (Int b') e2 st' in + let st' = inv_exp ~query_special (Int a') e1 st in + let st'' = inv_exp ~query_special (Int b') e2 st' in st'' | Float a, Float b -> let fkind = Cilfacade.get_fkind_exp e1 in (* both operands have the same type *) let a', b' = inv_bin_float (a, b) (c_float fkind) op in if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a\n" d_exp e FD.pretty (c_float fkind) FD.pretty a' FD.pretty b'; - let st' = inv_exp (Float a') e1 st in - let st'' = inv_exp (Float b') e2 st' in + let st' = inv_exp ~query_special (Float a') e1 st in + let st'' = inv_exp ~query_special (Float b') e2 st' in st'' (* Mixed Float and Int cases should never happen, as there are no binary operators with one float and one int parameter ?!*) | Int _, Float _ | Float _, Int _ -> failwith "ill-typed program"; @@ -712,22 +712,22 @@ struct begin match t with | TInt (ik, _) -> begin match x with - | ((Var v), offs) -> + | ((Var v), offs) when query_special -> if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs))); let tv_opt = ID.to_bool c in begin match tv_opt with | Some tv -> begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with - | `Lifted (Isfinite xFloat) when tv -> inv_exp (Float (FD.finite (unroll_fk_of_exp xFloat))) xFloat st - | `Lifted (Isnan xFloat) when tv -> inv_exp (Float (FD.nan_of (unroll_fk_of_exp xFloat))) xFloat st + | `Lifted (Isfinite xFloat) when tv -> inv_exp ~query_special:false (Float (FD.finite (unroll_fk_of_exp xFloat))) xFloat st + | `Lifted (Isnan xFloat) when tv -> inv_exp ~query_special:false (Float (FD.nan_of (unroll_fk_of_exp xFloat))) xFloat st (* should be correct according to C99 standard*) - | `Lifted (Isgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))) st - | `Lifted (Isgreaterequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Ge, xFloat, yFloat, (typeOf xFloat))) st - | `Lifted (Isless (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st - | `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st - | `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st + | `Lifted (Isgreater (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))) st + | `Lifted (Isgreaterequal (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (Ge, xFloat, yFloat, (typeOf xFloat))) st + | `Lifted (Isless (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st + | `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st + | `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st | `Lifted (Abs xInt) -> - inv_exp (Int (ID.of_bool ik tv)) (BinOp (LAnd, (BinOp (Le, xInt, Lval x, TInt (IInt,[]))), (BinOp (Le, (UnOp (Neg, Lval x, (typeOf xInt))), xInt, TInt (IInt,[]))), (TInt (IInt, [])))) st + inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (LAnd, (BinOp (Le, xInt, Lval x, TInt (IInt,[]))), (BinOp (Le, (UnOp (Neg, Lval x, (typeOf xInt))), xInt, TInt (IInt,[]))), (TInt (IInt, [])))) st | _ -> update_lval c x c' ID.pretty end | None -> update_lval c x c' ID.pretty @@ -749,17 +749,17 @@ struct begin match t with | TFloat (fk, _) -> begin match x with - | ((Var v), offs) -> + | ((Var v), offs) when query_special -> if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs))); begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with - | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st - | `Lifted (Floor (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_floor (FD.cast_to ret_fk c))) xFloat st + | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp ~query_special:false (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st + | `Lifted (Floor (ret_fk, xFloat)) -> inv_exp ~query_special:false (Float (FD.inv_floor (FD.cast_to ret_fk c))) xFloat st | `Lifted (Fabs (ret_fk, xFloat)) -> let inv = FD.inv_fabs (FD.cast_to ret_fk c) in if FD.is_bot inv then raise Analyses.Deadcode else - inv_exp (Float inv) xFloat st + inv_exp ~query_special:false (Float inv) xFloat st | _ -> update_lval c x c' FD.pretty end | _ -> update_lval c x c' FD.pretty @@ -779,7 +779,7 @@ struct | 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 + | TFloat (FFloat as fk, _), FFloat -> inv_exp ~query_special (Float (FD.cast_to fk c)) e st | _ -> fallback ("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. *) @@ -792,7 +792,20 @@ struct (* let c' = ID.cast_to ik_e c in *) let c' = ID.cast_to ik_e (ID.meet c (ID.cast_to ik (ID.top_of ik_e))) 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\n" 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 + inv_exp ~query_special (Int c') e st + | x -> fallback (GobPretty.sprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st + else + fallback (GobPretty.sprintf "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 + | Float i -> + let i = FD.to_int ik i in + if ID.leq i (ID.cast_to ik i) then + match unrollType (Cilfacade.typeOf e) with + | TInt(ik_e, _) + | TEnum ({ekind = ik_e; _ }, _) -> + (* let c' = ID.cast_to ik_e c in *) + let c' = ID.cast_to ik_e (ID.meet c (ID.cast_to ik (ID.top_of ik_e))) 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\n" 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 ~query_special (Int c') e st | x -> fallback (GobPretty.sprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st else fallback (GobPretty.sprintf "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 From 88957a8005c2eff0d51c8bd1402c9d91e2e2a84e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 18 Nov 2023 11:32:52 +0100 Subject: [PATCH 06/17] Add test which can be run in isolation --- tests/regression/39-signed-overflows/06-abs.c | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 tests/regression/39-signed-overflows/06-abs.c 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..b08a0f2209 --- /dev/null +++ b/tests/regression/39-signed-overflows/06-abs.c @@ -0,0 +1,15 @@ +//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial +#include +int main() { + int data; + if (data > (-0x7fffffff - 1)) + { + if (abs(data) < 100) + { + int result = data * data; + } + + int result = data * data; + } + return 8; +} \ No newline at end of file From 2ea8db4b64f1a55e25b2ae226d5d82815766a80c Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 18 Nov 2023 12:21:30 +0100 Subject: [PATCH 07/17] Wir sind alle Pfuscher vor dem HERRN --- src/analyses/base.ml | 46 +++++++++++++++---- src/analyses/baseInvariant.ml | 6 +-- tests/regression/39-signed-overflows/06-abs.c | 2 - .../39-signed-overflows/07-abs-sqrt.c | 10 ++++ 4 files changed, 50 insertions(+), 14 deletions(-) create mode 100644 tests/regression/39-signed-overflows/07-abs-sqrt.c diff --git a/src/analyses/base.ml b/src/analyses/base.ml index f25f0a9693..8b9b232913 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1753,15 +1753,43 @@ struct let branch ctx (exp:exp) (tv:bool) : store = let valu = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp in let refine () = - let res = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp tv in - if M.tracing then M.tracec "branch" "EqualSet result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.EqualSet exp)); - if M.tracing then M.tracec "branch" "CondVars result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.CondVars exp)); - if M.tracing then M.traceu "branch" "Invariant enforced!\n"; - match ctx.ask (Queries.CondVars exp) with - | s when Queries.ES.cardinal s = 1 -> - let e = Queries.ES.choose s in - invariant ctx (Analyses.ask_of_ctx ctx) ctx.global res e tv - | _ -> res + let refine0 = + let res = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp tv in + if M.tracing then M.tracec "branch" "EqualSet result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.EqualSet exp)); + if M.tracing then M.tracec "branch" "CondVars result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.CondVars exp)); + if M.tracing then M.traceu "branch" "Invariant enforced!\n"; + match ctx.ask (Queries.CondVars exp) with + | s when Queries.ES.cardinal s = 1 -> + let e = Queries.ES.choose s in + invariant ctx (Analyses.ask_of_ctx ctx) ctx.global res e tv + | _ -> res + in + match exp with + | BinOp (Lt, CastE(t,Lval (Var v, NoOffset)), e,_) when tv -> + (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with + | `Lifted (Abs arg) -> + (* e.g. |arg| < 40 *) + let v = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in + (* arg <= e (arg <= 40) *) + let le = BinOp (Le, CastE(t,arg), e, intType) in + (* arg >= -e (arg >= -40) *) + let gt = BinOp(Ge, CastE(t,arg), UnOp (Neg, e, Cilfacade.typeOf e), 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 + | _ -> refine0) + | BinOp (Lt, Lval (Var v, NoOffset), e, _) when tv -> + (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with + | `Lifted (Abs arg) -> + (* e.g. |arg| < 40 *) + let v = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in + (* arg <= e (arg <= 40) *) + let le = BinOp (Le, arg, e, intType) in + (* arg >= -e (arg >= -40) *) + let gt = BinOp(Ge, arg, UnOp (Neg, e, Cilfacade.typeOf e), 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 + | _ -> refine0) + | _ -> refine0 in if M.tracing then M.traceli "branch" ~subsys:["invariant"] "Evaluating branch for expression %a with value %a\n" d_exp exp VD.pretty valu; (* First we want to see, if we can determine a dead branch: *) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index b82ab88806..397bd1623e 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -712,7 +712,7 @@ struct begin match t with | TInt (ik, _) -> begin match x with - | ((Var v), offs) when query_special -> + | ((Var v), offs) -> if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs))); let tv_opt = ID.to_bool c in begin match tv_opt with @@ -730,7 +730,7 @@ struct inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (LAnd, (BinOp (Le, xInt, Lval x, TInt (IInt,[]))), (BinOp (Le, (UnOp (Neg, Lval x, (typeOf xInt))), xInt, TInt (IInt,[]))), (TInt (IInt, [])))) st | _ -> update_lval c x c' ID.pretty end - | None -> update_lval c x c' ID.pretty + | _ -> update_lval c x c' ID.pretty end | _ -> update_lval c x c' ID.pretty end @@ -749,7 +749,7 @@ struct begin match t with | TFloat (fk, _) -> begin match x with - | ((Var v), offs) when query_special -> + | ((Var v), offs) -> if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs))); begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp ~query_special:false (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st diff --git a/tests/regression/39-signed-overflows/06-abs.c b/tests/regression/39-signed-overflows/06-abs.c index b08a0f2209..e87e25d9fe 100644 --- a/tests/regression/39-signed-overflows/06-abs.c +++ b/tests/regression/39-signed-overflows/06-abs.c @@ -8,8 +8,6 @@ int main() { { int result = data * data; } - - int result = data * data; } 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..0f8ce396f2 --- /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; + } + return 8; +} \ No newline at end of file From 379733825fce688cec97a63a2fa32c951e7d2c10 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 18 Nov 2023 12:28:22 +0100 Subject: [PATCH 08/17] Reset baseInvariant to master --- src/analyses/baseInvariant.ml | 69 ++++++++++++++--------------------- 1 file changed, 27 insertions(+), 42 deletions(-) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 397bd1623e..72e00efbb1 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -562,7 +562,7 @@ struct | TFloat (fk, _) -> fk | _ -> failwith "value which was expected to be a float is of different type?!" in - let rec inv_exp ?(query_special=true) c_typed exp (st:D.t) : D.t = + let rec inv_exp c_typed exp (st:D.t): D.t = (* trying to improve variables in an expression so it is bottom means dead code *) if VD.is_bot_value c_typed then contra st else @@ -578,12 +578,12 @@ struct | Some false -> ID.of_bool ikind false | _ -> ID.top_of ikind in - inv_exp ~query_special (Int c') e st - | UnOp (Neg, e, _), Float c -> inv_exp ~query_special (Float (unop_FD Neg c)) e st - | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp ~query_special (Int (unop_ID op c)) e st + inv_exp (Int c') e st + | UnOp (Neg, e, _), Float c -> inv_exp (Float (unop_FD Neg c)) e st + | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp (Int (unop_ID op c)) e st (* no equivalent for Float, as VD.is_safe_cast fails for all float types anyways *) | BinOp((Eq | Ne) as op, CastE (t1, e1), CastE (t2, e2), t), Int c when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_safe_cast t2 (Cilfacade.typeOf e2) -> - inv_exp ~query_special (Int c) (BinOp (op, e1, e2, t)) st + inv_exp (Int c) (BinOp (op, e1, e2, t)) st | BinOp (LOr, arg1, arg2, typ) as exp, Int c -> (* copied & modified from eval_rv_base... *) let (let*) = Option.bind in @@ -631,7 +631,7 @@ struct in let definite_ad = to_definite_ad vs in let c' = VD.Address definite_ad in - Some (inv_exp ~query_special c' e st) + Some (inv_exp c' e st) | Int i -> let ik = ID.ikind i in let module BISet = IntDomain.BISet in @@ -648,20 +648,20 @@ struct in let int_id = to_int_id vs in let c' = VD.Int int_id in - Some (inv_exp ~query_special c' e st) + Some (inv_exp c' e st) | _ -> None in begin match eqs_st with | Some st -> st | None when ID.to_bool c = Some true -> - begin match inv_exp ~query_special (Int c) arg1 st with + begin match inv_exp (Int c) arg1 st with | st1 -> - begin match inv_exp ~query_special (Int c) arg2 st with + begin match inv_exp (Int c) arg2 st with | st2 -> D.join st1 st2 | exception Analyses.Deadcode -> st1 end - | exception Analyses.Deadcode -> inv_exp ~query_special (Int c) arg2 st (* Deadcode falls through *) + | exception Analyses.Deadcode -> inv_exp (Int c) arg2 st (* Deadcode falls through *) end | None -> st (* TODO: not bothering to fall back, no other case can refine LOr anyway *) @@ -676,15 +676,15 @@ struct let ikres = Cilfacade.get_ikind_exp e in (* might be different from argument types, e.g. for LT, GT, EQ, ... *) let a', b' = inv_bin_int (a, b) ikind (c_int ikres) op in if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a\n" d_exp e ID.pretty (c_int ikind) ID.pretty a' ID.pretty b'; - let st' = inv_exp ~query_special (Int a') e1 st in - let st'' = inv_exp ~query_special (Int b') e2 st' in + let st' = inv_exp (Int a') e1 st in + let st'' = inv_exp (Int b') e2 st' in st'' | Float a, Float b -> let fkind = Cilfacade.get_fkind_exp e1 in (* both operands have the same type *) let a', b' = inv_bin_float (a, b) (c_float fkind) op in if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a\n" d_exp e FD.pretty (c_float fkind) FD.pretty a' FD.pretty b'; - let st' = inv_exp ~query_special (Float a') e1 st in - let st'' = inv_exp ~query_special (Float b') e2 st' in + let st' = inv_exp (Float a') e1 st in + let st'' = inv_exp (Float b') e2 st' in st'' (* Mixed Float and Int cases should never happen, as there are no binary operators with one float and one int parameter ?!*) | Int _, Float _ | Float _, Int _ -> failwith "ill-typed program"; @@ -718,19 +718,17 @@ struct begin match tv_opt with | Some tv -> begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with - | `Lifted (Isfinite xFloat) when tv -> inv_exp ~query_special:false (Float (FD.finite (unroll_fk_of_exp xFloat))) xFloat st - | `Lifted (Isnan xFloat) when tv -> inv_exp ~query_special:false (Float (FD.nan_of (unroll_fk_of_exp xFloat))) xFloat st + | `Lifted (Isfinite xFloat) when tv -> inv_exp (Float (FD.finite (unroll_fk_of_exp xFloat))) xFloat st + | `Lifted (Isnan xFloat) when tv -> inv_exp (Float (FD.nan_of (unroll_fk_of_exp xFloat))) xFloat st (* should be correct according to C99 standard*) - | `Lifted (Isgreater (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))) st - | `Lifted (Isgreaterequal (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (Ge, xFloat, yFloat, (typeOf xFloat))) st - | `Lifted (Isless (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st - | `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st - | `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st - | `Lifted (Abs xInt) -> - inv_exp ~query_special:false (Int (ID.of_bool ik tv)) (BinOp (LAnd, (BinOp (Le, xInt, Lval x, TInt (IInt,[]))), (BinOp (Le, (UnOp (Neg, Lval x, (typeOf xInt))), xInt, TInt (IInt,[]))), (TInt (IInt, [])))) st + | `Lifted (Isgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))) st + | `Lifted (Isgreaterequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Ge, xFloat, yFloat, (typeOf xFloat))) st + | `Lifted (Isless (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st + | `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st + | `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st | _ -> update_lval c x c' ID.pretty end - | _ -> update_lval c x c' ID.pretty + | None -> update_lval c x c' ID.pretty end | _ -> update_lval c x c' ID.pretty end @@ -752,14 +750,14 @@ struct | ((Var v), offs) -> if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs))); begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with - | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp ~query_special:false (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st - | `Lifted (Floor (ret_fk, xFloat)) -> inv_exp ~query_special:false (Float (FD.inv_floor (FD.cast_to ret_fk c))) xFloat st + | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st + | `Lifted (Floor (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_floor (FD.cast_to ret_fk c))) xFloat st | `Lifted (Fabs (ret_fk, xFloat)) -> let inv = FD.inv_fabs (FD.cast_to ret_fk c) in if FD.is_bot inv then raise Analyses.Deadcode else - inv_exp ~query_special:false (Float inv) xFloat st + inv_exp (Float inv) xFloat st | _ -> update_lval c x c' FD.pretty end | _ -> update_lval c x c' FD.pretty @@ -779,7 +777,7 @@ struct | TFloat (FLongDouble as fk, _), FDouble | TFloat (fk, _), FLongDouble | TFloat (FDouble as fk, _), FDouble - | TFloat (FFloat as fk, _), FFloat -> inv_exp ~query_special (Float (FD.cast_to fk c)) e st + | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st | _ -> fallback ("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. *) @@ -792,20 +790,7 @@ struct (* let c' = ID.cast_to ik_e c in *) let c' = ID.cast_to ik_e (ID.meet c (ID.cast_to ik (ID.top_of ik_e))) 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\n" 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 ~query_special (Int c') e st - | x -> fallback (GobPretty.sprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st - else - fallback (GobPretty.sprintf "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 - | Float i -> - let i = FD.to_int ik i in - if ID.leq i (ID.cast_to ik i) then - match unrollType (Cilfacade.typeOf e) with - | TInt(ik_e, _) - | TEnum ({ekind = ik_e; _ }, _) -> - (* let c' = ID.cast_to ik_e c in *) - let c' = ID.cast_to ik_e (ID.meet c (ID.cast_to ik (ID.top_of ik_e))) 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\n" 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 ~query_special (Int c') e st + inv_exp (Int c') e st | x -> fallback (GobPretty.sprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st else fallback (GobPretty.sprintf "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 From 6895ac0cf305747f617d8b4c42f191484f6bc072 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 18 Nov 2023 12:41:37 +0100 Subject: [PATCH 09/17] Make bodge a bit nicer --- src/analyses/base.ml | 30 +++++++++++++----------------- 1 file changed, 13 insertions(+), 17 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 8b9b232913..8497f38615 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1764,30 +1764,26 @@ struct invariant ctx (Analyses.ask_of_ctx ctx) ctx.global res e tv | _ -> res in + (* bodge for abs(...); To be removed once we have a clean solution *) + let refineAbs absargexp valexp = + (* e.g. |arg| < 40 *) + (* arg <= e (arg <= 40) *) + let le = BinOp (Le, absargexp, valexp, intType) in + (* arg >= -e (arg >= -40) *) + let gt = BinOp(Ge, 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, CastE(t,Lval (Var v, NoOffset)), e,_) when tv -> + | BinOp (Lt, CastE(t, Lval (Var v, NoOffset)), e,_) when tv -> (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with | `Lifted (Abs arg) -> - (* e.g. |arg| < 40 *) - let v = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in - (* arg <= e (arg <= 40) *) - let le = BinOp (Le, CastE(t,arg), e, intType) in - (* arg >= -e (arg >= -40) *) - let gt = BinOp(Ge, CastE(t,arg), UnOp (Neg, e, Cilfacade.typeOf e), 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 + refineAbs (CastE (t, arg)) e | _ -> refine0) | BinOp (Lt, Lval (Var v, NoOffset), e, _) when tv -> (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with | `Lifted (Abs arg) -> - (* e.g. |arg| < 40 *) - let v = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in - (* arg <= e (arg <= 40) *) - let le = BinOp (Le, arg, e, intType) in - (* arg >= -e (arg >= -40) *) - let gt = BinOp(Ge, arg, UnOp (Neg, e, Cilfacade.typeOf e), 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 + refineAbs arg e | _ -> refine0) | _ -> refine0 in From ba6726a4515ca4873c1abb87b58f7d9a7f535da8 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 18 Nov 2023 12:50:57 +0100 Subject: [PATCH 10/17] Handle <= as well --- src/analyses/base.ml | 17 +++++++++-------- tests/regression/39-signed-overflows/06-abs.c | 11 ++++++++++- 2 files changed, 19 insertions(+), 9 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 8497f38615..4911b0d033 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1765,25 +1765,26 @@ struct | _ -> res in (* bodge for abs(...); To be removed once we have a clean solution *) - let refineAbs absargexp valexp = - (* e.g. |arg| < 40 *) + 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 (Le, absargexp, valexp, intType) in + let le = BinOp (op, absargexp, valexp, intType) in (* arg >= -e (arg >= -40) *) - let gt = BinOp(Ge, absargexp, UnOp (Neg, valexp, Cilfacade.typeOf valexp), intType) in + 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, CastE(t, Lval (Var v, NoOffset)), e,_) when tv -> + | BinOp ((Lt|Le) as op, CastE(t, Lval (Var v, NoOffset)), e,_) when tv -> (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with | `Lifted (Abs arg) -> - refineAbs (CastE (t, arg)) e + refineAbs op (CastE (t, arg)) e | _ -> refine0) - | BinOp (Lt, Lval (Var v, NoOffset), e, _) when tv -> + | BinOp ((Lt|Le) as op, Lval (Var v, NoOffset), e, _) when tv -> (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with | `Lifted (Abs arg) -> - refineAbs arg e + refineAbs op arg e | _ -> refine0) | _ -> refine0 in diff --git a/tests/regression/39-signed-overflows/06-abs.c b/tests/regression/39-signed-overflows/06-abs.c index e87e25d9fe..e56cc9ff7d 100644 --- a/tests/regression/39-signed-overflows/06-abs.c +++ b/tests/regression/39-signed-overflows/06-abs.c @@ -6,7 +6,16 @@ int main() { { if (abs(data) < 100) { - int result = data * data; + __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; From 8ea9ffa726f13f0d764cf2dbd7ee6a1d18270573 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 18 Nov 2023 12:51:32 +0100 Subject: [PATCH 11/17] 39/07: Add NOWARN annotation --- tests/regression/39-signed-overflows/07-abs-sqrt.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/39-signed-overflows/07-abs-sqrt.c b/tests/regression/39-signed-overflows/07-abs-sqrt.c index 0f8ce396f2..13ed863e51 100644 --- a/tests/regression/39-signed-overflows/07-abs-sqrt.c +++ b/tests/regression/39-signed-overflows/07-abs-sqrt.c @@ -4,7 +4,7 @@ int main() { int data; if (data > (-0x7fffffff - 1) && abs(data) < (long)sqrt((double)0x7fffffff)) { - int result = data * data; + int result = data * data; //NOWARN } return 8; } \ No newline at end of file From 9d77dec344287d4ad42e723abfa5777dc3d01afc Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 20 Nov 2023 11:59:44 +0200 Subject: [PATCH 12/17] Move abs refine to BaseInvariant --- src/analyses/base.ml | 43 ++++++++--------------------------- src/analyses/baseInvariant.ml | 27 ++++++++++++++++++++++ 2 files changed, 36 insertions(+), 34 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 4911b0d033..f25f0a9693 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1753,40 +1753,15 @@ struct let branch ctx (exp:exp) (tv:bool) : store = let valu = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp in let refine () = - let refine0 = - let res = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp tv in - if M.tracing then M.tracec "branch" "EqualSet result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.EqualSet exp)); - if M.tracing then M.tracec "branch" "CondVars result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.CondVars exp)); - if M.tracing then M.traceu "branch" "Invariant enforced!\n"; - match ctx.ask (Queries.CondVars exp) with - | s when Queries.ES.cardinal s = 1 -> - let e = Queries.ES.choose s in - invariant ctx (Analyses.ask_of_ctx ctx) ctx.global res e tv - | _ -> res - 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 -> - (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with - | `Lifted (Abs arg) -> - refineAbs op (CastE (t, arg)) e - | _ -> refine0) - | BinOp ((Lt|Le) as op, Lval (Var v, NoOffset), e, _) when tv -> - (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with - | `Lifted (Abs arg) -> - refineAbs op arg e - | _ -> refine0) - | _ -> refine0 + let res = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp tv in + if M.tracing then M.tracec "branch" "EqualSet result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.EqualSet exp)); + if M.tracing then M.tracec "branch" "CondVars result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.CondVars exp)); + if M.tracing then M.traceu "branch" "Invariant enforced!\n"; + match ctx.ask (Queries.CondVars exp) with + | s when Queries.ES.cardinal s = 1 -> + let e = Queries.ES.choose s in + invariant ctx (Analyses.ask_of_ctx ctx) ctx.global res e tv + | _ -> res in if M.tracing then M.traceli "branch" ~subsys:["invariant"] "Evaluating branch for expression %a with value %a\n" d_exp exp VD.pretty valu; (* First we want to see, if we can determine a dead branch: *) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 72e00efbb1..a99e25e7c6 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 -> + (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with + | `Lifted (Abs arg) -> + refineAbs op (CastE (t, arg)) e + | _ -> refine0) + | BinOp ((Lt|Le) as op, Lval (Var v, NoOffset), e, _) when tv -> + (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with + | `Lifted (Abs arg) -> + refineAbs op arg e + | _ -> refine0) + | _ -> refine0 + end From 0cb1b7e1135fee97db9d4d7da6a90c1bc8261fa5 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 20 Nov 2023 12:04:21 +0200 Subject: [PATCH 13/17] Fix BaseInvariant abs indentation --- src/analyses/baseInvariant.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index a99e25e7c6..86ec0d3bf7 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -837,15 +837,15 @@ struct in match exp with | BinOp ((Lt|Le) as op, CastE(t, Lval (Var v, NoOffset)), e,_) when tv -> - (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with - | `Lifted (Abs arg) -> - refineAbs op (CastE (t, arg)) e - | _ -> refine0) + begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with + | `Lifted (Abs arg) -> refineAbs op (CastE (t, arg)) e + | _ -> refine0 + end | BinOp ((Lt|Le) as op, Lval (Var v, NoOffset), e, _) when tv -> - (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with - | `Lifted (Abs arg) -> - refineAbs op arg e - | _ -> refine0) + begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with + | `Lifted (Abs arg) -> refineAbs op arg e + | _ -> refine0 + end | _ -> refine0 end From 19190ca63d43aaf14ae462823b3878ce65b25606 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 20 Nov 2023 11:09:26 +0100 Subject: [PATCH 14/17] remove special cases handled by general case --- src/analyses/base.ml | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index f25f0a9693..2a729c685e 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2339,13 +2339,9 @@ struct | None, _ -> ID.top_of ik | Some mx, Some mm when Z.equal mx mm -> ID.top_of ik | _, _ -> - match ID.le xcast (ID.of_int ik Z.zero) with - | d when d = ID.of_int ik Z.zero -> xcast (* x positive *) - | d when d = ID.of_int ik Z.one -> ID.neg xcast (* x negative *) - | _ -> (* both possible *) - 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 + 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 From c9be89e68cd01a189f336f350cf8cae12c505b43 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 20 Nov 2023 19:40:40 +0100 Subject: [PATCH 15/17] add support for labs and llabs --- src/analyses/base.ml | 2 +- src/analyses/baseInvariant.ml | 4 ++-- src/analyses/libraryDesc.ml | 4 ++-- src/analyses/libraryFunctions.ml | 4 +++- .../regression/39-signed-overflows/08-labs.c | 22 +++++++++++++++++++ .../39-signed-overflows/09-labs-sqrt.c | 10 +++++++++ 6 files changed, 40 insertions(+), 6 deletions(-) create mode 100644 tests/regression/39-signed-overflows/08-labs.c create mode 100644 tests/regression/39-signed-overflows/09-labs-sqrt.c diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 2a729c685e..84be8c7a19 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2375,7 +2375,7 @@ struct | 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 x -> Int (ID.cast_to IInt (apply_abs IInt 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 86ec0d3bf7..f391231628 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -838,12 +838,12 @@ struct 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 arg) -> refineAbs op (CastE (t, arg)) e + | `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 arg) -> refineAbs op arg e + | `Lifted (Abs (ik, arg)) -> refineAbs op arg e | _ -> refine0 end | _ -> refine0 diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 8cd3dfa1ba..45887b9c6b 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -27,7 +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 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) @@ -160,7 +160,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 exp -> Pretty.dprintf "abs(%a)" d_exp exp + | 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 diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index ae33f57f70..838d1817a9 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", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs 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 *) 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; +} From 75b3b83e1500f515ca6f3c4fecb3fe4908507fca Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 20 Nov 2023 20:19:07 +0100 Subject: [PATCH 16/17] add autotuner for math functions (activates tmpSpecial and float domain) --- src/autoTune.ml | 14 ++++++++++++++ src/common/util/options.schema.json | 2 +- 2 files changed, 15 insertions(+), 1 deletion(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 7ddc1aee43..77d91f9652 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -458,6 +458,17 @@ 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 @@ -518,6 +529,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 let options = if isActivated "octagon" then (apronOctagonOption factors file)::options else options in diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index 4e282b19a4..b392f56cd6 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" ] } }, From f6c9a52fb5c9fae1564ee038fd1c8ef374fa0304 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 21 Nov 2023 12:30:35 +0100 Subject: [PATCH 17/17] Add tmpSpecialAnalysis to ana.autotune.activated in svcomp.json. --- conf/svcomp.json | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/conf/svcomp.json b/conf/svcomp.json index 73f99500b9..c915620987 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -71,7 +71,8 @@ "octagon", "wideningThresholds", "loopUnrollHeuristic", - "memsafetySpecification" + "memsafetySpecification", + "tmpSpecialAnalysis" ] } },