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