Lines Matching defs:rm
334 (address_mode1 ii thumb2 (Mode1_register imm5 type rm) =
335 (read_reg ii rm ||| read_cflag ii) >>=
336 (\(rm,c).
338 shift_c (rm, shift_t, shift_n, c))) /\
339 (address_mode1 ii thumb2 (Mode1_register_shifted_register rs type rm) =
340 (read_reg ii rm ||| read_reg ii rs ||| read_cflag ii) >>=
341 (\(rm,rs,c).
344 shift_c (rm, shift_t, shift_n, c)))`;
351 (address_mode2 ii indx add rn (Mode2_register imm5 type rm) =
352 (read_reg ii rm ||| read_cflag ii) >>=
353 (\(rm,c).
355 shift (rm, shift_t, shift_n, c) >>=
365 (address_mode3 ii indx add rn (Mode3_register imm2 rm) =
366 (read_reg ii rm ||| read_cflag ii) >>=
367 (\(rm,c).
368 shift (rm, SRType_LSL, w2n imm2, c) >>=
469 signed_parallel_add_sub_16 op2 rn rm =
470 let bn = SInt (bot_half rn) and bm = SInt (bot_half rm)
471 and tn = SInt (top_half rn) and tm = SInt (top_half rm)
480 signed_normal_add_sub_16 op2 rn rm : word32 # word4 option =
481 let (r1,r2) = signed_parallel_add_sub_16 op2 rn rm in
488 signed_saturating_add_sub_16 op2 rn rm : word32 # word4 option =
489 let (r1,r2) = signed_parallel_add_sub_16 op2 rn rm in
493 signed_halving_add_sub_16 op2 rn rm : word32 # word4 option =
494 let (r1,r2) = signed_parallel_add_sub_16 op2 rn rm in
498 signed_parallel_add_sub_8 op2 rn rm =
500 and m = MAP SInt (bytes (rm,4))
506 signed_normal_add_sub_8 op2 rn rm : word32 # word4 option =
507 let r = signed_parallel_add_sub_8 op2 rn rm in
512 signed_saturating_add_sub_8 op2 rn rm : word32 # word4 option =
513 (word32 (MAP (\i. signed_sat (i,8)) (signed_parallel_add_sub_8 op2 rn rm)),
517 signed_halving_add_sub_8 op2 rn rm : word32 # word4 option =
519 (signed_parallel_add_sub_8 op2 rn rm)), NONE)`;
522 unsigned_parallel_add_sub_16 op2 rn rm =
523 let bn = UInt (bot_half rn) and bm = UInt (bot_half rm)
524 and tn = UInt (top_half rn) and tm = UInt (top_half rm)
533 unsigned_normal_add_sub_16 op2 rn rm : word32 # word4 option =
534 let (r1,r2) = unsigned_parallel_add_sub_16 op2 rn rm in
553 unsigned_saturating_add_sub_16 op2 rn rm : word32 # word4 option =
554 let (r1,r2) = unsigned_parallel_add_sub_16 op2 rn rm in
559 unsigned_halving_add_sub_16 op2 rn rm : word32 # word4 option =
560 let (r1,r2) = unsigned_parallel_add_sub_16 op2 rn rm in
564 unsigned_parallel_add_sub_8 op2 rn rm =
566 and m = MAP UInt (bytes (rm,4))
572 unsigned_normal_add_sub_8 op2 rn rm : word32 # word4 option =
573 let r = unsigned_parallel_add_sub_8 op2 rn rm
581 unsigned_saturating_add_sub_8 op2 rn rm : word32 # word4 option =
584 (unsigned_parallel_add_sub_8 op2 rn rm)), NONE)`;
587 unsigned_halving_add_sub_8 op2 rn rm : word32 # word4 option =
588 (word32 (MAP (\i. i2w (i / 2)) (unsigned_parallel_add_sub_8 op2 rn rm)),
592 parallel_add_sub u (op1,op2) rn rm =
595 signed_normal_add_sub_8 op2 rn rm
597 signed_normal_add_sub_8 op2 rn rm
599 signed_normal_add_sub_16 op2 rn rm
601 signed_saturating_add_sub_8 op2 rn rm
603 signed_saturating_add_sub_8 op2 rn rm
605 signed_saturating_add_sub_16 op2 rn rm
607 signed_halving_add_sub_8 op2 rn rm
609 signed_halving_add_sub_8 op2 rn rm
611 signed_halving_add_sub_16 op2 rn rm
613 unsigned_normal_add_sub_8 op2 rn rm
615 unsigned_normal_add_sub_8 op2 rn rm
617 unsigned_normal_add_sub_16 op2 rn rm
619 unsigned_saturating_add_sub_8 op2 rn rm
621 unsigned_saturating_add_sub_8 op2 rn rm
623 unsigned_saturating_add_sub_16 op2 rn rm
625 unsigned_halving_add_sub_8 op2 rn rm
627 unsigned_halving_add_sub_8 op2 rn rm
629 unsigned_halving_add_sub_16 op2 rn rm`;
912 (read_reg ii m >>= (\rm. bx_write_pc ii rm))`;
966 (\(pc,rm,iset).
976 (\u. bx_write_pc ii rm)))`;
1003 (\(pc,rn,rm).
1005 read_memU ii (rn + LSL(rm,1), 2)
1007 read_memU ii (rn + rm, 1)) >>=
1020 (\(pc,rn,rm,cpsr,teehbr).
1021 if rn <=+ rm then
1113 (\rm.
1115 write_reg ii d (n2w (count_leading_zeroes rm))) >>=
1331 (\(ra,rm,rn,version).
1332 (let result = rn * rm + (if acc then ra else 0w) in
1367 (\(rdhi,rdlo,rm,rn,version).
1369 (if signed then sw2sw rn * sw2sw rm else w2w rn * w2w rm) +
1401 (\(rdhi,rdlo,rm,rn).
1402 (let result : word64 = w2w rn * w2w rm + w2w rdhi + w2w rdlo in
1419 (\(rn,rm,ra). let result = ra - rn * rm in
1436 (\(rm,rn).
1439 of 0b00w => signed_sat_q (SInt rm + SInt rn,32)
1440 | 0b01w => signed_sat_q (SInt rm - SInt rn,32)
1445 signed_sat_q (SInt rm + SInt doubled,32)
1452 signed_sat_q (SInt rm - SInt doubled,32)
1475 (\(rm,rn,ra).
1477 and operand2 = if m_high then top_half rm else bot_half rm
1501 (\(rm,rn).
1503 and operand2 = if m_high then top_half rm else bot_half rm
1524 (\(rm,rn,ra).
1525 let operand2 = if m_high then top_half rm else bot_half rm
1551 (\(rm,rn).
1552 let operand2 = if m_high then top_half rm else bot_half rm
1575 (\(rm,rn,rdhi,rdlo).
1577 and operand2 = if m_high then top_half rm else bot_half rm
1603 (\(rm,rn,ra).
1604 let operand2 = if m_swap then ROR (rm,16) else rm in
1635 (\(rm,rn,rdhi,rdlo).
1636 let operand2 = if m_swap then ROR (rm,16) else rm in
1665 (\(rm,rn,ra).
1666 let result = SInt ((w2w ra : word64) << 32) + SInt rn * SInt rm in
1685 (\(rm,rn,ra).
1686 let result = SInt ((w2w ra :word64) << 32) - SInt rn * SInt rm in
1744 (\(rn,rm).
1745 let (result,ge) = parallel_add_sub u op rn rm in
1759 (\rm.
1760 if rm = 0w then
1772 write_reg ii d (if unsigned then rn // rm else rn / rm)) >>=
1787 (\(rn,rm,c).
1789 shift (rm, shift_t, shift_n, c) >>=
1839 (\(rn,rm).
1840 let rotated = ROR (rm, w2n rotate * 8) in
1858 (\(rn,rm,ge).
1859 let r1 = if ge ' 0 then ( 7 >< 0 ) rn else ( 7 >< 0 ) rm
1860 and r2 = if ge ' 1 then ( 15 >< 8 ) rn else ( 15 >< 8 ) rm
1861 and r3 = if ge ' 2 then ( 23 >< 16 ) rn else ( 23 >< 16 ) rm
1862 and r4 = if ge ' 3 then ( 31 >< 24 ) rn else ( 31 >< 24 ) rm
1915 (\(rn,rm).
1916 let rotated = ROR (rm, w2n rotate * 8) in
1934 (\rm.
1936 write_reg ii d (word32 (REVERSE (bytes (rm, 4))))) >>= unit2))`;
1957 (\(rn,rm).
1958 let rotated = ROR (rm, w2n rotate * 8) in
1977 (\rm.
1980 (let w = bytes (rm, 4) in
1995 (\rm.
1997 write_reg ii d (word_reverse rm)) >>= unit2))`;
2012 (\rm.
2013 let r1 = sw2sw (( 7 >< 0 ) rm : word8) : word24
2014 and r2 = ( 15 >< 8 ) rm : word8
2034 (\(rm,rn,ra).
2035 let absdiff1 = ABS (UInt (( 7 -- 0 ) rn) - UInt (( 7 -- 0 ) rm))
2036 and absdiff2 = ABS (UInt (( 15 -- 8 ) rn) - UInt (( 15 -- 8 ) rm))
2037 and absdiff3 = ABS (UInt (( 23 -- 16 ) rn) - UInt (( 23 -- 16 ) rm))
2038 and absdiff4 = ABS (UInt (( 31 -- 24 ) rn) - UInt (( 31 -- 24 ) rm))
3477 | Branch_Exchange rm =>
3481 | Branch_Link_Exchange_Register rm =>
3485 | Table_Branch_Byte rn h rm =>
3487 | Check_Array rn rm =>
3505 | Multiply a s rd ra rm rn =>
3507 | Multiply_Subtract rd ra rm rn =>
3509 | Signed_Halfword_Multiply 0w m n rd ra rm rn =>
3511 | Signed_Halfword_Multiply 1w m F rd ra rm rn =>
3513 | Signed_Halfword_Multiply 1w m T rd ra rm rn =>
3515 | Signed_Halfword_Multiply 2w m n rd ra rm rn =>
3517 | Signed_Halfword_Multiply opc m n rd ra rm rn =>
3519 | Signed_Multiply_Dual rd ra rm sub m_swap rn =>
3521 | Signed_Multiply_Long_Dual rdhi rdlo rm sub m_swap rn =>
3523 | Signed_Most_Significant_Multiply rd ra rm round rn =>
3525 | Signed_Most_Significant_Multiply_Subtract rd ra rm round rn =>
3527 | Multiply_Long u a s rdhi rdlo rm rn =>
3529 | Multiply_Accumulate_Accumulate rdhi rdlo rm rn =>
3535 | Saturating_Add_Subtract opc rn rd rm =>
3537 | Pack_Halfword rn rd imm5 tbform rm =>
3539 | Extend_Byte u rn rd rotate rm =>
3541 | Extend_Byte_16 u rn rd rotate rm =>
3543 | Extend_Halfword u rn rd rotate rm =>
3547 | Count_Leading_Zeroes rd rm =>
3549 | Reverse_Bits rd rm =>
3551 | Byte_Reverse_Word rd rm =>
3553 | Byte_Reverse_Packed_Halfword rd rm =>
3555 | Byte_Reverse_Signed_Halfword rd rm =>
3559 | Select_Bytes rn rd rm =>
3561 | Unsigned_Sum_Absolute_Differences rd ra rm rn =>
3563 | Parallel_Add_Subtract u op rn rd rm =>
3565 | Divide u rn rd rm =>