adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

x64 design: run Haskell translator

This commit is contained in:
Matthew Brecknell 2017-04-24 22:10:02 +10:00
parent 3c84f2ade3
commit d4fc2de959
3 changed files with 16 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
spec/design/X64/ArchVSpaceDecls_H.thy
View File

@ -145,13 +145,13 @@ consts'
maskVMRights :: "vmrights \<Rightarrow> cap_rights \<Rightarrow> vmrights"
consts'
flushAll :: "paddr \<Rightarrow> asid \<Rightarrow> unit kernel"
flushAll :: "machine_word \<Rightarrow> asid \<Rightarrow> unit kernel"
consts'
flushPDPT :: "paddr \<Rightarrow> asid \<Rightarrow> unit kernel"
flushPDPT :: "machine_word \<Rightarrow> asid \<Rightarrow> unit kernel"
consts'
flushPD :: "paddr \<Rightarrow> asid \<Rightarrow> unit kernel"
flushPD :: "machine_word \<Rightarrow> asid \<Rightarrow> unit kernel"
consts'
flushTable :: "machine_word \<Rightarrow> vptr \<Rightarrow> machine_word \<Rightarrow> asid \<Rightarrow> unit kernel"

8
spec/design/X64/ArchVSpace_H.thy
View File

@ -308,7 +308,7 @@ defs unmapPDPT_def:
| _ \<Rightarrow> throw InvalidRoot
);
withoutFailure $ (do
flushPDPT (addrFromPPtr vspace) asid;
flushPDPT (fromPPtr vspace) asid;
storePML4E pmSlot InvalidPML4E
od)
odE)"
@ -324,7 +324,7 @@ defs unmapPageDirectory_def:
| _ \<Rightarrow> throw InvalidRoot
);
withoutFailure $ (do
flushPD (addrFromPPtr vspace) asid;
flushPD (fromPPtr vspace) asid;
storePDPTE pdptSlot InvalidPDPTE;
invalidatePageStructureCacheASID (addrFromPPtr vspace) asid
od)
@ -464,7 +464,7 @@ defs isValidVTableRoot_def:
defs checkValidIPCBuffer_def:
"checkValidIPCBuffer vptr x1\<equiv> (case x1 of
(ArchObjectCap (PageCap _ _ _ _ _ _)) \<Rightarrow> (doE
(ArchObjectCap (PageCap _ _ _ _ False _)) \<Rightarrow> (doE
whenE (vptr && mask 10 \<noteq> 0) $ throw AlignmentError;
returnOk ()
odE)
@ -517,7 +517,7 @@ od)"
defs invalidateASIDEntry_def:
"invalidateASIDEntry asid vspace\<equiv> (do
doMachineOp $ hwASIDInvalidate (addrFromPPtr vspace) (fromASID asid);
doMachineOp $ hwASIDInvalidate (fromPPtr vspace) (fromASID asid);
invalidateASID' asid
od)"

13
spec/design/version
View File

@ -1,9 +1,14 @@
Built from git repo at /home/joelb/work/verification/l4v/spec/haskell by joelb
Built from git repo at /home/matthewb/verification/x64/l4v/spec/haskell by matthewb
Generated from changeset:
04d1026 x64: ainvs: fix broken proofs from strengthening of wellformed_pde et al
d998c2bec x64 haskell: check capVPIsDevice in checkValidIPCBuffer
Warning - uncomitted changes used:
M ../design/version
M src/SEL4/Object/ObjectType/X64.lhs
M ../../proof/refine/X64/Arch_R.thy
M ../../proof/refine/X64/Finalise_R.thy
M ../../proof/refine/X64/Schedule_R.thy
M ../../proof/refine/X64/VSpace_R.thy
M ../design/X64/ArchVSpaceDecls_H.thy
M ../design/X64/ArchVSpace_H.thy
MM ../design/version