1(* m0Script.sml - generated by L3 - Tue Jun 27 13:58:18 2017 *) 2open HolKernel boolLib bossLib Import 3 4val () = Import.start "m0" 5 6val _ = Record ("PRIMASK",[("PM",bTy),("primask'rst",FTy 31)]) 7; 8val _ = Record 9 ("PSR", 10 [("C",bTy),("ExceptionNumber",FTy 6),("N",bTy),("T",bTy),("V",bTy), 11 ("Z",bTy),("psr'rst",FTy 21)]) 12; 13val _ = Record 14 ("CONTROL",[("SPSEL",bTy),("control'rst",bTy),("nPRIV",bTy)]) 15; 16val _ = Record 17 ("AIRCR", 18 [("ENDIANNESS",bTy),("SYSRESETREQ",bTy),("VECTCLRACTIVE",bTy), 19 ("VECTKEY",F16),("aircr'rst",FTy 13)]) 20; 21val _ = Record 22 ("CCR",[("STKALIGN",bTy),("UNALIGN_TRP",bTy),("ccr'rst",FTy 30)]) 23; 24val _ = Record ("SHPR2",[("PRI_11",FTy 2),("shpr2'rst",FTy 30)]) 25; 26val _ = Record 27 ("SHPR3",[("PRI_14",FTy 2),("PRI_15",FTy 2),("shpr3'rst",FTy 28)]) 28; 29val _ = Record 30 ("IPR", 31 [("PRI_N0",FTy 2),("PRI_N1",FTy 2),("PRI_N2",FTy 2),("PRI_N3",FTy 2), 32 ("ipr'rst",FTy 24)]) 33; 34val _ = Construct [("Mode",[("Mode_Thread",[]),("Mode_Handler",[])])] 35; 36val _ = Construct 37 [("ARM_Exception", 38 [("ExternalInterrupt",[FTy 6]),("HardFault",[]),("NMI",[]), 39 ("PendSV",[]),("Reset",[]),("SVCall",[]),("SysTick",[])])] 40; 41val _ = Construct 42 [("RName", 43 [("RName_0",[]),("RName_1",[]),("RName_2",[]),("RName_3",[]), 44 ("RName_4",[]),("RName_5",[]),("RName_6",[]),("RName_7",[]), 45 ("RName_8",[]),("RName_9",[]),("RName_10",[]),("RName_11",[]), 46 ("RName_12",[]),("RName_SP_main",[]),("RName_SP_process",[]), 47 ("RName_LR",[]),("RName_PC",[])])] 48; 49val _ = Construct 50 [("SRType", 51 [("SRType_LSL",[]),("SRType_LSR",[]),("SRType_ASR",[]), 52 ("SRType_ROR",[]),("SRType_RRX",[])])] 53; 54val _ = Construct 55 [("offset",[("immediate_form",[F32]),("register_form",[F4])])] 56; 57val _ = Construct 58 [("Hint", 59 [("Breakpoint",[F32]),("DataMemoryBarrier",[F4]), 60 ("DataSynchronizationBarrier",[F4]), 61 ("InstructionSynchronizationBarrier",[F4]),("SendEvent",[uTy]), 62 ("WaitForEvent",[uTy]),("WaitForInterrupt",[uTy]),("Yield",[uTy])])] 63; 64val _ = Construct 65 [("System", 66 [("ChangeProcessorState",[bTy]), 67 ("MoveToRegisterFromSpecial",[PTy(F8,F4)]), 68 ("MoveToSpecialRegister",[PTy(F8,F4)]),("SupervisorCall",[F32])])] 69; 70val _ = Construct 71 [("Store", 72 [("Push",[FTy 9]),("StoreByte",[PTy(F4,PTy(F4,CTy"offset"))]), 73 ("StoreHalf",[PTy(F4,PTy(F4,CTy"offset"))]), 74 ("StoreMultiple",[PTy(F4,F8)]), 75 ("StoreWord",[PTy(F4,PTy(F4,CTy"offset"))])])] 76; 77val _ = Construct 78 [("Load", 79 [("LoadByte",[PTy(bTy,PTy(F4,PTy(F4,CTy"offset")))]), 80 ("LoadHalf",[PTy(bTy,PTy(F4,PTy(F4,CTy"offset")))]), 81 ("LoadLiteral",[PTy(F4,F32)]), 82 ("LoadMultiple",[PTy(bTy,PTy(F4,FTy 9))]), 83 ("LoadWord",[PTy(F4,PTy(F4,CTy"offset"))])])] 84; 85val _ = Construct 86 [("Media", 87 [("ByteReverse",[PTy(F4,F4)]), 88 ("ByteReversePackedHalfword",[PTy(F4,F4)]), 89 ("ByteReverseSignedHalfword",[PTy(F4,F4)]), 90 ("ExtendByte",[PTy(bTy,PTy(F4,F4))]), 91 ("ExtendHalfword",[PTy(bTy,PTy(F4,F4))])])] 92; 93val _ = Construct [("Multiply",[("Multiply32",[PTy(F4,PTy(F4,F4))])])] 94; 95val _ = Construct 96 [("Data", 97 [("ArithLogicImmediate",[PTy(F4,PTy(bTy,PTy(F4,PTy(F4,F32))))]), 98 ("CompareImmediate",[PTy(F4,F32)]),("Move",[PTy(F4,F32)]), 99 ("Register",[PTy(F4,PTy(bTy,PTy(F4,PTy(F4,F4))))]), 100 ("ShiftImmediate", 101 [PTy(bTy,PTy(bTy,PTy(F4,PTy(F4,PTy(CTy"SRType",nTy)))))]), 102 ("ShiftRegister",[PTy(F4,PTy(F4,PTy(CTy"SRType",F4)))]), 103 ("TestCompareRegister",[PTy(FTy 2,PTy(F4,F4))])])] 104; 105val _ = Construct 106 [("Branch", 107 [("BranchExchange",[F4]),("BranchLinkExchangeRegister",[F4]), 108 ("BranchLinkImmediate",[F32]),("BranchTarget",[F32])])] 109; 110val _ = Construct 111 [("instruction", 112 [("Branch",[CTy"Branch"]),("Data",[CTy"Data"]),("Hint",[CTy"Hint"]), 113 ("Load",[CTy"Load"]),("Media",[CTy"Media"]), 114 ("Multiply",[CTy"Multiply"]),("NoOperation",[uTy]), 115 ("Store",[CTy"Store"]),("System",[CTy"System"]),("Undefined",[F32])])] 116; 117val _ = Construct 118 [("MachineCode",[("Thumb",[F16]),("Thumb2",[PTy(F16,F16)])])] 119; 120val _ = Construct 121 [("exception", 122 [("ASSERT",[sTy]),("NoException",[]),("UNPREDICTABLE",[sTy])])] 123; 124val _ = Record 125 ("m0_state", 126 [("AIRCR",CTy"AIRCR"),("CCR",CTy"CCR"),("CONTROL",CTy"CONTROL"), 127 ("CurrentMode",CTy"Mode"),("ExceptionActive",ATy(FTy 6,bTy)), 128 ("MEM",ATy(F32,F8)),("NVIC_IPR",ATy(FTy 3,CTy"IPR")), 129 ("PRIMASK",CTy"PRIMASK"),("PSR",CTy"PSR"),("REG",ATy(CTy"RName",F32)), 130 ("SHPR2",CTy"SHPR2"),("SHPR3",CTy"SHPR3"),("VTOR",F32),("count",nTy), 131 ("exception",CTy"exception"),("pcinc",F32), 132 ("pending",OTy(CTy"ARM_Exception"))]) 133; 134val qTy = CTy "m0_state"; 135fun qVar v = Term.mk_var (v, ParseDatatype.pretypeToType qTy); 136val raise'exception_def = Def 137 ("raise'exception",Var("e",CTy"exception"), 138 Close 139 (qVar"state", 140 TP[LX(VTy"a"), 141 ITE(EQ(Dest("exception",CTy"exception",qVar"state"), 142 Const("NoException",CTy"exception")), 143 Rupd("exception",TP[qVar"state",Var("e",CTy"exception")]), 144 qVar"state")])) 145; 146val rec'PRIMASK_def = Def 147 ("rec'PRIMASK",Var("x",F32), 148 Rec(CTy"PRIMASK", 149 [Bop(Bit,Var("x",F32),LN 0),EX(Var("x",F32),LN 31,LN 1,FTy 31)])) 150; 151val reg'PRIMASK_def = Def 152 ("reg'PRIMASK",Var("x",CTy"PRIMASK"), 153 CS(Var("x",CTy"PRIMASK"), 154 [(Rec(CTy"PRIMASK",[bVar"PM",Var("primask'rst",FTy 31)]), 155 CC[Var("primask'rst",FTy 31),Mop(Cast F1,bVar"PM")])])) 156; 157val write'rec'PRIMASK_def = Def 158 ("write'rec'PRIMASK",TP[AVar F32,Var("x",CTy"PRIMASK")], 159 Call("reg'PRIMASK",F32,Var("x",CTy"PRIMASK"))) 160; 161val write'reg'PRIMASK_def = Def 162 ("write'reg'PRIMASK",TP[AVar(CTy"PRIMASK"),Var("x",F32)], 163 Call("rec'PRIMASK",CTy"PRIMASK",Var("x",F32))) 164; 165val rec'PSR_def = Def 166 ("rec'PSR",Var("x",F32), 167 Rec(CTy"PSR", 168 [Bop(Bit,Var("x",F32),LN 29),EX(Var("x",F32),LN 5,LN 0,FTy 6), 169 Bop(Bit,Var("x",F32),LN 31),Bop(Bit,Var("x",F32),LN 24), 170 Bop(Bit,Var("x",F32),LN 28),Bop(Bit,Var("x",F32),LN 30), 171 CC[EX(Var("x",F32),LN 23,LN 6,FTy 18), 172 EX(Var("x",F32),LN 27,LN 25,FTy 3)]])) 173; 174val reg'PSR_def = Def 175 ("reg'PSR",Var("x",CTy"PSR"), 176 CS(Var("x",CTy"PSR"), 177 [(Rec(CTy"PSR", 178 [bVar"C",Var("ExceptionNumber",FTy 6),bVar"N",bVar"T",bVar"V", 179 bVar"Z",Var("psr'rst",FTy 21)]), 180 CC[Mop(Cast F1,bVar"N"),Mop(Cast F1,bVar"Z"),Mop(Cast F1,bVar"C"), 181 Mop(Cast F1,bVar"V"),EX(Var("psr'rst",FTy 21),LN 2,LN 0,FTy 3), 182 Mop(Cast F1,bVar"T"), 183 EX(Var("psr'rst",FTy 21),LN 20,LN 3,FTy 18), 184 Var("ExceptionNumber",FTy 6)])])) 185; 186val write'rec'PSR_def = Def 187 ("write'rec'PSR",TP[AVar F32,Var("x",CTy"PSR")], 188 Call("reg'PSR",F32,Var("x",CTy"PSR"))) 189; 190val write'reg'PSR_def = Def 191 ("write'reg'PSR",TP[AVar(CTy"PSR"),Var("x",F32)], 192 Call("rec'PSR",CTy"PSR",Var("x",F32))) 193; 194val rec'CONTROL_def = Def 195 ("rec'CONTROL",Var("x",FTy 3), 196 Rec(CTy"CONTROL", 197 [Bop(Bit,Var("x",FTy 3),LN 1),Bop(Bit,Var("x",FTy 3),LN 2), 198 Bop(Bit,Var("x",FTy 3),LN 0)])) 199; 200val reg'CONTROL_def = Def 201 ("reg'CONTROL",Var("x",CTy"CONTROL"), 202 CS(Var("x",CTy"CONTROL"), 203 [(Rec(CTy"CONTROL",[bVar"SPSEL",bVar"control'rst",bVar"nPRIV"]), 204 CC[Mop(Cast F1,bVar"control'rst"),Mop(Cast F1,bVar"SPSEL"), 205 Mop(Cast F1,bVar"nPRIV")])])) 206; 207val write'rec'CONTROL_def = Def 208 ("write'rec'CONTROL",TP[AVar(FTy 3),Var("x",CTy"CONTROL")], 209 Call("reg'CONTROL",FTy 3,Var("x",CTy"CONTROL"))) 210; 211val write'reg'CONTROL_def = Def 212 ("write'reg'CONTROL",TP[AVar(CTy"CONTROL"),Var("x",FTy 3)], 213 Call("rec'CONTROL",CTy"CONTROL",Var("x",FTy 3))) 214; 215val rec'AIRCR_def = Def 216 ("rec'AIRCR",Var("x",F32), 217 Rec(CTy"AIRCR", 218 [Bop(Bit,Var("x",F32),LN 15),Bop(Bit,Var("x",F32),LN 2), 219 Bop(Bit,Var("x",F32),LN 1),EX(Var("x",F32),LN 31,LN 16,F16), 220 CC[EX(Var("x",F32),LN 0,LN 0,F1), 221 EX(Var("x",F32),LN 14,LN 3,FTy 12)]])) 222; 223val reg'AIRCR_def = Def 224 ("reg'AIRCR",Var("x",CTy"AIRCR"), 225 CS(Var("x",CTy"AIRCR"), 226 [(Rec(CTy"AIRCR", 227 [bVar"ENDIANNESS",bVar"SYSRESETREQ",bVar"VECTCLRACTIVE", 228 Var("VECTKEY",F16),Var("aircr'rst",FTy 13)]), 229 CC[Var("VECTKEY",F16),Mop(Cast F1,bVar"ENDIANNESS"), 230 EX(Var("aircr'rst",FTy 13),LN 11,LN 0,FTy 12), 231 Mop(Cast F1,bVar"SYSRESETREQ"), 232 Mop(Cast F1,bVar"VECTCLRACTIVE"), 233 EX(Var("aircr'rst",FTy 13),LN 12,LN 12,F1)])])) 234; 235val write'rec'AIRCR_def = Def 236 ("write'rec'AIRCR",TP[AVar F32,Var("x",CTy"AIRCR")], 237 Call("reg'AIRCR",F32,Var("x",CTy"AIRCR"))) 238; 239val write'reg'AIRCR_def = Def 240 ("write'reg'AIRCR",TP[AVar(CTy"AIRCR"),Var("x",F32)], 241 Call("rec'AIRCR",CTy"AIRCR",Var("x",F32))) 242; 243val rec'CCR_def = Def 244 ("rec'CCR",Var("x",F32), 245 Rec(CTy"CCR", 246 [Bop(Bit,Var("x",F32),LN 9),Bop(Bit,Var("x",F32),LN 3), 247 CC[EX(Var("x",F32),LN 2,LN 0,FTy 3), 248 EX(Var("x",F32),LN 8,LN 4,FTy 5), 249 EX(Var("x",F32),LN 31,LN 10,FTy 22)]])) 250; 251val reg'CCR_def = Def 252 ("reg'CCR",Var("x",CTy"CCR"), 253 CS(Var("x",CTy"CCR"), 254 [(Rec(CTy"CCR", 255 [bVar"STKALIGN",bVar"UNALIGN_TRP",Var("ccr'rst",FTy 30)]), 256 CC[EX(Var("ccr'rst",FTy 30),LN 21,LN 0,FTy 22), 257 Mop(Cast F1,bVar"STKALIGN"), 258 EX(Var("ccr'rst",FTy 30),LN 26,LN 22,FTy 5), 259 Mop(Cast F1,bVar"UNALIGN_TRP"), 260 EX(Var("ccr'rst",FTy 30),LN 29,LN 27,FTy 3)])])) 261; 262val write'rec'CCR_def = Def 263 ("write'rec'CCR",TP[AVar F32,Var("x",CTy"CCR")], 264 Call("reg'CCR",F32,Var("x",CTy"CCR"))) 265; 266val write'reg'CCR_def = Def 267 ("write'reg'CCR",TP[AVar(CTy"CCR"),Var("x",F32)], 268 Call("rec'CCR",CTy"CCR",Var("x",F32))) 269; 270val rec'SHPR2_def = Def 271 ("rec'SHPR2",Var("x",F32), 272 Rec(CTy"SHPR2", 273 [EX(Var("x",F32),LN 31,LN 30,FTy 2), 274 EX(Var("x",F32),LN 29,LN 0,FTy 30)])) 275; 276val reg'SHPR2_def = Def 277 ("reg'SHPR2",Var("x",CTy"SHPR2"), 278 CS(Var("x",CTy"SHPR2"), 279 [(Rec(CTy"SHPR2",[Var("PRI_11",FTy 2),Var("shpr2'rst",FTy 30)]), 280 CC[Var("PRI_11",FTy 2),Var("shpr2'rst",FTy 30)])])) 281; 282val write'rec'SHPR2_def = Def 283 ("write'rec'SHPR2",TP[AVar F32,Var("x",CTy"SHPR2")], 284 Call("reg'SHPR2",F32,Var("x",CTy"SHPR2"))) 285; 286val write'reg'SHPR2_def = Def 287 ("write'reg'SHPR2",TP[AVar(CTy"SHPR2"),Var("x",F32)], 288 Call("rec'SHPR2",CTy"SHPR2",Var("x",F32))) 289; 290val rec'SHPR3_def = Def 291 ("rec'SHPR3",Var("x",F32), 292 Rec(CTy"SHPR3", 293 [EX(Var("x",F32),LN 23,LN 22,FTy 2), 294 EX(Var("x",F32),LN 31,LN 30,FTy 2), 295 CC[EX(Var("x",F32),LN 21,LN 0,FTy 22), 296 EX(Var("x",F32),LN 29,LN 24,FTy 6)]])) 297; 298val reg'SHPR3_def = Def 299 ("reg'SHPR3",Var("x",CTy"SHPR3"), 300 CS(Var("x",CTy"SHPR3"), 301 [(Rec(CTy"SHPR3", 302 [Var("PRI_14",FTy 2),Var("PRI_15",FTy 2), 303 Var("shpr3'rst",FTy 28)]), 304 CC[Var("PRI_15",FTy 2), 305 EX(Var("shpr3'rst",FTy 28),LN 5,LN 0,FTy 6), 306 Var("PRI_14",FTy 2), 307 EX(Var("shpr3'rst",FTy 28),LN 27,LN 6,FTy 22)])])) 308; 309val write'rec'SHPR3_def = Def 310 ("write'rec'SHPR3",TP[AVar F32,Var("x",CTy"SHPR3")], 311 Call("reg'SHPR3",F32,Var("x",CTy"SHPR3"))) 312; 313val write'reg'SHPR3_def = Def 314 ("write'reg'SHPR3",TP[AVar(CTy"SHPR3"),Var("x",F32)], 315 Call("rec'SHPR3",CTy"SHPR3",Var("x",F32))) 316; 317val rec'IPR_def = Def 318 ("rec'IPR",Var("x",F32), 319 Rec(CTy"IPR", 320 [EX(Var("x",F32),LN 7,LN 6,FTy 2), 321 EX(Var("x",F32),LN 15,LN 14,FTy 2), 322 EX(Var("x",F32),LN 23,LN 22,FTy 2), 323 EX(Var("x",F32),LN 31,LN 30,FTy 2), 324 CC[EX(Var("x",F32),LN 5,LN 0,FTy 6), 325 EX(Var("x",F32),LN 13,LN 8,FTy 6), 326 EX(Var("x",F32),LN 21,LN 16,FTy 6), 327 EX(Var("x",F32),LN 29,LN 24,FTy 6)]])) 328; 329val reg'IPR_def = Def 330 ("reg'IPR",Var("x",CTy"IPR"), 331 CS(Var("x",CTy"IPR"), 332 [(Rec(CTy"IPR", 333 [Var("PRI_N0",FTy 2),Var("PRI_N1",FTy 2),Var("PRI_N2",FTy 2), 334 Var("PRI_N3",FTy 2),Var("ipr'rst",FTy 24)]), 335 CC[Var("PRI_N3",FTy 2),EX(Var("ipr'rst",FTy 24),LN 5,LN 0,FTy 6), 336 Var("PRI_N2",FTy 2),EX(Var("ipr'rst",FTy 24),LN 11,LN 6,FTy 6), 337 Var("PRI_N1",FTy 2), 338 EX(Var("ipr'rst",FTy 24),LN 17,LN 12,FTy 6), 339 Var("PRI_N0",FTy 2),EX(Var("ipr'rst",FTy 24),LN 23,LN 18,FTy 6)])])) 340; 341val write'rec'IPR_def = Def 342 ("write'rec'IPR",TP[AVar F32,Var("x",CTy"IPR")], 343 Call("reg'IPR",F32,Var("x",CTy"IPR"))) 344; 345val write'reg'IPR_def = Def 346 ("write'reg'IPR",TP[AVar(CTy"IPR"),Var("x",F32)], 347 Call("rec'IPR",CTy"IPR",Var("x",F32))) 348; 349val ProcessorID_def = Def ("ProcessorID",AVar uTy,LI 0) 350; 351val ConditionPassed_def = Def 352 ("ConditionPassed",Var("cond",F4), 353 Close 354 (qVar"state", 355 Let(TP[bVar"v",qVar"s"], 356 CS(EX(Var("cond",F4),LN 3,LN 1,FTy 3), 357 [(LW(0,3), 358 TP[Dest("Z",bTy,Dest("PSR",CTy"PSR",qVar"state")), 359 qVar"state"]), 360 (LW(1,3), 361 TP[Dest("C",bTy,Dest("PSR",CTy"PSR",qVar"state")), 362 qVar"state"]), 363 (LW(2,3), 364 TP[Dest("N",bTy,Dest("PSR",CTy"PSR",qVar"state")), 365 qVar"state"]), 366 (LW(3,3), 367 TP[Dest("V",bTy,Dest("PSR",CTy"PSR",qVar"state")), 368 qVar"state"]), 369 (LW(4,3), 370 TP[Bop(And,Dest("C",bTy,Dest("PSR",CTy"PSR",qVar"state")), 371 Mop(Not, 372 Dest("Z",bTy,Dest("PSR",CTy"PSR",qVar"state")))), 373 qVar"state"]), 374 (LW(5,3), 375 TP[EQ(Dest("N",bTy,Dest("PSR",CTy"PSR",qVar"state")), 376 Dest("V",bTy,Dest("PSR",CTy"PSR",qVar"state"))), 377 qVar"state"]), 378 (LW(6,3), 379 TP[Bop(And, 380 EQ(Dest("N",bTy,Dest("PSR",CTy"PSR",qVar"state")), 381 Dest("V",bTy,Dest("PSR",CTy"PSR",qVar"state"))), 382 Mop(Not, 383 Dest("Z",bTy,Dest("PSR",CTy"PSR",qVar"state")))), 384 qVar"state"]),(LW(7,3),TP[LT,qVar"state"])]), 385 ITE(Bop(And,Bop(Bit,Var("cond",F4),LN 0), 386 Mop(Not,EQ(Var("cond",F4),LW(15,4)))),Mop(Not,bVar"v"), 387 bVar"v")))) 388; 389val Raise_def = Def 390 ("Raise",Var("e",CTy"ARM_Exception"), 391 Close 392 (qVar"state", 393 Rupd 394 ("pending",TP[qVar"state",Mop(Some,Var("e",CTy"ARM_Exception"))]))) 395; 396val CurrentModeIsPrivileged_def = Def 397 ("CurrentModeIsPrivileged",AVar uTy, 398 Close 399 (qVar"state", 400 Bop(Or, 401 EQ(Dest("CurrentMode",CTy"Mode",qVar"state"), 402 LC("Mode_Handler",CTy"Mode")), 403 Mop(Not, 404 Dest("nPRIV",bTy,Dest("CONTROL",CTy"CONTROL",qVar"state")))))) 405; 406val LookUpSP_def = Def 407 ("LookUpSP",AVar uTy, 408 Close 409 (qVar"state", 410 ITE(Dest("SPSEL",bTy,Dest("CONTROL",CTy"CONTROL",qVar"state")), 411 LC("RName_SP_process",CTy"RName"),LC("RName_SP_main",CTy"RName")))) 412; 413val R_def = Def 414 ("R",Var("n",F4), 415 Close 416 (qVar"state", 417 ITB([(EQ(Var("n",F4),LW(15,4)), 418 Bop(Add, 419 Apply 420 (Dest("REG",ATy(CTy"RName",F32),qVar"state"), 421 LC("RName_PC",CTy"RName")),LW(4,32))), 422 (EQ(Var("n",F4),LW(14,4)), 423 Apply 424 (Dest("REG",ATy(CTy"RName",F32),qVar"state"), 425 LC("RName_LR",CTy"RName"))), 426 (EQ(Var("n",F4),LW(13,4)), 427 Apply 428 (Dest("REG",ATy(CTy"RName",F32),qVar"state"), 429 Apply(Call("LookUpSP",ATy(qTy,CTy"RName"),LU),qVar"state")))], 430 Apply 431 (Dest("REG",ATy(CTy"RName",F32),qVar"state"), 432 Mop(Cast(CTy"RName"),Var("n",F4)))))) 433; 434val write'R_def = Def 435 ("write'R",TP[Var("value",F32),Var("n",F4)], 436 Close 437 (qVar"state", 438 ITB([(EQ(Var("n",F4),LW(15,4)), 439 Mop(Snd, 440 Apply 441 (Call 442 ("raise'exception",ATy(qTy,PTy(uTy,qTy)), 443 Call("ASSERT",CTy"exception",LS"n >= 0 and n <= 14")), 444 qVar"state"))), 445 (EQ(Var("n",F4),LW(14,4)), 446 Rupd 447 ("REG", 448 TP[qVar"state", 449 Fupd 450 (Dest("REG",ATy(CTy"RName",F32),qVar"state"), 451 LC("RName_LR",CTy"RName"),Var("value",F32))])), 452 (EQ(Var("n",F4),LW(13,4)), 453 Rupd 454 ("REG", 455 TP[qVar"state", 456 Fupd 457 (Dest("REG",ATy(CTy"RName",F32),qVar"state"), 458 Apply 459 (Call("LookUpSP",ATy(qTy,CTy"RName"),LU), 460 qVar"state"), 461 CC[EX(Var("value",F32),LN 31,LN 2,FTy 30),LW(0,2)])]))], 462 Rupd 463 ("REG", 464 TP[qVar"state", 465 Fupd 466 (Dest("REG",ATy(CTy"RName",F32),qVar"state"), 467 Mop(Cast(CTy"RName"),Var("n",F4)),Var("value",F32))])))) 468; 469val SP_main_def = Def 470 ("SP_main",qVar"state", 471 Apply 472 (Dest("REG",ATy(CTy"RName",F32),qVar"state"), 473 LC("RName_SP_main",CTy"RName"))) 474; 475val write'SP_main_def = Def 476 ("write'SP_main",Var("value",F32), 477 Close 478 (qVar"state", 479 Rupd 480 ("REG", 481 TP[qVar"state", 482 Fupd 483 (Dest("REG",ATy(CTy"RName",F32),qVar"state"), 484 LC("RName_SP_main",CTy"RName"),Var("value",F32))]))) 485; 486val SP_process_def = Def 487 ("SP_process",qVar"state", 488 Apply 489 (Dest("REG",ATy(CTy"RName",F32),qVar"state"), 490 LC("RName_SP_process",CTy"RName"))) 491; 492val write'SP_process_def = Def 493 ("write'SP_process",Var("value",F32), 494 Close 495 (qVar"state", 496 Rupd 497 ("REG", 498 TP[qVar"state", 499 Fupd 500 (Dest("REG",ATy(CTy"RName",F32),qVar"state"), 501 LC("RName_SP_process",CTy"RName"),Var("value",F32))]))) 502; 503val SP_def = Def 504 ("SP",qVar"state",Apply(Call("R",ATy(qTy,F32),LW(13,4)),qVar"state")) 505; 506val write'SP_def = Def 507 ("write'SP",Var("value",F32), 508 Close 509 (qVar"state", 510 Apply 511 (Call("write'R",ATy(qTy,qTy),TP[Var("value",F32),LW(13,4)]), 512 qVar"state"))) 513; 514val LR_def = Def 515 ("LR",qVar"state",Apply(Call("R",ATy(qTy,F32),LW(14,4)),qVar"state")) 516; 517val write'LR_def = Def 518 ("write'LR",Var("value",F32), 519 Close 520 (qVar"state", 521 Apply 522 (Call("write'R",ATy(qTy,qTy),TP[Var("value",F32),LW(14,4)]), 523 qVar"state"))) 524; 525val PC_def = Def 526 ("PC",qVar"state",Apply(Call("R",ATy(qTy,F32),LW(15,4)),qVar"state")) 527; 528val write'PC_def = Def 529 ("write'PC",Var("value",F32), 530 Close 531 (qVar"state", 532 Rupd 533 ("REG", 534 TP[qVar"state", 535 Fupd 536 (Dest("REG",ATy(CTy"RName",F32),qVar"state"), 537 LC("RName_PC",CTy"RName"),Var("value",F32))]))) 538; 539val mem1_def = Def 540 ("mem1",Var("address",F32), 541 Close 542 (qVar"state", 543 Mop(Cast vTy, 544 Apply(Dest("MEM",ATy(F32,F8),qVar"state"),Var("address",F32))))) 545; 546val mem_def = Def 547 ("mem",TP[Var("address",F32),nVar"size"], 548 Close 549 (qVar"state", 550 CS(nVar"size", 551 [(LN 1, 552 TP[EX(Apply 553 (Call 554 ("mem1",ATy(qTy,vTy), 555 Bop(Add,Var("address",F32),LW(0,32))),qVar"state"), 556 LN 7,LN 0,vTy),qVar"state"]), 557 (LN 2, 558 TP[EX(CC[Apply 559 (Call 560 ("mem1",ATy(qTy,vTy), 561 Bop(Add,Var("address",F32),LW(1,32))), 562 qVar"state"), 563 Apply 564 (Call 565 ("mem1",ATy(qTy,vTy), 566 Bop(Add,Var("address",F32),LW(0,32))), 567 qVar"state")],LN 15,LN 0,vTy),qVar"state"]), 568 (LN 4, 569 TP[EX(CC[Apply 570 (Call 571 ("mem1",ATy(qTy,vTy), 572 Bop(Add,Var("address",F32),LW(3,32))), 573 qVar"state"), 574 Apply 575 (Call 576 ("mem1",ATy(qTy,vTy), 577 Bop(Add,Var("address",F32),LW(2,32))), 578 qVar"state"), 579 Apply 580 (Call 581 ("mem1",ATy(qTy,vTy), 582 Bop(Add,Var("address",F32),LW(1,32))), 583 qVar"state"), 584 Apply 585 (Call 586 ("mem1",ATy(qTy,vTy), 587 Bop(Add,Var("address",F32),LW(0,32))), 588 qVar"state")],LN 31,LN 0,vTy),qVar"state"]), 589 (AVar nTy, 590 Apply 591 (Call 592 ("raise'exception",ATy(qTy,PTy(vTy,qTy)), 593 Call("ASSERT",CTy"exception",LS"mem: size in {1, 2, 4}")), 594 qVar"state"))]))) 595; 596val write'mem_def = Def 597 ("write'mem",TP[vVar"value",Var("address",F32),nVar"size"], 598 Close 599 (qVar"state", 600 CS(nVar"size", 601 [(LN 1, 602 Rupd 603 ("MEM", 604 TP[qVar"state", 605 Fupd 606 (Dest("MEM",ATy(F32,F8),qVar"state"), 607 Bop(Add,Var("address",F32),LW(0,32)), 608 Mop(Cast F8,EX(vVar"value",LN 7,LN 0,vTy)))])), 609 (LN 2, 610 Let(qVar"s", 611 Rupd 612 ("MEM", 613 TP[qVar"state", 614 Fupd 615 (Dest("MEM",ATy(F32,F8),qVar"state"), 616 Bop(Add,Var("address",F32),LW(0,32)), 617 Mop(Cast F8,EX(vVar"value",LN 7,LN 0,vTy)))]), 618 Rupd 619 ("MEM", 620 TP[qVar"s", 621 Fupd 622 (Dest("MEM",ATy(F32,F8),qVar"s"), 623 Bop(Add,Var("address",F32),LW(1,32)), 624 Mop(Cast F8,EX(vVar"value",LN 15,LN 8,vTy)))]))), 625 (LN 4, 626 Let(qVar"s", 627 Rupd 628 ("MEM", 629 TP[qVar"state", 630 Fupd 631 (Dest("MEM",ATy(F32,F8),qVar"state"), 632 Bop(Add,Var("address",F32),LW(0,32)), 633 Mop(Cast F8,EX(vVar"value",LN 7,LN 0,vTy)))]), 634 Let(qVar"s", 635 Rupd 636 ("MEM", 637 TP[qVar"s", 638 Fupd 639 (Dest("MEM",ATy(F32,F8),qVar"s"), 640 Bop(Add,Var("address",F32),LW(1,32)), 641 Mop(Cast F8,EX(vVar"value",LN 15,LN 8,vTy)))]), 642 Let(qVar"s", 643 Rupd 644 ("MEM", 645 TP[qVar"s", 646 Fupd 647 (Dest("MEM",ATy(F32,F8),qVar"s"), 648 Bop(Add,Var("address",F32),LW(2,32)), 649 Mop(Cast F8, 650 EX(vVar"value",LN 23,LN 16,vTy)))]), 651 Rupd 652 ("MEM", 653 TP[qVar"s", 654 Fupd 655 (Dest("MEM",ATy(F32,F8),qVar"s"), 656 Bop(Add,Var("address",F32),LW(3,32)), 657 Mop(Cast F8, 658 EX(vVar"value",LN 31,LN 24,vTy)))]))))), 659 (AVar nTy, 660 Mop(Snd, 661 Apply 662 (Call 663 ("raise'exception",ATy(qTy,PTy(uTy,qTy)), 664 Call 665 ("ASSERT",CTy"exception",LS"mem: size in {1, 2, 4}")), 666 qVar"state")))]))) 667; 668val BigEndianReverse_def = Def 669 ("BigEndianReverse",TP[vVar"value",nVar"n"], 670 Close 671 (qVar"state", 672 CS(nVar"n", 673 [(LN 1,TP[EX(vVar"value",LN 7,LN 0,vTy),qVar"state"]), 674 (LN 2, 675 TP[CC[EX(vVar"value",LN 7,LN 0,vTy), 676 EX(vVar"value",LN 15,LN 8,vTy)],qVar"state"]), 677 (LN 4, 678 TP[CC[EX(vVar"value",LN 7,LN 0,vTy), 679 EX(vVar"value",LN 15,LN 8,vTy), 680 EX(vVar"value",LN 23,LN 16,vTy), 681 EX(vVar"value",LN 31,LN 24,vTy)],qVar"state"]), 682 (AVar nTy, 683 Apply 684 (Call 685 ("raise'exception",ATy(qTy,PTy(vTy,qTy)), 686 Call 687 ("ASSERT",CTy"exception", 688 LS"BigEndianReverse: n in {1, 2, 4}")),qVar"state"))]))) 689; 690val Align_def = Def 691 ("Align",TP[Var("w",BTy"N"),nVar"n"], 692 Mop(Cast(BTy"N"), 693 Bop(Mul,nVar"n",Bop(Div,Mop(Cast nTy,Var("w",BTy"N")),nVar"n")))) 694; 695val Aligned_def = Def 696 ("Aligned",TP[Var("w",BTy"N"),nVar"n"], 697 EQ(Var("w",BTy"N"),Call("Align",BTy"N",TP[Var("w",BTy"N"),nVar"n"]))) 698; 699val MemA_def = Def 700 ("MemA",TP[Var("address",F32),nVar"size"], 701 Close 702 (qVar"state", 703 ITE(Mop(Not,Call("Aligned",bTy,TP[Var("address",F32),nVar"size"])), 704 TP[LX(BTy"N"), 705 Apply 706 (Call 707 ("Raise",ATy(qTy,qTy), 708 Const("HardFault",CTy"ARM_Exception")),qVar"state")], 709 Let(TP[vVar"v",qVar"s"], 710 Apply 711 (Call 712 ("mem",ATy(qTy,PTy(vTy,qTy)), 713 TP[Var("address",F32),nVar"size"]),qVar"state"), 714 Let(TP[vVar"v",qVar"s"], 715 ITE(Dest 716 ("ENDIANNESS",bTy,Dest("AIRCR",CTy"AIRCR",qVar"s")), 717 Apply 718 (Call 719 ("BigEndianReverse",ATy(qTy,PTy(vTy,qTy)), 720 TP[vVar"v",nVar"size"]),qVar"s"), 721 TP[vVar"v",qVar"s"]), 722 TP[Mop(Cast(BTy"N"),vVar"v"),qVar"s"]))))) 723; 724val write'MemA_def = Def 725 ("write'MemA",TP[Var("value",BTy"N"),Var("address",F32),nVar"size"], 726 Close 727 (qVar"state", 728 ITE(Mop(Not,Call("Aligned",bTy,TP[Var("address",F32),nVar"size"])), 729 Apply 730 (Call 731 ("Raise",ATy(qTy,qTy),Const("HardFault",CTy"ARM_Exception")), 732 qVar"state"), 733 Let(TP[Var("v",PTy(vTy,PTy(F32,nTy))),qVar"s"], 734 Let(TP[vVar"v",qVar"s"], 735 ITE(Dest 736 ("ENDIANNESS",bTy, 737 Dest("AIRCR",CTy"AIRCR",qVar"state")), 738 Apply 739 (Call 740 ("BigEndianReverse",ATy(qTy,PTy(vTy,qTy)), 741 TP[Mop(Cast vTy,Var("value",BTy"N")), 742 nVar"size"]),qVar"state"), 743 TP[Mop(Cast vTy,Var("value",BTy"N")),qVar"state"]), 744 TP[TP[vVar"v",Var("address",F32),nVar"size"],qVar"s"]), 745 Apply 746 (Call 747 ("write'mem",ATy(qTy,qTy), 748 Var("v",PTy(vTy,PTy(F32,nTy)))),qVar"s"))))) 749; 750val MemU_def = Def 751 ("MemU",TP[Var("address",F32),nVar"size"], 752 Close 753 (qVar"state", 754 Apply 755 (Call 756 ("MemA",ATy(qTy,PTy(BTy"N",qTy)), 757 TP[Var("address",F32),nVar"size"]),qVar"state"))) 758; 759val write'MemU_def = Def 760 ("write'MemU",TP[Var("value",BTy"N"),Var("address",F32),nVar"size"], 761 Close 762 (qVar"state", 763 Apply 764 (Call 765 ("write'MemA",ATy(qTy,qTy), 766 TP[Var("value",BTy"N"),Var("address",F32),nVar"size"]), 767 qVar"state"))) 768; 769val ExcNumber_def = Def 770 ("ExcNumber",Var("e",CTy"ARM_Exception"), 771 CS(Var("e",CTy"ARM_Exception"), 772 [(Const("Reset",CTy"ARM_Exception"),LW(1,6)), 773 (Const("NMI",CTy"ARM_Exception"),LW(2,6)), 774 (Const("HardFault",CTy"ARM_Exception"),LW(3,6)), 775 (Const("SVCall",CTy"ARM_Exception"),LW(11,6)), 776 (Const("PendSV",CTy"ARM_Exception"),LW(14,6)), 777 (Const("SysTick",CTy"ARM_Exception"),LW(15,6)), 778 (Call("ExternalInterrupt",CTy"ARM_Exception",Var("n",FTy 6)), 779 Bop(Add,LW(16,6),Var("n",FTy 6)))])) 780; 781val TakeReset_def = Def 782 ("TakeReset",AVar uTy, 783 Close 784 (qVar"state", 785 Let(Var("v",F32),Dest("VTOR",F32,qVar"state"), 786 Let(TP[Var("v0",F32),qVar"s"], 787 Apply 788 (Call("MemA",ATy(qTy,PTy(F32,qTy)),TP[Var("v",F32),LN 4]), 789 Mop(Snd, 790 Apply 791 (For(TP[LN 0,LN 12, 792 Close 793 (nVar"i", 794 Close 795 (qVar"state", 796 TP[LU, 797 Apply 798 (Call 799 ("write'R",ATy(qTy,qTy), 800 TP[LX F32, 801 Mop(Cast F4,nVar"i")]), 802 qVar"state")]))]),qVar"state"))), 803 Let(TP[Var("v",F32),qVar"s"], 804 Apply 805 (Call 806 ("MemA",ATy(qTy,PTy(F32,qTy)), 807 TP[Bop(Add,Var("v",F32),LW(4,32)),LN 4]), 808 Apply 809 (Call("write'LR",ATy(qTy,qTy),LX F32), 810 Apply 811 (Call 812 ("write'SP_process",ATy(qTy,qTy), 813 CC[LX(FTy 30),LW(0,2)]), 814 Apply 815 (Call 816 ("write'SP_main",ATy(qTy,qTy), 817 Var("v0",F32)),qVar"s")))), 818 Let(qVar"s", 819 Rupd 820 ("PSR", 821 TP[Rupd 822 ("CurrentMode", 823 TP[Apply 824 (Call 825 ("write'PC",ATy(qTy,qTy), 826 Var("v",F32)),qVar"s"), 827 LC("Mode_Thread",CTy"Mode")]), 828 LX(CTy"PSR")]), 829 Let(qVar"s", 830 Rupd 831 ("PSR", 832 TP[qVar"s", 833 Rupd 834 ("ExceptionNumber", 835 TP[Dest("PSR",CTy"PSR",qVar"s"),LW(0,6)])]), 836 Let(qVar"s", 837 Rupd 838 ("PRIMASK", 839 TP[qVar"s", 840 Rupd 841 ("PM", 842 TP[Dest 843 ("PRIMASK",CTy"PRIMASK", 844 qVar"s"),LF])]), 845 Let(qVar"s", 846 Rupd 847 ("CONTROL", 848 TP[qVar"s", 849 Rupd 850 ("SPSEL", 851 TP[Dest 852 ("CONTROL",CTy"CONTROL", 853 qVar"s"),LF])]), 854 Mop(Snd, 855 Apply 856 (For(TP[LN 0,LN 63, 857 Close 858 (nVar"i", 859 Close 860 (qVar"state", 861 TP[LU, 862 Rupd 863 ("ExceptionActive", 864 TP[qVar"state", 865 Fupd 866 (Dest 867 ("ExceptionActive", 868 ATy(FTy 6, 869 bTy), 870 qVar"state"), 871 Mop(Cast 872 (FTy 6), 873 nVar"i"), 874 LF)])]))]), 875 Rupd 876 ("CONTROL", 877 TP[qVar"s", 878 Rupd 879 ("nPRIV", 880 TP[Dest 881 ("CONTROL", 882 CTy"CONTROL", 883 qVar"s"),LF])])))))))))))) 884; 885val ExceptionPriority_def = Def 886 ("ExceptionPriority",nVar"n", 887 Close 888 (qVar"state", 889 ITB([(EQ(nVar"n",LN 2),Mop(Neg,LI 2)), 890 (EQ(nVar"n",LN 1),Mop(Neg,LI 1)), 891 (EQ(nVar"n",LN 11), 892 Mop(Cast iTy, 893 Dest("PRI_11",FTy 2,Dest("SHPR2",CTy"SHPR2",qVar"state")))), 894 (EQ(nVar"n",LN 14), 895 Mop(Cast iTy, 896 Dest("PRI_14",FTy 2,Dest("SHPR3",CTy"SHPR3",qVar"state")))), 897 (EQ(nVar"n",LN 15), 898 Mop(Cast iTy, 899 Dest("PRI_15",FTy 2,Dest("SHPR3",CTy"SHPR3",qVar"state")))), 900 (Bop(Ge,nVar"n",LN 16), 901 Let(Var("v",CTy"IPR"), 902 Apply 903 (Dest("NVIC_IPR",ATy(FTy 3,CTy"IPR"),qVar"state"), 904 Mop(Cast(FTy 3),Bop(Div,Bop(Sub,nVar"n",LN 16),LN 4))), 905 CS(Mop(Cast(FTy 2),Bop(Mod,nVar"n",LN 4)), 906 [(LW(0,2), 907 Mop(Cast iTy,Dest("PRI_N0",FTy 2,Var("v",CTy"IPR")))), 908 (LW(1,2), 909 Mop(Cast iTy,Dest("PRI_N1",FTy 2,Var("v",CTy"IPR")))), 910 (LW(2,2), 911 Mop(Cast iTy,Dest("PRI_N2",FTy 2,Var("v",CTy"IPR")))), 912 (LW(3,2), 913 Mop(Cast iTy,Dest("PRI_N3",FTy 2,Var("v",CTy"IPR"))))])))], 914 LI 4))) 915; 916val ExecutionPriority_def = Def 917 ("ExecutionPriority",AVar uTy, 918 Close 919 (qVar"state", 920 Let(Var("s",PTy(iTy,PTy(iTy,qTy))), 921 Mop(Snd, 922 Apply 923 (For(TP[LN 2,LN 48, 924 Close 925 (nVar"i", 926 Close 927 (Var("state",PTy(iTy,PTy(iTy,qTy))), 928 ITE(Apply 929 (Dest 930 ("ExceptionActive",ATy(FTy 6,bTy), 931 Mop(Snd, 932 Mop(Snd, 933 Var("state", 934 PTy(iTy,PTy(iTy,qTy)))))), 935 Mop(Cast(FTy 6),nVar"i")), 936 Let(TP[iVar"v", 937 Var("s",PTy(iTy,PTy(iTy,qTy)))], 938 CS(Let(TP[iVar"v",qVar"s3"], 939 Let(qVar"s", 940 Mop(Snd, 941 Mop(Snd, 942 Var("state", 943 PTy(iTy, 944 PTy(iTy, 945 qTy))))), 946 TP[Apply 947 (Call 948 ("ExceptionPriority", 949 ATy(qTy,iTy), 950 nVar"i"),qVar"s"), 951 qVar"s"]), 952 TP[iVar"v", 953 Mop(Fst, 954 Mop(Snd, 955 Var("state", 956 PTy(iTy, 957 PTy(iTy, 958 qTy))))), 959 qVar"s3"]), 960 [(TP[iVar"v", 961 Var("s3",PTy(iTy,qTy))], 962 TP[iVar"v", 963 Mop(Fst, 964 Var("state", 965 PTy(iTy,PTy(iTy,qTy)))), 966 Var("s3",PTy(iTy,qTy))])]), 967 TP[LU, 968 ITE(Bop(Lt,iVar"v", 969 Mop(Fst, 970 Mop(Snd, 971 Var("s", 972 PTy(iTy, 973 PTy(iTy, 974 qTy)))))), 975 TP[Mop(Fst, 976 Var("s", 977 PTy(iTy, 978 PTy(iTy,qTy)))), 979 iVar"v", 980 Mop(Snd, 981 Mop(Snd, 982 Var("s", 983 PTy(iTy, 984 PTy(iTy, 985 qTy)))))], 986 Var("s",PTy(iTy,PTy(iTy,qTy))))]), 987 TP[LU,Var("state",PTy(iTy,PTy(iTy,qTy)))])))]), 988 TP[LI 4,LI 4,qVar"state"])), 989 Let(Var("s",PTy(iTy,PTy(iTy,qTy))), 990 ITE(Dest 991 ("PM",bTy, 992 Dest 993 ("PRIMASK",CTy"PRIMASK", 994 Mop(Snd,Mop(Snd,Var("s",PTy(iTy,PTy(iTy,qTy))))))), 995 TP[LI 0,Mop(Snd,Var("s",PTy(iTy,PTy(iTy,qTy))))], 996 Var("s",PTy(iTy,PTy(iTy,qTy)))), 997 Mop(Min, 998 TP[Mop(Fst,Var("s",PTy(iTy,PTy(iTy,qTy)))), 999 Mop(Fst,Mop(Snd,Var("s",PTy(iTy,PTy(iTy,qTy)))))]))))) 1000; 1001val ReturnAddress_def = Def 1002 ("ReturnAddress",AVar uTy, 1003 Close(qVar"state",Apply(Const("PC",ATy(qTy,F32)),qVar"state"))) 1004; 1005val PushStack_def = Def 1006 ("PushStack",AVar uTy, 1007 Close 1008 (qVar"state", 1009 Let(TP[Var("s0",F32),Var("s1",F1)],TP[LX F32,LX F1], 1010 Let(Var("s",PTy(F32,PTy(F1,qTy))), 1011 ITE(Bop(And, 1012 Dest 1013 ("SPSEL",bTy, 1014 Dest("CONTROL",CTy"CONTROL",qVar"state")), 1015 EQ(Dest("CurrentMode",CTy"Mode",qVar"state"), 1016 LC("Mode_Thread",CTy"Mode"))), 1017 Let(TP[Var("v",F32),Var("s",PTy(F32,PTy(F1,qTy)))], 1018 CS(TP[Apply 1019 (Const("SP_process",ATy(qTy,F32)), 1020 qVar"state"),Var("s1",F1),qVar"state"], 1021 [(TP[Var("v",F32),Var("s3",PTy(F1,qTy))], 1022 TP[Var("v",F32),Var("s0",F32), 1023 Var("s3",PTy(F1,qTy))])]), 1024 Let(qVar"s2", 1025 Mop(Snd,Mop(Snd,Var("s",PTy(F32,PTy(F1,qTy))))), 1026 Let(TP[Var("v",F32), 1027 Var("s",PTy(F32,PTy(F1,qTy)))], 1028 CS(TP[Apply 1029 (Const("SP_process",ATy(qTy,F32)), 1030 qVar"s2"), 1031 EX(Var("v",F32),LN 2,LN 2,F1),qVar"s2"], 1032 [(TP[Var("v",F32),Var("s3",PTy(F1,qTy))], 1033 TP[Var("v",F32), 1034 Mop(Fst, 1035 Var("s",PTy(F32,PTy(F1,qTy)))), 1036 Var("s3",PTy(F1,qTy))])]), 1037 Let(qVar"s2", 1038 Apply 1039 (Call 1040 ("write'SP_process",ATy(qTy,qTy), 1041 Bop(BAnd, 1042 Bop(Sub,Var("v",F32),LW(32,32)), 1043 Mop(BNot,Mop(Cast F32,LW(4,3))))), 1044 Mop(Snd, 1045 Mop(Snd, 1046 Var("s",PTy(F32,PTy(F1,qTy)))))), 1047 Let(TP[Var("v",F32), 1048 Var("s",PTy(F32,PTy(F1,qTy)))], 1049 CS(TP[Apply 1050 (Const 1051 ("SP_process", 1052 ATy(qTy,F32)),qVar"s2"), 1053 Mop(Fst, 1054 Mop(Snd, 1055 Var("s", 1056 PTy(F32, 1057 PTy(F1,qTy))))), 1058 qVar"s2"], 1059 [(TP[Var("v",F32), 1060 Var("s3",PTy(F1,qTy))], 1061 TP[Var("v",F32), 1062 Mop(Fst, 1063 Var("s", 1064 PTy(F32,PTy(F1,qTy)))), 1065 Var("s3",PTy(F1,qTy))])]), 1066 TP[Var("v",F32), 1067 Mop(Snd, 1068 Var("s",PTy(F32,PTy(F1,qTy))))]))))), 1069 Let(TP[Var("v",F32),Var("s",PTy(F32,PTy(F1,qTy)))], 1070 CS(TP[Apply 1071 (Const("SP_main",ATy(qTy,F32)),qVar"state"), 1072 Var("s1",F1),qVar"state"], 1073 [(TP[Var("v",F32),Var("s3",PTy(F1,qTy))], 1074 TP[Var("v",F32),Var("s0",F32), 1075 Var("s3",PTy(F1,qTy))])]), 1076 Let(qVar"s2", 1077 Mop(Snd,Mop(Snd,Var("s",PTy(F32,PTy(F1,qTy))))), 1078 Let(TP[Var("v",F32), 1079 Var("s",PTy(F32,PTy(F1,qTy)))], 1080 CS(TP[Apply 1081 (Const("SP_main",ATy(qTy,F32)), 1082 qVar"s2"), 1083 EX(Var("v",F32),LN 2,LN 2,F1),qVar"s2"], 1084 [(TP[Var("v",F32),Var("s3",PTy(F1,qTy))], 1085 TP[Var("v",F32), 1086 Mop(Fst, 1087 Var("s",PTy(F32,PTy(F1,qTy)))), 1088 Var("s3",PTy(F1,qTy))])]), 1089 Let(qVar"s2", 1090 Apply 1091 (Call 1092 ("write'SP_process",ATy(qTy,qTy), 1093 Bop(BAnd, 1094 Bop(Sub,Var("v",F32),LW(32,32)), 1095 Mop(BNot,Mop(Cast F32,LW(4,3))))), 1096 Mop(Snd, 1097 Mop(Snd, 1098 Var("s",PTy(F32,PTy(F1,qTy)))))), 1099 Let(TP[Var("v",F32), 1100 Var("s",PTy(F32,PTy(F1,qTy)))], 1101 CS(TP[Apply 1102 (Const 1103 ("SP_main",ATy(qTy,F32)), 1104 qVar"s2"), 1105 Mop(Fst, 1106 Mop(Snd, 1107 Var("s", 1108 PTy(F32, 1109 PTy(F1,qTy))))), 1110 qVar"s2"], 1111 [(TP[Var("v",F32), 1112 Var("s3",PTy(F1,qTy))], 1113 TP[Var("v",F32), 1114 Mop(Fst, 1115 Var("s", 1116 PTy(F32,PTy(F1,qTy)))), 1117 Var("s3",PTy(F1,qTy))])]), 1118 TP[Var("v",F32), 1119 Mop(Snd, 1120 Var("s",PTy(F32,PTy(F1,qTy))))])))))), 1121 Let(Var("s",PTy(F32,PTy(F1,qTy))), 1122 Let(TP[Var("v0",F32),Var("s0",PTy(F32,PTy(F1,qTy)))], 1123 CS(Let(TP[Var("v",F32),qVar"s3"], 1124 Let(qVar"s0", 1125 Mop(Snd, 1126 Mop(Snd,Var("s",PTy(F32,PTy(F1,qTy))))), 1127 TP[Apply 1128 (Call("R",ATy(qTy,F32),LW(0,4)), 1129 qVar"s0"),qVar"s0"]), 1130 TP[Var("v",F32), 1131 Mop(Fst, 1132 Mop(Snd,Var("s",PTy(F32,PTy(F1,qTy))))), 1133 qVar"s3"]), 1134 [(TP[Var("v",F32),Var("s3",PTy(F1,qTy))], 1135 TP[Var("v",F32), 1136 Mop(Fst,Var("s",PTy(F32,PTy(F1,qTy)))), 1137 Var("s3",PTy(F1,qTy))])]), 1138 TP[Mop(Fst,Var("s0",PTy(F32,PTy(F1,qTy)))), 1139 Mop(Fst,Mop(Snd,Var("s0",PTy(F32,PTy(F1,qTy))))), 1140 Apply 1141 (Call 1142 ("write'MemA",ATy(qTy,qTy), 1143 TP[Var("v0",F32), 1144 Mop(Fst,Var("s",PTy(F32,PTy(F1,qTy)))), 1145 LN 4]), 1146 Mop(Snd, 1147 Mop(Snd,Var("s0",PTy(F32,PTy(F1,qTy))))))]), 1148 Let(Var("s",PTy(F32,PTy(F1,qTy))), 1149 Let(TP[Var("v0",F32),Var("s0",PTy(F32,PTy(F1,qTy)))], 1150 CS(Let(TP[Var("v",F32),qVar"s3"], 1151 Let(qVar"s0", 1152 Mop(Snd, 1153 Mop(Snd, 1154 Var("s",PTy(F32,PTy(F1,qTy))))), 1155 TP[Apply 1156 (Call("R",ATy(qTy,F32),LW(1,4)), 1157 qVar"s0"),qVar"s0"]), 1158 TP[Var("v",F32), 1159 Mop(Fst, 1160 Mop(Snd, 1161 Var("s",PTy(F32,PTy(F1,qTy))))), 1162 qVar"s3"]), 1163 [(TP[Var("v",F32),Var("s3",PTy(F1,qTy))], 1164 TP[Var("v",F32), 1165 Mop(Fst,Var("s",PTy(F32,PTy(F1,qTy)))), 1166 Var("s3",PTy(F1,qTy))])]), 1167 TP[Mop(Fst,Var("s0",PTy(F32,PTy(F1,qTy)))), 1168 Mop(Fst, 1169 Mop(Snd,Var("s0",PTy(F32,PTy(F1,qTy))))), 1170 Apply 1171 (Call 1172 ("write'MemA",ATy(qTy,qTy), 1173 TP[Var("v0",F32), 1174 Bop(Add, 1175 Mop(Fst, 1176 Var("s",PTy(F32,PTy(F1,qTy)))), 1177 LW(4,32)),LN 4]), 1178 Mop(Snd, 1179 Mop(Snd,Var("s0",PTy(F32,PTy(F1,qTy))))))]), 1180 Let(Var("s",PTy(F32,PTy(F1,qTy))), 1181 Let(TP[Var("v0",F32), 1182 Var("s0",PTy(F32,PTy(F1,qTy)))], 1183 CS(Let(TP[Var("v",F32),qVar"s3"], 1184 Let(qVar"s0", 1185 Mop(Snd, 1186 Mop(Snd, 1187 Var("s", 1188 PTy(F32,PTy(F1,qTy))))), 1189 TP[Apply 1190 (Call 1191 ("R",ATy(qTy,F32),LW(2,4)), 1192 qVar"s0"),qVar"s0"]), 1193 TP[Var("v",F32), 1194 Mop(Fst, 1195 Mop(Snd, 1196 Var("s", 1197 PTy(F32,PTy(F1,qTy))))), 1198 qVar"s3"]), 1199 [(TP[Var("v",F32),Var("s3",PTy(F1,qTy))], 1200 TP[Var("v",F32), 1201 Mop(Fst, 1202 Var("s",PTy(F32,PTy(F1,qTy)))), 1203 Var("s3",PTy(F1,qTy))])]), 1204 TP[Mop(Fst,Var("s0",PTy(F32,PTy(F1,qTy)))), 1205 Mop(Fst, 1206 Mop(Snd, 1207 Var("s0",PTy(F32,PTy(F1,qTy))))), 1208 Apply 1209 (Call 1210 ("write'MemA",ATy(qTy,qTy), 1211 TP[Var("v0",F32), 1212 Bop(Add, 1213 Mop(Fst, 1214 Var("s", 1215 PTy(F32,PTy(F1,qTy)))), 1216 LW(8,32)),LN 4]), 1217 Mop(Snd, 1218 Mop(Snd, 1219 Var("s0",PTy(F32,PTy(F1,qTy))))))]), 1220 Let(Var("s",PTy(F32,PTy(F1,qTy))), 1221 Let(TP[Var("v0",F32), 1222 Var("s0",PTy(F32,PTy(F1,qTy)))], 1223 CS(Let(TP[Var("v",F32),qVar"s3"], 1224 Let(qVar"s0", 1225 Mop(Snd, 1226 Mop(Snd, 1227 Var("s", 1228 PTy(F32, 1229 PTy(F1,qTy))))), 1230 TP[Apply 1231 (Call 1232 ("R",ATy(qTy,F32), 1233 LW(3,4)),qVar"s0"), 1234 qVar"s0"]), 1235 TP[Var("v",F32), 1236 Mop(Fst, 1237 Mop(Snd, 1238 Var("s", 1239 PTy(F32, 1240 PTy(F1,qTy))))), 1241 qVar"s3"]), 1242 [(TP[Var("v",F32), 1243 Var("s3",PTy(F1,qTy))], 1244 TP[Var("v",F32), 1245 Mop(Fst, 1246 Var("s",PTy(F32,PTy(F1,qTy)))), 1247 Var("s3",PTy(F1,qTy))])]), 1248 TP[Mop(Fst, 1249 Var("s0",PTy(F32,PTy(F1,qTy)))), 1250 Mop(Fst, 1251 Mop(Snd, 1252 Var("s0",PTy(F32,PTy(F1,qTy))))), 1253 Apply 1254 (Call 1255 ("write'MemA",ATy(qTy,qTy), 1256 TP[Var("v0",F32), 1257 Bop(Add, 1258 Mop(Fst, 1259 Var("s", 1260 PTy(F32, 1261 PTy(F1,qTy)))), 1262 LW(12,32)),LN 4]), 1263 Mop(Snd, 1264 Mop(Snd, 1265 Var("s0", 1266 PTy(F32,PTy(F1,qTy))))))]), 1267 Let(Var("s",PTy(F32,PTy(F1,qTy))), 1268 Let(TP[Var("v0",F32), 1269 Var("s0",PTy(F32,PTy(F1,qTy)))], 1270 CS(Let(TP[Var("v",F32),qVar"s3"], 1271 Let(qVar"s0", 1272 Mop(Snd, 1273 Mop(Snd, 1274 Var("s", 1275 PTy(F32, 1276 PTy(F1, 1277 qTy))))), 1278 TP[Apply 1279 (Call 1280 ("R", 1281 ATy(qTy,F32), 1282 LW(12,4)), 1283 qVar"s0"),qVar"s0"]), 1284 TP[Var("v",F32), 1285 Mop(Fst, 1286 Mop(Snd, 1287 Var("s", 1288 PTy(F32, 1289 PTy(F1,qTy))))), 1290 qVar"s3"]), 1291 [(TP[Var("v",F32), 1292 Var("s3",PTy(F1,qTy))], 1293 TP[Var("v",F32), 1294 Mop(Fst, 1295 Var("s", 1296 PTy(F32,PTy(F1,qTy)))), 1297 Var("s3",PTy(F1,qTy))])]), 1298 TP[Mop(Fst, 1299 Var("s0",PTy(F32,PTy(F1,qTy)))), 1300 Mop(Fst, 1301 Mop(Snd, 1302 Var("s0", 1303 PTy(F32,PTy(F1,qTy))))), 1304 Apply 1305 (Call 1306 ("write'MemA",ATy(qTy,qTy), 1307 TP[Var("v0",F32), 1308 Bop(Add, 1309 Mop(Fst, 1310 Var("s", 1311 PTy(F32, 1312 PTy(F1, 1313 qTy)))), 1314 LW(16,32)),LN 4]), 1315 Mop(Snd, 1316 Mop(Snd, 1317 Var("s0", 1318 PTy(F32, 1319 PTy(F1,qTy))))))]), 1320 Let(Var("s",PTy(F32,PTy(F1,qTy))), 1321 Let(TP[Var("v0",F32), 1322 Var("s0",PTy(F32,PTy(F1,qTy)))], 1323 CS(Let(TP[Var("v",F32),qVar"s3"], 1324 Let(qVar"s0", 1325 Mop(Snd, 1326 Mop(Snd, 1327 Var("s", 1328 PTy(F32, 1329 PTy(F1, 1330 qTy))))), 1331 TP[Apply 1332 (Const 1333 ("LR", 1334 ATy(qTy,F32)), 1335 qVar"s0"), 1336 qVar"s0"]), 1337 TP[Var("v",F32), 1338 Mop(Fst, 1339 Mop(Snd, 1340 Var("s", 1341 PTy(F32, 1342 PTy(F1, 1343 qTy))))), 1344 qVar"s3"]), 1345 [(TP[Var("v",F32), 1346 Var("s3",PTy(F1,qTy))], 1347 TP[Var("v",F32), 1348 Mop(Fst, 1349 Var("s", 1350 PTy(F32, 1351 PTy(F1,qTy)))), 1352 Var("s3",PTy(F1,qTy))])]), 1353 TP[Mop(Fst, 1354 Var("s0", 1355 PTy(F32,PTy(F1,qTy)))), 1356 Mop(Fst, 1357 Mop(Snd, 1358 Var("s0", 1359 PTy(F32, 1360 PTy(F1,qTy))))), 1361 Apply 1362 (Call 1363 ("write'MemA", 1364 ATy(qTy,qTy), 1365 TP[Var("v0",F32), 1366 Bop(Add, 1367 Mop(Fst, 1368 Var("s", 1369 PTy(F32, 1370 PTy(F1, 1371 qTy)))), 1372 LW(20,32)),LN 4]), 1373 Mop(Snd, 1374 Mop(Snd, 1375 Var("s0", 1376 PTy(F32, 1377 PTy(F1,qTy))))))]), 1378 Let(Var("s",PTy(F32,PTy(F1,qTy))), 1379 Let(TP[Var("v0",F32), 1380 Var("s0", 1381 PTy(F32,PTy(F1,qTy)))], 1382 CS(Let(TP[Var("v",F32), 1383 qVar"s3"], 1384 Let(qVar"s0", 1385 Mop(Snd, 1386 Mop(Snd, 1387 Var("s", 1388 PTy(F32, 1389 PTy(F1, 1390 qTy))))), 1391 TP[Apply 1392 (Call 1393 ("ReturnAddress", 1394 ATy(qTy, 1395 F32), 1396 LU), 1397 qVar"s0"), 1398 qVar"s0"]), 1399 TP[Var("v",F32), 1400 Mop(Fst, 1401 Mop(Snd, 1402 Var("s", 1403 PTy(F32, 1404 PTy(F1, 1405 qTy))))), 1406 qVar"s3"]), 1407 [(TP[Var("v",F32), 1408 Var("s3",PTy(F1,qTy))], 1409 TP[Var("v",F32), 1410 Mop(Fst, 1411 Var("s", 1412 PTy(F32, 1413 PTy(F1, 1414 qTy)))), 1415 Var("s3",PTy(F1,qTy))])]), 1416 TP[Mop(Fst, 1417 Var("s0", 1418 PTy(F32, 1419 PTy(F1,qTy)))), 1420 Mop(Fst, 1421 Mop(Snd, 1422 Var("s0", 1423 PTy(F32, 1424 PTy(F1, 1425 qTy))))), 1426 Apply 1427 (Call 1428 ("write'MemA", 1429 ATy(qTy,qTy), 1430 TP[Var("v0",F32), 1431 Bop(Add, 1432 Mop(Fst, 1433 Var("s", 1434 PTy(F32, 1435 PTy(F1, 1436 qTy)))), 1437 LW(20,32)), 1438 LN 4]), 1439 Mop(Snd, 1440 Mop(Snd, 1441 Var("s0", 1442 PTy(F32, 1443 PTy(F1, 1444 qTy))))))]), 1445 Let(qVar"s2", 1446 Apply 1447 (Call 1448 ("write'MemA", 1449 ATy(qTy,qTy), 1450 TP[CC[EX(Call 1451 ("reg'PSR", 1452 F32, 1453 Dest 1454 ("PSR", 1455 CTy"PSR", 1456 Mop(Snd, 1457 Mop(Snd, 1458 Var("s", 1459 PTy(F32, 1460 PTy(F1, 1461 qTy))))))), 1462 LN 31,LN 10, 1463 FTy 22), 1464 Mop(Fst, 1465 Mop(Snd, 1466 Var("s", 1467 PTy(F32, 1468 PTy(F1, 1469 qTy))))), 1470 EX(Call 1471 ("reg'PSR", 1472 F32, 1473 Dest 1474 ("PSR", 1475 CTy"PSR", 1476 Mop(Snd, 1477 Mop(Snd, 1478 Var("s", 1479 PTy(F32, 1480 PTy(F1, 1481 qTy))))))), 1482 LN 8,LN 0, 1483 FTy 9)], 1484 Bop(Add, 1485 Mop(Fst, 1486 Var("s", 1487 PTy(F32, 1488 PTy(F1, 1489 qTy)))), 1490 LW(28,32)),LN 4]), 1491 Mop(Snd, 1492 Mop(Snd, 1493 Var("s", 1494 PTy(F32, 1495 PTy(F1, 1496 qTy)))))), 1497 ITB([(EQ(Dest 1498 ("CurrentMode", 1499 CTy"Mode", 1500 qVar"s2"), 1501 LC("Mode_Handler", 1502 CTy"Mode")), 1503 Apply 1504 (Call 1505 ("write'LR", 1506 ATy(qTy,qTy), 1507 LW(4294967281,32)), 1508 qVar"s2")), 1509 (Mop(Not, 1510 Dest 1511 ("SPSEL",bTy, 1512 Dest 1513 ("CONTROL", 1514 CTy"CONTROL", 1515 qVar"s2"))), 1516 Apply 1517 (Call 1518 ("write'LR", 1519 ATy(qTy,qTy), 1520 LW(4294967289,32)), 1521 qVar"s2"))], 1522 Apply 1523 (Call 1524 ("write'LR", 1525 ATy(qTy,qTy), 1526 LW(4294967293,32)), 1527 qVar"s2")))))))))))))) 1528; 1529val ExceptionTaken_def = Def 1530 ("ExceptionTaken",Var("ExceptionNumber",FTy 6), 1531 Close 1532 (qVar"state", 1533 Let(TP[Var("v",F32),qVar"s"], 1534 Apply 1535 (Call 1536 ("MemA",ATy(qTy,PTy(F32,qTy)), 1537 TP[Bop(Add,Dest("VTOR",F32,qVar"state"), 1538 Bop(Mul,LW(4,32), 1539 Mop(Cast F32,Var("ExceptionNumber",FTy 6)))), 1540 LN 4]), 1541 Apply 1542 (Call("write'R",ATy(qTy,qTy),TP[LX F32,LW(12,4)]), 1543 Mop(Snd, 1544 Apply 1545 (For(TP[LN 0,LN 3, 1546 Close 1547 (nVar"i", 1548 Close 1549 (qVar"state", 1550 TP[LU, 1551 Apply 1552 (Call 1553 ("write'R",ATy(qTy,qTy), 1554 TP[LX F32, 1555 Mop(Cast F4,nVar"i")]), 1556 qVar"state")]))]),qVar"state")))), 1557 Let(qVar"s", 1558 Rupd 1559 ("CurrentMode", 1560 TP[Rupd 1561 ("PSR", 1562 TP[Apply 1563 (Call("write'PC",ATy(qTy,qTy),Var("v",F32)), 1564 qVar"s"),LX(CTy"PSR")]), 1565 LC("Mode_Handler",CTy"Mode")]), 1566 Let(qVar"s", 1567 Rupd 1568 ("PSR", 1569 TP[qVar"s", 1570 Rupd 1571 ("ExceptionNumber", 1572 TP[Dest("PSR",CTy"PSR",qVar"s"), 1573 Var("ExceptionNumber",FTy 6)])]), 1574 Let(qVar"s", 1575 Rupd 1576 ("CONTROL", 1577 TP[qVar"s", 1578 Rupd 1579 ("SPSEL", 1580 TP[Dest("CONTROL",CTy"CONTROL",qVar"s"),LF])]), 1581 Rupd 1582 ("ExceptionActive", 1583 TP[qVar"s", 1584 Fupd 1585 (Dest 1586 ("ExceptionActive",ATy(FTy 6,bTy),qVar"s"), 1587 Var("ExceptionNumber",FTy 6),LT)]))))))) 1588; 1589val ExceptionEntry_def = Def 1590 ("ExceptionEntry",AVar uTy, 1591 Close 1592 (qVar"state", 1593 CS(Dest("pending",OTy(CTy"ARM_Exception"),qVar"state"), 1594 [(Mop(Some,Var("e",CTy"ARM_Exception")), 1595 Apply 1596 (Call 1597 ("ExceptionTaken",ATy(qTy,qTy), 1598 Call("ExcNumber",FTy 6,Var("e",CTy"ARM_Exception"))), 1599 Apply(Call("PushStack",ATy(qTy,qTy),LU),qVar"state"))), 1600 (LO(CTy"ARM_Exception"),qVar"state")]))) 1601; 1602val PopStack_def = Def 1603 ("PopStack",TP[Var("frameptr",F32),Var("EXC_RETURN",FTy 28)], 1604 Close 1605 (qVar"state", 1606 Let(TP[Var("v",F32),qVar"s"], 1607 Apply 1608 (Call 1609 ("MemA",ATy(qTy,PTy(F32,qTy)),TP[Var("frameptr",F32),LN 4]), 1610 qVar"state"), 1611 Let(TP[Var("v",F32),qVar"s"], 1612 Apply 1613 (Call 1614 ("MemA",ATy(qTy,PTy(F32,qTy)), 1615 TP[Bop(Add,Var("frameptr",F32),LW(4,32)),LN 4]), 1616 Apply 1617 (Call("write'R",ATy(qTy,qTy),TP[Var("v",F32),LW(0,4)]), 1618 qVar"s")), 1619 Let(TP[Var("v",F32),qVar"s"], 1620 Apply 1621 (Call 1622 ("MemA",ATy(qTy,PTy(F32,qTy)), 1623 TP[Bop(Add,Var("frameptr",F32),LW(8,32)),LN 4]), 1624 Apply 1625 (Call 1626 ("write'R",ATy(qTy,qTy),TP[Var("v",F32),LW(1,4)]), 1627 qVar"s")), 1628 Let(TP[Var("v",F32),qVar"s"], 1629 Apply 1630 (Call 1631 ("MemA",ATy(qTy,PTy(F32,qTy)), 1632 TP[Bop(Add,Var("frameptr",F32),LW(12,32)),LN 4]), 1633 Apply 1634 (Call 1635 ("write'R",ATy(qTy,qTy), 1636 TP[Var("v",F32),LW(2,4)]),qVar"s")), 1637 Let(TP[Var("v",F32),qVar"s"], 1638 Apply 1639 (Call 1640 ("MemA",ATy(qTy,PTy(F32,qTy)), 1641 TP[Bop(Add,Var("frameptr",F32),LW(16,32)), 1642 LN 4]), 1643 Apply 1644 (Call 1645 ("write'R",ATy(qTy,qTy), 1646 TP[Var("v",F32),LW(3,4)]),qVar"s")), 1647 Let(TP[Var("v",F32),qVar"s"], 1648 Apply 1649 (Call 1650 ("MemA",ATy(qTy,PTy(F32,qTy)), 1651 TP[Bop(Add,Var("frameptr",F32), 1652 LW(20,32)),LN 4]), 1653 Apply 1654 (Call 1655 ("write'R",ATy(qTy,qTy), 1656 TP[Var("v",F32),LW(12,4)]),qVar"s")), 1657 Let(TP[Var("v",F32),qVar"s"], 1658 Apply 1659 (Call 1660 ("MemA",ATy(qTy,PTy(F32,qTy)), 1661 TP[Bop(Add,Var("frameptr",F32), 1662 LW(24,32)),LN 4]), 1663 Apply 1664 (Call 1665 ("write'LR",ATy(qTy,qTy), 1666 Var("v",F32)),qVar"s")), 1667 Let(TP[Var("v",F32),qVar"s"], 1668 Apply 1669 (Call 1670 ("MemA",ATy(qTy,PTy(F32,qTy)), 1671 TP[Bop(Add, 1672 Var("frameptr",F32), 1673 LW(28,32)),LN 4]), 1674 Apply 1675 (Call 1676 ("write'PC",ATy(qTy,qTy), 1677 Var("v",F32)),qVar"s")), 1678 Let(Var("spmask",F32), 1679 Mop(Cast F32, 1680 CC[EX(Var("v",F32),LN 9, 1681 LN 9,F1),LW(0,2)]), 1682 Let(qVar"s", 1683 Let(TP[bVar"b'3",bVar"b'2", 1684 bVar"b'1",bVar"b'0"], 1685 BL(4, 1686 EX(Var("EXC_RETURN", 1687 FTy 28),LN 3, 1688 LN 0,F4)), 1689 ITE(Bop(And, 1690 Mop(Not, 1691 bVar"b'1"), 1692 bVar"b'0"), 1693 ITB([(Mop(Not, 1694 bVar"b'2"), 1695 Apply 1696 (Call 1697 ("write'SP_main", 1698 ATy(qTy, 1699 qTy), 1700 Bop(BOr, 1701 Bop(Add, 1702 Apply 1703 (Const 1704 ("SP_main", 1705 ATy(qTy, 1706 F32)), 1707 qVar"s"), 1708 LW(32, 1709 32)), 1710 Var("spmask", 1711 F32))), 1712 qVar"s")), 1713 (Bop(And, 1714 bVar"b'3", 1715 bVar"b'2"), 1716 Apply 1717 (Call 1718 ("write'SP_process", 1719 ATy(qTy, 1720 qTy), 1721 Bop(BOr, 1722 Bop(Add, 1723 Apply 1724 (Const 1725 ("SP_process", 1726 ATy(qTy, 1727 F32)), 1728 qVar"s"), 1729 LW(32, 1730 32)), 1731 Var("spmask", 1732 F32))), 1733 qVar"s"))], 1734 qVar"s"),qVar"s")), 1735 Let(qVar"s", 1736 Rupd 1737 ("PSR", 1738 TP[qVar"s", 1739 Call 1740 ("write'reg'PSR", 1741 CTy"PSR", 1742 TP[Dest 1743 ("PSR", 1744 CTy"PSR", 1745 qVar"s"), 1746 BFI(LN 31, 1747 LN 27, 1748 EX(Var("v", 1749 F32), 1750 LN 31, 1751 LN 27, 1752 FTy 5), 1753 Call 1754 ("reg'PSR", 1755 F32, 1756 Dest 1757 ("PSR", 1758 CTy"PSR", 1759 qVar"s")))])]), 1760 Let(qVar"s", 1761 Rupd 1762 ("PSR", 1763 TP[qVar"s", 1764 Call 1765 ("write'reg'PSR", 1766 CTy"PSR", 1767 TP[Dest 1768 ("PSR", 1769 CTy"PSR", 1770 qVar"s"), 1771 BFI(LN 1772 24, 1773 LN 1774 24, 1775 Mop(Cast 1776 F1, 1777 Bop(Bit, 1778 Var("v", 1779 F32), 1780 LN 1781 24)), 1782 Call 1783 ("reg'PSR", 1784 F32, 1785 Dest 1786 ("PSR", 1787 CTy"PSR", 1788 qVar"s")))])]), 1789 Rupd 1790 ("PSR", 1791 TP[qVar"s", 1792 Call 1793 ("write'reg'PSR", 1794 CTy"PSR", 1795 TP[Dest 1796 ("PSR", 1797 CTy"PSR", 1798 qVar"s"), 1799 BFI(LN 5, 1800 LN 0, 1801 EX(Var("v", 1802 F32), 1803 LN 1804 5, 1805 LN 1806 0, 1807 FTy 6), 1808 Call 1809 ("reg'PSR", 1810 F32, 1811 Dest 1812 ("PSR", 1813 CTy"PSR", 1814 qVar"s")))])]))))))))))))))) 1815; 1816val DeActivate_def = Def 1817 ("DeActivate",Var("ReturningExceptionNumber",FTy 6), 1818 Close 1819 (qVar"state", 1820 Rupd 1821 ("ExceptionActive", 1822 TP[qVar"state", 1823 Fupd 1824 (Dest("ExceptionActive",ATy(FTy 6,bTy),qVar"state"), 1825 Var("ReturningExceptionNumber",FTy 6),LF)]))) 1826; 1827val IsOnes_def = Def 1828 ("IsOnes",Var("w",BTy"N"),EQ(Var("w",BTy"N"),Mop(Neg,LY(1,"N")))) 1829; 1830val ExceptionActiveBitCount_def = Def 1831 ("ExceptionActiveBitCount",AVar uTy, 1832 Close 1833 (qVar"state", 1834 Let(TP[nVar"r",Var("s1",PTy(nTy,qTy))], 1835 Let(Var("s",PTy(nTy,qTy)), 1836 Mop(Snd, 1837 Apply 1838 (For(TP[LN 0,LN 63, 1839 Close 1840 (nVar"i", 1841 Close 1842 (Var("state",PTy(nTy,qTy)), 1843 TP[LU, 1844 ITE(Apply 1845 (Dest 1846 ("ExceptionActive", 1847 ATy(FTy 6,bTy), 1848 Mop(Snd, 1849 Var("state", 1850 PTy(nTy,qTy)))), 1851 Mop(Cast(FTy 6),nVar"i")), 1852 TP[Bop(Add, 1853 Mop(Fst, 1854 Var("state", 1855 PTy(nTy,qTy))), 1856 LN 1), 1857 Mop(Snd, 1858 Var("state",PTy(nTy,qTy)))], 1859 Var("state",PTy(nTy,qTy)))]))]), 1860 TP[LN 0,qVar"state"])), 1861 TP[Mop(Fst,Var("s",PTy(nTy,qTy))),Var("s",PTy(nTy,qTy))]), 1862 TP[nVar"r",Mop(Snd,Var("s1",PTy(nTy,qTy)))]))) 1863; 1864val ExceptionReturn_def = Def 1865 ("ExceptionReturn",Var("EXC_RETURN",FTy 28), 1866 Close 1867 (qVar"state", 1868 Let(qVar"s", 1869 ITE(Mop(Not, 1870 EQ(Dest("CurrentMode",CTy"Mode",qVar"state"), 1871 LC("Mode_Handler",CTy"Mode"))), 1872 Mop(Snd, 1873 Apply 1874 (Call 1875 ("raise'exception",ATy(qTy,PTy(uTy,qTy)), 1876 Call 1877 ("ASSERT",CTy"exception", 1878 LS"CurrentMode == Mode_Handler")),qVar"state")), 1879 qVar"state"), 1880 Let(qVar"s", 1881 ITE(Mop(Not, 1882 Call 1883 ("IsOnes",bTy, 1884 EX(Var("EXC_RETURN",FTy 28),LN 27,LN 4,FTy 24))), 1885 Mop(Snd, 1886 Apply 1887 (Call 1888 ("raise'exception",ATy(qTy,PTy(uTy,qTy)), 1889 Call 1890 ("UNPREDICTABLE",CTy"exception", 1891 LS"ExceptionReturn")),qVar"s")),qVar"s"), 1892 Let(Var("v",FTy 6), 1893 Dest 1894 ("ExceptionNumber",FTy 6,Dest("PSR",CTy"PSR",qVar"s")), 1895 Let(TP[nVar"v0",qVar"s"], 1896 Apply 1897 (Call 1898 ("ExceptionActiveBitCount", 1899 ATy(qTy,PTy(nTy,qTy)),LU),qVar"s"), 1900 ITE(Mop(Not, 1901 Apply 1902 (Dest 1903 ("ExceptionActive",ATy(FTy 6,bTy), 1904 qVar"s"),Var("v",FTy 6))), 1905 Mop(Snd, 1906 Apply 1907 (Call 1908 ("raise'exception", 1909 ATy(qTy,PTy(uTy,qTy)), 1910 Call 1911 ("UNPREDICTABLE",CTy"exception", 1912 LS"ExceptionReturn")),qVar"s")), 1913 Let(Var("s",PTy(F32,qTy)), 1914 CS(EX(Var("EXC_RETURN",FTy 28),LN 3,LN 0,F4), 1915 [(LW(1,4), 1916 ITE(EQ(nVar"v0",LN 1), 1917 TP[LX F32, 1918 Mop(Snd, 1919 Apply 1920 (Call 1921 ("raise'exception", 1922 ATy(qTy,PTy(uTy,qTy)), 1923 Call 1924 ("UNPREDICTABLE", 1925 CTy"exception", 1926 LS"ExceptionReturn")), 1927 qVar"s"))], 1928 Let(qVar"s1", 1929 Rupd 1930 ("CurrentMode", 1931 TP[qVar"s", 1932 LC("Mode_Handler", 1933 CTy"Mode")]), 1934 TP[Apply 1935 (Const 1936 ("SP_main",ATy(qTy,F32)), 1937 qVar"s"), 1938 Rupd 1939 ("CONTROL", 1940 TP[qVar"s1", 1941 Rupd 1942 ("SPSEL", 1943 TP[Dest 1944 ("CONTROL", 1945 CTy"CONTROL", 1946 qVar"s1"),LF])])]))), 1947 (LW(9,4), 1948 ITE(Mop(Not,EQ(nVar"v0",LN 1)), 1949 TP[LX F32, 1950 Mop(Snd, 1951 Apply 1952 (Call 1953 ("raise'exception", 1954 ATy(qTy,PTy(uTy,qTy)), 1955 Call 1956 ("UNPREDICTABLE", 1957 CTy"exception", 1958 LS"ExceptionReturn")), 1959 qVar"s"))], 1960 Let(qVar"s1", 1961 Rupd 1962 ("CurrentMode", 1963 TP[qVar"s", 1964 LC("Mode_Thread", 1965 CTy"Mode")]), 1966 TP[Apply 1967 (Const 1968 ("SP_main",ATy(qTy,F32)), 1969 qVar"s"), 1970 Rupd 1971 ("CONTROL", 1972 TP[qVar"s1", 1973 Rupd 1974 ("SPSEL", 1975 TP[Dest 1976 ("CONTROL", 1977 CTy"CONTROL", 1978 qVar"s1"),LF])])]))), 1979 (LW(13,4), 1980 ITE(Mop(Not,EQ(nVar"v0",LN 1)), 1981 TP[LX F32, 1982 Mop(Snd, 1983 Apply 1984 (Call 1985 ("raise'exception", 1986 ATy(qTy,PTy(uTy,qTy)), 1987 Call 1988 ("UNPREDICTABLE", 1989 CTy"exception", 1990 LS"ExceptionReturn")), 1991 qVar"s"))], 1992 Let(qVar"s1", 1993 Rupd 1994 ("CurrentMode", 1995 TP[qVar"s", 1996 LC("Mode_Thread", 1997 CTy"Mode")]), 1998 TP[Apply 1999 (Const 2000 ("SP_process", 2001 ATy(qTy,F32)),qVar"s"), 2002 Rupd 2003 ("CONTROL", 2004 TP[qVar"s1", 2005 Rupd 2006 ("SPSEL", 2007 TP[Dest 2008 ("CONTROL", 2009 CTy"CONTROL", 2010 qVar"s1"),LT])])]))), 2011 (AVar F4, 2012 TP[LX F32, 2013 Mop(Snd, 2014 Apply 2015 (Call 2016 ("raise'exception", 2017 ATy(qTy,PTy(uTy,qTy)), 2018 Call 2019 ("UNPREDICTABLE", 2020 CTy"exception", 2021 LS"ExceptionReturn")), 2022 qVar"s"))])]), 2023 Let(qVar"s1", 2024 Apply 2025 (Call 2026 ("PopStack",ATy(qTy,qTy), 2027 TP[Mop(Fst,Var("s",PTy(F32,qTy))), 2028 Var("EXC_RETURN",FTy 28)]), 2029 Apply 2030 (Call 2031 ("DeActivate",ATy(qTy,qTy), 2032 Var("v",FTy 6)), 2033 Mop(Snd,Var("s",PTy(F32,qTy))))), 2034 ITB([(EQ(Dest 2035 ("CurrentMode",CTy"Mode", 2036 qVar"s1"), 2037 LC("Mode_Handler",CTy"Mode")), 2038 ITE(EQ(Dest 2039 ("ExceptionNumber",FTy 6, 2040 Dest 2041 ("PSR",CTy"PSR", 2042 qVar"s1")),LW(0,6)), 2043 Mop(Snd, 2044 Apply 2045 (Call 2046 ("raise'exception", 2047 ATy(qTy,PTy(uTy,qTy)), 2048 Call 2049 ("UNPREDICTABLE", 2050 CTy"exception", 2051 LS 2052 "ExceptionReturn")), 2053 qVar"s1")),qVar"s1")), 2054 (Mop(Not, 2055 EQ(Dest 2056 ("ExceptionNumber",FTy 6, 2057 Dest 2058 ("PSR",CTy"PSR", 2059 qVar"s1")),LW(0,6))), 2060 Mop(Snd, 2061 Apply 2062 (Call 2063 ("raise'exception", 2064 ATy(qTy,PTy(uTy,qTy)), 2065 Call 2066 ("UNPREDICTABLE", 2067 CTy"exception", 2068 LS"ExceptionReturn")), 2069 qVar"s1")))],qVar"s1")))))))))) 2070; 2071val CallSupervisor_def = Def 2072 ("CallSupervisor",AVar uTy, 2073 Close 2074 (qVar"state", 2075 Apply 2076 (Call("Raise",ATy(qTy,qTy),Const("SVCall",CTy"ARM_Exception")), 2077 qVar"state"))) 2078; 2079val BranchTo_def = Def 2080 ("BranchTo",Var("address",F32), 2081 Close 2082 (qVar"state", 2083 Apply(Call("write'PC",ATy(qTy,qTy),Var("address",F32)),qVar"state"))) 2084; 2085val BranchWritePC_def = Def 2086 ("BranchWritePC",Var("address",F32), 2087 Close 2088 (qVar"state", 2089 Apply 2090 (Call 2091 ("BranchTo",ATy(qTy,qTy), 2092 CC[EX(Var("address",F32),LN 31,LN 1,FTy 31),LW(0,1)]), 2093 qVar"state"))) 2094; 2095val BXWritePC_def = Def 2096 ("BXWritePC",Var("address",F32), 2097 Close 2098 (qVar"state", 2099 ITE(Bop(And, 2100 EQ(Dest("CurrentMode",CTy"Mode",qVar"state"), 2101 LC("Mode_Handler",CTy"Mode")), 2102 EQ(EX(Var("address",F32),LN 31,LN 28,F4),LW(15,4))), 2103 Apply 2104 (Call 2105 ("ExceptionReturn",ATy(qTy,qTy), 2106 EX(Var("address",F32),LN 27,LN 0,FTy 28)),qVar"state"), 2107 Apply 2108 (Call 2109 ("BranchTo",ATy(qTy,qTy), 2110 CC[EX(Var("address",F32),LN 31,LN 1,FTy 31),LW(0,1)]), 2111 ITE(Mop(Not,Bop(Bit,Var("address",F32),LN 0)), 2112 Apply 2113 (Call 2114 ("Raise",ATy(qTy,qTy), 2115 Const("HardFault",CTy"ARM_Exception")),qVar"state"), 2116 qVar"state"))))) 2117; 2118val BLXWritePC_def = Def 2119 ("BLXWritePC",Var("address",F32), 2120 Close 2121 (qVar"state", 2122 Apply 2123 (Call 2124 ("BranchTo",ATy(qTy,qTy), 2125 CC[EX(Var("address",F32),LN 31,LN 1,FTy 31),LW(0,1)]), 2126 ITE(Mop(Not,Bop(Bit,Var("address",F32),LN 0)), 2127 Apply 2128 (Call 2129 ("Raise",ATy(qTy,qTy), 2130 Const("HardFault",CTy"ARM_Exception")),qVar"state"), 2131 qVar"state")))) 2132; 2133val LoadWritePC_def = Def 2134 ("LoadWritePC",Var("address",F32), 2135 Close 2136 (qVar"state", 2137 Apply(Call("BXWritePC",ATy(qTy,qTy),Var("address",F32)),qVar"state"))) 2138; 2139val ALUWritePC_def = Def 2140 ("ALUWritePC",Var("address",F32), 2141 Close 2142 (qVar"state", 2143 Apply 2144 (Call("BranchWritePC",ATy(qTy,qTy),Var("address",F32)),qVar"state"))) 2145; 2146val IncPC_def = Def 2147 ("IncPC",AVar uTy, 2148 Close 2149 (qVar"state", 2150 Apply 2151 (Call 2152 ("BranchTo",ATy(qTy,qTy), 2153 Bop(Add, 2154 Apply 2155 (Dest("REG",ATy(CTy"RName",F32),qVar"state"), 2156 LC("RName_PC",CTy"RName")), 2157 Dest("pcinc",F32,qVar"state"))),qVar"state"))) 2158; 2159val HighestSetBit_def = Def 2160 ("HighestSetBit",Var("w",BTy"N"), 2161 ITE(EQ(Var("w",BTy"N"),LY(0,"N")),Mop(Neg,LI 1), 2162 Mop(Cast iTy,Mop(Log,Var("w",BTy"N"))))) 2163; 2164val CountLeadingZeroBits_def = Def 2165 ("CountLeadingZeroBits",Var("w",BTy"N"), 2166 Mop(Cast nTy, 2167 Bop(Sub,Bop(Sub,Mop(Cast iTy,Mop(Size,LY(0,"N"))),LI 1), 2168 Call("HighestSetBit",iTy,Var("w",BTy"N"))))) 2169; 2170val LowestSetBit_def = Def 2171 ("LowestSetBit",Var("w",BTy"N"), 2172 Call("CountLeadingZeroBits",nTy,Mop(Rev,Var("w",BTy"N")))) 2173; 2174val BitCount_def = Def 2175 ("BitCount",Var("w",BTy"N"), 2176 Mop(Fst, 2177 Mop(Snd, 2178 Apply 2179 (For(TP[LN 0,Bop(Sub,Mop(Size,LY(0,"N")),LN 1), 2180 Close 2181 (nVar"i", 2182 Close 2183 (Var("state",PTy(nTy,uTy)), 2184 TP[LU, 2185 ITE(Bop(Bit,Var("w",BTy"N"),nVar"i"), 2186 TP[Bop(Add, 2187 Mop(Fst,Var("state",PTy(nTy,uTy))), 2188 LN 1),LU], 2189 Var("state",PTy(nTy,uTy)))]))]), 2190 TP[LN 0,LU])))) 2191; 2192val SignExtendFrom_def = Def 2193 ("SignExtendFrom",TP[Var("w",BTy"N"),nVar"p"], 2194 Let(nVar"s",Bop(Sub,Mop(Size,LY(0,"N")),nVar"p"), 2195 Bop(Asr,Bop(Lsl,Var("w",BTy"N"),nVar"s"),nVar"s"))) 2196; 2197val Extend_def = Def 2198 ("Extend",TP[bVar"unsigned",Var("w",BTy"M")], 2199 ITE(bVar"unsigned",Mop(Cast(BTy"N"),Var("w",BTy"M")), 2200 Mop(SE(BTy"N"),Var("w",BTy"M")))) 2201; 2202val UInt_def = Def 2203 ("UInt",Var("w",BTy"N"),Mop(Cast iTy,Mop(Cast nTy,Var("w",BTy"N")))) 2204; 2205val LSL_C_def = Def 2206 ("LSL_C",TP[Var("x",BTy"N"),nVar"shift"], 2207 Close 2208 (qVar"state", 2209 TP[TP[Bop(Lsl,Var("x",BTy"N"),nVar"shift"), 2210 Bop(Bit, 2211 CC[Mop(Cast vTy,Var("x",BTy"N")), 2212 Bop(Rep,LV"0",nVar"shift")],Mop(Size,LY(0,"N")))], 2213 ITE(EQ(nVar"shift",LN 0), 2214 Mop(Snd, 2215 Apply 2216 (Call 2217 ("raise'exception",ATy(qTy,PTy(uTy,qTy)), 2218 Call("ASSERT",CTy"exception",LS"LSL_C")), 2219 qVar"state")),qVar"state")])) 2220; 2221val LSL_def = Def 2222 ("LSL",TP[Var("x",BTy"N"),nVar"shift"], 2223 Close 2224 (qVar"state", 2225 ITE(EQ(nVar"shift",LN 0),TP[Var("x",BTy"N"),qVar"state"], 2226 Let(TP[Var("v",PTy(BTy"N",bTy)),qVar"s"], 2227 Apply 2228 (Call 2229 ("LSL_C",ATy(qTy,PTy(PTy(BTy"N",bTy),qTy)), 2230 TP[Var("x",BTy"N"),nVar"shift"]),qVar"state"), 2231 TP[Mop(Fst,Var("v",PTy(BTy"N",bTy))),qVar"s"])))) 2232; 2233val LSR_C_def = Def 2234 ("LSR_C",TP[Var("x",BTy"N"),nVar"shift"], 2235 Close 2236 (qVar"state", 2237 TP[TP[Bop(Lsr,Var("x",BTy"N"),nVar"shift"), 2238 Bop(And,Bop(Le,nVar"shift",Mop(Size,LY(0,"N"))), 2239 Bop(Bit,Var("x",BTy"N"),Bop(Sub,nVar"shift",LN 1)))], 2240 ITE(EQ(nVar"shift",LN 0), 2241 Mop(Snd, 2242 Apply 2243 (Call 2244 ("raise'exception",ATy(qTy,PTy(uTy,qTy)), 2245 Call("ASSERT",CTy"exception",LS"LSR_C")), 2246 qVar"state")),qVar"state")])) 2247; 2248val LSR_def = Def 2249 ("LSR",TP[Var("x",BTy"N"),nVar"shift"], 2250 Close 2251 (qVar"state", 2252 ITE(EQ(nVar"shift",LN 0),TP[Var("x",BTy"N"),qVar"state"], 2253 Let(TP[Var("v",PTy(BTy"N",bTy)),qVar"s"], 2254 Apply 2255 (Call 2256 ("LSR_C",ATy(qTy,PTy(PTy(BTy"N",bTy),qTy)), 2257 TP[Var("x",BTy"N"),nVar"shift"]),qVar"state"), 2258 TP[Mop(Fst,Var("v",PTy(BTy"N",bTy))),qVar"s"])))) 2259; 2260val ASR_C_def = Def 2261 ("ASR_C",TP[Var("x",BTy"N"),nVar"shift"], 2262 Close 2263 (qVar"state", 2264 TP[TP[Bop(Asr,Var("x",BTy"N"),nVar"shift"), 2265 Bop(Bit,Var("x",BTy"N"), 2266 Bop(Sub,Mop(Min,TP[Mop(Size,LY(0,"N")),nVar"shift"]),LN 1))], 2267 ITE(EQ(nVar"shift",LN 0), 2268 Mop(Snd, 2269 Apply 2270 (Call 2271 ("raise'exception",ATy(qTy,PTy(uTy,qTy)), 2272 Call("ASSERT",CTy"exception",LS"ASR_C")), 2273 qVar"state")),qVar"state")])) 2274; 2275val ASR_def = Def 2276 ("ASR",TP[Var("x",BTy"N"),nVar"shift"], 2277 Close 2278 (qVar"state", 2279 ITE(EQ(nVar"shift",LN 0),TP[Var("x",BTy"N"),qVar"state"], 2280 Let(TP[Var("v",PTy(BTy"N",bTy)),qVar"s"], 2281 Apply 2282 (Call 2283 ("ASR_C",ATy(qTy,PTy(PTy(BTy"N",bTy),qTy)), 2284 TP[Var("x",BTy"N"),nVar"shift"]),qVar"state"), 2285 TP[Mop(Fst,Var("v",PTy(BTy"N",bTy))),qVar"s"])))) 2286; 2287val ROR_C_def = Def 2288 ("ROR_C",TP[Var("x",BTy"N"),nVar"shift"], 2289 Close 2290 (qVar"state", 2291 TP[Let(Var("result",BTy"N"),Bop(Ror,Var("x",BTy"N"),nVar"shift"), 2292 TP[Var("result",BTy"N"),Mop(Msb,Var("result",BTy"N"))]), 2293 ITE(EQ(nVar"shift",LN 0), 2294 Mop(Snd, 2295 Apply 2296 (Call 2297 ("raise'exception",ATy(qTy,PTy(uTy,qTy)), 2298 Call("ASSERT",CTy"exception",LS"ROR_C")), 2299 qVar"state")),qVar"state")])) 2300; 2301val ROR_def = Def 2302 ("ROR",TP[Var("x",BTy"N"),nVar"shift"], 2303 Close 2304 (qVar"state", 2305 ITE(EQ(nVar"shift",LN 0),TP[Var("x",BTy"N"),qVar"state"], 2306 Let(TP[Var("v",PTy(BTy"N",bTy)),qVar"s"], 2307 Apply 2308 (Call 2309 ("ROR_C",ATy(qTy,PTy(PTy(BTy"N",bTy),qTy)), 2310 TP[Var("x",BTy"N"),nVar"shift"]),qVar"state"), 2311 TP[Mop(Fst,Var("v",PTy(BTy"N",bTy))),qVar"s"])))) 2312; 2313val RRX_C_def = Def 2314 ("RRX_C",TP[Var("x",BTy"N"),bVar"carry_in"], 2315 TP[Mop(Cast(BTy"N"), 2316 CC[Mop(Cast vTy,bVar"carry_in"), 2317 EX(Mop(Cast vTy,Var("x",BTy"N")), 2318 Bop(Sub,Mop(Size,LY(0,"N")),LN 1),LN 1,vTy)]), 2319 Bop(Bit,Var("x",BTy"N"),LN 0)]) 2320; 2321val RRX_def = Def 2322 ("RRX",TP[Var("x",BTy"N"),bVar"carry_in"], 2323 Mop(Fst, 2324 Call("RRX_C",PTy(BTy"N",bTy),TP[Var("x",BTy"N"),bVar"carry_in"]))) 2325; 2326val DecodeImmShift_def = Def 2327 ("DecodeImmShift",TP[Var("typ",FTy 2),Var("imm5",FTy 5)], 2328 CS(Var("typ",FTy 2), 2329 [(LW(0,2), 2330 TP[LC("SRType_LSL",CTy"SRType"),Mop(Cast nTy,Var("imm5",FTy 5))]), 2331 (LW(1,2), 2332 TP[LC("SRType_LSR",CTy"SRType"), 2333 ITE(EQ(Var("imm5",FTy 5),LW(0,5)),LN 32, 2334 Mop(Cast nTy,Var("imm5",FTy 5)))]), 2335 (LW(2,2), 2336 TP[LC("SRType_ASR",CTy"SRType"), 2337 ITE(EQ(Var("imm5",FTy 5),LW(0,5)),LN 32, 2338 Mop(Cast nTy,Var("imm5",FTy 5)))]), 2339 (LW(3,2), 2340 ITE(EQ(Var("imm5",FTy 5),LW(0,5)), 2341 TP[LC("SRType_RRX",CTy"SRType"),LN 1], 2342 TP[LC("SRType_ROR",CTy"SRType"), 2343 Mop(Cast nTy,Var("imm5",FTy 5))]))])) 2344; 2345val DecodeRegShift_def = Def 2346 ("DecodeRegShift",Var("typ",FTy 2), 2347 CS(Var("typ",FTy 2), 2348 [(LW(0,2),LC("SRType_LSL",CTy"SRType")), 2349 (LW(1,2),LC("SRType_LSR",CTy"SRType")), 2350 (LW(2,2),LC("SRType_ASR",CTy"SRType")), 2351 (LW(3,2),LC("SRType_ROR",CTy"SRType"))])) 2352; 2353val Shift_C_def = Def 2354 ("Shift_C", 2355 TP[Var("value",BTy"N"),Var("typ",CTy"SRType"),nVar"amount", 2356 bVar"carry_in"], 2357 Close 2358 (qVar"state", 2359 ITE(EQ(nVar"amount",LN 0), 2360 TP[TP[Var("value",BTy"N"),bVar"carry_in"],qVar"state"], 2361 CS(Var("typ",CTy"SRType"), 2362 [(LC("SRType_LSL",CTy"SRType"), 2363 Apply 2364 (Call 2365 ("LSL_C",ATy(qTy,PTy(PTy(BTy"N",bTy),qTy)), 2366 TP[Var("value",BTy"N"),nVar"amount"]),qVar"state")), 2367 (LC("SRType_LSR",CTy"SRType"), 2368 Apply 2369 (Call 2370 ("LSR_C",ATy(qTy,PTy(PTy(BTy"N",bTy),qTy)), 2371 TP[Var("value",BTy"N"),nVar"amount"]),qVar"state")), 2372 (LC("SRType_ASR",CTy"SRType"), 2373 Apply 2374 (Call 2375 ("ASR_C",ATy(qTy,PTy(PTy(BTy"N",bTy),qTy)), 2376 TP[Var("value",BTy"N"),nVar"amount"]),qVar"state")), 2377 (LC("SRType_ROR",CTy"SRType"), 2378 Apply 2379 (Call 2380 ("ROR_C",ATy(qTy,PTy(PTy(BTy"N",bTy),qTy)), 2381 TP[Var("value",BTy"N"),nVar"amount"]),qVar"state")), 2382 (LC("SRType_RRX",CTy"SRType"), 2383 TP[Call 2384 ("RRX_C",PTy(BTy"N",bTy), 2385 TP[Var("value",BTy"N"),bVar"carry_in"]),qVar"state"])])))) 2386; 2387val Shift_def = Def 2388 ("Shift", 2389 TP[Var("value",BTy"N"),Var("typ",CTy"SRType"),nVar"amount", 2390 bVar"carry_in"], 2391 Close 2392 (qVar"state", 2393 Let(TP[Var("v",PTy(BTy"N",bTy)),qVar"s"], 2394 Apply 2395 (Call 2396 ("Shift_C",ATy(qTy,PTy(PTy(BTy"N",bTy),qTy)), 2397 TP[Var("value",BTy"N"),Var("typ",CTy"SRType"), 2398 nVar"amount",bVar"carry_in"]),qVar"state"), 2399 TP[Mop(Fst,Var("v",PTy(BTy"N",bTy))),qVar"s"]))) 2400; 2401val AddWithCarry_def = Def 2402 ("AddWithCarry",TP[Var("x",BTy"N"),Var("y",BTy"N"),bVar"carry_in"], 2403 Let(nVar"unsigned_sum", 2404 Bop(Add, 2405 Bop(Add,Mop(Cast nTy,Var("x",BTy"N")), 2406 Mop(Cast nTy,Var("y",BTy"N"))),Mop(Cast nTy,bVar"carry_in")), 2407 Let(Var("result",BTy"N"),Mop(Cast(BTy"N"),nVar"unsigned_sum"), 2408 TP[Var("result",BTy"N"), 2409 Mop(Not, 2410 EQ(Mop(Cast nTy,Var("result",BTy"N")),nVar"unsigned_sum")), 2411 Mop(Not, 2412 EQ(Mop(Cast iTy,Var("result",BTy"N")), 2413 Bop(Add, 2414 Bop(Add,Mop(Cast iTy,Var("x",BTy"N")), 2415 Mop(Cast iTy,Var("y",BTy"N"))), 2416 Mop(Cast iTy,bVar"carry_in"))))]))) 2417; 2418val DataProcessingALU_def = Def 2419 ("DataProcessingALU", 2420 TP[Var("opc",F4),Var("a",F32),Var("b",F32),bVar"c"], 2421 CS(Var("opc",F4), 2422 [(LW(0,4),TP[Bop(BAnd,Var("a",F32),Var("b",F32)),bVar"c",LX bTy]), 2423 (LW(8,4),TP[Bop(BAnd,Var("a",F32),Var("b",F32)),bVar"c",LX bTy]), 2424 (LW(1,4),TP[Bop(BXor,Var("a",F32),Var("b",F32)),bVar"c",LX bTy]), 2425 (LW(9,4),TP[Bop(BXor,Var("a",F32),Var("b",F32)),bVar"c",LX bTy]), 2426 (LW(2,4), 2427 Call 2428 ("AddWithCarry",PTy(F32,PTy(bTy,bTy)), 2429 TP[Var("a",F32),Mop(BNot,Var("b",F32)),LT])), 2430 (LW(10,4), 2431 Call 2432 ("AddWithCarry",PTy(F32,PTy(bTy,bTy)), 2433 TP[Var("a",F32),Mop(BNot,Var("b",F32)),LT])), 2434 (LW(3,4), 2435 Call 2436 ("AddWithCarry",PTy(F32,PTy(bTy,bTy)), 2437 TP[Mop(BNot,Var("a",F32)),Var("b",F32),LT])), 2438 (LW(4,4), 2439 Call 2440 ("AddWithCarry",PTy(F32,PTy(bTy,bTy)), 2441 TP[Var("a",F32),Var("b",F32),LF])), 2442 (LW(11,4), 2443 Call 2444 ("AddWithCarry",PTy(F32,PTy(bTy,bTy)), 2445 TP[Var("a",F32),Var("b",F32),LF])), 2446 (LW(5,4), 2447 Call 2448 ("AddWithCarry",PTy(F32,PTy(bTy,bTy)), 2449 TP[Var("a",F32),Var("b",F32),bVar"c"])), 2450 (LW(6,4), 2451 Call 2452 ("AddWithCarry",PTy(F32,PTy(bTy,bTy)), 2453 TP[Var("a",F32),Mop(BNot,Var("b",F32)),bVar"c"])), 2454 (LW(7,4), 2455 Call 2456 ("AddWithCarry",PTy(F32,PTy(bTy,bTy)), 2457 TP[Mop(BNot,Var("a",F32)),Var("b",F32),bVar"c"])), 2458 (LW(12,4),TP[Bop(BOr,Var("a",F32),Var("b",F32)),bVar"c",LX bTy]), 2459 (LW(13,4),TP[Var("b",F32),bVar"c",LX bTy]), 2460 (LW(14,4), 2461 TP[Bop(BAnd,Var("a",F32),Mop(BNot,Var("b",F32))),bVar"c",LX bTy]), 2462 (LW(15,4),TP[Mop(BNot,Var("b",F32)),bVar"c",LX bTy])])) 2463; 2464val ArithmeticOpcode_def = Def 2465 ("ArithmeticOpcode",Var("opc",F4), 2466 Bop(And, 2467 Bop(Or,Bop(Bit,Var("opc",F4),LN 2),Bop(Bit,Var("opc",F4),LN 1)), 2468 Mop(Not, 2469 Bop(And,Bop(Bit,Var("opc",F4),LN 3),Bop(Bit,Var("opc",F4),LN 2))))) 2470; 2471val dfn'BranchTarget_def = Def 2472 ("dfn'BranchTarget",Var("imm32",F32), 2473 Close 2474 (qVar"state", 2475 Let(qVar"s", 2476 Apply 2477 (Call 2478 ("BranchWritePC",ATy(qTy,qTy), 2479 Bop(Add,Apply(Const("PC",ATy(qTy,F32)),qVar"state"), 2480 Var("imm32",F32))),qVar"state"), 2481 Rupd 2482 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 3)])))) 2483; 2484val dfn'BranchExchange_def = Def 2485 ("dfn'BranchExchange",Var("m",F4), 2486 Close 2487 (qVar"state", 2488 Let(qVar"s", 2489 Apply 2490 (Call 2491 ("BXWritePC",ATy(qTy,qTy), 2492 Apply(Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state")), 2493 qVar"state"), 2494 Rupd 2495 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 3)])))) 2496; 2497val dfn'BranchLinkImmediate_def = Def 2498 ("dfn'BranchLinkImmediate",Var("imm32",F32), 2499 Close 2500 (qVar"state", 2501 Let(TP[Var("v",F32),qVar"s"], 2502 Let(qVar"s0", 2503 Apply 2504 (Call 2505 ("write'LR",ATy(qTy,qTy), 2506 CC[EX(Apply(Const("PC",ATy(qTy,F32)),qVar"state"), 2507 LN 31,LN 1,FTy 31),LW(1,1)]),qVar"state"), 2508 TP[Apply(Const("PC",ATy(qTy,F32)),qVar"s0"),qVar"s0"]), 2509 Let(qVar"s", 2510 Apply 2511 (Call 2512 ("BranchWritePC",ATy(qTy,qTy), 2513 Bop(Add,Var("v",F32),Var("imm32",F32))),qVar"s"), 2514 Rupd 2515 ("count", 2516 TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 4)]))))) 2517; 2518val dfn'BranchLinkExchangeRegister_def = Def 2519 ("dfn'BranchLinkExchangeRegister",Var("m",F4), 2520 Close 2521 (qVar"state", 2522 Let(qVar"s", 2523 Apply 2524 (Call 2525 ("BLXWritePC",ATy(qTy,qTy), 2526 Apply(Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state")), 2527 Apply 2528 (Call 2529 ("write'LR",ATy(qTy,qTy), 2530 CC[EX(Bop(Sub, 2531 Apply(Const("PC",ATy(qTy,F32)),qVar"state"), 2532 LW(2,32)),LN 31,LN 1,FTy 31),LW(1,1)]), 2533 qVar"state")), 2534 Rupd 2535 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 3)])))) 2536; 2537val DataProcessing_def = Def 2538 ("DataProcessing", 2539 TP[Var("opc",F4),bVar"setflags",Var("d",F4),Var("n",F4), 2540 Var("imm32",F32),bVar"C"], 2541 Close 2542 (qVar"state", 2543 Let(TP[Var("result",F32),bVar"carry",bVar"overflow"], 2544 Call 2545 ("DataProcessingALU",PTy(F32,PTy(bTy,bTy)), 2546 TP[Var("opc",F4), 2547 ITB([(Bop(Or,EQ(Var("opc",F4),LW(13,4)), 2548 EQ(Var("opc",F4),LW(15,4))),LW(0,32)), 2549 (Bop(And,Bop(In,Var("opc",F4),SL[LW(4,4),LW(2,4)]), 2550 Bop(And,EQ(Var("n",F4),LW(15,4)), 2551 Mop(Not,bVar"setflags"))), 2552 Call 2553 ("Align",F32, 2554 TP[Apply(Const("PC",ATy(qTy,F32)),qVar"state"), 2555 LN 4]))], 2556 Apply(Call("R",ATy(qTy,F32),Var("n",F4)),qVar"state")), 2557 Var("imm32",F32),bVar"C"]), 2558 Let(qVar"s", 2559 ITE(Mop(Not,EQ(EX(Var("opc",F4),LN 3,LN 2,FTy 2),LW(2,2))), 2560 Apply 2561 (Call 2562 ("write'R",ATy(qTy,qTy), 2563 TP[Var("result",F32),Var("d",F4)]),qVar"state"), 2564 qVar"state"), 2565 Let(qVar"s", 2566 Apply 2567 (Call("IncPC",ATy(qTy,qTy),LU), 2568 ITE(bVar"setflags", 2569 Let(qVar"s", 2570 Rupd 2571 ("PSR", 2572 TP[qVar"s", 2573 Rupd 2574 ("N", 2575 TP[Dest("PSR",CTy"PSR",qVar"s"), 2576 Bop(Bit,Var("result",F32),LN 31)])]), 2577 Let(qVar"s", 2578 Rupd 2579 ("PSR", 2580 TP[qVar"s", 2581 Rupd 2582 ("Z", 2583 TP[Dest("PSR",CTy"PSR",qVar"s"), 2584 EQ(Var("result",F32),LW(0,32))])]), 2585 Let(qVar"s", 2586 Rupd 2587 ("PSR", 2588 TP[qVar"s", 2589 Rupd 2590 ("C", 2591 TP[Dest 2592 ("PSR",CTy"PSR",qVar"s"), 2593 bVar"carry"])]), 2594 ITE(Call 2595 ("ArithmeticOpcode",bTy, 2596 Var("opc",F4)), 2597 Rupd 2598 ("PSR", 2599 TP[qVar"s", 2600 Rupd 2601 ("V", 2602 TP[Dest 2603 ("PSR",CTy"PSR", 2604 qVar"s"), 2605 bVar"overflow"])]), 2606 qVar"s")))),qVar"s")), 2607 Rupd 2608 ("count", 2609 TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 1)])))))) 2610; 2611val DataProcessingPC_def = Def 2612 ("DataProcessingPC", 2613 TP[Var("opc",F4),Var("n",F4),Var("imm32",F32),bVar"C"], 2614 Close 2615 (qVar"state", 2616 Let(TP[Var("result",F32),AVar(PTy(bTy,bTy))], 2617 Call 2618 ("DataProcessingALU",PTy(F32,PTy(bTy,bTy)), 2619 TP[Var("opc",F4), 2620 ITB([(EQ(Var("opc",F4),LW(13,4)),LW(0,32)), 2621 (EQ(Var("n",F4),LW(15,4)), 2622 Apply(Const("PC",ATy(qTy,F32)),qVar"state"))], 2623 Apply(Call("R",ATy(qTy,F32),Var("n",F4)),qVar"state")), 2624 Var("imm32",F32),bVar"C"]), 2625 Let(qVar"s", 2626 Apply 2627 (Call("ALUWritePC",ATy(qTy,qTy),Var("result",F32)), 2628 qVar"state"), 2629 Rupd 2630 ("count", 2631 TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 3)]))))) 2632; 2633val dfn'Move_def = Def 2634 ("dfn'Move",TP[Var("d",F4),Var("imm32",F32)], 2635 Close 2636 (qVar"state", 2637 Apply 2638 (Call 2639 ("DataProcessing",ATy(qTy,qTy), 2640 TP[LW(13,4),LT,Var("d",F4),LW(15,4),Var("imm32",F32), 2641 Dest("C",bTy,Dest("PSR",CTy"PSR",qVar"state"))]), 2642 qVar"state"))) 2643; 2644val dfn'CompareImmediate_def = Def 2645 ("dfn'CompareImmediate",TP[Var("n",F4),Var("imm32",F32)], 2646 Close 2647 (qVar"state", 2648 Apply 2649 (Call 2650 ("DataProcessing",ATy(qTy,qTy), 2651 TP[LW(10,4),LT,LX F4,Var("n",F4),Var("imm32",F32), 2652 Dest("C",bTy,Dest("PSR",CTy"PSR",qVar"state"))]), 2653 qVar"state"))) 2654; 2655val dfn'ArithLogicImmediate_def = Def 2656 ("dfn'ArithLogicImmediate", 2657 TP[Var("opc",F4),bVar"setflags",Var("d",F4),Var("n",F4), 2658 Var("imm32",F32)], 2659 Close 2660 (qVar"state", 2661 Apply 2662 (Call 2663 ("DataProcessing",ATy(qTy,qTy), 2664 TP[Var("opc",F4),bVar"setflags",Var("d",F4),Var("n",F4), 2665 Var("imm32",F32), 2666 Dest("C",bTy,Dest("PSR",CTy"PSR",qVar"state"))]), 2667 qVar"state"))) 2668; 2669val doRegister_def = Def 2670 ("doRegister", 2671 TP[Var("opc",F4),bVar"setflags",Var("d",F4),Var("n",F4),Var("m",F4), 2672 Var("shift_t",CTy"SRType"),nVar"shift_n"], 2673 Close 2674 (qVar"state", 2675 Let(TP[Var("v",PTy(F32,bTy)),qVar"s"], 2676 Apply 2677 (Call 2678 ("Shift_C",ATy(qTy,PTy(PTy(F32,bTy),qTy)), 2679 TP[Apply(Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"), 2680 Var("shift_t",CTy"SRType"),nVar"shift_n", 2681 Dest("C",bTy,Dest("PSR",CTy"PSR",qVar"state"))]), 2682 qVar"state"), 2683 Let(TP[Var("shifted",F32),bVar"carry"],Var("v",PTy(F32,bTy)), 2684 Let(bVar"v", 2685 ITE(Call("ArithmeticOpcode",bTy,Var("opc",F4)), 2686 Dest("C",bTy,Dest("PSR",CTy"PSR",qVar"s")), 2687 bVar"carry"), 2688 ITE(EQ(Var("d",F4),LW(15,4)), 2689 Apply 2690 (Call 2691 ("DataProcessingPC",ATy(qTy,qTy), 2692 TP[Var("opc",F4),Var("n",F4), 2693 Var("shifted",F32),bVar"v"]),qVar"s"), 2694 Apply 2695 (Call 2696 ("DataProcessing",ATy(qTy,qTy), 2697 TP[Var("opc",F4),bVar"setflags",Var("d",F4), 2698 Var("n",F4),Var("shifted",F32),bVar"v"]), 2699 qVar"s"))))))) 2700; 2701val dfn'Register_def = Def 2702 ("dfn'Register", 2703 TP[Var("opc",F4),bVar"setflags",Var("d",F4),Var("n",F4),Var("m",F4)], 2704 Close 2705 (qVar"state", 2706 Apply 2707 (Call 2708 ("doRegister",ATy(qTy,qTy), 2709 TP[Var("opc",F4),bVar"setflags",Var("d",F4),Var("n",F4), 2710 Var("m",F4),LC("SRType_LSL",CTy"SRType"),LN 0]),qVar"state"))) 2711; 2712val dfn'TestCompareRegister_def = Def 2713 ("dfn'TestCompareRegister",TP[Var("opc",FTy 2),Var("n",F4),Var("m",F4)], 2714 Close 2715 (qVar"state", 2716 Apply 2717 (Call 2718 ("doRegister",ATy(qTy,qTy), 2719 TP[CC[LW(2,2),Var("opc",FTy 2)],LT,LW(0,4),Var("n",F4), 2720 Var("m",F4),LC("SRType_LSL",CTy"SRType"),LN 0]),qVar"state"))) 2721; 2722val dfn'ShiftImmediate_def = Def 2723 ("dfn'ShiftImmediate", 2724 TP[bVar"negate",bVar"setflags",Var("d",F4),Var("m",F4), 2725 Var("shift_t",CTy"SRType"),nVar"shift_n"], 2726 Close 2727 (qVar"state", 2728 ITE(bVar"negate", 2729 Apply 2730 (Call 2731 ("doRegister",ATy(qTy,qTy), 2732 TP[LW(15,4),bVar"setflags",Var("d",F4),LW(15,4), 2733 Var("m",F4),Var("shift_t",CTy"SRType"),nVar"shift_n"]), 2734 qVar"state"), 2735 Apply 2736 (Call 2737 ("doRegister",ATy(qTy,qTy), 2738 TP[LW(13,4),bVar"setflags",Var("d",F4),LX F4,Var("m",F4), 2739 Var("shift_t",CTy"SRType"),nVar"shift_n"]),qVar"state")))) 2740; 2741val dfn'ShiftRegister_def = Def 2742 ("dfn'ShiftRegister", 2743 TP[Var("d",F4),Var("n",F4),Var("shift_t",CTy"SRType"),Var("m",F4)], 2744 Close 2745 (qVar"state", 2746 Let(TP[Var("v",PTy(F32,bTy)),qVar"s"], 2747 Apply 2748 (Call 2749 ("Shift_C",ATy(qTy,PTy(PTy(F32,bTy),qTy)), 2750 TP[Apply(Call("R",ATy(qTy,F32),Var("n",F4)),qVar"state"), 2751 Var("shift_t",CTy"SRType"), 2752 Mop(Cast nTy, 2753 EX(Apply 2754 (Call("R",ATy(qTy,F32),Var("m",F4)), 2755 qVar"state"),LN 7,LN 0,F8)), 2756 Dest("C",bTy,Dest("PSR",CTy"PSR",qVar"state"))]), 2757 qVar"state"), 2758 Let(TP[Var("shifted",F32),bVar"carry"],Var("v",PTy(F32,bTy)), 2759 Apply 2760 (Call 2761 ("DataProcessing",ATy(qTy,qTy), 2762 TP[LW(13,4),LT,Var("d",F4),LX F4,Var("shifted",F32), 2763 bVar"carry"]),qVar"s"))))) 2764; 2765val dfn'Multiply32_def = Def 2766 ("dfn'Multiply32",TP[Var("d",F4),Var("n",F4),Var("m",F4)], 2767 Close 2768 (qVar"state", 2769 Let(Var("v",F32), 2770 Bop(Mul,Apply(Call("R",ATy(qTy,F32),Var("n",F4)),qVar"state"), 2771 Apply(Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state")), 2772 Let(qVar"s", 2773 Apply 2774 (Call("write'R",ATy(qTy,qTy),TP[Var("v",F32),Var("d",F4)]), 2775 qVar"state"), 2776 Let(qVar"s", 2777 Rupd 2778 ("PSR", 2779 TP[qVar"s", 2780 Rupd 2781 ("N", 2782 TP[Dest("PSR",CTy"PSR",qVar"s"), 2783 Bop(Bit,Var("v",F32),LN 31)])]), 2784 Let(qVar"s", 2785 Apply 2786 (Call("IncPC",ATy(qTy,qTy),LU), 2787 Rupd 2788 ("PSR", 2789 TP[qVar"s", 2790 Rupd 2791 ("Z", 2792 TP[Dest("PSR",CTy"PSR",qVar"s"), 2793 EQ(Var("v",F32),LW(0,32))])])), 2794 Rupd 2795 ("count", 2796 TP[qVar"s", 2797 Bop(Add,Dest("count",nTy,qVar"s"),LN 1)]))))))) 2798; 2799val dfn'ExtendByte_def = Def 2800 ("dfn'ExtendByte",TP[bVar"unsigned",Var("d",F4),Var("m",F4)], 2801 Close 2802 (qVar"state", 2803 Let(qVar"s", 2804 Apply 2805 (Call("IncPC",ATy(qTy,qTy),LU), 2806 Apply 2807 (Call 2808 ("write'R",ATy(qTy,qTy), 2809 TP[Call 2810 ("Extend",F32, 2811 TP[bVar"unsigned", 2812 EX(Apply 2813 (Call("R",ATy(qTy,F32),Var("m",F4)), 2814 qVar"state"),LN 7,LN 0,F8)]),Var("d",F4)]), 2815 qVar"state")), 2816 Rupd 2817 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 1)])))) 2818; 2819val dfn'ExtendHalfword_def = Def 2820 ("dfn'ExtendHalfword",TP[bVar"unsigned",Var("d",F4),Var("m",F4)], 2821 Close 2822 (qVar"state", 2823 Let(qVar"s", 2824 Apply 2825 (Call("IncPC",ATy(qTy,qTy),LU), 2826 Apply 2827 (Call 2828 ("write'R",ATy(qTy,qTy), 2829 TP[Call 2830 ("Extend",F32, 2831 TP[bVar"unsigned", 2832 EX(Apply 2833 (Call("R",ATy(qTy,F32),Var("m",F4)), 2834 qVar"state"),LN 15,LN 0,F16)]), 2835 Var("d",F4)]),qVar"state")), 2836 Rupd 2837 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 1)])))) 2838; 2839val dfn'ByteReverse_def = Def 2840 ("dfn'ByteReverse",TP[Var("d",F4),Var("m",F4)], 2841 Close 2842 (qVar"state", 2843 Let(Var("v",F32), 2844 Apply(Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"), 2845 Let(qVar"s", 2846 Apply 2847 (Call("IncPC",ATy(qTy,qTy),LU), 2848 Apply 2849 (Call 2850 ("write'R",ATy(qTy,qTy), 2851 TP[CC[EX(Var("v",F32),LN 7,LN 0,F8), 2852 EX(Var("v",F32),LN 15,LN 8,F8), 2853 EX(Var("v",F32),LN 23,LN 16,F8), 2854 EX(Var("v",F32),LN 31,LN 24,F8)],Var("d",F4)]), 2855 qVar"state")), 2856 Rupd 2857 ("count", 2858 TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 1)]))))) 2859; 2860val dfn'ByteReversePackedHalfword_def = Def 2861 ("dfn'ByteReversePackedHalfword",TP[Var("d",F4),Var("m",F4)], 2862 Close 2863 (qVar"state", 2864 Let(Var("v",F32), 2865 Apply(Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"), 2866 Let(qVar"s", 2867 Apply 2868 (Call("IncPC",ATy(qTy,qTy),LU), 2869 Apply 2870 (Call 2871 ("write'R",ATy(qTy,qTy), 2872 TP[CC[EX(Var("v",F32),LN 23,LN 16,F8), 2873 EX(Var("v",F32),LN 31,LN 24,F8), 2874 EX(Var("v",F32),LN 7,LN 0,F8), 2875 EX(Var("v",F32),LN 15,LN 8,F8)],Var("d",F4)]), 2876 qVar"state")), 2877 Rupd 2878 ("count", 2879 TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 1)]))))) 2880; 2881val dfn'ByteReverseSignedHalfword_def = Def 2882 ("dfn'ByteReverseSignedHalfword",TP[Var("d",F4),Var("m",F4)], 2883 Close 2884 (qVar"state", 2885 Let(Var("v",F32), 2886 Apply(Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"), 2887 Let(qVar"s", 2888 Apply 2889 (Call("IncPC",ATy(qTy,qTy),LU), 2890 Apply 2891 (Call 2892 ("write'R",ATy(qTy,qTy), 2893 TP[CC[Mop(SE(FTy 24),EX(Var("v",F32),LN 7,LN 0,F8)), 2894 EX(Var("v",F32),LN 15,LN 8,F8)],Var("d",F4)]), 2895 qVar"state")), 2896 Rupd 2897 ("count", 2898 TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 1)]))))) 2899; 2900val dfn'LoadWord_def = Def 2901 ("dfn'LoadWord",TP[Var("t",F4),Var("n",F4),Var("m",CTy"offset")], 2902 Close 2903 (qVar"state", 2904 Let(TP[Var("v",F32),qVar"s"], 2905 CS(Var("m",CTy"offset"), 2906 [(Call("register_form",CTy"offset",Var("m",F4)), 2907 Apply 2908 (Call 2909 ("Shift",ATy(qTy,PTy(F32,qTy)), 2910 TP[Apply 2911 (Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"), 2912 LC("SRType_LSL",CTy"SRType"),LN 0, 2913 Dest("C",bTy,Dest("PSR",CTy"PSR",qVar"state"))]), 2914 qVar"state")), 2915 (Call("immediate_form",CTy"offset",Var("imm32",F32)), 2916 TP[Var("imm32",F32),qVar"state"])]), 2917 Let(TP[Var("v",F32),qVar"s"], 2918 Apply 2919 (Call 2920 ("MemU",ATy(qTy,PTy(F32,qTy)), 2921 TP[Bop(Add, 2922 Apply 2923 (Call("R",ATy(qTy,F32),Var("n",F4)),qVar"s"), 2924 Var("v",F32)),LN 4]),qVar"s"), 2925 Let(qVar"s", 2926 Apply 2927 (Call("IncPC",ATy(qTy,qTy),LU), 2928 Apply 2929 (Call 2930 ("write'R",ATy(qTy,qTy), 2931 TP[Var("v",F32),Var("t",F4)]),qVar"s")), 2932 Rupd 2933 ("count", 2934 TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 2)])))))) 2935; 2936val dfn'LoadLiteral_def = Def 2937 ("dfn'LoadLiteral",TP[Var("t",F4),Var("imm32",F32)], 2938 Close 2939 (qVar"state", 2940 Let(TP[Var("v",F32),qVar"s"], 2941 Apply 2942 (Call 2943 ("MemU",ATy(qTy,PTy(F32,qTy)), 2944 TP[Bop(Add, 2945 Call 2946 ("Align",F32, 2947 TP[Apply(Const("PC",ATy(qTy,F32)),qVar"state"), 2948 LN 4]),Var("imm32",F32)),LN 4]),qVar"state"), 2949 Let(qVar"s", 2950 Apply 2951 (Call("IncPC",ATy(qTy,qTy),LU), 2952 Apply 2953 (Call 2954 ("write'R",ATy(qTy,qTy),TP[Var("v",F32),Var("t",F4)]), 2955 qVar"s")), 2956 Rupd 2957 ("count", 2958 TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 2)]))))) 2959; 2960val dfn'LoadByte_def = Def 2961 ("dfn'LoadByte", 2962 TP[bVar"unsigned",Var("t",F4),Var("n",F4),Var("m",CTy"offset")], 2963 Close 2964 (qVar"state", 2965 Let(TP[Var("v",F32),qVar"s"], 2966 CS(Var("m",CTy"offset"), 2967 [(Call("register_form",CTy"offset",Var("m",F4)), 2968 Apply 2969 (Call 2970 ("Shift",ATy(qTy,PTy(F32,qTy)), 2971 TP[Apply 2972 (Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"), 2973 LC("SRType_LSL",CTy"SRType"),LN 0, 2974 Dest("C",bTy,Dest("PSR",CTy"PSR",qVar"state"))]), 2975 qVar"state")), 2976 (Call("immediate_form",CTy"offset",Var("imm32",F32)), 2977 TP[Var("imm32",F32),qVar"state"])]), 2978 Let(TP[Var("v",F8),qVar"s"], 2979 Apply 2980 (Call 2981 ("MemU",ATy(qTy,PTy(F8,qTy)), 2982 TP[Bop(Add, 2983 Apply 2984 (Call("R",ATy(qTy,F32),Var("n",F4)),qVar"s"), 2985 Var("v",F32)),LN 1]),qVar"s"), 2986 Let(qVar"s", 2987 Apply 2988 (Call("IncPC",ATy(qTy,qTy),LU), 2989 Apply 2990 (Call 2991 ("write'R",ATy(qTy,qTy), 2992 TP[Call 2993 ("Extend",F32, 2994 TP[bVar"unsigned",Var("v",F8)]), 2995 Var("t",F4)]),qVar"s")), 2996 Rupd 2997 ("count", 2998 TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 2)])))))) 2999; 3000val dfn'LoadHalf_def = Def 3001 ("dfn'LoadHalf", 3002 TP[bVar"unsigned",Var("t",F4),Var("n",F4),Var("m",CTy"offset")], 3003 Close 3004 (qVar"state", 3005 Let(TP[Var("v",F32),qVar"s"], 3006 CS(Var("m",CTy"offset"), 3007 [(Call("register_form",CTy"offset",Var("m",F4)), 3008 Apply 3009 (Call 3010 ("Shift",ATy(qTy,PTy(F32,qTy)), 3011 TP[Apply 3012 (Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"), 3013 LC("SRType_LSL",CTy"SRType"),LN 0, 3014 Dest("C",bTy,Dest("PSR",CTy"PSR",qVar"state"))]), 3015 qVar"state")), 3016 (Call("immediate_form",CTy"offset",Var("imm32",F32)), 3017 TP[Var("imm32",F32),qVar"state"])]), 3018 Let(TP[Var("v",F16),qVar"s"], 3019 Apply 3020 (Call 3021 ("MemU",ATy(qTy,PTy(F16,qTy)), 3022 TP[Bop(Add, 3023 Apply 3024 (Call("R",ATy(qTy,F32),Var("n",F4)),qVar"s"), 3025 Var("v",F32)),LN 2]),qVar"s"), 3026 Let(qVar"s", 3027 Apply 3028 (Call("IncPC",ATy(qTy,qTy),LU), 3029 Apply 3030 (Call 3031 ("write'R",ATy(qTy,qTy), 3032 TP[Call 3033 ("Extend",F32, 3034 TP[bVar"unsigned",Var("v",F16)]), 3035 Var("t",F4)]),qVar"s")), 3036 Rupd 3037 ("count", 3038 TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 2)])))))) 3039; 3040val dfn'LoadMultiple_def = Def 3041 ("dfn'LoadMultiple",TP[bVar"wback",Var("n",F4),Var("registers",FTy 9)], 3042 Close 3043 (qVar"state", 3044 Let(Var("v",F32), 3045 Apply(Call("R",ATy(qTy,F32),Var("n",F4)),qVar"state"), 3046 Let(nVar"bitcount",Call("BitCount",nTy,Var("registers",FTy 9)), 3047 Let(Var("s",PTy(F32,qTy)), 3048 Mop(Snd, 3049 Apply 3050 (For(TP[LN 0,LN 7, 3051 Close 3052 (nVar"i", 3053 Close 3054 (Var("state",PTy(F32,qTy)), 3055 ITE(Bop(Bit,Var("registers",FTy 9), 3056 nVar"i"), 3057 Let(Var("s",PTy(F32,qTy)), 3058 Let(TP[Var("v",PTy(F32,F4)), 3059 Var("s",PTy(F32,qTy))], 3060 Let(TP[Var("v",F32), 3061 Var("s", 3062 PTy(F32,qTy))], 3063 CS(Apply 3064 (Call 3065 ("MemA", 3066 ATy(qTy, 3067 PTy(F32, 3068 qTy)), 3069 TP[Mop(Fst, 3070 Var("state", 3071 PTy(F32, 3072 qTy))), 3073 LN 4]), 3074 Mop(Snd, 3075 Var("state", 3076 PTy(F32, 3077 qTy)))), 3078 [(TP[Var("v",F32), 3079 qVar"s3"], 3080 TP[Var("v",F32), 3081 Mop(Fst, 3082 Var("state", 3083 PTy(F32, 3084 qTy))), 3085 qVar"s3"])]), 3086 TP[TP[Var("v",F32), 3087 Mop(Cast F4, 3088 nVar"i")], 3089 Var("s", 3090 PTy(F32,qTy))]), 3091 TP[Mop(Fst, 3092 Var("s", 3093 PTy(F32,qTy))), 3094 Apply 3095 (Call 3096 ("write'R", 3097 ATy(qTy,qTy), 3098 Var("v", 3099 PTy(F32,F4))), 3100 Mop(Snd, 3101 Var("s", 3102 PTy(F32, 3103 qTy))))]), 3104 TP[LU, 3105 Bop(Add, 3106 Mop(Fst, 3107 Var("s", 3108 PTy(F32,qTy))), 3109 LW(4,32)), 3110 Mop(Snd, 3111 Var("s",PTy(F32,qTy)))]), 3112 TP[LU,Var("state",PTy(F32,qTy))])))]), 3113 TP[Var("v",F32),qVar"state"])), 3114 Let(Var("s",PTy(F32,qTy)), 3115 ITE(Bop(Bit,Var("registers",FTy 9),LN 8), 3116 Let(Var("s",PTy(F32,qTy)), 3117 Let(TP[Var("v",F32),Var("s",PTy(F32,qTy))], 3118 CS(Apply 3119 (Call 3120 ("MemA",ATy(qTy,PTy(F32,qTy)), 3121 TP[Mop(Fst, 3122 Var("s",PTy(F32,qTy))), 3123 LN 4]), 3124 Mop(Snd,Var("s",PTy(F32,qTy)))), 3125 [(TP[Var("v",F32),qVar"s3"], 3126 TP[Var("v",F32), 3127 Mop(Fst,Var("s",PTy(F32,qTy))), 3128 qVar"s3"])]), 3129 TP[Mop(Fst,Var("s",PTy(F32,qTy))), 3130 Apply 3131 (Call 3132 ("LoadWritePC",ATy(qTy,qTy), 3133 Var("v",F32)), 3134 Mop(Snd,Var("s",PTy(F32,qTy))))]), 3135 TP[Mop(Fst,Var("s",PTy(F32,qTy))), 3136 Rupd 3137 ("count", 3138 TP[Mop(Snd,Var("s",PTy(F32,qTy))), 3139 Bop(Add, 3140 Bop(Add, 3141 Dest 3142 ("count",nTy, 3143 Mop(Snd, 3144 Var("s",PTy(F32,qTy)))), 3145 nVar"bitcount"),LN 4)])]), 3146 Let(qVar"s1", 3147 Apply 3148 (Call("IncPC",ATy(qTy,qTy),LU), 3149 Mop(Snd,Var("s",PTy(F32,qTy)))), 3150 TP[Mop(Fst,Var("s",PTy(F32,qTy))), 3151 Rupd 3152 ("count", 3153 TP[qVar"s1", 3154 Bop(Add, 3155 Bop(Add, 3156 Dest("count",nTy,qVar"s1"), 3157 nVar"bitcount"),LN 1)])])), 3158 ITE(Bop(And,bVar"wback", 3159 Mop(Not, 3160 Bop(Bit,Var("registers",FTy 9), 3161 Mop(Cast nTy,Var("n",F4))))), 3162 Apply 3163 (Call 3164 ("write'R",ATy(qTy,qTy), 3165 TP[Bop(Add,Var("v",F32), 3166 Bop(Mul,LW(4,32), 3167 Mop(Cast F32,nVar"bitcount"))), 3168 Var("n",F4)]), 3169 Mop(Snd,Var("s",PTy(F32,qTy)))), 3170 Mop(Snd,Var("s",PTy(F32,qTy)))))))))) 3171; 3172val dfn'StoreWord_def = Def 3173 ("dfn'StoreWord",TP[Var("t",F4),Var("n",F4),Var("m",CTy"offset")], 3174 Close 3175 (qVar"state", 3176 Let(TP[Var("v",F32),qVar"s"], 3177 CS(Var("m",CTy"offset"), 3178 [(Call("register_form",CTy"offset",Var("m",F4)), 3179 Apply 3180 (Call 3181 ("Shift",ATy(qTy,PTy(F32,qTy)), 3182 TP[Apply 3183 (Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"), 3184 LC("SRType_LSL",CTy"SRType"),LN 0, 3185 Dest("C",bTy,Dest("PSR",CTy"PSR",qVar"state"))]), 3186 qVar"state")), 3187 (Call("immediate_form",CTy"offset",Var("imm32",F32)), 3188 TP[Var("imm32",F32),qVar"state"])]), 3189 Let(qVar"s", 3190 Apply 3191 (Call("IncPC",ATy(qTy,qTy),LU), 3192 Apply 3193 (Call 3194 ("write'MemU",ATy(qTy,qTy), 3195 TP[Apply 3196 (Call("R",ATy(qTy,F32),Var("t",F4)),qVar"s"), 3197 Bop(Add, 3198 Apply 3199 (Call("R",ATy(qTy,F32),Var("n",F4)), 3200 qVar"s"),Var("v",F32)),LN 4]),qVar"s")), 3201 Rupd 3202 ("count", 3203 TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 2)]))))) 3204; 3205val dfn'StoreByte_def = Def 3206 ("dfn'StoreByte",TP[Var("t",F4),Var("n",F4),Var("m",CTy"offset")], 3207 Close 3208 (qVar"state", 3209 Let(TP[Var("v",F32),qVar"s"], 3210 CS(Var("m",CTy"offset"), 3211 [(Call("register_form",CTy"offset",Var("m",F4)), 3212 Apply 3213 (Call 3214 ("Shift",ATy(qTy,PTy(F32,qTy)), 3215 TP[Apply 3216 (Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"), 3217 LC("SRType_LSL",CTy"SRType"),LN 0, 3218 Dest("C",bTy,Dest("PSR",CTy"PSR",qVar"state"))]), 3219 qVar"state")), 3220 (Call("immediate_form",CTy"offset",Var("imm32",F32)), 3221 TP[Var("imm32",F32),qVar"state"])]), 3222 Let(qVar"s", 3223 Apply 3224 (Call("IncPC",ATy(qTy,qTy),LU), 3225 Apply 3226 (Call 3227 ("write'MemU",ATy(qTy,qTy), 3228 TP[EX(Apply 3229 (Call("R",ATy(qTy,F32),Var("t",F4)),qVar"s"), 3230 LN 7,LN 0,F8), 3231 Bop(Add, 3232 Apply 3233 (Call("R",ATy(qTy,F32),Var("n",F4)), 3234 qVar"s"),Var("v",F32)),LN 1]),qVar"s")), 3235 Rupd 3236 ("count", 3237 TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 2)]))))) 3238; 3239val dfn'StoreHalf_def = Def 3240 ("dfn'StoreHalf",TP[Var("t",F4),Var("n",F4),Var("m",CTy"offset")], 3241 Close 3242 (qVar"state", 3243 Let(TP[Var("v",F32),qVar"s"], 3244 CS(Var("m",CTy"offset"), 3245 [(Call("register_form",CTy"offset",Var("m",F4)), 3246 Apply 3247 (Call 3248 ("Shift",ATy(qTy,PTy(F32,qTy)), 3249 TP[Apply 3250 (Call("R",ATy(qTy,F32),Var("m",F4)),qVar"state"), 3251 LC("SRType_LSL",CTy"SRType"),LN 0, 3252 Dest("C",bTy,Dest("PSR",CTy"PSR",qVar"state"))]), 3253 qVar"state")), 3254 (Call("immediate_form",CTy"offset",Var("imm32",F32)), 3255 TP[Var("imm32",F32),qVar"state"])]), 3256 Let(qVar"s", 3257 Apply 3258 (Call("IncPC",ATy(qTy,qTy),LU), 3259 Apply 3260 (Call 3261 ("write'MemU",ATy(qTy,qTy), 3262 TP[EX(Apply 3263 (Call("R",ATy(qTy,F32),Var("t",F4)),qVar"s"), 3264 LN 15,LN 0,F16), 3265 Bop(Add, 3266 Apply 3267 (Call("R",ATy(qTy,F32),Var("n",F4)), 3268 qVar"s"),Var("v",F32)),LN 2]),qVar"s")), 3269 Rupd 3270 ("count", 3271 TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 2)]))))) 3272; 3273val dfn'StoreMultiple_def = Def 3274 ("dfn'StoreMultiple",TP[Var("n",F4),Var("registers",F8)], 3275 Close 3276 (qVar"state", 3277 Let(Var("v",F32), 3278 Apply(Call("R",ATy(qTy,F32),Var("n",F4)),qVar"state"), 3279 Let(nVar"bitcount",Call("BitCount",nTy,Var("registers",F8)), 3280 Let(qVar"s1", 3281 Apply 3282 (Call("IncPC",ATy(qTy,qTy),LU), 3283 Apply 3284 (Call 3285 ("write'R",ATy(qTy,qTy), 3286 TP[Bop(Add,Var("v",F32), 3287 Bop(Mul,LW(4,32), 3288 Mop(Cast F32,nVar"bitcount"))), 3289 Var("n",F4)]), 3290 Mop(Snd, 3291 Mop(Snd, 3292 Apply 3293 (For(TP[LN 0,LN 7, 3294 Close 3295 (nVar"i", 3296 Close 3297 (Var("state",PTy(F32,qTy)), 3298 TP[LU, 3299 ITE(Bop(Bit, 3300 Var("registers", 3301 F8),nVar"i"), 3302 TP[Bop(Add, 3303 Mop(Fst, 3304 Var("state", 3305 PTy(F32, 3306 qTy))), 3307 LW(4,32)), 3308 ITE(Bop(And, 3309 EQ(Mop(Cast 3310 F4, 3311 nVar"i"), 3312 Var("n", 3313 F4)), 3314 Mop(Not, 3315 EQ(nVar"i", 3316 Call 3317 ("LowestSetBit", 3318 nTy, 3319 Var("registers", 3320 F8))))), 3321 Apply 3322 (Call 3323 ("write'MemA", 3324 ATy(qTy, 3325 qTy), 3326 TP[LX F32, 3327 Mop(Fst, 3328 Var("state", 3329 PTy(F32, 3330 qTy))), 3331 LN 3332 4]), 3333 Mop(Snd, 3334 Var("state", 3335 PTy(F32, 3336 qTy)))), 3337 Apply 3338 (Call 3339 ("write'MemA", 3340 ATy(qTy, 3341 qTy), 3342 TP[Apply 3343 (Call 3344 ("R", 3345 ATy(qTy, 3346 F32), 3347 Mop(Cast 3348 F4, 3349 nVar"i")), 3350 Mop(Snd, 3351 Var("state", 3352 PTy(F32, 3353 qTy)))), 3354 Mop(Fst, 3355 Var("state", 3356 PTy(F32, 3357 qTy))), 3358 LN 3359 4]), 3360 Mop(Snd, 3361 Var("state", 3362 PTy(F32, 3363 qTy)))))], 3364 Var("state", 3365 PTy(F32,qTy)))]))]), 3366 TP[Var("v",F32),qVar"state"]))))), 3367 Rupd 3368 ("count", 3369 TP[qVar"s1", 3370 Bop(Add, 3371 Bop(Add,Dest("count",nTy,qVar"s1"), 3372 nVar"bitcount"),LN 1)])))))) 3373; 3374val dfn'Push_def = Def 3375 ("dfn'Push",Var("registers",FTy 9), 3376 Close 3377 (qVar"state", 3378 Let(Var("v",F32),Apply(Const("SP",ATy(qTy,F32)),qVar"state"), 3379 Let(nVar"bitcount",Call("BitCount",nTy,Var("registers",FTy 9)), 3380 Let(Var("length",F32), 3381 Bop(Mul,LW(4,32),Mop(Cast F32,nVar"bitcount")), 3382 Let(qVar"s1", 3383 Apply 3384 (Call("IncPC",ATy(qTy,qTy),LU), 3385 Apply 3386 (Call 3387 ("write'SP",ATy(qTy,qTy), 3388 Bop(Sub,Var("v",F32),Var("length",F32))), 3389 Mop(Snd, 3390 Mop(Snd, 3391 Apply 3392 (For(TP[LN 0,LN 8, 3393 Close 3394 (nVar"i", 3395 Close 3396 (Var("state", 3397 PTy(F32,qTy)), 3398 TP[LU, 3399 ITE(Bop(Bit, 3400 Var("registers", 3401 FTy 9), 3402 nVar"i"), 3403 TP[Bop(Add, 3404 Mop(Fst, 3405 Var("state", 3406 PTy(F32, 3407 qTy))), 3408 LW(4,32)), 3409 Apply 3410 (Call 3411 ("write'MemA", 3412 ATy(qTy, 3413 qTy), 3414 TP[ITE(EQ(nVar"i", 3415 LN 3416 8), 3417 Apply 3418 (Const 3419 ("LR", 3420 ATy(qTy, 3421 F32)), 3422 Mop(Snd, 3423 Var("state", 3424 PTy(F32, 3425 qTy)))), 3426 Apply 3427 (Call 3428 ("R", 3429 ATy(qTy, 3430 F32), 3431 Mop(Cast 3432 F4, 3433 nVar"i")), 3434 Mop(Snd, 3435 Var("state", 3436 PTy(F32, 3437 qTy))))), 3438 Mop(Fst, 3439 Var("state", 3440 PTy(F32, 3441 qTy))), 3442 LN 3443 4]), 3444 Mop(Snd, 3445 Var("state", 3446 PTy(F32, 3447 qTy))))], 3448 Var("state", 3449 PTy(F32,qTy)))]))]), 3450 TP[Bop(Sub,Var("v",F32), 3451 Var("length",F32)), 3452 qVar"state"]))))), 3453 Rupd 3454 ("count", 3455 TP[qVar"s1", 3456 Bop(Add, 3457 Bop(Add,Dest("count",nTy,qVar"s1"), 3458 nVar"bitcount"),LN 1)]))))))) 3459; 3460val dfn'SupervisorCall_def = Def 3461 ("dfn'SupervisorCall",Var("imm32",F32), 3462 Close 3463 (qVar"state", 3464 Let(qVar"s", 3465 Apply(Call("CallSupervisor",ATy(qTy,qTy),LU),qVar"state"), 3466 Rupd 3467 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LX nTy)])))) 3468; 3469val dfn'ChangeProcessorState_def = Def 3470 ("dfn'ChangeProcessorState",bVar"im", 3471 Close 3472 (qVar"state", 3473 Let(qVar"s", 3474 Apply 3475 (Call("IncPC",ATy(qTy,qTy),LU), 3476 ITE(Apply 3477 (Call("CurrentModeIsPrivileged",ATy(qTy,bTy),LU), 3478 qVar"state"), 3479 Rupd 3480 ("PRIMASK", 3481 TP[qVar"state", 3482 Rupd 3483 ("PM", 3484 TP[Dest("PRIMASK",CTy"PRIMASK",qVar"state"), 3485 bVar"im"])]),qVar"state")), 3486 Rupd 3487 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 1)])))) 3488; 3489val dfn'MoveToRegisterFromSpecial_def = Def 3490 ("dfn'MoveToRegisterFromSpecial",TP[Var("SYSm",F8),Var("d",F4)], 3491 Close 3492 (qVar"state", 3493 Let(qVar"s", 3494 Apply 3495 (Call("write'R",ATy(qTy,qTy),TP[LW(0,32),Var("d",F4)]), 3496 qVar"state"), 3497 Let(qVar"s", 3498 Apply 3499 (Call("IncPC",ATy(qTy,qTy),LU), 3500 CS(EX(Var("SYSm",F8),LN 7,LN 3,FTy 5), 3501 [(LW(0,5), 3502 Let(qVar"s", 3503 ITE(Bop(Bit,Var("SYSm",F8),LN 0), 3504 Apply 3505 (Call 3506 ("write'R",ATy(qTy,qTy), 3507 TP[BFI(LN 8,LN 0, 3508 EX(Call 3509 ("reg'PSR",F32, 3510 Dest 3511 ("PSR",CTy"PSR",qVar"s")), 3512 LN 8,LN 0,FTy 9), 3513 Apply 3514 (Call 3515 ("R",ATy(qTy,F32), 3516 Var("d",F4)),qVar"s")), 3517 Var("d",F4)]),qVar"s"),qVar"s"), 3518 Let(qVar"s", 3519 ITE(Bop(Bit,Var("SYSm",F8),LN 1), 3520 Apply 3521 (Call 3522 ("write'R",ATy(qTy,qTy), 3523 TP[BFI(LN 24,LN 24, 3524 Mop(Cast F1,LF), 3525 Apply 3526 (Call 3527 ("R",ATy(qTy,F32), 3528 Var("d",F4)),qVar"s")), 3529 Var("d",F4)]),qVar"s"),qVar"s"), 3530 ITE(Mop(Not,Bop(Bit,Var("SYSm",F8),LN 2)), 3531 Apply 3532 (Call 3533 ("write'R",ATy(qTy,qTy), 3534 TP[BFI(LN 31,LN 27, 3535 EX(Call 3536 ("reg'PSR",F32, 3537 Dest 3538 ("PSR",CTy"PSR", 3539 qVar"s")),LN 31, 3540 LN 27,FTy 5), 3541 Apply 3542 (Call 3543 ("R",ATy(qTy,F32), 3544 Var("d",F4)),qVar"s")), 3545 Var("d",F4)]),qVar"s"),qVar"s")))), 3546 (LW(1,5), 3547 CS(EX(Var("SYSm",F8),LN 2,LN 0,FTy 3), 3548 [(LW(0,3), 3549 Apply 3550 (Call 3551 ("write'R",ATy(qTy,qTy), 3552 TP[Apply 3553 (Const("SP_main",ATy(qTy,F32)), 3554 qVar"s"),Var("d",F4)]),qVar"s")), 3555 (LW(1,3), 3556 Apply 3557 (Call 3558 ("write'R",ATy(qTy,qTy), 3559 TP[Apply 3560 (Const("SP_process",ATy(qTy,F32)), 3561 qVar"s"),Var("d",F4)]),qVar"s")), 3562 (AVar(FTy 3),qVar"s")])), 3563 (LW(2,5), 3564 CS(EX(Var("SYSm",F8),LN 2,LN 0,FTy 3), 3565 [(LW(0,3), 3566 Apply 3567 (Call 3568 ("write'R",ATy(qTy,qTy), 3569 TP[BFI(LN 0,LN 0, 3570 Mop(Cast F1, 3571 Dest 3572 ("PM",bTy, 3573 Dest 3574 ("PRIMASK",CTy"PRIMASK", 3575 qVar"s"))), 3576 Apply 3577 (Call 3578 ("R",ATy(qTy,F32),Var("d",F4)), 3579 qVar"s")),Var("d",F4)]),qVar"s")), 3580 (LW(4,3), 3581 Apply 3582 (Call 3583 ("write'R",ATy(qTy,qTy), 3584 TP[BFI(LN 1,LN 0, 3585 EX(Call 3586 ("reg'CONTROL",FTy 3, 3587 Dest 3588 ("CONTROL",CTy"CONTROL", 3589 qVar"s")),LN 1,LN 0,FTy 2), 3590 Apply 3591 (Call 3592 ("R",ATy(qTy,F32),Var("d",F4)), 3593 qVar"s")),Var("d",F4)]),qVar"s")), 3594 (AVar(FTy 3),qVar"s")])),(AVar(FTy 5),qVar"s")])), 3595 Rupd 3596 ("count", 3597 TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 4)]))))) 3598; 3599val dfn'MoveToSpecialRegister_def = Def 3600 ("dfn'MoveToSpecialRegister",TP[Var("SYSm",F8),Var("n",F4)], 3601 Close 3602 (qVar"state", 3603 Let(Var("v",F32), 3604 Apply(Call("R",ATy(qTy,F32),Var("n",F4)),qVar"state"), 3605 Let(qVar"s", 3606 Apply 3607 (Call("IncPC",ATy(qTy,qTy),LU), 3608 CS(EX(Var("SYSm",F8),LN 7,LN 3,FTy 5), 3609 [(LW(0,5), 3610 ITE(Mop(Not,Bop(Bit,Var("SYSm",F8),LN 2)), 3611 Rupd 3612 ("PSR", 3613 TP[qVar"state", 3614 Call 3615 ("write'reg'PSR",CTy"PSR", 3616 TP[Dest("PSR",CTy"PSR",qVar"state"), 3617 BFI(LN 31,LN 27, 3618 EX(Var("v",F32),LN 31,LN 27, 3619 FTy 5), 3620 Call 3621 ("reg'PSR",F32, 3622 Dest 3623 ("PSR",CTy"PSR",qVar"state")))])]), 3624 qVar"state")), 3625 (LW(1,5), 3626 ITE(Apply 3627 (Call 3628 ("CurrentModeIsPrivileged",ATy(qTy,bTy),LU), 3629 qVar"state"), 3630 CS(EX(Var("SYSm",F8),LN 2,LN 0,FTy 3), 3631 [(LW(0,3), 3632 Apply 3633 (Call 3634 ("write'SP_main",ATy(qTy,qTy), 3635 CC[EX(Var("v",F32),LN 31,LN 2,FTy 30), 3636 LW(0,2)]),qVar"state")), 3637 (LW(1,3), 3638 Apply 3639 (Call 3640 ("write'SP_process",ATy(qTy,qTy), 3641 CC[EX(Var("v",F32),LN 31,LN 2,FTy 30), 3642 LW(0,2)]),qVar"state")), 3643 (AVar(FTy 3),qVar"state")]),qVar"state")), 3644 (LW(2,5), 3645 ITE(Apply 3646 (Call 3647 ("CurrentModeIsPrivileged",ATy(qTy,bTy),LU), 3648 qVar"state"), 3649 CS(EX(Var("SYSm",F8),LN 2,LN 0,FTy 3), 3650 [(LW(0,3), 3651 Rupd 3652 ("PRIMASK", 3653 TP[qVar"state", 3654 Rupd 3655 ("PM", 3656 TP[Dest 3657 ("PRIMASK",CTy"PRIMASK", 3658 qVar"state"), 3659 Bop(Bit,Var("v",F32),LN 0)])])), 3660 (LW(4,3), 3661 ITE(EQ(Dest 3662 ("CurrentMode",CTy"Mode", 3663 qVar"state"), 3664 LC("Mode_Thread",CTy"Mode")), 3665 Let(qVar"s", 3666 Rupd 3667 ("CONTROL", 3668 TP[qVar"state", 3669 Rupd 3670 ("SPSEL", 3671 TP[Dest 3672 ("CONTROL", 3673 CTy"CONTROL", 3674 qVar"state"), 3675 Bop(Bit,Var("v",F32), 3676 LN 1)])]), 3677 Rupd 3678 ("CONTROL", 3679 TP[qVar"s", 3680 Rupd 3681 ("nPRIV", 3682 TP[Dest 3683 ("CONTROL", 3684 CTy"CONTROL",qVar"s"), 3685 Bop(Bit,Var("v",F32), 3686 LN 0)])])), 3687 qVar"state")),(AVar(FTy 3),qVar"state")]), 3688 qVar"state")),(AVar(FTy 5),qVar"state")])), 3689 Rupd 3690 ("count", 3691 TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 4)]))))) 3692; 3693val dfn'Undefined_def = Def 3694 ("dfn'Undefined",Var("imm32",F32), 3695 Close 3696 (qVar"state", 3697 Apply 3698 (Call("Raise",ATy(qTy,qTy),Const("HardFault",CTy"ARM_Exception")), 3699 qVar"state"))) 3700; 3701val dfn'NoOperation_def = Def 3702 ("dfn'NoOperation",AVar uTy, 3703 Close 3704 (qVar"state", 3705 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"), 3706 Rupd 3707 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 1)])))) 3708; 3709val dfn'Breakpoint_def = Def 3710 ("dfn'Breakpoint",Var("imm32",F32), 3711 Close 3712 (qVar"state", 3713 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"), 3714 Rupd 3715 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LX nTy)])))) 3716; 3717val dfn'DataMemoryBarrier_def = Def 3718 ("dfn'DataMemoryBarrier",Var("option",F4), 3719 Close 3720 (qVar"state", 3721 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"), 3722 Rupd 3723 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 4)])))) 3724; 3725val dfn'DataSynchronizationBarrier_def = Def 3726 ("dfn'DataSynchronizationBarrier",Var("option",F4), 3727 Close 3728 (qVar"state", 3729 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"), 3730 Rupd 3731 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 4)])))) 3732; 3733val dfn'InstructionSynchronizationBarrier_def = Def 3734 ("dfn'InstructionSynchronizationBarrier",Var("option",F4), 3735 Close 3736 (qVar"state", 3737 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"), 3738 Rupd 3739 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 4)])))) 3740; 3741val dfn'SendEvent_def = Def 3742 ("dfn'SendEvent",AVar uTy, 3743 Close 3744 (qVar"state", 3745 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"), 3746 Rupd 3747 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 1)])))) 3748; 3749val dfn'WaitForEvent_def = Def 3750 ("dfn'WaitForEvent",AVar uTy, 3751 Close 3752 (qVar"state", 3753 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"), 3754 Rupd 3755 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 2)])))) 3756; 3757val dfn'WaitForInterrupt_def = Def 3758 ("dfn'WaitForInterrupt",AVar uTy, 3759 Close 3760 (qVar"state", 3761 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"), 3762 Rupd 3763 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 2)])))) 3764; 3765val dfn'Yield_def = Def 3766 ("dfn'Yield",AVar uTy, 3767 Close 3768 (qVar"state", 3769 Let(qVar"s",Apply(Call("IncPC",ATy(qTy,qTy),LU),qVar"state"), 3770 Rupd 3771 ("count",TP[qVar"s",Bop(Add,Dest("count",nTy,qVar"s"),LN 1)])))) 3772; 3773val Run_def = Def 3774 ("Run",Var("v0",CTy"instruction"), 3775 Close 3776 (qVar"state", 3777 CS(Var("v0",CTy"instruction"), 3778 [(Call("NoOperation",CTy"instruction",uVar"v48"), 3779 Apply 3780 (Call("dfn'NoOperation",ATy(qTy,qTy),uVar"v48"),qVar"state")), 3781 (Call("Undefined",CTy"instruction",Var("v49",F32)), 3782 Apply 3783 (Call("dfn'Undefined",ATy(qTy,qTy),Var("v49",F32)), 3784 qVar"state")), 3785 (Call("Branch",CTy"instruction",Var("v1",CTy"Branch")), 3786 CS(Var("v1",CTy"Branch"), 3787 [(Call("BranchExchange",CTy"Branch",Var("v2",F4)), 3788 Apply 3789 (Call("dfn'BranchExchange",ATy(qTy,qTy),Var("v2",F4)), 3790 qVar"state")), 3791 (Call 3792 ("BranchLinkExchangeRegister",CTy"Branch",Var("v3",F4)), 3793 Apply 3794 (Call 3795 ("dfn'BranchLinkExchangeRegister",ATy(qTy,qTy), 3796 Var("v3",F4)),qVar"state")), 3797 (Call("BranchLinkImmediate",CTy"Branch",Var("v4",F32)), 3798 Apply 3799 (Call 3800 ("dfn'BranchLinkImmediate",ATy(qTy,qTy),Var("v4",F32)), 3801 qVar"state")), 3802 (Call("BranchTarget",CTy"Branch",Var("v5",F32)), 3803 Apply 3804 (Call("dfn'BranchTarget",ATy(qTy,qTy),Var("v5",F32)), 3805 qVar"state"))])), 3806 (Call("Data",CTy"instruction",Var("v6",CTy"Data")), 3807 CS(Var("v6",CTy"Data"), 3808 [(Call 3809 ("ArithLogicImmediate",CTy"Data", 3810 Var("v7",PTy(F4,PTy(bTy,PTy(F4,PTy(F4,F32)))))), 3811 Apply 3812 (Call 3813 ("dfn'ArithLogicImmediate",ATy(qTy,qTy), 3814 Var("v7",PTy(F4,PTy(bTy,PTy(F4,PTy(F4,F32)))))), 3815 qVar"state")), 3816 (Call("CompareImmediate",CTy"Data",Var("v8",PTy(F4,F32))), 3817 Apply 3818 (Call 3819 ("dfn'CompareImmediate",ATy(qTy,qTy), 3820 Var("v8",PTy(F4,F32))),qVar"state")), 3821 (Call("Move",CTy"Data",Var("v9",PTy(F4,F32))), 3822 Apply 3823 (Call("dfn'Move",ATy(qTy,qTy),Var("v9",PTy(F4,F32))), 3824 qVar"state")), 3825 (Call 3826 ("Register",CTy"Data", 3827 Var("v10",PTy(F4,PTy(bTy,PTy(F4,PTy(F4,F4)))))), 3828 Apply 3829 (Call 3830 ("dfn'Register",ATy(qTy,qTy), 3831 Var("v10",PTy(F4,PTy(bTy,PTy(F4,PTy(F4,F4)))))), 3832 qVar"state")), 3833 (Call 3834 ("ShiftImmediate",CTy"Data", 3835 Var("v11", 3836 PTy(bTy, 3837 PTy(bTy,PTy(F4,PTy(F4,PTy(CTy"SRType",nTy))))))), 3838 Apply 3839 (Call 3840 ("dfn'ShiftImmediate",ATy(qTy,qTy), 3841 Var("v11", 3842 PTy(bTy, 3843 PTy(bTy,PTy(F4,PTy(F4,PTy(CTy"SRType",nTy))))))), 3844 qVar"state")), 3845 (Call 3846 ("ShiftRegister",CTy"Data", 3847 Var("v12",PTy(F4,PTy(F4,PTy(CTy"SRType",F4))))), 3848 Apply 3849 (Call 3850 ("dfn'ShiftRegister",ATy(qTy,qTy), 3851 Var("v12",PTy(F4,PTy(F4,PTy(CTy"SRType",F4))))), 3852 qVar"state")), 3853 (Call 3854 ("TestCompareRegister",CTy"Data", 3855 Var("v13",PTy(FTy 2,PTy(F4,F4)))), 3856 Apply 3857 (Call 3858 ("dfn'TestCompareRegister",ATy(qTy,qTy), 3859 Var("v13",PTy(FTy 2,PTy(F4,F4)))),qVar"state"))])), 3860 (Call("Hint",CTy"instruction",Var("v14",CTy"Hint")), 3861 CS(Var("v14",CTy"Hint"), 3862 [(Call("Breakpoint",CTy"Hint",Var("v15",F32)), 3863 Apply 3864 (Call("dfn'Breakpoint",ATy(qTy,qTy),Var("v15",F32)), 3865 qVar"state")), 3866 (Call("DataMemoryBarrier",CTy"Hint",Var("v16",F4)), 3867 Apply 3868 (Call 3869 ("dfn'DataMemoryBarrier",ATy(qTy,qTy),Var("v16",F4)), 3870 qVar"state")), 3871 (Call("DataSynchronizationBarrier",CTy"Hint",Var("v17",F4)), 3872 Apply 3873 (Call 3874 ("dfn'DataSynchronizationBarrier",ATy(qTy,qTy), 3875 Var("v17",F4)),qVar"state")), 3876 (Call 3877 ("InstructionSynchronizationBarrier",CTy"Hint", 3878 Var("v18",F4)), 3879 Apply 3880 (Call 3881 ("dfn'InstructionSynchronizationBarrier", 3882 ATy(qTy,qTy),Var("v18",F4)),qVar"state")), 3883 (Call("SendEvent",CTy"Hint",uVar"v19"), 3884 Apply 3885 (Call("dfn'SendEvent",ATy(qTy,qTy),uVar"v19"), 3886 qVar"state")), 3887 (Call("WaitForEvent",CTy"Hint",uVar"v20"), 3888 Apply 3889 (Call("dfn'WaitForEvent",ATy(qTy,qTy),uVar"v20"), 3890 qVar"state")), 3891 (Call("WaitForInterrupt",CTy"Hint",uVar"v21"), 3892 Apply 3893 (Call("dfn'WaitForInterrupt",ATy(qTy,qTy),uVar"v21"), 3894 qVar"state")), 3895 (Call("Yield",CTy"Hint",uVar"v22"), 3896 Apply 3897 (Call("dfn'Yield",ATy(qTy,qTy),uVar"v22"),qVar"state"))])), 3898 (Call("Load",CTy"instruction",Var("v23",CTy"Load")), 3899 CS(Var("v23",CTy"Load"), 3900 [(Call 3901 ("LoadByte",CTy"Load", 3902 Var("v24",PTy(bTy,PTy(F4,PTy(F4,CTy"offset"))))), 3903 Apply 3904 (Call 3905 ("dfn'LoadByte",ATy(qTy,qTy), 3906 Var("v24",PTy(bTy,PTy(F4,PTy(F4,CTy"offset"))))), 3907 qVar"state")), 3908 (Call 3909 ("LoadHalf",CTy"Load", 3910 Var("v25",PTy(bTy,PTy(F4,PTy(F4,CTy"offset"))))), 3911 Apply 3912 (Call 3913 ("dfn'LoadHalf",ATy(qTy,qTy), 3914 Var("v25",PTy(bTy,PTy(F4,PTy(F4,CTy"offset"))))), 3915 qVar"state")), 3916 (Call("LoadLiteral",CTy"Load",Var("v26",PTy(F4,F32))), 3917 Apply 3918 (Call 3919 ("dfn'LoadLiteral",ATy(qTy,qTy), 3920 Var("v26",PTy(F4,F32))),qVar"state")), 3921 (Call 3922 ("LoadMultiple",CTy"Load", 3923 Var("v27",PTy(bTy,PTy(F4,FTy 9)))), 3924 Apply 3925 (Call 3926 ("dfn'LoadMultiple",ATy(qTy,qTy), 3927 Var("v27",PTy(bTy,PTy(F4,FTy 9)))),qVar"state")), 3928 (Call 3929 ("LoadWord",CTy"Load", 3930 Var("v28",PTy(F4,PTy(F4,CTy"offset")))), 3931 Apply 3932 (Call 3933 ("dfn'LoadWord",ATy(qTy,qTy), 3934 Var("v28",PTy(F4,PTy(F4,CTy"offset")))),qVar"state"))])), 3935 (Call("Media",CTy"instruction",Var("v29",CTy"Media")), 3936 CS(Var("v29",CTy"Media"), 3937 [(Call("ByteReverse",CTy"Media",Var("v30",PTy(F4,F4))), 3938 Apply 3939 (Call 3940 ("dfn'ByteReverse",ATy(qTy,qTy),Var("v30",PTy(F4,F4))), 3941 qVar"state")), 3942 (Call 3943 ("ByteReversePackedHalfword",CTy"Media", 3944 Var("v31",PTy(F4,F4))), 3945 Apply 3946 (Call 3947 ("dfn'ByteReversePackedHalfword",ATy(qTy,qTy), 3948 Var("v31",PTy(F4,F4))),qVar"state")), 3949 (Call 3950 ("ByteReverseSignedHalfword",CTy"Media", 3951 Var("v32",PTy(F4,F4))), 3952 Apply 3953 (Call 3954 ("dfn'ByteReverseSignedHalfword",ATy(qTy,qTy), 3955 Var("v32",PTy(F4,F4))),qVar"state")), 3956 (Call 3957 ("ExtendByte",CTy"Media",Var("v33",PTy(bTy,PTy(F4,F4)))), 3958 Apply 3959 (Call 3960 ("dfn'ExtendByte",ATy(qTy,qTy), 3961 Var("v33",PTy(bTy,PTy(F4,F4)))),qVar"state")), 3962 (Call 3963 ("ExtendHalfword",CTy"Media", 3964 Var("v34",PTy(bTy,PTy(F4,F4)))), 3965 Apply 3966 (Call 3967 ("dfn'ExtendHalfword",ATy(qTy,qTy), 3968 Var("v34",PTy(bTy,PTy(F4,F4)))),qVar"state"))])), 3969 (Call("Multiply",CTy"instruction",Var("v35",CTy"Multiply")), 3970 CS(Var("v35",CTy"Multiply"), 3971 [(Call 3972 ("Multiply32",CTy"Multiply", 3973 Var("v36",PTy(F4,PTy(F4,F4)))), 3974 Apply 3975 (Call 3976 ("dfn'Multiply32",ATy(qTy,qTy), 3977 Var("v36",PTy(F4,PTy(F4,F4)))),qVar"state"))])), 3978 (Call("Store",CTy"instruction",Var("v37",CTy"Store")), 3979 CS(Var("v37",CTy"Store"), 3980 [(Call("Push",CTy"Store",Var("v38",FTy 9)), 3981 Apply 3982 (Call("dfn'Push",ATy(qTy,qTy),Var("v38",FTy 9)), 3983 qVar"state")), 3984 (Call 3985 ("StoreByte",CTy"Store", 3986 Var("v39",PTy(F4,PTy(F4,CTy"offset")))), 3987 Apply 3988 (Call 3989 ("dfn'StoreByte",ATy(qTy,qTy), 3990 Var("v39",PTy(F4,PTy(F4,CTy"offset")))),qVar"state")), 3991 (Call 3992 ("StoreHalf",CTy"Store", 3993 Var("v40",PTy(F4,PTy(F4,CTy"offset")))), 3994 Apply 3995 (Call 3996 ("dfn'StoreHalf",ATy(qTy,qTy), 3997 Var("v40",PTy(F4,PTy(F4,CTy"offset")))),qVar"state")), 3998 (Call("StoreMultiple",CTy"Store",Var("v41",PTy(F4,F8))), 3999 Apply 4000 (Call 4001 ("dfn'StoreMultiple",ATy(qTy,qTy), 4002 Var("v41",PTy(F4,F8))),qVar"state")), 4003 (Call 4004 ("StoreWord",CTy"Store", 4005 Var("v42",PTy(F4,PTy(F4,CTy"offset")))), 4006 Apply 4007 (Call 4008 ("dfn'StoreWord",ATy(qTy,qTy), 4009 Var("v42",PTy(F4,PTy(F4,CTy"offset")))),qVar"state"))])), 4010 (Call("System",CTy"instruction",Var("v43",CTy"System")), 4011 CS(Var("v43",CTy"System"), 4012 [(Call("ChangeProcessorState",CTy"System",bVar"v44"), 4013 Apply 4014 (Call("dfn'ChangeProcessorState",ATy(qTy,qTy),bVar"v44"), 4015 qVar"state")), 4016 (Call 4017 ("MoveToRegisterFromSpecial",CTy"System", 4018 Var("v45",PTy(F8,F4))), 4019 Apply 4020 (Call 4021 ("dfn'MoveToRegisterFromSpecial",ATy(qTy,qTy), 4022 Var("v45",PTy(F8,F4))),qVar"state")), 4023 (Call 4024 ("MoveToSpecialRegister",CTy"System", 4025 Var("v46",PTy(F8,F4))), 4026 Apply 4027 (Call 4028 ("dfn'MoveToSpecialRegister",ATy(qTy,qTy), 4029 Var("v46",PTy(F8,F4))),qVar"state")), 4030 (Call("SupervisorCall",CTy"System",Var("v47",F32)), 4031 Apply 4032 (Call("dfn'SupervisorCall",ATy(qTy,qTy),Var("v47",F32)), 4033 qVar"state"))]))]))) 4034; 4035val Fetch_def = Def 4036 ("Fetch",qVar"state", 4037 Let(Var("v",F32), 4038 Apply 4039 (Dest("REG",ATy(CTy"RName",F32),qVar"state"), 4040 LC("RName_PC",CTy"RName")), 4041 Let(TP[Var("v0",F16),qVar"s"], 4042 Apply 4043 (Call("MemA",ATy(qTy,PTy(F16,qTy)),TP[Var("v",F32),LN 2]), 4044 qVar"state"), 4045 ITE(Bop(And,EQ(EX(Var("v0",F16),LN 15,LN 13,FTy 3),LW(7,3)), 4046 Mop(Not,EQ(EX(Var("v0",F16),LN 12,LN 11,FTy 2),LW(0,2)))), 4047 Let(TP[Var("v1",F16),qVar"s"], 4048 Apply 4049 (Call 4050 ("MemA",ATy(qTy,PTy(F16,qTy)), 4051 TP[Bop(Add,Var("v",F32),LW(2,32)),LN 2]),qVar"s"), 4052 TP[Call 4053 ("Thumb2",CTy"MachineCode", 4054 TP[Var("v0",F16),Var("v1",F16)]),qVar"s"]), 4055 TP[Call("Thumb",CTy"MachineCode",Var("v0",F16)),qVar"s"])))) 4056; 4057val DECODE_UNPREDICTABLE_def = Def 4058 ("DECODE_UNPREDICTABLE",TP[Var("mc",CTy"MachineCode"),sVar"s"], 4059 Close 4060 (qVar"state", 4061 Mop(Snd, 4062 Apply 4063 (Call 4064 ("raise'exception",ATy(qTy,PTy(uTy,qTy)), 4065 Call 4066 ("UNPREDICTABLE",CTy"exception", 4067 CC[LS"Decode ", 4068 CS(Var("mc",CTy"MachineCode"), 4069 [(Call("Thumb",CTy"MachineCode",Var("opc",F16)), 4070 CC[Mop(Cast sTy,Mop(Cast vTy,Var("opc",F16))), 4071 LS"; Thumb; "]), 4072 (Call 4073 ("Thumb2",CTy"MachineCode", 4074 TP[Var("opc1",F16),Var("opc2",F16)]), 4075 CC[Mop(Cast sTy,Mop(Cast vTy,Var("opc1",F16))), 4076 LS", ", 4077 Mop(Cast sTy,Mop(Cast vTy,Var("opc2",F16))), 4078 LS"; Thumb2; "])]),sVar"s"])),qVar"state")))) 4079; 4080val DecodeThumb_def = Def 4081 ("DecodeThumb",Var("h",F16), 4082 Close 4083 (qVar"state", 4084 Let(Var("mc",CTy"MachineCode"), 4085 Call("Thumb",CTy"MachineCode",Var("h",F16)), 4086 Let(TP[bVar"b'15",bVar"b'14",bVar"b'13",bVar"b'12",bVar"b'11", 4087 bVar"b'10",bVar"b'9",bVar"b'8",bVar"b'7",bVar"b'6", 4088 bVar"b'5",bVar"b'4",bVar"b'3",bVar"b'2",bVar"b'1", 4089 bVar"b'0"],BL(16,Var("h",F16)), 4090 ITB([(bVar"b'15", 4091 ITB([(bVar"b'13", 4092 ITB([(Bop(And,Mop(Not,bVar"b'14"), 4093 Mop(Not,bVar"b'12")), 4094 TP[Call 4095 ("Data",CTy"instruction", 4096 Call 4097 ("ArithLogicImmediate",CTy"Data", 4098 TP[LW(4,4),LF, 4099 Mop(Cast F4, 4100 Mop(Cast(FTy 3), 4101 LL[bVar"b'10", 4102 bVar"b'9",bVar"b'8"])), 4103 ITE(EQ(Mop(Cast F1, 4104 LL[bVar"b'11"]), 4105 LW(1,1)),LW(13,4), 4106 LW(15,4)), 4107 Mop(Cast F32, 4108 CC[Mop(Cast F8, 4109 LL[bVar"b'7", 4110 bVar"b'6", 4111 bVar"b'5", 4112 bVar"b'4", 4113 bVar"b'3", 4114 bVar"b'2", 4115 bVar"b'1", 4116 bVar"b'0"]), 4117 LW(0,2)])])), 4118 qVar"state"]), 4119 (Bop(And,Mop(Not,bVar"b'14"), 4120 Bop(And,bVar"b'12", 4121 Bop(And,Mop(Not,bVar"b'11"), 4122 Bop(And,Mop(Not,bVar"b'10"), 4123 Bop(And, 4124 Mop(Not,bVar"b'9"), 4125 Mop(Not,bVar"b'8")))))), 4126 TP[Call 4127 ("Data",CTy"instruction", 4128 Call 4129 ("ArithLogicImmediate",CTy"Data", 4130 TP[ITE(EQ(Mop(Cast F1, 4131 LL[bVar"b'7"]), 4132 LW(1,1)),LW(2,4), 4133 LW(4,4)),LF,LW(13,4), 4134 LW(13,4), 4135 Mop(Cast F32, 4136 CC[Mop(Cast(FTy 7), 4137 LL[bVar"b'6", 4138 bVar"b'5", 4139 bVar"b'4", 4140 bVar"b'3", 4141 bVar"b'2", 4142 bVar"b'1", 4143 bVar"b'0"]), 4144 LW(0,2)])])), 4145 qVar"state"]), 4146 (Bop(And,Mop(Not,bVar"b'14"), 4147 Bop(And,bVar"b'12", 4148 Bop(And,Mop(Not,bVar"b'11"), 4149 Bop(And,Mop(Not,bVar"b'10"), 4150 Bop(And,bVar"b'9", 4151 Bop(And, 4152 Mop(Not,bVar"b'8"), 4153 Mop(Not,bVar"b'6"))))))), 4154 TP[Call 4155 ("Media",CTy"instruction", 4156 Call 4157 ("ExtendHalfword",CTy"Media", 4158 TP[EQ(Mop(Cast F1,LL[bVar"b'7"]), 4159 LW(1,1)), 4160 Mop(Cast F4, 4161 Mop(Cast(FTy 3), 4162 LL[bVar"b'2", 4163 bVar"b'1",bVar"b'0"])), 4164 Mop(Cast F4, 4165 Mop(Cast(FTy 3), 4166 LL[bVar"b'5", 4167 bVar"b'4",bVar"b'3"]))])), 4168 qVar"state"]), 4169 (Bop(And,Mop(Not,bVar"b'14"), 4170 Bop(And,bVar"b'12", 4171 Bop(And,Mop(Not,bVar"b'11"), 4172 Bop(And,Mop(Not,bVar"b'10"), 4173 Bop(And,bVar"b'9", 4174 Bop(And, 4175 Mop(Not,bVar"b'8"), 4176 bVar"b'6")))))), 4177 TP[Call 4178 ("Media",CTy"instruction", 4179 Call 4180 ("ExtendByte",CTy"Media", 4181 TP[EQ(Mop(Cast F1,LL[bVar"b'7"]), 4182 LW(1,1)), 4183 Mop(Cast F4, 4184 Mop(Cast(FTy 3), 4185 LL[bVar"b'2", 4186 bVar"b'1",bVar"b'0"])), 4187 Mop(Cast F4, 4188 Mop(Cast(FTy 3), 4189 LL[bVar"b'5", 4190 bVar"b'4",bVar"b'3"]))])), 4191 qVar"state"]), 4192 (Bop(And,Mop(Not,bVar"b'14"), 4193 Bop(And,bVar"b'12", 4194 Bop(And,Mop(Not,bVar"b'11"), 4195 Bop(And,bVar"b'10", 4196 Mop(Not,bVar"b'9"))))), 4197 Let(Var("registers",FTy 9), 4198 Mop(Cast(FTy 9), 4199 LL[bVar"b'8",bVar"b'7",bVar"b'6", 4200 bVar"b'5",bVar"b'4",bVar"b'3", 4201 bVar"b'2",bVar"b'1",bVar"b'0"]), 4202 TP[Call 4203 ("Store",CTy"instruction", 4204 Call 4205 ("Push",CTy"Store", 4206 Var("registers",FTy 9))), 4207 ITE(Bop(Lt, 4208 Call 4209 ("BitCount",nTy, 4210 Var("registers",FTy 9)), 4211 LN 1), 4212 Apply 4213 (Call 4214 ("DECODE_UNPREDICTABLE", 4215 ATy(qTy,qTy), 4216 TP[Var("mc", 4217 CTy"MachineCode"), 4218 LS"Push"]),qVar"state"), 4219 qVar"state")])), 4220 (Bop(And,Mop(Not,bVar"b'14"), 4221 Bop(And,bVar"b'12", 4222 Bop(And,Mop(Not,bVar"b'11"), 4223 Bop(And,bVar"b'10", 4224 Bop(And,bVar"b'9", 4225 Bop(And, 4226 Mop(Not,bVar"b'8"), 4227 Bop(And, 4228 Mop(Not, 4229 bVar"b'7"), 4230 Bop(And, 4231 bVar"b'6", 4232 bVar"b'5")))))))), 4233 TP[Call 4234 ("System",CTy"instruction", 4235 Call 4236 ("ChangeProcessorState", 4237 CTy"System", 4238 Mop(Cast bTy, 4239 Mop(Cast F1,LL[bVar"b'4"])))), 4240 qVar"state"]), 4241 (Bop(And,Mop(Not,bVar"b'14"), 4242 Bop(And,bVar"b'12", 4243 Bop(And,bVar"b'11", 4244 Bop(And,Mop(Not,bVar"b'10"), 4245 Bop(And,bVar"b'9", 4246 Mop(Not,bVar"b'8")))))), 4247 Let(Var("Rd",FTy 3), 4248 Mop(Cast(FTy 3), 4249 LL[bVar"b'2",bVar"b'1",bVar"b'0"]), 4250 Let(Var("Rm",FTy 3), 4251 Mop(Cast(FTy 3), 4252 LL[bVar"b'5",bVar"b'4", 4253 bVar"b'3"]), 4254 TP[CS(Mop(Cast(FTy 2), 4255 LL[bVar"b'7",bVar"b'6"]), 4256 [(LW(0,2), 4257 Call 4258 ("Media", 4259 CTy"instruction", 4260 Call 4261 ("ByteReverse", 4262 CTy"Media", 4263 TP[Mop(Cast F4, 4264 Var("Rd", 4265 FTy 3)), 4266 Mop(Cast F4, 4267 Var("Rm", 4268 FTy 3))]))), 4269 (LW(1,2), 4270 Call 4271 ("Media", 4272 CTy"instruction", 4273 Call 4274 ("ByteReversePackedHalfword", 4275 CTy"Media", 4276 TP[Mop(Cast F4, 4277 Var("Rd", 4278 FTy 3)), 4279 Mop(Cast F4, 4280 Var("Rm", 4281 FTy 3))]))), 4282 (LW(3,2), 4283 Call 4284 ("Media", 4285 CTy"instruction", 4286 Call 4287 ("ByteReverseSignedHalfword", 4288 CTy"Media", 4289 TP[Mop(Cast F4, 4290 Var("Rd", 4291 FTy 3)), 4292 Mop(Cast F4, 4293 Var("Rm", 4294 FTy 3))]))), 4295 (AVar(FTy 2), 4296 Call 4297 ("Undefined", 4298 CTy"instruction", 4299 LW(0,32)))]), 4300 qVar"state"]))), 4301 (Bop(And,Mop(Not,bVar"b'14"), 4302 Bop(And,bVar"b'12", 4303 Bop(And,bVar"b'11", 4304 Bop(And,bVar"b'10", 4305 Mop(Not,bVar"b'9"))))), 4306 Let(Var("registers",FTy 9), 4307 Mop(Cast(FTy 9), 4308 LL[bVar"b'8",bVar"b'7",bVar"b'6", 4309 bVar"b'5",bVar"b'4",bVar"b'3", 4310 bVar"b'2",bVar"b'1",bVar"b'0"]), 4311 TP[Call 4312 ("Load",CTy"instruction", 4313 Call 4314 ("LoadMultiple",CTy"Load", 4315 TP[LT,LW(13,4), 4316 Var("registers",FTy 9)])), 4317 ITE(Bop(Lt, 4318 Call 4319 ("BitCount",nTy, 4320 Var("registers",FTy 9)), 4321 LN 1), 4322 Apply 4323 (Call 4324 ("DECODE_UNPREDICTABLE", 4325 ATy(qTy,qTy), 4326 TP[Var("mc", 4327 CTy"MachineCode"), 4328 LS"POP"]),qVar"state"), 4329 qVar"state")]))], 4330 TP[ITB([(Bop(And,Mop(Not,bVar"b'14"), 4331 Bop(And,bVar"b'12", 4332 Bop(And,bVar"b'11", 4333 Bop(And,bVar"b'10", 4334 Bop(And,bVar"b'9", 4335 Mop(Not, 4336 bVar"b'8")))))), 4337 Call 4338 ("Hint",CTy"instruction", 4339 Call 4340 ("Breakpoint",CTy"Hint", 4341 Mop(Cast F32, 4342 Mop(Cast F8, 4343 LL[bVar"b'7", 4344 bVar"b'6", 4345 bVar"b'5", 4346 bVar"b'4", 4347 bVar"b'3", 4348 bVar"b'2", 4349 bVar"b'1", 4350 bVar"b'0"]))))), 4351 (Bop(And,Mop(Not,bVar"b'14"), 4352 Bop(And,bVar"b'12", 4353 Bop(And,bVar"b'11", 4354 Bop(And,bVar"b'10", 4355 Bop(And,bVar"b'9", 4356 Bop(And, 4357 bVar"b'8", 4358 Bop(And, 4359 Mop(Not, 4360 bVar"b'3"), 4361 Bop(And, 4362 Mop(Not, 4363 bVar"b'2"), 4364 Bop(And, 4365 Mop(Not, 4366 bVar"b'1"), 4367 Mop(Not, 4368 bVar"b'0")))))))))), 4369 CS(Mop(Cast F4, 4370 LL[bVar"b'7",bVar"b'6", 4371 bVar"b'5",bVar"b'4"]), 4372 [(LW(1,4), 4373 Call 4374 ("Hint",CTy"instruction", 4375 Call("Yield",CTy"Hint",LU))), 4376 (LW(2,4), 4377 Call 4378 ("Hint",CTy"instruction", 4379 Call 4380 ("WaitForEvent", 4381 CTy"Hint",LU))), 4382 (LW(3,4), 4383 Call 4384 ("Hint",CTy"instruction", 4385 Call 4386 ("WaitForInterrupt", 4387 CTy"Hint",LU))), 4388 (LW(4,4), 4389 Call 4390 ("Hint",CTy"instruction", 4391 Call 4392 ("SendEvent",CTy"Hint",LU))), 4393 (AVar F4, 4394 Call 4395 ("NoOperation", 4396 CTy"instruction",LU))])), 4397 (Bop(And,bVar"b'14", 4398 Bop(And,Mop(Not,bVar"b'12"), 4399 Mop(Not,bVar"b'11"))), 4400 Call 4401 ("Branch",CTy"instruction", 4402 Call 4403 ("BranchTarget",CTy"Branch", 4404 Mop(SE F32, 4405 CC[Mop(Cast(FTy 11), 4406 LL[bVar"b'10", 4407 bVar"b'9", 4408 bVar"b'8", 4409 bVar"b'7", 4410 bVar"b'6", 4411 bVar"b'5", 4412 bVar"b'4", 4413 bVar"b'3", 4414 bVar"b'2", 4415 bVar"b'1", 4416 bVar"b'0"]), 4417 LW(0,1)]))))], 4418 Call 4419 ("Undefined",CTy"instruction", 4420 LW(0,32))),qVar"state"])), 4421 (Bop(And,Mop(Not,bVar"b'14"),Mop(Not,bVar"b'12")), 4422 Let(Var("Rt",FTy 3), 4423 Mop(Cast(FTy 3), 4424 LL[bVar"b'2",bVar"b'1",bVar"b'0"]), 4425 Let(Var("Rn",FTy 3), 4426 Mop(Cast(FTy 3), 4427 LL[bVar"b'5",bVar"b'4",bVar"b'3"]), 4428 TP[Let(Var("m",CTy"offset"), 4429 Call 4430 ("immediate_form",CTy"offset", 4431 Mop(Cast F32, 4432 CC[Mop(Cast(FTy 5), 4433 LL[bVar"b'10", 4434 bVar"b'9", 4435 bVar"b'8", 4436 bVar"b'7", 4437 bVar"b'6"]), 4438 LW(0,1)])), 4439 ITE(EQ(Mop(Cast F1,LL[bVar"b'11"]), 4440 LW(1,1)), 4441 Call 4442 ("Load",CTy"instruction", 4443 Call 4444 ("LoadHalf",CTy"Load", 4445 TP[LT, 4446 Mop(Cast F4, 4447 Var("Rt",FTy 3)), 4448 Mop(Cast F4, 4449 Var("Rn",FTy 3)), 4450 Var("m",CTy"offset")])), 4451 Call 4452 ("Store",CTy"instruction", 4453 Call 4454 ("StoreHalf",CTy"Store", 4455 TP[Mop(Cast F4, 4456 Var("Rt",FTy 3)), 4457 Mop(Cast F4, 4458 Var("Rn",FTy 3)), 4459 Var("m",CTy"offset")])))), 4460 qVar"state"]))), 4461 (Bop(And,Mop(Not,bVar"b'14"),bVar"b'12"), 4462 Let(Var("Rt",FTy 3), 4463 Mop(Cast(FTy 3), 4464 LL[bVar"b'10",bVar"b'9",bVar"b'8"]), 4465 TP[Let(Var("m",CTy"offset"), 4466 Call 4467 ("immediate_form",CTy"offset", 4468 Mop(Cast F32, 4469 CC[Mop(Cast F8, 4470 LL[bVar"b'7",bVar"b'6", 4471 bVar"b'5",bVar"b'4", 4472 bVar"b'3",bVar"b'2", 4473 bVar"b'1",bVar"b'0"]), 4474 LW(0,2)])), 4475 ITE(EQ(Mop(Cast F1,LL[bVar"b'11"]), 4476 LW(1,1)), 4477 Call 4478 ("Load",CTy"instruction", 4479 Call 4480 ("LoadWord",CTy"Load", 4481 TP[Mop(Cast F4, 4482 Var("Rt",FTy 3)), 4483 LW(13,4), 4484 Var("m",CTy"offset")])), 4485 Call 4486 ("Store",CTy"instruction", 4487 Call 4488 ("StoreWord",CTy"Store", 4489 TP[Mop(Cast F4, 4490 Var("Rt",FTy 3)), 4491 LW(13,4), 4492 Var("m",CTy"offset")])))), 4493 qVar"state"])), 4494 (Bop(And,bVar"b'14", 4495 Bop(And,Mop(Not,bVar"b'12"), 4496 Mop(Not,bVar"b'11"))), 4497 Let(Var("registers",F8), 4498 Mop(Cast F8, 4499 LL[bVar"b'7",bVar"b'6",bVar"b'5", 4500 bVar"b'4",bVar"b'3",bVar"b'2", 4501 bVar"b'1",bVar"b'0"]), 4502 TP[Call 4503 ("Store",CTy"instruction", 4504 Call 4505 ("StoreMultiple",CTy"Store", 4506 TP[Mop(Cast F4, 4507 Mop(Cast(FTy 3), 4508 LL[bVar"b'10",bVar"b'9", 4509 bVar"b'8"])), 4510 Var("registers",F8)])), 4511 ITE(Bop(Lt, 4512 Call 4513 ("BitCount",nTy, 4514 Var("registers",F8)),LN 1), 4515 Apply 4516 (Call 4517 ("DECODE_UNPREDICTABLE", 4518 ATy(qTy,qTy), 4519 TP[Var("mc",CTy"MachineCode"), 4520 LS"StoreMultiple"]), 4521 qVar"state"),qVar"state")])), 4522 (Bop(And,bVar"b'14", 4523 Bop(And,Mop(Not,bVar"b'12"),bVar"b'11")), 4524 Let(Var("Rn",FTy 3), 4525 Mop(Cast(FTy 3), 4526 LL[bVar"b'10",bVar"b'9",bVar"b'8"]), 4527 Let(Var("registers",FTy 9), 4528 Mop(Cast(FTy 9), 4529 Mop(Cast F8, 4530 LL[bVar"b'7",bVar"b'6", 4531 bVar"b'5",bVar"b'4", 4532 bVar"b'3",bVar"b'2", 4533 bVar"b'1",bVar"b'0"])), 4534 TP[Call 4535 ("Load",CTy"instruction", 4536 Call 4537 ("LoadMultiple",CTy"Load", 4538 TP[Mop(Not, 4539 Bop(Bit, 4540 Var("registers", 4541 FTy 9), 4542 Mop(Cast nTy, 4543 Var("Rn",FTy 3)))), 4544 Mop(Cast F4,Var("Rn",FTy 3)), 4545 Var("registers",FTy 9)])), 4546 ITE(Bop(Lt, 4547 Call 4548 ("BitCount",nTy, 4549 Var("registers",FTy 9)), 4550 LN 1), 4551 Apply 4552 (Call 4553 ("DECODE_UNPREDICTABLE", 4554 ATy(qTy,qTy), 4555 TP[Var("mc", 4556 CTy"MachineCode"), 4557 LS"LoadMultiple"]), 4558 qVar"state"),qVar"state")])))], 4559 TP[ITB([(Bop(And,bVar"b'14", 4560 Bop(And,bVar"b'12", 4561 Bop(And,bVar"b'11", 4562 Bop(And,bVar"b'10", 4563 Bop(And,bVar"b'9", 4564 Mop(Not,bVar"b'8")))))), 4565 Call 4566 ("Undefined",CTy"instruction", 4567 Mop(Cast F32, 4568 Mop(Cast F8, 4569 LL[bVar"b'7",bVar"b'6", 4570 bVar"b'5",bVar"b'4", 4571 bVar"b'3",bVar"b'2", 4572 bVar"b'1",bVar"b'0"])))), 4573 (Bop(And,bVar"b'14", 4574 Bop(And,bVar"b'12", 4575 Bop(And,bVar"b'11", 4576 Bop(And,bVar"b'10", 4577 Bop(And,bVar"b'9", 4578 bVar"b'8"))))), 4579 Call 4580 ("System",CTy"instruction", 4581 Call 4582 ("SupervisorCall",CTy"System", 4583 Mop(Cast F32, 4584 Mop(Cast F8, 4585 LL[bVar"b'7",bVar"b'6", 4586 bVar"b'5",bVar"b'4", 4587 bVar"b'3",bVar"b'2", 4588 bVar"b'1",bVar"b'0"]))))), 4589 (Bop(And,bVar"b'14",bVar"b'12"), 4590 ITE(Apply 4591 (Call 4592 ("ConditionPassed",ATy(qTy,bTy), 4593 Mop(Cast F4, 4594 LL[bVar"b'11",bVar"b'10", 4595 bVar"b'9",bVar"b'8"])), 4596 qVar"state"), 4597 Call 4598 ("Branch",CTy"instruction", 4599 Call 4600 ("BranchTarget",CTy"Branch", 4601 Mop(SE F32, 4602 CC[Mop(Cast F8, 4603 LL[bVar"b'7", 4604 bVar"b'6", 4605 bVar"b'5", 4606 bVar"b'4", 4607 bVar"b'3", 4608 bVar"b'2", 4609 bVar"b'1", 4610 bVar"b'0"]), 4611 LW(0,1)]))), 4612 Call 4613 ("NoOperation",CTy"instruction",LU)))], 4614 Call("Undefined",CTy"instruction",LW(0,32))), 4615 qVar"state"])), 4616 (bVar"b'14", 4617 ITB([(Bop(And,Mop(Not,bVar"b'13"), 4618 Bop(And,Mop(Not,bVar"b'12"), 4619 Bop(And,Mop(Not,bVar"b'11"), 4620 Mop(Not,bVar"b'10")))), 4621 Let(Var("Ry",FTy 3), 4622 Mop(Cast(FTy 3), 4623 LL[bVar"b'2",bVar"b'1",bVar"b'0"]), 4624 Let(Var("Rx",FTy 3), 4625 Mop(Cast(FTy 3), 4626 LL[bVar"b'5",bVar"b'4",bVar"b'3"]), 4627 Let(Var("opc",F4), 4628 Mop(Cast F4, 4629 LL[bVar"b'9",bVar"b'8", 4630 bVar"b'7",bVar"b'6"]), 4631 TP[CS(Var("opc",F4), 4632 [(LW(0,4), 4633 Let(Var("d",F4), 4634 Mop(Cast F4, 4635 Var("Ry",FTy 3)), 4636 Call 4637 ("Data", 4638 CTy"instruction", 4639 Call 4640 ("Register", 4641 CTy"Data", 4642 TP[Var("opc",F4), 4643 LT,Var("d",F4), 4644 Var("d",F4), 4645 Mop(Cast F4, 4646 Var("Rx", 4647 FTy 3))])))), 4648 (LW(1,4), 4649 Let(Var("d",F4), 4650 Mop(Cast F4, 4651 Var("Ry",FTy 3)), 4652 Call 4653 ("Data", 4654 CTy"instruction", 4655 Call 4656 ("Register", 4657 CTy"Data", 4658 TP[Var("opc",F4), 4659 LT,Var("d",F4), 4660 Var("d",F4), 4661 Mop(Cast F4, 4662 Var("Rx", 4663 FTy 3))])))), 4664 (LW(5,4), 4665 Let(Var("d",F4), 4666 Mop(Cast F4, 4667 Var("Ry",FTy 3)), 4668 Call 4669 ("Data", 4670 CTy"instruction", 4671 Call 4672 ("Register", 4673 CTy"Data", 4674 TP[Var("opc",F4), 4675 LT,Var("d",F4), 4676 Var("d",F4), 4677 Mop(Cast F4, 4678 Var("Rx", 4679 FTy 3))])))), 4680 (LW(6,4), 4681 Let(Var("d",F4), 4682 Mop(Cast F4, 4683 Var("Ry",FTy 3)), 4684 Call 4685 ("Data", 4686 CTy"instruction", 4687 Call 4688 ("Register", 4689 CTy"Data", 4690 TP[Var("opc",F4), 4691 LT,Var("d",F4), 4692 Var("d",F4), 4693 Mop(Cast F4, 4694 Var("Rx", 4695 FTy 3))])))), 4696 (LW(12,4), 4697 Let(Var("d",F4), 4698 Mop(Cast F4, 4699 Var("Ry",FTy 3)), 4700 Call 4701 ("Data", 4702 CTy"instruction", 4703 Call 4704 ("Register", 4705 CTy"Data", 4706 TP[Var("opc",F4), 4707 LT,Var("d",F4), 4708 Var("d",F4), 4709 Mop(Cast F4, 4710 Var("Rx", 4711 FTy 3))])))), 4712 (LW(14,4), 4713 Let(Var("d",F4), 4714 Mop(Cast F4, 4715 Var("Ry",FTy 3)), 4716 Call 4717 ("Data", 4718 CTy"instruction", 4719 Call 4720 ("Register", 4721 CTy"Data", 4722 TP[Var("opc",F4), 4723 LT,Var("d",F4), 4724 Var("d",F4), 4725 Mop(Cast F4, 4726 Var("Rx", 4727 FTy 3))])))), 4728 (LW(2,4), 4729 Let(Var("d",F4), 4730 Mop(Cast F4, 4731 Var("Ry",FTy 3)), 4732 Call 4733 ("Data", 4734 CTy"instruction", 4735 Call 4736 ("ShiftRegister", 4737 CTy"Data", 4738 TP[Var("d",F4), 4739 Var("d",F4), 4740 Call 4741 ("DecodeRegShift", 4742 CTy"SRType", 4743 Mop(Cast 4744 (FTy 2), 4745 Bop(Sub, 4746 Var("opc", 4747 F4), 4748 LW(2, 4749 4)))), 4750 Mop(Cast F4, 4751 Var("Rx", 4752 FTy 3))])))), 4753 (LW(3,4), 4754 Let(Var("d",F4), 4755 Mop(Cast F4, 4756 Var("Ry",FTy 3)), 4757 Call 4758 ("Data", 4759 CTy"instruction", 4760 Call 4761 ("ShiftRegister", 4762 CTy"Data", 4763 TP[Var("d",F4), 4764 Var("d",F4), 4765 Call 4766 ("DecodeRegShift", 4767 CTy"SRType", 4768 Mop(Cast 4769 (FTy 2), 4770 Bop(Sub, 4771 Var("opc", 4772 F4), 4773 LW(2, 4774 4)))), 4775 Mop(Cast F4, 4776 Var("Rx", 4777 FTy 3))])))), 4778 (LW(4,4), 4779 Let(Var("d",F4), 4780 Mop(Cast F4, 4781 Var("Ry",FTy 3)), 4782 Call 4783 ("Data", 4784 CTy"instruction", 4785 Call 4786 ("ShiftRegister", 4787 CTy"Data", 4788 TP[Var("d",F4), 4789 Var("d",F4), 4790 Call 4791 ("DecodeRegShift", 4792 CTy"SRType", 4793 Mop(Cast 4794 (FTy 2), 4795 Bop(Sub, 4796 Var("opc", 4797 F4), 4798 LW(2, 4799 4)))), 4800 Mop(Cast F4, 4801 Var("Rx", 4802 FTy 3))])))), 4803 (LW(7,4), 4804 Let(Var("d",F4), 4805 Mop(Cast F4, 4806 Var("Ry",FTy 3)), 4807 Call 4808 ("Data", 4809 CTy"instruction", 4810 Call 4811 ("ShiftRegister", 4812 CTy"Data", 4813 TP[Var("d",F4), 4814 Var("d",F4), 4815 LC("SRType_ROR", 4816 CTy"SRType"), 4817 Mop(Cast F4, 4818 Var("Rx", 4819 FTy 3))])))), 4820 (LW(8,4), 4821 Call 4822 ("Data",CTy"instruction", 4823 Call 4824 ("TestCompareRegister", 4825 CTy"Data", 4826 TP[EX(Var("opc",F4), 4827 LN 1,LN 0,FTy 2), 4828 Mop(Cast F4, 4829 Var("Ry",FTy 3)), 4830 Mop(Cast F4, 4831 Var("Rx",FTy 3))]))), 4832 (LW(10,4), 4833 Call 4834 ("Data",CTy"instruction", 4835 Call 4836 ("TestCompareRegister", 4837 CTy"Data", 4838 TP[EX(Var("opc",F4), 4839 LN 1,LN 0,FTy 2), 4840 Mop(Cast F4, 4841 Var("Ry",FTy 3)), 4842 Mop(Cast F4, 4843 Var("Rx",FTy 3))]))), 4844 (LW(11,4), 4845 Call 4846 ("Data",CTy"instruction", 4847 Call 4848 ("TestCompareRegister", 4849 CTy"Data", 4850 TP[EX(Var("opc",F4), 4851 LN 1,LN 0,FTy 2), 4852 Mop(Cast F4, 4853 Var("Ry",FTy 3)), 4854 Mop(Cast F4, 4855 Var("Rx",FTy 3))]))), 4856 (LW(9,4), 4857 Call 4858 ("Data",CTy"instruction", 4859 Call 4860 ("ArithLogicImmediate", 4861 CTy"Data", 4862 TP[LW(3,4),LT, 4863 Mop(Cast F4, 4864 Var("Ry",FTy 3)), 4865 Mop(Cast F4, 4866 Var("Rx",FTy 3)), 4867 LW(0,32)]))), 4868 (LW(13,4), 4869 Let(Var("d",F4), 4870 Mop(Cast F4, 4871 Var("Ry",FTy 3)), 4872 Call 4873 ("Multiply", 4874 CTy"instruction", 4875 Call 4876 ("Multiply32", 4877 CTy"Multiply", 4878 TP[Var("d",F4), 4879 Mop(Cast F4, 4880 Var("Rx", 4881 FTy 3)), 4882 Var("d",F4)])))), 4883 (LW(15,4), 4884 Call 4885 ("Data",CTy"instruction", 4886 Call 4887 ("ShiftImmediate", 4888 CTy"Data", 4889 TP[LT,LT, 4890 Mop(Cast F4, 4891 Var("Ry",FTy 3)), 4892 Mop(Cast F4, 4893 Var("Rx",FTy 3)), 4894 LC("SRType_LSL", 4895 CTy"SRType"), 4896 LN 0])))]), 4897 qVar"state"])))), 4898 (Bop(And,Mop(Not,bVar"b'13"), 4899 Bop(And,Mop(Not,bVar"b'12"), 4900 Bop(And,Mop(Not,bVar"b'11"), 4901 Bop(And,bVar"b'10", 4902 Bop(And,Mop(Not,bVar"b'9"), 4903 Mop(Not,bVar"b'8")))))), 4904 Let(Var("Rm",F4), 4905 Mop(Cast F4, 4906 LL[bVar"b'6",bVar"b'5",bVar"b'4", 4907 bVar"b'3"]), 4908 Let(Var("d",F4), 4909 CC[Mop(Cast F1,LL[bVar"b'7"]), 4910 Mop(Cast(FTy 3), 4911 LL[bVar"b'2",bVar"b'1",bVar"b'0"])], 4912 TP[Call 4913 ("Data",CTy"instruction", 4914 Call 4915 ("Register",CTy"Data", 4916 TP[LW(4,4),LF,Var("d",F4), 4917 Var("d",F4),Var("Rm",F4)])), 4918 ITE(Bop(And,EQ(Var("d",F4),LW(15,4)), 4919 EQ(Var("Rm",F4),LW(15,4))), 4920 Apply 4921 (Call 4922 ("DECODE_UNPREDICTABLE", 4923 ATy(qTy,qTy), 4924 TP[Var("mc", 4925 CTy"MachineCode"), 4926 LS"ADD"]),qVar"state"), 4927 qVar"state")]))), 4928 (Bop(And,Mop(Not,bVar"b'13"), 4929 Bop(And,Mop(Not,bVar"b'12"), 4930 Bop(And,Mop(Not,bVar"b'11"), 4931 Bop(And,bVar"b'10", 4932 Bop(And,Mop(Not,bVar"b'9"), 4933 bVar"b'8"))))), 4934 Let(Var("Rm",F4), 4935 Mop(Cast F4, 4936 LL[bVar"b'6",bVar"b'5",bVar"b'4", 4937 bVar"b'3"]), 4938 Let(Var("n",F4), 4939 CC[Mop(Cast F1,LL[bVar"b'7"]), 4940 Mop(Cast(FTy 3), 4941 LL[bVar"b'2",bVar"b'1",bVar"b'0"])], 4942 TP[Call 4943 ("Data",CTy"instruction", 4944 Call 4945 ("TestCompareRegister", 4946 CTy"Data", 4947 TP[LW(2,2),Var("n",F4), 4948 Var("Rm",F4)])), 4949 ITE(Bop(Or, 4950 Bop(And, 4951 Bop(Ult,Var("n",F4), 4952 LW(8,4)), 4953 Bop(Ult,Var("Rm",F4), 4954 LW(8,4))), 4955 Bop(Or, 4956 EQ(Var("n",F4),LW(15,4)), 4957 EQ(Var("Rm",F4),LW(15,4)))), 4958 Apply 4959 (Call 4960 ("DECODE_UNPREDICTABLE", 4961 ATy(qTy,qTy), 4962 TP[Var("mc", 4963 CTy"MachineCode"), 4964 LS"CMP"]),qVar"state"), 4965 qVar"state")]))), 4966 (Bop(And,Mop(Not,bVar"b'13"), 4967 Bop(And,Mop(Not,bVar"b'12"), 4968 Bop(And,Mop(Not,bVar"b'11"), 4969 Bop(And,bVar"b'10", 4970 Bop(And,bVar"b'9", 4971 Mop(Not,bVar"b'8")))))), 4972 TP[Call 4973 ("Data",CTy"instruction", 4974 Call 4975 ("ShiftImmediate",CTy"Data", 4976 TP[LF,LF, 4977 CC[Mop(Cast F1,LL[bVar"b'7"]), 4978 Mop(Cast(FTy 3), 4979 LL[bVar"b'2",bVar"b'1", 4980 bVar"b'0"])], 4981 Mop(Cast F4, 4982 LL[bVar"b'6",bVar"b'5", 4983 bVar"b'4",bVar"b'3"]), 4984 LC("SRType_LSL",CTy"SRType"),LN 0])), 4985 qVar"state"]), 4986 (Bop(And,Mop(Not,bVar"b'13"), 4987 Bop(And,Mop(Not,bVar"b'12"), 4988 Bop(And,Mop(Not,bVar"b'11"), 4989 Bop(And,bVar"b'10", 4990 Bop(And,bVar"b'9", 4991 Bop(And,bVar"b'8", 4992 Mop(Not,bVar"b'7"))))))), 4993 TP[Call 4994 ("Branch",CTy"instruction", 4995 Call 4996 ("BranchExchange",CTy"Branch", 4997 Mop(Cast F4, 4998 LL[bVar"b'6",bVar"b'5",bVar"b'4", 4999 bVar"b'3"]))),qVar"state"]), 5000 (Bop(And,Mop(Not,bVar"b'13"), 5001 Bop(And,Mop(Not,bVar"b'12"), 5002 Bop(And,Mop(Not,bVar"b'11"), 5003 Bop(And,bVar"b'10", 5004 Bop(And,bVar"b'9", 5005 Bop(And,bVar"b'8",bVar"b'7")))))), 5006 TP[Call 5007 ("Branch",CTy"instruction", 5008 Call 5009 ("BranchLinkExchangeRegister", 5010 CTy"Branch", 5011 Mop(Cast F4, 5012 LL[bVar"b'6",bVar"b'5",bVar"b'4", 5013 bVar"b'3"]))),qVar"state"]), 5014 (Bop(And,Mop(Not,bVar"b'13"), 5015 Bop(And,Mop(Not,bVar"b'12"),bVar"b'11")), 5016 TP[Call 5017 ("Load",CTy"instruction", 5018 Call 5019 ("LoadLiteral",CTy"Load", 5020 TP[Mop(Cast F4, 5021 Mop(Cast(FTy 3), 5022 LL[bVar"b'10",bVar"b'9", 5023 bVar"b'8"])), 5024 Mop(Cast F32, 5025 CC[Mop(Cast F8, 5026 LL[bVar"b'7",bVar"b'6", 5027 bVar"b'5",bVar"b'4", 5028 bVar"b'3",bVar"b'2", 5029 bVar"b'1",bVar"b'0"]), 5030 LW(0,2)])])),qVar"state"]), 5031 (Bop(And,Mop(Not,bVar"b'13"),bVar"b'12"), 5032 Let(Var("Rt",FTy 3), 5033 Mop(Cast(FTy 3), 5034 LL[bVar"b'2",bVar"b'1",bVar"b'0"]), 5035 Let(Var("Rn",FTy 3), 5036 Mop(Cast(FTy 3), 5037 LL[bVar"b'5",bVar"b'4",bVar"b'3"]), 5038 TP[Let(Var("m",CTy"offset"), 5039 Call 5040 ("register_form",CTy"offset", 5041 Mop(Cast F4, 5042 Mop(Cast(FTy 3), 5043 LL[bVar"b'8", 5044 bVar"b'7",bVar"b'6"]))), 5045 CS(Mop(Cast(FTy 3), 5046 LL[bVar"b'11",bVar"b'10", 5047 bVar"b'9"]), 5048 [(LW(0,3), 5049 Call 5050 ("Store",CTy"instruction", 5051 Call 5052 ("StoreWord", 5053 CTy"Store", 5054 TP[Mop(Cast F4, 5055 Var("Rt",FTy 3)), 5056 Mop(Cast F4, 5057 Var("Rn",FTy 3)), 5058 Var("m",CTy"offset")]))), 5059 (LW(1,3), 5060 Call 5061 ("Store",CTy"instruction", 5062 Call 5063 ("StoreHalf", 5064 CTy"Store", 5065 TP[Mop(Cast F4, 5066 Var("Rt",FTy 3)), 5067 Mop(Cast F4, 5068 Var("Rn",FTy 3)), 5069 Var("m",CTy"offset")]))), 5070 (LW(2,3), 5071 Call 5072 ("Store",CTy"instruction", 5073 Call 5074 ("StoreByte", 5075 CTy"Store", 5076 TP[Mop(Cast F4, 5077 Var("Rt",FTy 3)), 5078 Mop(Cast F4, 5079 Var("Rn",FTy 3)), 5080 Var("m",CTy"offset")]))), 5081 (LW(3,3), 5082 Call 5083 ("Load",CTy"instruction", 5084 Call 5085 ("LoadByte",CTy"Load", 5086 TP[LF, 5087 Mop(Cast F4, 5088 Var("Rt",FTy 3)), 5089 Mop(Cast F4, 5090 Var("Rn",FTy 3)), 5091 Var("m",CTy"offset")]))), 5092 (LW(4,3), 5093 Call 5094 ("Load",CTy"instruction", 5095 Call 5096 ("LoadWord",CTy"Load", 5097 TP[Mop(Cast F4, 5098 Var("Rt",FTy 3)), 5099 Mop(Cast F4, 5100 Var("Rn",FTy 3)), 5101 Var("m",CTy"offset")]))), 5102 (LW(5,3), 5103 Call 5104 ("Load",CTy"instruction", 5105 Call 5106 ("LoadHalf",CTy"Load", 5107 TP[LT, 5108 Mop(Cast F4, 5109 Var("Rt",FTy 3)), 5110 Mop(Cast F4, 5111 Var("Rn",FTy 3)), 5112 Var("m",CTy"offset")]))), 5113 (LW(6,3), 5114 Call 5115 ("Load",CTy"instruction", 5116 Call 5117 ("LoadByte",CTy"Load", 5118 TP[LT, 5119 Mop(Cast F4, 5120 Var("Rt",FTy 3)), 5121 Mop(Cast F4, 5122 Var("Rn",FTy 3)), 5123 Var("m",CTy"offset")]))), 5124 (LW(7,3), 5125 Call 5126 ("Load",CTy"instruction", 5127 Call 5128 ("LoadHalf",CTy"Load", 5129 TP[LF, 5130 Mop(Cast F4, 5131 Var("Rt",FTy 3)), 5132 Mop(Cast F4, 5133 Var("Rn",FTy 3)), 5134 Var("m",CTy"offset")])))])), 5135 qVar"state"]))), 5136 (Bop(And,bVar"b'13",Mop(Not,bVar"b'12")), 5137 Let(Var("Rt",FTy 3), 5138 Mop(Cast(FTy 3), 5139 LL[bVar"b'2",bVar"b'1",bVar"b'0"]), 5140 Let(Var("Rn",FTy 3), 5141 Mop(Cast(FTy 3), 5142 LL[bVar"b'5",bVar"b'4",bVar"b'3"]), 5143 TP[Let(Var("m",CTy"offset"), 5144 Call 5145 ("immediate_form",CTy"offset", 5146 Mop(Cast F32, 5147 CC[Mop(Cast(FTy 5), 5148 LL[bVar"b'10", 5149 bVar"b'9", 5150 bVar"b'8", 5151 bVar"b'7", 5152 bVar"b'6"]), 5153 LW(0,2)])), 5154 ITE(EQ(Mop(Cast F1,LL[bVar"b'11"]), 5155 LW(1,1)), 5156 Call 5157 ("Load",CTy"instruction", 5158 Call 5159 ("LoadWord",CTy"Load", 5160 TP[Mop(Cast F4, 5161 Var("Rt",FTy 3)), 5162 Mop(Cast F4, 5163 Var("Rn",FTy 3)), 5164 Var("m",CTy"offset")])), 5165 Call 5166 ("Store",CTy"instruction", 5167 Call 5168 ("StoreWord",CTy"Store", 5169 TP[Mop(Cast F4, 5170 Var("Rt",FTy 3)), 5171 Mop(Cast F4, 5172 Var("Rn",FTy 3)), 5173 Var("m",CTy"offset")])))), 5174 qVar"state"]))), 5175 (Bop(And,bVar"b'13",bVar"b'12"), 5176 Let(Var("Rt",FTy 3), 5177 Mop(Cast(FTy 3), 5178 LL[bVar"b'2",bVar"b'1",bVar"b'0"]), 5179 Let(Var("Rn",FTy 3), 5180 Mop(Cast(FTy 3), 5181 LL[bVar"b'5",bVar"b'4",bVar"b'3"]), 5182 TP[Let(Var("m",CTy"offset"), 5183 Call 5184 ("immediate_form",CTy"offset", 5185 Mop(Cast F32, 5186 Mop(Cast(FTy 5), 5187 LL[bVar"b'10", 5188 bVar"b'9", 5189 bVar"b'8", 5190 bVar"b'7",bVar"b'6"]))), 5191 ITE(EQ(Mop(Cast F1,LL[bVar"b'11"]), 5192 LW(1,1)), 5193 Call 5194 ("Load",CTy"instruction", 5195 Call 5196 ("LoadByte",CTy"Load", 5197 TP[LT, 5198 Mop(Cast F4, 5199 Var("Rt",FTy 3)), 5200 Mop(Cast F4, 5201 Var("Rn",FTy 3)), 5202 Var("m",CTy"offset")])), 5203 Call 5204 ("Store",CTy"instruction", 5205 Call 5206 ("StoreByte",CTy"Store", 5207 TP[Mop(Cast F4, 5208 Var("Rt",FTy 3)), 5209 Mop(Cast F4, 5210 Var("Rn",FTy 3)), 5211 Var("m",CTy"offset")])))), 5212 qVar"state"])))], 5213 TP[Call("Undefined",CTy"instruction",LW(0,32)), 5214 qVar"state"]))], 5215 TP[ITB([(Bop(And,Mop(Not,bVar"b'13"), 5216 Bop(And,bVar"b'12", 5217 Bop(And,bVar"b'11",Mop(Not,bVar"b'10")))), 5218 Call 5219 ("Data",CTy"instruction", 5220 Call 5221 ("Register",CTy"Data", 5222 TP[ITE(EQ(Mop(Cast F1,LL[bVar"b'9"]), 5223 LW(1,1)),LW(2,4),LW(4,4)),LT, 5224 Mop(Cast F4, 5225 Mop(Cast(FTy 3), 5226 LL[bVar"b'2",bVar"b'1", 5227 bVar"b'0"])), 5228 Mop(Cast F4, 5229 Mop(Cast(FTy 3), 5230 LL[bVar"b'5",bVar"b'4", 5231 bVar"b'3"])), 5232 Mop(Cast F4, 5233 Mop(Cast(FTy 3), 5234 LL[bVar"b'8",bVar"b'7", 5235 bVar"b'6"]))]))), 5236 (Bop(And,Mop(Not,bVar"b'13"), 5237 Bop(And,bVar"b'12", 5238 Bop(And,bVar"b'11",bVar"b'10"))), 5239 Call 5240 ("Data",CTy"instruction", 5241 Call 5242 ("ArithLogicImmediate",CTy"Data", 5243 TP[ITE(EQ(Mop(Cast F1,LL[bVar"b'9"]), 5244 LW(1,1)),LW(2,4),LW(4,4)),LT, 5245 Mop(Cast F4, 5246 Mop(Cast(FTy 3), 5247 LL[bVar"b'2",bVar"b'1", 5248 bVar"b'0"])), 5249 Mop(Cast F4, 5250 Mop(Cast(FTy 3), 5251 LL[bVar"b'5",bVar"b'4", 5252 bVar"b'3"])), 5253 Mop(Cast F32, 5254 Mop(Cast(FTy 3), 5255 LL[bVar"b'8",bVar"b'7", 5256 bVar"b'6"]))]))), 5257 (Mop(Not,bVar"b'13"), 5258 Let(TP[Var("shift_t",CTy"SRType"),nVar"shift_n"], 5259 Call 5260 ("DecodeImmShift",PTy(CTy"SRType",nTy), 5261 TP[Mop(Cast(FTy 2), 5262 LL[bVar"b'12",bVar"b'11"]), 5263 Mop(Cast(FTy 5), 5264 LL[bVar"b'10",bVar"b'9", 5265 bVar"b'8",bVar"b'7",bVar"b'6"])]), 5266 Call 5267 ("Data",CTy"instruction", 5268 Call 5269 ("ShiftImmediate",CTy"Data", 5270 TP[LF,LT, 5271 Mop(Cast F4, 5272 Mop(Cast(FTy 3), 5273 LL[bVar"b'2",bVar"b'1", 5274 bVar"b'0"])), 5275 Mop(Cast F4, 5276 Mop(Cast(FTy 3), 5277 LL[bVar"b'5",bVar"b'4", 5278 bVar"b'3"])), 5279 Var("shift_t",CTy"SRType"), 5280 nVar"shift_n"])))), 5281 (Bop(And,bVar"b'13", 5282 Bop(And,Mop(Not,bVar"b'12"), 5283 Mop(Not,bVar"b'11"))), 5284 Call 5285 ("Data",CTy"instruction", 5286 Call 5287 ("Move",CTy"Data", 5288 TP[Mop(Cast F4, 5289 Mop(Cast(FTy 3), 5290 LL[bVar"b'10",bVar"b'9", 5291 bVar"b'8"])), 5292 Mop(Cast F32, 5293 Mop(Cast F8, 5294 LL[bVar"b'7",bVar"b'6", 5295 bVar"b'5",bVar"b'4", 5296 bVar"b'3",bVar"b'2", 5297 bVar"b'1",bVar"b'0"]))]))), 5298 (Bop(And,bVar"b'13", 5299 Bop(And,Mop(Not,bVar"b'12"),bVar"b'11")), 5300 Call 5301 ("Data",CTy"instruction", 5302 Call 5303 ("CompareImmediate",CTy"Data", 5304 TP[Mop(Cast F4, 5305 Mop(Cast(FTy 3), 5306 LL[bVar"b'10",bVar"b'9", 5307 bVar"b'8"])), 5308 Mop(Cast F32, 5309 Mop(Cast F8, 5310 LL[bVar"b'7",bVar"b'6", 5311 bVar"b'5",bVar"b'4", 5312 bVar"b'3",bVar"b'2", 5313 bVar"b'1",bVar"b'0"]))]))), 5314 (Bop(And,bVar"b'13",bVar"b'12"), 5315 Let(Var("d",F4), 5316 Mop(Cast F4, 5317 Mop(Cast(FTy 3), 5318 LL[bVar"b'10",bVar"b'9",bVar"b'8"])), 5319 Call 5320 ("Data",CTy"instruction", 5321 Call 5322 ("ArithLogicImmediate",CTy"Data", 5323 TP[ITE(EQ(Mop(Cast F1,LL[bVar"b'11"]), 5324 LW(1,1)),LW(2,4),LW(4,4)), 5325 LT,Var("d",F4),Var("d",F4), 5326 Mop(Cast F32, 5327 Mop(Cast F8, 5328 LL[bVar"b'7",bVar"b'6", 5329 bVar"b'5",bVar"b'4", 5330 bVar"b'3",bVar"b'2", 5331 bVar"b'1",bVar"b'0"]))]))))], 5332 Call("Undefined",CTy"instruction",LW(0,32))), 5333 qVar"state"]))))) 5334; 5335val DecodeThumb2_def = Def 5336 ("DecodeThumb2",Var("h",PTy(F16,F16)), 5337 Close 5338 (qVar"state", 5339 Let(Var("mc",CTy"MachineCode"), 5340 Call("Thumb2",CTy"MachineCode",Var("h",PTy(F16,F16))), 5341 Let(TP[TP[bVar"b'31",bVar"b'30",bVar"b'29",bVar"b'28", 5342 bVar"b'27",bVar"b'26",bVar"b'25",bVar"b'24", 5343 bVar"b'23",bVar"b'22",bVar"b'21",bVar"b'20", 5344 bVar"b'19",bVar"b'18",bVar"b'17",bVar"b'16"], 5345 bVar"b'15",bVar"b'14",bVar"b'13",bVar"b'12",bVar"b'11", 5346 bVar"b'10",bVar"b'9",bVar"b'8",bVar"b'7",bVar"b'6", 5347 bVar"b'5",bVar"b'4",bVar"b'3",bVar"b'2",bVar"b'1", 5348 bVar"b'0"], 5349 TP[BL(16,Mop(Fst,Var("h",PTy(F16,F16)))), 5350 BL(16,Mop(Snd,Var("h",PTy(F16,F16))))], 5351 ITE(Bop(And,bVar"b'31", 5352 Bop(And,bVar"b'30", 5353 Bop(And,bVar"b'29", 5354 Bop(And,bVar"b'28", 5355 Bop(And,Mop(Not,bVar"b'27"),bVar"b'15"))))), 5356 ITB([(Bop(And,Mop(Not,bVar"b'26"), 5357 Bop(And,bVar"b'25", 5358 Bop(And,bVar"b'24", 5359 Bop(And,bVar"b'23", 5360 Bop(And,Mop(Not,bVar"b'22"), 5361 Bop(And,Mop(Not,bVar"b'21"), 5362 Bop(And, 5363 Mop(Not,bVar"b'14"), 5364 Mop(Not,bVar"b'12")))))))), 5365 Let(Var("Rn",F4), 5366 Mop(Cast F4, 5367 LL[bVar"b'19",bVar"b'18",bVar"b'17", 5368 bVar"b'16"]), 5369 Let(Var("SYSm",F8), 5370 Mop(Cast F8, 5371 LL[bVar"b'7",bVar"b'6",bVar"b'5", 5372 bVar"b'4",bVar"b'3",bVar"b'2", 5373 bVar"b'1",bVar"b'0"]), 5374 TP[Call 5375 ("System",CTy"instruction", 5376 Call 5377 ("MoveToSpecialRegister", 5378 CTy"System", 5379 TP[Var("SYSm",F8),Var("Rn",F4)])), 5380 ITE(Bop(Or, 5381 Bop(In,Var("Rn",F4), 5382 SL[LW(13,4),LW(15,4)]), 5383 Mop(Not, 5384 Bop(In,Var("SYSm",F8), 5385 SL[LW(0,8),LW(1,8), 5386 LW(2,8),LW(3,8), 5387 LW(5,8),LW(6,8), 5388 LW(7,8),LW(8,8), 5389 LW(9,8),LW(16,8), 5390 LW(17,8),LW(18,8), 5391 LW(19,8),LW(20,8)]))), 5392 Apply 5393 (Call 5394 ("DECODE_UNPREDICTABLE", 5395 ATy(qTy,qTy), 5396 TP[Var("mc",CTy"MachineCode"), 5397 LS"MoveToSpecialRegister"]), 5398 qVar"state"),qVar"state")]))), 5399 (Bop(And,Mop(Not,bVar"b'26"), 5400 Bop(And,bVar"b'25", 5401 Bop(And,bVar"b'24", 5402 Bop(And,bVar"b'23", 5403 Bop(And,Mop(Not,bVar"b'22"), 5404 Bop(And,bVar"b'21", 5405 Bop(And,bVar"b'20", 5406 Bop(And, 5407 Mop(Not,bVar"b'14"), 5408 Mop(Not,bVar"b'12"))))))))), 5409 Let(Var("option",F4), 5410 Mop(Cast F4, 5411 LL[bVar"b'3",bVar"b'2",bVar"b'1",bVar"b'0"]), 5412 TP[CS(Mop(Cast F4, 5413 LL[bVar"b'7",bVar"b'6",bVar"b'5", 5414 bVar"b'4"]), 5415 [(LW(4,4), 5416 Call 5417 ("Hint",CTy"instruction", 5418 Call 5419 ("DataSynchronizationBarrier", 5420 CTy"Hint",Var("option",F4)))), 5421 (LW(5,4), 5422 Call 5423 ("Hint",CTy"instruction", 5424 Call 5425 ("DataMemoryBarrier",CTy"Hint", 5426 Var("option",F4)))), 5427 (LW(6,4), 5428 Call 5429 ("Hint",CTy"instruction", 5430 Call 5431 ("InstructionSynchronizationBarrier", 5432 CTy"Hint",Var("option",F4)))), 5433 (AVar F4, 5434 Call 5435 ("Undefined",CTy"instruction", 5436 LW(0,32)))]),qVar"state"])), 5437 (Bop(And,Mop(Not,bVar"b'26"), 5438 Bop(And,bVar"b'25", 5439 Bop(And,bVar"b'24", 5440 Bop(And,bVar"b'23", 5441 Bop(And,bVar"b'22", 5442 Bop(And,bVar"b'21", 5443 Bop(And, 5444 Mop(Not,bVar"b'14"), 5445 Mop(Not,bVar"b'12")))))))), 5446 Let(Var("SYSm",F8), 5447 Mop(Cast F8, 5448 LL[bVar"b'7",bVar"b'6",bVar"b'5", 5449 bVar"b'4",bVar"b'3",bVar"b'2", 5450 bVar"b'1",bVar"b'0"]), 5451 Let(Var("Rd",F4), 5452 Mop(Cast F4, 5453 LL[bVar"b'11",bVar"b'10",bVar"b'9", 5454 bVar"b'8"]), 5455 TP[Call 5456 ("System",CTy"instruction", 5457 Call 5458 ("MoveToRegisterFromSpecial", 5459 CTy"System", 5460 TP[Var("SYSm",F8),Var("Rd",F4)])), 5461 ITE(Bop(Or, 5462 Bop(In,Var("Rd",F4), 5463 SL[LW(13,4),LW(15,4)]), 5464 Mop(Not, 5465 Bop(In,Var("SYSm",F8), 5466 SL[LW(0,8),LW(1,8), 5467 LW(2,8),LW(3,8), 5468 LW(5,8),LW(6,8), 5469 LW(7,8),LW(8,8), 5470 LW(9,8),LW(16,8), 5471 LW(17,8),LW(18,8), 5472 LW(19,8),LW(20,8)]))), 5473 Apply 5474 (Call 5475 ("DECODE_UNPREDICTABLE", 5476 ATy(qTy,qTy), 5477 TP[Var("mc",CTy"MachineCode"), 5478 LS 5479 "MoveToRegisterFromSpecial"]), 5480 qVar"state"),qVar"state")]))), 5481 (Bop(And,bVar"b'26", 5482 Bop(And,bVar"b'25", 5483 Bop(And,bVar"b'24", 5484 Bop(And,bVar"b'23", 5485 Bop(And,bVar"b'22", 5486 Bop(And,bVar"b'21", 5487 Bop(And,bVar"b'20", 5488 Bop(And, 5489 Mop(Not,bVar"b'14"), 5490 Bop(And, 5491 bVar"b'13", 5492 Mop(Not, 5493 bVar"b'12")))))))))), 5494 TP[Call 5495 ("Undefined",CTy"instruction", 5496 Mop(Cast F32, 5497 CC[Mop(Cast F4, 5498 LL[bVar"b'19",bVar"b'18", 5499 bVar"b'17",bVar"b'16"]), 5500 Mop(Cast(FTy 12), 5501 LL[bVar"b'11",bVar"b'10", 5502 bVar"b'9",bVar"b'8",bVar"b'7", 5503 bVar"b'6",bVar"b'5",bVar"b'4", 5504 bVar"b'3",bVar"b'2",bVar"b'1", 5505 bVar"b'0"])])),qVar"state"]), 5506 (Bop(And,bVar"b'14",bVar"b'12"), 5507 Let(Var("S",F1),Mop(Cast F1,LL[bVar"b'26"]), 5508 TP[Call 5509 ("Branch",CTy"instruction", 5510 Call 5511 ("BranchLinkImmediate",CTy"Branch", 5512 Mop(SE F32, 5513 CC[Var("S",F1), 5514 Mop(BNot, 5515 Bop(BXor, 5516 Mop(Cast F1, 5517 LL[bVar"b'13"]), 5518 Var("S",F1))), 5519 Mop(BNot, 5520 Bop(BXor, 5521 Mop(Cast F1, 5522 LL[bVar"b'11"]), 5523 Var("S",F1))), 5524 Mop(Cast(FTy 10), 5525 LL[bVar"b'25",bVar"b'24", 5526 bVar"b'23",bVar"b'22", 5527 bVar"b'21",bVar"b'20", 5528 bVar"b'19",bVar"b'18", 5529 bVar"b'17",bVar"b'16"]), 5530 Mop(Cast(FTy 11), 5531 LL[bVar"b'10",bVar"b'9", 5532 bVar"b'8",bVar"b'7", 5533 bVar"b'6",bVar"b'5", 5534 bVar"b'4",bVar"b'3", 5535 bVar"b'2",bVar"b'1", 5536 bVar"b'0"]),LW(0,1)]))), 5537 qVar"state"]))], 5538 TP[Call("Undefined",CTy"instruction",LW(0,32)), 5539 qVar"state"]), 5540 TP[Call("Undefined",CTy"instruction",LW(0,32)), 5541 qVar"state"]))))) 5542; 5543val Decode_def = Def 5544 ("Decode",Var("mc",CTy"MachineCode"), 5545 Close 5546 (qVar"state", 5547 CS(Var("mc",CTy"MachineCode"), 5548 [(Call("Thumb",CTy"MachineCode",Var("h",F16)), 5549 Apply 5550 (Call 5551 ("DecodeThumb",ATy(qTy,PTy(CTy"instruction",qTy)), 5552 Var("h",F16)),Rupd("pcinc",TP[qVar"state",LW(2,32)]))), 5553 (Call("Thumb2",CTy"MachineCode",Var("hs",PTy(F16,F16))), 5554 Apply 5555 (Call 5556 ("DecodeThumb2",ATy(qTy,PTy(CTy"instruction",qTy)), 5557 Var("hs",PTy(F16,F16))), 5558 Rupd("pcinc",TP[qVar"state",LW(4,32)])))]))) 5559; 5560val Next_def = Def 5561 ("Next",qVar"state", 5562 Let(TP[Var("v",CTy"MachineCode"),qVar"s"], 5563 Apply 5564 (Const("Fetch",ATy(qTy,PTy(CTy"MachineCode",qTy))),qVar"state"), 5565 Let(TP[Var("v",CTy"instruction"),qVar"s"], 5566 Apply 5567 (Call 5568 ("Decode",ATy(qTy,PTy(CTy"instruction",qTy)), 5569 Var("v",CTy"MachineCode")),qVar"s"), 5570 Apply 5571 (Call("Run",ATy(qTy,qTy),Var("v",CTy"instruction")),qVar"s")))) 5572 5573val () = Import.finish 0