Driver.ml 15.9 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

13
open Printf
14
open Commandline
15
open Clflags
16
open CommonOptions
17
open Timing
18
19
open Driveraux
open Frontend
20
21
open Assembler
open Linker
22
open Diagnostics
23

24
25
26
(* Name used for version string etc. *)
let tool_name = "C verified compiler"

27
28
(* Optional sdump suffix *)
let sdump_suffix = ref ".json"
29

30
31
32
33
34
35
let nolink () =
  !option_c || !option_S || !option_E || !option_interp

let object_filename sourcename suff =
  if nolink () then
    output_filename ~final: !option_c sourcename suff ".o"
36
37
  else
    tmp_file ".o"
38

39
40
(* From CompCert C AST to asm *)

41
let compile_c_file sourcename ifile ofile =
42
  (* Prepare to dump Clight, RTL, etc, if requested *)
xleroy's avatar
xleroy committed
43
  let set_dest dst opt ext =
44
    dst := if !opt then Some (output_filename sourcename ".c" ext)
45
46
47
      else None in
  set_dest Cprint.destination option_dparse ".parsed.c";
  set_dest PrintCsyntax.destination option_dcmedium ".compcert.c";
xleroy's avatar
xleroy committed
48
49
  set_dest PrintClight.destination option_dclight ".light.c";
  set_dest PrintCminor.destination option_dcminor ".cm";
50
  set_dest PrintRTL.destination option_drtl ".rtl";
51
  set_dest Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
52
  set_dest PrintLTL.destination option_dltl ".ltl";
53
  set_dest PrintMach.destination option_dmach ".mach";
54
  set_dest AsmToJSON.destination option_sdump !sdump_suffix;
55
56
  (* Parse the ast *)
  let csyntax = parse_c_file sourcename ifile in
57
  (* Convert to Asm *)
58
  let asm =
59
60
61
    match Compiler.apply_partial
               (Compiler.transf_c_program csyntax)
               Asmexpand.expand_program with
62
    | Errors.OK asm ->
63
        asm
64
    | Errors.Error msg ->
65
66
      let loc = file_loc sourcename in
        fatal_error loc "%a"  print_error msg in
67
  (* Dump Asm in binary and JSON format *)
68
  AsmToJSON.print_if asm sourcename;
69
  (* Print Asm in text form *)
70
  let oc = open_out ofile in
Bernhard Schommer's avatar
Bernhard Schommer committed
71
  PrintAsm.print_program oc asm;
72
73
  close_out oc

74
75
(* From C source to asm *)

76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
let compile_i_file sourcename preproname =
  if !option_interp then begin
    Machine.config := Machine.compcert_interpreter !Machine.config;
    let csyntax = parse_c_file sourcename preproname in
    Interp.execute csyntax;
        ""
  end else if !option_S then begin
    compile_c_file sourcename preproname
      (output_filename ~final:true sourcename ".c" ".s");
    ""
  end else begin
    let asmname =
      if !option_dasm
      then output_filename sourcename ".c" ".s"
      else tmp_file ".s" in
    compile_c_file sourcename preproname asmname;
    let objname = object_filename sourcename ".c" in
    assemble asmname objname;
    objname
  end
96
97
98
99

(* Processing of a .c file *)

let process_c_file sourcename =
100
  ensure_inputfile_exists sourcename;
101
  if !option_E then begin
102
103
    preprocess sourcename (output_filename_default "-");
    ""
104
  end else begin
105
    let preproname = if !option_dprepro then
106
107
      output_filename sourcename ".c" ".i"
    else
108
      tmp_file ".i" in
109
    preprocess sourcename preproname;
110
    compile_i_file sourcename preproname
111
  end
112

113
114
115
(* Processing of a .i / .p file (preprocessed C) *)

let process_i_file sourcename =
116
  ensure_inputfile_exists sourcename;
117
  compile_i_file sourcename sourcename
118
119
120
121

(* Processing of .S and .s files *)

let process_s_file sourcename =
122
  ensure_inputfile_exists sourcename;
123
  let objname = object_filename sourcename ".s" in
124
125
  assemble sourcename objname;
  objname
126
127

let process_S_file sourcename =
128
  ensure_inputfile_exists sourcename;
129
  if !option_E then begin
130
131
    preprocess sourcename (output_filename_default "-");
    ""
132
  end else begin
133
    let preproname = tmp_file ".s" in
134
    preprocess sourcename preproname;
135
    let objname = object_filename sourcename ".S" in
136
137
138
    assemble preproname objname;
    objname
  end
139

140
141
142
143
(* Processing of .h files *)

let process_h_file sourcename =
  if !option_E then begin
144
    ensure_inputfile_exists sourcename;
145
146
    preprocess sourcename (output_filename_default "-");
    ""
