diff options
-rw-r--r-- | backend/Duplicate.v | 13 | ||||
-rw-r--r-- | backend/Duplicateaux.ml | 2 | ||||
-rw-r--r-- | backend/Duplicateproof.v | 5 |
3 files changed, 12 insertions, 8 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 46f0855d..c53ff425 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -1,5 +1,6 @@ (** RTL node duplication using external oracle. Used to form superblock - structures *) + structures. Also swaps the ifso and ifnot of the Icond based on the + traces identified by the oracle *) Require Import AST RTL Maps Globalenvs. Require Import Coqlib Errors Op. @@ -7,9 +8,10 @@ Require Import Coqlib Errors Op. Local Open Scope error_monad_scope. Local Open Scope positive_scope. -(** 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). +(** 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). Extract Constant duplicate_aux => "Duplicateaux.duplicate_aux". @@ -187,7 +189,8 @@ Definition verify_mapping dupmap (f f': function) : res unit := (** * Entry points *) Definition transf_function (f: function) : res function := - let (tcte, dupmap) := duplicate_aux f in + let (tctedupmap, invertlist) := duplicate_aux f in + let (tcte, dupmap) := tctedupmap 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 f86cf39b..38b3ee23 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 ebb17774..67d16580 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -76,7 +76,8 @@ 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 (tcte & mp). destruct tcte as (tc & te). monadInv H. + intros. unfold transf_function in H. destruct (duplicate_aux _) as (tctemp & invl). destruct tctemp as (tcte & mp). destruct tcte as (tc & te). + monadInv H. repeat (split; try reflexivity). Qed. @@ -227,7 +228,7 @@ Theorem transf_function_correct f f': Proof. unfold transf_function. intros TRANSF. - destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). + destruct (duplicate_aux _) as (tctemp & invl). destruct tctemp as (tcte & mp). destruct tcte as (tc & te). monadInv TRANSF. unfold verify_mapping in EQ. monadInv EQ. exists mp; constructor 1; simpl; auto. |