1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11theory Glue_CAMKES 12imports Types_CAMKES 13begin 14 15abbreviation "seL4_MsgMaxLength \<equiv> 120::nat" 16 17type_synonym ipc = "nat list" 18definition wellformed_ipc :: "ipc \<Rightarrow> bool" 19where "wellformed_ipc i = (length i < seL4_MsgMaxLength)" 20 21(* FIXME: These definitions need to diverge from the implementation definitions because we 22 * need to distinguish between primitive types and things like strings. The implementation 23 * does this in a pretty ad hoc way. 24 *) 25record parameter_value = 26 p_type :: param_type 27 p_value :: "nat list" (* FIXME: Better type for generic values. *) 28definition 29 wellformed_parameter :: "parameter_value \<Rightarrow> bool" 30where 31 "wellformed_parameter p = (case p_type p of 32 Primitive _ \<Rightarrow> length (p_value p) = 1 33 | Array t \<Rightarrow> (case t of 34 SizedArray _ \<Rightarrow> True 35 | TerminatedArray _ \<Rightarrow> length (p_value p) > 0 \<and> hd (rev (p_value p)) = 0))" 36 37abbreviation "prim_value \<equiv> \<lambda>(x::parameter_value). hd (p_value x)" 38 39definition 40 marshal_primitive :: "ipc \<Rightarrow> parameter_value \<Rightarrow> ipc" 41where 42 "marshal_primitive i p = i @ [hd (p_value p)]" 43 44(* TODO: The implementation does some optimisations that are not represented in these 45 * definitions (e.g. packing multiple chars into a single message register). 46 *) 47function 48 marshal_array :: "ipc \<Rightarrow> parameter_value \<Rightarrow> ipc" 49where 50 "marshal_array i p = (case p_value p of 51 [] \<Rightarrow> i 52 | _ # xs \<Rightarrow> marshal_array (marshal_primitive i p) \<lparr>p_type = p_type p, p_value = xs\<rparr>)" 53 by fast+ 54 55definition 56 marshal :: "ipc \<Rightarrow> parameter_value \<Rightarrow> ipc" 57where 58 "marshal i p = (case p_type p of 59 Primitive _ \<Rightarrow> marshal_primitive i p 60 |Array _ \<Rightarrow> marshal_array i p)" 61 62definition 63 unmarshal_primitive :: "ipc \<Rightarrow> primitive \<Rightarrow> parameter_value \<times> ipc" 64where 65 "unmarshal_primitive i t = (\<lparr>p_type = Primitive t, p_value = [hd i]\<rparr>, tl i)" 66 67fun 68 unmarshal_array_by_size :: "ipc \<Rightarrow> primitive \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> parameter_value \<times> ipc" 69where 70 "unmarshal_array_by_size i t 0 ac = (\<lparr>p_type = Array (SizedArray t), p_value = ac\<rparr>, i)" 71 |"unmarshal_array_by_size i t sz ac = unmarshal_array_by_size (snd (unmarshal_primitive i t)) t (sz - 1) (ac @ p_value (fst (unmarshal_primitive i t)))" 72 73function 74 unmarshal_array_by_terminator :: "ipc \<Rightarrow> primitive \<Rightarrow> nat list \<Rightarrow> parameter_value \<times> ipc" 75where 76 "unmarshal_array_by_terminator i t ac = (case (prim_value (fst (unmarshal_primitive i t))) of 77 0 \<Rightarrow> (\<lparr>p_type = Array (TerminatedArray t), p_value = ac @ [0]\<rparr>, snd (unmarshal_primitive i t)) 78 |_ \<Rightarrow> unmarshal_array_by_terminator (snd (unmarshal_primitive i t)) t (ac @ p_value (fst (unmarshal_primitive i t))))" 79 by fast+ 80 81definition 82 unmarshal_array :: "ipc \<Rightarrow> primitive \<Rightarrow> nat option \<Rightarrow> parameter_value \<times> ipc" 83where 84 "unmarshal_array i t n = (case n of 85 None \<Rightarrow> unmarshal_array_by_terminator i t [] 86 |Some nn \<Rightarrow> unmarshal_array_by_size i t nn [])" 87 88(* Some sanity checks *) 89 90(* Marshalling something into an empty IPC and then unmarshalling it does not 91 * alter the value or the IPC. 92 *) 93lemma "\<lbrakk>marshal_primitive [] p = i2; wellformed_parameter p; p_type p = Primitive q; unmarshal_primitive i2 q = (n, i3)\<rbrakk> 94 \<Longrightarrow> wellformed_ipc i2 \<and> [] = i3 \<and> n = p" 95 apply (simp add:marshal_primitive_def unmarshal_primitive_def) 96 apply (clarsimp simp:wellformed_ipc_def wellformed_parameter_def) 97 apply (induct p, clarsimp, case_tac p_value, simp+) 98 done 99 100(* Unmarshalling anything from an empty IPC gives you nothing. *) 101lemma "\<forall>t. \<exists>p. (unmarshal_primitive [] t = (\<lparr>p_type = p, p_value = [hd []]\<rparr>, []))" 102 by (simp add:unmarshal_primitive_def) 103 104(* TODO: Definitions of send/receive as basically thin wrappers around the syscalls. *) 105 106(* TODO: Definitions of the connectors' operations in terms of send and receive. *) 107 108end 109