Adds an over-approximation for syscall function

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

regression/cbmc-library/syscall-01/main.c

@@ -0,0 +1,17 @@
+#include <sys/syscall.h>
+
+#include <assert.h>
+#include <errno.h>
+#include <unistd.h>
+
+int main()
+{
+  long int rc;
+  errno = 0;
+  rc = syscall(SYS_chmod, "/etc/passwd", 0444);
+  assert(!(rc != -1) || (errno == 0));
+
+  pid_t tid;
+  // arithmetic overflow
+  tid = syscall(SYS_gettid);
+}

regression/cbmc-library/syscall-01/test.desc

@@ -0,0 +1,11 @@
+CORE unix
+main.c
+--pointer-check --bounds-check --conversion-check
+^\[main.assertion.\d+\] line \d+ assertion !\(rc != -1\) || \(errno == 0\): SUCCESS$
+^\[main.overflow.\d+\] line \d+ arithmetic overflow on signed type conversion in \(pid\_t\)return\_value\_syscall: FAILURE$
+^\*\* 1 of \d+ failed .*$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^\*\*\*\* WARNING: no body for function syscall

src/ansi-c/library/unistd.c

@@ -385,3 +385,42 @@ __CPROVER_HIDE:;
   // Thus, modelling it as non-deterministic.
   return retval;
 }
+
+/* FUNCTION: syscall */
+
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
+long int __VERIFIER_nondet_long_int(void);
+int __VERIFIER_nondet_int(void);
+
+long int syscall(long int sysno, ...);
+
+// This overapproximation is based on the syscall specification available at
+// https://man7.org/linux/man-pages/man2/syscall.2.html and
+// https://www.gnu.org/software/libc/manual/html_node/System-Calls.html.
+//
+// sysno is the system call number. The remaining arguments are the arguments
+// for the system call. Each kind of system call has a definite number of
+// arguments, from zero to five. If you code more arguments than the system
+// call takes, the extra ones to the right are ignored.
+long int syscall(long int sysno, ...)
+{
+__CPROVER_HIDE:;
+  (void)sysno;
+  long int retval = __VERIFIER_nondet_long_int();
+
+  if(retval == -1)
+  {
+    // We should keep errno as non-deterministic as possible, since this model
+    // never takes into account any input.
+    errno = __VERIFIER_nondet_int();
+  }
+
+  // The return value is the return value from the system call, unless the
+  // system call failed. This over-approximation doesn't take into account
+  // any system call operation, so we leave the return value as non-det.
+  return retval;
+}