From 830a60f99d62ac2f665aea52935e214ea4ed3ba9 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Thu, 22 Jun 2023 20:42:36 +0000
Subject: [PATCH] Adds an over-approximation model for sysconf

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 regression/cbmc-library/sysconf-01/main.c    | 27 +++++++++++++++++
 regression/cbmc-library/sysconf-01/test.desc | 12 ++++++++
 src/ansi-c/library/unistd.c                  | 31 ++++++++++++++++++++
 3 files changed, 70 insertions(+)
 create mode 100644 regression/cbmc-library/sysconf-01/main.c
 create mode 100644 regression/cbmc-library/sysconf-01/test.desc

diff --git a/regression/cbmc-library/sysconf-01/main.c b/regression/cbmc-library/sysconf-01/main.c
new file mode 100644
index 00000000000..59f08ef24b9
--- /dev/null
+++ b/regression/cbmc-library/sysconf-01/main.c
@@ -0,0 +1,27 @@
+#include <errno.h>
+#include <unistd.h>
+
+main()
+{
+  long result;
+  int name;
+
+  errno = 0;
+  // Testing sysconf as an over-apporximation.
+  // We expect to cover all branches, thus, all assertions should fail.
+  if((result = sysconf(name)) == -1)
+  {
+    if(errno == 0)
+    {
+      __CPROVER_assert(0, "ARG_MAX is not supported");
+    }
+    else
+    {
+      __CPROVER_assert(0, "sysconf() error");
+    }
+  }
+  else
+  {
+    __CPROVER_assert(0, "ARG_MAX is supported");
+  }
+}
diff --git a/regression/cbmc-library/sysconf-01/test.desc b/regression/cbmc-library/sysconf-01/test.desc
new file mode 100644
index 00000000000..49ed341331a
--- /dev/null
+++ b/regression/cbmc-library/sysconf-01/test.desc
@@ -0,0 +1,12 @@
+CORE unix
+main.c
+
+^\[main.assertion.\d+\] line \d+ ARG\_MAX is not supported: FAILURE$
+^\[main.assertion.\d+\] line \d+ sysconf\(\) error: FAILURE$
+^\[main.assertion.\d+\] line \d+ ARG\_MAX is supported: FAILURE$
+^\*\* 3 of 3 failed .*$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^WARNING: no body for function sysconf
diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c
index 8563c41f020..dc2983ba748 100644
--- a/src/ansi-c/library/unistd.c
+++ b/src/ansi-c/library/unistd.c
@@ -319,3 +319,34 @@ ret_type _read(int fildes, void *buf, size_type nbyte)
   __CPROVER_HIDE:;
   return read(fildes, buf, nbyte);
 }
+
+/* FUNCTION: sysconf */
+
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
+long __VERIFIER_nondet_long(void);
+unsigned int __VERIFIER_nondet_unsigned_int(void);
+
+long sysconf(int name);
+
+// This overapproximation is based on the sysconf specification available at
+// https://pubs.opengroup.org/onlinepubs/9699919799/functions/sysconf.html.
+long sysconf(int name)
+{
+__CPROVER_HIDE:;
+  (void)name;
+  long retval = __VERIFIER_nondet_long();
+
+  // We should keep errno as non-determinist as possible, since this model
+  // nver takes into account the name input.
+  errno = __VERIFIER_nondet_unsigned_int();
+
+  // Spec states "some returned values may be huge; they are not suitable
+  // for allocating memory". There aren't also guarantees about return
+  // values being strickly equal or greater to -1.
+  // Thus, modelling it as non-deterministic.
+  return retval;
+}