mkm: integrated possibly-failing malloc()

GaloisInc · Jan 1, 2025 · 8466469 · 8466469
1 parent e0f081f
commit 8466469
Show file tree

Hide file tree

Showing 4 changed files with 59 additions and 8 deletions.
diff --git a/components/include/cn_memory.h b/components/include/cn_memory.h
@@ -69,4 +69,30 @@ ensures
     take i = each(u64 j; j >= 0u64 && j < n) {Block<uint8_t>(array_shift<uint8_t>(return, j))};
 $*/
 
+/*$
+datatype newmem {
+    NewMemF {{u64 base, u64 size} al, map<u64, u8> bu}
+}
+predicate (datatype newmem) MallocResult(pointer p, u64 n)
+{
+  if (is_null(p)) {
+    return NewMemF { al : default<{u64 base, u64 size}>, bu : default<map<u64, u8> >};
+  } else {
+    take log = Alloc(p);
+    assert(allocs[(alloc_id)p] == log);
+    assert(log.base == (u64) p);
+    assert(log.size == n);
+    take i = each(u64 j; j >= 0u64 && j < n) {Block<uint8_t>(array_shift<uint8_t>(p, j))};
+    return NewMemF { al : log, bu : i};
+  }
+}
+$*/
+
+void *_malloc_canfail(size_t n);
+/*$
+spec _malloc_canfail(u64 n);
+requires true;
+ensures  take Out = MallocResult(return, n);
+$*/
+
 #endif // CN_MEMCPY_H_
diff --git a/components/mission_key_management/client.c b/components/mission_key_management/client.c
@@ -74,12 +74,22 @@ requires ValidState( state );
 }
 
 struct client* client_new(int fd) 
-// TODO Specification doesn't handle the case where malloc fails 
+// TODO totally dumb hack forced by `cn test` not supporting default values  
+#if ! defined(CN_TEST)
 /*$ 
-ensures take Client_out = ClientPred(return);
-        Client_out.fd == fd; 
-        ((i32) Client_out.state) == CS_RECV_KEY_ID;
+ensures 
+    take Client_out = MaybeClientPred(return);
+    is_null(return) ? true : Client_out.fd == fd; 
+    is_null(return) ? true : ((i32) Client_out.state) == CS_RECV_KEY_ID;
 $*/
+#else 
+/*$ 
+ensures 
+    take Client_out = ClientPred(return);
+    Client_out.fd == fd; 
+    ((i32) Client_out.state) == CS_RECV_KEY_ID;
+$*/
+#endif 
 {
     struct client* c = malloc(sizeof(struct client));
     if (c == NULL) {

diff --git a/components/mission_key_management/client.h b/components/mission_key_management/client.h
@@ -73,7 +73,7 @@ predicate (boolean) KeyPred (pointer p)
 {
     if (! is_null(p)) { 
         take K = each(u64 i; i < KEY_SIZE()) {Owned<uint8_t>(array_shift<uint8_t>(p,i))}; 
-        // TODO: better to use `default` here, but it's not supported by cn test yet 
+        // TODO: should use `default` here, but it's not supported by `cn test` yet 
         return true; 
     } else {
         return false; 
@@ -93,8 +93,8 @@ function (boolean) ValidState (u32 state) {
 }
 $*/
 
-// Wrapper predicate for the allocation record. We distinguish between cases
-// because `cn test` doesn't handle Alloc() yet
+// TODO Wrapper predicate for the allocation record. We distinguish between
+// cases because `cn test` doesn't handle Alloc() yet
 #if ! defined(CN_TEST)
 /*$
 predicate (boolean) ClientAlloc (pointer p)
@@ -126,6 +126,21 @@ predicate (struct client) ClientPred (pointer p)
 }
 $*/ 
 
+#if ! defined(CN_TEST)
+// TODO This is a hack. CN should have a proper Option type 
+/*$ 
+predicate (struct client) MaybeClientPred(pointer p)
+{
+    if (is_null(p)) {
+        return default<struct client>; 
+    } else {
+        take Client_out = ClientPred(p);
+        return Client_out;  
+    }
+}
+$*/
+#endif 
+
 // Pure predicate representing the MKM state machine transitions 
 /*$
 function (boolean) ValidTransition (u32 pre, u32 post) {

diff --git a/components/mission_key_management/cn_stubs.h b/components/mission_key_management/cn_stubs.h
@@ -13,7 +13,7 @@
 // For verification, use specs in ../../components/include/cn_memory.h
 # define memcpy(d,s,n) _memcpy(d,s,n)
 # define memcmp(s1,s2,n) _memcmp(s1,s2,n)
-# define malloc(x) _malloc(x)
+# define malloc(x) _malloc_canfail(x)
 # define free(x) _free(x)
 #else 
 // For testing, use the CN-specific instrumented malloc() / free()