From 529a37564bf18de4ebddcb6e120f1b6711d802bc Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 1 Mar 2023 14:28:58 +0100
Subject: [PATCH] [machdep] add posix_version and wordsize fields to schema
---
share/libc/unistd.h | 7 +++++++
share/machdeps/machdep-schema.yaml | 11 +++++++++++
share/machdeps/machdep_avr_16.yaml | 2 ++
share/machdeps/machdep_gcc_x86_16.yaml | 2 ++
share/machdeps/machdep_gcc_x86_32.yaml | 2 ++
share/machdeps/machdep_gcc_x86_64.yaml | 2 ++
share/machdeps/machdep_msvc_x86_64.yaml | 2 ++
share/machdeps/machdep_ppc_32.yaml | 2 ++
share/machdeps/machdep_x86_16.yaml | 2 ++
share/machdeps/machdep_x86_32.yaml | 2 ++
share/machdeps/machdep_x86_64.yaml | 2 ++
share/machdeps/make_machdep/make_machdep.py | 11 +++++++++--
share/machdeps/make_machdep/posix_version.c | 3 +++
share/machdeps/make_machdep/wordsize.c | 2 ++
src/kernel_internals/runtime/machdep.ml | 11 +++++++----
src/kernel_services/ast_data/cil_types.ml | 4 +++-
src/kernel_services/ast_queries/cil_datatype.ml | 4 +++-
tests/misc/custom_machdep.ml | 2 ++
tests/misc/custom_machdep.yaml | 2 ++
tests/syntax/machdep_char_unsigned.ml | 4 +++-
20 files changed, 70 insertions(+), 9 deletions(-)
create mode 100644 share/machdeps/make_machdep/posix_version.c
create mode 100644 share/machdeps/make_machdep/wordsize.c
diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index b6e8f0b5462..a5ba5bf7da3 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -38,6 +38,13 @@ __PUSH_FC_STDLIB
#include "__fc_define_intptr_t.h"
#include "__fc_define_fds.h"
#include "limits.h"
+
+#ifndef __FC_POSIX_VERSION
+#error "unistd.h should only be included with a POSIX machdep"
+#endif
+
+#define _POSIX_VERSION __FC_POSIX_VERSION
+
__BEGIN_DECLS
extern volatile int Frama_C_entropy_source;
diff --git a/share/machdeps/machdep-schema.yaml b/share/machdeps/machdep-schema.yaml
index a48241896c2..3b0ea4d4f2b 100644
--- a/share/machdeps/machdep-schema.yaml
+++ b/share/machdeps/machdep-schema.yaml
@@ -107,6 +107,11 @@ little_endian:
type: boolean
+posix_version:
+ description: |
+ value of the macro '_POSIX_VERSION'
+ leave empty for non-POSIX systems
+
ptrdiff_t:
description: definition of 'ptrdiff_t'
@@ -214,3 +219,9 @@ wint_t:
description: definition of 'wint_t'
type: string
+
+wordsize:
+
+ description: value of "__WORDSIZE" macro
+
+ type: string
diff --git a/share/machdeps/machdep_avr_16.yaml b/share/machdeps/machdep_avr_16.yaml
index be755d979fb..6f2e4bec15e 100644
--- a/share/machdeps/machdep_avr_16.yaml
+++ b/share/machdeps/machdep_avr_16.yaml
@@ -18,6 +18,7 @@ cpp_arch_flags:
has__builtin_va_list: true
intptr_t: int
little_endian: true
+posix_version: 200809L
ptrdiff_t: int
size_t: unsigned int
sizeof_double: 4
@@ -36,3 +37,4 @@ version: clang version 15.0.7
wchar_t: int
weof: (0xffffffffu)
wint_t: int
+wordsize: '32'
diff --git a/share/machdeps/machdep_gcc_x86_16.yaml b/share/machdeps/machdep_gcc_x86_16.yaml
index f15c429e025..007ce9e7d3f 100644
--- a/share/machdeps/machdep_gcc_x86_16.yaml
+++ b/share/machdeps/machdep_gcc_x86_16.yaml
@@ -34,3 +34,5 @@ version: none
wchar_t: int
weof: (0xffffffffUL)
wint_t: unsigned long
+wordsize: '16'
+posix_version: '200809L'
diff --git a/share/machdeps/machdep_gcc_x86_32.yaml b/share/machdeps/machdep_gcc_x86_32.yaml
index c2b6c927b7b..ed625f542eb 100644
--- a/share/machdeps/machdep_gcc_x86_32.yaml
+++ b/share/machdeps/machdep_gcc_x86_32.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
has__builtin_va_list: true
intptr_t: int
little_endian: true
+posix_version: 200809L
ptrdiff_t: int
size_t: unsigned int
sizeof_double: 8
@@ -34,3 +35,4 @@ version: gcc (GCC) 12.2.1 20230201
wchar_t: long
weof: (0xffffffffu)
wint_t: unsigned int
+wordsize: '32'
diff --git a/share/machdeps/machdep_gcc_x86_64.yaml b/share/machdeps/machdep_gcc_x86_64.yaml
index be370464cd6..b3b1c4b03b3 100644
--- a/share/machdeps/machdep_gcc_x86_64.yaml
+++ b/share/machdeps/machdep_gcc_x86_64.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
has__builtin_va_list: true
intptr_t: long
little_endian: true
+posix_version: 200809L
ptrdiff_t: long
size_t: unsigned long
sizeof_double: 8
@@ -34,3 +35,4 @@ version: gcc (GCC) 12.2.1 20230201
wchar_t: int
weof: (0xffffffffu)
wint_t: unsigned int
+wordsize: '64'
diff --git a/share/machdeps/machdep_msvc_x86_64.yaml b/share/machdeps/machdep_msvc_x86_64.yaml
index b530584b990..c0d9ec1d73a 100644
--- a/share/machdeps/machdep_msvc_x86_64.yaml
+++ b/share/machdeps/machdep_msvc_x86_64.yaml
@@ -34,3 +34,5 @@ version: MSVC - X86-64bits mode
wchar_t: unsigned short
weof: (0xffffU)
wint_t: unsigned short
+wordsize: '64'
+posix_version: ''
diff --git a/share/machdeps/machdep_ppc_32.yaml b/share/machdeps/machdep_ppc_32.yaml
index 7f0e1a922d1..4f309f9155c 100644
--- a/share/machdeps/machdep_ppc_32.yaml
+++ b/share/machdeps/machdep_ppc_32.yaml
@@ -18,6 +18,7 @@ cpp_arch_flags:
has__builtin_va_list: true
intptr_t: int
little_endian: false
+posix_version: 200809L
ptrdiff_t: int
size_t: unsigned int
sizeof_double: 8
@@ -36,3 +37,4 @@ version: clang version 15.0.7
wchar_t: int
weof: (0xffffffffu)
wint_t: unsigned int
+wordsize: '32'
diff --git a/share/machdeps/machdep_x86_16.yaml b/share/machdeps/machdep_x86_16.yaml
index 0ef5ad977a0..8d417a3b9e1 100644
--- a/share/machdeps/machdep_x86_16.yaml
+++ b/share/machdeps/machdep_x86_16.yaml
@@ -34,3 +34,5 @@ version: none
wchar_t: int
weof: (0xffffffffUL)
wint_t: unsigned long
+wordsize: '16'
+posix_version: '200809L'
diff --git a/share/machdeps/machdep_x86_32.yaml b/share/machdeps/machdep_x86_32.yaml
index cf02c8f3bfc..ed6a4c8423e 100644
--- a/share/machdeps/machdep_x86_32.yaml
+++ b/share/machdeps/machdep_x86_32.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
has__builtin_va_list: true
intptr_t: int
little_endian: true
+posix_version: 200809L
ptrdiff_t: int
size_t: unsigned int
sizeof_double: 8
@@ -34,3 +35,4 @@ version: gcc (GCC) 12.2.1 20230201
wchar_t: long
weof: (0xffffffffu)
wint_t: unsigned int
+wordsize: '32'
diff --git a/share/machdeps/machdep_x86_64.yaml b/share/machdeps/machdep_x86_64.yaml
index 8d9a2386e8f..5e322f71b45 100644
--- a/share/machdeps/machdep_x86_64.yaml
+++ b/share/machdeps/machdep_x86_64.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
has__builtin_va_list: true
intptr_t: long
little_endian: true
+posix_version: 200809L
ptrdiff_t: long
size_t: unsigned long
sizeof_double: 8
@@ -34,3 +35,4 @@ version: gcc (GCC) 12.2.1 20230201
wchar_t: int
weof: (0xffffffffu)
wint_t: unsigned int
+wordsize: '64'
diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py
index e8766ab6cee..b1bbccd739a 100755
--- a/share/machdeps/make_machdep/make_machdep.py
+++ b/share/machdeps/make_machdep/make_machdep.py
@@ -170,6 +170,8 @@ source_files = [
("little_endian.c", "bool"),
("has__builtin_va_list.c", "has__builtin_va_list"),
("weof.c", "macro"),
+ ("wordsize.c", "macro"),
+ ("posix_version.c", "macro"),
]
@@ -227,7 +229,9 @@ def find_macro_value(name,output):
else:
warnings.warn(f"unexpected symbol '{name}', ignoring")
else:
- warnings.warn(f"cannot find value of field '{name}', skipping")
+ warnings.warn(f"cannot find value of field '{name}', treating as empty")
+ if name in machdep:
+ machdep[name] = ''
if args.verbose:
print(f"compiler output is:{output}")
@@ -244,9 +248,12 @@ for (f, typ) in source_files:
Path(f).with_suffix(".o").unlink(missing_ok=True)
if typ == "macro":
if proc.returncode != 0:
- warnings.warn(f"error in determining value of '{p,stem}', skipping")
+ warnings.warn(f"error in determining value of '{p,stem}', treating as empty")
if args.verbose:
print(f"compiler output is:{proc.stderr.decode()}")
+ name = p.stem
+ if name in machdep:
+ machdep[name] = ''
continue
find_macro_value(p.stem,cleanup_cpp(proc.stdout.decode()))
continue
diff --git a/share/machdeps/make_machdep/posix_version.c b/share/machdeps/make_machdep/posix_version.c
new file mode 100644
index 00000000000..ded2e9b3de3
--- /dev/null
+++ b/share/machdeps/make_machdep/posix_version.c
@@ -0,0 +1,3 @@
+#include <unistd.h>
+
+long posix_version_is = _POSIX_VERSION;
diff --git a/share/machdeps/make_machdep/wordsize.c b/share/machdeps/make_machdep/wordsize.c
new file mode 100644
index 00000000000..ff430111be0
--- /dev/null
+++ b/share/machdeps/make_machdep/wordsize.c
@@ -0,0 +1,2 @@
+#include <features.h>
+const int wordsize_is = __WORDSIZE;
diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml
index 1caae68014c..3df712561bd 100644
--- a/src/kernel_internals/runtime/machdep.ml
+++ b/src/kernel_internals/runtime/machdep.ml
@@ -11,6 +11,10 @@ let gen_define_string fmt macro def =
let gen_define_literal_string fmt macro def =
gen_define fmt macro Format.pp_print_string ("\"" ^ def ^ "\"")
+let gen_define_macro fmt macro def =
+ if def = "" then gen_undef fmt macro
+ else gen_define_string fmt macro def
+
let gen_define_int fmt macro def = gen_define fmt macro Format.pp_print_int def
let gen_byte_order fmt mach =
@@ -201,13 +205,13 @@ let gen_all_defines fmt mach =
gen_intlike_max fmt "__FC_PTRDIFF" mach.ptrdiff_t mach;
gen_intlike_min fmt "__FC_WINT" mach.wint_t mach;
gen_intlike_max fmt "__FC_WINT" mach.wint_t mach;
- gen_define_string fmt "__FC_WEOF" mach.weof;
+ gen_define_macro fmt "__FC_WEOF" mach.weof;
(* NB: Frama-C's inttypes.h is assuming that intptr_t and uintptr_t have the
same rank when it comes to define PRI.?PTR macros. *)
gen_define_literal_string fmt "__PRIPTR_PREFIX"
(List.assoc (no_signedness mach.intptr_t) pp_of_kind);
-
- (* TODO: __FC_POSIX_VERSION *)
+ gen_define_macro fmt "__FC_WORDSIZE" mach.wordsize;
+ gen_define_macro fmt "__FC_POSIX_VERSION" mach.posix_version;
(* TODO: __FC_HOST_NAME_MAX *)
(* TODO: __FC_TTY_NAME_MAX *)
(* TODO: __FC_SIG_ATOMIC_MIN *)
@@ -224,7 +228,6 @@ let gen_all_defines fmt mach =
(* TODO: __FC_TIME_T *)
(* TODO: __FC_NSIG *)
(* TODO: __FC__NSIG *)
- (* TODO: __WORDSIZE *)
(* TODO: gcc builtins *)
Format.fprintf fmt "#endif // __FC_MACHDEP@\n"
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 1b77b2e5856..b9361bc473e 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1901,7 +1901,9 @@ type mach = {
cpp_arch_flags: string list; (* Architecture-specific flags to be given to
the preprocessor (if supported) *)
version: string; (* Information on this machdep *)
- weof: string; (* expansion of WEOF macro *)
+ weof: string; (* expansion of WEOF macro, empty if undefined *)
+ wordsize: string; (* expansion of __WORDSIZE macro, empty if undefined *)
+ posix_version: string; (* expansion of _POSIX_VERSION macro, empty if undefined *)
}
(*
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 8819cba4a61..b6efe80bca2 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2663,7 +2663,9 @@ let dummy_machdep =
compiler = "none";
cpp_arch_flags = [];
version = "N/A";
- weof = "(-1)"
+ weof = "(-1)";
+ wordsize = "64";
+ posix_version = "";
}
module Machdep = Datatype.Make_with_collections(struct
diff --git a/tests/misc/custom_machdep.ml b/tests/misc/custom_machdep.ml
index fc497312b09..e00cd79dc58 100644
--- a/tests/misc/custom_machdep.ml
+++ b/tests/misc/custom_machdep.ml
@@ -37,6 +37,8 @@ let mach =
little_endian = true;
has__builtin_va_list = true;
weof = "(-1)";
+ wordsize = "24";
+ posix_version = "200809L";
}
let mach2 = { mach with compiler = "baz" }
diff --git a/tests/misc/custom_machdep.yaml b/tests/misc/custom_machdep.yaml
index 11e6ed0cab1..7b1dbeb487f 100644
--- a/tests/misc/custom_machdep.yaml
+++ b/tests/misc/custom_machdep.yaml
@@ -33,3 +33,5 @@ ssize_t: long
version: foo
wchar_t: int
weof: (-1)
+wordsize: '24'
+posix_version: '200809L'
diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml
index 51b9b7655e2..c35154121ae 100644
--- a/tests/syntax/machdep_char_unsigned.ml
+++ b/tests/syntax/machdep_char_unsigned.ml
@@ -35,7 +35,9 @@ let md = {
ptrdiff_t = "int";
wint_t = "long";
has__builtin_va_list = true;
- weof = "(-1L)"
+ weof = "(-1L)";
+ wordsize = "16";
+ posix_version = "";
}
let () =
--
GitLab