1/* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 */ 6typedef 7unsigned 8size_t 9; 10typedef 11int 12ptrdiff_t 13; 14typedef 15unsigned 16wchar_t 17; 18typedef 19signed 20char 21int8_t 22; 23typedef 24short 25int16_t 26; 27typedef 28int 29int32_t 30; 31typedef 32long 33long 34int64_t 35; 36typedef 37unsigned 38char 39uint8_t 40; 41typedef 42unsigned 43short 44uint16_t 45; 46typedef 47unsigned 48int 49uint32_t 50; 51typedef 52unsigned 53long 54long 55uint64_t 56; 57typedef 58int8_t 59int_fast8_t 60; 61typedef 62int 63int_fast16_t 64; 65typedef 66int 67int_fast32_t 68; 69typedef 70int64_t 71int_fast64_t 72; 73typedef 74unsigned 75char 76uint_fast8_t 77; 78typedef 79unsigned 80int 81uint_fast16_t 82; 83typedef 84unsigned 85int 86uint_fast32_t 87; 88typedef 89uint64_t 90uint_fast64_t 91; 92typedef 93long 94intptr_t 95; 96typedef 97unsigned 98long 99uintptr_t 100; 101typedef 102int8_t 103int_least8_t 104; 105typedef 106int16_t 107int_least16_t 108; 109typedef 110int32_t 111int_least32_t 112; 113typedef 114int64_t 115int_least64_t 116; 117typedef 118uint8_t 119uint_least8_t 120; 121typedef 122uint16_t 123uint_least16_t 124; 125typedef 126uint32_t 127uint_least32_t 128; 129typedef 130uint64_t 131uint_least64_t 132; 133typedef 134long 135long 136intmax_t 137; 138typedef 139unsigned 140long 141long 142uintmax_t 143; 144typedef 145uint32_t 146seL4_Word 147; 148typedef 149seL4_Word 150seL4_CPtr 151; 152typedef 153seL4_CPtr 154seL4_ARM_Page 155; 156typedef 157seL4_CPtr 158seL4_ARM_PageTable 159; 160typedef 161seL4_CPtr 162seL4_ARM_PageDirectory 163; 164typedef 165seL4_CPtr 166seL4_ARM_ASIDControl 167; 168typedef 169seL4_CPtr 170seL4_ARM_ASIDPool 171; 172typedef 173struct 174{ 175/* frame registers */ 176seL4_Word 177pc 178, 179sp 180, 181cpsr 182, 183r0 184, 185r1 186, 187r8 188, 189r9 190, 191r10 192, 193r11 194, 195r12 196; 197/* other integer registers */ 198seL4_Word 199r2 200, 201r3 202, 203r4 204, 205r5 206, 207r6 208, 209r7 210, 211r14 212; 213} 214seL4_UserContext 215; 216typedef 217enum 218{ 219seL4_ARM_PageCacheable 220= 2210x01 222, 223seL4_ARM_ParityEnabled 224= 2250x02 226, 227seL4_ARM_Default_VMAttributes 228= 2290x03 230, 231/* seL4_ARM_PageCacheable | seL4_ARM_ParityEnabled */ 232_enum_pad_seL4_ARM_VMAttributes 233= 234( 2351U 236<< 237( 238( 239sizeof 240( 241int 242) 243* 2448 245) 246- 2471 248) 249) 250, 251} 252seL4_ARM_VMAttributes 253; 254struct 255seL4_MessageInfo 256{ 257uint32_t 258words 259[ 2601 261] 262; 263} 264; 265typedef 266struct 267seL4_MessageInfo 268seL4_MessageInfo_t 269; 270struct 271seL4_CapData 272{ 273uint32_t 274words 275[ 2761 277] 278; 279} 280; 281typedef 282struct 283seL4_CapData 284seL4_CapData_t 285; 286enum 287seL4_CapData_tag 288{ 289seL4_CapData_Badge 290= 2910 292, 293seL4_CapData_Guard 294= 2951 296} 297; 298typedef 299enum 300seL4_CapData_tag 301seL4_CapData_tag_t 302; 303typedef 304enum 305{ 306seL4_SysCall 307= 308- 3091 310, 311seL4_SysReplyWait 312= 313- 3142 315, 316seL4_SysSend 317= 318- 3193 320, 321seL4_SysNBSend 322= 323- 3244 325, 326seL4_SysWait 327= 328- 3295 330, 331seL4_SysReply 332= 333- 3346 335, 336seL4_SysYield 337= 338- 3397 340, 341seL4_SysPoll 342= 343- 3448 345, 346seL4_SysDebugPutChar 347= 348- 3499 350, 351seL4_SysDebugHalt 352= 353- 35410 355, 356seL4_SysDebugCapIdentify 357= 358- 35911 360, 361seL4_SysDebugSnapshot 362= 363- 36412 365, 366_enum_pad_seL4_Syscall_ID 367= 368( 3691U 370<< 371( 372( 373sizeof 374( 375int 376) 377* 3788 379) 380- 3811 382) 383) 384} 385seL4_Syscall_ID 386; 387typedef 388enum 389api_object 390{ 391seL4_UntypedObject 392, 393seL4_TCBObject 394, 395seL4_EndpointObject 396, 397seL4_NotificationObject 398, 399seL4_CapTableObject 400, 401seL4_NonArchObjectTypeCount 402, 403} 404seL4_ObjectType 405; 406typedef 407uint32_t 408api_object_t 409; 410typedef 411enum 412{ 413seL4_NoError 414= 4150 416, 417seL4_InvalidArgument 418, 419seL4_InvalidCapability 420, 421seL4_IllegalOperation 422, 423seL4_RangeError 424, 425seL4_AlignmentError 426, 427seL4_FailedLookup 428, 429seL4_TruncatedMessage 430, 431seL4_DeleteFirst 432, 433seL4_RevokeFirst 434, 435seL4_NotEnoughMemory 436, 437} 438seL4_Error 439; 440enum 441priorityConstants 442{ 443seL4_InvalidPrio 444= 445- 4461 447, 448seL4_MinPrio 449= 4500 451, 452seL4_MaxPrio 453= 454255 455} 456; 457enum 458seL4_MsgLimits 459{ 460seL4_MsgLengthBits 461= 4627 463, 464seL4_MsgExtraCapBits 465= 4662 467} 468; 469typedef 470enum 471{ 472seL4_NoFault 473= 4740 475, 476seL4_CapFault 477, 478seL4_VMFault 479, 480seL4_UnknownSyscall 481, 482seL4_UserException 483, 484_enum_pad_seL4_FaultType 485= 486( 4871U 488<< 489( 490( 491sizeof 492( 493int 494) 495* 4968 497) 498- 4991 500) 501) 502, 503} 504seL4_FaultType 505; 506typedef 507enum 508{ 509seL4_NoFailure 510= 5110 512, 513seL4_InvalidRoot 514, 515seL4_MissingCapability 516, 517seL4_DepthMismatch 518, 519seL4_GuardMismatch 520, 521_enum_pad_seL4_LookupFailureType 522= 523( 5241U 525<< 526( 527( 528sizeof 529( 530int 531) 532* 5338 534) 535- 5361 537) 538) 539, 540} 541seL4_LookupFailureType 542; 543typedef 544enum 545{ 546seL4_CanWrite 547= 5480x01 549, 550seL4_CanRead 551= 5520x02 553, 554seL4_CanGrant 555= 5560x04 557, 558seL4_AllRights 559= 5600x07 561, 562/* seL4_CanWrite | seL4_CanRead | seL4_CanGrant */ 563seL4_Transfer_Mint 564= 5650x100 566, 567_enum_pad_seL4_CapRights 568= 569( 5701U 571<< 572( 573( 574sizeof 575( 576int 577) 578* 5798 580) 581- 5821 583) 584) 585, 586} 587seL4_CapRights 588; 589typedef 590struct 591seL4_IPCBuffer_ 592{ 593seL4_MessageInfo_t 594tag 595; 596seL4_Word 597msg 598[ 599120 600] 601; 602seL4_Word 603userData 604; 605seL4_Word 606caps_or_badges 607[ 608( 609( 6101ul 611<< 612( 613seL4_MsgExtraCapBits 614) 615) 616- 6171 618) 619] 620; 621seL4_CPtr 622receiveCNode 623; 624seL4_CPtr 625receiveIndex 626; 627seL4_Word 628receiveDepth 629; 630} 631seL4_IPCBuffer 632; typedef 633seL4_CPtr 634seL4_CNode 635; 636typedef 637seL4_CPtr 638seL4_IRQHandler 639; 640typedef 641seL4_CPtr 642seL4_IRQControl 643; 644typedef 645seL4_CPtr 646seL4_TCB 647; 648typedef 649seL4_CPtr 650seL4_Untyped 651; 652typedef 653seL4_CPtr 654seL4_DomainSet 655; 656typedef 657enum 658_object 659{ 660seL4_ARM_SmallPageObject 661= 662seL4_NonArchObjectTypeCount 663, 664seL4_ARM_LargePageObject 665, 666seL4_ARM_SectionObject 667, 668seL4_ARM_SuperSectionObject 669, 670seL4_ARM_PageTableObject 671, 672seL4_ARM_PageDirectoryObject 673, 674seL4_ObjectTypeCount 675} 676seL4_ArchObjectType 677; 678typedef 679uint32_t 680object_t 681; 682enum 683invocation_label 684{ 685InvalidInvocation 686, 687UntypedRetype 688, 689TCBReadRegisters 690, 691TCBWriteRegisters 692, 693TCBCopyRegisters 694, 695TCBConfigure 696, 697TCBSetPriority 698, 699TCBSetIPCBuffer 700, 701TCBSetSpace 702, 703TCBSuspend 704, 705TCBResume 706, 707TCBBindNotification 708, 709TCBUnbindNotification 710, 711CNodeRevoke 712, 713CNodeDelete 714, 715CNodeRecycle 716, 717CNodeCopy 718, 719CNodeMint 720, 721CNodeMove 722, 723CNodeMutate 724, 725CNodeRotate 726, 727CNodeSaveCaller 728, 729IRQIssueIRQHandler 730, 731IRQInterruptControl 732, 733IRQAckIRQ 734, 735IRQSetIRQHandler 736, 737IRQClearIRQHandler 738, 739DomainSetSet 740, 741nInvocationLabels 742} 743; 744enum 745arch_invocation_label 746{ 747ARMPDClean_Data 748= 749nInvocationLabels 750+ 7510 752, 753ARMPDInvalidate_Data 754= 755nInvocationLabels 756+ 7571 758, 759ARMPDCleanInvalidate_Data 760= 761nInvocationLabels 762+ 7632 764, 765ARMPDUnify_Instruction 766= 767nInvocationLabels 768+ 7693 770, 771ARMPageTableMap 772= 773nInvocationLabels 774+ 7754 776, 777ARMPageTableUnmap 778= 779nInvocationLabels 780+ 7815 782, 783ARMPageMap 784= 785nInvocationLabels 786+ 7876 788, 789ARMPageRemap 790= 791nInvocationLabels 792+ 7937 794, 795ARMPageUnmap 796= 797nInvocationLabels 798+ 7998 800, 801ARMPageClean_Data 802= 803nInvocationLabels 804+ 8059 806, 807ARMPageInvalidate_Data 808= 809nInvocationLabels 810+ 81110 812, 813ARMPageCleanInvalidate_Data 814= 815nInvocationLabels 816+ 81711 818, 819ARMPageUnify_Instruction 820= 821nInvocationLabels 822+ 82312 824, 825ARMPageGetAddress 826= 827nInvocationLabels 828+ 82913 830, 831ARMASIDControlMakePool 832= 833nInvocationLabels 834+ 83514 836, 837ARMASIDPoolAssign 838= 839nInvocationLabels 840+ 84115 842, 843nArchInvocationLabels 844} 845; 846enum 847{ 848seL4_GlobalsFrame 849= 8500xffffc000 851, 852} 853; 854static 855inline 856seL4_IPCBuffer 857* 858seL4_GetIPCBuffer 859( 860void 861) 862{ 863return 864* 865( 866seL4_IPCBuffer 867* 868* 869) 870seL4_GlobalsFrame 871; 872} 873static 874inline 875void 876seL4_SetMR 877( 878int 879i 880, 881seL4_Word 882mr 883) 884{ 885seL4_GetIPCBuffer 886( 887) 888-> 889msg 890[ 891i 892] 893= 894mr 895; 896} 897static 898inline 899seL4_MessageInfo_t 900seL4_Wait 901( 902seL4_CPtr 903src 904, 905seL4_Word 906* 907sender 908) 909{ 910register 911seL4_Word 912src_and_badge 913asm 914( 915"r0" 916) 917= 918( 919seL4_Word 920) 921src 922; 923register 924seL4_MessageInfo_t 925info 926asm 927( 928"r1" 929) 930; 931/* Incoming message registers. */ 932register 933seL4_Word 934msg0 935asm 936( 937"r2" 938) 939; 940register 941seL4_Word 942msg1 943asm 944( 945"r3" 946) 947; 948register 949seL4_Word 950msg2 951asm 952( 953"r4" 954) 955; 956register 957seL4_Word 958msg3 959asm 960( 961"r5" 962) 963; 964/* Perform the system call. */ 965register 966seL4_Word 967scno 968asm 969( 970"r7" 971) 972= 973seL4_SysWait 974; 975asm 976volatile 977( 978"swi %[swi_num]" 979: 980"=r" 981( 982msg0 983) 984, 985"=r" 986( 987msg1 988) 989, 990"=r" 991( 992msg2 993) 994, 995"=r" 996( 997msg3 998) 999, 1000"=r" 1001( 1002info 1003) 1004, 1005"+r" 1006( 1007src_and_badge 1008) 1009: 1010[ 1011swi_num 1012] 1013"i" 1014( 1015( 1016seL4_SysWait 1017) 1018& 10190x00ffffff 1020) 1021, 1022"r" 1023( 1024scno 1025) 1026: 1027"memory" 1028) 1029; 1030/* Write the message back out to memory. */ 1031seL4_SetMR 1032( 10330 1034, 1035msg0 1036) 1037; 1038seL4_SetMR 1039( 10401 1041, 1042msg1 1043) 1044; 1045seL4_SetMR 1046( 10472 1048, 1049msg2 1050) 1051; 1052seL4_SetMR 1053( 10543 1055, 1056msg3 1057) 1058; 1059/* Return back sender and message information. */ 1060if 1061( 1062sender 1063) 1064{ 1065* 1066sender 1067= 1068src_and_badge 1069; 1070} 1071return 1072info 1073; 1074} 1075static 1076inline 1077seL4_MessageInfo_t 1078seL4_Poll 1079( 1080seL4_CPtr 1081src 1082, 1083seL4_Word 1084* 1085sender 1086) 1087{ 1088register 1089seL4_Word 1090src_and_badge 1091asm 1092( 1093"r0" 1094) 1095= 1096( 1097seL4_Word 1098) 1099src 1100; 1101register 1102seL4_MessageInfo_t 1103info 1104asm 1105( 1106"r1" 1107) 1108; 1109/* Incoming message registers. */ 1110register 1111seL4_Word 1112msg0 1113asm 1114( 1115"r2" 1116) 1117; 1118register 1119seL4_Word 1120msg1 1121asm 1122( 1123"r3" 1124) 1125; 1126register 1127seL4_Word 1128msg2 1129asm 1130( 1131"r4" 1132) 1133; 1134register 1135seL4_Word 1136msg3 1137asm 1138( 1139"r5" 1140) 1141; 1142/* Perform the system call. */ 1143register 1144seL4_Word 1145scno 1146asm 1147( 1148"r7" 1149) 1150= 1151seL4_SysPoll 1152; 1153asm 1154volatile 1155( 1156"swi %[swi_num]" 1157: 1158"=r" 1159( 1160msg0 1161) 1162, 1163"=r" 1164( 1165msg1 1166) 1167, 1168"=r" 1169( 1170msg2 1171) 1172, 1173"=r" 1174( 1175msg3 1176) 1177, 1178"=r" 1179( 1180info 1181) 1182, 1183"+r" 1184( 1185src_and_badge 1186) 1187: 1188[ 1189swi_num 1190] 1191"i" 1192( 1193( 1194seL4_SysPoll 1195) 1196& 11970x00ffffff 1198) 1199, 1200"r" 1201( 1202scno 1203) 1204: 1205"memory" 1206) 1207; 1208/* Write the message back out to memory. */ 1209seL4_SetMR 1210( 12110 1212, 1213msg0 1214) 1215; 1216seL4_SetMR 1217( 12181 1219, 1220msg1 1221) 1222; 1223seL4_SetMR 1224( 12252 1226, 1227msg2 1228) 1229; 1230seL4_SetMR 1231( 12323 1233, 1234msg3 1235) 1236; 1237/* Return back sender and message information. */ 1238if 1239( 1240sender 1241) 1242{ 1243* 1244sender 1245= 1246src_and_badge 1247; 1248} 1249return 1250info 1251; 1252} 1253typedef 1254unsigned 1255long 1256__type_uint8_t_size_incorrect 1257[ 1258( 1259sizeof 1260( 1261uint8_t 1262) 1263== 12641 1265) 1266? 12671 1268: 1269- 12701 1271] 1272; 1273typedef 1274unsigned 1275long 1276__type_uint16_t_size_incorrect 1277[ 1278( 1279sizeof 1280( 1281uint16_t 1282) 1283== 12842 1285) 1286? 12871 1288: 1289- 12901 1291] 1292; 1293typedef 1294unsigned 1295long 1296__type_uint32_t_size_incorrect 1297[ 1298( 1299sizeof 1300( 1301uint32_t 1302) 1303== 13044 1305) 1306? 13071 1308: 1309- 13101 1311] 1312; 1313typedef 1314unsigned 1315long 1316__type_uint64_t_size_incorrect 1317[ 1318( 1319sizeof 1320( 1321uint64_t 1322) 1323== 13248 1325) 1326? 13271 1328: 1329- 13301 1331] 1332; 1333typedef 1334unsigned 1335long 1336__type_int_size_incorrect 1337[ 1338( 1339sizeof 1340( 1341int 1342) 1343== 13444 1345) 1346? 13471 1348: 1349- 13501 1351] 1352; 1353typedef 1354unsigned 1355long 1356__type_bool_size_incorrect 1357[ 1358( 1359sizeof 1360( 1361_Bool 1362) 1363== 13641 1365) 1366? 13671 1368: 1369- 13701 1371] 1372; 1373typedef 1374unsigned 1375long 1376__type_seL4_Word_size_incorrect 1377[ 1378( 1379sizeof 1380( 1381seL4_Word 1382) 1383== 13844 1385) 1386? 13871 1388: 1389- 13901 1391] 1392; 1393typedef 1394unsigned 1395long 1396__type_seL4_CapRights_size_incorrect 1397[ 1398( 1399sizeof 1400( 1401seL4_CapRights 1402) 1403== 14044 1405) 1406? 14071 1408: 1409- 14101 1411] 1412; 1413typedef 1414unsigned 1415long 1416__type_seL4_CapData_t_size_incorrect 1417[ 1418( 1419sizeof 1420( 1421seL4_CapData_t 1422) 1423== 14244 1425) 1426? 14271 1428: 1429- 14301 1431] 1432; 1433typedef 1434unsigned 1435long 1436__type_seL4_CPtr_size_incorrect 1437[ 1438( 1439sizeof 1440( 1441seL4_CPtr 1442) 1443== 14444 1445) 1446? 14471 1448: 1449- 14501 1451] 1452; 1453typedef 1454unsigned 1455long 1456__type_seL4_CNode_size_incorrect 1457[ 1458( 1459sizeof 1460( 1461seL4_CNode 1462) 1463== 14644 1465) 1466? 14671 1468: 1469- 14701 1471] 1472; 1473typedef 1474unsigned 1475long 1476__type_seL4_IRQHandler_size_incorrect 1477[ 1478( 1479sizeof 1480( 1481seL4_IRQHandler 1482) 1483== 14844 1485) 1486? 14871 1488: 1489- 14901 1491] 1492; 1493typedef 1494unsigned 1495long 1496__type_seL4_IRQControl_size_incorrect 1497[ 1498( 1499sizeof 1500( 1501seL4_IRQControl 1502) 1503== 15044 1505) 1506? 15071 1508: 1509- 15101 1511] 1512; 1513typedef 1514unsigned 1515long 1516__type_seL4_TCB_size_incorrect 1517[ 1518( 1519sizeof 1520( 1521seL4_TCB 1522) 1523== 15244 1525) 1526? 15271 1528: 1529- 15301 1531] 1532; 1533typedef 1534unsigned 1535long 1536__type_seL4_Untyped_size_incorrect 1537[ 1538( 1539sizeof 1540( 1541seL4_Untyped 1542) 1543== 15444 1545) 1546? 15471 1548: 1549- 15501 1551] 1552; 1553typedef 1554unsigned 1555long 1556__type_seL4_DomainSet_size_incorrect 1557[ 1558( 1559sizeof 1560( 1561seL4_DomainSet 1562) 1563== 15644 1565) 1566? 15671 1568: 1569- 15701 1571] 1572; 1573typedef 1574unsigned 1575long 1576__type_seL4_ARM_VMAttributes_size_incorrect 1577[ 1578( 1579sizeof 1580( 1581seL4_ARM_VMAttributes 1582) 1583== 15844 1585) 1586? 15871 1588: 1589- 15901 1591] 1592; 1593typedef 1594unsigned 1595long 1596__type_seL4_ARM_Page_size_incorrect 1597[ 1598( 1599sizeof 1600( 1601seL4_ARM_Page 1602) 1603== 16044 1605) 1606? 16071 1608: 1609- 16101 1611] 1612; 1613typedef 1614unsigned 1615long 1616__type_seL4_ARM_PageTable_size_incorrect 1617[ 1618( 1619sizeof 1620( 1621seL4_ARM_PageTable 1622) 1623== 16244 1625) 1626? 16271 1628: 1629- 16301 1631] 1632; 1633typedef 1634unsigned 1635long 1636__type_seL4_ARM_PageDirectory_size_incorrect 1637[ 1638( 1639sizeof 1640( 1641seL4_ARM_PageDirectory 1642) 1643== 16444 1645) 1646? 16471 1648: 1649- 16501 1651] 1652; 1653typedef 1654unsigned 1655long 1656__type_seL4_ARM_ASIDControl_size_incorrect 1657[ 1658( 1659sizeof 1660( 1661seL4_ARM_ASIDControl 1662) 1663== 16644 1665) 1666? 16671 1668: 1669- 16701 1671] 1672; 1673typedef 1674unsigned 1675long 1676__type_seL4_ARM_ASIDPool_size_incorrect 1677[ 1678( 1679sizeof 1680( 1681seL4_ARM_ASIDPool 1682) 1683== 16844 1685) 1686? 16871 1688: 1689- 16901 1691] 1692; 1693typedef 1694unsigned 1695long 1696__type_seL4_UserContext_size_incorrect 1697[ 1698( 1699sizeof 1700( 1701seL4_UserContext 1702) 1703== 170468 1705) 1706? 17071 1708: 1709- 17101 1711] 1712; 1713struct 1714seL4_ARM_Page_GetAddress 1715{ 1716int 1717error 1718; 1719seL4_Word 1720paddr 1721; 1722} 1723; 1724typedef 1725struct 1726seL4_ARM_Page_GetAddress 1727seL4_ARM_Page_GetAddress_t 1728; 1729enum 1730{ 1731seL4_CapNull 1732= 17330 1734, 1735/* null cap */ 1736seL4_CapInitThreadTCB 1737= 17381 1739, 1740/* initial thread's TCB cap */ 1741seL4_CapInitThreadCNode 1742= 17432 1744, 1745/* initial thread's root CNode cap */ 1746seL4_CapInitThreadPD 1747= 17483 1749, 1750/* initial thread's PD cap */ 1751seL4_CapIRQControl 1752= 17534 1754, 1755/* global IRQ controller cap */ 1756seL4_CapASIDControl 1757= 17585 1759, 1760/* global ASID controller cap */ 1761seL4_CapInitThreadASIDPool 1762= 17636 1764, 1765/* initial thread's ASID pool cap */ 1766seL4_CapIOPort 1767= 17687 1769, 1770/* global IO port cap (null cap if not supported) */ 1771seL4_CapIOSpace 1772= 17738 1774, 1775/* global IO space cap (null cap if no IOMMU support) */ 1776seL4_CapBootInfoFrame 1777= 17789 1779, 1780/* bootinfo frame cap */ 1781seL4_CapInitThreadIPCBuffer 1782= 178310 1784, 1785/* initial thread's IPC buffer frame cap */ 1786seL4_CapDomain 1787= 178811 1789/* global domain controller cap */ 1790} 1791; 1792typedef 1793struct 1794{ 1795seL4_Word 1796start 1797; 1798/* first CNode slot position OF region */ 1799seL4_Word 1800end 1801; 1802/* first CNode slot position AFTER region */ 1803} 1804seL4_SlotRegion 1805; 1806typedef 1807struct 1808{ 1809seL4_Word 1810basePaddr 1811; 1812/* base physical address of device region */ 1813seL4_Word 1814frameSizeBits 1815; 1816/* size (2^n bytes) of a device-region frame */ 1817seL4_SlotRegion 1818frames 1819; 1820/* device-region frame caps */ 1821} 1822seL4_DeviceRegion 1823; 1824typedef 1825struct 1826{ 1827seL4_Word 1828nodeID 1829; 1830/* ID [0..numNodes-1] of the seL4 node (0 if uniprocessor) */ 1831seL4_Word 1832numNodes 1833; 1834/* number of seL4 nodes (1 if uniprocessor) */ 1835seL4_Word 1836numIOPTLevels 1837; 1838/* number of IOMMU PT levels (0 if no IOMMU support) */ 1839seL4_IPCBuffer 1840* 1841ipcBuffer 1842; 1843/* pointer to initial thread's IPC buffer */ 1844seL4_SlotRegion 1845empty 1846; 1847/* empty slots (null caps) */ 1848seL4_SlotRegion 1849sharedFrames 1850; 1851/* shared-frame caps (shared between seL4 nodes) */ 1852seL4_SlotRegion 1853userImageFrames 1854; 1855/* userland-image frame caps */ 1856seL4_SlotRegion 1857userImagePTs 1858; 1859/* userland-image PT caps */ 1860seL4_SlotRegion 1861untyped 1862; 1863/* untyped-object caps (untyped caps) */ 1864seL4_Word 1865untypedPaddrList 1866[ 1867167 1868] 1869; 1870/* physical address of each untyped cap */ 1871uint8_t 1872untypedSizeBitsList 1873[ 1874167 1875] 1876; 1877/* size (2^n) bytes of each untyped cap */ 1878uint8_t 1879initThreadCNodeSizeBits 1880; 1881/* initial thread's root CNode size (2^n slots) */ 1882seL4_Word 1883numDeviceRegions 1884; 1885/* number of device regions */ 1886seL4_DeviceRegion 1887deviceRegions 1888[ 1889199 1890] 1891; 1892/* device regions */ 1893uint8_t 1894initThreadDomain 1895; 1896/* Initial thread's domain ID */ 1897} 1898seL4_BootInfo 1899; 1900typedef 1901struct 1902camkes_tls_t 1903{ 1904seL4_CPtr 1905tcb_cap 1906; 1907unsigned 1908int 1909thread_index 1910; 1911} 1912camkes_tls_t 1913; 1914static 1915inline 1916camkes_tls_t 1917* 1918__attribute__ 1919( 1920( 1921__unused__ 1922) 1923) 1924camkes_get_tls 1925( 1926void 1927) 1928{ 1929/* We store TLS data in the same page as the thread's IPC buffer, but at 1930 * the start of the page. 1931 */ 1932uintptr_t 1933ipc_buffer 1934= 1935( 1936uintptr_t 1937) 1938seL4_GetIPCBuffer 1939( 1940) 1941; 1942/* Normally we would just use MASK here, but the verification C parser 1943 * doesn't like the GCC extension used in that macro. 1944 */ 1945typedef 1946char 1947_assertion_failed__static_assert_0 1948[ 1949( 1950( 195112 1952<= 195331 1954) 1955) 1956? 19571 1958: 1959- 19601 1961] 1962__attribute__ 1963( 1964( 1965__unused__ 1966) 1967) 1968; 1969uintptr_t 1970tls 1971= 1972ipc_buffer 1973& 1974~ 1975( 1976( 1977( 19781ul 1979<< 1980( 198112 1982) 1983) 1984- 19851ul 1986) 1987) 1988; 1989/* We should have enough room for the TLS data preceding the IPC buffer. */ 1990( 1991( 1992void 1993) 19940 1995) 1996; 1997/* We'd better be returning a valid pointer. */ 1998( 1999( 2000void 2001) 20020 2003) 2004; 2005return 2006( 2007camkes_tls_t 2008* 2009) 2010tls 2011; 2012} 2013void 2014abort 2015( 2016void 2017) 2018; 2019typedef 2020struct 2021{ 2022int 2023quot 2024, 2025rem 2026; 2027} 2028div_t 2029; 2030typedef 2031struct 2032{ 2033long 2034quot 2035, 2036rem 2037; 2038} 2039ldiv_t 2040; 2041typedef 2042struct 2043{ 2044long 2045long 2046quot 2047, 2048rem 2049; 2050} 2051lldiv_t 2052; 2053int 2054EventTo__run 2055( 2056void 2057) 2058{ 2059return 20600 2061; 2062} 2063static 2064seL4_Word 2065badge_1 2066; 2067static 2068seL4_Word 2069badge_2 2070; 2071static 2072seL4_Word 2073* 2074__attribute__ 2075( 2076( 2077unused 2078) 2079) 2080get_badge 2081( 2082void 2083) 2084{ 2085switch 2086( 2087camkes_get_tls 2088( 2089) 2090-> 2091thread_index 2092) 2093{ 2094case 20951 2096: 2097return 2098& 2099badge_1 2100; 2101case 21022 2103: 2104return 2105& 2106badge_2 2107; 2108default 2109: 2110( 2111( 2112void 2113) 21140 2115) 2116; 2117abort 2118( 2119) 2120; 2121} 2122} 2123int 2124EventTo_poll 2125( 2126void 2127) 2128{ 2129seL4_Word 2130* 2131badge 2132= 2133get_badge 2134( 2135) 2136; 2137seL4_Poll 2138( 21396 2140, 2141badge 2142) 2143; 2144return 2145* 2146badge 2147== 2148195894762 2149; 2150} 2151void 2152EventTo_wait 2153( 2154void 2155) 2156{ 2157seL4_Wait 2158( 21596 2160, 2161( 2162( 2163void 2164* 2165) 21660 2167) 2168) 2169; 2170} 2171