From d75f762589074554d1dacc9d3e1eac38d03d666c Mon Sep 17 00:00:00 2001
From: Gus O'Hanley <guso@galois.com>
Date: Fri, 20 Dec 2024 16:47:07 -0600
Subject: [PATCH] simple example of failable malloc

---
 components/include/cn_memory.h             | 27 ++++++++++++++----
 components/mission_key_management/client.c | 32 +++++++++++++++++++---
 2 files changed, 49 insertions(+), 10 deletions(-)

diff --git a/components/include/cn_memory.h b/components/include/cn_memory.h
index f4fce0bb..5aa11183 100644
--- a/components/include/cn_memory.h
+++ b/components/include/cn_memory.h
@@ -56,17 +56,32 @@ ensures
     true;
 $*/
 
+/*$
+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(size_t n);
 /*$
 spec _malloc(u64 n);
 requires true;
 ensures
-    !is_null(return);
-    take log = Alloc(return);
-    allocs[(alloc_id)return] == log;
-    log.base == (u64) return;
-    log.size == n;
-    take i = each(u64 j; j >= 0u64 && j < n) {Block<uint8_t>(array_shift<uint8_t>(return, j))};
+    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
index 94d11f68..900727c9 100644
--- a/components/mission_key_management/client.c
+++ b/components/mission_key_management/client.c
@@ -74,14 +74,38 @@ requires ValidState( state );
         } 
     }
 }
+/*$
+datatype newmem_client {
+NewMemClientF {{u64 base, u64 size} al, struct client bu}
+}
 
+predicate (datatype newmem_client) MallocResult_Owned_struct_client(pointer p)
+{
+  if (is_null(p)) {
+    return NewMemClientF { al : default<{u64 base, u64 size}>, bu : default<struct client>};
+  } else {
+    let n = sizeof<struct client>;
+    take log = Alloc(p);
+    assert(allocs[(alloc_id)p] == log);
+    assert(log.base == (u64) p);
+    assert(log.size == n);
+    take i = Owned<struct client>(p);
+
+    return NewMemClientF { al : log, bu : i};
+  }
+}
+$*/
 struct client* client_new(int fd) 
 // TODO: Specification doesn't handle the case where malloc fails 
 /*$ 
-ensures take Client_out = ClientPred(return);
-        take log = Alloc(return);
-        Client_out.fd == fd; 
-        ((i32) Client_out.state) == CS_RECV_KEY_ID;
+ensures
+    take nmem = MallocResult_Owned_struct_client(return);
+    let Client_out = match nmem {
+      NewMemClientF {al: _, bu: x} => {x}
+    };
+    is_null(return) ? true : Client_out.fd == fd;
+    is_null(return) ? true : Client_out.pos == 0u8;
+    is_null(return) ? true : ((i32) Client_out.state) == CS_RECV_KEY_ID;
 $*/
 {
     struct client* c = malloc(sizeof(struct client));