[Libc] add specs for sendto and recvfrom

share/libc/sys/socket.h

@@ -443,8 +443,29 @@ extern int listen(int sockfd, int backlog);
  */
 extern ssize_t recv(int sockfd, void * buf, size_t len, int flags);
 
-extern ssize_t recvfrom(int, void *, size_t, int,
-        struct sockaddr *, socklen_t *);
+
+/*@
+  requires valid_sockfd: 0 <= sockfd < __FC_MAX_OPEN_SOCKETS;
+  requires valid_buffer_length: \valid((char *)buf+(0 .. len-1));
+  requires valid_addrbuf_or_null: (\valid(addrbuf_len) &&
+                                   \initialized(addrbuf_len) &&
+                                   \valid((char *)addrbuf+(0 .. *addrbuf_len-1)))
+                                  || (addrbuf == \null && addrbuf_len == \null);
+  assigns *((char *)buf+(0 .. len-1)), __fc_sockfds[sockfd], \result
+          \from sockfd, len, flags, __fc_sockfds[sockfd];
+  assigns *addrbuf_len \from indirect:sockfd, indirect: len,
+                             indirect:flags, __fc_sockfds[sockfd];
+  assigns *((char *)addrbuf+(0 .. \old(*addrbuf_len)-1))
+          \from indirect:sockfd, indirect: len,
+                         indirect:flags, __fc_sockfds[sockfd];
+  ensures result_error_or_received_length: \result == -1 || 0 <= \result <= len;
+  ensures initialization:buf: \initialized(((char *)buf+(0 .. \result-1)));
+  ensures initialization:addrbuf:
+          addrbuf != \null ==>
+            \initialized(((char *)addrbuf+(0 .. \old(*addrbuf_len)-1)));
+*/
+extern ssize_t recvfrom(int sockfd, void *buf, size_t len, int flags,
+                        struct sockaddr *addrbuf, socklen_t *addrbuf_len);
 
 /*@ requires valid_sockfd: 0 <= sockfd < __FC_MAX_OPEN_SOCKETS;
   @ requires msg_control_has_room:
@@ -483,8 +504,22 @@ extern ssize_t recvmsg(int sockfd, struct msghdr *hdr, int flags);
  */
 extern ssize_t send(int sockfd, const void *buf, size_t len, int flags);
 extern ssize_t sendmsg(int, const struct msghdr *, int);
