Handle sqrt & Some Bodged Solution for computing through abs

src/analyses/base.ml

@@ -1753,15 +1753,40 @@ 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
+      (* 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
     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: *)
@@ -2328,6 +2353,28 @@ 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
+             | _, _ ->
+               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)
@@ -2356,6 +2403,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 x -> Int (ID.cast_to IInt (apply_abs IInt x))
         end
       in
       begin match lv with

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)
@@ -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. *)
@@ -158,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
@@ -170,6 +173,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,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 *)
@@ -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" []]);

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

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;
+}