[machdep] various fixes on machdeps, __fc_machdep.h generation and tests

- fix various typos and inconsistencies
- add an option in make_machdep.py to validate an existing yaml file,
  and use it to validate manually written machdeps
- add macro with the name of the machdep (used in tests/syntax/assembly_gmp.c)
- add option to Frama-C to print the content of __fc_machdep.h on stdout
  and use that to compile our libc with gcc outside of Frama-C
  (as in tests/libc/runtime.c)

share/libc/stdint.h

@@ -147,9 +147,9 @@ typedef __UINTMAX_T uintmax_t;
 /* ISO C: 7.18.2.4 - Done directly with definition of corresponding types. */
 
 /* ISO C: 7.18.2.5 */
-#define INTMAX_MIN __FC_INTMAX_MIN
-#define INTMAX_MAX __FC_INTMAX_MAX
-#define UINTMAX_MAX __FC_UINTMAX_MAX
+#define INTMAX_MIN __INTMAX_MIN
+#define INTMAX_MAX __INTMAX_MAX
+#define UINTMAX_MAX __UINTMAX_MAX
 
 /* ISO C: 7.18.3 */
 

share/libc/sys/socket.h

@@ -25,7 +25,7 @@
 #include "../features.h"
 __PUSH_FC_STDLIB
 __BEGIN_DECLS
-#include "../__fc_machdep.h"
+#include "__fc_machdep.h"
 
 #include "../errno.h"
 

share/libc/sys/types.h

@@ -26,7 +26,7 @@
 __PUSH_FC_STDLIB
 __BEGIN_DECLS
 
-#include "../__fc_machdep.h"
+#include "__fc_machdep.h"
 #include "../__fc_define_id_t.h"
 #include "../__fc_define_pid_t.h"
 #include "../__fc_define_size_t.h"

share/machdeps/Makefile

@@ -19,8 +19,9 @@
 #  for more details (enclosed in the file licenses/LGPLv2.1).            #
 #                                                                        #
 ##########################################################################
+MANUAL_MACHDEPS=machdep_gcc_x86_16.yaml machdep_msvc_x86_64.yaml
 
-update-all: machdep_*.yaml
+update-all: machdep_*.yaml $(MANUAL_MACHDEPS:%=.%.validated)
 
 machdep_avr_16.yaml \
 machdep_gcc_x86_32.yaml \
@@ -35,8 +36,10 @@ machdep_%.yaml: machdep_gcc_%.yaml Makefile
              -e 's/sizeof_void: .*/sizeof_void: -1/' \
              -e 's/alignof_fun: .*/alignof_fun: -1/' \
              -e 's/compiler: .*/compiler: generic/' \
+             -e 's/machdep_name: *machdep_gcc_\([[:alnum:]]*\)/machdep_name: machdep_\1/' \
              $< > $@
 
-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
+.%.validated: % machdep-schema.yaml
+	@echo "Checking $*"
+	@./make_machdep/make_machdep.py --from-file $* --check-only
+	@touch $@

share/machdeps/machdep-schema.yaml

@@ -153,6 +153,14 @@ little_endian:
 
   type: boolean
 
+machdep_name:
+
+  description: |
+    name of the machdep. Will be used to define a macro allowing
+    to know during preprocessing which machdep has been selected.
+
+  type: string
+
 mb_cur_max:
 
   description: expansion of 'MB_CUR_MAX' macro

share/machdeps/machdep_avr_16.yaml

@@ -144,6 +144,7 @@ has__builtin_va_list: true
 intptr_t: int
 l_tmpnam: '20'
 little_endian: true
+machdep_name: machdep_avr_16
 mb_cur_max: ((size_t)16)
 nsig: (64 + 1)
 posix_version: 200809L

share/machdeps/machdep_gcc_x86_16.yaml

@@ -168,3 +168,4 @@ l_tmpnam: '2048'
 tmp_max: '0xFFFFFFFF'
 rand_max: '32767'
 mb_cur_max: '((size_t)16)'
+machdep_name: machdep_gcc_x86_16

share/machdeps/machdep_gcc_x86_32.yaml

@@ -142,6 +142,7 @@ has__builtin_va_list: true
 intptr_t: int
 l_tmpnam: '20'
 little_endian: true
+machdep_name: machdep_gcc_x86_32
 mb_cur_max: ((size_t) 16 )
 nsig: (64 + 1)
 posix_version: 200809L

share/machdeps/machdep_gcc_x86_64.yaml

@@ -142,6 +142,7 @@ has__builtin_va_list: true
 intptr_t: long
 l_tmpnam: '20'
 little_endian: true
+machdep_name: machdep_gcc_x86_64
 mb_cur_max: ((size_t) 16 )
 nsig: (64 + 1)
 posix_version: 200809L