-extern ssize_t sendto(int, const void *, size_t, int, const struct sockaddr *,
-        socklen_t);
+
+/*@
+  requires available_sockfd: 0 <= sockfd < __FC_MAX_OPEN_SOCKETS;
+  requires buf_len_ok: \valid_read(((char*)buf)+(0 .. len - 1));
+  assigns errno
+    \from indirect:sockfd, indirect:__fc_sockfds[sockfd],
+          indirect:((char *)buf)[0..len], flags;
+  assigns __fc_sockfds[sockfd]
+    \from __fc_sockfds[sockfd], ((char *)buf)[0..len], flags;
+  assigns \result
+    \from indirect:sockfd, indirect:__fc_sockfds[sockfd],
+          indirect:((char*)buf)[0..len], indirect:flags;
+  ensures error_or_chars_sent: \result == -1 || 0 <= \result <= len;
+ */
+extern ssize_t sendto(int sockfd, const void *buf, size_t len, int flags,
+                      const struct sockaddr *address, socklen_t address_len);
 
 /*@
   requires valid_sockfd: 0 <= sockfd < __FC_MAX_OPEN_SOCKETS;

tests/libc/oracle/fc_libc.0.res.oracle

 [kernel] Parsing tests/libc/fc_libc.c (with preprocessing)
+[kernel] share/libc/sys/socket.h:451: Warning: 
+  clause with '\initialized' must contain name 'initialization'
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
@@ -41,7 +43,7 @@
    wcscpy (0 call); wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call);
    wmemcpy (0 call); wmemset (0 call); 
   
-  Specified-only functions (411)
+  Specified-only functions (413)
   ==============================
    FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
    Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -133,38 +135,39 @@
    putchar (0 call); putchar_unlocked (0 call); puts (0 call); qsort (0 call);
    quick_exit (0 call); raise (0 call); rand (0 call); random (0 call);
    read (0 call); readdir (0 call); readv (0 call); realloc (3 calls);
-   recv (0 call); recvmsg (0 call); remove (0 call); rename (0 call);
-   rewind (0 call); round (0 call); roundf (0 call); roundl (0 call);
-   seed48 (0 call); select (0 call); send (0 call); setbuf (0 call);
-   setegid (0 call); seteuid (0 call); setgid (0 call); sethostname (0 call);
-   setitimer (0 call); setjmp (0 call); setlogmask (0 call); setpgid (0 call);
-   setpriority (0 call); setregid (0 call); setresgid (0 call);
-   setresuid (0 call); setreuid (0 call); setrlimit (0 call); setsid (0 call);
-   setsockopt (0 call); settimeofday (0 call); setuid (0 call);
-   setvbuf (0 call); shutdown (0 call); sigaction (0 call); sigaddset (0 call);
-   sigdelset (0 call); sigemptyset (0 call); sigfillset (0 call);
-   sigismember (0 call); siglongjmp (0 call); signal (0 call);
-   sigprocmask (0 call); sin (0 call); sinf (0 call); sinl (0 call);
-   socket (0 call); socketpair (0 call); sqrt (0 call); sqrtf (0 call);
-   sqrtl (0 call); srand (0 call); srand48 (0 call); srandom (0 call);
-   stat (0 call); stpcpy (0 call); strcasestr (0 call); strchrnul (0 call);
-   strcoll (0 call); strcspn (0 call); strftime (0 call); strlcat (0 call);
-   strlcpy (0 call); strncasecmp (0 call); strpbrk (0 call); strsep (0 call);
-   strspn (0 call); strtod (0 call); strtof (0 call); strtoimax (0 call);
-   strtok (0 call); strtok_r (0 call); strtol (0 call); strtold (0 call);
-   strtoll (0 call); strtoul (0 call); strtoull (0 call); strxfrm (0 call);
-   sync (0 call); sysconf (0 call); syslog (0 call); system (0 call);
-   tcflush (0 call); tcgetattr (0 call); tcsetattr (0 call); time (0 call);
-   times (0 call); tmpfile (0 call); tmpnam (0 call); trunc (0 call);
-   truncf (0 call); truncl (0 call); ttyname (0 call); tzset (0 call);
-   umask (0 call); uname (0 call); ungetc (0 call); unlink (0 call);
-   usleep (0 call); utimes (0 call); vfprintf (0 call); vfscanf (0 call);
-   vprintf (0 call); vscanf (0 call); vsnprintf (0 call); vsprintf (0 call);
-   vsyslog (0 call); wait (0 call); waitpid (0 call); wcschr (0 call);
-   wcscmp (0 call); wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call);
-   wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call);
-   wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
-   wmemcmp (0 call); wmemmove (0 call); write (0 call); 
+   recv (0 call); recvfrom (0 call); recvmsg (0 call); remove (0 call);
+   rename (0 call); rewind (0 call); round (0 call); roundf (0 call);
+   roundl (0 call); seed48 (0 call); select (0 call); send (0 call);
+   sendto (0 call); setbuf (0 call); setegid (0 call); seteuid (0 call);
+   setgid (0 call); sethostname (0 call); setitimer (0 call); setjmp (0 call);
+   setlogmask (0 call); setpgid (0 call); setpriority (0 call);
+   setregid (0 call); setresgid (0 call); setresuid (0 call);
+   setreuid (0 call); setrlimit (0 call); setsid (0 call); setsockopt (0 call);
+   settimeofday (0 call); setuid (0 call); setvbuf (0 call); shutdown (0 call);
+   sigaction (0 call); sigaddset (0 call); sigdelset (0 call);
+   sigemptyset (0 call); sigfillset (0 call); sigismember (0 call);
+   siglongjmp (0 call); signal (0 call); sigprocmask (0 call); sin (0 call);
+   sinf (0 call); sinl (0 call); socket (0 call); socketpair (0 call);
+   sqrt (0 call); sqrtf (0 call); sqrtl (0 call); srand (0 call);
+   srand48 (0 call); srandom (0 call); stat (0 call); stpcpy (0 call);
+   strcasestr (0 call); strchrnul (0 call); strcoll (0 call); strcspn (0 call);
+   strftime (0 call); strlcat (0 call); strlcpy (0 call); strncasecmp (0 call);
+   strpbrk (0 call); strsep (0 call); strspn (0 call); strtod (0 call);
+   strtof (0 call); strtoimax (0 call); strtok (0 call); strtok_r (0 call);
+   strtol (0 call); strtold (0 call); strtoll (0 call); strtoul (0 call);
+   strtoull (0 call); strxfrm (0 call); sync (0 call); sysconf (0 call);
+   syslog (0 call); system (0 call); tcflush (0 call); tcgetattr (0 call);
+   tcsetattr (0 call); time (0 call); times (0 call); tmpfile (0 call);
+   tmpnam (0 call); trunc (0 call); truncf (0 call); truncl (0 call);
+   ttyname (0 call); tzset (0 call); umask (0 call); uname (0 call);
+   ungetc (0 call); unlink (0 call); usleep (0 call); utimes (0 call);
+   vfprintf (0 call); vfscanf (0 call); vprintf (0 call); vscanf (0 call);
+   vsnprintf (0 call); vsprintf (0 call); vsyslog (0 call); wait (0 call);
+   waitpid (0 call); wcschr (0 call); wcscmp (0 call); wcscspn (0 call);
+   wcslcat (0 call); wcslcpy (0 call); wcsncmp (0 call); wcspbrk (0 call);
+   wcsrchr (0 call); wcsspn (0 call); wcsstr (0 call); wcstombs (0 call);
+   wctomb (0 call); wmemchr (0 call); wmemcmp (0 call); wmemmove (0 call);
+   write (0 call); 
   
   Undefined and unspecified functions (1)
   =======================================
@@ -191,7 +194,7 @@
   Goto = 97
   Assignment = 459
   Exit point = 83
-  Function = 495
+  Function = 497
   Function call = 93
   Pointer dereferencing = 159
   Cyclomatic complexity = 296

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

@@ -3686,6 +3686,40 @@ extern int listen(int sockfd, int backlog);
  */
 extern ssize_t recv(int sockfd, void *buf, size_t len, int flags);
 
