diff options
Diffstat (limited to 'backend/Duplicate.v')
| -rw-r--r-- | backend/Duplicate.v | 23 |
1 files changed, 16 insertions, 7 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index cb52ec04..ac67cfe1 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -6,23 +6,32 @@ Require Import Coqlib Errors. Local Open Scope error_monad_scope. -(** External oracle returning the new RTL function, along with a mapping - of new nodes to old nodes *) -Axiom duplicate_aux: RTL.function -> RTL.function * (PTree.t nat). +(** External oracle returning the new RTL code (entry point unchanged), + along with a mapping of new nodes to old nodes *) +Axiom duplicate_aux: RTL.function -> RTL.code * (PTree.t nat). Extract Constant duplicate_aux => "Duplicateaux.duplicate_aux". (** * Verification of node duplications *) (** Verifies that the mapping [mp] is giving correct information *) -Definition verify_mapping (f tf: function) (mp: PTree.t nat) : res unit := OK tt. (* TODO *) +Definition verify_mapping (f: function) (tc: code) (mp: PTree.t nat) : res unit := OK tt. (* TODO *) (** * Entry points *) Definition transf_function (f: function) : res function := - let (tf, mp) := duplicate_aux f in - do u <- verify_mapping f tf mp; - OK tf. + let (tc, mp) := duplicate_aux f in + do u <- verify_mapping f tc mp; + OK (mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc (fn_entrypoint f)). + +Theorem transf_function_preserves: + forall f tf, + transf_function f = OK tf -> + fn_sig f = fn_sig tf /\ fn_params f = fn_params tf /\ fn_stacksize f = fn_stacksize tf /\ fn_entrypoint f = fn_entrypoint tf. +Proof. + intros. unfold transf_function in H. destruct (duplicate_aux _) as (tc & mp). monadInv H. + repeat (split; try reflexivity). +Qed. Definition transf_fundef (f: fundef) : res fundef := transf_partial_fundef transf_function f. |