[Libc] add specs for sys/stat.h functions

share/libc/sys/stat.h

@@ -28,13 +28,72 @@ __BEGIN_DECLS
 
 #include "../__fc_define_stat.h"
 #include "../__fc_string_axiomatic.h"
+#include "../errno.h"
 
-extern int    chmod(const char *, mode_t);
-extern int    fchmodat(int fd, const char *path, mode_t mode, int flag);
-extern int    fchmod(int, mode_t);
-extern int    fstat(int, struct stat *);
-extern int    fstatat(int fd, const char *restrict path,
-                      struct stat *restrict buf, int flag);
+/*@
+  // missing: assigns 'filesystem' \frompath, path[0..], mode;
+  requires valid_path: valid_read_string(path);
+  assigns \result, __fc_errno
+          \from indirect:path, indirect:path[0 .. strlen(path)],
+                indirect:mode; //missing: \from 'filesystem'
+  ensures errno_set: __fc_errno == \old(__fc_errno) ||
+                     __fc_errno \in {EACCES, ELOOP, ENAMETOOLONG, ENOENT,
+                                     ENOTDIR, EPERM, EROFS};
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int chmod(const char *path, mode_t mode);
+
+/*@
+  // missing: assigns 'filesystem' \from fd, path, path[0..], mode, flag;
+  requires valid_path: valid_read_string(path);
+  assigns \result, __fc_errno
+          \from indirect:fd, indirect:path, indirect:path[0 .. strlen(path)],
+                indirect:mode, indirect:flag; //missing: \from 'filesystem'
+  ensures errno_set: __fc_errno == \old(__fc_errno) ||
+                     __fc_errno \in {EACCES, EBADF, EINTR, EINVAL, ELOOP,
+                                     ENAMETOOLONG, ENOENT, EOPNOTSUPP, ENOTDIR,
+                                     EPERM, EROFS};
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int fchmodat(int fd, const char *path, mode_t mode, int flag);
+
+/*@
+  // missing: assigns 'filesystem' \from fildes, mode;
+  assigns \result, __fc_errno
+          \from indirect:fildes, indirect:mode; //missing: \from 'filesystem'
+  ensures errno_set: __fc_errno == \old(__fc_errno) ||
+                     __fc_errno \in {EBADF, EINTR, EINVAL, EPERM, EROFS};
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int fchmod(int fildes, mode_t mode);
+
+/*@
+  //TODO: define proper initialization postcondition; it involves only a few
+  //      specific fields, and only a few bits within those fields.
+  requires valid_buf: \valid(buf);
+  assigns \result, *buf, __fc_errno
+          \from indirect:fildes; //missing: \from 'filesystem'
+  ensures errno_set: __fc_errno == \old(__fc_errno) ||
+                     __fc_errno \in {EBADF, EIO, EOVERFLOW};
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int fstat(int fildes, struct stat *buf);
+
+/*@
+  // missing: assigns 'filesystem' \from fd, path, path[0..], flag;
+  requires valid_path: valid_read_string(path);
+  requires valid_buf: \valid(buf);
+  assigns \result, *buf, __fc_errno
+          \from indirect:fd, indirect:path, indirect:path[0 .. strlen(path)],
+                indirect:flag; //missing: \from 'filesystem'
+  ensures errno_set: __fc_errno == \old(__fc_errno) ||
+                     __fc_errno \in {EACCES, EBADF, EINVAL, ELOOP,
+                                     ENAMETOOLONG, ENOENT, ENOMEM, ENOTDIR,
+                                     EOVERFLOW};
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int fstatat(int fd, const char *restrict path,
+                   struct stat *restrict buf, int flag);
 
 /*@ // missing: may assign to errno: EACCES, ELOOP, ENAMETOOLONG,
     //                               ENOENT, ENOMEM, ENOTDIR, EOVERFLOW,

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

@@ -8979,6 +8979,83 @@ extern int __va_openat_mode_t(int dirfd, char const *filename, int flags,
 extern int select(int nfds, fd_set *readfds, fd_set *writefds,
                   fd_set *errorfds, struct timeval *timeout);
 
+/*@ requires valid_path: valid_read_string(path);
+    ensures
+      errno_set:
+        __fc_errno ≡ \old(__fc_errno) ∨
+        __fc_errno ∈ {13, 40, 36, 2, 20, 1, 30};
+    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result, __fc_errno;
+    assigns \result
+      \from (indirect: path), (indirect: *(path + (0 .. strlen{Old}(path)))),
+            (indirect: mode);
+    assigns __fc_errno
+      \from (indirect: path), (indirect: *(path + (0 .. strlen{Old}(path)))),
+            (indirect: mode);
+ */
+extern int chmod(char const *path, mode_t mode);
+
+/*@ requires valid_path: valid_read_string(path);
+    ensures
+      errno_set:
+        __fc_errno ≡ \old(__fc_errno) ∨
+        __fc_errno ∈ {13, 9, 4, 22, 40, 36, 2, 95, 20, 1, 30};
+    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result, __fc_errno;
+    assigns \result
+      \from (indirect: fd), (indirect: path),
+            (indirect: *(path + (0 .. strlen{Old}(path)))), (indirect: mode),
+            (indirect: flag);
+    assigns __fc_errno
+      \from (indirect: fd), (indirect: path),
+            (indirect: *(path + (0 .. strlen{Old}(path)))), (indirect: mode),
+            (indirect: flag);
+ */
+extern int fchmodat(int fd, char const *path, mode_t mode, int flag);
+
+/*@ ensures
+      errno_set:
+        __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ∈ {9, 4, 22, 1, 30};
+    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result, __fc_errno;
+    assigns \result \from (indirect: fildes), (indirect: mode);
+    assigns __fc_errno \from (indirect: fildes), (indirect: mode);
+ */
+extern int fchmod(int fildes, mode_t mode);
+
+/*@ requires valid_buf: \valid(buf);
+    ensures
+      errno_set:
+        __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ∈ {9, 5, 75};
+    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result, *buf, __fc_errno;
+    assigns \result \from (indirect: fildes);
+    assigns *buf \from (indirect: fildes);
+    assigns __fc_errno \from (indirect: fildes);
+ */
+extern int fstat(int fildes, struct stat *buf);
+
+/*@ requires valid_path: valid_read_string(path);
+    requires valid_buf: \valid(buf);
+    ensures
+      errno_set:
+        __fc_errno ≡ \old(__fc_errno) ∨
+        __fc_errno ∈ {13, 9, 22, 40, 36, 2, 12, 20, 75};
+    ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result, *buf, __fc_errno;
+    assigns \result
+      \from (indirect: fd), (indirect: path),
+            (indirect: *(path + (0 .. strlen{Old}(path)))), (indirect: flag);
+    assigns *buf
+      \from (indirect: fd), (indirect: path),
+            (indirect: *(path + (0 .. strlen{Old}(path)))), (indirect: flag);
+    assigns __fc_errno
+      \from (indirect: fd), (indirect: path),
+            (indirect: *(path + (0 .. strlen{Old}(path)))), (indirect: flag);
+ */
+extern int fstatat(int fd, char const * restrict path,
+                   struct stat * restrict buf, int flag);
+
 /*@ requires valid_path: valid_read_string(path);
     requires valid_buf: \valid(buf);
     ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;

tests/libc/oracle/sys_stat_h.res.oracle

@@ -69,10 +69,47 @@
 [eva] computing for function mknod <- main.
   Called from sys_stat_h.c:25.
 [eva] Done for function mknod
+[eva] computing for function chmod <- main.
+  Called from sys_stat_h.c:27.
+[eva] using specification for function chmod
+[eva] sys_stat_h.c:27: 
+  function chmod: precondition 'valid_path' got status valid.
+[eva] Done for function chmod
+[eva] computing for function fchmod <- main.
+  Called from sys_stat_h.c:29.
+[eva] using specification for function fchmod
+[eva] Done for function fchmod
+[eva] computing for function fchmod <- main.
+  Called from sys_stat_h.c:29.
+[eva] Done for function fchmod
+[eva] computing for function fchmodat <- main.
+  Called from sys_stat_h.c:31.
+[eva] using specification for function fchmodat
+[eva] sys_stat_h.c:31: 
+  function fchmodat: precondition 'valid_path' got status valid.
+[eva] Done for function fchmodat
+[eva] computing for function fstat <- main.
+  Called from sys_stat_h.c:35.
+[eva] using specification for function fstat
+[eva] sys_stat_h.c:35: 
+  function fstat: precondition 'valid_buf' got status valid.
+[eva] Done for function fstat
+[eva] computing for function fstat <- main.
+  Called from sys_stat_h.c:35.
+[eva] Done for function fstat
+[eva] computing for function fstatat <- main.
+  Called from sys_stat_h.c:37.
+[eva] using specification for function fstatat
+[eva] sys_stat_h.c:37: 
+  function fstatat: precondition 'valid_path' got status valid.
+[eva] sys_stat_h.c:37: 
+  function fstatat: precondition 'valid_buf' got status valid.
+[eva] Done for function fstatat
 [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_fds[0..1023] ∈ [--..--]
   fd ∈ [-1..1023]
   st ∈ [--..--] or UNINITIALIZED
@@ -82,4 +119,10 @@
   r2 ∈ {-1; 0}
   r3 ∈ {-1; 0}
   r4 ∈ {-1; 0}
+  r5 ∈ {-1; 0}
+  r6 ∈ {-1; 0}
+  r7 ∈ {-1; 0}
+  buf ∈ [--..--] or UNINITIALIZED
+  r8 ∈ {-1; 0}
+  r9 ∈ {-1; 0}
   __retres ∈ {-1; 0; 1; 2; 3}

tests/libc/sys_stat_h.c

@@ -23,5 +23,18 @@ int main() {
   int r2 = lstat("/tmp/bla", &st);
   int r3 = mkfifo("/tmp/fifo", 0644);
   int r4 = mknod("/tmp/fifo2", 0644, 42);
+
+  int r5 = chmod("/tmp/bla", 0700);
+
+  int r6 = fchmod(fd, 0700);
+
+  int r7 = fchmodat(AT_FDCWD, "bla", 0700, AT_SYMLINK_NOFOLLOW);
+
+  struct stat buf;
+
+  int r8 = fstat(fd, &buf);
+
+  int r9 = fstatat(AT_FDCWD, "bla", &buf, AT_SYMLINK_NOFOLLOW);
+
   return 0;
 }