CI: test EasyCrypt extraction

.gitlab-ci.yml

@@ -226,6 +226,31 @@ libjade-extract-to-ec:
     paths:
     - libjade-main/proof/check.tar.gz
 
+test-extract-to-ec:
+  stage: test
+  parallel:
+    matrix:
+      - EASYCRYPT_REF: [release, dev]
+  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
+    JSJOBS: $(NIX_BUILD_CORES)
+  extends: .common
+  needs:
+  - coq
+  - ocaml
+  dependencies:
+  - coq
+  - 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=extraction check'
+  artifacts:
+    when: always
+    paths:
+    - compiler/report.log
+
 push-compiler-code:
   stage: deploy
   environment: deployment

CHANGELOG.md

@@ -105,6 +105,13 @@
   fixes [#29](https://github.com/jasmin-lang/jasmin/issues/29),
   fixes [#150](https://github.com/jasmin-lang/jasmin/issues/150)).
 
+- Using option `-oec` without option `-ec` extracts all functions.
+
+- Extraction to EasyCrypt is now tested in continuous integration
+  ([PR #260](https://github.com/jasmin-lang/jasmin/pull/260);
+  fixes [#136](https://github.com/jasmin-lang/jasmin/issues/136),
+  fixes [#104](https://github.com/jasmin-lang/jasmin/issues/104)).
+
 # Jasmin 22.0
 
 This release is the result of more than two years of active development. It thus

compiler/config/tests.config

@@ -16,9 +16,14 @@ okdirs = !CCT/success
 kodirs = !CCT/fail
 
 [test-all]
-okdirs = examples examples/gimli tests/success tests/success/pointers tests/success/subroutines tests/success/subarrays tests/success/syscall
+okdirs = !examples !tests/success
 kodirs = tests/fail tests/fail/annotation
 
 [test-print]
 bin = ./scripts/parse-print-parse
 okdirs = tests/success
+
+[test-extraction]
+bin = ./scripts/extract-and-check
+okdirs = !examples !tests/success
+exclude = tests/success/noextract

compiler/examples/gimli/ecproof/gimli_ref.jazz

@@ -52,7 +52,7 @@ fn gimli_body(stack u32[12] state) -> stack u32[12] {
    return state;
 }
 
-export
+inline
 fn gimli(reg u64 istate) {
   stack u32[12] state;
   inline int i;

compiler/examples/gimli/ecproof/gimli_ref1.jazz

@@ -52,7 +52,7 @@ fn gimli_body(stack u32[12] state) -> stack u32[12] {
    return state;
 }
 
-export
+inline
 fn gimli(reg u64 istate) {
   stack u32[12] state;
   inline int i;

compiler/scripts/extract-and-check

@@ -0,0 +1,17 @@
+#!/bin/sh
+
+set -e
+
+DIR=$(mktemp -d jasminXXXXXX)
+EC=${DIR}/jasmin.ec
+CT=${DIR}/jasmin_ct.ec
+
+trap "rm -r ${DIR}" EXIT
+
+set -x
+
+$(dirname $0)/../jasminc.native -oecarray ${DIR} -oec ${EC} "$@"
+$(dirname $0)/../jasminc.native -oecarray ${DIR} -CT -oec ${CT} "$@"
+
+easycrypt ${ECARGS} ${EC}
+easycrypt ${ECARGS} ${CT}

compiler/src/main_compiler.ml

@@ -213,17 +213,21 @@ let main () =
 
     visit_prog_after_pass ~debug:true Compiler.ParamsExpansion prog;
 
-    if !ec_list <> [] then begin
+    if !ec_list <> [] || !ecfile <> "" then begin
       let fmt, close =
         if !ecfile = "" then Format.std_formatter, fun () -> ()
         else
           let out = open_out !ecfile in
           let fmt = Format.formatter_of_out_channel out in
           fmt, fun () -> close_out out in
+      let fnames =
+        match !ec_list with
+        | [] -> List.map (fun { f_name ; _ } -> f_name.fn_name) (snd prog)
+        | fnames -> fnames in
       begin try
         BatPervasives.finally
           (fun () -> close ())
-          (fun () -> ToEC.extract Arch.reg_size Arch.asmOp fmt !model prog !ec_list)
+          (fun () -> ToEC.extract Arch.reg_size Arch.asmOp fmt !model prog fnames)
           ()
       with e ->
         BatPervasives.ignore_exceptions