diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-04-13 10:11:05 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-05-20 18:00:46 +0200 |
| commit | d002919334e83904447957f666f0d48704c5e55b (patch) | |
| tree | aec12f1218490c75f3592c3443e98df706409577 /powerpc/Asmgenproof1.v | |
| parent | 43e7b6702a76306f20687bc9aba93ae465d6e4be (diff) | |
| download | compcert-kvx-d002919334e83904447957f666f0d48704c5e55b.tar.gz compcert-kvx-d002919334e83904447957f666f0d48704c5e55b.zip | |
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.
Diffstat (limited to 'powerpc/Asmgenproof1.v')
| -rw-r--r-- | powerpc/Asmgenproof1.v | 4 |
1 files changed, 2 insertions, 2 deletions
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]. |