147
148
  end else
    fatal_error no_loc "input file %s ignored (not in -E mode)\n" sourcename
149

150
151
let target_help =
  if Configuration.arch = "arm" && Configuration.model <> "armv6" then
Bernhard Schommer's avatar
Bernhard Schommer committed
152
153
154
155
{|Target processor options:
  -mthumb        Use Thumb2 instruction encoding
  -marm          Use classic ARM instruction encoding
|}
156
157
158
else
  ""

159
160
161
162
163
164
165
let toolchain_help =
  if not Configuration.gnu_toolchain then begin
{|Toolchain options:
  -t tof:env     Select target processor for the diab toolchain
|} end else
    ""

166
let usage_string =
167
  version_string tool_name ^
Bernhard Schommer's avatar
Bernhard Schommer committed
168
169
170
171
172
  {|Usage: ccomp [options] <source files>
Recognized source files:
  .c             C source file
  .i or .p       C source file that should not be preprocessed
  .s             Assembly file
Bernhard Schommer's avatar
Bernhard Schommer committed
173
  .S or .sx      Assembly file that must be preprocessed
Bernhard Schommer's avatar
Bernhard Schommer committed
174
175
176
177
178
179
180
181
  .o             Object file
  .a             Library file
Processing options:
  -c             Compile to object file only (no linking), result in <file>.o
  -E             Preprocess only, send result to standard output
  -S             Compile to assembler only, save result in <file>.s
  -o <file>      Generate output in <file>
|} ^
182
  prepro_help ^
183
  language_support_help ^
184
 DebugInit.debugging_help ^
Bernhard Schommer's avatar
Bernhard Schommer committed
185
186
187
188
189
{|Optimization options: (use -fno-<opt> to turn off -f<opt>)
  -O             Optimize the compiled code [on by default]
  -O0            Do not optimize the compiled code
  -O1 -O2 -O3    Synonymous for -O
  -Os            Optimize for code size in preference to code speed
190
  -Obranchless   Optimize to generate fewer conditional branches; try to produce
191
                 branch-free instruction sequences as much as possible
Bernhard Schommer's avatar
Bernhard Schommer committed
192
193
194
195
196
197
  -ftailcalls    Optimize function calls in tail position [on]
  -fconst-prop   Perform global constant propagation  [on]
  -ffloat-const-prop <n>  Control constant propagation of floats
                   (<n>=0: none, <n>=1: limited, <n>=2: full; default is full)
  -fcse          Perform common subexpression elimination [on]
  -fredundancy   Perform redundancy elimination [on]
Bernhard Schommer's avatar
Bernhard Schommer committed
198
  -finline       Perform inlining of functions [on]
199
200
  -finline-functions-called-once Integrate functions only required by their
                 single caller [on]
Xavier Leroy's avatar
Xavier Leroy committed
201
  -fif-conversion Perform if-conversion (generation of conditional moves) [on]
Bernhard Schommer's avatar
Bernhard Schommer committed
202
203
204
205
206
207
Code generation options: (use -fno-<opt> to turn off -f<opt>)
  -ffpu          Use FP registers for some integer operations [on]
  -fsmall-data <n>  Set maximal size <n> for allocation in small data area
  -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
  -falign-functions <n>  Set alignment (in bytes) of function entry points
  -falign-branch-targets <n>  Set alignment (in bytes) of branch targets
Bernhard Schommer's avatar
Bernhard Schommer committed
208
  -falign-cond-branches <n>  Set alignment (in bytes) of conditional branches
209
  -fcommon       Put uninitialized globals in the common section [on].
Bernhard Schommer's avatar
Bernhard Schommer committed
210
|} ^
211
 target_help ^
212
 toolchain_help ^
213
 assembler_help ^
214
 linker_help ^
Bernhard Schommer's avatar
Bernhard Schommer committed
215
216
217
218
219
220
221
222
223
224
225
226
227
{|Tracing options:
  -dprepro       Save C file after preprocessing in <file>.i
  -dparse        Save C file after parsing and elaboration in <file>.parsed.c
  -dc            Save generated Compcert C in <file>.compcert.c
  -dclight       Save generated Clight in <file>.light.c
  -dcminor       Save generated Cminor in <file>.cm
  -drtl          Save RTL at various optimization points in <file>.rtl.<n>
  -dltl          Save LTL after register allocation in <file>.ltl
  -dmach         Save generated Mach code in <file>.mach
  -dasm          Save generated assembly in <file>.s
  -dall          Save all generated intermediate files in <file>.<ext>
  -sdump         Save info for post-linking validation in <file>.json
|} ^
228
  general_help ^
229
  warning_help ^
