Skip to content

Commit

Permalink
Support building with GHC 9.4
Browse files Browse the repository at this point in the history
This contains a variety of tweaks needed to make the libraries in the
`macaw` repo build with GHC 9.4:

* `ST` no longer has a `MonadFail` instance. See
  [this section](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.4?version_id=b60e52482a666d25638d59cd7e86851ddf971dc1#st-is-no-longer-an-instance-of-monadfail)
  of the GHC 9.4 Migration Guide. To adapt to this change, I had to change some
  uses of `fail` to `panic`, and I also had to avoid some partial pattern
  matches in `do`-notation to avoid incurring `MonadFail (ST s)` constraints.
* GHC 9.4 is pickier about undecidable superclass checking. As such, I needed to
  explicitly enable `UndecidableSuperClasses` in a handful of places.
* The following submodule changes were brought in to support building with
  GHC 9.4:
  * `asl-translator`: GaloisInc/asl-translator#51
  * `bv-sized`: GaloisInc/bv-sized#27
  * `bv-sized-float`: GaloisInc/bv-sized-float#4
  * `crucible`: GaloisInc/crucible#1073

    (This also requires bumping the `llvm-pretty`, `llvm-pretty-bc-parser`,
    and `what4` submodules as a side effect)
  * `dismantle`: GaloisInc/dismantle#40
  * `grift`: GaloisInc/grift#8
  * `macaw-loader`: GaloisInc/macaw-loader#17
  * `semmc`: GaloisInc/semmc#79
  • Loading branch information
RyanGlScott committed Apr 18, 2023
1 parent 02c2bc4 commit e55add0
Show file tree
Hide file tree
Showing 15 changed files with 19 additions and 13 deletions.
1 change: 1 addition & 0 deletions base/src/Data/Macaw/CFG/Core.hs
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ single CFG.
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Data.Macaw.CFG.Core
( -- * Stmt level declarations
Stmt(..)
Expand Down
7 changes: 5 additions & 2 deletions base/src/Data/Macaw/CFG/Rewriter.hs
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,7 @@ import Data.STRef
import Data.Macaw.CFG.App
import Data.Macaw.CFG.Core
import Data.Macaw.Memory
import qualified Data.Macaw.Panic as P
import Data.Macaw.Types
import Data.Macaw.CFG.Block (TermStmt)

Expand Down Expand Up @@ -185,7 +186,8 @@ addBinding srcId val = Rewriter $ do
lift $ do
m <- readSTRef ref
when (MapF.member srcId m) $ do
fail $ "Assignment " ++ show srcId ++ " is already bound."
P.panic P.Base "addBinding"
["Assignment " ++ show srcId ++ " is already bound."]
writeSTRef ref $! MapF.insert srcId val m

-- | Return true if values are identical
Expand Down Expand Up @@ -716,7 +718,8 @@ rewriteValue v =
srcMap <- lift $ readSTRef ref
case MapF.lookup aid srcMap of
Just tgtVal -> pure tgtVal
Nothing -> fail $ "Could not resolve source assignment " ++ show aid ++ "."
Nothing -> P.panic P.Base "rewriteValue"
["Could not resolve source assignment " ++ show aid ++ "."]
Initial r -> pure (Initial r)

-- | Apply optimizations to a statement.
Expand Down
1 change: 1 addition & 0 deletions base/src/Data/Macaw/Memory.hs
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ Declares 'Memory', a type for representing segmented memory with permissions.
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Data.Macaw.Memory
( Memory
-- * Inspecting memory
Expand Down
2 changes: 1 addition & 1 deletion deps/bv-sized
2 changes: 1 addition & 1 deletion deps/bv-sized-float
2 changes: 1 addition & 1 deletion deps/crucible
Submodule crucible updated 65 files
+11 −5 .github/workflows/crucible-go-build.yml
+11 −5 .github/workflows/crucible-jvm-build.yml
+11 −5 .github/workflows/crucible-wasm-build.yml
+14 −7 .github/workflows/crux-llvm-build.yml
+8 −3 .github/workflows/crux-mir-build.yml
+38 −34 cabal.GHC-8.10.7.config
+38 −34 cabal.GHC-8.8.4.config
+0 −295 cabal.GHC-9.2.2.config
+0 −294 cabal.GHC-9.2.3.config
+42 −38 cabal.GHC-9.2.7.config
+58 −54 cabal.GHC-9.4.4.config
+1 −0 crucible-concurrency/src/Cruces/ExploreCrux.hs
+2 −2 crucible-llvm/crucible-llvm.cabal
+7 −12 crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs
+2 −0 crucible-llvm/src/Lang/Crucible/LLVM/TypeContext.hs
+1 −0 crucible-llvm/test/TestMemory.hs
+1 −1 crucible-mir/crucible-mir.cabal
+1 −1 crucible-mir/src/Mir/Generator.hs
+28 −14 crucible-mir/src/Mir/Trans.hs
+7 −3 crucible-mir/src/Mir/TransCustom.hs
+2 −2 crucible-symio/crucible-symio.cabal
+0 −3 crucible-symio/src/Data/Parameterized/IntervalsMap.hs
+0 −3 crucible-symio/src/What4/CachedArray.hs
+2 −2 crucible-syntax/crucible-syntax.cabal
+1 −0 crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs
+1 −1 crucible-wasm/crucible-wasm.cabal
+1 −1 crucible-wasm/src/Lang/Crucible/Wasm.hs
+1 −1 crucible-wasm/src/Lang/Crucible/Wasm/Instantiate.hs
+34 −6 crucible-wasm/src/Lang/Crucible/Wasm/Main.hs
+74 −23 crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs
+1 −0 crucible-wasm/test-data/.gitignore
+0 −0 crucible-wasm/test-data/basic-binary.good
+ crucible-wasm/test-data/basic-binary.wasm
+1 −0 crucible-wasm/test-data/basic-script.good
+6 −0 crucible-wasm/test-data/basic-script.wast
+0 −2 crucible-wasm/test-data/basic.config
+0 −0 crucible-wasm/test-data/basic.z3.result.out
+1 −0 crucible-wasm/test-data/multi-value.good
+39 −0 crucible-wasm/test-data/multi-value.wast
+1 −0 crucible-wasm/test-data/sign-extend.good
+57 −0 crucible-wasm/test-data/sign-extend.wast
+13 −14 crucible-wasm/test/Test.hs
+1 −1 crucible/crucible.cabal
+2 −2 crux-llvm/README.md
+2 −2 crux-llvm/crux-llvm.cabal
+1 −1 crux-mir/README.md
+1 −1 crux-mir/crux-mir.cabal
+1 −1 crux/crux.cabal
+10 −2 crux/src/Crux.hs
+1 −0 crux/src/Crux/Goal.hs
+1 −1 dependencies/aig
+1 −1 dependencies/haskell-wasm
+1 −1 dependencies/llvm-pretty
+1 −1 dependencies/llvm-pretty-bc-parser
+1 −1 dependencies/what4
+1 −0 uc-crux-llvm/src/UCCrux/LLVM/Overrides/Skip.hs
+1 −0 uc-crux-llvm/src/UCCrux/LLVM/Overrides/Spec.hs
+1 −0 uc-crux-llvm/src/UCCrux/LLVM/Overrides/Unsound.hs
+1 −0 uc-crux-llvm/src/UCCrux/LLVM/Postcondition/Apply.hs
+1 −0 uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs
+1 −0 uc-crux-llvm/src/UCCrux/LLVM/Specs/Type.hs
+1 −0 uc-crux-llvm/src/UCCrux/LLVM/View/Postcond.hs
+1 −0 uc-crux-llvm/src/UCCrux/LLVM/View/Precond.hs
+1 −0 uc-crux-llvm/src/UCCrux/LLVM/View/Specs.hs
+3 −3 uc-crux-llvm/uc-crux-llvm.cabal
2 changes: 1 addition & 1 deletion deps/dismantle
2 changes: 1 addition & 1 deletion deps/grift
2 changes: 1 addition & 1 deletion deps/llvm-pretty
2 changes: 1 addition & 1 deletion deps/semmc
Submodule semmc updated 35 files
+15 −3 .github/workflows/ci.yml
+31 −31 cabal.GHC-8.10.7.config
+0 −267 cabal.GHC-8.8.4.config
+37 −35 cabal.GHC-9.2.7.config
+52 −51 cabal.GHC-9.4.4.config
+1 −0 semmc-arm/src/SemMC/Architecture/ARM/Eval.hs
+1 −0 semmc-arm/test/TestFormulas.hs
+1 −0 semmc-arm/tools/GenBase.hs
+1 −1 semmc-learning/semmc-learning.cabal
+1 −0 semmc-learning/src/SemMC/Stochastic/CandidateProgram.hs
+1 −0 semmc-ppc/src/SemMC/Architecture/PPC.hs
+1 −0 semmc-ppc/src/SemMC/Architecture/PPC/Eval.hs
+1 −0 semmc-ppc/src/SemMC/Architecture/PPC/Pseudo.hs
+1 −0 semmc-ppc/tests/Main.hs
+2 −1 semmc-ppc/tools/GenBase.hs
+1 −0 semmc-ppc/tools/SynthDemo.hs
+1 −0 semmc-synthesis/src/SemMC/Synthesis.hs
+1 −1 semmc-synthesis/src/SemMC/Synthesis/Cegis/EvalFormula.hs
+3 −3 semmc-synthesis/src/SemMC/Synthesis/Cegis/Types.hs
+1 −0 semmc-synthesis/src/SemMC/Synthesis/Core.hs
+1 −0 semmc-synthesis/src/SemMC/Synthesis/DivideAndConquer.hs
+1 −0 semmc-synthesis/src/SemMC/Synthesis/Testing.hs
+1 −1 semmc-toy/semmc-toy.cabal
+1 −0 semmc-toy/src/SemMC/Toy/Tests.hs
+2 −2 semmc/semmc.cabal
+6 −5 semmc/src/SemMC/Architecture.hs
+1 −0 semmc/src/SemMC/Architecture/AllocatedOperand.hs
+1 −0 semmc/src/SemMC/Architecture/Concrete.hs
+1 −0 semmc/src/SemMC/Architecture/Pseudo.hs
+1 −0 semmc/src/SemMC/Formula/Equivalence.hs
+2 −2 semmc/tests/semstore/ParamFormulaTests.hs
+1 −1 submodules/asl-translator
+1 −1 submodules/crucible
+1 −1 submodules/dismantle
+1 −1 submodules/llvm-pretty
1 change: 1 addition & 0 deletions macaw-semmc/src/Data/Macaw/SemMC/Operands.hs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Macaw.SemMC.Operands (
ExtractValue(..),
Expand Down

0 comments on commit e55add0

Please sign in to comment.