From e280469cee39b4d4a4529ee63f4560f6fb1d6bc9 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 28 Feb 2023 18:19:20 +0100
Subject: [PATCH] [machdep] add ssize_t and weof to schema + auto regenerate
default machdeps
Now, only msvc_x86_64 and gcc_x86_16 need to be edited by hand when schema changes
---
share/machdeps/Makefile | 20 ++++++++++
share/machdeps/machdep-schema.yaml | 12 ++++++
share/machdeps/machdep_avr_16.yaml | 3 +-
share/machdeps/machdep_gcc_x86_16.yaml | 2 +
share/machdeps/machdep_gcc_x86_32.yaml | 2 +
share/machdeps/machdep_gcc_x86_64.yaml | 3 +-
share/machdeps/machdep_msvc_x86_64.yaml | 2 +
share/machdeps/machdep_ppc_32.yaml | 3 +-
share/machdeps/machdep_x86_16.yaml | 2 +
share/machdeps/machdep_x86_32.yaml | 4 +-
share/machdeps/machdep_x86_64.yaml | 4 +-
share/machdeps/make_machdep/make_machdep.py | 38 +++++++++++++++++--
share/machdeps/make_machdep/ssize_t.c | 30 +++++++++++++++
share/machdeps/make_machdep/weof.c | 3 ++
src/kernel_internals/runtime/machdep.ml | 6 +--
src/kernel_services/ast_data/cil_types.ml | 2 +
.../ast_queries/cil_datatype.ml | 2 +
tests/misc/custom_machdep.ml | 2 +
tests/misc/custom_machdep.yaml | 2 +
tests/syntax/machdep_char_unsigned.ml | 3 +-
20 files changed, 133 insertions(+), 12 deletions(-)
create mode 100644 share/machdeps/Makefile
create mode 100644 share/machdeps/make_machdep/ssize_t.c
create mode 100644 share/machdeps/make_machdep/weof.c
diff --git a/share/machdeps/Makefile b/share/machdeps/Makefile
new file mode 100644
index 00000000000..348bb70e140
--- /dev/null
+++ b/share/machdeps/Makefile
@@ -0,0 +1,20 @@
+update-all: machdep_*.yaml
+
+machdep_avr_16.yaml \
+machdep_gcc_x86_32.yaml \
+machdep_gcc_x86_64.yaml \
+machdep_ppc_32.yaml : \
+%.yaml: machdep-schema.yaml make_machdep/make_machdep.py
+ @./make_machdep/make_machdep.py -i --from-file $@ --check
+
+machdep_x86_16.yaml machdep_x86_32.yaml machdep_x86_64.yaml: \
+machdep_%.yaml: machdep_gcc_%.yaml Makefile
+ @sed -e 's/sizeof_fun: .*/sizeof_fun: -1/' \
+ -e 's/sizeof_void: .*/sizeof_void: -1/' \
+ -e 's/alignof_fun: .*/alignof_fun: -1/' \
+ -e 's/compiler: .*/compiler: generic/' \
+ $< > $@
+
+machdep_gcc_x86_16.yaml machdep_msvc_x86_64.yaml: %.yaml: machdep-schema.yaml
+ @echo "$@ is newer than $< and must be updated manually"
+ @exit 1
diff --git a/share/machdeps/machdep-schema.yaml b/share/machdeps/machdep-schema.yaml
index cbc7163ae36..a48241896c2 100644
--- a/share/machdeps/machdep-schema.yaml
+++ b/share/machdeps/machdep-schema.yaml
@@ -179,6 +179,12 @@ sizeof_void:
type: integer
+ssize_t:
+
+ description: definition of 'ssize_t' (POSIX standard type)
+
+ type: string
+
uintptr_t:
description: definition of 'uintptr_t'
@@ -197,6 +203,12 @@ wchar_t:
type: string
+weof:
+
+ description: value of 'WEOF' macro
+
+ type: string
+
wint_t:
description: definition of 'wint_t'
diff --git a/share/machdeps/machdep_avr_16.yaml b/share/machdeps/machdep_avr_16.yaml
index ec24d4f54c5..be755d979fb 100644
--- a/share/machdeps/machdep_avr_16.yaml
+++ b/share/machdeps/machdep_avr_16.yaml
@@ -30,8 +30,9 @@ sizeof_longlong: 8
sizeof_ptr: 2
sizeof_short: 2
sizeof_void: 1
+ssize_t: int
uintptr_t: unsigned int
version: clang version 15.0.7
wchar_t: int
+weof: (0xffffffffu)
wint_t: int
-
diff --git a/share/machdeps/machdep_gcc_x86_16.yaml b/share/machdeps/machdep_gcc_x86_16.yaml
index 7e4f537bb2c..f15c429e025 100644
--- a/share/machdeps/machdep_gcc_x86_16.yaml
+++ b/share/machdeps/machdep_gcc_x86_16.yaml
@@ -28,7 +28,9 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: 1
+ssize_t: int
uintptr_t: unsigned long
version: none
wchar_t: int
+weof: (0xffffffffUL)
wint_t: unsigned long
diff --git a/share/machdeps/machdep_gcc_x86_32.yaml b/share/machdeps/machdep_gcc_x86_32.yaml
index 66e15e9ca00..c2b6c927b7b 100644
--- a/share/machdeps/machdep_gcc_x86_32.yaml
+++ b/share/machdeps/machdep_gcc_x86_32.yaml
@@ -28,7 +28,9 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: 1
+ssize_t: int
uintptr_t: unsigned int
version: gcc (GCC) 12.2.1 20230201
wchar_t: long
+weof: (0xffffffffu)
wint_t: unsigned int
diff --git a/share/machdeps/machdep_gcc_x86_64.yaml b/share/machdeps/machdep_gcc_x86_64.yaml
index cd58ca56090..be370464cd6 100644
--- a/share/machdeps/machdep_gcc_x86_64.yaml
+++ b/share/machdeps/machdep_gcc_x86_64.yaml
@@ -28,8 +28,9 @@ sizeof_longlong: 8
sizeof_ptr: 8
sizeof_short: 2
sizeof_void: 1
+ssize_t: long
uintptr_t: unsigned long
version: gcc (GCC) 12.2.1 20230201
wchar_t: int
+weof: (0xffffffffu)
wint_t: unsigned int
-
diff --git a/share/machdeps/machdep_msvc_x86_64.yaml b/share/machdeps/machdep_msvc_x86_64.yaml
index b39d6e20ca8..b530584b990 100644
--- a/share/machdeps/machdep_msvc_x86_64.yaml
+++ b/share/machdeps/machdep_msvc_x86_64.yaml
@@ -28,7 +28,9 @@ sizeof_longlong: 8
sizeof_ptr: 8
sizeof_short: 2
sizeof_void: 0
+ssize_t: long long
uintptr_t: unsigned long long
version: MSVC - X86-64bits mode
wchar_t: unsigned short
+weof: (0xffffU)
wint_t: unsigned short
diff --git a/share/machdeps/machdep_ppc_32.yaml b/share/machdeps/machdep_ppc_32.yaml
index 304e2140688..7f0e1a922d1 100644
--- a/share/machdeps/machdep_ppc_32.yaml
+++ b/share/machdeps/machdep_ppc_32.yaml
@@ -30,8 +30,9 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: 1
+ssize_t: int
uintptr_t: unsigned int
version: clang version 15.0.7
wchar_t: int
+weof: (0xffffffffu)
wint_t: unsigned int
-
diff --git a/share/machdeps/machdep_x86_16.yaml b/share/machdeps/machdep_x86_16.yaml
index cf3183d3458..0ef5ad977a0 100644
--- a/share/machdeps/machdep_x86_16.yaml
+++ b/share/machdeps/machdep_x86_16.yaml
@@ -28,7 +28,9 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: -1
+ssize_t: int
uintptr_t: unsigned long
version: none
wchar_t: int
+weof: (0xffffffffUL)
wint_t: unsigned long
diff --git a/share/machdeps/machdep_x86_32.yaml b/share/machdeps/machdep_x86_32.yaml
index 344ef9ad036..cf02c8f3bfc 100644
--- a/share/machdeps/machdep_x86_32.yaml
+++ b/share/machdeps/machdep_x86_32.yaml
@@ -28,7 +28,9 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: -1
-uintptr_t: unsigned
+ssize_t: int
+uintptr_t: unsigned int
version: gcc (GCC) 12.2.1 20230201
wchar_t: long
+weof: (0xffffffffu)
wint_t: unsigned int
diff --git a/share/machdeps/machdep_x86_64.yaml b/share/machdeps/machdep_x86_64.yaml
index ff21378b903..8d9a2386e8f 100644
--- a/share/machdeps/machdep_x86_64.yaml
+++ b/share/machdeps/machdep_x86_64.yaml
@@ -28,7 +28,9 @@ sizeof_longlong: 8
sizeof_ptr: 8
sizeof_short: 2
sizeof_void: -1
+ssize_t: long
uintptr_t: unsigned long
-version: clang version 15.0.7
+version: gcc (GCC) 12.2.1 20230201
wchar_t: int
+weof: (0xffffffffu)
wint_t: unsigned int
diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py
index 0a61c5e6693..e8766ab6cee 100755
--- a/share/machdeps/make_machdep/make_machdep.py
+++ b/share/machdeps/make_machdep/make_machdep.py
@@ -108,8 +108,6 @@ def print_machdep(machdep):
if args.in_place:
args.dest_file = open(args.from_file, "w")
yaml.dump(machdep, args.dest_file, indent=4, sort_keys=True)
- # Python does not end the dump with a newline by itself
- args.dest_file.write("\n")
def make_schema():
schema_filename = my_path.parent / "machdep-schema.yaml"
@@ -162,6 +160,7 @@ source_files = [
("alignof_str.c", "number"),
("alignof_aligned.c", "number"),
("size_t.c", "type"),
+ ("ssize_t.c", "type"),
("wchar_t.c", "type"),
("ptrdiff_t.c", "type"),
("intptr_t.c", "type"),
@@ -170,6 +169,7 @@ source_files = [
("char_is_unsigned.c", "bool"),
("little_endian.c", "bool"),
("has__builtin_va_list.c", "has__builtin_va_list"),
+ ("weof.c", "macro"),
]
@@ -191,7 +191,6 @@ def find_value(name, typ, output):
def conversion(x):
return x
-
else:
warnings.warn(f"unexpected type '{typ}' for field '{name}', skipping")
return
@@ -210,14 +209,47 @@ def find_value(name, typ, output):
if args.verbose:
print(f"compiler output is:{output}")
+def cleanup_cpp(output):
+ lines = output.splitlines()
+ macro = filter(lambda s: s != '' and s[0] != '#', lines)
+ macro = map(lambda s: s.strip(),macro)
+ return ' '.join(macro)
+
+def find_macro_value(name,output):
+ msg = re.compile(name + "_is = ([^;]+);")
+ res = re.search(msg,output)
+ if res:
+ if name in machdep:
+ value = res.group(1).strip()
+ if args.verbose:
+ print(f"[INFO] setting {name} to {value}")
+ machdep[name] = value
+ else:
+ warnings.warn(f"unexpected symbol '{name}', ignoring")
+ else:
+ warnings.warn(f"cannot find value of field '{name}', skipping")
+ if args.verbose:
+ print(f"compiler output is:{output}")
for (f, typ) in source_files:
p = my_path / f
cmd = compilation_command + [str(p)]
+ if typ == "macro":
+ # We're just interested in expanding a macro,
+ # treatment is a bit different than the rest.
+ cmd = cmd + ["-E"]
if args.verbose:
print(f"[INFO] running command: {' '.join(cmd)}")
proc = subprocess.run(cmd, capture_output=True)
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")
+ if args.verbose:
+ print(f"compiler output is:{proc.stderr.decode()}")
+ continue
+ find_macro_value(p.stem,cleanup_cpp(proc.stdout.decode()))
+ continue
if typ == "has__builtin_va_list":
# Special case: compilation success determines presence or absence
machdep["has__builtin_va_list"] = proc.returncode == 0
diff --git a/share/machdeps/make_machdep/ssize_t.c b/share/machdeps/make_machdep/ssize_t.c
new file mode 100644
index 00000000000..95260cbfc10
--- /dev/null
+++ b/share/machdeps/make_machdep/ssize_t.c
@@ -0,0 +1,30 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2023 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#include "make_machdep_common.h"
+#include <sys/types.h>
+
+#define TEST_TYPE ssize_t
+
+TEST_TYPE_IS(int)
+TEST_TYPE_IS(long)
+TEST_TYPE_IS(long long)
diff --git a/share/machdeps/make_machdep/weof.c b/share/machdeps/make_machdep/weof.c
new file mode 100644
index 00000000000..67d58eb031c
--- /dev/null
+++ b/share/machdeps/make_machdep/weof.c
@@ -0,0 +1,3 @@
+#include <wchar.h>
+
+const wint_t weof_is = WEOF;
diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml
index e2daa153cec..1caae68014c 100644
--- a/src/kernel_internals/runtime/machdep.ml
+++ b/src/kernel_internals/runtime/machdep.ml
@@ -189,19 +189,19 @@ let gen_all_defines fmt mach =
gen_define_string fmt "__UINTPTR_T" mach.uintptr_t;
gen_define_string fmt "__PTRDIFF_T" mach.ptrdiff_t;
gen_define_string fmt "__WINT_T" mach.wint_t;
- (* gen_define_string fmt "__SSIZE_T" mach.ssize_t; *)
+ gen_define_string fmt "__SSIZE_T" mach.ssize_t;
gen_intlike_max fmt "__FC_SIZE" mach.size_t mach;
gen_intlike_min fmt "__FC_INTPTR" mach.intptr_t mach;
gen_intlike_max fmt "__FC_INTPTR" mach.intptr_t mach;
gen_intlike_max fmt "__FC_UINTPTR" mach.uintptr_t mach;
gen_intlike_min fmt "__FC_WCHAR" mach.wchar_t mach;
gen_intlike_max fmt "__FC_WCHAR" mach.wchar_t mach;
- (* TODO: __SSIZE_MAX *)
+ gen_intlike_max fmt "__SSIZE_MAX" mach.ssize_t mach;
gen_intlike_min fmt "__FC_PTRDIFF" mach.ptrdiff_t 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;
- (* TODO: __FC_WEOF *)
+ gen_define_string 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"
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index b80ed81244c..1b77b2e5856 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1876,6 +1876,7 @@ type mach = {
sizeof_void: int; (* Size of "void" *)
sizeof_fun: int; (* Size of function. Negative if unsupported. *)
size_t: string; (* Type of "sizeof(T)" *)
+ ssize_t: string; (* representation of ssize_t *)
wchar_t: string; (* Type of "wchar_t" *)
ptrdiff_t: string; (* Type of "ptrdiff_t" *)
intptr_t: string; (* Type of "intptr_t" *)
@@ -1900,6 +1901,7 @@ 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 *)
}
(*
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 72e9e135a1e..8819cba4a61 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2640,6 +2640,7 @@ let dummy_machdep =
sizeof_void = -1;
sizeof_fun = -1;
size_t = "unsigned long";
+ ssize_t = "long";
wchar_t = "int";
ptrdiff_t = "long";
intptr_t = "long"; (* Type of "intptr_t" *)
@@ -2662,6 +2663,7 @@ let dummy_machdep =
compiler = "none";
cpp_arch_flags = [];
version = "N/A";
+ weof = "(-1)"
}
module Machdep = Datatype.Make_with_collections(struct
diff --git a/tests/misc/custom_machdep.ml b/tests/misc/custom_machdep.ml
index 7d929b77693..fc497312b09 100644
--- a/tests/misc/custom_machdep.ml
+++ b/tests/misc/custom_machdep.ml
@@ -16,6 +16,7 @@ let mach =
sizeof_void = 1;
sizeof_fun = 1;
size_t = "unsigned long";
+ ssize_t = "long";
intptr_t = "long";
uintptr_t = "unsigned long";
wint_t = "int";
@@ -35,6 +36,7 @@ let mach =
char_is_unsigned = false;
little_endian = true;
has__builtin_va_list = true;
+ weof = "(-1)";
}
let mach2 = { mach with compiler = "baz" }
diff --git a/tests/misc/custom_machdep.yaml b/tests/misc/custom_machdep.yaml
index 67b759afe50..11e6ed0cab1 100644
--- a/tests/misc/custom_machdep.yaml
+++ b/tests/misc/custom_machdep.yaml
@@ -29,5 +29,7 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: 1
+ssize_t: long
version: foo
wchar_t: int
+weof: (-1)
diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml
index 9ccf6d9691e..51b9b7655e2 100644
--- a/tests/syntax/machdep_char_unsigned.ml
+++ b/tests/syntax/machdep_char_unsigned.ml
@@ -1,4 +1,3 @@
-
open Cil_types
let md = {
@@ -29,12 +28,14 @@ let md = {
char_is_unsigned = true;
little_endian = true;
size_t = "unsigned int";
+ ssize_t = "int";
wchar_t = "int";
intptr_t = "int";
uintptr_t = "unsigned int";
ptrdiff_t = "int";
wint_t = "long";
has__builtin_va_list = true;
+ weof = "(-1L)"
}
let () =
--
GitLab