Merge branch 'issue-1342' into 'master'

machdep: change format of custom_defs in yaml

Closes #1342

See merge request frama-c/frama-c!4460

doc/userman/user-analysis-scripts.tex

@@ -162,7 +162,7 @@ such as when multiple test files define a \texttt{main} function.
 \end{itemize}
 
 \subsection{Using a JSON Compilation Database (JCDB)}
-
+\label{sec:using-json-comp}
 Independently of the chosen workflow, some partial information can be retrieved
 when CMake or Makefile scripts are available for compiling the sources.
 They allow the production of a JSON Compilation Database

doc/userman/user-changes.tex

@@ -5,13 +5,15 @@ release. First we list changes of the last release.
 
 \section*{Frama-C+dev}
 \begin{itemize}
+\item \textbf{Normalizing the Source Code:} document the possibility of
+  undefining builtin macros from the chosen \texttt{-machdep}.
 \item \textbf{Preparing the Sources:} add subsection on standard library about
   portability considerations.
 \end{itemize}
 
 \section*{27.0 (Cobalt)}
 \begin{itemize}
-\item \textbf{Normalizing the Source Code:} new usage of \texttt{-machdep}
+\item \textbf{Normalizing the Source Code:} new usage of \texttt{-machdep}.
 \item \textbf{Normalizing the Source Code:} deprecated option \texttt{-c11}
   (enabled by default).
 \end{itemize}
@@ -26,7 +28,7 @@ release. First we list changes of the last release.
 
 \section*{24.0 (Chromium)}
 \begin{itemize}
-\item \textbf{Standard library (libc):} Section added
+\item \textbf{Standard library (libc):} Section added.
 \end{itemize}
 
 \section*{23.0 (Vanadium)}
@@ -56,7 +58,7 @@ release. First we list changes of the last release.
 \item \textbf{Preparing the Sources:} added option
   \texttt{-cpp-extra-args-per-file}.
 \item \textbf{Customizing Analyzers:} added options
-  \texttt{-warn-invalid-pointer} and \texttt{-warn-pointer-downcast}
+  \texttt{-warn-invalid-pointer} and \texttt{-warn-pointer-downcast}.
 \end{itemize}
 
 \section*{20.0 (Calcium)}
@@ -70,7 +72,7 @@ release. First we list changes of the last release.
 \section*{18.0 (Argon)}
 
 \begin{itemize}
-\item \textbf{Feedback Options:} change options governing status of warning categories
+\item \textbf{Feedback Options:} changed options governing status of warning categories.
 \item \textbf{Normalizing the Source Code:} added category \texttt{@inline} to
 option \texttt{-inline-calls}, and added option \texttt{-remove-inlined}.
 \item \textbf{Customizing Analyzers:} added options
@@ -124,8 +126,8 @@ option \texttt{-inline-calls}, and added option \texttt{-remove-inlined}.
 \section*{Silicon-20161101}
 
 \begin{itemize}
-\item \textbf{Getting Started:} OCaml version greater or equal than 4.05.0 is required
-\item \textbf{Normalizing the Source Code:} New option \texttt{-c11}
+\item \textbf{Getting Started:} OCaml version greater or equal than 4.05.0 is required.
+\item \textbf{Normalizing the Source Code:} New option \texttt{-c11}.
 \end{itemize}
 
 \section*{Aluminium-20160501}
@@ -138,7 +140,7 @@ option \texttt{-inline-calls}, and added option \texttt{-remove-inlined}.
 \item \textbf{Getting Started:} document new option
   \texttt{-<plug-in shortname>-log}.
 \item \textbf{Normalizing the Source Code:} document new options
-  \texttt{-asm-contracts} and\\ \texttt{-asm-contracts-auto-validate}
+  \texttt{-asm-contracts} and\\ \texttt{-asm-contracts-auto-validate}.
 \item \textbf{Graphical User Interface:} Option \texttt{-collect-messages} is
   active by default, and cannot be deactivated.
 \end{itemize}

doc/userman/user-sources.tex

@@ -287,7 +287,14 @@ Apart from these default platforms, it is possible to give as argument
 to \texttt{-machdep} option the path of a YAML file containing the information
 needed by \FramaC. The Plug-in Development Guide~\cite{plugin-dev-guide} describes
 this format in more detail, as well as the use of the \texttt{make\_machdep.py}
