1/* The Rust const asserts that span packages and call functions, the FRAMES guard, and the Rust's
2 * layout_tests::regions_have_no_aliased_fields, over the whole contract. */
3#include "mesh/abi.h"
4#include "mesh/check.h"
5
6int main(void) {
7    CHECK(mesh_disjoint(MESH_HEADER_FIELDS, MESH_HEADER_FIELDS_LEN)); /* disjoint(&HEADER_FIELDS) */
8    CHECK(mesh_disjoint(MESH_EXT_FIELDS, MESH_EXT_FIELDS_LEN)); /* disjoint(&EXT_FIELDS) */
9    CHECK(mesh_disjoint(MESH_HOST_FIELDS, MESH_HOST_FIELDS_LEN)); /* disjoint(&HOST_FIELDS) */
10    CHECK(mesh_disjoint(MESH_MEMBER_FIELDS, MESH_MEMBER_FIELDS_LEN)); /* disjoint(&MEMBER_FIELDS) */
11    CHECK(mesh_disjoint(MESH_LINK_FIELDS, MESH_LINK_FIELDS_LEN)); /* disjoint(&LINK_FIELDS) */
12    CHECK(mesh_disjoint(MESH_NIC_FIELDS, MESH_NIC_FIELDS_LEN)); /* disjoint(&NIC_FIELDS) */
13    CHECK(mesh_disjoint(MESH_CTL_FIELDS, MESH_CTL_FIELDS_LEN)); /* disjoint(&CTL_FIELDS) */
14    CHECK(mesh_fields_end(MESH_CTL_FIELDS, MESH_CTL_FIELDS_LEN) <= MESH_LINE); /* fields_end(&CTL_FIELDS) <= LINE */
15    CHECK(mesh_disjoint(MESH_NODE_FIELDS, MESH_NODE_FIELDS_LEN)); /* disjoint(&NODE_FIELDS) */
16    CHECK(mesh_fields_end(MESH_NODE_FIELDS, MESH_NODE_FIELDS_LEN) <= MESH_NODE_STRIDE); /* fields_end(&NODE_FIELDS) <= NODE_STRIDE */
17    CHECK(mesh_disjoint(MESH_NODE_LOAD_FIELDS, MESH_NODE_LOAD_FIELDS_LEN)); /* disjoint(&NODE_LOAD_FIELDS) */
18    CHECK(mesh_fields_end(MESH_NODE_LOAD_FIELDS, MESH_NODE_LOAD_FIELDS_LEN) <= MESH_NL_STRIDE); /* fields_end(&NODE_LOAD_FIELDS) <= NL_STRIDE */
19    CHECK(mesh_disjoint(MESH_MLOAD_FIELDS, MESH_MLOAD_FIELDS_LEN)); /* disjoint(&MLOAD_FIELDS) */
20    CHECK(mesh_fields_end(MESH_MLOAD_FIELDS, MESH_MLOAD_FIELDS_LEN) <= MESH_MLOAD_BYTES); /* fields_end(&MLOAD_FIELDS) <= MLOAD_BYTES */
21    CHECK(mesh_disjoint(MESH_PLOAD_FIELDS, MESH_PLOAD_FIELDS_LEN)); /* disjoint(&PLOAD_FIELDS) */
22    CHECK(mesh_fields_end(MESH_PLOAD_FIELDS, MESH_PLOAD_FIELDS_LEN) <= MESH_PLOAD_BYTES); /* fields_end(&PLOAD_FIELDS) <= PLOAD_BYTES */
23    CHECK(mesh_prog_ext(MESH_PROG_SLOTS ) + 0x8000 <= MESH_NODE_LOAD); /* prog_ext(PROG_SLOTS as u32) + 0x8000 <= NODE_LOAD */
24    CHECK(mesh_node_load(MESH_PROG_SLOTS , 0) <= MESH_LOAD_PAGE); /* node_load(PROG_SLOTS as u32, 0) <= LOAD_PAGE */
25    CHECK(mesh_load_page(MESH_S_LOAD_END) <= MESH_PIPE_TABLE); /* load_page(S_LOAD_END) <= PIPE_TABLE */
26    CHECK(mesh_pipe_entry(MESH_PROG_SLOTS ) <= MESH_VIEW_HEAP); /* pipe_entry(PROG_SLOTS as u32) <= VIEW_HEAP */
27    CHECK(mesh_disjoint(MESH_PIPE_FIELDS, MESH_PIPE_FIELDS_LEN)); /* disjoint(&PIPE_FIELDS) */
28    CHECK(mesh_fields_end(MESH_PIPE_FIELDS, MESH_PIPE_FIELDS_LEN) <= MESH_PP_BYTES); /* fields_end(&PIPE_FIELDS) <= PP_BYTES */
29    CHECK(mesh_nic(MESH_MAX_NICS) <= MESH_S_LOAD); /* nic(MAX_NICS) <= S_LOAD */
30    CHECK(mesh_mload(MESH_MAX_SYSTEMS) <= 0x1400); /* mload(MAX_SYSTEMS) <= 0x1400 */
31    CHECK(mesh_pload(MESH_PROG_SLOTS ) == MESH_S_LOAD_END); /* pload(PROG_SLOTS as u32) == S_LOAD_END */
32    CHECK(mesh_mload(MESH_MAX_SYSTEMS) <= MESH_S_FLEET); /* mload(MAX_SYSTEMS) <= S_FLEET */
33    CHECK(mesh_fmember(MESH_MAX_SYSTEMS) <= MESH_S_GROUP); /* fmember(MAX_SYSTEMS) <= S_GROUP */
34    CHECK(mesh_placed(MESH_PROG_SLOTS ) <= MESH_S_SCHED_END); /* placed(PROG_SLOTS as u32) <= S_SCHED_END */
35    CHECK(mesh_frame_kind(MESH_F_JOB_STATE) == MESH_KIND_LOAD); /* frame_kind(F_JOB_STATE) == KIND_LOAD */
36    CHECK(mesh_frame_kind(MESH_F_RESULT) == MESH_KIND_LOAD); /* frame_kind(F_RESULT) == KIND_LOAD */
37    CHECK(mesh_frame_kind(MESH_F_VIEW) == MESH_KIND_LOAD); /* frame_kind(F_VIEW) == KIND_LOAD */
38    CHECK(mesh_frame_kind(MESH_F_BLOB) == MESH_KIND_LOAD); /* frame_kind(F_BLOB) == KIND_LOAD */
39    CHECK(mesh_disjoint(MESH_FMEMBER_FIELDS, MESH_FMEMBER_FIELDS_LEN)); /* disjoint(&FMEMBER_FIELDS) */
40    CHECK(mesh_fields_end(MESH_FMEMBER_FIELDS, MESH_FMEMBER_FIELDS_LEN) <= MESH_FMEMBER_BYTES); /* fields_end(&FMEMBER_FIELDS) <= FMEMBER_BYTES */
41    CHECK(mesh_fields_end(MESH_HEADER_FIELDS, MESH_HEADER_FIELDS_LEN) <= MESH_H_BYTES); /* fields_end(&HEADER_FIELDS) <= H_BYTES */
42    CHECK(mesh_fields_end(MESH_EXT_FIELDS, MESH_EXT_FIELDS_LEN) <= MESH_PX_BYTES); /* fields_end(&EXT_FIELDS) <= PX_BYTES */
43    CHECK(mesh_fields_end(MESH_HOST_FIELDS, MESH_HOST_FIELDS_LEN) <= MESH_SNAP_HOST); /* fields_end(&HOST_FIELDS) <= SNAP_HOST */
44    CHECK(mesh_fields_end(MESH_MEMBER_FIELDS, MESH_MEMBER_FIELDS_LEN) <= MESH_MEMBER_BYTES); /* fields_end(&MEMBER_FIELDS) <= MEMBER_BYTES */
45    CHECK(mesh_fields_end(MESH_LINK_FIELDS, MESH_LINK_FIELDS_LEN) <= MESH_LINK_BYTES); /* fields_end(&LINK_FIELDS) <= LINK_BYTES */
46    CHECK(mesh_fields_end(MESH_NIC_FIELDS, MESH_NIC_FIELDS_LEN) <= MESH_NIC_BYTES); /* fields_end(&NIC_FIELDS) <= NIC_BYTES */
47    CHECK(mesh_member(MESH_MAX_SYSTEMS) <= MESH_S_NET_AT_MS); /* member(MAX_SYSTEMS) <= S_NET_AT_MS */
48    CHECK(mesh_link(MESH_MAX_SYSTEMS) <= MESH_S_NICS); /* link(MAX_SYSTEMS) <= S_NICS */
49    CHECK(mesh_nic(MESH_MAX_NICS) <= MESH_SNAP_HOST); /* nic(MAX_NICS) <= SNAP_HOST */
50    CHECK(mesh_frame_kind(MESH_F_ROUND) == MESH_KIND_ROUND); /* frame_kind(F_ROUND) == KIND_ROUND */
51    CHECK(mesh_frame_kind(MESH_F_FRAME) == MESH_KIND_PLACE); /* frame_kind(F_FRAME) == KIND_PLACE */
52    CHECK(mesh_frame_kind(MESH_F_STATE) == MESH_KIND_LOAD); /* frame_kind(F_STATE) == KIND_LOAD */
53    CHECK(mesh_frame_kind(MESH_F_BEAT) == MESH_KIND_CTL); /* frame_kind(F_BEAT) == KIND_CTL */
54    CHECK(mesh_frame_kind(MESH_F_JOIN) == MESH_KIND_CTL); /* frame_kind(F_JOIN) == KIND_CTL */
55    CHECK(mesh_prog_entry(MESH_PROG_SLOTS ) <= MESH_PROG_CTL); /* prog_entry(PROG_SLOTS as u32) <= PROG_CTL */
56    CHECK(mesh_prog_ctl(MESH_PROG_SLOTS ) <= MESH_PROG_NODES); /* prog_ctl(PROG_SLOTS as u32) <= PROG_NODES */
57    CHECK(mesh_trace_rec(MESH_PROG_SLOTS  - 1, MESH_TRACE_PER_PROG - 1) + MESH_TRACE_BYTES <= MESH_EX_BASE); /* trace_rec(PROG_SLOTS as u32 - 1, TRACE_PER_PROG - 1) + TRACE_BYTES <= EX_BASE */
58    CHECK(mesh_ex_counter(MESH_MAX_SYSTEMS) <= mesh_ex_slots(0)); /* ex_counter(MAX_SYSTEMS) <= ex_slots(0) */
59    CHECK(mesh_ex_slots(MESH_MAX_SYSTEMS - 1) + MESH_EX_REGION_BYTES <= MESH_EX_BASE + MESH_EX_BYTES); /* ex_slots(MAX_SYSTEMS - 1) + EX_REGION_BYTES <= EX_BASE + EX_BYTES */
60    CHECK(mesh_prog_ext(MESH_PROG_SLOTS ) <= MESH_VIEW_HEAP); /* prog_ext(PROG_SLOTS as u32) <= VIEW_HEAP */
61    CHECK(mesh_member(MESH_MAX_SYSTEMS) <= MESH_SNAP_HOST); /* member(MAX_SYSTEMS) <= SNAP_HOST */
62    /* Every peer frame type, in id order: unique and dense (1..=32). */
63    for (size_t i = 0; i < MESH_FRAMES_LEN; i++) CHECK_U(MESH_FRAMES[i], i + 1);
64    /* regions_have_no_aliased_fields */
65    struct { const char *name; const mesh_field *f; size_t n; } regions[] = {
66        {"header", MESH_HEADER_FIELDS, MESH_HEADER_FIELDS_LEN}, {"extension", MESH_EXT_FIELDS, MESH_EXT_FIELDS_LEN},
67        {"host", MESH_HOST_FIELDS, MESH_HOST_FIELDS_LEN}, {"member", MESH_MEMBER_FIELDS, MESH_MEMBER_FIELDS_LEN},
68        {"link", MESH_LINK_FIELDS, MESH_LINK_FIELDS_LEN}, {"nic", MESH_NIC_FIELDS, MESH_NIC_FIELDS_LEN},
69        {"node", MESH_NODE_FIELDS, MESH_NODE_FIELDS_LEN}, {"node load", MESH_NODE_LOAD_FIELDS, MESH_NODE_LOAD_FIELDS_LEN},
70        {"member load", MESH_MLOAD_FIELDS, MESH_MLOAD_FIELDS_LEN}, {"program load", MESH_PLOAD_FIELDS, MESH_PLOAD_FIELDS_LEN},
71        {"control", MESH_CTL_FIELDS, MESH_CTL_FIELDS_LEN}, {"pipe", MESH_PIPE_FIELDS, MESH_PIPE_FIELDS_LEN},
72        {"fleet member", MESH_FMEMBER_FIELDS, MESH_FMEMBER_FIELDS_LEN},
73    };
74    for (size_t i = 0; i < sizeof regions / sizeof regions[0]; i++)
75        if (!CHECK(mesh_disjoint(regions[i].f, regions[i].n))) fprintf(stderr, "%s: two fields overlap\n", regions[i].name);
76    return mesh_check_done();
77}