From b9e7e99e8e566559c1e9c931c693f2c4fa065f2b Mon Sep 17 00:00:00 2001
From: Joel Beeren <joel.beeren@nicta.com.au>
Date: Thu, 23 Mar 2017 16:48:20 +1100
Subject: [PATCH] x64: haskell: remove VMWriteOnly

---
 spec/design/X64/Hardware_H.thy                  | 11 +++--------
 spec/design/version                             | 10 +++-------
 spec/haskell/src/SEL4/Machine/Hardware/X64.lhs  | 11 +++--------
 spec/haskell/src/SEL4/Object/ObjectType/X64.lhs |  1 +
 4 files changed, 10 insertions(+), 23 deletions(-)

diff --git a/spec/design/X64/Hardware_H.thy b/spec/design/X64/Hardware_H.thy
index 620d6ad89..fa0fa75e5 100644
--- a/spec/design/X64/Hardware_H.thy
+++ b/spec/design/X64/Hardware_H.thy
@@ -28,7 +28,6 @@ datatype vmrights =
     VMKernelOnly
   | VMReadOnly
   | VMReadWrite
-  | VMWriteOnly
 
 datatype pml4e =
     InvalidPML4E
@@ -686,9 +685,8 @@ definition
 vmRightsToBits :: "vmrights \<Rightarrow> machine_word"
 where
 "vmRightsToBits x0\<equiv> (case x0 of
-    VMKernelOnly \<Rightarrow>    0x0
+    VMKernelOnly \<Rightarrow>    0x01
   | VMReadOnly \<Rightarrow>    0x10
-  | VMWriteOnly \<Rightarrow>    0x01
   | VMReadWrite \<Rightarrow>    0x11
   )"
 
@@ -699,7 +697,6 @@ where
     VMKernelOnly \<Rightarrow>    False
   | VMReadOnly \<Rightarrow>    False
   | VMReadWrite \<Rightarrow>    True
-  | VMWriteOnly \<Rightarrow>    True
   )"
 
 definition
@@ -707,9 +704,8 @@ allowRead :: "vmrights \<Rightarrow> bool"
 where
 "allowRead x0\<equiv> (case x0 of
     VMKernelOnly \<Rightarrow>    False
-  | VMReadOnly \<Rightarrow>    False
+  | VMReadOnly \<Rightarrow>    True
   | VMReadWrite \<Rightarrow>    True
-  | VMWriteOnly \<Rightarrow>    False
   )"
 
 definition
@@ -718,8 +714,7 @@ where
 "getVMRights x0 x1\<equiv> (case (x0, x1) of
     (True, True) \<Rightarrow>    VMReadWrite
   | (True, False) \<Rightarrow>    VMReadOnly
-  | (False, True) \<Rightarrow>    VMWriteOnly
-  | (False, False) \<Rightarrow>    VMKernelOnly
+  | (_, _) \<Rightarrow>    VMKernelOnly
   )"
 
 definition
diff --git a/spec/design/version b/spec/design/version
index b1edebe0e..9b6a02903 100644
--- a/spec/design/version
+++ b/spec/design/version
@@ -1,15 +1,11 @@
 Built from git repo at /home/joelb/work/verification/l4v/spec/haskell by joelb
 
 Generated from changeset:
-263ebe9 x64: s/ARM/X64/g proof/refine/X64/*.thy
+e6fcfaf x64: refine: ArchAcc_R done
 
 
 Warning - uncomitted changes used:
- M ../../proof/refine/X64/ArchAcc_R.thy
- M ../../proof/refine/X64/Invariants_H.thy
- M ../../proof/refine/X64/StateRelation.thy
- M ../design/X64/Hardware_H.thy
- M ../design/skel/X64/Hardware_H.thy
+ M ../../proof/refine/X64/CSpace_I.thy
  M ../design/version
- M ../../tools/haskell-translator/caseconvs
+ M src/SEL4/Machine/Hardware/X64.lhs
  M ../../tools/haskell-translator/make_spec.sh
diff --git a/spec/haskell/src/SEL4/Machine/Hardware/X64.lhs b/spec/haskell/src/SEL4/Machine/Hardware/X64.lhs
index af0ef6a29..f3d7530f0 100644
--- a/spec/haskell/src/SEL4/Machine/Hardware/X64.lhs
+++ b/spec/haskell/src/SEL4/Machine/Hardware/X64.lhs
@@ -530,32 +530,27 @@ Page entries -- any of PTEs, PDEs or PDPTEs.
 >     = VMKernelOnly
 >     | VMReadOnly
 >     | VMReadWrite
->     | VMWriteOnly
 >     deriving (Show, Eq)
 
 > vmRightsToBits :: VMRights -> Word
-> vmRightsToBits VMKernelOnly = 0x0
+> vmRightsToBits VMKernelOnly = 0x01
 > vmRightsToBits VMReadOnly = 0x10
-> vmRightsToBits VMWriteOnly = 0x01
 > vmRightsToBits VMReadWrite = 0x11
 
 > allowWrite :: VMRights -> Bool
 > allowWrite VMKernelOnly = False
 > allowWrite VMReadOnly = False
 > allowWrite VMReadWrite = True
-> allowWrite VMWriteOnly = True
 
 > allowRead :: VMRights -> Bool
 > allowRead VMKernelOnly = False
-> allowRead VMReadOnly = False
+> allowRead VMReadOnly = True
 > allowRead VMReadWrite = True
-> allowRead VMWriteOnly = False
 
 > getVMRights :: Bool -> Bool -> VMRights
 > getVMRights True True = VMReadWrite
 > getVMRights True False = VMReadOnly
-> getVMRights False True = VMWriteOnly
-> getVMRights False False = VMKernelOnly
+> getVMRights _ _ = VMKernelOnly
 
 > vmRightsFromBits ::  Word -> VMRights
 > vmRightsFromBits rw = getVMRights (testBit rw 1) (testBit rw 0)
diff --git a/spec/haskell/src/SEL4/Object/ObjectType/X64.lhs b/spec/haskell/src/SEL4/Object/ObjectType/X64.lhs
index ab8cc994a..e0de274be 100644
--- a/spec/haskell/src/SEL4/Object/ObjectType/X64.lhs
+++ b/spec/haskell/src/SEL4/Object/ObjectType/X64.lhs
@@ -223,6 +223,7 @@ Deletion of a final capability to a page table that has been mapped requires tha
 
 > isPhysicalCap :: ArchCapability -> Bool
 > isPhysicalCap ASIDControlCap = False
+> isPhysicalCap (IOPortCap _ _) = False
 > isPhysicalCap _ = True
 
 > sameObjectAs :: ArchCapability -> ArchCapability -> Bool