-script to automatically generate it.
+script to automatically generate it. The YAML schema contains a list of builtin
+macros with their values. However, any such \texttt{MACRO} can be undefined by passing
+\texttt{-UMACRO} in the preprocessor arguments
+(using \texttt{-cpp-extra-args} or its per-file counterpart as in Sect.~\ref{sec:preprocessing},
+or a compilation database as in Sect.~\ref{sec:using-json-comp}). In addition,
+since compilers tend to define builtin macros with a varying number of
+underscores as prefix and suffix, \texttt{-UMACRO} will also undefine
+\texttt{\_MACRO}, \texttt{\_\_MACRO}, \texttt{\_\_MACRO\_\_}, etc.
 
 \item \optiondef{-}{simplify-cfg} allows \FramaC to remove break, continue and
   switch statements. This option is automatically set by some plug-ins that

nix/kernel-tests.nix

@@ -20,5 +20,6 @@ mk_tests {
       src/plugins/server/tests/batch \
       tests/fc_script \
       tests/syntax
+    make -C share/machdeps check-schema
   '';
 }

nix/mk_tests.nix

@@ -30,6 +30,7 @@
 , clang
 , frama-c
 , perl
+, python3Packages
 , stdenvNoCC
 , time
 , unixtools
@@ -56,6 +57,7 @@ stdenvNoCC.mkDerivation {
     clang
     frama-c
     perl
+    python3Packages.jsonschema
     time
     unixtools.getopt
     yq

share/machdeps/Makefile

@@ -39,10 +39,17 @@ machdep_%.yaml: machdep_gcc_%.yaml Makefile
              -e 's/alignof_fun: .*/alignof_fun: -1/' \
              -e 's/compiler: .*/compiler: generic/' \
              -e 's/machdep_name: *machdep_gcc_\([[:alnum:]]*\)/machdep_name: machdep_\1/' \
-             -e '/ *#undef __GCC.*/d' -e '/ *#define __GCC.*/d' \
+             -e '/ *__GCC.*/d' -e '/ *__GNU/d' -e '/ *__gnu/d' -e '/ *GXX/d' \
              $< > $@
 
 .%.validated: % machdep-schema.yaml
 	@echo "Checking $*"
 	@./make_machdep/make_machdep.py --from-file $* --check-only
 	@touch $@
+
+.PHONY: check-schema
+
+check-schema:
+	@$(foreach machdep, $(wildcard machdep_*.yaml), \
+           ./make_machdep/make_machdep.py --from-file $(machdep) --check-only \
+           || echo "$(machdep) does not conform to machdep schema";)

share/machdeps/machdep-schema.yaml

@@ -98,9 +98,17 @@ cpp_arch_flags:
 
 custom_defs:
   description: |
-    arbitrary text that will be reproduced verbatim in the generated
-    header
-  type: string
+    builtin macros (and their definition) for the given architecture and
+    compiler
+  type: list
+  items:
+    type: object
+    name:
+      description: macro name
+      type: string
+    value:
+      description: actual value
+      type: string
 
 eof:
 

share/machdeps/machdep_msvc_x86_64.yaml

@@ -13,35 +13,72 @@ char_is_unsigned: false
 compiler: msvc
 cpp_arch_flags:
 - -m64
-custom_defs: |
-  #define _MSC_FULL_VER 160040219
-  #define _MSC_VER 1600
-  #undef __ptr64
-  #define __ptr64
-  #undef __ptr32
-  #define __ptr32
-  #undef __unaligned
-  #define __unaligned
-  #undef __cdecl
-  #define __cdecl
-  #undef __possibly_notnullterminated
-  #define __possibly_notnullterminated
-  #ifndef errno_t
-  # define errno_t int
-  # define _ERRNO_T_DEFINED
-  #endif
-  #ifndef _WIN64
-  # define _WIN64 1
-  #endif
-  #ifndef _AMD64_
-  # define _AMD64_ 1
-  #endif
-  #ifndef _M_AMD64
-  # define _M_AMD64 1
-  #endif
-  #ifndef _M_X64
-  # define _M_X64 1
-  #endif
+has__builtin_va_list: false
+int_fast8_t: signed char
+int_fast16_t: signed int
+int_fast32_t: signed int
+int_fast64_t: signed long long
+intptr_t: signed long long
+little_endian: true
+nsig: '23'
+ptrdiff_t: long long
+# NB: wasn't defined at all in old __fc_machdep.h
+sig_atomic_t: int
+size_t: unsigned long long
+sizeof_double: 8
+sizeof_float: 4
+sizeof_fun: -1
+sizeof_int: 4
+sizeof_long: 4
+sizeof_longdouble: 8
+sizeof_longlong: 8
+sizeof_ptr: 8
+sizeof_short: 2
+sizeof_void: 0
+ssize_t: long long
+time_t: long long
+uint_fast8_t: unsigned char
+uint_fast16_t: unsigned int
+uint_fast32_t: unsigned int
+uint_fast64_t: unsigned long long
+uintptr_t: unsigned long long
+version: MSVC - X86-64bits mode
+wchar_t: unsigned short
+weof: (0xffffU)
+wint_t: unsigned short
+wordsize: '64'
+posix_version: ''
+
+# NB: except for l_tmpnam, the following macros are not defined in the old
+# __fc_machdep.h in the MSVC_X86_64 section. The values below have thus been 
+# taken from gnu
+bufsiz: '8192'
+eof: '(-1)'
+fopen_max: '20'
+host_name_max: '255'
+path_max: '256'
+tty_name_max: '32'
+filename_max: '2048'
+l_tmpnam: '20'
+tmp_max: '0xFFFFFFFF'
+rand_max: '32767'
+mb_cur_max: '((size_t)16)'
+machdep_name: machdep_msvc_x86_64
+
+custom_defs:
+    _MSC_FULL_VER: '160040219'
+    _MSC_VER: '1600'
+    __ptr64: ''
+    __ptr32: ''
+    __unaligned: ''
+    __cdecl: ''
+    __possibly_notnullterminated: ''
+    errno_t: int
+    _ERRNO_T_DEFINED: ''
+    _WIN64: '1'
+    _AMD64_: '1'
+    _M_AMD64: '1'
+    _M_X64: '1'
 
 errno:
     eperm: '1'
@@ -123,53 +160,3 @@ errno:
     ecanceled: '105'
     eownerdead: '133'
     enotrecoverable: '127'
-has__builtin_va_list: false
-int_fast8_t: signed char
-int_fast16_t: signed int
-int_fast32_t: signed int
-int_fast64_t: signed long long
-intptr_t: signed long long
-little_endian: true
-nsig: '23'
-ptrdiff_t: long long
-# NB: wasn't defined at all in old __fc_machdep.h
-sig_atomic_t: int
-size_t: unsigned long long
-sizeof_double: 8
-sizeof_float: 4
-sizeof_fun: -1
-sizeof_int: 4
-sizeof_long: 4
-sizeof_longdouble: 8
-sizeof_longlong: 8
-sizeof_ptr: 8
-sizeof_short: 2
-sizeof_void: 0
-ssize_t: long long
-time_t: long long
-uint_fast8_t: unsigned char
-uint_fast16_t: unsigned int
-uint_fast32_t: unsigned int
-uint_fast64_t: unsigned long long
-uintptr_t: unsigned long long
-version: MSVC - X86-64bits mode
-wchar_t: unsigned short
-weof: (0xffffU)
-wint_t: unsigned short
-wordsize: '64'
-posix_version: ''
-# NB: except for l_tmpnam, the corresponding macro are not defined in the old
-# __fc_machdep.h in the MSVC_X86_64 section. The values below have thus been 
-# taken from gnu
-bufsiz: '8192'
-eof: '(-1)'
-fopen_max: '20'
-host_name_max: '255'
-path_max: '256'
-tty_name_max: '32'
-filename_max: '2048'
-l_tmpnam: '20'
-tmp_max: '0xFFFFFFFF'
-rand_max: '32767'
-mb_cur_max: '((size_t)16)'
-machdep_name: machdep_msvc_x86_64

share/machdeps/make_machdep/make_machdep.py

@@ -45,7 +45,6 @@ import subprocess
 import sys
 import logging
 import yaml
-from yaml.representer import Representer
 
 my_path = Path(sys.argv[0]).parent
 
@@ -159,7 +158,7 @@ def print_machdep(machdep):
         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)
