diff --git a/.github/Dockerfile-crux-llvm b/.github/Dockerfile-crux-llvm index 5a7db4044..fb952984b 100644 --- a/.github/Dockerfile-crux-llvm +++ b/.github/Dockerfile-crux-llvm @@ -17,7 +17,10 @@ ENV LANGUAGE en_US:en ENV LC_ALL en_US.UTF-8 WORKDIR /usr/local/bin -RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-22.04-bin.zip" +# The URL here is based on the same logic used to specify BUILD_TARGET_OS and +# BUILD_TARGET_ARCH in `.github/workflow/crux-llvm-build.yml`, but specialized +# to x86-64 Ubuntu. +RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20240212/ubuntu-22.04-X64-bin.zip" RUN unzip solvers.zip && rm solvers.zip && chmod +x * ENV PATH=/root/ghcup-download/bin:/root/.ghcup/bin:$PATH diff --git a/.github/Dockerfile-crux-mir b/.github/Dockerfile-crux-mir index 0a6895fce..41609cd67 100644 --- a/.github/Dockerfile-crux-mir +++ b/.github/Dockerfile-crux-mir @@ -27,7 +27,10 @@ RUN apt-get update && \ COPY --from=mir_json /usr/local/cargo /usr/local/cargo COPY --from=mir_json /usr/local/rustup /usr/local/rustup WORKDIR /usr/local/bin -RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-22.04-bin.zip" +# The URL here is based on the same logic used to specify BUILD_TARGET_OS and +# BUILD_TARGET_ARCH in `.github/workflow/crux-mir-build.yml`, but specialized +# to x86-64 Ubuntu. +RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20240212/ubuntu-22.04-X64-bin.zip" RUN unzip solvers.zip && rm solvers.zip && chmod +x * ENV CARGO_HOME=/usr/local/cargo diff --git a/.github/ci.sh b/.github/ci.sh index e732e1764..c4b620e0f 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -65,8 +65,12 @@ test() { install_llvm() { if [[ "$RUNNER_OS" = "Linux" ]]; then sudo apt-get update -q && sudo apt-get install -y clang-12 llvm-12-tools + echo "LLVM_LINK=llvm-link-12" >> "$GITHUB_ENV" + echo "LLVM_AS=llvm-as-12" >> "$GITHUB_ENV" + echo "CLANG=clang-12" >> "$GITHUB_ENV" elif [[ "$RUNNER_OS" = "macOS" ]]; then brew install llvm@12 + echo "$(brew --prefix)/opt/llvm@12/bin" >> "$GITHUB_PATH" elif [[ "$RUNNER_OS" = "Windows" ]]; then choco install llvm else @@ -76,7 +80,7 @@ install_llvm() { } install_solvers() { - (cd $BIN && curl -o bins.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/$SOLVER_PKG_VERSION/$BUILD_TARGET_OS-bin.zip" && unzip -o bins.zip && rm bins.zip) + (cd $BIN && curl -o bins.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/$SOLVER_PKG_VERSION/$BUILD_TARGET_OS-$BUILD_TARGET_ARCH-bin.zip" && unzip -o bins.zip && rm bins.zip) cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT chmod +x $BIN/* export PATH=$BIN:$PATH @@ -111,7 +115,7 @@ setup_dist() { zip_dist() { : "${VERSION?VERSION is required as an environment variable}" - pkgname="${pkgname:-"$1-$VERSION-$OS_TAG-x86_64"}" + pkgname="${pkgname:-"$1-$VERSION-$OS_TAG-$ARCH_TAG"}" mv dist "$pkgname" tar -czf "$pkgname".tar.gz "$pkgname" rm -rf dist diff --git a/.github/workflows/README.md b/.github/workflows/README.md index aa6eeb5c4..8dc09496f 100644 --- a/.github/workflows/README.md +++ b/.github/workflows/README.md @@ -5,16 +5,19 @@ on CI, whose CI configurations are located here. We use the following conventions when picking with operating systems to test: * For each project, we test the latest LTS release of Ubuntu on the three most - recent stable releases of GHC. In the case of `crux-llvm-build.yml`, we also - test some older versions of GHC. + recent stable releases of GHC. * In addition, we also test the previous LTS release of Ubuntu on the - `crux-llvm-build.yml` workflow, but only using the latest supported version - of GHC. -* For each project, we test macOS and Windows only using the latest - supported version of GHC. This is because the turnaround time for macOS and - Windows builders on GitHub Actions is longer, so we try to avoid - bottlenecking CI workflows on these operating systems. + `crux-llvm-build.yml` and `crux-mir-build.yml` workflows, but only using a + single version of GHC. +* For each project, we test macOS and Windows only using a single version of + GHC. This is because the turnaround time for macOS and Windows builders on + GitHub Actions is longer, so we try to avoid bottlenecking CI workflows on + these operating systems. - Note that we do not currently run LLVM-related tests on Windows as it is not - straightforward to obtain Windows builds of LLVM that include all of the - developer tools that we need, such as `llvm-link` and `llvm-as`. + Note that: + + * We do not currently run LLVM-related tests on Windows, as it is not + straightforward to obtain Windows builds of LLVM that include all of the + developer tools that we need, such as `llvm-link` and `llvm-as`. + * We do not currently run MIR-related tests on Windows, as it is not + straightforward to install `mir-json` on Windows. diff --git a/.github/workflows/crucible-go-build.yml b/.github/workflows/crucible-go-build.yml index 7e7263d4a..61ff0b013 100644 --- a/.github/workflows/crucible-go-build.yml +++ b/.github/workflows/crucible-go-build.yml @@ -42,7 +42,7 @@ jobs: with: submodules: true - - uses: haskell/actions/setup@v2 + - uses: haskell-actions/setup@v2 id: setup-haskell with: ghc-version: ${{ matrix.ghc }} @@ -78,8 +78,9 @@ jobs: - shell: bash run: .github/ci.sh install_system_deps env: - SOLVER_PKG_VERSION: "snapshot-20220902" + SOLVER_PKG_VERSION: "snapshot-20240212" BUILD_TARGET_OS: ${{ matrix.os }} + BUILD_TARGET_ARCH: ${{ runner.arch }} - name: Setup Environment Vars if: runner.os == 'Linux' diff --git a/.github/workflows/crucible-jvm-build.yml b/.github/workflows/crucible-jvm-build.yml index 30a2704cf..b36eafcfb 100644 --- a/.github/workflows/crucible-jvm-build.yml +++ b/.github/workflows/crucible-jvm-build.yml @@ -42,7 +42,7 @@ jobs: with: submodules: true - - uses: haskell/actions/setup@v2 + - uses: haskell-actions/setup@v2 id: setup-haskell with: ghc-version: ${{ matrix.ghc }} @@ -78,8 +78,9 @@ jobs: - shell: bash run: .github/ci.sh install_system_deps env: - SOLVER_PKG_VERSION: "snapshot-20220902" + SOLVER_PKG_VERSION: "snapshot-20240212" BUILD_TARGET_OS: ${{ matrix.os }} + BUILD_TARGET_ARCH: ${{ runner.arch }} - name: Setup Environment Vars if: runner.os == 'Linux' diff --git a/.github/workflows/crucible-wasm-build.yml b/.github/workflows/crucible-wasm-build.yml index fbcf05a21..cabf3c22d 100644 --- a/.github/workflows/crucible-wasm-build.yml +++ b/.github/workflows/crucible-wasm-build.yml @@ -42,7 +42,7 @@ jobs: with: submodules: true - - uses: haskell/actions/setup@v2 + - uses: haskell-actions/setup@v2 id: setup-haskell with: ghc-version: ${{ matrix.ghc }} @@ -78,8 +78,9 @@ jobs: - shell: bash run: .github/ci.sh install_system_deps env: - SOLVER_PKG_VERSION: "snapshot-20220902" + SOLVER_PKG_VERSION: "snapshot-20240212" BUILD_TARGET_OS: ${{ matrix.os }} + BUILD_TARGET_ARCH: ${{ runner.arch }} - name: Setup Environment Vars if: runner.os == 'Linux' diff --git a/.github/workflows/crux-llvm-build.yml b/.github/workflows/crux-llvm-build.yml index 724317f46..9d23571b5 100644 --- a/.github/workflows/crux-llvm-build.yml +++ b/.github/workflows/crux-llvm-build.yml @@ -31,7 +31,7 @@ jobs: event-tag: ${{ steps.config.outputs.tag }} event-schedule: ${{ steps.config.outputs.schedule }} publish: ${{ steps.config.outputs.publish }} - release: ${{ steps.env.outputs.release }} + release: ${{ steps.config.outputs.release }} retention-days: ${{ steps.config.outputs.retention-days }} steps: - uses: actions/checkout@v2 @@ -52,7 +52,7 @@ jobs: .github/ci.sh output tag $EVENT_TAG .github/ci.sh output schedule $EVENT_SCHEDULE .github/ci.sh output publish $({ $EVENT_TAG || $EVENT_SCHEDULE; } && echo true || echo false) - .github/ci.sh output release $([[ "refs/heads/release-$(.github/ci.sh crux_llvm_ver)" == "${{ github.event.ref }}" ]] && echo true || echo false) + .github/ci.sh output release $([[ "refs/heads/release-crux-$(.github/ci.sh crux_llvm_ver)" == "${{ github.event.ref }}" ]] && echo true || echo false) .github/ci.sh output retention-days $($RELEASE && echo 90 || echo 5) build: @@ -67,13 +67,10 @@ jobs: cabal: ["3.10.1.0"] ghc: ["9.2.8", "9.4.5", "9.6.2"] include: - - os: ubuntu-22.04 - cabal: 3.10.1.0 - ghc: 8.10.7 - os: ubuntu-20.04 cabal: 3.10.1.0 - ghc: 9.6.2 - - os: macos-12 + ghc: 9.2.8 + - os: macos-14 cabal: 3.10.1.0 ghc: 9.2.8 - os: windows-2019 @@ -85,7 +82,7 @@ jobs: with: submodules: true - - uses: haskell/actions/setup@v2 + - uses: haskell-actions/setup@v2 id: setup-haskell with: ghc-version: ${{ matrix.ghc }} @@ -121,8 +118,9 @@ jobs: - shell: bash run: .github/ci.sh install_system_deps env: - SOLVER_PKG_VERSION: "snapshot-20220902" + SOLVER_PKG_VERSION: "snapshot-20240212" BUILD_TARGET_OS: ${{ matrix.os }} + BUILD_TARGET_ARCH: ${{ runner.arch }} - name: Setup Environment Vars if: runner.os == 'Linux' @@ -186,93 +184,45 @@ jobs: run: .github/ci.sh test crucible-cli - shell: bash - name: Test crucible-symio (Linux) + name: Test crucible-symio run: cabal test pkg:crucible-symio if: runner.os == 'Linux' - shell: bash - name: Test crucible-llvm (Linux) + name: Test crucible-llvm run: .github/ci.sh test crucible-llvm - if: runner.os == 'Linux' - env: - LLVM_LINK: "llvm-link-12" - LLVM_AS: "llvm-as-12" - CLANG: "clang-12" + if: runner.os == 'Linux' || runner.os == 'macOS' - shell: bash - name: Test crucible-llvm-syntax (Linux) + name: Test crucible-llvm-syntax run: .github/ci.sh test crucible-llvm-syntax if: runner.os == 'Linux' - shell: bash - name: Test crucible-llvm-cli (Linux) + name: Test crucible-llvm-cli run: .github/ci.sh test crucible-llvm-cli if: runner.os == 'Linux' - shell: bash - name: Test crux-llvm (Linux) + name: Test crux-llvm run: .github/ci.sh test crux-llvm - if: runner.os == 'Linux' - env: - LLVM_LINK: "llvm-link-12" - CLANG: "clang-12" + if: runner.os == 'Linux' || runner.os == 'macOS' - shell: bash name: Test uc-crux-llvm (Linux) run: .github/ci.sh test uc-crux-llvm if: matrix.os == 'ubuntu-22.04' - env: - LLVM_LINK: "llvm-link-12" - CLANG: "clang-12" - - - shell: bash - name: Install LLVM-11 for MacOS - if: runner.os == 'macOS' - run: | - LLVM_TAR=https://github.com/llvm/llvm-project/releases/download/llvmorg-11.0.0/clang+llvm-11.0.0-x86_64-apple-darwin.tar.xz - curl -sSL $LLVM_TAR -o llvm.tar.xz && tar xzf llvm.tar.xz && mv clang+llvm-* llvm - echo "#!/usr/bin/env bash" > llvm/bin/clang-withIncl - echo "clang -I${{ github.workspace }}/llvm/include -I${{ github.workspace }}/llvm/include/c++/v1" >> llvm/bin/clang-withIncl - chmod +x llvm/bin/clang-withIncl - echo "$PWD/llvm/bin" >> $GITHUB_PATH - - - uses: actions/cache@v2 - name: Cache LLVM-11 - if: runner.os == 'macOS' - with: - path: ${{ github.workspace }}/llvm - key: llvm-11.0.0 - restore-keys: llvm-11.0.0 - - - shell: bash - name: Test crucible-llvm (macOS) - run: .github/ci.sh test crucible-llvm - if: runner.os == 'macOS' - env: - LLVM_LINK: "${{ github.workspace }}/llvm/bin/llvm-link" - LLVM_AS: "${{ github.workspace }}/llvm/bin/llvm-as" - CLANG: "${{ github.workspace }}/llvm/bin/clang" - - # We disable the crux-llvm test suite on macOS due to - # https://github.com/GaloisInc/crucible/issues/885 and - # https://github.com/GaloisInc/crucible/issues/999 - - shell: bash - name: Test crux-llvm (macOS) - run: .github/ci.sh test crux-llvm - if: runner.os == 'macOS' && false - env: - LLVM_LINK: "${{ github.workspace }}/llvm/bin/llvm-link" - CLANG: "${{ github.workspace }}/llvm/bin/clang-withIncl" - name: Create binary artifact shell: bash run: | - NAME="crux-llvm-${{ needs.config.outputs.crux-llvm-version }}-${{ matrix.os }}-x86_64" + NAME="crux-llvm-${{ needs.config.outputs.crux-llvm-version }}-${{ matrix.os }}-${{ runner.arch }}" echo "NAME=$NAME" >> $GITHUB_ENV .github/ci.sh bundle_crux_llvm_files if: github.repository == 'GaloisInc/crucible' env: OS_TAG: ${{ matrix.os }} + ARCH_TAG: ${{ runner.arch }} VERSION: ${{ needs.config.outputs.crux-llvm-version }} - name: Sign binary artifact @@ -369,9 +319,9 @@ jobs: docker push ${{ matrix.image }}:nightly - if: needs.config.outputs.release == 'true' - name: ${{ matrix.image }}:${{ needs.config.outputs.version }} + name: ${{ matrix.image }}:${{ needs.config.outputs.crux-llvm-version }} run: | - docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.version }} - docker push ${{ matrix.image }}:${{ needs.config.outputs.version }} + docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.crux-llvm-version }} + docker push ${{ matrix.image }}:${{ needs.config.outputs.crux-llvm-version }} docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:latest docker push ${{ matrix.image }}:latest diff --git a/.github/workflows/crux-mir-build.yml b/.github/workflows/crux-mir-build.yml index 235b1c8ab..be6d4b276 100644 --- a/.github/workflows/crux-mir-build.yml +++ b/.github/workflows/crux-mir-build.yml @@ -33,7 +33,7 @@ jobs: event-tag: ${{ steps.config.outputs.tag }} event-schedule: ${{ steps.config.outputs.schedule }} publish: ${{ steps.config.outputs.publish }} - release: ${{ steps.env.outputs.release }} + release: ${{ steps.config.outputs.release }} retention-days: ${{ steps.config.outputs.retention-days }} steps: - uses: actions/checkout@v2 @@ -54,7 +54,7 @@ jobs: .github/ci.sh output tag $EVENT_TAG .github/ci.sh output schedule $EVENT_SCHEDULE .github/ci.sh output publish $({ $EVENT_TAG || $EVENT_SCHEDULE; } && echo true || echo false) - .github/ci.sh output release $([[ "refs/heads/release-$(.github/ci.sh crux_mir_ver)" == "${{ github.event.ref }}" ]] && echo true || echo false) + .github/ci.sh output release $([[ "refs/heads/release-crux-$(.github/ci.sh crux_mir_ver)" == "${{ github.event.ref }}" ]] && echo true || echo false) .github/ci.sh output retention-days $($RELEASE && echo 90 || echo 5) build: @@ -67,7 +67,10 @@ jobs: cabal: ["3.10.1.0"] ghc: ["9.2.8", "9.4.5", "9.6.2"] include: - - os: macos-12 + - os: ubuntu-20.04 + cabal: 3.10.1.0 + ghc: 9.2.8 + - os: macos-14 cabal: 3.10.1.0 ghc: 9.2.8 @@ -78,7 +81,7 @@ jobs: with: submodules: true - - uses: haskell/actions/setup@v2 + - uses: haskell-actions/setup@v2 id: setup-haskell with: ghc-version: ${{ matrix.ghc }} @@ -121,8 +124,9 @@ jobs: - shell: bash run: .github/ci.sh install_system_deps env: - SOLVER_PKG_VERSION: "snapshot-20220902" + SOLVER_PKG_VERSION: "snapshot-20240212" BUILD_TARGET_OS: ${{ matrix.os }} + BUILD_TARGET_ARCH: ${{ runner.arch }} - name: Setup Environment Vars if: runner.os == 'Linux' @@ -174,12 +178,13 @@ jobs: - name: Create binary artifact shell: bash run: | - NAME="crux-mir-${{ needs.config.outputs.crux-mir-version }}-${{ matrix.os }}-x86_64" + NAME="crux-mir-${{ needs.config.outputs.crux-mir-version }}-${{ matrix.os }}-${{ runner.arch }}" echo "NAME=$NAME" >> $GITHUB_ENV .github/ci.sh bundle_crux_mir_files if: github.repository == 'GaloisInc/crucible' env: OS_TAG: ${{ matrix.os }} + ARCH_TAG: ${{ runner.arch }} VERSION: ${{ needs.config.outputs.crux-mir-version }} - name: Sign binary artifact @@ -196,10 +201,10 @@ jobs: .github/ci.sh sign "${NAME}.tar.gz" - uses: actions/upload-artifact@v2 - if: startsWith(github.ref, 'refs/heads/release-') + if: github.repository == 'GaloisInc/crucible' with: path: crux-mir-*.tar.gz* - name: crux-mir-${{ runner.os }}-${{ matrix.ghc }} + name: crux-mir-${{ matrix.os }}-${{ matrix.ghc }} - uses: actions/cache/save@v3 name: Save cabal store cache @@ -276,9 +281,9 @@ jobs: docker push ${{ matrix.image }}:nightly - if: needs.config.outputs.release == 'true' - name: ${{ matrix.image }}:${{ needs.config.outputs.version }} + name: ${{ matrix.image }}:${{ needs.config.outputs.crux-mir-version }} run: | - docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.version }} - docker push ${{ matrix.image }}:${{ needs.config.outputs.version }} + docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.crux-mir-version }} + docker push ${{ matrix.image }}:${{ needs.config.outputs.crux-mir-version }} docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:latest docker push ${{ matrix.image }}:latest diff --git a/cabal.GHC-8.10.7.config b/cabal.GHC-8.10.7.config deleted file mode 100644 index 68cd86be5..000000000 --- a/cabal.GHC-8.10.7.config +++ /dev/null @@ -1,289 +0,0 @@ -active-repositories: hackage.haskell.org:merge -constraints: any.BoundedChan ==1.0.3.0, - any.Cabal ==3.2.1.0, - any.Glob ==0.10.2, - any.HUnit ==1.6.2.0, - any.IntervalMap ==0.6.2.1, - any.OneTuple ==0.4.1.1, - any.QuickCheck ==2.14.3, - QuickCheck -old-random +templatehaskell, - any.SHA ==1.6.4.4, - SHA -exe, - any.StateVar ==1.2.2, - any.adjunctions ==4.4.2, - any.aeson ==2.1.2.1, - aeson -cffi +ordered-keymap, - any.alex ==3.2.7.4 || ==3.5.0.0, - any.ansi-terminal ==1.0.2, - ansi-terminal -example, - any.ansi-terminal-types ==0.11.5, - any.array ==0.5.4.0, - any.assoc ==1.1, - assoc +tagged, - any.async ==2.2.5, - async -bench, - any.atomic-primops ==0.8.4, - atomic-primops -debug, - any.attoparsec ==0.14.4, - attoparsec -developer, - any.barbies ==2.0.5.0, - any.base ==4.14.3.0, - any.base-compat ==0.13.1, - any.base-compat-batteries ==0.13.1, - any.base-orphans ==0.9.1, - any.base16-bytestring ==1.0.2.0, - any.base64-bytestring ==1.2.1.0, - any.bifunctors ==5.6.1, - bifunctors +tagged, - any.bimap ==0.5.0, - any.binary ==0.8.8.0, - any.bitvec ==1.1.5.0, - bitvec +simd, - any.bitwise ==1.0.0.1, - any.blaze-builder ==0.4.2.3, - any.boomerang ==1.4.9.1, - any.boring ==0.2.1, - boring +tagged, - any.bv-sized ==1.0.5, - any.bytestring ==0.10.12.0, - any.call-stack ==0.4.0, - any.case-insensitive ==1.2.1.0, - any.cereal ==0.5.8.3, - cereal -bytestring-builder, - any.clock ==0.8.4, - clock -llvm, - any.colour ==2.3.6, - any.comonad ==5.0.8, - comonad +containers +distributive +indexed-traversable, - any.concurrent-extra ==0.7.0.12, - any.concurrent-output ==1.10.20, - any.conduit ==1.3.5, - any.config-schema ==1.3.0.0, - any.config-value ==0.8.3, - any.constraints ==0.14, - any.containers ==0.6.5.1, - any.contravariant ==1.5.5, - contravariant +semigroups +statevar +tagged, - crucible +unsafe-operations, - any.cryptohash-sha1 ==0.11.101.0, - any.cryptohash-sha256 ==0.11.102.1, - cryptohash-sha256 -exe +use-cbits, - any.data-array-byte ==0.1.0.1, - any.data-binary-ieee754 ==0.4.4, - any.data-default-class ==0.1.2.0, - any.data-fix ==0.3.2, - any.deepseq ==1.4.4.0, - any.deriving-compat ==0.6.5, - deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, - any.directory ==1.3.6.0, - any.distributive ==0.6.2.1, - distributive +semigroups +tagged, - any.dlist ==1.0, - dlist -werror, - any.dotgen ==0.4.3, - dotgen -devel, - any.entropy ==0.4.1.10, - entropy -donotgetentropy, - any.erf ==2.0.0.0, - any.exceptions ==0.10.4, - any.extra ==1.7.14, - any.fgl ==5.8.2.0, - fgl +containers042, - any.fgl-visualize ==0.1.0.1, - any.filemanip ==0.3.6.3, - any.filepath ==1.4.2.1, - any.fingertree ==0.1.5.0, - any.foldable1-classes-compat ==0.1, - foldable1-classes-compat +tagged, - any.free ==5.2, - any.generic-lens ==2.2.2.0, - any.generic-lens-core ==2.2.1.0, - any.generic-random ==1.5.0.1, - generic-random -enable-inspect, - any.generically ==0.1.1, - any.ghc-boot-th ==8.10.7, - any.ghc-prim ==0.6.1, - any.gitrev ==1.3.1, - any.happy ==1.20.1.1, - any.hashable ==1.4.3.0, - hashable +integer-gmp -random-initial-seed, - any.hashtables ==1.3.1, - hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, - any.haskeline ==0.8.2, - any.haskell-lexer ==1.1.1, - any.haskell-src-exts ==1.23.1, - any.haskell-src-meta ==0.8.13, - any.hedgehog ==1.4, - any.hsc2hs ==0.68.10, - hsc2hs -in-ghc-tree, - any.hspec ==2.11.7, - any.hspec-api ==2.11.7, - any.hspec-core ==2.11.7, - any.hspec-discover ==2.11.7, - any.hspec-expectations ==0.8.4, - any.ieee754 ==0.8.0, - any.indexed-profunctors ==0.1.1.1, - any.indexed-traversable ==0.1.3, - any.indexed-traversable-instances ==0.1.1.2, - any.integer-gmp ==1.0.3.0, - any.integer-logarithms ==1.0.3.1, - integer-logarithms -check-bounds +integer-gmp, - any.invariant ==0.6.2, - any.io-streams ==1.5.2.2, - io-streams +network -nointeractivetests +zlib, - any.itanium-abi ==0.1.2, - any.json ==0.11, - json +generic -mapdict +parsec +pretty +split-base, - any.kan-extensions ==5.2.5, - any.kvitable ==1.0.2.1, - any.lens ==5.2.3, - lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.7, - libBF -system-libbf, - any.libyaml ==0.1.2, - libyaml -no-unicode -system-libyaml, - any.lifted-async ==0.10.2.5, - any.lifted-base ==0.2.3.12, - llvm-pretty-bc-parser -fuzz -regressions, - any.logict ==0.8.1.0, - any.lucid ==2.11.20230408, - any.lumberjack ==1.0.3.0, - any.megaparsec ==9.2.1, - megaparsec -dev, - any.microlens ==0.4.13.1, - any.microlens-th ==0.4.3.14, - any.mmorph ==1.2.0, - any.monad-control ==1.0.3.1, - any.monadLib ==3.10.1, - any.mono-traversable ==1.0.15.3, - any.mtl ==2.2.2, - any.network ==3.1.4.0, - network -devel, - any.optparse-applicative ==0.18.1.0, - optparse-applicative +process, - any.ordered-containers ==0.2.3, - any.panic ==0.4.0.1, - any.parallel ==3.2.2.0, - any.parameterized-utils ==2.1.8.0, - parameterized-utils +unsafe-operations, - any.parsec ==3.1.14.0, - any.parser-combinators ==1.3.0, - parser-combinators -dev, - any.pretty ==1.1.3.6, - any.pretty-show ==1.10, - any.prettyprinter ==1.7.1, - prettyprinter -buildreadme +text, - any.prettyprinter-ansi-terminal ==1.1.3, - any.primitive ==0.7.4.0, - any.process ==1.6.13.2, - any.profunctors ==5.6.2, - any.pvar ==1.0.0.0, - any.quickcheck-io ==0.2.0, - any.random ==1.2.1.1, - any.raw-strings-qq ==1.1, - any.reflection ==2.1.7, - reflection -slow +template-haskell, - any.regex-base ==0.94.0.2, - any.regex-compat ==0.95.2.1, - any.regex-posix ==0.96.0.1, - regex-posix -_regex-posix-clib, - any.resourcet ==1.3.0, - any.rts ==1.0.1, - any.s-cargot ==0.1.6.0, - s-cargot -build-example, - any.safe ==0.3.20, - any.safe-exceptions ==0.1.7.4, - any.scheduler ==2.0.0.1, - any.scientific ==0.3.7.0, - scientific -bytestring-builder -integer-simple, - any.semialign ==1.3, - semialign +semigroupoids, - any.semigroupoids ==6.0.0.1, - semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, - any.semigroups ==0.20, - semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, - any.simple-get-opt ==0.4, - any.smallcheck ==1.2.1.1, - any.split ==0.2.5, - any.splitmix ==0.1.0.5, - splitmix -optimised-mixer, - any.stm ==2.5.0.1, - any.streaming-commons ==0.2.2.6, - streaming-commons -use-bytestring-builder, - any.strict ==0.5, - any.string-interpolate ==0.3.2.1, - string-interpolate -bytestring-builder -extended-benchmarks -text-builder, - any.syb ==0.7.2.4, - any.tagged ==0.8.8, - tagged +deepseq +transformers, - any.tasty ==1.5, - tasty +unix, - any.tasty-checklist ==1.0.6.0, - any.tasty-expected-failure ==0.12.3, - any.tasty-golden ==2.3.5, - tasty-golden -build-example, - any.tasty-hedgehog ==1.4.0.2, - any.tasty-hspec ==1.2.0.4, - any.tasty-hunit ==0.10.1, - any.tasty-quickcheck ==0.10.3, - any.tasty-smallcheck ==0.8.2, - any.tasty-sugar ==2.2.1.0, - any.template-haskell ==2.16.0.0, - any.temporary ==1.3, - any.terminal-size ==0.3.3, - any.terminfo ==0.4.1.4, - any.text ==1.2.4.1, - any.text-conversions ==0.3.1.1, - any.text-short ==0.1.5, - text-short -asserts, - any.tf-random ==0.5, - any.th-abstraction ==0.5.0.0, - any.th-compat ==0.1.4, - any.th-expand-syns ==0.4.11.0, - any.th-lift ==0.8.4, - any.th-lift-instances ==0.1.20, - any.th-orphans ==0.13.14, - any.th-reify-many ==0.1.10, - any.these ==1.2, - any.time ==1.9.3, - any.time-compat ==1.9.6.1, - time-compat -old-locale, - any.transformers ==0.5.6.2, - any.transformers-base ==0.4.6, - transformers-base +orphaninstances, - any.transformers-compat ==0.7.2, - transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, - any.type-equality ==1, - any.typed-process ==0.2.11.1, - any.unbounded-delays ==0.1.1.1, - any.uniplate ==1.6.13, - any.unix ==2.7.2.2, - any.unix-compat ==0.7.1, - unix-compat -old-time, - any.unliftio ==0.2.25.0, - any.unliftio-core ==0.2.1.0, - any.unordered-containers ==0.2.20, - unordered-containers -debug, - any.utf8-string ==1.0.2, - any.uuid-types ==1.0.5.1, - any.vector ==0.13.1.0, - vector +boundschecks -internalchecks -unsafechecks -wall, - any.vector-algorithms ==0.9.0.1, - vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, - any.vector-stream ==0.1.0.1, - any.versions ==6.0.4, - any.void ==0.7.3, - void -safe, - any.websockets ==0.13.0.0, - websockets -example, - what4 -drealtestdisable -solvertests -stptestdisable, - any.witherable ==0.4.2, - any.wl-pprint-annotated ==0.1.0.1, - any.xml ==1.3.14, - any.yaml ==0.11.11.2, - yaml +no-examples +no-exe, - any.zenc ==0.1.2, - any.zlib ==0.6.3.0, - zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, - any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2024-01-15T23:27:26Z diff --git a/cabal.GHC-9.2.8.config b/cabal.GHC-9.2.8.config index e63dbfb3b..0908e7658 100644 --- a/cabal.GHC-9.2.8.config +++ b/cabal.GHC-9.2.8.config @@ -26,7 +26,7 @@ constraints: any.BoundedChan ==1.0.3.0, atomic-primops -debug, any.attoparsec ==0.14.4, attoparsec -developer, - any.barbies ==2.0.5.0, + any.barbies ==2.1.1.0, any.base ==4.16.4.0, any.base-compat ==0.13.1, any.base-compat-batteries ==0.13.1, @@ -179,7 +179,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.profunctors ==5.6.2, any.pvar ==1.0.0.0, any.quickcheck-io ==0.2.0, - any.random ==1.2.1.1, + any.random ==1.2.1.2, any.raw-strings-qq ==1.1, any.reflection ==2.1.7, reflection -slow +template-haskell, @@ -191,7 +191,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.rts ==1.0.2, any.s-cargot ==0.1.6.0, s-cargot -build-example, - any.safe ==0.3.20, + any.safe ==0.3.21, any.safe-exceptions ==0.1.7.4, any.scheduler ==2.0.0.1, any.scientific ==0.3.7.0, @@ -211,7 +211,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.streaming-commons ==0.2.2.6, streaming-commons -use-bytestring-builder, any.strict ==0.5, - any.string-interpolate ==0.3.2.1, + any.string-interpolate ==0.3.3.0, string-interpolate -bytestring-builder -extended-benchmarks -text-builder, any.syb ==0.7.2.4, any.tagged ==0.8.8, @@ -271,7 +271,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.vector-algorithms ==0.9.0.1, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, any.vector-stream ==0.1.0.1, - any.versions ==6.0.4, + any.versions ==6.0.5, any.void ==0.7.3, void -safe, any.websockets ==0.13.0.0, @@ -286,4 +286,4 @@ constraints: any.BoundedChan ==1.0.3.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2024-01-15T23:27:26Z +index-state: hackage.haskell.org 2024-02-05T11:57:43Z diff --git a/cabal.GHC-9.4.5.config b/cabal.GHC-9.4.5.config index 68a2e610d..cbf2fbe08 100644 --- a/cabal.GHC-9.4.5.config +++ b/cabal.GHC-9.4.5.config @@ -27,7 +27,7 @@ constraints: any.BoundedChan ==1.0.3.0, atomic-primops -debug, any.attoparsec ==0.14.4, attoparsec -developer, - any.barbies ==2.0.5.0, + any.barbies ==2.1.1.0, any.base ==4.17.1.0, any.base-compat ==0.13.1, any.base-compat-batteries ==0.13.1, @@ -179,7 +179,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.profunctors ==5.6.2, any.pvar ==1.0.0.0, any.quickcheck-io ==0.2.0, - any.random ==1.2.1.1, + any.random ==1.2.1.2, any.raw-strings-qq ==1.1, any.reflection ==2.1.7, reflection -slow +template-haskell, @@ -191,7 +191,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.rts ==1.0.2, any.s-cargot ==0.1.6.0, s-cargot -build-example, - any.safe ==0.3.20, + any.safe ==0.3.21, any.safe-exceptions ==0.1.7.4, any.scheduler ==2.0.0.1, any.scientific ==0.3.7.0, @@ -211,7 +211,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.streaming-commons ==0.2.2.6, streaming-commons -use-bytestring-builder, any.strict ==0.5, - any.string-interpolate ==0.3.2.1, + any.string-interpolate ==0.3.3.0, string-interpolate -bytestring-builder -extended-benchmarks -text-builder, any.syb ==0.7.2.4, any.tagged ==0.8.8, @@ -271,7 +271,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.vector-algorithms ==0.9.0.1, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, any.vector-stream ==0.1.0.1, - any.versions ==6.0.4, + any.versions ==6.0.5, any.void ==0.7.3, void -safe, any.websockets ==0.13.0.0, @@ -286,4 +286,4 @@ constraints: any.BoundedChan ==1.0.3.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2024-01-15T23:27:26Z +index-state: hackage.haskell.org 2024-02-05T11:57:43Z diff --git a/cabal.GHC-9.6.2.config b/cabal.GHC-9.6.2.config index b3fb185de..96a402649 100644 --- a/cabal.GHC-9.6.2.config +++ b/cabal.GHC-9.6.2.config @@ -27,7 +27,7 @@ constraints: any.BoundedChan ==1.0.3.0, atomic-primops -debug, any.attoparsec ==0.14.4, attoparsec -developer, - any.barbies ==2.0.5.0, + any.barbies ==2.1.1.0, any.base ==4.18.0.0, any.base-compat ==0.13.1, any.base-compat-batteries ==0.13.1, @@ -177,7 +177,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.profunctors ==5.6.2, any.pvar ==1.0.0.0, any.quickcheck-io ==0.2.0, - any.random ==1.2.1.1, + any.random ==1.2.1.2, any.raw-strings-qq ==1.1, any.reflection ==2.1.7, reflection -slow +template-haskell, @@ -189,7 +189,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.rts ==1.0.2, any.s-cargot ==0.1.6.0, s-cargot -build-example, - any.safe ==0.3.20, + any.safe ==0.3.21, any.safe-exceptions ==0.1.7.4, any.scheduler ==2.0.0.1, any.scientific ==0.3.7.0, @@ -209,7 +209,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.streaming-commons ==0.2.2.6, streaming-commons -use-bytestring-builder, any.strict ==0.5, - any.string-interpolate ==0.3.2.1, + any.string-interpolate ==0.3.3.0, string-interpolate -bytestring-builder -extended-benchmarks -text-builder, any.syb ==0.7.2.4, any.tagged ==0.8.8, @@ -269,7 +269,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.vector-algorithms ==0.9.0.1, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, any.vector-stream ==0.1.0.1, - any.versions ==6.0.4, + any.versions ==6.0.5, any.void ==0.7.3, void -safe, any.websockets ==0.13.0.0, @@ -284,4 +284,4 @@ constraints: any.BoundedChan ==1.0.3.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2024-01-15T23:27:26Z +index-state: hackage.haskell.org 2024-02-05T11:57:43Z diff --git a/cabal.project b/cabal.project index 0cfa9bba9..d5c65311a 100644 --- a/cabal.project +++ b/cabal.project @@ -20,7 +20,6 @@ packages: crux/ crux-llvm/ crux-mir/ - crucible-mc/ uc-crux-llvm/ optional-packages: diff --git a/crucible-cli/CHANGELOG.md b/crucible-cli/CHANGELOG.md new file mode 100644 index 000000000..362245e3b --- /dev/null +++ b/crucible-cli/CHANGELOG.md @@ -0,0 +1,3 @@ +# 0.1 -- 2024-02-05 + +* Initial version. Split off from `crucible-syntax`. diff --git a/crucible-cli/crucible-cli.cabal b/crucible-cli/crucible-cli.cabal index 3ed59bd14..ec925bb05 100644 --- a/crucible-cli/crucible-cli.cabal +++ b/crucible-cli/crucible-cli.cabal @@ -10,7 +10,7 @@ Category: Language Synopsis: A library for sharing code between Crucible CLI frontends -- Description: -extra-doc-files: README.md +extra-doc-files: CHANGELOG.md, README.md extra-source-files: test-data/**/*.cbl test-data/**/*.out.good diff --git a/crucible-concurrency/crucible-concurrency.cabal b/crucible-concurrency/crucible-concurrency.cabal index 738e82783..1f4e07031 100644 --- a/crucible-concurrency/crucible-concurrency.cabal +++ b/crucible-concurrency/crucible-concurrency.cabal @@ -3,7 +3,7 @@ cabal-version: 2.4 -- For further documentation, see http://haskell.org/cabal/users-guide/ name: crucible-concurrency -version: 0.1.0.0 +version: 0.1 -- synopsis: -- description: -- bug-reports: diff --git a/crucible-go/CHANGELOG.md b/crucible-go/CHANGELOG.md index 956a58949..95d60e2fd 100644 --- a/crucible-go/CHANGELOG.md +++ b/crucible-go/CHANGELOG.md @@ -1,3 +1,4 @@ -# next +# 0.1 -- 2024-02-05 -* TODO: Describe API changes here +* Change `SomeOverride`, as well as related functions in + `Lang.Crucible.Go.Overrides`, to use a `TypedOverride`. diff --git a/crucible-go/crucible-go.cabal b/crucible-go/crucible-go.cabal index c3080e797..60b075f72 100644 --- a/crucible-go/crucible-go.cabal +++ b/crucible-go/crucible-go.cabal @@ -1,5 +1,5 @@ name: crucible-go -version: 0.1.0.0 +version: 0.1 synopsis: A Go frontend for Crucible license: BSD3 license-file: LICENSE diff --git a/crucible-jvm/CHANGELOG.md b/crucible-jvm/CHANGELOG.md index 956a58949..b102740ad 100644 --- a/crucible-jvm/CHANGELOG.md +++ b/crucible-jvm/CHANGELOG.md @@ -1,3 +1,4 @@ -# next +# 0.2 -- 2024-02-05 -* TODO: Describe API changes here +* Change `jvmOverride_def` in `Lang.Crucible.JVM.Overrides` to use a + `TypedOverride`. diff --git a/crucible-llvm-cli/CHANGELOG.md b/crucible-llvm-cli/CHANGELOG.md new file mode 100644 index 000000000..688e82de1 --- /dev/null +++ b/crucible-llvm-cli/CHANGELOG.md @@ -0,0 +1,3 @@ +# 0.1 -- 2024-02-05 + +* Initial version. diff --git a/crucible-llvm-cli/crucible-llvm-cli.cabal b/crucible-llvm-cli/crucible-llvm-cli.cabal index 53c282bab..c10704349 100644 --- a/crucible-llvm-cli/crucible-llvm-cli.cabal +++ b/crucible-llvm-cli/crucible-llvm-cli.cabal @@ -10,7 +10,7 @@ Category: Language Synopsis: A Crucible CLI frontend for the LLVM language extension -- Description: -extra-doc-files: README.md +extra-doc-files: CHANGELOG.md, README.md extra-source-files: test-data/*.cbl test-data/*.out.good diff --git a/crucible-llvm-syntax/CHANGELOG.md b/crucible-llvm-syntax/CHANGELOG.md new file mode 100644 index 000000000..688e82de1 --- /dev/null +++ b/crucible-llvm-syntax/CHANGELOG.md @@ -0,0 +1,3 @@ +# 0.1 -- 2024-02-05 + +* Initial version. diff --git a/crucible-llvm-syntax/crucible-llvm-syntax.cabal b/crucible-llvm-syntax/crucible-llvm-syntax.cabal index 94283e72a..04d436f0a 100644 --- a/crucible-llvm-syntax/crucible-llvm-syntax.cabal +++ b/crucible-llvm-syntax/crucible-llvm-syntax.cabal @@ -10,7 +10,7 @@ Category: Language Synopsis: A syntax for reading and writing Crucible-LLVM control-flow graphs -- Description: -extra-doc-files: README.md +extra-doc-files: CHANGELOG.md, README.md extra-source-files: test-data/*.cbl test-data/*.out.good diff --git a/crucible-llvm/CHANGELOG.md b/crucible-llvm/CHANGELOG.md index 811beceb3..76d070fe7 100644 --- a/crucible-llvm/CHANGELOG.md +++ b/crucible-llvm/CHANGELOG.md @@ -1,7 +1,18 @@ -# next +# 0.6 -- 2024-02-05 * `bindLLVMFunPtr` now accepts an `Text.LLVM.AST.Symbol` rather than a whole `Declare`. Use `decName` to get a `Symbol` from a `Declare`. +* Implement overrides for the LLVM `llvm.is.fpclass.f*` intrinsics. +* Implement overrides for the `isinf`, `__isinf`, and `__isinff` C functions. +* Implement overrides for the LLVM `llvm.fma.f*` and `llvm.fmuladd.f*` + intrinsics. +* Implement overrides for the `fma` and `fmaf` C functions. +* Add a `Lang.Crucible.LLVM.MemModel.CallStack.null` function. +* Add a `ppLLVMLatest` function to `Lang.Crucible.LLVM.PrettyPrint`, which + pretty-prints an LLVM AST using the latest LLVM version that `llvm-pretty` + currently supports. Also add derived combinators (`ppDeclare`, `ppIdent`, + etc.) for calling the `llvm-pretty` functions of the same names in tandem + with `ppLLVMLatest`. # 0.5 * Add `?memOpts :: MemOptions` constraints to the following functions: diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal index 603d1325a..6b3c24b5f 100644 --- a/crucible-llvm/crucible-llvm.cabal +++ b/crucible-llvm/crucible-llvm.cabal @@ -1,9 +1,9 @@ Cabal-version: 2.2 Name: crucible-llvm -Version: 0.5 +Version: 0.6.0.99 Author: Galois Inc. Copyright: (c) Galois, Inc 2014-2022 -Maintainer: rdockins@galois.com +Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com License: BSD-3-Clause License-file: LICENSE Build-type: Simple @@ -14,6 +14,11 @@ Description: for Crucible-based simulation and verification of LLVM-compiled applications. extra-source-files: CHANGELOG.md, README.md +source-repository head + type: git + location: https://github.com/GaloisInc/crucible + subdir: crucible-llvm + common bldflags ghc-options: -Wall -Werror=incomplete-patterns @@ -21,7 +26,7 @@ common bldflags -Werror=overlapping-patterns -Wpartial-fields -Wincomplete-uni-patterns - ghc-prof-options: -O2 -fprof-auto-top + ghc-prof-options: -O2 -fprof-auto-exported default-language: Haskell2010 @@ -39,7 +44,7 @@ library extra, lens, itanium-abi >= 0.1.1.1 && < 0.2, - llvm-pretty >= 0.8 && < 0.12, + llvm-pretty >= 0.12 && < 0.13, mtl, parameterized-utils >= 2.1.5 && < 2.2, pretty, diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs index c3a83eec3..accec4ed7 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs @@ -98,6 +98,8 @@ filterTemplates ts decl = filter (f . overrideTemplateMatcher) ts f (ExactMatch x) = x == nm f (PrefixMatch pfx) = pfx `isPrefixOf` nm f (SubstringsMatch as) = filterSubstrings as nm + -- See Note [Darwin aliases] in Lang.Crucible.LLVM.Intrinsics.Common + f (DarwinAliasMatch x) = x == stripDarwinAliases nm filterSubstrings [] _ = True filterSubstrings (a:as) xs = @@ -331,6 +333,7 @@ declare_overrides = , basic_llvm_override Libc.llvmIsnanOverride , basic_llvm_override Libc.llvm__isnanOverride , basic_llvm_override Libc.llvm__isnanfOverride + , basic_llvm_override Libc.llvm__isnandOverride , basic_llvm_override Libc.llvmSqrtOverride , basic_llvm_override Libc.llvmSqrtfOverride , basic_llvm_override Libc.llvmSinOverride @@ -377,6 +380,8 @@ declare_overrides = , basic_llvm_override Libc.llvmLog2fOverride , basic_llvm_override Libc.llvmExp10Override , basic_llvm_override Libc.llvmExp10fOverride + , basic_llvm_override Libc.llvm__exp10Override + , basic_llvm_override Libc.llvm__exp10fOverride , basic_llvm_override Libc.llvmLog10Override , basic_llvm_override Libc.llvmLog10fOverride diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs index d816be917..a3bc5311e 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs @@ -25,6 +25,7 @@ module Lang.Crucible.LLVM.Intrinsics.Common , llvmSSizeT , OverrideTemplate(..) , TemplateMatcher(..) + , stripDarwinAliases , callStackFromMemVar' -- ** register_llvm_override , basic_llvm_override @@ -48,8 +49,11 @@ import Control.Lens import Control.Monad.Reader (ReaderT, ask, lift) import Control.Monad.Trans.Maybe (MaybeT) import qualified Data.List as List +import qualified Data.List.Extra as List (stripInfix) +import Data.Maybe (fromMaybe) import qualified Data.Text as Text import Numeric (readDec) +import qualified System.Info as Info import qualified ABI.Itanium as ABI import qualified Data.Parameterized.Context as Ctx @@ -119,6 +123,33 @@ data TemplateMatcher = ExactMatch String | PrefixMatch String | SubstringsMatch [String] + | DarwinAliasMatch String + -- ^ Match a name up to some number of Darwin aliases. + -- See @Note [Darwin aliases]@. + +-- | Remove all prefixes and suffixes that might occur in a Darwin alias for +-- a function name. See @Note [Darwin aliases]@. +stripDarwinAliases :: String -> String +stripDarwinAliases str = + -- Remove the \01_ prefix, if it exists... + let strNoPrefix = fromMaybe str (List.stripPrefix "\01_" str) in + -- ...and remove any suffixes as well. Because there can be multiple suffixes + -- in an alias, we use `stripInfix` in case one of the prefixes does not + -- appear at the very end of the name. + foldr (\suf s -> + case List.stripInfix suf s of + Just (before, after) -> before ++ after + Nothing -> s) + strNoPrefix + suffixes + where + suffixes :: [String] + suffixes = [ "$UNIX2003" + , "$INODE64" + , "$1050" + , "$NOCANCEL" + , "$DARWIN_EXTSN" + ] type RegOverrideM p sym arch rtp l a = ReaderT (L.Declare, Maybe ABI.DecodedName, LLVMContext arch) @@ -129,6 +160,40 @@ callStackFromMemVar' :: OverrideSim p sym ext r args ret CallStack callStackFromMemVar' mvar = use (to (flip callStackFromMemVar mvar)) +{- +Note [Darwin aliases] +~~~~~~~~~~~~~~~~~~~~~ +Operating systems derived from Darwin, such as macOS, define several aliases +for common libc functions for versioning purposes. These aliases are defined +using __asm, so when Clang compiles these aliases, the name that appears in the +resulting bitcode will look slightly different from what appears in the source +C file. For example, compiling the write() function with Clang on macOS will +produce LLVM bitcode with the name \01_write(), where \01 represents a leading +ASCII character with code 0x01. + +Aside from the \01_ prefix, there also a number of suffixes that can be used +in alias names (see `stripDarwinAliases` for the complete list). There are +enough possible combinations that it is not wise to try and write them all out +by hand. Instead, we take the approach that when using crucible-llvm on Darwin, +we treat any C function as possibly containing Darwin aliases. That is: + +* In `basic_llvm_override`, we use a special DarwinAliasMatch template matcher + on Darwin. When matching against possible overrides, DarwinAliasMatch + indicates that function should be match the underlying name after removing + any possible Darwin-related prefixes or suffixes (see the + `stripDarwinAliases` function, which implements this). +* If a function name in a program matches an override name after stripping + Darwin aliases, then we proceed to use the override, but with the override's + name switched out for the name of the function from the program. This way, + we write overrides for the "normalized" name (e.g., write) but have them work + seamlessly for aliases names (e.g., \01_write) as well. + +Currently, we only apply this special treatment in `basic_llvm_override`, as +we have only observed the aliases being used on libc functions. We may need to +apply this special case to other override functions (e.g., +`register_cpp_override`) if that proves insufficient. +-} + ------------------------------------------------------------------------ -- ** register_llvm_override @@ -250,9 +315,32 @@ basic_llvm_override :: forall p args ret sym arch wptr l a rtp. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a -basic_llvm_override ovr = OverrideTemplate (ExactMatch nm) (register_llvm_override ovr) - where L.Symbol nm = L.decName (llvmOverride_declare ovr) - +basic_llvm_override ovr = OverrideTemplate matcher regOvr + where + ovrDecl = llvmOverride_declare ovr + L.Symbol ovrNm = L.decName ovrDecl + isDarwin = Info.os == "darwin" + + matcher :: TemplateMatcher + matcher | isDarwin = DarwinAliasMatch ovrNm + | otherwise = ExactMatch ovrNm + + regOvr :: RegOverrideM p sym arch rtp l a () + regOvr = do + (requestedDecl, _ ,_) <- ask + let L.Symbol requestedNm = L.decName requestedDecl + -- If we are on Darwin and the function name contains Darwin-specific + -- prefixes or suffixes, change the name of the override to the name + -- containing prefixes/suffixes. See Note [Darwin aliases] for an + -- explanation of why we do this. + let ovr' | isDarwin + , ovrNm == stripDarwinAliases requestedNm + = ovr { llvmOverride_declare = + ovrDecl { L.decName = L.Symbol requestedNm }} + + | otherwise + = ovr + register_llvm_override ovr' -- | Check that the requested declaration matches the provided declaration. In -- this context, \"matching\" means that both declarations have identical names, diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs index 7c632091d..b93ba7421 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs @@ -508,8 +508,7 @@ callStrlen bak mvar (regValue -> strPtr) = do callAssert :: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) - => Bool -- ^ 'True' if this is @__assert_fail()@, 'False' otherwise. - -> GlobalVar Mem + => GlobalVar Mem -> bak -> Ctx.Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr @@ -518,7 +517,7 @@ callAssert ::> LLVMPointerType wptr) -> forall r args reg. OverrideSim p sym ext r args reg (RegValue sym UnitType) -callAssert assert_fail mvar bak (Empty :> _pfn :> _pfile :> _pline :> ptxt ) = +callAssert mvar bak (Empty :> _pfn :> _pfile :> _pline :> ptxt ) = do let sym = backendGetSym bak when failUponExit $ do mem <- readGlobal mvar @@ -531,10 +530,7 @@ callAssert assert_fail mvar bak (Empty :> _pfn :> _pfile :> _pline :> ptxt ) = where failUponExit :: Bool failUponExit - | assert_fail = abnormalExitBehavior ?intrinsicsOpts `elem` [AlwaysFail, OnlyAssertFail] - | otherwise - = abnormalExitBehavior ?intrinsicsOpts == AlwaysFail callExit :: ( IsSymBackend sym bak , ?intrinsicsOpts :: IntrinsicsOptions ) @@ -837,6 +833,15 @@ llvm__isnanfOverride = [llvmOvr| i32 @__isnanf( float ) |] (\_memOps sym args -> Ctx.uncurryAssignment (callIsnan sym (knownNat @32)) args) +-- macOS compiles isnan() to __isnand() when the argument is a double. +llvm__isnandOverride :: + IsSymInterface sym => + LLVMOverride p sym + (EmptyCtx ::> FloatType DoubleFloat) + (BVType 32) +llvm__isnandOverride = + [llvmOvr| i32 @__isnand( double ) |] + (\_memOps sym args -> Ctx.uncurryAssignment (callIsnan sym (knownNat @32)) args) llvmSqrtOverride :: IsSymInterface sym => @@ -1410,6 +1415,26 @@ llvmExp10fOverride = [llvmOvr| float @exp10f( float ) |] (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp10) args) +-- macOS uses __exp10(f) instead of exp10(f). + +llvm__exp10Override :: + IsSymInterface sym => + LLVMOverride p sym + (EmptyCtx ::> FloatType DoubleFloat) + (FloatType DoubleFloat) +llvm__exp10Override = + [llvmOvr| double @__exp10( double ) |] + (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp10) args) + +llvm__exp10fOverride :: + IsSymInterface sym => + LLVMOverride p sym + (EmptyCtx ::> FloatType SingleFloat) + (FloatType SingleFloat) +llvm__exp10fOverride = + [llvmOvr| float @__exp10f( float ) |] + (\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp10) args) + -- log10(f) llvmLog10Override :: @@ -1445,7 +1470,7 @@ llvmAssertRtnOverride UnitType llvmAssertRtnOverride = [llvmOvr| void @__assert_rtn( i8*, i8*, i32, i8* ) |] - (callAssert False) + callAssert -- From glibc llvmAssertFailOverride @@ -1459,7 +1484,7 @@ llvmAssertFailOverride UnitType llvmAssertFailOverride = [llvmOvr| void @__assert_fail( i8*, i8*, i32, i8* ) |] - (callAssert True) + callAssert llvmAbortOverride diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Options.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Options.hs index b6e577a6a..042544db2 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Options.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Options.hs @@ -20,9 +20,9 @@ data AbnormalExitBehavior -- ^ Functions which trigger an abnormal exit will always cause Crucible -- to fail. | OnlyAssertFail - -- ^ The @__assert_fail()@ function will cause Crucible to fail, while - -- other functions which triggern an abnormal exit will not cause - -- failures. This option is primarily useful for SV-COMP. + -- ^ The @__assert_fail()@ or @__assert_rtn()@ functions will cause Crucible + -- to fail, while other functions which trigger an abnormal exit will not + -- cause failures. This option is primarily useful for SV-COMP. | NeverFail -- ^ Functions which trigger an abnormal exit will never cause Crucible -- to fail. This option is primarily useful for SV-COMP. diff --git a/crucible-mc/CHANGELOG.md b/crucible-mc/CHANGELOG.md deleted file mode 100644 index 21bb76539..000000000 --- a/crucible-mc/CHANGELOG.md +++ /dev/null @@ -1,5 +0,0 @@ -# Revision history for crucible-mc - -## 0.1.0.0 -- YYYY-mm-dd - -* First version. Released on an unsuspecting world. diff --git a/crucible-mc/LICENSE b/crucible-mc/LICENSE deleted file mode 100644 index 56e18d41f..000000000 --- a/crucible-mc/LICENSE +++ /dev/null @@ -1,13 +0,0 @@ -Copyright (c) 2019-2022 Iavor Diatchki - -Permission to use, copy, modify, and/or distribute this software for any purpose -with or without fee is hereby granted, provided that the above copyright notice -and this permission notice appear in all copies. - -THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH -REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY AND -FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, -INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS -OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER -TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF -THIS SOFTWARE. diff --git a/crucible-mc/README b/crucible-mc/README deleted file mode 100644 index bca00c54e..000000000 --- a/crucible-mc/README +++ /dev/null @@ -1,2 +0,0 @@ -This package is for experimenting with adding model-checking -support to Crucible. diff --git a/crucible-mc/Setup.hs b/crucible-mc/Setup.hs deleted file mode 100644 index 9a994af67..000000000 --- a/crucible-mc/Setup.hs +++ /dev/null @@ -1,2 +0,0 @@ -import Distribution.Simple -main = defaultMain diff --git a/crucible-mc/crucible-mc.cabal b/crucible-mc/crucible-mc.cabal deleted file mode 100644 index 6cdf2c414..000000000 --- a/crucible-mc/crucible-mc.cabal +++ /dev/null @@ -1,33 +0,0 @@ -cabal-version: 2.2 -name: crucible-mc -version: 0.1.0.0 --- synopsis: --- description: --- bug-reports: -license: ISC -license-file: LICENSE -author: Iavor Diatchki -maintainer: iavor.diatchki@gmail.com --- copyright: --- category: -extra-source-files: CHANGELOG.md - -executable crucible-mc - main-is: Main.hs - other-modules: Print - build-depends: - base >= 4.11.0 && < 5.0 , - containers, - lens, - parameterized-utils, - crucible, - llvm-pretty, - llvm-pretty-bc-parser, - crucible-llvm, - crux, - crux-llvm, - what4, - pretty - hs-source-dirs: exe - default-language: Haskell2010 - ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns diff --git a/crucible-mc/exe/Main.hs b/crucible-mc/exe/Main.hs deleted file mode 100644 index 8c5f8e32f..000000000 --- a/crucible-mc/exe/Main.hs +++ /dev/null @@ -1,96 +0,0 @@ -{-# Language RankNTypes, TypeApplications, TypeFamilies #-} -{-# Language ImplicitParams #-} -{-# Language PatternSynonyms #-} -module Main(main) where - -import System.IO(stdout) -import Control.Exception(throwIO,Exception(..)) - -import Data.Parameterized.Nonce(withIONonceGenerator) -import Data.Parameterized.Context (pattern Empty) - -import qualified Data.LLVM.BitCode as BC - -import Lang.Crucible.Types(TypeRepr(..)) -import Lang.Crucible.Backend.Online - ( Z3OnlineBackend, withZ3OnlineBackend, UnsatFeatures(..) - , Flags, FloatIEEE, FloatModeRepr(..) - ) -import Lang.Crucible.Backend(IsSymInterface) -import Lang.Crucible.CFG.Core(AnyCFG(..),cfgArgTypes,cfgReturnType) -import Lang.Crucible.Simulator -import What4.ProblemFeatures ( noFeatures ) - -import Lang.Crucible.LLVM.MemModel(defaultMemOptions) -import Lang.Crucible.LLVM.Run - -import Crux.LLVM.Simulate( registerFunctions ) -import Crux.Model - -import Print - -test_file :: FilePath -test_file = "crucible-mc/test/example.bc" - -test_fun :: String -test_fun = "f" - -main :: IO () -main = - parseLLVM test_file >>= \llvm_mod -> - withZ3 $ \sym -> - runCruxLLVM llvm_mod defaultMemOptions False False $ - CruxLLVM $ \mt -> - withPtrWidthOf mt $ - case findCFG mt test_fun of - Nothing -> throwIO (UnknownFunction test_fun) - Just (AnyCFG cfg) -> - case (cfgArgTypes cfg, cfgReturnType cfg) of - (Empty, UnitRepr) -> - let ?recordLLVMAnnotation = \_ _ _ -> pure () in - pure Setup - { cruxOutput = stdout - , cruxBackend = sym - , cruxInitCodeReturns = UnitRepr - , cruxInitCode = do registerFunctions llvm_mod mt - _ <- callCFG cfg emptyRegMap - pure () - , cruxUserState = emptyModel - , cruxGo = runFrom - } - - _ -> throwIO (UnsupportedFunType test_fun) - -runFrom :: (IsSymInterface sym, HasPtrWidth (ArchWidth arch)) => - ExecState p sym (LLVM arch) rtp -> IO () -runFrom st = - do print (ppExecState st) - _ <- getLine - st1 <- singleStepCrucible 5 st - runFrom st1 - - --- | Create a Z3 backend for the simulator. -withZ3 :: (forall s. Z3OnlineBackend s (Flags FloatIEEE) -> IO a) -> IO a -withZ3 k = - withIONonceGenerator $ \nonceGen -> - withZ3OnlineBackend FloatIEEERepr nonceGen ProduceUnsatCores noFeatures k - - --- | This exception is thrown when we fail to parse a bit-code file. -data Err = BitcodeError BC.Error - | UnknownFunction String - | UnsupportedFunType String - deriving Show - -instance Exception Err - --- | Parse an LLVM bit-code file. -parseLLVM :: FilePath -> IO Module -parseLLVM file = - do ok <- BC.parseBitCodeFromFile file - case ok of - Left err -> throwIO (BitcodeError err) - Right m -> pure m - - diff --git a/crucible-mc/exe/Print.hs b/crucible-mc/exe/Print.hs deleted file mode 100644 index 307c81d00..000000000 --- a/crucible-mc/exe/Print.hs +++ /dev/null @@ -1,28 +0,0 @@ -{-# Language GADTs #-} -{-# Language OverloadedStrings #-} -module Print where - -import Text.PrettyPrint -import Lang.Crucible.Simulator.ExecutionTree - - -ppExecState :: ExecState p sym ext rtp -> Doc -ppExecState st = - case st of - ResultState {} -> "ResultState" - AbortState {} -> "AbortState" - UnwindCallState {} -> "UnwindCallState" - CallState {} -> "CallState" - TailCallState {} -> "TailCallState" - ReturnState {} -> "ReturnState" - RunningState {} -> "RunningState" - SymbolicBranchState {} -> "SymbolicBranchState" - ControlTransferState {} -> "ControlTransferState" - OverrideState {} -> "OverrideState" - BranchMergeState t _st -> "BranchMergeState" <+> text (ppBranchTarget t) - InitialState {} -> "InitialState" - - - - - diff --git a/crucible-mc/test/Makefile b/crucible-mc/test/Makefile deleted file mode 100644 index 7906e525b..000000000 --- a/crucible-mc/test/Makefile +++ /dev/null @@ -1,12 +0,0 @@ -CLANG=clang -CFLAGS=-O1 -Wall - -.PHONY: all clean - -all: example.bc - -clean: - -rm *.bc *.ll - -%.bc: %.c - $(CLANG) $(CFLAGS) -emit-llvm -o $@ -c $< diff --git a/crucible-mc/test/example.c b/crucible-mc/test/example.c deleted file mode 100644 index 20f80b0d5..000000000 --- a/crucible-mc/test/example.c +++ /dev/null @@ -1,7 +0,0 @@ -#include -void __VERIFIER_assert(uint32_t b); - -void f () { - __VERIFIER_assert(0); -} - diff --git a/crucible-mir/CHANGELOG.md b/crucible-mir/CHANGELOG.md index 59762abdc..0e5085815 100644 --- a/crucible-mir/CHANGELOG.md +++ b/crucible-mir/CHANGELOG.md @@ -1,3 +1,40 @@ +# 0.2 -- 2024-02-05 + +* `crucible-mir` now supports the `nightly-2023-01-23` Rust toolchain. Some of + the highlights of this include: + + * Properly support for Rust's new constant forms + * Better support for zero-sized constants + * Encoding enum discriminant types so that `crucible-mir` can know about + non-`isize` discriminant types (e.g., `Ordering`, which uses an `i8` + discriminant) + * A more intelligent way of computing crate disambiguators for looking up + known types such as `MaybeUninit` and `Option` +* Functions in `Mir.Intrinsics` now avoid taking or returning `SimState` values + as arguments, instead preferring `SymGlobalState` and `IntrinsicTypes`. This + makes it possible to call into the `crucible-mir` memory model from SAW + without needing a full-blown `SimState`, which isn't readily at hand in the + parts of SAW that need the memory model. +* There are now variants of the memory model–related functions in + `Mir.Intrinsics` whose names are suffixed with `*IO`. These functions live in + `IO` instead of `MuxLeafT sym IO`, which make them easier to call from `IO` + contexts. +* Support enums marked with `repr(transparent)`. +* Fix a bug in which the custom overrides for `rotate_left` and related + intrinsics were not applied. + # 0.1 -* TODO: Describe API changes here +* Much of the `crux-mir` library has been split off into a `crucible-mir` + library, which removes all of the `crux`-specific code. The following modules + were _not_ migrated to `crucible-mir`: + + * `Mir.Generate` + * `Mir.Language` + * `Mir.Log` + * `Mir.Concurrency` + * `Mir.Overrides` + + Note that `Mir.Generate` now only exports the `generateMIR` function. The + `parseMIR` and `translateMIR` functions have been moved to a new + `Mir.ParseTranslate` module in `crucible-mir`. diff --git a/crucible-mir/crucible-mir.cabal b/crucible-mir/crucible-mir.cabal index c5846ce1d..ab459807f 100644 --- a/crucible-mir/crucible-mir.cabal +++ b/crucible-mir/crucible-mir.cabal @@ -1,5 +1,5 @@ name: crucible-mir -version: 0.1 +version: 0.2 -- synopsis: -- description: homepage: https://github.com/GaloisInc/crucible/blob/master/crucible-mir/README.md diff --git a/crucible-symio/CHANGELOG.md b/crucible-symio/CHANGELOG.md index cff4521b6..5c1073d8e 100644 --- a/crucible-symio/CHANGELOG.md +++ b/crucible-symio/CHANGELOG.md @@ -1,5 +1,5 @@ # Revision history for crucible-symio -## 0.1.0.0 -- YYYY-mm-dd +## 0.1 -- 2024-02-05 * First version. Released on an unsuspecting world. diff --git a/crucible-symio/crucible-symio.cabal b/crucible-symio/crucible-symio.cabal index e992d521c..12602db01 100644 --- a/crucible-symio/crucible-symio.cabal +++ b/crucible-symio/crucible-symio.cabal @@ -6,13 +6,20 @@ description: reading and writing symbolic data. An example use case would be to support verifying programs that e.g., use configuration files or accept input from files. name: crucible-symio -version: 0.1.0.0 +version: 0.1.0.99 +license: BSD-3-Clause license-file: LICENSE author: Daniel Matichuk -maintainer: dmatichuk@galois.com +maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com build-type: Simple +category: Language extra-source-files: CHANGELOG.md +source-repository head + type: git + location: https://github.com/GaloisInc/crucible + subdir: crucible-symio + common shared build-depends: base >=4.12 && <4.19, aeson, diff --git a/crucible-syntax/CHANGELOG.md b/crucible-syntax/CHANGELOG.md index 0c4925904..4ce9021cc 100644 --- a/crucible-syntax/CHANGELOG.md +++ b/crucible-syntax/CHANGELOG.md @@ -1,9 +1,19 @@ -# next +# 0.4 -- 2024-02-05 * The type `ACFG` has been removed in favor of `Lang.Crucible.CFG.Reg.AnyCFG`, which serves a similar purpose (hiding the argument and return types). The CFG argument and return types can be recovered via `Lang.Crucible.CFG.Reg.{cfgArgTypes,cfgReturnType}`. +* `crucible-syntax` now supports simulating CFGs with language-specific syntax + extensions: + + * `SimulateProgramHooks` now has a `setupHook` field that can run an arbitrary + override action before simulation. (For example, this is used in + `crucible-llvm-syntax` to initialize the LLVM memory global variable.) + * `SimulateProgramHooks` now has an extra `ext` type variable so that hooks + can be extension-specific. +* `execCommand` and related data types in `Lang.Crucible.Syntax.Prog` have been + split off into a separate `crucible-cli` library. # 0.3 diff --git a/crucible-syntax/crucible-syntax.cabal b/crucible-syntax/crucible-syntax.cabal index 2839dba14..3f6c14cad 100644 --- a/crucible-syntax/crucible-syntax.cabal +++ b/crucible-syntax/crucible-syntax.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: crucible-syntax -Version: 0.3 +Version: 0.4 Author: Galois Inc. Maintainer: dtc@galois.com Build-type: Simple diff --git a/crucible/CHANGELOG.md b/crucible/CHANGELOG.md index b9c6e08f4..8a502f7ef 100644 --- a/crucible/CHANGELOG.md +++ b/crucible/CHANGELOG.md @@ -1,3 +1,17 @@ +# next -- TBA + +* Rename `Lang.Crucible.Backend.popFrame` to `popFrameOrPanic`, + provide helpers such as `popFrame` to manage assumptions without `panic`ing. + +# 0.7 -- 2024-02-05 + +* Add `TypedOverride`, `SomeTypedOverride`, and `runTypedOverride` to + `Lang.Crucible.Simulator.OverrideSim`. These allow one to define an + `OverrideSim` action and bundle `TypeRepr`s for its argument and result + types, which is a common pattern in several Crucible backends. +* Add `Lang.Crucible.Simulator.OverrideSim.bindCFG`, a utility function for + binding a CFG to its handle in an `OverrideSim`. + # 0.6 * Separate backend data structures. The "symbolic backend" is a diff --git a/crucible/crucible.cabal b/crucible/crucible.cabal index 8e0201d24..d1f853645 100644 --- a/crucible/crucible.cabal +++ b/crucible/crucible.cabal @@ -1,8 +1,8 @@ Cabal-version: 2.2 Name: crucible -Version: 0.6 +Version: 0.7.0.99 Author: Galois Inc. -Maintainer: jhendrix@galois.com, rdockins@galois.com +Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com Copyright: (c) Galois, Inc 2014-2022 License: BSD-3-Clause License-file: LICENSE @@ -16,6 +16,11 @@ Description: a variety of SAT and SMT solvers, including Z3, CVC4, Yices, STP, and dReal. extra-source-files: CHANGELOG.md +source-repository head + type: git + location: https://github.com/GaloisInc/crucible + subdir: crucible + -- Many (but not all, sadly) uses of unsafe operations are -- controlled by this compile flag. When this flag is set -- to False, alternate implementations are used to avoid @@ -32,7 +37,7 @@ common bldflags -Werror=overlapping-patterns -Wpartial-fields -Wincomplete-uni-patterns - ghc-prof-options: -O2 -fprof-auto-top + ghc-prof-options: -O2 -fprof-auto-exported default-language: Haskell2010 diff --git a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs index 345425f10..eb076d174 100644 --- a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs +++ b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs @@ -18,6 +18,7 @@ solvers. -} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-} @@ -32,13 +33,15 @@ module Lang.Crucible.Backend.AssumptionStack , FrameIdentifier , AssumptionFrame(..) , AssumptionFrames(..) - , AssumptionStack(..) + , AssumptionStack -- ** Manipulating assumption stacks , initAssumptionStack , saveAssumptionStack , restoreAssumptionStack , pushFrame + , PopFrameError(..) , popFrame + , popFrameOrPanic , popFrameAndGoals , popFramesUntil , resetStack @@ -54,10 +57,13 @@ module Lang.Crucible.Backend.AssumptionStack ) where import Control.Exception (bracketOnError) +import Data.Functor ((<&>)) import qualified Data.Foldable as F import Data.IORef import Data.Parameterized.Nonce +import qualified Prettyprinter as PP + import Lang.Crucible.Backend.ProofGoals import Lang.Crucible.Panic (panic) @@ -173,12 +179,10 @@ popFramesUntil ident stk = atomicModifyIORef' (proofObligations stk) (go 1) where go n gc = case gcPop gc of - Left (ident', _assumes, mg, gc1) - | ident == ident' -> (gc',n) + Left frm + | ident == poppedFrameId frm -> (gc',n) | otherwise -> go (n+1) gc' - where gc' = case mg of - Nothing -> gc1 - Just g -> gcAddGoals g gc1 + where gc' = collectPoppedGoals frm Right _ -> panic "AssumptionStack.popFrameUntil" [ "Frame not found in stack." @@ -187,60 +191,84 @@ popFramesUntil ident stk = atomicModifyIORef' (proofObligations stk) (go 1) showFrameId (FrameIdentifier x) = show x +-- | Call 'gcPop' on the 'proofObligations' of this 'AssumptionStack' +popFrameUnchecked :: + Monoid asmp => + AssumptionStack asmp ast -> + IO (Either (PoppedFrame asmp ast) (Maybe (Goals asmp ast))) +popFrameUnchecked stk = + atomicModifyIORef' (proofObligations stk) $ \gc -> + case gcPop gc of + Left frm -> (collectPoppedGoals frm, Left frm) + Right mgs -> (gc, Right mgs) + +data PopFrameError + = NoFrames + -- | Expected, actual + | WrongFrame FrameIdentifier FrameIdentifier + +instance PP.Pretty PopFrameError where + pretty = + \case + NoFrames -> PP.pretty "Pop with no push in goal collector." + WrongFrame expected actual -> + PP.hsep + [ PP.pretty "Mismatch in assumption stack frames." + , PP.pretty "Expected ident:" + , PP.viaShow expected + , PP.pretty "Current frame:" + , PP.viaShow actual + ] + +instance Show PopFrameError where + show = show . PP.pretty + -- | Pop a previously-pushed assumption frame from the stack. -- All assumptions in that frame will be forgotten. The -- assumptions contained in the popped frame are returned. -popFrame :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO asmp +-- +-- Returns 'Left' if there are no frames on the stack, or if the top frame +-- doesn\'t have the provided 'FrameIdentifier'. +popFrame :: + Monoid asmp => + FrameIdentifier -> + AssumptionStack asmp ast -> + IO (Either PopFrameError (PoppedFrame asmp ast)) popFrame ident stk = - atomicModifyIORef' (proofObligations stk) $ \gc -> - case gcPop gc of - Left (ident', assumes, mg, gc1) - | ident == ident' -> - let gc' = case mg of - Nothing -> gc1 - Just g -> gcAddGoals g gc1 - in (gc', assumes) - | otherwise -> - panic "AssumptionStack.popFrame" - [ "Push/pop mismatch in assumption stack!" - , "*** Current frame: " ++ showFrameId ident - , "*** Expected ident: " ++ showFrameId ident' - ] - Right _ -> - panic "AssumptionStack.popFrame" - [ "Pop with no push in goal collector." - , "*** Current frame: " ++ showFrameId ident - ] - - where - showFrameId (FrameIdentifier x) = show x + popFrameUnchecked stk <&> + \case + Left frm + | ident == poppedFrameId frm -> Right frm + | otherwise -> Left (WrongFrame ident (poppedFrameId frm)) + Right _ -> Left NoFrames +-- | Pop a previously-pushed assumption frame from the stack. +-- All assumptions in that frame will be forgotten. The +-- assumptions contained in the popped frame are returned. +-- +-- Panics if there are no frames on the stack, or if the top frame doesn\'t +-- have the provided 'FrameIdentifier'. +popFrameOrPanic :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO asmp +popFrameOrPanic ident stk = + popFrame ident stk <&> + \case + Left err -> panic "AssumptionStack.popFrame" [show err] + Right frm -> poppedAssumptions frm +-- | Pop the assumptions and goals from the top frame. +-- +-- Panics if there are no frames on the stack, or if the top frame doesn\'t +-- have the provided 'FrameIdentifier'. popFrameAndGoals :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO (asmp, Maybe (Goals asmp ast)) popFrameAndGoals ident stk = - atomicModifyIORef' (proofObligations stk) $ \gc -> - case gcPop gc of - Left (ident', assumes, mg, gc1) - | ident == ident' -> (gc1, (assumes, mg)) - | otherwise -> - panic "AssumptionStack.popFrameAndGoals" - [ "Push/pop mismatch in assumption stack!" - , "*** Current frame: " ++ showFrameId ident - , "*** Expected ident: " ++ showFrameId ident' - ] - Right _ -> - panic "AssumptionStack.popFrameAndGoals" - [ "Pop with no push in goal collector." - , "*** Current frame: " ++ showFrameId ident - ] - - where - showFrameId (FrameIdentifier x) = show x - + popFrame ident stk <&> + \case + Left err -> panic "AssumptionStack.popFrameAndGoals" [show err] + Right frm -> (poppedAssumptions frm, poppedGoals frm) -- | Run an action in the scope of a fresh assumption frame. -- The frame will be popped and returned on successful @@ -252,5 +280,5 @@ inFreshFrame stk action = (pushFrame stk) (\ident -> popFrame ident stk) (\ident -> do x <- action - frm <- popFrame ident stk + frm <- popFrameOrPanic ident stk return (frm, x)) diff --git a/crucible/src/Lang/Crucible/Backend/Online.hs b/crucible/src/Lang/Crucible/Backend/Online.hs index 1142e42e8..8b46d96b8 100644 --- a/crucible/src/Lang/Crucible/Backend/Online.hs +++ b/crucible/src/Lang/Crucible/Backend/Online.hs @@ -579,7 +579,7 @@ instance (IsSymInterface (B.ExprBuilder scope st fs), OnlineSolver solver) => popAssumptionFrame bak ident = -- NB, pop the frame whether or not the solver pop succeeds - do frm <- popFrame ident (assumptionStack bak) + do frm <- popFrameOrPanic ident (assumptionStack bak) withSolverProcess bak (pure ()) pop return frm diff --git a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs index 38ea32b42..504765c8b 100644 --- a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs +++ b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs @@ -28,6 +28,8 @@ module Lang.Crucible.Backend.ProofGoals , traverseGoalCollectorWithAssumptions -- ** Context management + , PoppedFrame(..) + , collectPoppedGoals , gcAddAssumes, gcProve , gcPush, gcPop, gcAddGoals, @@ -265,23 +267,35 @@ gcAddAssumes :: Monoid asmp => asmp -> GoalCollector asmp goal -> GoalCollector gcAddAssumes as' (CollectingAssumptions as gls) = CollectingAssumptions (as <> as') gls gcAddAssumes as' gls = CollectingAssumptions as' gls -{- | Pop to the last push, or all the way to the top, if there were no more pushes. -If the result is 'Left', then we popped until an explicitly marked push; -in that case we return: - - 1. the frame identifier of the popped frame, - 2. the assumptions that were forgotten, - 3. any proof goals that were generated since the frame push, and - 4. the state of the collector before the push. +-- | A frame, popped by 'gcPop' +data PoppedFrame asmp goal + = PoppedFrame + { -- | The frame identifier of the popped frame + poppedFrameId :: !FrameIdentifier + -- | The assumptions that were forgotten by the pop + , poppedAssumptions :: asmp + -- | Any proof goals that were generated since the frame push + , poppedGoals :: Maybe (Goals asmp goal) + -- | The state of the collector before the push. + , poppedCollector :: GoalCollector asmp goal + } + +-- | Retrieve the 'GoalCollector' from a 'PoppedFrame', adding the +-- 'poppedGoals' (if there are any) via 'gcAddGoals'. +collectPoppedGoals :: PoppedFrame asmp goal -> GoalCollector asmp goal +collectPoppedGoals frm = + case poppedGoals frm of + Nothing -> poppedCollector frm + Just goals -> gcAddGoals goals (poppedCollector frm) +{- | Pop to the last push, or all the way to the top, if there were no more pushes. +If the result is 'Left', then we popped until an explicitly marked push. If the result is 'Right', then we popped all the way to the top, and the result is the goal tree, or 'Nothing' if there were no goals. -} - gcPop :: Monoid asmp => GoalCollector asmp goal -> - Either (FrameIdentifier, asmp, Maybe (Goals asmp goal), GoalCollector asmp goal) - (Maybe (Goals asmp goal)) + Either (PoppedFrame asmp goal) (Maybe (Goals asmp goal)) gcPop = go Nothing mempty where @@ -293,7 +307,7 @@ gcPop = go Nothing mempty Right (goalsConj (proveAll gs) hole) go hole as (CollectorFrame fid gc) = - Left (fid, as, hole, gc) + Left (PoppedFrame fid as hole gc) go hole as (CollectingAssumptions as' gc) = go (assuming as' <$> hole) (as' <> as) gc @@ -303,10 +317,10 @@ gcPop = go Nothing mempty -- | Get all currently collected goals. gcFinish :: Monoid asmp => GoalCollector asmp goal -> Maybe (Goals asmp goal) -gcFinish gc = case gcPop gc of - Left (_,_,Just g,gc1) -> gcFinish (gcAddGoals g gc1) - Left (_,_,Nothing,gc1) -> gcFinish gc1 - Right a -> a +gcFinish gc = + case gcPop gc of + Left poppedFrame -> gcFinish (collectPoppedGoals poppedFrame) + Right a -> a -- | Reset the goal collector to the empty assumption state; but first -- collect all the pending proof goals and stash them. diff --git a/crucible/src/Lang/Crucible/Backend/Simple.hs b/crucible/src/Lang/Crucible/Backend/Simple.hs index 8c23ecb58..f550a98f1 100644 --- a/crucible/src/Lang/Crucible/Backend/Simple.hs +++ b/crucible/src/Lang/Crucible/Backend/Simple.hs @@ -103,7 +103,7 @@ instance IsSymInterface (B.ExprBuilder t st fs) => AS.pushFrame (sbAssumptionStack bak) popAssumptionFrame bak ident = do - AS.popFrame ident (sbAssumptionStack bak) + AS.popFrameOrPanic ident (sbAssumptionStack bak) popAssumptionFrameAndObligations bak ident = do AS.popFrameAndGoals ident (sbAssumptionStack bak) diff --git a/crux-llvm/CHANGELOG.md b/crux-llvm/CHANGELOG.md index 90d201578..85da156ba 100644 --- a/crux-llvm/CHANGELOG.md +++ b/crux-llvm/CHANGELOG.md @@ -1,3 +1,7 @@ +# 0.8 -- 2024-02-05 + +* Add support for LLVM bitcode files generated by Apple Clang on macOS. + # 0.7 -- 2023-06-26 ## New features diff --git a/crux-llvm/README.md b/crux-llvm/README.md index 1a809f2e2..7961816a7 100644 --- a/crux-llvm/README.md +++ b/crux-llvm/README.md @@ -42,8 +42,8 @@ software: * `echo 'export PATH="/usr/local/opt/llvm/bin:$PATH"' >> ~/.bash_profile` * run `crux-llvm` in a new console to reload `.bash_profile` -We have tested `crux-llvm` most heavily with GHC 8.10.7, GHC 9.2.7, GHC 9.4.4, -and `cabal` version 3.8.1.0. We recommend Yices 2.6.x, and Z3 +We have tested `crux-llvm` most heavily with GHC 9.2, GHC 9.4, GHC 9.6, +and `cabal` version 3.10. We recommend Yices 2.6.x, and Z3 4.8.x. Technically, only one of Yices or Z3 is required, and CVC4 is also supported. However, in practice, having both tends to be convenient. Finally, LLVM versions from 3.6 through 16 are likely to diff --git a/crux-llvm/crux-llvm.cabal b/crux-llvm/crux-llvm.cabal index 44354cde5..91d3cc35d 100644 --- a/crux-llvm/crux-llvm.cabal +++ b/crux-llvm/crux-llvm.cabal @@ -1,8 +1,8 @@ Cabal-version: 2.2 Name: crux-llvm -Version: 0.7.0.99 +Version: 0.8.0.99 Author: Galois Inc. -Maintainer: iavor.diatchki@gmail.com +Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com Copyright: (c) Galois, Inc 2014-2022 License: BSD-3-Clause License-file: LICENSE @@ -41,6 +41,11 @@ data-files: c-src/libcxx-7.1.0.bc extra-source-files: CHANGELOG.md, README.md +source-repository head + type: git + location: https://github.com/GaloisInc/crucible + subdir: crux-llvm + common bldflags ghc-options: -Wall -Werror=incomplete-patterns diff --git a/crux-llvm/svcomp/mk-svcomp-bindist.sh b/crux-llvm/svcomp/mk-svcomp-bindist.sh index 421eff17f..371952281 100755 --- a/crux-llvm/svcomp/mk-svcomp-bindist.sh +++ b/crux-llvm/svcomp/mk-svcomp-bindist.sh @@ -5,6 +5,7 @@ DATE=$(date "+%Y-%m-%d") EXT="" IS_WIN=false OS_TAG=Linux +ARCH_TAG=X64 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )" extract_exe() { @@ -23,7 +24,7 @@ setup_dist() { zip_dist() { : "${VERSION?VERSION is required as an environment variable}" - pkgname="${pkgname:-"$1-$VERSION-$OS_TAG-x86_64"}" + pkgname="${pkgname:-"$1-$VERSION-$OS_TAG-$ARCH_TAG"}" mv dist "$pkgname" zip -r "$pkgname".zip "$pkgname" rm -rf dist diff --git a/crux-llvm/test-data/golden/T785a.c b/crux-llvm/test-data/golden/T785a.c index 7d522c52b..d05a33ccd 100644 --- a/crux-llvm/test-data/golden/T785a.c +++ b/crux-llvm/test-data/golden/T785a.c @@ -10,10 +10,13 @@ int main() { abort(); } else if (crucible_int8_t("test_exit")) { exit(1); - } else if (crucible_int8_t("test_assert_fail")) { - __assert_fail("0", "T785a.c", 16, "__assert_fail"); +#if defined(__APPLE__) + __assert_rtn("0", "T785b.c", 15, "__assert_rtn"); +#else + __assert_fail("0", "T785b.c", 17, "__assert_fail"); +#endif } else if (crucible_int8_t("test_crucible_assert")) { - crucible_assert(0, "T785a.c", 18); + crucible_assert(0, "T785b.c", 20); } else if (crucible_int8_t("test_CPROVER_assert")) { __CPROVER_assert(0, "__CPROVER_assert"); } diff --git a/crux-llvm/test-data/golden/T785b.c b/crux-llvm/test-data/golden/T785b.c index 03b9365c4..d0186ecef 100644 --- a/crux-llvm/test-data/golden/T785b.c +++ b/crux-llvm/test-data/golden/T785b.c @@ -5,15 +5,22 @@ extern void __CPROVER_assert(int32_t, const char *); +#if defined(__APPLE__) +// The expected output for this test case specifically mentions __assert_fail, +// so we need to call that in particular. __assert_fail isn't defined on macOS, +// so define a shim for it so that we can simulate it. +extern void __assert_fail(const char *, const char *, unsigned int, const char *); +#endif + int main() { if (crucible_int8_t("test_abort")) { abort(); } else if (crucible_int8_t("test_exit")) { exit(1); } else if (crucible_int8_t("test_assert_fail")) { - __assert_fail("0", "T785b.c", 16, "__assert_fail"); + __assert_fail("0", "T785b.c", 21, "__assert_fail"); } else if (crucible_int8_t("test_crucible_assert")) { - crucible_assert(0, "T785b.c", 18); + crucible_assert(0, "T785b.c", 23); } else if (crucible_int8_t("test_CPROVER_assert")) { __CPROVER_assert(0, "__CPROVER_assert"); } diff --git a/crux-llvm/test-data/golden/T785b.z3.good b/crux-llvm/test-data/golden/T785b.z3.good index db3fb6819..f980d79a6 100644 --- a/crux-llvm/test-data/golden/T785b.z3.good +++ b/crux-llvm/test-data/golden/T785b.z3.good @@ -1,5 +1,5 @@ [Crux] Found counterexample for verification goal -[Crux] test-data/golden/T785b.c:14:5: error: in main +[Crux] test-data/golden/T785b.c:21:5: error: in main [Crux] Call to assert() [Crux] Details: [Crux] __assert_fail diff --git a/crux-llvm/test-data/golden/golden/double_free.c b/crux-llvm/test-data/golden/golden/double_free.c index 1c1fd0549..4353749a1 100644 --- a/crux-llvm/test-data/golden/golden/double_free.c +++ b/crux-llvm/test-data/golden/golden/double_free.c @@ -2,7 +2,7 @@ #include #include -void do_free(int *p) __attribute__((noinline)) { +void __attribute__((noinline)) do_free(int *p) { free(p); } diff --git a/crux-llvm/test-data/golden/isinf.c b/crux-llvm/test-data/golden/isinf.c index 662f91a70..d9d662a16 100644 --- a/crux-llvm/test-data/golden/isinf.c +++ b/crux-llvm/test-data/golden/isinf.c @@ -11,22 +11,30 @@ int main(void) { double d3 = -INFINITY; // Infinite double d4 = NAN; // Not infinite (and also not finite) - check(isinf(d1) == 0); - check(isinf(d2) == 1); - check(isinf(d3) == -1); - check(isinf(d4) == 0); + // The C standard only requires that isinf(x) return a non-zero value when x + // is infinite. Unlike __builtin_isinf_sign(x), we cannot guarantee that this + // return value will be a specific number, so we make the tests below as + // generic as possible. + check(!(isinf(d1))); + check(isinf(d2)); + check(isinf(d3)); + check(!(isinf(d4))); +#if !defined(__APPLE__) // The parentheses around (isinf) are important here, as this instructs Clang - // to compile isinf as a direct function call rather than as a macro. - check((isinf)(d1) == 0); - check((isinf)(d2) == 1); - check((isinf)(d3) == -1); - check((isinf)(d4) == 0); + // to compile isinf as a direct function call rather than as a macro. This is + // not portable, however, For instance, macOS only provides isinf as a macro, + // not as a function. + check(!((isinf)(d1))); + check((isinf)(d2)); + check((isinf)(d3)); + check(!((isinf)(d4))); - check(__isinf(d1) == 0); - check(__isinf(d2) == 1); - check(__isinf(d3) == -1); - check(__isinf(d4) == 0); + check(!(__isinf(d1))); + check(__isinf(d2)); + check(__isinf(d3)); + check(!(__isinf(d4))); +#endif check(__builtin_isinf_sign(d1) == 0); check(__builtin_isinf_sign(d2) == 1); @@ -41,20 +49,22 @@ int main(void) { float f3 = -INFINITY; // Infinite float f4 = NAN; // Not infinite (and also not finite) - check(isinf(f1) == 0); - check(isinf(f2) == 1); - check(isinf(f3) == -1); - check(isinf(f4) == 0); + check(!(isinf(f1))); + check(isinf(f2)); + check(isinf(f3)); + check(!(isinf(f4))); - check((isinf)(f1) == 0); - check((isinf)(f2) == 1); - check((isinf)(f3) == -1); - check((isinf)(f4) == 0); +#if !defined(__APPLE__) + check(!((isinf)(f1))); + check((isinf)(f2)); + check((isinf)(f3)); + check(!((isinf)(f4))); - check(__isinff(f1) == 0); - check(__isinff(f2) == 1); - check(__isinff(f3) == -1); - check(__isinff(f4) == 0); + check(!(__isinff(f1))); + check(__isinff(f2)); + check(__isinff(f3)); + check(!(__isinff(f4))); +#endif check(__builtin_isinf_sign(f1) == 0); check(__builtin_isinf_sign(f2) == 1); diff --git a/crux-llvm/test-data/golden/isnan.c b/crux-llvm/test-data/golden/isnan.c index 1a6cb995f..5436f718c 100644 --- a/crux-llvm/test-data/golden/isnan.c +++ b/crux-llvm/test-data/golden/isnan.c @@ -5,17 +5,23 @@ int main() { // double double d = NAN; check(isnan(d)); - check((isnan)(d)); // The parentheses around (isnan) are important here, - // as this instructs Clang to compile isnan as a - // direct function call rather than as a macro. +#if !defined(__APPLE__) + // The parentheses around (isnan) are important here, as this instructs Clang + // to compile isnan as a direct function call rather than as a macro. This is + // not portable, however, For instance, macOS only provides isnan as a macro, + // not as a function. + check((isnan)(d)); check(__isnan(d)); +#endif check(__builtin_isnan(d)); // float float f = NAN; check(isnan(f)); +#if !defined(__APPLE__) check((isnan)(f)); check(__isnanf(f)); +#endif check(__builtin_isnan(f)); return 0; diff --git a/crux-llvm/test-data/golden/special-functions.c b/crux-llvm/test-data/golden/special-functions.c index 825df5b81..735c519f0 100644 --- a/crux-llvm/test-data/golden/special-functions.c +++ b/crux-llvm/test-data/golden/special-functions.c @@ -2,6 +2,11 @@ #include #include +#if defined(__APPLE__) +# define exp10f __exp10f +# define exp10 __exp10 +#endif + int main() { /////////////// // constants // diff --git a/crux-llvm/test/Test.hs b/crux-llvm/test/Test.hs index a980d1744..325ebe513 100644 --- a/crux-llvm/test/Test.hs +++ b/crux-llvm/test/Test.hs @@ -21,6 +21,7 @@ import Numeric.Natural import System.Environment ( withArgs, lookupEnv ) import System.Exit ( ExitCode(..) ) import System.FilePath ( (-<.>) ) +import qualified System.Info as Info import System.IO import System.Process ( readProcess ) import Text.Read ( readMaybe ) @@ -375,13 +376,19 @@ mkTest sweet _ expct = , TS.rootBaseName sweet == "nested_unsafe" ] + -- T972-fail requires an x86-64 compiler, so skip it on non-x86-64 + -- architectures. + let skipX86_64Tests = + Info.arch /= "x86_64" && + TS.rootBaseName sweet == "T972-fail" + -- If a .good file begins with SKIP_TEST, skip that test entirely. For test -- cases that require a minimum Clang version, this technique is used to -- prevent running the test on older Clang versions. skipTest <- ("SKIP_TEST" `BSIO.isPrefixOf`) <$> BSIO.readFile (TS.expectedFile expct) - if or [ skipTest, testLevel == "0" && longTests ] + if or [ skipTest, skipX86_64Tests, testLevel == "0" && longTests ] then do when (testLevel == "0" && longTests) $ putStrLn "*** Longer running test skipped; set CI_TEST_LEVEL=1 env var to enable" diff --git a/crux-mir/CHANGELOG.md b/crux-mir/CHANGELOG.md index 67282381f..0e83e1715 100644 --- a/crux-mir/CHANGELOG.md +++ b/crux-mir/CHANGELOG.md @@ -1,3 +1,17 @@ +# 0.8 -- 2024-02-05 + +* `crux-mir` now supports the `nightly-2023-01-23` Rust toolchain. Some of the + highlights of this include: + + * Properly support for Rust's new constant forms + * Better support for zero-sized constants + * Encoding enum discriminant types so that `crux-mir` can know about + non-`isize` discriminant types (e.g., `Ordering`, which uses an `i8` + discriminant) + * A more intelligent way of computing crate disambiguators for looking up + known types such as `MaybeUninit` and `Option` +* Support code that uses `vec::IntoIter` on length-0 `Vec` values. + # 0.7 -- 2023-06-26 ## API changes diff --git a/crux-mir/README.md b/crux-mir/README.md index 993b161a9..922cc0d90 100644 --- a/crux-mir/README.md +++ b/crux-mir/README.md @@ -24,7 +24,7 @@ README][mir-json-readme]. ## Installation -Use 8.10.7, 9.2.7, or 9.4.4. From the `crux-mir` directory, run: +Use GHC 9.2, 9.4, or 9.6. From the `crux-mir` directory, run: $ cabal v2-install exe:crux-mir --overwrite-policy=always diff --git a/crux-mir/crux-mir.cabal b/crux-mir/crux-mir.cabal index efabd85b3..31d9245f1 100644 --- a/crux-mir/crux-mir.cabal +++ b/crux-mir/crux-mir.cabal @@ -1,5 +1,5 @@ name: crux-mir -version: 0.7.0.99 +version: 0.8.0.99 -- synopsis: -- description: homepage: https://github.com/GaloisInc/crucible/blob/master/crux-mir/README.md diff --git a/crux/CHANGELOG.md b/crux/CHANGELOG.md index 875f684b1..cd505f4c2 100644 --- a/crux/CHANGELOG.md +++ b/crux/CHANGELOG.md @@ -1,3 +1,8 @@ +# 0.7 -- 2024-02-05 + +* Add a `Crux.Overrides` module, which defines common functionality for defining + overrides, which are shared among several Crux backends. + # 0.6 * Corresponds to the 0.6 release of `crux-llvm` and `crux-mir`. diff --git a/crux/crux.cabal b/crux/crux.cabal index 60d1d3fea..eeceb3036 100644 --- a/crux/crux.cabal +++ b/crux/crux.cabal @@ -1,9 +1,9 @@ Cabal-version: 2.2 Name: crux -Version: 0.6.0.99 +Version: 0.7.0.99 Copyright: (c) Galois, Inc. 2018-2022 Author: sweirich@galois.com -Maintainer: rdockins@galois.com +Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com License: BSD-3-Clause License-file: LICENSE Build-type: Simple @@ -17,6 +17,11 @@ Description: verification, usually by embedding verification specifications in the source language. +source-repository head + type: git + location: https://github.com/GaloisInc/crucible + subdir: crux + library build-depends: diff --git a/dependencies/llvm-pretty b/dependencies/llvm-pretty index 8124fc026..780e7c01c 160000 --- a/dependencies/llvm-pretty +++ b/dependencies/llvm-pretty @@ -1 +1 @@ -Subproject commit 8124fc0265b6ca5fde5812c789f40b2ea54af678 +Subproject commit 780e7c01cbd0b85172f11ea8edf0d7bbe6a84967 diff --git a/dependencies/llvm-pretty-bc-parser b/dependencies/llvm-pretty-bc-parser index 39b4a5ff2..395754789 160000 --- a/dependencies/llvm-pretty-bc-parser +++ b/dependencies/llvm-pretty-bc-parser @@ -1 +1 @@ -Subproject commit 39b4a5ff26ad88f7db250185cc5b471fac50141d +Subproject commit 395754789b2f1b1f3ffae22383f9522a3e44d68e diff --git a/dependencies/mir-json b/dependencies/mir-json index 117ec97f9..64dff1bb5 160000 --- a/dependencies/mir-json +++ b/dependencies/mir-json @@ -1 +1 @@ -Subproject commit 117ec97f971171cfac3eea37e5009e1f6bfa9ae8 +Subproject commit 64dff1bb538640bf61616e9ac3c2d87e2da8a1ff diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs b/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs index 89ab0aed5..d470430aa 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs @@ -337,6 +337,8 @@ registerOverrides appCtx modCtx kind overrides = "functions with prefix " <> Text.pack nm LLVMIntrinsics.SubstringsMatch nms -> "functions with names containing " <> Text.pack (show nms) + LLVMIntrinsics.DarwinAliasMatch nm -> + Text.pack (LLVMIntrinsics.stripDarwinAliases nm) registerDefinedFns :: (?intrinsicsOpts :: LLVMIntrinsics.IntrinsicsOptions) =>