diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2020-11-03 15:06:45 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2020-11-03 15:06:45 +0100 |
commit | 535a8f8706de231f1bd8a7f0243025d84906b03c (patch) | |
tree | 5a4def9024c63d318de6b716bab83523b983961a /backend | |
parent | e6612fdfd69037099037def2acba5df553c3b49a (diff) | |
download | compcert-kvx-535a8f8706de231f1bd8a7f0243025d84906b03c.tar.gz compcert-kvx-535a8f8706de231f1bd8a7f0243025d84906b03c.zip |
Loop Rotate with -flooprotate
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Duplicateaux.ml | 50 | ||||
-rw-r--r-- | backend/Duplicatepasses.v | 12 |
2 files changed, 61 insertions, 1 deletions
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index 2b13ab5d..fac0ba76 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -836,6 +836,56 @@ let unroll_inner_loops_body f code revmap = (!code', !revmap') end +let extract_upto_icond f code head = + let rec extract h = + let inst = get_some @@ PTree.get h code in + match inst with + | Icond _ -> [h] + | _ -> ( match rtl_successors inst with + | [n] -> h :: (extract n) + | _ -> failwith "Found a node with more than one successor??" + ) + in List.rev @@ extract head + +let rotate_inner_loop f code revmap iloop = + let header = extract_upto_icond f code iloop.head in + let limit = !Clflags.option_flooprotate in + if count_ignore_nops code header > limit then begin + debug "Loop Rotate: too many nodes to duplicate (%d > %d)" (List.length header) limit; + (code, revmap) + end else + let (code2, revmap2, dupheader, fwmap) = clone code revmap header in + let code' = ref code2 in + let head' = apply_map fwmap iloop.head in + begin + code' := change_pointers !code' iloop.head head' iloop.preds; + (!code', revmap2) + end + +let rotate_inner_loops f code revmap = + let is_loop_header = get_loop_headers code (f.fn_entrypoint) in + let inner_loops = get_inner_loops f code is_loop_header in + let code' = ref code in + let revmap' = ref revmap in + begin + print_inner_loops inner_loops; + List.iter (fun iloop -> + let (new_code, new_revmap) = rotate_inner_loop f !code' !revmap' iloop in + code' := new_code; revmap' := new_revmap + ) inner_loops; + (!code', !revmap') + end + +let loop_rotate f = + let entrypoint = f.fn_entrypoint in + let code = f.fn_code in + let revmap = make_identity_ptree code in + let (code, revmap) = + if !Clflags.option_flooprotate > 0 then + rotate_inner_loops f code revmap + else (code, revmap) in + ((code, entrypoint), revmap) + let static_predict f = let entrypoint = f.fn_entrypoint in let code = f.fn_code in diff --git a/backend/Duplicatepasses.v b/backend/Duplicatepasses.v index dc96f966..7e58eedf 100644 --- a/backend/Duplicatepasses.v +++ b/backend/Duplicatepasses.v @@ -45,4 +45,14 @@ End TailDuplicateOracle. Module Tailduplicateproof := DuplicateProof TailDuplicateOracle. -Module Tailduplicate := Tailduplicateproof.
\ No newline at end of file +Module Tailduplicate := Tailduplicateproof. + +(** Loop Rotate *) + +Module LoopRotateOracle <: DuplicateOracle. + Axiom duplicate_aux : function -> code * node * (PTree.t node). + Extract Constant duplicate_aux => "Duplicateaux.loop_rotate". +End LoopRotateOracle. + +Module Looprotateproof := DuplicateProof LoopRotateOracle. +Module Looprotate := Looprotateproof. |