[Libc] add and improve specs in sys/socket.h and unistd.h

share/libc/sys/socket.h

@@ -443,11 +443,10 @@ 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 < __FC_MAX_OPEN_SOCKETS;
   requires valid_buffer_length: \valid((char *)buf+(0 .. len-1));
-  requires valid_addrbuf_or_null: (\valid(addrbuf_len) &&
+  requires valid_addrbuf_or_null:initialization: (\valid(addrbuf_len) &&
                                    \initialized(addrbuf_len) &&
                                    \valid((char *)addrbuf+(0 .. *addrbuf_len-1)))
                                   || (addrbuf == \null && addrbuf_len == \null);
@@ -503,7 +502,23 @@ extern ssize_t recvmsg(int sockfd, struct msghdr *hdr, int flags);
   ensures error_or_chars_sent: \result == -1 || 0 <= \result <= len;
  */
 extern ssize_t send(int sockfd, const void *buf, size_t len, int flags);
-extern ssize_t sendmsg(int, const struct msghdr *, int);
+
+/*@
+  requires available_sockfd: 0 <= sockfd < __FC_MAX_OPEN_SOCKETS;
+  requires valid_message: \valid_read(message);
+  requires valid_msg_iov:
+    \valid_read(message->msg_iov+(0 .. message->msg_iovlen - 1));
+  assigns __fc_sockfds[sockfd]
+    \from __fc_sockfds[sockfd],
+          indirect:*message,
+          indirect:message->msg_iov[0 .. message->msg_iovlen - 1],
+          indirect:flags;
+  assigns \result \from indirect:sockfd, indirect:__fc_sockfds[sockfd],
+          indirect:*message,
+          indirect:message->msg_iov[0 .. message->msg_iovlen - 1];
+  ensures error_or_chars_sent: \result == -1 || 0 <= \result;
+ */
+extern ssize_t sendmsg(int sockfd, const struct msghdr *message, int flags);
 
 /*@
   requires available_sockfd: 0 <= sockfd < __FC_MAX_OPEN_SOCKETS;

share/libc/unistd.h

@@ -947,7 +947,21 @@ extern char        *getwd(char *);
 extern int          isatty(int fd);
 
 extern int          lchown(const char *, uid_t, gid_t);
-extern int          link(const char *, const char *);
+
+/*@ //missing: may assign to errno: EACCES, EEXIST, ELOOP, EMLINK, ENAMETOOLONG,
+    //                              ENOENT, ENOSPC, ENOTDIR, EPERM, EROFS,
+    //                              EXDEV, EBADF, ENOTDIR, EINVAL;
+    // missing: assigns 'filesystem' \from path1[0..strlen(path1)],
+    //                                     path2[0..strlen(path2)];
+    // missing: assigns \result \from 'paths in filesystem'
+  requires valid_path: valid_read_string(path1);
+  requires valid_path: valid_read_string(path2);
+  assigns \result \from indirect:path1[0 .. strlen(path1)],
+                        indirect:path2[0 .. strlen(path2)];
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+ */
+extern int          link(const char *path1, const char *path2);
+
 extern int          lockf(int, int, off_t);
 
 /*@ //missing: may assign to errno: EBADF, EINVAL, EOVERFLOW, ESPIPE, ENXIO (Linux);
@@ -1108,7 +1122,7 @@ extern useconds_t   ualarm(useconds_t, useconds_t);
   // missing: assigns 'filesystem' \from path[0..];
   // missing: assigns \result \from 'filesystem';
   requires valid_string_path: valid_read_string(path);
-  assigns \result \from path[0..];
+  assigns \result \from indirect:path[0..strlen(path)];
   ensures result_ok_or_error: \result == 0 || \result == -1;
  */
 extern int          unlink(const char *path);

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

@@ -14,8 +14,6 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   
-[kernel] FRAMAC_SHARE/libc/sys/socket.h:451: Warning: 
-  clause with '\initialized' must contain name 'initialization'
 /* Generated by Frama-C */
 #include "__fc_builtin.c"
 #include "__fc_builtin.h"

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

@@ -3098,6 +3098,16 @@ extern uid_t getuid(void);
  */
 extern int isatty(int fd);
 
+/*@ requires valid_path: valid_read_string(path1);
+    requires valid_path: valid_read_string(path2);
+    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result;
+    assigns \result
+      \from (indirect: *(path1 + (0 .. strlen{Old}(path1)))),
+            (indirect: *(path2 + (0 .. strlen{Old}(path2))));
+ */
+extern int link(char const *path1, char const *path2);
+
 /*@ requires valid_fd: 0 ≤ fd < 1024;
     requires valid_whence: whence ≡ 0 ∨ whence ≡ 1 ∨ whence ≡ 2;
     ensures result_error_or_offset: \result ≡ -1 ∨ 0 ≤ \result;
@@ -3218,7 +3228,7 @@ extern char *ttyname(int fildes);
 /*@ requires valid_string_path: valid_read_string(path);
     ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
     assigns \result;
-    assigns \result \from *(path + (0 ..));
+    assigns \result \from (indirect: *(path + (0 .. strlen{Old}(path))));
  */
 extern int unlink(char const *path);
 
@@ -4772,7 +4782,7 @@ 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_or_null: initialization:
         (\valid(addrbuf_len) ∧ \initialized(addrbuf_len) ∧
          \valid((char *)addrbuf + (0 .. *addrbuf_len - 1))) ∨
         (addrbuf ≡ \null ∧ addrbuf_len ≡ \null);
@@ -4854,6 +4864,24 @@ 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 valid_message: \valid_read(message);
+    requires
+      valid_msg_iov:
+        \valid_read(message->msg_iov + (0 .. message->msg_iovlen - 1));
+    ensures error_or_chars_sent: \result ≡ -1 ∨ 0 ≤ \result;
+    assigns __fc_sockfds[sockfd], \result;
+    assigns __fc_sockfds[sockfd]
+      \from __fc_sockfds[sockfd], (indirect: *message),
+            (indirect: *(message->msg_iov + (0 .. message->msg_iovlen - 1))),
+            (indirect: flags);
+    assigns \result
+      \from (indirect: sockfd), (indirect: __fc_sockfds[sockfd]),
+            (indirect: *message),
+            (indirect: *(message->msg_iov + (0 .. message->msg_iovlen - 1)));
+ */
+extern ssize_t sendmsg(int sockfd, struct msghdr const *message, int flags);
+
 /*@ requires available_sockfd: 0 ≤ sockfd < 1024;
     requires buf_len_ok: \valid_read((char *)buf + (0 .. len - 1));
     ensures

tests/libc/oracle/socket_h.res.oracle

@@ -82,7 +82,7 @@
 [eva] socket_h.c:31: 
   function recvfrom: precondition 'valid_buffer_length' got status valid.
 [eva] socket_h.c:31: 
-  function recvfrom: precondition 'valid_addrbuf_or_null' got status valid.
+  function recvfrom: precondition 'valid_addrbuf_or_null,initialization' got status valid.
 [eva] Done for function recvfrom
 [eva] socket_h.c:35: assertion got status valid.
 [eva] computing for function recvfrom <- main.
@@ -92,7 +92,7 @@
 [eva] socket_h.c:37: 
   function recvfrom: precondition 'valid_buffer_length' got status valid.
 [eva] socket_h.c:37: 
-  function recvfrom: precondition 'valid_addrbuf_or_null' got status valid.
+  function recvfrom: precondition 'valid_addrbuf_or_null,initialization' got status valid.
 [eva:invalid-assigns] socket_h.c:37: 
   Completely invalid destination for assigns clause *addrbuf_len. Ignoring.
 [eva:invalid-assigns] socket_h.c:37: 

tests/libc/oracle/sys_socket_h.res.oracle

+[kernel] Parsing sys_socket_h.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  dest ∈ [--..--]
+  v ∈ [--..--]
+[eva] sys_socket_h.c:26: Call to builtin strlen
+[eva] sys_socket_h.c:26: 
+  function strlen: precondition 'valid_string_s' got status valid.
+[eva] computing for function socket <- main.
+  Called from sys_socket_h.c:40.
+[eva] using specification for function socket
+[eva] Done for function socket
+[eva] computing for function sendmsg <- main.
+  Called from sys_socket_h.c:42.
+[eva] using specification for function sendmsg
+[eva] sys_socket_h.c:42: 
+  function sendmsg: precondition 'available_sockfd' got status valid.
+[eva] sys_socket_h.c:42: 
+  function sendmsg: precondition 'valid_message' got status valid.
+[eva] sys_socket_h.c:42: 
+  function sendmsg: precondition 'valid_msg_iov' got status valid.
+[eva] Done for function sendmsg
+[eva] sys_socket_h.c:43: assertion 'valid' got status valid.
+[eva] computing for function sendmsg <- main.
+  Called from sys_socket_h.c:47.
+[eva] sys_socket_h.c:47: 
+  function sendmsg: precondition 'available_sockfd' got status valid.
+[eva] sys_socket_h.c:47: 
+  function sendmsg: precondition 'valid_message' got status valid.
+[eva:alarm] sys_socket_h.c:47: Warning: 
+  function sendmsg: precondition 'valid_msg_iov' got status invalid.
+[eva] Done for function sendmsg
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  __fc_sockfds[0..1023] ∈ [--..--]
+  __fc_socket_counter ∈ [--..--]
+  d1 ∈ {{ "message" }}
+  s1.a ∈ {42}
+    .b ∈ {65}
+    .[bits 40 to 63] ∈ {0}
+  s2.p ∈ {0}
+    .d ∈ {3.125}
+  n ∈ {501}
+  d ∈ {5.5}
+  iov[0].iov_base ∈ {{ "message" }}
+     [0].iov_len ∈ {7}
+     [1].iov_base ∈ {{ (void *)&s1 }}
+     [1].iov_len ∈ {8}
+     [2].iov_base ∈ {{ (void *)&s2 }}
+     [2].iov_len ∈ {12}
+     [3].iov_base ∈ {{ (void *)&n }}
+     [3].iov_len ∈ {4}
+     [4].iov_base ∈ {{ (void *)&d }}
+     [4].iov_len ∈ {8}
+  msg{.msg_name; .msg_namelen} ∈ {0}
+     .msg_iov ∈ {{ &iov[0] }}
+     .msg_iovlen ∈ {5; 6}
+     {.msg_control; .msg_controllen; .msg_flags} ∈ UNINITIALIZED
+  sockfd ∈ [-1..1023]
+  r ∈ [-1..2147483647]
+  __retres ∈ {0; 1}

tests/libc/sys_socket_h.c

+#include <sys/socket.h>
+#include <netinet/in.h>
+#include <string.h>
+
+struct s1 {
+  int a;
+  char b;
+};
+
+struct s2 {
+  int *p;
+  double d;
+};
+
+volatile struct sockaddr_in dest;
+volatile int v;
+
+int main() {
+  char *d1 = "message";
+  struct s1 s1 = {42, 'A'};
+  struct s2 s2 = {0, 3.125};
+  int n = 501;
+  double d = 5.5;
+  struct iovec iov[5];
+  iov[0].iov_base = d1;
+  iov[0].iov_len = strlen(d1);
+  iov[1].iov_base = &s1;
+  iov[1].iov_len = sizeof(struct s1);
+  iov[2].iov_base = &s2;
+  iov[2].iov_len = sizeof(struct s2);
+  iov[3].iov_base = &n;
+  iov[3].iov_len = sizeof(int);
+  iov[4].iov_base = &d;
+  iov[4].iov_len = sizeof(double);
+  struct msghdr msg;
+   msg.msg_name = 0;
+   msg.msg_namelen = 0;
+   msg.msg_iov = iov;
+   msg.msg_iovlen = 5;
+   int sockfd = socket(AF_INET, SOCK_STREAM, 0);
+   if (sockfd < 0) return 1;
+   int r = sendmsg(sockfd, &msg, 0);
+   //@ assert valid: r == -1 || r >= 0;
+
+   msg.msg_iovlen = 6; // invalid length
+   if (v) {
+     sendmsg(sockfd, &msg, 0); // must fail
+     //@ assert unreachable: \false;
+   }
+   return 0;
+}

tests/metrics/oracle/libc.json

@@ -87,6 +87,7 @@
     { "isspace": { "calls": 0, "address_taken": false } },
     { "isupper": { "calls": 0, "address_taken": false } },
     { "isxdigit": { "calls": 0, "address_taken": false } },
+    { "link": { "calls": 0, "address_taken": false } },
     { "lseek": { "calls": 0, "address_taken": false } },
     { "pathconf": { "calls": 0, "address_taken": false } },
     { "pclose": { "calls": 0, "address_taken": false } },