From b8048726a6fa754b19acdd40efb369cac22e49f1 Mon Sep 17 00:00:00 2001
From: Joel Beeren <joel.beeren@nicta.com.au>
Date: Wed, 19 Oct 2016 10:52:46 +1100
Subject: [PATCH] X64: added dummy VMPML4E to vm_page_entry.

needs to be reviewed
---
 spec/abstract/X64/ArchVSpace_A.thy   | 2 ++
 spec/abstract/X64/Arch_A.thy         | 4 +++-
 spec/abstract/X64/Arch_Structs_A.thy | 2 +-
 3 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/spec/abstract/X64/ArchVSpace_A.thy b/spec/abstract/X64/ArchVSpace_A.thy
index 572ba23b9..268c3aa01 100644
--- a/spec/abstract/X64/ArchVSpace_A.thy
+++ b/spec/abstract/X64/ArchVSpace_A.thy
@@ -89,6 +89,8 @@ where
 "ensure_safe_mapping (VMPDE (PageTablePDE _ _ _), _) = fail"
 |
 "ensure_safe_mapping (VMPDPTE (PageDirectoryPDPTE _ _ _), _) = fail"
+|
+"ensure_safe_mapping (VMPML4E _, _) = fail"
 
 text {* Look up a thread's IPC buffer and check that the thread has the right
 authority to read or (in the receiver case) write to it. *}
diff --git a/spec/abstract/X64/Arch_A.thy b/spec/abstract/X64/Arch_A.thy
index 8ca5befe1..94b883e7b 100644
--- a/spec/abstract/X64/Arch_A.thy
+++ b/spec/abstract/X64/Arch_A.thy
@@ -153,11 +153,13 @@ perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s
        of (VMPTE pte, slot) \<Rightarrow> store_pte slot pte
         | (VMPDE pde, slot) \<Rightarrow> store_pde slot pde
         | (VMPDPTE pdpte, slot) \<Rightarrow> store_pdpte slot pdpte
+        | _ \<Rightarrow> fail
       od
   | PageRemap entries \<Rightarrow> (case entries
        of (VMPTE pte, slot) \<Rightarrow> store_pte slot pte
         | (VMPDE pde, slot) \<Rightarrow> store_pde slot pde
-        | (VMPDPTE pdpte, slot) \<Rightarrow> store_pdpte slot pdpte)
+        | (VMPDPTE pdpte, slot) \<Rightarrow> store_pdpte slot pdpte
+        | _ \<Rightarrow> fail)
   | PageUnmap cap ct_slot \<Rightarrow>
       (case cap
          of PageCap dev base rights map_type sz mapped \<Rightarrow>
diff --git a/spec/abstract/X64/Arch_Structs_A.thy b/spec/abstract/X64/Arch_Structs_A.thy
index 9cc54dffa..3a9dc30f4 100644
--- a/spec/abstract/X64/Arch_Structs_A.thy
+++ b/spec/abstract/X64/Arch_Structs_A.thy
@@ -110,7 +110,7 @@ datatype pte
          (pte_rights : cap_rights)
 
 
-datatype vm_page_entry = VMPTE pte | VMPDE pde | VMPDPTE pdpte
+datatype vm_page_entry = VMPTE pte | VMPDE pde | VMPDPTE pdpte | VMPML4E pml4e
 
 datatype translation_type = NotTranslated | Translated