mkm: Add test script for cn test, modify other files to make it work

components/mission_key_management/client.c

@@ -34,46 +34,6 @@
  - make the key access table into a global?? 
 */
 
-/*$ predicate (map<u64,u8>) KeyPred (pointer p) 
-{
-    if (! is_null(p)) { 
-        take K = each(u64 i; i < KEY_SIZE()) {Owned<uint8_t>(array_shift<uint8_t>(p,i))}; 
-        return K; 
-    } else {
-        return default< map<u64,u8> >; 
-    }
-}
-
-// TODO: should be implicit from the fact client_state is an enum 
-function (boolean) ValidState (u32 state) {
-   ((state == (u32) CS_RECV_KEY_ID) || 
-    (state == (u32) CS_SEND_CHALLENGE) || 
-    (state == (u32) CS_RECV_RESPONSE) || 
-    (state == (u32) CS_SEND_KEY) || 
-    (state == (u32) CS_DONE) )
-}
-
-// TODO: wrap up the alloc() in the ClientPred predicate 
-predicate (struct client) ClientPred (pointer p)
-{
-    take C = Owned<struct client>(p); 
-    assert ( ValidState(C.state) ) ; 
-    take K = KeyPred(C.key); // Discard the key
-    return C; 
-}
-
-function (boolean) ValidTransition (u32 pre, u32 post) {
-   (
-       ( pre == post ) 
-    || ( (pre == (u32) CS_RECV_KEY_ID)    && (post == (u32) CS_SEND_CHALLENGE) ) 
-    || ( (pre == (u32) CS_SEND_CHALLENGE) && (post == (u32) CS_RECV_RESPONSE)  ) 
-    || ( (pre == (u32) CS_RECV_RESPONSE)  && (post == (u32) CS_SEND_KEY)       ) 
-    || ( ValidState(pre)                  && (post == (u32) CS_DONE)           ) 
-   )
-}
-$*/
-
-
 uint32_t client_state_epoll_events(enum client_state state) 
 /*$
 requires ValidState( state ); 

components/mission_key_management/client.h

@@ -62,3 +62,53 @@ int client_epoll_ctl(struct client* c, int epfd, int op);
 // and started a new one, so the caller should next call `client_epoll_ctl`
 // netx to update the epoll event mask.
 enum client_event_result client_event(struct client* c, uint32_t events);
+
+// Either the key is in memory and owned, or the pointer is null 
+/*$ 
+predicate (map<u64,u8>) KeyPred (pointer p) 
+{
+    if (! is_null(p)) { 
+        take K = each(u64 i; i < KEY_SIZE()) {Owned<uint8_t>(array_shift<uint8_t>(p,i))}; 
+        return K; 
+    } else {
+        return default< map<u64,u8> >; 
+    }
+}
+$*/ 
+
+// Pure predicate representing valid states of `enum client_state`. 
+// CN could easily generate this automatically (see #796) 
+/*$
+function (boolean) ValidState (u32 state) {
+   ((state == (u32) CS_RECV_KEY_ID) || 
+    (state == (u32) CS_SEND_CHALLENGE) || 
+    (state == (u32) CS_RECV_RESPONSE) || 
+    (state == (u32) CS_SEND_KEY) || 
+    (state == (u32) CS_DONE) )
+}
+$*/
+
+// Predicate representing a valid client object 
+/*$
+// TODO: wrap up the alloc() in the ClientPred predicate? 
+predicate (struct client) ClientPred (pointer p)
+{
+    take C = Owned<struct client>(p); 
+    assert ( ValidState(C.state) ) ; 
+    take K = KeyPred(C.key); // Discard the key
+    return C; 
+}
+$*/ 
+
+// Pure predicate representing the MKM state machine transitions 
+/*$
+function (boolean) ValidTransition (u32 pre, u32 post) {
+   (
+       ( pre == post ) 
+    || ( (pre == (u32) CS_RECV_KEY_ID)    && (post == (u32) CS_SEND_CHALLENGE) ) 
+    || ( (pre == (u32) CS_SEND_CHALLENGE) && (post == (u32) CS_RECV_RESPONSE)  ) 
+    || ( (pre == (u32) CS_RECV_RESPONSE)  && (post == (u32) CS_SEND_KEY)       ) 
+    || ( ValidState(pre)                  && (post == (u32) CS_DONE)           ) 
+   )
+}
+$*/

components/mission_key_management/cn_stubs.h

@@ -5,6 +5,7 @@
 
 // Cerberus puts some POSIX headers under the `posix/` directory.
 #include "policy.h"
+#include "client.h"
 
 // From `sys/epoll.h`
 #define EPOLLIN 1
@@ -16,7 +17,7 @@
 // From `policy.h`
 
 // This is the idiomatic CN lifting of macro constants, per 
