@@ -214,7 +214,7 @@ instruction set architecture PPC64SFS = {
214214 , me : Bits<5> // end index of bit mask
215215 , rc : Bits<1> // if set the instruction modifies the CR
216216 , mb6 = mb as Bits<6> // start index zero extended to 6 bits
217- , me6 = me as Bits<6> // end index zero extended to 6 bits
217+ , me6 = me as Bits<6> // end index zero extended to 6 bits
218218 }
219219
220220 format SCForm : Instruction =
@@ -382,30 +382,30 @@ instruction set architecture PPC64SFS = {
382382
383383 // converts binary coded decimal to declet
384384 function bcdtodpd (n : Bits<12>) -> Bits<10> =
385- ((n(6) & n(11) & n(3) & ~n(7)) | (n(2) & n(11) & ~n(3)) | (n(10) & ~n(11)),
386- (n(5) & n(11) & n(3) & ~n(7)) | (n(1) & n(11) & ~n(3)) | (n(9) & ~n(11)),
385+ ((n(6) & n(11) & n(3) & ~n(7)) | (n(2) & n(11) & ~n(3)) | (n(10) & ~n(11)),
386+ (n(5) & n(11) & n(3) & ~n(7)) | (n(1) & n(11) & ~n(3)) | (n(9) & ~n(11)),
387387 n(8),
388- (n(2) & ~n(11) & n(7) & ~n(3)) | (n(6) & ~n(3) & ~n(7)) | (n(6) & ~n(11) & ~n(7)) | (n(7) & n(3)),
389- (n(1) & ~n(11) & n(7) & ~n(3)) | (n(5) & ~n(3) & ~n(7)) | (n(5) & ~n(11) & ~n(7)) | (n(11) & n(3)),
390- n(4),
391- n(11) | n(7) | n(3),
392- (~n(7) & n(2) & ~n(3)) | (n(7) & n(3)) | n(11),
393- (~n(11) & n(1) & ~n(3)) | (n(11) & n(3)) | n(7),
388+ (n(2) & ~n(11) & n(7) & ~n(3)) | (n(6) & ~n(3) & ~n(7)) | (n(6) & ~n(11) & ~n(7)) | (n(7) & n(3)),
389+ (n(1) & ~n(11) & n(7) & ~n(3)) | (n(5) & ~n(3) & ~n(7)) | (n(5) & ~n(11) & ~n(7)) | (n(11) & n(3)),
390+ n(4),
391+ n(11) | n(7) | n(3),
392+ (~n(7) & n(2) & ~n(3)) | (n(7) & n(3)) | n(11),
393+ (~n(11) & n(1) & ~n(3)) | (n(11) & n(3)) | n(7),
394394 n(0))
395395
396396 // converts declet to binary coded decimal
397397 function dpdtobcd (n : Bits<10>) -> Bits<12> =
398- ((~n(6) & n(3) & n(2)) | (n(5) & n(3) & n(2) & n(6)) | (n(3) & n(2) & ~n(1)),
399- (n(9) & n(6) & n(1) & ~n(5)) | (n(9) & ~n(2)) | (n(9) & ~n(3)),
400- (n(8) & n(6) & n(1) & ~n(5)) | (n(8) & ~n(2)) | (n(8) & ~n(3)),
401- n(7),
402- (n(3) & ~n(2) & n(1)) | (n(6) & n(3) & n(2) & n(1)) | (~n(5) & n(3) & n(1) & n(2)),
403- (n(9) & n(5) & n(3) & n(2) & n(1) & ~n(6)) | (n(6) & ~n(1) & n(3)) | (n(6) & ~n(3)),
404- (n(8) & n(5) & n(2) & n(3) & n(1) & ~n(6)) | (n(5) & ~n(1) & n(3)) | (n(5) & ~n(3)),
405- n(4),
406- (n(5) & n(3) & n(2) & n(1)) | (n(6) & n(3) & n(2) & n(1)) | (n(3) & ~n(2) & ~n(1)),
407- (n(9) & ~n(6) & ~n(5) & n(2) & n(3)) | (n(6) & n(3) & ~n(2) & n(1)) | (n(9) & n(2) & ~n(1) & n(3)) | (n(2) & ~n(3)),
408- (n(8) & ~n(6) & ~n(5) & n(3) & n(2)) | (n(5) & n(3) & ~n(2) & n(1)) | (n(8) & n(3) & n(2) & ~n(1)) | (n(1) & ~n(3)),
398+ ((~n(6) & n(3) & n(2)) | (n(5) & n(3) & n(2) & n(6)) | (n(3) & n(2) & ~n(1)),
399+ (n(9) & n(6) & n(1) & ~n(5)) | (n(9) & ~n(2)) | (n(9) & ~n(3)),
400+ (n(8) & n(6) & n(1) & ~n(5)) | (n(8) & ~n(2)) | (n(8) & ~n(3)),
401+ n(7),
402+ (n(3) & ~n(2) & n(1)) | (n(6) & n(3) & n(2) & n(1)) | (~n(5) & n(3) & n(1) & n(2)),
403+ (n(9) & n(5) & n(3) & n(2) & n(1) & ~n(6)) | (n(6) & ~n(1) & n(3)) | (n(6) & ~n(3)),
404+ (n(8) & n(5) & n(2) & n(3) & n(1) & ~n(6)) | (n(5) & ~n(1) & n(3)) | (n(5) & ~n(3)),
405+ n(4),
406+ (n(5) & n(3) & n(2) & n(1)) | (n(6) & n(3) & n(2) & n(1)) | (n(3) & ~n(2) & ~n(1)),
407+ (n(9) & ~n(6) & ~n(5) & n(2) & n(3)) | (n(6) & n(3) & ~n(2) & n(1)) | (n(9) & n(2) & ~n(1) & n(3)) | (n(2) & ~n(3)),
408+ (n(8) & ~n(6) & ~n(5) & n(3) & n(2)) | (n(5) & n(3) & ~n(2) & n(1)) | (n(8) & n(3) & n(2) & ~n(1)) | (n(1) & ~n(3)),
409409 n(0))
410410
411411 // reverses the byte order of each halfword in a word
@@ -627,28 +627,34 @@ instruction set architecture PPC64SFS = {
627627 }
628628 }
629629
630+ // TODO: rev is inverted, should be $rev = true, requires big endian support
630631 // reads Byte/ Halfword/ Word from memory into X(dst)
631632 model ReadMem (ea : Id, unit : SymEx, dst : Ex, rev : Bool, type : Id) : Stat = {
632633 match : Stat
633- ( $unit = Unit::Word => if $rev
634- then X($dst) := byterevw(MEM<4>($ea)) as $type
635- else X($dst) := MEM<4>($ea) as $type
636- ; $unit = Unit::Half => if $rev
637- then X($dst) := byterevh(MEM<2>($ea)) as $type
638- else X($dst) := MEM<2>($ea) as $type
634+ ( $unit = Unit::Word => match : Stat
635+ ( $rev = false => X($dst) := byterevw(MEM<4>($ea)) as $type
636+ ; _ => X($dst) := MEM<4>($ea) as $type
637+ )
638+ ; $unit = Unit::Half => match : Stat
639+ ( $rev = false => X($dst) := byterevh(MEM<2>($ea)) as $type
640+ ; _ => X($dst) := MEM<2>($ea) as $type
641+ )
639642 ; _ => X($dst) := MEM($ea) as $type
640643 )
641644 }
642645
646+ // TODO: rev is inverted, should be $rev = true, requires big endian support
643647 // writes Byte/ Halfword/ Word from X(src) into memory
644648 model WriteMem (ea : Id, unit : SymEx, src : Id, rev : Bool) : Stat = {
645649 match : Stat
646- ( $unit = Unit::Word => if $rev
647- then MEM<4>($ea) := byterevw(XW($src))
648- else MEM<4>($ea) := XW($src)
649- ; $unit = Unit::Half => if $rev
650- then MEM<2>($ea) := byterevh(XH($src))
651- else MEM<2>($ea) := XH($src)
650+ ( $unit = Unit::Word => match : Stat
651+ ( $rev = false => MEM<4>($ea) := byterevw(XW($src))
652+ ; _ => MEM<4>($ea) := XW($src)
653+ )
654+ ; $unit = Unit::Half => match : Stat
655+ ( $rev = false => MEM<2>($ea) := byterevh(XH($src))
656+ ; _ => MEM<2>($ea) := XH($src)
657+ )
652658 ; _ => MEM($ea) := XB($src)
653659 )
654660 }
@@ -757,7 +763,7 @@ instruction set architecture PPC64SFS = {
757763 let a = XW(rs) as SDWord in
758764 if ((VADL::slth(a, immS)) & to(4)) | ((VADL::sgth(a, immS)) & to(3)) |
759765 ((a = immS) & to(2)) | ((VADL::ulth(a, immS)) & to(1)) |
760- ((VADL::ugth(a, immS)) & to(0))
766+ ((VADL::ugth(a, immS)) & to(0))
761767 then raise Trap
762768 encoding AsId($asm) = {opcd = 0b000011}
763769 assembly AsId($asm) = ($asm, " ", decimal(to), ",", decimal(rs), ",", decimal(imm))
@@ -939,7 +945,7 @@ instruction set architecture PPC64SFS = {
939945 // instruction: mfmsr
940946 model XFormMSRGPRInstr (asm : Str) : IsaDefs = {
941947 instruction AsId($asm) : XFormA =
942- if MSR.pr = 0 then X(rs) := MSR
948+ if MSR.pr = 0 then X(rs) := MSR
943949 else raise Privilege
944950 encoding AsId($asm) = {opcd = 0b011111, ra = 0b00000, rb = 0b00000, extopcd = 0b00010'10011, rc = 0b0}
945951 assembly AsId($asm) = ($asm, " ", decimal(rs))
@@ -1051,8 +1057,8 @@ instruction set architecture PPC64SFS = {
10511057 // instructions: mtmsr
10521058 model XFormMoveGPRMSRInstr (asm : Str) : IsaDefs = {
10531059 instruction AsId($asm) : XFormF =
1054- if MSR.pr = 0
1055- then MSR := if l = 0
1060+ if MSR.pr = 0
1061+ then MSR := if l = 0
10561062 then (MSR(63..32), X(rs)(31..23), MSR(22), X(rs)(21..16),
10571063 X(rs)(15) | X(rs)(14), X(rs)(14..13), MSR(12), X(rs)(11..6),
10581064 (X(rs)(5) | X(rs)(14)) & ~(MSR(22) & MSR(60) & ~X(rs)(14)),
@@ -1071,7 +1077,7 @@ instruction set architecture PPC64SFS = {
10711077 let b = XW(rb) as SDWord in
10721078 if ((VADL::slth(a, b)) & to(4)) | ((VADL::sgth(a, b)) & to(3)) |
10731079 ((a = b) & to(2)) | ((VADL::ulth(a, b)) & to(1)) |
1074- ((VADL::ugth(a, b)) & to(0))
1080+ ((VADL::ugth(a, b)) & to(0))
10751081 then raise Trap
10761082 encoding AsId($asm) = {opcd = 0b011111, extopcd = 0b00000'00100, rsv = 0b0}
10771083 assembly AsId($asm) = ($asm, " ", decimal(to), ",", decimal(ra), ",", decimal(rb))
@@ -1097,7 +1103,7 @@ instruction set architecture PPC64SFS = {
10971103 // instructions: mtocrf
10981104 model XFXMoveGPROCRFInstr (asm : Str) : IsaDefs = {
10991105 instruction AsId($asm) : XFXFormA =
1100- CR := if VADL::cob(fxm) = 1
1106+ CR := if VADL::cob(fxm) = 1
11011107 then let mask = crmask(fxm) in (XW(rs) & mask) | (CR & ~mask)
11021108 else 0
11031109 encoding AsId($asm) = {opcd = 0b011111, m = 0b1, rsv1 = 0b0, extopcd = 0b00100'10000, rsv2 = 0b0}
@@ -1107,7 +1113,7 @@ instruction set architecture PPC64SFS = {
11071113 // instructions: mfocrf
11081114 model XFXMoveOCRFGPRInstr (asm : Str) : IsaDefs = {
11091115 instruction AsId($asm) : XFXFormA =
1110- X(rs) := if VADL::cob(fxm) = 1
1116+ X(rs) := if VADL::cob(fxm) = 1
11111117 then (CR & crmask(fxm)) as UDWord
11121118 else 0
11131119 encoding AsId($asm) = {opcd = 0b011111, m = 0b1, rsv1 = 0b0, extopcd = 0b00000'10011, rsv2 = 0b0}
@@ -1189,7 +1195,7 @@ instruction set architecture PPC64SFS = {
11891195 $XOFormAddSubInstrExt(AsId($r.x.asm, "O_"); $r; true ; true )
11901196 }
11911197
1192- record XOFormDivInstrRec (x : AsmOpExt, a : TwoArgs, type : Id, exc : Ex)
1198+ record XOFormDivInstrRec (x : AsmOpExt, a : TwoArgs, type : Id, exc : Ex, res0 : Ex )
11931199
11941200 model XOFormDivInstrExt (eid : Id, r : XOFormDivInstrRec, oe : Bool, rc : Bool) : IsaDefs = {
11951201 instruction $eid : XOForm =
@@ -1200,7 +1206,7 @@ instruction set architecture PPC64SFS = {
12001206 X(rs) := result
12011207 $SetXERAndCRWithOV($oe; false; $rc; exc | flags.overflow)
12021208 }
1203- else let result = $r.a.arg1 as $r.type in {
1209+ else let result = $r.res0 as UDWord in {
12041210 X(rs) := result
12051211 $SetXERAndCRWithOV($oe; false; $rc; true)
12061212 }
@@ -1302,13 +1308,13 @@ instruction set architecture PPC64SFS = {
13021308 $XOFormMulInstr((("MULHWU"; umull; 0b0000'01011); prod(63..32)); false)
13031309
13041310 $XOFormDivInstr((("DIVW" ; sdivs; 0b1111'01011); (XW(ra) ; XW(rb) ); UDWord;
1305- XW(ra) = 0x8000'0000 & XW(rb) = maxU32 ))
1311+ XW(ra) = 0x8000'0000 & XW(rb) = maxU32 ; XW(ra) ))
13061312 $XOFormDivInstr((("DIVWU" ; udivs; 0b1110'01011); (XW(ra) ; XW(rb) ); UDWord;
1307- false ))
1313+ false ; XW(ra) ))
13081314 $XOFormDivInstr((("DIVWE" ; sdivs; 0b1101'01011); (XW(ra) as SDWord << 32; XW(rb) as SDWord); SDWord;
1309- (XW(ra) = 0x8000'0000 & XW(rb) = 0xFFFF'FFFF) | (res != (res as SWord) as SDWord)))
1315+ (XW(ra) = 0x8000'0000 & XW(rb) = 0xFFFF'FFFF) | (res != (res as SWord) as SDWord); 0 ))
13101316 $XOFormDivInstr((("DIVWEU"; udivs; 0b1100'01011); (XW(ra) as UDWord << 32; XW(rb) as UDWord); UDWord;
1311- VADL::ugeq(res as UDWord, maxU32E) ))
1317+ VADL::ugeq(res as UDWord, maxU32E) ; 0 ))
13121318
13131319 $XOFormNegateInstr("NEG")
13141320
@@ -1359,7 +1365,7 @@ instruction set architecture PPC64SFS = {
13591365 $XFormArithmeticShiftInstr((("SRAW" ; 0b11000'11000); X(rb)(5..0);
13601366 if X(rb)(5) = 0 then r(63..32) as SDWord else X(rs)(31) as SDWord))
13611367 $XFormArithmeticShiftInstr((("SRAWI"; 0b11001'11000); rb ;
1362- r(63..32) as SDWord))
1368+ r(63..32) as SDWord ))
13631369
13641370 //------------------------Compare----------------------------
13651371 $XFormCmpInstr(("CMP" ; 0b00000'00000); false)
0 commit comments