From 0a8fdf572477726f254ed30fda0fd1313b464d88 Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Wed, 17 Jan 2024 11:51:40 -0800 Subject: [PATCH] Bump submodules. (#2011) * Bump submodules. * CI: Regenerate cabal.GHC-*.config files * Address comments. * Fix tests. * Revert "Fix tests." This reverts commit b7ef1a1a1ce252ccc703f200ef20445a7f86e2a3. * Revert cryptol-specs bump. --------- Co-authored-by: Ryan Scott --- cabal.GHC-9.2.8.config | 51 ++++++++++--------- cabal.GHC-9.4.8.config | 51 ++++++++++--------- cabal.GHC-9.6.3.config | 51 ++++++++++--------- deps/crucible | 2 +- deps/elf-edit | 2 +- deps/llvm-pretty | 2 +- deps/llvm-pretty-bc-parser | 2 +- deps/macaw | 2 +- deps/what4 | 2 +- .../Verifier/SAW/Heapster/LLVMGlobalConst.hs | 9 ++-- src/SAWScript/Crucible/LLVM/Builtins.hs | 14 ++--- src/SAWScript/Crucible/LLVM/MethodSpecIR.hs | 6 +-- src/SAWScript/Crucible/LLVM/Setup/Value.hs | 12 +++-- src/SAWScript/HeapsterBuiltins.hs | 4 +- src/SAWScript/Value.hs | 4 +- 15 files changed, 110 insertions(+), 104 deletions(-) diff --git a/cabal.GHC-9.2.8.config b/cabal.GHC-9.2.8.config index 8e9e5cad34..56547308e5 100644 --- a/cabal.GHC-9.2.8.config +++ b/cabal.GHC-9.2.8.config @@ -20,8 +20,8 @@ constraints: any.BoundedChan ==1.0.3.0, aeson -cffi +ordered-keymap, any.aeson-pretty ==0.8.10, aeson-pretty -lib-only, - any.alex ==3.4.0.1, - any.ansi-terminal ==0.11.5, + any.alex ==3.5.0.0, + any.ansi-terminal ==1.0.2, ansi-terminal -example, any.ansi-terminal-types ==0.11.5, any.ansi-wl-pprint ==0.6.9, @@ -34,7 +34,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.asn1-types ==0.3.4, any.assoc ==1.1, assoc +tagged, - any.async ==2.2.4, + any.async ==2.2.5, async -bench, any.attoparsec ==0.14.4, attoparsec -developer, @@ -59,7 +59,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.blaze-builder ==0.4.2.3, any.blaze-html ==0.9.1.2, any.blaze-markup ==0.8.3.0, - any.boomerang ==1.4.9, + any.boomerang ==1.4.9.1, any.bsb-http-chunked ==0.0.0.4, any.bv-sized ==1.0.5, any.byteorder ==1.0.4, @@ -74,7 +74,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.cborg-json ==0.2.6.0, any.cereal ==0.5.8.3, cereal -bytestring-builder, - any.chimera ==0.3.4.0, + any.chimera ==0.4.0.0, chimera +representable, any.clock ==0.8.4, clock -llvm, @@ -170,7 +170,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.ghc-prim ==0.8.0, any.ghci ==9.2.8, any.gitrev ==1.3.1, - any.graphviz ==2999.20.1.0, + any.graphviz ==2999.20.2.0, graphviz -test-parsing, any.half ==0.3.1, any.happy ==1.20.1.1, @@ -182,7 +182,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.haskell-lexer ==1.1.1, any.haskell-src-exts ==1.23.1, any.haskell-src-meta ==0.8.13, - any.hedgehog ==1.2, + any.hedgehog ==1.4, any.hedgehog-classes ==0.2.5.4, hedgehog-classes +aeson +comonad +primitive +semirings +vector, any.heredoc ==0.2.0.0, @@ -199,14 +199,14 @@ constraints: any.BoundedChan ==1.0.3.0, any.hspec-discover ==2.11.7, any.hspec-expectations ==0.8.4, any.http-date ==0.0.11, - any.http-types ==0.12.3, - any.http2 ==4.2.2, + any.http-types ==0.12.4, + any.http2 ==5.0.1, http2 -devel -h2spec, 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.infinite-list ==0.1, + any.infinite-list ==0.1.1, any.integer-gmp ==1.1, any.integer-logarithms ==1.0.3.1, integer-logarithms -check-bounds +integer-gmp, @@ -223,12 +223,12 @@ constraints: any.BoundedChan ==1.0.3.0, any.kan-extensions ==5.2.5, any.kvitable ==1.0.2.1, any.language-c99 ==0.2.0, - any.language-c99-simple ==0.2.3, + any.language-c99-simple ==0.3.0, any.language-c99-util ==0.2.0, language-rust +enablequasiquotes +usebytestrings, any.lens ==5.2.3, lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.6, + any.libBF ==0.6.7, libBF -system-libbf, any.libffi ==0.2.1, libffi +ghc-bundled-libffi, @@ -243,7 +243,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.lumberjack ==1.0.3.0, any.math-functions ==0.3.4.3, math-functions +system-erf +system-expm1, - any.megaparsec ==9.3.1, + any.megaparsec ==9.6.1, megaparsec -dev, any.memory ==0.18.0, memory +support_bytestring +support_deepseq, @@ -263,11 +263,12 @@ constraints: any.BoundedChan ==1.0.3.0, any.network ==3.1.4.0, network -devel, any.network-byte-order ==0.1.7, + any.network-control ==0.0.2, any.network-info ==0.2.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, + any.old-time ==1.1.0.4, any.optparse-applicative ==0.18.1.0, optparse-applicative +process, any.ordered-containers ==0.2.3, @@ -305,7 +306,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.19, + any.safe ==0.3.20, any.safe-exceptions ==0.1.7.4, any.sbv ==10.2, any.scientific ==0.3.7.0, @@ -327,7 +328,7 @@ constraints: any.BoundedChan ==1.0.3.0, simple-sendfile +allow-bsd -fallback, any.simple-smt ==0.9.7, any.smallcheck ==1.2.1.1, - any.split ==0.2.4, + any.split ==0.2.5, any.splitmix ==0.1.0.5, splitmix -optimised-mixer, any.statistics ==0.16.2.1, @@ -347,7 +348,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.tasty-expected-failure ==0.12.3, any.tasty-golden ==2.3.5, tasty-golden -build-example, - any.tasty-hedgehog ==1.4.0.1, + 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.2, @@ -390,12 +391,12 @@ constraints: any.BoundedChan ==1.0.3.0, any.unbounded-delays ==0.1.1.1, any.uniplate ==1.6.13, any.unix ==2.7.2.2, - any.unix-compat ==0.7, + any.unix-compat ==0.7.1, unix-compat -old-time, any.unix-time ==0.4.11, any.unliftio ==0.2.25.0, any.unliftio-core ==0.2.1.0, - any.unordered-containers ==0.2.19.1, + any.unordered-containers ==0.2.20, unordered-containers -debug, any.utf8-string ==1.0.2, any.uuid ==1.3.15, @@ -407,16 +408,16 @@ constraints: any.BoundedChan ==1.0.3.0, 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-stream ==0.1.0.0, + any.vector-stream ==0.1.0.1, any.vector-th-unbox ==0.2.2, - any.versions ==5.0.5, + any.versions ==6.0.4, any.void ==0.7.3, void -safe, - any.wai ==3.2.3, - any.wai-extra ==3.1.13.0, + any.wai ==3.2.4, + any.wai-extra ==3.1.14, wai-extra -build-example, any.wai-logger ==2.4.0, - any.warp ==3.3.30, + any.warp ==3.3.31, warp +allow-sendfilefd -network-bytestring -warp-debug +x509, any.warp-tls ==3.4.3, any.weigh ==0.0.17, @@ -432,4 +433,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 2023-11-20T16:07:24Z +index-state: hackage.haskell.org 2024-01-15T23:27:26Z diff --git a/cabal.GHC-9.4.8.config b/cabal.GHC-9.4.8.config index ba4f1fa561..97c2fc01e3 100644 --- a/cabal.GHC-9.4.8.config +++ b/cabal.GHC-9.4.8.config @@ -21,8 +21,8 @@ constraints: any.BoundedChan ==1.0.3.0, aeson -cffi +ordered-keymap, any.aeson-pretty ==0.8.10, aeson-pretty -lib-only, - any.alex ==3.4.0.1, - any.ansi-terminal ==0.11.5, + any.alex ==3.5.0.0, + any.ansi-terminal ==1.0.2, ansi-terminal -example, any.ansi-terminal-types ==0.11.5, any.ansi-wl-pprint ==0.6.9, @@ -35,7 +35,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.asn1-types ==0.3.4, any.assoc ==1.1, assoc +tagged, - any.async ==2.2.4, + any.async ==2.2.5, async -bench, any.attoparsec ==0.14.4, attoparsec -developer, @@ -60,7 +60,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.blaze-builder ==0.4.2.3, any.blaze-html ==0.9.1.2, any.blaze-markup ==0.8.3.0, - any.boomerang ==1.4.9, + any.boomerang ==1.4.9.1, any.bsb-http-chunked ==0.0.0.4, any.bv-sized ==1.0.5, any.byteorder ==1.0.4, @@ -75,7 +75,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.cborg-json ==0.2.6.0, any.cereal ==0.5.8.3, cereal -bytestring-builder, - any.chimera ==0.3.4.0, + any.chimera ==0.4.0.0, chimera +representable, any.clock ==0.8.4, clock -llvm, @@ -170,7 +170,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.ghc-prim ==0.9.1, any.ghci ==9.4.8, any.gitrev ==1.3.1, - any.graphviz ==2999.20.1.0, + any.graphviz ==2999.20.2.0, graphviz -test-parsing, any.half ==0.3.1, any.happy ==1.20.1.1, @@ -182,7 +182,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.haskell-lexer ==1.1.1, any.haskell-src-exts ==1.23.1, any.haskell-src-meta ==0.8.13, - any.hedgehog ==1.2, + any.hedgehog ==1.4, any.hedgehog-classes ==0.2.5.4, hedgehog-classes +aeson +comonad +primitive +semirings +vector, any.heredoc ==0.2.0.0, @@ -199,14 +199,14 @@ constraints: any.BoundedChan ==1.0.3.0, any.hspec-discover ==2.11.7, any.hspec-expectations ==0.8.4, any.http-date ==0.0.11, - any.http-types ==0.12.3, - any.http2 ==4.2.2, + any.http-types ==0.12.4, + any.http2 ==5.0.1, http2 -devel -h2spec, 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.infinite-list ==0.1, + any.infinite-list ==0.1.1, any.integer-gmp ==1.1, any.integer-logarithms ==1.0.3.1, integer-logarithms -check-bounds +integer-gmp, @@ -223,12 +223,12 @@ constraints: any.BoundedChan ==1.0.3.0, any.kan-extensions ==5.2.5, any.kvitable ==1.0.2.1, any.language-c99 ==0.2.0, - any.language-c99-simple ==0.2.3, + any.language-c99-simple ==0.3.0, any.language-c99-util ==0.2.0, language-rust +enablequasiquotes +usebytestrings, any.lens ==5.2.3, lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.6, + any.libBF ==0.6.7, libBF -system-libbf, any.libffi ==0.2.1, libffi +ghc-bundled-libffi, @@ -243,7 +243,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.lumberjack ==1.0.3.0, any.math-functions ==0.3.4.3, math-functions +system-erf +system-expm1, - any.megaparsec ==9.3.1, + any.megaparsec ==9.6.1, megaparsec -dev, any.memory ==0.18.0, memory +support_bytestring +support_deepseq, @@ -263,11 +263,12 @@ constraints: any.BoundedChan ==1.0.3.0, any.network ==3.1.4.0, network -devel, any.network-byte-order ==0.1.7, + any.network-control ==0.0.2, any.network-info ==0.2.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, + any.old-time ==1.1.0.4, any.optparse-applicative ==0.18.1.0, optparse-applicative +process, any.ordered-containers ==0.2.3, @@ -305,7 +306,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.19, + any.safe ==0.3.20, any.safe-exceptions ==0.1.7.4, any.sbv ==10.2, any.scientific ==0.3.7.0, @@ -327,7 +328,7 @@ constraints: any.BoundedChan ==1.0.3.0, simple-sendfile +allow-bsd -fallback, any.simple-smt ==0.9.7, any.smallcheck ==1.2.1.1, - any.split ==0.2.4, + any.split ==0.2.5, any.splitmix ==0.1.0.5, splitmix -optimised-mixer, any.statistics ==0.16.2.1, @@ -347,7 +348,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.tasty-expected-failure ==0.12.3, any.tasty-golden ==2.3.5, tasty-golden -build-example, - any.tasty-hedgehog ==1.4.0.1, + 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.2, @@ -390,12 +391,12 @@ constraints: any.BoundedChan ==1.0.3.0, any.unbounded-delays ==0.1.1.1, any.uniplate ==1.6.13, any.unix ==2.7.3, - any.unix-compat ==0.7, + any.unix-compat ==0.7.1, unix-compat -old-time, any.unix-time ==0.4.11, any.unliftio ==0.2.25.0, any.unliftio-core ==0.2.1.0, - any.unordered-containers ==0.2.19.1, + any.unordered-containers ==0.2.20, unordered-containers -debug, any.utf8-string ==1.0.2, any.uuid ==1.3.15, @@ -407,16 +408,16 @@ constraints: any.BoundedChan ==1.0.3.0, 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-stream ==0.1.0.0, + any.vector-stream ==0.1.0.1, any.vector-th-unbox ==0.2.2, - any.versions ==5.0.5, + any.versions ==6.0.4, any.void ==0.7.3, void -safe, - any.wai ==3.2.3, - any.wai-extra ==3.1.13.0, + any.wai ==3.2.4, + any.wai-extra ==3.1.14, wai-extra -build-example, any.wai-logger ==2.4.0, - any.warp ==3.3.30, + any.warp ==3.3.31, warp +allow-sendfilefd -network-bytestring -warp-debug +x509, any.warp-tls ==3.4.3, any.weigh ==0.0.17, @@ -432,4 +433,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 2023-11-20T16:07:24Z +index-state: hackage.haskell.org 2024-01-15T23:27:26Z diff --git a/cabal.GHC-9.6.3.config b/cabal.GHC-9.6.3.config index 2930e65284..a942452b35 100644 --- a/cabal.GHC-9.6.3.config +++ b/cabal.GHC-9.6.3.config @@ -21,8 +21,8 @@ constraints: any.BoundedChan ==1.0.3.0, aeson -cffi +ordered-keymap, any.aeson-pretty ==0.8.10, aeson-pretty -lib-only, - any.alex ==3.4.0.1, - any.ansi-terminal ==0.11.5, + any.alex ==3.5.0.0, + any.ansi-terminal ==1.0.2, ansi-terminal -example, any.ansi-terminal-types ==0.11.5, any.ansi-wl-pprint ==0.6.9, @@ -35,7 +35,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.asn1-types ==0.3.4, any.assoc ==1.1, assoc +tagged, - any.async ==2.2.4, + any.async ==2.2.5, async -bench, any.attoparsec ==0.14.4, attoparsec -developer, @@ -60,7 +60,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.blaze-builder ==0.4.2.3, any.blaze-html ==0.9.1.2, any.blaze-markup ==0.8.3.0, - any.boomerang ==1.4.9, + any.boomerang ==1.4.9.1, any.bsb-http-chunked ==0.0.0.4, any.bv-sized ==1.0.5, any.byteorder ==1.0.4, @@ -75,7 +75,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.cborg-json ==0.2.6.0, any.cereal ==0.5.8.3, cereal -bytestring-builder, - any.chimera ==0.3.4.0, + any.chimera ==0.4.0.0, chimera +representable, any.clock ==0.8.4, clock -llvm, @@ -168,7 +168,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.ghc-prim ==0.10.0, any.ghci ==9.6.3, any.gitrev ==1.3.1, - any.graphviz ==2999.20.1.0, + any.graphviz ==2999.20.2.0, graphviz -test-parsing, any.half ==0.3.1, any.happy ==1.20.1.1, @@ -180,7 +180,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.haskell-lexer ==1.1.1, any.haskell-src-exts ==1.23.1, any.haskell-src-meta ==0.8.13, - any.hedgehog ==1.2, + any.hedgehog ==1.4, any.hedgehog-classes ==0.2.5.4, hedgehog-classes +aeson +comonad +primitive +semirings +vector, any.heredoc ==0.2.0.0, @@ -197,14 +197,14 @@ constraints: any.BoundedChan ==1.0.3.0, any.hspec-discover ==2.11.7, any.hspec-expectations ==0.8.4, any.http-date ==0.0.11, - any.http-types ==0.12.3, - any.http2 ==4.2.2, + any.http-types ==0.12.4, + any.http2 ==5.0.1, http2 -devel -h2spec, 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.infinite-list ==0.1, + any.infinite-list ==0.1.1, any.integer-gmp ==1.1, any.integer-logarithms ==1.0.3.1, integer-logarithms -check-bounds +integer-gmp, @@ -221,12 +221,12 @@ constraints: any.BoundedChan ==1.0.3.0, any.kan-extensions ==5.2.5, any.kvitable ==1.0.2.1, any.language-c99 ==0.2.0, - any.language-c99-simple ==0.2.3, + any.language-c99-simple ==0.3.0, any.language-c99-util ==0.2.0, language-rust +enablequasiquotes +usebytestrings, any.lens ==5.2.3, lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.6, + any.libBF ==0.6.7, libBF -system-libbf, any.libffi ==0.2.1, libffi +ghc-bundled-libffi, @@ -241,7 +241,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.lumberjack ==1.0.3.0, any.math-functions ==0.3.4.3, math-functions +system-erf +system-expm1, - any.megaparsec ==9.3.1, + any.megaparsec ==9.6.1, megaparsec -dev, any.memory ==0.18.0, memory +support_bytestring +support_deepseq, @@ -261,11 +261,12 @@ constraints: any.BoundedChan ==1.0.3.0, any.network ==3.1.4.0, network -devel, any.network-byte-order ==0.1.7, + any.network-control ==0.0.2, any.network-info ==0.2.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, + any.old-time ==1.1.0.4, any.optparse-applicative ==0.18.1.0, optparse-applicative +process, any.ordered-containers ==0.2.3, @@ -303,7 +304,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.19, + any.safe ==0.3.20, any.safe-exceptions ==0.1.7.4, any.sbv ==10.2, any.scientific ==0.3.7.0, @@ -325,7 +326,7 @@ constraints: any.BoundedChan ==1.0.3.0, simple-sendfile +allow-bsd -fallback, any.simple-smt ==0.9.7, any.smallcheck ==1.2.1.1, - any.split ==0.2.4, + any.split ==0.2.5, any.splitmix ==0.1.0.5, splitmix -optimised-mixer, any.statistics ==0.16.2.1, @@ -345,7 +346,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.tasty-expected-failure ==0.12.3, any.tasty-golden ==2.3.5, tasty-golden -build-example, - any.tasty-hedgehog ==1.4.0.1, + 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.2, @@ -388,12 +389,12 @@ constraints: any.BoundedChan ==1.0.3.0, any.unbounded-delays ==0.1.1.1, any.uniplate ==1.6.13, any.unix ==2.8.1.0, - any.unix-compat ==0.7, + any.unix-compat ==0.7.1, unix-compat -old-time, any.unix-time ==0.4.11, any.unliftio ==0.2.25.0, any.unliftio-core ==0.2.1.0, - any.unordered-containers ==0.2.19.1, + any.unordered-containers ==0.2.20, unordered-containers -debug, any.utf8-string ==1.0.2, any.uuid ==1.3.15, @@ -405,16 +406,16 @@ constraints: any.BoundedChan ==1.0.3.0, 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-stream ==0.1.0.0, + any.vector-stream ==0.1.0.1, any.vector-th-unbox ==0.2.2, - any.versions ==5.0.5, + any.versions ==6.0.4, any.void ==0.7.3, void -safe, - any.wai ==3.2.3, - any.wai-extra ==3.1.13.0, + any.wai ==3.2.4, + any.wai-extra ==3.1.14, wai-extra -build-example, any.wai-logger ==2.4.0, - any.warp ==3.3.30, + any.warp ==3.3.31, warp +allow-sendfilefd -network-bytestring -warp-debug +x509, any.warp-tls ==3.4.3, any.weigh ==0.0.17, @@ -430,4 +431,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 2023-11-20T16:07:24Z +index-state: hackage.haskell.org 2024-01-15T23:27:26Z diff --git a/deps/crucible b/deps/crucible index dba7b1be42..c4e01c5306 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit dba7b1be429554bcedc82514defd0c40df41392e +Subproject commit c4e01c5306e4af2aacc860fd1201cc3a4f8188f4 diff --git a/deps/elf-edit b/deps/elf-edit index 3ba7d7148a..fa665faeeb 160000 --- a/deps/elf-edit +++ b/deps/elf-edit @@ -1 +1 @@ -Subproject commit 3ba7d7148adc6029b0046229c4fecbb9ee048f9b +Subproject commit fa665faeeb02211a76fbf6eb06fb75bed934dc48 diff --git a/deps/llvm-pretty b/deps/llvm-pretty index 94e384842b..34cf64c697 160000 --- a/deps/llvm-pretty +++ b/deps/llvm-pretty @@ -1 +1 @@ -Subproject commit 94e384842b214ba72446d1694446fb5261ab6ce2 +Subproject commit 34cf64c69700020667fcd440bc3490af0a165962 diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser index ac9fff49ef..39b4a5ff26 160000 --- a/deps/llvm-pretty-bc-parser +++ b/deps/llvm-pretty-bc-parser @@ -1 +1 @@ -Subproject commit ac9fff49ef1670e58be9ce90075eaa02726f8662 +Subproject commit 39b4a5ff26ad88f7db250185cc5b471fac50141d diff --git a/deps/macaw b/deps/macaw index 299c227a77..9d8cdcc587 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit 299c227a77cbad480175e64f8ef2ae27070eb7ad +Subproject commit 9d8cdcc58746f65dde96118162ad3ad6c6c845bb diff --git a/deps/what4 b/deps/what4 index 28744e48e0..e46dff4209 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit 28744e48e01dc9c35d5aeebb914a9bb425cfe0f1 +Subproject commit e46dff42096550d860d210bd9cf6e435d8cd7ce5 diff --git a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs index ee0906ee1e..da6e07c0bb 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs @@ -30,6 +30,7 @@ import Data.Parameterized.Some import Lang.Crucible.Types import Lang.Crucible.LLVM.DataLayout import Lang.Crucible.LLVM.MemModel +import Lang.Crucible.LLVM.PrettyPrint import Verifier.SAW.OpenTerm import Verifier.SAW.Term.Functor (ModuleName) @@ -86,12 +87,12 @@ traceAndZeroM msg = -- | Helper function to pretty-print the value of a global ppLLVMValue :: L.Value -> String ppLLVMValue val = - L.withConfig (L.Config True True True) (show $ PPHPJ.nest 2 $ L.ppValue val) + show $ PPHPJ.nest 2 $ ppValue val -- | Helper function to pretty-print an LLVM constant expression ppLLVMConstExpr :: L.ConstExpr -> String ppLLVMConstExpr ce = - L.withConfig (L.Config True True True) (show $ PPHPJ.nest 2 $ L.ppConstExpr ce) + ppLLVMLatest (show $ PPHPJ.nest 2 $ L.ppConstExpr ce) -- | Translate a typed LLVM 'L.Value' to a Heapster shape + an element of the -- translation of that shape to a SAW core type @@ -182,7 +183,7 @@ translateLLVMType _ (L.PrimType (L.Integer n)) (bvTypeOpenTerm n)) translateLLVMType _ tp = traceAndZeroM ("translateLLVMType does not yet handle:\n" - ++ show (L.ppType tp)) + ++ show (ppType tp)) -- | Helper function for 'translateLLVMValue' applied to a constant expression translateLLVMConstExpr :: (1 <= w, KnownNat w) => NatRepr w -> L.ConstExpr -> @@ -251,7 +252,7 @@ translateZeroInit w (L.PackedStruct tps) = translateZeroInit _ tp = traceAndZeroM ("translateZeroInit cannot handle type:\n" - ++ show (L.ppType tp)) + ++ show (ppType tp)) -- | Top-level call to 'translateLLVMValue', running the 'LLVMTransM' monad translateLLVMValueTop :: (1 <= w, KnownNat w) => DebugLevel -> EndianForm -> diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 1a6d914e2f..d31f8e6f1f 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -124,7 +124,6 @@ import qualified Data.Vector as V import Prettyprinter import System.IO import qualified Text.LLVM.AST as L -import qualified Text.LLVM.PP as L (ppType, ppSymbol) import Text.URI import qualified Control.Monad.Trans.Maybe as MaybeT @@ -167,6 +166,7 @@ import qualified Lang.Crucible.LLVM.Bytes as Crucible import qualified Lang.Crucible.LLVM.Intrinsics as Crucible import qualified Lang.Crucible.LLVM.MemModel as Crucible import qualified Lang.Crucible.LLVM.MemType as Crucible +import qualified Lang.Crucible.LLVM.PrettyPrint as Crucible import Lang.Crucible.LLVM.QQ( llvmOvr ) import qualified Lang.Crucible.LLVM.Translation as Crucible @@ -231,13 +231,13 @@ displayVerifExceptionOpts opts (DefNotFound (L.Symbol nm) nms) = [ "Could not find definition for function named `" ++ nm ++ "`." ] ++ if simVerbose opts < 3 then [ "Run SAW with --sim-verbose=3 to see all function names" ] - else "Available function names:" : map ((" " ++) . show . L.ppSymbol) nms + else "Available function names:" : map ((" " ++) . show . Crucible.ppSymbol) nms displayVerifExceptionOpts opts (DeclNotFound (L.Symbol nm) nms) = unlines $ [ "Could not find declaration for function named `" ++ nm ++ "`." ] ++ if simVerbose opts < 3 then [ "Run SAW with --sim-verbose=3 to see all function names" ] - else "Available function names:" : map ((" " ++) . show . L.ppSymbol) nms + else "Available function names:" : map ((" " ++) . show . Crucible.ppSymbol) nms displayVerifExceptionOpts _ (SetupError e) = "Error during simulation setup: " ++ show (ppSetupError e) @@ -1825,7 +1825,7 @@ handleTranslationWarning :: Options -> Crucible.LLVMTranslationWarning -> IO () handleTranslationWarning opts (Crucible.LLVMTranslationWarning s p msg) = printOutLn opts Warn $ unwords [ "LLVM bitcode translation warning" - , show (L.ppSymbol s) + , show (Crucible.ppSymbol s) , show p , Text.unpack msg ] @@ -2163,7 +2163,7 @@ llvm_fresh_var name lty = sc <- lift $ lift getSharedContext let dl = Crucible.llvmDataLayout (ccTypeCtx cctx) case cryptolTypeOfActual dl lty' of - Nothing -> throwCrucibleSetup loc $ "Unsupported type in llvm_fresh_var: " ++ show (L.ppType lty) + Nothing -> throwCrucibleSetup loc $ "Unsupported type in llvm_fresh_var: " ++ show (Crucible.ppType lty) Just cty -> Setup.freshVariable sc name cty llvm_fresh_cryptol_var :: @@ -2261,7 +2261,7 @@ memTypeForLLVMType loc lty = case Crucible.liftMemType lty of Right m -> return m Left err -> throwCrucibleSetup loc $ unlines - [ "unsupported type: " ++ show (L.ppType lty) + [ "unsupported type: " ++ show (Crucible.ppType lty) , "Details:" , err ] @@ -2277,7 +2277,7 @@ llvm_sizeof (Some lm) lty = case Crucible.liftMemType lty of Right mty -> pure (Crucible.bytesToInteger (Crucible.memTypeSize dl mty)) Left err -> fail $ unlines - [ "llvm_sizeof: Unsupported type: " ++ show (L.ppType lty) + [ "llvm_sizeof: Unsupported type: " ++ show (Crucible.ppType lty) , "Details:" , err ] diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index f627d36508..058fc3545d 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -121,7 +121,6 @@ import Data.Functor.Compose (Compose(..)) import qualified Data.Map as Map import qualified Prettyprinter as PPL import qualified Text.LLVM.AST as L -import qualified Text.LLVM.PP as L import Data.Parameterized.All (All(All)) import Data.Parameterized.Some (Some(Some)) @@ -132,6 +131,7 @@ import What4.ProgramLoc (ProgramLoc) import qualified Lang.Crucible.Types as Crucible (SymbolRepr, knownSymbol) import qualified Lang.Crucible.Simulator.Intrinsics as Crucible (IntrinsicMuxFn(IntrinsicMuxFn)) +import qualified Lang.Crucible.LLVM.PrettyPrint as Crucible.LLVM import SAWScript.Crucible.Common import qualified SAWScript.Crucible.Common.MethodSpec as MS @@ -243,11 +243,11 @@ data SetupError ppSetupError :: SetupError -> PPL.Doc ann ppSetupError (InvalidReturnType t) = PPL.pretty "Can't lift return type" PPL.<+> - PPL.viaShow (L.ppType t) PPL.<+> + PPL.viaShow (Crucible.LLVM.ppType t) PPL.<+> PPL.pretty "to a Crucible type." ppSetupError (InvalidArgTypes ts) = PPL.pretty "Can't lift argument types " PPL.<+> - PPL.encloseSep PPL.lparen PPL.rparen PPL.comma (map (PPL.viaShow . L.ppType) ts) PPL.<+> + PPL.encloseSep PPL.lparen PPL.rparen PPL.comma (map (PPL.viaShow . Crucible.LLVM.ppType) ts) PPL.<+> PPL.pretty "to Crucible types." resolveArgs :: diff --git a/src/SAWScript/Crucible/LLVM/Setup/Value.hs b/src/SAWScript/Crucible/LLVM/Setup/Value.hs index 2f9133e03f..5e115647b6 100644 --- a/src/SAWScript/Crucible/LLVM/Setup/Value.hs +++ b/src/SAWScript/Crucible/LLVM/Setup/Value.hs @@ -83,6 +83,7 @@ module SAWScript.Crucible.LLVM.Setup.Value import Control.Lens import Data.Map ( Map ) import qualified Data.Map as Map +import Data.Maybe import qualified Data.Text as Text import Data.Type.Equality (TestEquality(..)) import Data.Void (Void) @@ -100,6 +101,7 @@ import What4.ProgramLoc (ProgramLoc) import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator) import qualified Lang.Crucible.Simulator.ExecutionTree as Crucible (SimContext) import qualified Lang.Crucible.Simulator.GlobalState as Crucible (SymGlobalState) +import qualified Lang.Crucible.LLVM.PrettyPrint as Crucible.LLVM import SAWScript.Crucible.Common import qualified SAWScript.Crucible.Common.Setup.Value as Setup @@ -236,19 +238,19 @@ showLLVMModule :: LLVMModule arch -> String showLLVMModule (LLVMModule name m _) = unlines [ "Module: " ++ name , "Types:" - , showParts L.ppTypeDecl (L.modTypes m) + , showParts (Crucible.LLVM.ppLLVMLatest L.ppTypeDecl) (L.modTypes m) , "Globals:" - , showParts ppGlobal' (L.modGlobals m) + , showParts (Crucible.LLVM.ppLLVMLatest ppGlobal') (L.modGlobals m) , "External references:" - , showParts L.ppDeclare (L.modDeclares m) + , showParts Crucible.LLVM.ppDeclare (L.modDeclares m) , "Definitions:" - , showParts ppDefine' (L.modDefines m) + , showParts (Crucible.LLVM.ppLLVMLatest ppDefine') (L.modDefines m) ] where showParts pp xs = unlines $ map (show . PP.nest 2 . pp) xs ppGlobal' g = L.ppSymbol (L.globalSym g) PP.<+> PP.char '=' PP.<+> - L.ppGlobalAttrs (L.globalAttrs g) PP.<+> + L.ppGlobalAttrs (isJust $ L.globalValue g) (L.globalAttrs g) PP.<+> L.ppType (L.globalType g) ppDefine' d = L.ppMaybe L.ppLinkage (L.defLinkage d) PP.<+> diff --git a/src/SAWScript/HeapsterBuiltins.hs b/src/SAWScript/HeapsterBuiltins.hs index 491b4c75e4..cfc1508c78 100644 --- a/src/SAWScript/HeapsterBuiltins.hs +++ b/src/SAWScript/HeapsterBuiltins.hs @@ -101,6 +101,7 @@ import Lang.Crucible.FunctionHandle import Lang.Crucible.CFG.Core import Lang.Crucible.LLVM.Extension import Lang.Crucible.LLVM.MemModel +import qualified Lang.Crucible.LLVM.PrettyPrint as Crucible.LLVM import Lang.Crucible.LLVM.Translation -- import Lang.Crucible.LLVM.Translation.Types import Lang.Crucible.LLVM.TypeContext @@ -108,7 +109,6 @@ import Lang.Crucible.LLVM.DataLayout import qualified Text.LLVM.AST as L import qualified Text.LLVM.Parser as L -import qualified Text.LLVM.PP as L import qualified Text.PrettyPrint.HughesPJ as L (render) import SAWScript.TopLevel @@ -973,7 +973,7 @@ heapster_find_symbol_commands _bic _opts henv str = return $ concatMap (\tp -> "heapster_find_symbol_with_type env\n \"" ++ str ++ "\"\n " ++ - print_as_saw_script_string (L.render $ L.ppType tp) ++ ";\n") $ + print_as_saw_script_string (L.render $ Crucible.LLVM.ppType tp) ++ ";\n") $ concatMap (\(Some lm) -> mapMaybe (\decl -> if isInfixOf str (symString $ L.decName decl) diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 532c4bd654..c4571bf067 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -74,7 +74,6 @@ import qualified SAWScript.Crucible.JVM.MethodSpecIR () import qualified SAWScript.Crucible.MIR.MethodSpecIR () import qualified Lang.JVM.Codebase as JSS import qualified Text.LLVM.AST as LLVM (Type) -import qualified Text.LLVM.PP as LLVM (ppType) import SAWScript.JavaExpr (JavaType(..)) import SAWScript.JavaPretty (prettyClass) import SAWScript.MGU (instantiate) @@ -118,6 +117,7 @@ import qualified Lang.Crucible.JVM as CJ import Lang.Crucible.Utils.StateContT import Lang.Crucible.LLVM.ArraySizeProfile +import qualified Lang.Crucible.LLVM.PrettyPrint as Crucible.LLVM import Mir.Generator import Mir.Intrinsics (MIR) @@ -373,7 +373,7 @@ showsPrecValue opts nenv p v = VLLVMSkeletonState _ -> showString "<>" VLLVMFunctionProfile _ -> showString "<>" VJavaType {} -> showString "<>" - VLLVMType t -> showString (show (LLVM.ppType t)) + VLLVMType t -> showString (show (Crucible.LLVM.ppType t)) VMIRType t -> showString (show (PP.pretty t)) VCryptolModule m -> showString (showCryptolModule m) VLLVMModule (Some m) -> showString (CMSLLVM.showLLVMModule m)