From 2e556d4a3384d27e01af279121b5cd4e5ed3d324 Mon Sep 17 00:00:00 2001
From: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
Date: Tue, 18 Jun 2019 12:04:43 +1000
Subject: [PATCH] reduce UserLevelFault code to 28 bits

This makes room for a 4-bit seL4_FaultType field.
---
 spec/abstract/Syscall_A.thy           | 2 +-
 spec/haskell/src/SEL4/API/Syscall.lhs | 2 +-
 spec/sep-abstract/Syscall_SA.thy      | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/spec/abstract/Syscall_A.thy b/spec/abstract/Syscall_A.thy
index a222f5ffe..261630309 100644
--- a/spec/abstract/Syscall_A.thy
+++ b/spec/abstract/Syscall_A.thy
@@ -349,7 +349,7 @@ where
 
 | "handle_event (UserLevelFault w1 w2) = (without_preemption $ do
     thread \<leftarrow> gets cur_thread;
-    handle_fault thread $ UserException (w1 && mask 32) (w2 && mask 29);
+    handle_fault thread $ UserException (w1 && mask 32) (w2 && mask 28);
     return ()
   od)"
 
diff --git a/spec/haskell/src/SEL4/API/Syscall.lhs b/spec/haskell/src/SEL4/API/Syscall.lhs
index 8f20ee8f7..7ec0d1c1a 100644
--- a/spec/haskell/src/SEL4/API/Syscall.lhs
+++ b/spec/haskell/src/SEL4/API/Syscall.lhs
@@ -127,7 +127,7 @@ bottom 32 bits be communicated to the fault handler, for the second word
 
 > handleEvent (UserLevelFault w1 w2) = withoutPreemption $ do
 >     thread <- getCurThread
->     handleFault thread $ UserException (w1 .&. mask 32) (w2 .&. mask 29)
+>     handleFault thread $ UserException (w1 .&. mask 32) (w2 .&. mask 28)
 >     return ()
 
 \subsubsection{Virtual Memory Faults}
diff --git a/spec/sep-abstract/Syscall_SA.thy b/spec/sep-abstract/Syscall_SA.thy
index 05d1a02f1..96841b826 100644
--- a/spec/sep-abstract/Syscall_SA.thy
+++ b/spec/sep-abstract/Syscall_SA.thy
@@ -216,7 +216,7 @@ where
 
 | "handle_event (UserLevelFault w1 w2) = (without_preemption $ do
     thread \<leftarrow> gets cur_thread;
-    handle_fault thread $ UserException w1 (w2 && mask 29);
+    handle_fault thread $ UserException w1 (w2 && mask 28);
     return ()
   od)"