diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2020-01-23 17:12:48 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2020-01-23 17:12:48 +0100 |
commit | 903ed0cfa5cb91d99ee373fc8cf408c0a80f968a (patch) | |
tree | aa2c764c4269a42e4a947182f1a76c3585cc15d3 | |
parent | 1acafe8f7f61a8908f47de4c98f3d873f8f9afbd (diff) | |
download | compcert-kvx-903ed0cfa5cb91d99ee373fc8cf408c0a80f968a.tar.gz compcert-kvx-903ed0cfa5cb91d99ee373fc8cf408c0a80f968a.zip |
Revert "Modified the hook for the oracle"
This reverts commit 04a46f516487557df00f43453c8decbc8567c458.
It was actually not needed
-rw-r--r-- | backend/Duplicate.v | 13 | ||||
-rw-r--r-- | backend/Duplicateaux.ml | 2 | ||||
-rw-r--r-- | backend/Duplicateproof.v | 5 |
3 files changed, 8 insertions, 12 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 18869f39..82c17367 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -1,6 +1,5 @@ (** RTL node duplication using external oracle. Used to form superblock - structures. Also swaps the ifso and ifnot of the Icond based on the - traces identified by the oracle *) + structures *) Require Import AST RTL Maps Globalenvs. Require Import Coqlib Errors Op. @@ -8,10 +7,9 @@ Require Import Coqlib Errors Op. Local Open Scope error_monad_scope. Local Open Scope positive_scope. -(** External oracle returning the new RTL code, - along with the new entrypoint, a mapping of new nodes to old nodes, - and a list of nodes to invert the condition on *) -Axiom duplicate_aux: function -> code * node * (PTree.t node) * (list node). +(** External oracle returning the new RTL code (entry point unchanged), + along with the new entrypoint, and a mapping of new nodes to old nodes *) +Axiom duplicate_aux: function -> code * node * (PTree.t node). Extract Constant duplicate_aux => "Duplicateaux.duplicate_aux". @@ -192,8 +190,7 @@ Definition verify_mapping dupmap (f f': function) : res unit := (** * Entry points *) Definition transf_function (f: function) : res function := - let (tctedupmap, invertlist) := duplicate_aux f in - let (tcte, dupmap) := tctedupmap in + let (tcte, dupmap) := duplicate_aux f in let (tc, te) := tcte in let f' := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in do u <- verify_mapping dupmap f f'; diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index 38b3ee23..f86cf39b 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -541,4 +541,4 @@ let duplicate_aux f = 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 - (((new_code, (fn_entrypoint f)), pTreeId), []) + ((new_code, (fn_entrypoint f)), pTreeId) diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index c285e4b3..a8e9b16b 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -79,8 +79,7 @@ Theorem transf_function_preserves: transf_function f = OK f' -> fn_sig f = fn_sig f' /\ fn_params f = fn_params f' /\ fn_stacksize f = fn_stacksize f'. Proof. - intros. unfold transf_function in H. destruct (duplicate_aux _) as (tctemp & invl). destruct tctemp as (tcte & mp). destruct tcte as (tc & te). - monadInv H. + intros. unfold transf_function in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). monadInv H. repeat (split; try reflexivity). Qed. @@ -235,7 +234,7 @@ Theorem transf_function_correct f f': Proof. unfold transf_function. intros TRANSF. - destruct (duplicate_aux _) as (tctemp & invl). destruct tctemp as (tcte & mp). destruct tcte as (tc & te). + destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). monadInv TRANSF. unfold verify_mapping in EQ. monadInv EQ. exists mp; constructor 1; simpl; auto. |