.gitlab-ci.yml

# This file is part of the SV-Benchmarks collection of verification tasks:
# https://github.com/sosy-lab/sv-benchmarks
#
# SPDX-FileCopyrightText: 2011-2020 The SV-Benchmarks Community
#
# SPDX-License-Identifier: Apache-2.0

stages:
  - images
  - checks

# have CI for both branches and merge requests, but no duplicates
# (i.e., do not run branch CI if there is a MR open)
# https://docs.gitlab.com/ee/ci/yaml/index.html#switch-between-branch-pipelines-and-merge-request-pipelines
workflow:
  rules:
    - if: '$CI_COMMIT_BRANCH && $CI_OPEN_MERGE_REQUESTS && $CI_PIPELINE_SOURCE == "push"'
      when: never
    - when: always

sanity-checks:
  stage: checks
  image: registry.gitlab.com/sosy-lab/benchmarking/sv-benchmarks/ci/sanity-checks:latest
  script: "c/check.py"

# for jobs that should only be executed on branches (and MRs)
.branch-rules:
  rules:
    - if: '$CI_PIPELINE_SOURCE == "merge_request_event"'
    - if: '$CI_COMMIT_BRANCH && $CI_COMMIT_BRANCH != $CI_DEFAULT_BRANCH'

# for jobs that should not be executed on branches and MRs, but for main, tags, schedules, etc.
.main-rules:
  rules:
    - if: '$CI_PIPELINE_SOURCE == "merge_request_event"'
      when: never
    - if: '$CI_COMMIT_BRANCH && $CI_COMMIT_BRANCH != $CI_DEFAULT_BRANCH'
      when: never
    - when: always

.branch-compile-check: &branch-compile-check
  stage: checks
  rules:
    - !reference [.branch-rules, rules]
  script:
    - "${CC} -v --version"
    - "cd c"
    - "./diff_ci.sh 'make -j2 -C'"

.clang-3-9: &clang-3-9
  image: registry.gitlab.com/sosy-lab/benchmarking/sv-benchmarks/ci/clang:3.9
  variables:
    CC: clang-3.9

.gcc-5: &gcc-5
  image: registry.gitlab.com/sosy-lab/benchmarking/sv-benchmarks/ci/gcc:5
  variables:
    CC: gcc-5 
    
branch-compile-clang:3.9:
  <<: *branch-compile-check
  <<: *clang-3-9

branch-compile-gcc:5:
  <<: *branch-compile-check
  <<: *gcc-5

.main-compile-check: &main-compile-check
  stage: checks
  rules:
    - !reference [.main-rules, rules]
  script:
    - "${CC} -v --version"
    - "cd c"
    - "make -j2"
    
.main-compile-check-juliet: &main-compile-check-juliet
  stage: checks
  rules:
    - !reference [.main-rules, rules]
  script:
    - "${CC} -v --version"
    - "cd c/Juliet_Test"
    - "make -j2"    

main-compile-clang:3.9:
  <<: *main-compile-check
  <<: *clang-3-9

main-compile-gcc:5:
  <<: *main-compile-check
  <<: *gcc-5    
    
main-compile-clang:3.9-juliet:
  <<: *main-compile-check-juliet
  <<: *clang-3-9

main-compile-gcc:5-juliet:
  <<: *main-compile-check-juliet
  <<: *gcc-5

branch-preprocessing-consistency:
  stage: checks
  rules:
    - !reference [.branch-rules, rules]
  image: registry.gitlab.com/sosy-lab/benchmarking/sv-benchmarks/ci/preprocessing-consistency:latest
  script:
    - "cd c"
    - "./diff_ci.sh './compare.py --keep-going --skip-large --directory'"

main-preprocessing-consistency:
  stage: checks
  rules:
    - !reference [.main-rules, rules]
  image: registry.gitlab.com/sosy-lab/benchmarking/sv-benchmarks/ci/preprocessing-consistency:latest
  script:
    - "goto-diff --version"
    - "cd c"
    - "./compare.py --keep-going --skip-large"

java:
  stage: checks
  image: registry.gitlab.com/sosy-lab/benchmarking/sv-benchmarks/ci/java:latest
  script:
    - "cd java"
    - "javac -version"
    - "./check-compile.py"

java-format:
  stage: checks
  image: openjdk:11
  script: "java/check-format.sh"
  cache:
    key: "$CI_JOB_NAME"
    paths:
      - "java/*.jar"

check-links:
    stage: checks
    image: "$CI_REGISTRY/sosy-lab/benchmarking/sv-benchmarks/ci/link-checks:latest"
    script: "FAIL=0; for md in $(find . -name '*.md'); do pandoc -t html5 \"$md\" -o \"$md\".html; echo -e \"\\n\\nFILE: $md\"; linkchecker --check-extern --config .linkchecker.config  \"$md\".html; FAIL=$((FAIL += $?)); rm \"$md\".html; done; exit $FAIL" 

.build-docker:
  image:
    name: gcr.io/kaniko-project/executor:debug
    entrypoint: [""]
  script:
    - mkdir -p /root/.docker
    - echo "{\"auths\":{\"$CI_REGISTRY\":{\"username\":\"$CI_REGISTRY_USER\",\"password\":\"$CI_REGISTRY_PASSWORD\"}}}" > /kaniko/.docker/config.json
    - /kaniko/executor --dockerfile $CI_PROJECT_DIR/$DOCKERFILE --destination $CI_REGISTRY_IMAGE/$IMAGE
  rules:
    - if: '$CI_PIPELINE_SOURCE == "schedule"'
    - if: '$CI_PIPELINE_SOURCE == "web"'

build-docker:clang:3.9:
  extends: .build-docker
  stage: images
  variables:
    DOCKERFILE: c/.Dockerfile.clang-3.9
    IMAGE: ci/clang:3.9

build-docker:gcc:5:
  extends: .build-docker
  stage: images
  variables:
    DOCKERFILE: c/.Dockerfile.gcc-5
    IMAGE: ci/gcc:5

build-docker:preprocessing-consistency:latest:
  extends: .build-docker
  stage: images
  variables:
    DOCKERFILE: c/.Dockerfile.preprocessing-consistency
    IMAGE: ci/preprocessing-consistency:latest

build-docker:sanity-checks:latest:
  extends: .build-docker
  stage: images
  variables:
    DOCKERFILE: c/.Dockerfile.sanity-checks
    IMAGE: ci/sanity-checks:latest

build-docker:java:latest:
  extends: .build-docker
  stage: images
  variables:
    DOCKERFILE: java/.Dockerfile
    IMAGE: ci/java:latest

build-docker:link-checks:latest:
  extends: .build-docker
  stage: images
  variables:
    DOCKERFILE: .Dockerfile.link-checks
    IMAGE: ci/link-checks:latest


# check license declarations etc.
reuse:
  stage: checks
  image:
    name: fsfe/reuse:latest
    entrypoint: [""]
  script:
    - reuse lint