WIP ipc verification

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)
 

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

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

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,18 +40,22 @@ 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
 # should be at least MAX_BUFFER_SIZE
   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

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)

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.

seahorn/sea_libc/include/assert.h

@@ -0,0 +1,4 @@
+#pragma once
+#undef assert
+
+#define assert(x) sassert(x)

seahorn/sea_libc/include/sea_allocators.h

@@ -0,0 +1,60 @@
+/** Different memory allocators*/
+#pragma once
+#include <stddef.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+#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);

seahorn/sea_libc/src/realloc.c

@@ -0,0 +1,3 @@
+#include <sea_allocators.h>
+
+void *realloc(void *ptr, size_t new_size) { return sea_realloc(ptr, new_size); }

seahorn/sea_libc/src/sea_allocators.c

@@ -0,0 +1,80 @@
+/** Memory allocating functions */
+#include <sea_allocators.h>
+
+#include <nondet.h>
+#include <seahorn/seahorn.h>
+
+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);
+}

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)
+add_subdirectory(jobs/ipc/port_create_destroy)
+add_subdirectory(jobs/ipc/ipc_session)

seahorn/storage/include/sea_ipc_helper.h

@@ -1,19 +1,18 @@
 #pragma once
 
 #include <ipc.h>
-#include <trusty_ipc.h>
+// #include <trusty_ipc.h>
 
 /*
  * 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);
+                         const uuid_t *peer_uuid, handle_t chan_handle);

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)
+sea_add_unsat_test(storage_ipc_indirect_handlers)

seahorn/storage/jobs/ipc/indirect_handlers/indirect_handlers_harness.c

@@ -20,11 +20,11 @@
 #include <trusty_log.h>
 #include <uapi/err.h>
 
-#include "ipc.h"
+#include <ipc.h>
 
-#include <sea_handle_table.h>
 #include "seahorn/seahorn.h"
-#include "sea_ipc_helper.h"
+#include <sea_handle_table.h>
+#include <sea_ipc_helper.h>
 
 #include "tipc_limits.h"
 #include <interface/storage/storage.h>

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)