From d24eb65453fdb2352ee2ceddb0570f908f7624a8 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 24 Feb 2023 18:22:06 +0100
Subject: [PATCH] [machdep] import some types from __fc_machdep.h to yaml +
refactor generator
---
share/machdeps/machdep-schema.yaml | 27 ++++++++---
share/machdeps/machdep_avr_16.yaml | 4 ++
share/machdeps/machdep_gcc_x86_16.yaml | 3 ++
share/machdeps/machdep_gcc_x86_32.yaml | 3 ++
share/machdeps/machdep_gcc_x86_64.yaml | 4 ++
share/machdeps/machdep_msvc_x86_64.yaml | 3 ++
share/machdeps/machdep_ppc_32.yaml | 4 ++
share/machdeps/machdep_x86_16.yaml | 3 ++
share/machdeps/machdep_x86_32.yaml | 3 ++
share/machdeps/machdep_x86_64.yaml | 3 ++
share/machdeps/make_machdep/intptr_t.c | 29 +++++++++++
share/machdeps/make_machdep/make_machdep.py | 54 ++++++---------------
share/machdeps/make_machdep/uintptr_t.c | 29 +++++++++++
share/machdeps/make_machdep/wint_t.c | 32 ++++++++++++
14 files changed, 155 insertions(+), 46 deletions(-)
create mode 100644 share/machdeps/make_machdep/intptr_t.c
create mode 100644 share/machdeps/make_machdep/uintptr_t.c
create mode 100644 share/machdeps/make_machdep/wint_t.c
diff --git a/share/machdeps/machdep-schema.yaml b/share/machdeps/machdep-schema.yaml
index 2c3cec943e1..cbc7163ae36 100644
--- a/share/machdeps/machdep-schema.yaml
+++ b/share/machdeps/machdep-schema.yaml
@@ -60,18 +60,12 @@ alignof_short:
type: integer
-alignof_string:
+alignof_str:
description: alignment of string
type: integer
-alignof_void:
-
- description: (non-standard) alignment of 'void' type. Negative if unsupported
-
- type: integer
-
char_is_unsigned:
description: whether 'char' is unsigned
@@ -102,13 +96,18 @@ has__builtin_va_list:
type: boolean
+intptr_t:
+ description: definition of 'intptr_t'
+
+ type: string
+
little_endian:
description: whether the architecture is little-endian
type: boolean
-ptr_diff_t:
+ptrdiff_t:
description: definition of 'ptrdiff_t'
@@ -180,6 +179,12 @@ sizeof_void:
type: integer
+uintptr_t:
+
+ description: definition of 'uintptr_t'
+
+ type: string
+
version:
description: information on this machdep
@@ -191,3 +196,9 @@ wchar_t:
description: definition of 'wchar_t'
type: string
+
+wint_t:
+
+ description: definition of 'wint_t'
+
+ type: string
diff --git a/share/machdeps/machdep_avr_16.yaml b/share/machdeps/machdep_avr_16.yaml
index fdfbf0d6c9f..ec24d4f54c5 100644
--- a/share/machdeps/machdep_avr_16.yaml
+++ b/share/machdeps/machdep_avr_16.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
- avr
- -m16
has__builtin_va_list: true
+intptr_t: int
little_endian: true
ptrdiff_t: int
size_t: unsigned int
@@ -29,5 +30,8 @@ sizeof_longlong: 8
sizeof_ptr: 2
sizeof_short: 2
sizeof_void: 1
+uintptr_t: unsigned int
version: clang version 15.0.7
wchar_t: int
+wint_t: int
+
diff --git a/share/machdeps/machdep_gcc_x86_16.yaml b/share/machdeps/machdep_gcc_x86_16.yaml
index 7dc8c9fe446..7e4f537bb2c 100644
--- a/share/machdeps/machdep_gcc_x86_16.yaml
+++ b/share/machdeps/machdep_gcc_x86_16.yaml
@@ -14,6 +14,7 @@ compiler: gcc
cpp_arch_flags:
- -m16
has__builtin_va_list: true
+intptr_t: long
little_endian: true
ptrdiff_t: int
size_t: unsigned int
@@ -27,5 +28,7 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: 1
+uintptr_t: unsigned long
version: none
wchar_t: int
+wint_t: unsigned long
diff --git a/share/machdeps/machdep_gcc_x86_32.yaml b/share/machdeps/machdep_gcc_x86_32.yaml
index e98f9707ad1..66e15e9ca00 100644
--- a/share/machdeps/machdep_gcc_x86_32.yaml
+++ b/share/machdeps/machdep_gcc_x86_32.yaml
@@ -14,6 +14,7 @@ compiler: gcc
cpp_arch_flags:
- -m32
has__builtin_va_list: true
+intptr_t: int
little_endian: true
ptrdiff_t: int
size_t: unsigned int
@@ -27,5 +28,7 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: 1
+uintptr_t: unsigned int
version: gcc (GCC) 12.2.1 20230201
wchar_t: long
+wint_t: unsigned int
diff --git a/share/machdeps/machdep_gcc_x86_64.yaml b/share/machdeps/machdep_gcc_x86_64.yaml
index cfc63451a76..cd58ca56090 100644
--- a/share/machdeps/machdep_gcc_x86_64.yaml
+++ b/share/machdeps/machdep_gcc_x86_64.yaml
@@ -14,6 +14,7 @@ compiler: gcc
cpp_arch_flags:
- -m64
has__builtin_va_list: true
+intptr_t: long
little_endian: true
ptrdiff_t: long
size_t: unsigned long
@@ -27,5 +28,8 @@ sizeof_longlong: 8
sizeof_ptr: 8
sizeof_short: 2
sizeof_void: 1
+uintptr_t: unsigned long
version: gcc (GCC) 12.2.1 20230201
wchar_t: int
+wint_t: unsigned int
+
diff --git a/share/machdeps/machdep_msvc_x86_64.yaml b/share/machdeps/machdep_msvc_x86_64.yaml
index 73c60421095..b39d6e20ca8 100644
--- a/share/machdeps/machdep_msvc_x86_64.yaml
+++ b/share/machdeps/machdep_msvc_x86_64.yaml
@@ -14,6 +14,7 @@ compiler: msvc
cpp_arch_flags:
- -m64
has__builtin_va_list: false
+intptr_t: signed long long
little_endian: true
ptrdiff_t: long long
size_t: unsigned long long
@@ -27,5 +28,7 @@ sizeof_longlong: 8
sizeof_ptr: 8
sizeof_short: 2
sizeof_void: 0
+uintptr_t: unsigned long long
version: MSVC - X86-64bits mode
wchar_t: unsigned short
+wint_t: unsigned short
diff --git a/share/machdeps/machdep_ppc_32.yaml b/share/machdeps/machdep_ppc_32.yaml
index 43a2779dbd1..304e2140688 100644
--- a/share/machdeps/machdep_ppc_32.yaml
+++ b/share/machdeps/machdep_ppc_32.yaml
@@ -16,6 +16,7 @@ cpp_arch_flags:
- powerpc-apple-linux
- -mcpu=603
has__builtin_va_list: true
+intptr_t: int
little_endian: false
ptrdiff_t: int
size_t: unsigned int
@@ -29,5 +30,8 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: 1
+uintptr_t: unsigned int
version: clang version 15.0.7
wchar_t: int
+wint_t: unsigned int
+
diff --git a/share/machdeps/machdep_x86_16.yaml b/share/machdeps/machdep_x86_16.yaml
index a139bf041da..cf3183d3458 100644
--- a/share/machdeps/machdep_x86_16.yaml
+++ b/share/machdeps/machdep_x86_16.yaml
@@ -14,6 +14,7 @@ compiler: generic
cpp_arch_flags:
- -m16
has__builtin_va_list: true
+intptr_t: long
little_endian: true
ptrdiff_t: int
size_t: unsigned int
@@ -27,5 +28,7 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: -1
+uintptr_t: unsigned long
version: none
wchar_t: int
+wint_t: unsigned long
diff --git a/share/machdeps/machdep_x86_32.yaml b/share/machdeps/machdep_x86_32.yaml
index df6493927a4..344ef9ad036 100644
--- a/share/machdeps/machdep_x86_32.yaml
+++ b/share/machdeps/machdep_x86_32.yaml
@@ -14,6 +14,7 @@ compiler: generic
cpp_arch_flags:
- -m32
has__builtin_va_list: true
+intptr_t: int
little_endian: true
ptrdiff_t: int
size_t: unsigned int
@@ -27,5 +28,7 @@ sizeof_longlong: 8
sizeof_ptr: 4
sizeof_short: 2
sizeof_void: -1
+uintptr_t: unsigned
version: gcc (GCC) 12.2.1 20230201
wchar_t: long
+wint_t: unsigned int
diff --git a/share/machdeps/machdep_x86_64.yaml b/share/machdeps/machdep_x86_64.yaml
index 6ab3b343b0f..ff21378b903 100644
--- a/share/machdeps/machdep_x86_64.yaml
+++ b/share/machdeps/machdep_x86_64.yaml
@@ -14,6 +14,7 @@ compiler: generic
cpp_arch_flags:
- -m64
has__builtin_va_list: true
+intptr_t: long
little_endian: true
ptrdiff_t: long
size_t: unsigned long
@@ -27,5 +28,7 @@ sizeof_longlong: 8
sizeof_ptr: 8
sizeof_short: 2
sizeof_void: -1
+uintptr_t: unsigned long
version: clang version 15.0.7
wchar_t: int
+wint_t: unsigned int
diff --git a/share/machdeps/make_machdep/intptr_t.c b/share/machdeps/make_machdep/intptr_t.c
new file mode 100644
index 00000000000..ec1f36e633d
--- /dev/null
+++ b/share/machdeps/make_machdep/intptr_t.c
@@ -0,0 +1,29 @@
+/**************************************************************************/
+/* */
+/* 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 <stdint.h>
+#define TEST_TYPE intptr_t
+
+TEST_TYPE_IS(int);
+TEST_TYPE_IS(long);
+TEST_TYPE_IS(long long);
diff --git a/share/machdeps/make_machdep/make_machdep.py b/share/machdeps/make_machdep/make_machdep.py
index fe84a770ce4..0a61c5e6693 100755
--- a/share/machdeps/make_machdep/make_machdep.py
+++ b/share/machdeps/make_machdep/make_machdep.py
@@ -111,15 +111,17 @@ def print_machdep(machdep):
# 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"
+ with open(schema_filename, "r") as schema:
+ return yaml.safe_load(schema)
+
+schema = make_schema()
def check_machdep(machdep):
try:
from jsonschema import validate, ValidationError
-
- schema_filename = my_path.parent / "machdep-schema.json"
-
- with open(schema_filename, "r") as schema:
- validate(machdep, json.load(schema))
+ validate(machdep,schema)
except ImportError:
warnings.warn("jsonschema is not available: no validation will be performed")
except OSError:
@@ -127,40 +129,13 @@ def check_machdep(machdep):
except ValidationError:
warnings.warn("machdep object is not conforming to machdep schema")
+def make_machdep():
+ machdep = { }
+ for key in schema.keys():
+ machdep[key] = None
+ return machdep
-# This must remain synchronized with cil_types.ml's 'mach' type
-machdep = {
- "sizeof_short": None,
- "sizeof_int": None,
- "sizeof_long": None,
- "sizeof_longlong": None,
- "sizeof_ptr": None,
- "sizeof_float": None,
- "sizeof_double": None,
- "sizeof_longdouble": None,
- "sizeof_void": None,
- "sizeof_fun": None,
- "size_t": None,
- "wchar_t": None,
- "ptrdiff_t": None,
- "alignof_short": None,
- "alignof_int": None,
- "alignof_long": None,
- "alignof_longlong": None,
- "alignof_ptr": None,
- "alignof_float": None,
- "alignof_double": None,
- "alignof_longdouble": None,
- "alignof_str": None,
- "alignof_fun": None,
- "char_is_unsigned": None,
- "little_endian": None,
- "alignof_aligned": None,
- "has__builtin_va_list": None,
- "compiler": None,
- "cpp_arch_flags": None,
- "version": None,
-}
+machdep = make_machdep()
compilation_command = [args.compiler] + args.cpp_arch_flags + args.compiler_flags
@@ -189,6 +164,9 @@ source_files = [
("size_t.c", "type"),
("wchar_t.c", "type"),
("ptrdiff_t.c", "type"),
+ ("intptr_t.c", "type"),
+ ("uintptr_t.c", "type"),
+ ("wint_t.c", "type"),
("char_is_unsigned.c", "bool"),
("little_endian.c", "bool"),
("has__builtin_va_list.c", "has__builtin_va_list"),
diff --git a/share/machdeps/make_machdep/uintptr_t.c b/share/machdeps/make_machdep/uintptr_t.c
new file mode 100644
index 00000000000..655dd30616e
--- /dev/null
+++ b/share/machdeps/make_machdep/uintptr_t.c
@@ -0,0 +1,29 @@
+/**************************************************************************/
+/* */
+/* 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 <stdint.h>
+#define TEST_TYPE uintptr_t
+
+TEST_TYPE_IS(unsigned int);
+TEST_TYPE_IS(unsigned long);
+TEST_TYPE_IS(unsigned long long);
diff --git a/share/machdeps/make_machdep/wint_t.c b/share/machdeps/make_machdep/wint_t.c
new file mode 100644
index 00000000000..233eb0986e2
--- /dev/null
+++ b/share/machdeps/make_machdep/wint_t.c
@@ -0,0 +1,32 @@
+/**************************************************************************/
+/* */
+/* 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 <wchar.h>
+#define TEST_TYPE wint_t
+
+TEST_TYPE_IS(unsigned int);
+TEST_TYPE_IS(int);
+TEST_TYPE_IS(unsigned long);
+TEST_TYPE_IS(long);
+TEST_TYPE_IS(unsigned long long);
+TEST_TYPE_IS(long long);
--
GitLab