Rework C compiler detection

This patch makes karamel pick, by default, 'cc' from the path as the C
compiler. This command can be overriden with the -cc option (taking the
name of a program in the PATH, or a full path to an executable), or the
CC environment variable (idem).

Since karamel passes specific options to different compilers, there is
now logic to detect the flavor of compiler that karamel is talking to
(e.g. by looking at `cc --version`).

The flavor can be overridden with -ccflavor.

There is a special case when the compiler is exactly "msvc" (either via
-cc or CC): this is not taken to be a command nor path, and we instead
use the wrapper script exactly as before.

lib/Driver.ml

@@ -6,34 +6,40 @@
 
 open Warn
 
-(* Abstracting over - (dash) for msvc. vs. gcc-like. *)
+(** These three filled in by [detect_cc] and others *)
+let cc = ref ""
+let cc_args = ref []
+let cc_flavor = ref Options.Generic
+
+(* Abstracting over - (dash) for msvc. vs. gcc-like. This module
+ reads cc_flavor. *)
 module Dash = struct
   let i dir =
-    if !Options.cc = "msvc" then
+    if !cc_flavor = MSVC then
       [ "/I"; dir ]
     else
       [ "-I"; dir ]
 
   let c file =
-    if !Options.cc = "msvc" then
+    if !cc_flavor = MSVC then
       [ "/c"; file ]
     else
       [ "-c"; file ]
 
   let d opt =
-    if !Options.cc = "msvc" then
+    if !cc_flavor = MSVC then
       "/D" ^ opt
     else
       "-D" ^ opt
 
   let o_obj file =
-    if !Options.cc = "msvc" then
+    if !cc_flavor = MSVC then
       [ "/Fo:"; file ]
     else
       [ "-o"; file ]
 
   let o_exe file =
-    if !Options.cc = "msvc" then
+    if !cc_flavor = MSVC then
       [ "/Fe:"; file ]
     else
       [ "-o"; file ]
@@ -44,6 +50,8 @@ module P = Process
 (* Note: don't open [Process], otherwise any reference to [Output] will be
  * understood as a cyclic dependency on our own [Output] module. *)
 
+let cc_flavor_callback = ref (fun (_ : Options.compiler_flavor) -> ())
+
 (** These three variables filled in by [detect_fstar] *)
 let fstar = Options.fstar
 let fstar_lib = ref ""
@@ -57,10 +65,6 @@ let include_dir = ref ""
 let misc_dir = ref ""
 let krml_rev = ref "<unknown>"
 
-(** These two filled in by [detect_gcc] and others *)
-let cc = ref ""
-let cc_args = ref []
-
 (** The base tools *)
 let readlink = ref ""
 
@@ -339,41 +343,46 @@ let run_fstar verify skip_extract skip_translate files =
       exit 0;
     !Options.tmpdir ^^ "out.krml"
 
-let detect_gnu flavor =
-  if not !Options.silent then
-    KPrint.bprintf "%s⚙ KaRaMeL will drive the C compiler.%s Here's what we found:\n" Ansi.blue Ansi.reset;
-  let rec search = function
-    | fmt :: rest ->
-        let cmd = KPrint.bsprintf fmt flavor in
-        if success "which" [| cmd |] then
-          cc := cmd
-        else
-          search rest
-    | [] ->
-        Warn.fatal_error "gcc not found in path!";
+let detect_compiler_flavor cc =
+  let is_gcc () =
+    try
+      (* If cc points to gcc, cc --version will say "cc version ...", instead of
+      gcc. So use -v instead, but that prints to stderr. *)
+      let rc = Process.run cc [| "-v" |] in
+      let lines = rc.stderr in
+      List.exists (fun l -> KString.starts_with l "gcc version") lines
+    with | _ -> false
   in
-  let crosscc = if !Options.m32 then format_of_string "i686-w64-mingw32-%s" else format_of_string "x86_64-w64-mingw32-%s" in
-  search [ "%s-10"; "%s-9"; "%s-8"; "%s-7"; "%s-6"; "%s-5"; crosscc; "%s" ];
-
-  if not !Options.silent then
-    KPrint.bprintf "%sgcc is:%s %s\n" Ansi.underline Ansi.reset !cc;
-
-  if !Options.m32 then
-    cc_args := "-m32" :: !cc_args;
-  if not !Options.silent then
-    KPrint.bprintf "%s%s options are:%s %s\n" Ansi.underline !cc Ansi.reset
-      (String.concat " " !cc_args)
-
-
-let detect_compcert () =
-  if success "which" [| "ccomp" |] then
-    cc := "ccomp"
-  else
-    Warn.fatal_error "ccomp not found in path!"
-
+  let is_clang () =
+    try
+      let lines = Process.read_stdout cc [| "--version" |] in
+      List.exists (fun l -> KString.exists l "clang version") lines
+    with | _ -> false
+  in
+  let is_compcert () =
+    try
+      let lines = Process.read_stdout cc [| "--version" |] in
+      List.exists (fun l -> KString.exists l "CompCert") lines
+    with | _ -> false
+  in
+  let is_msvc () =
+    try
+      let rc = Process.run cc [| |] in
+      let lines = rc.stderr in
+      List.exists (fun l -> KString.exists l "Microsoft") lines
+    with | _ -> false
+  in
+  if is_gcc ()           then Options.GCC
+  else if is_clang ()    then Options.Clang
+  else if is_compcert () then Options.Compcert
+  else if is_msvc ()     then Options.MSVC
+  else (
+    Warn.maybe_fatal_error ("detect_compiler_flavor", UnrecognizedCCompiler cc);
+    Generic
+  )
 
 let fill_cc_args () =
