From d4fa29ca82b9a12ae5cc33f29b42cb32d5c17ee4 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 5 Apr 2024 17:07:03 +0200
Subject: [PATCH] [machdep] allows censoring macros from machdep's builtins for
.h generation
---
src/kernel_internals/runtime/machdep.ml | 19 +++++++++++++------
src/kernel_internals/runtime/machdep.mli | 19 ++++++++++++++++---
src/kernel_services/ast_queries/file.ml | 23 ++++++++++++++++++++---
3 files changed, 49 insertions(+), 12 deletions(-)
diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml
index 5336176113d..eb162d73b21 100644
--- a/src/kernel_internals/runtime/machdep.ml
+++ b/src/kernel_internals/runtime/machdep.ml
@@ -46,8 +46,15 @@ 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 key_values =
- List.iter (fun (k,v) -> gen_undef fmt k; gen_define_macro fmt k v) key_values
+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
@@ -276,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;
@@ -347,17 +354,17 @@ let gen_all_defines fmt mach =
if mach.compiler = "gcc" then
gen_include fmt "__fc_gcc_builtins.h";
- gen_define_custom_macros fmt 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
diff --git a/src/kernel_internals/runtime/machdep.mli b/src/kernel_internals/runtime/machdep.mli
index 8b4118076ab..90d8718b698 100644
--- a/src/kernel_internals/runtime/machdep.mli
+++ b/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
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 72343997ad8..7e6d6938479 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -502,9 +502,24 @@ let silence_cpp_machdep_warnings cmdl =
else
[]
+let known_bad_macros = [ "SSE" ]
+
+let censored_macros cpp_args =
+ List.fold_left
+ (fun acc arg ->
+ let open Option.Operators in
+ let none = acc in
+ let some = Fun.flip Datatype.String.Set.add acc in
+ (let+ name = Extlib.string_del_prefix "-U" arg in
+ Extlib.strip_underscore name)
+ |> Option.fold ~none ~some)
+ (Datatype.String.Set.of_list known_bad_macros)
+ (List.(flatten (map (String.split_on_char ' ') cpp_args)))
+
let build_cpp_cmd = function
| NoCPP _ | External _ -> None
| NeedCPP (f, cmdl, extra_for_this_file, is_gnu_like) ->
+ let extra_args = extra_for_this_file @ Kernel.CppExtraArgs.get () in
if not (Filepath.exists f) then
Kernel.abort "source file %a does not exist"
Filepath.Normalized.pretty f;
@@ -530,7 +545,10 @@ let build_cpp_cmd = function
let fc_include_args =
if Kernel.FramaCStdLib.get () then
begin
- let machdep_dir = Machdep.generate_machdep_header (get_machdep()) in
+ let censored_macros = censored_macros extra_args in
+ let machdep_dir =
+ Machdep.generate_machdep_header ~censored_macros (get_machdep())
+ in
[(machdep_dir:>string); (Fc_config.framac_libc:>string)]
end
else []
@@ -558,8 +576,7 @@ let build_cpp_cmd = function
in
let supp_args =
string_of_supp_args
- (gnu_implicit_args @ clang_no_warn @
- extra_for_this_file @ (Kernel.CppExtraArgs.get ()))
+ (gnu_implicit_args @ clang_no_warn @ extra_args)
fc_include_args fc_define_args
in
let cpp_command =
--
GitLab