Stubs for Duplicate pass

3 files changed, 63 insertions, 0 deletions

diff --git a/backend/Duplicate.v b/backend/Duplicate.v
new file mode 100644
index 00000000..cb52ec04
--- /dev/null
+++ b/backend/Duplicate.v
@@ -0,0 +1,31 @@
+(** RTL node duplication using external oracle. Used to form superblock
+  structures *)
+
+Require Import AST RTL Maps.
+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).
+
+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 *)
+
+(** * 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.
+
+Definition transf_fundef (f: fundef) : res fundef :=
+  transf_partial_fundef transf_function f.
+
+Definition transf_program (p: program) : res program :=
+  transform_partial_program transf_fundef p.
\ No newline at end of file
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
new file mode 100644
index 00000000..8a57f364
--- /dev/null
+++ b/backend/Duplicateaux.ml
@@ -0,0 +1,3 @@
+open Maps
+
+let duplicate_aux f = (f, PTree.empty)
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
new file mode 100644
index 00000000..5cf6b368
--- /dev/null
+++ b/backend/Duplicateproof.v
@@ -0,0 +1,29 @@
+(** Correctness proof for code duplication *)
+Require Import AST Linking Errors.
+Require Import RTL Globalenvs Smallstep.
+Require Import Duplicate.
+
+Definition match_prog (p tp: program) :=
+  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
+
+Lemma transf_program_match:
+  forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
+Proof.
+  intros. eapply match_transform_partial_program_contextual; eauto.
+Qed.
+
+Section PRESERVATION.
+
+Variable prog: program.
+Variable tprog: program.
+Hypothesis TRANSL: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Theorem transf_program_correct:
+  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
+Proof.
+  (* TODO *)
+Admitted.
+
+End PRESERVATION.
\ No newline at end of file