Merge pull request #1107 from goblint/issue_1088

Add special function for `rand()` to improve precision

src/analyses/apron/relationAnalysis.apron.ml

@@ -507,6 +507,12 @@ struct
     | Unknown, "__goblint_assume_join" ->
       let id = List.hd args in
       Priv.thread_join ~force:true ask ctx.global id st
+    | Rand, _ ->
+      (match r with
+       | Some lv ->
+         let st = invalidate_one ask ctx st lv in
+         assert_fn {ctx with local = st} (BinOp (Ge, Lval lv, zero, intType)) true
+       | None -> st)
     | _, _ ->
       let lvallist e =
         let s = ask.f (Queries.MayPointTo e) in

src/analyses/base.ml

@@ -2346,6 +2346,13 @@ struct
       let rv = ensure_not_zero @@ eval_rv ask ctx.global ctx.local value in
       let t = Cilfacade.typeOf value in
       set ~ctx ~t_override:t ask ctx.global ctx.local (AD.of_var !longjmp_return) t rv (* Not raising Deadcode here, deadcode is raised at a higher level! *)
+    | Rand, _ ->
+      begin match lv with
+      | Some x -> 
+        let result:value = (Int (ID.starting IInt Z.zero)) in
+        set ~ctx (Analyses.ask_of_ctx ctx) gs st (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st x) (Cilfacade.typeOfLval x) result
+      | None -> st
+      end
     | _, _ ->
       let st =
         special_unknown_invalidate ctx (Analyses.ask_of_ctx ctx) gs st f args

src/analyses/libraryDesc.ml

@@ -72,6 +72,7 @@ type special =
   | Identity of Cil.exp (** Identity function. Some compiler optimization annotation functions map to this. *)
   | Setjmp of { env: Cil.exp; }
   | Longjmp of { env: Cil.exp; value: Cil.exp; }
+  | Rand
   | Unknown (** Anything not belonging to other types. *) (* TODO: rename to Other? *)
 
 

src/analyses/libraryFunctions.ml

@@ -70,6 +70,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
     ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env });
     ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
+    ("rand", special [] Rand);
   ]
 
 (** C POSIX library functions.
@@ -872,7 +873,6 @@ let invalidate_actions = [
     "sendto", writes [2;4]; (*keep [2;4]*)
     "recvfrom", writes [4;5]; (*keep [4;5]*)
     "srand", readsAll; (*safe*)
-    "rand", readsAll; (*safe*)
     "gethostname", writesAll; (*unsafe*)
     "fork", readsAll; (*safe*)
     "setrlimit", readsAll; (*safe*)

tests/regression/01-cpa/74-rand.c

@@ -0,0 +1,12 @@
+//PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <goblint.h>
+
+int main () {
+  int r = rand();
+
+  __goblint_check(r >= 0);
+
+  return 0;
+}

tests/regression/46-apron2/57-rand.c

@@ -0,0 +1,11 @@
+// SKIP PARAM: --disable ana.int.def_exc --enable ana.int.congruence --set ana.activated[+] apron --set ana.base.privatization none --set ana.relation.privatization top
+// Strange int domains, I know: The ranges of def_exc are already able to prove this assertion, meaning it is no longer about apron also knowing this.
+// Disabling all int domains leads to all queries returning top though, meaning the assertion is not proven.
+// Congruence offers support for constants, but does not contain any poor man's intervals. => That's why we use it here.
+#include <goblint.h>
+#include <stdlib.h>
+
+int main() {
+    int i = rand();
+    __goblint_check(i >= 0);
+}