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/*- if configuration[me.instance.name].get('environment', 'c').lower() == 'cakeml' -*/ 14 15/*- from 'rpc-connector.c' import establish_recv_rpc, recv_first_rpc, complete_recv, begin_recv, begin_reply, complete_reply, reply_recv with context -*/ 16 17/*# Construct a dict from interface types to list of from ends indicies #*/ 18/*- set type_dict = {} -*/ 19/*- for f in me.parent.from_ends -*/ 20 /*- set cur_list = type_dict.get(f.interface.type, []) -*/ 21 /*- do cur_list.append(loop.index0) -*/ 22 /*- do type_dict.update({f.interface.type: cur_list}) -*/ 23/*- endfor -*/ 24 25/*- set connector = namespace() -*/ 26 27/*- set int_types = ['uint8_t', 'uint16_t', 'uint32_t', 'uint64_t'] -*/ 28 29/*- macro cakeml_unmarshal(val, type, buf, offset) -*/ 30 /*- if type in int_types -*/ 31 /*- set sz = macros.sizeof(options.architecture, type) -*/ 32 val /*? val ?*/ = Utils.bytes_to_int /*? buf ?*/ /*? offset ?*/ /*? sz ?*/; 33 val /*? offset ?*/ = /*? offset ?*/ + /*? sz ?*/; 34 /*- elif type == 'string' -*/ 35 (* FIXME: compute the max length statically *) 36 val (/*? val ?*/, str_len) = Utils.read_c_string /*? buf ?*/ /*? offset ?*/ 37 (Word8Array.length /*? buf ?*/); 38 val /*? offset ?*/ = /*? offset ?*/ + str_len + 1; 39 /*- else -*/ 40 /*? raise(TemplateError('CakeML does not support this type: %s' % type)) ?*/ 41 /*- endif -*/ 42/*- endmacro -*/ 43 44/*- macro cakeml_unmarshal_param(val, param, buf, offset) -*/ 45 /*- if param.array -*/ 46 /*? raise(TemplateError('CakeML does not support arrays')) ?*/ 47 /*- endif -*/ 48 /*? cakeml_unmarshal(val, param.type, buf, offset) ?*/ 49/*- endmacro -*/ 50 51/*- macro cakeml_marshal(val, type, buf, offset) -*/ 52 /*- if type in int_types -*/ 53 /*- set sz = macros.sizeof(options.architecture, type) -*/ 54 val _ = Word8Array.copy (Utils.int_to_bytes /*? val ?*/ /*? sz ?*/) 0 /*? sz ?*/ /*? buf ?*/ /*? offset ?*/; 55 val /*? offset ?*/ = /*? offset ?*/ + /*? sz ?*/; 56 /*- elif type == 'string' -*/ 57 val byte_array_output = Utils.string_to_bytes /*? val ?*/; 58 val len = Word8Array.length byte_array_output; 59 (* FIXME: compute buffer length statically (should be bsize) *) 60 val space_remaining = Word8Array.length /*? buf ?*/ - offset - 1; 61 val copy_len = if len <= space_remaining then len else space_remaining; 62 val _ = Word8Array.copy byte_array_output 0 copy_len /*? buf ?*/ /*? offset ?*/; 63 (* Null byte at the end of the string *) 64 val _ = Word8Array.update /*? buf ?*/ (/*? offset ?*/ + copy_len) (Word8.fromInt 0); 65 val /*? offset ?*/ = /*? offset ?*/ + copy_len + 1; 66 /*- else -*/ 67 /*? raise(TemplateError('CakeML only supports int types right now')) ?*/ 68 /*- endif -*/ 69/*- endmacro -*/ 70 71/*- macro cakeml_marshal_param(val, param, buf, offset) -*/ 72 /*- if param.array -*/ 73 /*? raise(TemplateError('CakeML does not support arrays')) ?*/ 74 /*- endif -*/ 75 /*? cakeml_marshal(val, param.type, buf, offset) ?*/ 76/*- endmacro -*/ 77 78/*- macro log2(val) -*/ 79 /*- if val <= 2 ** 8 -*/ 80 1 81 /*- elif val <= 2 ** 16 -*/ 82 2 83 /*- elif val <= 2 ** 32 -*/ 84 4 85 /*- elif val <= 2 ** 64 -*/ 86 8 87 /*- else -*/ 88 /*? raise(TemplateError('Value too large')) ?*/ 89 /*- endif -*/ 90/*- endmacro -*/ 91 92open preamble basis componentTheory; 93 94val _ = new_theory "connector"; 95 96val _ = translation_extends "component"; 97 98/*- set buffer = configuration[me.parent.name].get('buffer') -*/ 99/*- if buffer is none -*/ 100 /*? establish_recv_rpc(connector, me.interface.name, language='cakeml') ?*/ 101/*- else -*/ 102 /*? raise(TemplateError('CakeML connector does not support custom buffers')) ?*/ 103/*- endif -*/ 104 105val _ = ml_prog_update (open_module "Connector"); 106 107val rpc_loop_def = process_topdecs ` 108 fun rpc_loop length badge = 109 /*- for from_type in type_dict.keys() -*/ 110 /*- if not loop.first -*/ 111 else 112 /*- endif -*/ 113 if ( 114 /*- for from_index in type_dict.get(from_type) -*/ 115 /*- if not loop.first -*/ 116 orelse 117 /*- endif -*/ 118 badge = /*? connector.badges[from_index] ?*/ 119 /*- endfor -*/ 120 ) then let 121 /*- set methods_len = len(from_type.methods) -*/ 122 val offset = /*? connector.cakeml_reserved_buf ?*/; 123 (* Extract the method id if there is more than 1 method *) 124 /*- if methods_len <= 1 -*/ 125 val method_id = 0; 126 /*- else -*/ 127 val method_id_len = /*? log2(methods_len) ?*/; 128 val method_id = Utils.bytes_to_int /*? connector.recv_buffer ?*/ offset method_id_len; 129 val offset = offset + method_id_len; 130 /*- endif -*/ 131 val _ = case method_id of 132 /*- for i, m in enumerate(from_type.methods) -*/ 133 /*- set input_parameters = list(filter(lambda('x: x.direction in [\'refin\', \'in\', \'inout\']'), m.parameters)) -*/ 134 /*- set output_parameters = list(filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters)) -*/ 135 /*- if not loop.first -*/ 136 | 137 /*- endif -*/ 138 /*? i ?*/ (* /*? m.name ?*/ *) => let 139 (* Unmarshal input parameters *) 140 /*- for j, p in enumerate(input_parameters) -*/ 141 /*? cakeml_unmarshal_param('input_val%s' % j, p, connector.recv_buffer, 'offset') ?*/ 142 /*- endfor -*/ 143 (* Call the implementation and deconstruct any result *) 144 val 145 ( 146 /*- if m.return_type is not none -*/ 147 return_val 148 /*- if len(output_parameters) > 0 -*/ 149 , 150 /*- endif -*/ 151 /*- endif -*/ 152 /*- for j, _ in enumerate(output_parameters) -*/ 153 /*- if not loop.first -*/ 154 , 155 /*- endif -*/ 156 result_val/*? j?*/ 157 /*- endfor -*/ 158 ) = Component./*? me.interface.name ?*/_/*? m.name ?*/ 159 /*- for j, _ in enumerate(input_parameters) -*/ 160 input_val/*? j ?*/ 161 /*- endfor -*/ 162 /*- if len(input_parameters) == 0 -*/ 163 () 164 /*- endif -*/ 165 ; 166 /*? complete_recv(connector) ?*/ 167 /*? begin_reply(connector) ?*/ 168 val offset = /*? connector.cakeml_reserved_buf ?*/; 169 (* Marshal return value *) 170 /*- if m.return_type is not none -*/ 171 /*? cakeml_marshal('return_val', m.return_type, connector.send_buffer, 'offset') ?*/ 172 /*- endif -*/ 173 (* Marshal other output parameters *) 174 /*- for j, p in enumerate(output_parameters) -*/ 175 /*? cakeml_marshal_param('result_val%s' % j, p, connector.send_buffer, 'offset') ?*/ 176 /*- endfor -*/ 177 val length = offset - /*? connector.cakeml_reserved_buf ?*/; 178 /*? reply_recv(connector, 'length', 'size', me.might_block()) ?*/ 179 in rpc_loop size /*? connector.badge_symbol ?*/ end 180 /*- endfor -*/ 181 | unused => (Utils.fail "Unexpected method_id") 182 in () end 183 /*- endfor -*/ 184 else 185 (Utils.fail "Unexpected badge") 186`; 187 188val run_def = process_topdecs ` 189 fun run u = let 190 /*? recv_first_rpc(connector, 'size', me.might_block()) ?*/ 191 in (rpc_loop size /*? connector.badge_symbol ?*/) end; 192`; 193 194val _ = app append_prog [ 195 rpc_loop_def, 196 run_def 197]; 198 199val _ = ml_prog_update (close_module NONE); 200 201val _ = export_theory (); 202 203/*- endif -*/ 204