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/Asm.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/Asm.v')
| -rw-r--r-- | powerpc/Asm.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 748058c4..e821c6c4 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -866,7 +866,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Vint n => if Int.eq n Int.zero then rs#r2 else rs#r1 | _ => Vundef end in - Next (nextinstr (rs#rd <- v)) m + Next (nextinstr (rs #rd <- v #GPR0 <- Vundef)) m | Plbz rd cst r1 => load1 Mint8unsigned rd cst r1 rs m | Plbzx rd r1 r2 => |