+/*@ requires valid_sockfd: 0 ≤ sockfd < 1024;
+    requires valid_buffer_length: \valid((char *)buf + (0 .. len - 1));
+    requires
+      valid_addrbuf_or_null:
+        (\valid(addrbuf_len) ∧ \initialized(addrbuf_len) ∧
+         \valid((char *)addrbuf + (0 .. *addrbuf_len - 1))) ∨
+        (addrbuf ≡ \null ∧ addrbuf_len ≡ \null);
+    ensures
+      result_error_or_received_length:
+        \result ≡ -1 ∨ (0 ≤ \result ≤ \old(len));
+    ensures
+      initialization: buf:
+        \initialized((char *)\old(buf) + (0 .. \result - 1));
+    ensures
+      initialization: addrbuf:
+        \old(addrbuf) ≢ \null ⇒
+        \initialized((char *)\old(addrbuf) + (0 .. \old(*addrbuf_len) - 1));
+    assigns *((char *)buf + (0 .. len - 1)), __fc_sockfds[sockfd], \result,
+            *addrbuf_len, *((char *)addrbuf + (0 .. \old(*addrbuf_len) - 1));
+    assigns *((char *)buf + (0 .. len - 1))
+      \from sockfd, len, flags, __fc_sockfds[sockfd];
+    assigns __fc_sockfds[sockfd]
+      \from sockfd, len, flags, __fc_sockfds[sockfd];
+    assigns \result \from sockfd, len, flags, __fc_sockfds[sockfd];
+    assigns *addrbuf_len
+      \from (indirect: sockfd), (indirect: len), (indirect: flags),
+            __fc_sockfds[sockfd];
+    assigns *((char *)addrbuf + (0 .. \old(*addrbuf_len) - 1))
+      \from (indirect: sockfd), (indirect: len), (indirect: flags),
+            __fc_sockfds[sockfd];
+ */
+extern ssize_t recvfrom(int sockfd, void *buf, size_t len, int flags,
+                        struct sockaddr *addrbuf, socklen_t *addrbuf_len);
+
 /*@ requires valid_sockfd: 0 ≤ sockfd < 1024;
     requires
       msg_control_has_room:
@@ -3737,6 +3771,23 @@ extern ssize_t recvmsg(int sockfd, struct msghdr *hdr, int flags);
  */
 extern ssize_t send(int sockfd, void const *buf, size_t len, int flags);
 
