From 23cc439654abbc0c3714a7035d026453c234d9c4 Mon Sep 17 00:00:00 2001 From: Andrei Stefanescu Date: Wed, 24 Jan 2024 00:35:41 -0800 Subject: [PATCH] Changes (#1165) * Cleanup. * Derive Show. * Add updateHandleMap. * Add parentWTOComponent. * Export writeSourceSize. * Add runCHC and helpers. * Bump what4. * CI: Regenerate cabal.GHC-*.config files * Update parentWTOComponent. * Update test output. --------- Co-authored-by: Ryan Scott --- cabal.GHC-8.10.7.config | 108 ++++++++--------- cabal.GHC-9.2.8.config | 110 +++++++++--------- cabal.GHC-9.4.5.config | 110 +++++++++--------- cabal.GHC-9.6.2.config | 110 +++++++++--------- .../src/Lang/Crucible/LLVM/Intrinsics/Libc.hs | 1 - .../src/Lang/Crucible/LLVM/MemModel/MemLog.hs | 1 + .../Lang/Crucible/LLVM/Translation/Expr.hs | 1 - .../Crucible/Analysis/Fixpoint/Components.hs | 18 +++ crucible/src/Lang/Crucible/Backend.hs | 66 +++++++++++ .../src/Lang/Crucible/Backend/ProofGoals.hs | 2 +- crucible/src/Lang/Crucible/CFG/Expr.hs | 1 - crucible/src/Lang/Crucible/FunctionHandle.hs | 15 +++ .../src/Lang/Crucible/Simulator/EvalStmt.hs | 1 - crucible/src/Lang/Crucible/Types.hs | 11 +- .../golden/golden/float-cast2.z3.good | 2 +- dependencies/what4 | 2 +- 16 files changed, 323 insertions(+), 236 deletions(-) diff --git a/cabal.GHC-8.10.7.config b/cabal.GHC-8.10.7.config index c37b495db..68cd86be5 100644 --- a/cabal.GHC-8.10.7.config +++ b/cabal.GHC-8.10.7.config @@ -13,54 +13,54 @@ constraints: any.BoundedChan ==1.0.3.0, any.adjunctions ==4.4.2, any.aeson ==2.1.2.1, aeson -cffi +ordered-keymap, - any.alex ==3.2.7.4 || ==3.4.0.0, - any.ansi-terminal ==1.0, + any.alex ==3.2.7.4 || ==3.5.0.0, + any.ansi-terminal ==1.0.2, ansi-terminal -example, any.ansi-terminal-types ==0.11.5, any.array ==0.5.4.0, any.assoc ==1.1, assoc +tagged, - any.async ==2.2.4, + any.async ==2.2.5, async -bench, any.atomic-primops ==0.8.4, atomic-primops -debug, any.attoparsec ==0.14.4, attoparsec -developer, - any.barbies ==2.0.4.0, + any.barbies ==2.0.5.0, any.base ==4.14.3.0, - any.base-compat ==0.13.0, - any.base-compat-batteries ==0.13.0, - any.base-orphans ==0.9.0, + any.base-compat ==0.13.1, + any.base-compat-batteries ==0.13.1, + any.base-orphans ==0.9.1, any.base16-bytestring ==1.0.2.0, any.base64-bytestring ==1.2.1.0, any.bifunctors ==5.6.1, bifunctors +tagged, any.bimap ==0.5.0, any.binary ==0.8.8.0, - any.bitvec ==1.1.4.0, - bitvec -libgmp, + any.bitvec ==1.1.5.0, + bitvec +simd, any.bitwise ==1.0.0.1, - any.blaze-builder ==0.4.2.2, - any.boomerang ==1.4.9, + any.blaze-builder ==0.4.2.3, + any.boomerang ==1.4.9.1, + any.boring ==0.2.1, + boring +tagged, any.bv-sized ==1.0.5, any.bytestring ==0.10.12.0, - any.bytestring-builder ==0.10.8.2.0, - bytestring-builder +bytestring_has_builder, any.call-stack ==0.4.0, any.case-insensitive ==1.2.1.0, any.cereal ==0.5.8.3, cereal -bytestring-builder, - any.clock ==0.8.3, + any.clock ==0.8.4, clock -llvm, any.colour ==2.3.6, any.comonad ==5.0.8, comonad +containers +distributive +indexed-traversable, any.concurrent-extra ==0.7.0.12, - any.concurrent-output ==1.10.18, + any.concurrent-output ==1.10.20, any.conduit ==1.3.5, any.config-schema ==1.3.0.0, any.config-value ==0.8.3, - any.constraints ==0.13.4, + any.constraints ==0.14, any.containers ==0.6.5.1, any.contravariant ==1.5.5, contravariant +semigroups +statevar +tagged, @@ -73,7 +73,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.data-default-class ==0.1.2.0, any.data-fix ==0.3.2, any.deepseq ==1.4.4.0, - any.deriving-compat ==0.6.3, + any.deriving-compat ==0.6.5, deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, any.directory ==1.3.6.0, any.distributive ==0.6.2.1, @@ -87,7 +87,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.erf ==2.0.0.0, any.exceptions ==0.10.4, any.extra ==1.7.14, - any.fgl ==5.8.1.1, + any.fgl ==5.8.2.0, fgl +containers042, any.fgl-visualize ==0.1.0.1, any.filemanip ==0.3.6.3, @@ -105,44 +105,44 @@ constraints: any.BoundedChan ==1.0.3.0, any.ghc-prim ==0.6.1, any.gitrev ==1.3.1, any.happy ==1.20.1.1, - any.hashable ==1.4.2.0, + any.hashable ==1.4.3.0, hashable +integer-gmp -random-initial-seed, any.hashtables ==1.3.1, hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, any.haskeline ==0.8.2, any.haskell-lexer ==1.1.1, any.haskell-src-exts ==1.23.1, - any.haskell-src-meta ==0.8.12, - any.hedgehog ==1.3, - any.hsc2hs ==0.68.9, + any.haskell-src-meta ==0.8.13, + any.hedgehog ==1.4, + any.hsc2hs ==0.68.10, hsc2hs -in-ghc-tree, - any.hspec ==2.11.3, - any.hspec-api ==2.11.3, - any.hspec-core ==2.11.3, - any.hspec-discover ==2.11.3, - any.hspec-expectations ==0.8.3, + any.hspec ==2.11.7, + any.hspec-api ==2.11.7, + any.hspec-core ==2.11.7, + any.hspec-discover ==2.11.7, + any.hspec-expectations ==0.8.4, any.ieee754 ==0.8.0, any.indexed-profunctors ==0.1.1.1, - any.indexed-traversable ==0.1.2.1, + any.indexed-traversable ==0.1.3, any.indexed-traversable-instances ==0.1.1.2, any.integer-gmp ==1.0.3.0, any.integer-logarithms ==1.0.3.1, integer-logarithms -check-bounds +integer-gmp, - any.invariant ==0.6.1, + any.invariant ==0.6.2, any.io-streams ==1.5.2.2, io-streams +network -nointeractivetests +zlib, any.itanium-abi ==0.1.2, - any.json ==0.10, + any.json ==0.11, json +generic -mapdict +parsec +pretty +split-base, any.kan-extensions ==5.2.5, any.kvitable ==1.0.2.1, - any.lens ==5.2.2, + any.lens ==5.2.3, lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.5.1, + any.libBF ==0.6.7, libBF -system-libbf, any.libyaml ==0.1.2, libyaml -no-unicode -system-libyaml, - any.lifted-async ==0.10.2.4, + any.lifted-async ==0.10.2.5, any.lifted-base ==0.2.3.12, llvm-pretty-bc-parser -fuzz -regressions, any.logict ==0.8.1.0, @@ -151,7 +151,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.megaparsec ==9.2.1, megaparsec -dev, any.microlens ==0.4.13.1, - any.microlens-th ==0.4.3.13, + any.microlens-th ==0.4.3.14, any.mmorph ==1.2.0, any.monad-control ==1.0.3.1, any.monadLib ==3.10.1, @@ -164,7 +164,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.ordered-containers ==0.2.3, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, - any.parameterized-utils ==2.1.7.0, + any.parameterized-utils ==2.1.8.0, parameterized-utils +unsafe-operations, any.parsec ==3.1.14.0, any.parser-combinators ==1.3.0, @@ -191,7 +191,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.rts ==1.0.1, 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.scheduler ==2.0.0.1, any.scientific ==0.3.7.0, @@ -204,8 +204,8 @@ constraints: any.BoundedChan ==1.0.3.0, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, any.simple-get-opt ==0.4, any.smallcheck ==1.2.1.1, - any.split ==0.2.3.5, - any.splitmix ==0.1.0.4, + any.split ==0.2.5, + any.splitmix ==0.1.0.5, splitmix -optimised-mixer, any.stm ==2.5.0.1, any.streaming-commons ==0.2.2.6, @@ -213,19 +213,19 @@ constraints: any.BoundedChan ==1.0.3.0, any.strict ==0.5, any.string-interpolate ==0.3.2.1, string-interpolate -bytestring-builder -extended-benchmarks -text-builder, - any.syb ==0.7.2.3, - any.tagged ==0.8.7, + any.syb ==0.7.2.4, + any.tagged ==0.8.8, tagged +deepseq +transformers, - any.tasty ==1.4.3, + any.tasty ==1.5, tasty +unix, any.tasty-checklist ==1.0.6.0, any.tasty-expected-failure ==0.12.3, any.tasty-golden ==2.3.5, tasty-golden -build-example, - any.tasty-hedgehog ==1.4.0.1, + any.tasty-hedgehog ==1.4.0.2, any.tasty-hspec ==1.2.0.4, - any.tasty-hunit ==0.10.0.3, - any.tasty-quickcheck ==0.10.2, + any.tasty-hunit ==0.10.1, + any.tasty-quickcheck ==0.10.3, any.tasty-smallcheck ==0.8.2, any.tasty-sugar ==2.2.1.0, any.template-haskell ==2.16.0.0, @@ -240,7 +240,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.th-abstraction ==0.5.0.0, any.th-compat ==0.1.4, any.th-expand-syns ==0.4.11.0, - any.th-lift ==0.8.3, + any.th-lift ==0.8.4, any.th-lift-instances ==0.1.20, any.th-orphans ==0.13.14, any.th-reify-many ==0.1.10, @@ -254,27 +254,27 @@ constraints: any.BoundedChan ==1.0.3.0, any.transformers-compat ==0.7.2, transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, any.type-equality ==1, - any.typed-process ==0.2.11.0, + any.typed-process ==0.2.11.1, any.unbounded-delays ==0.1.1.1, any.uniplate ==1.6.13, any.unix ==2.7.2.2, - any.unix-compat ==0.7, + any.unix-compat ==0.7.1, unix-compat -old-time, any.unliftio ==0.2.25.0, any.unliftio-core ==0.2.1.0, - any.unordered-containers ==0.2.19.1, + any.unordered-containers ==0.2.20, unordered-containers -debug, any.utf8-string ==1.0.2, - any.uuid-types ==1.0.5, - any.vector ==0.13.0.0, + any.uuid-types ==1.0.5.1, + any.vector ==0.13.1.0, vector +boundschecks -internalchecks -unsafechecks -wall, any.vector-algorithms ==0.9.0.1, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, - any.vector-stream ==0.1.0.0, - any.versions ==5.0.5, + any.vector-stream ==0.1.0.1, + any.versions ==6.0.4, any.void ==0.7.3, void -safe, - any.websockets ==0.12.7.3, + any.websockets ==0.13.0.0, websockets -example, what4 -drealtestdisable -solvertests -stptestdisable, any.witherable ==0.4.2, @@ -286,4 +286,4 @@ constraints: any.BoundedChan ==1.0.3.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2023-08-03T16:21:02Z +index-state: hackage.haskell.org 2024-01-15T23:27:26Z diff --git a/cabal.GHC-9.2.8.config b/cabal.GHC-9.2.8.config index 06015562d..e63dbfb3b 100644 --- a/cabal.GHC-9.2.8.config +++ b/cabal.GHC-9.2.8.config @@ -13,54 +13,54 @@ constraints: any.BoundedChan ==1.0.3.0, any.adjunctions ==4.4.2, any.aeson ==2.1.2.1, aeson -cffi +ordered-keymap, - any.alex ==3.2.7.4 || ==3.4.0.0, - any.ansi-terminal ==1.0, + any.alex ==3.2.7.4 || ==3.5.0.0, + any.ansi-terminal ==1.0.2, ansi-terminal -example, any.ansi-terminal-types ==0.11.5, any.array ==0.5.4.0, any.assoc ==1.1, assoc +tagged, - any.async ==2.2.4, + any.async ==2.2.5, async -bench, any.atomic-primops ==0.8.4, atomic-primops -debug, any.attoparsec ==0.14.4, attoparsec -developer, - any.barbies ==2.0.4.0, + any.barbies ==2.0.5.0, any.base ==4.16.4.0, - any.base-compat ==0.13.0, - any.base-compat-batteries ==0.13.0, - any.base-orphans ==0.9.0, + any.base-compat ==0.13.1, + any.base-compat-batteries ==0.13.1, + any.base-orphans ==0.9.1, any.base16-bytestring ==1.0.2.0, any.base64-bytestring ==1.2.1.0, any.bifunctors ==5.6.1, bifunctors +tagged, any.bimap ==0.5.0, any.binary ==0.8.9.0, - any.bitvec ==1.1.4.0, - bitvec -libgmp, + any.bitvec ==1.1.5.0, + bitvec +simd, any.bitwise ==1.0.0.1, - any.blaze-builder ==0.4.2.2, - any.boomerang ==1.4.9, + any.blaze-builder ==0.4.2.3, + any.boomerang ==1.4.9.1, + any.boring ==0.2.1, + boring +tagged, any.bv-sized ==1.0.5, any.bytestring ==0.11.4.0, - any.bytestring-builder ==0.10.8.2.0, - bytestring-builder +bytestring_has_builder, any.call-stack ==0.4.0, any.case-insensitive ==1.2.1.0, any.cereal ==0.5.8.3, cereal -bytestring-builder, - any.clock ==0.8.3, + any.clock ==0.8.4, clock -llvm, any.colour ==2.3.6, any.comonad ==5.0.8, comonad +containers +distributive +indexed-traversable, any.concurrent-extra ==0.7.0.12, - any.concurrent-output ==1.10.18, + any.concurrent-output ==1.10.20, any.conduit ==1.3.5, any.config-schema ==1.3.0.0, any.config-value ==0.8.3, - any.constraints ==0.13.4, + any.constraints ==0.14, any.containers ==0.6.5.1, any.contravariant ==1.5.5, contravariant +semigroups +statevar +tagged, @@ -73,7 +73,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.data-default-class ==0.1.2.0, any.data-fix ==0.3.2, any.deepseq ==1.4.6.1, - any.deriving-compat ==0.6.3, + any.deriving-compat ==0.6.5, deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, any.directory ==1.3.6.2, any.distributive ==0.6.2.1, @@ -87,7 +87,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.erf ==2.0.0.0, any.exceptions ==0.10.4, any.extra ==1.7.14, - any.fgl ==5.8.1.1, + any.fgl ==5.8.2.0, fgl +containers042, any.fgl-visualize ==0.1.0.1, any.filemanip ==0.3.6.3, @@ -106,52 +106,52 @@ constraints: any.BoundedChan ==1.0.3.0, any.ghc-prim ==0.8.0, any.gitrev ==1.3.1, any.happy ==1.20.1.1, - any.hashable ==1.4.2.0, + any.hashable ==1.4.3.0, hashable +integer-gmp -random-initial-seed, any.hashtables ==1.3.1, hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, any.haskeline ==0.8.2, any.haskell-lexer ==1.1.1, any.haskell-src-exts ==1.23.1, - any.haskell-src-meta ==0.8.12, - any.hedgehog ==1.3, - any.hsc2hs ==0.68.9, + any.haskell-src-meta ==0.8.13, + any.hedgehog ==1.4, + any.hsc2hs ==0.68.10, hsc2hs -in-ghc-tree, - any.hspec ==2.11.3, - any.hspec-api ==2.11.3, - any.hspec-core ==2.11.3, - any.hspec-discover ==2.11.3, - any.hspec-expectations ==0.8.3, + any.hspec ==2.11.7, + any.hspec-api ==2.11.7, + any.hspec-core ==2.11.7, + any.hspec-discover ==2.11.7, + any.hspec-expectations ==0.8.4, any.ieee754 ==0.8.0, any.indexed-profunctors ==0.1.1.1, - any.indexed-traversable ==0.1.2.1, + any.indexed-traversable ==0.1.3, any.indexed-traversable-instances ==0.1.1.2, any.integer-logarithms ==1.0.3.1, integer-logarithms -check-bounds +integer-gmp, - any.invariant ==0.6.1, + any.invariant ==0.6.2, any.io-streams ==1.5.2.2, io-streams +network -nointeractivetests +zlib, any.itanium-abi ==0.1.2, - any.json ==0.10, + any.json ==0.11, json +generic -mapdict +parsec +pretty +split-base, any.kan-extensions ==5.2.5, any.kvitable ==1.0.2.1, - any.lens ==5.2.2, + any.lens ==5.2.3, lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.5.1, + any.libBF ==0.6.7, libBF -system-libbf, any.libyaml ==0.1.2, libyaml -no-unicode -system-libyaml, - any.lifted-async ==0.10.2.4, + any.lifted-async ==0.10.2.5, any.lifted-base ==0.2.3.12, llvm-pretty-bc-parser -fuzz -regressions, any.logict ==0.8.1.0, any.lucid ==2.11.20230408, any.lumberjack ==1.0.3.0, - any.megaparsec ==9.3.1, + any.megaparsec ==9.6.1, megaparsec -dev, any.microlens ==0.4.13.1, - any.microlens-th ==0.4.3.13, + any.microlens-th ==0.4.3.14, any.mmorph ==1.2.0, any.monad-control ==1.0.3.1, any.monadLib ==3.10.1, @@ -164,7 +164,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.ordered-containers ==0.2.3, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, - any.parameterized-utils ==2.1.7.0, + any.parameterized-utils ==2.1.8.0, parameterized-utils +unsafe-operations, any.parsec ==3.1.15.0, any.parser-combinators ==1.3.0, @@ -191,7 +191,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.rts ==1.0.2, any.s-cargot ==0.1.6.0, s-cargot -build-example, - any.safe ==0.3.19, + any.safe ==0.3.20, any.safe-exceptions ==0.1.7.4, any.scheduler ==2.0.0.1, any.scientific ==0.3.7.0, @@ -204,8 +204,8 @@ constraints: any.BoundedChan ==1.0.3.0, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, any.simple-get-opt ==0.4, any.smallcheck ==1.2.1.1, - any.split ==0.2.3.5, - any.splitmix ==0.1.0.4, + any.split ==0.2.5, + any.splitmix ==0.1.0.5, splitmix -optimised-mixer, any.stm ==2.5.0.2, any.streaming-commons ==0.2.2.6, @@ -213,19 +213,19 @@ constraints: any.BoundedChan ==1.0.3.0, any.strict ==0.5, any.string-interpolate ==0.3.2.1, string-interpolate -bytestring-builder -extended-benchmarks -text-builder, - any.syb ==0.7.2.3, - any.tagged ==0.8.7, + any.syb ==0.7.2.4, + any.tagged ==0.8.8, tagged +deepseq +transformers, - any.tasty ==1.4.3, + any.tasty ==1.5, tasty +unix, any.tasty-checklist ==1.0.6.0, any.tasty-expected-failure ==0.12.3, any.tasty-golden ==2.3.5, tasty-golden -build-example, - any.tasty-hedgehog ==1.4.0.1, + any.tasty-hedgehog ==1.4.0.2, any.tasty-hspec ==1.2.0.4, - any.tasty-hunit ==0.10.0.3, - any.tasty-quickcheck ==0.10.2, + any.tasty-hunit ==0.10.1, + any.tasty-quickcheck ==0.10.3, any.tasty-smallcheck ==0.8.2, any.tasty-sugar ==2.2.1.0, any.template-haskell ==2.18.0.0, @@ -240,7 +240,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.th-abstraction ==0.5.0.0, any.th-compat ==0.1.4, any.th-expand-syns ==0.4.11.0, - any.th-lift ==0.8.3, + any.th-lift ==0.8.4, any.th-lift-instances ==0.1.20, any.th-orphans ==0.13.14, any.th-reify-many ==0.1.10, @@ -254,27 +254,27 @@ constraints: any.BoundedChan ==1.0.3.0, any.transformers-compat ==0.7.2, transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, any.type-equality ==1, - any.typed-process ==0.2.11.0, + any.typed-process ==0.2.11.1, any.unbounded-delays ==0.1.1.1, any.uniplate ==1.6.13, any.unix ==2.7.2.2, - any.unix-compat ==0.7, + any.unix-compat ==0.7.1, unix-compat -old-time, any.unliftio ==0.2.25.0, any.unliftio-core ==0.2.1.0, - any.unordered-containers ==0.2.19.1, + any.unordered-containers ==0.2.20, unordered-containers -debug, any.utf8-string ==1.0.2, - any.uuid-types ==1.0.5, - any.vector ==0.13.0.0, + any.uuid-types ==1.0.5.1, + any.vector ==0.13.1.0, vector +boundschecks -internalchecks -unsafechecks -wall, any.vector-algorithms ==0.9.0.1, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, - any.vector-stream ==0.1.0.0, - any.versions ==5.0.5, + any.vector-stream ==0.1.0.1, + any.versions ==6.0.4, any.void ==0.7.3, void -safe, - any.websockets ==0.12.7.3, + any.websockets ==0.13.0.0, websockets -example, what4 -drealtestdisable -solvertests -stptestdisable, any.witherable ==0.4.2, @@ -286,4 +286,4 @@ constraints: any.BoundedChan ==1.0.3.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2023-08-03T16:21:02Z +index-state: hackage.haskell.org 2024-01-15T23:27:26Z diff --git a/cabal.GHC-9.4.5.config b/cabal.GHC-9.4.5.config index 9c77487b7..68a2e610d 100644 --- a/cabal.GHC-9.4.5.config +++ b/cabal.GHC-9.4.5.config @@ -14,54 +14,54 @@ constraints: any.BoundedChan ==1.0.3.0, any.adjunctions ==4.4.2, any.aeson ==2.1.2.1, aeson -cffi +ordered-keymap, - any.alex ==3.2.7.4 || ==3.4.0.0, - any.ansi-terminal ==1.0, + any.alex ==3.2.7.4 || ==3.5.0.0, + any.ansi-terminal ==1.0.2, ansi-terminal -example, any.ansi-terminal-types ==0.11.5, any.array ==0.5.4.0, any.assoc ==1.1, assoc +tagged, - any.async ==2.2.4, + any.async ==2.2.5, async -bench, any.atomic-primops ==0.8.4, atomic-primops -debug, any.attoparsec ==0.14.4, attoparsec -developer, - any.barbies ==2.0.4.0, + any.barbies ==2.0.5.0, any.base ==4.17.1.0, - any.base-compat ==0.13.0, - any.base-compat-batteries ==0.13.0, - any.base-orphans ==0.9.0, + any.base-compat ==0.13.1, + any.base-compat-batteries ==0.13.1, + any.base-orphans ==0.9.1, any.base16-bytestring ==1.0.2.0, any.base64-bytestring ==1.2.1.0, any.bifunctors ==5.6.1, bifunctors +tagged, any.bimap ==0.5.0, any.binary ==0.8.9.1, - any.bitvec ==1.1.4.0, - bitvec -libgmp, + any.bitvec ==1.1.5.0, + bitvec +simd, any.bitwise ==1.0.0.1, - any.blaze-builder ==0.4.2.2, - any.boomerang ==1.4.9, + any.blaze-builder ==0.4.2.3, + any.boomerang ==1.4.9.1, + any.boring ==0.2.1, + boring +tagged, any.bv-sized ==1.0.5, any.bytestring ==0.11.4.0, - any.bytestring-builder ==0.10.8.2.0, - bytestring-builder +bytestring_has_builder, any.call-stack ==0.4.0, any.case-insensitive ==1.2.1.0, any.cereal ==0.5.8.3, cereal -bytestring-builder, - any.clock ==0.8.3, + any.clock ==0.8.4, clock -llvm, any.colour ==2.3.6, any.comonad ==5.0.8, comonad +containers +distributive +indexed-traversable, any.concurrent-extra ==0.7.0.12, - any.concurrent-output ==1.10.18, + any.concurrent-output ==1.10.20, any.conduit ==1.3.5, any.config-schema ==1.3.0.0, any.config-value ==0.8.3, - any.constraints ==0.13.4, + any.constraints ==0.14, any.containers ==0.6.7, any.contravariant ==1.5.5, contravariant +semigroups +statevar +tagged, @@ -73,7 +73,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.data-default-class ==0.1.2.0, any.data-fix ==0.3.2, any.deepseq ==1.4.8.0, - any.deriving-compat ==0.6.3, + any.deriving-compat ==0.6.5, deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, any.directory ==1.3.7.1, any.distributive ==0.6.2.1, @@ -87,7 +87,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.erf ==2.0.0.0, any.exceptions ==0.10.5, any.extra ==1.7.14, - any.fgl ==5.8.1.1, + any.fgl ==5.8.2.0, fgl +containers042, any.fgl-visualize ==0.1.0.1, any.filemanip ==0.3.6.3, @@ -106,52 +106,52 @@ constraints: any.BoundedChan ==1.0.3.0, any.ghc-prim ==0.9.0, any.gitrev ==1.3.1, any.happy ==1.20.1.1, - any.hashable ==1.4.2.0, + any.hashable ==1.4.3.0, hashable +integer-gmp -random-initial-seed, any.hashtables ==1.3.1, hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, any.haskeline ==0.8.2, any.haskell-lexer ==1.1.1, any.haskell-src-exts ==1.23.1, - any.haskell-src-meta ==0.8.12, - any.hedgehog ==1.3, - any.hsc2hs ==0.68.9, + any.haskell-src-meta ==0.8.13, + any.hedgehog ==1.4, + any.hsc2hs ==0.68.10, hsc2hs -in-ghc-tree, - any.hspec ==2.11.3, - any.hspec-api ==2.11.3, - any.hspec-core ==2.11.3, - any.hspec-discover ==2.11.3, - any.hspec-expectations ==0.8.3, + any.hspec ==2.11.7, + any.hspec-api ==2.11.7, + any.hspec-core ==2.11.7, + any.hspec-discover ==2.11.7, + any.hspec-expectations ==0.8.4, any.ieee754 ==0.8.0, any.indexed-profunctors ==0.1.1.1, - any.indexed-traversable ==0.1.2.1, + any.indexed-traversable ==0.1.3, any.indexed-traversable-instances ==0.1.1.2, any.integer-logarithms ==1.0.3.1, integer-logarithms -check-bounds +integer-gmp, - any.invariant ==0.6.1, + any.invariant ==0.6.2, any.io-streams ==1.5.2.2, io-streams +network -nointeractivetests +zlib, any.itanium-abi ==0.1.2, - any.json ==0.10, + any.json ==0.11, json +generic -mapdict +parsec +pretty +split-base, any.kan-extensions ==5.2.5, any.kvitable ==1.0.2.1, - any.lens ==5.2.2, + any.lens ==5.2.3, lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.5.1, + any.libBF ==0.6.7, libBF -system-libbf, any.libyaml ==0.1.2, libyaml -no-unicode -system-libyaml, - any.lifted-async ==0.10.2.4, + any.lifted-async ==0.10.2.5, any.lifted-base ==0.2.3.12, llvm-pretty-bc-parser -fuzz -regressions, any.logict ==0.8.1.0, any.lucid ==2.11.20230408, any.lumberjack ==1.0.3.0, - any.megaparsec ==9.3.1, + any.megaparsec ==9.6.1, megaparsec -dev, any.microlens ==0.4.13.1, - any.microlens-th ==0.4.3.13, + any.microlens-th ==0.4.3.14, any.mmorph ==1.2.0, any.monad-control ==1.0.3.1, any.monadLib ==3.10.1, @@ -164,7 +164,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.ordered-containers ==0.2.3, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, - any.parameterized-utils ==2.1.7.0, + any.parameterized-utils ==2.1.8.0, parameterized-utils +unsafe-operations, any.parsec ==3.1.16.1, any.parser-combinators ==1.3.0, @@ -191,7 +191,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.rts ==1.0.2, any.s-cargot ==0.1.6.0, s-cargot -build-example, - any.safe ==0.3.19, + any.safe ==0.3.20, any.safe-exceptions ==0.1.7.4, any.scheduler ==2.0.0.1, any.scientific ==0.3.7.0, @@ -204,8 +204,8 @@ constraints: any.BoundedChan ==1.0.3.0, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, any.simple-get-opt ==0.4, any.smallcheck ==1.2.1.1, - any.split ==0.2.3.5, - any.splitmix ==0.1.0.4, + any.split ==0.2.5, + any.splitmix ==0.1.0.5, splitmix -optimised-mixer, any.stm ==2.5.1.0, any.streaming-commons ==0.2.2.6, @@ -213,19 +213,19 @@ constraints: any.BoundedChan ==1.0.3.0, any.strict ==0.5, any.string-interpolate ==0.3.2.1, string-interpolate -bytestring-builder -extended-benchmarks -text-builder, - any.syb ==0.7.2.3, - any.tagged ==0.8.7, + any.syb ==0.7.2.4, + any.tagged ==0.8.8, tagged +deepseq +transformers, - any.tasty ==1.4.3, + any.tasty ==1.5, tasty +unix, any.tasty-checklist ==1.0.6.0, any.tasty-expected-failure ==0.12.3, any.tasty-golden ==2.3.5, tasty-golden -build-example, - any.tasty-hedgehog ==1.4.0.1, + any.tasty-hedgehog ==1.4.0.2, any.tasty-hspec ==1.2.0.4, - any.tasty-hunit ==0.10.0.3, - any.tasty-quickcheck ==0.10.2, + any.tasty-hunit ==0.10.1, + any.tasty-quickcheck ==0.10.3, any.tasty-smallcheck ==0.8.2, any.tasty-sugar ==2.2.1.0, any.template-haskell ==2.19.0.0, @@ -240,7 +240,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.th-abstraction ==0.5.0.0, any.th-compat ==0.1.4, any.th-expand-syns ==0.4.11.0, - any.th-lift ==0.8.3, + any.th-lift ==0.8.4, any.th-lift-instances ==0.1.20, any.th-orphans ==0.13.14, any.th-reify-many ==0.1.10, @@ -254,27 +254,27 @@ constraints: any.BoundedChan ==1.0.3.0, any.transformers-compat ==0.7.2, transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, any.type-equality ==1, - any.typed-process ==0.2.11.0, + any.typed-process ==0.2.11.1, 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.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-types ==1.0.5, - any.vector ==0.13.0.0, + any.uuid-types ==1.0.5.1, + any.vector ==0.13.1.0, vector +boundschecks -internalchecks -unsafechecks -wall, any.vector-algorithms ==0.9.0.1, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, - any.vector-stream ==0.1.0.0, - any.versions ==5.0.5, + any.vector-stream ==0.1.0.1, + any.versions ==6.0.4, any.void ==0.7.3, void -safe, - any.websockets ==0.12.7.3, + any.websockets ==0.13.0.0, websockets -example, what4 -drealtestdisable -solvertests -stptestdisable, any.witherable ==0.4.2, @@ -286,4 +286,4 @@ constraints: any.BoundedChan ==1.0.3.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2023-08-03T16:21:02Z +index-state: hackage.haskell.org 2024-01-15T23:27:26Z diff --git a/cabal.GHC-9.6.2.config b/cabal.GHC-9.6.2.config index 9dee4f4a2..b3fb185de 100644 --- a/cabal.GHC-9.6.2.config +++ b/cabal.GHC-9.6.2.config @@ -14,54 +14,54 @@ constraints: any.BoundedChan ==1.0.3.0, any.adjunctions ==4.4.2, any.aeson ==2.1.2.1, aeson -cffi +ordered-keymap, - any.alex ==3.2.7.4 || ==3.4.0.0, - any.ansi-terminal ==1.0, + any.alex ==3.2.7.4 || ==3.5.0.0, + any.ansi-terminal ==1.0.2, ansi-terminal -example, any.ansi-terminal-types ==0.11.5, any.array ==0.5.5.0, any.assoc ==1.1, assoc +tagged, - any.async ==2.2.4, + any.async ==2.2.5, async -bench, any.atomic-primops ==0.8.4, atomic-primops -debug, any.attoparsec ==0.14.4, attoparsec -developer, - any.barbies ==2.0.4.0, + any.barbies ==2.0.5.0, any.base ==4.18.0.0, - any.base-compat ==0.13.0, - any.base-compat-batteries ==0.13.0, - any.base-orphans ==0.9.0, + any.base-compat ==0.13.1, + any.base-compat-batteries ==0.13.1, + any.base-orphans ==0.9.1, any.base16-bytestring ==1.0.2.0, any.base64-bytestring ==1.2.1.0, any.bifunctors ==5.6.1, bifunctors +tagged, any.bimap ==0.5.0, any.binary ==0.8.9.1, - any.bitvec ==1.1.4.0, - bitvec -libgmp, + any.bitvec ==1.1.5.0, + bitvec +simd, any.bitwise ==1.0.0.1, - any.blaze-builder ==0.4.2.2, - any.boomerang ==1.4.9, + any.blaze-builder ==0.4.2.3, + any.boomerang ==1.4.9.1, + any.boring ==0.2.1, + boring +tagged, any.bv-sized ==1.0.5, any.bytestring ==0.11.4.0, - any.bytestring-builder ==0.10.8.2.0, - bytestring-builder +bytestring_has_builder, any.call-stack ==0.4.0, any.case-insensitive ==1.2.1.0, any.cereal ==0.5.8.3, cereal -bytestring-builder, - any.clock ==0.8.3, + any.clock ==0.8.4, clock -llvm, any.colour ==2.3.6, any.comonad ==5.0.8, comonad +containers +distributive +indexed-traversable, any.concurrent-extra ==0.7.0.12, - any.concurrent-output ==1.10.18, + any.concurrent-output ==1.10.20, any.conduit ==1.3.5, any.config-schema ==1.3.0.0, any.config-value ==0.8.3, - any.constraints ==0.13.4, + any.constraints ==0.14, any.containers ==0.6.7, any.contravariant ==1.5.5, contravariant +semigroups +statevar +tagged, @@ -73,7 +73,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.data-default-class ==0.1.2.0, any.data-fix ==0.3.2, any.deepseq ==1.4.8.1, - any.deriving-compat ==0.6.3, + any.deriving-compat ==0.6.5, deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, any.directory ==1.3.8.1, any.distributive ==0.6.2.1, @@ -87,7 +87,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.erf ==2.0.0.0, any.exceptions ==0.10.7, any.extra ==1.7.14, - any.fgl ==5.8.1.1, + any.fgl ==5.8.2.0, fgl +containers042, any.fgl-visualize ==0.1.0.1, any.filemanip ==0.3.6.3, @@ -104,52 +104,52 @@ constraints: any.BoundedChan ==1.0.3.0, any.ghc-prim ==0.10.0, any.gitrev ==1.3.1, any.happy ==1.20.1.1, - any.hashable ==1.4.2.0, + any.hashable ==1.4.3.0, hashable +integer-gmp -random-initial-seed, any.hashtables ==1.3.1, hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, any.haskeline ==0.8.2.1, any.haskell-lexer ==1.1.1, any.haskell-src-exts ==1.23.1, - any.haskell-src-meta ==0.8.12, - any.hedgehog ==1.3, - any.hsc2hs ==0.68.9, + any.haskell-src-meta ==0.8.13, + any.hedgehog ==1.4, + any.hsc2hs ==0.68.10, hsc2hs -in-ghc-tree, - any.hspec ==2.11.3, - any.hspec-api ==2.11.3, - any.hspec-core ==2.11.3, - any.hspec-discover ==2.11.3, - any.hspec-expectations ==0.8.3, + any.hspec ==2.11.7, + any.hspec-api ==2.11.7, + any.hspec-core ==2.11.7, + any.hspec-discover ==2.11.7, + any.hspec-expectations ==0.8.4, any.ieee754 ==0.8.0, any.indexed-profunctors ==0.1.1.1, - any.indexed-traversable ==0.1.2.1, + any.indexed-traversable ==0.1.3, any.indexed-traversable-instances ==0.1.1.2, any.integer-logarithms ==1.0.3.1, integer-logarithms -check-bounds +integer-gmp, - any.invariant ==0.6.1, + any.invariant ==0.6.2, any.io-streams ==1.5.2.2, io-streams +network -nointeractivetests +zlib, any.itanium-abi ==0.1.2, - any.json ==0.10, + any.json ==0.11, json +generic -mapdict +parsec +pretty +split-base, any.kan-extensions ==5.2.5, any.kvitable ==1.0.2.1, - any.lens ==5.2.2, + any.lens ==5.2.3, lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.5.1, + any.libBF ==0.6.7, libBF -system-libbf, any.libyaml ==0.1.2, libyaml -no-unicode -system-libyaml, - any.lifted-async ==0.10.2.4, + any.lifted-async ==0.10.2.5, any.lifted-base ==0.2.3.12, llvm-pretty-bc-parser -fuzz -regressions, any.logict ==0.8.1.0, any.lucid ==2.11.20230408, any.lumberjack ==1.0.3.0, - any.megaparsec ==9.3.1, + any.megaparsec ==9.6.1, megaparsec -dev, any.microlens ==0.4.13.1, - any.microlens-th ==0.4.3.13, + any.microlens-th ==0.4.3.14, any.mmorph ==1.2.0, any.monad-control ==1.0.3.1, any.monadLib ==3.10.1, @@ -162,7 +162,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.ordered-containers ==0.2.3, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, - any.parameterized-utils ==2.1.7.0, + any.parameterized-utils ==2.1.8.0, parameterized-utils +unsafe-operations, any.parsec ==3.1.16.1, any.parser-combinators ==1.3.0, @@ -189,7 +189,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.rts ==1.0.2, any.s-cargot ==0.1.6.0, s-cargot -build-example, - any.safe ==0.3.19, + any.safe ==0.3.20, any.safe-exceptions ==0.1.7.4, any.scheduler ==2.0.0.1, any.scientific ==0.3.7.0, @@ -202,8 +202,8 @@ constraints: any.BoundedChan ==1.0.3.0, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, any.simple-get-opt ==0.4, any.smallcheck ==1.2.1.1, - any.split ==0.2.3.5, - any.splitmix ==0.1.0.4, + any.split ==0.2.5, + any.splitmix ==0.1.0.5, splitmix -optimised-mixer, any.stm ==2.5.1.0, any.streaming-commons ==0.2.2.6, @@ -211,19 +211,19 @@ constraints: any.BoundedChan ==1.0.3.0, any.strict ==0.5, any.string-interpolate ==0.3.2.1, string-interpolate -bytestring-builder -extended-benchmarks -text-builder, - any.syb ==0.7.2.3, - any.tagged ==0.8.7, + any.syb ==0.7.2.4, + any.tagged ==0.8.8, tagged +deepseq +transformers, - any.tasty ==1.4.3, + any.tasty ==1.5, tasty +unix, any.tasty-checklist ==1.0.6.0, any.tasty-expected-failure ==0.12.3, any.tasty-golden ==2.3.5, tasty-golden -build-example, - any.tasty-hedgehog ==1.4.0.1, + any.tasty-hedgehog ==1.4.0.2, any.tasty-hspec ==1.2.0.4, - any.tasty-hunit ==0.10.0.3, - any.tasty-quickcheck ==0.10.2, + any.tasty-hunit ==0.10.1, + any.tasty-quickcheck ==0.10.3, any.tasty-smallcheck ==0.8.2, any.tasty-sugar ==2.2.1.0, any.template-haskell ==2.20.0.0, @@ -238,7 +238,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.th-abstraction ==0.5.0.0, any.th-compat ==0.1.4, any.th-expand-syns ==0.4.11.0, - any.th-lift ==0.8.3, + any.th-lift ==0.8.4, any.th-lift-instances ==0.1.20, any.th-orphans ==0.13.14, any.th-reify-many ==0.1.10, @@ -252,27 +252,27 @@ constraints: any.BoundedChan ==1.0.3.0, any.transformers-compat ==0.7.2, transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, any.type-equality ==1, - any.typed-process ==0.2.11.0, + any.typed-process ==0.2.11.1, 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.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-types ==1.0.5, - any.vector ==0.13.0.0, + any.uuid-types ==1.0.5.1, + any.vector ==0.13.1.0, vector +boundschecks -internalchecks -unsafechecks -wall, any.vector-algorithms ==0.9.0.1, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, - any.vector-stream ==0.1.0.0, - any.versions ==5.0.5, + any.vector-stream ==0.1.0.1, + any.versions ==6.0.4, any.void ==0.7.3, void -safe, - any.websockets ==0.12.7.3, + any.websockets ==0.13.0.0, websockets -example, what4 -drealtestdisable -solvertests -stptestdisable, any.witherable ==0.4.2, @@ -284,4 +284,4 @@ constraints: any.BoundedChan ==1.0.3.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2023-08-03T16:21:02Z +index-state: hackage.haskell.org 2024-01-15T23:27:26Z diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs index 5396c371f..7c632091d 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs @@ -43,7 +43,6 @@ import Data.Parameterized.Context ( pattern (:>), pattern Empty ) import qualified Data.Parameterized.Context as Ctx import What4.Interface -import What4.InterpretedFloatingPoint (IsInterpretedFloatExprBuilder(..)) import What4.ProgramLoc (plSourceLoc) import qualified What4.SpecialFunctions as W4 diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs index c004e26ea..735575e85 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs @@ -68,6 +68,7 @@ module Lang.Crucible.LLVM.MemModel.MemLog -- * Write ranges , writeRangesMem + , writeSourceSize -- * Concretization , concPtr diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Expr.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Expr.hs index 6af46020d..6962a94e3 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Expr.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Expr.hs @@ -101,7 +101,6 @@ import Lang.Crucible.LLVM.TypeContext import Lang.Crucible.Syntax import Lang.Crucible.Types -import What4.InterpretedFloatingPoint (X86_80Val(..)) ------------------------------------------------------------------------- -- LLVMExpr diff --git a/crucible/src/Lang/Crucible/Analysis/Fixpoint/Components.hs b/crucible/src/Lang/Crucible/Analysis/Fixpoint/Components.hs index db296717b..5adbea650 100644 --- a/crucible/src/Lang/Crucible/Analysis/Fixpoint/Components.hs +++ b/crucible/src/Lang/Crucible/Analysis/Fixpoint/Components.hs @@ -21,6 +21,7 @@ module Lang.Crucible.Analysis.Fixpoint.Components ( weakTopologicalOrdering, WTOComponent(..), SCC(..), + parentWTOComponent, -- * Special cases cfgWeakTopologicalOrdering, cfgSuccessors, @@ -239,6 +240,23 @@ unlabeled = Label 0 maxLabel :: Label maxLabel = Label maxBound +-- | Construct a map from each vertex to the head of its parent WTO component. +-- In particular, the head of a component is not in the map. The vertices that +-- are not in any component are not in the map. +parentWTOComponent :: (Ord n) => [WTOComponent n] -> M.Map n n +parentWTOComponent = F.foldMap' $ \case + SCC scc' -> parentWTOComponent' scc' + Vertex{} -> M.empty + +parentWTOComponent' :: (Ord n) => SCC n -> M.Map n n +parentWTOComponent' scc = + F.foldMap' + (\case + SCC scc' -> parentWTOComponent' scc' + Vertex v -> M.singleton v $ wtoHead scc) + (wtoComps scc) + + {- Note [Bourdoncle Components] Bourdoncle components are a weak topological ordering of graph diff --git a/crucible/src/Lang/Crucible/Backend.hs b/crucible/src/Lang/Crucible/Backend.hs index 69aa1f43c..f8adec788 100644 --- a/crucible/src/Lang/Crucible/Backend.hs +++ b/crucible/src/Lang/Crucible/Backend.hs @@ -95,6 +95,11 @@ module Lang.Crucible.Backend , addFailedAssertion , assertIsInteger , readPartExpr + , runCHC + , proofObligationsAsImplications + , convertProofObligationsAsImplications + , proofObligationsUninterpConstants + , pathConditionUninterpConstants , ppProofObligation , backendOptions , assertThenAssumeConfigOption @@ -110,17 +115,25 @@ import Data.Functor.Identity import Data.Functor.Const import qualified Data.Sequence as Seq import Data.Sequence (Seq) +import Data.Set (Set) import qualified Prettyprinter as PP import GHC.Stack +import System.IO + +import Data.Parameterized.Map (MapF) import What4.Concrete import What4.Config +import What4.Expr.Builder import What4.Interface import What4.InterpretedFloatingPoint import What4.LabeledPred import What4.Partial import What4.ProgramLoc import What4.Expr (GroundValue, GroundValueWrapper(..)) +import What4.Solver +import qualified What4.Solver.CVC5 as CVC5 +import qualified What4.Solver.Z3 as Z3 import qualified Lang.Crucible.Backend.AssumptionStack as AS import qualified Lang.Crucible.Backend.ProofGoals as PG @@ -613,6 +626,59 @@ readPartExpr bak (PE p v) msg = do addAssertion bak (LabeledPred p (SimError loc msg)) return v + +-- | Run the CHC solver on the current proof obligations, and return the +-- solution as a substitution from the uninterpreted functions to their +-- definitions. +runCHC :: + (IsSymBackend sym bak, sym ~ ExprBuilder t st fs, MonadIO m) => + bak -> + [SomeSymFn sym] -> + m (MapF (SymFnWrapper sym) (SymFnWrapper sym)) +runCHC bak uninterp_inv_fns = liftIO $ do + let sym = backendGetSym bak + + implications <- proofObligationsAsImplications bak + clearProofObligations bak + + -- log to stdout + let logData = defaultLogData + { logCallbackVerbose = \_ -> putStrLn + , logReason = "SAW inv" + } + Z3.runZ3Horn sym True logData uninterp_inv_fns implications >>= \case + Sat sub -> return sub + Unsat{} -> fail "Prover returned Infeasible" + Unknown -> fail "Prover returned Fail" + + +-- | Get proof obligations as What4 implications. +proofObligationsAsImplications :: IsSymBackend sym bak => bak -> IO [Pred sym] +proofObligationsAsImplications bak = do + let sym = backendGetSym bak + convertProofObligationsAsImplications sym =<< getProofObligations bak + +-- | Convert proof obligations to What4 implications. +convertProofObligationsAsImplications :: IsSymInterface sym => sym -> ProofObligations sym -> IO [Pred sym] +convertProofObligationsAsImplications sym goals = do + let obligations = maybe [] PG.goalsToList goals + forM obligations $ \(AS.ProofGoal hyps (LabeledPred concl _err)) -> do + hyp <- assumptionsPred sym hyps + impliesPred sym hyp concl + +-- | Get the set of uninterpreted constants that appear in the path condition. +pathConditionUninterpConstants :: IsSymBackend sym bak => bak -> IO (Set (Some (BoundVar sym))) +pathConditionUninterpConstants bak = do + let sym = backendGetSym bak + exprUninterpConstants sym <$> getPathCondition bak + +-- | Get the set of uninterpreted constants that appear in the proof obligations. +proofObligationsUninterpConstants :: IsSymBackend sym bak => bak -> IO (Set (Some (BoundVar sym))) +proofObligationsUninterpConstants bak = do + let sym = backendGetSym bak + foldMap (exprUninterpConstants sym) <$> proofObligationsAsImplications bak + + ppProofObligation :: IsExprBuilder sym => sym -> ProofObligation sym -> IO (PP.Doc ann) ppProofObligation sym (AS.ProofGoal asmps gl) = do as <- flattenAssumptions sym asmps diff --git a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs index dada74071..38ea32b42 100644 --- a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs +++ b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs @@ -166,7 +166,7 @@ traverseGoalsWithAssumptions f gls = -- primarily a debugging aid, to ensure that stack management -- remains well-bracketed. newtype FrameIdentifier = FrameIdentifier Word64 - deriving(Eq,Ord) + deriving(Eq,Ord,Show) -- | A data-strucutre that can incrementally collect goals in context. diff --git a/crucible/src/Lang/Crucible/CFG/Expr.hs b/crucible/src/Lang/Crucible/CFG/Expr.hs index 5455f9e15..e823bdbbc 100644 --- a/crucible/src/Lang/Crucible/CFG/Expr.hs +++ b/crucible/src/Lang/Crucible/CFG/Expr.hs @@ -75,7 +75,6 @@ import qualified Data.Parameterized.TH.GADT as U import Data.Parameterized.TraversableFC import What4.Interface (RoundingMode(..),StringLiteral(..), stringLiteralInfo) -import What4.InterpretedFloatingPoint (X86_80Val(..)) import Lang.Crucible.CFG.Extension import Lang.Crucible.FunctionHandle diff --git a/crucible/src/Lang/Crucible/FunctionHandle.hs b/crucible/src/Lang/Crucible/FunctionHandle.hs index 269d086bd..6bb84138c 100644 --- a/crucible/src/Lang/Crucible/FunctionHandle.hs +++ b/crucible/src/Lang/Crucible/FunctionHandle.hs @@ -34,6 +34,7 @@ module Lang.Crucible.FunctionHandle , emptyHandleMap , insertHandleMap , lookupHandleMap + , updateHandleMap , searchHandleMap , handleMapToHandles -- * Reference cells @@ -44,6 +45,7 @@ module Lang.Crucible.FunctionHandle import Data.Hashable import Data.Kind +import Data.Functor.Identity import qualified Data.List as List import Data.Ord (comparing) @@ -217,6 +219,19 @@ lookupHandleMap hdl (FnHandleMap m) = Just (HandleElt _ x) -> Just x Nothing -> Nothing +-- | Update the entry of the function handle in the map. +updateHandleMap :: (f args ret -> f args ret) + -> FnHandle args ret + -> FnHandleMap f + -> FnHandleMap f +updateHandleMap f hdl (FnHandleMap m) = + FnHandleMap $ MapF.updatedValue $ runIdentity $ + MapF.updateAtKey + (handleID hdl) + (Identity Nothing) + (\(HandleElt hdl' x) -> Identity $ MapF.Set $ HandleElt hdl' $ f x) + m + -- | Lookup the function name in the map by a linear scan of all -- entries. This will be much slower than using 'lookupHandleMap' to -- find the function by ID, so the latter should be used if possible. diff --git a/crucible/src/Lang/Crucible/Simulator/EvalStmt.hs b/crucible/src/Lang/Crucible/Simulator/EvalStmt.hs index c3cb1dd10..c155f4f91 100644 --- a/crucible/src/Lang/Crucible/Simulator/EvalStmt.hs +++ b/crucible/src/Lang/Crucible/Simulator/EvalStmt.hs @@ -60,7 +60,6 @@ import Prettyprinter import What4.Config import What4.Interface -import What4.InterpretedFloatingPoint (freshFloatConstant) import What4.Partial import What4.ProgramLoc diff --git a/crucible/src/Lang/Crucible/Types.hs b/crucible/src/Lang/Crucible/Types.hs index 1b01ffd04..156745756 100644 --- a/crucible/src/Lang/Crucible/Types.hs +++ b/crucible/src/Lang/Crucible/Types.hs @@ -95,16 +95,7 @@ module Lang.Crucible.Types , module Data.Parameterized.NatRepr , module Data.Parameterized.SymbolRepr , module What4.BaseTypes - , FloatInfo - , HalfFloat - , SingleFloat - , DoubleFloat - , QuadFloat - , X86_80Float - , DoubleDoubleFloat - , FloatInfoRepr(..) - , FloatInfoToBitWidth - , floatInfoToBVTypeRepr + , module What4.InterpretedFloatingPoint ) where import Data.Hashable diff --git a/crux-llvm/test-data/golden/golden/float-cast2.z3.good b/crux-llvm/test-data/golden/golden/float-cast2.z3.good index 4334bf91d..63af98236 100644 --- a/crux-llvm/test-data/golden/golden/float-cast2.z3.good +++ b/crux-llvm/test-data/golden/golden/float-cast2.z3.good @@ -1,2 +1,2 @@ -bvZext 32 (ite (floatIsNaN cX@3:f) 0x0:[1] 0x1:[1]) +ite (floatIsNaN cX@3:f) 0x0:[32] 0x1:[32] [Crux] Overall status: Valid. diff --git a/dependencies/what4 b/dependencies/what4 index 28744e48e..670c8aca5 160000 --- a/dependencies/what4 +++ b/dependencies/what4 @@ -1 +1 @@ -Subproject commit 28744e48e01dc9c35d5aeebb914a9bb425cfe0f1 +Subproject commit 670c8aca552e8b748b20d127d1310430880a45e8