Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Frontend.ml 8.8 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*      Bernhard Schommer, AbsInt Angewandte Informatik GmbH           *)
(*                                                                     *)
(*  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.     *)
(*                                                                     *)
(* *********************************************************************)

14
open Printf
15
16
17
18
19
20
open Clflags
open Commandline
open Driveraux

(* Common frontend functions between clightgen and ccomp *)

21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
(* Split the version number into major.minor *)

let re_version = Str.regexp {|\([0-9]+\)\.\([0-9]+\)|}

let (v_major, v_minor) =
  let get n = int_of_string (Str.matched_group n Version.version) in
  assert (Str.string_match re_version Version.version 0);
  (get 1, get 2)

let v_number =
  assert (v_minor < 100);
  100 * v_major + v_minor

(* Predefined macros: version numbers, C11 features *)

36
let predefined_macros =
37
  let macros = [  
38
    "-D__COMPCERT__";
39
40
41
    sprintf "-D__COMPCERT_MAJOR__=%d" v_major;    
    sprintf "-D__COMPCERT_MINOR__=%d" v_minor;    
    sprintf "-D__COMPCERT_VERSION__=%d" v_number;    
42
43
44
45
46
    "-U__STDC_IEC_559_COMPLEX__";
    "-D__STDC_NO_ATOMICS__";
    "-D__STDC_NO_COMPLEX__";
    "-D__STDC_NO_THREADS__";
    "-D__STDC_NO_VLA__"
47
48
49
50
  ] in
  if Version.buildnr = ""
  then macros
  else sprintf "-D__COMPCERT_BUILDNR__=%s" Version.buildnr :: macros
51
52
53
54

(* From C to preprocessed C *)

let preprocess ifile ofile =
55
  Diagnostics.raise_on_errors ();
56
57
58
59
  let output =
    if ofile = "-" then None else Some ofile in
  let cmd = List.concat [
    Configuration.prepro;
60
    predefined_macros;
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
    (if !Clflags.use_standard_headers
     then ["-I" ^ Filename.concat !Clflags.stdlib_path "include" ]
     else []);
    List.rev !prepro_options;
    [ifile]
  ] in
  let exc = command ?stdout:output cmd in
  if exc <> 0 then begin
    if ofile <> "-" then safe_remove ofile;
    command_error "preprocessor" exc;
  end

(* From preprocessed C to Csyntax *)

let parse_c_file sourcename ifile =
  Debug.init_compile_unit sourcename;
  Sections.initialize();
78
  CPragmas.reset();
79
80
81
82
83
84
85
86
  (* Simplification options *)
  let simplifs =
    "b" (* blocks: mandatory *)
  ^ (if !option_fstruct_passing then "s" else "")
  ^ (if !option_fbitfields then "f" else "")
  ^ (if !option_fpacked_structs then "p" else "")
  in
  (* Parsing and production of a simplified C AST *)
87
  let ast = Parse.preprocessed_file simplifs sourcename ifile in
88
  (* Save C AST if requested *)
89
  Cprint.print_if ast;
90
  (* Conversion to Csyntax *)
91
  let csyntax = Timing.time "CompCert C generation" C2C.convertProgram ast in
92
  (* Save CompCert C AST if requested *)
93
  PrintCsyntax.print_if csyntax;
94
95
  csyntax

96
97
98
let init () =
  Machine.config:=
    begin match Configuration.arch with
99
100
101
102
103
104
    | "powerpc" -> if Configuration.model = "e5500" || Configuration.model = "ppc64"
                   then if Configuration.abi = "linux" then Machine.ppc_32_r64_linux_bigendian
                   else if Configuration.gnu_toolchain then Machine.ppc_32_r64_bigendian
                   else Machine.ppc_32_r64_diab_bigendian
                   else if Configuration.abi = "linux" then Machine.ppc_32_linux_bigendian
                   else if Configuration.gnu_toolchain then Machine.ppc_32_bigendian
105
106
107
108
109
110
111
                   else Machine.ppc_32_diab_bigendian
    | "arm"     -> if Configuration.is_big_endian
                   then Machine.arm_bigendian
                   else Machine.arm_littleendian
    | "x86"     -> if Configuration.model = "64" then
                     Machine.x86_64
                   else
Xavier Leroy's avatar
Xavier Leroy committed
112
113
                     if Configuration.abi = "macos"
                     then Machine.x86_32_macos
114
115
                     else if Configuration.system = "bsd"
                     then Machine.x86_32_bsd
116
117
118
119
                     else Machine.x86_32
    | "riscV"   -> if Configuration.model = "64"
                   then Machine.rv64
                   else Machine.rv32
120
121
    | "kvx" -> if Configuration.os = "cos" then Machine.kvxcos
               else if Configuration.os = "mbr" then Machine.kvxmbr
Cyril SIX's avatar
Cyril SIX committed
122
               else if Configuration.os = "elf" then Machine.kvxelf
