diff options
| -rw-r--r-- | backend/Duplicate.v | 18 | ||||
| -rw-r--r-- | backend/Duplicateproof.v | 11 |
2 files changed, 25 insertions, 4 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index cb3936bb..a18892cd 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -5,6 +5,7 @@ Require Import AST RTL Maps Globalenvs. Require Import Coqlib Errors. 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 *) @@ -29,8 +30,19 @@ Definition fundef_RTL (fu: xfundef) : fundef := (** * Verification of node duplications *) -(** Verifies that the mapping [mp] is giving correct information *) -Definition verify_mapping (xf: xfunction) (tc: code) (tentry: node) : res unit := OK tt. (* TODO *) +Definition verify_mapping_entrypoint (f: function) (xf: xfunction) : res unit := + match ((fn_revmap xf)!(fn_entrypoint (fn_RTL xf))) with + | None => Error (msg "verify_mapping: No node in xf revmap for entrypoint") + | Some n => match (Pos.compare n (fn_entrypoint f)) with + | Eq => OK tt + | _ => Error (msg "verify_mapping_entrypoint: xf revmap for entrypoint does not correspond to the entrypoint of f") + end + end. + +(** Verifies that the [fn_revmap] of the translated function [xf] is giving correct information in regards to [f] *) +Definition verify_mapping (f: function) (xf: xfunction) : res unit := + do u <- verify_mapping_entrypoint f xf; OK tt. +(* TODO - verify the other axiom *) (** * Entry points *) @@ -38,7 +50,7 @@ Definition transf_function_aux (f: function) : res xfunction := let (tcte, mp) := duplicate_aux f in let (tc, te) := tcte in let xf := {| fn_RTL := (mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te); fn_revmap := mp |} in - do u <- verify_mapping xf tc te; + do u <- verify_mapping f xf; OK xf. Theorem transf_function_aux_preserves: diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index a368174f..fe26db55 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -3,6 +3,8 @@ Require Import AST Linking Errors Globalenvs Smallstep. Require Import Coqlib Maps Events Values. Require Import Op RTL Duplicate. +Local Open Scope positive_scope. + Definition match_prog (p tp: program) := match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. @@ -41,8 +43,15 @@ Axiom revmap_correct: forall f xf n n', (fn_revmap xf)!n' = Some n -> (forall i, (fn_code f)!n = Some i -> exists i', (fn_code (fn_RTL xf))!n' = Some i' /\ match_inst (fun n => (fn_revmap xf)!n) i i'). -Axiom revmap_entrypoint: +Theorem revmap_entrypoint: forall f xf, transf_function_aux f = OK xf -> (fn_revmap xf)!(fn_entrypoint (fn_RTL xf)) = Some (fn_entrypoint f). +Proof. + intros. unfold transf_function_aux in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). + monadInv H. simpl. monadInv EQ. unfold verify_mapping_entrypoint in EQ0. simpl in EQ0. + destruct (mp ! te) eqn:PT; try discriminate. + destruct (n ?= fn_entrypoint f) eqn:EQ; try discriminate. inv EQ0. + apply Pos.compare_eq in EQ. congruence. +Qed. Section PRESERVATION. |