From 06c95d694e9bea24737434f4e24aa6ece98d8600 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 21 Nov 2022 14:26:41 +0000
Subject: [PATCH] C library: Avoid arithmetic overflow with pipe operations

We may be trying to access file descriptors that haven't been fully
initialised. Don't yield spurious arithmetic overflows (that are just
caused by our modelling) in such situations.

Fixes: #5570
---
 regression/cbmc-library/write-01/main.c    | 17 +++++++++++++----
 regression/cbmc-library/write-01/test.desc |  4 ++--
 src/ansi-c/library/unistd.c                | 19 +++++++++++++++----
 3 files changed, 30 insertions(+), 10 deletions(-)

diff --git a/regression/cbmc-library/write-01/main.c b/regression/cbmc-library/write-01/main.c
index 5f774eb6e17..cc7c90ddddb 100644
--- a/regression/cbmc-library/write-01/main.c
+++ b/regression/cbmc-library/write-01/main.c
@@ -1,9 +1,18 @@
-#include <assert.h>
+#include <limits.h>
 #include <unistd.h>
 
+extern const __CPROVER_size_t SIZE;
+
 int main()
 {
-  write();
-  assert(0);
-  return 0;
+  __CPROVER_assume(SIZE < SSIZE_MAX);
+
+  int fd;
+  char ptr[SIZE];
+  __CPROVER_size_t nbytes;
+
+  __CPROVER_assume(fd >= 0);
+  __CPROVER_assume(nbytes < SIZE);
+
+  write(fd, ptr, nbytes);
 }
diff --git a/regression/cbmc-library/write-01/test.desc b/regression/cbmc-library/write-01/test.desc
index 9542d988e8d..741451e9924 100644
--- a/regression/cbmc-library/write-01/test.desc
+++ b/regression/cbmc-library/write-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE unix
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --conversion-check --unwind 1
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c
index d4bc309954f..333cfc2a045 100644
--- a/src/ansi-c/library/unistd.c
+++ b/src/ansi-c/library/unistd.c
@@ -63,6 +63,7 @@ int pipe(int fildes[2])
   }
 
   __CPROVER_atomic_begin();
+  __CPROVER_assume(__CPROVER_pipe_offset >= 0);
   __CPROVER_assume(__CPROVER_pipe_offset%2==0);
   __CPROVER_assume(__CPROVER_pipe_offset<=(int)(__CPROVER_pipe_offset+__CPROVER_pipe_count));
   fildes[0]=__CPROVER_pipe_offset+__CPROVER_pipe_count;
@@ -106,6 +107,8 @@ int close(int fildes)
   if((fildes>=0 && fildes<=2) || fildes < __CPROVER_pipe_offset)
     return 0;
 
+  __CPROVER_assume(__CPROVER_pipe_offset >= 0);
+
   int retval=-1;
   fildes-=__CPROVER_pipe_offset;
   if(fildes%2==1)
@@ -164,14 +167,18 @@ ret_type write(int fildes, const void *buf, size_type nbyte)
     return retval;
   }
 
+  __CPROVER_assume(__CPROVER_pipe_offset >= 0);
+
   int retval=-1;
   fildes-=__CPROVER_pipe_offset;
   if(fildes%2==1)
     --fildes;
   __CPROVER_atomic_begin();
-  if(!__CPROVER_pipes[fildes].widowed &&
-      sizeof(__CPROVER_pipes[fildes].data) >=
-      __CPROVER_pipes[fildes].next_avail+nbyte)
+  if(
+    !__CPROVER_pipes[fildes].widowed &&
+    __CPROVER_pipes[fildes].next_avail >= 0 &&
+    sizeof(__CPROVER_pipes[fildes].data) >=
+      __CPROVER_pipes[fildes].next_avail + nbyte)
   {
     for(size_type i=0; i<nbyte; ++i)
       __CPROVER_pipes[fildes].data[i+__CPROVER_pipes[fildes].next_avail]=
@@ -262,12 +269,16 @@ ret_type read(int fildes, void *buf, size_type nbyte)
     return error ? -1 : nread;
   }
 
+  __CPROVER_assume(__CPROVER_pipe_offset >= 0);
+
   int retval=0;
   fildes-=__CPROVER_pipe_offset;
   if(fildes%2==1)
     --fildes;
   __CPROVER_atomic_begin();
-  if(!__CPROVER_pipes[fildes].widowed)
+  if(
+    !__CPROVER_pipes[fildes].widowed &&
+    __CPROVER_pipes[fildes].next_unread >= 0)
   {
     for(size_type i=0; i<nbyte &&
       __CPROVER_pipes[fildes].next_unread <