From 37ad0670e1dc02c47b4987c16602aadb462c44c2 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 23 Oct 2020 01:53:05 +0200 Subject: aarch64 compiles again (but ccomp generates incorrect assembly) --- aarch64/Asmgen.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'aarch64/Asmgen.v') diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 5dec10e9..af069929 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -28,19 +28,19 @@ Local Open Scope error_monad_scope. Module Asmblock_TRANSF. (* STUB *) -Definition ireg_of_preg (p : Asmblock.preg) : res ireg := +Definition ireg_of_preg (p : Asm.preg) : res ireg := match p with | DR (IR' (RR1 r)) => OK r | _ => Error (msg "Asmgen.ireg_of_preg") end. -Definition freg_of_preg (p : Asmblock.preg) : res freg := +Definition freg_of_preg (p : Asm.preg) : res freg := match p with | DR (FR' r) => OK r | _ => Error (msg "Asmgen.freg_of_preg") end. -Definition iregsp_of_preg (p : Asmblock.preg) : res iregsp := +Definition iregsp_of_preg (p : Asm.preg) : res iregsp := match p with | DR (IR' r) => OK r | _ => Error (msg "Asmgen.iregsp_of_preg") @@ -61,7 +61,7 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction := OK (Asm.Pfmovimmd rd' f) | PArith (PArithPP (Pmovk sz n pos) rd rs) => - if (Asmblock.preg_eq rd rs) then ( + if (Asm.preg_eq rd rs) then ( do rd' <- ireg_of_preg rd; OK (Asm.Pmovk sz rd' n pos) ) else @@ -359,4 +359,4 @@ 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'; - Asmblock_TRANSF.transf_program abp. + Asmblock_TRANSF.transf_program abp. \ No newline at end of file -- cgit