From f15e5f77cb751c2c3065e0587c790bfb598d02d6 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 15 Nov 2014 10:22:55 +0100 Subject: cchecklink: added option "-files-from" to read .sdump file names from a file or from standard input. --- Changelog | 3 ++- checklink/Validator.ml | 30 +++++++++++++++++++++++++++--- 2 files changed, 29 insertions(+), 4 deletions(-) diff --git a/Changelog b/Changelog index 4b102d78..87b2174f 100644 --- a/Changelog +++ b/Changelog @@ -1,7 +1,8 @@ - In string and character literals, treat illegal escape sequences (e.g. "\%" or "\0") as an error instead of a warning. - Upgraded Flocq to version 2.4.0. - +- cchecklink: added option "-files-from" to read .sdump file names + from a file or from standard input. Release 2.4, 2014-09-17 ======================= diff --git a/checklink/Validator.ml b/checklink/Validator.ml index baf06fca..6969409a 100644 --- a/checklink/Validator.ml +++ b/checklink/Validator.ml @@ -22,6 +22,27 @@ let set_conf_file s = | Some _ -> raise (Arg.Bad "multiple configuration files given on command line") end +let read_sdumps_from_channel ic = + try + while true do + let l = input_line ic in + if l <> "" then sdump_files := l :: !sdump_files + done + with End_of_file -> + () + +let read_sdumps_from_file f = + if f = "-" then + read_sdumps_from_channel stdin + else begin + try + let ic = open_in f in + read_sdumps_from_channel ic; + close_in ic + with Sys_error msg -> + Printf.eprintf "Error reading file: %s\n" msg; exit 2 + end + let option_disassemble = ref false let disassemble_list = ref ([]: string list) let add_disassemble s = @@ -31,12 +52,15 @@ let add_disassemble s = let options = [ (* Main options *) "-exe", Arg.String set_elf_file, - " Specify the ELF executable file to analyze"; + " Specify the ELF executable file to analyze"; "-conf", Arg.String set_conf_file, - " Specify a configuration file"; + " Specify a configuration file"; + "-files-from", Arg.String read_sdumps_from_file, + " Read names of .sdump files from the given file\n\ + \t(or from standard input if is '-')"; (* Parsing behavior *) "-relaxed", Arg.Set ELF_parsers.relaxed, - "Allows the following behaviors in the ELF parser: + "Allows the following behaviors in the ELF parser:\n\ \t* Use of a fallback heuristic to resolve symbols bootstrapped at load time"; (* Printing behavior *) "-no-exhaustive", Arg.Clear Check.exhaustivity, -- cgit From c0e30d13ba9f9fac433828f046346281904508f2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 15 Nov 2014 18:28:04 +0100 Subject: build_from_parsed: simplified code + correctness proof. --- lib/Floats.v | 101 ++++++++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 86 insertions(+), 15 deletions(-) diff --git a/lib/Floats.v b/lib/Floats.v index e867cba8..f86632b9 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -92,28 +92,99 @@ Proof. destruct x as [[]|]; simpl; intros; discriminate. Qed. -(** Function used to parse floats *) +Section FP_PARSING. -Program Definition build_from_parsed - (prec:Z) (emax:Z) (prec_gt_0 : Prec_gt_0 prec) (Hmax:prec < emax) - (base:positive) (intPart:positive) (expPart:Z) := - match expPart return _ with +Variables prec emax: Z. +Context (prec_gt_0 : Prec_gt_0 prec). +Hypothesis Hmax : (prec < emax)%Z. + +(** Function used to convert literals into FP numbers during parsing. + [intPart] is the mantissa + [expPart] is the exponent + [base] is the base for the exponent (usually 10 or 16). + The result is [intPart * base^expPart] rounded to the nearest FP number, + ties to even. *) + +Definition build_from_parsed (base:positive) (intPart:positive) (expPart:Z) : binary_float prec emax := + match expPart with | Z0 => binary_normalize prec emax prec_gt_0 Hmax mode_NE (Zpos intPart) Z0 false | Zpos p => binary_normalize prec emax prec_gt_0 Hmax mode_NE ((Zpos intPart) * Zpower_pos (Zpos base) p) Z0 false | Zneg p => - let exp := Zpower_pos (Zpos base) p in - match exp return 0 < exp -> _ with - | Zneg _ | Z0 => _ - | Zpos p => - fun _ => - FF2B prec emax _ (proj1 (Bdiv_correct_aux prec emax prec_gt_0 Hmax mode_NE false intPart Z0 false p Z0)) - end _ + FF2B prec emax _ (proj1 (Bdiv_correct_aux prec emax prec_gt_0 Hmax mode_NE + false intPart Z0 false (Pos.pow base p) Z0)) end. -Next Obligation. - apply Zpower_pos_gt_0. reflexivity. -Qed. + +Let emin := (3 - emax - prec)%Z. +Let fexp := FLT_exp emin prec. + +Theorem build_from_parsed_correct: + forall base m e (BASE: 2 <= Zpos base), + let base_r := {| radix_val := Zpos base; radix_prop := Zle_imp_le_bool _ _ BASE |} in + let r := round radix2 fexp (round_mode mode_NE) (Z2R (Zpos m) * bpow base_r e) in + if Rlt_bool (Rabs r) (bpow radix2 emax) then + B2R _ _ (build_from_parsed base m e) = r + /\ is_finite _ _ (build_from_parsed base m e) = true + /\ Bsign _ _ (build_from_parsed base m e) = false + else + B2FF _ _ (build_from_parsed base m e) = F754_infinity false. +Proof. + intros. + assert (A: forall x, @F2R radix2 {| Fnum := x; Fexp := 0 |} = Z2R x). + { intros. unfold F2R, Fnum; simpl. ring. } + unfold build_from_parsed, r; destruct e. +- change (bpow base_r 0) with (1%R). rewrite Rmult_1_r. + generalize (binary_normalize_correct _ _ _ Hmax mode_NE (Zpos m) 0 false). + fold emin; fold fexp. rewrite ! A. + destruct (Rlt_bool (Rabs (round radix2 fexp (round_mode mode_NE) (Z2R (Z.pos m)))) + (bpow radix2 emax)). + + intros (P & Q & R). split. auto. split. auto. rewrite R. rewrite Rcompare_Gt; auto. + apply (Z2R_lt 0). compute; auto. + + intros P; rewrite P. unfold binary_overflow. + replace (Rlt_bool (Z2R (Z.pos m)) 0%R) with false. auto. + rewrite Rlt_bool_false; auto. apply (Z2R_le 0). xomega. +- generalize (binary_normalize_correct _ _ _ Hmax mode_NE (Zpos m * Z.pow_pos (Zpos base) p) 0 false). + fold emin; fold fexp. rewrite ! A. + assert (B: Z2R (Z.pos m * Z.pow_pos (Z.pos base) p) = (Z2R (Z.pos m) * bpow base_r (Z.pos p))%R). + { unfold bpow. apply Z2R_mult. } + rewrite B. + destruct (Rlt_bool + (Rabs + (round radix2 fexp (round_mode mode_NE) + (Z2R (Z.pos m) * bpow base_r (Z.pos p)))) (bpow radix2 emax)). + + intros (P & Q & R). split. auto. split. auto. rewrite R. rewrite Rcompare_Gt; auto. + apply Rmult_lt_0_compat. apply (Z2R_lt 0). xomega. apply bpow_gt_0. + + intros P. rewrite P. unfold binary_overflow. + replace (Rlt_bool (Z2R (Z.pos m) * bpow base_r (Z.pos p)) 0) with false. + auto. + rewrite Rlt_bool_false; auto. apply Rlt_le. apply Rmult_lt_0_compat. apply (Z2R_lt 0). xomega. apply bpow_gt_0. +- generalize (Bdiv_correct_aux prec emax prec_gt_0 Hmax mode_NE false m 0 false (base ^ p) 0). + set (f := + match Fdiv_core_binary prec (Z.pos m) 0 (Z.pos (base ^ p)) 0 with + | (0, _, _) => F754_nan false 1 + | (Z.pos mz0, ez, lz) => + binary_round_aux prec emax mode_NE (xorb false false) mz0 ez lz + | (Z.neg _, _, _) => F754_nan false 1 + end). + fold emin; fold fexp. rewrite ! A. unfold cond_Zopp. + assert (B: (Z2R (Z.pos m) / Z2R (Z.pos (base ^ p)) = + Z2R (Z.pos m) * bpow base_r (Z.neg p))%R). + { change (Z.neg p) with (- (Z.pos p)). rewrite bpow_opp. unfold Rdiv. f_equal. f_equal. + unfold bpow. f_equal. simpl. apply Pos2Z.inj_pow_pos. } + rewrite ! B. + destruct (Rlt_bool + (Rabs + (round radix2 fexp (round_mode mode_NE) + (Z2R (Z.pos m) * bpow base_r (Z.neg p)))) (bpow radix2 emax)). + + intros (P & Q & R & S). + split. rewrite B2R_FF2B. exact Q. + split. rewrite is_finite_FF2B. auto. + rewrite Bsign_FF2B. auto. + + intros (P & Q). rewrite B2FF_FF2B. auto. +Qed. + +End FP_PARSING. Local Notation __ := (refl_equal Datatypes.Lt). -- cgit From ef4334c5b3984277a0844ba94f6b3945152e3637 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 16 Nov 2014 14:00:11 +0100 Subject: Revised parsing of command-line arguments (in preparation for adding more). Honor "ccomp -E foo.h" for GCC compatibility. Accept .o.ext files as object files for GCC compatibility. Fixed and improved handling of Cminor source files. --- driver/Commandline.ml | 105 +++++++++++++++++++++++ driver/Commandline.mli | 41 +++++++++ driver/Driver.ml | 222 +++++++++++++++++++++++-------------------------- 3 files changed, 250 insertions(+), 118 deletions(-) create mode 100644 driver/Commandline.ml create mode 100644 driver/Commandline.mli diff --git a/driver/Commandline.ml b/driver/Commandline.ml new file mode 100644 index 00000000..bc095af6 --- /dev/null +++ b/driver/Commandline.ml @@ -0,0 +1,105 @@ +(* *********************************************************************) +(* *) +(* 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 GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Parsing of command-line flags and arguments *) + +open Printf + +type pattern = + | Exact of string + | Prefix of string + | Suffix of string + | Regexp of Str.regexp + +let _Regexp re = Regexp (Str.regexp re) + +type action = + | Set of bool ref + | Unset of bool ref + | Self of (string -> unit) + | String of (string -> unit) + | Integer of (int -> unit) + +let match_pattern text = function + | Exact s -> + text = s + | Prefix pref -> + let lpref = String.length pref and ltext = String.length text in + lpref < ltext && String.sub text 0 lpref = pref + (* strict prefix: no match if pref = text. See below. *) + | Suffix suff -> + let lsuff = String.length suff and ltext = String.length text in + lsuff < ltext && String.sub text (ltext - lsuff) lsuff = suff + (* strict suffix: no match if suff = text, so that e.g. ".c" + causes an error rather than being treated as a C source file. *) + | Regexp re -> + Str.string_match re text 0 + +let rec find_action text = function + | [] -> None + | (pat, act) :: rem -> + if match_pattern text pat then Some act else find_action text rem + +let parse_array spec usage argv first last = + (* Split the spec into Exact patterns (in a hashtable) and other patterns *) + let exact_cases = (Hashtbl.create 29 : (string, action) Hashtbl.t) in + let rec split_spec = function + | [] -> [] + | (Exact s, act) :: rem -> Hashtbl.add exact_cases s act; split_spec rem + | (pat, act) :: rem -> (pat, act) :: split_spec rem in + let inexact_cases = split_spec spec in + (* Parse the vector of arguments *) + let rec parse i = + if i <= last then begin + let s = argv.(i) in + let optact = + try Some (Hashtbl.find exact_cases s) + with Not_found -> find_action s inexact_cases in + match optact with + | None -> + if s <> "-help" && s <> "--help" + then eprintf "Unknown argument `%s'\n" s + else printf "%s" usage; + exit 2 + | Some(Set r) -> + r := true; parse (i+1) + | Some(Unset r) -> + r := false; parse (i+1) + | Some(Self fn) -> + fn s; parse (i+1) + | Some(String fn) -> + if i + 1 <= last then begin + fn argv.(i+1); parse (i+2) + end else begin + eprintf "Option `%s' expects an argument\n" s; exit 2 + end + | Some(Integer fn) -> + if i + 1 <= last then begin + let n = + try + int_of_string argv.(i+1) + with Failure _ -> + eprintf "Argument to option `%s' must be an integer\n" s; + exit 2 + in + fn n; parse (i+2) + end else begin + eprintf "Option `%s' expects an argument\n" s; exit 2 + end + end + in parse first + +let parse_cmdline spec usage = + parse_array spec usage Sys.argv 1 (Array.length Sys.argv - 1) diff --git a/driver/Commandline.mli b/driver/Commandline.mli new file mode 100644 index 00000000..7a18905f --- /dev/null +++ b/driver/Commandline.mli @@ -0,0 +1,41 @@ +(* *********************************************************************) +(* *) +(* 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 GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Parsing of command-line flags and arguments *) + +(* A command-line specification is a list of pairs (pattern, action). + Command-line words are matched against the patterns, and the + corresponding actions are invoked. *) + +type pattern = + | Exact of string (** exactly this string *) + | Prefix of string (** any string starting with this prefix *) + | Suffix of string (** any string ending with this suffix *) + | Regexp of Str.regexp (** any string matching this anchored regexp *) + +val _Regexp: string -> pattern (** text of an [Str] regexp *) + +type action = + | Set of bool ref (** set the given ref to true *) + | Unset of bool ref (** set the given ref to false *) + | Self of (string -> unit) (** call the function with the matched string *) + | String of (string -> unit) (** read next arg as a string, call function *) + | Integer of (int -> unit) (** read next arg as an int, call function *) + +val parse_cmdline: + (pattern * action) list -> string (* usage string *) -> unit + +(* Note on precedence: [Exact] patterns are tried first, then the other + patterns are tried in the order in which they appear in the list. *) diff --git a/driver/Driver.ml b/driver/Driver.ml index 18005302..602b01be 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -11,6 +11,7 @@ (* *********************************************************************) open Printf +open Commandline open Camlcoq open Clflags open Timing @@ -89,7 +90,6 @@ let parse_c_file sourcename ifile = (* Simplification options *) let simplifs = "b" (* blocks: mandatory *) -(* ^ (if !option_flonglong then "l" else "") *) ^ (if !option_fstruct_return then "s" else "") ^ (if !option_fbitfields then "f" else "") ^ (if !option_fpacked_structs then "p" else "") @@ -170,6 +170,14 @@ let compile_c_file sourcename ifile ofile = (* From Cminor to asm *) let compile_cminor_file ifile ofile = + (* Prepare to dump RTL, Mach, etc, if requested *) + let set_dest dst opt ext = + dst := if !opt then Some (output_filename ifile ".cm" ext) + else None in + set_dest PrintRTL.destination option_drtl ".rtl"; + set_dest Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; + set_dest PrintLTL.destination option_dltl ".ltl"; + set_dest PrintMach.destination option_dmach ".mach"; Sections.initialize(); let ic = open_in ifile in let lb = Lexing.from_channel ic in @@ -292,7 +300,7 @@ let process_cminor_file sourcename = then output_filename sourcename ".cm" ".s" else Filename.temp_file "compcert" ".s" in compile_cminor_file sourcename asmname; - let objname = output_filename ~final: !option_c sourcename ".c" ".o" in + let objname = output_filename ~final: !option_c sourcename ".cm" ".o" in assemble asmname objname; if not !option_dasm then safe_remove asmname; objname @@ -318,6 +326,17 @@ let process_S_file sourcename = objname end +(* Processing of .h files *) + +let process_h_file sourcename = + if !option_E then begin + preprocess sourcename (output_filename_default "-"); + "" + end else begin + eprintf "Error: input file %s ignored (not in -E mode)\n" sourcename; + exit 2 + end + (* Record actions to be performed after parsing the command line *) let actions : ((string -> string) * string) list ref = ref [] @@ -341,57 +360,6 @@ let explode_comma_option s = | [] -> assert false | hd :: tl -> tl -type action = - | Set of bool ref - | Unset of bool ref - | Self of (string -> unit) - | String of (string -> unit) - | Integer of (int -> unit) - -let rec find_action s = function - | [] -> None - | (re, act) :: rem -> - if Str.string_match re s 0 then Some act else find_action s rem - -let parse_cmdline spec usage = - let acts = List.map (fun (pat, act) -> (Str.regexp pat, act)) spec in - let rec parse i = - if i < Array.length Sys.argv then begin - let s = Sys.argv.(i) in - match find_action s acts with - | None -> - if s <> "-help" && s <> "--help" - then eprintf "Unknown argument `%s'\n" s - else printf "%s" usage; - exit 2 - | Some(Set r) -> - r := true; parse (i+1) - | Some(Unset r) -> - r := false; parse (i+1) - | Some(Self fn) -> - fn s; parse (i+1) - | Some(String fn) -> - if i + 1 < Array.length Sys.argv then begin - fn Sys.argv.(i+1); parse (i+2) - end else begin - eprintf "Option `%s' expects an argument\n" s; exit 2 - end - | Some(Integer fn) -> - if i + 1 < Array.length Sys.argv then begin - let n = - try - int_of_string Sys.argv.(i+1) - with Failure _ -> - eprintf "Argument to option `%s' must be an integer\n" s; - exit 2 - in - fn n; parse (i+2) - end else begin - eprintf "Option `%s' expects an argument\n" s; exit 2 - end - end - in parse 1 - let usage_string = "The CompCert C verified compiler, version " ^ Configuration.version ^ " Usage: ccomp [options] @@ -478,75 +446,91 @@ let num_source_files = ref 0 let cmdline_actions = let f_opt name ref = - ["-f" ^ name ^ "$", Set ref; "-fno-" ^ name ^ "$", Unset ref] in + [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in [ - "-I$", String(fun s -> prepro_options := s :: "-I" :: !prepro_options); - "-D$", String(fun s -> prepro_options := s :: "-D" :: !prepro_options); - "-U$", String(fun s -> prepro_options := s :: "-U" :: !prepro_options); - "-[IDU].", Self(fun s -> prepro_options := s :: !prepro_options); - "-[lL].", Self(fun s -> push_linker_arg s); - "-o$", String(fun s -> option_o := Some s); - "-E$", Set option_E; - "-S$", Set option_S; - "-c$", Set option_c; - "-v$", Set option_v; - "-g$", Self (fun s -> option_g := true; push_linker_arg s); - "-stdlib$", String(fun s -> stdlib_path := s); - "-dparse$", Set option_dparse; - "-dc$", Set option_dcmedium; - "-dclight$", Set option_dclight; - "-dcminor", Set option_dcminor; - "-drtl$", Set option_drtl; - "-dltl$", Set option_dltl; - "-dalloctrace$", Set option_dalloctrace; - "-dmach$", Set option_dmach; - "-dasm$", Set option_dasm; - "-sdump$", Set option_sdump; - "-interp$", Set option_interp; - "-quiet$", Self (fun _ -> Interp.trace := 0); - "-trace$", Self (fun _ -> Interp.trace := 2); - "-random$", Self (fun _ -> Interp.mode := Interp.Random); - "-all$", Self (fun _ -> Interp.mode := Interp.All); - ".*\\.c$", Self (fun s -> - push_action process_c_file s; - incr num_source_files); - ".*\\.[ip]$", Self (fun s -> - push_action process_i_file s; - incr num_source_files); - ".*\\.cm$", Self (fun s -> - push_action process_cminor_file s; - incr num_source_files); - ".*\\.s$", Self (fun s -> - push_action process_s_file s; - incr num_source_files); - ".*\\.S$", Self (fun s -> - push_action process_S_file s; - incr num_source_files); - ".*\\.[oa]$", Self (fun s -> - push_linker_arg s); - "-Wp,", Self (fun s -> - prepro_options := List.rev_append (explode_comma_option s) !prepro_options); - "-Wa,", Self (fun s -> - assembler_options := s :: !assembler_options); - "-Wl,", Self (fun s -> - push_linker_arg s); - "-Os$", Set option_Osize; - "-O$", Unset option_Osize; - "-timings$", Set option_timings; - "-mthumb$", Set option_mthumb; - "-marm$", Unset option_mthumb; - "-fsmall-data$", Integer(fun n -> option_small_data := n); - "-fsmall-const$", Integer(fun n -> option_small_const := n); - "-ffloat-const-prop$", Integer(fun n -> option_ffloatconstprop := n); - "-falign-functions$", Integer(fun n -> option_falignfunctions := Some n); - "-falign-branch-targets", Integer(fun n -> option_falignbranchtargets := n); - "-falign-cond-branches", Integer(fun n -> option_faligncondbranchs := n); - "-fall$", Self (fun _ -> +(* File arguments *) + Suffix ".c", Self (fun s -> + push_action process_c_file s; incr num_source_files); + Suffix ".i", Self (fun s -> + push_action process_i_file s; incr num_source_files); + Suffix ".p", Self (fun s -> + push_action process_i_file s; incr num_source_files); + Suffix ".cm", Self (fun s -> + push_action process_cminor_file s; incr num_source_files); + Suffix ".s", Self (fun s -> + push_action process_s_file s; incr num_source_files); + Suffix ".S", Self (fun s -> + push_action process_S_file s; incr num_source_files); + Suffix ".o", Self push_linker_arg; + Suffix ".a", Self push_linker_arg; + (* GCC compatibility: .o.ext files are also object files *) + _Regexp ".*\\.o\\.", Self push_linker_arg; + (* GCC compatibility: .h files can be preprocessed with -E *) + Suffix ".h", Self (fun s -> + push_action process_h_file s; incr num_source_files); +(* Processing options *) + Exact "-c", Set option_c; + Exact "-E", Set option_E; + Exact "-S", Set option_S; + Exact "-o", String(fun s -> option_o := Some s); +(* Preprocessing options *) + Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options); + Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_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); +(* Language support options -- more below *) + Exact "-fall", Self (fun _ -> List.iter (fun r -> r := true) language_support_options); - "-fnone$", Self (fun _ -> + Exact "-fnone", Self (fun _ -> List.iter (fun r -> r := false) language_support_options); +(* Debugging options *) + Exact "-g", Self (fun s -> option_g := true; push_linker_arg s); +(* Code generation options -- more below *) + Exact "-Os", Set option_Osize; + Exact "-O", Unset option_Osize; + Exact "-fsmall-data", Integer(fun n -> option_small_data := n); + Exact "-fsmall-const", Integer(fun n -> option_small_const := n); + Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); + Exact "-falign-functions", Integer(fun n -> option_falignfunctions := Some n); + Exact "-falign-branch-targets", Integer(fun n -> option_falignbranchtargets := n); + Exact "-falign-cond-branches", Integer(fun n -> option_faligncondbranchs := n); +(* Target processor options *) + Exact "-mthumb", Set option_mthumb; + Exact "-marm", Unset option_mthumb; +(* Assembling options *) + Prefix "-Wa,", Self (fun s -> assembler_options := s :: !assembler_options); +(* Linking options *) + Prefix "-l", Self push_linker_arg; + Prefix "-L", Self push_linker_arg; + Prefix "-Wl,", Self push_linker_arg; +(* Tracing options *) + 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; + Exact "-sdump", Set option_sdump; +(* General options *) + Exact "-v", Set option_v; + Exact "-stdlib", String(fun s -> stdlib_path := s); + Exact "-timings", Set option_timings; +(* Interpreter mode *) + Exact "-interp", Set option_interp; + Exact "-quiet", Self (fun _ -> Interp.trace := 0); + Exact "-trace", Self (fun _ -> Interp.trace := 2); + Exact "-random", Self (fun _ -> Interp.mode := Interp.Random); + Exact "-all", Self (fun _ -> Interp.mode := Interp.All) ] - @ f_opt "tailcalls" option_ftailcalls +(* -f options: come in -f and -fno- variants *) +(* Language support options *) @ f_opt "longdouble" option_flongdouble @ f_opt "struct-return" option_fstruct_return @ f_opt "bitfields" option_fbitfields @@ -554,6 +538,8 @@ let cmdline_actions = @ f_opt "unprototyped" option_funprototyped @ f_opt "packed-structs" option_fpacked_structs @ f_opt "inline-asm" option_finline_asm +(* Code generation options *) + @ f_opt "tailcalls" option_ftailcalls @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) -- cgit From bda5ee25ac991c38f5541a234936f1f6e2226072 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 16 Nov 2014 18:39:43 +0100 Subject: Add flags to control individual optimization passes + flag -O0 for turning them off. --- backend/Tailcall.v | 3 +- backend/Tailcallproof.v | 10 ++--- driver/Clflags.ml | 3 ++ driver/Compiler.v | 98 +++++++++++++++++++++++++++++++++++++------------ driver/Compopts.v | 11 +++++- driver/Driver.ml | 41 +++++++++++++++------ extraction/extraction.v | 8 +++- 7 files changed, 128 insertions(+), 46 deletions(-) diff --git a/backend/Tailcall.v b/backend/Tailcall.v index 25da531c..db246fec 100644 --- a/backend/Tailcall.v +++ b/backend/Tailcall.v @@ -14,7 +14,6 @@ Require Import Coqlib. Require Import Maps. -Require Import Compopts. Require Import AST. Require Import Registers. Require Import Op. @@ -100,7 +99,7 @@ Definition transf_instr (f: function) (pc: node) (instr: instruction) := using a compilation option. *) Definition transf_function (f: function) : function := - if zeq f.(fn_stacksize) 0 && eliminate_tailcalls tt + if zeq f.(fn_stacksize) 0 then RTL.transf_function (transf_instr f) f else f. diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 1965b18e..cc4ff55e 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -13,7 +13,6 @@ (** Recognition of tail calls: correctness proof *) Require Import Coqlib. -Require Import Compopts. Require Import Maps. Require Import AST. Require Import Integers. @@ -183,11 +182,10 @@ Lemma transf_instr_lookup: exists i', (transf_function f).(fn_code)!pc = Some i' /\ transf_instr_spec f i i'. Proof. intros. unfold transf_function. - destruct (zeq (fn_stacksize f) 0). destruct (eliminate_tailcalls tt). + destruct (zeq (fn_stacksize f) 0). simpl. rewrite PTree.gmap. rewrite H. simpl. exists (transf_instr f pc i); split. auto. apply transf_instr_charact; auto. exists i; split. auto. constructor. - exists i; split. auto. constructor. Qed. (** * Semantic properties of the code transformation *) @@ -263,14 +261,14 @@ Lemma sig_preserved: forall f, funsig (transf_fundef f) = funsig f. Proof. destruct f; auto. simpl. unfold transf_function. - destruct (zeq (fn_stacksize f) 0 && eliminate_tailcalls tt); auto. + destruct (zeq (fn_stacksize f) 0); auto. Qed. Lemma stacksize_preserved: forall f, fn_stacksize (transf_function f) = fn_stacksize f. Proof. unfold transf_function. intros. - destruct (zeq (fn_stacksize f) 0 && eliminate_tailcalls tt); auto. + destruct (zeq (fn_stacksize f) 0); auto. Qed. Lemma find_function_translated: @@ -556,7 +554,7 @@ Proof. assert (fn_stacksize (transf_function f) = fn_stacksize f /\ fn_entrypoint (transf_function f) = fn_entrypoint f /\ fn_params (transf_function f) = fn_params f). - unfold transf_function. destruct (zeq (fn_stacksize f) 0 && eliminate_tailcalls tt); auto. + unfold transf_function. destruct (zeq (fn_stacksize f) 0); auto. destruct H0 as [EQ1 [EQ2 EQ3]]. left. econstructor; split. simpl. eapply exec_function_internal; eauto. rewrite EQ1; eauto. diff --git a/driver/Clflags.ml b/driver/Clflags.ml index c6217ba1..ead27b36 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -24,6 +24,9 @@ let option_fpacked_structs = ref false let option_ffpu = ref true let option_ffloatconstprop = ref 2 let option_ftailcalls = ref true +let option_fconstprop = ref true +let option_fcse = ref true +let option_fredundancy = ref true let option_falignfunctions = ref (None: int option) let option_falignbranchtargets = ref 0 let option_faligncondbranchs = ref 0 diff --git a/driver/Compiler.v b/driver/Compiler.v index ae54f487..fb813c7c 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -71,6 +71,8 @@ Require Linearizeproof. Require CleanupLabelsproof. Require Stackingproof. Require Asmgenproof. +(** Command-line flags. *) +Require Import Compopts. (** Pretty-printers (defined in Caml). *) Parameter print_Clight: Clight.program -> unit. @@ -103,6 +105,14 @@ Definition print {A: Type} (printer: A -> unit) (prog: A) : A := Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. +Definition total_if {A: Type} + (flag: unit -> bool) (f: A -> A) (prog: A) : A := + if flag tt then f prog else prog. + +Definition partial_if {A: Type} + (flag: unit -> bool) (f: A -> res A) (prog: A) : res A := + if flag tt then f prog else OK prog. + (** We define three translation functions for whole programs: one starting with a C program, one with a Cminor program, one with an RTL program. The three translations produce Asm programs ready for @@ -111,24 +121,24 @@ Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. Definition transf_rtl_program (f: RTL.program) : res Asm.program := OK f @@ print (print_RTL 0) - @@ time "Tail calls" Tailcall.transf_program + @@ total_if Compopts.optim_tailcalls (time "Tail calls" Tailcall.transf_program) @@ print (print_RTL 1) @@@ time "Inlining" Inlining.transf_program @@ print (print_RTL 2) @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 3) - @@ time "Constant propagation" Constprop.transf_program + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 4) - @@ time "Renumbering" Renumber.transf_program + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 5) - @@@ time "CSE" CSE.transf_program + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 6) - @@@ time "Dead code" Deadcode.transf_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 7) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program - @@@ Linearize.transf_program + @@@ time "CFG linearization" Linearize.transf_program @@ time "Label cleanup" CleanupLabels.transf_program @@@ time "Mach generation" Stacking.transf_program @@ print print_Mach @@ -175,6 +185,33 @@ Proof. intros. destruct x; simpl. rewrite print_identity. auto. auto. Qed. +Remark forward_simulation_identity: + forall sem, forward_simulation sem sem. +Proof. + intros. apply forward_simulation_step with (fun s1 s2 => s2 = s1); intros. +- auto. +- exists s1; auto. +- subst s2; auto. +- subst s2. exists s1'; auto. +Qed. + +Lemma total_if_simulation: + forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (f: A -> A) (prog: A), + (forall p, forward_simulation (sem p) (sem (f p))) -> + forward_simulation (sem prog) (sem (total_if flag f prog)). +Proof. + intros. unfold total_if. destruct (flag tt). auto. apply forward_simulation_identity. +Qed. + +Lemma partial_if_simulation: + forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (f: A -> res A) (prog tprog: A), + partial_if flag f prog = OK tprog -> + (forall p tp, f p = OK tp -> forward_simulation (sem p) (sem tp)) -> + forward_simulation (sem prog) (sem tprog). +Proof. + intros. unfold partial_if in *. destruct (flag tt). eauto. inv H. apply forward_simulation_identity. +Qed. + (** * Semantic preservation *) (** We prove that the [transf_program] translations preserve semantics @@ -200,31 +237,44 @@ Proof. unfold transf_rtl_program, time in H. repeat rewrite compose_print_identity in H. simpl in H. - set (p1 := Tailcall.transf_program p) in *. + set (p1 := total_if optim_tailcalls Tailcall.transf_program p) in *. destruct (Inlining.transf_program p1) as [p11|] eqn:?; simpl in H; try discriminate. set (p12 := Renumber.transf_program p11) in *. - set (p2 := Constprop.transf_program p12) in *. - set (p21 := Renumber.transf_program p2) in *. - destruct (CSE.transf_program p21) as [p3|] eqn:?; simpl in H; try discriminate. - destruct (Deadcode.transf_program p3) as [p31|] eqn:?; simpl in H; try discriminate. + set (p2 := total_if optim_constprop Constprop.transf_program p12) in *. + set (p21 := total_if optim_constprop Renumber.transf_program p2) in *. + destruct (partial_if optim_CSE CSE.transf_program p21) as [p3|] eqn:?; simpl in H; try discriminate. + destruct (partial_if optim_redundancy Deadcode.transf_program p3) as [p31|] eqn:?; simpl in H; try discriminate. destruct (Allocation.transf_program p31) as [p4|] eqn:?; simpl in H; try discriminate. set (p5 := Tunneling.tunnel_program p4) in *. destruct (Linearize.transf_program p5) as [p6|] eqn:?; simpl in H; try discriminate. set (p7 := CleanupLabels.transf_program p6) in *. destruct (Stacking.transf_program p7) as [p8|] eqn:?; simpl in H; try discriminate. - eapply compose_forward_simulation. apply Tailcallproof.transf_program_correct. - eapply compose_forward_simulation. apply Inliningproof.transf_program_correct. eassumption. - eapply compose_forward_simulation. apply Renumberproof.transf_program_correct. - eapply compose_forward_simulation. apply Constpropproof.transf_program_correct. - eapply compose_forward_simulation. apply Renumberproof.transf_program_correct. - eapply compose_forward_simulation. apply CSEproof.transf_program_correct. eassumption. - eapply compose_forward_simulation. apply Deadcodeproof.transf_program_correct. eassumption. - eapply compose_forward_simulation. apply Allocproof.transf_program_correct. eassumption. - eapply compose_forward_simulation. apply Tunnelingproof.transf_program_correct. - eapply compose_forward_simulation. apply Linearizeproof.transf_program_correct. eassumption. - eapply compose_forward_simulation. apply CleanupLabelsproof.transf_program_correct. - eapply compose_forward_simulation. apply Stackingproof.transf_program_correct. - eexact Asmgenproof.return_address_exists. eassumption. + apply compose_forward_simulation with (RTL.semantics p1). + apply total_if_simulation. apply Tailcallproof.transf_program_correct. + apply compose_forward_simulation with (RTL.semantics p11). + apply Inliningproof.transf_program_correct; auto. + apply compose_forward_simulation with (RTL.semantics p12). + apply Renumberproof.transf_program_correct. + apply compose_forward_simulation with (RTL.semantics p2). + apply total_if_simulation. apply Constpropproof.transf_program_correct. + apply compose_forward_simulation with (RTL.semantics p21). + apply total_if_simulation. apply Renumberproof.transf_program_correct. + apply compose_forward_simulation with (RTL.semantics p3). + eapply partial_if_simulation; eauto. apply CSEproof.transf_program_correct. + apply compose_forward_simulation with (RTL.semantics p31). + eapply partial_if_simulation; eauto. apply Deadcodeproof.transf_program_correct. + apply compose_forward_simulation with (LTL.semantics p4). + apply Allocproof.transf_program_correct; auto. + apply compose_forward_simulation with (LTL.semantics p5). + apply Tunnelingproof.transf_program_correct. + apply compose_forward_simulation with (Linear.semantics p6). + apply Linearizeproof.transf_program_correct; auto. + apply compose_forward_simulation with (Linear.semantics p7). + apply CleanupLabelsproof.transf_program_correct. + apply compose_forward_simulation with (Mach.semantics Asmgenproof0.return_address_offset p8). + apply Stackingproof.transf_program_correct. + exact Asmgenproof.return_address_exists. + auto. apply Asmgenproof.transf_program_correct; eauto. split. auto. apply forward_to_backward_simulation. auto. diff --git a/driver/Compopts.v b/driver/Compopts.v index 01109f52..d0c6686e 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -28,7 +28,16 @@ Parameter generate_float_constants: unit -> bool. Parameter va_strict: unit -> bool. (** Flag -ftailcalls. For tail call optimization. *) -Parameter eliminate_tailcalls: unit -> bool. +Parameter optim_tailcalls: unit -> bool. + +(** Flag -fconstprop. For constant propagation. *) +Parameter optim_constprop: unit -> bool. + +(** Flag -fcse. For common subexpression elimination. *) +Parameter optim_CSE: unit -> bool. + +(** Flag -fredundancy. For dead code elimination. *) +Parameter optim_redundancy: unit -> bool. (** Flag -fthumb. For the ARM back-end. *) Parameter thumb: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 602b01be..76509f41 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -393,15 +393,21 @@ Language support options (use -fno- to turn off -f) : -fnone Turn off all language support options above Debugging options: -g Generate debugging information -Code generation options: (use -fno- to turn off -f) : - -O Optimize for speed [on by default] - -Os Optimize for code size +Optimization options: (use -fno- to turn off -f) + -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 + -ftailcalls Optimize function calls in tail position [on] + -fconst-prop Perform global constant propagation [on] + -ffloat-const-prop Control constant propagation of floats + (=0: none, =1: limited, =2: full; default is full) + -fcse Perform common subexpression elimination [on] + -fredundancy Perform redundancy elimination [on] +Code generation options: (use -fno- to turn off -f) -ffpu Use FP registers for some integer operations [on] -fsmall-data Set maximal size for allocation in small data area -fsmall-const Set maximal size for allocation in small constant area - -ffloat-const-prop Control constant propagation of floats - (=0: none, =1: limited, =2: full; default is full) - -ftailcalls Optimize function calls in tail position [on] -falign-functions Set alignment (in bytes) of function entry points -falign-branch-targets Set alignment (in bytes) of branch targets -falign-cond-branches Set alignment (in bytes) of conditional branches @@ -442,6 +448,13 @@ let language_support_options = [ option_fpacked_structs; option_finline_asm ] +let optimization_options = [ + option_ftailcalls; option_fconstprop; option_fcse; option_fredundancy +] + +let set_all opts = List.iter (fun r -> r := true) opts +let unset_all opts = List.iter (fun r -> r := false) opts + let num_source_files = ref 0 let cmdline_actions = @@ -483,15 +496,15 @@ let cmdline_actions = Prefix "-Wp,", Self (fun s -> prepro_options := List.rev_append (explode_comma_option s) !prepro_options); (* Language support options -- more below *) - Exact "-fall", Self (fun _ -> - List.iter (fun r -> r := true) language_support_options); - Exact "-fnone", Self (fun _ -> - List.iter (fun r -> r := false) language_support_options); + Exact "-fall", Self (fun _ -> set_all language_support_options); + Exact "-fnone", Self (fun _ -> unset_all language_support_options); (* Debugging options *) Exact "-g", Self (fun s -> option_g := true; push_linker_arg s); (* Code generation options -- more below *) + Exact "-O0", Self (fun _ -> unset_all optimization_options); + Exact "-O", Self (fun _ -> set_all optimization_options); + _Regexp "-O[123]$", Self (fun _ -> set_all optimization_options); Exact "-Os", Set option_Osize; - Exact "-O", Unset option_Osize; Exact "-fsmall-data", Integer(fun n -> option_small_data := n); Exact "-fsmall-const", Integer(fun n -> option_small_const := n); Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); @@ -538,8 +551,12 @@ let cmdline_actions = @ f_opt "unprototyped" option_funprototyped @ f_opt "packed-structs" option_fpacked_structs @ f_opt "inline-asm" option_finline_asm -(* Code generation options *) +(* Optimization options *) @ f_opt "tailcalls" option_ftailcalls + @ f_opt "const-prop" option_fconstprop + @ f_opt "cse" option_fcse + @ f_opt "redundancy" option_fredundancy +(* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) diff --git a/extraction/extraction.v b/extraction/extraction.v index 5b71a150..ee496ffa 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -92,8 +92,14 @@ Extract Constant Compopts.propagate_float_constants => "fun _ -> !Clflags.option_ffloatconstprop >= 1". Extract Constant Compopts.generate_float_constants => "fun _ -> !Clflags.option_ffloatconstprop >= 2". -Extract Constant Compopts.eliminate_tailcalls => +Extract Constant Compopts.optim_tailcalls => "fun _ -> !Clflags.option_ftailcalls". +Extract Constant Compopts.optim_constprop => + "fun _ -> !Clflags.option_fconstprop". +Extract Constant Compopts.optim_CSE => + "fun _ -> !Clflags.option_fcse". +Extract Constant Compopts.optim_redundancy => + "fun _ -> !Clflags.option_fredundancy". Extract Constant Compopts.thumb => "fun _ -> !Clflags.option_mthumb". -- cgit