aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativelib.ml
blob: e9c0e171acf7a9131bd5a6033486fa4cf4ab5787 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)
open Util
open Nativevalues
open Nativecode
open CErrors
open Envars

(** This file provides facilities to access OCaml compiler and dynamic linker,
used by the native compiler. *)

let get_load_paths =
  ref (fun _ -> anomaly (Pp.str "get_load_paths not initialized.") : unit -> string list)

let open_header = ["Nativevalues";
                   "Nativecode";
                   "Nativelib";
		   "Nativeconv";
                   "Declaremods"]
let open_header = List.map mk_open open_header

(* Directory where compiled files are stored *)
let output_dir = ".coq-native"

(* Extension of genereted ml files, stored for debugging purposes *)
let source_ext = ".native"

let ( / ) = Filename.concat

(* We have to delay evaluation of include_dirs because coqlib cannot be guessed
until flags have been properly initialized *)
let include_dirs () =
  [Filename.get_temp_dir_name (); coqlib () / "kernel"; coqlib () / "library"]

(* Pointer to the function linking an ML object into coq's toplevel *)
let load_obj = ref (fun x -> () : string -> unit)

let rt1 = ref (dummy_value ())
let rt2 = ref (dummy_value ())

let get_ml_filename () =
  let filename = Filename.temp_file "Coq_native" source_ext in
  let prefix = Filename.chop_extension (Filename.basename filename) ^ "." in
  filename, prefix

let write_ml_code fn ?(header=[]) code =
  let header = open_header@header in
  let ch_out = open_out fn in
  let fmt = Format.formatter_of_out_channel ch_out in
  List.iter (pp_global fmt) (header@code);
  close_out ch_out

let warn_native_compiler_failed =
  let print = function
  | Inl (Unix.WEXITED n) -> Pp.(strbrk "Native compiler exited with status" ++ str" " ++ int n)
  | Inl (Unix.WSIGNALED n) -> Pp.(strbrk "Native compiler killed by signal" ++ str" " ++ int n)
  | Inl (Unix.WSTOPPED n) -> Pp.(strbrk "Native compiler stopped by signal" ++ str" " ++ int n)
  | Inr e -> Pp.(strbrk "Native compiler failed with error: " ++ strbrk (Unix.error_message e))
  in
  CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print

let call_compiler ?profile:(profile=false) ml_filename =
  let load_path = !get_load_paths () in
  let load_path = List.map (fun dn -> dn / output_dir) load_path in
  let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (include_dirs () @ load_path)) in
  let f = Filename.chop_extension ml_filename in
  let link_filename = f ^ ".cmo" in
  let link_filename = Dynlink.adapt_filename link_filename in
  let remove f = if Sys.file_exists f then Sys.remove f in
  remove link_filename;
  remove (f ^ ".cmi");
  let initial_args =
    if Dynlink.is_native then
      ["opt"; "-shared"]
     else
      ["ocamlc"; "-c"]
  in
  let profile_args =
    if profile then
      ["-g"]
    else
      []
  in
  let flambda_args =
    if Coq_config.caml_version_nums >= [4;3;0] then
      (* We play safe for now, and use the native compiler
         with -Oclassic, however it is likely that `native_compute`
         users can benefit from tweaking here.
      *)
      ["-Oclassic"]
    else
      []
  in
  let args =
    initial_args @
      profile_args @
        flambda_args @
      ("-o"::link_filename
       ::"-rectypes"
       ::"-w"::"a"
       ::include_dirs) @
      ["-impl"; ml_filename] in
  if !Flags.debug then Feedback.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args)));
  try
    let res = CUnix.sys_command (ocamlfind ()) args in
    let res = match res with
      | Unix.WEXITED 0 -> true
      | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n ->
        warn_native_compiler_failed (Inl res); false
    in
    res, link_filename
  with Unix.Unix_error (e,_,_) ->
    warn_native_compiler_failed (Inr e);
    false, link_filename

let compile fn code ~profile:profile =
  write_ml_code fn code;
  let r = call_compiler ~profile fn in
  if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn;
  r

let compile_library dir code fn =
  let header = mk_library_header dir in
  let fn = fn ^ source_ext in
  let basename = Filename.basename fn in
  let dirname = Filename.dirname fn in
  let dirname = dirname / output_dir in
  let () =
    try Unix.mkdir dirname 0o755
    with Unix.Unix_error (Unix.EEXIST, _, _) -> ()
  in
  let fn = dirname / basename in
  write_ml_code fn ~header code;
  let r = fst (call_compiler fn) in
  if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn;
  r

(* call_linker links dynamically the code for constants in environment or a  *)
(* conversion test. *)
let call_linker ?(fatal=true) prefix f upds =
  rt1 := dummy_value ();
  rt2 := dummy_value ();
  if not (Sys.file_exists f) then
    begin
      let msg = "Cannot find native compiler file " ^ f in
      if fatal then CErrors.user_err Pp.(str msg)
      else if !Flags.debug then Feedback.msg_debug (Pp.str msg)
    end
  else
  (try
    if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
    register_native_file prefix
   with Dynlink.Error e as exn ->
     let exn = CErrors.push exn in
     let msg = "Dynlink error, " ^ Dynlink.error_message e in
     if fatal then (Feedback.msg_error (Pp.str msg); iraise exn)
     else if !Flags.debug then Feedback.msg_debug (Pp.str msg));
  match upds with Some upds -> update_locations upds | _ -> ()

let link_library ~prefix ~dirname ~basename =
  let f = dirname / output_dir / basename in
  call_linker ~fatal:false prefix f None