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