[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

@@ -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)|" \

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)

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@
 
 ###############

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@

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.

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;

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

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

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;

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;