share/machdeps/machdep_msvc_x86_64.yaml

@@ -96,7 +96,7 @@ errno:
 has__builtin_va_list: false
 intptr_t: signed long long
 little_endian: true
-nsig: 23
+nsig: '23'
 ptrdiff_t: long long
 # NB: wasn't defined at all in old __fc_machdep.h
 sig_atomic_t: int
@@ -129,5 +129,6 @@ fopen_max: '16'
 filename_max: '2048'
 l_tmpnam: '20'
 tmp_max: '0xFFFFFFFF'
-rand_max: 32767
+rand_max: '32767'
 mb_cur_max: '((size_t)16)'
+machdep_name: machdep_msvc_x86_64

share/machdeps/machdep_ppc_32.yaml

@@ -144,6 +144,7 @@ has__builtin_va_list: true
 intptr_t: int
 l_tmpnam: '20'
 little_endian: false
+machdep_name: machdep_ppc_32
 mb_cur_max: ((size_t)16)
 nsig: (64 + 1)
 posix_version: 200809L

share/machdeps/machdep_x86_16.yaml

@@ -168,3 +168,4 @@ l_tmpnam: '2048'
 tmp_max: '0xFFFFFFFF'
 rand_max: '32767'
 mb_cur_max: '((size_t)16)'
+machdep_name: machdep_x86_16

share/machdeps/machdep_x86_32.yaml

@@ -142,6 +142,7 @@ has__builtin_va_list: true
 intptr_t: int
 l_tmpnam: '20'
 little_endian: true
+machdep_name: machdep_x86_32
 mb_cur_max: ((size_t) 16 )
 nsig: (64 + 1)
 posix_version: 200809L

share/machdeps/machdep_x86_64.yaml

@@ -142,6 +142,7 @@ has__builtin_va_list: true
 intptr_t: long
 l_tmpnam: '20'
 little_endian: true
+machdep_name: machdep_x86_64
 mb_cur_max: ((size_t) 16 )
 nsig: (64 + 1)
 posix_version: 200809L

share/machdeps/make_machdep/make_machdep.py

@@ -51,7 +51,7 @@ my_path = Path(sys.argv[0]).parent
 
 parser = argparse.ArgumentParser(prog="make_machdep")
 parser.add_argument("-v", "--verbose", action="store_true")
-parser.add_argument("-o", default=sys.stdout, type=argparse.FileType("w"), dest="dest_file")
+parser.add_argument("-o", type=argparse.FileType("w"), dest="dest_file")
 parser.add_argument("--compiler", default="cc", help="which compiler to use; default is 'cc'")
 parser.add_argument(
     "--compiler-version",
@@ -83,33 +83,22 @@ parser.add_argument(
     type=str,
     help="flags to be given to the compiler (other than those set by --cpp-arch-flags); default is '-c'",
 )
-parser.add_argument("--check", action="store_true")
+parser.add_argument(
+    "--check",
+    action="store_true",
+    help="checks that the generated machdep is conforming to the schema"
+)
+parser.add_argument(
+    "--check-only",
+    action="store_true",
+    help="must be used in conjunction with --from-file to check that the provided input file is conforming to the schema"
+)
 
 args, other_args = parser.parse_known_args()
 
 if not args.compiler_flags:
     args.compiler_flags = ["-c"]
 
-
-if args.from_file:
-    orig_file = open(args.from_file, "r")
-    orig_machdep = yaml.safe_load(orig_file)
-    orig_file.close()
-    if not "compiler" in orig_machdep or not "cpp_arch_flags" in orig_machdep:
-        raise Exception("Missing fields in yaml file")
-    args.compiler = orig_machdep["compiler"]
-    if isinstance(orig_machdep["cpp_arch_flags"], list):
-        args.cpp_arch_flags = orig_machdep["cpp_arch_flags"]
-    else:  # old version of the schema used a single string
-        args.cpp_arch_flags = orig_machdep["cpp_arch_flags"].split()
-
-
-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)
-
-
 def make_schema():
     schema_filename = my_path.parent / "machdep-schema.yaml"
     with open(schema_filename, "r") as schema:
@@ -124,13 +113,40 @@ def check_machdep(machdep):
         from jsonschema import validate, ValidationError
 
         validate(machdep, schema)
+        return True
     except ImportError:
         warnings.warn("jsonschema is not available: no validation will be performed")
+        return True
     except OSError:
         warnings.warn(f"error opening {schema_filename}: no validation will be performed")
+        return True
     except ValidationError:
         warnings.warn("machdep object is not conforming to machdep schema")
+        return False
 