+/*@ requires available_sockfd: 0 ≤ sockfd < 1024;
+    requires buf_len_ok: \valid_read((char *)buf + (0 .. len - 1));
+    ensures
+      error_or_chars_sent: \result ≡ -1 ∨ (0 ≤ \result ≤ \old(len));
+    assigns __fc_errno, __fc_sockfds[sockfd], \result;
+    assigns __fc_errno
+      \from (indirect: sockfd), (indirect: __fc_sockfds[sockfd]),
+            (indirect: *((char *)buf + (0 .. len))), flags;
+    assigns __fc_sockfds[sockfd]
+      \from __fc_sockfds[sockfd], *((char *)buf + (0 .. len)), flags;
+    assigns \result
+      \from (indirect: sockfd), (indirect: __fc_sockfds[sockfd]),
+            (indirect: *((char *)buf + (0 .. len))), (indirect: flags);
+ */
+extern ssize_t sendto(int sockfd, void const *buf, size_t len, int flags,
+                      struct sockaddr const *address, socklen_t address_len);
+
 /*@ requires valid_sockfd: 0 ≤ sockfd < 1024;
     requires
       optval_null_or_has_room:

tests/libc/oracle/socket_h.res.oracle

@@ -59,10 +59,52 @@
 [eva] tests/libc/socket_h.c:21: 
   function getsockname: precondition 'valid_address' got status valid.
 [eva] Done for function getsockname
+[eva] computing for function sendto <- main.
+  Called from tests/libc/socket_h.c:24.
+[eva] using specification for function sendto
+[eva] tests/libc/socket_h.c:24: 
+  function sendto: precondition 'available_sockfd' got status valid.
+[eva] tests/libc/socket_h.c:24: 
+  function sendto: precondition 'buf_len_ok' got status valid.
+[eva] Done for function sendto
+[eva] computing for function sendto <- main.
+  Called from tests/libc/socket_h.c:27.
+[eva] tests/libc/socket_h.c:27: 
+  function sendto: precondition 'available_sockfd' got status valid.
+[eva] tests/libc/socket_h.c:27: 
+  function sendto: precondition 'buf_len_ok' got status valid.
+[eva] Done for function sendto
+[eva] computing for function recvfrom <- main.
+  Called from tests/libc/socket_h.c:31.
+[eva] using specification for function recvfrom
+[eva] tests/libc/socket_h.c:31: 
+  function recvfrom: precondition 'valid_sockfd' got status valid.
+[eva] tests/libc/socket_h.c:31: 
+  function recvfrom: precondition 'valid_buffer_length' got status valid.
+[eva] tests/libc/socket_h.c:31: 
+  function recvfrom: precondition 'valid_addrbuf_or_null' got status valid.
+[eva] Done for function recvfrom
+[eva] tests/libc/socket_h.c:35: assertion got status valid.
+[eva] computing for function recvfrom <- main.
+  Called from tests/libc/socket_h.c:37.
+[eva] tests/libc/socket_h.c:37: 
+  function recvfrom: precondition 'valid_sockfd' got status valid.
+[eva] tests/libc/socket_h.c:37: 
+  function recvfrom: precondition 'valid_buffer_length' got status valid.
+[eva] tests/libc/socket_h.c:37: 
+  function recvfrom: precondition 'valid_addrbuf_or_null' got status valid.
+[eva:invalid-assigns] tests/libc/socket_h.c:37: 
+  Completely invalid destination for assigns clause *addrbuf_len. Ignoring.
+[eva:invalid-assigns] tests/libc/socket_h.c:37: 
+  Completely invalid destination
+  for assigns clause *((char *)addrbuf + (0 .. \old(*addrbuf_len) - 1)).
+  Ignoring.
+[eva] Done for function recvfrom
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
+  __fc_errno ∈ [--..--]
   __fc_sockfds[0..1023] ∈ [--..--]
   __fc_socket_counter ∈ [--..--]
   sockfd ∈ [0..1023]
@@ -73,3 +115,10 @@
   optlen ∈ {4}
   addr2 ∈ [--..--] or UNINITIALIZED
   socklen ∈ [0..8]
+  buf[0..39] ∈ [--..--]
+  sent ∈ {-1; 0; 1; 2; 3}
+  sent2 ∈ {-1; 0; 1; 2; 3}
+  recvfrom_addr ∈ [--..--]
+  recvfrom_addr_len ∈ [--..--]
+  received ∈ [-1..40]
+  received2 ∈ [-1..40]

tests/libc/socket_h.c

@@ -19,5 +19,21 @@ int main() {
   struct sockaddr_in addr2;
   socklen_t socklen = sizeof(addr2);
   rc = getsockname(sockfd, (struct sockaddr *)&addr2, &socklen);
+
+  char buf[40] = {'a', 'b', 'c'};
+  ssize_t sent = sendto(sockfd, buf, 3, 0, (struct sockaddr *)&addr,
+                        sizeof(addr));
+
+  ssize_t sent2 = sendto(sockfd, buf, 3, 0, 0, 0);
+
+  struct sockaddr_in recvfrom_addr;
+  socklen_t recvfrom_addr_len = sizeof(recvfrom_addr);
+  ssize_t received = recvfrom(sockfd, buf, sizeof(buf), 0,
+                              (struct sockaddr *)&recvfrom_addr,
+                              &recvfrom_addr_len);
+  if (received != -1) {
+    //@ assert \initialized(&recvfrom_addr);
+  }
+  ssize_t received2 = recvfrom(sockfd, buf, sizeof(buf), 0, 0, 0);
   return rc;
 }