Prove exec_body_dont_move_PC

Modify Asmblock.preg to combine iregsp and freg into dreg (dreg might be
a misnomer since not all iregs are data regs)
TODO: Adjust names of PArithP, PArithPP and the like

1 files changed, 5 insertions, 5 deletions

diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index e1a38c45..4e81a936 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -30,19 +30,19 @@ Module Asmblock_TRANSF.
 
 Definition ireg_of_preg (p : Asmblock.preg) : res ireg :=
   match p with
-  | IR (RR1 r) => OK r
+  | DR (IR' (RR1 r)) => OK r
   | _ => Error (msg "Asmgen.ireg_of_preg")
   end.
 
 Definition freg_of_preg (p : Asmblock.preg) : res freg :=
   match p with
-  | FR r => OK r
+  | DR (FR' r) => OK r
   | _ => Error (msg "Asmgen.freg_of_preg")
   end.
 
 Definition iregsp_of_preg (p : Asmblock.preg) : res iregsp :=
   match p with
-  | 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', IR r2' => do rd' <- freg_of_preg rd;
+      | FR' r1', IR' 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)