Bernhard Schommer's avatar
Bernhard Schommer committed
230
231
232
233
234
235
  {|Interpreter mode:
  -interp        Execute given .c files using the reference interpreter
  -quiet         Suppress diagnostic messages for the interpreter
  -trace         Have the interpreter produce a detailed trace of reductions
  -random        Randomize execution order
  -all           Simulate all possible execution orders
236
  -main <name>   Start executing at function <name> instead of main()
Bernhard Schommer's avatar
Bernhard Schommer committed
237
|}
238

239
let print_usage_and_exit () =
240
241
  printf "%s" usage_string; exit 0

242
243
244
245
246
247
248
249
let dump_mnemonics destfile =
  let oc = open_out_bin destfile in
  let pp = Format.formatter_of_out_channel oc in
  AsmToJSON.pp_mnemonics pp;
  Format.pp_print_flush pp ();
  close_out oc;
  exit 0

250
let optimization_options = [
Xavier Leroy's avatar
Xavier Leroy committed
251
  option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse;
252
  option_fredundancy; option_finline; option_finline_functions_called_once;
253
254
]

255
256
let set_all opts () = List.iter (fun r -> r := true) opts
let unset_all opts () = List.iter (fun r -> r := false) opts
257

258
259
let num_source_files = ref 0

260
let num_input_files = ref 0
261

262
263
let cmdline_actions =
  let f_opt name ref =
264
    [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in
265
266
267
268
  let check_align n =
    if n <= 0 || ((n land (n - 1)) <> 0) then
      error no_loc "requested alignment %d is not a power of 2" n
    in
269
  [
270
(* Getting help *)
271
  Exact "-help", Unit print_usage_and_exit;
272
  Exact "--help", Unit print_usage_and_exit;]
273
(* Getting version info *)
274
  @ version_options tool_name @
275
(* Enforcing CompCert build numbers for QSKs and mnemonics dump *)
276
  (if Version.buildnr <> "" then
277
     [Exact "-dump-mnemonics", String  dump_mnemonics;]
278
   else []) @
279
(* Processing options *)
280
 [ Exact "-c", Set option_c;
281
282
283
  Exact "-E", Set option_E;
  Exact "-S", Set option_S;
  Exact "-o", String(fun s -> option_o := Some s);
284
  Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in
285
286
287
                              option_o := Some s);]
  (* Preprocessing options *)
    @ prepro_actions @
288
289
290
  (* Language support options *)
    language_support_options
  (* Debugging options *)
291
    @ DebugInit.debugging_actions @
292
(* Code generation options -- more below *)
293
 [
294
295
296
  Exact "-O0", Unit (unset_all optimization_options);
  Exact "-O", Unit (set_all optimization_options);
  _Regexp "-O[123]$", Unit (set_all optimization_options);
297
  Exact "-Os", Set option_Osize;
298
  Exact "-Obranchless", Set option_Obranchless;
299
300
  Exact "-fsmall-data", Integer(fun n -> option_small_data := n);
  Exact "-fsmall-const", Integer(fun n -> option_small_const := n);
Xavier Leroy's avatar
Xavier Leroy committed
301
  Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); 
302
303
304
  Exact "-falign-functions", Integer(fun n -> check_align n; option_falignfunctions := Some n);
  Exact "-falign-branch-targets", Integer(fun n -> check_align n; option_falignbranchtargets := n);
  Exact "-falign-cond-branches", Integer(fun n -> check_align n; option_faligncondbranchs := n);] @
305
      f_opt "common" option_fcommon @
306
(* Target processor options *)
307
  (if Configuration.arch = "arm" then
308
309
310
311
312
    if Configuration.model = "armv6" then
      [ Exact "-marm", Ignore ] (* Thumb needs ARMv6T2 or ARMv7 *)
    else
      [ Exact "-mthumb", Set option_mthumb;
        Exact "-marm", Unset option_mthumb; ]
313
314
315
316
317
318
319
320
   else []) @
(* Toolchain options *)
    (if not Configuration.gnu_toolchain then
       [Exact "-t", String (fun arg -> push_linker_arg "-t"; push_linker_arg arg;
                             prepro_options := arg :: "-t" :: !prepro_options;
                             assembler_options := arg :: "-t" :: !assembler_options;)]
     else
       []) @
321
(* Assembling options *)
322
  assembler_actions @
323
(* Linking options *)
324
  linker_actions @
