From 6e483e06ca723349f002da93f728a78904e00976 Mon Sep 17 00:00:00 2001 From: bmourad01 Date: Sat, 4 May 2024 15:26:37 -0400 Subject: [PATCH 1/2] Fixes failing PowerPC unit tests --- plugins/powerpc/powerpc.mli | 2 ++ plugins/powerpc/powerpc_dsl.ml | 5 +++++ plugins/powerpc/powerpc_dsl.mli | 1 + plugins/powerpc/powerpc_load.ml | 22 +++++++++++----------- plugins/powerpc/powerpc_store.ml | 16 ++++++++-------- 5 files changed, 27 insertions(+), 19 deletions(-) diff --git a/plugins/powerpc/powerpc.mli b/plugins/powerpc/powerpc.mli index 9ac219d38..bb4d83b81 100644 --- a/plugins/powerpc/powerpc.mli +++ b/plugins/powerpc/powerpc.mli @@ -399,6 +399,8 @@ module Std : sig (** imm constructor - constructs an immediate from operand *) val imm : (op -> exp) ec + val imm16 : (op -> exp) ec + (** var constructor - constructs a variable of bitwidth *) val var : (bitwidth -> exp) ec diff --git a/plugins/powerpc/powerpc_dsl.ml b/plugins/powerpc/powerpc_dsl.ml index c1664d590..0036d0b3c 100644 --- a/plugins/powerpc/powerpc_dsl.ml +++ b/plugins/powerpc/powerpc_dsl.ml @@ -32,6 +32,11 @@ let imm signed op = if signed then Exp.(signed @@ of_word w) else Exp.(unsigned @@ of_word w) +let imm16 signed op = + let w = Word.of_int ~width:16 (int_of_imm op) in + if signed then Exp.(signed @@ of_word w) + else Exp.(unsigned @@ of_word w) + let signed f = f true let unsigned f = f false diff --git a/plugins/powerpc/powerpc_dsl.mli b/plugins/powerpc/powerpc_dsl.mli index f83c29ede..1a4e300cd 100644 --- a/plugins/powerpc/powerpc_dsl.mli +++ b/plugins/powerpc/powerpc_dsl.mli @@ -16,6 +16,7 @@ val bitwidth : int -> bitwidth val int_of_bitwidth : bitwidth -> int val imm : (op -> exp) ec +val imm16 : (op -> exp) ec val var : (bitwidth -> exp) ec val reg : (reg -> exp) -> (op -> exp) ec val const : (bitwidth -> int -> exp) ec diff --git a/plugins/powerpc/powerpc_load.ml b/plugins/powerpc/powerpc_load.ml index e8640ad2a..c127e2e6e 100644 --- a/plugins/powerpc/powerpc_load.ml +++ b/plugins/powerpc/powerpc_load.ml @@ -9,19 +9,19 @@ open Powerpc.Std 83 eb ff fc - lwz r31, -4(r11) *) let lbz cpu ops = let rt = unsigned cpu.reg ops.(0) in - let im = signed imm ops.(1) in + let im = signed imm16 ops.(1) in let ra = signed cpu.reg ops.(2) in RTL.[ rt := cpu.load (ra + im) byte; ] let lhz cpu ops = let rt = unsigned cpu.reg ops.(0) in - let im = signed imm ops.(1) in + let im = signed imm16 ops.(1) in let ra = signed cpu.reg ops.(2) in RTL.[ rt := cpu.load (ra + im) halfword; ] let lwz cpu ops = let rt = unsigned cpu.reg ops.(0) in - let im = signed imm ops.(1) in + let im = signed imm16 ops.(1) in let ra = signed cpu.reg ops.(2) in RTL.[ rt := cpu.load (ra + im) word; ] @@ -57,7 +57,7 @@ let lwzx cpu ops = 85 3f ff fc lwzu r9, -4(r31) *) let lbzu cpu ops = let rt = unsigned cpu.reg ops.(0) in - let im = signed imm ops.(2) in + let im = signed imm16 ops.(2) in let ra = signed cpu.reg ops.(3) in RTL.[ rt := cpu.load (ra + im) byte; @@ -66,7 +66,7 @@ let lbzu cpu ops = let lhzu cpu ops = let rt = unsigned cpu.reg ops.(0) in - let im = signed imm ops.(2) in + let im = signed imm16 ops.(2) in let ra = signed cpu.reg ops.(3) in RTL.[ rt := cpu.load (ra + im) halfword; @@ -75,7 +75,7 @@ let lhzu cpu ops = let lwzu cpu ops = let rt = unsigned cpu.reg ops.(0) in - let im = signed imm ops.(2) in + let im = signed imm16 ops.(2) in let ra = signed cpu.reg ops.(3) in RTL.[ rt := cpu.load (ra + im) word; @@ -122,7 +122,7 @@ let lwzux cpu ops = a8 29 00 05 lha r1, 5(r9) *) let lha cpu ops = let rt = signed cpu.reg ops.(0) in - let im = signed imm ops.(1) in + let im = signed imm16 ops.(1) in let ra = signed cpu.reg ops.(2) in RTL.[ rt := cpu.load (ra + im) halfword; @@ -134,7 +134,7 @@ let lha cpu ops = eb eb 01 16 lwa r31, 276(r11) *) let lwa cpu ops = let rt = signed cpu.reg ops.(0) in - let im = signed imm ops.(1) in + let im = signed imm16 ops.(1) in let ra = signed cpu.reg ops.(2) in RTL.[ rt := cpu.load (ra + im) word; @@ -168,7 +168,7 @@ let lwax cpu ops = let lhau cpu ops = let rt = signed cpu.reg ops.(0) in let ra = signed cpu.reg ops.(1) in - let im = signed imm ops.(2) in + let im = signed imm16 ops.(2) in RTL.[ rt := cpu.load (ra + im) halfword; ra := ra + im @@ -203,7 +203,7 @@ let lwaux cpu ops = e8 29 00 08 ld r1, 8(r9) *) let ld cpu ops = let rt = unsigned cpu.reg ops.(0) in - let im = signed imm ops.(1) in + let im = signed imm16 ops.(1) in let ra = signed cpu.reg ops.(2) in RTL.[ rt := cpu.load (ra + im) doubleword; @@ -228,7 +228,7 @@ let ldx cpu ops = let ldu cpu ops = let rt = unsigned cpu.reg ops.(0) in let ra = signed cpu.reg ops.(1) in - let im = unsigned imm ops.(2) in + let im = unsigned imm16 ops.(2) in RTL.[ rt := cpu.load (ra + im) doubleword; ra := ra + im; diff --git a/plugins/powerpc/powerpc_store.ml b/plugins/powerpc/powerpc_store.ml index 28b5eb6c8..bdc4eebae 100644 --- a/plugins/powerpc/powerpc_store.ml +++ b/plugins/powerpc/powerpc_store.ml @@ -9,19 +9,19 @@ open Powerpc.Std 91 28 ff d4 stw r9,-44(r8) *) let stb cpu ops = let rs = unsigned cpu.reg ops.(0) in - let im = signed imm ops.(1) in + let im = signed imm16 ops.(1) in let ra = signed cpu.reg ops.(2) in RTL.[ cpu.store (ra + im) rs byte; ] let sth cpu ops = let rs = unsigned cpu.reg ops.(0) in - let im = signed imm ops.(1) in + let im = signed imm16 ops.(1) in let ra = signed cpu.reg ops.(2) in RTL.[ cpu.store (ra + im) rs halfword; ] let stw cpu ops = let rs = unsigned cpu.reg ops.(0) in - let im = signed imm ops.(1) in + let im = signed imm16 ops.(1) in let ra = signed cpu.reg ops.(2) in RTL.[ cpu.store (ra + im) rs word; ] @@ -64,7 +64,7 @@ let stdx cpu ops = 94 21 ff f0 stwu r1,-16(r1) *) let stbu cpu ops = let rs = unsigned cpu.reg ops.(1) in - let im = signed imm ops.(2) in + let im = signed imm16 ops.(2) in let ra = signed cpu.reg ops.(3) in RTL.[ cpu.store (ra + im) rs byte; @@ -73,7 +73,7 @@ let stbu cpu ops = let sthu cpu ops = let rs = unsigned cpu.reg ops.(1) in - let im = signed imm ops.(2) in + let im = signed imm16 ops.(2) in let ra = signed cpu.reg ops.(3) in RTL.[ cpu.store (ra + im) rs halfword; @@ -82,7 +82,7 @@ let sthu cpu ops = let stwu cpu ops = let rs = unsigned cpu.reg ops.(1) in - let im = signed imm ops.(2) in + let im = signed imm16 ops.(2) in let ra = signed cpu.reg ops.(3) in RTL.[ cpu.store (ra + im) rs word; @@ -138,7 +138,7 @@ let stdux cpu ops = f8 29 00 08 std r1, 8(r9) *) let std cpu ops = let rs = unsigned cpu.reg ops.(0) in - let im = signed imm ops.(1) in + let im = signed imm16 ops.(1) in let ra = signed cpu.reg ops.(2) in RTL.[ cpu.store (ra + im) rs doubleword; @@ -150,7 +150,7 @@ let std cpu ops = f8 29 00 09 stdu r1, 8(r9) *) let stdu cpu ops = let rs = unsigned cpu.reg ops.(1) in - let im = signed imm ops.(2) in + let im = signed imm16 ops.(2) in let ra = signed cpu.reg ops.(3) in let ea = unsigned var doubleword in RTL.[ From 6ee00e72fab9dbef4dcafa6a0a2401bc95bb221f Mon Sep 17 00:00:00 2001 From: bmourad01 Date: Thu, 9 May 2024 17:31:22 -0400 Subject: [PATCH 2/2] Fix `ldu` The manual says that this immediate is also sign-extended --- plugins/powerpc/powerpc_load.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/powerpc/powerpc_load.ml b/plugins/powerpc/powerpc_load.ml index c127e2e6e..a93a34a00 100644 --- a/plugins/powerpc/powerpc_load.ml +++ b/plugins/powerpc/powerpc_load.ml @@ -228,7 +228,7 @@ let ldx cpu ops = let ldu cpu ops = let rt = unsigned cpu.reg ops.(0) in let ra = signed cpu.reg ops.(1) in - let im = unsigned imm16 ops.(2) in + let im = signed imm16 ops.(2) in RTL.[ rt := cpu.load (ra + im) doubleword; ra := ra + im;