1case \x of 0 -> 1 -> _ -> ---> if \x = 0 2 then ->1 else if \x = 1 then ->2 else ->3 3 4case \x of nodeCap@(CNodeCap {}) -> _ -> ---> let nodeCap = \x in 5 if isCNodeCap nodeCap 6 then ->1 else ->2 7 8case \x of root@(CNodeCap {}) -> _ -> ---> let root = \x in 9 if isCNodeCap root 10 then ->1 else ->2 11 12case \x of rt@(CNodeCap {}) -> _ -> ---> let rt = \x in 13 if isCNodeCap rt 14 then ->1 else ->2 15 16case \x of cap@(EndpointCap { capEPCanSend = True }) -> cap@(NotificationCap { capNtfnCanSend = True }) -> cap -> ---> let cap = \x in 17 if isEndpointCap cap \<and> capEPCanSend cap 18 then ->1 else if isNotificationCap cap \<and> capNtfnCanSend cap 19 then ->2 else ->3 20 21case \x of EndpointCap { \v0\EPCanReceive = True } -> NotificationCap { \v0\NtfnCanReceive = True } -> _ -> ---> let \v0\ = \x in 22 if isEndpointCap \v0\ \<and> \v0\EPCanReceive \v0 23 then ->1 else if isNotificationCap \v0\ \<and> \v0\NtfnCanReceive \v0 24 then ->2 else ->3 25 26case \x of (_, _, cap@(ThreadCap {capTCBCanWrite = True})) -> (_, _, cap@(CNodeCap {})) -> (_, capIndex, cap@(UntypedCap {})) -> (blocking, capIndex, cap@(ArchObjectCap {})) -> (True, ptr, cap) -> (False, _, _) -> ---> let (blocking, capIndex, cap) = \x in if isThreadCap cap \<and> capTCBCanWrite cap 27 then ->1 else if isCNodeCap cap 28 then ->2 else if isUntypedCap cap 29 then ->3 else if isArchObjectCap cap 30 then ->4 else if blocking 31 then ->5 else ->6 32 33case \x of (index:bits:args, cap@(CNodeCap {capCNodeCanModify=True})) -> (_, CNodeCap {capCNodeCanModify=True}) -> (_, _) -> ---> let (\v0\, cap) = \x in 34 if length (\v0\) > 1 \<and> isCNodeCap cap \<and> capCNodeCanModify cap then let index = \v0\ !! 0; 35 bits = \v0\ !! 1; 36 args = drop 2 \v0 37 in ->1 else if isCNodeCap cap \<and> capCNodeCanModify cap then ->2 else ->3 38 39case \x of (_, _, cap@(ThreadCap {capTCBCanWrite = True})) -> (_, _, cap@(CNodeCap {capCNodeCanModify = True})) -> (_, capIndex, cap@(UntypedCap {})) -> (blocking, capIndex, cap@(ArchObjectCap {})) -> (True, ptr, cap) -> (False, _, _) -> ---> let (blocking, capIndex, cap) = \x in if isThreadCap cap \<and> capTCBCanWrite cap 40 then ->1 else if isCNodeCap cap \<and> capCNodeCanModify cap 41 then ->2 else if isUntypedCap cap 42 then ->3 else if isArchObjectCap cap 43 then ->4 else if blocking 44 then let ptr = capIndex in ->5 else ->6 45 46case \x of (capPtr, cap@(ThreadCap{capTCBCanWrite = True})) -> (_, cap@(CNodeCap {capCNodeCanModify = True})) -> (capIndex, cap@(UntypedCap {})) -> (capIndex, cap@(ArchObjectCap {})) -> (capPtr, cap) -> ---> let (capPtr, cap) = \x; capIndex = capPtr in 47 if isThreadCap cap \<and> capTCBCanWrite cap 48 then ->1 else if isCNodeCap cap \<and> capCNodeCanModify cap 49 then ->2 else if isUntypedCap cap 50 then ->3 else if isArchObjectCap cap 51 then ->4 else ->5 52 53case \x of (capPtr, cap@(ThreadCap{capTCBCanWrite = True})) -> (_, cap@(CNodeCap {capCNodeCanModify = True})) -> (_, cap@(UntypedCap {})) -> (capIndex, cap@(ArchObjectCap {})) -> (capPtr, cap) -> ---> let (capPtr, cap) = \x; capIndex = capPtr in 54 if isThreadCap cap \<and> capTCBCanWrite cap 55 then ->1 else if isCNodeCap cap \<and> capCNodeCanModify cap 56 then ->2 else if isUntypedCap cap 57 then ->3 else if isArchObjectCap cap 58 then ->4 else ->5 59 60case \x of Just (slot, 0, rights) -> _ -> ---> case \x of 61 Some \v0\ \<Rightarrow> let (slot, \v1\, rights) = \v0\ in 62 if \v1\ = 0 then ->1 else ->2 | None \<Rightarrow> ->2 63 64case \x of (slot, 0, rights) -> (_, bitsLeft, _) -> ---> let (slot, bitsLeft, rights) = \x in 65 if bitsLeft = 0 66 then ->1 else ->2 67 68case \x of (index:bits:args, cnode@(CNodeCap {})) -> (_, _) -> ---> let (L, cnode) = \x in 69 if isCNodeCap cnode \<and> length L > 1 then 70 let index = L !! 0; 71 bits = L !! 1; 72 args = drop 2 L 73 in ->1 else ->2 74 75case \x of (index:bits:args, cnode@(CNodeCap { capCNodeCanModify = True })) -> (_, CNodeCap { capCNodeCanModify = True }) -> (_, _) -> ---> let (L, cnode) = \x in 76 if isCNodeCap cnode \<and> capCNodeCanModify cnode then 77 if length L > 1 then 78 let index = L !! 0; 79 bits = L !! 1; 80 args = drop 2 L 81 in ->1 else ->2 else ->3 82 83case \x of (YieldToCall, _, thread) -> (call@(ThreadControlCall {}), faultep:replyep:priority:cRoot:cRootData:vRoot:vRootData:buffer:_, target) -> (call@(ExchangeRegistersCall {}), src:save:_, dest) -> (_, _, _) -> ---> let (call, L, \v0\) = \x in 84 if isYieldToCall call 85 then let thread = \v0\ in ->1 else if isThreadControlCall call \<and> length L > 6 86 then let target = \v0\; 87 faultep = L !! 0; 88 replyep = L !! 1; 89 priority = L !! 2; 90 cRoot = L !! 3; 91 cRootData = L !! 4; 92 vRoot = L !! 5; 93 vRootData = L !! 6; 94 buffer = L !! 7 95 in ->2 else if isExchangeRegistersCall call \<and> length L > 1 96 then let dest = \v0\; 97 src = L !! 0; 98 save = L !! 1 99 in ->3 else ->4 100 101case \x of (call@(ThreadControlCall{threadSetCRoot = True}), False) -> (call@(ThreadControlCall{threadSetVRoot = True}), False) -> (_,_) -> ---> let (call, \v0\) = \x in 102 if isThreadControlCall call \<and> threadSetCRoot call \<and> \<not> \v0 103 then ->1 else if isThreadControlCall call \<and> threadSetVRoot call \<and> \<not> \v0 104 then ->2 else ->3 105 106case \x of (call@(ThreadControlCall{threadSetCRoot = True}), False) -> (call@(ThreadControlCall{threadSetVRoot = True}), False) -> _ -> ---> let (call, \v0\) = \x in 107 if isThreadControlCall call \<and> threadSetCRoot call \<and> \<not> \v0 108 then ->1 else if isThreadControlCall call \<and> threadSetVRoot call \<and> \<not> \v0 109 then ->2 else ->3 110 111case \x of untypedCap@(UntypedCap {}) -> _ -> ---> let untypedCap = \x in 112 if isUntypedCap untypedCap 113 then ->1 114 else ->1 115 116case \x of ex2@(UserHandledFault {}) -> ex2 -> ---> let ex2 = \x in 117 if isUserHandledFault ex2 118 then ->1 else ->2 119 120case \x of 0 -> size -> ---> let size = \x in if size = 0 121 then ->1 else ->2 122 123case \x of 0 -> ctePtr -> ---> let ctePtr = \x in if ctePtr = 0 124 then ->1 else ->2 125 126case \x of (first:rest,_) -> ([], 0) -> ([], _) -> ---> let \v0\ = \x in case fst \v0\ of 127 first#rest \<Rightarrow> ->1 | [] \<Rightarrow> if snd \v0\ = 0 128 then ->2 else ->3 129 130case \x of Just x@(CNodeData {}) -> _ -> ---> let \v0\ = \x in 131 if \v0\ \<noteq> None \<and> isCNodeData (the \v0\) 132 then let x = the \v0\ in ->1 else ->2 133 134case \x of (Just new, EndpointData 0) -> (Just _, EndpointData _) -> (Just new, AsyncEndpointData 0) -> (Just _, AsyncEndpointData _) -> (Nothing, old@(CNodeData {})) -> (Just new, old@(CNodeData {})) -> (_, old) -> ---> let (\v0\, old) = \x; new = the \v0\; \v1\ = (\v0\ \<noteq> None) in 135 if \v1\ \<and> old = EndpointData 0 136 then ->1 else if \v1\ \<and> isEndpointData old 137 then ->2 else if \v1\ \<and> old = AsyncEndpointData 0 138 then ->3 else if \v1\ \<and> isAsyncEndpointData old 139 then ->4 else if (\<not> \v1\) \<and> isCNodeData old 140 then ->5 else if \v1\ \<and> isCNodeData old 141 then ->6 else ->7 142 143case \x of 0 -> slot -> ---> let slot = \x in 144 if slot = 0 then ->1 else ->2 145 146case \x of CTE { cteCap = UntypedCap {} } -> cte@(CTE { cteMDBNode = mdb }) -> ---> let cte = \x in 147 if isUntypedCap (cteCap cte) 148 then ->1 else let mdb = cteMDBNode cte 149 in ->2 150 151case \x of cap@(EndpointCap {}) -> _ -> ---> let cap = \x in 152 if isEndpointCap cap 153 then ->1 else ->2 154 155case \x of (a@UntypedCap {}, b@UntypedCap {}) -> (a@EndpointCap {}, b@EndpointCap {}) -> (a@NotificationCap {}, b@NotificationCap {}) -> (a@CNodeCap {}, b@CNodeCap {}) -> (a@ThreadCap {}, b@ThreadCap {}) -> (a@FrameCap {}, b@FrameCap {}) -> (ArchObjectCap a, ArchObjectCap b) -> (_, _) -> ---> let (a, b) = \x in 156 if isUntypedCap a \<and> isUntypedCap b 157 then ->1 else if isEndpointCap a \<and> isEndpointCap b 158 then ->2 else if isNotificationCap a \<and> isNotificationCap b 159 then ->3 else if isCNodeCap a \<and> isCNodeCap b 160 then ->4 else if isThreadCap a \<and> isThreadCap b 161 then ->5 else if isFrameCap a \<and> isFrameCap b 162 then ->6 else if isArchObjectCap a \<and> isArchObjectCap b 163 then let a = capCap a; b = capCap b in ->7 else ->8 164 165case \x of cap@(EndpointCap {capEPCanSend=True}) -> cap@(NotificationCap {capNtfnCanSend=True}) -> cap@(ThreadCap {capTCBCanWrite=True}) -> cap@(CNodeCap {capCNodeCanModify=True}) -> cap@(UntypedCap {}) -> cap@(ArchObjectCap {}) -> _ -> ---> let cap = \x in 166 if isEndpointCap cap \<and> capEPCanSend cap 167 then ->1 else if isNotificationCap cap \<and> capNtfnCanSend cap 168 then ->2 else if isThreadCap cap \<and> capTCBCanWrite cap 169 then ->3 else if isCNodeCap cap \<and> capCNodeCanModify cap 170 then ->4 else if isUntypedCap cap 171 then ->5 else if isArchObjectCap cap 172 then ->6 else ->7 173 174case \x of 0 -> 1 -> 2 -> _ -> ---> let \v0\ = \x in 175 if \v0\ = 0 then ->1 else if \v0\ = 1 then ->2 else if \v0\ = 2 then ->3 else ->4 176 177case \x of (CTE a@(UntypedCap {}) _, CTE b _) -> (CTE a mdbA, CTE b mdbB) -> ---> let (\v0\, \v1\) = \x in 178 case \v0\ of CTE a mdbA \<Rightarrow> ( 179 case \v1\ of CTE b mdbB \<Rightarrow> ( 180 if isUntypedCap a 181 then ->1 else ->2 )) 182 183case \x of EndpointCap { capEPBadge = 0 } -> NotificationCap { capNtfnBadge = 0 } -> EndpointCap {} -> (NotificationCap {}) -> _ -> ---> let \v0\ = \x in 184 if isEndpointCap \v0\ \<and> capEPBadge \v0\ = 0 185 then ->1 else if isNotificationCap \v0\ \<and> capNtfnBadge \v0\ = 0 186 then ->2 else if isEndpointCap \v0 187 then ->3 else if isNotificationCap \v0 188 then ->4 else ->5 189 190case \x of (EndpointCap { capEPPtr = ptr }, True, _) -> (NotificationCap { capNtfnPtr = ptr }, True, _) -> (cap@(CNodeCap {}), True, True) -> (ThreadCap { capTCBPtr = tcb }, True, True) -> (CNodeCap { capCNodePtr = cn }, True, False) -> (Zombie { zombieObject = Left (cn, n+1) }, _, False) -> (ThreadCap { capTCBPtr = tcb }, True, False) -> (Zombie { zombieObject = Right tcb }, True, False) -> (Zombie { zombieObject = Left (cn, n+1) }, _, True) -> (Zombie { zombieObject = Left (_, 0) }, True, _) -> (Zombie { zombieObject = Right tcb }, True, True) -> (ArchObjectCap { capCap = cap }, final, exposed) -> (FrameCap {}, _, _) -> (NullCap, _, _) -> (Zombie {}, False, _) -> (_, _, _) -> ---> let (\v0\, \v1\, \v2\) = \x in 191 if isEndpointCap \v0\ \<and> \v1 192 then let ptr = capEPPtr \v0 193 in ->1 else if isNotificationCap \v0\ \<and> \v1 194 then let ptr = capNtfnPtr \v0 195 in ->2 else if isCNodeCap \v0\ \<and> \v1\ \<and> \v2 196 then let cap = \v0 197 in ->3 else if isThreadCap \v0\ \<and> \v1\ \<and> \v2 198 then let tcb = capTCBPtr \v0 199 in ->4 else if isCNodeCap \v0\ \<and> \v1\ \<and> (\<not> \v2\) 200 then let cn = capCNodePtr \v0 201 in ->5 else if isZombie \v0\ \<and> (\<not> \v2\) \<and> (\<exists>cn n. zombieObject \v0\ = Left (cn, n + 1)) 202 then let (cn, \v3\) = theLeft (zombieObject \v0\); n = \v3\ - 1 203 in ->6 else if isThreadCap \v0\ \<and> \v1\ \<and> (\<not> \v2\) 204 then let tcb = capTCBPtr \v0 205 in ->7 else if isZombie \v0\ \<and> \v1\ \<and> (\<not> \v2\) \<and> isRight (zombieObject \v0\) 206 then let tcb = theRight (zombieObject \v0\) 207 in ->8 else if isZombie \v0\ \<and> \v2\ \<and> (\<exists>cn n. zombieObject \v0\ = Left (cn, n + 1)) 208 then let (cn, \v3\) = theLeft (zombieObject \v0\); n = \v3\ - 1 209 in ->9 else if isZombie \v0\ \<and> \v1\ \<and> (\<exists>\v3\. zombieObject \v0\ = Left (\v3\, 0)) 210 then ->10 else if isZombie \v0\ \<and> isRight (zombieObject \v0\) \<and> \v1\ \<and> \v2 211 then let tcb = theRight (zombieObject \v0\) 212 in ->11 else if isArchObjectCap \v0 213 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\) 214 in ->12 else if isFrameCap \v0 215 then ->13 else if isNullCap \v0 216 then ->14 else if isZombie \v0\ \<and> (\<not> \v1\) 217 then ->15 else ->16 218 219case \x of (new, cap@(EndpointCap {})) -> (new, cap@(NotificationCap {})) -> (w, cap@(CNodeCap {})) -> (w, ArchObjectCap { capCap = aoCap }) -> (_, cap) -> ---> let (new, cap) = \x; 220 w = new in 221 if isEndpointCap cap 222 then ->1 else if isNotificationCap cap 223 then ->2 else if isCNodeCap cap 224 then ->3 else if isArchObjectCap cap 225 then let aoCap = capCap cap 226 in ->4 else ->5 227 228case \x of cap@(EndpointCap { capEPCanSend = True }) -> _ -> ---> let cap = \x in 229 if isEndpointCap cap \<and> capEPCanSend cap 230 then ->1 else ->2 231 232case \x of (EndpointCap { capEPPtr = ptr }, True, _) -> (NotificationCap { capNtfnPtr = ptr }, True, _) -> (cap@(CNodeCap {}), True, exposed) -> (ThreadCap { capTCBPtr = tcb }, True, exposed) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, _, False) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, _, True) -> (Zombie { capNumber = 0 }, True, _) -> (ArchObjectCap { capCap = cap }, final, exposed) -> (FrameCap {}, _, _) -> (NullCap, _, _) -> (Zombie {}, False, _) -> (_, _, _) -> ---> let (\v0\, \v1\, \v2\) = \x in 233 if isEndpointCap \v0\ \<and> \v1 234 then let ptr = capEPPtr \v0 235 in ->1 else if isNotificationCap \v0\ \<and> \v1 236 then let ptr = capNtfnPtr \v0 237 in ->2 else if isCNodeCap \v0\ \<and> \v1 238 then let cap = \v0\; exposed = \v2 239 in ->3 else if isThreadCap \v0\ \<and> \v1 240 then let tcb = capTCBPtr \v0\; exposed = \v2 241 in ->4 else if isZombie \v0\ \<and> (\<not> \v2\) \<and> capNumber \v0\ \<noteq> 0 242 then let ptr = capCTEPtr \v0\; 243 n = capNumber \v0\ - 1 244 in ->5 else if isZombie \v0\ \<and> \v2\ \<and> capNumber \v0\ \<noteq> 0 245 then let ptr = capCTEPtr \v0\; 246 n = capNumber \v0\ - 1 247 in ->6 else if isZombie \v0\ \<and> capNumber \v0\ = 0 248 then ->7 else if isArchObjectCap \v0 249 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\) 250 in ->8 else if isFrameCap \v0 251 then ->9 else if isNullCap \v0 252 then ->10 else if isZombie \v0\ \<and> (\<not> \v1\) 253 then ->11 else ->12 254 255case \x of (index:bits:args, cap@(CNodeCap {capCNodeCanModify=True})) -> (_, CNodeCap {capCNodeCanModify=False}) -> (_, _) -> ---> let (\v0\, cap) = \x in 256 if length (\v0\) > 1 \<and> isCNodeCap cap \<and> capCNodeCanModify cap then let index = \v0\ !! 0; 257 bits = \v0\ !! 1; 258 args = drop 2 \v0 259 in ->1 else if isCNodeCap cap \<and> (\<not> capCNodeCanModify cap) then ->2 else ->3 260 261case \x of 32 -> 64 -> _ -> ---> if \x = 32 262 then ->1 else if \x = 64 263 then ->2 else ->3 264 265case \x of NullCap -> c@(UntypedCap {}) -> c@(EndpointCap {}) -> c@(NotificationCap {}) -> c@(CNodeCap {}) -> c@(ThreadCap {}) -> c@(FrameCap {}) -> ArchObjectCap {capCap = aoCap} -> c@(Zombie {}) -> ---> let c = \x in 266 if isNullCap c 267 then ->1 else if isUntypedCap c 268 then ->2 else if isEndpointCap c 269 then ->3 else if isNotificationCap c 270 then ->4 else if isCNodeCap c 271 then ->5 else if isThreadCap c 272 then ->6 else if isFrameCap c 273 then ->7 else if isArchObjectCap c 274 then let aoCap = capCap c 275 in ->8 else (* assuming Zombie *) ->9 276 277case \x of (src@EndpointCap {}, new@EndpointCap {}) -> (src@NotificationCap {}, new@NotificationCap {}) -> (_, _) -> ---> let (src, new) = \x in 278 if (isEndpointCap src \<and> isEndpointCap new) 279 then ->1 else if (isNotificationCap src \<and> isNotificationCap new) 280 then ->2 else ->3 281 282case \x of c2@(Zombie { capCTEPtr = ptr2 }) -> _ -> ---> let c2 = \x; 283 ptr2 = capCTEPtr c2 in 284 if isZombie c2 285 then ->1 else ->2 286 287case \x of (EndpointCap { capEPPtr = ptr }, True, _) -> (NotificationCap { capNtfnPtr = ptr }, True, _) -> (cap@(CNodeCap {}), True, exposed) -> (ThreadCap { capTCBPtr = tcb }, True, exposed) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, True, False) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, True, True) -> (Zombie { capNumber = 0 }, True, _) -> (ArchObjectCap { capCap = cap }, final, exposed) -> (FrameCap {}, _, _) -> (NullCap, _, _) -> (Zombie {}, False, _) -> (_, _, _) -> ---> let (\v0\, \v1\, \v2\) = \x in 288 if isEndpointCap \v0\ \<and> \v1 289 then let ptr = capEPPtr \v0 290 in ->1 else if isNotificationCap \v0\ \<and> \v1 291 then let ptr = capNtfnPtr \v0 292 in ->2 else if isCNodeCap \v0\ \<and> \v1 293 then let cap = \v0\; exposed = \v2 294 in ->3 else if isThreadCap \v0\ \<and> \v1 295 then let tcb = capTCBPtr \v0\; exposed = \v2 296 in ->4 else if isZombie \v0\ \<and> \v1\ \<and> (\<not> \v2\) \<and> capNumber \v0\ \<noteq> 0 297 then let ptr = capCTEPtr \v0\; 298 n = capNumber \v0\ - 1 299 in ->5 else if isZombie \v0\ \<and> \v1\ \<and> \v2\ \<and> capNumber \v0\ \<noteq> 0 300 then let ptr = capCTEPtr \v0\; 301 n = capNumber \v0\ - 1; 302 c = \v0 303 in ->6 else if isZombie \v0\ \<and> \v1\ \<and> capNumber \v0\ = 0 304 then ->7 else if isArchObjectCap \v0 305 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\) 306 in ->8 else if isFrameCap \v0 307 then ->9 else if isNullCap \v0 308 then ->10 else if isZombie \v0\ \<and> (\<not> \v1\) 309 then ->11 else ->12 310 311case \x of (src@EndpointCap {}, new@EndpointCap {}) -> (src@NotificationCap {}, new@NotificationCap {}) -> (_, _) -> ---> let (src,new) = \x in 312 if isEndpointCap src & isEndpointCap new 313 then ->1 314 else if isNotificationCap src & isNotificationCap new 315 then ->2 316 else ->3 317 318case \x of EndpointCap { capEPBadge = 0 } -> NotificationCap { capNtfnBadge = 0 } -> EndpointCap {} -> NotificationCap {} -> _ -> ---> if isEndpointCap \x \<and> capEPBadge \x = 0 319 then ->1 else if isNotificationCap \x \<and> capNtfnBadge \x = 0 320 then ->2 else if isEndpointCap \x then ->3 else if isNotificationCap \x 321 then ->4 else ->5 322 323case \x of (_, cap@(EndpointCap {capEPCanSend=True})) -> (_, cap@(NotificationCap {capNtfnCanSend=True})) -> (sl, cap@(ThreadCap {capTCBCanWrite=True})) -> (_, cap@(CNodeCap {capCNodeCanModify=True})) -> (slot, cap@(UntypedCap {})) -> (slot, cap@(ArchObjectCap {})) -> (_, _) -> ---> let (slot, cap) = \x in 324 if isEndpointCap cap \<and> capEPCanSend cap 325 then ->1 else if isNotificationCap cap \<and> capNtfnCanSend cap 326 then ->2 else if isThreadCap cap \<and> capTCBCanWrite cap 327 then let sl = slot 328 in ->3 else if isCNodeCap cap \<and> capCNodeCanModify cap 329 then ->4 else if isUntypedCap cap 330 then ->5 else if isArchObjectCap cap 331 then ->6 else ->7 332 333case \x of EndpointCap { capEPBadge = 0 } -> NotificationCap { capNtfnBadge = 0 } -> EndpointCap { capEPBadge = badge } | badge /= 0 -> NotificationCap { capNtfnBadge = badge } | badge /= 0 -> _ -> ---> if isEndpointCap \x & capEPBadge \x = 0 334 then ->1 335 else if isNotificationCap \x & capNtfnBadge \x = 0 336 then ->2 337 else if isEndpointCap \x 338 then let badge = capEPBadge \x in 339 ->3 340 else if isNotificationCap \x 341 then let badge = capNtfnBadge \x in 342 ->4 343 else ->5 344 345case \x of (_, NullCap) -> (a@(UntypedCap {}), b) -> (a@EndpointCap {}, b@EndpointCap {}) -> (a@NotificationCap {}, b@NotificationCap {}) -> (a@CNodeCap {}, b@CNodeCap {}) -> (a@ThreadCap {}, b@ThreadCap {}) -> (a@FrameCap {}, b@FrameCap {}) -> (ArchObjectCap a, ArchObjectCap b) -> (_, _) -> ---> let (a,b) = \x in 346 if b = NullCap 347 then ->1 348 else if isUntypedCap a 349 then ->2 350 else if isEndpointCap a & isEndpointCap b 351 then ->3 352 else if isNotificationCap a & isNotificationCap b 353 then ->4 354 else if isCNodeCap a & isCNodeCap b 355 then ->5 356 else if isThreadCap a & isThreadCap b 357 then ->6 358 else if isFrameCap a & isFrameCap b 359 then ->7 360 else if isArchObjectCap a & isArchObjectCap b 361 then let a = capCap a; b = capCap b in 362 ->8 363 else ->9 364 365case \x of EndpointCap { capEPBadge = badge } | badge /= 0 -> NotificationCap { capNtfnBadge = badge } | badge /= 0 -> _ -> ---> if isEndpointCap \x & capEPBadge \x ~= 0 366 then let badge = capEPBadge \x in 367 ->1 368 else if isNotificationCap \x & capNtfnBadge \x ~= 0 369 then let badge = capNtfnBadge \x in 370 ->2 371 else ->3 372 373case \x of (EndpointCap { capEPPtr = ptr }, True, _) -> (NotificationCap { capNtfnPtr = ptr }, True, _) -> (cap@(CNodeCap {}), True, exposed) -> (ThreadCap { capTCBPtr = tcb }, True, exposed) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, True, False) -> (z@(Zombie { capCTEPtr = ptr, capNumber = n+1 }), True, True) -> (Zombie { capNumber = 0 }, True, _) -> (ArchObjectCap { capCap = cap }, final, exposed) -> (FrameCap {}, _, _) -> (NullCap, _, _) -> (Zombie {}, False, _) -> (_, _, _) -> ---> let (\v0\, \v1\, \v2\) = \x in 374 if isEndpointCap \v0\ \<and> \v1 375 then let ptr = capEPPtr \v0 376 in ->1 else if isNotificationCap \v0\ \<and> \v1 377 then let ptr = capNtfnPtr \v0 378 in ->2 else if isCNodeCap \v0\ \<and> \v1 379 then let cap = \v0\; exposed = \v2 380 in ->3 else if isThreadCap \v0\ \<and> \v1 381 then let tcb = capTCBPtr \v0\; exposed = \v2 382 in ->4 else if isZombie \v0\ \<and> \v1\ \<and> (\<not> \v2\) \<and> capNumber \v0\ \<noteq> 0 383 then let ptr = capCTEPtr \v0\; 384 n = capNumber \v0\ - 1 385 in ->5 else if isZombie \v0\ \<and> \v1\ \<and> \v2\ \<and> capNumber \v0\ \<noteq> 0 386 then let z = \v0\; 387 ptr = capCTEPtr \v0\; 388 n = capNumber \v0\ - 1; 389 c = \v0 390 in ->6 else if isZombie \v0\ \<and> \v1\ \<and> capNumber \v0\ = 0 391 then ->7 else if isArchObjectCap \v0 392 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\) 393 in ->8 else if isFrameCap \v0 394 then ->9 else if isNullCap \v0 395 then ->10 else if isZombie \v0\ \<and> (\<not> \v1\) 396 then ->11 else ->12 397 398case \x of (srcIndex:srcDepth:args, srcRootCap:_) | label < 4 -> (_, _) | label == 4 -> (_, _) | label == 5 -> (pivotNewData:pivotIndex:pivotDepth:srcNewData:srcIndex:srcDepth:_, pivotRootCap:srcRootCap:_) | label == 6 -> (_, _) | label > 6 -> _ -> ---> let (\v0\, \v1\) = \x 399 in if length \v0\ >= 2 & length \v1\ >= 1 & label < 4 then let srcIndex = \v0\ !! 0; srcDepth = \v0\ !! 1; args = drop 2 \v0\; srcRootCap = \v1\ !! 0 in ->1 else if label = 4 then ->2 else if label = 5 then ->3 else if length \v0\ >= 6 & length \v1\ >= 2 & label = 6 then let pivotNewData = \v0\ !! 0; pivotIndex = \v0\ !! 1; pivotDepth = \v0\ !! 2; srcNewData = \v0\ !! 3; srcIndex = \v0\ !! 4; srcDepth = \v0\ !! 5; pivotRootCap = \v1\ !! 0; srcRootCap = \v1\ !! 1 in ->4 else if label > 6 then ->5 else ->6 400 401case \x of Zombie {} -> cap@(UntypedCap {}) -> ArchObjectCap cap -> cap -> ---> let cap = \x 402 in case cap of Zombie \v0\ \v1\ \v2\ \<Rightarrow> ->1 | UntypedCap \v0\ \v1\ \<Rightarrow> ->2 | ArchObjectCap cap \<Rightarrow> ->3 | _ \<Rightarrow> ->4 403 404case \x of 0 -> 1 -> 2 -> 3 -> 4 -> 5 -> 6 -> 7 -> _ -> ---> let \v0\ = \x 405 in if \v0\ = 0 then ->1 else if \v0\ = 1 then ->2 else if \v0\ = 2 then ->3 else if \v0\ = 3 then ->4 else if \v0\ = 4 then ->5 else if \v0\ = 5 then ->6 else if \v0\ = 6 then ->7 else if \v0\ = 7 then ->8 else ->9 406 407case \x of MI { msgExtraCaps = 0 } -> MI { msgExtraCaps = count } -> ---> let \v0\ = \x 408 in if msgExtraCaps \v0\ = 0 then ->1 else let count = msgExtraCaps \v0\ in ->2 409 410case \x of c@PageTableCap { capPTMappedAddress = Just _ } -> PageTableCap { capPTMappedAddress = Nothing } -> c@PageDirectoryCap { capPDMappedASID = Just _ } -> PageDirectoryCap { capPDMappedASID = Nothing } -> c@PageCap {} -> c@ASIDControlCap -> c@ASIDPoolCap {} -> ---> let c = \x 411 in case c of 412 PageTableCap \v0\ \v1\ \<Rightarrow> if \v1\ = None then ->2 else ->1 413 | PageDirectoryCap \v0\ \v1\ \<Rightarrow> if \v1\ = None then ->4 else ->3 414 | PageCap \v0\ \v1\ \v2\ \v3\ \<Rightarrow> ->5 415 | ASIDControlCap \<Rightarrow> ->6 416 | ASIDPoolCap \v0\ \v1\ \<Rightarrow> ->7 417 418case \x of c@(PageCap {}) -> c -> ---> let c = \x in 419 if isPageCap c 420 then ->1 421 else ->2 422 423case \x of (a@PageCap {}, b@PageCap {}) -> (a@PageTableCap {}, b@PageTableCap {}) -> (a@PageDirectoryCap {}, b@PageDirectoryCap {}) -> (ASIDControlCap, ASIDControlCap) -> (a@ASIDPoolCap {}, b@ASIDPoolCap {}) -> (_, _) -> ---> let (a, b) = \x in 424 if (isPageCap a & isPageCap b) then ->1 else if (isPageTableCap a & isPageTableCap b) then ->2 else if (isPageDirectoryCap a & isPageDirectoryCap b) then ->3 else if (isASIDControlCap a & isASIDControlCap b) then ->4 else if (isASIDPoolCap a & isASIDPoolCap b) then ->5 else ->6 425 426case \x of Arch.Types.APIObjectType _ -> Arch.Types.SmallPageObject -> Arch.Types.LargePageObject -> Arch.Types.SectionObject -> Arch.Types.SuperSectionObject -> Arch.Types.PageTableObject -> Arch.Types.PageDirectoryObject -> ---> case \x of 427 Arch.Types.APIObjectType \v0\ \<Rightarrow> ->1 | Arch.Types.SmallPageObject \<Rightarrow> ->2 | Arch.Types.LargePageObject \<Rightarrow> ->3 | Arch.Types.SectionObject \<Rightarrow> ->4 | Arch.Types.SuperSectionObject \<Rightarrow> ->5 | Arch.Types.PageTableObject \<Rightarrow> ->6 | Arch.Types.PageDirectoryObject \<Rightarrow> ->7 428 429case \x of (srcIndex:srcDepth:args, srcRootCap:_) | label < 4 -> (_, _) | label == 4 -> (_, _) | label == 5 -> (_, _) | label == 6 -> (pivotNewData:pivotIndex:pivotDepth:srcNewData:srcIndex:srcDepth:_, pivotRootCap:srcRootCap:_) | label == 7 -> (_, _) | label > 7 -> _ -> ---> let (\v0\, \v1\) = \x 430 in if length \v0\ >= 2 & length \v1\ >= 1 & label < 4 then let srcIndex = \v0\ !! 0; srcDepth = \v0\ !! 1; args = drop 2 \v0\; srcRootCap = \v1\ !! 0 in ->1 else if label = 4 then ->2 else if label = 5 then ->3 else if label = 6 then ->4 else if length \v0\ >= 6 & length \v1\ >= 2 & label = 7 then let pivotNewData = \v0\ !! 0; pivotIndex = \v0\ !! 1; pivotDepth = \v0\ !! 2; srcNewData = \v0\ !! 3; srcIndex = \v0\ !! 4; srcDepth = \v0\ !! 5; pivotRootCap = \v1\ !! 0; srcRootCap = \v1\ !! 1 in ->5 else if label > 7 then ->6 else ->7 431 432case \x of IdleEP | blocking -> SendEP queue | blocking -> IdleEP -> SendEP _ -> RecvEP (dest:queue) -> RecvEP [] -> ---> case \x of 433 IdleEP \<Rightarrow> if blocking then ->1 else ->3 | SendEP queue \<Rightarrow> if blocking then ->2 else ->4 | RecvEP \v0\ \<Rightarrow> (case \v0\ of dest # queue \<Rightarrow> ->5 | [] \<Rightarrow> ->6 ) 434 435case \x of Zombie {} -> cap@(UntypedCap {}) -> ReplyCap {} -> ArchObjectCap cap -> cap -> ---> let cap = \x 436 in case cap of 437 Zombie \v0\ \v1\ \v2\ \<Rightarrow> ->1 438 | UntypedCap \v0\ \v1\ \<Rightarrow> ->2 439 | ReplyCap \v0\ \v1\ \<Rightarrow> ->3 440 | ArchObjectCap cap \<Rightarrow> ->4 441 | _ \<Rightarrow> ->5 442 443case \x of (EndpointCap { capEPPtr = ptr }, True, _) -> (NotificationCap { capNtfnPtr = ptr }, True, _) -> (cap@(CNodeCap {}), True, exposed) -> (ThreadCap { capTCBPtr = tcb }, True, exposed) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, True, False) -> (z@(Zombie { capCTEPtr = ptr, capNumber = n+1 }), True, True) -> (Zombie { capNumber = 0 }, True, _) -> (IRQHandlerCap { capIRQ = irq }, True, _) -> (ArchObjectCap { capCap = cap }, final, exposed) -> (NullCap, _, _) -> (Zombie {}, False, _) -> (_, _, _) -> ---> let (\v0\, \v1\, \v2\) = \x in 444 if isEndpointCap \v0\ \<and> \v1\ 445 then let ptr = capEPPtr \v0 446 in ->1 447 else if isNotificationCap \v0\ \<and> \v1\ 448 then let ptr = capNtfnPtr \v0 449 in ->2 450 else if isCNodeCap \v0\ \<and> \v1\ 451 then let cap = \v0\; exposed = \v2\ in ->3 452 else if isThreadCap \v0\ \<and> \v1\ 453 then let tcb = capTCBPtr \v0\; exposed = \v2\ in ->4 454 else if isZombie \v0\ \<and> \v1\ \<and> (\<not> \v2\) \<and> capNumber \v0\ \<noteq> 0 455 then let ptr = capCTEPtr \v0\; 456 n = capNumber \v0\ - 1 457 in ->5 458 else if isZombie \v0\ \<and> \v1\ \<and> \v2\ \<and> capNumber \v0\ \<noteq> 0 459 then let z = \v0\; 460 ptr = capCTEPtr \v0\; 461 n = capNumber \v0\ - 1; 462 c = \v0\ 463 in ->6 464 else if isZombie \v0\ \<and> \v1\ \<and> capNumber \v0\ = 0 465 then ->7 466 else if isIRQHandlerCap \v0\ \<and> \v1\ 467 then let irq = capIRQ \v0\ in ->8 468 else if isArchObjectCap \v0\ 469 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\) in ->9 470 else if isNullCap \v0\ 471 then ->10 472 else if isZombie \v0\ \<and> (\<not> \v1\) 473 then ->11 474 else ->12 475 476case \x of (_, NullCap) -> (a@(UntypedCap {}), b) -> (a@EndpointCap {}, b@EndpointCap {}) -> (a@NotificationCap {}, b@NotificationCap {}) -> (a@CNodeCap {}, b@CNodeCap {}) -> (a@ThreadCap {}, b@ThreadCap {}) -> (IRQControlCap, IRQControlCap) -> (IRQHandlerCap a, IRQHandlerCap b) -> (ArchObjectCap a, ArchObjectCap b) -> (_, _) -> --->let (a,b) = \x in 477 if b = NullCap 478 then ->1 479 else if isUntypedCap a 480 then ->2 481 else if isEndpointCap a & isEndpointCap b 482 then ->3 483 else if isNotificationCap a & isNotificationCap b 484 then ->4 485 else if isCNodeCap a & isCNodeCap b 486 then ->5 487 else if isThreadCap a & isThreadCap b 488 then ->6 489 else if a = IRQControlCap & b = IRQControlCap 490 then ->7 491 else if isIRQHandlerCap a & isIRQHandlerCap b 492 then let a = capIRQ a; b = capIRQ b in ->8 493 else if isArchObjectCap a & isArchObjectCap b 494 then let a = capCap a; b = capCap b in 495 ->9 496 else ->10 497 498case \x of (preserve, new, cap@(EndpointCap {})) -> (preserve, new, cap@(NotificationCap {})) -> (_, w, cap@(CNodeCap {})) -> (p, w, ArchObjectCap { capCap = aoCap }) -> (_, _, cap) -> --->let (\v0\, \v1\, \v2\ ) = \x in 499 if isEndpointCap \v2\ 500 then let preserve = \v0\; new = \v1\; cap = \v2\ in ->1 501 else if isNotificationCap \v2\ 502 then let preserve = \v0\; new = \v1\; cap = \v2\ in ->2 503 else if isCNodeCap \v2\ 504 then let w = \v1\; cap = \v2\ in ->3 505 else if isArchObjectCap \v2\ 506 then let p = \v0\; w = \v1\; aoCap = capCap \v2\ in ->4 507 else let cap = \v2\ in ->5 508 509case \x of NullCap -> c@(UntypedCap {}) -> c@(EndpointCap {}) -> c@(NotificationCap {}) -> c@(ReplyCap {}) -> c@(CNodeCap {}) -> c@(ThreadCap {}) -> c@IRQControlCap -> c@(IRQHandlerCap {}) -> ArchObjectCap {capCap = aoCap} -> c@(Zombie {}) -> --->let c = \x in 510 if isNullCap c then ->1 511 else if isUntypedCap c then ->2 512 else if isEndpointCap c then ->3 513 else if isNotificationCap c then ->4 514 else if isReplyCap c then ->5 515 else if isCNodeCap c then ->6 516 else if isThreadCap c then ->7 517 else if isIRQControlCap c then ->8 518 else if isIRQHandlerCap c then ->9 519 else if isArchObjectCap c then let aoCap = capCap c in ->10 520 else (* assuming Zombie *) ->11 521 522case \x of 0 -> 1 -> 2 -> 3 -> 4 -> 5 -> 6 -> 7 -> 8 -> 9 -> _ -> --->let \v0\ = \x 523 in if \v0\ = 0 then ->1 else if \v0\ = 1 then ->2 else if \v0\ = 2 then ->3 else if \v0\ = 3 then ->4 else if \v0\ = 4 then ->5 else if \v0\ = 5 then ->6 else if \v0\ = 6 then ->7 else if \v0\ = 7 then ->8 else if \v0\ = 8 then ->9 else if \v0\ = 9 then ->10 else ->11 524 525case \x of ArchObjectCap (pageCap@PageCap {}) -> _ -> ---> let \v0\ = \x in 526 if isArchObjectCap \v0\ \<and> isPageCap (capCap \v0\) 527 then 528 let pageCap = capCap \v0\ 529 in ->1 530 else ->2 531 532case \x of ArchObjectCap (frameCap@PageCap {}) -> _ -> ---> let \v0\ = \x in 533 if isArchObjectCap \v0\ \<and> isPageCap (capCap \v0\) 534 then 535 let frameCap = capCap \v0\ 536 in ->1 537 else ->2 538 539case \x of ((Zombie { capCTEPtr = ptr, capNumber = n+1 }), False) -> (z@(Zombie { capCTEPtr = ptr, capNumber = n+1 }), True) -> (_, _) -> ---> let (\v0\, \v1\) = \x in 540 if isZombie \v0\ \<and> (\<not> \v1\) \<and> capNumber \v0\ \<noteq> 0 541 then let ptr = capCTEPtr \v0\; 542 n = capNumber \v0\ - 1 543 in ->1 544 else if isZombie \v0\ \<and> \v1\ \<and> capNumber \v0\ \<noteq> 0 545 then let z = \v0\; 546 ptr = capCTEPtr \v0\; 547 n = capNumber \v0\ - 1 548 in ->2 549 else ->3 550 551case \x of (c@PageTableCap { capPTMappedAddress = Just _ }) -> (PageTableCap { capPTMappedAddress = Nothing }) -> (c@PageDirectoryCap { capPDMappedASID = Just _ }) -> (PageDirectoryCap { capPDMappedASID = Nothing }) -> (c@PageCap {}) -> c@ASIDControlCap -> (c@ASIDPoolCap {}) -> ---> let c = \x in 552 if isPageTableCap c \<and> capPTMappedAddress c \<noteq> None 553 then ->1 554 else if isPageTableCap c \<and> capPTMappedAddress c = None 555 then ->2 556 else if isPageDirectoryCap c \<and> capPDMappedASID c \<noteq> None 557 then ->3 558 else if isPageDirectoryCap c \<and> capPDMappedASID c = None 559 then ->4 560 else if isPageCap c 561 then ->5 562 else if isASIDControlCap c 563 then ->6 564 else if isASIDPoolCap c 565 then ->7 566 else undefined 567 568case \x of ((a@PageCap {}), (b@PageCap {})) -> ((a@PageTableCap {}), (b@PageTableCap {})) -> ((a@PageDirectoryCap {}), (b@PageDirectoryCap {})) -> (ASIDControlCap, ASIDControlCap) -> ((a@ASIDPoolCap {}), (b@ASIDPoolCap {})) -> (_, _) -> ---> let (a, b) = \x in 569 if isPageCap a \<and> isPageCap b 570 then ->1 571 else if isPageTableCap a \<and> isPageTableCap b 572 then ->2 573 else if isPageDirectoryCap a \<and> isPageDirectoryCap b 574 then ->3 575 else if isASIDControlCap a \<and> isASIDControlCap b 576 then ->4 577 else if isASIDPoolCap a \<and> isASIDPoolCap b 578 then ->5 579 else ->6 580 581case \x of ArchObjectCap (frame@PageCap {}) -> _ -> ---> let \v0\ = \x in 582 if isArchObjectCap \v0\ \<and> isPageCap (capCap \v0\) 583 then let frame = capCap \v0\ 584 in ->1 585 else ->2 586 587case \x of ArchObjectCap (PageDirectoryCap { capPDMappedASID = Just _, capPDBasePtr = cur_pd }) | cur_pd == pd -> _ -> ---> let \v0\ = \x in 588 if isArchObjectCap \v0\ \<and> isPageDirectoryCap (capCap \v0\) \<and> capPDMappedASID (capCap \v0\) \<noteq> None \<and> capPDBasePtr (capCap \v0\) = pd 589 then let cur_pd = pd in ->1 590 else ->2 591 592case \x of (0, vaddr:attr:_, (pdCap,_):_) -> (0, _, _) -> _ -> ---> let (\v0\, \v1\, \v2\) = \x in 593 if \v0\ = 0 then 594 if length \v1\ > 1 \<and> length \v2\ > 0 595 then let vaddr = \v1\ !! 0; 596 attr = \v1\ !! 1; 597 pdCap = fst (\v2\ !! 0) 598 in ->1 599 else ->2 600 else ->3 601 602case \x of (0, vaddr:rightsMask:attr:_, (pdCap,_):_) -> (0, _, _) -> (1, rightsMask:attr:_, _) -> (1, _, _) -> (2, _, _) -> (3, _, _) -> _ -> ---> let (\v0\, \v1\, \v2\) = \x in 603 if \v0\ = 0 then 604 if length \v1\ > 2 \<and> length \v2\ > 0 605 then let vaddr = \v1\ !! 0; 606 rightsMask = \v1\ !! 1; 607 attr = \v1\ !! 2; 608 pdCap = fst (\v2\ !! 0) 609 in ->1 610 else ->2 611 else if \v0\ = 1 then 612 if length \v1\ > 1 613 then let rightsMask = \v1\ !! 0; 614 attr = \v1\ !! 1 615 in ->3 616 else ->4 617 else if \v0\ = 2 618 then ->5 619 else if \v0\ = 3 620 then ->6 621 else ->7 622 623case \x of (0, index:depth:_, (untyped,parentSlot):(croot,_):_) -> (0, _, _) -> _ -> ---> let (\v0\, \v1\, \v2\) = \x in 624 if \v0\ = 0 then 625 if length \v1\ > 1 \<and> length \v2\ > 1 626 then let index = \v1\ !! 0; 627 depth = \v1\ !! 1; 628 (untyped, parentSlot) = \v2\ !! 0; 629 croot = fst (\v2\ !! 1) 630 in ->1 631 else ->2 632 else ->3 633 634case \x of (0, (pdCap,pdCapSlot):_) -> (0, _) -> _ -> ---> let (\v0\, \v1\) = \x in 635 if \v0\ = 0 then 636 if length \v1\ > 0 637 then let (pdCap, pdCapSlot) = \v1\ !! 0 638 in ->1 639 else ->2 640 else ->3 641 642case \x of (PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) -> ---> let cap = \x in 643 if isPageDirectoryCap cap 644 then ->1 645 else if isPageTableCap cap 646 then ->2 647 else if isPageCap cap 648 then ->3 649 else if isASIDControlCap cap 650 then ->4 651 else if isASIDPoolCap cap 652 then ->5 653 else undefined 654 655case \x of ((index:bits:args), cap@(CNodeCap {capCNodeCanModify=True})) -> (_, (CNodeCap {capCNodeCanModify=True})) -> (_, _) -> ---> let (\v0\, cap) = \x in 656 if isCNodeCap cap \<and> capCNodeCanModify cap 657 then 658 (case \v0\ of 659 (index # bits # args) \<Rightarrow> ->1 660 | _ \<Rightarrow> ->2 661 ) 662 else ->3 663 664case \x of ((src@EndpointCap {}), (new@EndpointCap {})) -> ((src@NotificationCap {}), (new@NotificationCap {})) -> (_, _) -> ---> let (src, new) = \x in 665 if isEndpointCap src \<and> isEndpointCap new 666 then ->1 667 else if isNotificationCap src \<and> isNotificationCap new 668 then ->2 669 else ->3 670 671case \x of (CTE { cteCap = UntypedCap {} }) -> cte@(CTE { cteMDBNode = mdb }) -> ---> let \v0\ = \x in 672 if isUntypedCap (cteCap \v0\) 673 then ->1 674 else let cte = \v0\; 675 mdb = cteMDBNode cte 676 in ->2 677 678case \x of 0 | length msg >= length syscallMessage -> _ -> ---> if \x = 0 \<and> length msg \<ge> length syscallMessage 679 then ->1 680 else ->2 681 682case \x of 0 | length msg >= length exceptionMessage -> _ -> ---> if \x = 0 \<and> length msg \<ge> length exceptionMessage 683 then ->1 684 else ->2 685 686case \x of (0,irqW:index:depth:_,cnode:_) -> (0,_,_) -> (1,_,_) -> _ -> ---> let (\v0\, \v1\, \v2\) = \x in 687 if \v0\ = 0 then 688 if length \v1\ > 2 \<and> length \v2\ > 0 689 then let irqW = \v1\ !! 0; 690 index = \v1\ !! 1; 691 depth = \v1\ !! 2; 692 cnode = \v2\ !! 0 693 in ->1 694 else ->2 695 else if \v0\ = 1 696 then ->3 697 else ->4 698 699case \x of (0,_) -> (1,(cap,slot):_) -> (1,_) -> (2,_) -> _ -> ---> let (\v0\, \v1\) = \x in 700 if \v0\ = 0 701 then ->1 702 else if \v0\ = 1 703 then if length \v1\ > 0 704 then let (cap, slot) = \v1\ !! 0 705 in ->2 706 else ->3 707 else if \v0\ = 2 708 then ->4 709 else ->5 710 711case \x of (Zombie {}) -> cap@(UntypedCap {}) -> (ReplyCap {}) -> (ArchObjectCap cap) -> cap -> ---> let cap = \x in 712 if isZombie cap 713 then ->1 714 else if isUntypedCap cap 715 then ->2 716 else if isReplyCap cap 717 then ->3 718 else if isArchObjectCap cap 719 then let cap = capCap cap 720 in ->4 721 else ->5 722 723case \x of ((EndpointCap { capEPPtr = ptr }), True) -> ((NotificationCap { capNtfnPtr = ptr }), True) -> ((CNodeCap { capCNodePtr = ptr, capCNodeBits = bits }), True) -> ((ThreadCap { capTCBPtr = tcb}), True) -> (z@(Zombie {}), True) -> ((ArchObjectCap { capCap = cap }), final) -> ((IRQHandlerCap { capIRQ = irq }), True) -> (NullCap, _) -> ((Zombie {}), False) -> (_, _) -> ---> let (\v0\, \v1\) = \x in 724 if isEndpointCap \v0\ \<and> \v1\ 725 then let ptr = capEPPtr \v0\ 726 in ->1 727 else if isNotificationCap \v0\ \<and> \v1\ 728 then let ptr = capNtfnPtr \v0\ 729 in ->2 730 else if isCNodeCap \v0\ \<and> \v1\ 731 then let ptr = capCNodePtr \v0\; bits = capCNodeBits \v0\ 732 in ->3 733 else if isThreadCap \v0\ \<and> \v1\ 734 then let tcb = capTCBPtr \v0\ 735 in ->4 736 else if isZombie \v0\ \<and> \v1\ 737 then let z = \v0\ 738 in ->5 739 else if isArchObjectCap \v0\ 740 then let cap = capCap \v0\; final = \v1\ 741 in ->6 742 else if isIRQHandlerCap \v0\ \<and> \v1\ 743 then let irq = capIRQ \v0\ 744 in ->7 745 else if isNullCap \v0\ 746 then ->8 747 else if isZombie \v0\ \<and> \<not> \v1\ 748 then ->9 749 else ->10 750 751case \x of (_, NullCap) -> (a@(UntypedCap {}), b) -> ((a@EndpointCap {}), (b@EndpointCap {})) -> ((a@NotificationCap {}), (b@NotificationCap {})) -> ((a@CNodeCap {}), (b@CNodeCap {})) -> ((a@ThreadCap {}), (b@ThreadCap {})) -> (IRQControlCap, IRQControlCap) -> ((IRQHandlerCap a), (IRQHandlerCap b)) -> ((ArchObjectCap a), (ArchObjectCap b)) -> (_, _) -> ---> let (a, b) = \x in 752 if isNullCap b 753 then ->1 754 else if isUntypedCap a 755 then ->2 756 else if isEndpointCap a \<and> isEndpointCap b 757 then ->3 758 else if isNotificationCap a \<and> isNotificationCap b 759 then ->4 760 else if isCNodeCap a \<and> isCNodeCap b 761 then ->5 762 else if isThreadCap a \<and> isThreadCap b 763 then ->6 764 else if isIRQControlCap a \<and> isIRQControlCap b 765 then ->7 766 else if isIRQHandlerCap a \<and> isIRQHandlerCap b 767 then (case (a, b) of 768 (IRQHandlerCap a, IRQHandlerCap b) \<Rightarrow> ->8 769 ) 770 else if isArchObjectCap a \<and> isArchObjectCap b 771 then (case (a, b) of 772 (ArchObjectCap a, ArchObjectCap b) \<Rightarrow> ->9 773 ) 774 else ->10 775 776case \x of (preserve, new, cap@(EndpointCap {})) -> (preserve, new, cap@(NotificationCap {})) -> (_, w, cap@(CNodeCap {})) -> (p, w, (ArchObjectCap { capCap = aoCap })) -> (_, _, cap) -> ---> let (\v0\, \v1\, \v2\) = \x in 777 if isEndpointCap \v2\ 778 then let preserve = \v0\; new = \v1\; cap = \v2\ 779 in ->1 780 else if isNotificationCap \v2\ 781 then let preserve = \v0\; new = \v1\; cap = \v2\ 782 in ->2 783 else if isCNodeCap \v2\ 784 then let w = \v1\; cap = \v2\ 785 in ->3 786 else if isArchObjectCap \v2\ 787 then let p = \v0\; w = \v1\; aoCap = capCap \v2\ 788 in ->4 789 else let cap = \v2\ 790 in ->5 791 792case \x of NullCap -> c@(UntypedCap {}) -> c@(EndpointCap {}) -> c@(NotificationCap {}) -> c@(ReplyCap {}) -> c@(CNodeCap {}) -> c@(ThreadCap {}) -> c@IRQControlCap -> c@(IRQHandlerCap {}) -> (ArchObjectCap {capCap = aoCap}) -> c@(Zombie {}) -> ---> let c = \x; aoCap = capCap \x in 793 if isNullCap c 794 then ->1 795 else if isUntypedCap c 796 then ->2 797 else if isEndpointCap c 798 then ->3 799 else if isNotificationCap c 800 then ->4 801 else if isReplyCap c 802 then ->5 803 else if isCNodeCap c 804 then ->6 805 else if isThreadCap c 806 then ->7 807 else if isIRQControlCap c 808 then ->8 809 else if isIRQHandlerCap c 810 then ->9 811 else if isArchObjectCap c 812 then ->10 813 else if isZombie c 814 then ->11 815 else undefined 816 817case \x of cap@(EndpointCap {capEPCanSend=True}) -> cap@(NotificationCap {capNtfnCanSend=True}) -> cap@(ReplyCap {capReplyMaster=False}) -> cap@(ThreadCap {capTCBCanWrite=True}) -> cap@(CNodeCap {capCNodeCanModify=True}) -> cap@(UntypedCap {}) -> IRQControlCap -> (IRQHandlerCap { capIRQ = irq }) -> (ArchObjectCap cap) -> _ -> ---> let cap = \x in 818 if isEndpointCap cap \<and> capEPCanSend cap 819 then ->1 820 else if isNotificationCap cap \<and> capNtfnCanSend cap 821 then ->2 822 else if isReplyCap cap \<and> \<not> capReplyMaster cap 823 then ->3 824 else if isThreadCap cap \<and> capTCBCanWrite cap 825 then ->4 826 else if isCNodeCap cap \<and> capCNodeCanModify cap 827 then ->5 828 else if isUntypedCap cap 829 then ->6 830 else if isIRQControlCap cap 831 then ->7 832 else if isIRQHandlerCap cap 833 then let irq = capIRQ cap 834 in ->8 835 else if isArchObjectCap cap 836 then let cap = capCap cap 837 in ->9 838 else ->10 839 840case \x of (EndpointCap { capEPPtr = p1 }, Just p2, _) | p1 == p2 -> (_, _, destSlot:slots') -> _ -> ---> let (\v0\, \v1\, \v2\) = \x in 841 if isEndpointCap \v0\ \<and> \v1\ \<noteq> None \<and> capEPPtr \v0\ = the \v1\ 842 then let p1 = capEPPtr \v0\; p2 = p1 843 in ->1 844 else (case \v2\ of 845 destSlot # slots' \<Rightarrow> ->2 846 | _ \<Rightarrow> ->3 847 ) 848 849case \x of ((EndpointCap { capEPPtr = ptr }), final, _) -> ((NotificationCap { capNtfnPtr = ptr }), final, _) -> ((ReplyCap {}), _, _) -> (_, _, True) -> ((CNodeCap { capCNodePtr = ptr, capCNodeBits = bits }), True, _) -> ((ThreadCap { capTCBPtr = tcb}), True, _) -> (z@(Zombie {}), True, _) -> ((ArchObjectCap { capCap = cap }), final, _) -> ((IRQHandlerCap { capIRQ = irq }), True, _) -> (NullCap, _, _) -> ((Zombie {}), False, _) -> (_, _, _) -> ---> let (\v0\, \v1\, \v2\) = \x in 850 if isEndpointCap \v0\ 851 then let ptr = capEPPtr \v0\; final = \v1\ 852 in ->1 853 else if isNotificationCap \v0\ 854 then let ptr = capNtfnPtr \v0\; final = \v1\ 855 in ->2 856 else if isReplyCap \v0\ 857 then ->3 858 else if \v2\ 859 then ->4 860 else if isCNodeCap \v0\ \<and> \v1\ 861 then let ptr = capCNodePtr \v0\; bits = capCNodeBits \v0\ 862 in ->5 863 else if isThreadCap \v0\ \<and> \v1\ 864 then let tcb = capTCBPtr \v0\ 865 in ->6 866 else if isZombie \v0\ \<and> \v1\ 867 then let z = \v0\ 868 in ->7 869 else if isArchObjectCap \v0\ 870 then let cap = capCap \v0\; final = \v1\ 871 in ->8 872 else if isIRQHandlerCap \v0\ \<and> \v1\ 873 then let irq = capIRQ \v0\ 874 in ->9 875 else if isNullCap \v0\ 876 then ->10 877 else if isZombie \v0\ \<and> \<not> \v1\ 878 then ->11 879 else ->12 880 881case \x of (cap@PageCap { capVPIsDevice = isDevice }) -> (cap@PageTableCap { capPTBasePtr = ptr }) -> (cap@PageDirectoryCap { capPDBasePtr = ptr }) -> ASIDControlCap -> (cap@ASIDPoolCap { capASIDBase = base, capASIDPool = ptr }) -> ---> let cap = \x in 882 if isPageCap cap 883 then let isDevice = capVPIsDevice cap 884 in ->1 885 else if isPageTableCap cap 886 then let ptr = capPTBasePtr cap 887 in ->2 888 else if isPageDirectoryCap cap 889 then let ptr = capPDBasePtr cap 890 in ->3 891 else if isASIDControlCap cap 892 then ->4 893 else if isASIDPoolCap cap 894 then let base = capASIDBase cap; ptr = capASIDPool cap 895 in ->5 896 else undefined 897 898case \x of ArchObjectCap (frame@PageCap {capVPIsDevice = False}) -> _ -> ---> let cap = \x in 899 if isPageCap cap \<and> \<not> capVPIsDevice cap 900 then ->1 901 else ->2 902 903case \x of (srcIndex:srcDepth:args, srcRootCap:_) | label < 4 -> (_, _) | label == 4 -> (_, _) | label == 5 -> (_, _) | label == 6 -> (_, _) | label == 7 -> (pivotNewData:pivotIndex:pivotDepth:srcNewData:srcIndex:srcDepth:_, pivotRootCap:srcRootCap:_) | label == 8 -> (_, _) | label > 8 -> _ -> ---> let (\v0\, \v1\) = \x in 904 case (if label < 4 then 1 905 else if label = 4 then 2 906 else if label = 5 then 3 907 else if label = 6 then 4 908 else if label = 7 then 5 909 else if label = 8 then 6 910 else if label > 8 then 7 else 0, \v0\, \v1\) of 911 (Suc 0, srcIndex # srcDepth # args, srcRootCap # _) 912 \<Rightarrow> ->1 913 | (Suc (Suc 0), _, _) 914 \<Rightarrow> ->2 915 | (Suc (Suc (Suc 0)), _, _) 916 \<Rightarrow> ->3 917 | (Suc (Suc (Suc (Suc 0))), _, _) 918 \<Rightarrow> ->4 919 | (Suc (Suc (Suc (Suc (Suc 0)))), _, _) 920 \<Rightarrow> ->5 921 | (Suc (Suc (Suc (Suc (Suc (Suc 0))))), 922 pivotNewData#pivotIndex#pivotDepth#srcNewData#srcIndex#srcDepth#_, 923 pivotRootCap#srcRootCap#_) 924 \<Rightarrow> ->6 925 | (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))), _, _) 926 \<Rightarrow> ->7 927 | _ \<Rightarrow> ->8 928 929case \x of c2@(Zombie { capZombiePtr = ptr2 }) -> _ -> ---> let \v0\ = \x in 930 if isZombie \v0\ 931 then let c2 = \v0\; ptr2 = capZombiePtr c2 932 in ->1 933 else ->2 934 935case \x of ((Zombie { capZombieNumber = 0 }), _) -> ((Zombie { capZombiePtr = ptr }), False) -> (z@(Zombie { capZombiePtr = ptr, capZombieNumber = n+1 }), True) -> (_, _) -> ---> let (\v0\, \v1\) = \x in 936 if isZombie \v0\ \<and> capZombieNumber \v0\ = 0 937 then ->1 938 else if isZombie \v0\ \<and> \<not> \v1\ 939 then let ptr = capZombiePtr \v0\ 940 in ->2 941 else if isZombie \v0\ \<and> \v1\ 942 then let z = \v0\; ptr = capZombiePtr z; n = capZombieNumber z - 1 943 in ->3 944 else ->4 945 946case \x of NullCap -> (CNodeCap {}) -> (ThreadCap {}) -> (Zombie { capZombiePtr = ptr, capZombieType = tp, capZombieNumber = n}) -> (cap@EndpointCap { capEPPtr = ep, capEPBadge = b }) -> (ArchObjectCap cap) -> cap -> ---> let cap = \x in 947 if isNullCap cap 948 then ->1 949 else if isCNodeCap cap 950 then ->2 951 else if isThreadCap cap 952 then ->3 953 else if isZombie cap 954 then let ptr = capZombiePtr cap; tp = capZombieType cap; 955 n = capZombieNumber cap 956 in ->4 957 else if isEndpointCap cap 958 then let ep = capEPPtr cap; b = capEPBadge cap 959 in ->5 960 else if isArchObjectCap cap 961 then let cap = capCap cap 962 in ->6 963 else ->7 964 965case \x of (_, NullCap) -> (a@(UntypedCap {}), b) -> ((a@EndpointCap {}), (b@EndpointCap {})) -> ((a@NotificationCap {}), (b@NotificationCap {})) -> ((a@CNodeCap {}), (b@CNodeCap {})) -> ((a@ThreadCap {}), (b@ThreadCap {})) -> (IRQControlCap, IRQControlCap) -> (IRQControlCap, (IRQHandlerCap {})) -> ((IRQHandlerCap a), (IRQHandlerCap b)) -> ((ArchObjectCap a), (ArchObjectCap b)) -> (_, _) -> ---> let (a, b) = \x in 966 if isNullCap b 967 then ->1 968 else if isUntypedCap a 969 then ->2 970 else if isEndpointCap a \<and> isEndpointCap b 971 then ->3 972 else if isNotificationCap a \<and> isNotificationCap b 973 then ->4 974 else if isCNodeCap a \<and> isCNodeCap b 975 then ->5 976 else if isThreadCap a \<and> isThreadCap b 977 then ->6 978 else if isIRQControlCap a \<and> isIRQControlCap b 979 then ->7 980 else if isIRQControlCap a \<and> isIRQHandlerCap b 981 then ->8 982 else if isIRQHandlerCap a \<and> isIRQHandlerCap b 983 then (case (a, b) of 984 (IRQHandlerCap a, IRQHandlerCap b) \<Rightarrow> ->9 985 ) 986 else if isArchObjectCap a \<and> isArchObjectCap b 987 then (case (a, b) of 988 (ArchObjectCap a, ArchObjectCap b) \<Rightarrow> ->10 989 ) 990 else ->11 991 992case \x of (a@(UntypedCap {}), b) -> ((a@EndpointCap {}), (b@EndpointCap {})) -> ((a@NotificationCap {}), (b@NotificationCap {})) -> ((a@CNodeCap {}), (b@CNodeCap {})) -> ((a@ThreadCap {}), (b@ThreadCap {})) -> ((a@ReplyCap {}), (b@ReplyCap {})) -> (IRQControlCap, IRQControlCap) -> (IRQControlCap, (IRQHandlerCap {})) -> ((IRQHandlerCap a), (IRQHandlerCap b)) -> ((ArchObjectCap a), (ArchObjectCap b)) -> (_, _) -> ---> let (a, b) = \x in 993 if isUntypedCap a 994 then ->1 995 else if isEndpointCap a \<and> isEndpointCap b 996 then ->2 997 else if isNotificationCap a \<and> isNotificationCap b 998 then ->3 999 else if isCNodeCap a \<and> isCNodeCap b 1000 then ->4 1001 else if isThreadCap a \<and> isThreadCap b 1002 then ->5 1003 else if isReplyCap a \<and> isReplyCap b 1004 then ->6 1005 else if isIRQControlCap a \<and> isIRQControlCap b 1006 then ->7 1007 else if isIRQControlCap a \<and> isIRQHandlerCap b 1008 then ->8 1009 else if isIRQHandlerCap a \<and> isIRQHandlerCap b 1010 then (case (a, b) of 1011 (IRQHandlerCap a, IRQHandlerCap b) \<Rightarrow> ->9 1012 ) 1013 else if isArchObjectCap a \<and> isArchObjectCap b 1014 then (case (a, b) of 1015 (ArchObjectCap a, ArchObjectCap b) \<Rightarrow> ->10 1016 ) 1017 else ->11 1018 1019case \x of ((a@PageCap {}), (b@PageCap {})) -> (a, b) -> ---> let (a, b) = \x in 1020 if isPageCap a \<and> isPageCap b 1021 then ->1 1022 else ->2 1023 1024case \x of ((a@PageCap { capVPBasePtr = ptrA }), (b@PageCap {})) -> (a, b) -> ---> let (a, b) = \x in 1025 if isPageCap a \<and> isPageCap b 1026 then let ptrA = capVPBasePtr a 1027 in ->1 1028 else ->2 1029 1030case \x of NullCap -> c2@(Zombie { capZombiePtr = ptr2 }) -> _ -> ---> let c2 = \x in 1031 if isNullCap c2 1032 then ->1 1033 else if isZombie c2 1034 then let ptr2 = capZombiePtr c2 1035 in ->2 1036 else ->3 1037 1038case \x of ((EndpointCap { capEPPtr = ptr }), final, _) -> ((NotificationCap { capNtfnPtr = ptr }), final, _) -> ((ReplyCap {}), _, _) -> (NullCap, _, _) -> (_, _, True) -> ((CNodeCap { capCNodePtr = ptr, capCNodeBits = bits }), True, _) -> ((ThreadCap { capTCBPtr = tcb}), True, _) -> (z@(Zombie {}), True, _) -> ((ArchObjectCap { capCap = cap }), final, _) -> ((IRQHandlerCap { capIRQ = irq }), True, _) -> ((Zombie {}), False, _) -> (_, _, _) -> ---> let (\v0\, \v1\, \v2\) = \x in 1039 if isEndpointCap \v0\ 1040 then let ptr = capEPPtr \v0\; final = \v1\ 1041 in ->1 1042 else if isNotificationCap \v0\ 1043 then let ptr = capNtfnPtr \v0\; final = \v1\ 1044 in ->2 1045 else if isReplyCap \v0\ 1046 then ->3 1047 else if isNullCap \v0\ 1048 then ->4 1049 else if \v2\ 1050 then ->5 1051 else if isCNodeCap \v0\ \<and> \v1\ 1052 then let ptr = capCNodePtr \v0\; bits = capCNodeBits \v0\ 1053 in ->6 1054 else if isThreadCap \v0\ \<and> \v1\ 1055 then let tcb = capTCBPtr \v0\ 1056 in ->7 1057 else if isZombie \v0\ \<and> \v1\ 1058 then let z = \v0\ 1059 in ->8 1060 else if isArchObjectCap \v0\ 1061 then let cap = capCap \v0\; final = \v1\ 1062 in ->9 1063 else if isIRQHandlerCap \v0\ \<and> \v1\ 1064 then let irq = capIRQ \v0\ 1065 in ->10 1066 else if isZombie \v0\ \<and> \<not> \v1\ 1067 then ->11 1068 else ->12 1069 1070case \x of (cap@CNodeCap {}) -> (cap@Zombie {}) -> (cap@ThreadCap {}) -> _ -> ---> let cap = \x in 1071 if isCNodeCap cap then ->1 1072 else if isZombie cap then ->2 1073 else if isThreadCap cap then ->3 1074 else ->4 1075 1076case \x of (Zombie {}) -> (IRQControlCap) -> cap@(UntypedCap {}) -> (ReplyCap {}) -> (ArchObjectCap cap) -> cap -> ---> let cap = \x in 1077 if isZombie cap 1078 then ->1 1079 else if isIRQControlCap cap 1080 then ->2 1081 else if isUntypedCap cap 1082 then ->3 1083 else if isReplyCap cap 1084 then ->4 1085 else if isArchObjectCap cap 1086 then let cap = capCap cap 1087 in ->5 1088 else ->6 1089 1090case \x of NullCap -> (Zombie { capZombiePtr = ptr, capZombieType = tp }) -> (cap@EndpointCap { capEPPtr = ep, capEPBadge = b }) -> (ArchObjectCap cap) -> cap -> ---> let cap = \x in 1091 if isNullCap cap 1092 then ->1 1093 else if isZombie cap 1094 then let ptr = capZombiePtr cap; tp = capZombieType cap; 1095 n = capZombieNumber cap 1096 in ->2 1097 else if isEndpointCap cap 1098 then let ep = capEPPtr cap; b = capEPBadge cap 1099 in ->3 1100 else if isArchObjectCap cap 1101 then let cap = capCap cap 1102 in ->4 1103 else ->5 1104 1105case \x of cte@(CTE { cteMDBNode = mdb }) -> ---> let cte = \x; mdb = cteMDBNode cte 1106 in ->1 1107 1108case \x of (0, vaddr:attr:_, (pdCap,_):_) -> (0, _, _) -> (1, _, _) -> _ -> ---> let (\v0\, \v1\, \v2\) = \x in 1109 if \v0\ = 0 then 1110 if length \v1\ > 1 \<and> length \v2\ > 0 1111 then let vaddr = \v1\ !! 0; 1112 attr = \v1\ !! 1; 1113 pdCap = fst (\v2\ !! 0) 1114 in ->1 1115 else ->2 1116 else if \v0\ = 1 then ->3 1117 else ->4 1118 1119case \x of (slot, 0) -> (_, bitsLeft) -> ---> let (slot, bitsLeft) = \x in 1120 if bitsLeft = 0 1121 then ->1 else ->2 1122 1123case \x of ((index:bits:args), cap@(CNodeCap {})) -> (_, (CNodeCap {})) -> (_, _) -> ---> let (\v0\, cap) = \x in 1124 if isCNodeCap cap 1125 then 1126 (case \v0\ of 1127 (index # bits # args) \<Rightarrow> ->1 1128 | _ \<Rightarrow> ->2 1129 ) 1130 else ->3 1131 1132case \x of cap@(EndpointCap {capEPCanSend=True}) -> cap@(NotificationCap {capNtfnCanSend=True}) -> cap@(ReplyCap {capReplyMaster=False}) -> cap@(ThreadCap {}) -> cap@(CNodeCap {}) -> cap@(UntypedCap {}) -> IRQControlCap -> (IRQHandlerCap { capIRQ = irq }) -> (ArchObjectCap cap) -> _ -> ---> let cap = \x in 1133 if isEndpointCap cap \<and> capEPCanSend cap 1134 then ->1 1135 else if isNotificationCap cap \<and> capNtfnCanSend cap 1136 then ->2 1137 else if isReplyCap cap \<and> \<not> capReplyMaster cap 1138 then ->3 1139 else if isThreadCap cap 1140 then ->4 1141 else if isCNodeCap cap 1142 then ->5 1143 else if isUntypedCap cap 1144 then ->6 1145 else if isIRQControlCap cap 1146 then ->7 1147 else if isIRQHandlerCap cap 1148 then let irq = capIRQ cap 1149 in ->8 1150 else if isArchObjectCap cap 1151 then let cap = capCap cap 1152 in ->9 1153 else ->10 1154 1155case \x of (Zombie {}) -> (IRQControlCap) -> cap@(UntypedCap { capBlockSize = b }) -> (ReplyCap {}) -> (ArchObjectCap cap) -> cap -> ---> let cap = \x in 1156 if isZombie cap 1157 then ->1 1158 else if isIRQControlCap cap 1159 then ->2 1160 else if isUntypedCap cap 1161 then let b = capBlockSize cap 1162 in ->3 1163 else if isReplyCap cap 1164 then ->4 1165 else if isArchObjectCap cap 1166 then let cap = capCap cap 1167 in ->5 1168 else ->6 1169 1170case \x of ((Zombie { capZombieNumber = 0 }), _) -> ((Zombie { capZombiePtr = ptr }), False) -> (z@(Zombie { capZombiePtr = ptr, capZombieNumber = n }), True) -> (_, _) -> ---> let (\v0\, \v1\) = \x in 1171 if isZombie \v0\ \<and> capZombieNumber \v0\ = 0 1172 then ->1 1173 else if isZombie \v0\ \<and> \<not> \v1\ 1174 then let ptr = capZombiePtr \v0\ 1175 in ->2 1176 else if isZombie \v0\ \<and> \v1\ 1177 then let z = \v0\; ptr = capZombiePtr z; n = capZombieNumber z 1178 in ->3 1179 else ->4 1180 1181case \x of ((EndpointCap { capEPPtr = ptr }), final, _) -> ((NotificationCap { capNtfnPtr = ptr }), final, _) -> ((ReplyCap {}), _, _) -> (NullCap, _, _) -> (DomainCap, _, _) -> (_, _, True) -> ((CNodeCap { capCNodePtr = ptr, capCNodeBits = bits }), True, _) -> ((ThreadCap { capTCBPtr = tcb}), True, _) -> (z@(Zombie {}), True, _) -> ((ArchObjectCap { capCap = cap }), final, _) -> (cap@(IRQHandlerCap { capIRQ = irq }), True, _) -> ((Zombie {}), False, _) -> (_, _, _) -> ---> let (\v0\, \v1\, \v2\) = \x in 1182 if isEndpointCap \v0\ 1183 then let ptr = capEPPtr \v0\; final = \v1\ 1184 in ->1 1185 else if isNotificationCap \v0\ 1186 then let ptr = capNtfnPtr \v0\; final = \v1\ 1187 in ->2 1188 else if isReplyCap \v0\ 1189 then ->3 1190 else if isNullCap \v0\ 1191 then ->4 1192 else if isDomainCap \v0\ 1193 then ->5 1194 else if \v2\ 1195 then ->6 1196 else if isCNodeCap \v0\ \<and> \v1\ 1197 then let ptr = capCNodePtr \v0\; bits = capCNodeBits \v0\ 1198 in ->7 1199 else if isThreadCap \v0\ \<and> \v1\ 1200 then let tcb = capTCBPtr \v0\ 1201 in ->8 1202 else if isZombie \v0\ \<and> \v1\ 1203 then let z = \v0\ 1204 in ->9 1205 else if isArchObjectCap \v0\ 1206 then let cap = capCap \v0\; final = \v1\ 1207 in ->10 1208 else if isIRQHandlerCap \v0\ \<and> \v1\ 1209 then let irq = capIRQ \v0\; cap = \v0\ 1210 in ->11 1211 else if isZombie \v0\ \<and> \<not> \v1\ 1212 then ->12 1213 else ->13 1214 1215case \x of NullCap -> DomainCap -> (Zombie { capZombiePtr = ptr, capZombieType = tp }) -> (cap@EndpointCap { capEPPtr = ep, capEPBadge = b }) -> (ArchObjectCap cap) -> cap -> ---> let cap = \x in 1216 if isNullCap cap 1217 then ->1 1218 else if isDomainCap cap 1219 then ->2 1220 else if isZombie cap 1221 then let ptr = capZombiePtr cap; tp = capZombieType cap; 1222 n = capZombieNumber cap 1223 in ->3 1224 else if isEndpointCap cap 1225 then let ep = capEPPtr cap; b = capEPBadge cap 1226 in ->4 1227 else if isArchObjectCap cap 1228 then let cap = capCap cap 1229 in ->5 1230 else ->6 1231 1232case \x of NullCap -> DomainCap -> c@(UntypedCap {}) -> c@(EndpointCap {}) -> c@(NotificationCap {}) -> c@(ReplyCap {}) -> c@(CNodeCap {}) -> c@(ThreadCap {}) -> c@IRQControlCap -> c@(IRQHandlerCap {}) -> (ArchObjectCap {capCap = aoCap}) -> c@(Zombie {}) -> ---> let c = \x; aoCap = capCap \x in 1233 if isNullCap c 1234 then ->1 1235 else if isDomainCap c 1236 then ->2 1237 else if isUntypedCap c 1238 then ->3 1239 else if isEndpointCap c 1240 then ->4 1241 else if isNotificationCap c 1242 then ->5 1243 else if isReplyCap c 1244 then ->6 1245 else if isCNodeCap c 1246 then ->7 1247 else if isThreadCap c 1248 then ->8 1249 else if isIRQControlCap c 1250 then ->9 1251 else if isIRQHandlerCap c 1252 then ->10 1253 else if isArchObjectCap c 1254 then ->11 1255 else if isZombie c 1256 then ->12 1257 else undefined 1258 1259case \x of cap@(EndpointCap {capEPCanSend=True}) -> cap@(NotificationCap {capNtfnCanSend=True}) -> cap@(ReplyCap {capReplyMaster=False}) -> cap@(ThreadCap {}) -> DomainCap -> cap@(CNodeCap {}) -> cap@(UntypedCap {}) -> IRQControlCap -> (IRQHandlerCap { capIRQ = irq }) -> (ArchObjectCap cap) -> _ -> ---> let cap = \x in 1260 if isEndpointCap cap \<and> capEPCanSend cap 1261 then ->1 1262 else if isNotificationCap cap \<and> capNtfnCanSend cap 1263 then ->2 1264 else if isReplyCap cap \<and> \<not> capReplyMaster cap 1265 then ->3 1266 else if isThreadCap cap 1267 then ->4 1268 else if isDomainCap cap 1269 then ->5 1270 else if isCNodeCap cap 1271 then ->6 1272 else if isUntypedCap cap 1273 then ->7 1274 else if isIRQControlCap cap 1275 then ->8 1276 else if isIRQHandlerCap cap 1277 then let irq = capIRQ cap 1278 in ->9 1279 else if isArchObjectCap cap 1280 then let cap = capCap cap 1281 in ->10 1282 else ->11 1283 1284 1285case \x of (a@(UntypedCap {}), b) -> ((a@EndpointCap {}), (b@EndpointCap {})) -> ((a@NotificationCap {}), (b@NotificationCap {})) -> ((a@CNodeCap {}), (b@CNodeCap {})) -> ((a@ThreadCap {}), (b@ThreadCap {})) -> ((a@ReplyCap {}), (b@ReplyCap {})) -> (DomainCap, DomainCap) -> (IRQControlCap, IRQControlCap) -> (IRQControlCap, (IRQHandlerCap {})) -> ((IRQHandlerCap a), (IRQHandlerCap b)) -> ((ArchObjectCap a), (ArchObjectCap b)) -> (_, _) -> ---> let (a, b) = \x in 1286 if isUntypedCap a 1287 then ->1 1288 else if isEndpointCap a \<and> isEndpointCap b 1289 then ->2 1290 else if isNotificationCap a \<and> isNotificationCap b 1291 then ->3 1292 else if isCNodeCap a \<and> isCNodeCap b 1293 then ->4 1294 else if isThreadCap a \<and> isThreadCap b 1295 then ->5 1296 else if isReplyCap a \<and> isReplyCap b 1297 then ->6 1298 else if isDomainCap a \<and> isDomainCap b 1299 then ->7 1300 else if isIRQControlCap a \<and> isIRQControlCap b 1301 then ->8 1302 else if isIRQControlCap a \<and> isIRQHandlerCap b 1303 then ->9 1304 else if isIRQHandlerCap a \<and> isIRQHandlerCap b 1305 then (case (a, b) of 1306 (IRQHandlerCap a, IRQHandlerCap b) \<Rightarrow> ->10 1307 ) 1308 else if isArchObjectCap a \<and> isArchObjectCap b 1309 then (case (a, b) of 1310 (ArchObjectCap a, ArchObjectCap b) \<Rightarrow> ->11 1311 ) 1312 else ->12 1313 1314case \x of cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) -> ---> let cap = \x in 1315 if isPageDirectoryCap cap 1316 then ->1 1317 else if isPageTableCap cap 1318 then ->2 1319 else if isPageCap cap 1320 then ->3 1321 else if isASIDControlCap cap 1322 then ->4 1323 else if isASIDPoolCap cap 1324 then ->5 1325 else undefined 1326 1327case \x of (c@PageTableCap { capPTMappedAddress = Just _ }) -> (PageTableCap { capPTMappedAddress = Nothing }) -> (c@PageDirectoryCap { capPDMappedAddress = Just _ }) -> (PageDirectoryCap { capPDMappedAddress = Nothing }) -> (c@PDPointerTableCap { capPDPTMappedAddress = Just _ }) -> (PDPointerTableCap { capPDPTMappedAddress = Nothing }) -> (c@PML4Cap { capPML4MappedASID = Just _ }) -> (PML4Cap { capPML4MappedASID = Nothing }) -> (c@PageCap {}) -> c@ASIDControlCap -> (c@ASIDPoolCap {}) -> (c@IOPortCap {}) -> IOPortControlCap -> ---> let c = \x in 1328 if isPageTableCap c \<and> capPTMappedAddress c \<noteq> None 1329 then ->1 1330 else if isPageTableCap c \<and> capPTMappedAddress c = None 1331 then ->2 1332 else if isPageDirectoryCap c \<and> capPDMappedAddress c \<noteq> None 1333 then ->3 1334 else if isPageDirectoryCap c \<and> capPDMappedAddress c = None 1335 then ->4 1336 else if isPDPointerTableCap c \<and> capPDPTMappedAddress c \<noteq> None 1337 then ->5 1338 else if isPDPointerTableCap c \<and> capPDPTMappedAddress c = None 1339 then ->6 1340 else if isPML4Cap c \<and> capPML4MappedASID c \<noteq> None 1341 then ->7 1342 else if isPML4Cap c \<and> capPML4MappedASID c = None 1343 then ->8 1344 else if isPageCap c 1345 then ->9 1346 else if isASIDControlCap c 1347 then ->10 1348 else if isASIDPoolCap c 1349 then ->11 1350 else if isIOPortCap c 1351 then ->12 1352 else if isIOPortControlCap c 1353 then ->13 1354 else undefined 1355 1356case \x of (c@IOPortCap {}) -> c -> ---> let c = \x in 1357 if isIOPortCap c 1358 then ->1 1359 else ->2 1360 1361case \x of (cap@PageCap {}) -> (cap@PageTableCap { capPTBasePtr = ptr }) -> (cap@PageDirectoryCap { capPDBasePtr = ptr }) -> (cap@PDPointerTableCap { capPDPTBasePtr = ptr }) -> (cap@PML4Cap { capPML4BasePtr = ptr }) -> (cap@IOPortCap {}) -> (cap@IOSpaceCap) -> (cap@IOPageTableCap { capIOPTBasePtr = ptr }) -> ASIDControlCap -> (cap@ASIDPoolCap { capASIDBase = base, capASIDPool = ptr }) -> ---> let cap = \x in 1362 if isPageCap cap 1363 then ->1 1364 else if isPageTableCap cap 1365 then let ptr = capPTBasePtr cap 1366 in ->2 1367 else if isPageDirectoryCap cap 1368 then let ptr = capPDBasePtr cap 1369 in ->3 1370 else if isPDPointerTableCap cap 1371 then let ptr = capPDPTBasePtr cap 1372 in ->4 1373 else if isPML4Cap cap 1374 then let ptr = capPML4BasePtr cap 1375 in ->5 1376 else if isIOPortCap cap 1377 then ->6 1378 else if isIOSpaceCap cap 1379 then ->7 1380 else if isIOPageTableCap cap 1381 then let ptr = capIOPTBasePtr cap 1382 in ->8 1383 else if isASIDControlCap cap 1384 then ->9 1385 else if isASIDPoolCap cap 1386 then let base = capASIDBase cap; ptr = capASIDPool cap 1387 in ->10 1388 else undefined 1389 1390case \x of (ArchInvocationLabel ArchLabels.X64IRQIssueIRQHandlerIOAPIC, index:depth:ioapic:pin:level:polarity:irqW:_, cnode:_) -> (ArchInvocationLabel ArchLabels.X64IRQIssueIRQHandlerIOAPIC, _, _) -> (ArchInvocationLabel ArchLabels.X64IRQIssueIRQHandlerMSI, index:depth:pciBus:pciDev:pciFunc:handle:irqW:_, cnode:_) -> (ArchInvocationLabel ArchLabels.X64IRQIssueIRQHandlerMSI, _, _) -> _ -> ---> let (label, args, extraCaps) = \x in 1391 case (label, args, extraCaps) of 1392 (ArchInvocationLabel X64IRQIssueIRQHandlerIOAPIC, 1393 index#depth#ioapic#pin#level#polarity#irqW#_, cnode#_) => ->1 1394 | (ArchInvocationLabel X64IRQIssueIRQHandlerIOAPIC, _, _) => ->2 1395 | (ArchInvocationLabel X64IRQIssueIRQHandlerMSI, 1396 index#depth#pciBus#pciDev#pciFunc#handle#irqW#_, cnode#_) => ->3 1397 | (ArchInvocationLabel X64IRQIssueIRQHandlerMSI, _, _) => ->4 1398 | _ => ->5 1399 1400case \x of (ArchInv.IssueIRQHandlerIOAPIC (IRQ irq) destSlot srcSlot ioapic pin level polarity vector) -> (ArchInv.IssueIRQHandlerMSI (IRQ irq) destSlot srcSlot pciBus pciDev pciFunc handle) -> ---> let inv = \x in 1401 case inv of 1402 (IssueIRQHandlerIOAPIC irq destSlot srcSlot ioapic pin level polarity vector) => ->1 1403 | (IssueIRQHandlerMSI irq destSlot srcSlot pciBus pciDev pciFunc handle) => ->2 1404 1405case \x of (cap@PageCap {}) -> (cap@PageTableCap { capPTBasePtr = ptr }) -> (cap@PageDirectoryCap { capPDBasePtr = ptr }) -> (cap@PDPointerTableCap { capPDPTBasePtr = ptr }) -> (cap@PML4Cap { capPML4BasePtr = ptr }) -> (cap@IOPortCap {}) -> (cap@IOSpaceCap {}) -> (cap@IOPageTableCap { capIOPTBasePtr = ptr }) -> ASIDControlCap -> (cap@ASIDPoolCap { capASIDBase = base, capASIDPool = ptr }) -> ---> let cap = \x in 1406 if isPageCap cap 1407 then ->1 1408 else if isPageTableCap cap 1409 then let ptr = capPTBasePtr cap in ->2 1410 else if isPageDirectoryCap cap 1411 then let ptr = capPDBasePtr cap in ->3 1412 else if isPDPointerTableCap cap 1413 then let ptr = capPDPTBasePtr cap in ->4 1414 else if isPML4Cap cap 1415 then let ptr = capPML4BasePtr cap in ->5 1416 else if isIOPortCap cap 1417 then ->6 1418 else if isIOSpaceCap cap 1419 then ->7 1420 else if isIOPageTableCap cap 1421 then let ptr = capIOPTBasePtr cap in ->8 1422 else if isASIDControlCap cap 1423 then ->9 1424 else if isASIDPoolCap cap 1425 then let base = capASIDBase cap; ptr = capASIDPool cap in ->10 1426 else undefined 1427 1428case \x of Arch.Types.APIObjectType _ -> Arch.Types.SmallPageObject -> Arch.Types.LargePageObject -> Arch.Types.HugePageObject -> Arch.Types.PageTableObject -> Arch.Types.PageDirectoryObject -> Arch.Types.PDPointerTableObject -> Arch.Types.PML4Object -> ---> let t = \x in 1429 case t of 1430 APIObjectType _ => ->1 1431 | SmallPageObject => ->2 1432 | LargePageObject => ->3 1433 | HugePageObject => ->4 1434 | PageTableObject => ->5 1435 | PageDirectoryObject => ->6 1436 | PDPointerTableObject => ->7 1437 | PML4Object => ->8 1438 1439case \x of ((a@PageCap {}), (b@PageCap {})) -> ((a@PageTableCap {}), (b@PageTableCap {})) -> ((a@PageDirectoryCap {}), (b@PageDirectoryCap {})) -> ((a@PDPointerTableCap {}), (b@PDPointerTableCap {})) -> ((a@PML4Cap {}), (b@PML4Cap {})) -> (ASIDControlCap, ASIDControlCap) -> ((a@ASIDPoolCap {}), (b@ASIDPoolCap {})) -> ((a@IOPortCap {}), (b@IOPortCap {})) -> (IOPortControlCap, IOPortControlCap) -> (IOPortControlCap, (IOPortCap {})) -> (_, _) -> ---> let (a,b) = \x in 1440 if isPageCap a \<and> isPageCap b 1441 then ->1 1442 else if isPageTableCap a \<and> isPageTableCap b 1443 then ->2 1444 else if isPageDirectoryCap a \<and> isPageDirectoryCap b 1445 then ->3 1446 else if isPDPointerTableCap a \<and> isPDPointerTableCap b 1447 then ->4 1448 else if isPML4Cap a \<and> isPML4Cap b 1449 then ->5 1450 else if isASIDControlCap a \<and> isASIDControlCap b 1451 then ->6 1452 else if isASIDPoolCap a \<and> isASIDPoolCap b 1453 then ->7 1454 else if isIOPortCap a \<and> isIOPortCap b 1455 then ->8 1456 else if isIOPortControlCap a \<and> isIOPortControlCap b 1457 then ->9 1458 else if isIOPortControlCap a \<and> isIOPortCap b 1459 then ->10 1460 else ->11 1461 1462 1463case \x of (oper@(InvokeIOPort _)) -> (oper@(InvokeIOPortControl _)) -> oper -> ---> let oper = \x in 1464 case oper of 1465 InvokeIOPort _ => ->1 1466 | InvokeIOPortControl _ => ->2 1467 | _ => ->3 1468 1469case \x of (cap@PageCap {}) -> _ -> ---> let cap = \x in 1470 if isPageCap cap 1471 then ->1 1472 else ->2 1473 1474case \x of (ArchInvocationLabel X64IOPortControlIssue, f:l:index:depth:_, cnode:_) -> (ArchInvocationLabel X64IOPortControlIssue, _, _) -> _ -> ---> let (label, args, extraCaps) = \x in 1475 case (label, args, extraCaps) of 1476 (ArchInvocationLabel X64IOPortControlIssue, f#l#index#depth#_, cnode#_) => ->1 1477 | (ArchInvocationLabel X64IOPortControlIssue, _, _) => ->2 1478 | _ => ->3 1479 1480case \x of (ArchInvocationLabel X64PDPTMap, vaddr':attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PDPTMap, _, _) -> (ArchInvocationLabel X64PDPTUnmap, _, _) -> _ -> ---> let (label, args, extraCaps) = \x in 1481 case (label, args, extraCaps) of 1482 (ArchInvocationLabel X64PDPTMap, vaddr'#attr#_, (vspaceCap,_)#_) => ->1 1483 | (ArchInvocationLabel X64PDPTMap, _, _) => ->2 1484 | (ArchInvocationLabel X64PDPTUnmap, _, _) => ->3 1485 | _ => ->4 1486 1487case \x of (ArchInvocationLabel X64PageDirectoryMap, vaddr':attr:_, (pml4Cap,_):_) -> (ArchInvocationLabel X64PageDirectoryMap, _, _) -> (ArchInvocationLabel X64PageDirectoryUnmap, _, _) -> _ -> ---> let (label, args, extraCaps) = \x in 1488 case (label, args, extraCaps) of 1489 (ArchInvocationLabel X64PageDirectoryMap, vaddr'#attr#_, (pml4Cap,_)#_) => ->1 1490 | (ArchInvocationLabel X64PageDirectoryMap, _, _) => ->2 1491 | (ArchInvocationLabel X64PageDirectoryUnmap, _, _) => ->3 1492 | _ => ->4 1493 1494case \x of (ArchInvocationLabel X64PageTableMap, vaddr':attr:_, (pml4Cap,_):_) -> (ArchInvocationLabel X64PageTableMap, _, _) -> (ArchInvocationLabel X64PageTableUnmap, _, _) -> _ -> --->let (label, args, extraCaps) = \x in 1495 case (label, args, extraCaps) of 1496 (ArchInvocationLabel X64PageTableMap, vaddr'#attr#_, (pml4Cap,_)#_) => ->1 1497 | (ArchInvocationLabel X64PageTableMap, _, _) => ->2 1498 | (ArchInvocationLabel X64PageTableUnmap, _, _) => ->3 1499 | _ => ->4 1500 1501 1502case \x of (ArchInvocationLabel X64ASIDControlMakePool, index:depth:_, (untyped,parentSlot):(croot,_):_) -> (ArchInvocationLabel X64ASIDControlMakePool, _, _) -> _ -> ---> let (label, args, extraCaps) = \x in 1503 case (label, args, extraCaps) of 1504 (ArchInvocationLabel X64ASIDControlMakePool, index#depth#_, (untyped,parentSlot)#(croot,_):_) => ->1 1505 | (ArchInvocationLabel X64ASIDControlMakePool, _, _) => ->2 1506 | _ => ->3 1507 1508case \x of (ArchInvocationLabel X64ASIDPoolAssign, (vspaceCap,vspaceCapSlot):_) -> (ArchInvocationLabel X64ASIDPoolAssign, _) -> _ -> ---> let (label, extraCaps) = \x in 1509 case (label, extraCaps) of 1510 (ArchInvocationLabel X64ASIDPoolAssign, (vspaceCap,vspaceCapSlot)#_) => ->1 1511 | (ArchInvocationLabel X64ASIDPoolAssign, _) => ->2 1512 | _ => ->3 1513 1514case \x of cap@(PDPointerTableCap {}) -> cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) -> _ -> ---> let cap = \x in 1515 if isPDPointerTableCap cap 1516 then ->1 1517 else if isPageDirectoryCap cap 1518 then ->2 1519 else if isPageTableCap cap 1520 then ->3 1521 else if isPageCap cap 1522 then ->4 1523 else if isASIDPoolCap cap 1524 then ->5 1525 else ->6 1526 1527case \x of (cap@(IOPortCap { capIOPortFirstPort = first_allowed, capIOPortLastPort = last_allowed })) -> _ -> ---> let cap = \x in 1528 if isIOPortCap cap 1529 then let first_allowed = capIOPortFirstPort cap; last_allowed = capIOPortLastPort cap in ->1 1530 else ->2 1531 1532case \x of (ArchInvocationLabel X64IOPortIn8, port':_) -> (ArchInvocationLabel X64IOPortIn8, _) -> (ArchInvocationLabel X64IOPortIn16, port':_) -> (ArchInvocationLabel X64IOPortIn16, _) -> (ArchInvocationLabel X64IOPortIn32, port':_) -> (ArchInvocationLabel X64IOPortIn32, _) -> (ArchInvocationLabel X64IOPortOut8, port':out:_) -> (ArchInvocationLabel X64IOPortOut8, _) -> (ArchInvocationLabel X64IOPortOut16, port':out:_) -> (ArchInvocationLabel X64IOPortOut16, _) -> (ArchInvocationLabel X64IOPortOut32, port':out:_) -> (ArchInvocationLabel X64IOPortOut32, _) -> (_, _) -> ---> let (label, args) = \x in 1533 case (label, args) of 1534 (ArchInvocationLabel X64IOPortIn8, port'#_) => ->1 1535 | (ArchInvocationLabel X64IOPortIn8, _) => ->2 1536 | (ArchInvocationLabel X64IOPortIn16, port'#_) => ->3 1537 | (ArchInvocationLabel X64IOPortIn16, _) => ->4 1538 | (ArchInvocationLabel X64IOPortIn32, port'#_) => ->5 1539 | (ArchInvocationLabel X64IOPortIn32, _) => ->6 1540 | (ArchInvocationLabel X64IOPortOut8, port'#out:_) => ->7 1541 | (ArchInvocationLabel X64IOPortOut8, _) => ->8 1542 | (ArchInvocationLabel X64IOPortOut16, port'#out#_) => ->9 1543 | (ArchInvocationLabel X64IOPortOut16, _) => ->10 1544 | (ArchInvocationLabel X64IOPortOut32, port'#out#_) => ->11 1545 | (ArchInvocationLabel X64IOPortOut32, _) => ->12 1546 | _ => ->13 1547 1548case \x of cap@(IOPortCap {}) -> _ -> ---> let cap = \x in 1549 if isIOPortCap cap 1550 then ->1 1551 else ->2 1552 1553case \x of cap@(IOPortCap {}) -> IOPortControlCap -> _ -> ---> let cap = \x in 1554 if isIOPortCap cap 1555 then ->1 1556 else if isIOPortControlCap cap 1557 then ->2 1558 else ->3 1559 1560case \x of (cap @ (CNodeCap {})) -> (cap @ (ThreadCap {})) -> (cap @ (Zombie {})) -> _ -> ---> let cap = \x in 1561 if isCNodeCap cap 1562 then ->1 1563 else if isThreadCap cap 1564 then ->2 1565 else if isZombie cap 1566 then ->3 1567 else ->4 1568 1569case \x of ArchInv.IOPortIn8 -> ArchInv.IOPortIn16 -> ArchInv.IOPortIn32 -> ArchInv.IOPortOut8 w -> ArchInv.IOPortOut16 w -> ArchInv.IOPortOut32 w -> ---> let port_data = \x in 1570 case port_data of 1571 IOPortIn8 => ->1 1572 | IOPortIn16 => ->2 1573 | IOPortIn32 => ->3 1574 | IOPortOut8 w => ->4 1575 | IOPortOut16 w => ->5 1576 | IOPortOut32 w => ->6 1577 1578case \x of (ArchInvocationLabel X64PageMap, vaddr:rightsMask:attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PageMap, _, _) -> (ArchInvocationLabel X64PageRemap, rightsMask:attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PageRemap, _, _) -> (ArchInvocationLabel X64PageUnmap, _, _) -> (ArchInvocationLabel X64PageGetAddress, _, _) -> _ -> ---> let (ilabel, args, extraCaps) = \x in 1579 case (ilabel, args, extraCaps) of 1580 (ArchInvocationLabel X64PageMap, vaddr#rightsMask#attr#_, (vspaceCap, _)#_) => ->1 1581 | (ArchInvocationLabel X64PageMap, _, _) => ->2 1582 | (ArchInvocationLabel X64PageRemap, rightsMask#attr#_, (vspaceCap, _)#_) => ->3 1583 | (ArchInvocationLabel X64PageRemap, _, _) => ->4 1584 | (ArchInvocationLabel X64PageUnmap, _, _) => ->5 1585 | (ArchInvocationLabel X64PageGetAddress, _, _) => ->6 1586 | _ => ->7 1587 1588case \x of (ArchInvocationLabel X64IOPageTableMap, ioaddr:_, (iospaceCap,_):_) -> (ArchInvocationLabel X64IOPageTableMap, _, _) -> (ArchInvocationLabel X64IOPageTableUnmap, _, _) -> _ -> ---> let (ilabel, args, extraCaps) = \x in 1589 case (ilabel, args, extraCaps) of 1590 (ArchInvocationLabel X64IOPageTableMap, ioaddr#_, (iospaceCap,_)#_) => ->1 1591 | (ArchInvocationLabel X64IOPageTableMap, _, _) => ->2 1592 | (ArchInvocationLabel X64IOPageTableUnmap, _, _) => ->3 1593 | _ => ->4 1594 1595case \x of (ArchInvocationLabel X64PageMapIO, rw:ioaddr:_, (iospaceCap,_):_) -> (ArchInvocationLabel X64PageMapIO, _, _) -> (ArchInvocationLabel X64PageUnmap, _, _) -> _ -> ---> let (ilabel, args, extraCaps) = \x in 1596 case (ilabel, args, extraCaps) of 1597 (ArchInvocationLabel X64PageMapIO, rw:ioaddr#_, (iospaceCap,_)#_) => ->1 1598 | (ArchInvocationLabel X64PageMapIO, _, _) => ->2 1599 | (ArchInvocationLabel X64PageUnmap, _, _) => ->3 1600 | _ => ->4 1601 1602case \x of cap@(PDPointerTableCap {}) -> _ -> ---> let cap = \x in 1603 if isPDPointerTableCap cap 1604 then ->1 1605 else ->2 1606 1607case \x of cap@(PageDirectoryCap {}) -> _ -> ---> let cap = \x in 1608 if isPageDirectoryCap cap 1609 then ->1 1610 else ->2 1611 1612case \x of cap@(PageTableCap {}) -> _ -> ---> let cap = \x in 1613 if isPageTableCap cap 1614 then ->1 1615 else ->2 1616 1617case \x of cap@(ASIDPoolCap {}) -> _ -> ---> let cap = \x in 1618 if isASIDPoolCap cap 1619 then ->1 1620 else ->2 1621 1622case \x of cap@(PageCap {}) -> cap@(PDPointerTableCap {}) -> cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(ASIDControlCap {}) -> cap@(ASIDPoolCap {}) -> cap@(IOPageTableCap {}) -> cap@(PML4Cap {}) -> _ -> ---> let cap = \x in 1623 if isPageCap cap 1624 then ->1 1625 else if isPDPointerTableCap cap 1626 then ->2 1627 else if isPageDirectoryCap cap 1628 then ->3 1629 else if isPageTableCap cap 1630 then ->4 1631 else if isASIDControlCap cap 1632 then ->5 1633 else if isASIDPoolCap cap 1634 then ->6 1635 else if isIOPageTableCap cap 1636 then ->7 1637 else if isPML4Cap cap 1638 then ->8 1639 else ->9 1640 1641case \x of cap@(PageCap {}) -> cap@(PDPointerTableCap {}) -> cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(ASIDControlCap {}) -> cap@(ASIDPoolCap {}) -> (PML4Cap {}) -> _ -> ---> let cap = \x in 1642 if isPageCap cap 1643 then ->1 1644 else if isPDPointerTableCap cap 1645 then ->2 1646 else if isPageDirectoryCap cap 1647 then ->3 1648 else if isPageTableCap cap 1649 then ->4 1650 else if isASIDControlCap cap 1651 then ->5 1652 else if isASIDPoolCap cap 1653 then ->6 1654 else if isPML4Cap cap 1655 then ->7 1656 else ->8 1657 1658 1659case \x of cap@(IOPageTableCap {}) -> _ -> ---> let cap = \x in 1660 if isIOPageTableCap 1661 then ->1 1662 else ->2 1663 1664case \x of (cap@UntypedCap {}) -> _ -> ---> let cap = \x in 1665 if isUntypedCap cap 1666 then ->1 1667 else ->2 1668 1669case \x of cap@(PageCap {}) -> _ -> ---> let cap = \x in 1670 if isPageCap cap 1671 then ->1 1672 else ->2 1673 1674case \x of (PageMap asid cap ctSlot entries) -> (PageRemap entries) -> (PageUnmap cap ctSlot) -> (PageIOMap cap cptr vtdpte slot) -> (PageIOUnmap (ArchObjectCap cap@PageCap {}) ctSlot) -> (PageIOUnmap _ _) -> (PageGetAddr ptr) -> ---> let \v0\ = \x in 1675 case \v0\ of 1676 PageMap asid cap ct ctSlot entries => ->1 1677 | PageRemap entries => ->2 1678 | PageUnmap cap ctSlot => ->3 1679 | PageIOMap cap cptr ctdpte slot => ->4 1680 | PageIOUnmap (ArchObjectCap cap) ctSlot => 1681 if isPageCap cap 1682 then ->5 1683 else ->6 1684 | PageIOUnmap _ _ => ->6 1685 | PageGetAddr ptr => ->7 1686 1687case \x of UntypedCap {} | capBlockSize untyped == objBits pool -> _ -> ---> let \v0\ = \x in 1688 if isUntypedCap \v0\ \<and> capBlockSize \v0\ == objBits pool 1689 then ->1 1690 else ->2 1691 1692case \x of (cap@IOPageTableCap {}) -> _ -> ---> let cap = \x in 1693 if isIOPageTableCap cap 1694 then ->1 1695 else ->2 1696 1697case \x of cap@(PageCap {}) -> _ -> ---> let cap = \x in 1698 if isPageCap cap 1699 then ->1 1700 else ->2 1701 1702case \x of (PageMap asid cap ctSlot entries) -> (PageRemap entries) -> (PageUnmap cap ctSlot) -> (PageIOMap cap cptr vtdpte slot) -> (PageIOUnmap (ArchObjectCap cap@PageCap {}) ctSlot) -> (PageIOUnmap _ _) -> (PageGetAddr ptr) -> ---> let \v0\ = \x in 1703 case \v0\ of 1704 PageMap asid cap ct ctSlot entries => ->1 1705 | PageRemap entries => ->2 1706 | PageUnmap cap ctSlot => ->3 1707 | PageIOMap cap cptr ctdpte slot => ->4 1708 | PageIOUnmap (ArchObjectCap cap) ctSlot => 1709 if isPageCap cap 1710 then ->5 1711 else ->6 1712 | PageIOUnmap _ _ => ->6 1713 | PageGetAddr ptr => ->7 1714 1715case \x of UntypedCap {} | capBlockSize untyped == objBits pool -> _ -> ---> let \v0\ = \x in 1716 if isUntypedCap \v0\ \<and> capBlockSize \v0\ == objBits pool 1717 then ->1 1718 else ->2 1719 1720case \x of (cap@IOPageTableCap {}) -> _ -> ---> let cap = \x in 1721 if isIOPageTableCap cap 1722 then ->1 1723 else ->2 1724 1725case \x of (X64NoHypFaults) -> ---> let hyp = \x in 1726 case hyp of X64NoHypFaults => ->1 1727 1728case \x of ((a@PageCap { capVPBasePtr = ptrA }), (b@PageCap {})) -> (IOPortControlCap, (IOPortCap {})) -> (a, b) -> ---> let (a, b) = \x in 1729 if isPageCap a \<and> isPageCap b 1730 then let ptrA = capVPBasePtr a 1731 in ->1 1732 else if isIOPortControlCap a \<and> isIOPortCap b 1733 then -> 2 1734 else ->3 1735 1736 1737 1738 1739case \x of cap@(VCPUCap {}) -> _ -> ---> let cap = \x in 1740 if isVCPUCap cap then -> 1 1741 else ->2 1742 1743case \x of ((field:_), cap@(VCPUCap {})) -> (_, _) -> ---> let (ls, cap) = \x in 1744 if isVCPUCap cap \<and> length ls > 0 1745 then let field = ls !! 0 in ->1 1746 else ->2 1747 1748case \x of ((field:val:_), cap@(VCPUCap {})) -> (_, _) -> ---> let (ls, cap) = \x in 1749 if isVCPUCap cap \<and> length ls > 1 1750 then let field = ls !! 0; val = ls !! 1 1751 in ->1 1752 else ->2 1753 1754case \x of (c@PageTableCap { capPTMappedAddress = Just _ }) -> (PageTableCap { capPTMappedAddress = Nothing }) -> (c@PageDirectoryCap { capPDMappedASID = Just _ }) -> (PageDirectoryCap { capPDMappedASID = Nothing }) -> (c@PageCap {}) -> c@ASIDControlCap -> (c@ASIDPoolCap {}) -> (c@VCPUCap {}) -> ---> let c = \x in 1755 if isPageTableCap c \<and> capPTMappedAddress c \<noteq> None 1756 then ->1 1757 else if isPageTableCap c \<and> capPTMappedAddress c = None 1758 then ->2 1759 else if isPageDirectoryCap c \<and> capPDMappedASID c \<noteq> None 1760 then ->3 1761 else if isPageDirectoryCap c \<and> capPDMappedASID c = None 1762 then ->4 1763 else if isPageCap c 1764 then ->5 1765 else if isASIDControlCap c 1766 then ->6 1767 else if isASIDPoolCap c 1768 then ->7 1769 else if isVCPUCap c 1770 then ->8 1771 else undefined 1772 1773case \x of ((ASIDPoolCap { capASIDBase = b, capASIDPool = ptr }), True) -> ((PageDirectoryCap { capPDMappedASID = Just a, capPDBasePtr = ptr }), True) -> ((PageTableCap { capPTMappedAddress = Just (a, v), capPTBasePtr = ptr }), True) -> ((cap@PageCap { capVPMappedAddress = Just (a, v), capVPSize = s, capVPBasePtr = ptr }), _) -> ((VCPUCap {}), _) -> (_, _) -> ---> let (cap, bl) = \x in 1774 if isASIDPoolCap cap \<and> bl 1775 then let b = capASIDBase cap; ptr = capASIDPool cap 1776 in ->1 1777 else if isPageDirectoryCap cap \<and> bl \<and> capPDMappedASID cap \<noteq> None 1778 then let a = the (capPDMappedASID cap); ptr = capPDBasePtr cap 1779 in ->2 1780 else if isPageTableCap cap \<and> bl \<and> capPTMappedAddress cap \<noteq> None 1781 then let (a, v) = the (capPTMappedAddress cap); ptr = capPTBasePtr cap 1782 in ->3 1783 else if isPageCap cap \<and> capVPMappedAddress cap \<noteq> None 1784 then let (a, v) = the (capVPMappedAddress cap); s = capVPSize cap; ptr = capVPBasePtr cap in ->4 1785 else if isVCPUCap cap then ->5 1786 else ->6 1787 1788 1789case \x of (cap@PageCap {}) -> (cap@PageTableCap { capPTBasePtr = ptr }) -> (cap@PageDirectoryCap { capPDBasePtr = ptr }) -> ASIDControlCap -> (cap@ASIDPoolCap { capASIDBase = base, capASIDPool = ptr }) -> (VCPUCap {}) -> ---> let cap = \x in 1790 if isPageCap cap 1791 then ->1 1792 else if isPageTableCap cap 1793 then let ptr = capPTBasePtr cap 1794 in ->2 1795 else if isPageDirectoryCap cap 1796 then let ptr = capPDBasePtr cap 1797 in ->3 1798 else if isASIDControlCap cap 1799 then ->4 1800 else if isASIDPoolCap cap 1801 then let base = capASIDBase cap; ptr = capASIDPool cap 1802 in ->5 1803 else if isVCPUCap cap 1804 then ->6 1805 else undefined 1806 1807case \x of ((a@PageCap {}), (b@PageCap {})) -> ((a@PageTableCap {}), (b@PageTableCap {})) -> ((a@PageDirectoryCap {}), (b@PageDirectoryCap {})) -> (ASIDControlCap, ASIDControlCap) -> ((a@ASIDPoolCap {}), (b@ASIDPoolCap {})) -> ((a@VCPUCap {}), (b@VCPUCap {})) -> (_, _) -> ---> let (a, b) = \x in 1808 if isPageCap a \<and> isPageCap b 1809 then ->1 1810 else if isPageTableCap a \<and> isPageTableCap b 1811 then ->2 1812 else if isPageDirectoryCap a \<and> isPageDirectoryCap b 1813 then ->3 1814 else if isASIDControlCap a \<and> isASIDControlCap b 1815 then ->4 1816 else if isASIDPoolCap a \<and> isASIDPoolCap b 1817 then ->5 1818 else if isVCPUCap a \<and> isVCPUCap b 1819 then ->6 1820 else ->7 1821 1822case \x of Arch.Types.APIObjectType _ -> Arch.Types.SmallPageObject -> Arch.Types.LargePageObject -> Arch.Types.SectionObject -> Arch.Types.SuperSectionObject -> Arch.Types.PageTableObject -> Arch.Types.PageDirectoryObject -> Arch.Types.VCPUObject -> ---> case \x of 1823 Arch.Types.APIObjectType \v0\ \<Rightarrow> ->1 | Arch.Types.SmallPageObject \<Rightarrow> ->2 | Arch.Types.LargePageObject \<Rightarrow> ->3 | Arch.Types.SectionObject \<Rightarrow> ->4 | Arch.Types.SuperSectionObject \<Rightarrow> ->5 | Arch.Types.PageTableObject \<Rightarrow> ->6 | Arch.Types.PageDirectoryObject \<Rightarrow> ->7 | Arch.Type.VCPUObject \<Rightarrow> -> 8 1824 1825case \x of ArchInv.InvokeVCPU iv -> _ -> ---> let inv = \x 1826 in case inv of ArchInv.InvokeVCPU iv \<Rightarrow> ->1 | _ \<Rightarrow> ->2 1827 1828case \x of ((mr0:mr1:_), cap@(VCPUCap {})) -> (_, _) -> ---> let (ls, cap) = \x in 1829 if isVCPUCap cap \<and> length ls > 1 1830 then let mr0 = ls !! 0; mr1 = ls !! 1 1831 in ->1 1832 else ->2 1833 1834 1835case \x of cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) -> (VCPUCap {}) -> ---> let cap = \x in 1836 if isPageDirectoryCap cap 1837 then ->1 1838 else if isPageTableCap cap 1839 then ->2 1840 else if isPageCap cap 1841 then ->3 1842 else if isASIDControlCap cap 1843 then ->4 1844 else if isASIDPoolCap cap 1845 then ->5 1846 else if isVCPUCap cap 1847 then ->6 1848 else undefined 1849 1850case \x of ((ASIDPoolCap { capASIDBase = b, capASIDPool = ptr }), True) -> ((PageDirectoryCap { capPDMappedASID = Just a, capPDBasePtr = ptr }), True) -> ((PageTableCap { capPTMappedAddress = Just (a, v), capPTBasePtr = ptr }), True) -> ((cap@PageCap { capVPMappedAddress = Just (a, v), capVPSize = s, capVPBasePtr = ptr }), _) -> ((VCPUCap { capVCPUPtr = vcpu }), True) -> (_, _) -> ---> let (cap, bl) = \x in 1851 if isASIDPoolCap cap \<and> bl 1852 then let b = capASIDBase cap; ptr = capASIDPool cap 1853 in ->1 1854 else if isPageDirectoryCap cap \<and> bl \<and> capPDMappedASID cap \<noteq> None 1855 then let a = the (capPDMappedASID cap); ptr = capPDBasePtr cap 1856 in ->2 1857 else if isPageTableCap cap \<and> bl \<and> capPTMappedAddress cap \<noteq> None 1858 then let (a, v) = the (capPTMappedAddress cap); ptr = capPTBasePtr cap 1859 in ->3 1860 else if isPageCap cap \<and> capVPMappedAddress cap \<noteq> None 1861 then let (a, v) = the (capVPMappedAddress cap); s = capVPSize cap; ptr = capVPBasePtr cap 1862 in ->4 1863 else if isVCPUCap cap \<and> bl 1864 then let vcpu = capVCPUPtr cap 1865 in ->5 1866 else ->6 1867 1868 1869case \x of (cap@PageCap {}) -> (cap@PageTableCap { capPTBasePtr = ptr }) -> (cap@PageDirectoryCap { capPDBasePtr = ptr }) -> ASIDControlCap -> (cap@ASIDPoolCap { capASIDBase = base, capASIDPool = ptr }) -> (cap@VCPUCap { capVCPUPtr = vcpu }) -> ---> let cap = \x in 1870 if isPageCap cap 1871 then ->1 1872 else if isPageTableCap cap 1873 then let ptr = capPTBasePtr cap 1874 in ->2 1875 else if isPageDirectoryCap cap 1876 then let ptr = capPDBasePtr cap 1877 in ->3 1878 else if isASIDControlCap cap 1879 then ->4 1880 else if isASIDPoolCap cap 1881 then let base = capASIDBase cap; ptr = capASIDPool cap 1882 in ->5 1883 else if isVCPUCap cap 1884 then let vcpu = capVCPUPtr cap 1885 in ->6 1886 else undefined 1887 1888 1889case \x of ((ASIDPoolCap { capASIDBase = b, capASIDPool = ptr }), True) -> ((PageDirectoryCap { capPDMappedASID = Just a, capPDBasePtr = ptr }), True) -> ((PageTableCap { capPTMappedAddress = Just (a, v), capPTBasePtr = ptr }), True) -> ((cap@PageCap { capVPMappedAddress = Just (a, v), capVPSize = s, capVPBasePtr = ptr }), _) -> ((VCPUCap { capVCPUPtr = vcpu }), True) -> (_, _) -> ---> let (cap, bl) = \x in 1890 if isASIDPoolCap cap \<and> bl 1891 then let b = capASIDBase cap; ptr = capASIDPool cap 1892 in ->1 1893 else if isPageDirectoryCap cap \<and> bl \<and> capPDMappedASID cap \<noteq> None 1894 then let a = the (capPDMappedASID cap); ptr = capPDBasePtr cap 1895 in ->2 1896 else if isPageTableCap cap \<and> bl \<and> capPTMappedAddress cap \<noteq> None 1897 then let (a, v) = the (capPTMappedAddress cap); ptr = capPTBasePtr cap 1898 in ->3 1899 else if isPageCap cap \<and> capVPMappedAddress cap \<noteq> None 1900 then let (a, v) = the (capVPMappedAddress cap); s = capVPSize cap; ptr = capVPBasePtr cap 1901 in ->4 1902 else if isVCPUCap cap \<and> bl 1903 then let vcpu = capVCPUPtr cap 1904 in ->5 1905 else ->6 1906 1907case \x of ((ASIDPoolCap { capASIDBase = b, capASIDPool = ptr }), True) -> ((PageDirectoryCap { capPDMappedASID = Just a, capPDBasePtr = ptr }), True) -> ((PageTableCap { capPTMappedAddress = Just (a, v), capPTBasePtr = ptr }), True) -> ((cap@PageCap { capVPMappedAddress = Just (a, v), capVPSize = s, capVPBasePtr = ptr }), _) -> (_, _) -> ---> let (cap, bl) = \x in 1908 if isASIDPoolCap cap \<and> bl 1909 then let b = capASIDBase cap; ptr = capASIDPool cap 1910 in ->1 1911 else if isPageDirectoryCap cap \<and> bl \<and> capPDMappedASID cap \<noteq> None 1912 then let a = the (capPDMappedASID cap); ptr = capPDBasePtr cap 1913 in ->2 1914 else if isPageTableCap cap \<and> bl \<and> capPTMappedAddress cap \<noteq> None 1915 then let (a, v) = the (capPTMappedAddress cap); ptr = capPTBasePtr cap 1916 in ->3 1917 else if isPageCap cap \<and> capVPMappedAddress cap \<noteq> None 1918 then let (a, v) = the (capVPMappedAddress cap); s = capVPSize cap; ptr = capVPBasePtr cap 1919 in ->4 1920 else ->5 1921 1922case \x of cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) -> (VCPUCap {}) -> ---> let cap = \x in 1923 if isPageDirectoryCap cap 1924 then ->1 1925 else if isPageTableCap cap 1926 then ->2 1927 else if isPageCap cap 1928 then ->3 1929 else if isASIDControlCap cap 1930 then ->4 1931 else if isASIDPoolCap cap 1932 then ->5 1933 else if isVCPUCap cap 1934 then ->6 1935 else undefined 1936 1937case \x of UntypedCap { capIsDevice = False } | capBlockSize untyped == objBits pool -> _ -> ---> let \v0\ = \x in 1938 if isUntypedCap \v0\ \<and> capBlockSize \v0\ == objBits pool \<and> \<not> capIsDevice \v0\ 1939 then ->1 1940 else ->2 1941 1942case \x of UntypedCap {capIsDevice = False} | capBlockSize untyped == objBits pool -> _ -> ---> if isUntypedCap \x \<and> (\<not> capIsDevice \x) \<and> (capBlockSize \x = objBits pool) 1943 then ->1 1944 else ->2 1945 1946case \x of (c@PageTableCap { capPTMappedAddress = Just _ }) -> (PageTableCap { capPTMappedAddress = Nothing }) -> (c@FrameCap {}) -> c@ASIDControlCap -> (c@ASIDPoolCap {}) -> ---> let c = \x in 1947 if isPageTableCap c \<and> capPTMappedAddress c \<noteq> None 1948 then ->1 1949 else if isPageTableCap c \<and> capPTMappedAddress c = None 1950 then ->2 1951 else if isFrameCap c 1952 then ->3 1953 else if c = ASIDControlCap 1954 then ->4 1955 else if isASIDPoolCap c 1956 then ->5 1957 else undefined 1958 1959case \x of c@(FrameCap {}) -> c -> ---> let c = \x in 1960 if isFrameCap c 1961 then ->1 1962 else ->2 1963 1964case \x of ((a@FrameCap {}), (b@FrameCap {})) -> ((a@PageTableCap {}), (b@PageTableCap {})) -> (ASIDControlCap, ASIDControlCap) -> ((a@ASIDPoolCap {}), (b@ASIDPoolCap {})) -> (_, _) -> ---> let (a,b) = \x in 1965 if isFrameCap a \<and> isFrameCap b 1966 then ->1 1967 else if isPageTableCap a \<and> isPageTableCap b 1968 then ->2 1969 else if a = ASIDControlCap \<and> b = ASIDControlCap 1970 then ->3 1971 else if isASIDPoolCap a \<and> isASIDPoolCap b 1972 then ->4 1973 else ->5 1974 1975case \x of ((a@FrameCap { capFBasePtr = ptrA }), (b@FrameCap {})) -> (a, b) -> ---> let (a, b) = \x in 1976 if isFrameCap a \<and> isFrameCap b 1977 then let ptrA = capFBasePtr a in ->1 1978 else ->2 1979 1980case \x of Arch.Types.APIObjectType _ -> Arch.Types.SmallPageObject -> Arch.Types.LargePageObject -> Arch.Types.HugePageObject -> Arch.Types.PageTableObject -> ---> let t = \x in 1981 case t of 1982 APIObjectType _ => ->1 1983 | SmallPageObject => ->2 1984 | LargePageObject => ->3 1985 | HugePageObject => ->4 1986 | PageTableObject => ->5 1987 1988case \x of (cap@FrameCap {}) -> _ -> ---> let cap = \x in 1989 if isFrameCap cap 1990 then ->1 1991 else ->2 1992 1993case \x of cap@(FrameCap {}) -> cap@(PageTableCap {}) -> cap@(ASIDControlCap {}) -> cap@(ASIDPoolCap {}) -> ---> let cap = \x in 1994 if isFrameCap cap 1995 then ->1 1996 else if isPageTableCap cap 1997 then ->2 1998 else if isASIDControlCap cap 1999 then ->3 2000 else if isASIDPoolCap cap 2001 then ->4 2002 else undefined 2003 2004case \x of (ArchInvocationLabel ArchLabels.ARMIRQIssueIRQHandler, irqW:triggerW:index:depth:_, cnode:_) -> (ArchInvocationLabel ArchLabels.ARMIRQIssueIRQHandler,_,_) -> _ -> ---> let (label, args, extraCaps) = \x in 2005 case (label, args, extraCaps) of 2006 (ArchInvocationLabel ARMIRQIssueIRQHandler, 2007 irqW#triggerW#index#depth#_, cnode#_) => ->1 2008 | (ArchInvocationLabel ARMIRQIssueIRQHandler, _, _) => ->2 2009 | _ => ->3 2010 2011case \x of (ArchInv.IssueIRQHandler (IRQ irq) destSlot srcSlot trigger) -> ---> case \x of 2012 IssueIRQHandler irq destSlot srcSlot trigger => ->1 2013