GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-29 10:53:31 +03:00
Code Issues Projects Releases Wiki Activity

updated to master

Browse Source
This commit is contained in:
Henry Blanchette 2022-08-22 13:34:27 -07:00
commit 1cfad8affc
31 changed files with 530 additions and 362 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
.github/workflows/ci.yml vendored
View File

@ -9,7 +9,7 @@ on:
workflow_dispatch:
env:
SOLVER_PKG_VERSION: "snapshot-20220721"
SOLVER_PKG_VERSION: "snapshot-20220812"
# The CACHE_VERSION can be updated to force the use of a new cache if
# the current cache contents become corrupted/invalid. This can
# sometimes happen when (for example) the OS version is changed but
@ -20,7 +20,7 @@ env:
jobs:
config:
runs-on: ubuntu-20.04
runs-on: ubuntu-22.04
outputs:
name: ${{ steps.config.outputs.name }}
version: ${{ steps.config.outputs.version }}
@ -58,8 +58,8 @@ jobs:
strategy:
fail-fast: false
matrix:
os: [ubuntu-20.04, macos-12, windows-2019]
ghc-version: ["8.8.4", "8.10.7", "9.0.2", "9.2.2"]
os: [ubuntu-22.04, macos-12, windows-2019]
ghc-version: ["8.8.4", "8.10.7", "9.0.2", "9.2.4"]
exclude:
# https://gitlab.haskell.org/ghc/ghc/-/issues/18550
- os: windows-2019
@ -67,11 +67,11 @@ jobs:
- os: windows-2019
ghc-version: 9.0.2
- os: windows-2019
ghc-version: 9.2.2
ghc-version: 9.2.4
include:
# We include one job from an older Ubuntu LTS release to increase our
# coverage of possible Linux configurations.
- os: ubuntu-18.04
- os: ubuntu-22.04
ghc-version: 8.8.4
outputs:
test-lib-json: ${{ steps.test-lib.outputs.targets-json }}
@ -147,6 +147,8 @@ jobs:
cmd="cat \$1.stdout"
if ${{ runner.os == 'Windows' }}; then
cmd="cat \$1.stdout.mingw32 2>/dev/null || $cmd"
elif ${{ runner.os == 'macOS' }}; then
cmd="cat \$1.stdout.darwin 2>/dev/null || $cmd"
fi
./bin/test-runner --ext=.icry -r ./output --exe=$(which bash) -F -c -F "$cmd" -F -- ./tests
TARGETS_JSON=$(echo -n "$(ls -1 ./output/tests)" | jq -Rsc 'split("\n")')
@ -158,7 +160,7 @@ jobs:
- if: runner.os == 'Windows'
run: .github/wix.ps1
- if: runner.os == 'Windows'
- if: runner.os == 'Windows' && github.event.pull_request.head.repo.fork == false
shell: bash
env:
SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }}
@ -181,7 +183,8 @@ jobs:
env:
OS_TAG: ${{ matrix.os }}
- shell: bash
- if: github.event.pull_request.head.repo.fork == false
shell: bash
env:
SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }}
SIGNING_KEY: ${{ secrets.SIGNING_KEY }}
@ -231,12 +234,12 @@ jobs:
matrix:
suite: [test-lib]
target: ${{ fromJson(needs.build.outputs.test-lib-json) }}
os: [ubuntu-20.04, macos-12, windows-2019]
os: [ubuntu-22.04, macos-12, windows-2019]
continue-on-error: [false]
include:
- suite: rpc
target: ''
os: ubuntu-20.04
os: ubuntu-22.04
continue-on-error: false
#- suite: rpc
# target: ''
@ -311,7 +314,7 @@ jobs:
cryptol-remote-api/run_rpc_tests.sh
build-push-image:
runs-on: ubuntu-20.04
runs-on: ubuntu-22.04
needs: [config]
if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' || needs.config.outputs.release == 'true'
strategy:

27
Dockerfile
View File

