From d002919334e83904447957f666f0d48704c5e55b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 13 Apr 2019 10:11:05 +0200 Subject: Emulate the "isel" instruction on non-EREF PPC processors On non-EREF processors it expands to instructions that destroy GPR0. Reflect this in the Asm semantics for Pisel. --- powerpc/Asmgenproof1.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'powerpc/Asmgenproof1.v') diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 8c9fd2bd..2e609900 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1262,13 +1262,13 @@ Qed. Lemma transl_select_op_correct: forall cond args ty r1 r2 rd k rs m c, transl_select_op cond args r1 r2 rd k = OK c -> - important_preg r1 = true -> important_preg r2 = true -> + important_preg rd = true -> important_preg r1 = true -> important_preg r2 = true -> exists rs', exec_straight ge fn c rs m k rs' m /\ Val.lessdef (Val.select (eval_condition cond (map rs (map preg_of args)) m) rs#r1 rs#r2 ty) rs'#rd /\ forall r, important_preg r = true -> r <> rd -> rs'#r = rs#r. Proof. - intros until c. intros TR IMP1 IMP2. + intros until c. intros TR IMP1 IMP2 IMP3. unfold transl_select_op in TR. destruct (ireg_eq r1 r2). - inv TR. econstructor; split; [|split]. -- cgit