diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2020-01-24 13:32:28 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2020-01-24 13:32:28 +0100 |
commit | d69de4bcef55cb9c35acba1cc01b0b198a15008e (patch) | |
tree | 00bb0e23c8b2178762053c7378a21bd0c49d6ccc | |
parent | 903ed0cfa5cb91d99ee373fc8cf408c0a80f968a (diff) | |
download | compcert-kvx-d69de4bcef55cb9c35acba1cc01b0b198a15008e.tar.gz compcert-kvx-d69de4bcef55cb9c35acba1cc01b0b198a15008e.zip |
Oracle inverting branches when trace does not go in fallthru
-rw-r--r-- | backend/Duplicateaux.ml | 23 |
1 files changed, 21 insertions, 2 deletions
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index f86cf39b..a974133e 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -534,11 +534,30 @@ let superblockify_traces code preds traces = in f new_code new_ptree traces in f code ptree traces +let rec invert_iconds_trace code = function + | [] -> code + | n::[] -> code + | n :: n' :: t -> + let code' = match ptree_get_some n code with + | Icond (c, lr, ifso, ifnot) -> + assert (n' == ifso || n' == ifnot); + if (n' == ifso) then PTree.set n (Icond (Op.negate_condition c, lr, ifnot, ifso)) code + else code + | _ -> code + in invert_iconds_trace code' (n'::t) + +let rec invert_iconds code = function + | [] -> code + | t :: ts -> + let code' = invert_iconds_trace code t + in invert_iconds code' ts + (* For now, identity function *) let duplicate_aux f = let entrypoint = fn_entrypoint f in let code = fn_code f in let traces = select_traces (to_ttl_code code entrypoint) entrypoint in - let preds = get_predecessors_rtl code in - let (new_code, pTreeId) = (print_traces traces; superblockify_traces code preds traces) in + let icond_code = invert_iconds code traces in + let preds = get_predecessors_rtl icond_code in + let (new_code, pTreeId) = (print_traces traces; superblockify_traces icond_code preds traces) in ((new_code, (fn_entrypoint f)), pTreeId) |