From f1637021cd51505796e878a21d1b30df0b42e236 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 17 Sep 2019 19:44:22 +0200 Subject: Model GPR0 in isel (#199) If the first argument to `isel` is GPR0, it reads as the constant 0. This cannot occur in code generated by CompCert, due to the fact that GPR0 is not available as register for register allocation. However the assembler semantics should be as close as possible to the actual hardware. --- powerpc/Asm.v | 2 +- powerpc/Asmgenproof1.v | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index b9300fd7..4fb38ff8 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -864,7 +864,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pisel rd r1 r2 bit => let v := match rs#(reg_of_crbit bit) with - | Vint n => if Int.eq n Int.zero then rs#r2 else rs#r1 + | Vint n => if Int.eq n Int.zero then rs#r2 else (gpr_or_zero rs r1) | _ => Vundef end in Next (nextinstr (rs #rd <- v #GPR0 <- Vundef)) m diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 884d5366..20cf9c1d 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1284,7 +1284,9 @@ Proof. reflexivity. + Simpl. rewrite <- (C r1), <- (C r2) by auto. - rewrite B. destruct dir; destruct ob as [[]|]; simpl; auto using Val.lessdef_normalize. + rewrite B, gpr_or_zero_not_zero. + destruct dir; destruct ob as [[]|]; simpl; auto using Val.lessdef_normalize. + destruct dir; intros e; subst; discriminate. + intros. Simpl. Qed. -- cgit