abstract: add Hypervisor fault event to ARM

spec/abstract/ARM/Hypervisor_A.thy

@@ -0,0 +1,25 @@
+(*
+ * Copyright 2016, Data61, CSIRO
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(DATA61_GPL)
+ *)
+
+chapter "Handle Hyperviser Fault Event"
+
+theory Hypervisor_A
+imports "../Exceptions_A"
+begin
+
+context Arch begin global_naming ARM_A
+
+fun handle_hypervisor_fault :: "word32 \<Rightarrow> hyp_fault_type \<Rightarrow> (unit, 'z::state_ext) f_monad"
+where
+"handle_hypervisor_fault thread ARMNoHypFaults = returnOk ()"
+
+
+end
+end

spec/abstract/Syscall_A.thy

@@ -19,6 +19,7 @@ imports
   "../design/Event_H"
   Decode_A
   "./$L4V_ARCH/Init_A"
+  "./$L4V_ARCH/Hypervisor_A"
 begin
 
 context begin interpretation Arch .
@@ -26,7 +27,7 @@ context begin interpretation Arch .
 requalify_consts
   arch_perform_invocation
   handle_vm_fault
-
+  handle_hypervisor_fault
 end
 
 
@@ -364,6 +365,12 @@ where
     return ()
   od)"
 
+| "handle_event (HypervisorEvent hypfault_type) = (without_preemption $ do
+    thread \<leftarrow> gets cur_thread;
+    handle_hypervisor_fault thread hypfault_type;
+    return ()
+  od)"
+
 
 section {* Kernel entry point  *}