From 1e6f913593d3a32584f721e1a0441cf96b845eb7 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 21 Mar 2024 11:27:22 +0100
Subject: [PATCH] [Libc] add __FC_PTHREAD_T_IS_SCALAR to handle non-portable
code
---
share/libc/__fc_define_pthread_types.h | 7 ++
...ad_h.res.oracle => pthread_h.0.res.oracle} | 52 +++++-----
tests/libc/oracle/pthread_h.1.res.oracle | 94 +++++++++++++++++++
tests/libc/oracle/pthread_h.2.res.oracle | 10 ++
tests/libc/pthread_h.c | 14 +++
5 files changed, 151 insertions(+), 26 deletions(-)
rename tests/libc/oracle/{pthread_h.res.oracle => pthread_h.0.res.oracle} (79%)
create mode 100644 tests/libc/oracle/pthread_h.1.res.oracle
create mode 100644 tests/libc/oracle/pthread_h.2.res.oracle
diff --git a/share/libc/__fc_define_pthread_types.h b/share/libc/__fc_define_pthread_types.h
index 391d2ae3a1a..d7be74b4d9d 100644
--- a/share/libc/__fc_define_pthread_types.h
+++ b/share/libc/__fc_define_pthread_types.h
@@ -44,7 +44,14 @@ typedef struct __fc_pthread_once_t { int _fc; } pthread_once_t;
typedef struct __fc_pthread_rwlock_t { int _fc; } pthread_rwlock_t;
typedef struct __fc_pthread_rwlockattr_t { int _fc; } pthread_rwlockattr_t;
typedef struct __fc_pthread_spinlock_t { int _fc; } pthread_spinlock_t;
+
+#ifdef __FC_PTHREAD_T_IS_SCALAR
+// Some non-portable code assumes pthread_t as a scalar; this allows
+// such code to be parsed.
+typedef unsigned long pthread_t;
+#else
typedef struct __fc_pthread_t { int _fc; } pthread_t;
+#endif
__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/tests/libc/oracle/pthread_h.res.oracle b/tests/libc/oracle/pthread_h.0.res.oracle
similarity index 79%
rename from tests/libc/oracle/pthread_h.res.oracle
rename to tests/libc/oracle/pthread_h.0.res.oracle
index 6511a6631d2..41d84474ca4 100644
--- a/tests/libc/oracle/pthread_h.res.oracle
+++ b/tests/libc/oracle/pthread_h.0.res.oracle
@@ -6,73 +6,73 @@
retval ∈ {0}
v ∈ [--..--]
[eva] computing for function pthread_create <- main.
- Called from pthread_h.c:17.
+ Called from pthread_h.c:23.
[eva] using specification for function pthread_create
-[eva] pthread_h.c:17:
+[eva] pthread_h.c:23:
function pthread_create: precondition 'valid_thread' got status valid.
-[eva] pthread_h.c:17:
+[eva] pthread_h.c:23:
function pthread_create: precondition 'valid_null_attr' got status valid.
-[eva] pthread_h.c:17:
+[eva] pthread_h.c:23:
function pthread_create: precondition 'valid_routine' got status valid.
-[eva] pthread_h.c:17:
+[eva] pthread_h.c:23:
function pthread_create: precondition 'valid_null_arg' got status valid.
[eva] Done for function pthread_create
[eva] computing for function printf_va_2 <- main.
- Called from pthread_h.c:19.
+ Called from pthread_h.c:25.
[eva] using specification for function printf_va_2
-[eva] pthread_h.c:19: function printf_va_2: precondition got status valid.
+[eva] pthread_h.c:25: function printf_va_2: precondition got status valid.
[eva] Done for function printf_va_2
[eva] computing for function printf_va_3 <- main.
- Called from pthread_h.c:22.
+ Called from pthread_h.c:28.
[eva] using specification for function printf_va_3
-[eva] pthread_h.c:22: function printf_va_3: precondition got status valid.
+[eva] pthread_h.c:28: function printf_va_3: precondition got status valid.
[eva] Done for function printf_va_3
[eva] computing for function pthread_setname_np <- main.
- Called from pthread_h.c:23.
+ Called from pthread_h.c:29.
[eva] using specification for function pthread_setname_np
-[eva] pthread_h.c:23:
+[eva] pthread_h.c:29:
function pthread_setname_np: precondition 'valid_name' got status valid.
[eva] Done for function pthread_setname_np
[eva] computing for function pthread_getname_np <- main.
- Called from pthread_h.c:26.
+ Called from pthread_h.c:32.
[eva] using specification for function pthread_getname_np
-[eva] pthread_h.c:26:
+[eva] pthread_h.c:32:
function pthread_getname_np: precondition 'valid_name' got status valid.
[eva] Done for function pthread_getname_np
[eva] computing for function printf_va_4 <- main.
- Called from pthread_h.c:27.
+ Called from pthread_h.c:33.
[eva] using specification for function printf_va_4
-[eva:alarm] pthread_h.c:27: Warning:
+[eva:alarm] pthread_h.c:33: Warning:
function printf_va_4: precondition valid_read_string(param0) got status unknown.
-[eva] pthread_h.c:27:
+[eva] pthread_h.c:33:
function printf_va_4: precondition valid_read_string(format) got status valid.
[eva] Done for function printf_va_4
[eva] computing for function start_routine <- main.
- Called from pthread_h.c:32.
+ Called from pthread_h.c:38.
[eva] computing for function printf_va_1 <- start_routine <- main.
- Called from pthread_h.c:8.
+ Called from pthread_h.c:14.
[eva] using specification for function printf_va_1
-[eva] pthread_h.c:8: function printf_va_1: precondition got status valid.
+[eva] pthread_h.c:14: function printf_va_1: precondition got status valid.
[eva] Done for function printf_va_1
[eva] Recording results for start_routine
[eva] Done for function start_routine
[eva] computing for function pthread_join <- main.
- Called from pthread_h.c:34.
+ Called from pthread_h.c:40.
[eva] using specification for function pthread_join
-[eva] pthread_h.c:34:
+[eva] pthread_h.c:40:
function pthread_join: precondition 'valid_or_null_retval' got status valid.
[eva] Done for function pthread_join
[eva] computing for function printf_va_5 <- main.
- Called from pthread_h.c:36.
+ Called from pthread_h.c:42.
[eva] using specification for function printf_va_5
-[eva] pthread_h.c:36: function printf_va_5: precondition got status valid.
+[eva] pthread_h.c:42: function printf_va_5: precondition got status valid.
[eva] Done for function printf_va_5
-[eva:alarm] pthread_h.c:39: Warning:
+[eva:alarm] pthread_h.c:45: Warning:
out of bounds read. assert \valid_read(retv);
[eva] computing for function printf_va_6 <- main.
- Called from pthread_h.c:39.
+ Called from pthread_h.c:45.
[eva] using specification for function printf_va_6
-[eva] pthread_h.c:39: function printf_va_6: precondition got status valid.
+[eva] pthread_h.c:45: function printf_va_6: precondition got status valid.
[eva] Done for function printf_va_6
[eva] Recording results for main
[eva] Done for function main
diff --git a/tests/libc/oracle/pthread_h.1.res.oracle b/tests/libc/oracle/pthread_h.1.res.oracle
new file mode 100644
index 00000000000..e9962e514fb
--- /dev/null
+++ b/tests/libc/oracle/pthread_h.1.res.oracle
@@ -0,0 +1,94 @@
+[kernel] Parsing pthread_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
+ retval ∈ {0}
+ v ∈ [--..--]
+[eva] computing for function pthread_create <- main.
+ Called from pthread_h.c:23.
+[eva] using specification for function pthread_create
+[eva] pthread_h.c:23:
+ function pthread_create: precondition 'valid_thread' got status valid.
+[eva] pthread_h.c:23:
+ function pthread_create: precondition 'valid_null_attr' got status valid.
+[eva] pthread_h.c:23:
+ function pthread_create: precondition 'valid_routine' got status valid.
+[eva] pthread_h.c:23:
+ function pthread_create: precondition 'valid_null_arg' got status valid.
+[eva] Done for function pthread_create
+[eva] computing for function printf_va_2 <- main.
+ Called from pthread_h.c:25.
+[eva] using specification for function printf_va_2
+[eva] pthread_h.c:25: function printf_va_2: precondition got status valid.
+[eva] Done for function printf_va_2
+[eva] computing for function printf_va_3 <- main.
+ Called from pthread_h.c:28.
+[eva] using specification for function printf_va_3
+[eva] pthread_h.c:28: function printf_va_3: precondition got status valid.
+[eva] Done for function printf_va_3
+[eva:alarm] pthread_h.c:29: Warning:
+ accessing uninitialized left-value. assert \initialized(&thread);
+[eva] computing for function pthread_setname_np <- main.
+ Called from pthread_h.c:29.
+[eva] using specification for function pthread_setname_np
+[eva] pthread_h.c:29:
+ function pthread_setname_np: precondition 'valid_name' got status valid.
+[eva] Done for function pthread_setname_np
+[eva] computing for function pthread_getname_np <- main.
+ Called from pthread_h.c:32.
+[eva] using specification for function pthread_getname_np
+[eva] pthread_h.c:32:
+ function pthread_getname_np: precondition 'valid_name' got status valid.
+[eva] Done for function pthread_getname_np
+[eva] computing for function printf_va_4 <- main.
+ Called from pthread_h.c:33.
+[eva] using specification for function printf_va_4
+[eva:alarm] pthread_h.c:33: Warning:
+ function printf_va_4: precondition valid_read_string(param0) got status unknown.
+[eva] pthread_h.c:33:
+ function printf_va_4: precondition valid_read_string(format) got status valid.
+[eva] Done for function printf_va_4
+[eva] computing for function start_routine <- main.
+ Called from pthread_h.c:38.
+[eva] computing for function printf_va_1 <- start_routine <- main.
+ Called from pthread_h.c:14.
+[eva] using specification for function printf_va_1
+[eva] pthread_h.c:14: function printf_va_1: precondition got status valid.
+[eva] Done for function printf_va_1
+[eva] Recording results for start_routine
+[eva] Done for function start_routine
+[eva] computing for function pthread_join <- main.
+ Called from pthread_h.c:40.
+[eva] using specification for function pthread_join
+[eva] pthread_h.c:40:
+ function pthread_join: precondition 'valid_or_null_retval' got status valid.
+[eva] Done for function pthread_join
+[eva] computing for function printf_va_5 <- main.
+ Called from pthread_h.c:42.
+[eva] using specification for function printf_va_5
+[eva] pthread_h.c:42: function printf_va_5: precondition got status valid.
+[eva] Done for function printf_va_5
+[eva:alarm] pthread_h.c:45: Warning:
+ out of bounds read. assert \valid_read(retv);
+[eva] computing for function printf_va_6 <- main.
+ Called from pthread_h.c:45.
+[eva] using specification for function printf_va_6
+[eva] pthread_h.c:45: function printf_va_6: precondition got status valid.
+[eva] Done for function printf_va_6
+[eva] Recording results for main
+[eva] Done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function start_routine:
+ retval ∈ {43}
+ __retres ∈ {{ (void *)&retval }}
+ S___fc_stdout[0..1] ∈ [--..--]
+[eva:final-states] Values at end of function main:
+ retval ∈ {0; 43}
+ thread ∈ [--..--] or UNINITIALIZED
+ thread_arg ∈ {42}
+ r ∈ [--..--]
+ buf[0..15] ∈ [--..--] or UNINITIALIZED
+ retv ∈ {{ NULL + [--..--] ; &retval }} or UNINITIALIZED
+ __retres ∈ {0; 1; 2}
+ S___fc_stdout[0..1] ∈ [--..--]
diff --git a/tests/libc/oracle/pthread_h.2.res.oracle b/tests/libc/oracle/pthread_h.2.res.oracle
new file mode 100644
index 00000000000..e4df7ae1f77
--- /dev/null
+++ b/tests/libc/oracle/pthread_h.2.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing pthread_h.c (with preprocessing)
+[kernel] pthread_h.c:49: User Error:
+ cannot perform the following comparison thread == 0
+ 47 // Test non-portable usage of pthread_t
+ 48 #ifdef NON_PORTABLE
+ 49 if (thread == 0) {
+ ^^^^^^^^^^^
+ 50 return 2;
+ 51 }
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/libc/pthread_h.c b/tests/libc/pthread_h.c
index 28ba09c9d47..5b875173489 100644
--- a/tests/libc/pthread_h.c
+++ b/tests/libc/pthread_h.c
@@ -1,3 +1,9 @@
+/*run.config
+ STDOPT:
+ STDOPT: -cpp-extra-args="-D__FC_PTHREAD_T_IS_SCALAR -DNON_PORTABLE"
+ EXIT: 1
+ STDOPT: -cpp-extra-args="-DNON_PORTABLE"
+ */
#define _GNU_SOURCE // if you want to compile with GCC
#include <pthread.h>
#include <stdio.h>
@@ -37,5 +43,13 @@ int main() {
return 1;
}
printf("pthread_join succeeded, retval = %d\n", *retv);
+
+ // Test non-portable usage of pthread_t
+#ifdef NON_PORTABLE
+ if (thread == 0) {
+ return 2;
+ }
+#endif
+
return 0;
}
--
GitLab