325
(* Tracing options *)
326
 [ Exact "-dprepro", Set option_dprepro;
327
328
329
330
331
332
333
334
335
  Exact "-dparse", Set option_dparse;
  Exact "-dc", Set option_dcmedium;
  Exact "-dclight", Set option_dclight;
  Exact "-dcminor", Set option_dcminor;
  Exact "-drtl", Set option_drtl;
  Exact "-dltl", Set option_dltl;
  Exact "-dalloctrace", Set option_dalloctrace;
  Exact "-dmach", Set option_dmach;
  Exact "-dasm", Set option_dasm;
336
337
338
339
340
341
342
  Exact "-dall", Self (fun _ ->
    option_dprepro := true;
    option_dparse := true;
    option_dcmedium := true;
    option_dclight := true;
    option_dcminor := true;
    option_drtl := true;
343
    option_dltl := true;
344
345
    option_dalloctrace := true;
    option_dmach := true;
346
    option_dasm := true);
347
  Exact "-sdump", Set option_sdump;
348
  Exact "-sdump-suffix", String (fun s -> option_sdump := true; sdump_suffix:= s);
349
  Exact "-sdump-folder", String (fun s -> AsmToJSON.sdump_folder := s);] @
350
(* General options *)
351
   general_options @
352
(* Diagnostic options *)
353
  warning_options @
354
(* Interpreter mode *)
355
 [ Exact "-interp", Set option_interp;
356
357
358
  Exact "-quiet", Unit (fun () -> Interp.trace := 0);
  Exact "-trace", Unit (fun () -> Interp.trace := 2);
  Exact "-random", Unit (fun () -> Interp.mode := Interp.Random);
359
360
  Exact "-all", Unit (fun () -> Interp.mode := Interp.All);
  Exact "-main", String (fun s -> main_function_name := s)
361
 ]
362
(* Optimization options *)
363
(* -f options: come in -f and -fno- variants *)
364
  @ f_opt "tailcalls" option_ftailcalls
Xavier Leroy's avatar
Xavier Leroy committed
365
  @ f_opt "if-conversion" option_fifconversion
366
367
368
  @ f_opt "const-prop" option_fconstprop
  @ f_opt "cse" option_fcse
  @ f_opt "redundancy" option_fredundancy
369
  @ f_opt "inline" option_finline
370
  @ f_opt "inline-functions-called-once" option_finline_functions_called_once
371
(* Code generation options *)
372
373
  @ f_opt "fpu" option_ffpu
  @ f_opt "sse" option_ffpu (* backward compatibility *)
374
375
376
  @ [
(* Catch options that are not handled *)
  Prefix "-", Self (fun s ->
377
      fatal_error no_loc "Unknown option `%s'" s);
378
379
(* File arguments *)
  Suffix ".c", Self (fun s ->
380
      push_action process_c_file s; incr num_source_files; incr num_input_files);
381
  Suffix ".i", Self (fun s ->
382
      push_action process_i_file s; incr num_source_files; incr num_input_files);
383
  Suffix ".p", Self (fun s ->
384
      push_action process_i_file s; incr num_source_files; incr num_input_files);
385
  Suffix ".s", Self (fun s ->
386
      push_action process_s_file s; incr num_source_files; incr num_input_files);
387
  Suffix ".S", Self (fun s ->
388
      push_action process_S_file s; incr num_source_files; incr num_input_files);
389
390
  Suffix ".sx", Self (fun s ->
      push_action process_S_file s; incr num_source_files; incr num_input_files);
391
392
  Suffix ".o", Self (fun s -> push_linker_arg s; incr num_input_files);
  Suffix ".a", Self (fun s -> push_linker_arg s; incr num_input_files);
393
  (* GCC compatibility: .o.ext files and .so files are also object files *)
394
395
  _Regexp ".*\\.o\\.", Self (fun s -> push_linker_arg s; incr num_input_files);
  Suffix ".so", Self (fun s -> push_linker_arg s; incr num_input_files);
396
397
  (* GCC compatibility: .h files can be preprocessed with -E *)
  Suffix ".h", Self (fun s ->
398
      push_action process_h_file s; incr num_source_files; incr num_input_files);
399
  ]
400
401

let _ =
402
403
404
405
406
407
  try
    Gc.set { (Gc.get()) with
                Gc.minor_heap_size = 524288; (* 512k *)
                Gc.major_heap_increment = 4194304 (* 4M *)
           };
    Printexc.record_backtrace true;
408
    Frontend.init ();
409
    parse_cmdline cmdline_actions;
410
    DebugInit.init (); (* Initialize the debug functions *)
411
    if nolink () && !option_o <> None && !num_source_files >= 2 then
412
      fatal_error no_loc "ambiguous '-o' option (multiple source files)";
413
    if !num_input_files = 0 then
414
      fatal_error no_loc "no input file";
415
416
    if not !option_interp && !main_function_name <> "main" then
      fatal_error no_loc "option '-main' requires option '-interp'";
417
    let linker_args = time "Total compilation time" perform_actions () in
418
    if not (nolink ()) && linker_args <> [] then begin
419
      linker (output_filename_default "a.out") linker_args
420
    end;
421
422
423
424
    check_errors ()
  with
  | Sys_error msg
  | CmdError msg -> error no_loc "%s" msg; exit 2
425
  | Abort -> error_summary (); exit 2
426
  | e -> crash e