-  (** For the side-effect of filling in [Options.include] *)
+  (** For the side-effect of filling in [Options.includes] *)
   detect_karamel_if ();
 
   cc_args :=
@@ -383,26 +392,83 @@ let fill_cc_args () =
     @ List.rev !Options.ccopts
     @ !cc_args
 
+(* Sets cc, cc_flavor *)
+let auto_detect_cc () =
+  (* !cc can be relative or absolute, `which` handles both. *)
+  if not (success "which" [| !cc |]) then
+    Warn.fatal_error "C compiler '%s' not found!" !cc;
+
+  if not !Options.silent then begin
+    (* If not absolute print realpath too *)
+    let real =
+      if KString.starts_with !cc "/" then
+        ""
+      else
+        match
+          read_one_line !readlink [| "-f"; read_one_line "which" [| !cc |] |]
+        with
+        | exception _ -> " (couldn't resolve?)"
+        | s -> " (= " ^ s ^ ")"
+    in
+    KPrint.bprintf "%scc is:%s %s%s\n" Ansi.underline Ansi.reset !cc real
+  end;
+  match !Options.cc_flavor with
+  | Some f -> cc_flavor := f
+  | None ->   cc_flavor := detect_compiler_flavor !cc
+
+let detect_cc () =
+  detect_base_tools_if ();
+
+  if not !Options.silent then
+    KPrint.bprintf "%s⚙ KaRaMeL will drive the C compiler.%s Here's what we found:\n" Ansi.blue Ansi.reset;
+
+  (* Use Options.cc if passed, otherwise CC from env, otherwise "cc" *)
+  let cc_name =
+    if !Options.cc <> ""
+    then !Options.cc
+    else
+      match Sys.getenv "CC" with
+      | s -> s
+      | exception _ -> "cc"
+  in
+
+  if cc_name = "msvc" then (
+    (* We special-case "msvc" and use this wrapper script to find it
+       and set its environment up, it's not really feasible to
+       just find the cl.exe *)
+    KPrint.bprintf "%scc is:%s MSVC (will use cl-wrapper script)\n" Ansi.underline Ansi.reset;
+    cc := !misc_dir ^^ "cl-wrapper.bat";
+    cc_flavor := MSVC
+  ) else (
+    (* Otherwise cc_name is a normal command or path like gcc/clang,
+       auto-detect its flavor. *)
+    cc := cc_name;
+    auto_detect_cc ()
+  );
+
+  if not !Options.silent then
+    KPrint.bprintf "%scc flavor is:%s %s\n" Ansi.underline Ansi.reset
+      (Options.string_of_compiler_flavor !cc_flavor);
+
+  (* Now that we detected the flavor, call this callback to
+     right default arguments for the compiler filled in. *)
+  !cc_flavor_callback !cc_flavor;
 
-let detect_cc_if () =
   fill_cc_args ();
+
+  if !cc_flavor = GCC && !Options.m32 then
+    cc_args := "-m32" :: !cc_args;
+
+  if not !Options.silent then
+    KPrint.bprintf "%scc options are:%s %s\n" Ansi.underline Ansi.reset
+      (String.concat " " !cc_args)
+
+let detect_cc_if () =
   if !cc = "" then
-    match !Options.cc with
-    | "gcc" ->
-        detect_gnu "gcc"
-    | "compcert" ->
-        detect_compcert ()
-    | "g++" ->
-        detect_gnu "g++"
-    | "clang" ->
-        detect_gnu "clang"
-    | "msvc" ->
-        cc := !misc_dir ^^ "cl-wrapper.bat";
-    | _ ->
-        fatal_error "Unrecognized value for -cc: %s" !Options.cc
+    detect_cc ()
 
 let o_of_c f =
-  let dot_o = if !Options.cc = "msvc" then ".obj" else ".o" in
+  let dot_o = if !cc_flavor = MSVC then ".obj" else ".o" in
   !Options.tmpdir ^^ Filename.chop_suffix (Filename.basename f) ".c" ^ dot_o
 
 

