C library: implement getrandom

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

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

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