From 295860d336fa25cf39d9e29b66c412a23e3eb542 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@inria.fr>
Date: Fri, 21 Apr 2023 06:44:06 +0200
Subject: [PATCH] CI: check EC extraction of ARM examples

---
 .gitlab-ci.yml                     |  2 +-
 compiler/config/tests.config       |  6 ++++++
 compiler/scripts/extract-and-check | 12 ++++++++++--
 3 files changed, 17 insertions(+), 3 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 17d6aabd3..6f9ccba30 100644
--- 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
index 54236e34e..2b418c9aa 100644
--- 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
index 9ad6b19c3..46b11b34c 100755
--- 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}