diff --git a/seahorn/trusty_common/include/handle_table.h b/seahorn/trusty_common/include/handle_table.h deleted file mode 100644 index 389d675..0000000 --- a/seahorn/trusty_common/include/handle_table.h +++ /dev/null @@ -1,50 +0,0 @@ -#pragma once -#include "seahorn/seahorn.h" - -#include -#include - -#include // for INVALID_IPC_HANDLE and handle_t -/* -Single class for holding a map of handles -*/ -#ifdef __cplusplus -extern "C" { -#endif -typedef struct handle_table { - // In keymaster_ipc, assuming handles are treated one by one, - // each either "handled" or removed by close(), - // so one handle_t each for port and channel is sufficient - handle_t secure_port_handle; - bool secure_port_handle_active; - void* secure_port_cookie; - - handle_t non_secure_port_handle; - bool non_secure_port_handle_active; - void* non_secure_port_cookie; - - handle_t chan_handle; - bool chan_handle_active; - void* chan_cookie; -} handle_table_t; - -/* lookuptable-like functions */ -void handle_table_init(handle_t secure_port, handle_t non_secure_port, handle_t channel); -void add_handle(handle_t handle); -void remove_handle(handle_t handle); -bool contains_handle(handle_t handle); -void* get_handle_cookie(handle_t handle); -void set_handle_cookie(handle_t handle, void* cookie); - -/* Getters */ -handle_t get_secure_port_handle(void); -handle_t get_non_secure_port_handle(void); -handle_t get_current_chan_handle(void); - -bool is_secure_port_active(void); -bool is_non_secure_port_active(void); -bool is_current_chan_active(void); - -#ifdef __cplusplus -} -#endif diff --git a/seahorn/trusty_common/lib/CMakeLists.txt b/seahorn/trusty_common/lib/CMakeLists.txt deleted file mode 100644 index 678928a..0000000 --- a/seahorn/trusty_common/lib/CMakeLists.txt +++ /dev/null @@ -1,11 +0,0 @@ -# proof helpers -add_library(sea_common_proofs - handle_table.c - nondet.c - bcmp.c -) - -if(SEA_ALLOCATOR_CAN_FAIL) - target_compile_definitions(sea_common_proofs PRIVATE SEA_ALLOCATOR_CAN_FAIL) -endif() -sea_attach_bc(sea_common_proofs) diff --git a/seahorn/trusty_common/lib/bcmp.c b/seahorn/trusty_common/lib/bcmp.c deleted file mode 100644 index 9bf8e34..0000000 --- a/seahorn/trusty_common/lib/bcmp.c +++ /dev/null @@ -1,19 +0,0 @@ -#include - -#include -#include -#include -#include - -#define INLINE __attribute__((always_inline)) - -INLINE void *__memcpy_chk(void *dest, const void *src, size_t len, - size_t dstlen) { - sassert(!(dstlen < len)); - return __builtin_memcpy(dest, src, len); -} - -INLINE void *__memset_chk(void *dest, int c, size_t len, size_t dstlen) { - sassert(!(dstlen < len)); - return __builtin_memset(dest, c, len); -} \ No newline at end of file diff --git a/seahorn/trusty_common/lib/handle_table.c b/seahorn/trusty_common/lib/handle_table.c deleted file mode 100644 index fac73a6..0000000 --- a/seahorn/trusty_common/lib/handle_table.c +++ /dev/null @@ -1,93 +0,0 @@ -/** - Channel and Port Handles. - - Current implementation supports one channel, one secure port, and one non-secure port. - - A channel/port is active if a handle is registered for it. - - All handles are distinct. Ties are broken by priority on ports and channels (see code for details). - */ -#include "handle_table.h" - -// only allow access from functions within this file -static handle_table_t ht; - -void handle_table_init(handle_t secure_port, handle_t non_secure_port, handle_t channel) { - ht.secure_port_handle = secure_port; - ht.secure_port_handle_active = secure_port != INVALID_IPC_HANDLE; - - ht.non_secure_port_handle = non_secure_port; - ht.non_secure_port_handle_active = non_secure_port != INVALID_IPC_HANDLE; - - ht.chan_handle = channel; - ht.chan_handle_active = channel != INVALID_IPC_HANDLE; - return; -} - -#define IS_PORT_HANDLE(h) ((h) & 0x2) -#define IS_SECURE_HANDLE(h) ((h) & 0x1) -void add_handle(handle_t handle) { - if (IS_PORT_HANDLE(handle)) { - if (IS_SECURE_HANDLE(handle)) { - ht.secure_port_handle = handle; - ht.secure_port_handle_active = true; - } else { - ht.non_secure_port_handle = handle; - ht.non_secure_port_handle_active = true; - } - } else { - ht.chan_handle = handle; - ht.chan_handle_active = true; - } -} - -void remove_handle(handle_t handle) { - if (handle == ht.secure_port_handle) { - ht.secure_port_handle_active = false; - } else if (handle == ht.non_secure_port_handle) { - ht.non_secure_port_handle_active = false; - } else if (handle == ht.chan_handle) { - ht.chan_handle_active = false; - } -} - -bool contains_handle(handle_t handle) { - if (handle == ht.secure_port_handle) { - return ht.secure_port_handle_active; - } else if (handle == ht.non_secure_port_handle) { - return ht.non_secure_port_handle_active; - } else if (handle == ht.chan_handle) { - return ht.chan_handle_active; - } - return false; -} - -void *get_handle_cookie(handle_t handle) { - if (handle == ht.secure_port_handle) { - return ht.secure_port_cookie; - } else if (handle == ht.non_secure_port_handle) { - return ht.non_secure_port_cookie; - } else if (handle == ht.chan_handle) { - return ht.chan_cookie; - } - return NULL; -} - -void set_handle_cookie(handle_t handle, void *cookie) { - if (handle == ht.secure_port_handle) { - ht.secure_port_cookie = cookie; - } else if (handle == ht.non_secure_port_handle) { - ht.non_secure_port_cookie = cookie; - } else if (handle == ht.chan_handle) { - ht.chan_cookie = cookie; - } -} - -handle_t get_secure_port_handle(void) {return ht.secure_port_handle;} -handle_t get_non_secure_port_handle(void) {return ht.non_secure_port_handle;} -handle_t get_current_chan_handle(void) {return ht.chan_handle;} - -bool is_secure_port_active(void) {return ht.secure_port_handle_active;} -bool is_non_secure_port_active(void) {return ht.non_secure_port_handle_active;} -bool is_current_chan_active(void) {return ht.chan_handle_active;} - diff --git a/seahorn/trusty_common/lib/nondet.c b/seahorn/trusty_common/lib/nondet.c deleted file mode 100644 index 021d7b6..0000000 --- a/seahorn/trusty_common/lib/nondet.c +++ /dev/null @@ -1,26 +0,0 @@ -#include "nondet.h" -#include "seahorn/seahorn.h" - -int nd_trusty_errs(void) { - int ret = nd_int(); - assume(ret <= NO_ERROR); - return ret; -} - -int nd_get_msg_ret(void) { return nd_trusty_errs(); } - -int nd_put_msg_ret(void) { return nd_trusty_errs(); } - -int nd_wait_any_ret(void) { return nd_trusty_errs(); } - -uint32_t nd_event_flag(void) { - uint32_t flag = nd_unsigned(); - assume(flag < (uint32_t)0x16); // max is (1111)2 - return flag; -} - -int nd_set_cookie_ret(void) { return nd_trusty_errs(); } - -int nd_close_ret(void) { return nd_trusty_errs(); } - -int nd_wait_ret(void) { return nd_trusty_errs(); }