l3-machine-code/monadic-arm/armScript.sml

318 val raise'exception_def = Def
335 val ArchVersion_def = Def
351 val HaveDSPSupport_def = Def
362 val HaveThumb2_def = Def
372 val HaveThumbEE_def = Def
407 val HaveMPExt_def = Def
428 val HaveSecurityExt_def = Def
450 val HaveVirtExt_def = Def
471 val rec'PSR_def = Def
484 val reg'PSR_def = Def
525 val write'rec'PSR_def = Def
529 val write'reg'PSR_def = Def
533 val rec'SCTLR_def = Def
553 val reg'SCTLR_def = Def
610 val write'rec'SCTLR_def = Def
614 val write'reg'SCTLR_def = Def
618 val rec'HSCTLR_def = Def
633 val reg'HSCTLR_def = Def
697 val write'rec'HSCTLR_def = Def
701 val write'reg'HSCTLR_def = Def
705 val rec'HSR_def = Def
711 val reg'HSR_def = Def
751 val write'rec'HSR_def = Def
755 val write'reg'HSR_def = Def
759 val rec'SCR_def = Def
769 val reg'SCR_def = Def
822 val write'rec'SCR_def = Def
826 val write'reg'SCR_def = Def
830 val rec'NSACR_def = Def
839 val reg'NSACR_def = Def
895 val write'rec'NSACR_def = Def
899 val write'reg'NSACR_def = Def
903 val rec'HCR_def = Def
920 val reg'HCR_def = Def
964 val write'rec'HCR_def = Def
968 val write'reg'HCR_def = Def
972 val ProcessorID_def = Def ("ProcessorID",AVar uTy,LI 0)
974 val IsExternalAbort_def = Def
1001 val IsSecure_def = Def
1032 val UnalignedSupport_def = Def
1052 val BadMode_def = Def
1067 val CurrentModeIsNotUser_def = Def
1115 val CurrentModeIsUserOrSystem_def = Def
1163 val CurrentModeIsHyp_def = Def
1210 val IntegerZeroDivideTrappingEnabled_def = Def
1238 val write'ISETSTATE_def = Def
1269 val CurrentInstrSet_def = Def
1280 val SelectInstrSet_def = Def
1318 val write'ITSTATE_def = Def
1332 val ITAdvance_def = Def
1397 val InITBlock_def = Def
1406 val LastInITBlock_def = Def
1414 val ThumbCondition_def = Def
1458 val BigEndian_def = Def
1463 val CurrentCond_def = Def
1467 val ConditionPassed_def = Def
1655 val write'SPSR_def = Def
1754 val CPSRWriteByInstr_def = Def
2869 val SPSRWriteByInstr_def = Def
3027 val RBankSelect_def = Def
3053 val RfiqBankSelect_def = Def
3063 val LookUpRName_def = Def
3121 val Rmode_def = Def
3187 val write'Rmode_def = Def
3358 val R_def = Def
3393 val write'R_def = Def
3409 val write'SP_def = Def
3415 val write'LR_def = Def
3421 val BranchTo_def = Def
3435 val PCStoreValue_def = Def
3438 val BranchWritePC_def = Def
3479 val BXWritePC_def = Def
3522 val LoadWritePC_def = Def
3537 val ALUWritePC_def = Def
3563 val ThisInstrLength_def = Def
3572 val IncPC_def = Def
3596 val TranslateAddress_def = Def
3675 val mem1_def = Def
3683 val mem_def = Def
3854 val write'mem_def = Def
4317 val BigEndianReverse_def = Def
4345 val Align_def = Def
4350 val Aligned_def = Def
4354 val AlignmentFault_def = Def
4358 val MemA_with_priv_def = Def
4566 val write'MemA_with_priv_def = Def
4692 val MemA_unpriv_def = Def
4698 val write'MemA_unpriv_def = Def
4705 val MemA_def = Def
4720 val write'MemA_def = Def
4735 val MemU_with_priv_def = Def
4970 val write'MemU_with_priv_def = Def
5086 val MemU_unpriv_def = Def
5092 val write'MemU_unpriv_def = Def
5099 val MemU_def = Def
5114 val write'MemU_def = Def
5129 val NullCheckIfThumbEE_def = Def
5302 val HighestSetBit_def = Def
5307 val CountLeadingZeroBits_def = Def
5313 val LowestSetBit_def = Def
5317 val BitCount_def = Def
5341 val SignExtendFrom_def = Def
5346 val Extend_def = Def
5351 val UInt_def = Def
5354 val SignedSatQ_def = Def
5372 val UnsignedSatQ_def = Def
5388 val SignedSat_def = Def
5397 val UnsignedSat_def = Def
5406 val LSL_C_def = Def
5420 val LSL_def = Def
5430 val LSR_C_def = Def
5443 val LSR_def = Def
5453 val ASR_C_def = Def
5466 val ASR_def = Def
5476 val ROR_C_def = Def
5488 val ROR_def = Def
5498 val RRX_C_def = Def
5506 val RRX_def = Def
5511 val DecodeImmShift_def = Def
5530 val DecodeRegShift_def = Def
5538 val Shift_C_def = Def
5566 val Shift_def = Def
5578 val ARMExpandImm_C_def = Def
5587 val ARMExpandImm_def = Def
5603 val ThumbExpandImm_C_def = Def
5646 val ExpandImm_C_def = Def
5663 val AddWithCarry_def = Def
5680 val DataProcessingALU_def = Def
5727 val ArithmeticOpcode_def = Def
5734 val ExcVectorBase_def = Def
5758 val EnterMonitorMode_def = Def
6104 val EnterHypMode_def = Def
6450 val TakeReset_def = Def
6824 val TakeUndefInstrException_def = Def
7450 val TakeSVCException_def = Def
8056 val TakeSMCException_def = Def
8186 val TakeHVCException_def = Def
8236 val TakeDataAbortException_def = Def
9047 val TakePrefetchAbortException_def = Def
9857 val TakePhysicalIRQException_def = Def
10732 val TakeVirtualIRQException_def = Def
11109 val TakePhysicalFIQException_def = Def
12110 val TakeVirtualFIQException_def = Def
12523 val TakeHypTrapException_def = Def
12550 val WriteHSR_def = Def
13003 val CallSupervisor_def = Def
13109 val CallHypervisor_def = Def
13116 val BankedRegisterAccessValid_def = Def
13210 val SPSRAccessValid_def = Def
13299 val dfn'BranchTarget_def = Def
13309 val dfn'BranchExchange_def = Def
13315 val dfn'BranchLinkExchangeImmediate_def = Def
13380 val dfn'BranchLinkExchangeRegister_def = Def
13421 val dfn'CompareBranch_def = Def
13443 val dfn'TableBranchByte_def = Def
13520 val dfn'CheckArray_def = Def
13575 val dfn'HandlerBranchLink_def = Def
13604 val dfn'HandlerBranchLinkParameter_def = Def
13641 val dfn'HandlerBranchParameter_def = Def
13660 val dfn'EnterxLeavex_def = Def
13677 val dfn'IfThen_def = Def
13702 val dfn'CountLeadingZeroes_def = Def
13716 val dfn'MoveHalfword_def = Def
13731 val DataProcessing_def = Def
13897 val DataProcessingPC_def = Def
14031 val dfn'Move_def = Def
14061 val dfn'AddSub_def = Def
14068 val dfn'TestCompareImmediate_def = Def
14090 val dfn'ArithLogicImmediate_def = Def
14118 val doRegister_def = Def
14170 val dfn'Register_def = Def
14179 val dfn'TestCompareRegister_def = Def
14188 val dfn'ShiftImmediate_def = Def
14202 val doRegisterShiftedRegister_def = Def
14261 val dfn'RegisterShiftedRegister_def = Def
14270 val dfn'ShiftRegister_def = Def
14284 val dfn'SaturatingAddSubtract_def = Def
14684 val dfn'Multiply32_def = Def
14867 val dfn'MultiplyAccumulate_def = Def
15077 val dfn'MultiplyLong_def = Def
15449 val dfn'MultiplyAccumulateAccumulate_def = Def
15500 val dfn'MultiplySubtract_def = Def
15524 val dfn'Signed16Multiply32Accumulate_def = Def
15605 val dfn'Signed16Multiply32Result_def = Def
15633 val dfn'Signed16x32Multiply32Accumulate_def = Def
15720 val dfn'Signed16x32Multiply32Result_def = Def
15749 val dfn'Signed16Multiply64Accumulate_def = Def
15811 val dfn'SignedMultiplyDual_def = Def
15934 val dfn'SignedMultiplyLongDual_def = Def
16009 val dfn'SignedMostSignificantMultiply_def = Def
16047 val dfn'SignedMostSignificantMultiplySubtract_def = Def
16089 val SignedParallelAddSub16_def = Def
16144 val dfn'SignedAddSub16_def = Def
16256 val dfn'SignedSaturatingAddSub16_def = Def
16287 val dfn'SignedHalvingAddSub16_def = Def
16304 val SignedParallelAddSub8_def = Def
16339 val dfn'SignedAddSub8_def = Def
16577 val dfn'SignedSaturatingAddSub8_def = Def
16631 val dfn'SignedHalvingAddSub8_def = Def
16651 val UnsignedParallelAddSub16_def = Def
16722 val dfn'UnsignedAddSub16_def = Def
16852 val dfn'UnsignedSaturatingAddSub16_def = Def
16884 val dfn'UnsignedHalvingAddSub16_def = Def
16901 val UnsignedParallelAddSub8_def = Def
16959 val dfn'UnsignedAddSub8_def = Def
17204 val dfn'UnsignedSaturatingAddSub8_def = Def
17258 val dfn'UnsignedHalvingAddSub8_def = Def
17278 val dfn'UnsignedSumAbsoluteDifferences_def = Def
17349 val GenerateIntegerZeroDivide_def = Def
17353 val dfn'Divide_def = Def
17410 val dfn'PackHalfword_def = Def
17463 val dfn'Saturate_def = Def
17548 val dfn'Saturate16_def = Def
17633 val dfn'ExtendByte_def = Def
17662 val dfn'ExtendByte16_def = Def
17694 val dfn'ExtendHalfword_def = Def
17723 val dfn'SelectBytes_def = Def
17863 val dfn'ByteReverse_def = Def
17876 val dfn'ByteReversePackedHalfword_def = Def
17889 val dfn'ByteReverseSignedHalfword_def = Def
17900 val dfn'ReverseBits_def = Def
17913 val dfn'BitFieldExtract_def = Def
17945 val dfn'BitFieldClearOrInsert_def = Def
18021 val dfn'LoadWord_def = Def
18259 val dfn'LoadLiteral_def = Def
18418 val dfn'LoadUnprivileged_def = Def
18632 val dfn'LoadByte_def = Def
18746 val dfn'LoadByteLiteral_def = Def
18795 val dfn'LoadByteUnprivileged_def = Def
18906 val dfn'LoadSignedByteUnprivileged_def = Def
18972 val dfn'LoadHalf_def = Def
19133 val dfn'LoadHalfLiteral_def = Def
19225 val dfn'LoadHalfUnprivileged_def = Def
19342 val dfn'LoadMultiple_def = Def
19696 val dfn'LoadMultipleExceptionReturn_def = Def
20084 val dfn'LoadMultipleUserRegisters_def = Def
20342 val dfn'LoadDual_def = Def
20438 val dfn'LoadDualLiteral_def = Def
20515 val dfn'LoadExclusive_def = Def
20649 val dfn'LoadExclusiveByte_def = Def
20768 val dfn'LoadExclusiveHalf_def = Def
20887 val dfn'LoadExclusiveDoubleword_def = Def
21090 val dfn'StoreWord_def = Def
21286 val dfn'StoreUnprivileged_def = Def
21482 val dfn'StoreByte_def = Def
21600 val dfn'StoreByteUnprivileged_def = Def
21718 val dfn'StoreHalf_def = Def
21908 val dfn'StoreHalfUnprivileged_def = Def
22053 val dfn'StoreMultiple_def = Def
22437 val dfn'StoreMultipleUserRegisters_def = Def
22760 val dfn'StoreDual_def = Def
22889 val dfn'StoreExclusive_def = Def
23045 val dfn'StoreExclusiveByte_def = Def
23187 val dfn'StoreExclusiveHalf_def = Def
23329 val dfn'StoreExclusiveDoubleword_def = Def
23548 val dfn'Swap_def = Def
23621 val doChangeProcessorState_def = Def
24040 val dfn'ChangeProcessorState_def = Def
24049 val dfn'ChangeProcessorStateT1_def = Def
24162 val dfn'HypervisorCall_def = Def
24220 val dfn'MoveToRegisterFromSpecial_def = Def
24262 val dfn'MoveToRegisterFromBankedOrSpecial_def = Def
25025 val dfn'MoveToSpecialFromImmediate_def = Def
25069 val dfn'MoveToSpecialFromRegister_def = Def
25128 val dfn'MoveToBankedOrSpecialRegister_def = Def
25971 val dfn'ReturnFromException_def = Def
26144 val dfn'SecureMonitorCall_def = Def
26255 val dfn'SupervisorCall_def = Def
26261 val dfn'StoreReturnState_def = Def
26504 val dfn'Setend_def = Def
26519 val dfn'Undefined_def = Def
26526 val dfn'Breakpoint_def = Def
26530 val dfn'Debug_def = Def
26533 val dfn'DataMemoryBarrier_def = Def
26537 val dfn'DataSynchronizationBarrier_def = Def
26541 val dfn'InstructionSynchronizationBarrier_def = Def
26545 val dfn'PreloadData_def = Def
26550 val dfn'PreloadDataLiteral_def = Def
26554 val dfn'PreloadInstruction_def = Def
26571 val Run_def = Def
27505 val Take_def = Def
27523 val Skip_def = Def
27531 val UndefinedARM_def = Def
27543 val UndefinedThumb_def = Def
27551 val DECODE_UNPREDICTABLE_def = Def
27574 val DecodeHint_def = Def
27795 val DecodeParallelAdditionSubtraction_def = Def
27921 val DecodeARM_def = Def
38178 val DecodeThumb_def = Def
41542 val DecodeThumbEE_def = Def
42206 val DecodeThumb2_def = Def
54080 val Decode_def = Def