Lines Matching refs:Call
409 Bop(Ge,Apply(Call("ArchVersion",ATy(qTy,nTy),LU),qVar"state"),
430 Bop(Ge,Apply(Call("ArchVersion",ATy(qTy,nTy),LU),qVar"state"),
465 Call("reg'PSR",F32,Var("x",CTy"PSR")))
469 Call("rec'PSR",CTy"PSR",Var("x",F32)))
518 Call("reg'SCTLR",F32,Var("x",CTy"SCTLR")))
522 Call("rec'SCTLR",CTy"SCTLR",Var("x",F32)))
562 Call("reg'HSCTLR",F32,Var("x",CTy"HSCTLR")))
566 Call("rec'HSCTLR",CTy"HSCTLR",Var("x",F32)))
582 Call("reg'HSR",F32,Var("x",CTy"HSR")))
586 Call("rec'HSR",CTy"HSR",Var("x",F32)))
613 Call("reg'SCR",F32,Var("x",CTy"SCR")))
617 Call("rec'SCR",CTy"SCR",Var("x",F32)))
642 Call("reg'NSACR",F32,Var("x",CTy"NSACR")))
646 Call("rec'NSACR",CTy"NSACR",Var("x",F32)))
689 Call("reg'HCR",F32,Var("x",CTy"HCR")))
693 Call("rec'HCR",CTy"HCR",Var("x",F32)))
705 Apply(Call("HaveSecurityExt",ATy(qTy,bTy),LU),qVar"state")),
719 Let(nVar"v",Apply(Call("ArchVersion",ATy(qTy,nTy),LU),qVar"state"),
736 Apply(Call("HaveSecurityExt",ATy(qTy,bTy),LU),qVar"state"))),
739 Mop(Not,Apply(Call("HaveVirtExt",ATy(qTy,bTy),LU),qVar"state"))),
748 (Call
754 (Call
756 Call
774 (Call
780 (Call
782 Call
799 (Call
805 (Call
807 Call
868 (Call("CurrentInstrSet",ATy(qTy,CTy"InstrSet"),LU),
872 (Call
874 Call
878 (Call("write'ISETSTATE",ATy(qTy,qTy),LW(0,2)),qVar"state"))),
880 Apply(Call("write'ISETSTATE",ATy(qTy,qTy),LW(1,2)),qVar"state")),
882 Apply(Call("write'ISETSTATE",ATy(qTy,qTy),LW(2,2)),qVar"state")),
884 Apply(Call("write'ISETSTATE",ATy(qTy,qTy),LW(3,2)),qVar"state"))])))
888 ITE(Apply(Call("HaveThumb2",ATy(qTy,bTy),LU),qVar"state"),
905 ITE(Bop(And,Apply(Call("HaveThumb2",ATy(qTy,bTy),LU),qVar"state"),
912 (Call("write'ITSTATE",ATy(qTy,qTy),LW(0,8)),qVar"state"),
914 (Call
951 (Call
953 Call("UNPREDICTABLE",CTy"exception",LS"ThumbCondition")),
977 Apply(Call("CurrentCond",ATy(qTy,F4),LU),qVar"state"),
1020 (Call
1025 (Call
1027 Call
1043 (Call
1045 Call("UNPREDICTABLE",CTy"exception",LS"SPSR")),
1053 (Call
1059 (Call
1061 Call
1087 (Call
1089 Call("UNPREDICTABLE",CTy"exception",LS"SPSR")),
1099 (Call("CurrentModeIsNotUser",ATy(qTy,PTy(bTy,qTy)),LU),
1107 Call
1113 Call
1120 Call
1126 Call
1135 Call
1140 Call
1151 Call
1158 Call
1168 Call
1177 Call
1185 (Call
1199 Call
1210 Call
1223 Call
1232 Call
1258 (Call
1273 (Call
1280 Call
1291 Call
1303 Call
1315 Call
1325 (Call
1333 (Call
1337 Call
1354 (Call
1368 (Call
1373 Call
1381 (Call
1413 (Call
1418 Call
1451 (Call
1456 Call
1464 (Call
1497 (Call
1502 Call
1535 (Call
1540 Call
1550 Call
1568 Call
1583 (Call("CurrentModeIsUserOrSystem",ATy(qTy,PTy(bTy,qTy)),LU),
1589 (Call
1591 Call
1601 (Call
1603 Call
1609 Call
1620 (Call
1622 Call
1628 Call
1640 (Call
1642 Call
1648 Call
1661 (Call
1663 Call
1672 Call
1679 (Call
1687 (Call
1690 Call
1710 (Call
1713 Call
1723 Call
1738 (Call("BadMode",ATy(qTy,bTy),Var("mode",FTy 5)),qVar"state"),
1740 (Call
1742 Call
1763 (Call
1786 (Call
1792 (Call
1798 (Call
1804 (Call
1810 (Call
1816 (Call
1828 (Call
1840 (Call
1842 Call
1851 Mop(Not,Apply(Call("IsSecure",ATy(qTy,bTy),LU),qVar"state")),
1856 (Call
1858 Call("UNPREDICTABLE",CTy"exception",LS"Rmode")),
1870 (Call
1872 Call
1877 (Call
1889 Mop(Not,Apply(Call("IsSecure",ATy(qTy,bTy),LU),qVar"state")),
1894 (Call
1896 Call("UNPREDICTABLE",CTy"exception",LS"Rmode")),
1908 (Call
1910 Call
1915 (Call
1925 (Call
1933 (Call
1936 Call
1956 (Call
1961 (Call
1972 (Call
1980 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),LW(13,4)),qVar"state"))
1987 (Call("write'R",ATy(qTy,qTy),TP[Var("value",F32),LW(13,4)]),
1992 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),LW(14,4)),qVar"state"))
1999 (Call("write'R",ATy(qTy,qTy),TP[Var("value",F32),LW(14,4)]),
2004 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),LW(15,4)),qVar"state"))
2026 (Call("CurrentInstrSet",ATy(qTy,CTy"InstrSet"),LU),
2029 (Call
2035 (Call("ArchVersion",ATy(qTy,nTy),LU),
2041 (Call
2043 Call
2048 (Call
2058 (Call("CurrentInstrSet",ATy(qTy,CTy"InstrSet"),LU),
2062 (Call
2068 (Call
2070 Call
2075 (Call
2079 (Call
2084 (Call("BranchTo",ATy(qTy,qTy),Var("address",F32)),
2086 (Call
2091 (Call
2093 Call("UNPREDICTABLE",CTy"exception",LS"BXWritePC")),
2100 ITE(Bop(Ge,Apply(Call("ArchVersion",ATy(qTy,nTy),LU),qVar"state"),
2103 (Call("BXWritePC",ATy(qTy,qTy),Var("address",F32)),qVar"state"),
2105 (Call("BranchWritePC",ATy(qTy,qTy),Var("address",F32)),
2114 Apply(Call("ArchVersion",ATy(qTy,nTy),LU),qVar"state"),
2117 (Call("CurrentInstrSet",ATy(qTy,CTy"InstrSet"),LU),
2120 (Call("BXWritePC",ATy(qTy,qTy),Var("address",F32)),qVar"state"),
2122 (Call("BranchWritePC",ATy(qTy,qTy),Var("address",F32)),
2137 (Call
2144 (Call("ThisInstrLength",ATy(qTy,nTy),LU),
2162 (Call
2168 (Call
2173 (Call
2179 (Call
2184 (Call
2189 (Call
2194 (Call
2200 (Call
2205 (Call
2210 (Call
2215 (Call
2220 (Call
2225 (Call
2230 (Call
2235 (Call
2241 (Call
2243 Call
2397 (Call
2399 Call
2428 (Call
2430 Call
2441 EQ(Var("w",BTy"N"),Call("Align",BTy"N",TP[Var("w",BTy"N"),nVar"n"])))
2449 ITB([(Call("Aligned",bTy,TP[Var("address",F32),nVar"size"]),
2465 (Call
2467 Call
2470 TP[Call("Align",F32,TP[Var("address",F32),nVar"size"]),
2475 (Call
2493 (Call
2541 ITB([(Call("Aligned",bTy,TP[Var("address",F32),nVar"size"]),
2557 (Call
2559 Call
2562 TP[Call("Align",F32,TP[Var("address",F32),nVar"size"]),
2570 (Call
2578 (Call
2588 (Call
2598 (Call
2609 (Call("CurrentModeIsNotUser",ATy(qTy,PTy(bTy,qTy)),LU),
2612 (Call
2622 (Call("CurrentModeIsNotUser",ATy(qTy,PTy(bTy,qTy)),LU),
2625 (Call
2650 Call("Align",F32,TP[Var("address",F32),nVar"size"]),
2653 ITB([(Call
2658 (Call
2675 (Call
2678 Call
2702 (Call
2760 (Call
2798 Call("Align",F32,TP[Var("address",F32),nVar"size"]),
2800 ITB([(Call("Aligned",bTy,TP[Var("v",F32),nVar"size"]),
2802 (Call
2813 (Call
2815 Call
2821 (Call
2835 (Call
2856 (Call
2866 (Call
2877 (Call("CurrentModeIsNotUser",ATy(qTy,PTy(bTy,qTy)),LU),
2880 (Call
2890 (Call("CurrentModeIsNotUser",ATy(qTy,PTy(bTy,qTy)),LU),
2893 (Call
2905 (Call("CurrentInstrSet",ATy(qTy,CTy"InstrSet"),LU),
2914 ITE(EQ(Call("Align",F32,TP[Var("v",F32),LN 4]),
2919 (Call
2922 Call
2939 (Call
2942 Call
2951 (Call
2965 (Call
2969 (Call
2976 (Call
3000 Call("HighestSetBit",iTy,Var("w",BTy"N")))))
3004 Call("CountLeadingZeroBits",nTy,Mop(Rev,Var("w",BTy"N"))))
3050 (Call
3052 Call("ASSERT",CTy"exception",LS"SignedSatQ: M < N")),
3067 (Call
3069 Call
3079 (Call
3083 (Call
3093 (Call
3104 (Call
3120 (Call
3122 Call("ASSERT",CTy"exception",LS"LSL_C")),
3132 (Call
3147 (Call
3149 Call("ASSERT",CTy"exception",LS"LSR_C")),
3159 (Call
3174 (Call
3176 Call("ASSERT",CTy"exception",LS"ASR_C")),
3186 (Call
3200 (Call
3202 Call("ASSERT",CTy"exception",LS"ROR_C")),
3212 (Call
3228 Call("RRX_C",PTy(BTy"N",bTy),TP[Var("x",BTy"N"),bVar"carry_in"])))
3268 (Call
3273 (Call
3278 (Call
3283 (Call
3287 TP[Call
3299 (Call
3310 (Call
3324 (Call
3343 (Call
3345 Call
3354 (Call
3356 Call
3365 (Call
3367 Call
3377 (Call
3391 (Call
3395 (Call
3425 Call
3429 Call
3433 Call
3437 Call
3441 Call
3445 Call
3449 Call
3453 Call
3478 (Apply(Call("HaveSecurityExt",ATy(qTy,bTy),LU),qVar"state"),
3489 (Call
3493 (Call
3563 (Call
3582 (Call
3586 (Call
3656 (Call
3678 TP[Apply(Call("HaveSecurityExt",ATy(qTy,bTy),LU),qVar"s"),
3767 (Call
3772 (Call
3797 (Call("HaveVirtExt",ATy(qTy,bTy),LU),
3801 (Call
3817 (Call
3824 (Call("HaveVirtExt",ATy(qTy,bTy),LU),
3828 (Call
3834 (Call
3851 (Call
3879 (Call
3883 (Call
3964 (Call
3972 (Call
3986 Let(qVar"s",Apply(Call("ITAdvance",ATy(qTy,qTy),LU),qVar"state"),
3999 (Call("HaveVirtExt",ATy(qTy,bTy),LU),
4003 (Call
4019 (Call
4025 (Call("HaveVirtExt",ATy(qTy,bTy),LU),
4029 (Call
4035 (Call
4052 (Call
4079 (Call
4083 (Call
4164 (Call
4172 (Call
4186 Let(qVar"s",Apply(Call("ITAdvance",ATy(qTy,qTy),LU),qVar"state"),
4209 (Call
4224 Let(qVar"s",Apply(Call("ITAdvance",ATy(qTy,qTy),LU),qVar"state"),
4235 (Call
4240 (Call
4259 (Call("HaveSecurityExt",ATy(qTy,bTy),LU),
4267 Call("IsExternalAbort",bTy,LU))),
4269 (Call
4293 (Call("HaveVirtExt",ATy(qTy,bTy),LU),qVar"s"),
4296 (Call("HaveSecurityExt",ATy(qTy,bTy),LU),
4309 (Call
4317 (Call
4340 (Call
4344 (Call
4366 (Call
4374 (Call
4468 (Call
4476 (Call
4500 (Call("HaveSecurityExt",ATy(qTy,bTy),LU),
4508 Call("IsExternalAbort",bTy,LU))),
4510 (Call
4534 (Call("HaveVirtExt",ATy(qTy,bTy),LU),qVar"s"),
4537 (Call("HaveSecurityExt",ATy(qTy,bTy),LU),
4550 (Call
4558 (Call
4581 (Call
4585 (Call
4607 (Call
4615 (Call
4709 (Call
4717 (Call
4741 (Call("HaveSecurityExt",ATy(qTy,bTy),LU),
4749 (Call
4774 (Call("HaveVirtExt",ATy(qTy,bTy),LU),
4778 (Call
4800 (Call
4808 (Call
4841 (Call
4845 (Call
4867 (Call
4875 (Call
4977 (Call
4982 Call
4989 (Call
4995 (Call
5017 (Call("write'R",ATy(qTy,qTy),TP[Var("v",F32),LW(14,4)]),
5019 (Call
5095 (Call
5098 Call
5105 (Call
5109 (Call
5129 (Call("HaveSecurityExt",ATy(qTy,bTy),LU),
5137 (Call
5162 (Call("HaveVirtExt",ATy(qTy,bTy),LU),
5166 (Call
5188 (Call
5196 (Call
5229 (Call
5233 (Call
5255 (Call
5264 (Call
5299 (Call
5307 (Call
5414 (Call
5419 Call
5426 (Call
5432 (Call
5454 (Call("write'R",ATy(qTy,qTy),TP[Var("v",F32),LW(14,4)]),
5456 (Call
5544 (Call
5548 Call
5555 (Call
5560 (Call
5580 (Call
5599 (Call("ThisInstrLength",ATy(qTy,nTy),LU),
5608 (Call
5614 (Call("CurrentCond",ATy(qTy,F4),LU),
5626 (Call
5633 (Call
5641 (Call
5657 Call
5672 (Call("CurrentModeIsHyp",ATy(qTy,PTy(bTy,qTy)),LU),qVar"state"),
5674 (Call("TakeSVCException",ATy(qTy,qTy),LU),
5677 (Apply(Call("HaveVirtExt",ATy(qTy,bTy),LU),qVar"s"),
5680 (Call("IsSecure",ATy(qTy,bTy),LU),qVar"s")),
5683 (Call
5696 (Call
5701 (Call
5712 (Call("TakeHVCException",ATy(qTy,qTy),LU),
5714 (Call
5726 (Call
5728 Call
5735 (Call
5737 Call
5745 (Call
5747 Call
5754 (Call
5756 Call
5771 (Call("IsSecure",ATy(qTy,bTy),LU),
5775 (Call
5777 Call
5785 (Call
5787 Call
5794 (Call("IsSecure",ATy(qTy,bTy),LU),
5799 (Call
5801 Call
5808 (Call
5810 Call
5825 (Call("IsSecure",ATy(qTy,bTy),LU),qVar"state")),
5834 (Call
5836 Call
5844 (Call
5846 Call
5854 (Call
5856 Call
5864 (Call
5866 Call
5874 (Call
5876 Call
5883 Apply(Call("IsSecure",ATy(qTy,bTy),LU),qVar"state"))),
5886 (Call
5888 Call
5896 (Call
5898 Call
5905 (Call
5907 Call
5954 Call("reg'FPSCR",F32,Var("x",CTy"FPSCR")))
5958 Call("rec'FPSCR",CTy"FPSCR",Var("x",F32)))
6031 (Call
6038 (Call
6040 Call
6046 (Call
6048 Call
6065 (Call
6072 (Call
6074 Call
6080 (Call
6082 Call
6142 (Call("D",ATy(qTy,F64),Bop(Div,Var("n",FTy 5),LW(2,5))),
6145 (Call("D",ATy(qTy,F64),Bop(Div,Var("n",FTy 5),LW(2,5))),
6155 (Call
6159 (Call("D",ATy(qTy,F64),Var("x",FTy 5)),
6163 (Call
6167 (Call("D",ATy(qTy,F64),Var("x",FTy 5)),
6209 (Call("IncPC",ATy(qTy,qTy),LU),
6212 (Call
6217 (Call
6226 (Call("IncPC",ATy(qTy,qTy),LU),
6229 (Call
6232 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),qVar"state"),
6235 (Call
6238 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),qVar"state"),
6246 (Call("IncPC",ATy(qTy,qTy),LU),
6249 (Call
6252 (Call("S",ATy(qTy,F32),Var("n",FTy 5)),qVar"state"),
6256 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("t",F4)),
6259 (Call
6269 (Call("IncPC",ATy(qTy,qTy),LU),
6274 (Call
6277 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
6280 (Call
6285 (Call
6290 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("t",F4)),
6294 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("t2",F4)),
6296 (Call
6300 (Call
6311 (Call("IncPC",ATy(qTy,qTy),LU),
6316 (Call
6319 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),
6323 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),qVar"s0"),
6326 (Call
6334 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("t",F4)),
6337 (Call
6341 (Call
6346 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),qVar"s0"),
6350 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("t2",F4)),
6353 (Call
6363 (Call("IncPC",ATy(qTy,qTy),LU),
6366 (Call
6370 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),
6373 (Call
6377 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
6385 (Call("IncPC",ATy(qTy,qTy),LU),
6388 (Call
6392 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),
6395 (Call
6399 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
6407 (Call("IncPC",ATy(qTy,qTy),LU),
6410 (Call
6417 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),
6421 (Call
6428 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
6438 (Call("IncPC",ATy(qTy,qTy),LU),
6441 (Call
6448 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),
6452 (Call
6456 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
6466 (Call("IncPC",ATy(qTy,qTy),LU),
6471 (Call
6474 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),
6479 (Call("write'S",ATy(qTy,qTy),Var("v",PTy(F32,FTy 5))),
6484 (Call
6487 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
6492 (Call("write'S",ATy(qTy,qTy),Var("v",PTy(F32,FTy 5))),
6501 (Call("IncPC",ATy(qTy,qTy),LU),
6504 (Call
6507 (Call
6510 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
6514 (Call
6517 (Call
6520 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
6530 (Call("IncPC",ATy(qTy,qTy),LU),
6536 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),
6539 TP[Call("FPZero64",F64,LW(0,1)),qVar"state"])]),
6548 Call
6552 Call
6555 (Call
6559 Call
6566 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
6569 TP[Call("FPZero32",F32,LW(0,1)),qVar"state"])]),
6578 Call
6582 Call
6585 (Call
6589 Call
6598 (Call("IncPC",ATy(qTy,qTy),LU),
6603 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("t",F4)),
6606 Call
6620 (Call("IncPC",ATy(qTy,qTy),LU),
6623 (Call
6625 TP[Call
6685 (Call("IncPC",ATy(qTy,qTy),LU),
6688 (Call
6691 (Call
6694 (Call("D",ATy(qTy,F64),Var("n",FTy 5)),
6697 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),
6701 (Call
6704 (Call
6707 (Call("S",ATy(qTy,F32),Var("n",FTy 5)),
6710 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
6720 (Call("IncPC",ATy(qTy,qTy),LU),
6723 (Call
6726 (Call
6729 (Call("D",ATy(qTy,F64),Var("n",FTy 5)),
6732 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),
6736 (Call
6739 (Call
6742 (Call("S",ATy(qTy,F32),Var("n",FTy 5)),
6745 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
6755 (Call("IncPC",ATy(qTy,qTy),LU),
6758 (Call
6761 (Call
6764 (Call("D",ATy(qTy,F64),Var("n",FTy 5)),
6767 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),
6771 (Call
6774 (Call
6777 (Call("S",ATy(qTy,F32),Var("n",FTy 5)),
6780 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
6790 (Call("IncPC",ATy(qTy,qTy),LU),
6793 (Call
6800 (Call("D",ATy(qTy,F64),Var("n",FTy 5)),
6803 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),
6807 (Call
6814 (Call("S",ATy(qTy,F32),Var("n",FTy 5)),
6817 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
6828 (Call("IncPC",ATy(qTy,qTy),LU),
6832 (Call
6835 (Call("D",ATy(qTy,F64),Var("n",FTy 5)),
6838 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),
6841 (Call
6844 (Call
6847 (Call
6855 (Call
6858 (Call("S",ATy(qTy,F32),Var("n",FTy 5)),
6861 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
6864 (Call
6867 (Call
6870 (Call
6884 (Call("IncPC",ATy(qTy,qTy),LU),
6887 Apply(Call("D",ATy(qTy,F64),Var("n",FTy 5)),qVar"state"),
6889 (Call
6898 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),
6901 (Call("D",ATy(qTy,F64),Var("d",FTy 5)),
6905 Apply(Call("S",ATy(qTy,F32),Var("n",FTy 5)),qVar"state"),
6907 (Call
6916 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
6919 (Call("S",ATy(qTy,F32),Var("d",FTy 5)),
6930 (Call("IncPC",ATy(qTy,qTy),LU),
6933 Apply(Call("D",ATy(qTy,F64),Var("n",FTy 5)),qVar"state"),
6935 (Call
6944 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),
6948 (Call
6953 Apply(Call("S",ATy(qTy,F32),Var("n",FTy 5)),qVar"state"),
6955 (Call
6964 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
6968 (Call
6980 (Call("IncPC",ATy(qTy,qTy),LU),
6984 (Call
6987 (Call("D",ATy(qTy,F64),Var("n",FTy 5)),
6990 (Call("D",ATy(qTy,F64),Var("m",FTy 5)),
6995 (Call
6998 (Call
7002 (Call
7011 (Call
7014 (Call
7018 (Call
7026 (Call
7032 (Call
7035 (Call("S",ATy(qTy,F32),Var("n",FTy 5)),
7038 (Call("S",ATy(qTy,F32),Var("m",FTy 5)),
7043 (Call
7046 (Call
7050 (Call
7059 (Call
7062 (Call
7066 (Call
7074 (Call
7089 TP[Call("Align",F32,TP[Var("v",F32),LN 4]),qVar"s"]),
7091 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state")),
7096 (Call("IncPC",ATy(qTy,qTy),LU),
7100 (Call
7104 (Call
7109 (Call
7114 (Call
7119 (Call
7122 (Call
7139 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
7144 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
7148 (Call("IncPC",ATy(qTy,qTy),LU),
7151 (Call
7154 (Call("S",ATy(qTy,F32),Var("d",FTy 5)),qVar"s"),
7157 Apply(Call("D",ATy(qTy,F64),Var("d",FTy 5)),qVar"s"),
7161 (Call
7164 (Call
7171 (Call("BigEndian",ATy(qTy,bTy),LU),
7174 (Call
7192 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
7196 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
7222 (Call
7257 (Call
7278 (Call
7300 (Call
7335 (Call
7339 (Call
7362 (Call("IncPC",ATy(qTy,qTy),LU),
7368 (Call
7381 (Call
7393 (Call
7409 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
7413 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
7438 (Call
7442 (Call
7464 (Call
7479 (Call
7483 (Call
7516 (Call
7520 (Call
7544 (Call("IncPC",ATy(qTy,qTy),LU),
7550 (Call
7563 (Call
7575 (Call
7588 (Call
7597 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"state"),
7598 Apply(Call("BXWritePC",ATy(qTy,qTy),Var("v",F32)),qVar"s"))))
7607 (Call("CurrentInstrSet",ATy(qTy,CTy"InstrSet"),LU),
7612 (Call
7618 (Call
7627 TP[Bop(Add,Call("Align",F32,TP[Var("v",F32),LN 4]),
7633 (Call("BranchWritePC",ATy(qTy,qTy),Var("v",F32)),
7635 (Call
7644 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"state"),
7646 (Call("BXWritePC",ATy(qTy,qTy),Var("v",F32)),
7648 (Call("CurrentInstrSet",ATy(qTy,CTy"InstrSet"),LU),
7653 (Call
7659 (Call
7669 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state"),
7674 (Call
7677 Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"s")))))
7685 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
7692 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
7698 (Call
7703 (Call
7712 (Call
7717 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
7723 (Call
7730 (Call
7736 (Call
7748 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state"),
7752 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"s"),
7759 (Call("write'ITSTATE",ATy(qTy,qTy),LW(0,8)),
7761 (Call
7766 (Call
7773 Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"s"))))))
7785 (Call
7790 (Call
7804 (Call("write'R",ATy(qTy,qTy),TP[Var("imm32",F32),LW(8,4)]),
7808 (Call
7813 (Call
7826 (Call("write'R",ATy(qTy,qTy),TP[Var("imm32",F32),LW(8,4)]),
7829 (Call
7841 (Call("CurrentModeIsHyp",ATy(qTy,PTy(bTy,qTy)),LU),
7845 (Call("TakeUndefInstrException",ATy(qTy,qTy),LU),
7848 (Call("IncPC",ATy(qTy,qTy),LU),
7850 (Call
7854 (Call("IncPC",ATy(qTy,qTy),LU),
7856 (Call
7867 (Call("IncPC",ATy(qTy,qTy),LU),
7882 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"state"),
7884 (Call("IncPC",ATy(qTy,qTy),LU),
7886 (Call
7889 Call("CountLeadingZeroBits",nTy,Var("v",F32))),
7897 (Call("IncPC",ATy(qTy,qTy),LU),
7901 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("d",F4)),
7904 (Call
7909 (Call
7930 TP[Call("Align",F32,TP[Var("v",F32),LN 4]),qVar"s"]))],
7932 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state")),
7934 Call
7942 (Call
7947 (Call("IncPC",ATy(qTy,qTy),LU),
7965 ITE(Call
8012 TP[Call("Align",F32,TP[Var("v",F32),LN 4]),qVar"s"]))],
8014 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state")),
8016 Call
8023 (Call("CurrentModeIsHyp",ATy(qTy,PTy(bTy,qTy)),LU),
8027 (Call
8032 (Call
8038 (Call
8041 Call
8054 (Call
8057 TP[Call
8070 (Call
8079 (Call
8083 Call
8090 (Call
8096 (Call("ALUWritePC",ATy(qTy,qTy),Var("result",F32)),
8107 (Call
8115 (Call
8120 (Call
8133 (Call
8140 (Call
8153 (Call
8161 (Call
8166 (Call
8179 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"state"),
8182 (Call
8192 (Call
8197 (Call
8210 (Call
8223 (Call
8237 (Call
8243 (Call
8255 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"state"),
8261 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("s",F4)),
8268 (Call
8275 (Call
8288 (Call
8302 (Call
8308 (Call
8318 (Call
8335 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
8350 (Call
8380 (Call
8407 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
8422 (Call
8452 (Call
8479 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
8488 (Call
8512 (Call
8536 (Call
8577 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
8586 (Call
8610 (Call
8634 (Call
8672 (Call
8678 (Call("IncPC",ATy(qTy,qTy),LU),
8692 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state"),
8694 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"s"),
8698 (Call
8702 (Call("IncPC",ATy(qTy,qTy),LU),
8726 (Call
8760 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state"),
8762 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"s"),
8765 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("a",F4)),qVar"s"),
8771 (Call
8775 (Call("IncPC",ATy(qTy,qTy),LU),
8804 (Call
8844 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state"),
8846 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"s"),
8849 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("dhi",F4)),qVar"s"),
8852 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("dlo",F4)),
8865 (Call
8870 (Call
8876 (Call("IncPC",ATy(qTy,qTy),LU),
8905 (Call
8981 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state"),
8987 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
8993 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("dhi",F4)),
8999 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("dlo",F4)),
9004 (Call("IncPC",ATy(qTy,qTy),LU),
9006 (Call
9010 (Call
9021 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("a",F4)),qVar"state"),
9023 (Call("IncPC",ATy(qTy,qTy),LU),
9028 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
9033 (Call
9042 (Call("write'R",ATy(qTy,qTy),Var("v",PTy(F32,F4))),
9055 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
9060 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
9067 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
9072 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
9077 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("a",F4)),qVar"s"),
9086 (Call
9091 (Call("IncPC",ATy(qTy,qTy),LU),
9115 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
9120 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
9127 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
9132 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
9136 (Call("IncPC",ATy(qTy,qTy),LU),
9138 (Call
9154 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
9159 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
9165 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
9170 (Call
9182 (Call
9187 (Call("IncPC",ATy(qTy,qTy),LU),
9211 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
9216 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
9220 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
9222 (Call("IncPC",ATy(qTy,qTy),LU),
9224 (Call
9243 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
9248 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
9255 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
9260 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
9265 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("dhi",F4)),qVar"s"),
9271 (Call
9283 (Call("IncPC",ATy(qTy,qTy),LU),
9285 (Call
9290 (Call
9306 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
9309 (Call
9313 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"state")),
9315 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
9321 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
9333 (Call
9346 (Call
9351 (Call("IncPC",ATy(qTy,qTy),LU),
9376 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state"),
9381 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
9384 (Call
9388 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"s")),
9398 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("dhi",F4)),
9403 (Call
9420 (Call("IncPC",ATy(qTy,qTy),LU),
9422 (Call
9428 (Call
9442 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("a",F4)),qVar"state")),
9444 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
9449 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
9458 (Call("IncPC",ATy(qTy,qTy),LU),
9460 (Call
9474 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("a",F4)),qVar"state"),
9478 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
9482 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
9491 (Call("IncPC",ATy(qTy,qTy),LU),
9493 (Call
9506 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state"),
9508 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"s"),
9551 (Call
9557 (Call
9576 (Call("IncPC",ATy(qTy,qTy),LU),
9597 (Call
9603 (Call
9607 (Call("IncPC",ATy(qTy,qTy),LU),
9612 (Call
9618 (Call
9629 (Call
9634 (Call("IncPC",ATy(qTy,qTy),LU),
9636 (Call
9647 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state"),
9649 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"s"),
9683 (Call
9691 (Call
9739 (Call("IncPC",ATy(qTy,qTy),LU),
9763 (Call
9771 (Call
9775 (Call("IncPC",ATy(qTy,qTy),LU),
9780 (Call
9786 (Call
9794 (Call
9808 (Call
9819 (Call
9826 (Call("IncPC",ATy(qTy,qTy),LU),
9828 (Call
9841 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state"),
9843 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"s"),
9847 Call
9849 Call
9853 Call
9856 Call
9861 Call
9863 Call
9867 Call
9870 Call
9875 Call
9877 Call
9881 Call
9884 Call
9889 Call
9891 Call
9895 Call
9898 Call
9910 (Call
9916 (Call
9938 (Call("IncPC",ATy(qTy,qTy),LU),
9964 (Call
9970 (Call
9974 (Call("IncPC",ATy(qTy,qTy),LU),
9979 (Call
9986 (Call
9997 (Call
10002 (Call("IncPC",ATy(qTy,qTy),LU),
10004 (Call
10015 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state"),
10017 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"s"),
10020 Call("UInt",iTy,EX(Var("v",F32),LN 7,LN 0,F8)),
10021 Call
10024 Call
10026 Call
10029 Call
10031 Call
10034 Call
10036 Call
10039 Call("UInt",iTy,EX(Var("v",F32),LN 7,LN 0,F8)),
10040 Call
10043 Call
10045 Call
10048 Call
10050 Call
10053 Call
10055 Call
10066 (Call
10074 (Call
10130 (Call("IncPC",ATy(qTy,qTy),LU),
10158 (Call
10166 (Call
10170 (Call("IncPC",ATy(qTy,qTy),LU),
10175 (Call
10181 (Call
10189 (Call
10203 (Call
10214 (Call
10221 (Call("IncPC",ATy(qTy,qTy),LU),
10223 (Call
10239 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("a",F4)),qVar"state")),
10241 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
10244 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"s"),
10246 (Call("IncPC",ATy(qTy,qTy),LU),
10248 (Call
10255 Call
10260 Call
10266 Call
10274 Call
10278 Call
10284 Call
10288 Call
10294 Call
10298 Call
10308 Apply(Call("TakeUndefInstrException",ATy(qTy,qTy),LU),qVar"state")))
10315 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"state"),
10318 (Call
10322 (Call("GenerateIntegerZeroDivide",ATy(qTy,qTy),LU),
10325 (Call("IncPC",ATy(qTy,qTy),LU),
10327 (Call
10334 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
10338 (Call
10345 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
10349 (Call
10355 (Call("IncPC",ATy(qTy,qTy),LU),
10357 (Call
10368 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"state"),
10371 (Call
10382 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
10389 (Call
10395 (Call("IncPC",ATy(qTy,qTy),LU),
10397 (Call
10409 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state"),
10412 (Call
10421 (Call
10426 (Call
10434 (Call
10437 Call
10443 (Call("IncPC",ATy(qTy,qTy),LU),
10459 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state"),
10464 (Call
10471 (Call
10481 (Call
10488 (Call
10500 (Call
10505 CC[Call
10509 Call
10515 (Call("IncPC",ATy(qTy,qTy),LU),
10533 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state")),
10535 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"s"),
10538 (Call
10542 (Call("IncPC",ATy(qTy,qTy),LU),
10544 (Call
10547 Call
10561 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state")),
10563 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"s"),
10566 (Call
10570 (Call("IncPC",ATy(qTy,qTy),LU),
10572 (Call
10575 Call
10580 Call
10594 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state")),
10596 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"s"),
10599 (Call
10603 (Call("IncPC",ATy(qTy,qTy),LU),
10605 (Call
10608 Call
10619 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state"),
10621 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"s"),
10623 (Call("IncPC",ATy(qTy,qTy),LU),
10625 (Call
10660 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"state"),
10662 (Call("IncPC",ATy(qTy,qTy),LU),
10664 (Call
10677 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"state"),
10679 (Call("IncPC",ATy(qTy,qTy),LU),
10681 (Call
10694 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"state"),
10696 (Call("IncPC",ATy(qTy,qTy),LU),
10698 (Call
10709 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),qVar"state"),
10711 (Call("IncPC",ATy(qTy,qTy),LU),
10713 (Call
10727 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
10733 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
10735 TP[Call
10740 (Call("IncPC",ATy(qTy,qTy),LU),
10742 (Call
10754 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state")),
10756 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("d",F4)),qVar"s"),
10758 (Call("IncPC",ATy(qTy,qTy),LU),
10760 (Call
10777 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
10782 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
10785 [(Call
10791 (Call
10795 (Call
10804 (Call
10817 (Call
10824 (Call
10830 ITE(Call
10835 (Call
10841 (Call
10845 Call
10851 (Call("IncPC",ATy(qTy,qTy),LU),
10858 (Call
10864 Call
10879 (Call
10904 (Call
10917 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),LW(15,4)),
10923 Call("Align",F32,TP[Var("v",F32),LN 4]),
10930 (Call
10934 ITE(Call
10938 (Call
10943 (Call
10946 Call
10952 (Call("IncPC",ATy(qTy,qTy),LU),
10957 (Call
10961 Call
10973 (Call
10993 (Call
11006 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
11011 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
11014 [(Call
11020 (Call
11024 (Call
11033 (Call
11046 (Call
11055 (Call
11063 (Call
11068 (Call("IncPC",ATy(qTy,qTy),LU),
11073 Call
11088 (Call
11112 (Call
11125 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
11130 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
11133 [(Call
11139 (Call
11143 (Call
11152 (Call
11162 (Call
11169 (Call
11171 TP[Call
11177 (Call("IncPC",ATy(qTy,qTy),LU),
11180 (Call
11193 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),LW(15,4)),
11199 Call("Align",F32,TP[Var("v",F32),LN 4]),
11202 (Call
11211 (Call("IncPC",ATy(qTy,qTy),LU),
11213 (Call
11215 TP[Call
11228 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
11233 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
11236 [(Call
11242 (Call
11246 (Call
11255 (Call
11265 (Call
11272 (Call
11277 (Call("IncPC",ATy(qTy,qTy),LU),
11280 (Call
11294 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
11299 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
11302 [(Call("register_form2",CTy"offset2",Var("m",F4)),
11304 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
11306 (Call
11316 (Call
11323 (Call
11328 (Call("IncPC",ATy(qTy,qTy),LU),
11331 (Call
11345 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
11350 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
11353 [(Call
11359 (Call
11363 (Call
11372 (Call
11385 (Call
11393 (Call
11401 (Call
11406 (Call("IncPC",ATy(qTy,qTy),LU),
11408 (Call
11411 Call
11417 Call
11431 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),LW(15,4)),
11437 Call("Align",F32,TP[Var("v",F32),LN 4]),
11444 (Call
11448 (Call("IncPC",ATy(qTy,qTy),LU),
11450 (Call
11454 (Call
11458 Call
11462 Call
11477 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
11482 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
11485 [(Call("register_form2",CTy"offset2",Var("m",F4)),
11487 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
11489 (Call
11502 (Call
11511 (Call
11519 (Call
11524 (Call("IncPC",ATy(qTy,qTy),LU),
11526 (Call
11529 Call
11535 Call
11550 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
11555 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
11559 Call("BitCount",nTy,Var("registers",F16)))),
11584 (Call
11622 (Call
11662 (Call
11676 (Call
11682 (Call("IncPC",ATy(qTy,qTy),LU),
11688 (Call
11693 (Call
11713 (Call("CurrentModeIsHyp",ATy(qTy,PTy(bTy,qTy)),LU),qVar"state"),
11716 (Call
11720 (Call("TakeUndefInstrException",ATy(qTy,qTy),LU),
11724 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
11728 (Call
11731 Call
11739 Call
11766 (Call
11804 (Call
11841 (Call
11857 (Call
11863 (Call
11890 (Call
11894 (Call
11897 TP[Call
11910 (Call("CurrentModeIsHyp",ATy(qTy,PTy(bTy,qTy)),LU),qVar"state"),
11913 (Call
11917 (Call("TakeUndefInstrException",ATy(qTy,qTy),LU),
11923 (Call
11925 Call
11932 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
11936 (Call
11942 Call
11947 (Call("IncPC",ATy(qTy,qTy),LU),
11975 (Call
12015 (Call
12053 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
12058 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
12061 [(Call("register_form2",CTy"offset2",Var("m",F4)),
12063 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
12065 (Call
12078 (Call
12084 (Call
12089 (Call
12095 (Call
12100 (Call("IncPC",ATy(qTy,qTy),LU),
12103 (Call
12119 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),LW(15,4)),
12127 Call("Align",F32,TP[Var("v",F32),LN 4]),
12132 Call("Align",F32,TP[Var("v",F32),LN 4]),
12136 (Call
12141 (Call
12145 (Call
12149 (Call("IncPC",ATy(qTy,qTy),LU),
12151 (Call
12162 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
12167 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
12170 (Call
12175 (Call("IncPC",ATy(qTy,qTy),LU),
12177 (Call
12188 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
12193 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
12196 (Call
12200 (Call("IncPC",ATy(qTy,qTy),LU),
12202 (Call
12213 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
12218 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
12221 (Call
12225 (Call("IncPC",ATy(qTy,qTy),LU),
12227 (Call
12238 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
12243 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
12246 (Call
12252 (Call
12255 (Call
12262 (Call("BigEndian",ATy(qTy,bTy),LU),
12265 (Call("IncPC",ATy(qTy,qTy),LU),
12267 (Call
12282 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
12287 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
12290 [(Call
12296 (Call
12300 (Call
12309 (Call
12323 (Call
12328 (Call
12334 (Call
12339 Call
12344 (Call
12352 (Call
12358 (Call
12364 (Call("IncPC",ATy(qTy,qTy),LU),
12367 (Call
12382 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
12387 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
12390 [(Call
12396 (Call
12400 (Call
12409 (Call
12423 (Call
12428 (Call
12434 (Call
12439 Call
12444 (Call
12452 (Call
12459 (Call
12466 (Call("IncPC",ATy(qTy,qTy),LU),
12469 (Call
12484 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
12489 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
12492 [(Call
12498 (Call
12502 (Call
12511 (Call
12522 (Call
12526 (Call
12534 (Call("IncPC",ATy(qTy,qTy),LU),
12537 (Call
12551 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
12556 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
12559 [(Call
12565 (Call
12569 (Call
12578 (Call
12589 (Call
12593 (Call
12601 (Call("IncPC",ATy(qTy,qTy),LU),
12604 (Call
12618 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
12623 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
12626 [(Call
12632 (Call
12636 (Call
12645 (Call
12659 (Call
12662 Call
12667 (Call
12671 (Call
12678 (Call
12683 (Call("IncPC",ATy(qTy,qTy),LU),
12686 (Call
12700 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
12705 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
12708 [(Call("register_form2",CTy"offset2",Var("m",F4)),
12710 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
12712 (Call
12726 (Call
12729 Call
12734 (Call
12738 (Call
12746 (Call
12752 (Call("IncPC",ATy(qTy,qTy),LU),
12755 (Call
12769 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
12774 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
12778 Call("BitCount",nTy,Var("registers",F16)))),
12801 Call
12811 (Call
12831 (Call
12858 (Call
12903 (Call
12914 (Call
12923 (Call("IncPC",ATy(qTy,qTy),LU),
12926 (Call
12945 (Call("CurrentModeIsHyp",ATy(qTy,PTy(bTy,qTy)),LU),qVar"state"),
12948 (Call
12952 (Call("TakeUndefInstrException",ATy(qTy,qTy),LU),
12958 (Call
12960 Call
12967 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
12971 (Call
12977 Call
12998 (Call
13027 (Call
13060 (Call("IncPC",ATy(qTy,qTy),LU),
13065 (Call
13074 (Call
13091 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
13096 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
13099 [(Call("register_form2",CTy"offset2",Var("m",F4)),
13101 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("m",F4)),
13103 (Call
13117 (Call
13122 (Call
13127 (Call
13134 (Call
13141 (Call("IncPC",ATy(qTy,qTy),LU),
13144 (Call
13157 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
13162 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
13165 (Call("IncPC",ATy(qTy,qTy),LU),
13166 ITE(Call
13170 (Call
13175 (Call
13179 (Call
13184 (Call
13195 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
13200 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
13202 (Call("IncPC",ATy(qTy,qTy),LU),
13203 ITE(Call
13207 (Call
13212 (Call
13216 (Call
13221 (Call
13232 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
13237 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
13239 (Call("IncPC",ATy(qTy,qTy),LU),
13240 ITE(Call
13244 (Call
13249 (Call
13253 (Call
13258 (Call
13270 (Call("NullCheckIfThumbEE",ATy(qTy,PTy(bTy,qTy)),Var("n",F4)),
13275 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"s"),
13277 ITE(Apply(Call("BigEndian",ATy(qTy,bTy),LU),qVar"s"),
13280 (Call
13285 (Call
13292 (Call
13297 (Call
13303 (Call("IncPC",ATy(qTy,qTy),LU),
13304 ITE(Call
13308 (Call
13312 (Call
13317 (Call
13324 Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"))
13331 Apply(Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),qVar"state"),
13333 (Call("IncPC",ATy(qTy,qTy),LU),
13337 (Call
13341 (Call
13346 (Call
13350 (Call
13356 (Call
13361 (Call
13369 (Call
13373 (Call
13378 (Call
13390 (Call("CurrentModeIsNotUser",ATy(qTy,PTy(bTy,qTy)),LU),
13393 (Call("IncPC",ATy(qTy,qTy),LU),
13466 (Call
13469 TP[Call
13483 (Call
13492 (Call
13495 Call
13507 (Call("CurrentModeIsUserOrSystem",ATy(qTy,PTy(bTy,qTy)),LU),
13511 (Call("CurrentInstrSet",ATy(qTy,CTy"InstrSet"),LU),
13515 (Call
13517 Call
13522 (Call("CurrentModeIsHyp",ATy(qTy,PTy(bTy,qTy)),LU),
13527 (Call("R",ATy(qTy,PTy(F32,qTy)),LW(14,4)),qVar"s")),
13533 (Call
13535 TP[Call("reg'PSR",F32,Var("v0",CTy"PSR")),
13543 (Call
13550 (Call
13553 Call
13558 (Call
13568 Apply(Call("HaveVirtExt",ATy(qTy,bTy),LU),qVar"state")),
13570 (Apply(Call("IsSecure",ATy(qTy,bTy),LU),qVar"state"),
13574 (Call("CurrentModeIsNotUser",ATy(qTy,PTy(bTy,qTy)),LU),
13579 (Call
13581 Call
13590 (Call("CurrentModeIsHyp",ATy(qTy,PTy(bTy,qTy)),LU),
13595 (Call
13597 Call
13601 (Call("TakeUndefInstrException",ATy(qTy,qTy),LU),
13604 (Call("CallHypervisor",ATy(qTy,qTy),Var("imm16",F16)),
13612 (Call("IncPC",ATy(qTy,qTy),LU),
13616 (Call
13622 (Call
13624 Call
13632 (Call
13634 TP[Call("reg'PSR",F32,Var("v",CTy"PSR")),
13637 (Call
13640 Call
13652 (Call("CurrentModeIsNotUser",ATy(qTy,PTy(bTy,qTy)),LU),
13657 (Call
13659 Call
13665 (Call("IncPC",ATy(qTy,qTy),LU),
13669 (Call
13676 (Call
13678 TP[Call
13686 (Call
13688 TP[Call
13696 (Call
13698 TP[Call
13706 (Call
13708 TP[Call
13716 (Call
13718 TP[Call
13726 (Call
13728 TP[Call
13736 (Call
13738 TP[Call
13746 (Call
13755 (Call
13766 (Call
13774 (Call
13785 (Call
13796 (Call
13807 (Call
13815 (Call
13821 (Call
13827 (Call
13872 (Call
13875 Call
13888 (Call
13911 (Call
13923 (Call("IncPC",ATy(qTy,qTy),LU),
13926 (Call
13931 (Call
13938 (Call
13944 (Call
13946 Call
13957 (Call("IncPC",ATy(qTy,qTy),LU),
13961 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
13964 (Call
13969 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
13973 (Call
13981 (Call
13987 (Call
13990 Call
14002 (Call("CurrentModeIsNotUser",ATy(qTy,PTy(bTy,qTy)),LU),
14007 (Call
14009 Call
14015 (Call("IncPC",ATy(qTy,qTy),LU),
14019 (Call
14030 (Call
14039 TP[Call
14052 (Call
14061 TP[Call
14074 (Call
14083 TP[Call
14096 (Call
14105 TP[Call
14118 (Call
14127 TP[Call
14140 (Call
14149 TP[Call
14162 (Call
14171 TP[Call
14181 (Call
14190 (Call
14194 (Call
14208 (Call
14212 (Call
14229 (Call
14234 (Call
14248 (Call
14253 (Call
14261 (Call
14308 (Call
14311 Call
14321 (Call
14331 (Call
14353 (Call("CurrentModeIsHyp",ATy(qTy,PTy(bTy,qTy)),LU),qVar"state"),
14356 (Call("TakeUndefInstrException",ATy(qTy,qTy),LU),qVar"s"),
14359 (Call("CurrentModeIsNotUser",ATy(qTy,PTy(bTy,qTy)),LU),
14363 (Call
14369 (Call
14371 Call
14376 (Call("R",ATy(qTy,PTy(F32,qTy)),Var("n",F4)),
14387 (Call
14392 (Call
14405 (Call
14414 (Call
14443 (Call
14448 Call
14455 (Call
14466 ITE(Apply(Call("HaveSecurityExt",ATy(qTy,bTy),LU),qVar"state"),
14468 (Call("CurrentModeIsNotUser",ATy(qTy,PTy(bTy,qTy)),LU),
14472 ITE(Apply(Call("HaveVirtExt",ATy(qTy,bTy),LU),qVar"s"),
14475 (Call("IsSecure",ATy(qTy,bTy),LU),qVar"s")),
14478 (Call
14490 (Call("TakeHypTrapException",ATy(qTy,qTy),LU),
14492 (Call
14501 (Call("IsSecure",ATy(qTy,bTy),LU),qVar"s"),
14504 (Call
14507 Call
14511 (Call
14515 (Call("TakeSMCException",ATy(qTy,qTy),LU),qVar"s"))),
14517 (Call("TakeUndefInstrException",ATy(qTy,qTy),LU),qVar"s")))))
14524 (Call
14535 (Call("CurrentModeIsHyp",ATy(qTy,PTy(bTy,qTy)),LU),qVar"state"),
14538 (Call("TakeUndefInstrException",ATy(qTy,qTy),LU),qVar"s"),
14541 (Call
14546 (Call
14552 (Call
14554 Call
14560 (Call
14562 Call
14567 (Call
14572 (Call("IsSecure",ATy(qTy,bTy),LU),
14587 (Call
14590 Call
14616 (Call
14624 (Call
14626 TP[Call
14634 (Call("IncPC",ATy(qTy,qTy),LU),
14637 (Call
14656 (Call("IncPC",ATy(qTy,qTy),LU),
14668 Apply(Call("TakeUndefInstrException",ATy(qTy,qTy),LU),qVar"state")))
14672 Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"))
14676 Close(qVar"state",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state")))
14680 Close(qVar"state",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state")))
14684 Close(qVar"state",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state")))
14688 Close(qVar"state",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state")))
14692 Close(qVar"state",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state")))
14697 Close(qVar"state",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state")))
14701 Close(qVar"state",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state")))
14706 Close(qVar"state",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state")))
14710 Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"))
14714 Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"))
14718 Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"))
14722 Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"))
14733 (Call
14737 (Call
14740 (Call("IfThen",CTy"instruction",Var("v153",PTy(F4,F4))),
14742 (Call("dfn'IfThen",ATy(qTy,qTy),Var("v153",PTy(F4,F4))),
14744 (Call
14748 (Call
14751 (Call("Undefined",CTy"instruction",Var("v155",F32)),
14753 (Call("dfn'Undefined",ATy(qTy,qTy),Var("v155",F32)),
14755 (Call("Branch",CTy"instruction",Var("v1",CTy"Branch")),
14757 [(Call("BranchExchange",CTy"Branch",Var("v2",F4)),
14759 (Call("dfn'BranchExchange",ATy(qTy,qTy),Var("v2",F4)),
14761 (Call
14765 (Call
14768 (Call
14771 (Call
14774 (Call("BranchTarget",CTy"Branch",Var("v5",F32)),
14776 (Call("dfn'BranchTarget",ATy(qTy,qTy),Var("v5",F32)),
14778 (Call("CheckArray",CTy"Branch",Var("v6",PTy(F4,F4))),
14780 (Call
14783 (Call
14787 (Call
14790 (Call
14793 (Call
14796 (Call
14800 (Call
14803 (Call
14807 (Call
14810 (Call
14814 (Call
14817 (Call("Data",CTy"instruction",Var("v12",CTy"Data")),
14819 [(Call
14823 (Call
14827 (Call
14831 (Call
14835 (Call("CountLeadingZeroes",CTy"Data",Var("v15",PTy(F4,F4))),
14837 (Call
14840 (Call
14844 (Call
14848 (Call
14852 (Call
14855 (Call
14862 (Call
14870 (Call
14877 (Call
14885 (Call
14891 (Call
14897 (Call
14903 (Call
14909 (Call
14913 (Call
14916 (Call
14921 (Call
14926 (Call("Hint",CTy"instruction",Var("v24",CTy"Hint")),
14937 (Call("Breakpoint",CTy"Hint",Var("v25",F32)),
14939 (Call("dfn'Breakpoint",ATy(qTy,qTy),Var("v25",F32)),
14941 (Call("DataMemoryBarrier",CTy"Hint",Var("v26",F4)),
14943 (Call
14946 (Call("DataSynchronizationBarrier",CTy"Hint",Var("v27",F4)),
14948 (Call
14951 (Call("Debug",CTy"Hint",Var("v28",F4)),
14953 (Call("dfn'Debug",ATy(qTy,qTy),Var("v28",F4)),
14955 (Call
14959 (Call
14962 (Call
14966 (Call
14970 (Call
14973 (Call
14976 (Call
14980 (Call
14984 (Call("Load",CTy"instruction",Var("v33",CTy"Load")),
14986 [(Call
14994 (Call
15002 (Call
15006 (Call
15010 (Call
15015 (Call
15020 (Call
15028 (Call
15036 (Call
15040 (Call
15043 (Call
15047 (Call
15050 (Call("LoadExclusiveByte",CTy"Load",Var("v40",PTy(F4,F4))),
15052 (Call
15055 (Call
15059 (Call
15062 (Call("LoadExclusiveHalf",CTy"Load",Var("v42",PTy(F4,F4))),
15064 (Call
15067 (Call
15075 (Call
15083 (Call
15087 (Call
15091 (Call
15097 (Call
15104 (Call
15107 (Call
15110 (Call
15114 (Call
15118 (Call
15122 (Call
15126 (Call
15130 (Call
15134 (Call
15139 (Call
15144 (Call
15149 (Call
15154 (Call
15160 (Call
15167 (Call("Media",CTy"instruction",Var("v53",CTy"Media")),
15169 [(Call
15173 (Call
15176 (Call
15180 (Call
15184 (Call("ByteReverse",CTy"Media",Var("v56",PTy(F4,F4))),
15186 (Call
15189 (Call
15193 (Call
15196 (Call
15200 (Call
15203 (Call
15207 (Call
15211 (Call
15215 (Call
15219 (Call
15223 (Call
15227 (Call
15233 (Call
15239 (Call("ReverseBits",CTy"Media",Var("v63",PTy(F4,F4))),
15241 (Call
15244 (Call
15250 (Call
15256 (Call
15260 (Call
15263 (Call
15267 (Call
15271 (Call
15274 (Call
15277 (Call("Multiply",CTy"instruction",Var("v68",CTy"Multiply")),
15279 [(Call
15283 (Call
15286 (Call
15290 (Call
15294 (Call
15298 (Call
15301 (Call
15307 (Call
15313 (Call
15317 (Call
15320 (Call
15324 (Call
15329 (Call
15333 (Call
15337 (Call
15341 (Call
15346 (Call
15350 (Call
15354 (Call
15358 (Call
15361 (Call
15365 (Call
15369 (Call
15373 (Call
15378 (Call
15382 (Call
15387 (Call
15391 (Call
15396 (Call("SIMD",CTy"instruction",Var("v83",CTy"SIMD")),
15398 [(Call
15402 (Call
15406 (Call
15410 (Call
15413 (Call
15417 (Call
15421 (Call
15425 (Call
15428 (Call
15432 (Call
15436 (Call
15440 (Call
15443 (Call
15447 (Call
15451 (Call
15455 (Call
15458 (Call
15462 (Call
15466 (Call
15470 (Call
15473 (Call
15477 (Call
15481 (Call
15485 (Call
15488 (Call
15492 (Call
15495 (Call("Store",CTy"instruction",Var("v97",CTy"Store")),
15497 [(Call
15503 (Call
15510 (Call
15515 (Call
15520 (Call
15528 (Call
15536 (Call
15540 (Call
15543 (Call
15547 (Call
15550 (Call
15554 (Call
15557 (Call
15561 (Call
15564 (Call
15570 (Call
15577 (Call
15582 (Call
15587 (Call
15591 (Call
15595 (Call
15599 (Call
15603 (Call
15608 (Call
15613 (Call
15619 (Call
15626 (Call("System",CTy"instruction",Var("v111",CTy"System")),
15631 (Call
15637 (Call
15644 (Call("EnterxLeavex",CTy"System",bVar"v113"),
15646 (Call("dfn'EnterxLeavex",ATy(qTy,qTy),bVar"v113"),
15648 (Call("HypervisorCall",CTy"System",Var("v114",F16)),
15650 (Call("dfn'HypervisorCall",ATy(qTy,qTy),Var("v114",F16)),
15652 (Call
15656 (Call
15659 (Call
15663 (Call
15667 (Call
15671 (Call
15674 (Call
15678 (Call
15681 (Call
15685 (Call
15688 (Call
15692 (Call
15696 (Call("SecureMonitorCall",CTy"System",Var("v121",F4)),
15698 (Call
15701 (Call("Setend",CTy"System",bVar"v122"),
15703 (Call("dfn'Setend",ATy(qTy,qTy),bVar"v122"),qVar"state")),
15704 (Call
15708 (Call
15712 (Call("SupervisorCall",CTy"System",Var("v124",F32)),
15714 (Call("dfn'SupervisorCall",ATy(qTy,qTy),Var("v124",F32)),
15716 (Call("VFP",CTy"instruction",Var("v125",CTy"VFP")),
15718 [(Call
15721 (Call
15724 (Call
15728 (Call
15732 (Call
15736 (Call
15740 (Call
15744 (Call
15747 (Call
15751 (Call
15755 (Call
15759 (Call
15764 (Call
15768 (Call
15772 (Call
15777 (Call
15782 (Call
15787 (Call
15792 (Call
15797 (Call
15802 (Call
15806 (Call
15810 (Call
15815 (Call
15820 (Call
15823 (Call
15826 (Call
15830 (Call
15834 (Call
15837 (Call
15840 (Call
15844 (Call
15847 (Call
15851 (Call
15855 (Call("vmrs",CTy"VFP",Var("v143",F4)),
15857 (Call("dfn'vmrs",ATy(qTy,qTy),Var("v143",F4)),
15859 (Call("vmsr",CTy"VFP",Var("v144",F4)),
15861 (Call("dfn'vmsr",ATy(qTy,qTy),Var("v144",F4)),
15863 (Call
15867 (Call
15871 (Call
15874 (Call
15877 (Call
15883 (Call
15890 (Call
15893 (Call
15896 (Call
15901 (Call
15906 (Call
15910 (Call
15914 (Call
15918 (Call
15927 (Call("CurrentInstrSet",ATy(qTy,CTy"InstrSet"),LU),qVar"state"),
15939 (Call
15944 TP[Call("ARM",CTy"MachineCode",Var("v",F32)),qVar"s"]))),
15947 TP[Call("BadCode",CTy"MachineCode",LS"Fetch"),qVar"state"])],
15954 (Call
15964 (Call
15971 TP[Call
15984 (Call
15987 Call
15990 Call
16001 TP[Apply(Call("ConditionPassed",ATy(qTy,bTy),LU),qVar"s"),
16013 Call("Undefined",CTy"instruction",LW(0,32)),
16023 TP[Apply(Call("ConditionPassed",ATy(qTy,bTy),LU),qVar"s"),
16025 TP[ITE(bVar"v",Call("Undefined",CTy"instruction",LW(0,32)),
16034 (Call("ThumbCondition",ATy(qTy,PTy(F4,qTy)),LU),qVar"state"),
16036 (Call
16046 (Call
16048 Call
16052 [(Call("ARM",CTy"MachineCode",Var("opc",F32)),
16055 (Call("Thumb",CTy"MachineCode",Var("opc",F16)),
16058 (Call("ThumbEE",CTy"MachineCode",Var("opc",F16)),
16061 (Call
16068 (Call("BadCode",CTy"MachineCode",sVar"x"),
16088 (Call
16094 (Call("ArchVersion",ATy(qTy,nTy),LU),
16120 Call
16133 Call
16145 Call
16159 Call
16165 Call
16167 Call
16174 (Call("Skip",ATy(qTy,CTy"instruction"),LU),qVar"s")),
16184 Call
16186 Call
16191 Call
16193 Call
16197 Call
16199 Call
16203 Call
16205 Call
16210 Call
16212 Call
16216 Call
16218 Call
16222 Call
16224 Call
16229 Call
16231 Call
16235 Call
16237 Call
16241 Call("Undefined",CTy"instruction",LW(0,32)))]),
16244 Call
16246 Call
16251 Call
16253 Call
16257 Call
16259 Call
16263 Call
16265 Call
16270 Call
16272 Call
16276 Call
16278 Call
16282 Call
16284 Call
16289 Call
16291 Call
16295 Call
16297 Call
16301 Call("Undefined",CTy"instruction",LW(0,32)))])))
16387 Call
16396 Call
16412 Call
16436 Call
16448 Call
16464 Call
16474 Call
16548 Call
16551 Call
16622 Call
16625 Call
16702 Call
16705 Call
16768 Call
16771 Call
16825 Call
16828 Call
16883 Call
16886 Call
16939 Call
16942 Call
17001 Call
17004 Call
17014 Call
17056 Call
17058 Call
17068 Call
17116 Call
17119 Call
17154 Call
17156 Call
17199 Call
17201 Call
17252 Call
17254 Call
17262 Call
17302 Call
17304 Call
17346 Call
17348 Call
17357 Call
17359 Call
17363 Call("Undefined",CTy"instruction",LW(0,32))]),
17364 TP[LF,LS"",Call("Undefined",CTy"instruction",LW(0,32))])),
17446 Call
17452 Call
17464 Call
17545 Call
17551 Call
17561 Call
17607 Call
17612 Call
17619 Call
17672 Call
17674 Call
17713 Call
17715 Call
17725 TP[LF,LS"",Call("Undefined",CTy"instruction",LW(0,32))]))],
17726 TP[LF,LS"",Call("Undefined",CTy"instruction",LW(0,32))]))))
17733 Call("ARM",CTy"MachineCode",Var("w",F32)),
17763 (Call
17826 (Call
17837 (Call
17877 (Call
17884 (Call
17893 Call
17896 Call
17905 (Call
17917 (Call
17924 (Call
17933 TP[Call
17936 Call
17972 (Call
17983 (Call
17994 (Call
18001 (Call
18010 TP[Call
18013 Call
18049 (Call
18060 (Call
18068 (Call
18072 TP[Call
18078 (Call
18086 (Call
18090 TP[Call
18096 (Call
18108 (Call
18114 (Call
18122 TP[Call
18125 Call
18136 Call
18163 (Call
18171 (Call
18187 (Call
18193 (Call
18205 Call
18220 Call
18223 Call
18237 Call
18259 (Call
18270 (Call
18285 (Call
18290 (Call
18296 TP[Call
18299 Call
18334 (Call
18342 (Call
18354 (Call
18366 (Call
18386 (Call
18394 TP[Call
18397 Call
18413 Call
18441 (Call
18452 (Call
18476 (Call
18491 (Call
18512 (Call
18527 Call
18542 Call
18545 Call
18556 Call
18586 (Call
18597 (Call
18606 (Call
18610 TP[Call
18616 (Call
18624 (Call
18627 TP[Call
18632 (Call
18661 (Call
18666 (Call
18672 TP[Call
18674 Call
18705 (Call
18713 (Call
18749 (Call
18757 (Call
18766 TP[Call
18769 Call
18853 (Call
18864 (Call
18877 (Call
18882 (Call
18888 TP[Call
18890 Call
18936 (Call
18944 (Call
18959 (Call
18964 (Call
18970 TP[Call
18973 Call
19019 (Call
19028 (Call
19036 (Call
19041 (Call
19047 Call
19049 Call
19084 (Call
19090 (Call("ArchVersion",ATy(qTy,nTy),LU),
19092 TP[Call("Undefined",CTy"instruction",LW(0,32)),
19096 (Call
19130 (Call
19135 Call
19177 (Call
19192 Call
19215 Call
19218 Call
19229 Call
19232 Call
19263 (Call
19274 (Call
19298 (Call
19331 Call
19354 Call
19357 Call
19369 Call
19372 Call
19406 (Call
19417 (Call
19439 (Call
19451 Call
19474 Call
19477 Call
19488 Call
19491 Call
19516 (Call
19526 (Call
19547 (Call
19577 Call
19580 Call
19589 Call
19592 Call
19622 (Call
19632 (Call
19656 (Call
19689 Call
19712 Call
19715 Call
19728 Call
19731 Call
19760 (Call
19771 (Call
19803 (Call
19820 Call
19837 Call
19849 Call
19852 Call
19863 Call
19866 Call
19905 (Call
19918 (Call
19929 (Call
19962 (Call
19997 Call
20014 Call
20026 Call
20029 Call
20041 Call
20044 Call
20086 (Call
20101 (Call
20112 (Call
20140 (Call
20156 Call
20173 Call
20186 Call
20189 Call
20200 Call
20203 Call
20237 (Call
20250 (Call
20261 (Call
20293 (Call
20328 Call
20345 Call
20357 Call
20360 Call
20373 Call
20376 Call
20418 (Call
20433 (Call
20444 (Call
20471 (Call
20478 (Call
20487 TP[Call
20529 (Call
20540 (Call
20581 (Call
20590 (Call
20602 Call
20617 Call
20620 Call
20651 (Call
20662 (Call
20704 (Call
20711 (Call
20720 TP[Call
20723 Call
20757 (Call
20768 (Call
20799 (Call
20806 (Call
20823 Call
20839 Call
20842 Call
20875 (Call
20886 (Call
20924 (Call
20931 (Call
20945 Call
20948 Call
20988 (Call
20999 (Call
21032 (Call
21038 (Call
21047 TP[Call
21050 Call
21088 (Call
21098 (Call
21130 (Call
21136 (Call
21145 TP[Call
21148 Call
21186 (Call
21196 (Call
21226 (Call
21232 (Call
21241 TP[Call
21244 Call
21282 (Call
21292 (Call
21326 (Call
21332 (Call
21341 TP[Call
21344 Call
21377 (Call
21387 (Call
21420 (Call
21426 (Call
21435 TP[Call
21438 Call
21471 (Call
21481 (Call
21513 (Call
21519 (Call
21528 TP[Call
21531 Call
21564 (Call
21574 (Call
21607 (Call
21613 (Call
21622 TP[Call
21625 Call
21658 (Call
21668 (Call
21705 (Call
21712 (Call
21721 TP[Call
21724 Call
21764 (Call
21775 (Call
21817 (Call
21826 (Call
21835 TP[Call
21838 Call
21879 (Call
21890 (Call
21929 (Call
21936 (Call
21945 TP[Call
21948 Call
21983 (Call
21994 (Call
22036 (Call
22045 (Call
22054 TP[Call
22057 Call
22093 (Call
22104 (Call
22148 (Call
22155 (Call
22164 TP[Call
22167 Call
22197 (Call
22208 (Call
22234 (Call
22240 (Call
22266 TP[Call
22269 Call
22300 (Call
22311 (Call
22338 (Call
22344 (Call
22367 TP[Call
22370 Call
22392 (Call
22403 (Call
22413 (Call
22418 Call
22420 Call
22450 (Call
22462 (Call
22471 (Call
22483 (Call
22493 (Call
22500 (Call
22526 (Call
22534 TP[Call
22537 Call
22560 Call
22574 (Call
22585 (Call
22610 (Call
22616 TP[Call
22619 Call
22642 Call
22649 (Call
22659 (Call
22686 (Call
22694 TP[Call
22697 Call
22720 Call
22734 (Call
22745 (Call
22771 (Call
22783 TP[Call
22786 Call
22820 (Call
22829 (Call
22840 (Call
22865 (Call
22875 TP[Call
22878 Call
22903 Call
22922 (Call
22931 (Call
22942 (Call
22951 (Call
22956 Call
22958 Call
22989 (Call
22997 (Call
23002 Call
23004 Call
23038 (Call
23044 (Call
23059 (Call
23064 (Call
23070 TP[Call
23073 Call
23102 (Call
23111 (Call
23135 (Call
23159 (Call
23176 (Call
23184 (Call
23215 (Call
23224 TP[Call
23227 Call
23239 (Call
23268 (Call
23292 Call
23295 Call
23310 Call
23313 Call
23324 Call
23327 Call
23339 Call
23342 Call
23355 (Call
23382 (Call
23386 (Call
23391 TP[Call
23393 Call
23424 (Call
23433 (Call
23457 (Call
23462 TP[Call
23464 Call
23503 (Call
23512 (Call
23536 (Call
23540 (Call
23545 TP[Call
23547 Call
23579 (Call
23588 (Call
23616 (Call
23621 TP[Call
23624 Call
23662 (Call
23671 (Call
23691 (Call
23703 TP[Call
23705 Call
23732 (Call
23740 (Call
23767 (Call
23772 (Call
23778 TP[Call
23780 Call
23810 (Call
23819 (Call
23841 (Call
23846 (Call
23852 TP[Call
23854 Call
23884 (Call
23893 (Call
23919 (Call
23924 (Call
23930 TP[Call
23933 Call
23965 (Call
23974 (Call
23992 (Call("ArchVersion",ATy(qTy,nTy),LU),
23994 TP[Call
23996 Call
24021 (Call
24031 (Call
24036 Call
24054 (Call
24058 (Call
24063 TP[Call
24065 Call
24086 (Call
24094 (Call
24110 (Call
24114 (Call
24119 TP[Call
24121 Call
24143 (Call
24151 (Call
24180 (Call
24185 (Call
24192 TP[Call
24195 Call
24233 (Call
24244 (Call
24277 (Call
24282 (Call
24289 TP[Call
24292 Call
24326 (Call
24337 (Call
24365 (Call
24370 (Call
24376 TP[Call
24379 Call
24410 (Call
24419 (Call
24450 (Call
24455 (Call
24462 TP[Call
24465 Call
24503 (Call
24514 (Call
24541 (Call
24546 (Call
24552 TP[Call
24555 Call
24589 (Call
24598 (Call
24663 (Call
24667 (Call
24672 Call
24677 (Call
24685 TP[Call("Undefined",CTy"instruction",LW(0,32)),
24706 (Call
24719 Call
24743 Call
24746 Call
24770 Call
24773 Call
24789 Call
24792 Call
24808 (Call
24839 (Call
24854 Call
24870 Call
24873 Call
24890 Call
24893 Call
24940 (Call
24951 (Call
24986 (Call
25003 Call
25006 Call
25018 Call
25021 Call
25059 (Call
25072 (Call
25083 (Call
25120 (Call
25126 (Call
25135 TP[Call
25138 Call
25173 (Call
25184 (Call
25220 (Call
25225 (Call
25232 TP[Call
25235 Call
25265 (Call
25276 (Call
25306 (Call
25312 TP[Call
25315 Call
25365 (Call
25383 (Call
25394 (Call
25424 (Call
25430 TP[Call
25471 (Call
25479 (Call
25511 (Call
25517 (Call
25525 TP[Call
25528 Call
25567 (Call
25576 (Call
25604 (Call
25609 (Call
25615 TP[Call
25617 Call
25648 (Call
25657 (Call
25688 (Call
25708 TP[Call
25711 Call
25767 (Call
25778 (Call
25806 (Call
25822 TP[Call
25824 Call
25862 (Call
25871 (Call
25902 (Call
25919 TP[Call
25922 Call
25960 (Call
25969 (Call
25997 (Call
26013 TP[Call
26015 Call
26045 (Call
26054 (Call
26085 (Call
26102 TP[Call
26105 Call
26143 (Call
26152 (Call
26180 (Call
26196 TP[Call
26198 Call
26228 (Call
26237 (Call
26265 (Call
26270 (Call
26276 TP[Call
26279 Call
26288 Call
26319 (Call
26328 (Call
26355 (Call
26368 TP[Call
26371 Call
26388 Call
26423 (Call
26447 (Call
26458 (Call
26489 (Call
26506 (Call
26521 Call
26530 Call
26533 Call
26548 Call
26551 Call
26592 (Call
26603 (Call
26636 (Call
26684 Call
26697 Call
26700 Call
26713 Call
26716 Call
26743 (Call
26767 (Call
26778 (Call
26807 (Call
26813 (Call
26855 Call
26861 Call
26864 Call
26878 Call
26881 Call
26955 (Call
26979 (Call
26990 (Call
27015 (Call
27019 (Call
27026 TP[Call
27028 Call
27067 (Call
27076 (Call
27099 (Call
27105 (Call
27141 Call
27162 Call
27165 Call
27179 Call
27182 Call
27239 (Call
27250 (Call
27275 (Call
27290 (Call
27304 Call
27325 Call
27328 Call
27343 Call
27346 Call
27371 (Call
27382 (Call
27405 (Call
27444 Call
27447 Call
27456 Call
27459 Call
27484 (Call
27493 (Call
27517 (Call
27560 Call
27581 Call
27584 Call
27597 Call
27600 Call
27625 (Call
27636 (Call
27662 (Call
27666 (Call
27672 TP[Call
27675 Call
27683 Call
27708 (Call
27717 (Call
27739 (Call
27752 TP[Call
27755 Call
27770 Call
27803 (Call
27814 (Call
27821 (Call
27831 Call("Thumb",CTy"MachineCode",Var("h",F16)),
27842 (Call
27848 (Call
27852 Call
27854 Call
27880 (Call
27894 (Call
27900 (Call
27904 Call
27906 Call
27925 (Call
27936 (Call
27940 (Call
27945 TP[Call
27947 Call
27969 (Call
27974 (Call
27982 (Call
27996 (Call
28002 (Call
28007 (Call
28013 Call
28016 Call
28037 (Call
28052 (Call
28058 (Call
28063 (Call
28069 Call
28072 Call
28093 (Call
28105 (Call
28111 (Call
28129 TP[Call
28132 Call
28140 Call
28147 (Call
28156 (Call
28177 (Call
28182 (Call
28188 TP[Call
28190 Call
28197 (Call
28213 (Call
28221 (Call
28246 (Call
28252 (Call
28265 Call
28268 Call
28297 (Call
28310 (Call
28321 (Call
28342 (Call
28348 (Call
28354 (Call
28367 Call
28370 Call
28382 Call
28385 Call
28397 Call
28400 Call
28412 Call
28417 (Call
28430 (Call
28436 (Call
28453 TP[Call
28456 Call
28465 Call
28478 (Call
28486 (Call
28493 (Call
28502 (Call
28515 (Call
28520 (Call
28526 Call
28528 Call
28541 (Call
28564 (Call
28569 (Call
28597 (Call
28602 (Call
28608 TP[Call
28625 EQ(Call
28633 (Call
28640 (Call
28648 (Call
28659 (Call
28665 (Call
28669 TP[Call
28672 Call
28692 (Call
28698 (Call
28705 (Call
28714 (Call
28720 (Call
28729 (Call
28734 (Call
28738 Call
28740 Call
28744 (Call
28765 (Call
28773 (Call
28778 (Call
28782 Call
28784 Call
28804 (Call
28811 (Call
28816 (Call
28825 TP[Call
28827 Call
28836 (Call
28856 (Call
28869 (Call
28875 (Call
28882 Call
28897 Call
28900 Call
28915 Call
28918 Call
28934 (Call
28949 (Call
28955 (Call
28962 Call
28976 Call
28979 Call
28994 Call
28997 Call
29013 (Call
29020 (Call
29034 (Call
29040 (Call
29047 Call
29062 Call
29065 Call
29080 Call
29083 Call
29099 (Call
29111 (Call
29117 (Call
29122 Call
29139 Call
29142 Call
29152 Call
29155 Call
29166 (Call
29176 (Call
29181 (Call
29192 TP[Call
29194 Call
29205 Call
29210 (Call
29219 (Call
29230 (Call
29236 (Call
29251 TP[Call
29254 Call
29272 Call
29278 (Call
29287 (Call
29300 (Call
29305 (Call
29309 Call
29321 (Call
29332 (Call
29337 (Call
29341 Call
29343 Call
29357 (Call
29364 (Call
29371 TP[Call
29373 Call
29387 (Call
29391 (Call
29399 (Call
29404 (Call
29413 (Call("ThumbCondition",ATy(qTy,PTy(F4,qTy)),LU),
29417 (Call
29421 Call
29423 Call
29431 (Call
29450 (Call
29457 (Call("ThumbCondition",ATy(qTy,PTy(F4,qTy)),LU),
29461 (Call
29465 Call
29467 Call
29475 (Call
29492 (Call
29498 (Call("ThumbCondition",ATy(qTy,PTy(F4,qTy)),LU),
29502 (Call
29508 Call
29517 Call
29519 Call
29524 (Call
29541 (Call
29559 (Call
29565 (Call
29574 TP[Call
29577 Call
29584 (Call
29606 TP[Call
29609 Call
29616 (Call
29638 TP[Call
29641 Call
29648 (Call
29670 TP[Call
29673 Call
29680 (Call
29702 TP[Call
29705 Call
29712 (Call
29734 TP[Call
29737 Call
29744 (Call
29766 TP[Call
29769 Call
29775 (Call
29785 Call
29804 TP[Call
29807 Call
29813 (Call
29823 Call
29842 TP[Call
29845 Call
29851 (Call
29861 Call
29880 TP[Call
29883 Call
29889 (Call
29907 TP[Call
29910 Call
29928 TP[Call
29931 Call
29949 TP[Call
29952 Call
29970 TP[Call
29973 Call
29979 (Call
30007 (Call
30020 (Call
30031 (Call
30038 TP[Call
30041 Call
30054 TP[Call
30057 Call
30063 (Call
30080 (Call
30097 (Call
30102 (Call
30110 (Call
30121 TP[Call
30123 Call
30143 (Call
30151 (Call
30158 (Call
30166 (Call
30179 (Call
30182 Call
30195 (Call
30200 (Call
30209 TP[Call
30211 Call
30232 (Call
30240 (Call
30255 (Call
30260 (Call
30269 (Call
30280 TP[Call
30282 Call
30295 (Call
30303 (Call
30310 (Call
30318 (Call
30331 (Call("ThumbCondition",ATy(qTy,PTy(F4,qTy)),LU),
30335 (Call
30339 TP[Call
30341 Call
30349 (Call
30355 (Call
30366 (Call
30373 (Call
30387 (Call
30392 (Call
30397 (Call
30402 TP[Call
30404 Call
30412 (Call
30418 (Call
30431 (Call
30440 (Call
30448 (Call("ThumbCondition",ATy(qTy,PTy(F4,qTy)),LU),
30452 (Call
30456 Call
30458 Call
30477 (Call
30488 (Call
30493 (Call
30498 Call
30513 Call
30516 Call
30529 Call
30532 Call
30545 Call
30548 Call
30561 Call
30564 Call
30577 Call
30580 Call
30593 Call
30596 Call
30609 Call
30612 Call
30625 Call
30628 Call
30641 (Call
30646 (Call
30655 Call("Thumb",CTy"MachineCode",Var("h",F16)),
30670 (Call
30676 (Call
30687 Call
30696 Call
30708 TP[Call
30711 Call
30729 TP[Call
30732 Call
30750 TP[Call
30753 Call
30771 TP[Call
30774 Call
30793 TP[Call
30796 Call
30816 (Call
30825 (Call
30838 (Call
30843 (Call
30847 TP[Call
30849 Call
30867 (Call
30873 (Call
30878 (Call
30887 (Call
30897 TP[Call("Undefined",CTy"instruction",LW(0,32)),
30905 (Call
30910 (Call
30914 TP[Call
30916 Call
30935 (Call
30941 (Call
30946 (Call
30954 (Call
30963 (Call
30968 (Call
30972 TP[Call
30974 Call
30994 (Call
31000 (Call
31005 (Call
31014 (Call
31025 (Call
31030 (Call
31034 Call
31036 Call
31049 Call
31059 (Call
31074 (Call
31079 (Call
31088 TP[Call
31091 Call
31104 (Call
31112 (Call
31123 (Call
31128 (Call
31132 Call
31134 Call
31143 Call
31155 (Call
31167 (Call
31172 (Call
31177 Call
31192 Call
31195 Call
31205 Call
31208 Call
31219 (Call
31224 (Call
31235 (Call
31249 Call("Thumb2",CTy"MachineCode",Var("h",PTy(F16,F16))),
31306 (Call
31316 (Call
31324 (Call
31332 TP[Call
31335 Call
31348 Call
31381 (Call
31392 (Call
31428 (Call
31438 (Call
31446 (Call
31475 Call
31478 Call
31491 Call
31494 Call
31507 Call
31510 Call
31523 Call
31556 (Call
31567 (Call
31604 (Call
31614 (Call
31622 (Call
31630 TP[Call
31706 (Call
31717 (Call
31766 (Call
31776 (Call
31784 (Call
31792 TP[Call
31795 Call
31833 (Call
31844 (Call
31885 (Call
31894 (Call
31902 (Call
31916 Call
31919 Call
31928 Call
31931 Call
31940 Call
31943 Call
31952 Call
31955 Call
31988 (Call
31999 (Call
32052 (Call
32062 (Call
32070 (Call
32078 TP[Call
32081 Call
32114 (Call
32125 (Call
32170 (Call
32179 (Call
32187 (Call
32195 TP[Call
32198 Call
32231 (Call
32242 (Call
32281 (Call
32291 (Call
32299 (Call
32337 (Call
32370 TP[Call
32373 Call
32390 TP[Call
32393 Call
32414 (Call
32429 TP[Call
32432 Call
32450 TP[Call
32453 Call
32471 TP[Call
32474 Call
32494 TP[Call
32497 Call
32517 TP[Call
32520 Call
32537 TP[Call
32540 Call
32559 TP[Call
32562 Call
32582 TP[Call
32585 Call
32607 (Call
32622 TP[Call
32625 Call
32644 TP[Call
32647 Call
32664 TP[Call
32671 (Call
32710 (Call
32720 (Call
32729 (Call
32743 TP[Call
32791 (Call
32802 (Call
32837 (Call
32847 (Call
32855 (Call
32897 Call
32900 Call
32934 Call
32937 Call
32969 Call
32972 Call
33009 Call
33012 Call
33023 Call
33065 (Call
33076 (Call
33084 (Call
33090 (Call
33122 (Call
33132 (Call
33140 (Call
33148 TP[Call
33151 Call
33184 (Call
33192 (Call
33199 (Call
33210 (Call
33227 (Call
33237 (Call
33245 (Call
33253 TP[Call
33256 Call
33270 Call
33296 (Call
33304 (Call
33311 (Call
33322 (Call
33347 (Call
33357 (Call
33365 (Call
33373 TP[Call
33376 Call
33389 Call
33412 (Call
33423 (Call
33457 (Call
33467 (Call
33485 (Call
33498 TP[Call
33501 Call
33518 Call
33547 (Call
33555 (Call
33562 (Call
33573 (Call
33613 (Call
33623 (Call
33631 (Call
33639 TP[Call
33642 Call
33656 Call
33677 (Call
33685 (Call
33699 (Call
33710 (Call
33718 (Call
33725 (Call
33778 (Call
33788 (Call
33802 (Call
33810 TP[Call
33813 Call
33823 Call
33849 (Call
33860 (Call
33888 (Call
33898 (Call
33912 (Call
33920 TP[Call
33923 Call
33932 Call
33955 (Call
33966 (Call
33997 (Call
34007 (Call
34031 (Call
34044 TP[Call
34047 Call
34064 Call
34091 (Call
34102 (Call
34125 (Call
34135 (Call
34149 (Call
34157 TP[Call
34160 Call
34170 Call
34194 (Call
34205 (Call
34213 (Call
34220 (Call
34247 (Call
34270 (Call
34276 (Call
34282 (Call
34290 TP[Call
34293 Call
34323 (Call
34334 (Call
34357 (Call
34363 (Call
34370 (Call
34379 Call
34382 Call
34391 Call
34411 (Call
34429 (Call
34435 (Call
34442 (Call
34451 Call
34454 Call
34464 Call
34484 (Call
34501 (Call
34508 (Call
34519 (Call
34526 (Call
34534 Call
34537 Call
34551 Call
34571 (Call
34608 (Call
34615 (Call
34622 (Call
34665 Call
34668 Call
34677 Call
34680 Call
34694 (Call
34705 (Call
34727 (Call
34736 (Call
34744 (Call
34754 Call
34784 Call
34787 Call
34800 Call
34803 Call
34821 (Call
34832 (Call
34860 (Call
34867 (Call
34878 (Call
34885 (Call
34893 Call
34896 Call
34910 Call
34926 (Call
34955 (Call
34961 (Call
34968 (Call
34977 Call
34980 Call
34990 Call
35006 (Call
35017 TP[Call
35041 (Call
35050 (Call
35058 (Call
35088 Call
35098 Call
35101 Call
35114 Call
35117 Call
35126 Call
35131 Call
35134 Call
35153 (Call
35164 (Call
35210 (Call
35219 (Call
35227 (Call
35261 Call
35281 Call
35284 Call
35297 Call
35300 Call
35332 (Call
35343 (Call
35386 (Call
35395 (Call
35407 (Call
35414 (Call
35422 TP[Call
35425 Call
35439 Call
35460 (Call
35471 (Call
35512 (Call
35519 (Call
35527 (Call
35536 TP[Call
35539 Call
35549 Call
35570 (Call
35581 (Call
35654 (Call
35664 (Call
35672 (Call
35688 Call
35706 Call
35709 Call
35722 Call
35725 Call
35751 (Call
35762 (Call
35770 (Call
35776 (Call
35816 (Call
35825 (Call
35839 (Call
35849 Call
35867 Call
35870 Call
35882 Call
35885 Call
35913 (Call
35924 (Call
35947 (Call
35954 (Call
35967 (Call
35994 Call
35997 Call
36006 Call
36011 Call
36014 Call
36023 Call
36036 (Call
36047 (Call
36074 (Call
36084 (Call
36108 (Call
36134 Call
36154 Call
36157 Call
36169 Call
36172 Call
36199 (Call
36210 (Call
36229 (Call
36236 (Call
36249 (Call
36259 Call
36283 Call
36286 Call
36298 Call
36301 Call
36321 (Call
36332 (Call
36340 (Call
36346 (Call
36364 (Call
36370 (Call
36375 (Call
36403 TP[Call
36406 Call
36422 Call
36452 (Call
36463 (Call
36480 (Call
36486 (Call
36491 (Call
36519 TP[Call
36522 Call
36538 Call
36568 (Call
36579 (Call
36600 (Call
36606 (Call
36612 (Call
36645 TP[Call
36648 Call
36665 Call
36691 (Call
36699 (Call
36722 (Call
36733 (Call
36755 (Call
36761 (Call
36767 (Call
36800 TP[Call
36803 Call
36820 Call
36846 (Call
36854 (Call
36877 (Call
36888 (Call
36903 (Call
36909 (Call
36920 (Call
36926 TP[Call
36929 Call
36948 (Call
36982 (Call
36991 (Call
37008 (Call
37014 (Call
37025 (Call
37033 TP[Call
37036 Call
37051 (Call
37067 (Call
37075 (Call
37103 (Call
37114 (Call
37141 (Call
37147 (Call
37153 (Call
37161 TP[Call
37164 Call
37218 (Call
37229 (Call
37253 (Call
37259 (Call
37264 (Call
37270 TP[Call
37273 Call
37306 (Call
37317 (Call
37352 (Call
37358 (Call
37365 (Call
37378 Call
37381 Call
37390 Call
37393 Call
37443 (Call
37454 (Call
37497 (Call
37504 (Call
37513 (Call
37522 TP[Call
37525 Call
37575 (Call
37586 (Call
37618 (Call
37624 (Call
37629 (Call
37635 TP[Call
37638 Call
37664 (Call
37672 (Call
37697 (Call
37708 (Call
37738 (Call
37744 (Call
37750 (Call
37762 Call
37765 Call
37772 Call
37775 Call
37805 (Call
37816 (Call
37851 (Call
37857 (Call
37864 (Call
37873 TP[Call
37876 Call
37921 (Call
37932 (Call
37963 (Call
37973 (Call
37991 (Call
38004 TP[Call
38007 Call
38026 Call
38076 (Call
38087 (Call
38113 (Call
38119 (Call
38136 (Call
38144 TP[Call
38147 Call
38199 (Call
38210 (Call
38241 (Call
38251 (Call
38269 (Call
38282 TP[Call
38285 Call
38304 Call
38354 (Call
38365 (Call
38412 (Call
38422 (Call
38430 (Call
38441 Call
38476 TP[Call
38479 Call
38510 (Call
38526 TP[Call
38529 Call
38576 (Call
38592 TP[Call
38595 Call
38637 (Call
38654 TP[Call
38657 Call
38727 (Call
38756 (Call
38772 TP[Call
38775 Call
38814 (Call
38831 TP[Call
38834 Call
38865 (Call
38881 TP[Call
38884 Call
38923 (Call
38941 TP[Call
38944 Call
38975 (Call
38991 TP[Call
38994 Call
39041 (Call
39064 TP[Call
39070 TP[Call
39073 Call
39117 (Call
39135 TP[Call
39138 Call
39166 (Call
39185 Call
39195 Call
39198 Call
39242 (Call
39258 TP[Call
39261 Call
39303 (Call
39319 TP[Call
39322 Call
39364 (Call
39382 TP[Call
39385 Call
39413 (Call
39429 TP[Call
39432 Call
39476 (Call
39492 TP[Call
39495 Call
39537 (Call
39552 TP[Call
39559 (Call
39567 (Call
39572 (Call
39600 (Call
39606 (Call
39611 (Call
39616 TP[Call
39619 Call
39660 (Call
39669 (Call
39700 (Call
39706 (Call
39711 (Call
39717 TP[Call
39720 Call
39766 (Call
39776 (Call
39807 (Call
39826 (Call
39834 (Call
39878 (Call
39888 (Call
39896 (Call
39904 TP[Call
39907 Call
39970 (Call
39998 (Call
40009 (Call
40040 (Call
40047 (Call
40052 (Call
40061 (Call
40073 TP[Call
40076 Call
40083 (Call
40121 (Call
40130 (Call
40170 (Call
40176 (Call
40181 (Call
40199 (Call
40210 TP[Call
40213 Call
40221 (Call
40232 TP[Call
40235 Call
40243 (Call
40254 TP[Call
40257 Call
40265 (Call
40278 (Call
40285 TP[Call
40292 (Call
40302 (Call
40344 (Call
40350 (Call
40355 (Call
40363 (Call
40374 TP[Call
40384 (Call
40392 (Call
40403 (Call
40411 (Call
40420 (Call
40431 Call
40436 Call
40439 Call
40455 (Call
40480 (Call
40486 (Call
40491 (Call
40496 TP[Call
40499 Call
40540 (Call
40549 (Call
40575 (Call
40581 (Call
40586 (Call
40591 TP[Call
40594 Call
40639 (Call
40648 (Call
40673 (Call
40679 (Call
40683 (Call
40688 TP[Call
40690 Call
40712 (Call
40717 (Call
40726 (Call
40748 (Call
40754 (Call
40759 (Call
40772 TP[Call
40774 Call
40785 (Call
40791 (Call
40814 (Call
40823 (Call
40844 (Call
40850 (Call
40854 (Call
40859 Call
40882 (Call
40891 (Call
40897 (Call
40902 TP[Call
40904 Call
40934 (Call
40939 (Call
40947 (Call
40961 (Call
40968 (Call
40990 (Call
41046 Call
41049 Call
41056 Call
41059 Call
41066 (Call
41074 (Call
41081 (Call
41092 (Call
41107 (Call
41113 (Call
41122 (Call
41146 (Call
41155 (Call
41163 TP[Call
41166 Call
41214 (Call
41222 (Call
41229 (Call
41240 (Call
41247 (Call
41252 (Call
41270 (Call
41276 (Call
41281 (Call
41321 TP[Call
41324 Call
41341 (Call
41356 TP[Call
41359 Call
41392 (Call
41407 TP[Call
41410 Call
41438 (Call
41453 TP[Call
41456 Call
41473 (Call
41488 TP[Call
41491 Call
41516 (Call
41531 TP[Call
41534 Call
41551 (Call
41566 TP[Call
41569 Call
41594 (Call
41608 TP[Call
41611 Call
41628 (Call
41643 TP[Call
41646 Call
41679 (Call
41693 TP[Call
41696 Call
41710 (Call
41725 TP[Call
41728 Call
41758 (Call
41773 TP[Call
41776 Call
41804 (Call
41819 TP[Call
41822 Call
41850 (Call
41864 TP[Call
41867 Call
41881 (Call
41896 TP[Call
41899 Call
41929 (Call
41944 TP[Call
41947 Call
41975 (Call
41990 TP[Call
41997 (Call
42015 (Call
42021 (Call
42025 (Call
42030 TP[Call
42032 Call
42058 (Call
42067 (Call
42084 (Call
42090 (Call
42094 (Call
42099 TP[Call
42101 Call
42127 (Call
42136 (Call
42152 (Call
42158 (Call
42162 (Call
42167 TP[Call
42169 Call
42199 (Call
42208 (Call
42243 (Call
42249 (Call
42254 (Call
42264 Call
42267 Call
42317 (Call
42327 (Call
42351 (Call
42357 (Call
42362 (Call
42375 Call
42393 Call
42396 Call
42448 (Call
42458 (Call
42479 (Call
42485 (Call
42490 (Call
42514 TP[Call
42517 Call
42567 (Call
42578 (Call
42600 (Call
42606 (Call
42611 (Call
42635 TP[Call
42638 Call
42677 (Call
42688 (Call
42695 (Call
42700 (Call
42709 [(Call("ARM",CTy"MachineCode",Var("w",F32)),
42711 (Call
42714 (Call("Thumb",CTy"MachineCode",Var("h",F16)),
42716 (Call
42719 (Call("ThumbEE",CTy"MachineCode",Var("h",F16)),
42721 (Call
42724 (Call("Thumb2",CTy"MachineCode",Var("hs",PTy(F16,F16))),
42726 (Call
42729 (Call("BadCode",CTy"MachineCode",sVar"s"),
42731 (Call
42733 Call("UNPREDICTABLE",CTy"exception",sVar"s")),qVar"state"))])))
42741 (Call("ITAdvance",ATy(qTy,qTy),LU),
42744 (Call
42748 (Call("Run",ATy(qTy,qTy),Var("v",CTy"instruction")),
42758 Call
42764 Call("EncodeARMImmediate_aux",OTy(FTy 12),TP[LW(15,4),Var("x",F32)]))
42835 [(Call("BranchTarget",CTy"Branch",Var("imm32",F32)),
42838 Call("Aligned",bTy,TP[Var("imm32",F32),LN 4]))),
42839 Call
42843 Call("BadCode",CTy"MachineCode",LS"B: bad offset"))),
42844 (Call("BranchExchange",CTy"Branch",Var("Rm",F4)),
42845 Call
42848 (Call
42858 Call
42860 Call
42864 Call("BadCode",CTy"MachineCode",LS"BL: bad offset"))),
42868 Call("Aligned",bTy,TP[Var("imm32",F32),LN 2]))),
42869 Call
42873 Call
42876 Call("BadCode",CTy"MachineCode",LS"BLX (immediate)"))),
42877 (Call("BranchLinkExchangeRegister",CTy"Branch",Var("Rm",F4)),
42878 Call
42881 (Call
42884 Call("BadCode",CTy"MachineCode",LS"CBZ")),
42885 (Call
42888 Call("BadCode",CTy"MachineCode",LS"CBZ")),
42889 (Call("CheckArray",CTy"Branch",TP[Var("Rm",F4),Var("n",F4)]),
42890 Call("BadCode",CTy"MachineCode",LS"CHKA")),
42891 (Call
42894 Call("BadCode",CTy"MachineCode",LS"HB{L}")),
42895 (Call
42898 Call("BadCode",CTy"MachineCode",LS"HBLP")),
42899 (Call
42902 Call("BadCode",CTy"MachineCode",LS"CBZ"))]))
42907 [(Call("vmrs",CTy"VFP",Var("t",F4)),
42908 Call
42911 (Call("vmsr",CTy"VFP",Var("t",F4)),
42912 Call
42915 (Call
42919 Call
42923 Call
42926 Call
42932 (Call
42935 Call
42938 Call
42942 (Call
42946 Call
42950 Call
42953 Call
42959 (Call
42964 Call
42968 Call("EncodeVFPReg",PTy(F1,F4),TP[Var("m",FTy 5),LT]),
42969 Call
42976 (Call
42981 Call("EncodeVFPReg",PTy(F1,F4),TP[Var("d",FTy 5),LT]),
42983 Call
42986 Call
42993 (Call
42996 CS(Call
43001 Call
43004 Call
43011 (LO F8,Call("BadCode",CTy"MachineCode",LS"VMOV (immediate)"))])),
43012 (Call
43016 Call
43020 Call
43023 Call
43029 (Call
43033 Call("EncodeVFPReg",PTy(F1,F4),TP[Var("n",FTy 5),LT]),
43034 Call
43039 (Call
43044 Call("EncodeVFPReg",PTy(F1,F4),TP[Var("m",FTy 5),LT]),
43045 Call
43050 (Call
43055 Call("EncodeVFPReg",PTy(F1,F4),TP[Var("m",FTy 5),LF]),
43056 Call
43061 (Call
43065 Call
43069 Call
43072 Call
43078 (Call
43082 Call
43086 Call
43089 Call
43095 (Call
43099 Call
43103 Call
43106 Call
43112 (Call
43118 Call
43122 Call
43126 Call
43129 Call
43135 (Call
43141 Call
43145 Call
43149 Call
43152 Call
43158 (Call
43164 Call
43168 Call
43172 Call
43175 Call
43181 (Call
43187 Call
43191 Call
43195 Call
43198 Call
43204 (Call
43210 Call
43214 Call
43218 Call
43229 Call
43237 (Call
43243 Call
43247 Call
43251 Call
43254 Call
43261 (Call
43267 Call
43271 Call
43275 Call
43278 Call
43285 (Call
43291 Call
43295 Call
43299 Call
43302 Call
43309 (Call
43313 ITE(Bop(Or,Mop(Not,Call("Aligned",bTy,TP[Var("imm32",F32),LN 4])),
43316 Call("BadCode",CTy"MachineCode",LS"VLDR: bad immediate"),
43318 Call
43321 Call
43327 (Call
43331 ITE(Bop(Or,Mop(Not,Call("Aligned",bTy,TP[Var("imm32",F32),LN 4])),
43334 Call("BadCode",CTy"MachineCode",LS"VSTR: bad immediate"),
43336 Call
43339 Call
43345 (Call
43350 Call
43353 Call
43359 (Call
43364 Call
43367 Call
43377 [(Call("CountLeadingZeroes",CTy"Data",TP[Var("Rd",F4),Var("Rm",F4)]),
43378 Call
43381 (Call
43384 Call
43389 (Call
43392 Call
43397 (Call
43400 Call("BadCode",CTy"MachineCode",LS"ADDW/SUBW")),
43401 (Call
43404 Call
43408 (Call
43412 Call
43417 (Call
43422 Call
43425 Call
43430 (Call
43435 Call
43438 Call
43443 (Call
43448 Call
43451 Call
43456 (Call
43460 Call("BadCode",CTy"MachineCode",LS"RegisterShiftedRegister: rrx")),
43461 (Call
43465 Call
43470 Call("EncodeRegShift",FTy 2,Var("shift_t",CTy"SRType")),
43472 (Call
43476 Call("BadCode",CTy"MachineCode",LS"ShiftRegister: rrx")),
43477 (Call
43481 Call
43486 Call("EncodeRegShift",FTy 2,Var("shift_t",CTy"SRType")),
43492 [(Call
43495 Call
43499 (Call
43504 Call
43507 Call
43512 (Call
43517 Call
43520 Call
43528 (Call
43531 Call
43537 (Call
43541 Call
43547 (Call
43551 Call
43557 (Call
43561 Call
43567 (Call
43570 Call
43574 (Call("ByteReverse",CTy"Media",TP[Var("d",F4),Var("m",F4)]),
43575 Call
43578 (Call
43581 Call
43584 (Call
43587 Call
43590 (Call("ReverseBits",CTy"Media",TP[Var("Rd",F4),Var("Rm",F4)]),
43591 Call
43594 (Call
43598 Call
43603 (Call
43606 Call
43615 [(Call("Breakpoint",CTy"Hint",Var("imm32",F32)),
43616 Call
43620 (Call("Debug",CTy"Hint",Var("option",F4)),
43621 Call
43624 (Call("DataMemoryBarrier",CTy"Hint",Var("option",F4)),
43626 Call
43629 Call("BadCode",CTy"MachineCode",LS"DataMemoryBarrier"))),
43630 (Call("DataSynchronizationBarrier",CTy"Hint",Var("option",F4)),
43632 Call
43635 Call
43637 (Call
43640 Call
43643 Call
43647 Call("ARM",CTy"MachineCode",CC[Var("c",F4),LW(52490244,28)])),
43649 Call("ARM",CTy"MachineCode",CC[Var("c",F4),LW(52490242,28)])),
43651 Call("ARM",CTy"MachineCode",CC[Var("c",F4),LW(52490243,28)])),
43653 Call("ARM",CTy"MachineCode",CC[Var("c",F4),LW(52490241,28)])),
43654 (Call
43657 Call("immediate_form1",CTy"offset1",Var("imm32",F32))]),
43658 Call
43663 (Call
43666 Call
43671 Call
43674 Call
43680 Call("BadCode",CTy"MachineCode",LS"PreloadData"))),
43681 (Call
43684 Call
43688 Call("BadCode",CTy"MachineCode",LS"PreloadDataLiteral"))),
43689 (Call
43692 Call("immediate_form1",CTy"offset1",Var("imm32",F32))]),
43694 Call
43698 Call("BadCode",CTy"MachineCode",LS"PreloadInstruction"))),
43699 (Call
43702 Call
43706 Call
43709 Call
43718 [(Call("EnterxLeavex",CTy"System",bVar"is_enterx"),
43719 Call("BadCode",CTy"MachineCode",LS"EnterxLeavex")),
43720 (Call
43723 Call("BadCode",CTy"MachineCode",LS"ChangeProcessorState")),
43724 (Call
43734 Call
43742 Call("BadCode",CTy"MachineCode",LS"ChangeProcessorState"))),
43744 Call("ARM",CTy"MachineCode",CC[Var("c",F4),LW(23068782,28)])),
43745 (Call("HypervisorCall",CTy"System",Var("imm16",F16)),
43746 Call
43750 (Call
43753 Call
43757 (Call
43760 Call
43765 (Call
43768 CS(Call("EncodeARMImmediate",OTy(FTy 12),Var("imm32",F32)),
43770 Call
43775 Call
43777 (Call
43780 Call
43784 (Call
43787 Call
43792 (Call
43797 Call
43804 Call("BadCode",CTy"MachineCode",LS"ReturnFromException"))),
43805 (Call("SecureMonitorCall",CTy"System",Var("imm4",F4)),
43806 Call
43809 (Call
43815 Call
43822 Call("BadCode",CTy"MachineCode",LS"StoreReturnState"))),
43823 (Call("SupervisorCall",CTy"System",Var("imm32",F32)),
43824 Call
43827 (Call("Setend",CTy"System",bVar"E"),
43829 Call
43832 Call("BadCode",CTy"MachineCode",LS"Setend")))]))
43837 [(Call
43841 Call
43845 (Call
43848 Call
43852 (Call
43856 Call
43862 (Call
43865 Call
43869 (Call
43872 Call
43876 (Call
43880 Call
43885 (Call
43889 Call
43894 (Call
43898 Call
43902 (Call
43905 Call
43909 (Call
43913 Call
43918 (Call
43922 Call
43927 (Call
43931 Call
43936 (Call
43940 Call
43945 (Call
43949 Call
43958 [(Call
43961 Call
43965 (Call
43968 Call
43972 (Call
43975 Call
43979 (Call
43982 Call
43986 (Call
43989 Call
43993 (Call
43996 Call
44000 (Call
44003 Call
44007 (Call
44010 Call
44014 (Call
44017 Call
44021 (Call
44024 Call
44028 (Call
44031 Call
44035 (Call
44038 Call
44042 (Call
44045 Call
44053 [(Call
44056 Call("BadCode",CTy"MachineCode",LS"LoadWord")),
44057 (Call
44060 Call("immediate_form1",CTy"offset1",Var("imm32",F32))]),
44062 Call
44069 Call("BadCode",CTy"MachineCode",LS"LoadWord"))),
44070 (Call
44073 Call
44077 Call
44080 Call
44087 (Call
44091 Call
44095 Call("BadCode",CTy"MachineCode",LS"LoadLiteral"))),
44096 (Call
44099 Call("immediate_form1",CTy"offset1",Var("imm32",F32))]),
44101 Call
44106 Call("BadCode",CTy"MachineCode",LS"LoadUnprivileged"))),
44107 (Call
44110 Call
44115 Call
44118 Call
44123 Call("BadCode",CTy"MachineCode",LS"LoadUnprivileged"))),
44124 (Call
44127 Call("BadCode",CTy"MachineCode",LS"LoadByte")),
44128 (Call
44132 Call("immediate_form1",CTy"offset1",Var("imm32",F32))]),
44139 Call
44146 Call
44153 Call("BadCode",CTy"MachineCode",LS"LoadByte")))))),
44154 (Call
44158 Call
44162 Call
44170 Call
44181 Call
44187 Call("BadCode",CTy"MachineCode",LS"LoadByte"))))))),
44188 (Call
44194 Call
44200 Call
44205 Call("BadCode",CTy"MachineCode",LS"LoadByteLiteral")))),
44206 (Call
44209 Call("immediate_form1",CTy"offset1",Var("imm32",F32))]),
44211 Call
44216 Call("BadCode",CTy"MachineCode",LS"LoadByteUnprivileged"))),
44217 (Call
44220 Call
44225 Call
44228 Call
44233 Call("BadCode",CTy"MachineCode",LS"LoadByteUnprivileged"))),
44234 (Call
44237 Call("immediate_form2",CTy"offset2",Var("imm32",F32))]),
44239 Call
44245 Call
44247 (Call
44250 Call("register_form2",CTy"offset2",Var("Rm",F4))]),
44252 Call
44256 Call
44258 (Call
44261 Call("BadCode",CTy"MachineCode",LS"LoadHalf")),
44262 (Call
44266 Call("immediate_form1",CTy"offset1",Var("imm32",F32))]),
44268 Call
44277 Call("BadCode",CTy"MachineCode",LS"LoadHalf"))),
44278 (Call
44282 Call
44288 Call
44295 Call("BadCode",CTy"MachineCode",LS"LoadHalf"))),
44296 (Call
44300 Call
44306 Call("BadCode",CTy"MachineCode",LS"LoadHalfLiteral"))),
44307 (Call
44311 Call("immediate_form2",CTy"offset2",Var("imm32",F32))]),
44313 Call
44320 Call("BadCode",CTy"MachineCode",LS"LoadHalfUnprivileged"))),
44321 (Call
44325 Call("register_form2",CTy"offset2",Var("Rm",F4))]),
44327 Call
44333 Call("BadCode",CTy"MachineCode",LS"LoadHalfUnprivileged"))),
44334 (Call
44338 Call
44344 (Call
44348 Call
44357 (Call
44361 Call
44369 (Call
44373 Call("immediate_form2",CTy"offset2",Var("imm32",F32))]),
44376 Call
44384 Call("BadCode",CTy"MachineCode",LS"LoadDual"))),
44385 (Call
44389 Call("register_form2",CTy"offset2",Var("Rm",F4))]),
44391 Call
44397 Call("BadCode",CTy"MachineCode",LS"LoadDual"))),
44398 (Call
44403 Call
44408 Call("BadCode",CTy"MachineCode",LS"LoadDualLiteral"))),
44409 (Call
44413 Call
44417 Call("BadCode",CTy"MachineCode",LS"LoadExclusive"))),
44418 (Call("LoadExclusiveByte",CTy"Load",TP[Var("Rt",F4),Var("Rn",F4)]),
44419 Call
44422 (Call("LoadExclusiveHalf",CTy"Load",TP[Var("Rt",F4),Var("Rn",F4)]),
44423 Call
44426 (Call
44430 Call
44434 Call("BadCode",CTy"MachineCode",LS"LoadExclusiveDoubleword")))]))
44439 [(Call
44442 Call("BadCode",CTy"MachineCode",LS"StoreWord")),
44443 (Call
44446 Call("immediate_form1",CTy"offset1",Var("imm32",F32))]),
44448 Call
44455 Call("BadCode",CTy"MachineCode",LS"StoreWord"))),
44456 (Call
44459 Call
44463 Call
44466 Call
44473 (Call
44476 Call("immediate_form1",CTy"offset1",Var("imm32",F32))]),
44478 Call
44483 Call("BadCode",CTy"MachineCode",LS"StoreUnprivileged"))),
44484 (Call
44487 Call
44492 Call
44495 Call
44500 Call("BadCode",CTy"MachineCode",LS"StoreUnprivileged"))),
44501 (Call
44504 Call("BadCode",CTy"MachineCode",LS"StoreByte")),
44505 (Call
44508 Call("immediate_form1",CTy"offset1",Var("imm32",F32))]),
44510 Call
44517 Call("BadCode",CTy"MachineCode",LS"StoreByte"))),
44518 (Call
44521 Call
44525 Call
44528 Call
44535 (Call
44538 Call("immediate_form1",CTy"offset1",Var("imm32",F32))]),
44540 Call
44545 Call("BadCode",CTy"MachineCode",LS"StoreByteUnprivileged"))),
44546 (Call
44549 Call
44554 Call
44557 Call
44562 Call("BadCode",CTy"MachineCode",LS"StoreByteUnprivileged"))),
44563 (Call
44566 Call("BadCode",CTy"MachineCode",LS"StoreHalf")),
44567 (Call
44570 Call("immediate_form1",CTy"offset1",Var("imm32",F32))]),
44572 Call
44580 Call("BadCode",CTy"MachineCode",LS"StoreHalf"))),
44581 (Call
44584 Call
44590 Call
44596 Call("BadCode",CTy"MachineCode",LS"StoreHalf"))),
44597 (Call
44600 Call("immediate_form2",CTy"offset2",Var("imm32",F32))]),
44602 Call
44608 Call("BadCode",CTy"MachineCode",LS"StoreHalfUnprivileged"))),
44609 (Call
44612 Call("register_form2",CTy"offset2",Var("Rm",F4))]),
44614 Call
44618 Call("BadCode",CTy"MachineCode",LS"StoreHalfUnprivileged"))),
44619 (Call
44623 Call
44629 (Call
44633 Call
44641 (Call
44645 Call("immediate_form2",CTy"offset2",Var("imm32",F32))]),
44648 Call
44656 Call("BadCode",CTy"MachineCode",LS"StoreDual"))),
44657 (Call
44661 Call("register_form2",CTy"offset2",Var("Rm",F4))]),
44663 Call
44669 Call("BadCode",CTy"MachineCode",LS"StoreDual"))),
44670 (Call
44674 Call
44678 Call("BadCode",CTy"MachineCode",LS"StoreExclusive"))),
44679 (Call
44682 Call
44686 (Call
44689 Call
44693 (Call
44697 Call
44701 Call("BadCode",CTy"MachineCode",LS"StoreExclusiveDoubleword")))]))
44706 [(Call("Branch",CTy"instruction",Var("b",CTy"Branch")),
44707 Call
44710 (Call("Data",CTy"instruction",Var("d",CTy"Data")),
44711 Call("e_data",CTy"MachineCode",TP[Var("c",F4),Var("d",CTy"Data")])),
44712 (Call("Load",CTy"instruction",Var("l",CTy"Load")),
44713 Call("e_load",CTy"MachineCode",TP[Var("c",F4),Var("l",CTy"Load")])),
44714 (Call("Store",CTy"instruction",Var("s",CTy"Store")),
44715 Call
44717 (Call("Multiply",CTy"instruction",Var("m",CTy"Multiply")),
44718 Call
44721 (Call("Media",CTy"instruction",Var("m",CTy"Media")),
44722 Call
44724 (Call("SIMD",CTy"instruction",Var("m",CTy"SIMD")),
44725 Call("e_simd",CTy"MachineCode",TP[Var("c",F4),Var("m",CTy"SIMD")])),
44726 (Call("System",CTy"instruction",Var("s",CTy"System")),
44727 Call
44730 (Call("Hint",CTy"instruction",Var("h",CTy"Hint")),
44731 Call("e_hint",CTy"MachineCode",TP[Var("c",F4),Var("h",CTy"Hint")])),
44732 (Call("VFP",CTy"instruction",Var("v",CTy"VFP")),
44733 Call("e_vfp",CTy"MachineCode",TP[Var("c",F4),Var("v",CTy"VFP")])),
44734 (Call
44737 Call("BadCode",CTy"MachineCode",LS"IfThen")),
44738 (Call
44741 Call("BadCode",CTy"MachineCode",LS"Divide")),
44744 Call("ARM",CTy"MachineCode",LW(4118802463,32)),
44745 Call("BadCode",CTy"MachineCode",LS"ClearExclusive"))),
44746 (Call
44749 Call
44753 (Call("Undefined",CTy"instruction",Var("imm32",F32)),
44754 Call
44759 Call("ARM",CTy"MachineCode",CC[Var("c",F4),LW(52490240,28)]))]))