diff --git a/.github/ci.sh b/.github/ci.sh index 64e5ebef97..581662ee60 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -54,7 +54,7 @@ install_z3() { is_exe "$BIN" "z3" && return case "$RUNNER_OS" in - Linux) file="ubuntu-18.04.zip" ;; + Linux) file="glibc-2.31.zip" ;; macOS) file="osx-10.15.7.zip" ;; Windows) file="win.zip" ;; esac diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b44b81b824..438ddf4450 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -15,7 +15,7 @@ env: # ./saw/Dockerfile # ./saw-remote-api/Dockerfile # ./s2nTests/docker/saw.dockerfile - Z3_VERSION: "4.8.10" + Z3_VERSION: "4.8.12" CVC4_VERSION: "4.1.8" YICES_VERSION: "2.6.2" @@ -165,7 +165,7 @@ jobs: path: dist/bin name: ${{ runner.os }}-bins - - if: "matrix.os == 'ubuntu-18.04'" + - if: "matrix.os == 'ubuntu-20.04'" uses: actions/upload-artifact@v2 with: name: "saw-${{ runner.os }}-${{ matrix.ghc }}" @@ -200,6 +200,7 @@ jobs: - uses: ocaml/setup-ocaml@v2 with: ocaml-compiler: 4.09.x # coq-bits claims to support < 4.10 only + opam-depext: false - run: opam repo add coq-released https://coq.inria.fr/opam/released @@ -224,11 +225,11 @@ jobs: matrix: include: - test: saw-remote-api/scripts/run_rpc_tests.sh - os: ubuntu-18.04 + os: ubuntu-20.04 - test: saw-remote-api/scripts/run_rpc_tests.sh os: macos-latest - test: saw-remote-api/scripts/check_docs.sh - os: ubuntu-18.04 + os: ubuntu-20.04 steps: - uses: actions/checkout@v2 with: @@ -276,7 +277,7 @@ jobs: fail-fast: false matrix: suite: ${{ fromJson(needs.build.outputs.cabal-test-suites-json) }} - os: [ubuntu-18.04] + os: [ubuntu-20.04] continue-on-error: [false] include: - suite: integration_tests @@ -445,7 +446,7 @@ jobs: name: "Test s2n proofs" timeout-minutes: 60 needs: build - runs-on: ubuntu-18.04 + runs-on: ubuntu-20.04 strategy: fail-fast: false matrix: @@ -458,7 +459,7 @@ jobs: - hmac-failure - awslc - blst - ghc: ["8.10.3"] + ghc: ["8.10.4"] steps: - uses: actions/checkout@v2 - run: | diff --git a/cabal.GHC-8.10.4.config b/cabal.GHC-8.10.4.config index 3b26b14a4d..30f9d310d8 100644 --- a/cabal.GHC-8.10.4.config +++ b/cabal.GHC-8.10.4.config @@ -9,18 +9,18 @@ constraints: any.Cabal ==3.2.1.0, any.IntervalMap ==0.6.1.2, any.MemoTrie ==0.6.10, MemoTrie -examples, - any.MonadRandom ==0.5.2, + any.MonadRandom ==0.5.3, any.Only ==0.1, any.QuickCheck ==2.14.2, QuickCheck -old-random +templatehaskell, - any.StateVar ==1.2.1, - abcBridge -enable-extra-tests +enable-pthreads, + any.StateVar ==1.2.2, any.abstract-deque ==0.3, abstract-deque -usecas, any.abstract-par ==0.3.3, any.adjunctions ==4.4, any.aeson ==1.5.6.0, aeson -bytestring-builder -cffi -developer -fast, + any.aeson-typescript ==0.3.0.1, any.alex ==3.2.6, alex +small_base, any.ansi-terminal ==0.11, @@ -35,7 +35,7 @@ constraints: any.Cabal ==3.2.1.0, any.assoc ==1.0.2, any.async ==2.2.3, async -bench, - any.attoparsec ==0.13.2.5, + any.attoparsec ==0.14.1, attoparsec -developer, any.auto-update ==0.1.6, any.base ==4.14.1.0, @@ -44,27 +44,25 @@ constraints: any.Cabal ==3.2.1.0, any.base-orphans ==0.8.4, any.base16-bytestring ==1.0.1.0, any.base64-bytestring ==1.2.0.1, - any.basement ==0.0.11, - any.bifunctors ==5.5.7, + any.basement ==0.0.12, + any.bifunctors ==5.5.11, bifunctors +semigroups +tagged, any.bimap ==0.4.0, any.binary ==0.8.8.0, any.binary-orphans ==1.0.1, + any.binary-parsers ==0.2.4.0, any.bitwise ==1.0.0.1, any.blaze-builder ==0.4.2.1, any.blaze-html ==0.9.1.2, any.blaze-markup ==0.8.2.8, - any.boomerang ==1.4.6, + any.boomerang ==1.4.7, any.bsb-http-chunked ==0.0.0.4, - any.bv-sized ==1.0.2, + any.bv-sized ==1.0.3, any.byteorder ==1.0.4, any.bytestring ==0.10.12.0, - any.bytestring-builder ==0.10.8.2.0, - bytestring-builder +bytestring_has_builder, - any.c2hs ==0.28.7, - c2hs +base3 -regression, + any.bytestring-lexing ==0.5.0.2, any.cabal-doctest ==1.0.8, - any.call-stack ==0.3.0, + any.call-stack ==0.4.0, any.case-insensitive ==1.2.1.0, any.cassava ==0.5.2.0, cassava -bytestring--lt-0_10_4, @@ -73,7 +71,7 @@ constraints: any.Cabal ==3.2.1.0, any.clock ==0.8.2, clock -llvm, any.code-page ==0.2.1, - any.colour ==2.3.5, + any.colour ==2.3.6, any.comonad ==5.0.8, comonad +containers +distributive +indexed-traversable, any.concurrent-output ==1.10.12, @@ -81,34 +79,34 @@ constraints: any.Cabal ==3.2.1.0, any.conduit-extra ==1.3.5, any.config-schema ==1.2.2.0, any.config-value ==0.8.1, - any.constraints ==0.12, + any.constraints ==0.13, any.containers ==0.6.2.1, - any.contravariant ==1.5.3, + any.contravariant ==1.5.5, contravariant +semigroups +statevar +tagged, any.cookie ==0.4.5, any.crackNum ==2.4, any.criterion ==1.5.9.0, criterion -embed-data-files -fast, - any.criterion-measurement ==0.1.2.0, + any.criterion-measurement ==0.1.3.0, criterion-measurement -fast, crucible +unsafe-operations, any.cryptohash-md5 ==0.11.100.1, any.cryptohash-sha1 ==0.11.100.1, cryptol +relocatable -static, - cryptol-saw-core +build-css, - any.cryptonite ==0.28, + cryptol-remote-api -static, + any.cryptonite ==0.29, cryptonite -check_alignment +integer-gmp -old_toolchain_inliner +support_aesni +support_deepseq -support_pclmuldq +support_rdrand -support_sse +use_target_attributes, any.cryptonite-conduit ==0.2.2, any.data-accessor ==0.2.3, data-accessor +category +monadfail +splitbase, any.data-binary-ieee754 ==0.4.4, any.data-default-class ==0.1.2.0, - any.data-fix ==0.3.1, + any.data-fix ==0.3.2, any.data-inttrie ==0.1.4, any.data-ref ==0.0.2, any.deepseq ==1.4.4.0, any.dense-linear-algebra ==0.1.0.0, - any.deriving-compat ==0.5.9, + any.deriving-compat ==0.5.10, deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, any.directory ==1.3.6.0, any.distributive ==0.6.2.1, @@ -123,12 +121,13 @@ constraints: any.Cabal ==3.2.1.0, any.entropy ==0.4.1.6, entropy -halvm, any.erf ==2.0.0.0, + any.errors ==2.3.0, any.exceptions ==0.10.4, any.executable-path ==0.0.3.1, any.extensible-exceptions ==0.1.1.4, any.extra ==1.7.9, any.fail ==4.9.0.0, - any.fast-logger ==3.0.3, + any.fast-logger ==3.0.5, any.fgl ==5.7.0.3, fgl +containers042, any.fgl-visualize ==0.1.0.1, @@ -136,10 +135,11 @@ constraints: any.Cabal ==3.2.1.0, any.filemanip ==0.3.6.3, any.filepath ==1.4.2.1, any.fingertree ==0.1.4.2, - any.free ==5.1.3, - any.generic-deriving ==1.13.1, + any.free ==5.1.7, + any.generic-deriving ==1.14, generic-deriving +base-4-9, - any.generic-random ==1.3.0.1, + any.generic-random ==1.5.0.0, + generic-random -enable-inspect, any.ghc ==8.10.4, any.ghc-boot ==8.10.4, any.ghc-boot-th ==8.10.4, @@ -147,17 +147,20 @@ constraints: any.Cabal ==3.2.1.0, any.ghc-paths ==0.1.0.12, any.ghc-prim ==0.6.1, any.ghci ==8.10.4, + any.githash ==0.1.6.1, any.gitrev ==1.3.1, + any.graphviz ==2999.20.1.0, + graphviz -test-parsing, any.happy ==1.20.0, - any.hashable ==1.3.1.0, - hashable +integer-gmp, + any.hashable ==1.3.2.0, + hashable +integer-gmp -random-initial-seed, any.hashtables ==1.2.4.1, hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, any.haskeline ==0.8.0.1, any.haskell-lexer ==1.1, any.haskell-src-exts ==1.23.1, any.haskell-src-meta ==0.8.7, - any.hedgehog ==1.0.4, + any.hedgehog ==1.0.5, any.heredoc ==0.2.0.0, any.hobbits ==1.4, any.hostname ==1.0, @@ -165,30 +168,29 @@ constraints: any.Cabal ==3.2.1.0, any.hpc ==0.6.1.0, any.hsc2hs ==0.68.7, hsc2hs -in-ghc-tree, - any.hspec ==2.7.8, - any.hspec-core ==2.7.8, - any.hspec-discover ==2.7.8, + any.hspec ==2.8.2, + any.hspec-core ==2.8.2, + any.hspec-discover ==2.8.2, any.hspec-expectations ==0.8.2, any.http-date ==0.0.11, any.http-types ==0.12.3, - any.http2 ==2.0.6, - http2 -devel, + any.http2 ==3.0.2, + http2 -devel -doc -h2spec, any.indexed-traversable ==0.1.1, any.integer-gmp ==1.0.3.0, any.integer-logarithms ==1.0.3.1, integer-logarithms -check-bounds +integer-gmp, any.interpolate ==0.2.1, - any.invariant ==0.5.3, - any.io-streams ==1.5.2.0, + any.invariant ==0.5.4, + any.io-streams ==1.5.2.1, io-streams +network -nointeractivetests +zlib, any.iproute ==1.7.11, any.itanium-abi ==0.1.1.1, any.js-chart ==2.9.4.1, any.json ==0.10, json +generic -mapdict +parsec +pretty +split-base, - any.kan-extensions ==5.2.2, - any.language-c ==0.8.3, - language-c -allwarnings +iecfpextension +separatesyb +usebytestrings, + any.kan-extensions ==5.2.3, + any.kvitable ==1.0.0.0, language-rust +enablequasiquotes +usebytestrings, any.lens ==4.19.2, lens -benchmark-uniplate -dump-splices +inlining -j -old-inline-pragmas -safe +test-doctests +test-hunit +test-properties +test-templates +trustworthy, @@ -196,22 +198,25 @@ constraints: any.Cabal ==3.2.1.0, libBF -system-libbf, any.libyaml ==0.1.2, libyaml -no-unicode -system-libyaml, - any.lifted-async ==0.10.1.3, + any.lifted-async ==0.10.2.1, any.lifted-base ==0.2.3.12, llvm-pretty-bc-parser -fuzz -regressions, any.logict ==0.7.0.3, - any.math-functions ==0.3.4.1, + any.lucid ==2.9.12.1, + any.lumberjack ==1.0.0.1, + any.math-functions ==0.3.4.2, math-functions +system-erf +system-expm1, + any.megaparsec ==9.0.1, megaparsec -dev, - any.memory ==0.15.0, + any.memory ==0.16.0, memory +support_basement +support_bytestring +support_deepseq +support_foundation, any.microlens ==0.4.12.0, - any.microlens-th ==0.4.3.6, + any.microlens-th ==0.4.3.10, any.microstache ==1.0.1.2, any.mmorph ==1.1.5, any.modern-uri ==0.3.4.1, modern-uri -dev, - any.monad-control ==1.0.2.3, + any.monad-control ==1.0.3, any.monad-par ==0.3.5, monad-par -chaselev -newgeneric, any.monad-par-extras ==0.3.3, @@ -221,7 +226,7 @@ constraints: any.Cabal ==3.2.1.0, any.mwc-random ==0.15.0.1, any.nats ==1.1.2, nats +binary +hashable +template-haskell, - any.network ==3.1.2.1, + any.network ==3.1.2.2, network -devel, any.network-byte-order ==0.1.6, any.network-info ==0.2.0.10, @@ -230,6 +235,8 @@ constraints: any.Cabal ==3.2.1.0, any.old-time ==1.1.0.3, any.optparse-applicative ==0.16.1.0, optparse-applicative +process, + any.optparse-simple ==0.1.1.4, + optparse-simple -build-example, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, parameterized-utils +unsafe-operations, @@ -237,6 +244,7 @@ constraints: any.Cabal ==3.2.1.0, any.parser-combinators ==1.3.0, parser-combinators -dev, any.pem ==0.2.4, + any.polyparse ==1.13, any.pretty ==1.1.3.6, any.pretty-hex ==1.1, any.pretty-show ==1.10, @@ -245,7 +253,7 @@ constraints: any.Cabal ==3.2.1.0, any.prettyprinter-ansi-terminal ==1.1.2, any.primitive ==0.7.1.0, any.process ==1.6.9.0, - any.profunctors ==5.6, + any.profunctors ==5.6.2, any.psqueues ==0.2.7.2, any.quickcheck-instances ==0.3.25.2, quickcheck-instances -bytestring-builder, @@ -256,20 +264,19 @@ constraints: any.Cabal ==3.2.1.0, reflection -slow +template-haskell, any.regex-base ==0.94.0.1, any.regex-compat ==0.95.2.1, - any.regex-posix ==0.96.0.0, + any.regex-posix ==0.96.0.1, regex-posix -_regex-posix-clib, any.resourcet ==1.2.4.2, any.rts ==1.0, + any.s-cargot ==0.1.4.0, + s-cargot -build-example, any.safe ==0.3.19, - saw-remote-api +builtin-abc, - saw-script +builtin-abc, any.sbv ==8.15, - sbv -skiphlinttester, - any.scientific ==0.3.6.2, + any.scientific ==0.3.7.0, scientific -bytestring-builder -integer-simple, any.scotty ==0.12, - any.semigroupoids ==5.3.4, - semigroupoids +comonad +containers +contravariant +distributive +doctests +tagged +unordered-containers, + any.semigroupoids ==5.3.5, + semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, any.semigroups ==0.19.1, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, any.setenv ==0.1.1.3, @@ -288,18 +295,24 @@ constraints: any.Cabal ==3.2.1.0, streaming-commons -use-bytestring-builder, any.strict ==0.4.0.1, strict +assoc, + any.string-interpolate ==0.3.1.1, + string-interpolate -bytestring-builder -extended-benchmarks -text-builder, any.syb ==0.7.2.1, any.tagged ==0.8.6.1, tagged +deepseq +transformers, any.tasty ==1.4.1, tasty +clock +unix, any.tasty-ant-xml ==1.1.8, - any.tasty-hedgehog ==1.0.1.0, - any.tasty-hspec ==1.1.6, + any.tasty-checklist ==1.0.2.0, + any.tasty-expected-failure ==0.12.3, + any.tasty-golden ==2.3.4, + tasty-golden -build-example, + any.tasty-hedgehog ==1.1.0.0, + any.tasty-hspec ==1.2, any.tasty-hunit ==0.10.0.3, any.tasty-quickcheck ==0.10.1.2, any.tasty-smallcheck ==0.8.2, - any.tasty-sugar ==1.1.0.0, + any.tasty-sugar ==1.1.1.0, any.template-haskell ==2.16.0.0, any.temporary ==1.3, any.terminal-size ==0.3.2.1, @@ -308,12 +321,13 @@ constraints: any.Cabal ==3.2.1.0, any.test-framework-hunit ==0.3.0.2, test-framework-hunit -base3 +base4, any.text ==1.2.4.1, + any.text-conversions ==0.3.1, any.text-short ==0.1.3, text-short -asserts, any.tf-random ==0.5, - any.th-abstraction ==0.3.2.0, - any.th-compat ==0.1.1, - any.th-expand-syns ==0.4.6.0, + any.th-abstraction ==0.4.2.0, + any.th-compat ==0.1.2, + any.th-expand-syns ==0.4.8.0, any.th-lift ==0.8.2, any.th-lift-instances ==0.1.18, any.th-orphans ==0.13.11, @@ -321,7 +335,7 @@ constraints: any.Cabal ==3.2.1.0, any.these ==1.1.1.1, these +assoc, any.time ==1.9.3, - any.time-compat ==1.9.5, + any.time-compat ==1.9.6, time-compat -old-locale, any.time-manager ==0.0.0, any.transformers ==0.5.6.2, @@ -337,41 +351,43 @@ constraints: any.Cabal ==3.2.1.0, any.unix-compat ==0.5.3, unix-compat -old-time, any.unix-time ==0.4.7, + any.unliftio ==0.2.19, any.unliftio-core ==0.2.0.1, - any.unordered-containers ==0.2.13.0, + any.unordered-containers ==0.2.14.0, unordered-containers -debug, any.utf8-string ==1.0.2, - any.uuid ==1.3.14, - any.uuid-types ==1.0.4, + any.uuid ==1.3.15, + any.uuid-types ==1.0.5, any.vault ==0.3.1.5, vault +useghc, - any.vector ==0.12.2.0, + any.vector ==0.12.3.0, vector +boundschecks -internalchecks -unsafechecks -wall, any.vector-algorithms ==0.8.0.4, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, - any.vector-binary-instances ==0.2.5.1, + any.vector-binary-instances ==0.2.5.2, any.vector-th-unbox ==0.2.1.9, - any.versions ==4.0.3, + any.versions ==5.0.0, any.void ==0.7.3, void -safe, any.wai ==3.2.3, any.wai-extra ==3.1.6, wai-extra -build-example, any.wai-logger ==2.3.6, - any.warp ==3.3.14, + any.warp ==3.3.17, warp +allow-sendfilefd -network-bytestring -warp-debug, any.wcwidth ==0.0.2, wcwidth -cli +split-base, any.weigh ==0.0.16, what4 -drealtestdisable -solvertests -stptestdisable, any.wl-pprint-annotated ==0.1.0.1, + any.wl-pprint-text ==1.2.0.1, any.word8 ==0.1.3, any.x509 ==1.7.5, any.xml ==1.3.14, any.yaml ==0.11.5.0, yaml +no-examples +no-exe, - any.zenc ==0.1.1, + any.zenc ==0.1.2, any.zlib ==0.6.2.3, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2021-03-11T19:34:00Z +index-state: hackage.haskell.org 2021-07-28T15:46:36Z diff --git a/cabal.GHC-8.8.4.config b/cabal.GHC-8.8.4.config index 36163692ab..1aed1c5a66 100644 --- a/cabal.GHC-8.8.4.config +++ b/cabal.GHC-8.8.4.config @@ -347,7 +347,6 @@ constraints: any.Cabal ==3.0.1.0, warp +allow-sendfilefd -network-bytestring -warp-debug, any.wcwidth ==0.0.2, wcwidth -cli +split-base, - what4 -drealtestdisable -solvertests -stptestdisable, any.xdg-basedir ==0.2.2, any.wl-pprint-annotated ==0.1.0.1, any.word8 ==0.1.3, diff --git a/s2nTests/docker/s2n.dockerfile b/s2nTests/docker/s2n.dockerfile index 82b7af20c8..bfde1cfed6 100644 --- a/s2nTests/docker/s2n.dockerfile +++ b/s2nTests/docker/s2n.dockerfile @@ -1,4 +1,4 @@ -FROM ubuntu:18.04 +FROM ubuntu:20.04 RUN apt-get update -y -q && \ apt-get install -y software-properties-common && \ @@ -25,4 +25,4 @@ RUN mkdir -p /saw-script && \ COPY scripts/s2n-entrypoint.sh /entrypoint.sh ENTRYPOINT [ "/entrypoint.sh" ] -CMD [ "/bin/bash" ] \ No newline at end of file +CMD [ "/bin/bash" ] diff --git a/saw-remote-api/Dockerfile b/saw-remote-api/Dockerfile index c71249abbd..5c2d94e917 100644 --- a/saw-remote-api/Dockerfile +++ b/saw-remote-api/Dockerfile @@ -9,8 +9,8 @@ USER user WORKDIR /solvers RUN mkdir -p rootfs/usr/local/bin -# Get Z3 4.8.10 from GitHub -RUN curl -L https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip --output z3.zip +# Get Z3 4.8.12 from GitHub +RUN curl -L https://github.com/Z3Prover/z3/releases/download/z3-4.8.12/z3-4.8.12-x64-glibc-2.31.zip --output z3.zip RUN unzip z3.zip RUN mv z3-*/bin/z3 rootfs/usr/local/bin diff --git a/saw/Dockerfile b/saw/Dockerfile index 345bd48e2b..dd4e71cf02 100644 --- a/saw/Dockerfile +++ b/saw/Dockerfile @@ -9,8 +9,8 @@ USER user WORKDIR /solvers RUN mkdir -p rootfs/usr/local/bin -# Get Z3 4.8.10 from GitHub -RUN curl -L https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip --output z3.zip +# Get Z3 4.8.12 from GitHub +RUN curl -L https://github.com/Z3Prover/z3/releases/download/z3-4.8.12/z3-4.8.12-x64-glibc-2.31.zip --output z3.zip RUN unzip z3.zip RUN mv z3-*/bin/z3 rootfs/usr/local/bin