From 10fc3a0544cce0dcc345b2d14d2c00a33d9bbe92 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 5 Sep 2019 18:34:47 +0200 Subject: Duplicate: big progress on step_simulation, only Ijumptbl left --- backend/Duplicate.v | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) (limited to 'backend/Duplicate.v') diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 8a78ee80..743d62e4 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -7,29 +7,30 @@ Require Import Coqlib Errors. Local Open Scope error_monad_scope. (** 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). + along with the new entrypoint, and a mapping of new nodes to old nodes *) +Axiom duplicate_aux: RTL.function -> RTL.code * node * (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: function) (tc: code) (mp: PTree.t nat) : res unit := OK tt. (* TODO *) +Definition verify_mapping (f: function) (tc: code) (tentry: node) (mp: PTree.t nat) : res unit := OK tt. (* TODO *) (** * Entry points *) Definition transf_function (f: function) : res function := - 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)). + let (tcte, mp) := duplicate_aux f in + let (tc, te) := tcte in + do u <- verify_mapping f tc te mp; + OK (mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te). 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. + fn_sig f = fn_sig tf /\ fn_params f = fn_params tf /\ fn_stacksize f = fn_stacksize tf. Proof. - intros. unfold transf_function in H. destruct (duplicate_aux _) as (tc & mp). 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. @@ -39,8 +40,6 @@ Remark transf_function_fnparams: forall f tf, transf_function f = OK tf -> fn_pa Proof. apply transf_function_preserves. Qed. Remark transf_function_fnstacksize: forall f tf, transf_function f = OK tf -> fn_stacksize f = fn_stacksize tf. Proof. apply transf_function_preserves. Qed. -Remark transf_function_fnentrypoint: forall f tf, transf_function f = OK tf -> fn_entrypoint f = fn_entrypoint tf. - Proof. apply transf_function_preserves. Qed. Definition transf_fundef (f: fundef) : res fundef := transf_partial_fundef transf_function f. -- cgit