123
124
               else (Printf.eprintf "Configuration OS = %s\n" Configuration.os;
                 failwith "Wrong OS configuration for KVX")
Xavier Leroy's avatar
Xavier Leroy committed
125
126
127
    | "aarch64" -> if Configuration.abi = "apple"
                   then Machine.aarch64_apple
                   else Machine.aarch64
128
129
    | _         -> assert false
  end;
130
  Env.set_builtins C2C.builtins;
131
132
133
134
  Cutil.declare_attributes C2C.attributes;
  CPragmas.initialize()


135
136
(* Add gnu preprocessor list *)
let gnu_prepro_opt_key key s =
137
  prepro_options := s::key::!prepro_options
138
139
140

(* Add gnu preprocessor option *)
let gnu_prepro_opt s =
141
  prepro_options := s::!prepro_options
142

143
(* Add gnu preprocessor option s and the implicit -E *)
144
let gnu_prepro_opt_e s =
145
146
  prepro_options := s :: !prepro_options;
  option_E := true
147

148
let gnu_prepro_actions = [
149
150
151
152
153
154
155
156
157
158
159
  Exact "-M", Self gnu_prepro_opt_e;
  Exact "-MM", Self gnu_prepro_opt_e;
  Exact "-MF", String (gnu_prepro_opt_key "-MF");
  Exact "-MG", Self gnu_prepro_opt;
  Exact "-MP", Self gnu_prepro_opt;
  Exact "-MT", String (gnu_prepro_opt_key "-MT");
  Exact "-MQ", String (gnu_prepro_opt_key "-MQ");
  Exact "-nostdinc", Self (fun s -> gnu_prepro_opt s; use_standard_headers := false);
  Exact "-imacros", String (gnu_prepro_opt_key "-imacros");
  Exact "-idirafter", String (gnu_prepro_opt_key "-idirafter");
  Exact "-isystem", String (gnu_prepro_opt_key "-isystem");
160
  Exact "-iquote", String (gnu_prepro_opt_key "-iquote");
161
162
163
164
  Exact "-P", Self gnu_prepro_opt;
  Exact "-C", Self gnu_prepro_opt;
  Exact "-CC", Self gnu_prepro_opt;]

165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
let prepro_actions = [
  (* Preprocessing options *)
  Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options;
    assembler_options := s :: "-I" :: !assembler_options);
  Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options;
    assembler_options := s :: !assembler_options);
  Exact "-D", String(fun s -> prepro_options := s :: "-D" :: !prepro_options);
  Prefix "-D", Self(fun s -> prepro_options := s :: !prepro_options);
  Exact "-U", String(fun s -> prepro_options := s :: "-U" :: !prepro_options);
  Prefix "-U", Self(fun s -> prepro_options := s :: !prepro_options);
  Prefix "-Wp,", Self (fun s ->
    prepro_options := List.rev_append (explode_comma_option s) !prepro_options);
  Exact "-Xpreprocessor", String (fun s ->
    prepro_options := s :: !prepro_options);
  Exact "-include", String (fun s -> prepro_options := s :: "-include" :: !prepro_options);]
180
  @ (if Configuration.gnu_toolchain then gnu_prepro_actions else [])
181
182

let gnu_prepro_help =
183
{|  -M            Output a rule suitable for make describing the
Bernhard Schommer's avatar
Bernhard Schommer committed
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
                 dependencies of the main source file
  -MM            Like -M but do not mention system header files
  -MF <file>     Specifies file <file> as output file for -M or -MM
  -MG            Assumes missing header files are generated for -M
  -MP            Add a phony target for each dependency other than
                 the main file
  -MT <target>   Change the target of the rule emitted by dependency
                 generation
  -MQ <target>   Like -MT but quotes <target>
  -nostdinc      Do not search the standard system directories for
                 header files
  -imacros <file> Like -include but throws output produced by
                  preprocessing of <file> away
  -idirafter <dir> Search <dir> for header files after all directories
                   specified with -I and the standard system directories
  -isystem <dir>  Search <dir> for header files after all directories
                  specified by -I but before the standard system directories
  -iquote <dir>   Like -isystem but only for headers included with
                  quotes
  -P              Do not generate linemarkers
  -C              Do not discard comments
  -CC             Do not discard comments, including during macro
                  expansion
|}
208

Bernhard Schommer's avatar
Bernhard Schommer committed
209
210
211
212
213
214
215
216
217
let prepro_help = {|Preprocessing options:
  -I<dir>        Add <dir> to search path for #include files
  -include <file> Process <file> as if #include "<file>" appears at the first
                  line of the primary source file.
  -D<symb>=<val> Define preprocessor symbol
  -U<symb>       Undefine preprocessor symbol
  -Wp,<opt>      Pass option <opt> to the preprocessor
  -Xpreprocessor <opt> Pass option <opt> to the preprocessor
|}
218
  ^ (if Configuration.gnu_toolchain then gnu_prepro_help else "")