implement abs function for integers

goblint · Nov 17, 2023 · 0740491 · 0740491
1 parent 9420a08
commit 0740491
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 1 deletion.
diff --git 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
@@ -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
@@ -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 *)