x64: haskell: remove VMWriteOnly
This commit is contained in:
parent
e6fcfaf476
commit
b9e7e99e8e
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in New Issue