From ea123895b3d24589e5c243d12e1acad560802e0f Mon Sep 17 00:00:00 2001 From: yuyan Date: Mon, 31 May 2021 12:08:11 -0400 Subject: [PATCH 1/2] feat:initial attempts to test tipc;please provide gental feedback --- CMakeLists.txt | 1 + seahorn/trusty/CMakeLists.txt | 1 + .../trusty/user/base/lib/tipc/CMakeLists.txt | 14 ++++ .../base/lib/tipc/include/sea_tipc_helper.h | 8 +++ .../user/base/lib/tipc/proof/CMakeLists.txt | 2 + .../tipc/proof/tipc_connect/CMakeLists.txt | 5 ++ .../Testing/Temporary/CTestCostData.txt | 1 + .../Testing/Temporary/LastTest.log | 3 + .../base/lib/tipc/proof/tipc_connect/main.c | 13 ++++ .../lib/tipc/proof/tipc_send1/CMakeLists.txt | 5 ++ .../base/lib/tipc/proof/tipc_send1/main.c | 35 +++++++++ .../user/base/lib/tipc/trusty_ipc_impl.c | 72 +++++++++++++++++++ 12 files changed, 160 insertions(+) create mode 100644 seahorn/trusty/user/base/lib/tipc/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/tipc/include/sea_tipc_helper.h create mode 100644 seahorn/trusty/user/base/lib/tipc/proof/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/Testing/Temporary/CTestCostData.txt create mode 100644 seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/Testing/Temporary/LastTest.log create mode 100644 seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/main.c create mode 100644 seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/main.c create mode 100644 seahorn/trusty/user/base/lib/tipc/trusty_ipc_impl.c diff --git a/CMakeLists.txt b/CMakeLists.txt index 810b01d..dc6342f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -67,6 +67,7 @@ include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/hwkey/include) include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/keymaster/include) include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/rng/include) include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/storage/include) +include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/tipc/include) include_directories(${TRUSTY_ROOT}/trusty/kernel/include/uapi/) include_directories(${TRUSTY_ROOT}/trusty/kernel/lib/ubsan/include) include_directories(${TRUSTY_ROOT}/system/gatekeeper/include/) diff --git a/seahorn/trusty/CMakeLists.txt b/seahorn/trusty/CMakeLists.txt index e692b86..2bb96bd 100644 --- a/seahorn/trusty/CMakeLists.txt +++ b/seahorn/trusty/CMakeLists.txt @@ -1 +1,2 @@ add_subdirectory(user/base/lib/libc-trusty) +add_subdirectory(user/base/lib/tipc) diff --git a/seahorn/trusty/user/base/lib/tipc/CMakeLists.txt b/seahorn/trusty/user/base/lib/tipc/CMakeLists.txt new file mode 100644 index 0000000..f4e987a --- /dev/null +++ b/seahorn/trusty/user/base/lib/tipc/CMakeLists.txt @@ -0,0 +1,14 @@ +include_directories(include) + +set(EXTERNAL ${TRUSTY_ROOT}/trusty/user/base/lib/tipc) +add_library( + sea_trusty_tipc + ${EXTERNAL}/tipc.c + trusty_ipc_impl.c +) + +target_include_directories(sea_trusty_tipc PUBLIC ${CMAKE_CURRENT_SOURCE_DIR}) + +sea_attach_bc(sea_trusty_tipc) + +add_subdirectory(proof) \ No newline at end of file diff --git a/seahorn/trusty/user/base/lib/tipc/include/sea_tipc_helper.h b/seahorn/trusty/user/base/lib/tipc/include/sea_tipc_helper.h new file mode 100644 index 0000000..6cc4a52 --- /dev/null +++ b/seahorn/trusty/user/base/lib/tipc/include/sea_tipc_helper.h @@ -0,0 +1,8 @@ +#pragma once + +#include + + + +ssize_t send_msg(handle_t handle, struct ipc_msg *msg); +int msg_send_called; \ No newline at end of file diff --git a/seahorn/trusty/user/base/lib/tipc/proof/CMakeLists.txt b/seahorn/trusty/user/base/lib/tipc/proof/CMakeLists.txt new file mode 100644 index 0000000..545dccf --- /dev/null +++ b/seahorn/trusty/user/base/lib/tipc/proof/CMakeLists.txt @@ -0,0 +1,2 @@ +add_subdirectory(tipc_connect) +add_subdirectory(tipc_send1) \ No newline at end of file diff --git a/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/CMakeLists.txt b/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/CMakeLists.txt new file mode 100644 index 0000000..86c63e0 --- /dev/null +++ b/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/CMakeLists.txt @@ -0,0 +1,5 @@ +add_executable(tipc_connect_pf main.c) +sea_link_libraries(tipc_connect_pf sea_trusty_tipc.ir) + +sea_attach_bc(tipc_connect_pf) +sea_add_unsat_test(tipc_connect_pf) \ No newline at end of file diff --git a/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/Testing/Temporary/CTestCostData.txt b/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/Testing/Temporary/CTestCostData.txt new file mode 100644 index 0000000..ed97d53 --- /dev/null +++ b/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/Testing/Temporary/CTestCostData.txt @@ -0,0 +1 @@ +--- diff --git a/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/Testing/Temporary/LastTest.log b/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/Testing/Temporary/LastTest.log new file mode 100644 index 0000000..9a0339c --- /dev/null +++ b/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/Testing/Temporary/LastTest.log @@ -0,0 +1,3 @@ +Start testing: May 31 09:46 EDT +---------------------------------------------------------- +End testing: May 31 09:46 EDT diff --git a/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/main.c b/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/main.c new file mode 100644 index 0000000..c113264 --- /dev/null +++ b/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/main.c @@ -0,0 +1,13 @@ +#include +#include +#include + +int main(void) { + int rc; + handle_t h = INVALID_IPC_HANDLE; + char path[64]; + + /* Make tipc_connect fail and check if handle is unchanged */ + rc = tipc_connect(&h, NULL); + sassert(rc <= 0); +} \ No newline at end of file diff --git a/seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/CMakeLists.txt b/seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/CMakeLists.txt new file mode 100644 index 0000000..1db4fdb --- /dev/null +++ b/seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/CMakeLists.txt @@ -0,0 +1,5 @@ +add_executable(tipc_send1_pf main.c) +sea_link_libraries(tipc_send1_pf sea_trusty_tipc.ir) + +sea_attach_bc(tipc_send1_pf) +sea_add_unsat_test(tipc_send1_pf) \ No newline at end of file diff --git a/seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/main.c b/seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/main.c new file mode 100644 index 0000000..0f250b7 --- /dev/null +++ b/seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/main.c @@ -0,0 +1,35 @@ +#include +#include +#include +#include + +extern handle_t nd_handle(void); +extern int nd_size_t(void); +//extern void* can_fail_malloc(int); +extern int msg_send_called; + +/** Test harness for tpic_send1 */ +int main(void) { + + // msg_is_send_called = 0; + + /* assumptions */ + msg_send_called = 0; + handle_t handle = nd_handle(); + + size_t buf_len = nd_size_t(); + //void *buf = can_fail_malloc(buf_len); + void *buf = malloc(buf_len); + + //sea_tracking_on(); + + /* send single buf message */ + int rc = tipc_send1(handle, buf, buf_len); + + // sassert(msg_send_called == 1); + + //sassert(!sea_is_modified(buf)); + sassert(msg_send_called == 1); + + return 0; +} \ No newline at end of file diff --git a/seahorn/trusty/user/base/lib/tipc/trusty_ipc_impl.c b/seahorn/trusty/user/base/lib/tipc/trusty_ipc_impl.c new file mode 100644 index 0000000..aca9f96 --- /dev/null +++ b/seahorn/trusty/user/base/lib/tipc/trusty_ipc_impl.c @@ -0,0 +1,72 @@ +/** + * Stubbed version of trusty IPC + **/ + +//#include +#include +#include +#include + +extern int nd_size_t(void); +extern int msg_send_called; + +handle_t port_create(const char* path, + uint32_t num_recv_bufs, + uint32_t recv_buf_size, + uint32_t flags) { + return nd_port_handle(); +} + +handle_t connect(const char* path, uint32_t flags) { + handle_t rc = nd_chan_handle(); + assume(rc <= 0); + return rc; +} + +handle_t accept(handle_t handle, struct uuid* peer_uuid) { + return nd_chan_handle(); +} + +int close(handle_t handle) { + return nd_int(); +} + +int set_cookie(handle_t handle, void* cookie) { + return nd_int(); +} + +handle_t handle_set_create(void) { + return nd_chan_handle(); +} + +int handle_set_ctrl(handle_t handle, uint32_t cmd, struct uevent* evt) { + return nd_int(); +} + +int wait(handle_t handle, struct uevent* event, uint32_t timeout_msecs) { + return nd_int(); +} + +int wait_any(struct uevent* event, uint32_t timeout_msecs) { + return nd_int(); +} + +int get_msg(handle_t handle, struct ipc_msg_info* msg_info) { + return nd_int(); +} + +ssize_t read_msg(handle_t handle, + uint32_t msg_id, + uint32_t offset, + struct ipc_msg* msg) { + return nd_int(); +} + +int put_msg(handle_t handle, uint32_t msg_id) { + return nd_int(); +} + +ssize_t send_msg(handle_t handle, struct ipc_msg* msg) { + msg_send_called = 1; + return nd_size_t(); +} \ No newline at end of file From 5bf4bf8169c952cc306281a888496b7c254a5413 Mon Sep 17 00:00:00 2001 From: yuyan Date: Mon, 31 May 2021 17:08:25 -0400 Subject: [PATCH 2/2] feat:add a struct state and functions that modify the state --- .../base/lib/tipc/include/sea_tipc_helper.h | 14 ++++++- .../Testing/Temporary/CTestCostData.txt | 1 - .../Testing/Temporary/LastTest.log | 3 -- .../base/lib/tipc/proof/tipc_send1/main.c | 39 ++++++++++--------- .../user/base/lib/tipc/trusty_ipc_impl.c | 25 +++++++++++- 5 files changed, 56 insertions(+), 26 deletions(-) delete mode 100644 seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/Testing/Temporary/CTestCostData.txt delete mode 100644 seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/Testing/Temporary/LastTest.log diff --git a/seahorn/trusty/user/base/lib/tipc/include/sea_tipc_helper.h b/seahorn/trusty/user/base/lib/tipc/include/sea_tipc_helper.h index 6cc4a52..0e0bcef 100644 --- a/seahorn/trusty/user/base/lib/tipc/include/sea_tipc_helper.h +++ b/seahorn/trusty/user/base/lib/tipc/include/sea_tipc_helper.h @@ -5,4 +5,16 @@ ssize_t send_msg(handle_t handle, struct ipc_msg *msg); -int msg_send_called; \ No newline at end of file + +typedef struct State{ + int msg_send_called; + int msg_recv_called; +} state; + +state g_state; + +void state_init(void); +void msg_sent(void); +void msg_received(void); +void state_reset(void); +int get_msg_sent_times(void); \ No newline at end of file diff --git a/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/Testing/Temporary/CTestCostData.txt b/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/Testing/Temporary/CTestCostData.txt deleted file mode 100644 index ed97d53..0000000 --- a/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/Testing/Temporary/CTestCostData.txt +++ /dev/null @@ -1 +0,0 @@ ---- diff --git a/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/Testing/Temporary/LastTest.log b/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/Testing/Temporary/LastTest.log deleted file mode 100644 index 9a0339c..0000000 --- a/seahorn/trusty/user/base/lib/tipc/proof/tipc_connect/Testing/Temporary/LastTest.log +++ /dev/null @@ -1,3 +0,0 @@ -Start testing: May 31 09:46 EDT ----------------------------------------------------------- -End testing: May 31 09:46 EDT diff --git a/seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/main.c b/seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/main.c index 0f250b7..d7cd3e2 100644 --- a/seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/main.c +++ b/seahorn/trusty/user/base/lib/tipc/proof/tipc_send1/main.c @@ -1,35 +1,36 @@ #include #include #include -#include +#include extern handle_t nd_handle(void); extern int nd_size_t(void); -//extern void* can_fail_malloc(int); -extern int msg_send_called; +extern void *sea_malloc_havoc(size_t sz); /** Test harness for tpic_send1 */ int main(void) { - // msg_is_send_called = 0; + + /* assumptions */ + state_init(); + handle_t handle = nd_handle(); - /* assumptions */ - msg_send_called = 0; - handle_t handle = nd_handle(); + size_t buf_len = nd_size_t(); + assume(buf_len > 0); - size_t buf_len = nd_size_t(); - //void *buf = can_fail_malloc(buf_len); - void *buf = malloc(buf_len); + void *buf = sea_malloc_havoc(buf_len); + +// sea_tracking_on(); +// sea_reset_modified((char *)buf); - //sea_tracking_on(); + /* send single buf message */ + int rc = tipc_send1(handle, buf, buf_len); - /* send single buf message */ - int rc = tipc_send1(handle, buf, buf_len); + // sassert(!sea_is_modified((char *)buf)); - // sassert(msg_send_called == 1); - - //sassert(!sea_is_modified(buf)); - sassert(msg_send_called == 1); - - return 0; + /* testing the message is only sent once */ + int msg_sent = get_msg_sent_times(); + sassert(msg_sent == 1); + state_reset(); + return 0; } \ No newline at end of file diff --git a/seahorn/trusty/user/base/lib/tipc/trusty_ipc_impl.c b/seahorn/trusty/user/base/lib/tipc/trusty_ipc_impl.c index aca9f96..7078c1b 100644 --- a/seahorn/trusty/user/base/lib/tipc/trusty_ipc_impl.c +++ b/seahorn/trusty/user/base/lib/tipc/trusty_ipc_impl.c @@ -10,6 +10,26 @@ extern int nd_size_t(void); extern int msg_send_called; +void state_init(void) +{ + g_state.msg_recv_called = 0; + g_state.msg_send_called = 0; +} +void msg_sent(void){ + g_state.msg_send_called += 1; +} +void msg_received(void){ + g_state.msg_recv_called += 1; +} +void state_reset(void){ + g_state.msg_recv_called = 0; + g_state.msg_send_called = 0; +} + +int get_msg_sent_times(void){ + return g_state.msg_send_called; +} + handle_t port_create(const char* path, uint32_t num_recv_bufs, uint32_t recv_buf_size, @@ -67,6 +87,7 @@ int put_msg(handle_t handle, uint32_t msg_id) { } ssize_t send_msg(handle_t handle, struct ipc_msg* msg) { - msg_send_called = 1; + msg_sent(); return nd_size_t(); -} \ No newline at end of file +} +