Modified the hook for the oracle

3 files changed, 12 insertions, 8 deletions

diff --git a/backend/Duplicate.v b/backend/Duplicate.v
index 46f0855d..c53ff425 100644
--- a/backend/Duplicate.v
+++ b/backend/Duplicate.v
@@ -1,5 +1,6 @@
 (** RTL node duplication using external oracle. Used to form superblock
-  structures *)
+  structures. Also swaps the ifso and ifnot of the Icond based on the
+  traces identified by the oracle *)
 
 Require Import AST RTL Maps Globalenvs.
 Require Import Coqlib Errors Op.
@@ -7,9 +8,10 @@ Require Import Coqlib Errors Op.
 Local Open Scope error_monad_scope.
 Local Open Scope positive_scope.
 
-(** 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).
+(** 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).
 
 Extract Constant duplicate_aux => "Duplicateaux.duplicate_aux".
 
@@ -187,7 +189,8 @@ Definition verify_mapping dupmap (f f': function) : res unit :=
 (** * Entry points *)
 
 Definition transf_function (f: function) : res function :=
-  let (tcte, dupmap) := duplicate_aux f in
+  let (tctedupmap, invertlist) := duplicate_aux f in
+  let (tcte, dupmap) := tctedupmap 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 f86cf39b..38b3ee23 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 ebb17774..67d16580 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -76,7 +76,8 @@ 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 (tcte & mp). destruct tcte as (tc & te). monadInv H.
+  intros. unfold transf_function in H. destruct (duplicate_aux _) as (tctemp & invl). destruct tctemp as (tcte & mp). destruct tcte as (tc & te).
+  monadInv H.
   repeat (split; try reflexivity).
 Qed.
 
@@ -227,7 +228,7 @@ Theorem transf_function_correct f f':
 Proof.
   unfold transf_function.
   intros TRANSF.
-  destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te).
+  destruct (duplicate_aux _) as (tctemp & invl). destruct tctemp as (tcte & mp). destruct tcte as (tc & te).
   monadInv TRANSF.
   unfold verify_mapping in EQ. monadInv EQ.
   exists mp; constructor 1; simpl; auto.