From 67f7bfc50305f134821b24b104c4e9e2fe315f7d Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 30 Sep 2022 16:33:10 +0200
Subject: [PATCH] [libc] improve POSIX and non-POSIX compatibility
---
share/libc/fcntl.h | 15 ++++++---
share/libc/signal.h | 11 +++++++
share/libc/sys/socket.h | 33 ++++++++++---------
share/libc/sys/types.h | 5 +++
.../tests/known/oracle/fcntl.res.oracle | 6 ++--
.../tests/known/oracle/open.res.oracle | 6 ++--
.../tests/known/oracle/open_wrong.res.oracle | 6 ++--
.../tests/known/oracle/openat.res.oracle | 6 ++--
tests/libc/oracle/fc_libc.1.res.oracle | 9 +++++
tests/libc/oracle/signal_h.res.oracle | 11 ++++++-
tests/libc/signal_h.c | 9 ++++-
tests/syntax/oracle/signal.res.oracle | 1 +
12 files changed, 84 insertions(+), 34 deletions(-)
diff --git a/share/libc/fcntl.h b/share/libc/fcntl.h
index b5dabf3d70c..5e90adad1c4 100644
--- a/share/libc/fcntl.h
+++ b/share/libc/fcntl.h
@@ -72,6 +72,9 @@ __PUSH_FC_STDLIB
#define O_RSYNC 0x101000
#define O_SYNC 0x101000
+// Non-POSIX
+#define O_PATH 010000000
+
#define O_ACCMODE 3
//#define O_EXEC
@@ -81,15 +84,19 @@ __PUSH_FC_STDLIB
#define O_WRONLY 1
#define AT_FDCWD -100
-
#define AT_EACCESS 0x200
-
#define AT_SYMLINK_NOFOLLOW 0x100
-
#define AT_SYMLINK_FOLLOW 0x400
-
#define AT_REMOVEDIR 0x200
+// Non-POSIX (GNU extensions)
+#define AT_EMPTY_PATH 0x1000
+#define AT_RECURSIVE 0x8000
+#define AT_STATX_DONT_SYNC 0x4000
+#define AT_STATX_FORCE_SYNC 0x2000
+#define AT_STATX_SYNC_AS_STAT 0x0000
+#define AT_STATX_SYNC_TYPE 0x6000
+
#define POSIX_FADV_DONTNEED 4
#define POSIX_FADV_NOREUSE 5
#define POSIX_FADV_NORMAL 0
diff --git a/share/libc/signal.h b/share/libc/signal.h
index b594a4b53e1..09ee3a57aae 100644
--- a/share/libc/signal.h
+++ b/share/libc/signal.h
@@ -31,6 +31,7 @@ __PUSH_FC_STDLIB
#include "__fc_define_pid_t.h"
#include "__fc_define_uid_and_gid.h"
#include "__fc_define_pthread_types.h"
+#include "errno.h"
__BEGIN_DECLS
@@ -243,6 +244,16 @@ extern int sigaction(int signum, const struct sigaction *restrict act,
extern int sigprocmask(int how, const sigset_t * restrict set,
sigset_t *restrict oldset);
+/*@ // missing: assigns 'current signal mask'
+ // missing: assigns \result from 'possible thread interruption'
+ // missing: terminates 'only when interrupted'
+ requires valid_mask_or_null: sigmask == \null || \valid_read(sigmask);
+ assigns __fc_errno, \result \from indirect:sigmask;
+ ensures result_means_interrupted: \result == -1;
+ ensures errno_set: __fc_errno == EINTR;
+*/
+extern int sigsuspend(const sigset_t *sigmask);
+
/*@ // missing: errno may be set to EINVAL, EPERM, ESRCH
// missing: assigns 'other processes' \from 'other processes'
assigns \result \from indirect:pid, indirect: sig;
diff --git a/share/libc/sys/socket.h b/share/libc/sys/socket.h
index 114226d440b..846a297f0d7 100644
--- a/share/libc/sys/socket.h
+++ b/share/libc/sys/socket.h
@@ -66,6 +66,17 @@ struct msghdr {
int msg_flags;
};
+// POSIX requires these as macros; early uses of these macros (e.g. when
+// computing the size of arrays) prevent us from leaving them undefined and
+// using a function prototype. The following definitions are based on the
+// Linux version of the GNU libc.
+#define CMSG_DATA(cmsg) ((unsigned char *) ((struct cmsghdr *) (cmsg) + 1))
+#define CMSG_ALIGN(len) (((len) + sizeof (size_t) - 1) \
+ & (size_t) ~(sizeof (size_t) - 1))
+#define CMSG_SPACE(len) (CMSG_ALIGN (len) \
+ + CMSG_ALIGN (sizeof (struct cmsghdr)))
+#define CMSG_LEN(len) (CMSG_ALIGN (sizeof (struct cmsghdr)) + (len))
+
// POSIX.1-2008 requires these to be defined as macros, but we have no body
// for them, so we declare them as prototypes as well.
#ifndef CMSG_FIRSTHDR
@@ -76,22 +87,6 @@ extern struct cmsghdr *CMSG_FIRSTHDR(struct msghdr *msgh);
extern struct cmsghdr *CMSG_NXTHDR(struct msghdr *msgh, struct cmsghdr *cmsg);
# define CMSG_NXTHDR(h, c) CMSG_NXTHDR(h, c)
#endif
-#ifndef CMSG_ALIGN
-extern size_t CMSG_ALIGN(size_t length);
-# define CMSG_ALIGN(l) CMSG_ALIGN(l)
-#endif
-#ifndef CMSG_SPACE
-extern size_t CMSG_SPACE(size_t length);
-# define CMSG_SPACE(l) CMSG_SPACE(l)
-#endif
-#ifndef CMSG_LEN
-extern size_t CMSG_LEN(size_t length);
-# define CMSG_LEN(l) CMSG_LEN(l)
-#endif
-#ifndef CMSG_DATA
-extern unsigned char *CMSG_DATA(struct cmsghdr *cmsg);
-# define CMSG_DATA(c) CMSG_DATA(c)
-#endif
/* Socket types. */
#define SOCK_STREAM 1 /* stream (connection) socket */
@@ -295,6 +290,12 @@ struct __fc_sockfds_type { int x; };
// __fc_sockfds represents the state of open socket descriptors.
//@ ghost volatile int __fc_open_sock_fds;
+
+struct linger {
+ int l_onoff;
+ int l_linger;
+};
+
// TODO: Model the state of some functions more precisely.
/*@
diff --git a/share/libc/sys/types.h b/share/libc/sys/types.h
index 68f3deb924a..be288c41c42 100644
--- a/share/libc/sys/types.h
+++ b/share/libc/sys/types.h
@@ -59,6 +59,11 @@ typedef unsigned char u_char;
#define __u_char_defined
#endif
+// Non-POSIX
+#ifndef caddr_t
+typedef char *caddr_t;
+#endif
+
__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
index ff5a912894d..bb16be630f9 100644
--- a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:121:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:128:
Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:124: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:131:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:131: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:138:
Declaration of variadic function openat.
[variadic] fcntl.c:8:
Translating call to the specialized version fcntl(int, int).
diff --git a/src/plugins/variadic/tests/known/oracle/open.res.oracle b/src/plugins/variadic/tests/known/oracle/open.res.oracle
index 9b5c71ca58f..190fa3b120e 100644
--- a/src/plugins/variadic/tests/known/oracle/open.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:121:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:128:
Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:124: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:131:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:131: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:138:
Declaration of variadic function openat.
[variadic] open.c:7:
Translating call to the specialized version open(char const *, int, mode_t).
diff --git a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
index 1f4b8a7cd11..a3eb22c2716 100644
--- a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:121:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:128:
Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:124: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:131:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:131: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:138:
Declaration of variadic function openat.
[variadic:prototype] open_wrong.c:13: Warning:
No matching prototype found for this call to open.
diff --git a/src/plugins/variadic/tests/known/oracle/openat.res.oracle b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
index 30a3448710c..96183ba1107 100644
--- a/src/plugins/variadic/tests/known/oracle/openat.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:121:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:128:
Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:124: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:131:
+[variadic] FRAMAC_SHARE/libc/fcntl.h:131: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:138:
Declaration of variadic function openat.
[variadic] openat.c:8:
Translating call to the specialized version openat(int, char const *, int, mode_t).
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index a081af02056..4e29fd1c1c8 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -4465,6 +4465,15 @@ extern int sigaction(int signum, struct sigaction const * restrict act,
extern int sigprocmask(int how, sigset_t const * restrict set,
sigset_t * restrict oldset);
+/*@ requires valid_mask_or_null: sigmask ≡ \null ∨ \valid_read(sigmask);
+ ensures result_means_interrupted: \result ≡ -1;
+ ensures errno_set: __fc_errno ≡ 4;
+ assigns __fc_errno, \result;
+ assigns __fc_errno \from (indirect: sigmask);
+ assigns \result \from (indirect: sigmask);
+ */
+extern int sigsuspend(sigset_t const *sigmask);
+
/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
assigns \result;
assigns \result \from (indirect: pid), (indirect: sig);
diff --git a/tests/libc/oracle/signal_h.res.oracle b/tests/libc/oracle/signal_h.res.oracle
index 0141d180b8f..7c70744fb71 100644
--- a/tests/libc/oracle/signal_h.res.oracle
+++ b/tests/libc/oracle/signal_h.res.oracle
@@ -126,7 +126,7 @@
function sigaction: precondition 'valid_read_act_or_null' got status valid.
[eva] signal_h.c:48:
function sigaction: precondition 'separation,separated_acts' got status valid.
-[eva] FRAMAC_SHARE/libc/signal.h:222:
+[eva] FRAMAC_SHARE/libc/signal.h:223:
cannot evaluate ACSL term, unsupported ACSL construct: logic coercion struct sigaction -> set<struct sigaction>
[eva] Done for function sigaction
[eva] computing for function sigaction <- main.
@@ -143,10 +143,19 @@
Completely invalid destination for assigns clause *oldact. Ignoring.
[eva] Done for function sigaction
[eva] signal_h.c:55: assertion 'valid_nsig' got status valid.
+[eva] computing for function sigsuspend <- main.
+ Called from signal_h.c:59.
+[eva] using specification for function sigsuspend
+[eva] signal_h.c:59:
+ function sigsuspend: precondition 'valid_mask_or_null' got status valid.
+[eva] Done for function sigsuspend
+[eva] signal_h.c:60: assertion 'sigsuspend_errno_eintr' got status valid.
+[eva] signal_h.c:61: assertion 'sigsuspend_return' got status valid.
[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_sigaction[0]{.sa_handler; .sa_sigaction} ∈ {0}
[0]{.sa_mask; .sa_flags} ∈ [--..--]
[1]{.sa_handler; .sa_sigaction} ∈ {0}
diff --git a/tests/libc/signal_h.c b/tests/libc/signal_h.c
index bfb2fb979f9..0ece2aacd90 100644
--- a/tests/libc/signal_h.c
+++ b/tests/libc/signal_h.c
@@ -1,8 +1,8 @@
/* run.config
STDOPT: #"-eva-slevel 2"
*/
+#include <errno.h>
#include <signal.h>
-
volatile int nondet;
int main() {
@@ -54,5 +54,12 @@ int main() {
//@ assert valid_nsig: NSIG >= 0;
+ if (nondet) {
+ errno = 0;
+ int r = sigsuspend(&s);
+ //@ assert sigsuspend_errno_eintr: errno == EINTR;
+ //@ assert sigsuspend_return: r == -1;
+ }
+
return 0;
}
diff --git a/tests/syntax/oracle/signal.res.oracle b/tests/syntax/oracle/signal.res.oracle
index 8ce74a3d613..cda400014c7 100644
--- a/tests/syntax/oracle/signal.res.oracle
+++ b/tests/syntax/oracle/signal.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing signal.c (with preprocessing)
/* Generated by Frama-C */
+#include "errno.h"
#include "signal.h"
void f(void)
{
--
GitLab