From 64393c4bb570c4c9570ddc4c457618db6fb71108 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Fri, 19 Oct 2018 21:23:29 +0200 Subject: Use 'gpr_or_zero' for base register of indexed load/stores, bug 24776 --- powerpc/Asm.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'powerpc/Asm.v') 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. -- cgit