(**************************************************************************) (* *) (* This file is part of Frama-C. *) (* *) (* Copyright (C) 2007-2025 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) (* you can redistribute it and/or modify it under the terms of the GNU *) (* Lesser General Public License as published by the Free Software *) (* Foundation, version 2.1. *) (* *) (* It is distributed in the hope that it will be useful, *) (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) (* GNU Lesser General Public License for more details. *) (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) (* *) (**************************************************************************) module C = Configurator.V1 module Temp = struct (* Almost copied from configurator *) let (^/) a b = a ^ "/" ^ b let rec rm_rf dir = Array.iter (fun fn -> let fn = dir ^/ fn in if Sys.is_directory fn then rm_rf fn else Unix.unlink fn) (Sys.readdir dir); Unix.rmdir dir let prng = lazy (Random.State.make_self_init ()) let gen_name ~dir ~prefix ~suffix = let rnd = Random.State.bits (Lazy.force prng) land 0xFFFFFF in dir ^/ Printf.sprintf "%s%06x%s" prefix rnd suffix let create_dir () = let dir = gen_name ~dir:(Filename.get_temp_dir_name ()) ~prefix:"" ~suffix:"" in Unix.mkdir dir 0o700 ; at_exit (fun () -> rm_rf dir) ; dir let create ?(dir=create_dir ()) ?(prefix="") ?(suffix="") mk = let rec try_name counter = let name = gen_name ~dir ~prefix ~suffix in match mk name with | () -> name | exception Unix.Unix_error _ when counter < 1000 -> try_name (counter + 1) in try_name 0 end module C_preprocessor = struct (* This could be put in Dune? *) type t = { preprocessor: string ; pp_opt: string option } let stdout_contains out str = let re = Str.regexp_string str in try ignore (Str.search_forward re out 0); true with Not_found -> false let find_preprocessor configurator = let cc_env = try Sys.getenv "CPP" with Not_found -> "" in if cc_env <> "" then (cc_env, None) (* assume default CPP needs no args *) else let finder (command, _pp_opt) = C.which configurator command |> Option.is_some in (* Note: We could add 'cl.exe' to the list, but since it requires '/<opt>' and not '-<opt>' for its options, it will fail in every check anyway. So the user may manually specify it if they want it, but having it here brings no benefit. Note: 'cpp' is NOT the POSIX way to call the preprocessor, and it behaves VERY badly on macOS (as if using '-traditional', see https://stackoverflow.com/questions/9508159). Therefore, we try `gcc -E` and `cc -E`, but not 'cpp'. *) try List.find finder [("gcc", Some "-E"); ("cc", Some "-E")] with Not_found -> C.die "Could not find a C preprocessor" let write_file name code = let out = open_out name in Printf.fprintf out "%s" code ; close_out out let call configurator preprocessor options code = let dir = Temp.create_dir () in let file = Temp.create ~dir ~suffix:".c" (fun name -> write_file name code) in C.Process.run configurator ~dir preprocessor (options @ [ file ]) let get configurator = let preprocessor, pp_opt = find_preprocessor configurator in { preprocessor ; pp_opt } let preprocess configurator t options code = call configurator t.preprocessor (Option.to_list t.pp_opt @ options) code end (* Frama-C specific part *) module Cpp = struct module GnuLike = struct let code = {| #define foo 0 /* foo */ int main(){} |} let check configurator preprocessor = let options = ["-dD" ; "-nostdinc"] in (C_preprocessor.preprocess configurator preprocessor options code).exit_code = 0 end module KeepComments = struct let code = {|/* Check whether comments are kept in output */|} let keep_comments_option = "-C" let check configurator preprocessor = let result = C_preprocessor.preprocess configurator preprocessor [keep_comments_option] code in result.exit_code = 0 && C_preprocessor.stdout_contains result.stdout "kept" end module Archs = struct let opt_m_code value = Format.asprintf {|/* Check if preprocessor supports option -m%s */|} value let check configurator preprocessor arch = let code = opt_m_code arch in let options = [ Format.asprintf "-m%s" arch ] in if (C_preprocessor.preprocess configurator preprocessor options code).exit_code = 0 then Some arch else None let supported_archs configurator preprocessor archs = let check = check configurator preprocessor in List.map (fun s -> "-m" ^ s) @@ List.filter_map check archs end type t = { preprocessor : C_preprocessor.t ; default_args : string list ; is_gnu_like : bool ; keep_comments : bool ; supported_archs_opts : string list } let get configurator = let preprocessor = C_preprocessor.get configurator in let default_args = Option.to_list preprocessor.pp_opt @ [ "-C" ; "-I." ] in let is_gnu_like = GnuLike.check configurator preprocessor in let keep_comments = KeepComments.check configurator preprocessor in let supported_archs_opts = Archs.supported_archs configurator preprocessor [ "16" ; "32" ; "64" ] in { preprocessor; default_args; is_gnu_like; keep_comments; supported_archs_opts } let pp_flags fmt = let pp_sep fmt () = Format.fprintf fmt " " in Format.pp_print_list ~pp_sep Format.pp_print_string fmt let pp_default_cpp fmt cpp = Format.fprintf fmt "%s %a" cpp.preprocessor.preprocessor pp_flags cpp.default_args let pp_archs fmt cpp = let pp_arch fmt arch = Format.fprintf fmt "\"%s\"" arch in let pp_sep fmt () = Format.fprintf fmt "; " in Format.fprintf fmt "%a" (Format.pp_print_list ~pp_sep pp_arch) cpp.supported_archs_opts let add_macros tbl cpp = Hashtbl.replace tbl "@FRAMAC_DEFAULT_CPP@" (Format.asprintf "%a" pp_default_cpp cpp); Hashtbl.replace tbl "@FRAMAC_DEFAULT_CPP_ARGS@" (Format.asprintf "%a" pp_flags cpp.default_args); Hashtbl.replace tbl "@FRAMAC_GNU_CPP@" (string_of_bool cpp.is_gnu_like); Hashtbl.replace tbl "@DEFAULT_CPP_KEEP_COMMENTS@" (string_of_bool cpp.keep_comments); Hashtbl.replace tbl "@DEFAULT_CPP_KEEP_COMMENTS@" (string_of_bool cpp.keep_comments); Hashtbl.replace tbl "@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@" (Format.asprintf "%a" pp_archs cpp); end module Fc_version = struct type t = { major: string ; minor: string ; ext: string ; name: string } let head1 file = (* output first line from file, without '\n' *) try let ic = open_in file in let s = input_line ic in close_in ic; s with _exc -> C.die "Can't read %s." file let get () = let out_VERSION = head1 "VERSION" in let re_version = Str.regexp {|\([1-9][0-9]\)\.\([0-9]\)\(.*\)|} in let major, minor, ext = if Str.string_match re_version out_VERSION 0 then Str.matched_group 1 out_VERSION, Str.matched_group 2 out_VERSION, try Str.matched_group 3 out_VERSION with Not_found -> "" else C.die "Invalid VERSION contents." in let name = head1 "VERSION_CODENAME" in { major; minor; ext; name } let add_macros tbl version = Hashtbl.replace tbl "@VERSION@" (Format.asprintf "%s.%s%s" version.major version.minor version.ext); Hashtbl.replace tbl "@VERSION_CODENAME@" version.name; Hashtbl.replace tbl "@MAJOR_VERSION@" version.major; Hashtbl.replace tbl "@MINOR_VERSION@" version.minor end module OS = struct type t = Windows | MacOS | OtherUnix let get configurator = match C.ocaml_config_var_exn configurator "os_type" with | "Win32" -> Windows | _ -> match C.ocaml_config_var_exn configurator "system" with | "macosx" -> MacOS | _ -> OtherUnix let add_macros tbl t = let module_dirs = match t with | Windows -> "Win_dirs" | MacOS -> "Macos_dirs" | OtherUnix -> "Unix_dirs" in Hashtbl.replace tbl "@FRAMAC_TARGET_SYSTEM_CONFIG_INCLUDE@" module_dirs end let python_available configurator = let result = C.Process.run configurator "python3" ["--version"] in if result.exit_code <> 0 then false else let out = result.stdout in let re_version = Str.regexp {|.* \([0-9]\)\.\([0-9]+\).[0-9]+|} in try let maj, med = if Str.string_match re_version out 0 then int_of_string @@ Str.matched_group 1 out, int_of_string @@ Str.matched_group 2 out else raise Not_found in if maj <> 3 || med < 7 then raise Not_found ; true with Not_found | Failure _ -> false let re_macro = Str.regexp "@[A-Za-z0-9_]+@" let expand macros line = let line = ref line in try while true do ignore (Str.search_forward re_macro !line 0); let key = Str.matched_string !line in match Hashtbl.find_opt macros key with | None -> C.die "Unknown macro: %s" key | Some v -> line := Str.global_replace (Str.regexp_string key) v !line done; assert false with Not_found -> !line let configure configurator = let version = Fc_version.get () in let cpp = Cpp.get configurator in let os = OS.get configurator in let macros = Hashtbl.create 10 in Fc_version.add_macros macros version; Cpp.add_macros macros cpp; OS.add_macros macros os; let ic = open_in "src/kernel_internals/runtime/system_config.ml.in" in let oc = open_out "system_config.ml" in try while true; do let line = expand macros (input_line ic) in output_string oc line; output_char oc '\n'; done; with End_of_file -> close_in ic; close_out oc; let python = open_out "python-3.7-available" in Printf.fprintf python "%b" (python_available configurator); close_out python let () = C.main ~name:"frama_c_config" configure