Changing CVM to a fork/exec style with STDIO communication

README.md

@@ -14,6 +14,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 The Copland Virtual Machine (CVM) is a Rocq library that formalizes a virtual machine for the Copland Domain Specific Language for layered remote attestation.
 
+*NOTE*: The CVM expects to communicate with ASP's via a fork/exec style where the ASP is launched, reads input from stdin, and writes output to stdout. Utilizing the [`rust-am-lib`](https://github.com/ku-sldg/rust-am-lib) version 0.3.0 and greater should be sufficient to meet these requirements. The CVM does not currently support any other style of communication with ASP's, but support for additional styles may be added in the future.
+
 ## Meta
 
 - Author(s):

meta.yml

@@ -10,7 +10,7 @@ authors:
   - name: "Will Thomas"
     email: "30wthomas@ku.edu"
 opam-file-maintainer: "30wthomas@ku.edu" # Need a strong default here or we will accidentally email a Coq developer
-opam-file-version: "0.1.2"
+opam-file-version: "0.2.0"
 
 ######################################################
 # NOTE: Optional Extra Info

rocq-cvm.opam

@@ -3,7 +3,7 @@
 
 opam-version: "2.0"
 maintainer: "30wthomas@ku.edu"
-version: "0.1.2"
+version: "0.2.0"
 
 homepage: "https://github.com/ku-sldg/cvm"
 dev-repo: "git+https://github.com/ku-sldg/cvm.git"

stubs/FFI/SysFFI.cml

@@ -5,29 +5,35 @@ structure SysFFI = struct
 
   local 
       fun ffi_system x y = #(system) x y
-      fun ffi_popen_string x y = #(popen_string) x y
+      fun ffi_exec_process_io x y = #(exec_process_io) x y
   in
-    fun escFn c =
-        case Char.ord c of
-          8  => "\\b"
-        |  9  => "\\t"
-        | 10  => "\\n"
-        | 12  => "\\f"
-        | 13  => "\\r"
-        | 34  => "\\\""
-        | _   => String.str c
-
-    fun shellEscapeString str =
-        String.concat (List.map escFn (String.explode str))
-
-    (* () -> string *)
-    fun c_popen_string (com) = 
-      let val command_bs = BString.fromString com
-          val resp_bs = FFI.buffered_call ffi_popen_string command_bs
+    (**
+     * c_exec_process_io: Spawn a process and communicate via stdin/stdout.
+     *
+     * The process at `process` is executed directly via fork/exec.
+     * `arg_str` is written to the process's stdin, then stdin is closed
+     * (sending EOF). The process's stdout is read and returned.
+     *
+     * Input encoding sent to FFI:
+     *   [ ProcessPathLength : 4 bytes (big-endian) ;
+     *     ProcessPath       : ProcessPathLength bytes ;
+     *     ArgString         : remaining bytes ]
+     *
+     * @param process  Absolute path to the executable
+     * @param arg_str  String to write to the process's stdin
+     * @return         The process's stdout output as a string
+     *)
+    fun c_exec_process_io (process : string) (arg_str : string) = 
+      let val process_bs = BString.fromString process
+          val process_len_bs = BString.int_to_qword (BString.length process_bs)
+          val arg_bs = BString.fromString arg_str
+          val payload = BString.concat (BString.concat process_len_bs process_bs) arg_bs
+          val resp_bs = FFI.buffered_call ffi_exec_process_io payload
       in 
         BString.toString resp_bs
       end
-      handle _ => raise (Exception "Unknown Error thrown from c_popen_string, likely check that the word8 array is right length that is expected and not accessing something outside of its bounds")
+      handle Exception e => raise (Exception e)
+           | _ => raise (Exception "Unknown Error thrown from c_exec_process_io, likely check that the word8 array is right length that is expected and not accessing something outside of its bounds")
   end
 
 end