Merge pull request #1254 from goblint/no-overflow-sqrt-pfusch

Handle `sqrt` & Some Bodged Solution for computing through `abs`

conf/svcomp.json

@@ -72,6 +72,7 @@
         "wideningThresholds",
         "loopUnrollHeuristic",
         "memsafetySpecification",
+        "tmpSpecialAnalysis",
         "termination"
       ]
     }

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

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

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

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" []]);

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. *)

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 ()) =

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)) *)

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"
 

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
 

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)   \
     {                                                            \

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"
               ]
             }
           },

tests/regression/39-signed-overflows/06-abs.c

@@ -0,0 +1,22 @@
+//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial
+#include<math.h>
+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;
+}

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<math.h>
+int main() {
+    int data;
+    if (data > (-0x7fffffff - 1) && abs(data) < (long)sqrt((double)0x7fffffff))
+    {
+        int result = data * data; //NOWARN
+    }
+    return 8;
+}

tests/regression/39-signed-overflows/08-labs.c

@@ -0,0 +1,22 @@
+//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial
+#include<stdlib.h>
+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;
+}

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<math.h>
+int main() {
+    int data;
+    if (data > (-0x7fffffff - 1) && llabs(data) < (long)sqrt((double)0x7fffffff))
+    {
+        int result = data * data; //NOWARN
+    }
+    return 8;
+}