diff options
| -rw-r--r-- | Makefile | 5 | ||||
| -rw-r--r-- | arm/Asmexpand.ml | 2 | ||||
| -rwxr-xr-x | configure | 61 | ||||
| -rw-r--r-- | cparser/Cutil.ml | 2 | ||||
| -rw-r--r-- | driver/Configuration.ml | 15 | ||||
| -rw-r--r-- | driver/Driver.ml | 119 |
6 files changed, 176 insertions, 28 deletions
@@ -192,8 +192,11 @@ latexdoc: compcert.ini: Makefile.config (echo "stdlib_path=$(LIBDIR)"; \ echo "prepro=$(CPREPRO)"; \ - echo "asm=$(CASM)"; \ echo "linker=$(CLINKER)"; \ + echo "asm=$(CASM)"; \ + echo "prepro_options=$(CPREPRO_OPTIONS)";\ + echo "asm_options=$(CASM_OPTIONS)";\ + echo "linker_options=$(CLINKER_OPTIONS)";\ echo "arch=$(ARCH)"; \ echo "model=$(MODEL)"; \ echo "abi=$(ABI)"; \ diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index a64645ca..5415f78e 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -265,7 +265,7 @@ let rec next_arg_location ir ofs = function | (Tfloat | Tlong | Tany64) :: l -> if ir < 3 then next_arg_location (align ir 2 + 2) ofs l - else next_arg_location ir (align ofs 8 + 8) l + else next_arg_location 4 (align ofs 8 + 8) l let expand_builtin_va_start r = if not !current_function.fn_sig.sig_cc.cc_vararg then @@ -90,6 +90,9 @@ casmruntime="" asm_supports_cfi="" struct_passing="" struct_return="" +casm_options="" +cprepro_options="" +clinker_options="" case "$target" in powerpc-*|ppc-*|powerpc64-*|ppc64-*|e5500-*) @@ -109,7 +112,8 @@ case "$target" in *-eabi-diab) system="diab" cc="${toolprefix}dcc" - cprepro="${toolprefix}dcc -E -D__GNUC__" + cprepro="${toolprefix}dcc" + cprepro_options="-E -D__GNUC__" casm="${toolprefix}das" asm_supports_cfi=false clinker="${toolprefix}dcc" @@ -118,8 +122,10 @@ case "$target" in *) system="linux" cc="${toolprefix}gcc" - cprepro="${toolprefix}gcc -std=c99 -U__GNUC__ -E" - casm="${toolprefix}gcc -c" + cprepro="${toolprefix}gcc" + cprepro_options="-std=c99 -U__GNUC__ -E" + casm="${toolprefix}gcc" + casm_options="-c" casmruntime="${toolprefix}gcc -c -Wa,-mregnames" clinker="${toolprefix}gcc" libmath="-lm" @@ -149,8 +155,10 @@ case "$target" in struct_return="int1-4" system="linux" cc="${toolprefix}gcc" - cprepro="${toolprefix}gcc -std=c99 -U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E" - casm="${toolprefix}gcc -c" + cprepro="${toolprefix}gcc" + cprepro_options="-std=c99 -U__GNUC__ '-D__REDIRECT(name,proto,alias)=name proto' '-D__REDIRECT_NTH(name,proto,alias)=name proto' -E" + casm="${toolprefix}gcc" + casm_options="-c" clinker="${toolprefix}gcc" libmath="-lm";; ia32-linux) @@ -161,9 +169,12 @@ case "$target" in struct_return="ref" system="linux" cc="${toolprefix}gcc -m32" - cprepro="${toolprefix}gcc -std=c99 -m32 -U__GNUC__ -E" - casm="${toolprefix}gcc -m32 -c" - clinker="${toolprefix}gcc -m32" + cprepro="${toolprefix}gcc" + cprepro_options="-std=c99 -m32 -U__GNUC__ -E" + casm="${toolprefix}gcc" + casm_options="-m32 -c" + clinker="${toolprefix}gcc" + clinker_options="-m32" libmath="-lm";; ia32-bsd) arch="ia32" @@ -173,9 +184,12 @@ case "$target" in struct_return="int1248" # to check! system="bsd" cc="${toolprefix}gcc -m32" - cprepro="${toolprefix}gcc -std=c99 -m32 -U__GNUC__ -E" - casm="${toolprefix}gcc -m32 -c" - clinker="${toolprefix}gcc -m32" + cprepro="${toolprefix}gcc" + cprepro_options="-std=c99 -m32 -U__GNUC__ -E" + casm="${toolprefix}gcc" + casm_options="-m32 -c" + clinker="${toolprefix}gcc" + clinker_options="-m32" libmath="-lm";; ia32-macosx) arch="ia32" @@ -185,13 +199,16 @@ case "$target" in struct_return="int1248" system="macosx" cc="${toolprefix}gcc -arch i386" - cprepro="${toolprefix}gcc -std=c99 -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' -E" - casm="${toolprefix}gcc -arch i386 -c" + cprepro="${toolprefix}gcc" + cprepro_options="-std=c99 -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' -E" + casm="${toolprefix}gcc" + casm_options="-arch i386 -c" + clinker="${toolprefix}gcc" case `uname -r` in [1-9].*|10.*|11.*) # up to MacOS 10.7 included - clinker="${toolprefix}gcc -arch i386";; + clinker_option="-arch i386";; *) # MacOS 10.8 and up - clinker="${toolprefix}gcc -arch i386 -Wl,-no_pie";; + clinker_option="-arch i386 -Wl,-no_pie";; esac libmath="";; ia32-cygwin) @@ -202,9 +219,12 @@ case "$target" in struct_return="ref" system="cygwin" cc="${toolprefix}gcc -m32" - cprepro="${toolprefix}gcc -std=c99 -m32 -U__GNUC__ -E" - casm="${toolprefix}gcc -m32 -c" - clinker="${toolprefix}gcc -m32" + cprepro="${toolprefix}gcc" + cprepro_options="-std=c99 -m32 -U__GNUC__ -E" + casm="${toolprefix}gcc" + casm_options="-m32 -c" + clinker="${toolprefix}gcc" + clinker_options="-m32" libmath="-lm";; manual) ;; @@ -218,7 +238,7 @@ case "$target" in exit 2;; esac -if test -z "$casmruntime"; then casmruntime="$casm"; fi +if test -z "$casmruntime"; then casmruntime="$casm $casm_options"; fi # Test assembler support for CFI directives @@ -348,9 +368,12 @@ STRUCT_RETURN=$struct_return SYSTEM=$system CC=$cc CPREPRO=$cprepro +CPREPRO_OPTIONS=$cprepro_options CASM=$casm +CASM_OPTIONS=$casm_options CASMRUNTIME=$casmruntime CLINKER=$clinker +CLINKER_OPTIONS=$clinker_options LIBMATH=$libmath HAS_RUNTIME_LIB=$has_runtime_lib HAS_STANDARD_HEADERS=$has_standard_headers diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index c82ada26..c15a7adf 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -333,7 +333,7 @@ let rec equal_types env t1 t2 = | None, None -> true | Some s1, Some s2 -> s1 = s2 | _ -> false end in - size && a1 = a2 && equal_types env t1 t2 + size && a1 = a2 && equal_types env ty1 ty2 | TFun(ty1, params1, vararg1, a1), TFun(ty2, params2, vararg2, a2) -> let params = match params1, params2 with diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 3025391b..1914c1b3 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -103,9 +103,18 @@ let tool_absolute_path tools = absolute_path ini_dir tool in tool::args -let prepro = tool_absolute_path (get_config_list "prepro") -let asm = tool_absolute_path (get_config_list "asm") -let linker = tool_absolute_path (get_config_list "linker") +let opt_config_list key = + match Readconfig.key_val key with + | Some v -> v + | None -> [] + +let prepro = + tool_absolute_path (get_config_list "prepro")@(opt_config_list "prepro_options") +let asm = + tool_absolute_path (get_config_list "asm")@(opt_config_list "asm_options") +let linker = + tool_absolute_path (get_config_list "linker")@(opt_config_list "linker_options") + let arch = match get_config_string "arch" with | "powerpc"|"arm"|"ia32" as a -> a diff --git a/driver/Driver.ml b/driver/Driver.ml index 4b695d57..bbd949e0 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -20,6 +20,9 @@ open Timing let stdlib_path = ref Configuration.stdlib_path +(* Use standard headers *) +let use_standard_headers = ref Configuration.has_standard_headers + let dump_options = ref false (* Optional sdump suffix *) @@ -105,7 +108,7 @@ let preprocess ifile ofile = let cmd = List.concat [ Configuration.prepro; ["-D__COMPCERT__"]; - (if Configuration.has_standard_headers + (if !use_standard_headers then ["-I" ^ Filename.concat !stdlib_path "include" ] else []); List.rev !prepro_options; @@ -277,9 +280,18 @@ let linker exe_name files = exit 2 end +(* All input files should exist *) + +let ensure_inputfile_exists name = + if not (Sys.file_exists name) then begin + eprintf "error: no such file or directory: '%s'\n" name; + exit 2 + end + (* Processing of a .c file *) let process_c_file sourcename = + ensure_inputfile_exists sourcename; if !option_E then begin preprocess sourcename (output_filename_default "-"); "" @@ -324,6 +336,7 @@ let process_c_file sourcename = (* Processing of a .i / .p file (preprocessed C) *) let process_i_file sourcename = + ensure_inputfile_exists sourcename; if !option_interp then begin let csyntax,_ = parse_c_file sourcename sourcename in Interp.execute csyntax; @@ -351,6 +364,7 @@ let process_i_file sourcename = (* Processing of a .cm file *) let process_cminor_file sourcename = + ensure_inputfile_exists sourcename; if !option_S then begin compile_cminor_file sourcename (output_filename ~final:true sourcename ".cm" ".s"); @@ -372,11 +386,13 @@ let process_cminor_file sourcename = (* Processing of .S and .s files *) let process_s_file sourcename = + ensure_inputfile_exists sourcename; let objname = output_filename ~final: !option_c sourcename ".s" ".o" in assemble sourcename objname; objname let process_S_file sourcename = + ensure_inputfile_exists sourcename; if !option_E then begin preprocess sourcename (output_filename_default "-"); "" @@ -393,6 +409,7 @@ let process_S_file sourcename = let process_h_file sourcename = if !option_E then begin + ensure_inputfile_exists sourcename; preprocess sourcename (output_filename_default "-"); "" end else begin @@ -447,11 +464,36 @@ Processing options: -o <file> Generate output in <file> 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 - -include <file> Process <file> as if #include \"<file>\" appears at the first - line of the primary source file. + -Xpreprocessor <opt> Pass option <opt> to the preprocessor + -M (GCC only) Ouput a rule suitable for make describing the + dependencies of the main source file + -MM (GCC only) Like -M but do not mention system header files + -MF <file> (GCC only) Specifies file <file> as output file for -M or -MM + -MG (GCC only) Assumes missing header files are generated for -M + -MP (GCC only) Add a phony target for each dependency other than + the main file + -MT <target> (GCC only) Change the target of the rule emitted by dependency + generation + -MQ <target> (GCC only) Like -MT but quotes <target> + -nostdinc (GCC only) Do not search the standard system directories for + header files + -imacros <file> (GCC only) Like -include but throws output produced by + preprocessing of <file> away + -idirafter <dir> (GCC only) Search <dir> for header files after all directories + specified with -I and the standard system directories + -isystem <dir> (GCC only) Search <dir> for header files after all directories + specified by -I but before the standard system directories + -iquote <dir> (GCC only) Like -isystem but only for headers included with + quotes + -P (GCC only) Do not generate linemarkers + -C (GCC only) Do not discard comments + -CC (GCC only) Do not discard comments, including during macro + expansion Language support options (use -fno-<opt> to turn off -f<opt>) : -fbitfields Emulate bit fields in structs [off] -flongdouble Treat 'long double' as 'double' [off] @@ -494,12 +536,24 @@ Target processor options: -marm (ARM only) Use classic ARM instruction encoding Assembling options: -Wa,<opt> Pass option <opt> to the assembler + -Xassembler <opt> Pass <opt> as an option to the assembler Linking options: -l<lib> Link library <lib> -L<dir> Add <dir> to search path for libraries + -nostartfiles (GCC only) Do not use the standard system startup files when + linking + -nodefaultlibs (GCC only) Do not use the standard system libraries when + linking + -nostdlib (GCC only) Do not use the standard system startup files or + libraries when linking + -s Remove all symbol table and relocation information from the + executable -static Prevent linking with the shared libraries -T <file> Use <file> as linker command file -Wl,<opt> Pass option <opt> to the linker + -Xlinker <opt> Pass <opt> as an option to the linker + -u <symb> Pretend the symbol <symb> is undefined to force linking of + library modules to define it. Tracing options: -dprepro Save C file after preprocessing in <file>.i -dparse Save C file after parsing and elaboration in <file>.parse.c @@ -544,6 +598,35 @@ let optimization_options = [ let set_all opts = List.iter (fun r -> r := true) opts let unset_all opts = List.iter (fun r -> r := false) opts +let gnu_option s = + if Configuration.system <> "diab" then + true + else begin + eprintf "ccomp: warning: option %s only supported for gcc backend\n" s; + false + end + +let gnu_linker_opt s = + if gnu_option s then + push_linker_arg s + +(* Add gnu preprocessor list *) +let gnu_prepro_opt_key key s = + if gnu_option s then + prepro_options := s::key::!prepro_options + +(* Add gnu preprocessor option *) +let gnu_prepro_opt s = + if gnu_option s then + prepro_options := s::!prepro_options + +(* Add gnu preprocessor option s and the implict -E *) +let gnu_prepro_opt_e s = + if gnu_option s then begin + prepro_options := s :: !prepro_options; + option_E := true + end + let num_source_files = ref 0 let num_input_files = ref 0 @@ -576,7 +659,24 @@ let cmdline_actions = 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); + 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"); + Exact "-iquote", String (gnu_prepro_opt_key "-iquore"); + Exact "-P", Self gnu_prepro_opt; + Exact "-C", Self gnu_prepro_opt; + Exact "-CC", Self gnu_prepro_opt; (* Language support options -- more below *) Exact "-fall", Self (fun _ -> set_all language_support_options); Exact "-fnone", Self (fun _ -> unset_all language_support_options); @@ -615,9 +715,17 @@ let cmdline_actions = assembler_options := List.rev_append (explode_comma_option s) !assembler_options else assembler_options := s :: !assembler_options); + Exact "-Xassembler", String (fun s -> if Configuration.system = "diab" then + assembler_options := s::!assembler_options + else + assembler_options := s::"-Xassembler":: !assembler_options); (* Linking options *) Prefix "-l", Self push_linker_arg; Prefix "-L", Self push_linker_arg; + Exact "-nostartfiles", Self gnu_linker_opt; + Exact "-nodefaultlibs", Self gnu_linker_opt; + Exact "-nostdlib", Self gnu_linker_opt; + Exact "-s", Self push_linker_arg; Exact "-static", Self push_linker_arg; Exact "-T", String (fun s -> if Configuration.system = "diab" then push_linker_arg ("-Wm"^s) @@ -625,7 +733,12 @@ let cmdline_actions = push_linker_arg ("-T"); push_linker_arg(s) end); + Exact "-Xlinker", String (fun s -> if Configuration.system = "diab" then + push_linker_arg ("-Wl,"^s) + else + push_linker_arg s); Prefix "-Wl,", Self push_linker_arg; + Exact "-u", Self push_linker_arg; (* Tracing options *) Exact "-dprepro", Set option_dprepro; Exact "-dparse", Set option_dparse; |