From a4f9a2a23eaa10a9b3ae1a1038bca28a19373e12 Mon Sep 17 00:00:00 2001 From: Mike Dodds Date: Thu, 28 Nov 2024 13:55:49 -0800 Subject: [PATCH] mkm: verified memory safety of remaining client fns --- .../mission_key_management/client-reduced.c | 179 ++++++++++-------- .../mission_key_management/client-test-mp.c | 13 ++ components/mission_key_management/cn_stubs.h | 103 ++++++++-- components/mission_key_management/mkm.h | 14 ++ components/mission_key_management/test_funs.c | 179 ++++++++++++++++++ .../test_gen/client-test-mp-exec.c | 45 +++++ .../test_gen/client-test-mp_gen.h | 26 +++ .../test_gen/client-test-mp_test.c | 36 ++++ .../mission_key_management/test_gen/cn.c | 36 ++++ .../mission_key_management/test_gen/cn.h | 47 +++++ .../test_gen/run_tests.sh | 38 ++++ 11 files changed, 612 insertions(+), 104 deletions(-) create mode 100644 components/mission_key_management/client-test-mp.c create mode 100644 components/mission_key_management/mkm.h create mode 100644 components/mission_key_management/test_funs.c create mode 100644 components/mission_key_management/test_gen/client-test-mp-exec.c create mode 100644 components/mission_key_management/test_gen/client-test-mp_gen.h create mode 100644 components/mission_key_management/test_gen/client-test-mp_test.c create mode 100644 components/mission_key_management/test_gen/cn.c create mode 100644 components/mission_key_management/test_gen/cn.h create mode 100755 components/mission_key_management/test_gen/run_tests.sh diff --git a/components/mission_key_management/client-reduced.c b/components/mission_key_management/client-reduced.c index acf8f99a..12368331 100644 --- a/components/mission_key_management/client-reduced.c +++ b/components/mission_key_management/client-reduced.c @@ -38,15 +38,15 @@ uint32_t client_state_epoll_events(enum client_state state) { struct client* client_new(int fd) /*$ -trusted; +// TODO: Doesn't handle the case where malloc fails ensures take Client_out = Owned(return); Client_out.fd == fd; Client_out.pos == 0u8; - // TODO: can't refer to the enum in a specification - // Client_out.state == C_RECV_KEY_ID; + ((i32) Client_out.state) == CS_RECV_KEY_ID; $*/ { + // TODO: malloc spec assumes alloction always succeeds struct client* c = malloc(sizeof(struct client)); if (c == NULL) { perror("malloc (client_new)"); @@ -60,10 +60,8 @@ ensures void client_delete(struct client* c) /*$ -trusted; requires take Client_in = Owned(c); -// TODO: handle close / perror properly $*/ { int ret = close(c->fd); @@ -115,7 +113,7 @@ ensures ptr_eq( return, member_shift(c, challenge) ) } else { if (((i32) Client_in.state) == CS_SEND_KEY) { - // TODO: fix this case + // TODO: fix the mission_key case is_null(return) } else { is_null(return) @@ -127,9 +125,9 @@ ensures return c->challenge; case CS_SEND_KEY: { // /*$ extract Owned, 0u64; $*/ - // return get_mission_key(c->key_id[0]); - // TODO: fix the mission keys stuff - return NULL; + const uint8_t* ret = NULL; // get_mission_key(c->key_id[0]); + return ret; + // TODO: Fix mission key stuff } default: return NULL; @@ -143,7 +141,8 @@ requires ensures take Client_out = Owned(c); Client_out == Client_in; - // TODO: have to concretize the array sizes + // TODO: ideally we'd get the field sizes implicitly. + // Here we have to write them as concrete values return == ( if (((i32) Client_in.state) == CS_RECV_KEY_ID) { 1u64 @@ -170,7 +169,8 @@ ensures return 0; default: - // Unreachable + // Prove that this state is unreachable: + /*@ assert false; @*/ return 0; } } @@ -216,14 +216,15 @@ ensures return RES_DONE; } + // TODO: unclear why this works??? /*$ split_case(Client_in.state == (u32) CS_RECV_KEY_ID); $*/ + // TODO: array subsetting isn't handled. Probably need a lemma here int ret = read(c->fd, buf, buf_size); // int ret = read(c->fd, buf + c->pos, buf_size - (size_t) c->pos); if (ret < 0) { - // TODO: commented out perror, should give it a spec - // perror("read (client_read)"); + perror("read (client_read)"); return RES_ERROR; } else if (ret == 0) { return RES_EOF; @@ -253,13 +254,12 @@ ensures return RES_DONE; } - // TODO: array subsetting isn't handled. Probably need a lemma here + // TODO: Fix array subsetting. Probably need a lemma here int ret = write(c->fd, buf, buf_size); // int ret = write(c->fd, buf + c->pos, buf_size - c->pos); if (ret < 0) { - // TODO: re-enable this - // perror("write (client_write)"); + perror("write (client_write)"); return RES_ERROR; } else if (ret == 0) { return RES_EOF; @@ -290,70 +290,83 @@ ensures c->pos = 0; } -// enum client_event_result client_event(struct client* c, uint32_t events) { -// if (events & EPOLLIN) { -// enum client_event_result result = client_read(c); -// if (result != RES_DONE) { -// return result; -// } -// } -// if (events & EPOLLOUT) { -// enum client_event_result result = client_write(c); -// if (result != RES_DONE) { -// return result; -// } -// } - -// if (c->pos < client_buffer_size(c)) { -// // Async read/write operation isn't yet finished. -// // -// // This should be unreachable. `client_event` should only be called -// // when progress can be made on a current async read or write -// // operation, and the call to `client_read`/`client_write` above will -// // return `RES_PENDING` (causing `client_event` to return early) if the -// // operation isn't finished. -// return RES_PENDING; -// } - -// // The async operation for the current state is finished. We can now -// // transition to the next state. -// switch (c->state) { -// case CS_RECV_KEY_ID: -// memcpy(c->challenge, "This challenge is totally random", 32); -// client_change_state(c, CS_SEND_CHALLENGE); -// break; - -// case CS_SEND_CHALLENGE: -// client_change_state(c, CS_RECV_RESPONSE); -// break; - -// case CS_RECV_RESPONSE: -// { -// // TODO: properly validate the response -// int resp_ok = memcmp(c->challenge, c->response, 32) == 0; -// if (!resp_ok) { -// fprintf(stderr, "client %d: error: bad response\n", c->fd); -// return RES_ERROR; -// } -// uint8_t key_id = c->key_id[0]; -// if (key_id >= NUM_SECRET_KEYS) { -// fprintf(stderr, "client %d: error: bad request for key %u\n", c->fd, key_id); -// return RES_ERROR; -// } -// client_change_state(c, CS_SEND_KEY); -// fprintf(stderr, "client %d: sending key %u\n", c->fd, key_id); -// } -// break; - -// case CS_SEND_KEY: -// client_change_state(c, CS_DONE); -// break; - -// case CS_DONE: -// // No-op. This connection is finished, and the main loop should -// // disconnect. -// break; -// } - -// return RES_DONE; -// } +enum client_event_result client_event(struct client* c, uint32_t events) +/*$ +requires + take Client_in = Owned(c); +ensures + take Client_out = Owned(c); +$*/ +{ + if (events & EPOLLIN) { + enum client_event_result result = client_read(c); + if (result != RES_DONE) { + return result; + } + } + if (events & EPOLLOUT) { + enum client_event_result result = client_write(c); + if (result != RES_DONE) { + return result; + } + } + + if (c->pos < client_buffer_size(c)) { + // Async read/write operation isn't yet finished. + // + // This should be unreachable. `client_event` should only be called + // when progress can be made on a current async read or write + // operation, and the call to `client_read`/`client_write` above will + // return `RES_PENDING` (causing `client_event` to return early) if the + // operation isn't finished. + return RES_PENDING; + } + + // The async operation for the current state is finished. We can now + // transition to the next state. + + switch (c->state) { + case CS_RECV_KEY_ID: { // <-- TODO: note extra block needed for var declaration + // TODO: fix string argument nonsense here + // memcpy(c->challenge, "This challenge is totally random", 32); + uint8_t challenge[32] = "This challenge is totally random"; + memcpy(c->challenge, &challenge, 32); + client_change_state(c, CS_SEND_CHALLENGE); + break; + } + + case CS_SEND_CHALLENGE: + client_change_state(c, CS_RECV_RESPONSE); + break; + + case CS_RECV_RESPONSE: + { + // TODO: properly validate the response + int resp_ok = memcmp(c->challenge, c->response, 32) == 0; + if (!resp_ok) { + fprintf(stderr, "client %d: error: bad response\n", c->fd); + return RES_ERROR; + } + /*$ extract Owned, 0u64; $*/ + uint8_t key_id = c->key_id[0]; + if (key_id >= NUM_SECRET_KEYS) { + fprintf(stderr, "client %d: error: bad request for key %u\n", c->fd, key_id); + return RES_ERROR; + } + client_change_state(c, CS_SEND_KEY); + fprintf(stderr, "client %d: sending key %u\n", c->fd, key_id); + } + break; + + case CS_SEND_KEY: + client_change_state(c, CS_DONE); + break; + + case CS_DONE: + // No-op. This connection is finished, and the main loop should + // disconnect. + break; + } + + return RES_DONE; +} diff --git a/components/mission_key_management/client-test-mp.c b/components/mission_key_management/client-test-mp.c new file mode 100644 index 00000000..73551eee --- /dev/null +++ b/components/mission_key_management/client-test-mp.c @@ -0,0 +1,13 @@ +#include +#define EPOLLIN 1 + +enum client_state { + CS_RECV_KEY_ID, +}; + +uint32_t client_state_epoll_events(enum client_state state) { + switch (state) { + case CS_RECV_KEY_ID: + return EPOLLIN; + } +} diff --git a/components/mission_key_management/cn_stubs.h b/components/mission_key_management/cn_stubs.h index 7cec6bbe..130de37e 100644 --- a/components/mission_key_management/cn_stubs.h +++ b/components/mission_key_management/cn_stubs.h @@ -2,7 +2,6 @@ // Provides substitutes for some declarations that CN has trouble with. - // Cerberus puts some POSIX headers under the `posix/` directory. #include @@ -18,10 +17,13 @@ // not possible to call this due to CN issue #309 // this spec isn't right but can't develop it at all without #309 void perror(const char *msg); -/*$ spec perror(pointer msg); - requires take mi = Owned(msg); - ensures take mo = Owned(msg); - mi == mo; +/*$ +spec perror(pointer msg); +requires + take mi = Owned(msg); +ensures + take mo = Owned(msg); + mi == mo; $*/ #else # define perror(...) 0 @@ -37,6 +39,7 @@ void perror(const char *msg); // From `unistd.h` +// // Old version, updated by MDD below // ssize_t _read(int fildes, void *buf, size_t n); // /*$ spec _read(i32 fildes, pointer buf, u64 n); // // accesses errno; @@ -51,33 +54,33 @@ void perror(const char *msg); // take bufb = each(u64 i; (return == -1i64) ? (0u64 <= i && i < n) : ((u64)return <= i && i < n)) {Block(array_shift(buf, i))}; // $*/ -ssize_t _read(int fildes, void *buf, size_t n); +ssize_t _read_uint8_t(int fildes, void *buf, size_t n); /*$ -spec _read(i32 fildes, pointer buf, u64 n); +spec _read_uint8_t(i32 fildes, pointer buf, u64 n); requires - take buf_in = - each (u64 i; i < n) { Owned(array_shift(buf, i))}; + take buf_in = each (u64 i; i < n) { Owned(array_shift(buf, i))}; ensures return >= -1i64 && return <= (i64)n; - take buf_out = - each (u64 i; i < n) { Owned(array_shift(buf, i))}; + take buf_out = each (u64 i; i < n) { Owned(array_shift(buf, i))}; $*/ -#define read(f,b,s) _read(f,b,s) +#define read(f,b,s) _read_uint8_t(f,b,s) int _close(int fildes); -/*$ spec _close(i32 fildes); - requires true; - ensures true; +/*$ +spec _close(i32 fildes); +requires true; +ensures true; $*/ #define close(x) _close(x) -ssize_t _write(int fildes, const void *buf, size_t nbyte); -/*$ spec _write(i32 fildes, pointer buf, u64 nbyte); - requires +ssize_t _write_uint8_t(int fildes, const void *buf, size_t nbyte); +/*$ +spec _write_uint8_t(i32 fildes, pointer buf, u64 nbyte); +requires ((i32)nbyte) >= 0i32; - take bufi = each(u64 i; i >= 0u64 && i < nbyte) {Owned(array_shift(buf,i))}; - ensures - take bufo = each(u64 i; i >= 0u64 && i < nbyte) {Owned(array_shift(buf,i))}; + take bufi = each(u64 i; i < nbyte) {Owned(array_shift(buf,i))}; +ensures + take bufo = each(u64 i; i < nbyte) {Owned(array_shift(buf,i))}; bufi == bufo; return >= -1i64 && return < (i64)nbyte; $*/ @@ -90,3 +93,61 @@ int _shutdown(int fildes, int how); $*/ #define shutdown(x,h) _shutdown(x,h) +#define write(f,b,s) _write_uint8_t(f,b,s) + +void *_memcpy_uint8_t(void *dest, const void *src, size_t nbyte); +/*$ +spec _memcpy_uint8_t(pointer dest, pointer src, u64 nbyte); +requires + ((i32)nbyte) >= 0i32; + take src_in = each (u64 i; i < nbyte) { Owned(array_shift(src,i)) }; + take dest_in = each (u64 i; i < nbyte) { Owned(array_shift(dest,i)) }; +ensures + take src_out = each (u64 i; i < nbyte) { Owned(array_shift(src,i)) }; + take dest_out = each (u64 i; i < nbyte) { Owned(array_shift(dest,i)) }; + src_in == src_out; + // TODO: is this the right behavior? + if (is_null(return)) { + dest_out == dest_in + } else { + ptr_eq(return, dest) + && + dest_out == src_out + }; +$*/ +#define memcpy(d,s,n) _memcpy_uint8_t(d,s,n) + +int _memcmp_uint8_t(const void *s1, const void *s2, size_t nbyte); +/*$ +spec _memcmp_uint8_t(pointer s1, pointer s2, u64 nbyte); +requires + ((i32)nbyte) >= 0i32; + take S1_in = each (u64 i; i < nbyte) { Owned(array_shift(s1,i)) }; + take S2_in = each (u64 i; i < nbyte) { Owned(array_shift(s2,i)) }; +ensures + take S1_out = each (u64 i; i < nbyte) { Owned(array_shift(s1,i)) }; + take S2_out = each (u64 i; i < nbyte) { Owned(array_shift(s2,i)) }; + S1_out == S1_in; S2_out == S2_in; + if (S1_in == S2_in) { return > 0i32 } else { return == 0i32 }; +$*/ +#define memcmp(s1,s2,n) _memcmp_uint8_t(s1,s2,n) + +struct client *_malloc_struct_client(size_t nbyte); +/*$ +spec _malloc_struct_client(u64 nbyte); +requires + ((i32)nbyte) >= 0i32; +ensures + take Client_out = Owned(return); +$*/ +#define malloc(n) _malloc_struct_client(n) + +void _free_struct_client(struct client *target); +/*$ +spec _free_struct_client(pointer target); +requires + take Client_out = Owned(target); +ensures + true; +$*/ +#define free(t) _free_struct_client(t) diff --git a/components/mission_key_management/mkm.h b/components/mission_key_management/mkm.h new file mode 100644 index 00000000..cd32b1b0 --- /dev/null +++ b/components/mission_key_management/mkm.h @@ -0,0 +1,14 @@ +#pragma once + +#include + +#define NUM_SECRET_KEYS 2 +#define SECRET_KEY_SIZE 32 +const uint8_t* get_mission_key(uint8_t key_id); +/*$ // TODO: spec is wrong, need to handle this properly +spec get_mission_key(u8 key_id); +requires + true; +ensures + is_null(return); +$*/ diff --git a/components/mission_key_management/test_funs.c b/components/mission_key_management/test_funs.c new file mode 100644 index 00000000..94a93955 --- /dev/null +++ b/components/mission_key_management/test_funs.c @@ -0,0 +1,179 @@ +#include +#include + +#include "client.h" +#include "mkm.h" +#include "cn_stubs.h" + +// uint8_t *client_field_ptr(struct client *c) +// /*@ +// requires +// take Client = Owned(c); +// ensures +// take Client_ = Owned(c); +// return == member_shift(c, key_id); +// @*/ +// { +// /*@ extract Owned, 0u64; @*/ +// return c->key_id; +// } + +// void client_buf_size_1(struct client *c, uint8_t pos) +// /*@ +// requires +// take Client = Owned(c); +// ensures +// take Client_ = Owned(c); +// @*/ +// { +// size_t buf_size = sizeof(c->response); +// uint8_t* buf = c->response; + +// if (pos >= buf_size) { +// return; +// } + +// uint8_t* tmp = buf + pos; +// } + +// uint8_t* client_read_buffer__(struct client* c) +// /*@ +// requires +// take Client = Owned(c); +// ensures +// take Client_ = Owned(c); +// ptr_eq(return, member_shift(c,response) ); +// @*/ +// { +// return c->response; +// } + +// const size_t client_buffer_size__(struct client* c) +// /*@ +// ensures +// return == 32u64; +// @*/ +// { +// return sizeof(c->response); +// } + + +// void client_buf_size_2(struct client *c, uint8_t pos) +// /*@ +// requires +// take Client = Owned(c); +// ensures +// take Client_ = Owned(c); +// @*/ +// { +// size_t buf_size = client_buffer_size__(c); +// uint8_t* buf = client_read_buffer__(c); + +// if (pos >= buf_size) { +// return; +// } + +// uint8_t* tmp = buf + pos; +// } + +// static const uint8_t mission_keys__[2][2] = { +// {'a', 'b'}, +// {'c', 'd'} +// }; + +// const uint8_t* get_mission_key__(uint8_t key_id) +// /*@ +// accesses mission_keys__; +// ensures +// return == array_shift(mission_keys__[(u64) key_id], 0u64); +// @*/ +// { +// // /*@ extract Owned, key_id; @*/ +// return mission_keys[key_id]; +// } + +void mem_access(void *buf, size_t n); +/*$ +spec mem_access(pointer buf, u64 n); +requires + take buf_in = each (u64 i; i < n) { Owned(array_shift(buf, i))}; +ensures + take buf_out = each (u64 i; i < n) { Owned(array_shift(buf, i))}; +$*/ + + +void test_mem_access_whole(uint8_t *target, size_t size, size_t offset) +/*$ +requires + offset < size; + take target_in = each (u64 i; 0u64 <= i && i < size) + { Owned(array_shift(target, i))}; +ensures + take target_out = each (u64 i; 0u64 <= i && i < size) + { Owned(array_shift(target, i))}; +$*/ +{ + mem_access(target, size); +} + +/*$ +lemma mem_merge(pointer head, u64 seg1, u64 seg2) +requires + take seg1_in = each (u64 i; i < seg1) + { Owned(array_shift(head, i))}; + take seg2_in = each (u64 i; seg1 <= i && i < (seg1 + seg2)) + { Owned(array_shift(head, i))}; +ensures + take seg_out = each (u64 i; i < (seg1 + seg2) ) + { Owned(array_shift(head, i))}; +$*/ + +void test_mem_access_cutoff_end(uint8_t *target, size_t size, size_t offset) +/*$ +requires + // size <= 4u64; + offset < size; + take target_in = each (u64 i; i < size) + { Owned(array_shift(target, i))}; +ensures + take target_out = each (u64 i; i < size) + { Owned(array_shift(target, i))}; +$*/ +{ + mem_access(target, offset); + /*$ apply mem_merge(target, offset, (size - offset)); $*/ +} + +/*$ +lemma mem_split(pointer head, u64 size, u64 seg1) +requires + seg1 <= size; + take seg_out = each (u64 i; i < size) + { Owned(array_shift(head, i))}; +ensures + take seg1_out = each (u64 i; i < seg1) + { Owned(array_shift(head, i))}; + take seg2_out = each (u64 i; seg1 <= i && i < size) + { Owned(array_shift(head, i))}; +$*/ + +// Doesn't work: + +void test_mem_access_cutoff_start(uint8_t *target, size_t size, size_t offset) +/*$ +requires + // offset == 2u64; // make the counterexamples nicer + // size == 4u64; // make the counterexamples nicer + offset < size; + take target_in = each (u64 i; i < size) + { Owned(array_shift(target, i))}; +ensures + take target_out = each (u64 i; i < size) + { Owned(array_shift(target, i))}; +$*/ +{ + /*$ apply mem_split(target, size, offset); $*/ + /*$ extract Owned, offset; $*/ // Needed so target + offset is defined + mem_access(target + offset, size - offset); + // TODO: need a mem_merge here too ... +} \ No newline at end of file diff --git a/components/mission_key_management/test_gen/client-test-mp-exec.c b/components/mission_key_management/test_gen/client-test-mp-exec.c new file mode 100644 index 00000000..94ccdae6 --- /dev/null +++ b/components/mission_key_management/test_gen/client-test-mp-exec.c @@ -0,0 +1,45 @@ +#include "cn.h" +#include +#include +#include +#include + +#include +#define EPOLLIN 1 + +enum client_state { + CS_RECV_KEY_ID, +}; + +uint32_t client_state_epoll_events(enum client_state state) { + /* EXECUTABLE CN PRECONDITION */ + unsigned int __cn_ret; + ghost_stack_depth_incr(); + cn_bits_u32* state_cn = convert_to_cn_bits_u32(state); + + /* C OWNERSHIP */ + + c_add_to_ghost_state((uintptr_t) &state, sizeof(enum client_state), get_cn_stack_depth()); + + switch (CN_LOAD(state)) { + case CS_RECV_KEY_ID: + { __cn_ret = E; goto __cn_epilogue; }OLLIN; + } + +/* EXECUTABLE CN POSTCONDITION */ +__cn_epilogue: + + + /* C OWNERSHIP */ + + + c_remove_from_ghost_state((uintptr_t) &state, sizeof(enum client_state)); + +{ + cn_bits_u32* return_cn = convert_to_cn_bits_u32(__cn_ret); + ghost_stack_depth_decr(); +} + +return __cn_ret; + +} diff --git a/components/mission_key_management/test_gen/client-test-mp_gen.h b/components/mission_key_management/test_gen/client-test-mp_gen.h new file mode 100644 index 00000000..82a7921b --- /dev/null +++ b/components/mission_key_management/test_gen/client-test-mp_gen.h @@ -0,0 +1,26 @@ +#ifndef CN_GEN_H +#define CN_GEN_H + +#include + +#include "cn.h" + +struct cn_gen_client_state_epoll_events_record { + cn_bits_u32* cn_gen_state; +}; + +struct cn_gen_client_state_epoll_events_record* cn_gen_client_state_epoll_events(); + +struct cn_gen_client_state_epoll_events_record* cn_gen_client_state_epoll_events() +{ + CN_GEN_INIT(); + CN_GEN_LET_BEGIN(25, cn_gen_state); + CN_GEN_LET_BODY(cn_bits_u32, cn_gen_state, CN_GEN_UNIFORM(cn_bits_u32)); + CN_GEN_LET_END(25, cn_gen_state, bennet, NULL); + struct cn_gen_client_state_epoll_events_record* a_720 = (struct cn_gen_client_state_epoll_events_record*) alloc(sizeof(struct cn_gen_client_state_epoll_events_record)); + a_720->cn_gen_state = cn_gen_state; + cn_gen_decrement_depth(); + return (struct cn_gen_client_state_epoll_events_record*) a_720; +} + +#endif // CN_GEN_H diff --git a/components/mission_key_management/test_gen/client-test-mp_test.c b/components/mission_key_management/test_gen/client-test-mp_test.c new file mode 100644 index 00000000..06de279a --- /dev/null +++ b/components/mission_key_management/test_gen/client-test-mp_test.c @@ -0,0 +1,36 @@ +#include "client-test-mp_gen.h" +#include "client-test-mp-exec.c" +#include "cn.c" + +////////////////////////////// +// Assume Ownership Functions // +////////////////////////////// + +void assume_client_state_epoll_events(enum client_state); + +void assume_client_state_epoll_events(enum client_state state) +{ + cn_bits_u32* state_cn = convert_to_cn_bits_u32(state); + return; +} +////////////////////////////// +///////// Unit tests ///////// +////////////////////////////// + + + +////////////////////////////// +//////// Random tests //////// +////////////////////////////// + +CN_RANDOM_TEST_CASE(client-test-mp, client_state_epoll_events, 100, convert_from_cn_bits_u32(res->cn_gen_state)) + +////////////////////////////// +/////// Main function /////// +////////////////////////////// + +int main(int argc, char* argv[]) +{ + cn_register_test_case((char*)"client-test-mp", (char*)"client_state_epoll_events", &cn_test_client_state_epoll_events); + return cn_test_main(argc, argv); +} diff --git a/components/mission_key_management/test_gen/cn.c b/components/mission_key_management/test_gen/cn.c new file mode 100644 index 00000000..ddc3bf66 --- /dev/null +++ b/components/mission_key_management/test_gen/cn.c @@ -0,0 +1,36 @@ +#include "cn.h" +cn_bool* struct_a_673_record_equality(void* x, void* y) +{ + struct a_673_record* x_cast = (struct a_673_record*) x; + struct a_673_record* y_cast = (struct a_673_record*) y; + return convert_to_cn_bool(true); +} + +struct a_673_record* default_struct_a_673_record() +{ + struct a_673_record* a_693 = (struct a_673_record*) alloc(sizeof(struct a_673_record)); + return a_693; +} + +void* cn_map_get_struct_a_673_record(cn_map* m, cn_integer* key) +{ + void* ret = ht_get(m, (&key->val)); + if (0 == ret) + return (void*) default_struct_a_673_record(); + else + return ret; +} + +/* GENERATED STRUCT FUNCTIONS */ + + + +/* OWNERSHIP FUNCTIONS */ + + + + + +/* CN PREDICATES */ + + diff --git a/components/mission_key_management/test_gen/cn.h b/components/mission_key_management/test_gen/cn.h new file mode 100644 index 00000000..ee615b32 --- /dev/null +++ b/components/mission_key_management/test_gen/cn.h @@ -0,0 +1,47 @@ +#ifndef CN_HEADER +#define CN_HEADER +#include + + + + +/* CN RECORDS */ + + +struct a_673_record { + ; +}; + + +/* ORIGINAL C STRUCTS */ + + + +/* CN VERSIONS OF C STRUCTS */ + + + + + + +/* OWNERSHIP FUNCTIONS */ + + + + + +/* GENERATED STRUCT FUNCTIONS */ + + + +cn_bool* struct_a_673_record_equality(void*, void*); +struct a_673_record* default_struct_a_673_record(); +void* cn_map_get_struct_a_673_record(cn_map*, cn_integer*); + +/* CN FUNCTIONS */ + + + + + +#endif \ No newline at end of file diff --git a/components/mission_key_management/test_gen/run_tests.sh b/components/mission_key_management/test_gen/run_tests.sh new file mode 100755 index 00000000..da4cb331 --- /dev/null +++ b/components/mission_key_management/test_gen/run_tests.sh @@ -0,0 +1,38 @@ +#!/bin/bash + +# copied from cn-runtime-single-file.sh +RUNTIME_PREFIX="$OPAM_SWITCH_PREFIX/lib/cn/runtime" +[ -d "${RUNTIME_PREFIX}" ] || ( + printf "Could not find CN's runtime directory (looked at: '${RUNTIME_PREFIX}')" + exit 1 +) + +TEST_DIR=test_gen +pushd $TEST_DIR > /dev/null + +# Compile +if cc -g -c "-I${RUNTIME_PREFIX}/include/" -o "./client-test-mp_test.o" "./client-test-mp_test.c" ; then + echo "Compiled C files." +else + printf "Failed to compile C files in ${TEST_DIR}." + exit 1 +fi + +# Link +if cc -g "-I${RUNTIME_PREFIX}/include" -o "./tests.out" client-test-mp_test.o "${RUNTIME_PREFIX}/libcn.a" ; then + echo "Linked C .o files." +else + printf "Failed to link *.o files in ${TEST_DIR}." + exit 1 +fi + +# Run +./tests.out +test_exit_code=$? # Save tests exit code for later + + + + +popd > /dev/null + +exit $test_exit_code