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/Asmgenproof1.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'powerpc/Asmgenproof1.v') 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