transf_initial_states

3 files changed, 84 insertions, 12 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.
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 8a57f364..621a2dbe 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -1,3 +1,4 @@
+open RTL
 open Maps
 
-let duplicate_aux f = (f, PTree.empty)
+let duplicate_aux f = ((fn_code f), PTree.empty)
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index 264b7dff..b30c2c14 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -20,6 +20,31 @@ Hypothesis TRANSL: match_prog prog tprog.
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
 
+Lemma symbols_preserved:
+  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof (Genv.find_symbol_match TRANSL).
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match TRANSL).
+
+Lemma function_ptr_translated:
+  forall v f,
+  Genv.find_funct_ptr ge v = Some f ->
+  exists tf,
+  Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
+Proof (Genv.find_funct_ptr_transf_partial TRANSL).
+
+Lemma sig_preserved:
+  forall f tf,
+  transf_fundef f = OK tf ->
+  funsig tf = funsig f.
+Proof.
+  unfold transf_fundef, transf_partial_fundef; intros.
+  destruct f. monadInv H. simpl. symmetry; apply transf_function_preserves. assumption.
+  inv H. reflexivity.
+Qed.
+
 Inductive match_nodes (f: function): node -> node -> Prop :=
   | match_node_intro: forall n, match_nodes f n n
   | match_node_nop: forall n n' n1 n1',
@@ -84,7 +109,7 @@ Inductive match_states: state -> state -> Prop :=
   | match_states_intro:
     forall st f sp pc rs m st' f' pc'
       (STACKS: list_forall2 match_stackframes st st')
-      (TRANSL: transf_function f = OK f')
+      (TRANSF: transf_function f = OK f')
       (DUPLIC: match_nodes f pc pc'),
       match_states (State st f sp pc rs m) (State st' f' sp pc' rs m)
   | match_states_call:
@@ -97,10 +122,47 @@ Inductive match_states: state -> state -> Prop :=
       (STACKS: list_forall2 match_stackframes st st'),
       match_states (Returnstate st v m) (Returnstate st' v m).
 
-Theorem transf_program_correct:
-  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
+Theorem transf_initial_states:
+  forall s1, initial_state prog s1 ->
+  exists s2, initial_state tprog s2 /\ match_states s1 s2.
+Proof.
+  intros. inv H.
+  exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF).
+  eexists. split.
+  - econstructor.
+    + eapply (Genv.init_mem_transf_partial TRANSL); eauto.
+    + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto.
+      symmetry. eapply match_program_main. eauto.
+    + exploit function_ptr_translated; eauto.
+    + destruct f.
+      * monadInv TRANSF. rewrite <- H3. symmetry; eapply transf_function_preserves. assumption.
+      * monadInv TRANSF. assumption.
+  - constructor; eauto. constructor.
+Qed.
+
+Theorem transf_final_states:
+  forall s1 s2 r,
+  match_states s1 s2 -> final_state s1 r -> final_state s2 r.
+Proof.
+Admitted.
+
+Theorem step_simulation:
+  forall s1 t s1', step ge s1 t s1' ->
+  forall s2, match_states s1 s2 ->
+  exists s2',
+     step tge s2 t s2'
+  /\ match_states s1' s2'.
 Proof.
-  (* TODO *)
 Admitted.
 
+Theorem transf_program_correct:
+  forward_simulation (semantics prog) (semantics tprog).
+Proof.
+  eapply forward_simulation_step with match_states.
+  - eapply senv_preserved.
+  - eapply transf_initial_states.
+  - eapply transf_final_states.
+  - eapply step_simulation.
+Qed.
+
 End PRESERVATION.