Merge pull request #1772 from tautschnig/fix-1771

Bounds checks in fgets, read

Author: kroening

regression/cbmc/fgets1/test.desc

@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 \[main.assertion.3\] assertion p\[1\]=='b': FAILURE
-\*\* 1 of \d+ failed 
+\*\* 2 of \d+ failed
 --
 ^warning: ignoring

regression/cbmc/read1/main.c

@@ -0,0 +1,19 @@
+#ifdef _WIN32
+#include <io.h>
+#else
+#include <unistd.h>
+#endif
+
+#include <stdio.h>
+
+int main()
+{
+	char data[20];
+
+	if(read(0, data, 100) < 0)
+		printf("An error has occurred");
+	else
+		printf("Read occurred");
+
+	return 0;
+}

regression/cbmc/read1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--bounds-check --pointer-check --unwind 100
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[.*] dereference failure: pointer outside object bounds in .*: FAILURE
+\*\* 1 of .* failed \(.*\)
+--
+^warning: ignoring

src/ansi-c/library/stdio.c

@@ -247,6 +247,9 @@ char *fgets(char *str, int size, FILE *stream)
   {
     int str_length=__VERIFIER_nondet_int();
     __CPROVER_assume(str_length>=0 && str_length<size);
+    // check that the memory is accessible
+    (void)*(char *)str;
+    (void)*(((const char *)str) + str_length - 1);
     char contents_nondet[str_length];
     __CPROVER_array_replace(str, contents_nondet);
     if(!error)

src/ansi-c/library/unistd.c

@@ -123,27 +123,30 @@ inline int _close(int fildes)
 // write to _write; this is covered by the explicit definition of
 // _write below
 #ifdef _MSC_VER
-#define ssize_t signed long
+#define ret_type int
+#define size_type unsigned
 #else
 #ifndef __CPROVER_SYS_TYPES_H_INCLUDED
 #include <sys/types.h>
 #define __CPROVER_SYS_TYPES_H_INCLUDED
 #endif
+#define ret_type ssize_t
+#define size_type size_t
 #endif
 
 extern struct __CPROVER_pipet __CPROVER_pipes[];
 // offset to make sure we don't collide with other fds
 extern const int __CPROVER_pipe_offset;
 
-ssize_t __VERIFIER_nondet_ssize_t();
+ret_type __VERIFIER_nondet_ret_type();
 
-ssize_t write(int fildes, const void *buf, size_t nbyte)
+ret_type write(int fildes, const void *buf, size_type nbyte)
 {
   __CPROVER_HIDE:;
   if((fildes>=0 && fildes<=2) || fildes < __CPROVER_pipe_offset)
   {
-    ssize_t retval=__VERIFIER_nondet_ssize_t();
-    __CPROVER_assume(retval>=-1 && retval<=(ssize_t)nbyte);
+    ret_type retval=__VERIFIER_nondet_ret_type();
+    __CPROVER_assume(retval>=-1 && retval<=(ret_type)nbyte);
     return retval;
   }
 
@@ -156,7 +159,7 @@ ssize_t write(int fildes, const void *buf, size_t nbyte)
       sizeof(__CPROVER_pipes[fildes].data) >=
       __CPROVER_pipes[fildes].next_avail+nbyte)
   {
-    for(size_t i=0; i<nbyte; ++i)
+    for(size_type i=0; i<nbyte; ++i)
       __CPROVER_pipes[fildes].data[i+__CPROVER_pipes[fildes].next_avail]=
         ((char*)buf)[i];
     __CPROVER_pipes[fildes].next_avail+=nbyte;
@@ -169,17 +172,20 @@ ssize_t write(int fildes, const void *buf, size_t nbyte)
 /* FUNCTION: _write */
 
 #ifdef _MSC_VER
-#define ssize_t signed long
+#define ret_type int
+#define size_type unsigned
 #else
 #ifndef __CPROVER_SYS_TYPES_H_INCLUDED
 #include <sys/types.h>
 #define __CPROVER_SYS_TYPES_H_INCLUDED
 #endif
+#define ret_type ssize_t
+#define size_type size_t
 #endif
 
-ssize_t write(int fildes, const void *buf, size_t nbyte);
+ret_type write(int fildes, const void *buf, size_type nbyte);
 
-inline ssize_t _write(int fildes, const void *buf, size_t nbyte)
+inline ret_type _write(int fildes, const void *buf, size_type nbyte)
 {
   __CPROVER_HIDE:;
   return write(fildes, buf, nbyte);
@@ -191,42 +197,54 @@ inline ssize_t _write(int fildes, const void *buf, size_t nbyte)
 // read to _read; this is covered by the explicit definition of _read
 // below
 #ifdef _MSC_VER
-#define ssize_t signed long
+#define ret_type int
+#define size_type unsigned
 #else
 #ifndef __CPROVER_SYS_TYPES_H_INCLUDED
 #include <sys/types.h>
 #define __CPROVER_SYS_TYPES_H_INCLUDED
 #endif
+#define ret_type ssize_t
+#define size_type size_t
 #endif
 
 extern struct __CPROVER_pipet __CPROVER_pipes[];
 // offset to make sure we don't collide with other fds
 extern const int __CPROVER_pipe_offset;
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
-ssize_t __VERIFIER_nondet_ssize_t();
+ret_type __VERIFIER_nondet_ret_type();
+size_type __VERIFIER_nondet_size_type();
 
-ssize_t read(int fildes, void *buf, size_t nbyte)
+ret_type read(int fildes, void *buf, size_type nbyte)
 {
   __CPROVER_HIDE:;
   if((fildes>=0 && fildes<=2) || fildes < __CPROVER_pipe_offset)
   {
-    ssize_t nread=__VERIFIER_nondet_ssize_t();
-    __CPROVER_assume(0<=nread && (size_t)nread<=nbyte);
+    ret_type nread=__VERIFIER_nondet_ret_type();
+    __CPROVER_assume(0<=nread && (size_type)nread<=nbyte);
 
+    __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
 #if 0
-    size_t i;
+    size_type i;
     for(i=0; i<nbyte; i++)
     {
       char nondet_char;
       ((char *)buf)[i]=nondet_char;
     }
 #else
-    char nondet_bytes[nbyte];
-    __CPROVER_array_replace((char*)buf, nondet_bytes);
+    if(nbyte>0)
+    {
+      size_type str_length=__VERIFIER_nondet_size_type();
+      __CPROVER_assume(error ? str_length<=nbyte : str_length==nbyte);
+      // check that the memory is accessible
+      (void)*(char *)buf;
+      (void)*(((const char *)buf) + str_length - 1);
+      char contents_nondet[str_length];
+      __CPROVER_array_replace((char*)buf, contents_nondet);
+    }
 #endif
 
-    __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
     return error ? -1 : nread;
   }
 
@@ -237,7 +255,7 @@ ssize_t read(int fildes, void *buf, size_t nbyte)
   __CPROVER_atomic_begin();
   if(!__CPROVER_pipes[fildes].widowed)
   {
-    for(size_t i=0; i<nbyte &&
+    for(size_type i=0; i<nbyte &&
       __CPROVER_pipes[fildes].next_unread <
       __CPROVER_pipes[fildes].next_avail;
       ++i)
@@ -258,17 +276,20 @@ ssize_t read(int fildes, void *buf, size_t nbyte)
 /* FUNCTION: _read */
 
 #ifdef _MSC_VER
-#define ssize_t signed long
+#define ret_type int
+#define size_type unsigned
 #else
 #ifndef __CPROVER_SYS_TYPES_H_INCLUDED
 #include <sys/types.h>
 #define __CPROVER_SYS_TYPES_H_INCLUDED
 #endif
+#define ret_type ssize_t
+#define size_type size_t
 #endif
 
-ssize_t read(int fildes, void *buf, size_t nbyte);
+ret_type read(int fildes, void *buf, size_type nbyte);
 
-inline ssize_t _read(int fildes, void *buf, size_t nbyte)
+inline ret_type _read(int fildes, void *buf, size_type nbyte)
 {
   __CPROVER_HIDE:;
   return read(fildes, buf, nbyte);