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