Test improvements (keep temp files, eclib location)

- Do not remove temporary files after running the tests.
- Put test temporary files in deterministic locations, in a file
  hierarchy under compiler/tests/results.
- Tell easycrypt to use eclib from this repo for extraction tests.

.gitignore

@@ -35,6 +35,7 @@ Makefile.coq.conf
 /jasmin.tar.gz
 /compiler/config/checker_config_default.json
 /compiler/config/checker_config_doc.json
+/compiler/tests/results/
 
 # nix build output
 result

.gitlab-ci.yml

@@ -234,7 +234,7 @@ test-extract-to-ec:
   variables:
     EXTRA_NIX_ARGUMENTS: --arg ocamlDeps true --arg testDeps true --argstr ecRef $EASYCRYPT_REF
     WHY3_CONF: $CI_PROJECT_DIR/why3.conf
-    ECARGS: -why3 $WHY3_CONF -I Jasmin:$CI_PROJECT_DIR/eclib
+    ECARGS: -why3 $WHY3_CONF
     JSJOBS: $(NIX_BUILD_CORES)
   extends: .common
   needs:

compiler/config/tests.config

@@ -43,10 +43,12 @@ exclude = tests/fail/warning
 
 [test-x86-64-print]
 bin = ./scripts/parse-print-parse
+args = x86-64
 okdirs = tests/success/**/x86-64 tests/success/**/common
 
 [test-x86-64-extraction]
 bin = ./scripts/extract-and-check
+args = x86-64
 okdirs = examples/**/x86-64 tests/success/**/x86-64 tests/success/**/common
 exclude = tests/success/noextract
 

compiler/scripts/check-arm-m4

@@ -1,12 +1,20 @@
-#!/bin/sh
+#!/usr/bin/env bash
 
 set -e
 
-DIR=$(mktemp -d jasminXXXXXX)
+ROOT_DIR=tests/results/check-arm-m4
+TEST_FILE="${@: -1}"
+# Concatenate all args (except test file name - last arg)
+ARGS_CAT=args-$(
+	IFS=""
+	echo "${*:1:$#-1}"
+)
+DIR=$ROOT_DIR/${TEST_FILE%.jazz}/$ARGS_CAT
 ASM=${DIR}/jasmin.s
 OBJ=${DIR}/jasmin.o
 
-trap "rm -r ${DIR}" EXIT
+if [ -d "${DIR}" ]; then rm -r ${DIR}; fi
+mkdir -p $DIR
 
 set -x
 

compiler/scripts/check-x86-64

@@ -1,13 +1,21 @@
-#!/bin/sh
+#!/usr/bin/env bash
 
 set -e
 
-DIR=$(mktemp -d jasminXXXXXX)
+ROOT_DIR=tests/results/check-x86-64
+TEST_FILE=${@: -1}
+# Concatenate all args (except test file name - last arg)
+ARGS_CAT=args-$(
+	IFS=""
+	echo "${*:1:$#-1}"
+)
+DIR=$ROOT_DIR/${TEST_FILE%.jazz}/$ARGS_CAT
 ASM=${DIR}/jasmin.s
 OBJ=${DIR}/jasmin.o
 DLL=${DIR}/jasmin.so
 
-trap "rm -r ${DIR}" EXIT
+if [ -d "${DIR}" ]; then rm -r ${DIR}; fi
+mkdir -p $DIR
 
 set -x
 

compiler/scripts/extract-and-check

@@ -1,25 +1,27 @@
-#!/bin/sh
+#!/usr/bin/env bash
 
 set -e
 
-DIR=$(mktemp -d jasminXXXXXX)
+ROOT_DIR=tests/results/extraction
+DIR=$ROOT_DIR/${2%.jazz}/$1
+ECLIB=$(dirname $0)/../../eclib
 EC=${DIR}/jasmin.ec
 CT=${DIR}/jasmin_ct.ec
 
-if [ "$1" = "arm" ]
-then
-	shift
+if [ -d "${DIR}" ]; then rm -r ${DIR}; fi
+mkdir -p $DIR
+
+if [ "$1" = "arm" ]; then
 	ARCH="-arch arm-m4"
 else
 	ARCH="-arch x86-64"
 fi
 
-trap "rm -r ${DIR}" EXIT
-
 set -x
+set -o xtrace
 
-$(dirname $0)/../jasminc ${ARCH} -oecarray ${DIR} -oec ${EC} "$@"
-$(dirname $0)/../jasminc ${ARCH} -oecarray ${DIR} -CT -oec ${CT} "$@"
+$(dirname $0)/../jasminc ${ARCH} -oecarray ${DIR} -oec ${EC} "$2"
+$(dirname $0)/../jasminc ${ARCH} -oecarray ${DIR} -CT -oec ${CT} "$2"
 
-easycrypt ${ECARGS} ${EC}
-easycrypt ${ECARGS} ${CT}
+easycrypt -I Jasmin:${ECLIB} ${ECARGS} ${EC}
+easycrypt -I Jasmin:${ECLIB} ${ECARGS} ${CT}

compiler/scripts/parse-print-parse

@@ -1,15 +1,17 @@
-#!/bin/sh
+#!/usr/bin/env bash
 
 set -e
 
-DIR=$(mktemp -d jasminXXXXXX)
+ROOT_DIR=tests/results/parse-print-parse
+TEST_FILE=${@: -1}
+DIR=$ROOT_DIR/${2%.jazz}/$1
 OUT=${DIR}/jasmin.jazz
 
-trap "rm -r ${DIR}" EXIT
+if [ -d "${DIR}" ]; then rm -r ${DIR}; fi
+mkdir -p $DIR
 
 if [ "$1" = "arm" ]
 then
-    shift
     ARCH="-arch arm-m4"
 else
     ARCH="-arch x86-64"
@@ -18,8 +20,8 @@ fi
 set -x
 
 # Check that no printer crashes
-$(dirname $0)/../jasminc ${ARCH} -pall "$@" >/dev/null
+$(dirname $0)/../jasminc ${ARCH} -pall "$2" >/dev/null
 # Pretty-print the program before compilation
-$(dirname $0)/../jasminc ${ARCH} -ptyping "$@" > ${OUT}
+$(dirname $0)/../jasminc ${ARCH} -ptyping "$2" > ${OUT}
 # Try to parse it and type-check it again
 $(dirname $0)/../jasminc ${ARCH} -until_typing ${OUT}