Lines Matching defs:rn
1389 fun narrow_okay_imm m i (rd,rn) =
1392 if is_SP rn then
1400 narrow_register rn andalso
1401 if rd = rn then
1406 m = RSB andalso v = 0 andalso narrow_registers [rd,rn]
1410 (rd,rn,rm,mode1) =
1414 of ADD => if narrow_registers [rd,rn] then
1416 not sflag andalso rd = rn andalso
1419 not sflag andalso rd = rn andalso
1421 | SUB => sflag = not InITBlock andalso narrow_registers [rd,rn,rm]
1425 | _ => sflag = not InITBlock andalso rd = rn andalso
1426 narrow_registers [rn,rm]);
1431 fun data_processing_immediate m (rd,rn,i) =
1433 if (m = ADD orelse m = SUB) andalso is_F sflag andalso is_PC rn then
1441 not (is_SP rn))
1443 andalso narrow_okay_imm m i (rd,rn)
1451 (opc,sflag,rn,rd,mk_Mode1_immediate imm12)))
1459 mk_Data_Processing (opc,sflag,rn,rd,mk_Mode1_immediate imm12))
1462 fun data_processing_register m (rd,rn,rm,mode1) =
1470 let val mode1' = mode1_register rn
1473 val narrow_okay = thumb_test (rd,rn,rm,mode1)
1476 thumb_test (rd,rm,rn,mode1')
1478 val (mode1,rn) = if swap_okay then (mode1',rm) else (mode1,rn)
1483 mk_Data_Processing (dp_opcode m,sflag,rn,rd,mode1)))
1490 mk_Data_Processing (dp_opcode m,sflag,rn,rd,mode1)))));
1505 arm_parse_register >>= (fn rn =>
1509 (fn i => data_processing_immediate m (rd,rn,i))
1514 data_processing_register m (rd,rn,rm,mode1)))
1516 (tryT (arm_parse_mode1_shift rn) return
1517 (fn _ => return (mode1_register rn))) >>=
1519 data_processing_register m (rd,rd,rn,mode1)))))
1521 data_processing_register m (rd,rd,rn,mode1_register rn)))));
1564 val (rd,rn) = if mem m [MOV,MVN] then (rdn,r15) else (r15,rdn)
1568 mk_Data_Processing (opc,sflag,rn,rd,mk_Mode1_immediate imm12)))
1574 val (rd,rn) = if m = MOV orelse m = MVN then (rdn,r0) else (r0,rdn)
1577 mk_Data_Processing (opc,sflag,rn,rd,mk_Mode1_immediate imm12))
1598 val (rd,rn) = if mem m [MOV,MVN] then (rdn,r15) else (r15,rdn)
1602 mk_Data_Processing (dp_opcode m,sflag,rn,rd,mode1)))
1607 val (rd,rn) = if mem m [MOV,MVN] then (rdn,r0) else (r0,rdn)
1610 mk_Data_Processing (dp_opcode m,sflag,rn,rd,mode1))
1638 val rn = mk_word4 (if thumb then 15 else 0)
1645 mk_Data_Processing (dp_opcode MOV,sflag,rn,rd,
1649 fun shift_register m thumb q InITBlock sflag (rd,rn,rm) =
1650 let val narrow_okay = q <> Wide andalso rd = rn andalso
1652 narrow_registers [rd,rn,rm]
1653 val rn' = mk_word4 (if thumb then 15 else 0)
1657 mk_Data_Processing (dp_opcode MOV,sflag,rn',rd,
1658 mk_Mode1_register_shifted_register (rm,shift_type m,rn))))
1672 arm_parse_register >>= (fn rn =>
1676 (fn i => shift_immediate m thumb q InITBlock sflag (rd,rn,i))
1679 shift_register m thumb q InITBlock sflag (rd,rn,rm))))
1680 (fn _ => shift_register m thumb q InITBlock sflag (rd,rd,rn)))))))));
1716 (fn rn => arm_parse_comma >>- return rn)
1717 (fn _ => return rd) >>= (fn rn =>
1726 return (Encoding_Thumb2_tm, mk_Add_Sub (add,rn,rd,imm12))
1946 (arm_parse_register >>= (fn rn =>
1947 assertT (narrow_register rn)
1954 mk_word3 (uint_of_word rn)))
1964 mk_word3 (uint_of_word rn)))))
2079 arm_parse_register >>= (fn rn =>
2086 (return (Encoding_Thumb2_tm,mk_Table_Branch_Byte (rn,F,rm)))))));
2091 arm_parse_register >>= (fn rn =>
2103 (return (Encoding_Thumb2_tm,mk_Table_Branch_Byte (rn,T,rm))))
2112 arm_parse_register >>= (fn rn =>
2114 (fn _ => arm_parse_register >>= (fn rm => return (rd,rn,rm)))
2115 (fn _ => return (rd,rd,rn)) >>=
2116 (fn (rd,rn,rm) =>
2124 (rd = rn orelse rd = rm) andalso
2125 narrow_registers [rn,rm]
2127 val (rn,rm) = if narrow_okay andalso rd <> rm
2128 then (rm,rn) else (rn,rm)
2132 mk_Multiply (F,sflag,rd,mk_word4 0,rm,rn)))
2136 (Encoding_ARM_tm, mk_Multiply (F,sflag,rd,mk_word4 0,rm,rn)))))));
2199 arm_parse_register >>= (fn rn =>
2201 (fn _ => arm_parse_register >>= (fn rm => return (rd,rn,rm)))
2202 (fn _ => return (rd,rd,rn)) >>= (fn (rd,rn,rm) =>
2211 v6 (mk_Parallel_Add_Subtract (u,opc,rn,rd,rm))
2215 of SMULBB => return_mk_shm (mk_word2 3,F,F,rd,r0,rm,rn)
2216 | SMULTB => return_mk_shm (mk_word2 3,F,T,rd,r0,rm,rn)
2217 | SMULBT => return_mk_shm (mk_word2 3,T,F,rd,r0,rm,rn)
2218 | SMULTT => return_mk_shm (mk_word2 3,T,T,rd,r0,rm,rn)
2219 | SMULWB => return_mk_shm (mk_word2 1,F,T,rd,r0,rm,rn)
2220 | SMULWT => return_mk_shm (mk_word2 1,T,T,rd,r0,rm,rn)
2221 | SMUAD => v6 (mk_Signed_Multiply_Dual (rd,r15,rm,F,F,rn))
2222 | SMUADX => v6 (mk_Signed_Multiply_Dual (rd,r15,rm,F,T,rn))
2223 | SMUSD => v6 (mk_Signed_Multiply_Dual (rd,r15,rm,T,F,rn))
2224 | SMUSDX => v6 (mk_Signed_Multiply_Dual (rd,r15,rm,T,T,rn))
2225 | SMMUL => v6 (mk_Signed_Most_Significant_Multiply (rd,r15,rm,F,rn))
2226 | SMMULR => v6 (mk_Signed_Most_Significant_Multiply (rd,r15,rm,T,rn))
2227 | SEL => v6 (mk_Select_Bytes (rn,rd,rm))
2228 | USAD8 => v6 (mk_Unsigned_Sum_Absolute_Differences (rd,r15,rm,rn))
2229 | QADD => dsp (mk_Saturating_Add_Subtract (mk_word2 0,rm,rd,rn))
2230 | QSUB => dsp (mk_Saturating_Add_Subtract (mk_word2 1,rm,rd,rn))
2231 | QDADD => dsp (mk_Saturating_Add_Subtract (mk_word2 2,rm,rd,rn))
2232 | QDSUB => dsp (mk_Saturating_Add_Subtract (mk_word2 3,rm,rd,rn))
2242 arm_parse_register >>= (fn rn =>
2255 of MLA => return (enc,mk_Multiply (T,sflag,rd,ra,rm,rn))
2256 | MLS => t2 (mk_Multiply_Subtract (rd,ra,rm,rn))
2257 | UMULL => return (enc,mk_Multiply_Long (F,F,sflag,rn,rd,ra,rm))
2258 | UMLAL => return (enc,mk_Multiply_Long (F,T,sflag,rn,rd,ra,rm))
2259 | SMULL => return (enc,mk_Multiply_Long (T,F,sflag,rn,rd,ra,rm))
2260 | SMLAL => return (enc,mk_Multiply_Long (T,T,sflag,rn,rd,ra,rm))
2261 | UMAAL => v6 (mk_Multiply_Accumulate_Accumulate (rn,rd,ra,rm))
2262 | SMLABB => return_mk_shm (mk_word2 0,F,F,rd,ra,rm,rn)
2263 | SMLATB => return_mk_shm (mk_word2 0,F,T,rd,ra,rm,rn)
2264 | SMLABT => return_mk_shm (mk_word2 0,T,F,rd,ra,rm,rn)
2265 | SMLATT => return_mk_shm (mk_word2 0,T,T,rd,ra,rm,rn)
2266 | SMLAWB => return_mk_shm (mk_word2 1,F,F,rd,ra,rm,rn)
2267 | SMLAWT => return_mk_shm (mk_word2 1,T,F,rd,ra,rm,rn)
2268 | SMLALBB => return_mk_shm (mk_word2 2,F,F,rd,ra,rm,rn)
2269 | SMLALTB => return_mk_shm (mk_word2 2,F,T,rd,ra,rm,rn)
2270 | SMLALBT => return_mk_shm (mk_word2 2,T,F,rd,ra,rm,rn)
2271 | SMLALTT => return_mk_shm (mk_word2 2,T,T,rd,ra,rm,rn)
2272 | SMLAD => v6 (mk_Signed_Multiply_Dual (rd,ra,rm,F,F,rn))
2273 | SMLADX => v6 (mk_Signed_Multiply_Dual (rd,ra,rm,F,T,rn))
2274 | SMLSD => v6 (mk_Signed_Multiply_Dual (rd,ra,rm,T,F,rn))
2275 | SMLSDX => v6 (mk_Signed_Multiply_Dual (rd,ra,rm,T,T,rn))
2276 | SMLALD => v6 (mk_Signed_Multiply_Long_Dual (rn,rd,ra,F,F,rm))
2277 | SMLALDX => v6 (mk_Signed_Multiply_Long_Dual (rn,rd,ra,F,T,rm))
2278 | SMLSLD => v6 (mk_Signed_Multiply_Long_Dual (rn,rd,ra,T,F,rm))
2279 | SMLSLDX => v6 (mk_Signed_Multiply_Long_Dual (rn,rd,ra,T,T,rm))
2280 | SMMLA => v6 (mk_Signed_Most_Significant_Multiply (rd,ra,rm,F,rn))
2281 | SMMLAR => v6 (mk_Signed_Most_Significant_Multiply (rd,ra,rm,T,rn))
2283 (rd,ra,rm,F,rn))
2285 (rd,ra,rm,T,rn))
2286 | USADA8 => v6 (mk_Unsigned_Sum_Absolute_Differences (rd,ra,rm,rn))
2298 arm_parse_register >>= (fn rn =>
2300 (fn _ => arm_parse_register >>= (fn rm => return (rd,rn,rm)))
2301 (fn _ => return (rd,rd,rn)) >>=
2302 (fn (rd,rn,rm) =>
2303 return (Encoding_Thumb2_tm,mk_Divide (u,rn,rd,rm))))))));
2312 arm_parse_register >>= (fn rn =>
2314 (fn rm => return (rd,rn,rm))
2315 (fn _ => return (rd,rd,rn)) >>=
2316 (fn (rd,rn,rm) =>
2326 return (enc,mk_Pack_Halfword (rn,rd,imm5,tbform,rm))
2331 return (enc,mk_Pack_Halfword (rm,rd,mk_word5 0,F,rn))
2333 return (enc,mk_Pack_Halfword (rn,rd,mk_word5 0,F,rm))))))));
2364 fn (ld,indx,byte,unpriv,rt,rn) =>
2385 is_R9 rn andalso 0 <= v andalso v <= 252
2387 is_R10 rn andalso 0 <= v andalso v <= 124
2389 narrow_register rn andalso ~28 <= v
2393 (is_R9 rn andalso v <= 252 orelse
2394 narrow_register rn andalso v <= 124)
2398 narrow_register rn andalso v <= 31
2401 if is_SP rn orelse ld andalso is_PC rn
2405 narrow_register rn andalso v <= 124
2427 (mk_bool indx,u,byte,w,unpriv,rn,rt,
2444 narrow_registers [rt,rn,rm] andalso
2454 (mk_bool indx,mk_bool pos,byte,w,unpriv,rn,rt,mode2)))
2465 arm_parse_register >>= (fn rn =>
2467 (fn _ => arm_parse_mode2_offset (ld,true,byte,F,rt,rn))
2471 (fn _ => arm_parse_mode2_offset (ld,false,byte,F,rt,rn))
2474 andalso (narrow_register rn orelse
2475 is_F byte andalso is_SP rn)
2483 (T,T,byte,F,F,rn,rt,
2525 arm_parse_register >>= (fn rn =>
2539 mk_Load (T,T,byte,F,T,rn,rt,mode2)
2541 mk_Store (T,T,byte,F,T,rn,rt,mode2)))
2550 (arm_parse_mode2_offset (ld,false,byte,T,rt,rn)))
2554 (mk_bool (enc = Encoding_Thumb2_tm),T,byte,F,T,rn,rt,
2577 fn (opt,indx,unpriv,rt,rn) =>
2593 val narrow_okay = q <> Wide andalso narrow_registers [rt,rn]
2619 (mk_bool indx,u,w,signed,half,unpriv,rn,rt,
2622 mk_Store_Halfword (mk_bool indx,u,w,unpriv,rn,rt,
2639 narrow_registers [rt,rn,rm] andalso
2652 rn,rt,mode3)
2655 (mk_bool indx,mk_bool pos,w,unpriv,rn,rt,mode3)))
2666 arm_parse_register >>= (fn rn =>
2668 (fn _ => arm_parse_mode3_offset (opt,true,F,rt,rn))
2672 (fn _ => arm_parse_mode3_offset (opt,false,F,rt,rn))
2675 narrow_registers [rt,rn] andalso
2687 (T,T,F,signed,half,F,rn,rt,
2691 (T,T,F,F,rn,rt,
2731 arm_parse_register >>= (fn rn =>
2746 mk_Load_Halfword (T,T,F,signed,half,T,rn,rt,mode3)
2748 mk_Store_Halfword (T,T,F,T,rn,rt,mode3)))
2782 mk_Load_Halfword (indx,add,w,signed,half,T,rn,rt,tm)
2784 mk_Store_Halfword (indx,add,w,T,rn,rt,tm))
2835 arm_parse_register >>= (fn rn =>
2844 (enc, mk_Load_Dual (T,add,wb,rn,rt,rt2,tm))
2846 (enc, mk_Store_Dual (T,add,wb,rn,rt,rt2,tm))))))
2859 (enc, mk_Load_Dual (indx,add,w,rn,rt,rt2,tm))
2861 (enc, mk_Store_Dual (indx,add,w,rn,rt,rt2,tm)))
2899 arm_parse_register >>= (fn rn =>
2911 mk_Load_Exclusive (rn,rt,mk_word8 (Int.abs (v div 4)))))
2916 return (enc, mk_Load_Exclusive (rn,rt,mk_word8 0)))))));
2927 arm_parse_register >>= (fn rn =>
2940 (rn,rd,rt,mk_word8 (Int.abs (v div 4)))))
2945 return (enc, mk_Store_Exclusive (rn,rd,rt,mk_word8 0))))))));
2956 arm_parse_register >>= (fn rn =>
2965 mk_Load_Exclusive_Doubleword (rn,rt,rt2)))
2979 arm_parse_register >>= (fn rn =>
2988 mk_Store_Exclusive_Doubleword (rn,rd,rt,rt2)))
3000 arm_parse_register >>= (fn rn =>
3004 mk_Load_Exclusive_Halfword (rn,rt)
3006 mk_Load_Exclusive_Byte (rn,rt))))));
3019 arm_parse_register >>= (fn rn =>
3023 mk_Store_Exclusive_Halfword (rn,rd,rt)
3025 mk_Store_Exclusive_Byte (rn,rd,rt)))))));
3037 arm_parse_register >>= (fn rn =>
3039 return (Encoding_ARM_tm, mk_Swap (byte,rn,rt,rt2)))))));
3163 arm_parse_register >>= (fn rn =>
3175 val n = uint_of_word rn
3185 (narrow_register rn andalso high_bits = 0 orelse
3186 is_SP rn andalso mem high_bits [0,128] andalso
3191 narrow_register rn andalso high_bits = 0 orelse
3193 is_SP rn andalso mem high_bits [0,64])
3207 mk_Load (indx,add,F,F,w,rn,singleton_list_to_reg list,
3210 mk_Store (indx,add,F,w,F,rn,singleton_list_to_reg list,
3221 mk_Load_Multiple (indx,add,F,w,rn,list)
3223 mk_Store_Multiple (indx,add,F,w,rn,list)))
3230 mk_Load_Multiple (indx,add,sys,w,rn,list)
3232 mk_Store_Multiple (indx,add,sys,w,rn,list)))))))));
3243 arm_parse_register >>= (fn rn =>
3266 mk_bool wide,rn,mode2)
3271 rn,mode2)))
3288 (mk_bool pos,mk_bool wide,rn,mode2)
3291 (mk_bool pos,rn,mode2))))))
3298 mk_Preload_Data (T,mk_bool wide,rn,
3301 mk_Preload_Instruction (T,rn,
3351 (arm_parse_register >>= (fn rn =>
3372 mk_word5 sat_imm,rd,imm5,sh,rn)))
3377 (mk_bool unsigned,mk_word5 sat_imm,rd,mk_word5 0,F,rn)))))
3394 arm_parse_register >>= (fn rn =>
3397 (mk_bool unsigned,mk_word4 sat_imm,rd,rn))))
3459 arm_parse_register >>= (fn rn =>
3461 (fn rm => return (rd,rn,rm))
3462 (fn _ => return (rd,rd,rn)) >>= (fn (rd,rn,rm) =>
3469 of SXTAB => mk_Extend_Byte (F,rn,rd,rot,rm)
3470 | UXTAB => mk_Extend_Byte (T,rn,rd,rot,rm)
3471 | SXTAB16 => mk_Extend_Byte_16 (F,rn,rd,rot,rm)
3472 | UXTAB16 => mk_Extend_Byte_16 (T,rn,rd,rot,rm)
3473 | SXTAH => mk_Extend_Halfword (F,rn,rd,rot,rm)
3474 | UXTAH => mk_Extend_Halfword (T,rn,rd,rot,rm)
3532 arm_parse_register) >>= (fn rn =>
3547 of SBFX => mk_Bit_Field_Extract (F,mk_word5 v,rd,lsb,rn)
3548 | UBFX => mk_Bit_Field_Extract (T,mk_word5 v,rd,lsb,rn)
3550 (mk_word5 (l + v),rd,lsb,rn)
3552 (mk_word5 (l + v),rd,lsb,rn)
3652 (fn rn =>
3653 return (enc,mk_Register_to_Status (spsr,mask,rn)))
3750 (arm_parse_register >>= (fn rn =>
3755 (return (enc, mk_Return_From_Exception (p,inc,w,rn)))))))));
3868 (arm_parse_register >>= (fn rn =>
3871 return (Encoding_ThumbEE_tm, mk_Check_Array (rn,rm)))))));
3932 arm_parse_register >>= (fn rn =>
3976 of LDC => mk_Coprocessor_Load (p,u,F,w,rn,crd,coproc,imm8)
3977 | LDC2 => mk_Coprocessor_Load (p,u,F,w,rn,crd,coproc,imm8)
3978 | LDCL => mk_Coprocessor_Load (p,u,T,w,rn,crd,coproc,imm8)
3979 | LDC2L => mk_Coprocessor_Load (p,u,T,w,rn,crd,coproc,imm8)
3980 | STC => mk_Coprocessor_Store (p,u,F,w,rn,crd,coproc,imm8)
3981 | STC2 => mk_Coprocessor_Store (p,u,F,w,rn,crd,coproc,imm8)
3982 | STCL => mk_Coprocessor_Store (p,u,T,w,rn,crd,coproc,imm8)
3983 | STC2L => mk_Coprocessor_Store (p,u,T,w,rn,crd,coproc,imm8)