arm8/model/arm8Script.sml

352   [("instruction",
2486   ("Run",Var("v0",CTy"instruction"),
2489       CS(Var("v0",CTy"instruction"),
2490          [(Const("Reserved",CTy"instruction"),
2492           (Const("Unallocated",CTy"instruction"),
2495              ("Address",CTy"instruction",
2501           (Call("ClearExclusive",CTy"instruction",Var("v82",F4)),
2505           (Call("Hint",CTy"instruction",Var("v83",CTy"SystemHintOp")),
2510              ("MemoryBarrier",CTy"instruction",
2516           (Call("Branch",CTy"instruction",Var("v1",CTy"Branch")),
2570           (Call("CRCExt",CTy"instruction",Var("v9",CTy"CRCExt")),
2608           (Call("Data",CTy"instruction",Var("v14",CTy"Data")),
3129           (Call("Debug",CTy"instruction",Var("v51",CTy"Debug")),
3145           (Call("LoadStore",CTy"instruction",Var("v55",CTy"LoadStore")),
3593           (Call("System",CTy"instruction",Var("v74",CTy"System")),
3655    Call("Hint",CTy"instruction",LC("SystemHintOp_NOP",CTy"SystemHintOp")))
3665           ("LoadStore",CTy"instruction",
3674           ("LoadStore",CTy"instruction",
3683           ("LoadStore",CTy"instruction",
3692           ("LoadStore",CTy"instruction",
3709           ("LoadStore",CTy"instruction",
3719           ("LoadStore",CTy"instruction",
3729           ("LoadStore",CTy"instruction",
3739           ("LoadStore",CTy"instruction",
3771                     ("LoadStoreImmediateN",CTy"instruction",
3779                     ("LoadStoreImmediateN",CTy"instruction",
3785                  (LW(2,2),Const("Unallocated",CTy"instruction")),
3786                  (LW(3,2),Const("NoOperation",CTy"instruction"))])),
3795                     ("LoadStoreImmediateN",CTy"instruction",
3803                     ("LoadStoreImmediateN",CTy"instruction",
3809                  (LW(2,2),Const("Unallocated",CTy"instruction")),
3810                  (LW(3,2),Const("NoOperation",CTy"instruction"))]))],
3812              ("LoadStoreImmediateN",CTy"instruction",
3827          ("LoadStore",CTy"instruction",
3836          ("LoadStore",CTy"instruction",
3859                 ("LoadStorePairN",CTy"instruction",
3866                 ("LoadStorePairN",CTy"instruction",
3871              (LW(2,2),Const("Unallocated",CTy"instruction")),
3872              (LW(3,2),Const("NoOperation",CTy"instruction"))])),
3882                 ("LoadStorePairN",CTy"instruction",
3889                 ("LoadStorePairN",CTy"instruction",
3894              (LW(2,2),Const("Unallocated",CTy"instruction")),
3895              (LW(3,2),Const("NoOperation",CTy"instruction"))])),
3901                 ("LoadStorePairN",CTy"instruction",
3906              (LW(1,2),Const("Unallocated",CTy"instruction")),
3907              (AVar(FTy 2),Const("NoOperation",CTy"instruction"))]))],
3909          ("LoadStorePairN",CTy"instruction",
3924              ("LoadStore",CTy"instruction",
3932              ("LoadStore",CTy"instruction",
3942               ("LoadStore",CTy"instruction",
3951               ("LoadStore",CTy"instruction",
3960               ("LoadStore",CTy"instruction",
3969               ("LoadStore",CTy"instruction",
3983           Var("ast",OTy(CTy"instruction"))],
3988               [(LW(0,2),TP[LT,LF,LO(CTy"instruction")]),
3990                 TP[LF,LF,Mop(Some,Const("Unallocated",CTy"instruction"))]),
3992                 TP[LF,LF,Mop(Some,Const("NoOperation",CTy"instruction"))])]),
3993            TP[LF,LF,LO(CTy"instruction")]),
3995               Var("ast",OTy(CTy"instruction"))],
4008                        Var("ast",OTy(CTy"instruction"))]),
4011                        Var("ast",OTy(CTy"instruction"))]),
4014                        Mop(Some,Const("Unallocated",CTy"instruction"))]),
4017                        Mop(Some,Const("NoOperation",CTy"instruction"))])]),
4019                   Var("ast",OTy(CTy"instruction"))]),
4021                   Var("ast",OTy(CTy"instruction"))],
4033                            Var("ast",OTy(CTy"instruction"))]),
4036                            Var("ast",OTy(CTy"instruction"))]),
4039                            Mop(Some,Const("Unallocated",CTy"instruction"))]),
4042                            Mop(Some,Const("NoOperation",CTy"instruction"))])]),
4044                       Var("ast",OTy(CTy"instruction"))]),
4045                CS(Var("ast",OTy(CTy"instruction")),
4046                   [(Mop(Some,Var("i",CTy"instruction")),
4047                     Var("i",CTy"instruction")),
4048                    (LO(CTy"instruction"),
4050                       ("LoadStoreAcquireN",CTy"instruction",
4082                            ("Address",CTy"instruction",
4102              Const("Reserved",CTy"instruction")),
4114                      Const("Reserved",CTy"instruction"),
4116                        ("Data",CTy"instruction",
4142                ("Data",CTy"instruction",
4174                      Const("Reserved",CTy"instruction"),
4176                        ("Data",CTy"instruction",
4208                      Const("Reserved",CTy"instruction"),
4210                        ("Data",CTy"instruction",
4235              Const("Reserved",CTy"instruction")),
4247                    ("Data",CTy"instruction",
4275                    ("Data",CTy"instruction",
4318                ("Data",CTy"instruction",
4358                ("Data",CTy"instruction",
4382                      Const("Reserved",CTy"instruction"),
4388                            ("Data",CTy"instruction",
4418                    ("Data",CTy"instruction",
4448              Const("Reserved",CTy"instruction")),
4471                         ("Data",CTy"instruction",
4482                  (LO(PTy(F32,F32)),Const("Reserved",CTy"instruction"))])),
4505                         ("Data",CTy"instruction",
4516                  (LO(PTy(F64,F64)),Const("Reserved",CTy"instruction"))])),
4541                ("Data",CTy"instruction",
4581                ("Data",CTy"instruction",
4604              Const("Unallocated",CTy"instruction")),
4613              Const("Unallocated",CTy"instruction")),
4641                                    ("Data",CTy"instruction",
4649                                    ("Data",CTy"instruction",
4664              Const("Unallocated",CTy"instruction")),
4683                              Const("Reserved",CTy"instruction"),
4699                                         ("Data",CTy"instruction",
4719                                       Const("Reserved",CTy"instruction"))]))))))),
4736                              Const("Reserved",CTy"instruction"),
4752                                         ("Data",CTy"instruction",
4772                                       Const("Reserved",CTy"instruction"))]))))))),
4791                ("Data",CTy"instruction",
4826                ("Data",CTy"instruction",
4863                ("Data",CTy"instruction",
4899                ("Data",CTy"instruction",
4928                ("Data",CTy"instruction",
4957                ("Data",CTy"instruction",
5015                ("Data",CTy"instruction",
5067                ("Data",CTy"instruction",
5092                        Const("Unallocated",CTy"instruction")),
5094                        Const("Reserved",CTy"instruction"))],
5096                        ("Data",CTy"instruction",
5120                  Const("Unallocated",CTy"instruction"),
5122                    ("Data",CTy"instruction",
5165                ("Data",CTy"instruction",
5205                ("Data",CTy"instruction",
5231                ("Data",CTy"instruction",
5260                ("Data",CTy"instruction",
5287                ("Data",CTy"instruction",
5317                ("Data",CTy"instruction",
5373              Const("Unallocated",CTy"instruction")),
5414                ("Data",CTy"instruction",
5466                ("Data",CTy"instruction",
5505                ("CRCExt",CTy"instruction",
5544                ("CRCExt",CTy"instruction",
5583                ("CRCExt",CTy"instruction",
5621                ("CRCExt",CTy"instruction",
5644                ("Branch",CTy"instruction",
5663                ("Branch",CTy"instruction",
5737                ("Branch",CTy"instruction",
5799                ("Branch",CTy"instruction",
5862                ("Branch",CTy"instruction",
5918              Const("Unallocated",CTy"instruction")),
5940                                ("Branch",CTy"instruction",
5946                                ("Branch",CTy"instruction",
5980                                        ("Branch",CTy"instruction",
5990                                        ("Branch",CTy"instruction",
6010              Const("Unallocated",CTy"instruction")),
6020              Const("Unallocated",CTy"instruction")),
6032              Const("Unallocated",CTy"instruction")),
6047              Const("Unallocated",CTy"instruction")),
6057                ("LoadStoreImmediate",CTy"instruction",
6082                ("LoadStoreImmediate",CTy"instruction",
6107                    ("LoadStoreImmediate",CTy"instruction",
6138              Const("Unallocated",CTy"instruction")),
6150              Const("Reserved",CTy"instruction")),
6162              Const("Reserved",CTy"instruction")),
6190                            ("LoadStoreRegister",CTy"instruction",
6230                             ("LoadStore",CTy"instruction",
6237                             ("LoadStore",CTy"instruction",
6244                             ("LoadStore",CTy"instruction",
6251                             ("LoadStore",CTy"instruction",
6264              Const("Unallocated",CTy"instruction")),
6272              Const("Unallocated",CTy"instruction")),
6280              Const("Unallocated",CTy"instruction")),
6297                                    ("LoadStorePair",CTy"instruction",
6344              Const("Unallocated",CTy"instruction")),
6352              Const("Unallocated",CTy"instruction")),
6361              Const("Unallocated",CTy"instruction")),
6369                ("LoadStoreAcquire",CTy"instruction",
6404                ("System",CTy"instruction",
6476                ("System",CTy"instruction",
6537                ("System",CTy"instruction",
6597                ("System",CTy"instruction",
6655              Const("Unallocated",CTy"instruction")),
6705                ("MemoryBarrier",CTy"instruction",
6737                ("Debug",CTy"instruction",
6795                    ("Hint",CTy"instruction",
6858                ("ClearExclusive",CTy"instruction",
6925                ("Debug",CTy"instruction",Const("DebugRestore",CTy"Debug"))),
6947                ("Debug",CTy"instruction",
6979                ("Debug",CTy"instruction",
7054                ("System",CTy"instruction",
7084                ("System",CTy"instruction",
7120                ("System",CTy"instruction",
7155                ("System",CTy"instruction",
7179                ("System",CTy"instruction",
7192            Const("Unallocated",CTy"instruction"))))
7212                  Call("Decode",CTy"instruction",Var("v",F32))),qVar"s"),
8466   ("Encode",Var("i",CTy"instruction"),
8467    CS(Var("i",CTy"instruction"),
8469           ("Address",CTy"instruction",
8494        (Call("Data",CTy"instruction",Var("x",CTy"Data")),
8496        (Call("Branch",CTy"instruction",Var("x",CTy"Branch")),
8498        (Call("LoadStore",CTy"instruction",Var("x",CTy"LoadStore")),
8500        (Call("CRCExt",CTy"instruction",Var("x",CTy"CRCExt")),
8503        (Call("Debug",CTy"instruction",Var("x",CTy"Debug")),
8506        (Call("System",CTy"instruction",Var("x",CTy"System")),
8511           ("MemoryBarrier",CTy"instruction",
8517        (Call("ClearExclusive",CTy"instruction",Var("crm",F4)),
8521        (Call("Hint",CTy"instruction",Var("opc",CTy"SystemHintOp")),
8526        (Const("Unallocated",CTy"instruction"),
8528        (Const("Reserved",CTy"instruction"),