-// https://rems-project.github.io/cn-tutorial/getting-started/style-guide/?h=constant
+// https://rems-project.github.io/cn-tutorial/getting-started/style-guide/#constants
 
 /*$ function (u64) KEY_ID_SIZE () $*/
 static uint64_t c_KEY_ID_SIZE() /*$ cn_function KEY_ID_SIZE; $*/ { return KEY_ID_SIZE; }

components/mission_key_management/policy.h

@@ -1,6 +1,8 @@
 #pragma once
 
+#ifndef CN_ENV
 #include <stdint.h>
+#endif
 
 #define KEY_ID_SIZE 1
 #define NONCE_SIZE 16

components/mission_key_management/process.sh → components/mission_key_management/process-cn-test.sh

@@ -27,7 +27,7 @@ OUTPUT_FILE="${2:-$DEFAULT_OUTPUT}"
 TMP_DIR="$(mktemp -d)"
 trap 'rm -rf "$TMP_DIR"' EXIT
 
-# 1. Split at the first occurrence of /\/\/SYSTEM_HEADERS/
+# 1. Split the file at the first occurrence of string "//SYSTEM_HEADERS"
 csplit -s -f "${TMP_DIR}/split_" -n 1 "$INPUT_FILE" "/\/\/SYSTEM_HEADERS/"
 
 # 2. Run the C preprocessor on the second chunk
@@ -38,21 +38,26 @@ eval "$(opam env)"
 
 # gcc flags, stored in an array for robustness
 GCC_FLAGS=(
+  "-H" # Print the include tree - useful for debugging 
   "-E" "-P" "-CC" "-x" "c"
-  "--include=${ROOT_DIR}/../include/wars.h"
+  # TODO: revisit the line below. This is needed when running `cn verify`, but I
+  # think is redundant here: 
+  # "--include=${ROOT_DIR}/../include/wars.h" 
   "-I${ROOT_DIR}/../include"
   "-I."
   "-I${OPAM_SWITCH_PREFIX}/lib/cerberus/runtime/libc/include/posix"
-  "-DCN_ENV"
+  "-DCN_ENV" "-DWAR_CN_309"
 )
 
-# # Print the exact command for debug purposes  
-# echo "Running gcc command:"
-# echo gcc "${GCC_FLAGS[@]}" "${TMP_DIR}/split_1" -o "${TMP_DIR}/split_1_out.c"
+# Print the exact command for debug purposes  
+echo "Running gcc command:"
+echo gcc "${GCC_FLAGS[@]}" "${TMP_DIR}/split_1" -o "${TMP_DIR}/split_1_out.c"
+echo ""
 
+echo "Include tree:" 
 gcc "${GCC_FLAGS[@]}" "${TMP_DIR}/split_1" -o "${TMP_DIR}/split_1_out.c"
 
 # 3. Concatenate the first chunk and preprocessed second chunk
 cat "${TMP_DIR}/split_0" "${TMP_DIR}/split_1_out.c" > "$OUTPUT_FILE"
 
-echo "Done. Merged output is in: $OUTPUT_FILE"
+echo "\nDone. Merged output is in: $OUTPUT_FILE"

components/mission_key_management/run-cn-test.sh

@@ -0,0 +1,39 @@
+#!/usr/bin/env bash
+
+set -euo pipefail
+
+# Check arguments
+if [[ $# -lt 1 ]]; then
+  echo "Usage: $0 <input-file> [<testgen-dir>]"
+  exit 1
+fi
+
+INPUT_FILE="$1"
+OUTBASE="${INPUT_FILE%.c}"
+OUTPUT_FILE="${OUTBASE}-out.c"
+
+./process-cn-test.sh "${INPUT_FILE}" "${OUTPUT_FILE}" 
+
+# Create a temporary directory and ensure it's cleaned up on exit
+TMP_DIR="$(mktemp -d)"
+trap 'rm -rf "$TMP_DIR"' EXIT
+TESTGEN_DIR="${2:-$TMP_DIR}"
+
+ROOT_DIR="$(pwd)"
+
+eval "$(opam env)"
+
+# CN flags, stored in an array for robustness
+CN_FLAGS=(
+  "--output=${TESTGEN_DIR}"
+  "--include=${ROOT_DIR}/../include/wars.h"
+  # "-I${ROOT_DIR}/../include" # Already preprocessed away 
+  "-I${OPAM_SWITCH_PREFIX}/lib/cerberus/runtime/libc/include/posix"
+  "--magic-comment-char-dollar"
+)
+
+# Sanity check - the resulting file should be verifiable if the original is 
+# cn verify "${CN_FLAGS[@]}" "${OUTPUT_FILE}" 
+
+# Run CN-test on the resulting file 
+cn test "${CN_FLAGS[@]}" "${OUTPUT_FILE}"