Duplicate: big progress on step_simulation, only Ijumptbl left

1 files changed, 9 insertions, 10 deletions

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.