1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7(* 8Monad instantiations, handling of faults, errors, and interrupts. 9*) 10 11chapter "Basic Kernel and Exception Monads" 12 13theory Exceptions_A 14imports Deterministic_A 15begin 16 17text \<open>This theory contains abbreviations for the monadic types used 18in the specification and a number of lifting functions between them.\<close> 19 20text \<open>The basic kernel monad without faults, interrupts, or errors.\<close> 21type_synonym ('a,'z) s_monad = "('z state, 'a) nondet_monad" 22 23text \<open>The fault monad: may throw a @{text fault} exception which 24will usually be reported to the current thread's fault handler.\<close> 25type_synonym ('a,'z) f_monad = "(fault + 'a,'z) s_monad" 26 27term "a::(unit,'a) s_monad" 28 29text \<open>The error monad: may throw a @{text syscall_error} exception 30which will usually be reported to the current thread as system call 31result.\<close> 32type_synonym ('a,'z) se_monad = "(syscall_error + 'a,'z) s_monad" 33 34text \<open>The lookup failure monad: may throw a @{text lookup_failure} 35exception. Depending on context it may either be reported directly to 36the current thread or to its fault handler. 37\<close> 38type_synonym ('a,'z) lf_monad = "(lookup_failure + 'a,'z) s_monad" 39 40text \<open>The preemption monad. May throw an interrupt exception.\<close> 41type_synonym ('a,'z) p_monad = "(unit + 'a,'z) s_monad" 42 43 44text \<open> 45 Printing abbreviations for the above types. 46\<close> 47translations 48 (type) "'a s_monad" <= (type) "state \<Rightarrow> (('a \<times> state) \<Rightarrow> bool) \<times> bool" 49 (type) "'a f_monad" <= (type) "(fault + 'a) s_monad" 50 (type) "'a se_monad" <= (type) "(syscall_error + 'a) s_monad" 51 (type) "'a lf_monad" <= (type) "(lookup_failure + 'a) s_monad" 52 (type) "'a p_monad" <=(type) "(unit + 'a) s_monad" 53 54text \<open>Perform non-preemptible operations within preemptible blocks.\<close> 55definition 56 without_preemption :: "('a,'z::state_ext) s_monad \<Rightarrow> ('a,'z::state_ext) p_monad" 57where without_preemption_def[simp]: 58 "without_preemption \<equiv> liftE" 59 60text \<open>Allow preemption at this point.\<close> 61definition 62 preemption_point :: "(unit,'z::state_ext) p_monad" where 63 "preemption_point \<equiv> doE liftE $ do_extended_op update_work_units; 64 OR_choiceE (work_units_limit_reached) 65 (doE liftE $ do_extended_op reset_work_units; 66 irq_opt \<leftarrow> liftE $ do_machine_op (getActiveIRQ True); 67 case_option (returnOk ()) (K (throwError $ ())) irq_opt 68 odE) (returnOk ()) 69 odE" 70 71text \<open>Lift one kind of exception monad into another by converting the error 72into various other kinds of error or return value.\<close> 73definition 74 cap_fault_on_failure :: "obj_ref \<Rightarrow> bool \<Rightarrow> ('a,'z::state_ext) lf_monad \<Rightarrow> ('a,'z::state_ext) f_monad" where 75 "cap_fault_on_failure cptr rp m \<equiv> handleE' m (throwError \<circ> CapFault cptr rp)" 76 77definition 78 lookup_error_on_failure :: "bool \<Rightarrow> ('a,'z::state_ext) lf_monad \<Rightarrow> ('a,'z::state_ext) se_monad" where 79 "lookup_error_on_failure s m \<equiv> handleE' m (throwError \<circ> FailedLookup s)" 80 81definition 82 null_cap_on_failure :: "(cap,'z::state_ext) lf_monad \<Rightarrow> (cap,'z::state_ext) s_monad" where 83 "null_cap_on_failure \<equiv> liftM (case_sum (\<lambda>x. NullCap) id)" 84 85definition 86 unify_failure :: "('f + 'a,'z::state_ext) s_monad \<Rightarrow> (unit + 'a,'z::state_ext) s_monad" where 87 "unify_failure m \<equiv> handleE' m (\<lambda>x. throwError ())" 88 89definition 90 empty_on_failure :: "('f + 'a list,'z::state_ext) s_monad \<Rightarrow> ('a list,'z::state_ext) s_monad" where 91 "empty_on_failure m \<equiv> m <catch> (\<lambda>x. return [])" 92 93definition 94 const_on_failure :: "'a \<Rightarrow> ('f + 'a,'z::state_ext) s_monad \<Rightarrow> ('a,'z::state_ext) s_monad" where 95 "const_on_failure c m \<equiv> m <catch> (\<lambda>x. return c)" 96 97text \<open>Checks whether first argument is between second and third (inclusive).\<close> 98 99definition 100 range_check :: "machine_word \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> (unit,'z::state_ext) se_monad" 101where 102 "range_check v min_v max_v \<equiv> 103 unlessE (v \<ge> min_v \<and> v \<le> max_v) $ throwError $ RangeError min_v max_v" 104 105end 106