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

Author: tautschnig

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);
 }

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$

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 <