[Libc] add better requires for writev; improve test case

share/libc/sys/uio.h

@@ -38,8 +38,8 @@ __BEGIN_DECLS
 /*@
   requires valid_fd: 0 <= fd < __FC_MAX_OPEN_FILES;
   requires initialization:initialized_inputs:
-     \forall integer i; 0 <= i < iovcnt ==>
-    \initialized(&iov[i].iov_base) && \initialized(&iov[i].iov_len);
+    \forall integer i; 0 <= i < iovcnt ==>
+      \initialized(&iov[i].iov_base) && \initialized(&iov[i].iov_len);
   requires valid_iov: \forall integer i; 0 <= i < iovcnt ==>
     \valid( ((char*)&iov[i].iov_base)+(0 .. iov[i].iov_len-1));
   requires bounded_iovcnt: 0 <= iovcnt <= IOV_MAX;
@@ -57,8 +57,11 @@ extern ssize_t readv(int fd, const struct iovec *iov, int iovcnt);
   requires valid_fd: 0 <= fd < __FC_MAX_OPEN_FILES;
   requires initialization:initialized_inputs:
     \forall integer i; 0 <= i < iovcnt ==>
-    \initialized(&iov[i].iov_base) && \initialized(&iov[i].iov_len);
+      \initialized(&iov[i].iov_base) && \initialized(&iov[i].iov_len);
   requires valid_read_iov: \valid_read(&iov[0 .. iovcnt-1]);
+  requires valid_read_iov_bases:
+    \forall integer i; 0 <= i < iovcnt ==>
+      \valid_read(((char*)iov[i].iov_base) + (0 .. iov[i].iov_len-1));
   requires bounded_iovcnt: 0 <= iovcnt <= IOV_MAX;
   requires bounded_lengths:
      \sum(0, iovcnt-1, \lambda integer k; iov[k].iov_len) <= SSIZE_MAX;

tests/libc/oracle/fc_libc.1.res.oracle

@@ -4559,6 +4559,12 @@ extern ssize_t readv(int fd, struct iovec const *iov, int iovcnt);
           \initialized(&(iov + i)->iov_base) ∧
           \initialized(&(iov + i)->iov_len);
     requires valid_read_iov: \valid_read(iov + (0 .. iovcnt - 1));
+    requires
+      valid_read_iov_bases:
+        ∀ ℤ i;
+          0 ≤ i < iovcnt ⇒
+          \valid_read((char *)(iov + i)->iov_base +
+                      (0 .. (iov + i)->iov_len - 1));
     requires bounded_iovcnt: 0 ≤ iovcnt ≤ 1024;
     requires
       bounded_lengths:

tests/libc/oracle/sys_uio_h.res.oracle

@@ -3,65 +3,92 @@
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
-  
+  nondet ∈ [--..--]
 [eva] computing for function __va_open_mode_t <- main.
   Called from tests/libc/sys_uio_h.c:17.
 [eva] using specification for function __va_open_mode_t
 [eva] tests/libc/sys_uio_h.c:17: 
   function __va_open_mode_t: precondition 'valid_filename' got status valid.
 [eva] Done for function __va_open_mode_t
+[eva] tests/libc/sys_uio_h.c:19: assertion got status valid.
+[eva] tests/libc/sys_uio_h.c:20: assertion got status valid.
+[eva] tests/libc/sys_uio_h.c:21: assertion got status valid.
 [eva] computing for function writev <- main.
-  Called from tests/libc/sys_uio_h.c:19.
+  Called from tests/libc/sys_uio_h.c:22.
 [eva] using specification for function writev
-[eva] tests/libc/sys_uio_h.c:19: 
+[eva] tests/libc/sys_uio_h.c:22: 
   function writev: precondition 'valid_fd' got status valid.
-[eva] tests/libc/sys_uio_h.c:19: 
+[eva] tests/libc/sys_uio_h.c:22: 
   function writev: precondition 'initialization,initialized_inputs' got status valid.
-[eva] tests/libc/sys_uio_h.c:19: 
+[eva] tests/libc/sys_uio_h.c:22: 
   function writev: precondition 'valid_read_iov' got status valid.
-[eva] tests/libc/sys_uio_h.c:19: 
+[eva:alarm] tests/libc/sys_uio_h.c:22: Warning: 
+  function writev: precondition 'valid_read_iov_bases' got status unknown.
+[eva] tests/libc/sys_uio_h.c:22: 
   function writev: precondition 'bounded_iovcnt' got status valid.
-[eva] share/libc/sys/uio.h:64: 
+[eva] share/libc/sys/uio.h:67: 
   cannot evaluate ACSL term, unsupported ACSL construct: logic function \sum
-[eva:alarm] tests/libc/sys_uio_h.c:19: Warning: 
+[eva:alarm] tests/libc/sys_uio_h.c:22: Warning: 
   function writev: precondition 'bounded_lengths' got status unknown.
-[eva] share/libc/sys/uio.h:69: 
+[eva] share/libc/sys/uio.h:72: 
   cannot evaluate ACSL term, unsupported ACSL construct: logic function \sum
 [eva] Done for function writev
 [eva] computing for function close <- main.
-  Called from tests/libc/sys_uio_h.c:20.
+  Called from tests/libc/sys_uio_h.c:23.
 [eva] using specification for function close
-[eva] tests/libc/sys_uio_h.c:20: 
+[eva] tests/libc/sys_uio_h.c:23: 
   function close: precondition 'valid_fd' got status valid.
 [eva] Done for function close
 [eva] computing for function __va_open_void <- main.
-  Called from tests/libc/sys_uio_h.c:21.
+  Called from tests/libc/sys_uio_h.c:24.
 [eva] using specification for function __va_open_void
-[eva] tests/libc/sys_uio_h.c:21: 
+[eva] tests/libc/sys_uio_h.c:24: 
   function __va_open_void: precondition 'valid_filename' got status valid.
-[eva] tests/libc/sys_uio_h.c:21: 
+[eva] tests/libc/sys_uio_h.c:24: 
   function __va_open_void: precondition 'flag_not_CREAT' got status valid.
 [eva] Done for function __va_open_void
 [eva] computing for function readv <- main.
-  Called from tests/libc/sys_uio_h.c:22.
+  Called from tests/libc/sys_uio_h.c:25.
 [eva] using specification for function readv
-[eva:alarm] tests/libc/sys_uio_h.c:22: Warning: 
+[eva:alarm] tests/libc/sys_uio_h.c:25: Warning: 
   function readv: precondition 'valid_fd' got status unknown.
-[eva] tests/libc/sys_uio_h.c:22: 
+[eva] tests/libc/sys_uio_h.c:25: 
   function readv: precondition 'initialization,initialized_inputs' got status valid.
-[eva:alarm] tests/libc/sys_uio_h.c:22: Warning: 
+[eva:alarm] tests/libc/sys_uio_h.c:25: Warning: 
   function readv: precondition 'valid_iov' got status unknown.
-[eva] tests/libc/sys_uio_h.c:22: 
+[eva] tests/libc/sys_uio_h.c:25: 
   function readv: precondition 'bounded_iovcnt' got status valid.
 [eva] share/libc/sys/uio.h:52: 
   cannot evaluate ACSL term, unsupported ACSL construct: logic function \sum
 [eva] Done for function readv
 [eva] computing for function close <- main.
-  Called from tests/libc/sys_uio_h.c:23.
-[eva] tests/libc/sys_uio_h.c:23: 
+  Called from tests/libc/sys_uio_h.c:26.
+[eva] tests/libc/sys_uio_h.c:26: 
   function close: precondition 'valid_fd' got status valid.
 [eva] Done for function close
-[eva:alarm] tests/libc/sys_uio_h.c:24: Warning: 
+[eva] computing for function __va_open_mode_t <- main.
+  Called from tests/libc/sys_uio_h.c:37.
+[eva] tests/libc/sys_uio_h.c:37: 
+  function __va_open_mode_t: precondition 'valid_filename' got status valid.
+[eva] Done for function __va_open_mode_t
+[eva] computing for function writev <- main.
+  Called from tests/libc/sys_uio_h.c:39.
+[eva] tests/libc/sys_uio_h.c:39: 
+  function writev: precondition 'valid_fd' got status valid.
+[eva] tests/libc/sys_uio_h.c:39: 
+  function writev: precondition 'initialization,initialized_inputs' got status valid.
+[eva] tests/libc/sys_uio_h.c:39: 
+  function writev: precondition 'valid_read_iov' got status valid.
+[eva:alarm] tests/libc/sys_uio_h.c:39: Warning: 
+  function writev: precondition 'valid_read_iov_bases' got status unknown.
+[eva] tests/libc/sys_uio_h.c:39: 
+  function writev: precondition 'bounded_iovcnt' got status valid.
+[eva:alarm] tests/libc/sys_uio_h.c:39: Warning: 
+  function writev: precondition 'bounded_lengths' got status unknown.
+[eva] Done for function writev
+[eva:alarm] tests/libc/sys_uio_h.c:40: Warning: 
+  assertion 'unreachable' got status invalid (stopping propagation).
+[eva:alarm] tests/libc/sys_uio_h.c:43: Warning: 
   signed overflow. assert w + r ≤ 2147483647;
 [eva] Recording results for main
 [eva] done for function main

tests/libc/sys_uio_h.c

 #include <sys/uio.h>
 #include <unistd.h>
 #include <fcntl.h>
-
+volatile int nondet;
 int main() {
   char *str = "A small string";
   char *empty_buf = 0;
@@ -16,10 +16,29 @@ int main() {
     };
   int fd = open("/tmp/uio.txt", O_WRONLY | O_CREAT, 0660);
   if (fd < 0) return 1;
+  //@ assert \valid_read(((char*)v[0].iov_base) + (0 .. v[0].iov_len-1));
+  //@ assert \valid_read(((char*)v[1].iov_base) + (0 .. v[1].iov_len-1));
+  //@ assert \valid_read(((char*)v[2].iov_base) + (0 .. v[2].iov_len-1));
   ssize_t w = writev(fd, v, 3);
   close(fd);
   fd = open("/tmp/uio.txt", O_RDONLY);
   ssize_t r = readv(fd, v+2, 2);
   close(fd);
+
+  if (nondet) {
+    char buf3[10] = "\n\n\nbuffer";
+    char buf4[14];
+    struct iovec v2[4] =
+      {
+        {str, 15},
+        {empty_buf, 0},
+        {buf3, 11}, // invalid length
+      };
+    int fd2 = open("/tmp/uio2.txt", O_WRONLY | O_CREAT, 0660);
+    if (fd2 < 0) return 1;
+    ssize_t w = writev(fd2, v2, 3); // must fail
+    //@ assert unreachable: \false;
+  }
+
   return w + r;
 }