Revert "Modified the hook for the oracle"

This reverts commit 04a46f516487557df00f43453c8decbc8567c458.

It was actually not needed

3 files changed, 8 insertions, 12 deletions

diff --git a/backend/Duplicate.v b/backend/Duplicate.v
index 18869f39..82c17367 100644
--- a/backend/Duplicate.v
+++ b/backend/Duplicate.v
@@ -1,6 +1,5 @@
 (** RTL node duplication using external oracle. Used to form superblock
-  structures. Also swaps the ifso and ifnot of the Icond based on the
-  traces identified by the oracle *)
+  structures *)
 
 Require Import AST RTL Maps Globalenvs.
 Require Import Coqlib Errors Op.
@@ -8,10 +7,9 @@ Require Import Coqlib Errors Op.
 Local Open Scope error_monad_scope.
 Local Open Scope positive_scope.
 
-(** External oracle returning the new RTL code,
-    along with the new entrypoint, a mapping of new nodes to old nodes,
-    and a list of nodes to invert the condition on *)
-Axiom duplicate_aux: function -> code * node * (PTree.t node) * (list node).
+(** External oracle returning the new RTL code (entry point unchanged),
+    along with the new entrypoint, and a mapping of new nodes to old nodes *)
+Axiom duplicate_aux: function -> code * node * (PTree.t node).
 
 Extract Constant duplicate_aux => "Duplicateaux.duplicate_aux".
 
@@ -192,8 +190,7 @@ Definition verify_mapping dupmap (f f': function) : res unit :=
 (** * Entry points *)
 
 Definition transf_function (f: function) : res function :=
-  let (tctedupmap, invertlist) := duplicate_aux f in
-  let (tcte, dupmap) := tctedupmap in
+  let (tcte, dupmap) := duplicate_aux f in
   let (tc, te) := tcte in
   let f' := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in
   do u <- verify_mapping dupmap f f';
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 38b3ee23..f86cf39b 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -541,4 +541,4 @@ let duplicate_aux f =
   let traces = select_traces (to_ttl_code code entrypoint) entrypoint in
   let preds = get_predecessors_rtl code in
   let (new_code, pTreeId) = (print_traces traces; superblockify_traces code preds traces) in
-  (((new_code, (fn_entrypoint f)), pTreeId), [])
+  ((new_code, (fn_entrypoint f)), pTreeId)
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index c285e4b3..a8e9b16b 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -79,8 +79,7 @@ Theorem transf_function_preserves:
   transf_function f = OK f' ->
      fn_sig f = fn_sig f' /\ fn_params f = fn_params f' /\ fn_stacksize f = fn_stacksize f'.
 Proof.
-  intros. unfold transf_function in H. destruct (duplicate_aux _) as (tctemp & invl). destruct tctemp as (tcte & mp). destruct tcte as (tc & te).
-  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.
 
@@ -235,7 +234,7 @@ Theorem transf_function_correct f f':
 Proof.
   unfold transf_function.
   intros TRANSF.
-  destruct (duplicate_aux _) as (tctemp & invl). destruct tctemp as (tcte & mp). destruct tcte as (tc & te).
+  destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te).
   monadInv TRANSF.
   unfold verify_mapping in EQ. monadInv EQ.
   exists mp; constructor 1; simpl; auto.