+if args.from_file:
+    orig_file = open(args.from_file, "r")
+    orig_machdep = yaml.safe_load(orig_file)
+    orig_file.close()
+    if args.check_only:
+        if check_machdep(orig_machdep):
+            exit(0)
+        else:
+            exit(1)
+    if not "compiler" in orig_machdep or not "cpp_arch_flags" in orig_machdep:
+        raise Exception("Missing fields in yaml file")
+    args.compiler = orig_machdep["compiler"]
+    if isinstance(orig_machdep["cpp_arch_flags"], list):
+        args.cpp_arch_flags = orig_machdep["cpp_arch_flags"]
+    else:  # old version of the schema used a single string
+        args.cpp_arch_flags = orig_machdep["cpp_arch_flags"].split()
+
+def print_machdep(machdep):
+    if args.from_file and args.in_place:
+        args.dest_file = open(args.from_file, "w")
+    elif args.dest_file is None:
+        args.dest_file = sys.stdout
+    yaml.dump(machdep, args.dest_file, indent=4, sort_keys=True)
 
 def make_machdep():
     machdep = {}
@@ -251,7 +267,6 @@ def find_macros_value(output,is_list=False,entry=None):
     if args.verbose:
         print(f"compiler output is:{output}")
 
-
 for (f, typ) in source_files:
     p = my_path / f
     cmd = compilation_command + [str(p)]
@@ -304,6 +319,12 @@ version = version_output.stdout.splitlines()[0]
 machdep["compiler"] = args.compiler
 machdep["cpp_arch_flags"] = args.cpp_arch_flags
 machdep["version"] = version
+if args.from_file and args.in_place:
+    machdep["machdep_name"] = Path(args.from_file).stem
+elif args.dest_file:
+    machdep["machdep_name"] = Path(args.dest_file.name).stem
+else:
+    machdep["machdep_name"] = "anonymous_machdep"
 
 missing_fields = [f for [f, v] in machdep.items() if v is None]
 
@@ -311,7 +332,4 @@ if missing_fields:
     print("WARNING: the following fields are missing from the machdep definition:")
     print(", ".join(missing_fields))
 
-if args.check:
-    check_machdep(machdep)
-
 print_machdep(machdep)

src/kernel_internals/runtime/machdep.ml

@@ -49,6 +49,7 @@ let gen_byte_order fmt mach =
 let no_signedness s =
   let s = Option.value  ~default:s (Extlib.string_del_prefix "signed" s) in
   let s = Option.value  ~default:s (Extlib.string_del_prefix "unsigned" s) in
+  let s = String.trim s in
   if s = "" then "int" else s
 
 let suff_of_kind =
@@ -123,8 +124,10 @@ let std_type_name mach =
     "unsigned", ("UINT", false);
     "unsigned int", ("UINT", false);
     "long", ("LONG", true);
+    "signed long", ("LONG", true);
     "unsigned long", ("ULONG", false);
     "long long", ("LLONG", true);
+    "signed long long", ("LLONG" ,true);
     "unsigned long long", ("ULLONG", false)
   ]
 
@@ -203,6 +206,7 @@ let gen_define_errno_macro fmt (name, v) =
 let gen_all_defines fmt mach =
   Format.fprintf fmt "/* Machdep-specific info for Frama-C's libc */@\n";
   Format.fprintf fmt "#ifndef __FC_MACHDEP@\n#define __FC_MACHDEP@\n";
+  gen_define_int fmt ("__FC_" ^ (String.uppercase_ascii mach.machdep_name)) 1;
   gen_byte_order fmt mach;
   gen_fixed_size_family fmt 8 mach;
   gen_fixed_size_family fmt 16 mach;
@@ -228,7 +232,7 @@ let gen_all_defines fmt 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;
-  gen_intlike_max fmt "__SSIZE_MAX" mach.ssize_t mach;
+  gen_intlike_max fmt "__SSIZE" 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;

src/kernel_internals/runtime/machdep.mli

@@ -22,8 +22,12 @@
 
 (** Managing machine-dependent information. *)
 
-(** generates a [__fc_machdep.h] file in a temp directory and returns the
-    directory name. The generated header contains all [#define] directives
+
+(** Prints on the given formatter all [#define] directives
     required by [share/libc/features.h] and other system-dependent headers.
 *)
+val gen_all_defines: Format.formatter -> Cil_types.mach -> unit
+
+(** generates a [__fc_machdep.h] file in a temp directory and returns the
+    directory name, to be added to the search path for preprocessing stdlib *)
 val generate_machdep_header: Cil_types.mach -> Filepath.Normalized.t

src/kernel_services/ast_data/cil_types.ml

@@ -1916,6 +1916,7 @@ type mach = {
   mb_cur_max: string; (* expansion of MB_CUR_MAX macro *)
   nsig: string; (* expansion of non-standard NSIG macro, empty if undefined *)
   errno: (string * string) list; (* list of macros defining errors in errno.h*)
+  machdep_name: string; (* name of the machdep *)
 }
 
 (*