diff --git a/seahorn/CMakeLists.txt b/seahorn/CMakeLists.txt index 2e31b25..b564f50 100644 --- a/seahorn/CMakeLists.txt +++ b/seahorn/CMakeLists.txt @@ -263,6 +263,7 @@ add_definitions( configure_file(sea.yaml sea.yaml @ONLY) configure_file(sea_cex_base.yaml sea.cex.yaml @ONLY) configure_file(sea_vac.yaml sea.vac.yaml @ONLY) +add_subdirectory(sea_libc) add_subdirectory(trusty_common) diff --git a/seahorn/sea.yaml b/seahorn/sea.yaml index 38316b0..7374c3d 100644 --- a/seahorn/sea.yaml +++ b/seahorn/sea.yaml @@ -18,7 +18,7 @@ verify_options: # context-sensitive type-aware alias analysis dsa: sea-cs-t # weak support for function pointers. sea-dsa is better but less stable - devirt-functions: 'sea-dsa' + devirt-functions: 'types' # bit-precise memory-precise operational semantics bmc: opsem horn-vcgen-use-ite: '' @@ -29,9 +29,9 @@ verify_options: # static allocator supports symbolic allocation size sea-opsem-allocator: static # stack allocation from a symbolic starting point - horn-explicit-sp0: false + horn-explicit-sp0: true # lambdas for memory - horn-bv2-lambdas: '' + horn-bv2-lambdas: true # use z3 simplifier during vcgen horn-bv2-simplify: true # wide memory manager to track pointer sizes @@ -40,6 +40,10 @@ verify_options: '-S': '' # keep intermediate results for debugging keep-temps: '' - temp-dir: /tmp/verifyTrusty + temp-dir: /tmp/verifyTrusty_sid # time and result stats horn-stats: true +# Use smtfd tactic + horn-bmc-tactic: 'smtfd' +# set tracking memory (shadow mem) on + horn-bv2-tracking-mem: true diff --git a/seahorn/sea_base.yaml b/seahorn/sea_base.yaml index 865245b..86c9352 100644 --- a/seahorn/sea_base.yaml +++ b/seahorn/sea_base.yaml @@ -40,6 +40,6 @@ verify_options: '-S': '' # keep intermediate results for debugging keep-temps: '' - temp-dir: /tmp/verifyTrusty + temp-dir: /tmp/verifyTrusty_sid # time and result stats horn-stats: true diff --git a/seahorn/sea_cex_base.yaml b/seahorn/sea_cex_base.yaml index de15a5f..d104103 100644 --- a/seahorn/sea_cex_base.yaml +++ b/seahorn/sea_cex_base.yaml @@ -29,7 +29,7 @@ verify_options: # static allocator supports symbolic allocation size sea-opsem-allocator: static # stack allocation from a symbolic starting point - horn-explicit-sp0: false + horn-explicit-sp0: true # lambdas for memory horn-bv2-lambdas: false # use z3 simplifier during vcgen @@ -40,11 +40,11 @@ verify_options: '-S': '' # keep intermediate results for debugging keep-temps: '' - temp-dir: /tmp/verifyTrusty + temp-dir: /tmp/verifyTrusty_sid # time and result stats horn-stats: true # produce counterexample harness - cex: /tmp/h.ll + cex: /tmp/verifytrusty_sid/h.ll # printable counterexample log log: cex # number of words to unroll symbolic memcpy for array-based memory representation @@ -52,6 +52,10 @@ verify_options: horn-array-sym-memcpy-unroll-count: 10 # print memory state as a table # XXX still flaky, sometimes only the last byte can be trusted - horn-bmc-hexdump: true + horn-bmc-hexdump: false horn-bmc-logic: QF_ABV - +# Use horn-bv2-lambdas + horn-bv2-lambdas: true +# horn-bmc-solver: 'smt-y2' +# set tracking memory (shadow mem) on + horn-bv2-tracking-mem: true diff --git a/seahorn/sea_libc/CMakeLists.txt b/seahorn/sea_libc/CMakeLists.txt new file mode 100644 index 0000000..9f5c083 --- /dev/null +++ b/seahorn/sea_libc/CMakeLists.txt @@ -0,0 +1,6 @@ +option(SEA_ALLOCATOR_CAN_FAIL "Use can fail allocator" OFF) +add_library(sea_libc + src/realloc.c + src/sea_allocators.c) +target_include_directories(sea_libc PUBLIC include) +sea_attach_bc(sea_libc) diff --git a/seahorn/sea_libc/README b/seahorn/sea_libc/README new file mode 100644 index 0000000..ff33397 --- /dev/null +++ b/seahorn/sea_libc/README @@ -0,0 +1,6 @@ +sea_libc is an implementation of the standard C library for software +verification in the SEAHORN verification environment. + +Directory structure is as follows: +* include/ -- The include directory that contains header files. +* src/ -- libc functions that delegate to SEAHORN specific logic. diff --git a/seahorn/sea_libc/include/assert.h b/seahorn/sea_libc/include/assert.h new file mode 100644 index 0000000..382730d --- /dev/null +++ b/seahorn/sea_libc/include/assert.h @@ -0,0 +1,4 @@ +#pragma once +#undef assert + +#define assert(x) sassert(x) diff --git a/seahorn/sea_libc/include/sea_allocators.h b/seahorn/sea_libc/include/sea_allocators.h new file mode 100644 index 0000000..0b5a7b1 --- /dev/null +++ b/seahorn/sea_libc/include/sea_allocators.h @@ -0,0 +1,60 @@ +/** Different memory allocators*/ +#pragma once +#include +#include +#include + +#define INLINE __attribute__((always_inline)) + +/** + Basic memory allocator to be used instead of malloc() + + Same semantics as malloc(). Can non-deterministically return NULL to indicate + allocation failure. + */ +INLINE void *sea_malloc(size_t sz); + +/** + Aligned memory allocator + + Same as sea_malloc() but rounds the allocation size up to the nearest word +*/ +INLINE void *sea_malloc_aligned(size_t sz); + +/** + Initializing memory allcator + + Same as malloc() but initializes memory non-deterministically + */ +INLINE void *sea_malloc_havoc(size_t sz); + +/** + Non-failing memory allocator + + Same as malloc() but guarantees that allocation does not fail + */ +INLINE void *sea_malloc_safe(size_t sz); + +/** + Non-failing initializing allocator + + Combination of sea_malloc_havoc() with sea_malloc_safe() + */ +INLINE void *sea_malloc_havoc_safe(size_t sz); + +/** + Non-failing aligned allocator + + Combination of sea_malloc_safe() with sea_malloc_aligned() + */ +INLINE void *sea_malloc_aligned_safe(size_t sz); + +/** + Initializing aligned allocator + + Combination of sea_malloc_havoc() with sea_malloc_aligned() + */ +INLINE void *sea_malloc_aligned_havoc(size_t sz); + +INLINE void sea_free(void *ptr); +INLINE void *sea_realloc(void *ptr, size_t sz); diff --git a/seahorn/sea_libc/src/realloc.c b/seahorn/sea_libc/src/realloc.c new file mode 100644 index 0000000..c5ad0db --- /dev/null +++ b/seahorn/sea_libc/src/realloc.c @@ -0,0 +1,3 @@ +#include + +void *realloc(void *ptr, size_t new_size) { return sea_realloc(ptr, new_size); } diff --git a/seahorn/sea_libc/src/sea_allocators.c b/seahorn/sea_libc/src/sea_allocators.c new file mode 100644 index 0000000..f564b2e --- /dev/null +++ b/seahorn/sea_libc/src/sea_allocators.c @@ -0,0 +1,80 @@ +/** Memory allocating functions */ +#include + +#include +#include + +extern void memhavoc(void *, size_t); + +extern NONDET_FN_ATTR bool nd_malloc_is_fail(void); +INLINE void *sea_malloc(size_t sz) { +#ifdef SEA_ALLOCATOR_CAN_FAIL + return nd_malloc_is_fail() ? NULL : malloc(sz); +#else + return malloc(sz); +#endif +} + +// from: aws-c-common/source/allocator.c +#define AWS_ALIGN_ROUND_UP(value, alignment) \ + (((value) + ((alignment)-1)) & ~((alignment)-1)) +#ifdef __KLEE__ +INLINE void *klee_malloc_aligned(size_t *sz) { + enum { S_ALIGNMENT = sizeof(intmax_t) }; + *sz = AWS_ALIGN_ROUND_UP(*sz, S_ALIGNMENT); + return sea_malloc(*sz); +} +#endif +INLINE void *sea_malloc_aligned(size_t sz) { + enum { S_ALIGNMENT = sizeof(intmax_t) }; + size_t alloc_sz = AWS_ALIGN_ROUND_UP(sz, S_ALIGNMENT); + return sea_malloc(alloc_sz); +} +#undef AWS_ALIGN_ROUND_UP + +INLINE void *sea_malloc_havoc(size_t sz) { + void *data = sea_malloc(sz); + memhavoc(data, sz); + return data; +} + +INLINE void *sea_malloc_safe(size_t sz) { + void *data = malloc(sz); + assume(data); + return data; +} + +INLINE void *sea_malloc_havoc_safe(size_t sz) { + void *data = sea_malloc_havoc(sz); + assume(data); + return data; +} + +INLINE void *sea_malloc_aligned_safe(size_t sz) { + void *data = sea_malloc_aligned(sz); + assume(data); + return data; +} + +#ifdef __KLEE__ +INLINE void *sea_malloc_aligned_havoc(size_t sz) { + void *data = klee_malloc_aligned(&sz); + if (data) + memhavoc(data, sz); + return data; +} +#else +INLINE void *sea_malloc_aligned_havoc(size_t sz) { + void *data = sea_malloc_aligned(sz); + memhavoc(data, sz); + return data; +} +#endif + +INLINE void sea_free(void *ptr) { free(ptr); } + +INLINE void *sea_realloc(void *ptr, size_t sz) { + if (ptr) + sea_free(ptr); + return sea_malloc(sz); +} diff --git a/seahorn/storage/CMakeLists.txt b/seahorn/storage/CMakeLists.txt index da4e4ed..81774b4 100644 --- a/seahorn/storage/CMakeLists.txt +++ b/seahorn/storage/CMakeLists.txt @@ -2,10 +2,10 @@ include_directories(include) add_compile_definitions(CAN_RETURN_INVALID_IPC_HANDLE=1) if (HANDLE_TYPE_IS_PTR) - set(IPC_SRC ${TRUSTY_MOD_ROOT}/trusty/user/app/storage/ipc.c) + set(STORAGE_IPC_SRC ${TRUSTY_MOD_ROOT}/trusty/user/app/storage/ipc.c) add_compile_definitions(HANDLE_TYPE_IS_PTR=1) else () - set(IPC_SRC ${TRUSTY_ROOT}/trusty/user/app/storage/ipc.c) + set(STORAGE_IPC_SRC ${TRUSTY_ROOT}/trusty/user/app/storage/ipc.c) endif () add_subdirectory(lib) @@ -14,4 +14,5 @@ add_subdirectory(stubs) # The following jobs will be built add_subdirectory(jobs/ipc/indirect_handlers) add_subdirectory(jobs/ipc/msg_buffer) -add_subdirectory(jobs/ipc/port_create_destroy) \ No newline at end of file +add_subdirectory(jobs/ipc/port_create_destroy) +add_subdirectory(jobs/ipc/ipc_session) diff --git a/seahorn/storage/include/sea_ipc_helper.h b/seahorn/storage/include/sea_ipc_helper.h index 491a675..805fec2 100644 --- a/seahorn/storage/include/sea_ipc_helper.h +++ b/seahorn/storage/include/sea_ipc_helper.h @@ -1,19 +1,18 @@ #pragma once #include -#include +// #include /* * Same functionality as dispatch_event but non-static */ -void sea_dispatch_event(const uevent_t* ev); +void sea_dispatch_event(const uevent_t *ev); /* * Initialize a port context by given a channel context handler */ -struct ipc_port_context* create_port_context(void); - +struct ipc_port_context *create_port_context(void); struct ipc_channel_context * sea_sync_channel_connect(struct ipc_port_context *parent_ctx, - const uuid_t *peer_uuid, handle_t chan_handle); \ No newline at end of file + const uuid_t *peer_uuid, handle_t chan_handle); diff --git a/seahorn/storage/jobs/ipc/indirect_handlers/CMakeLists.txt b/seahorn/storage/jobs/ipc/indirect_handlers/CMakeLists.txt index 72a710d..80bfb36 100644 --- a/seahorn/storage/jobs/ipc/indirect_handlers/CMakeLists.txt +++ b/seahorn/storage/jobs/ipc/indirect_handlers/CMakeLists.txt @@ -1,14 +1,16 @@ add_executable(storage_ipc_indirect_handlers - ${IPC_SRC} - indirect_handlers_harness.c) + ${STORAGE_IPC_SRC} + indirect_handlers_harness.c + ) target_include_directories(storage_ipc_indirect_handlers PRIVATE ${TRUSTY_ROOT}/trusty/user/app/storage ) sea_link_libraries(storage_ipc_indirect_handlers sea_storage_ipc_proofs.ir) -sea_overlink_libraries(storage_ipc_indirect_handlers realloc_override.ir) -sea_overlink_libraries(storage_ipc_indirect_handlers fprintf_override.ir) +sea_link_libraries(storage_ipc_indirect_handlers sea_libc.ir) +#sea_overlink_libraries(storage_ipc_indirect_handlers realloc_override.ir) +#sea_overlink_libraries(storage_ipc_indirect_handlers fprintf_override.ir) sea_overlink_libraries(storage_ipc_indirect_handlers ipc_loop_override.ir) sea_attach_bc_link(storage_ipc_indirect_handlers) configure_file(sea.yaml sea.yaml @ONLY) -sea_add_unsat_test(storage_ipc_indirect_handlers) \ No newline at end of file +sea_add_unsat_test(storage_ipc_indirect_handlers) diff --git a/seahorn/storage/jobs/ipc/indirect_handlers/indirect_handlers_harness.c b/seahorn/storage/jobs/ipc/indirect_handlers/indirect_handlers_harness.c index 4cf5956..5f65b92 100644 --- a/seahorn/storage/jobs/ipc/indirect_handlers/indirect_handlers_harness.c +++ b/seahorn/storage/jobs/ipc/indirect_handlers/indirect_handlers_harness.c @@ -20,11 +20,11 @@ #include #include -#include "ipc.h" +#include -#include #include "seahorn/seahorn.h" -#include "sea_ipc_helper.h" +#include +#include #include "tipc_limits.h" #include diff --git a/seahorn/storage/jobs/ipc/ipc_session/CMakeLists.txt b/seahorn/storage/jobs/ipc/ipc_session/CMakeLists.txt new file mode 100644 index 0000000..386c7ee --- /dev/null +++ b/seahorn/storage/jobs/ipc/ipc_session/CMakeLists.txt @@ -0,0 +1,15 @@ +# We verify a modified copy of ipc.c since the original +# casts between a handle_t and int. +# This breaks the original spec that handle_t is a 32-bit opaque number +# and hence breaks our impl of type(handle_t) == 32 bit pointer. +add_executable(storage_ipc_session + ${STORAGE_IPC_SRC} + ipc_session_harness.c) +target_include_directories(storage_ipc_session PRIVATE + ${TRUSTY_ROOT}/trusty/user/app/storage) +sea_link_libraries(storage_ipc_session sea_storage_ipc_proofs.ir) +sea_link_libraries(storage_ipc_session sea_libc.ir) +sea_overlink_libraries(storage_ipc_session fprintf_override.ir) +#sea_overlink_libraries(storage_ipc_session ipc_loop_override.ir) +sea_attach_bc_link(storage_ipc_session) +sea_add_unsat_test(storage_ipc_session) diff --git a/seahorn/storage/jobs/ipc/ipc_session/ipc_session_harness.c b/seahorn/storage/jobs/ipc/ipc_session/ipc_session_harness.c new file mode 100644 index 0000000..b0bd6df --- /dev/null +++ b/seahorn/storage/jobs/ipc/ipc_session/ipc_session_harness.c @@ -0,0 +1,175 @@ +#include +#include +#include +#include +#include +#include + +#include + +// #include "handle_table.h" +#include "sea_handle_table.h" + +#include "seahorn/seahorn.h" +#include + +#include "tipc_limits.h" +#include + +#define ND __declspec(noalias) + +extern void sea_reset_modified(char *); +extern bool sea_is_modified(char *); +extern void sea_tracking_on(void); +extern void sea_tracking_off(void); +extern ND void memhavoc(void *ptr, size_t size); + +extern void sea_printf(const char *format, ...); + +static void dispatch_event(const uevent_t *ev) { + sassert(ev); + if (ev->event == IPC_HANDLE_POLL_NONE) { + return; + } + + struct ipc_context *context = ev->cookie; + // When handle is IPC_INVALID_HANDLE then context + // is NULL + if (context) { + sassert(context->evt_handler); + sassert(context->handle == ev->handle); + + context->evt_handler(context, ev); + } +} + +static void accept_and_dispatch_request(void) { + int rc; + uevent_t event; + + event.handle = INVALID_IPC_HANDLE; + event.event = 0; + event.cookie = NULL; + rc = wait_any(&event, INFINITE_TIME); + assume(rc == NO_ERROR); + + if (rc == NO_ERROR) { /* got an event */ + dispatch_event(&event); + } +} + +static void sea_ipc_disconnect_handler(struct ipc_channel_context *context) { + if (context) + free(context); +} + +/* +** Send a ND message. Called when a message is received. +** +*/ +static int sync_ipc_msg_handler(struct ipc_channel_context *context, void *msg, + size_t msg_size) { + sassert(!sea_is_modified((char *)msg)); + /* + * The following logic can be used to trigger a CEX (OOB write) + **/ + /* if (msg_size > 0) { */ + /* *((char *)msg + msg_size + 1) = 0xFF; */ + /* } */ + uint8_t *snd_buf = malloc(sizeof(msg_size)); + memhavoc(snd_buf, msg_size); + /* reset modified bit to track unexpected writes */ + sea_reset_modified((char *)snd_buf); + uint8_t *recv_buf = malloc(sizeof(msg_size)); + memhavoc(recv_buf, msg_size); + + struct iovec tx_iov = { + .iov_base = snd_buf, + .iov_len = msg_size, + }; + struct iovec rx_iov = { + .iov_base = recv_buf, + .iov_len = msg_size, + }; + int rc = sync_ipc_send_msg(context->common.handle, &tx_iov, 1, &rx_iov, 1); + + if (rc < 0) + return rc; + + if (rc > 0) + sassert(rc == msg_size); + // Check that ipc send logic does not modify the message to be sent. + sassert(!sea_is_modified((char *)snd_buf)); + return NO_ERROR; +} + +static struct ipc_channel_context * +sea_channel_onconnect(struct ipc_port_context *parent_ctx, + const uuid_t *peer_uuid, handle_t chan_handle) { + struct ipc_channel_context *pctx = malloc(sizeof(struct ipc_channel_context)); + pctx->ops.on_disconnect = sea_ipc_disconnect_handler; + pctx->ops.on_handle_msg = sync_ipc_msg_handler; + // NOTE: Second wait_any call: return channel handle on next wait_any. + on_waitany_return(chan_handle); + return pctx; +} + +/* + * Test harness entry point + * + * This tests the following + * 1. This harness establishes a port + * 2. It then waits for and receives a connection request (port handle) + * 3. It then creates a channel handle and waits for incoming messages on the + * channel + * 4. It receives a message and sends a reply and receives ack. + * + * The properties being tested are: + * 1. spatial memory safety + * 2. no tampering of messages by ipc layer (messages are never modified after + * creation) + * + * This model uses a rudimentary mock design instead of a fake handle generator. + * Before every wait_any call, we set the handle to be returned. This is a + * simpler design than the fake used and is also groundwork for mock-like + * expectations. For example, checking that a function has been called + * exactly/atmost/atleast n times. */ +int main(void) { + sea_tracking_on(); +// This job is for handle_type_is_ptr model +#ifndef HANDLE_TYPE_IS_PTR + assert(false); +#endif + + /* setup port context */ + struct ipc_port_context ctx = { + .ops = {.on_connect = sea_channel_onconnect}, + }; + + /* call ipc_port_create */ + int rc = + ipc_port_create(&ctx, STORAGE_DISK_PROXY_PORT, 1, STORAGE_MAX_BUFFER_SIZE, + IPC_PORT_ALLOW_TA_CONNECT | IPC_PORT_ALLOW_NS_CONNECT); + + /* bail out if error but flag it as an error */ + + sassert(rc >= 0); + + // NOTE: First wait_any call: return port handle on next wait_any. + on_waitany_return(ctx.common.handle); + + accept_and_dispatch_request(); + + // now expect to handle a channel + accept_and_dispatch_request(); + + /* check that handle is registered if connection succeeds */ + sassert(sea_ht_is_active_port(ctx.common.handle)); + + /* destroy port */ + ipc_port_destroy(&ctx); + /* check that handle is unregistered properly */ + + sassert(!sea_ht_is_active_port(ctx.common.handle)); + return 0; +} diff --git a/seahorn/storage/jobs/ipc/msg_buffer/CMakeLists.txt b/seahorn/storage/jobs/ipc/msg_buffer/CMakeLists.txt index 4cdc4af..76b5dc4 100644 --- a/seahorn/storage/jobs/ipc/msg_buffer/CMakeLists.txt +++ b/seahorn/storage/jobs/ipc/msg_buffer/CMakeLists.txt @@ -1,5 +1,5 @@ add_executable(storage_ipc_msg_buffer - ${IPC_SRC} + ${STORAGE_IPC_SRC} msg_buffer_harness.c) target_include_directories(storage_ipc_msg_buffer @@ -11,4 +11,4 @@ sea_overlink_libraries(storage_ipc_msg_buffer fprintf_override.ir) sea_overlink_libraries(storage_ipc_msg_buffer ipc_loop_override.ir) sea_attach_bc_link(storage_ipc_msg_buffer) configure_file(sea.yaml sea.yaml @ONLY) -sea_add_unsat_test(storage_ipc_msg_buffer) \ No newline at end of file +sea_add_unsat_test(storage_ipc_msg_buffer) diff --git a/seahorn/storage/jobs/ipc/port_create_destroy/CMakeLists.txt b/seahorn/storage/jobs/ipc/port_create_destroy/CMakeLists.txt index a1be337..78a6a5d 100644 --- a/seahorn/storage/jobs/ipc/port_create_destroy/CMakeLists.txt +++ b/seahorn/storage/jobs/ipc/port_create_destroy/CMakeLists.txt @@ -3,7 +3,7 @@ # This breaks the original spec that handle_t is a 32-bit opaque number # and hence breaks our impl of type(handle_t) == 32 bit pointer. add_executable(storage_ipc_port_create_destroy - ${IPC_SRC} + ${STORAGE_IPC_SRC} port_create_destroy_harness.c) target_include_directories(storage_ipc_port_create_destroy PRIVATE ${TRUSTY_ROOT}/trusty/user/app/storage @@ -13,4 +13,4 @@ sea_overlink_libraries(storage_ipc_port_create_destroy realloc_override.ir) sea_overlink_libraries(storage_ipc_port_create_destroy fprintf_override.ir) sea_overlink_libraries(storage_ipc_port_create_destroy ipc_loop_override.ir) sea_attach_bc_link(storage_ipc_port_create_destroy) -sea_add_unsat_test(storage_ipc_port_create_destroy) \ No newline at end of file +sea_add_unsat_test(storage_ipc_port_create_destroy) diff --git a/seahorn/storage/lib/CMakeLists.txt b/seahorn/storage/lib/CMakeLists.txt index 44be6d0..9f79815 100644 --- a/seahorn/storage/lib/CMakeLists.txt +++ b/seahorn/storage/lib/CMakeLists.txt @@ -4,7 +4,7 @@ add_library(sea_storage_ipc_proofs ) target_include_directories(sea_storage_ipc_proofs PRIVATE - ${TRUSTY_ROOT}/trusty/user/app/storage) + ${TRUSTY_ROOT}/trusty/user/app/storage) if(SEA_ALLOCATOR_CAN_FAIL) diff --git a/seahorn/storage/lib/sea_ipc_helper.c b/seahorn/storage/lib/sea_ipc_helper.c index ff10a81..b078ba1 100644 --- a/seahorn/storage/lib/sea_ipc_helper.c +++ b/seahorn/storage/lib/sea_ipc_helper.c @@ -1,23 +1,22 @@ +#include #include -#include -#include #include +#include #include -#include -void sea_dispatch_event(const uevent_t* ev) { - sassert(ev); +void sea_dispatch_event(const uevent_t *ev) { + sassert(ev); - if (ev->event == IPC_HANDLE_POLL_NONE) { - return; - } + if (ev->event == IPC_HANDLE_POLL_NONE) { + return; + } - struct ipc_context* context = ev->cookie; - sassert(context); - sassert(context->evt_handler); - sassert(context->handle == ev->handle); + struct ipc_context *context = ev->cookie; + sassert(context); + sassert(context->evt_handler); + sassert(context->handle == ev->handle); - context->evt_handler(context, ev); + context->evt_handler(context, ev); } static void sea_ipc_disconnect_handler(struct ipc_channel_context *context) { @@ -44,7 +43,7 @@ static int sea_ipc_msg_handler(struct ipc_channel_context *context, void *msg, } static int sync_ipc_msg_handler(struct ipc_channel_context *context, void *msg, - size_t msg_size) { + size_t msg_size) { uint8_t *snd_buf = malloc(sizeof(msg_size)); uint8_t *recv_buf = malloc(sizeof(msg_size)); struct iovec tx_iov = { @@ -84,7 +83,7 @@ sea_channel_connect(struct ipc_port_context *parent_ctx, */ struct ipc_channel_context * sea_sync_channel_connect(struct ipc_port_context *parent_ctx, - const uuid_t *peer_uuid, handle_t chan_handle) { + const uuid_t *peer_uuid, handle_t chan_handle) { struct ipc_channel_context *pctx = malloc(sizeof(struct ipc_channel_context)); pctx->ops.on_disconnect = sea_ipc_disconnect_handler; pctx->ops.on_handle_msg = sync_ipc_msg_handler; @@ -94,10 +93,11 @@ sea_sync_channel_connect(struct ipc_port_context *parent_ctx, /* * constant variable of ipc_port_context */ + static struct ipc_port_context port_ctx = { - .ops = {.on_connect = sea_channel_connect}, - }; + .ops = {.on_connect = sea_channel_connect}, +}; -struct ipc_port_context* create_port_context(){ +struct ipc_port_context *create_port_context() { return &port_ctx; -} \ No newline at end of file +} diff --git a/seahorn/trusty/user/base/lib/CMakeLists.txt b/seahorn/trusty/user/base/lib/CMakeLists.txt index 0a7296f..b8bc002 100644 --- a/seahorn/trusty/user/base/lib/CMakeLists.txt +++ b/seahorn/trusty/user/base/lib/CMakeLists.txt @@ -1,9 +1,9 @@ -set(EXTERNAL ${TRUSTY_ROOT}/trusty/user/base/lib/libc-trusty) +set(TRUSTY_IPC_DIR ${TRUSTY_ROOT}/trusty/user/base/lib/libc-trusty) + add_library( sea_libc_trusty - ${EXTERNAL}/ipc.c + ${TRUSTY_IPC_DIR}/ipc.c ) - if (HANDLE_TYPE_IS_PTR) add_subdirectory(libc-trusty-ptr) else () diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/sea_handle_table.c b/seahorn/trusty/user/base/lib/libc-trusty-ptr/sea_handle_table.c index 8123a95..5ae14eb 100644 --- a/seahorn/trusty/user/base/lib/libc-trusty-ptr/sea_handle_table.c +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/sea_handle_table.c @@ -10,13 +10,16 @@ Implementation of table of handles to be used by IPC #include #include +extern void sea_printf(const char *format, ...); +static unsigned int num_choose_handle = 0; +static unsigned int num_on_waitany_return = 0; #define ND __declspec(noalias) // Records the handle to return on wait_any -handle_t g_on_waitany_handle; +static handle_t g_on_waitany_handle; // Records the handle to return on connect -handle_t g_on_connect_handle; +static handle_t g_on_connect_handle; extern ND bool nd_bool(void); @@ -114,13 +117,17 @@ Non-deterministically chooses an active handle Blocks if no active handle is available */ +// TODO: Change spec to include invalid handle handle_t sea_ht_choose_active_handle(void) { if (g_on_waitany_handle == NULL) { return INVALID_IPC_HANDLE; } // Check that the user set an active handle sassert(g_on_waitany_handle->active == true); - return g_on_waitany_handle; + handle_t handle = g_on_waitany_handle; + // NOTE: unset the handle after one use + g_on_waitany_handle = NULL; + return handle; } handle_t sea_ht_new_channel(handle_t parent_port) { @@ -159,7 +166,7 @@ void sea_ht_set_cookie_channel(handle_t handle, void *cookie) { // assume we are passed a channel void *sea_ht_get_cookie_channel(handle_t handle) { - return htop(handle)->cookie; + return handle == NULL ? NULL : htop(handle)->cookie; } // set cookie for both port/channel type @@ -168,7 +175,9 @@ void sea_ht_set_cookie(handle_t handle, void *cookie) { } // get cookie for both port/channel type -void *sea_ht_get_cookie(handle_t handle) { return htop(handle)->cookie; } +void *sea_ht_get_cookie(handle_t handle) { + return handle == NULL ? NULL : htop(handle)->cookie; +} // Set the handle to return on next wait_any call. // This remains set unless unset explicitly. @@ -176,4 +185,4 @@ void on_waitany_return(handle_t handle) { g_on_waitany_handle = handle; } // Set the handle to return on next connect call // This remains set unless unset explicitly. -void on_connect_return(handle_t handle) { g_on_connect_handle = handle; } \ No newline at end of file +void on_connect_return(handle_t handle) { g_on_connect_handle = handle; } diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/sea_handle_table.h b/seahorn/trusty/user/base/lib/libc-trusty-ptr/sea_handle_table.h index 4a2557e..b8b7175 100644 --- a/seahorn/trusty/user/base/lib/libc-trusty-ptr/sea_handle_table.h +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/sea_handle_table.h @@ -46,4 +46,5 @@ void on_waitany_return(handle_t handle); // Set the handle to return on next connect call void on_connect_return(handle_t handle); + #endif diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/trusty_syscalls_impl.c b/seahorn/trusty/user/base/lib/libc-trusty-ptr/trusty_syscalls_impl.c index c3d67af..0b8ebb4 100644 --- a/seahorn/trusty/user/base/lib/libc-trusty-ptr/trusty_syscalls_impl.c +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/trusty_syscalls_impl.c @@ -8,6 +8,12 @@ #define ND __declspec(noalias) extern ND void memhavoc(void *ptr, size_t size); +extern void sea_printf(const char *format, ...); + +extern void sea_reset_modified(char *); +extern bool sea_is_modified(char *); +extern void sea_tracking_on(void); +extern void sea_tracking_off(void); handle_t _trusty_port_create(const char *path, uint32_t num_recv_bufs, uint32_t recv_buf_size, uint32_t flags) { @@ -82,6 +88,7 @@ extern uint32_t nd_trusty_ipc_event(void); int _trusty_wait(handle_t handle, struct uevent *event, uint32_t timeout_msecs) { int err = nd_trusty_ipc_err(); + sea_printf("wait called\n"); if (err < NO_ERROR) return err; @@ -102,6 +109,9 @@ int _trusty_wait_any(uevent_t *ev, uint32_t timeout_msecs) { return err; handle_t h = sea_ht_choose_active_handle(); + if (h == INVALID_IPC_HANDLE) { + return ERR_BAD_HANDLE; + } ev->handle = h; ev->cookie = sea_ht_get_cookie(h); ev->event = nd_trusty_ipc_event(); @@ -131,7 +141,6 @@ ssize_t _trusty_read_msg(handle_t handle, uint32_t msg_id, uint32_t offset, if (msg_len == 0) return ERR_GENERIC; sassert(offset <= msg_len); - msg_len -= offset; sassert(1 <= msg->num_iov); @@ -139,9 +148,13 @@ ssize_t _trusty_read_msg(handle_t handle, uint32_t msg_id, uint32_t offset, if (msg_len < msg->iov[0].iov_len) { memhavoc(msg->iov[0].iov_base, msg_len); + /* reset modified bit to track unexpected writes */ + sea_reset_modified((char *)(msg->iov[0].iov_base)); return msg_len; } memhavoc(msg->iov->iov_base, msg->iov[0].iov_len); + /* reset modified bit to track unexpected writes */ + sea_reset_modified((char *)(msg->iov[0].iov_base)); size_t num_bytes_read = msg->iov[0].iov_len; if (msg->num_iov == 1) return num_bytes_read; @@ -149,10 +162,14 @@ ssize_t _trusty_read_msg(handle_t handle, uint32_t msg_id, uint32_t offset, if (msg_len < msg->iov[1].iov_len) { memhavoc(msg->iov[1].iov_base, msg_len); + /* reset modified bit to track unexpected writes */ + sea_reset_modified((char *)(msg->iov[1].iov_base)); num_bytes_read += msg_len; return num_bytes_read; } memhavoc(msg->iov->iov_base, msg->iov[1].iov_len); + sea_reset_modified((char *)(msg->iov->iov_base)); + num_bytes_read += msg->iov[1].iov_len; return num_bytes_read; } diff --git a/seahorn/trusty_common/include/nondet.h b/seahorn/trusty_common/include/nondet.h index 8346722..fb4e38d 100644 --- a/seahorn/trusty_common/include/nondet.h +++ b/seahorn/trusty_common/include/nondet.h @@ -7,13 +7,22 @@ #ifdef __cplusplus extern "C" { #endif + +/** + * Mark nondet functions as not accessing memory + * Note: if the attribute is too agressive, the optimizer might remove + * calls to nondet functions, thus reducing the amount of non-determinism. + * Note: using each nondet function only once grately simplifies debugging. + */ +#define NONDET_FN_ATTR __declspec(noalias) + // generic long nd_long(void); uint16_t nd_short(void); int32_t nd_int(void); -uint8_t nd_char(void); +char nd_char(void); uint32_t nd_unsigned(void); -void* nd_ptr(void); +void *nd_ptr(void); /** * for functions with return pattern: diff --git a/seahorn/trusty_common/stubs/realloc_override.c b/seahorn/trusty_common/stubs/realloc_override.c index 1130be0..6f158f0 100644 --- a/seahorn/trusty_common/stubs/realloc_override.c +++ b/seahorn/trusty_common/stubs/realloc_override.c @@ -4,17 +4,19 @@ */ -#include "sea_mem_helper.h" #include "nondet.h" +#include "sea_mem_helper.h" -#include #include +#include -int8_t *g_ptr0 = NULL; -size_t g_ptr0_size; +static int8_t *g_ptr0 = NULL; +static size_t g_ptr0_size; void *realloc(void *ptr, size_t new_size) { - if (ptr) {free(ptr);} + if (ptr) { + free(ptr); + } ptr = malloc(new_size); diff --git a/trusty_mod/trusty/user/app/storage/ipc.c b/trusty_mod/trusty/user/app/storage/ipc.c index 1aaed6d..475205b 100644 --- a/trusty_mod/trusty/user/app/storage/ipc.c +++ b/trusty_mod/trusty/user/app/storage/ipc.c @@ -21,7 +21,9 @@ #include #include -#include "ipc.h" +#include "seahorn/seahorn.h" +#include +#include #define MSG_BUF_MAX_SIZE 4096 @@ -87,7 +89,6 @@ static int do_connect(struct ipc_port_context *ctx, const uevent_t *ev) { handle_t rc1; handle_t chan_handle; struct ipc_channel_context *chan_ctx; - if (ev->event & IPC_HANDLE_POLL_READY) { /* incoming connection: accept it */ uuid_t peer_uuid; @@ -98,16 +99,13 @@ static int do_connect(struct ipc_port_context *ctx, const uevent_t *ev) { } chan_handle = (handle_t)rc1; - chan_ctx = ctx->ops.on_connect(ctx, &peer_uuid, chan_handle); if (chan_ctx == NULL) { TLOGE("%s: failure initializing channel state (%p)\n", __func__, rc1); rc = ERR_GENERIC; goto err_on_connect; } - assert(is_valid_chan_ops(&chan_ctx->ops)); - chan_ctx->common.evt_handler = handle_channel; chan_ctx->common.handle = chan_handle; @@ -116,9 +114,9 @@ static int do_connect(struct ipc_port_context *ctx, const uevent_t *ev) { TLOGE("failed (%d) to set_cookie on chan %p\n", rc, chan_handle); goto err_set_cookie; } + list_add_tail(&ctx->channels, &chan_ctx->node); } - return NO_ERROR; err_set_cookie: @@ -130,7 +128,6 @@ static int do_connect(struct ipc_port_context *ctx, const uevent_t *ev) { static int do_handle_msg(struct ipc_channel_context *ctx, const uevent_t *ev) { handle_t chan = ev->handle; - /* get message info */ ipc_msg_info_t msg_inf; int rc = get_msg(chan, &msg_inf); @@ -170,7 +167,6 @@ static int do_handle_msg(struct ipc_channel_context *ctx, const uevent_t *ev) { TLOGE("invalid message of size (%d, %p)\n", rc, chan); return ERR_NOT_VALID; } - rc = ctx->ops.on_handle_msg(ctx, msg_buf, msg_inf.len); err_handle_msg: @@ -244,6 +240,7 @@ static int read_response(handle_t session, uint32_t msg_id, static int await_response(handle_t session, struct ipc_msg_info *inf) { uevent_t uevt; long rc = wait(session, &uevt, INFINITE_TIME); + if (rc != NO_ERROR) { TLOGE("%s: interrupted waiting for response (%ld)", __func__, rc); return rc; @@ -367,7 +364,7 @@ static void dispatch_event(const uevent_t *ev) { int ipc_port_create(struct ipc_port_context *ctxp, const char *port_name, size_t queue_size, size_t max_buffer_size, uint32_t flags) { - int rc; + int rc = -1; handle_t rc1; assert(ctxp); assert(is_valid_port_ops(&ctxp->ops)); diff --git a/verify.py.in b/verify.py.in index 4bd3196..5f25ed8 100755 --- a/verify.py.in +++ b/verify.py.in @@ -14,28 +14,44 @@ import sys SEAHORN_ROOT = "@SEAHORN_ROOT@" ASSERT_ERROR_PREFIX = r'^Error: assertion failed' # the plan is to have two sets, vac error and info and put filepath:linenumbers) into both -VACUITY_CHECK_RE = r'^(?PInfo|Error).*(?Pvacuity).*(?Ppassed|failed).*sat\) (?P.*)$' - -def check_vacuity(line, passed_set, failed_set): +VACUITY_CHECK_RE = r'^(?PInfo|Error).*(?Pvacuity|assertion).*(?Ppassed|failed).*sat\) (?P.*)$' + +# inspired from https://stackoverflow.com/questions/287871/how-do-i-print-colored-text-to-the-terminal +class bcolors: + HEADER = '\033[95m' + OKBLUE = '\033[94m' + OKCYAN = '\033[96m' + OKGREEN = '\033[92m' + WARNING = '\033[93m' + ERROR = '\033[91m' + ENDC = '\033[0m' + BOLD = '\033[1m' + UNDERLINE = '\033[4m' + +# return true if found a 'vacuity' line, false otherwise +def check_vacuity(line, key, passed_set, failed_set): m = re.match(VACUITY_CHECK_RE, line) if not m: - return + return False debugInfo = m.group('debuginfo') if (m.group('stream') == 'Info' - and m.group('what') == 'vacuity' + and m.group('what') == key and m.group('result') == 'passed'): passed_set.add(debugInfo.strip()) + return True elif (m.group('stream') == 'Error' - and m.group('what') == 'vacuity' + and m.group('what') == key and m.group('result') == 'failed'): failed_set.add(debugInfo.strip()) + return True + return False def main(argv): import sea - def check_vacuity_inner(line, passed_set, failed_set): - return check_vacuity(line, passed_set, failed_set) + def check_vacuity_inner(line, key, passed_set, failed_set): + return check_vacuity(line, key, passed_set, failed_set) class VerifyCmd(sea.CliCmd): def __init__(self): @@ -66,7 +82,6 @@ def main(argv): def run(self, args=None, _extra=[]): extra = _extra + args.extra - script_dir = os.path.abspath(sys.argv[0]) script_dir = os.path.dirname(script_dir) @@ -123,10 +138,14 @@ def main(argv): if args.verbose: print(' '.join(cmd)) - - if args.expect is None: + # NOTE: When running in vac mode we always + # want to post-process after seahorn run. + # Thus, don't exec! + # TODO: Remove exec-and-never-return logic + # since it complicates how sea is run, possibly + # unecessarily. + if args.expect is None and not args.vac: os.execv(cmd[0], cmd) - import subprocess process = subprocess.Popen(cmd, shell=False, encoding='utf-8', @@ -137,21 +156,30 @@ def main(argv): found_error = False vacuity_passed = set() vacuity_failed = set() + assertion_passed = set() + assertion_failed = set() for line in iter(process.stdout.readline, ''): - if not args.silent: - print(line, end='') - + assertion_line = check_vacuity_inner(line, 'assertion', assertion_passed, assertion_failed) + vacuity_line = False # checks after this line are mutually exclusive if not found_expected and args.expect is not None and line.strip() == args.expect: found_expected = True elif re.match(ASSERT_ERROR_PREFIX, line): found_error = True else: - check_vacuity_inner(line, vacuity_passed, vacuity_failed) - + vacuity_line = check_vacuity_inner(line, 'vacuity', vacuity_passed, vacuity_failed) + if not args.silent and not vacuity_line and not assertion_line: + print(line, end='') process.stdout.close() rcode = process.wait() - + if args.vac: + for passed in assertion_passed: + print(f"{bcolors.OKGREEN}Assertion passed: {passed}{bcolors.ENDC}") + for fail in assertion_failed: + print(f"{bcolors.ERROR}Assertion failed: {fail}{bcolors.ENDC}", file=sys.stderr) + fails = (vacuity_failed - vacuity_passed) + for fail in fails: + print(f"{bcolors.ERROR}Vacuity failed: {fail}{bcolors.ENDC}", file=sys.stderr) if args.vac and found_error: return 2 elif args.vac and (vacuity_failed - vacuity_passed):