From d5c0b4054c8490bda3b3d191724c58d5d4002e58 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 27 Mar 2019 11:27:07 +0100 Subject: Define macros with CompCert's version number (#284) As suggested in #282, it can be useful to #ifdef code depending on specific versions of CompCert. Assuming a version number of the form MM.mm , the following macros are predefined: __COMPCERT_MAJOR__=MM (the major version number) __COMPCERT_MINOR__=mm (the minor version number) __COMPCERT_VERSION__=MMmm (two decimal digits for the minor, e.g. 305 for version 3.5) We also define __COMPCERT_BUILDNR__ if the build number is not empty in file ./VERSION. Closes: #282 --- driver/Frontend.ml | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 88b47854..929d9fd7 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -11,21 +11,43 @@ (* *) (* *********************************************************************) +open Printf open Clflags open Commandline open Driveraux (* Common frontend functions between clightgen and ccomp *) +(* 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 *) + let predefined_macros = - [ + let macros = [ "-D__COMPCERT__"; + sprintf "-D__COMPCERT_MAJOR__=%d" v_major; + sprintf "-D__COMPCERT_MINOR__=%d" v_minor; + sprintf "-D__COMPCERT_VERSION__=%d" v_number; "-U__STDC_IEC_559_COMPLEX__"; "-D__STDC_NO_ATOMICS__"; "-D__STDC_NO_COMPLEX__"; "-D__STDC_NO_THREADS__"; "-D__STDC_NO_VLA__" - ] + ] in + if Version.buildnr = "" + then macros + else sprintf "-D__COMPCERT_BUILDNR__=%s" Version.buildnr :: macros (* From C to preprocessed C *) -- cgit From 47c86d46a329ee2c4c26a82b29edd40bb4b4c35c Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 6 May 2019 17:26:08 +0200 Subject: Check for alignment of command-line switches. Add a check for alignment on command-line switches `-falign-*`. The check is similar to the one for the alignment attribute and ensures that only powers of two can be specified. --- driver/Driver.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 8ab8557c..5f7d0b20 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -262,6 +262,10 @@ let num_input_files = ref 0 let cmdline_actions = let f_opt name ref = [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in + 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 [ (* Getting help *) Exact "-help", Unit print_usage_and_exit; @@ -297,9 +301,9 @@ let cmdline_actions = 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);] @ + 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);] @ (* Target processor options *) (if Configuration.arch = "arm" then if Configuration.model = "armv6" then -- cgit From b49feed2f88c0a6ae9cc2ca4b2982096f18a2112 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 6 May 2019 17:07:24 +0200 Subject: Expand the responsefiles earlier * Move the expansion of response files to module Commandline, during the initialization of `Commandline.argv`. This way we're sure it's done exactly once. * Make `Commandline.argv` a `string array` instead of a `string array ref`. We no longer need to update it after initialization! * Improve reporting of errors during expansion of response files. --- driver/Commandline.ml | 14 +++++++------- driver/Commandline.mli | 6 +++--- driver/Configuration.ml | 6 +++--- 3 files changed, 13 insertions(+), 13 deletions(-) (limited to 'driver') diff --git a/driver/Commandline.ml b/driver/Commandline.ml index 75ca1683..672ed834 100644 --- a/driver/Commandline.ml +++ b/driver/Commandline.ml @@ -16,7 +16,6 @@ (* Parsing of command-line flags and arguments *) open Printf -open Responsefile type pattern = | Exact of string @@ -114,14 +113,15 @@ let parse_array spec argv first last = end in parse first -let argv : string array ref = ref [||] +let argv = + try + Responsefile.expandargv Sys.argv + with Responsefile.Error msg | Sys_error msg -> + eprintf "Error while processing the command line: %s\n" msg; + exit 2 let parse_cmdline spec = - try - argv := expandargv Sys.argv; - parse_array spec !argv 1 (Array.length !argv - 1) - with Responsefile.Error s -> - raise (CmdError s) + parse_array spec argv 1 (Array.length argv - 1) let long_int_action key s = let ls = String.length s diff --git a/driver/Commandline.mli b/driver/Commandline.mli index e1b917f2..0f903af4 100644 --- a/driver/Commandline.mli +++ b/driver/Commandline.mli @@ -42,8 +42,8 @@ exception CmdError of string (** Raise by [parse_cmdline] when an error occured *) val parse_cmdline: (pattern * action) list -> unit -(** [parse_cmdline actions] parses the commandline and performs all [actions]. - Raises [CmdError] if an error occurred. +(** [parse_cmdline actions] parses the command line (after @-file expansion) + and performs all [actions]. Raises [CmdError] if an error occurred. *) val longopt_int: string -> (int -> unit) -> pattern * action @@ -51,5 +51,5 @@ val longopt_int: string -> (int -> unit) -> pattern * action options of the form [key=] and calls [fn] with the integer argument *) -val argv: string array ref +val argv: string array (** [argv] contains the complete command line after @-file expandsion *) diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 972fd295..68531701 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -13,11 +13,11 @@ open Printf let search_argv key = - let len = Array.length Sys.argv in + let len = Array.length Commandline.argv in let res: string option ref = ref None in for i = 1 to len - 2 do - if Sys.argv.(i) = key then - res := Some Sys.argv.(i + 1); + if Commandline.argv.(i) = key then + res := Some Commandline.argv.(i + 1); done; !res -- cgit From 1e821bc1f1fb7a6b73ff1468b8b34f61b78cf304 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 6 May 2019 18:54:31 +0200 Subject: Change to AbsInt version string. The AbsInt build number no longer contains "release", so it must be printed additionally. --- driver/CommonOptions.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml index 58dd4007..c151ecf2 100644 --- a/driver/CommonOptions.ml +++ b/driver/CommonOptions.ml @@ -14,9 +14,9 @@ open Clflags open Commandline (* The version string for [tool_name] *) -let version_string tool_name= +let version_string tool_name = if Version.buildnr <> "" && Version.tag <> "" then - Printf.sprintf "The CompCert %s, %s, Build: %s, Tag: %s\n" tool_name Version.version Version.buildnr Version.tag + Printf.sprintf "The CompCert %s, Release: %s, Build: %s, Tag: %s\n" tool_name Version.version Version.buildnr Version.tag else Printf.sprintf "The CompCert %s, version %s\n" tool_name Version.version -- cgit From 1eaf745c5e4e32784a8e919b1a82d4d725036214 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 10 May 2019 14:46:05 +0200 Subject: Added options -fcommon and -fno-common (#164) The option -fcommon controls whether uninitialized global variables are placed in the COMMON section. If the option is given in the negated form, -fno-common, variables are not placed in the COMMON section. They are placed in the same sections as gcc does. If the variables are not placed in the COMMON section merging of tentative definitions is inhibited and multiple definitions lead to a linker error, as it does for gcc. --- driver/Clflags.ml | 1 + driver/Driver.ml | 2 ++ 2 files changed, 3 insertions(+) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index a886ee9b..fc12863d 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -31,6 +31,7 @@ let option_falignfunctions = ref (None: int option) let option_falignbranchtargets = ref 0 let option_faligncondbranchs = ref 0 let option_finline_asm = ref false +let option_fcommon = ref true let option_mthumb = ref (Configuration.model = "armv7m") let option_Osize = ref false let option_finline = ref true diff --git a/driver/Driver.ml b/driver/Driver.ml index 5f7d0b20..50f14d13 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -203,6 +203,7 @@ Code generation options: (use -fno- to turn off -f) -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 + -fcommon Put uninitialized globals in the common section [on]. |} ^ target_help ^ toolchain_help ^ @@ -304,6 +305,7 @@ let cmdline_actions = 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);] @ + f_opt "common" option_fcommon @ (* Target processor options *) (if Configuration.arch = "arm" then if Configuration.model = "armv6" then -- cgit From 66ee59d3dc8a861b468cfaf0ff46fc71dfb8fec2 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 May 2019 21:54:18 +0200 Subject: option -faddx (off by default until questions cleared) --- driver/Clflags.ml | 3 ++- driver/Compopts.v | 9 ++++++--- driver/Driver.ml | 3 ++- 3 files changed, 10 insertions(+), 5 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index b1afab6f..651d644e 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -70,4 +70,5 @@ let use_standard_headers = ref Configuration.has_standard_headers let option_fglobaladdrtmp = ref false let option_fglobaladdroffset = ref false let option_fxsaddr = ref true -let option_coalesce_mem = ref true +let option_faddx = ref false +let option_fcoalesce_mem = ref true diff --git a/driver/Compopts.v b/driver/Compopts.v index f7de596c..9c6448b7 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -43,17 +43,20 @@ Parameter optim_redundancy: unit -> bool. Parameter optim_postpass: unit -> bool. (** FIXME TEMPORARY Flag -fglobaladdrtmp. Use a temporary register for loading the address of global variables (default false) *) -Parameter optim_fglobaladdrtmp: unit -> bool. +Parameter optim_globaladdrtmp: unit -> bool. (** FIXME TEMPORARY Flag -fglobaladdroffset. Fold offsets into global addresses (default false) *) -Parameter optim_fglobaladdroffset: unit -> bool. +Parameter optim_globaladdroffset: unit -> bool. (** FIXME TEMPORARY Flag -fxsaddr. Use .xs addressing mode (default true) *) -Parameter optim_fxsaddr: unit -> bool. +Parameter optim_xsaddr: unit -> bool. (** FIXME TEMPORARY Flag -fcoaelesce-mem. Fuse (default true) *) Parameter optim_coalesce_mem: unit -> bool. +(** FIXME TEMPORARY Flag -faddx. Fuse (default false) *) +Parameter optim_addx: unit -> bool. + (** Flag -fthumb. For the ARM back-end. *) Parameter thumb: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index cfafcaa3..74e7ae77 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -375,7 +375,8 @@ let cmdline_actions = @ f_opt "globaladdrtmp" option_fglobaladdrtmp @ f_opt "globaladdroffset" option_fglobaladdroffset @ f_opt "xsaddr" option_fxsaddr - @ f_opt "coalesce-mem" option_coalesce_mem + @ f_opt "addx" option_faddx + @ f_opt "coalesce-mem" option_fcoalesce_mem (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) -- cgit From 8b0724fdb1af4f89a603f7bde4b5b625c870e111 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 31 May 2019 11:55:57 +0200 Subject: Fix misspellings in messages, man pages, and comments This is a manual, partial merge of Github pull request #296 by @Fourchaux. flocq/, cparser/MenhirLib/ and parts of test/ have not been changed because these are local copies and the fixes should be performed upstream. --- driver/Commandline.mli | 2 +- driver/Frontend.ml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'driver') diff --git a/driver/Commandline.mli b/driver/Commandline.mli index 0f903af4..8bb6f18f 100644 --- a/driver/Commandline.mli +++ b/driver/Commandline.mli @@ -39,7 +39,7 @@ type action = patterns are tried in the order in which they appear in the list. *) exception CmdError of string -(** Raise by [parse_cmdline] when an error occured *) +(** Raise by [parse_cmdline] when an error occurred *) val parse_cmdline: (pattern * action) list -> unit (** [parse_cmdline actions] parses the command line (after @-file expansion) diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 929d9fd7..36b5c354 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -131,7 +131,7 @@ let gnu_prepro_opt_key key s = let gnu_prepro_opt s = prepro_options := s::!prepro_options -(* Add gnu preprocessor option s and the implict -E *) +(* Add gnu preprocessor option s and the implicit -E *) let gnu_prepro_opt_e s = prepro_options := s :: !prepro_options; option_E := true @@ -171,7 +171,7 @@ let prepro_actions = [ @ (if Configuration.gnu_toolchain then gnu_prepro_actions else []) let gnu_prepro_help = -{| -M Ouput a rule suitable for make describing the +{| -M Output a rule suitable for make describing the dependencies of the main source file -MM Like -M but do not mention system header files -MF Specifies file as output file for -M or -MM -- cgit From 95938a8732b572d61955b1de8c49362c9e162640 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 31 May 2019 19:15:19 +0200 Subject: If-conversion optimization Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches. --- driver/Clflags.ml | 2 ++ driver/Driver.ml | 10 ++++++++-- 2 files changed, 10 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index fc12863d..d27871ef 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -27,6 +27,8 @@ let option_ftailcalls = ref true let option_fconstprop = ref true let option_fcse = ref true let option_fredundancy = ref true +let option_fifconversion = ref true +let option_ffavor_branchless = ref false let option_falignfunctions = ref (None: int option) let option_falignbranchtargets = ref 0 let option_faligncondbranchs = ref 0 diff --git a/driver/Driver.ml b/driver/Driver.ml index 50f14d13..84392ef6 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -196,6 +196,9 @@ Processing options: -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their single caller [on] + -fif-conversion Perform if-conversion (generation of conditional moves) [on] + -ffavor-branchless Favor the generation of branch-free instruction sequences, + even when possibly more costly than the default [off] 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 @@ -250,7 +253,8 @@ let dump_mnemonics destfile = exit 0 let optimization_options = [ - option_ftailcalls; option_fconstprop; option_fcse; option_fredundancy; option_finline_functions_called_once; + option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse; + option_fredundancy; option_finline_functions_called_once; ] let set_all opts () = List.iter (fun r -> r := true) opts @@ -301,7 +305,8 @@ let cmdline_actions = Exact "-Os", Set 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 "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); + Exact "-ffavor-branchless", Set option_ffavor_branchless; 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);] @ @@ -364,6 +369,7 @@ let cmdline_actions = (* Optimization options *) (* -f options: come in -f and -fno- variants *) @ f_opt "tailcalls" option_ftailcalls + @ f_opt "if-conversion" option_fifconversion @ f_opt "const-prop" option_fconstprop @ f_opt "cse" option_fcse @ f_opt "redundancy" option_fredundancy -- cgit From 8e3a73448c5ddfa4be3871d7f4fd80281a7549f4 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 31 May 2019 19:15:19 +0200 Subject: If-conversion optimization Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches. --- driver/Clflags.ml | 2 ++ driver/Driver.ml | 10 ++++++++-- 2 files changed, 10 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index fc12863d..d27871ef 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -27,6 +27,8 @@ let option_ftailcalls = ref true let option_fconstprop = ref true let option_fcse = ref true let option_fredundancy = ref true +let option_fifconversion = ref true +let option_ffavor_branchless = ref false let option_falignfunctions = ref (None: int option) let option_falignbranchtargets = ref 0 let option_faligncondbranchs = ref 0 diff --git a/driver/Driver.ml b/driver/Driver.ml index 50f14d13..84392ef6 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -196,6 +196,9 @@ Processing options: -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their single caller [on] + -fif-conversion Perform if-conversion (generation of conditional moves) [on] + -ffavor-branchless Favor the generation of branch-free instruction sequences, + even when possibly more costly than the default [off] 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 @@ -250,7 +253,8 @@ let dump_mnemonics destfile = exit 0 let optimization_options = [ - option_ftailcalls; option_fconstprop; option_fcse; option_fredundancy; option_finline_functions_called_once; + option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse; + option_fredundancy; option_finline_functions_called_once; ] let set_all opts () = List.iter (fun r -> r := true) opts @@ -301,7 +305,8 @@ let cmdline_actions = Exact "-Os", Set 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 "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); + Exact "-ffavor-branchless", Set option_ffavor_branchless; 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);] @ @@ -364,6 +369,7 @@ let cmdline_actions = (* Optimization options *) (* -f options: come in -f and -fno- variants *) @ f_opt "tailcalls" option_ftailcalls + @ f_opt "if-conversion" option_fifconversion @ f_opt "const-prop" option_fconstprop @ f_opt "cse" option_fcse @ f_opt "redundancy" option_fredundancy -- cgit From ea6807fdaeaa2e46e1c7471c91056fdc4736cc2f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 5 Jul 2019 15:38:45 +0200 Subject: Rename option `-ffavor-branchless` into `-Obranchless` Easier to type, and consistent with `-Os` (optimize for smaller code / optimize for fewer conditional branches). --- driver/Clflags.ml | 2 +- driver/Driver.ml | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index d27871ef..2db9399f 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -28,7 +28,7 @@ let option_fconstprop = ref true let option_fcse = ref true let option_fredundancy = ref true let option_fifconversion = ref true -let option_ffavor_branchless = ref false +let option_Obranchless = ref false let option_falignfunctions = ref (None: int option) let option_falignbranchtargets = ref 0 let option_faligncondbranchs = ref 0 diff --git a/driver/Driver.ml b/driver/Driver.ml index 84392ef6..88be8933 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -187,6 +187,8 @@ Processing options: -O0 Do not optimize the compiled code -O1 -O2 -O3 Synonymous for -O -Os Optimize for code size in preference to code speed + -Obranchless Optimize to avoid conditional branches; try to generate + branch-free instruction sequences as much as possible -ftailcalls Optimize function calls in tail position [on] -fconst-prop Perform global constant propagation [on] -ffloat-const-prop Control constant propagation of floats @@ -197,8 +199,6 @@ Processing options: -finline-functions-called-once Integrate functions only required by their single caller [on] -fif-conversion Perform if-conversion (generation of conditional moves) [on] - -ffavor-branchless Favor the generation of branch-free instruction sequences, - even when possibly more costly than the default [off] 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 @@ -303,10 +303,10 @@ let cmdline_actions = Exact "-O", Unit (set_all optimization_options); _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; + Exact "-Obranchless", Set option_Obranchless; 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 "-ffavor-branchless", Set option_ffavor_branchless; 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);] @ -- cgit From 467eb744ae2e7d913744c04866fa3e1a4558cdbe Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 5 Jul 2019 15:50:26 +0200 Subject: Update documentation of -Obranchless Updated man page + better usage message. --- driver/Driver.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 88be8933..bd2b4cee 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -187,7 +187,7 @@ Processing options: -O0 Do not optimize the compiled code -O1 -O2 -O3 Synonymous for -O -Os Optimize for code size in preference to code speed - -Obranchless Optimize to avoid conditional branches; try to generate + -Obranchless Optimize to generate fewer conditional branches; try to produce branch-free instruction sequences as much as possible -ftailcalls Optimize function calls in tail position [on] -fconst-prop Perform global constant propagation [on] -- cgit From 96383f6dbccd4b280acad395b9a2683a645a9de3 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 8 Jul 2019 10:48:24 +0200 Subject: Compatibility with OCaml 4.08 (#302) * Do not use `Pervasives.xxx` qualified names Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`, and uses of `Pervasives` cause fatal warnings. This commit uses unqualified names instead, as no ambiguity occurs. * Clarify "open" statements OCaml 4.08.0 has stricter warnings concerning open statements that shadow module names. Closes: #300 --- driver/Interp.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Interp.ml b/driver/Interp.ml index 6760e76c..a6841460 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -15,7 +15,7 @@ open Format open Camlcoq open AST -open Integers +open !Integers open Values open Memory open Globalenvs @@ -145,7 +145,7 @@ let print_state p (prog, ge, s) = let compare_mem m1 m2 = (* assumes nextblocks were already compared equal *) (* should permissions be taken into account? *) - Pervasives.compare m1.Mem.mem_contents m2.Mem.mem_contents + compare m1.Mem.mem_contents m2.Mem.mem_contents (* Comparing continuations *) -- cgit From 026d8bf506a0a4afebe4e41ad5ce2e7523c45ffc Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Tue, 9 Jul 2019 10:38:36 +0200 Subject: -O0 now implies -fno-inlining --- driver/Driver.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index bd2b4cee..be1252f9 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -254,7 +254,7 @@ let dump_mnemonics destfile = let optimization_options = [ option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse; - option_fredundancy; option_finline_functions_called_once; + option_fredundancy; option_finline; option_finline_functions_called_once; ] let set_all opts () = List.iter (fun r -> r := true) opts -- cgit From fb20aab431a768299118ed30822af59cab13325e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 2 Jul 2019 14:55:31 +0200 Subject: Remove the cparser/Builtins module Move its definitions to modules C (the type `builtins`) and Env (the operations that deal with the initial environment). Reasons for the refactoring: 1- The name "Builtins" will soon be reused for a Coq module 2- `Env.initial()` makes more sense than `Builtins.environment()`. --- driver/Frontend.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 36b5c354..bfb3542b 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -118,7 +118,7 @@ let init () = else Machine.rv32 | _ -> assert false end; - Builtins.set C2C.builtins; + Env.set_builtins C2C.builtins; Cutil.declare_attributes C2C.attributes; CPragmas.initialize() -- cgit From 31802695bf6673831674836817456142ab293e6b Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 17 Jul 2019 16:41:11 +0200 Subject: (#142) Desactivating scheduling when using -O1 optimization --- driver/Driver.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 404271cd..9748ebf6 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -185,7 +185,8 @@ Processing options: {|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 + -O1 Perform all optimization passes except scheduling + -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] @@ -308,6 +309,7 @@ let cmdline_actions = [ Exact "-O0", Unit (unset_all optimization_options); Exact "-O", Unit (set_all optimization_options); + _Regexp "-O1", Self (fun _ -> set_all optimization_options (); option_fpostpass := false); _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; Exact "-fsmall-data", Integer(fun n -> option_small_data := n); -- cgit From 4c379d48b35e7c8156f3953fede31d5e47faf8ca Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 19 Jul 2019 18:59:44 +0200 Subject: helpers broke compilation --- driver/Driver.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 05d51402..288bb436 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -258,11 +258,7 @@ let dump_mnemonics destfile = let optimization_options = [ option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse; -<<<<<<< HEAD option_fpostpass; option_fredundancy; option_finline_functions_called_once; -======= - option_fredundancy; option_finline; option_finline_functions_called_once; ->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf ] let set_all opts () = List.iter (fun r -> r := true) opts -- cgit From 7cdd676d002e33015b496f609538a9e86d77c543 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 8 Aug 2019 11:18:38 +0200 Subject: AArch64 port This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode. --- driver/Configuration.ml | 2 +- driver/Frontend.ml | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 68531701..2188acf0 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -123,7 +123,7 @@ let get_bool_config key = let arch = match get_config_string "arch" with - | "powerpc"|"arm"|"x86"|"riscV" as a -> a + | "powerpc"|"arm"|"x86"|"riscV"|"aarch64" as a -> a | v -> bad_config "arch" [v] let model = get_config_string "model" let abi = get_config_string "abi" diff --git a/driver/Frontend.ml b/driver/Frontend.ml index bfb3542b..74791247 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -116,6 +116,7 @@ let init () = | "riscV" -> if Configuration.model = "64" then Machine.rv64 else Machine.rv32 + | "aarch64" -> Machine.aarch64 | _ -> assert false end; Env.set_builtins C2C.builtins; -- cgit From 863b65cc49fb49ad203694cac36e3cbd4f45dab7 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 3 Sep 2019 17:34:02 +0200 Subject: Stubs for Duplicate pass --- driver/Compiler.v | 64 +++++++++++++++++++++++++++++++------------------------ 1 file changed, 36 insertions(+), 28 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 6d398327..49fa2e86 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -38,6 +38,7 @@ Require RTLgen. Require Tailcall. Require Inlining. Require Renumber. +Require Duplicate. Require Constprop. Require CSE. Require Deadcode. @@ -59,6 +60,7 @@ Require RTLgenproof. Require Tailcallproof. Require Inliningproof. Require Renumberproof. +Require Duplicateproof. Require Constpropproof. Require CSEproof. Require Deadcodeproof. @@ -126,16 +128,18 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 2) @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 3) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@@ time "Duplicating" Duplicate.transf_program @@ print (print_RTL 4) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 5) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 7) - @@@ time "Unused globals" Unusedglob.transform_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 8) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 9) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -238,6 +242,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog ::: mkpass Renumberproof.match_prog + ::: mkpass Duplicateproof.match_prog ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) @@ -281,17 +286,18 @@ Proof. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. set (p9 := Renumber.transf_program p8) in *. - set (p10 := total_if optim_constprop Constprop.transf_program p9) in *. - set (p11 := total_if optim_constprop Renumber.transf_program p10) in *. - destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. - destruct (partial_if optim_redundancy Deadcode.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. - destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. - destruct (Allocation.transf_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. - set (p16 := Tunneling.tunnel_program p15) in *. - destruct (Linearize.transf_program p16) as [p17|e] eqn:P17; simpl in T; try discriminate. - set (p18 := CleanupLabels.transf_program p17) in *. - destruct (partial_if debug Debugvar.transf_program p18) as [p19|e] eqn:P19; simpl in T; try discriminate. - destruct (Stacking.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. + set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. + destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. + destruct (partial_if optim_redundancy Deadcode.transf_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. + destruct (Unusedglob.transform_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. + destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. + set (p17 := Tunneling.tunnel_program p16) in *. + destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. + set (p19 := CleanupLabels.transf_program p18) in *. + destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -302,17 +308,18 @@ Proof. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. exists p9; split. apply Renumberproof.transf_program_match; auto. - exists p10; split. apply total_if_match. apply Constpropproof.transf_program_match. - exists p11; split. apply total_if_match. apply Renumberproof.transf_program_match. - exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. - exists p13; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. - exists p14; split. apply Unusedglobproof.transf_program_match; auto. - exists p15; split. apply Allocproof.transf_program_match; auto. - exists p16; split. apply Tunnelingproof.transf_program_match. - exists p17; split. apply Linearizeproof.transf_program_match; auto. - exists p18; split. apply CleanupLabelsproof.transf_program_match; auto. - exists p19; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. - exists p20; split. apply Stackingproof.transf_program_match; auto. + exists p10; split. apply Duplicateproof.transf_program_match; auto. + exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. + exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. + exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. + exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. + exists p15; split. apply Unusedglobproof.transf_program_match; auto. + exists p16; split. apply Allocproof.transf_program_match; auto. + exists p17; split. apply Tunnelingproof.transf_program_match. + exists p18; split. apply Linearizeproof.transf_program_match; auto. + exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. + exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. + exists p21; split. apply Stackingproof.transf_program_match; auto. exists tp; split. apply Asmgenproof.transf_program_match; auto. reflexivity. Qed. @@ -364,7 +371,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p21)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p22)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -383,6 +390,7 @@ Ltac DestructM := eapply compose_forward_simulations. eapply Inliningproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. eapply Duplicateproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. eapply compose_forward_simulations. -- cgit From 4392758d3e9032edb1ea4a899b92fef886749fca Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 9 Sep 2019 22:34:21 +0200 Subject: -fall-loads-nontrap --- driver/Clflags.ml | 1 + driver/Compiler.v | 13 +++++++++++-- driver/Compopts.v | 3 +++ driver/Driver.ml | 1 + 4 files changed, 16 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index cf1220d1..fd8227c9 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -75,3 +75,4 @@ let option_fglobaladdroffset = ref false let option_fxsaddr = ref true let option_faddx = ref false let option_fcoalesce_mem = ref true +let option_all_loads_nontrap = ref false diff --git a/driver/Compiler.v b/driver/Compiler.v index 6d398327..d006a7d1 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -42,6 +42,7 @@ Require Constprop. Require CSE. Require Deadcode. Require Unusedglob. +Require Allnontrap. Require Allocation. Require Tunneling. Require Linearize. @@ -63,6 +64,7 @@ Require Constpropproof. Require CSEproof. Require Deadcodeproof. Require Unusedglobproof. +Require Allnontrapproof. Require Allocproof. Require Tunnelingproof. Require Linearizeproof. @@ -136,6 +138,8 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 7) @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 8) + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@ print (print_RTL 9) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -243,6 +247,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass Unusedglobproof.match_prog + ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) ::: mkpass Allocproof.match_prog ::: mkpass Tunnelingproof.match_prog ::: mkpass Linearizeproof.match_prog @@ -286,7 +291,8 @@ Proof. destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. destruct (partial_if optim_redundancy Deadcode.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. - destruct (Allocation.transf_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. + set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. + destruct (Allocation.transf_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. set (p16 := Tunneling.tunnel_program p15) in *. destruct (Linearize.transf_program p16) as [p17|e] eqn:P17; simpl in T; try discriminate. set (p18 := CleanupLabels.transf_program p17) in *. @@ -307,6 +313,7 @@ Proof. exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. exists p14; split. apply Unusedglobproof.transf_program_match; auto. + exists p14bis; split. apply total_if_match. apply Allnontrapproof.transf_program_match. exists p15; split. apply Allocproof.transf_program_match; auto. exists p16; split. apply Tunnelingproof.transf_program_match. exists p17; split. apply Linearizeproof.transf_program_match; auto. @@ -364,7 +371,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p21)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p22)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -393,6 +400,8 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Unusedglobproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. eapply compose_forward_simulations. eapply Allocproof.transf_program_correct; eassumption. eapply compose_forward_simulations. diff --git a/driver/Compopts.v b/driver/Compopts.v index 9c6448b7..26d888ae 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -62,3 +62,6 @@ Parameter thumb: unit -> bool. (** Flag -g. For insertion of debugging information. *) Parameter debug: unit -> bool. + +(** Flag -fall-loads-nontrap. Turn user loads into non trapping. *) +Parameter all_loads_nontrap: unit -> bool. \ No newline at end of file diff --git a/driver/Driver.ml b/driver/Driver.ml index 288bb436..59b7b222 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -391,6 +391,7 @@ let cmdline_actions = @ f_opt "xsaddr" option_fxsaddr @ f_opt "addx" option_faddx @ f_opt "coalesce-mem" option_fcoalesce_mem + @ f_opt "all-loads-nontrap" option_all_loads_nontrap (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) -- cgit From a42baf15372e64f398685aaef079a82ea0db834e Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 18 Sep 2019 14:05:09 +0200 Subject: Timings for Machblockgen, Asmblockgen and postpass scheduling --- driver/Compiler.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 6d398327..c683c136 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -144,7 +144,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@@ partial_if Compopts.debug (time "Debugging info for local variables" Debugvar.transf_program) @@@ time "Mach generation" Stacking.transf_program @@ print print_Mach - @@@ time "Asm generation" Asmgen.transf_program. + @@@ time "Total Mach->Asm generation" Asmgen.transf_program. Definition transf_cminor_program (p: Cminor.program) : res Asm.program := OK p -- cgit From adc142066720798ca2e6f7709de6fba93559a336 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 20 Sep 2019 17:07:16 +0200 Subject: fix compiling --- driver/Compopts.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'driver') diff --git a/driver/Compopts.v b/driver/Compopts.v index 9c6448b7..4f86901b 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -62,3 +62,7 @@ Parameter thumb: unit -> bool. (** Flag -g. For insertion of debugging information. *) Parameter debug: unit -> bool. + +(* TODO is there a more appropriate place? *) +Require Import Coqlib. +Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. -- cgit From 4e0258fcb21aa0d23c04d4b58dbd4d34672234c1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 20 Sep 2019 20:39:43 +0200 Subject: to v3.6 --- driver/Compopts.v | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Compopts.v b/driver/Compopts.v index 26d888ae..6e3b0d62 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -64,4 +64,8 @@ Parameter thumb: unit -> bool. Parameter debug: unit -> bool. (** Flag -fall-loads-nontrap. Turn user loads into non trapping. *) -Parameter all_loads_nontrap: unit -> bool. \ No newline at end of file +Parameter all_loads_nontrap: unit -> bool. + +(* TODO is there a more appropriate place? *) +Require Import Coqlib. +Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. -- cgit From 553714035fc08f9b145b89b3dd7c455f06e917df Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 2 Dec 2019 21:39:20 +0100 Subject: finish merge --- driver/Compiler.v | 50 +++++++++++++++++++------------------------------- 1 file changed, 19 insertions(+), 31 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index f948d595..72db86e9 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -141,8 +141,9 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 8) @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program - @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 9) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 10) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -250,8 +251,8 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) - ::: mkpass Unusedglobproof.match_prog ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) + ::: mkpass Unusedglobproof.match_prog ::: mkpass Allocproof.match_prog ::: mkpass Tunnelingproof.match_prog ::: mkpass Linearizeproof.match_prog @@ -290,18 +291,19 @@ Proof. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. set (p9 := Renumber.transf_program p8) in *. - set (p10 := total_if optim_constprop Constprop.transf_program p9) in *. - set (p11 := total_if optim_constprop Renumber.transf_program p10) in *. - destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. - destruct (partial_if optim_redundancy Deadcode.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. - destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. + destruct (Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. + set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. + destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. + destruct (partial_if optim_redundancy Deadcode.transf_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. - destruct (Allocation.transf_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. - set (p16 := Tunneling.tunnel_program p15) in *. - destruct (Linearize.transf_program p16) as [p17|e] eqn:P17; simpl in T; try discriminate. - set (p18 := CleanupLabels.transf_program p17) in *. - destruct (partial_if debug Debugvar.transf_program p18) as [p19|e] eqn:P19; simpl in T; try discriminate. - destruct (Stacking.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. + destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. + set (p17 := Tunneling.tunnel_program p16) in *. + destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. + set (p19 := CleanupLabels.transf_program p18) in *. + destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -312,25 +314,12 @@ Proof. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. exists p9; split. apply Renumberproof.transf_program_match; auto. -<<<<<<< HEAD - exists p10; split. apply total_if_match. apply Constpropproof.transf_program_match. - exists p11; split. apply total_if_match. apply Renumberproof.transf_program_match. - exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. - exists p13; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. - exists p14; split. apply Unusedglobproof.transf_program_match; auto. - exists p14bis; split. apply total_if_match. apply Allnontrapproof.transf_program_match. - exists p15; split. apply Allocproof.transf_program_match; auto. - exists p16; split. apply Tunnelingproof.transf_program_match. - exists p17; split. apply Linearizeproof.transf_program_match; auto. - exists p18; split. apply CleanupLabelsproof.transf_program_match; auto. - exists p19; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. - exists p20; split. apply Stackingproof.transf_program_match; auto. -======= exists p10; split. apply Duplicateproof.transf_program_match; auto. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. + exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. exists p15; split. apply Unusedglobproof.transf_program_match; auto. exists p16; split. apply Allocproof.transf_program_match; auto. exists p17; split. apply Tunnelingproof.transf_program_match. @@ -338,7 +327,6 @@ Proof. exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. exists p21; split. apply Stackingproof.transf_program_match; auto. ->>>>>>> origin/mppa-work exists tp; split. apply Asmgenproof.transf_program_match; auto. reflexivity. Qed. @@ -390,7 +378,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p22)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p23)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -418,10 +406,10 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply Unusedglobproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. + eapply compose_forward_simulations. + eapply Unusedglobproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Allocproof.transf_program_correct; eassumption. eapply compose_forward_simulations. -- cgit From 2347476653201f154ffaea84f520e41cc0f32090 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Jan 2020 12:46:10 +0100 Subject: connect forward-moves to compiler --- driver/Clflags.ml | 3 ++- driver/Compiler.v | 19 ++++++++++++++----- driver/Compopts.v | 3 +++ driver/Driver.ml | 1 + 4 files changed, 20 insertions(+), 6 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index fd8227c9..9aa4a2bf 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -74,5 +74,6 @@ let option_fglobaladdrtmp = ref false let option_fglobaladdroffset = ref false let option_fxsaddr = ref true let option_faddx = ref false -let option_fcoalesce_mem = ref true +let option_fcoalesce_mem = ref true +let option_fforward_moves = ref true let option_all_loads_nontrap = ref false diff --git a/driver/Compiler.v b/driver/Compiler.v index 72db86e9..24964237 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -41,6 +41,7 @@ Require Renumber. Require Duplicate. Require Constprop. Require CSE. +Require ForwardMoves. Require Deadcode. Require Unusedglob. Require Allnontrap. @@ -64,6 +65,7 @@ Require Renumberproof. Require Duplicateproof. Require Constpropproof. Require CSEproof. +Require ForwardMovesproof. Require Deadcodeproof. Require Unusedglobproof. Require Allnontrapproof. @@ -138,12 +140,14 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 6) @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 7) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 8) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 9) - @@@ time "Unused globals" Unusedglob.transform_program + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program @@ print (print_RTL 10) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 11) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -250,6 +254,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) + ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) ::: mkpass Unusedglobproof.match_prog @@ -295,7 +300,8 @@ Proof. set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. - destruct (partial_if optim_redundancy Deadcode.transf_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. + set (p13bis := total_if optim_forward_moves ForwardMoves.transf_program p13) in *. + destruct (partial_if optim_redundancy Deadcode.transf_program p13bis) as [p14|e] eqn:P14; simpl in T; try discriminate. set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. @@ -318,6 +324,7 @@ Proof. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. + exists p13bis; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. exists p15; split. apply Unusedglobproof.transf_program_match; auto. @@ -378,7 +385,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p23)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p24)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -404,6 +411,8 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. eapply compose_forward_simulations. diff --git a/driver/Compopts.v b/driver/Compopts.v index 6e3b0d62..fdd2b1d6 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -66,6 +66,9 @@ Parameter debug: unit -> bool. (** Flag -fall-loads-nontrap. Turn user loads into non trapping. *) Parameter all_loads_nontrap: unit -> bool. +(** Flag -fforward-moves. Forward moves after CSE. *) +Parameter optim_forward_moves: unit -> bool. + (* TODO is there a more appropriate place? *) Require Import Coqlib. Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. diff --git a/driver/Driver.ml b/driver/Driver.ml index 59b7b222..eab66a2b 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -392,6 +392,7 @@ let cmdline_actions = @ f_opt "addx" option_faddx @ f_opt "coalesce-mem" option_fcoalesce_mem @ f_opt "all-loads-nontrap" option_all_loads_nontrap + @ f_opt "forward-moves" option_fforward_moves (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) -- cgit From fd2181ce5f6a3a5ba27349d1642ee4c59a6d9b34 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 17 Jan 2020 11:08:11 +0100 Subject: Added description for forward moves --- driver/Driver.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index eab66a2b..992cf8c4 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -199,6 +199,7 @@ Processing options: -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= Perform postpass scheduling with the specified optimization [list] (=list: list scheduling, =ilp: ILP, =greedy: just packing bundles) + -fforward-moves Forward moves after CSE -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their single caller [on] -- cgit From 893827f54addca2facc19a8f342b380d63114130 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 27 Jan 2020 11:43:00 +0100 Subject: Added a flag to desactivate tail duplication --- driver/Clflags.ml | 1 + driver/Compiler.v | 11 ++++++----- driver/Compopts.v | 4 ++++ driver/Driver.ml | 5 ++++- 4 files changed, 15 insertions(+), 6 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 9aa4a2bf..67ec9702 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -24,6 +24,7 @@ let option_fpacked_structs = ref false let option_ffpu = ref true let option_ffloatconstprop = ref 2 let option_ftailcalls = ref true +let option_fduplicate = ref true let option_fconstprop = ref true let option_fcse = ref true let option_fredundancy = ref true diff --git a/driver/Compiler.v b/driver/Compiler.v index 24964237..9f53a4fc 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -132,7 +132,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 2) @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 3) - @@@ time "Duplicating" Duplicate.transf_program + @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) @@ print (print_RTL 4) @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 5) @@ -250,7 +250,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog ::: mkpass Renumberproof.match_prog - ::: mkpass Duplicateproof.match_prog + ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) @@ -296,7 +296,7 @@ Proof. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. set (p9 := Renumber.transf_program p8) in *. - destruct (Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. @@ -320,7 +320,7 @@ Proof. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. exists p9; split. apply Renumberproof.transf_program_match; auto. - exists p10; split. apply Duplicateproof.transf_program_match; auto. + exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. @@ -404,7 +404,8 @@ Ltac DestructM := eapply compose_forward_simulations. eapply Inliningproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. eapply Duplicateproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. eapply compose_forward_simulations. diff --git a/driver/Compopts.v b/driver/Compopts.v index fdd2b1d6..a979c69b 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -27,6 +27,10 @@ Parameter generate_float_constants: unit -> bool. (** For value analysis. Currently always false. *) Parameter va_strict: unit -> bool. +(** Flag -fduplicate. For tail duplication optimization. Necessary to have + * bigger superblocks *) +Parameter optim_duplicate: unit -> bool. + (** Flag -ftailcalls. For tail call optimization. *) Parameter optim_tailcalls: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 992cf8c4..5d08dc6b 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -199,6 +199,7 @@ Processing options: -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= Perform postpass scheduling with the specified optimization [list] (=list: list scheduling, =ilp: ILP, =greedy: just packing bundles) + -fduplicate Perform tail duplication to form superblocks on predicted traces -fforward-moves Forward moves after CSE -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their @@ -260,6 +261,7 @@ let dump_mnemonics destfile = let optimization_options = [ option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse; option_fpostpass; option_fredundancy; option_finline_functions_called_once; + option_fduplicate ] let set_all opts () = List.iter (fun r -> r := true) opts @@ -310,7 +312,7 @@ let cmdline_actions = [ Exact "-O0", Unit (unset_all optimization_options); Exact "-O", Unit (set_all optimization_options); - _Regexp "-O1", Self (fun _ -> set_all optimization_options (); option_fpostpass := false); + _Regexp "-O1", Self (fun _ -> set_all optimization_options (); option_fpostpass := false; option_fduplicate := false); _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; Exact "-Obranchless", Set option_Obranchless; @@ -384,6 +386,7 @@ let cmdline_actions = @ f_opt "cse" option_fcse @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass + @ f_opt "duplicate" option_fduplicate @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once -- cgit From b54d18e2e26b3f7745870894d8087162eb33c545 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 27 Jan 2020 13:25:56 +0100 Subject: Tail duplication optimization defaulting to off --- driver/Clflags.ml | 2 +- driver/Driver.ml | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 67ec9702..088845fe 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -24,10 +24,10 @@ let option_fpacked_structs = ref false let option_ffpu = ref true let option_ffloatconstprop = ref 2 let option_ftailcalls = ref true -let option_fduplicate = ref true let option_fconstprop = ref true let option_fcse = ref true let option_fredundancy = ref true +let option_fduplicate = ref false let option_fpostpass = ref true let option_fpostpass_sched = ref "list" let option_fifconversion = ref true diff --git a/driver/Driver.ml b/driver/Driver.ml index 5d08dc6b..129248dc 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -261,7 +261,6 @@ let dump_mnemonics destfile = let optimization_options = [ option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse; option_fpostpass; option_fredundancy; option_finline_functions_called_once; - option_fduplicate ] let set_all opts () = List.iter (fun r -> r := true) opts -- cgit From 5412aea57eafe2868244a514471d480b83fc51bd Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jan 2020 13:59:55 +0100 Subject: connected (just a silly problem) --- driver/Clflags.ml | 1 + driver/Compiler.v | 36 ++++++++++++++++++++++++++++++++---- driver/Compopts.v | 3 +++ driver/Driver.ml | 7 +++++-- 4 files changed, 41 insertions(+), 6 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 2db9399f..b4ab51e7 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -26,6 +26,7 @@ let option_ffloatconstprop = ref 2 let option_ftailcalls = ref true let option_fconstprop = ref true let option_fcse = ref true +let option_fcse2 = ref true let option_fredundancy = ref true let option_fifconversion = ref true let option_Obranchless = ref false diff --git a/driver/Compiler.v b/driver/Compiler.v index 75247f71..33e31057 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -40,6 +40,7 @@ Require Inlining. Require Renumber. Require Constprop. Require CSE. +Require CSE2. Require Deadcode. Require Unusedglob. Require Allocation. @@ -61,6 +62,7 @@ Require Inliningproof. Require Renumberproof. Require Constpropproof. Require CSEproof. +Require CSE2proof. Require Deadcodeproof. Require Unusedglobproof. Require Allocproof. @@ -132,10 +134,12 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 5) @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 7) - @@@ time "Unused globals" Unusedglob.transform_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 8) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 9) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -241,6 +245,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) + ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass Unusedglobproof.match_prog ::: mkpass Allocproof.match_prog @@ -284,7 +289,27 @@ Proof. set (p10 := total_if optim_constprop Constprop.transf_program p9) in *. set (p11 := total_if optim_constprop Renumber.transf_program p10) in *. destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. - destruct (partial_if optim_redundancy Deadcode.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. + set (p12bis := @total_if RTL.program optim_CSE2 CSE2.transf_program p12). + change (@eq (res Asm.program) + (apply_partial Mach.program Asm.program + (apply_partial Linear.program Mach.program + (apply_partial Linear.program Linear.program + (apply_total Linear.program Linear.program + (apply_partial LTL.program Linear.program + (apply_total LTL.program LTL.program + (apply_partial RTL.program LTL.program + (apply_partial RTL.program RTL.program + (@partial_if RTL.program optim_redundancy + Deadcode.transf_program + p12bis) + Unusedglob.transform_program) + Allocation.transf_program) + Tunneling.tunnel_program) Linearize.transf_program) + CleanupLabels.transf_program) + (@partial_if Linear.program debug Debugvar.transf_program)) + Stacking.transf_program) Asmgen.transf_program) + (@OK Asm.program tp)) in T. + destruct (partial_if optim_redundancy Deadcode.transf_program p12bis) as [p13|e] eqn:P13; simpl in T; try discriminate. destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. destruct (Allocation.transf_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. set (p16 := Tunneling.tunnel_program p15) in *. @@ -305,6 +330,7 @@ Proof. exists p10; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p11; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. + exists p12bis; split. apply total_if_match. apply CSE2proof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. exists p14; split. apply Unusedglobproof.transf_program_match; auto. exists p15; split. apply Allocproof.transf_program_match; auto. @@ -364,7 +390,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p21)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p22)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -389,6 +415,8 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. eapply compose_forward_simulations. diff --git a/driver/Compopts.v b/driver/Compopts.v index 2a213350..594b74f1 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -36,6 +36,9 @@ Parameter optim_constprop: unit -> bool. (** Flag -fcse. For common subexpression elimination. *) Parameter optim_CSE: unit -> bool. +(** Flag -fcse2. For DMonniaux's common subexpression elimination. *) +Parameter optim_CSE2: unit -> bool. + (** Flag -fredundancy. For dead code elimination. *) Parameter optim_redundancy: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index be1252f9..bdf72250 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -194,6 +194,7 @@ Processing options: -ffloat-const-prop Control constant propagation of floats (=0: none, =1: limited, =2: full; default is full) -fcse Perform common subexpression elimination [on] + -fcse2 Perform inter-loop common subexpression elimination [on] -fredundancy Perform redundancy elimination [on] -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their @@ -253,8 +254,9 @@ let dump_mnemonics destfile = exit 0 let optimization_options = [ - option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse; - option_fredundancy; option_finline; option_finline_functions_called_once; + option_ftailcalls; option_fifconversion; option_fconstprop; + option_fcse; option_fcse2; + option_fredundancy; option_finline; option_finline_functions_called_once; ] let set_all opts () = List.iter (fun r -> r := true) opts @@ -372,6 +374,7 @@ let cmdline_actions = @ f_opt "if-conversion" option_fifconversion @ f_opt "const-prop" option_fconstprop @ f_opt "cse" option_fcse + @ f_opt "cse2" option_fcse2 @ f_opt "redundancy" option_fredundancy @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once -- cgit From 1f994be34eac3ca0d938c213c58a36b3a57bad8c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 28 Jan 2020 19:08:42 +0100 Subject: forgot a "in *" --- driver/Compiler.v | 21 +-------------------- 1 file changed, 1 insertion(+), 20 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 33e31057..0dd413f5 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -289,26 +289,7 @@ Proof. set (p10 := total_if optim_constprop Constprop.transf_program p9) in *. set (p11 := total_if optim_constprop Renumber.transf_program p10) in *. destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. - set (p12bis := @total_if RTL.program optim_CSE2 CSE2.transf_program p12). - change (@eq (res Asm.program) - (apply_partial Mach.program Asm.program - (apply_partial Linear.program Mach.program - (apply_partial Linear.program Linear.program - (apply_total Linear.program Linear.program - (apply_partial LTL.program Linear.program - (apply_total LTL.program LTL.program - (apply_partial RTL.program LTL.program - (apply_partial RTL.program RTL.program - (@partial_if RTL.program optim_redundancy - Deadcode.transf_program - p12bis) - Unusedglob.transform_program) - Allocation.transf_program) - Tunneling.tunnel_program) Linearize.transf_program) - CleanupLabels.transf_program) - (@partial_if Linear.program debug Debugvar.transf_program)) - Stacking.transf_program) Asmgen.transf_program) - (@OK Asm.program tp)) in T. + set (p12bis := @total_if RTL.program optim_CSE2 CSE2.transf_program p12) in *. destruct (partial_if optim_redundancy Deadcode.transf_program p12bis) as [p13|e] eqn:P13; simpl in T; try discriminate. destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. destruct (Allocation.transf_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. -- cgit From 7dca7590aa212806ee939244b253a6a067f34bfc Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 3 Feb 2020 10:52:53 +0100 Subject: Added flag to desactivate condition inversion --- driver/Clflags.ml | 1 + driver/Driver.ml | 3 +++ 2 files changed, 4 insertions(+) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 088845fe..a195e38b 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -28,6 +28,7 @@ let option_fconstprop = ref true let option_fcse = ref true let option_fredundancy = ref true let option_fduplicate = ref false +let option_finvertcond = ref true (* only active if option_fduplicate is also true *) let option_fpostpass = ref true let option_fpostpass_sched = ref "list" let option_fifconversion = ref true diff --git a/driver/Driver.ml b/driver/Driver.ml index 129248dc..3af1a937 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -200,6 +200,8 @@ Processing options: -fpostpass= Perform postpass scheduling with the specified optimization [list] (=list: list scheduling, =ilp: ILP, =greedy: just packing bundles) -fduplicate Perform tail duplication to form superblocks on predicted traces + -finvertcond Invert conditions based on predicted paths (to prefer fallthrough). + Requires -fduplicate to be also activated [on] -fforward-moves Forward moves after CSE -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their @@ -386,6 +388,7 @@ let cmdline_actions = @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass @ f_opt "duplicate" option_fduplicate + @ f_opt "invertcond" option_finvertcond @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once -- cgit From 117a26880e27ae7d8efcb26d194c5ded3be642d6 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 12 Feb 2020 16:47:03 +0100 Subject: Added option -ftracelinearize which linearizes based on ifnot branches --- driver/Clflags.ml | 1 + driver/Driver.ml | 3 +++ 2 files changed, 4 insertions(+) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index a195e38b..a4ebee9c 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -29,6 +29,7 @@ let option_fcse = ref true let option_fredundancy = ref true let option_fduplicate = ref false let option_finvertcond = ref true (* only active if option_fduplicate is also true *) +let option_ftracelinearize = ref false let option_fpostpass = ref true let option_fpostpass_sched = ref "list" let option_fifconversion = ref true diff --git a/driver/Driver.ml b/driver/Driver.ml index 3af1a937..70a3739b 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -202,6 +202,8 @@ Processing options: -fduplicate Perform tail duplication to form superblocks on predicted traces -finvertcond Invert conditions based on predicted paths (to prefer fallthrough). Requires -fduplicate to be also activated [on] + -ftracelinearize Linearizes based on the traces identified by duplicate phase + It is recommended to also activate -fduplicate with this pass [off] -fforward-moves Forward moves after CSE -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their @@ -389,6 +391,7 @@ let cmdline_actions = @ f_opt "postpass" option_fpostpass @ f_opt "duplicate" option_fduplicate @ f_opt "invertcond" option_finvertcond + @ f_opt "tracelinearize" option_ftracelinearize @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once -- cgit From be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 18 Feb 2020 16:57:17 +0100 Subject: Refine the type of function results in AST.signature Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions. --- driver/Interp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Interp.ml b/driver/Interp.ml index a6841460..3fae70e9 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -20,7 +20,7 @@ open Values open Memory open Globalenvs open Events -open Ctypes +open !Ctypes open Csyntax open Csem -- cgit From 3bffda879e214345635e575a696e8f184bef0e55 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 20 Feb 2020 09:41:16 +0100 Subject: Cosmetic: in OCaml code, write "open! Module" instead of "open !Module" "open!" is the form used in the examples in the OCaml manual. Based on a quick poll it seems to be the preferred form of the OCaml core dev team. --- driver/Interp.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Interp.ml b/driver/Interp.ml index 3fae70e9..d4286779 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -15,12 +15,12 @@ open Format open Camlcoq open AST -open !Integers +open! Integers open Values open Memory open Globalenvs open Events -open !Ctypes +open! Ctypes open Csyntax open Csem -- cgit From b016de5a1a8230b5a6c51d8e7cd8829d39a4c781 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 9 Mar 2020 15:16:08 +0100 Subject: [BROKEN] Replacing the boolean -fduplicate option by an integer To control the threshold for duplication --- driver/Clflags.ml | 4 ++-- driver/Compiler.v | 10 +++++----- driver/Driver.ml | 4 ++-- 3 files changed, 9 insertions(+), 9 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 6d6f1df4..79c0bce0 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -28,8 +28,8 @@ let option_fconstprop = ref true let option_fcse = ref true let option_fcse2 = ref true let option_fredundancy = ref true -let option_fduplicate = ref false -let option_finvertcond = ref true (* only active if option_fduplicate is also true *) +let option_fduplicate = ref 0 +let option_finvertcond = ref true let option_ftracelinearize = ref false let option_fpostpass = ref true let option_fpostpass_sched = ref "list" diff --git a/driver/Compiler.v b/driver/Compiler.v index 499feff2..da19a0b9 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -134,7 +134,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 2) @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 3) - @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) + @@@ time "Tail-duplicating" Duplicate.transf_program @@ print (print_RTL 4) @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 5) @@ -254,7 +254,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog ::: mkpass Renumberproof.match_prog - ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) + ::: mkpass Duplicateproof.match_prog ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) @@ -301,7 +301,7 @@ Proof. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. set (p9 := Renumber.transf_program p8) in *. - destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + destruct (Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. @@ -326,7 +326,7 @@ Proof. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. exists p9; split. apply Renumberproof.transf_program_match; auto. - exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. + exists p10; split. apply Duplicateproof.transf_program_match; auto. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. @@ -412,7 +412,7 @@ Ltac DestructM := eapply Inliningproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. + eapply Duplicateproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. eapply compose_forward_simulations. diff --git a/driver/Driver.ml b/driver/Driver.ml index db71aef9..dd357423 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -204,7 +204,7 @@ Processing options: -finvertcond Invert conditions based on predicted paths (to prefer fallthrough). Requires -fduplicate to be also activated [on] -ftracelinearize Linearizes based on the traces identified by duplicate phase - It is recommended to also activate -fduplicate with this pass [off] + It is heavily recommended to activate -finvertcond with this pass [off] -fforward-moves Forward moves after CSE -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their @@ -393,7 +393,7 @@ let cmdline_actions = @ f_opt "cse2" option_fcse2 @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass - @ f_opt "duplicate" option_fduplicate + @ [ Exact "-fduplicate", Integer (fun n -> option_fduplicate := n) ] @ f_opt "invertcond" option_finvertcond @ f_opt "tracelinearize" option_ftracelinearize @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched -- cgit From 103083dfcef7a71a57fd6c05af276db1f034ac75 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 10 Mar 2020 11:18:06 +0100 Subject: Fixing build --- driver/Driver.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index dd357423..43aedf50 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -318,7 +318,7 @@ let cmdline_actions = [ Exact "-O0", Unit (unset_all optimization_options); Exact "-O", Unit (set_all optimization_options); - _Regexp "-O1", Self (fun _ -> set_all optimization_options (); option_fpostpass := false; option_fduplicate := false); + _Regexp "-O1", Self (fun _ -> set_all optimization_options (); option_fpostpass := false); _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; Exact "-Obranchless", Set option_Obranchless; -- cgit From 192d5f379b3f1efa6f12b45af36f7cfea21d6d50 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 15 Mar 2020 00:00:33 +0100 Subject: more inlining --- driver/Clflags.ml | 1 + driver/Driver.ml | 2 ++ 2 files changed, 3 insertions(+) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 79c0bce0..ee5e9eeb 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -81,3 +81,4 @@ let option_faddx = ref false let option_fcoalesce_mem = ref true let option_fforward_moves = ref true let option_all_loads_nontrap = ref false +let option_inline_auto_threshold = ref 30 diff --git a/driver/Driver.ml b/driver/Driver.ml index 43aedf50..01451e07 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -190,6 +190,7 @@ Processing options: -Os Optimize for code size in preference to code speed -Obranchless Optimize to generate fewer conditional branches; try to produce branch-free instruction sequences as much as possible + -finline-auto-threshold n Inline functions under size n -ftailcalls Optimize function calls in tail position [on] -fconst-prop Perform global constant propagation [on] -ffloat-const-prop Control constant propagation of floats @@ -322,6 +323,7 @@ let cmdline_actions = _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; Exact "-Obranchless", Set option_Obranchless; + Exact "-finline-auto-threshold", Integer (fun n -> option_inline_auto_threshold := n); 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); -- cgit From d0326db1105704e02e2b40facc2a85a267a2b9b5 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 15 Mar 2020 09:18:02 +0100 Subject: by default do not inline much --- driver/Clflags.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index ee5e9eeb..8054eb5b 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -81,4 +81,4 @@ let option_faddx = ref false let option_fcoalesce_mem = ref true let option_fforward_moves = ref true let option_all_loads_nontrap = ref false -let option_inline_auto_threshold = ref 30 +let option_inline_auto_threshold = ref 0 -- cgit From fb43d1078c0b0824132b30d7dd9bfe6b0ac47122 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 17 Mar 2020 15:12:06 +0100 Subject: Desactivating branch predictions by default --- driver/Clflags.ml | 2 +- driver/Driver.ml | 6 +++++- 2 files changed, 6 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 8054eb5b..6986fb96 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -28,7 +28,7 @@ let option_fconstprop = ref true let option_fcse = ref true let option_fcse2 = ref true let option_fredundancy = ref true -let option_fduplicate = ref 0 +let option_fduplicate = ref (-1) let option_finvertcond = ref true let option_ftracelinearize = ref false let option_fpostpass = ref true diff --git a/driver/Driver.ml b/driver/Driver.ml index 01451e07..388482a0 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -201,7 +201,11 @@ Processing options: -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= Perform postpass scheduling with the specified optimization [list] (=list: list scheduling, =ilp: ILP, =greedy: just packing bundles) - -fduplicate Perform tail duplication to form superblocks on predicted traces + -fduplicate Perform tail duplication to form superblocks on predicted traces + nb_nodes control the heuristic deciding to duplicate or not + A value of -1 desactivates the entire pass (including branch prediction) + A value of 0 desactivates the duplication (but activates the branch prediction) + FIXME : this is desactivated by default for now -finvertcond Invert conditions based on predicted paths (to prefer fallthrough). Requires -fduplicate to be also activated [on] -ftracelinearize Linearizes based on the traces identified by duplicate phase -- cgit From 7ad6991534ba4ab10fe29d5456393f45cb4e5605 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 1 Apr 2020 10:35:42 +0200 Subject: -fduplicate -1 really desactivates the pass in Coq now --- driver/Compiler.v | 10 +++++----- driver/Compopts.v | 3 +-- 2 files changed, 6 insertions(+), 7 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index da19a0b9..499feff2 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -134,7 +134,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 2) @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 3) - @@@ time "Tail-duplicating" Duplicate.transf_program + @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) @@ print (print_RTL 4) @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 5) @@ -254,7 +254,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog ::: mkpass Renumberproof.match_prog - ::: mkpass Duplicateproof.match_prog + ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) @@ -301,7 +301,7 @@ Proof. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. set (p9 := Renumber.transf_program p8) in *. - destruct (Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. @@ -326,7 +326,7 @@ Proof. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. exists p9; split. apply Renumberproof.transf_program_match; auto. - exists p10; split. apply Duplicateproof.transf_program_match; auto. + exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. @@ -412,7 +412,7 @@ Ltac DestructM := eapply Inliningproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations. - eapply Duplicateproof.transf_program_correct; eassumption. + eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. eapply compose_forward_simulations. diff --git a/driver/Compopts.v b/driver/Compopts.v index b4b9f30d..848657e5 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -27,8 +27,7 @@ Parameter generate_float_constants: unit -> bool. (** For value analysis. Currently always false. *) Parameter va_strict: unit -> bool. -(** Flag -fduplicate. For tail duplication optimization. Necessary to have - * bigger superblocks *) +(** Flag -fduplicate. Branch prediction annotation + tail duplication *) Parameter optim_duplicate: unit -> bool. (** Flag -ftailcalls. For tail call optimization. *) -- cgit