-
Notifications
You must be signed in to change notification settings - Fork 62
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Run intTests and s2n proofs in Travis CI. (#607)
* Run intTests and s2n proofs in Travis CI. Split Travis CI jobs into three stages: `build`, `test`, and `s2n test`. The `build` stage consists of two jobs, one that builds with `ghc-8.6.5`, and one that builds with `ghc-8.4.4`, and caches `dist-newstyle`. The `test` stage runs the LLVM tests in `intTests` with `ghc-8.6.5`. The `test s2n` stage runs all the `s2n` proofs with `ghc-8.6.5`. * Use `cabal new-exec` to find the path of `saw`.
- Loading branch information
1 parent
4b0019b
commit 4acafb3
Showing
1 changed file
with
127 additions
and
35 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,45 +1,137 @@ | ||
dist: trusty | ||
sudo: false | ||
|
||
language: c | ||
|
||
cache: | ||
directories: | ||
- $HOME/.ghc | ||
- $HOME/.cabal | ||
sudo: required | ||
|
||
# Normally, travis tries `git submodule update --init --recursive`, but | ||
# that fails for us right now due to some submodules from `macaw`. We | ||
# only really care about one recursive submodule, so we do the update | ||
# manually in the `script` section. | ||
git: | ||
submodules: false | ||
depth: 3 | ||
|
||
matrix: | ||
include: | ||
- env: CABALVER="2.4" GHCVER="8.6.5" | ||
compiler: ": #GHC 8.6.5" | ||
addons: {apt: {packages: [cabal-install-2.4,ghc-8.6.5], sources: [hvr-ghc]}} | ||
- env: CABALVER="2.4" GHCVER="8.4.4" | ||
compiler: ": #GHC 8.4.4" | ||
addons: {apt: {packages: [cabal-install-2.4,ghc-8.4.4], sources: [hvr-ghc]}} | ||
# - os: osx | ||
# env: CABALVER="2.4" GHCVER="8.6.5" | ||
# compiler: ": #GHC 8.6.5" | ||
|
||
before_install: | ||
# - if [[ $TRAVIS_OS_NAME == 'osx' ]]; | ||
# then | ||
# brew update; | ||
# brew install ghc; | ||
# brew install cabal-install; | ||
# fi | ||
- unset CC | ||
- export PATH=/opt/ghc/bin:$HOME/.cabal/bin:$PATH | ||
stages: | ||
- build | ||
- test | ||
- test s2n | ||
|
||
stage: build | ||
|
||
os: linux | ||
dist: xenial | ||
|
||
language: haskell | ||
cabal: 2.4 | ||
ghc: | ||
- 8.6.5 | ||
- 8.4.4 | ||
|
||
cache: | ||
directories: | ||
- $HOME/.ghc | ||
- $HOME/.cabal | ||
- dist-newstyle | ||
- bin | ||
|
||
install: | ||
- git submodule update --init | ||
- (pushd deps/abcBridge && git submodule update --init && popd) | ||
script: | ||
- git submodule init | ||
- git submodule update | ||
- (cd deps/abcBridge && git submodule init && git submodule update) | ||
- cabal v2-update | ||
- cabal v2-build -j --disable-optimization | ||
- cabal new-update | ||
# `libabc.a` is built in by `cabal configure`, not by `cabal build`. | ||
# caching `dist-newstyle` means it must be manually built each time | ||
- (pushd deps/abcBridge && scripts/build-abc.sh X86_64 Linux --init && popd) | ||
- cabal new-build -j saw jss | ||
- cp `cabal new-exec --verbose=silent -- sh -c 'which saw'` bin | ||
- cp `cabal new-exec --verbose=silent -- sh -c 'which jss'` bin | ||
|
||
jobs: | ||
include: | ||
- stage: test | ||
addons: | ||
apt: | ||
packages: | ||
- openjdk-8-jdk | ||
before_install: | ||
- sudo add-apt-repository -y ppa:sri-csl/formal-methods | ||
- sudo apt-get update -q | ||
- sudo apt-get install -y yices2 | ||
- wget -t 3 https://github.com/Z3Prover/z3/releases/download/z3-4.8.7/z3-4.8.7-x64-ubuntu-16.04.zip | ||
- unzip z3-4.8.7-x64-ubuntu-16.04.zip | ||
- cp z3-4.8.7-x64-ubuntu-16.04/bin/z3 bin | ||
script: | ||
- cd intTests | ||
- for t in test0001 test0019_jss_switch_statement test_crucible_jvm test_ecdsa test_examples test_issue108 test_tutorial1 test_tutorial2 test_tutorial_w4; do echo $t >> disabled_tests.txt; done | ||
- BIN=$TRAVIS_BUILD_DIR/bin RT_JAR=/usr/lib/jvm/java-8-openjdk-amd64/jre/lib/rt.jar LOUD=true ./runtests.sh | ||
- sh -c "! grep '<failure>' results.xml" | ||
# jobs share the cache if they have identical parameters, including | ||
# identical environmental variables. In order to share the cache with the | ||
# build job, each `s2n` test job exports environment variables manually, | ||
# instead of using the `env` key. | ||
- &s2n-test-staging | ||
stage: test s2n | ||
name: hmac md5 | ||
addons: | ||
apt: | ||
packages: | ||
- clang-3.8 | ||
- llvm-3.8 | ||
install: | ||
# - git clone https://github.com/awslabs/s2n.git | ||
- git clone https://github.com/GaloisInc/s2n.git | ||
- mkdir -p s2n/test-deps/saw/bin | ||
- cp bin/saw s2n/test-deps/saw/bin | ||
- cd s2n | ||
- git checkout bump-saw | ||
before_script: | ||
- export TESTS=sawHMAC | ||
- export SAW_HMAC_TEST=md5 | ||
script: | ||
- source .travis/s2n_setup_env.sh | ||
- SAW=true travis_retry .travis/s2n_install_test_dependencies.sh | ||
- .travis/s2n_travis_build.sh | ||
- <<: *s2n-test-staging | ||
name: hmac sha1 | ||
before_script: | ||
- export TESTS=sawHMAC | ||
- export SAW_HMAC_TEST=sha1 | ||
- <<: *s2n-test-staging | ||
name: hmac sha224 | ||
before_script: | ||
- export TESTS=sawHMAC | ||
- export SAW_HMAC_TEST=sha224 | ||
- <<: *s2n-test-staging | ||
name: hmac sha256 | ||
before_script: | ||
- export TESTS=sawHMAC | ||
- export SAW_HMAC_TEST=sha256 | ||
- <<: *s2n-test-staging | ||
name: hmac sha384 | ||
before_script: | ||
- export TESTS=sawHMAC | ||
- export SAW_HMAC_TEST=sha384 | ||
- <<: *s2n-test-staging | ||
name: hmac sha512 | ||
before_script: | ||
- export TESTS=sawHMAC | ||
- export SAW_HMAC_TEST=sha512 | ||
- <<: *s2n-test-staging | ||
name: drbg | ||
before_script: | ||
- export TESTS=sawDRBG | ||
- <<: *s2n-test-staging | ||
name: sike | ||
before_script: | ||
- export TESTS=sawSIKE | ||
- <<: *s2n-test-staging | ||
name: bike | ||
before_script: | ||
- export TESTS=sawBIKE | ||
- export S2N_LIBCRYPTO=openssl-1.0.2 | ||
- <<: *s2n-test-staging | ||
name: tls | ||
before_script: | ||
- export TESTS=tls | ||
- <<: *s2n-test-staging | ||
name: hmac failure | ||
before_script: | ||
- export TESTS=sawHMACFailure | ||
|