Merge pull request #7365 from tautschnig/bugfixes/5570-unistd

C library: Avoid arithmetic overflow with pipe operations

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 <