+    yaml.dump(machdep, args.dest_file, indent=4, sort_keys=False)
 
 
 def default_value(typ):
@@ -377,50 +376,32 @@ machdep["compiler"] = args.compiler
 machdep["cpp_arch_flags"] = args.cpp_arch_flags
 machdep["version"] = version
 
-machdep["custom_defs"] = ""
+machdep["custom_defs"] = list()
 
 # Extract predefined macros; we're assuming a gcc-like compiler here.
 # Leave custom_defs empty if this fails.
 
-# in case we have all the predefined macros, custom_defs will be very long.
-# we thus want to output it as a literal block, not a simple string.
-# For that, use a custom object and tell PyYaml to output it in a particular way
-# Based on SO's answer:
-
-
-class custom_defs(str):
-    pass
-
-
-def change_style(style, representer):
-    def new_representer(dumper, data):
-        scalar = representer(dumper, data)
-        scalar.style = style
-        return scalar
-
-    return new_representer
-
-
-custom_defs_representer = change_style("|", Representer.represent_str)
-
-yaml.add_representer(custom_defs, custom_defs_representer)
-
 cmd = compilation_command + ["-dM", "-E", "-"]
 if args.verbose:
     print(f"[INFO] running command: {' '.join(cmd)}")
 proc = subprocess.run(cmd, stdin=subprocess.DEVNULL, capture_output=True, text=True)
 if proc.returncode == 0:
