From 78bcaf77e359747afd694371817527fb9886371d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 18 May 2022 08:26:26 +0000
Subject: [PATCH] C library: implement getrandom

Adds a model of getrandom as available on Linux.
---
 regression/cbmc-library/getrandom-01/main.c   | 18 +++++++++++
 .../cbmc-library/getrandom-01/test.desc       |  8 +++++
 src/ansi-c/library/random.c                   | 30 +++++++++++++++++++
 3 files changed, 56 insertions(+)
 create mode 100644 regression/cbmc-library/getrandom-01/main.c
 create mode 100644 regression/cbmc-library/getrandom-01/test.desc
 create mode 100644 src/ansi-c/library/random.c

diff --git a/regression/cbmc-library/getrandom-01/main.c b/regression/cbmc-library/getrandom-01/main.c
new file mode 100644
index 00000000000..01334f7ac09
--- /dev/null
+++ b/regression/cbmc-library/getrandom-01/main.c
@@ -0,0 +1,18 @@
+#ifdef __linux__
+#  include <sys/random.h>
+
+#  include <assert.h>
+
+int main()
+{
+  char zero_bytes[6] = {0};
+  ssize_t res = getrandom(zero_bytes, 5, 0);
+  assert(res <= 5);
+  assert(zero_bytes[5] == 0);
+  return 0;
+}
+#else
+int main()
+{
+}
+#endif
diff --git a/regression/cbmc-library/getrandom-01/test.desc b/regression/cbmc-library/getrandom-01/test.desc
new file mode 100644
index 00000000000..f456d4fb459
--- /dev/null
+++ b/regression/cbmc-library/getrandom-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check --signed-overflow-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/ansi-c/library/random.c b/src/ansi-c/library/random.c
new file mode 100644
index 00000000000..9a7cff665ad
--- /dev/null
+++ b/src/ansi-c/library/random.c
@@ -0,0 +1,30 @@
+/* FUNCTION: getrandom */
+
+#ifdef __linux__
+
+#  ifndef __CPROVER_SYS_RANDOM_H_INCLUDED
+#    include <sys/random.h>
+#    define __CPROVER_SYS_RANDOM_H_INCLUDED
+#  endif
+
+#  ifndef GRND_NONBLOCK
+#    define GRND_NONBLOCK 0
+#  endif
+
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+size_t __VERIFIER_nondet_size_t();
+
+ssize_t getrandom(void *buf, size_t buflen, unsigned int flags)
+{
+  if(flags & GRND_NONBLOCK && __VERIFIER_nondet___CPROVER_bool())
+    return -1;
+
+  char bytes[buflen];
+  __CPROVER_array_replace(buf, bytes);
+
+  size_t actual_bytes = __VERIFIER_nondet_size_t();
+  __CPROVER_assume(actual_bytes <= buflen);
+  return (ssize_t)actual_bytes;
+}
+
+#endif