-
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 1 commit
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,8 @@ | ||
#pragma once | ||
|
||
#include <trusty_ipc.h> | ||
|
||
|
||
|
||
ssize_t send_msg(handle_t handle, struct ipc_msg *msg); | ||
int msg_send_called; | ||
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. comment on what this global variable is for. By convention, we name globals using 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. Not sure this variable should be declared in the header file. |
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 @@ | ||
--- | ||
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 file should not have been included. |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
Start testing: May 31 09:46 EDT | ||
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. file should not be included |
||
---------------------------------------------------------- | ||
End testing: May 31 09:46 EDT |
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,35 @@ | ||
#include <seahorn/seahorn.h> | ||
#include <lib/tipc/tipc.h> | ||
#include <trusty_ipc.h> | ||
#include <stdlib.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* 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; | ||
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 now understand why the variable is declared in the header file. |
||
handle_t handle = nd_handle(); | ||
|
||
size_t buf_len = nd_size_t(); | ||
//void *buf = can_fail_malloc(buf_len); | ||
void *buf = malloc(buf_len); | ||
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. need to use our allocation library. This has potentially undefined behaviour. The buffer is allocated but is never written to. It is then given to a function that might read from it. 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. ok 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. one way to fix this locally is to call memhavoc after malloc. @danblitzhou can help with that. |
||
|
||
//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; | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,72 @@ | ||
/** | ||
* 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; | ||
|
||
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(); | ||
} |
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.