Merge branch 'feature-annotation' into cryptoline

.editorconfig

@@ -0,0 +1,10 @@
+root=true
+
+[*]
+end_of_line = lf
+insert_final_newline = true
+charset = utf-8
+
+[*.{ml,mli}]
+indent_style = space
+indent_size = 2

.gitlab-ci.yml

@@ -0,0 +1,281 @@
+stages:
+- prepare
+- prove
+- build
+- test
+- deploy
+
+image: nixos/nix:2.18.2
+
+variables:
+  NIX_PATH: nixpkgs=channel:nixpkgs-unstable
+
+  EXTRA_SUBSTITUTERS: https://jasmin.cachix.org
+  EXTRA_PUBLIC_KEYS: jasmin.cachix.org-1:aA5r1ovq4HYKUa+8QHVvIP7K6Fi9L75b0SaN/sooWSY=
+  NIXOS_PUBLIC_KEY: cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
+  NIXPKGS_ALLOW_UNFREE: 1
+
+  VERSION: development version at commit $CI_COMMIT_SHA on branch $CI_COMMIT_REF_NAME
+
+.common:
+  before_script:
+  - >-
+    nix-shell
+    --extra-substituters "$EXTRA_SUBSTITUTERS"
+    --trusted-public-keys "$NIXOS_PUBLIC_KEY $EXTRA_PUBLIC_KEYS"
+    --arg inCI true
+    $EXTRA_NIX_ARGUMENTS
+    --run 'echo done'
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'sed -i -e "s|@VERSION@|$VERSION|" compiler/src/glob_options.ml'
+
+cache dependencies:
+  stage: prepare
+  extends: .common
+  variables:
+    EXTRA_NIX_ARGUMENTS: --arg coqDeps true --arg ocamlDeps true --arg testDeps true --argstr ecRef release --arg opamDeps true
+  environment: cachix
+  only:
+    variables:
+    - $CACHIX_SIGNING_KEY
+  script:
+  - >-
+    nix-shell -p cachix --run
+    'nix-store --query --references $(nix-instantiate --arg inCI true $EXTRA_NIX_ARGUMENTS default.nix)
+    | xargs nix-store --realise
+    | xargs nix-store --query --requisites
+    | cachix push jasmin'
+
+coq-program:
+  stage: prove
+  variables:
+    EXTRA_NIX_ARGUMENTS: --arg coqDeps true
+  extends: .common
+  script:
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C compiler CIL'
+  artifacts:
+    paths:
+    - proofs/
+    - compiler/src/CIL/
+
+coq-proof:
+  stage: prove
+  variables:
+    EXTRA_NIX_ARGUMENTS: --arg coqDeps true
+  extends: .common
+  needs:
+  - coq-program
+  script:
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C proofs'
+
+coq-master:
+  stage: prove
+  allow_failure: true
+  rules:
+    - if: $CI_COMMIT_BRANCH !~ /^release-/
+  variables:
+    EXTRA_NIX_ARGUMENTS: --arg coqDeps true --arg coqMaster true
+  extends: .common
+  script:
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C proofs'
+
+ocaml:
+  stage: build
+  variables:
+    EXTRA_NIX_ARGUMENTS: --arg ocamlDeps true
+  extends: .common
+  needs:
+  - coq-program
+  script:
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C compiler'
+  artifacts:
+    paths:
+    - compiler/_build/
+    - compiler/jasmin2tex
+    - compiler/jasminc
+    - compiler/jasmin-ct
+
+eclib:
+  stage: prove
+  parallel:
+    matrix:
+      - EASYCRYPT_REF: [release, dev]
+  variables:
+    EXTRA_NIX_ARGUMENTS: --argstr ecRef $EASYCRYPT_REF
+  extends: .common
+  script:
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'easycrypt why3config -why3 eclib/why3.conf'
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'easycrypt     config -why3 eclib/why3.conf'
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make ECARGS="-why3 why3.conf" -C eclib'
+
+opam-compiler:
+  stage: build
+  variables:
+    OPAMROOTISOK: 'true'
+    OPAMROOT: mapo
+    EXTRA_NIX_ARGUMENTS: --arg opamDeps true
+  extends: .common
+  needs:
+  - coq-program
+  cache:
+    key:
+      files:
+        - scripts/nixpkgs.nix
+      prefix: opam
+    paths:
+      - $OPAMROOT
+  script:
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'scripts/opam-setup.sh'
+  - >-
+    nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run
+    'eval $(opam env) &&
+     make -C compiler -j$NIX_BUILD_CORES &&
+     (cd compiler && mkdir -p bin && cp -L _build/install/default/bin/* bin/ && mkdir -p lib/jasmin/easycrypt && cp ../eclib/*.ec lib/jasmin/easycrypt/)'
+  artifacts:
+    paths:
+    - compiler/bin/
+    - compiler/lib/
+
+tarball:
+  stage: build
+  variables:
+    EXTRA_NIX_ARGUMENTS: --arg testDeps true
+    TARBALL: jasmin-compiler-$CI_COMMIT_SHORT_SHA
+  extends: .common
+  needs:
+  - coq-program
+  script:
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -C compiler dist DISTDIR=$TARBALL'
+  artifacts:
+    paths:
+    - compiler/$TARBALL.tgz
+
+build-from-tarball:
+  stage: test
+  variables:
+    TARBALL: jasmin-compiler-$CI_COMMIT_SHORT_SHA
+  needs:
+  - tarball
+  script:
+  - tar xvf compiler/$TARBALL.tgz
+  - nix-build -o out $TARBALL
+  - ./out/bin/jasminc -version
+
+check:
+  stage: test
+  variables:
+    EXTRA_NIX_ARGUMENTS: --arg testDeps true --arg ocamlDeps true
+  extends: .common
+  needs:
+  - coq-program
+  - ocaml
+  script:
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run './compiler/jasminc -version'
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'cd compiler && dune runtest'
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -j$NIX_BUILD_CORES -C compiler check-ci $EXTRA_MAKE_ARGUMENTS'
+
+check-proofs:
+  stage: test
+  parallel:
+    matrix:
+      - EASYCRYPT_REF: [release, dev]
+  variables:
+    EXTRA_NIX_ARGUMENTS: --arg testDeps true --argstr ecRef $EASYCRYPT_REF
+    WHY3_CONF: $CI_PROJECT_DIR/why3.conf
+    ECARGS: -why3 $WHY3_CONF -I Jasmin:$CI_PROJECT_DIR/eclib
+  extends: .common
+  needs:
+  - coq-program
+  - ocaml
+  script:
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run './compiler/jasminc -version'
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'easycrypt why3config -why3 $WHY3_CONF'
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'easycrypt     config -why3 $WHY3_CONF'
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -C compiler/examples/gimli/proofs'
+
+libjade-compile-to-asm:
+  stage: test
+  variables:
+    EXTRA_NIX_ARGUMENTS: --arg testDeps true
+  extends: .common
+  needs:
+  - coq-program
+  - ocaml
+  script:
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run './scripts/test-libjade.sh src'
+  artifacts:
+    when: always
+    paths:
+    - libjade/src/check.tar.gz
+
+libjade-extract-to-ec:
+  stage: test
+  variables:
+    EXTRA_NIX_ARGUMENTS: --arg testDeps true --argstr ecRef release
+    WHY3_CONF: $CI_PROJECT_DIR/why3.conf
+    ECARGS: -why3 $WHY3_CONF -I Jasmin:$CI_PROJECT_DIR/eclib
+    ECJOBS: '$(NIX_BUILD_CORES)'
+  extends: .common
+  needs:
+  - coq-program
+  - 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 './scripts/test-libjade.sh proof'
+  artifacts:
+    when: always
+    paths:
+    - libjade/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-program
+  - 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 arm-m4-extraction" check'
+  artifacts:
+    when: always
+    paths:
+    - compiler/report.log
+
+push-compiler-code:
+  stage: deploy
+  environment: deployment
+  only:
+    variables:
+    - $DEPLOY_KEY
+  variables:
+    TARBALL: jasmin-compiler-$CI_COMMIT_SHORT_SHA
+  needs:
+  - tarball
+  before_script:
+  - nix-env -iA nixpkgs.git
+  - nix-env -iA nixpkgs.openssh
+  - eval $(ssh-agent -s)
+  - mkdir -p ~/.ssh
+  - chmod 700 ~/.ssh
+  - ssh-keyscan gitlab.com >> ~/.ssh/known_hosts
+  - git config --global user.name "Jasmin Contributors"
+  - git config --global user.email "[email protected]"
+  script:
+  - echo "$DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null
+  - git clone [email protected]:jasmin-lang/jasmin-compiler.git _deploy
+  - cd _deploy
+  - git checkout $CI_COMMIT_REF_NAME || git checkout --orphan $CI_COMMIT_REF_NAME
+  - rm -rf compiler eclib
+  - tar xzvf ../compiler/$TARBALL.tgz
+  - mv $TARBALL/ compiler
+  - mv ../eclib .
+  - git add compiler eclib
+  - git commit -m "Jasmin compiler on branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA"  || true
+  - git push --set-upstream origin $CI_COMMIT_REF_NAME

AUTHORS

@@ -2,6 +2,7 @@ The following people have contributed code and/or ideas to Jasmin:
 
 Aaron Kaiser
 Adrien Koutsos
+Alexandre Bourbeillon
 Amber Sprenkels
 Antoine Séré
 Antoine Toussaint
@@ -14,6 +15,7 @@ Clément Sartori
 François Dupressoir
 Gaëtan Cassiers
 Gilles Barthe
+Ján Jančár
 Jean-Christophe Léchenet
 José Bacelar Almeida
 Kai-Chun Ning