[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

+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

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'

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
-

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

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

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
-

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

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
-

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

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

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

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

share/machdeps/make_machdep/ssize_t.c

+/**************************************************************************/
+/*                                                                        */
+/*  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)

share/machdeps/make_machdep/weof.c

+#include <wchar.h>
+
+const wint_t weof_is = WEOF;

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"

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 *)
 }
 
 (*

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

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" }

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)

tests/syntax/machdep_char_unsigned.ml

-
 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 () =