-
Notifications
You must be signed in to change notification settings - Fork 4
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat:initial attempts to test tipc;please provide gental feedback #11
base: master
Are you sure you want to change the base?
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1 +1,2 @@ | ||
add_subdirectory(user/base/lib/libc-trusty) | ||
add_subdirectory(user/base/lib/tipc) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
#pragma once | ||
|
||
#include <trusty_ipc.h> | ||
|
||
|
||
|
||
ssize_t send_msg(handle_t handle, struct ipc_msg *msg); | ||
|
||
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); |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
add_subdirectory(tipc_connect) | ||
add_subdirectory(tipc_send1) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
#include <seahorn/seahorn.h> | ||
#include <lib/tipc/tipc.h> | ||
#include <trusty_ipc.h> | ||
|
||
int main(void) { | ||
int rc; | ||
handle_t h = INVALID_IPC_HANDLE; | ||
char path[64]; | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. unused? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is the example Xiang set for me. The goal is to teach me how to write tests :) |
||
|
||
/* Make tipc_connect fail and check if handle is unchanged */ | ||
rc = tipc_connect(&h, NULL); | ||
sassert(rc <= 0); | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,36 @@ | ||
#include <seahorn/seahorn.h> | ||
#include <lib/tipc/tipc.h> | ||
#include <trusty_ipc.h> | ||
#include <sea_tipc_helper.h> | ||
|
||
extern handle_t nd_handle(void); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. include |
||
extern int nd_size_t(void); | ||
extern void *sea_malloc_havoc(size_t sz); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I don't think this function signature is recognized by seahorn op sem; you would still need to implement the actual function There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I guess I have not ported these. They have to be part of our libc port |
||
|
||
/** Test harness for tpic_send1 */ | ||
int main(void) { | ||
|
||
|
||
/* assumptions */ | ||
state_init(); | ||
handle_t handle = nd_handle(); | ||
|
||
size_t buf_len = nd_size_t(); | ||
assume(buf_len > 0); | ||
|
||
void *buf = sea_malloc_havoc(buf_len); | ||
|
||
// sea_tracking_on(); | ||
// sea_reset_modified((char *)buf); | ||
|
||
/* send single buf message */ | ||
int rc = tipc_send1(handle, buf, buf_len); | ||
|
||
// sassert(!sea_is_modified((char *)buf)); | ||
|
||
/* testing the message is only sent once */ | ||
int msg_sent = get_msg_sent_times(); | ||
sassert(msg_sent == 1); | ||
state_reset(); | ||
return 0; | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,93 @@ | ||
/** | ||
* Stubbed version of trusty IPC | ||
**/ | ||
|
||
//#include <trusty_ipc.h> | ||
#include <nondet.h> | ||
#include <seahorn/seahorn.h> | ||
#include <sea_tipc_helper.h> | ||
|
||
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, | ||
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_sent(); | ||
return nd_size_t(); | ||
} | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
it is better to move include directories where they are actually used.
But I guess we can refactor it all at once since other directories are already globally included.