Move Candle specific files to a new subdirectory

basics.ml

@@ -8,7 +8,7 @@
 (*     (c) Copyright, Andrea Gabrielli, Marco Maggesi 2017-2018              *)
 (* ========================================================================= *)
 
-needs "candle_kernel.ml";;
+needs "candle/kernel.ml";;
 
 (* ------------------------------------------------------------------------- *)
 (* Create probably-fresh variable                                            *)

build-instructions.sh

@@ -1,32 +1,44 @@
 #!/bin/bash
+# Set up "strict mode" for bash
 set -euo pipefail
 
+# Create (if needed) + Change into the build directory
+mkdir -p candle/build
+cd candle/build
+
 # Get the 64-bit CakeML compiler from here:
-curl -OL https://cakeml.org/regression/artefacts/3276/cake-x64-64.tar.gz
-tar xvzf cake-x64-64.tar.gz
+curl -OL https://cakeml.org/regression/artefacts/3286/cake-x64-64.tar.gz
+tar xvzf cake-x64-64.tar.gz --strip-components=1
 
 # By default, the CakeML compiler reserves a few kilobytes for constants and
 # code produced by the dynamic compiler. Using Candle requires setting these
 # to some megabytes:
-patch cake-x64-64/cake.S cake.S.patch
+patch cake.S ../cake.S.patch
 
-# Build the compiler binary
-cd cake-x64-64 && make && cd ..
+# Patching in useful FFI calls
+patch basis_ffi.c ../basis_ffi.c.patch
 
-# Copy the compiler binary, the exported compiler state and candle_boot.ml into
-# this directory:
-cp cake-x64-64/cake cake-x64-64/config_enc_str.txt cake-x64-64/candle_boot.ml .
+# Build the compiler binary
+make
 
 # Create the types.txt file necessary for candle_insulate.py
 ./cake --types < /dev/null > types.txt 2>&1
 
 # Generate candle_insulate.ml
-python candle_insulate.py types.txt candle_insulate.ml
+python ../insulate.py types.txt insulate.ml
+
+#  The working directory of the binary will be CANDLE_ROOT/candle/build,
+#  so it needs to change directory to CANDLE_ROOT after booting..
+#
+#  Q: Why do we not start the cake binary from CANDLE_ROOT?
+#  A: The cake binary looks for config_enc_str.txt and candle_boot.ml relative
+#     to the current working directoy. I find it neater if these files are not
+#     copied to CANDLE_ROOT, but stay tucked away in the build folder.
+#
+cat ../chdir_to_root.ml >> candle_boot.ml
 
 # You can now run Candle by writing:
-#   $ ./cake --candle
-# or:
-#   $ ./candle
+#   $ ./candle.sh
 # (without the $) at your prompt. Load the HOL Light sources by writing:
 #   > #use "hol.ml";;
 # (without > and with double semicolons) in the REPL.

candle.sh

@@ -0,0 +1,11 @@
+#!/bin/bash
+# Set up "strict mode" for bash
+set -euo pipefail
+
+# Change into correct directory - note that Candle must take care to change back
+# to script_dir (see build-instructions.sh for more information)
+script_dir=$(dirname -- "$(readlink -f -- "${BASH_SOURCE[0]}")")
+cd $script_dir/candle/build
+
+# Start Candle
+./cake --candle

candle/.gitignore

@@ -0,0 +1 @@
+build/

candle/basis_ffi.c.patch

@@ -0,0 +1,20 @@
+--- basis_ffi.c
++++ basis_ffi.c
+@@ -294,6 +294,13 @@
+ }
+
+ void fficustom (unsigned char *c, long clen, unsigned char *a, long alen) {
+-  assert(0 <= alen);
+-  assert(0 <= clen);
++  if (strcmp(c, "chdir") == 0) {
++    assert(1 <= alen);
++    a[0] = chdir(a) != 0;
++  } else if (strcmp(c, "getcwd") == 0) {
++    assert(1 <= alen);
++    a[0] = getcwd(a + 1, alen - 1) == NULL;
++  } else {
++    return;
++  }
+ }
+
+ // ---------------------------------------------------------------------------

candle/chdir_to_root.ml

@@ -0,0 +1,18 @@
+
+exception Sys_error of string;;
+let pp_exn e =
+  match e with
+  | Sys_error s ->
+     Pretty_printer.app_block "Sys_error" [Pretty_printer.pp_string s]
+  | _ -> pp_exn e;;
+
+let chdir dir =
+  let len = String.size dir in
+  let _ = if len = 0 then raise (Sys_error "Sys.chdir: empty input") else () in
+  let bytes = Word8_array.array (len + 1) (Word8.fromInt 0) in
+  let _ = Word8_array.copyVec dir 0 len bytes 0 in
+  let _ = Runtime.customFFI "chdir" bytes in
+  let ret = Word8.toInt (Word8_array.sub bytes 0) in
+  if ret <> 0 then raise (Sys_error "Sys.chdir: unsuccessful FFI") else ();;
+
+let _ = chdir "../..";;

