From e595faf749e96cdff4df0d35444f7ff7a5c03a89 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 15 Jun 2021 15:52:12 +0000
Subject: [PATCH] C library: model rand, rand_r so as not to return negative
 numbers

The modelling remains over-approximating as we return a
non-deterministic value rather than some sequence of random numbers.
Still, we should not be returning a negative number.
---
 regression/cbmc-library/rand-01/main.c      |  9 +++++++
 regression/cbmc-library/rand-01/test.desc   |  8 ++++++
 regression/cbmc-library/rand_r-01/main.c    | 10 ++++++++
 regression/cbmc-library/rand_r-01/test.desc |  8 ++++++
 src/ansi-c/library/stdlib.c                 | 27 +++++++++++++++++++++
 5 files changed, 62 insertions(+)
 create mode 100644 regression/cbmc-library/rand-01/main.c
 create mode 100644 regression/cbmc-library/rand-01/test.desc
 create mode 100644 regression/cbmc-library/rand_r-01/main.c
 create mode 100644 regression/cbmc-library/rand_r-01/test.desc

diff --git a/regression/cbmc-library/rand-01/main.c b/regression/cbmc-library/rand-01/main.c
new file mode 100644
index 00000000000..30cb24de187
--- /dev/null
+++ b/regression/cbmc-library/rand-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  int r = rand();
+  assert(r >= 0);
+  return 0;
+}
diff --git a/regression/cbmc-library/rand-01/test.desc b/regression/cbmc-library/rand-01/test.desc
new file mode 100644
index 00000000000..96c9b4bcd7b
--- /dev/null
+++ b/regression/cbmc-library/rand-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-library/rand_r-01/main.c b/regression/cbmc-library/rand_r-01/main.c
new file mode 100644
index 00000000000..73e3ef626ff
--- /dev/null
+++ b/regression/cbmc-library/rand_r-01/main.c
@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  unsigned int seed;
+  int r = rand_r(&seed);
+  assert(r >= 0);
+  return 0;
+}
diff --git a/regression/cbmc-library/rand_r-01/test.desc b/regression/cbmc-library/rand_r-01/test.desc
new file mode 100644
index 00000000000..96c9b4bcd7b
--- /dev/null
+++ b/regression/cbmc-library/rand_r-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index a3fdda93263..d3299f883fe 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/src/ansi-c/library/stdlib.c
@@ -564,3 +564,30 @@ long random(void)
   __CPROVER_assume(result>=0 && result<=2147483647);
   return result;
 }
+
+/* FUNCTION: rand */
+
+int __VERIFIER_nondet_int();
+
+int rand(void)
+{
+__CPROVER_HIDE:;
+  // We return a non-deterministic value instead of a random one.
+  int result = __VERIFIER_nondet_int();
+  __CPROVER_assume(result >= 0);
+  return result;
+}
+
+/* FUNCTION: rand_r */
+
+int __VERIFIER_nondet_int();
+
+int rand_r(unsigned int *seed)
+{
+__CPROVER_HIDE:;
+  // We return a non-deterministic value instead of a random one.
+  (void)*seed;
+  int result = __VERIFIER_nondet_int();
+  __CPROVER_assume(result >= 0);
+  return result;
+}