lib/Error.ml

@@ -35,6 +35,7 @@ and raw_error =
   | IfDefOnGlobal of lident
   | NotLowStarCast of expr
   | LibraryPointerAmbiguity of lident * expr
+  | UnrecognizedCCompiler of string
 
 and location =
   string

lib/Options.ml

@@ -3,6 +3,28 @@
 
 type include_ = All | HeaderOnly of string | COnly of string
 
+type compiler_flavor =
+  | Generic
+  | GCC
+  | Clang
+  | Compcert
+  | MSVC
+
+let string_of_compiler_flavor = function
+  | Generic -> "generic"
+  | GCC -> "gcc"
+  | Clang -> "clang"
+  | Compcert -> "compcert"
+  | MSVC -> "msvc"
+
+let compiler_flavor_of_string = function
+  | "generic" -> Generic
+  | "gcc" -> GCC
+  | "clang" -> Clang
+  | "compcert" -> Compcert
+  | "msvc" -> MSVC
+  | s -> failwith ("unrecognized compiler flavor: " ^ s)
+
 let pinc b = function
   | All -> Buffer.add_string b "*"
   | HeaderOnly h -> Buffer.add_string b h; Buffer.add_string b ".h"
@@ -22,13 +44,14 @@ let fstar = ref "fstar.exe" (* F* command to use *)
 let add_include: (include_ * string) list ref = ref [ ]
 let add_include_tmh = ref false
 let add_early_include: (include_ * string) list ref = ref [ ]
-let warn_error = ref "+1@2@3+4..8@9+10@11+12..18@19+20..22+24..25@26@27"
+let warn_error = ref "+1@2@3+4..8@9+10@11+12..18@19+20..22+24..25@26..28"
 let tmpdir = ref "."
 let includes: string list ref = ref []
 let verbose = ref false
 let silent = ref false
 let exe_name = ref ""
-let cc = ref "gcc"
+let cc = ref ""
+let cc_flavor : compiler_flavor option ref = ref None
 let m32 = ref false
 let fsopts: string list ref = ref []
 let ccopts: string list ref = ref []
@@ -91,8 +114,8 @@ let c89_std = ref false
 let c89_scope = ref false
 
 (* A set of extra command-line arguments one gets for free depending on the
- * value of -cc *)
-let default_options () =
+ * detected C compiler. *)
+let default_options (k : compiler_flavor) =
   (* Note: the 14.04 versions of Ubuntu rely on the presence of _BSD_SOURCE to
    * enable the macros in endian.h; future versions use _DEFAULT_SOURCE which is
    * enabled by default, it seems, but there are talks of issuing a warning if
@@ -108,21 +131,20 @@ let default_options () =
   let gcc_options = Array.append gcc_like_options
     [| "-ccopt"; if !c89_std then "-std=c89" else "-std=c11" |]
   in
-  [
-    "gcc", gcc_options;
-    "clang", gcc_options;
-    "g++", gcc_like_options;
-    "compcert", [|
+  match k with
+  | GCC | Clang ->
+    if !cxx_compat
+    then gcc_like_options
+    else gcc_options
+  | Compcert -> [|
       "-warn-error"; "@6@8";
       "-fnostruct-passing"; "-fnoanonymous-unions";
       "-ccopts"; "-g,-D_BSD_SOURCE,-D_DEFAULT_SOURCE";
-    |];
-    "msvc", [|
+    |]
+  | MSVC -> [|
       "-warn-error"; "+6"; "-falloca"
-    |];
-    "", [| |]
-  ]
-
+    |]
+  | Generic -> [| |]
 
 (** Drop is now deprecated and there is not a single situation left that calls
     for it. If you must implement something with macros or static inline (i.e.,

lib/Warn.ml

@@ -45,7 +45,7 @@ let failwith fmt =
 
 (* The main error printing function. *)
 
-let flags = Array.make 28 CError;;
+let flags = Array.make 29 CError;;
 
 (* When adding a new user-configurable error, there are *several* things to
  * update:
@@ -108,6 +108,8 @@ let errno_of_error = function
       26
   | LibraryPointerAmbiguity _ ->
       27
+  | UnrecognizedCCompiler _ ->
+      28
   | _ ->
       (** Things that cannot be silenced! *)
       0
@@ -216,6 +218,8 @@ let rec perr buf (loc, raw_error) =
       -library; and its definition is too ambiguous to tell whether it's an \
       array or a pointer. Disabling this warning is unsound. Definition \
       below:\n%a" plid lid pexpr e
+  | UnrecognizedCCompiler cc ->
+      p "Unrecognized C compiler: %s" cc
 
 let maybe_fatal_error error =
   flush stdout;