Preparation for postpass in aarch64 and refactoring

1 files changed, 7 insertions, 6 deletions

diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index fcd12eef..fcc64956 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -17,7 +17,7 @@
 Require Import Recdef Coqlib Zwf Zbits.
 Require Import Errors AST Integers Floats Op.
 Require Import Locations Compopts.
-Require Import Mach Asm Asmblock Asmblockgen Machblockgen PseudoAsmblock PseudoAsmblockproof.
+Require Import Mach Asm Asmblock Asmblockgen Machblockgen PseudoAsmblock PseudoAsmblockproof PostpassScheduling.
 
 
 Local Open Scope error_monad_scope.
@@ -30,19 +30,19 @@ Module Asmblock_TRANSF.
 
 Definition ireg_of_preg (p : Asm.preg) : res ireg :=
   match p with
-  | DR (IR' (RR1 r)) => OK r
+  | DR (IR (RR1 r)) => OK r
   | _ => Error (msg "Asmgen.ireg_of_preg")
   end.
 
 Definition freg_of_preg (p : Asm.preg) : res freg :=
   match p with
-  | DR (FR' r) => OK r
+  | DR (FR r) => OK r
   | _ => Error (msg "Asmgen.freg_of_preg")
   end.
 
 Definition iregsp_of_preg (p : Asm.preg) : res iregsp :=
   match p with
-  | DR (IR' r) => OK r
+  | DR (IR r) => OK r
   | _ => Error (msg "Asmgen.iregsp_of_preg")
   end.
 
@@ -219,11 +219,11 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction :=
   | PArith (Pfmovi fsz rd r1) => OK (Asm.Pfmovi fsz rd r1)
   | PArith (Pcsel rd r1 r2 c) =>
       match r1, r2 with
-      | IR' r1', IR' r2' => do rd' <- ireg_of_preg rd;
+      | IR r1', IR r2' => do rd' <- ireg_of_preg rd;
                           do r1'' <- ireg_of_preg r1';
                           do r2'' <- ireg_of_preg r2';
                           OK (Asm.Pcsel rd' r1'' r2'' c)
-      | FR' r1', FR' r2' => do rd' <- freg_of_preg rd;
+      | FR r1', FR r2' => do rd' <- freg_of_preg rd;
                           do r1'' <- freg_of_preg r1';
                           do r2'' <- freg_of_preg r2';
                           OK (Asm.Pfsel rd' r1'' r2'' c)
@@ -359,4 +359,5 @@ Definition transf_program (p: Mach.program) : res Asm.program :=
   let mbp := Machblockgen.transf_program p in
   do mbp' <- PseudoAsmblockproof.transf_program mbp;
   do abp <- Asmblockgen.transf_program mbp';
+  (*do abp' <- (time "PostpassScheduling total oracle+verification" PostpassScheduling.transf_program) abp;*)
   Asmblock_TRANSF.transf_program abp.