From ed672d7a92b0e45fbb4915d0c26502262d60d9d3 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Fri, 25 Nov 2016 18:31:37 +0100
Subject: [PATCH] [kernel] compatibility between machdep and CPP options
- Extend machdep information to include required CPP arguments (p.ex. -m32);
- Check supported architecture options during configure;
- Automatically apply options according to chosen machdep.
Note: this may generate extra warnings when using old versions of GCC or
compilers that do not support options -m32/-m64 and similar.
---
Makefile.generating | 1 +
configure.in | 33 +++++++++++++++++++++
share/Makefile.config.in | 1 +
src/kernel_internals/runtime/config.ml.in | 2 ++
src/kernel_internals/runtime/config.mli | 7 +++++
src/kernel_internals/runtime/machdeps.ml | 5 ++++
src/kernel_services/ast_data/cil_types.mli | 2 ++
src/kernel_services/ast_queries/file.ml | 29 ++++++++++++++++--
tests/misc/custom_machdep/custom_machdep.ml | 1 +
tests/syntax/machdep_char_unsigned.ml | 1 +
10 files changed, 80 insertions(+), 2 deletions(-)
diff --git a/Makefile.generating b/Makefile.generating
index 4bb84658c1e..063b2a11c93 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -85,6 +85,7 @@ $(CONFIG_FILE): $(CONFIG_FILE).in VERSION share/Makefile.config Makefile.generat
-e "s|@FRAMAC_DEFAULT_CPP@|$(FRAMAC_DEFAULT_CPP)|" \
-e "s|@FRAMAC_GNU_CPP@|$(FRAMAC_GNU_CPP)|" \
-e "s|@DEFAULT_CPP_KEEP_COMMENTS@|$(DEFAULT_CPP_KEEP_COMMENTS)|" \
+ -e "s|@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@|$(DEFAULT_CPP_SUPPORTED_ARCH_OPTS)|" \
-e "s|@STATIC_PLUGINS@|$(STATIC_PLUGINS)|" \
-e "s|@STATIC_GUI_PLUGINS@|$(STATIC_GUI_PLUGINS)|" \
-e "s|@COMPILATION_UNITS@|$(COMPILATION_UNITS)|" \
diff --git a/configure.in b/configure.in
index cbdd6db7736..5b1ec3eca26 100644
--- a/configure.in
+++ b/configure.in
@@ -528,6 +528,38 @@ AC_ARG_WITH(
AC_MSG_RESULT(Default preprocessor is '$FRAMAC_DEFAULT_CPP'.)
+
+# Test if preprocessor supports options such as -m16/-m32/-m64
+
+DEFAULT_CPP_SUPPORTED_ARCH_OPTS=
+
+rm -f conftest.i
+CPPFLAGS="-m32"
+AC_PREPROC_IFELSE(
+ [AC_LANG_SOURCE([/* Check if preprocessor supports option -m32 */])],
+ [if test -e conftest.i; then
+ DEFAULT_CPP_SUPPORTED_ARCH_OPTS+='\"-m32\"; ';
+ fi], [])
+
+rm -f conftest.i
+CPPFLAGS="-m64"
+AC_PREPROC_IFELSE(
+ [AC_LANG_SOURCE([/* Check if preprocessor supports option -m64 */])],
+ [if test -e conftest.i; then
+ DEFAULT_CPP_SUPPORTED_ARCH_OPTS+='\"-m64\"; ';
+ fi], [])
+
+rm -f conftest.i
+CPPFLAGS="-m16"
+AC_PREPROC_IFELSE(
+ [AC_LANG_SOURCE([/* Check if preprocessor supports option -m16 */])],
+ [if test -e conftest.i; then
+ DEFAULT_CPP_SUPPORTED_ARCH_OPTS+='\"-m16\"; ';
+ fi], [])
+
+AC_MSG_RESULT(Default preprocessor supported architecture-related options: $DEFAULT_CPP_SUPPORTED_ARCH_OPTS)
+
+
#################
# Plugin wished #
#################
@@ -954,6 +986,7 @@ AC_SUBST(CYCLES_PER_USEC)
AC_SUBST(LOCAL_MACHDEP)
AC_SUBST(datarootdir)
AC_SUBST(FRAMAC_DEFAULT_CPP)
+AC_SUBST(DEFAULT_CPP_SUPPORTED_ARCH_OPTS)
AC_SUBST(FRAMAC_GNU_CPP)
AC_SUBST(DEFAULT_CPP_KEEP_COMMENTS)
AC_SUBST(CC)
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index e254ddc93d9..0f2a08ce440 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -50,6 +50,7 @@ EMACS_DATADIR ?=$(DATADIR)/emacs/site-lisp
FRAMAC_DEFAULT_CPP ?=@FRAMAC_DEFAULT_CPP@
FRAMAC_GNU_CPP ?=@FRAMAC_GNU_CPP@
DEFAULT_CPP_KEEP_COMMENTS?=@DEFAULT_CPP_KEEP_COMMENTS@
+DEFAULT_CPP_SUPPORTED_ARCH_OPTS?=@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@
CC =@CC@
###############
diff --git a/src/kernel_internals/runtime/config.ml.in b/src/kernel_internals/runtime/config.ml.in
index 9fa1d0a2938..a44de6874d7 100644
--- a/src/kernel_internals/runtime/config.ml.in
+++ b/src/kernel_internals/runtime/config.ml.in
@@ -58,6 +58,8 @@ let preprocessor =
let preprocessor_is_gnu_like =
try ignore (Sys.getenv "CPP"); false with Not_found -> @FRAMAC_GNU_CPP@
+let preprocessor_supported_arch_options = [@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@]
+
let preprocessor_keep_comments =
try (ignore (Sys.getenv "CPP"); true)
with Not_found -> @DEFAULT_CPP_KEEP_COMMENTS@
diff --git a/src/kernel_internals/runtime/config.mli b/src/kernel_internals/runtime/config.mli
index bff595458dc..95a80251b1d 100644
--- a/src/kernel_internals/runtime/config.mli
+++ b/src/kernel_internals/runtime/config.mli
@@ -81,6 +81,13 @@ val preprocessor_is_gnu_like: bool
@since Sodium-20150201
*)
+val preprocessor_supported_arch_options: string list
+ (** architecture-related options (e.g. -m32) known to be supported by
+ the default preprocessor. Used to match preprocessor commands to
+ selected machdeps.
+ @since Frama-C+dev
+ *)
+
val preprocessor_keep_comments: bool
(** [true] if the default preprocessor selected during compilation is
able to keep comments (hence ACSL annotations) in its output.
diff --git a/src/kernel_internals/runtime/machdeps.ml b/src/kernel_internals/runtime/machdeps.ml
index a77f65ef77b..2af52070783 100644
--- a/src/kernel_internals/runtime/machdeps.ml
+++ b/src/kernel_internals/runtime/machdeps.ml
@@ -47,6 +47,7 @@ let x86_16 = {
version =
"x86 16 bits mode (gcc like compiler) with big or huge memory model";
compiler = "generic";
+ cpp_arch_flags = ["-m16"];
sizeof_short = 2;
sizeof_int = 2;
sizeof_long = 4;
@@ -86,6 +87,7 @@ let gcc_x86_16 = { x86_16 with compiler = "gcc" }
let x86_32 = {
version = "gcc 4.0.3 - X86-32bits mode";
compiler = "generic";
+ cpp_arch_flags = ["-m32"];
sizeof_short = 2;
sizeof_int = 4;
sizeof_long = 4;
@@ -123,6 +125,7 @@ let gcc_x86_32 = { x86_32 with compiler = "gcc" }
let x86_64 = {
version = "gcc 4.0.3 AMD64";
compiler = "generic";
+ cpp_arch_flags = ["-m64"];
sizeof_short = 2;
sizeof_int = 4;
sizeof_long = 8;
@@ -160,6 +163,7 @@ let gcc_x86_64 = { x86_64 with compiler = "gcc" }
let ppc_32 = {
version = "4.0.1 (Apple Computer, Inc. build 5367)";
compiler = "standard";
+ cpp_arch_flags = ["-m32"];
sizeof_short = 2;
sizeof_int = 4;
sizeof_long = 4;
@@ -195,6 +199,7 @@ let ppc_32 = {
let msvc_x86_64 = {
version = "MSVC - X86-64bits mode";
compiler = "msvc";
+ cpp_arch_flags = ["-m64"];
sizeof_short = 2;
sizeof_int = 4;
sizeof_long = 4;
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 331057aef90..27c1664773e 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1765,6 +1765,8 @@ type mach = {
__thread_is_keyword: bool (* Whether [__thread] is a keyword *);
compiler: string; (* Compiler being used. Currently recognized names
are 'gcc', 'msvc' and 'generic'. *)
+ cpp_arch_flags: string list; (* Architecture-specific flags to be given to
+ the preprocessor (if supported) *)
version: string; (* Information on this machdep *)
}
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 05adaed0f21..ac7fb7ceca4 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -439,6 +439,25 @@ let parse_cabs = function
else add_if_gnu "-nostdinc"
in
let define_args = "__FRAMAC__" :: define_args in
+ (* Hypothesis: the preprocessor does support the arch-related
+ options tested when 'configure' was run. *)
+ let required_cpp_arch_args = (get_machdep ()).cpp_arch_flags in
+ let supported_cpp_arch_args, unsupported_cpp_arch_args =
+ List.partition (fun arg ->
+ List.mem arg Config.preprocessor_supported_arch_options)
+ required_cpp_arch_args
+ in
+ if unsupported_cpp_arch_args <> [] then
+ Kernel.warning ~once:true
+ "your preprocessor is not known to handle option(s) `%a', \
+ considered necessary for machdep `%s'. To ensure compatibility \
+ between your preprocessor and the machdep, consider using \
+ -cpp-command with the appropriate flags. \
+ Your preprocessor is known to support these flags: %a"
+ (Pretty_utils.pp_list ~sep:" " Format.pp_print_string)
+ unsupported_cpp_arch_args (Kernel.Machdep.get ())
+ (Pretty_utils.pp_list ~sep:" " Format.pp_print_string)
+ Config.preprocessor_supported_arch_options;
let extra_args =
if Kernel.ReadAnnot.get () then
if Kernel.PreprocessAnnot.is_set () then
@@ -459,7 +478,7 @@ let parse_cabs = function
in
let supp_args =
string_of_supp_args include_args define_args
- (extra_args @ Kernel.CppExtraArgs.get ())
+ (extra_args @ Kernel.CppExtraArgs.get () @ supported_cpp_arch_args)
in
if Kernel.is_debug_key_enabled dkey_pp then
Kernel.feedback ~dkey:dkey_pp
@@ -485,8 +504,14 @@ preprocessor command or use the option \"-cpp-command\"." cpp_command
"trying to preprocess annotation with an unknown \
preprocessor."; true))
then begin
+ let pp_annot_supp_args =
+ Format.asprintf "-nostdinc %a"
+ (Pretty_utils.pp_list ~sep:" " Format.pp_print_string)
+ supported_cpp_arch_args
+ in
let ppf' =
- try Logic_preprocess.file ".c" (build_cpp_cmd cmdl "-nostdinc") ppf
+ try Logic_preprocess.file ".c"
+ (build_cpp_cmd cmdl pp_annot_supp_args) ppf
with Sys_error _ as e ->
safe_remove_file ppf;
Kernel.abort "preprocessing of annotations failed (%s)"
diff --git a/tests/misc/custom_machdep/custom_machdep.ml b/tests/misc/custom_machdep/custom_machdep.ml
index 3b50162d8a8..da8ee8cf9ba 100644
--- a/tests/misc/custom_machdep/custom_machdep.ml
+++ b/tests/misc/custom_machdep/custom_machdep.ml
@@ -4,6 +4,7 @@ let mach =
{
version = "foo";
compiler = "bar";
+ cpp_arch_flags = [];
sizeof_short = 2;
sizeof_int = 3;
sizeof_long = 4;
diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml
index e23ac489ab3..494492e8be2 100644
--- a/tests/syntax/machdep_char_unsigned.ml
+++ b/tests/syntax/machdep_char_unsigned.ml
@@ -4,6 +4,7 @@ open Cil_types
let md = {
version = "";
compiler = "gcc";
+ cpp_arch_flags = ["-m32"];
sizeof_short = 2;
sizeof_int = 2;
sizeof_long = 4;
--
GitLab