@ -1,21 +1,36 @@
FROM haskell:8.8.4 AS build
FROM ubuntu:22.04 AS build
RUN apt-get update && apt-get install -y libncurses-dev unzip
RUN apt-get update && \
apt-get install -y \
# ghcup requirements
build-essential curl libffi-dev libffi8 libgmp-dev libgmp10 libncurses-dev libncurses6 libtinfo6 \
# Cryptol dependencies
zlib1g-dev \
# Miscellaneous
unzip
RUN useradd -m cryptol
COPY --chown=cryptol:cryptol . /cryptol
USER cryptol
WORKDIR /cryptol
RUN mkdir -p rootfs/usr/local/bin
WORKDIR /cryptol/rootfs/usr/local/bin
RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220114/ubuntu-18.04-bin.zip"
RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220812/ubuntu-22.04-bin.zip"
RUN unzip solvers.zip && rm solvers.zip && chmod +x *
WORKDIR /cryptol
ENV PATH=/cryptol/rootfs/usr/local/bin:$PATH
ENV PATH=/cryptol/rootfs/usr/local/bin:/home/cryptol/.local/bin:/home/cryptol/.ghcup/bin:$PATH
RUN z3 --version
ARG CRYPTOLPATH="/cryptol/.cryptol"
ENV LANG=C.UTF-8 \
LC_ALL=C.UTF-8
COPY cabal.GHC-8.8.4.config cabal.project.freeze
RUN mkdir -p /home/cryptol/.local/bin && \
curl -L https://downloads.haskell.org/~ghcup/0.1.17.7/x86_64-linux-ghcup-0.1.17.7 -o /home/cryptol/.local/bin/ghcup && \
chmod +x /home/cryptol/.local/bin/ghcup
RUN mkdir -p /home/cryptol/.ghcup && \
ghcup --version && \
ghcup install cabal 3.6.2.0 && \
ghcup install ghc 8.8.4 && \
ghcup set ghc 8.8.4
RUN cabal v2-update && \
cabal v2-build -j cryptol:exe:cryptol && \
cp $(cabal v2-exec which cryptol) rootfs/usr/local/bin && \
@ -33,9 +48,9 @@ RUN mkdir -p rootfs/"${CRYPTOLPATH}" \
USER root
RUN chown -R root:root /cryptol/rootfs
FROM debian:buster-20210511-slim
FROM ubuntu:22.04
RUN apt-get update \
&& apt-get install -y libgmp10 libgomp1 libffi6 libncurses6 libtinfo6 libreadline7 \
&& apt-get install -y libgmp10 libgomp1 libffi8 libncurses6 libtinfo6 libreadline8 \
&& apt-get clean && rm -rf /var/lib/apt/lists/*
RUN useradd -m cryptol && chown -R cryptol:cryptol /home/cryptol
COPY --from=build /cryptol/rootfs /

6
README.md
View File

@ -46,7 +46,7 @@ Cryptol currently uses Microsoft Research's [Z3 SMT
solver](https://github.com/Z3Prover/z3) by default to solve constraints
during type checking, and as the default solver for the `:sat` and
`:prove` commands. Cryptol generally requires the most recent version
of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20220721).
of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20220812).
You can download Z3 binaries for a variety of platforms from their
[releases page](https://github.com/Z3Prover/z3/releases). If you
@ -75,15 +75,15 @@ Cryptol builds and runs on various flavors of Linux, Mac OS X, and
Windows. We regularly build and test it in the following environments:
- macOS 12, 64-bit
- Ubuntu 18.04, 64-bit
- Ubuntu 20.04, 64-bit
- Ubuntu 22.04, 64-bit
- Windows Server 2019, 64-bit
## Prerequisites
Cryptol is regularly built and tested with the three most recent
versions of GHC, which at the time of this writing are 8.10.7, 9.0.2, and
9.2.2. The easiest way to install an approporiate version of GHC is
9.2.4. The easiest way to install an approporiate version of GHC is
with [ghcup](https://www.haskell.org/ghcup/).
Some supporting non-Haskell libraries are required to build

90
cabal.GHC-8.10.7.config
View File

@ -11,10 +11,7 @@ constraints: any.Cabal ==3.2.1.0,
any.QuickCheck ==2.14.2,
QuickCheck -old-random +templatehaskell,
any.StateVar ==1.2.2,
any.abstract-deque ==0.3,
abstract-deque -usecas,
any.abstract-par ==0.3.3,
any.adjunctions ==4.4,
any.adjunctions ==4.4.1,
any.aeson ==2.0.3.0,
aeson -cffi +ordered-keymap,
any.alex ==3.2.7.1,
@ -23,7 +20,7 @@ constraints: any.Cabal ==3.2.1.0,
any.ansi-wl-pprint ==0.6.9,
ansi-wl-pprint -example,
any.appar ==0.1.8,
any.arithmoi ==0.12.0.1,
any.arithmoi ==0.12.0.2,
any.array ==0.5.4.0,
any.asn1-encoding ==0.9.6,
any.asn1-parse ==0.9.5,
@ -35,16 +32,18 @@ constraints: any.Cabal ==3.2.1.0,
attoparsec -developer,
any.auto-update ==0.1.6,
any.base ==4.14.3.0,
any.base-compat ==0.12.1,
any.base-compat-batteries ==0.12.1,
any.base-orphans ==0.8.6,
any.base-compat ==0.12.2,
any.base-compat-batteries ==0.12.2,
any.base-orphans ==0.8.7,
any.base64-bytestring ==1.2.1.0,
any.basement ==0.0.14,
any.bifunctors ==5.5.11,
any.bifunctors ==5.5.12,
bifunctors +semigroups +tagged,
any.bimap ==0.4.0,
any.bimap ==0.5.0,
any.binary ==0.8.8.0,
any.binary-orphans ==1.0.2,
any.binary-orphans ==1.0.3,
any.bitvec ==1.1.3.0,
bitvec -libgmp,
any.bitwise ==1.0.0.1,
any.blaze-builder ==0.4.2.2,
any.blaze-html ==0.9.1.2,
@ -56,9 +55,9 @@ constraints: any.Cabal ==3.2.1.0,
any.cabal-doctest ==1.0.9,
any.call-stack ==0.4.0,
any.case-insensitive ==1.2.1.0,
any.cassava ==0.5.2.0,
any.cassava ==0.5.3.0,
cassava -bytestring--lt-0_10_4,
any.cereal ==0.5.8.2,
any.cereal ==0.5.8.3,
cereal -bytestring-builder,
any.chimera ==0.3.2.0,
chimera +representable,
@ -69,15 +68,15 @@ constraints: any.Cabal ==3.2.1.0,
any.comonad ==5.0.8,
comonad +containers +distributive +indexed-traversable,
any.concurrent-extra ==0.7.0.12,
any.config-value ==0.8.2.1,
any.constraints ==0.13.3,
any.config-value ==0.8.3,
any.constraints ==0.13.4,
any.containers ==0.6.5.1,
any.contravariant ==1.5.5,
contravariant +semigroups +statevar +tagged,
any.cookie ==0.4.5,
any.criterion ==1.5.13.0,
any.criterion ==1.6.0.0,
criterion -embed-data-files -fast,
any.criterion-measurement ==0.1.3.0,
any.criterion-measurement ==0.2.0.0,
criterion-measurement -fast,
any.cryptohash-md5 ==0.11.101.0,
any.cryptohash-sha1 ==0.11.101.0,
@ -91,7 +90,7 @@ constraints: any.Cabal ==3.2.1.0,
any.data-fix ==0.3.2,
any.deepseq ==1.4.4.0,
any.dense-linear-algebra ==0.1.0.0,
any.deriving-compat ==0.6,
any.deriving-compat ==0.6.1,
deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11,
any.directory ==1.3.6.0,
any.distributive ==0.6.2.1,
@ -110,7 +109,7 @@ constraints: any.Cabal ==3.2.1.0,
any.filelock ==0.1.1.5,
any.filepath ==1.4.2.1,
any.fingertree ==0.1.5.0,
any.free ==5.1.7,
any.free ==5.1.9,
any.ghc-boot-th ==8.10.7,
any.ghc-prim ==0.6.1,
any.gitrev ==1.3.1,
@ -130,34 +129,33 @@ constraints: any.Cabal ==3.2.1.0,
any.http2 ==3.0.3,
http2 -devel -doc -h2spec,
any.indexed-traversable ==0.1.2,
any.indexed-traversable-instances ==0.1.1,
any.indexed-traversable-instances ==0.1.1.1,
any.integer-gmp ==1.0.3.0,
any.integer-logarithms ==1.0.3.1,
integer-logarithms -check-bounds +integer-gmp,
any.integer-roots ==1.0.2.0,
any.invariant ==0.5.5,
any.invariant ==0.6,
any.io-streams ==1.5.2.1,
io-streams +network -nointeractivetests +zlib,
any.iproute ==1.7.12,
any.js-chart ==2.9.4.1,
any.kan-extensions ==5.2.3,
any.lens ==5.1,
any.kan-extensions ==5.2.5,
any.lens ==5.1.1,
lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy,
any.libBF ==0.6.3,
any.libBF ==0.6.4,
libBF -system-libbf,
any.libffi ==0.2,
libffi +ghc-bundled-libffi,
any.math-functions ==0.3.4.2,
math-functions +system-erf +system-expm1,
any.megaparsec ==9.2.0,
any.megaparsec ==9.2.1,
megaparsec -dev,
any.memory ==0.17.0,
memory +support_bytestring +support_deepseq,
any.microstache ==1.0.2,
any.microstache ==1.0.2.2,
any.mod ==0.1.2.2,
mod +semirings +vector,
any.monad-control ==1.0.3.1,
any.monad-par ==0.3.5,
monad-par -chaselev -newgeneric,
any.monad-par-extras ==0.3.3,
any.monadLib ==3.10.1,
any.mtl ==2.2.2,
any.mwc-random ==0.15.0.2,
@ -167,7 +165,7 @@ constraints: any.Cabal ==3.2.1.0,
network -devel,
any.network-byte-order ==0.1.6,
any.network-info ==0.2.1,
any.newtype-generics ==0.6.1,
any.newtype-generics ==0.6.2,
any.numtype-dk ==0.5.0.3,
any.old-locale ==1.0.0.7,
any.old-time ==1.1.0.3,
@ -184,20 +182,20 @@ constraints: any.Cabal ==3.2.1.0,
any.pretty ==1.1.3.6,
any.prettyprinter ==1.7.1,
prettyprinter -buildreadme +text,
any.primitive ==0.7.3.0,
any.primitive ==0.7.4.0,
any.process ==1.6.13.2,
any.profunctors ==5.6.2,
any.psqueues ==0.2.7.3,
any.quickcheck-instances ==0.3.27,
any.quickcheck-instances ==0.3.28,
quickcheck-instances -bytestring-builder,
any.random ==1.2.1,
any.random ==1.2.1.1,
any.reflection ==2.1.6,
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.2.4.3,
any.resourcet ==1.2.6,
any.rts ==1.0.1,
any.safe ==0.3.19,
any.sbv ==9.0,
@ -219,7 +217,7 @@ constraints: any.Cabal ==3.2.1.0,
any.simple-smt ==0.9.7,
any.splitmix ==0.1.0.4,
splitmix -optimised-mixer,
any.statistics ==0.16.0.2,
any.statistics ==0.16.1.0,
any.stm ==2.5.0.1,
any.streaming-commons ==0.2.2.4,
streaming-commons -use-bytestring-builder,
@ -228,7 +226,7 @@ constraints: any.Cabal ==3.2.1.0,
any.syb ==0.7.2.1,
any.tagged ==0.8.6.1,
tagged +deepseq +transformers,
any.tasty ==1.4.2.1,
any.tasty ==1.4.2.3,
tasty +clock +unix,
any.tasty-hunit ==0.10.0.3,
any.tasty-quickcheck ==0.10.2,
@ -243,7 +241,7 @@ constraints: any.Cabal ==3.2.1.0,
any.text-short ==0.1.5,
text-short -asserts,
any.tf-random ==0.5,
any.th-abstraction ==0.4.3.0,
any.th-abstraction ==0.4.4.0,
any.th-lift ==0.8.2,
any.th-lift-instances ==0.1.19,
any.these ==1.1.1.1,
@ -252,19 +250,19 @@ constraints: any.Cabal ==3.2.1.0,
any.time-compat ==1.9.6.1,
time-compat -old-locale,
any.time-manager ==0.0.0,
any.tls ==1.5.7,
any.tls ==1.6.0,
tls +compat -hans +network,
any.tls-session-manager ==0.0.4,
any.transformers ==0.5.6.2,
any.transformers-base ==0.4.6,
transformers-base +orphaninstances,
any.transformers-compat ==0.7.1,
any.transformers-compat ==0.7.2,
transformers-compat -five +five-three -four +generic-deriving +mtl -three -two,
any.type-equality ==1,
any.unbounded-delays ==0.1.1.1,
any.uniplate ==1.6.13,
any.unix ==2.7.2.2,
any.unix-compat ==0.5.4,
any.unix-compat ==0.6,
unix-compat -old-time,
any.unix-time ==0.4.7,
any.unliftio ==0.2.22.0,
@ -278,7 +276,7 @@ constraints: any.Cabal ==3.2.1.0,
vault +useghc,
any.vector ==0.12.3.1,
vector +boundschecks -internalchecks -unsafechecks -wall,
any.vector-algorithms ==0.8.0.4,
any.vector-algorithms ==0.9.0.1,
vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks,
any.vector-binary-instances ==0.2.5.2,
any.vector-th-unbox ==0.2.2,
@ -286,19 +284,19 @@ constraints: any.Cabal ==3.2.1.0,
any.void ==0.7.3,
void -safe,
any.wai ==3.2.3,
any.wai-extra ==3.1.10,
any.wai-extra ==3.1.12.1,
wai-extra -build-example,
any.wai-logger ==2.4.0,
any.warp ==3.3.20,
any.warp ==3.3.22,
warp +allow-sendfilefd -network-bytestring -warp-debug +x509,
any.warp-tls ==3.3.2,
any.warp-tls ==3.3.3,
any.wcwidth ==0.0.2,
wcwidth -cli +split-base,
any.what4 ==1.3,
what4 -drealtestdisable -solvertests -stptestdisable,
any.witherable ==0.4.2,
any.word8 ==0.1.3,
any.x509 ==1.7.6,
any.x509 ==1.7.7,
any.x509-store ==1.6.9,
any.x509-validation ==1.6.12,
any.xml ==1.3.14,
@ -306,4 +304,4 @@ constraints: any.Cabal ==3.2.1.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 2022-05-04T18:13:54Z
index-state: hackage.haskell.org 2022-08-12T18:38:07Z

92
cabal.GHC-8.8.4.config
View File

@ -11,10 +11,7 @@ constraints: any.Cabal ==3.0.1.0,
any.QuickCheck ==2.14.2,
QuickCheck -old-random +templatehaskell,
any.StateVar ==1.2.2,
any.abstract-deque ==0.3,
abstract-deque -usecas,
any.abstract-par ==0.3.3,
any.adjunctions ==4.4,
any.adjunctions ==4.4.1,
any.aeson ==2.0.3.0,
aeson -cffi +ordered-keymap,
any.alex ==3.2.7.1,
@ -23,7 +20,7 @@ constraints: any.Cabal ==3.0.1.0,
any.ansi-wl-pprint ==0.6.9,
ansi-wl-pprint -example,
any.appar ==0.1.8,
any.arithmoi ==0.12.0.1,
any.arithmoi ==0.12.0.2,
any.array ==0.5.4.0,
any.asn1-encoding ==0.9.6,
any.asn1-parse ==0.9.5,
@ -35,16 +32,18 @@ constraints: any.Cabal ==3.0.1.0,
attoparsec -developer,
any.auto-update ==0.1.6,
any.base ==4.13.0.0,
any.base-compat ==0.12.1,
any.base-compat-batteries ==0.12.1,
any.base-orphans ==0.8.6,
any.base-compat ==0.12.2,
any.base-compat-batteries ==0.12.2,
any.base-orphans ==0.8.7,
any.base64-bytestring ==1.2.1.0,
any.basement ==0.0.14,
any.bifunctors ==5.5.11,
any.bifunctors ==5.5.12,
bifunctors +semigroups +tagged,
any.bimap ==0.4.0,
any.bimap ==0.5.0,
any.binary ==0.8.7.0,
any.binary-orphans ==1.0.2,
any.binary-orphans ==1.0.3,
any.bitvec ==1.1.3.0,
bitvec -libgmp,
any.bitwise ==1.0.0.1,
any.blaze-builder ==0.4.2.2,
any.blaze-html ==0.9.1.2,
@ -56,9 +55,9 @@ constraints: any.Cabal ==3.0.1.0,
any.cabal-doctest ==1.0.9,
any.call-stack ==0.4.0,
any.case-insensitive ==1.2.1.0,
any.cassava ==0.5.2.0,
any.cassava ==0.5.3.0,
cassava -bytestring--lt-0_10_4,
any.cereal ==0.5.8.2,
any.cereal ==0.5.8.3,
cereal -bytestring-builder,
any.chimera ==0.3.2.0,
chimera +representable,
@ -69,15 +68,15 @@ constraints: any.Cabal ==3.0.1.0,
any.comonad ==5.0.8,
comonad +containers +distributive +indexed-traversable,
any.concurrent-extra ==0.7.0.12,
any.config-value ==0.8.2.1,
any.constraints ==0.13.3,
any.config-value ==0.8.3,
any.constraints ==0.13.4,
any.containers ==0.6.2.1,
any.contravariant ==1.5.5,
contravariant +semigroups +statevar +tagged,
any.cookie ==0.4.5,
any.criterion ==1.5.13.0,
any.criterion ==1.6.0.0,
criterion -embed-data-files -fast,
any.criterion-measurement ==0.1.3.0,
any.criterion-measurement ==0.2.0.0,
criterion-measurement -fast,
any.cryptohash-md5 ==0.11.101.0,
any.cryptohash-sha1 ==0.11.101.0,
@ -91,7 +90,7 @@ constraints: any.Cabal ==3.0.1.0,
any.data-fix ==0.3.2,
any.deepseq ==1.4.4.0,
any.dense-linear-algebra ==0.1.0.0,
any.deriving-compat ==0.6,
any.deriving-compat ==0.6.1,
deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11,
any.directory ==1.3.6.0,
any.distributive ==0.6.2.1,
@ -102,7 +101,7 @@ constraints: any.Cabal ==3.0.1.0,
any.entropy ==0.4.1.7,
entropy -halvm,
any.exact-pi ==0.5.0.2,
any.exceptions ==0.10.4,
any.exceptions ==0.10.5,
exceptions +transformers-0-4,
any.extensible-exceptions ==0.1.1.4,
any.extra ==1.7.10,
@ -111,7 +110,7 @@ constraints: any.Cabal ==3.0.1.0,
any.filelock ==0.1.1.5,
any.filepath ==1.4.2.1,
any.fingertree ==0.1.5.0,
any.free ==5.1.7,
any.free ==5.1.9,
any.ghc-boot-th ==8.8.4,
any.ghc-prim ==0.5.3,
any.gitrev ==1.3.1,
@ -131,34 +130,33 @@ constraints: any.Cabal ==3.0.1.0,
any.http2 ==3.0.3,
http2 -devel -doc -h2spec,
any.indexed-traversable ==0.1.2,
any.indexed-traversable-instances ==0.1.1,
any.indexed-traversable-instances ==0.1.1.1,
any.integer-gmp ==1.0.2.0,
any.integer-logarithms ==1.0.3.1,
integer-logarithms -check-bounds +integer-gmp,
any.integer-roots ==1.0.2.0,
any.invariant ==0.5.5,
any.invariant ==0.6,
any.io-streams ==1.5.2.1,
io-streams +network -nointeractivetests +zlib,
any.iproute ==1.7.12,
any.js-chart ==2.9.4.1,
any.kan-extensions ==5.2.3,
any.lens ==5.1,
any.kan-extensions ==5.2.5,
any.lens ==5.1.1,
lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy,
any.libBF ==0.6.3,
any.libBF ==0.6.4,
libBF -system-libbf,
any.libffi ==0.2,
libffi +ghc-bundled-libffi,
any.math-functions ==0.3.4.2,
math-functions +system-erf +system-expm1,
any.megaparsec ==9.2.0,
any.megaparsec ==9.2.1,
megaparsec -dev,
any.memory ==0.17.0,
memory +support_bytestring +support_deepseq,
any.microstache ==1.0.2,
any.microstache ==1.0.2.2,
any.mod ==0.1.2.2,
mod +semirings +vector,
any.monad-control ==1.0.3.1,
any.monad-par ==0.3.5,
monad-par -chaselev -newgeneric,
any.monad-par-extras ==0.3.3,
any.monadLib ==3.10.1,
any.mtl ==2.2.2,
any.mwc-random ==0.15.0.2,
@ -168,7 +166,7 @@ constraints: any.Cabal ==3.0.1.0,
network -devel,
any.network-byte-order ==0.1.6,
any.network-info ==0.2.1,
any.newtype-generics ==0.6.1,
any.newtype-generics ==0.6.2,
any.numtype-dk ==0.5.0.3,
any.old-locale ==1.0.0.7,
any.old-time ==1.1.0.3,
@ -185,20 +183,20 @@ constraints: any.Cabal ==3.0.1.0,
any.pretty ==1.1.3.6,
any.prettyprinter ==1.7.1,
prettyprinter -buildreadme +text,
any.primitive ==0.7.3.0,
any.primitive ==0.7.4.0,
any.process ==1.6.9.0,
any.profunctors ==5.6.2,
any.psqueues ==0.2.7.3,
any.quickcheck-instances ==0.3.27,
any.quickcheck-instances ==0.3.28,
quickcheck-instances -bytestring-builder,
any.random ==1.2.1,
any.random ==1.2.1.1,
any.reflection ==2.1.6,
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.2.4.3,
any.resourcet ==1.2.6,
any.rts ==1.0,
any.safe ==0.3.19,
any.sbv ==9.0,
@ -220,7 +218,7 @@ constraints: any.Cabal ==3.0.1.0,
any.simple-smt ==0.9.7,
any.splitmix ==0.1.0.4,
splitmix -optimised-mixer,
any.statistics ==0.16.0.2,
any.statistics ==0.16.1.0,
any.stm ==2.5.0.0,
any.streaming-commons ==0.2.2.4,
streaming-commons -use-bytestring-builder,
@ -229,7 +227,7 @@ constraints: any.Cabal ==3.0.1.0,
any.syb ==0.7.2.1,
any.tagged ==0.8.6.1,
tagged +deepseq +transformers,
any.tasty ==1.4.2.1,
any.tasty ==1.4.2.3,
tasty +clock +unix,
any.tasty-hunit ==0.10.0.3,
any.tasty-quickcheck ==0.10.2,
@ -244,7 +242,7 @@ constraints: any.Cabal ==3.0.1.0,
any.text-short ==0.1.5,
text-short -asserts,
any.tf-random ==0.5,
any.th-abstraction ==0.4.3.0,
any.th-abstraction ==0.4.4.0,
any.th-lift ==0.8.2,
any.th-lift-instances ==0.1.19,
any.these ==1.1.1.1,
@ -253,19 +251,19 @@ constraints: any.Cabal ==3.0.1.0,
any.time-compat ==1.9.6.1,
time-compat -old-locale,
any.time-manager ==0.0.0,
any.tls ==1.5.7,
any.tls ==1.6.0,
tls +compat -hans +network,
any.tls-session-manager ==0.0.4,
any.transformers ==0.5.6.2,
any.transformers-base ==0.4.6,
transformers-base +orphaninstances,
any.transformers-compat ==0.7.1,
any.transformers-compat ==0.7.2,
transformers-compat -five +five-three -four +generic-deriving +mtl -three -two,
any.type-equality ==1,
any.unbounded-delays ==0.1.1.1,
any.uniplate ==1.6.13,
any.unix ==2.7.2.2,
any.unix-compat ==0.5.4,
any.unix-compat ==0.6,
unix-compat -old-time,
any.unix-time ==0.4.7,
any.unliftio ==0.2.22.0,
@ -279,7 +277,7 @@ constraints: any.Cabal ==3.0.1.0,
vault +useghc,
any.vector ==0.12.3.1,
vector +boundschecks -internalchecks -unsafechecks -wall,
any.vector-algorithms ==0.8.0.4,
any.vector-algorithms ==0.9.0.1,
vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks,
any.vector-binary-instances ==0.2.5.2,
any.vector-th-unbox ==0.2.2,
@ -287,19 +285,19 @@ constraints: any.Cabal ==3.0.1.0,
any.void ==0.7.3,
void -safe,
any.wai ==3.2.3,
any.wai-extra ==3.1.10,
any.wai-extra ==3.1.12.1,
wai-extra -build-example,
any.wai-logger ==2.4.0,
any.warp ==3.3.20,
any.warp ==3.3.22,
warp +allow-sendfilefd -network-bytestring -warp-debug +x509,
any.warp-tls ==3.3.2,
any.warp-tls ==3.3.3,
any.wcwidth ==0.0.2,
wcwidth -cli +split-base,
any.what4 ==1.3,
what4 -drealtestdisable -solvertests -stptestdisable,
any.witherable ==0.4.2,
any.word8 ==0.1.3,
any.x509 ==1.7.6,
any.x509 ==1.7.7,
any.x509-store ==1.6.9,
any.x509-validation ==1.6.12,
any.xml ==1.3.14,
@ -307,4 +305,4 @@ constraints: any.Cabal ==3.0.1.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 2022-05-04T18:13:54Z
index-state: hackage.haskell.org 2022-08-12T18:38:07Z

90
cabal.GHC-9.0.2.config
View File

@ -11,10 +11,7 @@ constraints: any.Cabal ==3.4.1.0,
any.QuickCheck ==2.14.2,
QuickCheck -old-random +templatehaskell,
any.StateVar ==1.2.2,
any.abstract-deque ==0.3,
abstract-deque -usecas,
any.abstract-par ==0.3.3,
any.adjunctions ==4.4,
any.adjunctions ==4.4.1,
any.aeson ==2.0.3.0,
aeson -cffi +ordered-keymap,
any.alex ==3.2.7.1,
@ -23,7 +20,7 @@ constraints: any.Cabal ==3.4.1.0,
any.ansi-wl-pprint ==0.6.9,
ansi-wl-pprint -example,
any.appar ==0.1.8,
any.arithmoi ==0.12.0.1,
any.arithmoi ==0.12.0.2,
any.array ==0.5.4.0,
any.asn1-encoding ==0.9.6,
any.asn1-parse ==0.9.5,
@ -35,16 +32,18 @@ constraints: any.Cabal ==3.4.1.0,
attoparsec -developer,
any.auto-update ==0.1.6,
any.base ==4.15.1.0,
any.base-compat ==0.12.1,
any.base-compat-batteries ==0.12.1,
any.base-orphans ==0.8.6,
any.base-compat ==0.12.2,
any.base-compat-batteries ==0.12.2,
any.base-orphans ==0.8.7,
any.base64-bytestring ==1.2.1.0,
any.basement ==0.0.14,
any.bifunctors ==5.5.11,
any.bifunctors ==5.5.12,
bifunctors +semigroups +tagged,
any.bimap ==0.4.0,
any.bimap ==0.5.0,
any.binary ==0.8.8.0,
any.binary-orphans ==1.0.2,
any.binary-orphans ==1.0.3,
any.bitvec ==1.1.3.0,
bitvec -libgmp,
any.bitwise ==1.0.0.1,
any.blaze-builder ==0.4.2.2,
any.blaze-html ==0.9.1.2,
@ -56,9 +55,9 @@ constraints: any.Cabal ==3.4.1.0,
any.cabal-doctest ==1.0.9,
any.call-stack ==0.4.0,
any.case-insensitive ==1.2.1.0,
any.cassava ==0.5.2.0,
any.cassava ==0.5.3.0,
cassava -bytestring--lt-0_10_4,
any.cereal ==0.5.8.2,
any.cereal ==0.5.8.3,
cereal -bytestring-builder,
any.chimera ==0.3.2.0,
chimera +representable,
@ -69,15 +68,15 @@ constraints: any.Cabal ==3.4.1.0,
any.comonad ==5.0.8,
comonad +containers +distributive +indexed-traversable,
any.concurrent-extra ==0.7.0.12,
any.config-value ==0.8.2.1,
any.constraints ==0.13.3,
any.config-value ==0.8.3,
any.constraints ==0.13.4,
any.containers ==0.6.4.1,
any.contravariant ==1.5.5,
contravariant +semigroups +statevar +tagged,
any.cookie ==0.4.5,
any.criterion ==1.5.13.0,
any.criterion ==1.6.0.0,
criterion -embed-data-files -fast,
any.criterion-measurement ==0.1.3.0,
any.criterion-measurement ==0.2.0.0,
criterion-measurement -fast,
any.cryptohash-md5 ==0.11.101.0,
any.cryptohash-sha1 ==0.11.101.0,
@ -91,7 +90,7 @@ constraints: any.Cabal ==3.4.1.0,
any.data-fix ==0.3.2,
any.deepseq ==1.4.5.0,
any.dense-linear-algebra ==0.1.0.0,
any.deriving-compat ==0.6,
any.deriving-compat ==0.6.1,
deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11,
any.directory ==1.3.6.2,
any.distributive ==0.6.2.1,
@ -110,7 +109,7 @@ constraints: any.Cabal ==3.4.1.0,
any.filelock ==0.1.1.5,
any.filepath ==1.4.2.1,
any.fingertree ==0.1.5.0,
any.free ==5.1.7,
any.free ==5.1.9,
any.ghc-bignum ==1.1,
any.ghc-boot-th ==9.0.2,
any.ghc-prim ==0.7.0,
@ -131,34 +130,33 @@ constraints: any.Cabal ==3.4.1.0,
any.http2 ==3.0.3,
http2 -devel -doc -h2spec,
any.indexed-traversable ==0.1.2,
any.indexed-traversable-instances ==0.1.1,
any.indexed-traversable-instances ==0.1.1.1,
any.integer-gmp ==1.1,
any.integer-logarithms ==1.0.3.1,
integer-logarithms -check-bounds +integer-gmp,
any.integer-roots ==1.0.2.0,
any.invariant ==0.5.5,
any.invariant ==0.6,
any.io-streams ==1.5.2.1,
io-streams +network -nointeractivetests +zlib,
any.iproute ==1.7.12,
any.js-chart ==2.9.4.1,
any.kan-extensions ==5.2.3,
any.lens ==5.1,
any.kan-extensions ==5.2.5,
any.lens ==5.1.1,
lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy,
any.libBF ==0.6.3,
any.libBF ==0.6.4,
libBF -system-libbf,
any.libffi ==0.2,
libffi +ghc-bundled-libffi,
any.math-functions ==0.3.4.2,
math-functions +system-erf +system-expm1,
any.megaparsec ==9.2.0,
any.megaparsec ==9.2.1,
megaparsec -dev,
any.memory ==0.17.0,
memory +support_bytestring +support_deepseq,
any.microstache ==1.0.2,
any.microstache ==1.0.2.2,
any.mod ==0.1.2.2,
mod +semirings +vector,
any.monad-control ==1.0.3.1,
any.monad-par ==0.3.5,
monad-par -chaselev -newgeneric,
any.monad-par-extras ==0.3.3,
any.monadLib ==3.10.1,
any.mtl ==2.2.2,
any.mwc-random ==0.15.0.2,
@ -168,7 +166,7 @@ constraints: any.Cabal ==3.4.1.0,
network -devel,
any.network-byte-order ==0.1.6,
any.network-info ==0.2.1,
any.newtype-generics ==0.6.1,
any.newtype-generics ==0.6.2,
any.numtype-dk ==0.5.0.3,
any.old-locale ==1.0.0.7,
any.old-time ==1.1.0.3,
@ -185,20 +183,20 @@ constraints: any.Cabal ==3.4.1.0,
any.pretty ==1.1.3.6,
any.prettyprinter ==1.7.1,
prettyprinter -buildreadme +text,
any.primitive ==0.7.3.0,
any.primitive ==0.7.4.0,
any.process ==1.6.13.2,
any.profunctors ==5.6.2,
any.psqueues ==0.2.7.3,
any.quickcheck-instances ==0.3.27,
any.quickcheck-instances ==0.3.28,
quickcheck-instances -bytestring-builder,
any.random ==1.2.1,
any.random ==1.2.1.1,
any.reflection ==2.1.6,
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.2.4.3,
any.resourcet ==1.2.6,
any.rts ==1.0.2,
any.safe ==0.3.19,
any.sbv ==9.0,
@ -220,7 +218,7 @@ constraints: any.Cabal ==3.4.1.0,
any.simple-smt ==0.9.7,
any.splitmix ==0.1.0.4,
splitmix -optimised-mixer,
any.statistics ==0.16.0.2,
any.statistics ==0.16.1.0,
any.stm ==2.5.0.0,
any.streaming-commons ==0.2.2.4,
streaming-commons -use-bytestring-builder,
@ -229,7 +227,7 @@ constraints: any.Cabal ==3.4.1.0,
any.syb ==0.7.2.1,
any.tagged ==0.8.6.1,
tagged +deepseq +transformers,
any.tasty ==1.4.2.1,
any.tasty ==1.4.2.3,
tasty +clock +unix,
any.tasty-hunit ==0.10.0.3,
any.tasty-quickcheck ==0.10.2,
@ -244,7 +242,7 @@ constraints: any.Cabal ==3.4.1.0,
any.text-short ==0.1.5,
text-short -asserts,
any.tf-random ==0.5,
any.th-abstraction ==0.4.3.0,
any.th-abstraction ==0.4.4.0,
any.th-lift ==0.8.2,
any.th-lift-instances ==0.1.19,
any.these ==1.1.1.1,
@ -253,19 +251,19 @@ constraints: any.Cabal ==3.4.1.0,
any.time-compat ==1.9.6.1,
time-compat -old-locale,
any.time-manager ==0.0.0,
any.tls ==1.5.7,
any.tls ==1.6.0,
tls +compat -hans +network,
any.tls-session-manager ==0.0.4,
any.transformers ==0.5.6.2,
any.transformers-base ==0.4.6,
transformers-base +orphaninstances,
any.transformers-compat ==0.7.1,
any.transformers-compat ==0.7.2,
transformers-compat -five +five-three -four +generic-deriving +mtl -three -two,
any.type-equality ==1,
any.unbounded-delays ==0.1.1.1,
any.uniplate ==1.6.13,
any.unix ==2.7.2.2,
any.unix-compat ==0.5.4,
any.unix-compat ==0.6,
unix-compat -old-time,
any.unix-time ==0.4.7,
any.unliftio ==0.2.22.0,
@ -279,7 +277,7 @@ constraints: any.Cabal ==3.4.1.0,
vault +useghc,
any.vector ==0.12.3.1,
vector +boundschecks -internalchecks -unsafechecks -wall,
any.vector-algorithms ==0.8.0.4,
any.vector-algorithms ==0.9.0.1,
vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks,
any.vector-binary-instances ==0.2.5.2,
any.vector-th-unbox ==0.2.2,
@ -287,19 +285,19 @@ constraints: any.Cabal ==3.4.1.0,
any.void ==0.7.3,
void -safe,
any.wai ==3.2.3,
any.wai-extra ==3.1.10,
any.wai-extra ==3.1.12.1,
wai-extra -build-example,
any.wai-logger ==2.4.0,
any.warp ==3.3.20,
any.warp ==3.3.22,
warp +allow-sendfilefd -network-bytestring -warp-debug +x509,
any.warp-tls ==3.3.2,
any.warp-tls ==3.3.3,
any.wcwidth ==0.0.2,
wcwidth -cli +split-base,
any.what4 ==1.3,
what4 -drealtestdisable -solvertests -stptestdisable,
any.witherable ==0.4.2,
any.word8 ==0.1.3,
any.x509 ==1.7.6,
any.x509 ==1.7.7,
any.x509-store ==1.6.9,
any.x509-validation ==1.6.12,
any.xml ==1.3.14,
@ -307,4 +305,4 @@ constraints: any.Cabal ==3.4.1.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 2022-05-04T18:13:54Z
index-state: hackage.haskell.org 2022-08-12T18:38:07Z

94
cabal.GHC-9.2.2.config → cabal.GHC-9.2.4.config
View File

@ -11,10 +11,7 @@ constraints: any.Cabal ==3.6.3.0,
any.QuickCheck ==2.14.2,
QuickCheck -old-random +templatehaskell,
any.StateVar ==1.2.2,
any.abstract-deque ==0.3,
abstract-deque -usecas,
any.abstract-par ==0.3.3,
any.adjunctions ==4.4,
any.adjunctions ==4.4.1,
any.aeson ==2.0.3.0,
aeson -cffi +ordered-keymap,
any.alex ==3.2.7.1,
@ -23,7 +20,7 @@ constraints: any.Cabal ==3.6.3.0,
any.ansi-wl-pprint ==0.6.9,
ansi-wl-pprint -example,
any.appar ==0.1.8,
any.arithmoi ==0.12.0.1,
any.arithmoi ==0.12.0.2,
any.array ==0.5.4.0,
any.asn1-encoding ==0.9.6,
any.asn1-parse ==0.9.5,
@ -34,17 +31,19 @@ constraints: any.Cabal ==3.6.3.0,
any.attoparsec ==0.14.4,
attoparsec -developer,
any.auto-update ==0.1.6,
any.base ==4.16.1.0,
any.base-compat ==0.12.1,
any.base-compat-batteries ==0.12.1,
any.base-orphans ==0.8.6,
any.base ==4.16.3.0,
any.base-compat ==0.12.2,
any.base-compat-batteries ==0.12.2,
any.base-orphans ==0.8.7,
any.base64-bytestring ==1.2.1.0,
any.basement ==0.0.14,
any.bifunctors ==5.5.11,
any.bifunctors ==5.5.12,
bifunctors +semigroups +tagged,
any.bimap ==0.4.0,
any.bimap ==0.5.0,
any.binary ==0.8.9.0,
any.binary-orphans ==1.0.2,
any.binary-orphans ==1.0.3,
any.bitvec ==1.1.3.0,
bitvec -libgmp,
any.bitwise ==1.0.0.1,
any.blaze-builder ==0.4.2.2,
any.blaze-html ==0.9.1.2,
@ -56,9 +55,9 @@ constraints: any.Cabal ==3.6.3.0,
any.cabal-doctest ==1.0.9,
any.call-stack ==0.4.0,
any.case-insensitive ==1.2.1.0,
any.cassava ==0.5.2.0,
any.cassava ==0.5.3.0,
cassava -bytestring--lt-0_10_4,
any.cereal ==0.5.8.2,
any.cereal ==0.5.8.3,
cereal -bytestring-builder,
any.chimera ==0.3.2.0,
chimera +representable,
@ -69,15 +68,15 @@ constraints: any.Cabal ==3.6.3.0,
any.comonad ==5.0.8,
comonad +containers +distributive +indexed-traversable,
any.concurrent-extra ==0.7.0.12,
any.config-value ==0.8.2.1,
any.constraints ==0.13.3,
any.config-value ==0.8.3,
any.constraints ==0.13.4,
any.containers ==0.6.5.1,
any.contravariant ==1.5.5,
contravariant +semigroups +statevar +tagged,
any.cookie ==0.4.5,
any.criterion ==1.5.13.0,
any.criterion ==1.6.0.0,
criterion -embed-data-files -fast,
any.criterion-measurement ==0.1.3.0,
any.criterion-measurement ==0.2.0.0,
criterion-measurement -fast,
any.cryptohash-md5 ==0.11.101.0,
any.cryptohash-sha1 ==0.11.101.0,
@ -91,7 +90,7 @@ constraints: any.Cabal ==3.6.3.0,
any.data-fix ==0.3.2,
any.deepseq ==1.4.6.1,
any.dense-linear-algebra ==0.1.0.0,
any.deriving-compat ==0.6,
any.deriving-compat ==0.6.1,
deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11,
any.directory ==1.3.6.2,
any.distributive ==0.6.2.1,
@ -110,9 +109,9 @@ constraints: any.Cabal ==3.6.3.0,
any.filelock ==0.1.1.5,
any.filepath ==1.4.2.2,
any.fingertree ==0.1.5.0,
any.free ==5.1.7,
any.free ==5.1.9,
any.ghc-bignum ==1.2,
any.ghc-boot-th ==9.2.2,
any.ghc-boot-th ==9.2.4,
any.ghc-prim ==0.8.0,
any.gitrev ==1.3.1,
any.happy ==1.20.0,
@ -131,34 +130,33 @@ constraints: any.Cabal ==3.6.3.0,
any.http2 ==3.0.3,
http2 -devel -doc -h2spec,
any.indexed-traversable ==0.1.2,
any.indexed-traversable-instances ==0.1.1,
any.indexed-traversable-instances ==0.1.1.1,
any.integer-gmp ==1.1,
any.integer-logarithms ==1.0.3.1,
integer-logarithms -check-bounds +integer-gmp,
any.integer-roots ==1.0.2.0,
any.invariant ==0.5.5,
any.invariant ==0.6,
any.io-streams ==1.5.2.1,
io-streams +network -nointeractivetests +zlib,
any.iproute ==1.7.12,
any.js-chart ==2.9.4.1,
any.kan-extensions ==5.2.3,
any.lens ==5.1,
any.kan-extensions ==5.2.5,
any.lens ==5.1.1,
lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy,
any.libBF ==0.6.3,
any.libBF ==0.6.4,
libBF -system-libbf,
any.libffi ==0.2,
libffi +ghc-bundled-libffi,
any.math-functions ==0.3.4.2,
math-functions +system-erf +system-expm1,
any.megaparsec ==9.2.0,
any.megaparsec ==9.2.1,
megaparsec -dev,
any.memory ==0.17.0,
memory +support_bytestring +support_deepseq,
any.microstache ==1.0.2,
any.microstache ==1.0.2.2,
any.mod ==0.1.2.2,
mod +semirings +vector,
any.monad-control ==1.0.3.1,
any.monad-par ==0.3.5,
monad-par -chaselev -newgeneric,
any.monad-par-extras ==0.3.3,
any.monadLib ==3.10.1,
any.mtl ==2.2.2,
any.mwc-random ==0.15.0.2,
@ -168,7 +166,7 @@ constraints: any.Cabal ==3.6.3.0,
network -devel,
any.network-byte-order ==0.1.6,
any.network-info ==0.2.1,
any.newtype-generics ==0.6.1,
any.newtype-generics ==0.6.2,
any.numtype-dk ==0.5.0.3,
any.old-locale ==1.0.0.7,
any.old-time ==1.1.0.3,
@ -185,20 +183,20 @@ constraints: any.Cabal ==3.6.3.0,
any.pretty ==1.1.3.6,
any.prettyprinter ==1.7.1,
prettyprinter -buildreadme +text,
any.primitive ==0.7.3.0,
any.primitive ==0.7.4.0,
any.process ==1.6.13.2,
any.profunctors ==5.6.2,
any.psqueues ==0.2.7.3,
any.quickcheck-instances ==0.3.27,
any.quickcheck-instances ==0.3.28,
quickcheck-instances -bytestring-builder,
any.random ==1.2.1,
any.random ==1.2.1.1,
any.reflection ==2.1.6,
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.2.4.3,
any.resourcet ==1.2.6,
any.rts ==1.0.2,
any.safe ==0.3.19,
any.sbv ==9.0,
@ -220,7 +218,7 @@ constraints: any.Cabal ==3.6.3.0,
any.simple-smt ==0.9.7,
any.splitmix ==0.1.0.4,
splitmix -optimised-mixer,
any.statistics ==0.16.0.2,
any.statistics ==0.16.1.0,
any.stm ==2.5.0.2,
any.streaming-commons ==0.2.2.4,
streaming-commons -use-bytestring-builder,
@ -229,7 +227,7 @@ constraints: any.Cabal ==3.6.3.0,
any.syb ==0.7.2.1,
any.tagged ==0.8.6.1,
tagged +deepseq +transformers,
any.tasty ==1.4.2.1,
any.tasty ==1.4.2.3,
tasty +clock +unix,
any.tasty-hunit ==0.10.0.3,
any.tasty-quickcheck ==0.10.2,
@ -244,7 +242,7 @@ constraints: any.Cabal ==3.6.3.0,
any.text-short ==0.1.5,
text-short -asserts,
any.tf-random ==0.5,
any.th-abstraction ==0.4.3.0,
any.th-abstraction ==0.4.4.0,
any.th-lift ==0.8.2,
any.th-lift-instances ==0.1.19,
any.these ==1.1.1.1,
@ -253,19 +251,19 @@ constraints: any.Cabal ==3.6.3.0,
any.time-compat ==1.9.6.1,
time-compat -old-locale,
any.time-manager ==0.0.0,
any.tls ==1.5.7,
any.tls ==1.6.0,
tls +compat -hans +network,
any.tls-session-manager ==0.0.4,
any.transformers ==0.5.6.2,
any.transformers-base ==0.4.6,
transformers-base +orphaninstances,
any.transformers-compat ==0.7.1,
any.transformers-compat ==0.7.2,
transformers-compat -five +five-three -four +generic-deriving +mtl -three -two,
any.type-equality ==1,
any.unbounded-delays ==0.1.1.1,
any.uniplate ==1.6.13,
any.unix ==2.7.2.2,
any.unix-compat ==0.5.4,
any.unix-compat ==0.6,
unix-compat -old-time,
any.unix-time ==0.4.7,
any.unliftio ==0.2.22.0,
@ -279,7 +277,7 @@ constraints: any.Cabal ==3.6.3.0,
vault +useghc,
any.vector ==0.12.3.1,
vector +boundschecks -internalchecks -unsafechecks -wall,
any.vector-algorithms ==0.8.0.4,
any.vector-algorithms ==0.9.0.1,
vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks,
any.vector-binary-instances ==0.2.5.2,
any.vector-th-unbox ==0.2.2,
@ -287,19 +285,19 @@ constraints: any.Cabal ==3.6.3.0,
any.void ==0.7.3,
void -safe,
any.wai ==3.2.3,
any.wai-extra ==3.1.10,
any.wai-extra ==3.1.12.1,
wai-extra -build-example,
any.wai-logger ==2.4.0,
any.warp ==3.3.20,
any.warp ==3.3.22,
warp +allow-sendfilefd -network-bytestring -warp-debug +x509,
any.warp-tls ==3.3.2,
any.warp-tls ==3.3.3,
any.wcwidth ==0.0.2,
wcwidth -cli +split-base,
any.what4 ==1.3,
what4 -drealtestdisable -solvertests -stptestdisable,
any.witherable ==0.4.2,
any.word8 ==0.1.3,
any.x509 ==1.7.6,
any.x509 ==1.7.7,
any.x509-store ==1.6.9,
any.x509-validation ==1.6.12,
any.xml ==1.3.14,
@ -307,4 +305,4 @@ constraints: any.Cabal ==3.6.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 2022-05-04T18:13:54Z
index-state: hackage.haskell.org 2022-08-12T18:38:07Z

21
cryptol-remote-api/Dockerfile
View File

@ -1,10 +1,17 @@
ARG GHCVER="8.10.7"
ARG GHCVER_BOOTSTRAP="8.10.2"
FROM debian:buster-20210511 AS toolchain
FROM ubuntu:22.04 AS toolchain
ARG PORTABILITY=false
RUN apt-get update && apt-get install -y libncurses-dev libz-dev unzip \
build-essential curl libffi-dev libffi6 libgmp-dev libgmp10 libncurses-dev libncurses5 libtinfo5 libnuma-dev \
$(if ${PORTABILITY}; then echo git autoconf python3; fi)
RUN apt-get update && \
apt-get install -y \
# ghcup requirements
build-essential curl libffi-dev libffi8 libgmp-dev libgmp10 libncurses-dev libncurses6 libtinfo6 \
# Cryptol dependencies
zlib1g-dev \
# GHC build dependencies
$(if ${PORTABILITY}; then echo git autoconf python3 libnuma-dev; fi) \
# Miscellaneous
unzip
ENV GHCUP_INSTALL_BASE_PREFIX=/opt \
PATH=/opt/.ghcup/bin:$PATH
RUN curl -o /usr/local/bin/ghcup "https://downloads.haskell.org/~ghcup/0.1.17.7/x86_64-linux-ghcup-0.1.17.7" && \
@ -57,14 +64,14 @@ ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH
RUN mkdir -p rootfs/"${CRYPTOLPATH}" \
&& cp -r lib/* rootfs/"${CRYPTOLPATH}"
WORKDIR /cryptol/rootfs/usr/local/bin
RUN curl -sL -o solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220114/ubuntu-18.04-bin.zip" && \
RUN curl -sL -o solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220812/ubuntu-22.04-bin.zip" && \
unzip solvers.zip && rm solvers.zip && chmod +x *
USER root
RUN chown -R root:root /cryptol/rootfs
FROM debian:buster-20210511-slim
FROM ubuntu:22.04
RUN apt-get update \
&& apt-get install -y libgmp10 libgomp1 libffi6 libncurses6 libtinfo6 libreadline7 libnuma-dev openssl \
&& apt-get install -y libgmp10 libgomp1 libffi8 libncurses6 libtinfo6 libreadline8 libnuma-dev openssl \
&& apt-get clean && rm -rf /var/lib/apt/lists/*
RUN useradd -m cryptol && chown -R cryptol:cryptol /home/cryptol
COPY --from=build /cryptol/rootfs /

31
docs/RefMan/FFI.rst
View File

@ -188,20 +188,23 @@ Other sizes of floating points are not supported.
Sequences
~~~~~~~~~
Let ``n : #`` be a Cryptol type, possibly containing type variables, that
satisfies ``fin n``, and ``T`` be one of the above Cryptol *integral types* or
*floating point types*. Let ``U`` be the C type that ``T`` corresponds to.
Let ``n1, n2, ..., nk : #`` be Cryptol types (with ``k >= 1``), possibly
containing type variables, that satisfy ``fin n1, fin n2, ..., fin nk``, and
``T`` be one of the above Cryptol *integral types* or *floating point types*.
Let ``U`` be the C type that ``T`` corresponds to.
============ ===========
Cryptol type C type
============ ===========
``[n]T`` ``U*``
============ ===========
==================== ===========
Cryptol type C type
==================== ===========
``[n1][n2]...[nk]T`` ``U*``
==================== ===========
The C pointer points to an array of ``n`` elements of type ``U``. Note that,
while the length of the array itself is not explicitly passed along with the
pointer, any type arguments contained in the size are passed as C ``size_t``'s
earlier, so the C code can always know the length of the array.
The C pointer points to an array of ``n1 * n2 * ... * nk`` elements of type
``U``. If the sequence is multidimensional, it is flattened and stored
contiguously, similar to the representation of multidimensional arrays in C.
Note that, while the dimensions of the array itself are not explicitly passed
along with the pointer, any type arguments contained in the size are passed as C
``size_t``'s earlier, so the C code can always know the dimensions of the array.
Tuples and records
~~~~~~~~~~~~~~~~~~
@ -258,12 +261,12 @@ Cryptol type (or kind) C argument type(s) C return type C output
``[K]Bit`` where ``32 < K <= 64`` ``uint64_t`` ``uint64_t`` ``uint64_t*``
``Float32`` ``float`` ``float`` ``float*``
``Float64`` ``double`` ``double`` ``double*``
``[n]T`` ``U*`` N/A ``U*``
``[n1][n2]...[nk]T`` ``U*`` N/A ``U*``
``(T1, T2, ..., Tn)`` ``U1, U2, ..., Un`` N/A ``V1, V2, ..., Vn``
``{f1: T1, f2: T2, ..., fn: Tn}`` ``U1, U2, ..., Un`` N/A ``V1, V2, ..., Vn``
================================== =================== ============= =========================
where ``K`` is a constant number, ``n`` is a variable number, ``Ti`` is a type,
where ``K`` is a constant number, ``ni`` are variable numbers, ``Ti`` is a type,
``Ui`` is its C argument type, and ``Vi`` is its C output argument type.
Memory

BIN
docs/RefMan/_build/doctrees/FFI.doctree
View File

Binary file not shown.

BIN
docs/RefMan/_build/doctrees/environment.pickle
View File

Binary file not shown.

27
docs/RefMan/_build/html/FFI.html
View File

@ -303,13 +303,14 @@ Other sizes of floating points are not supported.</p>
</section>
<section id="sequences">
<h3>Sequences<a class="headerlink" href="#sequences" title="Permalink to this heading"></a></h3>
<p>Let <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">:</span> <span class="pre">#</span></code> be a Cryptol type, possibly containing type variables, that
satisfies <code class="docutils literal notranslate"><span class="pre">fin</span> <span class="pre">n</span></code>, and <code class="docutils literal notranslate"><span class="pre">T</span></code> be one of the above Cryptol <em>integral types</em> or
<em>floating point types</em>. Let <code class="docutils literal notranslate"><span class="pre">U</span></code> be the C type that <code class="docutils literal notranslate"><span class="pre">T</span></code> corresponds to.</p>
<p>Let <code class="docutils literal notranslate"><span class="pre">n1,</span> <span class="pre">n2,</span> <span class="pre">...,</span> <span class="pre">nk</span> <span class="pre">:</span> <span class="pre">#</span></code> be Cryptol types (with <code class="docutils literal notranslate"><span class="pre">k</span> <span class="pre">&gt;=</span> <span class="pre">1</span></code>), possibly
containing type variables, that satisfy <code class="docutils literal notranslate"><span class="pre">fin</span> <span class="pre">n1,</span> <span class="pre">fin</span> <span class="pre">n2,</span> <span class="pre">...,</span> <span class="pre">fin</span> <span class="pre">nk</span></code>, and
<code class="docutils literal notranslate"><span class="pre">T</span></code> be one of the above Cryptol <em>integral types</em> or <em>floating point types</em>.
Let <code class="docutils literal notranslate"><span class="pre">U</span></code> be the C type that <code class="docutils literal notranslate"><span class="pre">T</span></code> corresponds to.</p>
<table class="docutils align-default">
<colgroup>
<col style="width: 52%" />
<col style="width: 48%" />
<col style="width: 65%" />
<col style="width: 35%" />
</colgroup>
<thead>
<tr class="row-odd"><th class="head"><p>Cryptol type</p></th>
@ -317,15 +318,17 @@ satisfies <code class="docutils literal notranslate"><span class="pre">fin</span
</tr>
</thead>
<tbody>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">[n]T</span></code></p></td>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">[n1][n2]...[nk]T</span></code></p></td>
<td><p><code class="docutils literal notranslate"><span class="pre">U*</span></code></p></td>
</tr>
</tbody>
</table>
<p>The C pointer points to an array of <code class="docutils literal notranslate"><span class="pre">n</span></code> elements of type <code class="docutils literal notranslate"><span class="pre">U</span></code>. Note that,
while the length of the array itself is not explicitly passed along with the
pointer, any type arguments contained in the size are passed as C <code class="docutils literal notranslate"><span class="pre">size_t</span></code>’s
earlier, so the C code can always know the length of the array.</p>
<p>The C pointer points to an array of <code class="docutils literal notranslate"><span class="pre">n1</span> <span class="pre">*</span> <span class="pre">n2</span> <span class="pre">*</span> <span class="pre">...</span> <span class="pre">*</span> <span class="pre">nk</span></code> elements of type
<code class="docutils literal notranslate"><span class="pre">U</span></code>. If the sequence is multidimensional, it is flattened and stored
contiguously, similar to the representation of multidimensional arrays in C.
Note that, while the dimensions of the array itself are not explicitly passed
along with the pointer, any type arguments contained in the size are passed as C
<code class="docutils literal notranslate"><span class="pre">size_t</span></code>’s earlier, so the C code can always know the dimensions of the array.</p>
</section>
<section id="tuples-and-records">
<h3>Tuples and records<a class="headerlink" href="#tuples-and-records" title="Permalink to this heading"></a></h3>
@ -432,7 +435,7 @@ input versions are the same type, because it is already a pointer.</p>
<td><p><code class="docutils literal notranslate"><span class="pre">double</span></code></p></td>
<td><p><code class="docutils literal notranslate"><span class="pre">double*</span></code></p></td>
</tr>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">[n]T</span></code></p></td>
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">[n1][n2]...[nk]T</span></code></p></td>
<td><p><code class="docutils literal notranslate"><span class="pre">U*</span></code></p></td>
<td><p>N/A</p></td>
<td><p><code class="docutils literal notranslate"><span class="pre">U*</span></code></p></td>
@ -449,7 +452,7 @@ input versions are the same type, because it is already a pointer.</p>
</tr>
</tbody>
</table>
<p>where <code class="docutils literal notranslate"><span class="pre">K</span></code> is a constant number, <code class="docutils literal notranslate"><span class="pre">n</span></code> is a variable number, <code class="docutils literal notranslate"><span class="pre">Ti</span></code> is a type,
<p>where <code class="docutils literal notranslate"><span class="pre">K</span></code> is a constant number, <code class="docutils literal notranslate"><span class="pre">ni</span></code> are variable numbers, <code class="docutils literal notranslate"><span class="pre">Ti</span></code> is a type,
<code class="docutils literal notranslate"><span class="pre">Ui</span></code> is its C argument type, and <code class="docutils literal notranslate"><span class="pre">Vi</span></code> is its C output argument type.</p>
</section>
</section>

31
docs/RefMan/_build/html/_sources/FFI.rst.txt
View File

@ -188,20 +188,23 @@ Other sizes of floating points are not supported.
Sequences
~~~~~~~~~
Let ``n : #`` be a Cryptol type, possibly containing type variables, that
satisfies ``fin n``, and ``T`` be one of the above Cryptol *integral types* or
*floating point types*. Let ``U`` be the C type that ``T`` corresponds to.
Let ``n1, n2, ..., nk : #`` be Cryptol types (with ``k >= 1``), possibly
containing type variables, that satisfy ``fin n1, fin n2, ..., fin nk``, and
``T`` be one of the above Cryptol *integral types* or *floating point types*.
Let ``U`` be the C type that ``T`` corresponds to.
============ ===========
Cryptol type C type
============ ===========
``[n]T`` ``U*``
============ ===========
==================== ===========
Cryptol type C type
==================== ===========
``[n1][n2]...[nk]T`` ``U*``
==================== ===========
The C pointer points to an array of ``n`` elements of type ``U``. Note that,
while the length of the array itself is not explicitly passed along with the
pointer, any type arguments contained in the size are passed as C ``size_t``'s
earlier, so the C code can always know the length of the array.
The C pointer points to an array of ``n1 * n2 * ... * nk`` elements of type
``U``. If the sequence is multidimensional, it is flattened and stored
contiguously, similar to the representation of multidimensional arrays in C.
Note that, while the dimensions of the array itself are not explicitly passed
along with the pointer, any type arguments contained in the size are passed as C
``size_t``'s earlier, so the C code can always know the dimensions of the array.
Tuples and records
~~~~~~~~~~~~~~~~~~
@ -258,12 +261,12 @@ Cryptol type (or kind) C argument type(s) C return type C output
``[K]Bit`` where ``32 < K <= 64`` ``uint64_t`` ``uint64_t`` ``uint64_t*``
``Float32`` ``float`` ``float`` ``float*``
``Float64`` ``double`` ``double`` ``double*``
``[n]T`` ``U*`` N/A ``U*``
``[n1][n2]...[nk]T`` ``U*`` N/A ``U*``
``(T1, T2, ..., Tn)`` ``U1, U2, ..., Un`` N/A ``V1, V2, ..., Vn``
``{f1: T1, f2: T2, ..., fn: Tn}`` ``U1, U2, ..., Un`` N/A ``V1, V2, ..., Vn``
================================== =================== ============= =========================
where ``K`` is a constant number, ``n`` is a variable number, ``Ti`` is a type,
where ``K`` is a constant number, ``ni`` are variable numbers, ``Ti`` is a type,
``Ui`` is its C argument type, and ``Vi`` is its C output argument type.
Memory

2
docs/RefMan/_build/html/searchindex.js
View File

File diff suppressed because one or more lines are too long

27
src/Cryptol/Backend/FFI.hs
View File

@ -12,6 +12,7 @@
-- libraries. Currently works on Unix only.
module Cryptol.Backend.FFI
( ForeignSrc
, getForeignSrcPath
, loadForeignSrc
, unloadForeignSrc
#ifdef FFI_ENABLED
@ -56,12 +57,14 @@ import GHC.Generics
-- | A source from which we can retrieve implementations of foreign functions.
data ForeignSrc = ForeignSrc
{ -- | The 'ForeignPtr' wraps the pointer returned by 'dlopen', where the
{ -- | The file path of the 'ForeignSrc'.
foreignSrcPath :: FilePath
-- | The 'ForeignPtr' wraps the pointer returned by 'dlopen', where the
-- finalizer calls 'dlclose' when the library is no longer needed. We keep
-- references to the 'ForeignPtr' in each foreign function that is in the
-- evaluation environment, so that the shared library will stay open as long
-- as there are references to it.
foreignSrcFPtr :: ForeignPtr ()
, foreignSrcFPtr :: ForeignPtr ()
-- | We support explicit unloading of the shared library so we keep track of
-- if it has already been unloaded, and if so the finalizer does nothing.
-- This is updated atomically when the library is unloaded.
@ -73,16 +76,20 @@ instance Show ForeignSrc where
instance NFData ForeignSrc where
rnf ForeignSrc {..} = foreignSrcFPtr `seq` foreignSrcLoaded `deepseq` ()
-- | Get the file path of the 'ForeignSrc'.
getForeignSrcPath :: ForeignSrc -> Maybe FilePath
getForeignSrcPath = Just . foreignSrcPath
-- | Load a 'ForeignSrc' for the given __Cryptol__ file path. The file path of
-- the shared library that we try to load is the same as the Cryptol file path
-- except with a platform specific extension.
loadForeignSrc :: FilePath -> IO (Either FFILoadError ForeignSrc)
loadForeignSrc = loadForeignLib >=> traverse \ptr -> do
loadForeignSrc = loadForeignLib >=> traverse \(foreignSrcPath, ptr) -> do
foreignSrcLoaded <- newMVar True
foreignSrcFPtr <- newForeignPtr ptr (unloadForeignSrc' foreignSrcLoaded ptr)
pure ForeignSrc {..}
loadForeignLib :: FilePath -> IO (Either FFILoadError (Ptr ()))
loadForeignLib :: FilePath -> IO (Either FFILoadError (FilePath, Ptr ()))
#ifdef darwin_HOST_OS
-- On Darwin, try loading .dylib first, and if that fails try .so
loadForeignLib path =
@ -95,9 +102,12 @@ loadForeignLib path =
loadForeignLib path =
tryLoad (CantLoadFFISrc path) $ open "so"
#endif
where -- RTLD_NOW so we can make sure that the symbols actually exist at
-- module loading time
open ext = undl <$> dlopen (path -<.> ext) [RTLD_NOW]
where open ext = do
let libPath = path -<.> ext
-- RTLD_NOW so we can make sure that the symbols actually exist at
-- module loading time
ptr <- undl <$> dlopen libPath [RTLD_NOW]
pure (libPath, ptr)
-- | Explicitly unload a 'ForeignSrc' immediately instead of waiting for the
-- garbage collector to do it. This can be useful if you want to immediately
@ -218,6 +228,9 @@ callForeignImpl ForeignImpl {..} xs = withForeignSrc foreignImplSrc \_ ->
data ForeignSrc = ForeignSrc deriving (Show, Generic, NFData)
getForeignSrcPath :: ForeignSrc -> Maybe FilePath
getForeignSrcPath _ = Nothing
loadForeignSrc :: FilePath -> IO (Either FFILoadError ForeignSrc)
loadForeignSrc _ = pure $ Right ForeignSrc

114
src/Cryptol/Eval/FFI.hs
View File

@ -1,3 +1,4 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
@ -12,29 +13,31 @@
-- | Evaluation of foreign functions.
module Cryptol.Eval.FFI
( evalForeignDecls
( findForeignDecls
, evalForeignDecls
) where
import Data.Maybe
import Cryptol.Backend.FFI
import Cryptol.Backend.FFI.Error
import Cryptol.Eval
import Cryptol.ModuleSystem.Env
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.FFI.FFIType
#ifdef FFI_ENABLED
import Data.Either
import Data.Foldable
import Data.IORef
import Data.Maybe
import Data.Proxy
import Data.Traversable
import Data.Word
import Foreign
import Foreign.C.Types
import GHC.Float
import LibBF (bfFromDouble, bfToDouble,
pattern NearEven)
import System.Directory
import LibBF (bfFromDouble, bfToDouble,
pattern NearEven)
import Cryptol.Backend.Concrete
import Cryptol.Backend.FloatHelpers
@ -45,42 +48,36 @@ import Cryptol.Eval.Prims
import Cryptol.Eval.Type
import Cryptol.Eval.Value
import Cryptol.ModuleSystem.Name
import Cryptol.TypeCheck.FFI.FFIType
import Cryptol.Utils.Ident
import Cryptol.Utils.RecordMap
-- | Find all the foreign declarations in the module and add them to the
-- environment. This is a separate pass from the main evaluation functions in
-- "Cryptol.Eval" since it only works for the Concrete backend.
--
-- Note: 'Right' is only returned if we successfully loaded some foreign
-- functions and the environment was modified. If there were no foreign
-- declarations at all then @Left []@ is returned, so 'Left' does not
-- necessarily indicate an error.
evalForeignDecls :: ModulePath -> Module -> EvalEnv ->
Eval (Either [FFILoadError] (ForeignSrc, EvalEnv))
evalForeignDecls path m env = io
case mapMaybe getForeign $ mDecls m of
[] -> pure $ Left []
foreigns ->
case path of
InFile p -> canonicalizePath p >>= loadForeignSrc >>=
\case
Right fsrc -> collect <$> for foreigns \(name, ffiType) ->
fmap ((name,) . foreignPrimPoly name ffiType) <$>
loadForeignImpl fsrc (unpackIdent $ nameIdent name)
where collect (partitionEithers -> (errs, primMap))
| null errs = Right
(fsrc, foldr (uncurry bindVarDirect) env primMap)
| otherwise = Left errs
Left err -> pure $ Left [err]
-- We don't handle in-memory modules for now
InMem _ _ -> evalPanic "evalForeignDecls"
["Can't find foreign source of in-memory module"]
#endif
-- | Find all the foreign declarations in the module and return their names and
-- FFIFunTypes.
findForeignDecls :: Module -> [(Name, FFIFunType)]
findForeignDecls = mapMaybe getForeign . mDecls
where getForeign (NonRecursive Decl { dName, dDefinition = DForeign ffiType })
= Just (dName, ffiType)
-- Recursive DeclGroups can't have foreign decls
getForeign _ = Nothing
#ifdef FFI_ENABLED
-- | Add the given foreign declarations to the environment, loading their
-- implementations from the given 'ForeignSrc'. This is a separate pass from the
-- main evaluation functions in "Cryptol.Eval" since it only works for the
-- Concrete backend.
evalForeignDecls :: ForeignSrc -> [(Name, FFIFunType)] -> EvalEnv ->
Eval (Either [FFILoadError] EvalEnv)
evalForeignDecls fsrc decls env = io do
ePrims <- for decls \(name, ffiType) ->
fmap ((name,) . foreignPrimPoly name ffiType) <$>
loadForeignImpl fsrc (unpackIdent $ nameIdent name)
pure case partitionEithers ePrims of
([], prims) -> Right $ foldr (uncurry bindVarDirect) env prims
(errs, _) -> Left errs
-- | Generate a 'Prim' value representing the given foreign function, containing
-- all the code necessary to marshal arguments and return values and do the
-- actual FFI call.
@ -153,13 +150,21 @@ foreignPrim name FFIFunType {..} impl tenv = buildFun ffiArgTypes []
marshalArg (FFIBasic t) val f = getMarshalBasicArg t \m -> do
arg <- m val
f [SomeFFIArg arg]
marshalArg (FFIArray (evalFinType -> n) t) val f =
getMarshalBasicArg t \m -> do
args <- traverse (>>= m) $ enumerateSeqMap n $ fromVSeq val
-- Since we need to do an Eval action in an IO callback, we need to
-- manually unwrap and wrap the Eval datatype
marshalArg (FFIArray (map evalFinType -> sizes) t) val f =
getMarshalBasicArg t \m ->
-- Since we need to do Eval actions in an IO callback, we need to manually
-- unwrap and wrap the Eval datatype
Eval \stk ->
withArray args \ptr ->
allocaArray (fromInteger $ product sizes) \ptr -> do
-- Traverse the nested sequences and write the elements to the array
-- in order
let write (n:ns) !i v = do
vs <- traverse (runEval stk) $ enumerateSeqMap n $ fromVSeq v
foldlM (write ns) i vs
write [] !i v = do
runEval stk (m v) >>= pokeElemOff ptr i
pure (i + 1)
_ <- write sizes 0 val
runEval stk $ f [SomeFFIArg ptr]
marshalArg (FFITuple types) val f = do
vals <- sequence $ fromVTuple val
@ -177,17 +182,26 @@ foreignPrim name FFIFunType {..} impl tenv = buildFun ffiArgTypes []
go ((t, v):tvs) prevArgs = marshalArg t v \currArgs ->
go tvs (prevArgs ++ currArgs)
-- Given a FFIType and a GetRet, obtain a return value and convert it to a
-- Given an FFIType and a GetRet, obtain a return value and convert it to a
-- Cryptol value. The return value is obtained differently depending on the
-- FFIType.
marshalRet :: FFIType -> GetRet -> Eval (GenValue Concrete)
marshalRet FFIBool gr = VBit . toBool <$> io (getRetAsValue gr @Word8)
marshalRet (FFIBasic t) gr = getMarshalBasicRet t (io (getRetAsValue gr) >>=)
marshalRet (FFIArray (evalFinType -> n) t) gr = getMarshalBasicRet t \m ->
fmap (VSeq n . finiteSeqMap Concrete . map m) $
io $ allocaArray (fromInteger n) \ptr -> do
getRetAsOutArgs gr [SomeFFIArg ptr]
peekArray (fromInteger n) ptr
marshalRet (FFIArray (map evalFinType -> sizes) t) gr =
getMarshalBasicRet t \m ->
Eval \stk ->
allocaArray (fromInteger $ product sizes) \ptr -> do
getRetAsOutArgs gr [SomeFFIArg ptr]
let build (n:ns) !i = do
-- We need to be careful to actually run this here and not just
-- stick the IO action into the sequence with io, or else we
-- will read from the array after it is deallocated.
vs <- for [0 .. fromInteger n - 1] \j ->
build ns (i * fromInteger n + j)
pure $ VSeq n $ finiteSeqMap Concrete $ map pure vs
build [] !i = peekElemOff ptr i >>= runEval stk . m
build sizes 0
marshalRet (FFITuple types) gr = VTuple <$> marshalMultiRet types gr
marshalRet (FFIRecord typeMap) gr =
VRecord . recordFromFields . zip (displayOrder typeMap) <$>
@ -274,8 +288,8 @@ withWordType FFIWord64 f = f $ Proxy @Word64
-- | Dummy implementation for when FFI is disabled. Does not add anything to
-- the environment.
evalForeignDecls :: ModulePath -> Module -> EvalEnv ->
Eval (Either [FFILoadError] (ForeignSrc, EvalEnv))
evalForeignDecls _ _ _ = pure $ Left []
evalForeignDecls :: ForeignSrc -> [(Name, FFIFunType)] -> EvalEnv ->
Eval (Either [FFILoadError] EvalEnv)
evalForeignDecls _ _ env = pure $ Right env
#endif

37
src/Cryptol/ModuleSystem/Base.hs
View File

@ -19,7 +19,6 @@ module Cryptol.ModuleSystem.Base where
import qualified Control.Exception as X
import Control.Monad (unless,when)
import Data.Functor.Compose
import Data.Maybe (fromMaybe)
import Data.Monoid ((<>))
import Data.Text.Encoding (decodeUtf8')
@ -51,6 +50,7 @@ import Cryptol.ModuleSystem.Env (lookupModule
, meCoreLint, CoreLint(..)
, ModContext(..)
, ModulePath(..), modulePathLabel)
import Cryptol.Backend.FFI
import qualified Cryptol.Eval as E
import qualified Cryptol.Eval.Concrete as Concrete
import Cryptol.Eval.Concrete (Concrete(..))
@ -251,16 +251,11 @@ doLoadModule quiet isrc path fp pm0 =
let ?evalPrim = \i -> Right <$> Map.lookup i tbl
callStacks <- getCallStacks
let ?callStacks = callStacks
foreignSrc <-
if T.isParametrizedModule tcm
then pure Nothing
else (getCompose
<$> modifyEvalEnvM (fmap Compose . evalForeignDecls path tcm)
>>= \case
Left [] -> pure Nothing
Left errs -> ffiLoadErrors (T.mName tcm) errs
Right (foreignSrc, ()) -> pure (Just foreignSrc))
<* modifyEvalEnv (E.moduleEnv Concrete tcm)
foreignSrc <- if T.isParametrizedModule tcm
then pure Nothing
else evalForeign tcm
unless (T.isParametrizedModule tcm) $
modifyEvalEnv (E.moduleEnv Concrete tcm)
loadedModule path fp nameEnv foreignSrc tcm
return tcm
@ -274,7 +269,25 @@ doLoadModule quiet isrc path fp pm0 =
else notAParameterizedModule (T.mName tcm)
| otherwise = return tcm
evalForeign tcm
| null foreigns = pure Nothing
| otherwise = case path of
InFile p -> io (canonicalizePath p >>= loadForeignSrc) >>=
\case
Right fsrc -> do
unless quiet $
case getForeignSrcPath fsrc of
Just fpath -> withLogger logPutStrLn $
"Loading dynamic library " ++ takeFileName fpath
Nothing -> pure ()
modifyEvalEnvM (evalForeignDecls fsrc foreigns) >>=
\case
Right () -> pure $ Just fsrc
Left errs -> ffiLoadErrors (T.mName tcm) errs
Left err -> ffiLoadErrors (T.mName tcm) [err]
InMem m _ -> panic "doLoadModule"
["Can't find foreign source of in-memory module", m]
where foreigns = findForeignDecls tcm

14
src/Cryptol/TypeCheck/FFI.hs
View File

@ -8,6 +8,7 @@ module Cryptol.TypeCheck.FFI
( toFFIFunType
) where
import Data.Bifunctor
import Data.Containers.ListUtils
import Data.Either
@ -62,11 +63,14 @@ toFFIType t =
case t of
TCon (TC TCBit) [] -> Right ([], FFIBool)
(toFFIBasicType -> Just r) -> (\fbt -> ([], FFIBasic fbt)) <$> r
TCon (TC TCSeq) [sz, bt] ->
case toFFIBasicType bt of
Just (Right fbt) -> Right ([fin sz], FFIArray sz fbt)
Just (Left err) -> Left $ FFITypeError t $ FFIBadComponentTypes [err]
Nothing -> Left $ FFITypeError t FFIBadArrayType
TCon (TC TCSeq) _ ->
(\(szs, fbt) -> (map fin szs, FFIArray szs fbt)) <$> go t
where go (toFFIBasicType -> Just r) =
case r of
Right fbt -> Right ([], fbt)
Left err -> Left $ FFITypeError t $ FFIBadComponentTypes [err]
go (TCon (TC TCSeq) [sz, ty]) = first (sz:) <$> go ty
go _ = Left $ FFITypeError t FFIBadArrayType
TCon (TC (TCTuple _)) ts ->
case partitionEithers $ map toFFIType ts of
([], unzip -> (pss, fts)) -> Right (concat pss, FFITuple fts)

8
src/Cryptol/TypeCheck/FFI/Error.hs
View File

@ -71,12 +71,12 @@ instance PP (WithNames FFITypeErrorReason) where
, "Only Float32 and Float64 are supported" ]
FFIBadArrayType -> vcat
[ "Unsupported sequence element type"
, "Only words or floats are supported as the element type of sequences"
, "Only words or floats are supported as the element type of"
, "(possibly multidimensional) sequences"
]
FFIBadComponentTypes errs ->
indent 2 $ vcat $ map (ppWithNames names) errs
FFIBadType -> vcat
[ "Only Bit, words, floats, sequences of words or floats,"
, "or structs or tuples of the above are supported as FFI"
, "argument or return types"]
[ "Only Bit, words, floats, sequences, or structs or tuples"
, "of the above are supported as FFI argument or return types" ]
FFINotFunction -> "FFI binding must be a function"

13
src/Cryptol/TypeCheck/FFI/FFIType.hs
View File

@ -27,21 +27,20 @@ data FFIFunType = FFIFunType
data FFIType
= FFIBool
| FFIBasic FFIBasicType
| FFIArray
Type -- ^ Size (should be of kind @\#@)
FFIBasicType -- ^ Element type
-- | [n][m][p]T --> FFIArray [n, m, p] T
| FFIArray [Type] FFIBasicType
| FFITuple [FFIType]
| FFIRecord (RecordMap Ident FFIType)
deriving (Show, Generic, NFData)
-- | Types which can be elements of FFI sequences.
-- | Types which can be elements of FFI arrays.
data FFIBasicType
= FFIWord
Integer -- ^ The size of the Cryptol type
Integer -- ^ The size of the Cryptol type
FFIWordSize -- ^ The machine word size that it corresponds to
| FFIFloat
Integer -- ^ Exponent
Integer -- ^ Precision
Integer -- ^ Exponent
Integer -- ^ Precision
FFIFloatSize -- ^ The machine float size that it corresponds to
deriving (Show, Generic, NFData)

2
tests/ffi/ffi-reload.icry.stdout
View File

@ -1,7 +1,9 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
Loading dynamic library ffi-reload.so
False
Loading module Cryptol
Loading module Main
Loading dynamic library ffi-reload.so
True

9
tests/ffi/ffi-reload.icry.stdout.darwin Normal file
View File

@ -0,0 +1,9 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
Loading dynamic library ffi-reload.dylib
False
Loading module Cryptol
Loading module Main
Loading dynamic library ffi-reload.dylib
True

1
tests/ffi/ffi-runtime-errors.icry.stdout
View File

@ -1,6 +1,7 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
Loading dynamic library ffi-runtime-errors.so
numeric type argument to foreign function is too large: 18446744073709551616
in type parameter n`899 of function Main::f

29
tests/ffi/ffi-runtime-errors.icry.stdout.darwin Normal file
View File

@ -0,0 +1,29 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
Loading dynamic library ffi-runtime-errors.dylib
numeric type argument to foreign function is too large: 18446744073709551616
in type parameter n`899 of function Main::f
type arguments must fit in a C `size_t`
-- Backtrace --
Main::f called at ffi-runtime-errors.icry:4:1--4:2
cannot call foreign function Main::g
FFI calls are not supported in this context
If you are trying to evaluate an expression, try rebuilding
Cryptol with FFI support enabled.
cannot call foreign function Main::g
FFI calls are not supported in this context
If you are trying to evaluate an expression, try rebuilding
Cryptol with FFI support enabled.
cannot call foreign function Main::g
FFI calls are not supported in this context
If you are trying to evaluate an expression, try rebuilding
Cryptol with FFI support enabled.
cannot call foreign function Main::g
FFI calls are not supported in this context
If you are trying to evaluate an expression, try rebuilding
Cryptol with FFI support enabled.

3
tests/ffi/ffi-type-errors.cry
View File

@ -2,7 +2,8 @@ import Float
foreign badWordSizes : [65] -> [128]
foreign badFloatSizes : Float16 -> Float128
foreign badArrayTypes : {n} (fin n) => [n]Bit -> [n]([16], [16]) -> [n][4][8]
foreign badArrayTypes : {n} (fin n) =>
[n]Bit -> [n]([16], [16]) -> [n][4][8]{a : [n], b : [2]}
foreign badTypes : Integer -> Z 3
foreign notFunction : [32]
foreign badKind : {t} t -> [32]

44
tests/ffi/ffi-type-errors.icry.stdout
View File

@ -33,70 +33,72 @@ Loading module Main
Unsupported Float format
Only Float32 and Float64 are supported
When checking the type of 'Main::badFloatSizes'
[error] at ffi-type-errors.cry:5:9--5:78:
[error] at ffi-type-errors.cry:5:9--6:59:
Type unsupported for FFI:
[n`969] -> [n`969]([16], [16]) -> [n`969][4][8]
[n`969] -> [n`969]([16], [16]) -> [n`969][4][8]{a : [n`969],
b : [2]}
Due to:
Type unsupported for FFI:
[n`969]
Due to:
Unsupported sequence element type
Only words or floats are supported as the element type of sequences
Only words or floats are supported as the element type of
(possibly multidimensional) sequences
Type unsupported for FFI:
[n`969]([16], [16])
Due to:
Unsupported sequence element type
Only words or floats are supported as the element type of sequences
Only words or floats are supported as the element type of
(possibly multidimensional) sequences
Type unsupported for FFI:
[n`969][4][8]
[n`969][4][8]{a : [n`969], b : [2]}
Due to:
Unsupported sequence element type
Only words or floats are supported as the element type of sequences
Only words or floats are supported as the element type of
(possibly multidimensional) sequences
When checking the type of 'Main::badArrayTypes'
[error] at ffi-type-errors.cry:6:9--6:34:
[error] at ffi-type-errors.cry:7:9--7:34:
Type unsupported for FFI:
Integer -> Z 3
Due to:
Type unsupported for FFI:
Integer
Due to:
Only Bit, words, floats, sequences of words or floats,
or structs or tuples of the above are supported as FFI
argument or return types
Only Bit, words, floats, sequences, or structs or tuples
of the above are supported as FFI argument or return types
Type unsupported for FFI:
Z 3
Due to:
Only Bit, words, floats, sequences of words or floats,
or structs or tuples of the above are supported as FFI
argument or return types
Only Bit, words, floats, sequences, or structs or tuples
of the above are supported as FFI argument or return types
When checking the type of 'Main::badTypes'
[error] at ffi-type-errors.cry:7:9--7:27:
[error] at ffi-type-errors.cry:8:9--8:27:
Type unsupported for FFI:
[32]
Due to:
FFI binding must be a function
When checking the type of 'Main::notFunction'
[error] at ffi-type-errors.cry:8:9--8:32:
[error] at ffi-type-errors.cry:9:9--9:32:
Kind of type variable unsupported for FFI:
t`970 : *
Only type variables of kind # are supported
When checking the type of 'Main::badKind'
[error] at ffi-type-errors.cry:9:9--9:43:
[error] at ffi-type-errors.cry:10:9--10:43:
Failed to validate user-specified signature.
in the definition of 'Main::noFin', at ffi-type-errors.cry:9:9--9:14,
in the definition of 'Main::noFin', at ffi-type-errors.cry:10:9--10:14,
we need to show that
for any type n
the following constraints hold:
• fin n
arising from
declaration of foreign function Main::noFin
at ffi-type-errors.cry:9:9--9:43
[error] at ffi-type-errors.cry:10:9--10:34:
at ffi-type-errors.cry:10:9--10:43
[error] at ffi-type-errors.cry:11:9--11:34:
• Unsolvable constraint:
fin inf
arising from
declaration of foreign function Main::infSeq
at ffi-type-errors.cry:10:9--10:34
[error] at ffi-type-errors.cry:11:48--11:49:
at ffi-type-errors.cry:11:9--11:34
[error] at ffi-type-errors.cry:12:48--12:49:
Wild card types are not allowed in this context
(e.g., they cannot be used in type synonyms or FFI declarations).

6
tests/ffi/test-ffi.c
View File

@ -116,3 +116,9 @@ void zipMul3(size_t n, size_t m, size_t p, float *xs, float *ys, float *zs,
out[i] = xs[i] * ys[i] * zs[i];
}
}
void nestedSeq(size_t n, size_t m, size_t p, uint8_t *in, uint8_t *out) {
for (unsigned i = 0; i < n * m * p; ++i) {
out[i] = in[i];
}
}

4
tests/ffi/test-ffi.cry
View File

@ -38,3 +38,7 @@ foreign sumPoly : {n} (fin n) => [n]Word32 -> Word32
foreign inits : {n} (fin n) => [n][8] -> [n * (n + 1) / 2][8]
foreign zipMul3 : {n, m, p} (fin n, fin m, fin p) =>
[n]Float32 -> [m]Float32 -> [p]Float32 -> [min n (min m p)]Float32
// Nested sequences
foreign nestedSeq : {n, m, p} (fin n, fin m, fin p, n * m * p == 4 * 3 * 2) =>
[n][m][p][8] -> [4][3][2][8]

2
tests/ffi/test-ffi.icry
View File

@ -32,3 +32,5 @@ sumPoly [1..10]
sumPoly [1..10000]
inits [1..5]
zipMul3 [1, 2, 3] [3, 4, 5, 6] [6, 7, 8, 9, 10]
nestedSeq [split`{4} x | x <- split`{2} [1..24]]

5
tests/ffi/test-ffi.icry.stdout
View File

@ -2,6 +2,7 @@ Loading module Cryptol
Loading module Cryptol
Loading module Float
Loading module Main
Loading dynamic library test-ffi.so
0x03
0x15b4
0x3a0f1880
@ -31,3 +32,7 @@ True
[0x01, 0x01, 0x02, 0x01, 0x02, 0x03, 0x01, 0x02, 0x03, 0x04, 0x01,
0x02, 0x03, 0x04, 0x05]
[0x12.0, 0x38.0, 0x78.0]
[[[0x01, 0x02], [0x03, 0x04], [0x05, 0x06]],
[[0x07, 0x08], [0x09, 0x0a], [0x0b, 0x0c]],
[[0x0d, 0x0e], [0x0f, 0x10], [0x11, 0x12]],
[[0x13, 0x14], [0x15, 0x16], [0x17, 0x18]]]

38
tests/ffi/test-ffi.icry.stdout.darwin Normal file
View File

@ -0,0 +1,38 @@
Loading module Cryptol
Loading module Cryptol
Loading module Float
Loading module Main
Loading dynamic library test-ffi.dylib
0x03
0x15b4
0x3a0f1880
0x00000002e90edc8f
0x07
0x7
0x0
False
0x45.1eb8
-0x1e61.c71de69ad5
fpPosInf
fpNegInf
fpNaN
-0.0
True
0x00000037
[0xb.cd, -0x9.0a, 0x6.78, -0x3.45, 0x1.23]
{a = (0x1234, 0x5678),
b = {c = [0x0000a, 0x00014, 0x0001e, 0x00028, 0x00032, 0x0003c,
0x00046, 0x00050],
d = 0x09,
e = 0x0c}}
0x12345678deadbeef
0x00000000
0x00000037
0x02fb0408
[0x01, 0x01, 0x02, 0x01, 0x02, 0x03, 0x01, 0x02, 0x03, 0x04, 0x01,
0x02, 0x03, 0x04, 0x05]
[0x12.0, 0x38.0, 0x78.0]
[[[0x01, 0x02], [0x03, 0x04], [0x05, 0x06]],
[[0x07, 0x08], [0x09, 0x0a], [0x0b, 0x0c]],
[[0x0d, 0x0e], [0x0f, 0x10], [0x11, 0x12]],
[[0x13, 0x14], [0x15, 0x16], [0x17, 0x18]]]