-    lines = ""
+    custom = dict()
     for line in proc.stdout.splitlines():
         # Preprocessor emits a warning if we're trying to #undef
         # standard macros. Leave them alone.
         if re.match(r"#define *__STDC", line):
             continue
-        macro = re.match(r"#define *(\w+)", line)
-        if macro:
-            lines += f"#undef {macro.group(1)}\n"
-        lines += f"{line.strip()}\n"
-    machdep["custom_defs"] = custom_defs(lines)
+        macro = re.match(r"# *define *([^ ]*) *(.*)", line)
+        if not macro:
+            # This skips over ifndef/endif blocs for msvc, maybe this
+            # will be a problem later.
+            continue
+        macro_var = macro.group(1)
+        macro_val = macro.group(2)
+        # Python >= 3.7: dict is guaranteed to preserve insertion order
+        custom[macro_var] = macro_val
+    machdep["custom_defs"] = custom
 else:
     logging.warning(f"could not determine predefined macros. compiler output is:\n{proc.stderr}")
 

src/kernel_internals/runtime/machdep.ml

@@ -28,7 +28,13 @@ let gen_define fmt macro pp def =
 let gen_include fmt file =
   Format.fprintf fmt "#include <%s>@\n" file
 
-let gen_undef fmt macro = Format.fprintf fmt "#undef %s@\n" macro
+let gen_undef fmt macro =
+  let macro =
+    match String.index_from_opt macro 0 '(' with
+    | None -> macro
+    | Some n -> String.sub macro 0 n
+  in
+  Format.fprintf fmt "#undef %s@\n" macro
 
 let gen_define_string fmt macro def =
   gen_define fmt macro Format.pp_print_string def
@@ -40,6 +46,16 @@ let gen_define_macro fmt macro def =
   if def = "" then gen_undef fmt macro
   else gen_define_string fmt macro def
 
+let gen_define_custom_macros fmt censored key_values =
+  List.iter
+    (fun (k,v) ->
+       if not (Datatype.String.Set.mem (Extlib.strip_underscore k) censored)
+       then begin
+         gen_undef fmt k;
+         gen_define_macro fmt k v
+       end)
+    key_values
+
 let gen_define_int fmt macro def = gen_define fmt macro Format.pp_print_int def
 
 let gen_byte_order fmt mach =
@@ -267,7 +283,7 @@ let machdep_macro_name s =
   in
   String.map tr s
 
-let gen_all_defines fmt mach =
+let gen_all_defines fmt ?(censored_macros=Datatype.String.Set.empty) 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_" ^ (machdep_macro_name mach.machdep_name)) 1;
@@ -338,17 +354,17 @@ let gen_all_defines fmt mach =
   if mach.compiler = "gcc" then
     gen_include fmt "__fc_gcc_builtins.h";
 
-  Format.fprintf fmt "%s@\n" mach.custom_defs;
+  gen_define_custom_macros fmt censored_macros mach.custom_defs;
 
   Format.fprintf fmt "#endif // __FC_MACHDEP@\n"
 
-let generate_machdep_header mach =
+let generate_machdep_header ?censored_macros mach =
   let debug = Kernel.(is_debug_key_enabled dkey_pp) in
   let temp = Extlib.temp_dir_cleanup_at_exit ~debug "__fc_machdep" in
   let file = Filepath.Normalized.concat temp "__fc_machdep.h" in
   let chan = open_out (file:>string) in
   let fmt = Format.formatter_of_out_channel chan in
-  gen_all_defines fmt mach;
+  gen_all_defines fmt ?censored_macros mach;
   flush chan;
   close_out chan;
   temp

src/kernel_internals/runtime/machdep.mli

@@ -25,9 +25,22 @@
 
 (** Prints on the given formatter all [#define] directives
     required by [share/libc/features.h] and other system-dependent headers.
+    @param censored_macros prevents the generation of directives for the
+    builtin macros in [mach.custom_defs] whose names match. empty by default.
+    @before Frama-C+dev censored_macros did not exist
 *)
-val gen_all_defines: Format.formatter -> Cil_types.mach -> unit
+val gen_all_defines:
+  Format.formatter ->
+  ?censored_macros:Datatype.String.Set.t ->
+  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
+    directory name, to be added to the search path for preprocessing stdlib.
+    @param see {!gen_all_defines}
+    @before Frama-C+dev censored_macros did not exist.
+*)
+val generate_machdep_header:
+  ?censored_macros:Datatype.String.Set.t ->
+  Cil_types.mach ->
+  Filepath.Normalized.t