diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2020-02-12 16:47:03 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2020-02-12 16:47:03 +0100 |
commit | 117a26880e27ae7d8efcb26d194c5ded3be642d6 (patch) | |
tree | 6dbac778988ebc2b227d1317add359b723962a12 | |
parent | e882ee6daa01579bf717b43b55091c859ed75661 (diff) | |
download | compcert-kvx-117a26880e27ae7d8efcb26d194c5ded3be642d6.tar.gz compcert-kvx-117a26880e27ae7d8efcb26d194c5ded3be642d6.zip |
Added option -ftracelinearize which linearizes based on ifnot branches
-rw-r--r-- | backend/Duplicateaux.ml | 2 | ||||
-rw-r--r-- | backend/Linearizeaux.ml | 57 | ||||
-rw-r--r-- | driver/Clflags.ml | 1 | ||||
-rw-r--r-- | driver/Driver.ml | 3 |
4 files changed, 59 insertions, 4 deletions
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index c3340cca..d0b7129e 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -529,7 +529,7 @@ let tail_duplicate code preds ptree trace = in (new_code, new_ptree, !nb_duplicated) let superblockify_traces code preds traces = - let max_nb_duplicated = 2 (* FIXME - should be architecture dependent *) + let max_nb_duplicated = 1 (* FIXME - should be architecture dependent *) in let ptree = make_identity_ptree code in let rec f code ptree = function | [] -> (code, ptree, 0) diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index 902724e0..a6964233 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -1,4 +1,4 @@ -(* *********************************************************************) + (* *) (* The Compcert verified compiler *) (* *) @@ -12,7 +12,6 @@ open LTL open Maps -open Camlcoq (* Trivial enumeration, in decreasing order of PC *) @@ -29,6 +28,8 @@ let enumerate_aux f reach = (* More clever enumeration that flattens basic blocks *) +open Camlcoq + module IntSet = Set.Make(struct type t = int let compare = compare end) (* Determine join points: reachable nodes that have > 1 predecessor *) @@ -110,5 +111,55 @@ let flatten_blocks blks = (* Build the enumeration *) -let enumerate_aux f reach = +let enumerate_aux_flat f reach = flatten_blocks (basic_blocks f (join_points f)) + +(** + * Enumeration based on traces as identified by Duplicate.v + * + * The Duplicate phase heuristically identifies the most frequented paths. Each + * Icond is modified so that the preferred condition is a fallthrough (ifnot) + * rather than a branch (ifso). + * + * The enumeration below takes advantage of this - preferring to layout nodes + * following the fallthroughs of the Lcond branches + *) + +let get_some = function +| None -> failwith "Did not get some" +| Some thing -> thing + +exception EmptyList + +let rec last_element = function + | [] -> raise EmptyList + | e :: [] -> e + | e' :: e :: l -> last_element (e::l) + +let dfs code entrypoint = + let visited = ref (PTree.map (fun n i -> false) code) in + let rec dfs_list code = function + | [] -> [] + | node :: ln -> + let node_dfs = + if not (get_some @@ PTree.get node !visited) then begin + visited := PTree.set node true !visited; + match PTree.get node code with + | None -> failwith "No such node" + | Some bb -> [node] @ match (last_element bb) with + | Lop _ | Lload _ | Lgetstack _ | Lsetstack _ | Lstore _ | Lcall _ + | Lbuiltin _ -> assert false + | Ltailcall _ | Lreturn -> [] + | Lbranch n -> dfs_list code [n] + | Lcond (_, _, ifso, ifnot) -> dfs_list code [ifnot; ifso] + | Ljumptable(_, ln) -> dfs_list code ln + end + else [] + in node_dfs @ (dfs_list code ln) + in dfs_list code [entrypoint] + +let enumerate_aux_trace f reach = dfs f.fn_code f.fn_entrypoint + +let enumerate_aux f reach = + if !Clflags.option_ftracelinearize then enumerate_aux_trace f reach + else enumerate_aux_flat f reach 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 |