candle_ocaml.ml → candle/ocaml.ml

@@ -1,5 +1,4 @@
 exception Invalid_argument of string;;
-exception Sys_error of string;;
 exception End_of_file;;
 exception Not_found;;
 

candle-regression.py → candle/regression.py

@@ -1,3 +1,21 @@
+"""
+Simple Python script to test Candle.
+
+Note that this script assumes passwordless sudo for criu, which can be
+achieved by:
+1. Calling visudo
+2. Adding
+   user ALL = (root) NOPASSWD: /usr/bin/criu
+   to it, taking care to replace user with the proper username.
+
+No claims are made on whether this a good idea in regards to security.
+
+The reason criu is used, is because DMTCP segfaulted on my machine.
+However, I suspect that that might have been due to the packaged
+version being outdated, so it is worth reconsidering, as it appears
+that DMTCP supports one checkpoint to be restored multiple times
+simulatenously, which would make parallelism during testing easier.
+"""
 import sys
 import pexpect
 import time
@@ -6,6 +24,10 @@
 import argparse
 from dataclasses import dataclass
 from enum import Enum
+from pathlib import Path
+
+# <root>/candle/candle-regression.py
+CANDLE_ROOT = Path(__file__).resolve().parent.parent
 
 # ---------------------------------------------------------------------------
 # Exceptions
@@ -61,18 +83,17 @@ class TestResult:
 # ---------------------------------------------------------------------------
 
 class CandleREPL:
-    def __init__(self, base, restore=False):
+    def __init__(self, restore=False):
         # Easier to assume that we are in the candle directory for now.
-        os.chdir(base)
+        os.chdir(CANDLE_ROOT)
 
         # Indicates whether we are a restored instance. In that case, I suspect
         # that the pid of self.process might be of sudo criu restore instead of
         # Candle.
         self._cake_pid = None
 
         self._logfile = sys.stdout
-        self._base = base
-        self._checkpoint_dir = "checkpoint"
+        self._checkpoint_dir = str(CANDLE_ROOT / "checkpoint")
         self._pidfile_name = "cake.pid"
 
         self.load_stack = []
@@ -82,7 +103,11 @@ def __init__(self, base, restore=False):
             self.restore()
         else:
             try:
-                self.process = pexpect.spawn("./candle", encoding='utf-8', logfile=self._logfile)
+                self.process = pexpect.spawn(
+                    str(CANDLE_ROOT / "candle.sh"),
+                    encoding='utf-8',
+                    logfile=self._logfile
+                )
             except Exception as e:
                 raise StartFailure from e
             try:
@@ -262,20 +287,19 @@ def print_summary(results):
 # ---------------------------------------------------------------------------
 
 class TestRunner:
-    def __init__(self, base_dir, timeout=600, fail_fast=False):
-        self.base_dir = base_dir
+    def __init__(self, timeout=600, fail_fast=False):
         self.timeout = timeout
         self.fail_fast = fail_fast
 
     def setup(self, reuse_checkpoint=False):
         """Start candle, load hol.ml, and dump a checkpoint."""
-        checkpoint_path = os.path.join(self.base_dir, "checkpoint")
+        checkpoint_path = CANDLE_ROOT / "checkpoint"
         if reuse_checkpoint and os.path.isdir(checkpoint_path):
             print("Reusing existing checkpoint.")
             return
 
         print("Starting candle and loading hol.ml...")
-        repl = CandleREPL(self.base_dir)
+        repl = CandleREPL()
         try:
             repl.load("hol.ml", timeout=3600)
             print("hol.ml loaded. Dumping checkpoint...")
@@ -290,7 +314,7 @@ def run_test(self, name):
         start = time.perf_counter()
 
         try:
-            repl = CandleREPL(self.base_dir, restore=True)
+            repl = CandleREPL(restore=True)
         except Exception as e:
             elapsed = time.perf_counter() - start
             return TestResult(
@@ -401,10 +425,6 @@ def main():
         "--timeout", type=int, default=600,
         help="Per-test timeout in seconds (default: 600)",
     )
-    parser.add_argument(
-        "--base-dir", default=os.path.dirname(os.path.abspath(__file__)),
-        help="Candle base directory (default: script directory)",
-    )
 
     args = parser.parse_args()
 
@@ -422,7 +442,6 @@ def main():
         tests = list(TESTS)
 
     runner = TestRunner(
-        base_dir=args.base_dir,
         timeout=args.timeout,
         fail_fast=args.fail_fast,
     )