From 903ed0cfa5cb91d99ee373fc8cf408c0a80f968a Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 23 Jan 2020 17:12:48 +0100 Subject: Revert "Modified the hook for the oracle" This reverts commit 04a46f516487557df00f43453c8decbc8567c458. It was actually not needed --- backend/Duplicate.v | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) (limited to 'backend/Duplicate.v') 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'; -- cgit