1(*
2 * Copyright 2018, Data61
3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 * ABN 41 687 119 230.
5 *
6 * This software may be distributed and modified according to the terms of
7 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 * See "LICENSE_BSD2.txt" for details.
9 *
10 * @TAG(DATA61_BSD)
11 *)
12
13(* /*? macros.generated_file_notice() ?*/ *)
14
15open preamble basis
16
17val _ = new_theory "camkesStart";
18
19val _ = translation_extends "basisProg";
20
21val _ = ml_prog_update (open_module "Utils")
22
23val get_word_size_def = process_topdecs `
24    fun get_word_size u = /*? macros.get_word_size(options.architecture) ?*/
25`;
26
27val int_to_bytes_def = process_topdecs `
28    fun int_to_bytes w len = let
29        val array = Word8Array.array len (Word8.fromInt 0);
30        fun loop i divisor =
31            if i = len then
32                ()
33            else
34                let val _ = Word8Array.update array i (Word8.fromInt (w div divisor));
35                in loop (i + 1) (divisor * 256)
36                end
37        val _ = loop 0 1;
38        in array end;
39`;
40
41(* Read the first `len` bytes of `buf` beginning at `off` into a int *)
42val bytes_to_int_def = process_topdecs `
43    fun bytes_to_int buf off len = let
44        fun loop i acc =
45            if i = len then
46                acc
47            else
48                loop (i + 1) (acc * 256 + (Word8.toInt (Word8Array.sub buf (off + len - i - 1))))
49        in loop 0 0 end;
50`;
51
52(* Read the a nul-terminated string from `buf` beginning at `off` *)
53val read_c_string_def = process_topdecs `
54  fun read_c_string buf off len = let
55    fun nul_byte_idx i =
56      if i = len orelse Word8Array.sub buf i = Word8.fromInt 0 then
57        i
58      else
59        nul_byte_idx (i + 1);
60    val str_len = nul_byte_idx off - off;
61    in (Word8Array.substring buf off str_len, str_len) end;
62`;
63
64(* Convert a string to a Word8Array *)
65val string_to_bytes_def = process_topdecs `
66  fun string_to_bytes str = let
67    val len = String.size str;
68    val result = Word8Array.array len (Word8.fromInt 0);
69    val _ = Word8Array.copyVec str 0 len result 0;
70    in result end;
71`;
72
73val seL4_ReplyRecv_def = process_topdecs `
74    fun seL4_ReplyRecv ep send_length ipcbuf = let
75        val word_size = /*? macros.get_word_size(options.architecture) ?*/;
76        val _ = Word8Array.copy (int_to_bytes ep word_size) 0 word_size ipcbuf 1;
77        val _ = Word8Array.copy (int_to_bytes send_length word_size) 0 word_size ipcbuf (1 + word_size);
78        val _ = #(seL4_ReplyRecv) "" ipcbuf;
79        val len = bytes_to_int ipcbuf 1 word_size;
80        val badge = bytes_to_int ipcbuf (1 + word_size) word_size;
81        in (len, badge) end;
82`;
83
84val seL4_Recv_def = process_topdecs `
85    fun seL4_Recv ep ipcbuf = let
86        val word_size = /*? macros.get_word_size(options.architecture) ?*/;
87        val _ = Word8Array.copy (int_to_bytes ep word_size) 0 word_size ipcbuf 1;
88        val _ = #(seL4_Recv) "" ipcbuf;
89        val len = bytes_to_int ipcbuf 1 word_size;
90        val badge = bytes_to_int ipcbuf (1 + word_size) word_size;
91        in (len, badge) end;
92`;
93
94val seL4_Send_def = process_topdecs `
95    fun seL4_Send ep send_length ipcbuf = let
96        val word_size = /*? macros.get_word_size(options.architecture) ?*/;
97        val _ = Word8Array.copy (int_to_bytes ep word_size) 0 word_size ipcbuf 1;
98        val _ = Word8Array.copy (int_to_bytes send_length 8) 0 word_size ipcbuf (1 + word_size);
99        val _ = #(seL4_Send) "" ipcbuf;
100        in () end;
101`;
102
103val seL4_Wait_def = process_topdecs `
104    fun seL4_Wait src = let
105        val word_size = /*? macros.get_word_size(options.architecture) ?*/;
106        val buf = Word8Array.array (1 + word_size)  (Word8.fromInt 0);
107        val _ = Word8Array.copy (int_to_bytes src word_size) 0 word_size buf 1;
108        val _ = #(seL4_Wait) "" buf;
109        val badge = bytes_to_int buf 1 word_size;
110        in badge end;
111`;
112
113val camkes_declare_reply_cap_def = process_topdecs `
114    fun camkes_declare_reply_cap slot = let
115        val word_size = /*? macros.get_word_size(options.architecture) ?*/;
116        val buf = Word8Array.array (1 + word_size) (Word8.fromInt 0);
117        val _ = Word8Array.copy (int_to_bytes slot word_size) 0 word_size buf 1;
118        val _ = #(camkes_declare_reply_cap) "" buf;
119        in () end;
120`;
121
122val clear_tls_reply_cap_in_tcb_def = process_topdecs `
123    fun clear_tls_reply_cap_in_tcb u = let
124        val buf = Word8Array.array 2 (Word8.fromInt 0);
125        val _ = #(clear_tls_reply_cap_in_tcb) "" buf;
126        in (Word8Array.sub buf 1) <> (Word8.fromInt 0) end;
127`;
128
129val fail_def = process_topdecs `
130    fun fail msg = let
131        val _ = TextIO.print (msg ^ "\n");
132        val _ = #(fail) "" (Word8Array.array 0 (Word8.fromInt 0));
133        in () end;
134`;
135
136val _ = app append_prog [
137    int_to_bytes_def,
138    bytes_to_int_def,
139    read_c_string_def,
140    string_to_bytes_def,
141    get_word_size_def,
142    fail_def,
143    seL4_Recv_def,
144    seL4_ReplyRecv_def,
145    seL4_Send_def,
146    seL4_Wait_def,
147    camkes_declare_reply_cap_def,
148    clear_tls_reply_cap_in_tcb_def
149];
150
151val _ = ml_prog_update (close_module NONE);
152
153val _ = export_theory ();
154
155