diff options
| author | Michael Schmidt <github@mschmidt.me> | 2018-10-19 21:23:29 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-10-20 10:02:59 +0200 |
| commit | 64393c4bb570c4c9570ddc4c457618db6fb71108 (patch) | |
| tree | 41cbf65b2e787bee3e950af781b83002188ab3bc /powerpc/Asm.v | |
| parent | 791971d203068a032477c7627cc97c06fac95da2 (diff) | |
| download | compcert-kvx-64393c4bb570c4c9570ddc4c457618db6fb71108.tar.gz compcert-kvx-64393c4bb570c4c9570ddc4c457618db6fb71108.zip | |
Use 'gpr_or_zero' for base register of indexed load/stores, bug 24776
Diffstat (limited to 'powerpc/Asm.v')
| -rw-r--r-- | powerpc/Asm.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index aa15547b..ad24f563 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -606,7 +606,7 @@ Definition load1 (chunk: memory_chunk) (rd: preg) Definition load2 (chunk: memory_chunk) (rd: preg) (r1 r2: ireg) (rs: regset) (m: mem) := - match Mem.loadv chunk m (Val.add rs#r1 rs#r2) with + match Mem.loadv chunk m (Val.add (gpr_or_zero rs r1) rs#r2) with | None => Stuck | Some v => Next (nextinstr (rs#rd <- v)) m end. @@ -620,7 +620,7 @@ Definition store1 (chunk: memory_chunk) (r: preg) Definition store2 (chunk: memory_chunk) (r: preg) (r1 r2: ireg) (rs: regset) (m: mem) := - match Mem.storev chunk m (Val.add rs#r1 rs#r2) (rs#r) with + match Mem.storev chunk m (Val.add (gpr_or_zero rs r1) rs#r2) (rs#r) with | None => Stuck | Some m' => Next (nextinstr rs) m' end. |