CI: check EC extraction of ARM examples

jasmin-lang · May 4, 2023 · 295860d · 295860d
1 parent 9642d9e
commit 295860d
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 3 deletions.
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
@@ -235,7 +235,7 @@ test-extract-to-ec:
   - ocaml
   script:
   - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'easycrypt why3config -why3 $WHY3_CONF'
-  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -C compiler CHECKCATS=x86-64-extraction check'
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -C compiler CHECKCATS="x86-64-extraction arm-m4-extraction" check'
   artifacts:
     when: always
     paths:

diff --git a/compiler/config/tests.config b/compiler/config/tests.config
@@ -47,3 +47,9 @@ kodirs = tests/fail/**/arm-m4
 bin = ./scripts/parse-print-parse
 args = arm
 okdirs = tests/success/**/arm-m4
+
+[test-arm-m4-extraction]
+bin = ./scripts/extract-and-check
+args = arm
+okdirs = examples/**/arm-m4 tests/success/**/arm-m4
+exclude = !tests/success/noextract
diff --git a/compiler/scripts/extract-and-check b/compiler/scripts/extract-and-check
@@ -6,12 +6,20 @@ DIR=$(mktemp -d jasminXXXXXX)
 EC=${DIR}/jasmin.ec
 CT=${DIR}/jasmin_ct.ec
 
+if [ "$1" = "arm" ]
+then
+	shift
+	ARCH="-arch arm-m4"
+else
+	ARCH="-arch x86-64"
+fi
+
 trap "rm -r ${DIR}" EXIT
 
 set -x
 
-$(dirname $0)/../jasminc -oecarray ${DIR} -oec ${EC} "$@"
-$(dirname $0)/../jasminc -oecarray ${DIR} -CT -oec ${CT} "$@"
+$(dirname $0)/../jasminc ${ARCH} -oecarray ${DIR} -oec ${EC} "$@"
+$(dirname $0)/../jasminc ${ARCH} -oecarray ${DIR} -CT -oec ${CT} "$@"
 
 easycrypt ${ECARGS} ${EC}
 easycrypt ${ECARGS} ${CT}