Fixes failing PowerPC unit tests

Also includes a fix for `ldu`. The manual says that the
immediate is sign-extended.

Author: bmourad01

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
 

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
 

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

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 = signed imm16 ops.(2) in
   RTL.[
     rt := cpu.load (ra + im) doubleword;
     ra := ra + im;

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.[