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
`semmc` repo build with GHC 9.4:

* GHC 9.4 is pickier about undecidable superclass checking. As such, I needed to
  explicitly enable `UndecidableSuperClasses` in a handful of places.
* The upper version bounds on `text` were raised to `< 2.1` to allow building
  with `text-2.0.*`, which is bundled with GHC 9.4.
* The following submodule changes were brought in to support building with
  GHC 9.4:
  * `asl-translator`: GaloisInc/asl-translator#51
  * `crucible`: GaloisInc/crucible#1073
  * `dismantle`: GaloisInc/dismantle#40
  • Loading branch information
RyanGlScott committed Apr 17, 2023
1 parent 9b2a03b commit 3606eac
Show file tree
Hide file tree
Showing 11 changed files with 16 additions and 6 deletions.
6 changes: 6 additions & 0 deletions cabal.project.newbuild
Original file line number Diff line number Diff line change
Expand Up @@ -31,3 +31,9 @@ constraints:
regex == 1.0.1.3
allow-newer:
regex:template-haskell

-- TODO RGS: Remove this when on Hackage
source-repository-package
type: git
location: https://github.com/GaloisInc/s-cargot-letbind
tag: a00bba1ffa27a605f4d2f9585bf7ea77e1c63726
2 changes: 1 addition & 1 deletion semmc-learning/semmc-learning.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ library
mtl,
containers,
stm,
text >= 1 && < 2,
text >= 1 && < 2.1,
time,
filepath,
bytestring >=0.10 && < 0.12,
Expand Down
1 change: 1 addition & 0 deletions semmc-ppc/src/SemMC/Architecture/PPC.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module SemMC.Architecture.PPC ( AnyPPC, Variant, V32, V64
, VariantRepr(..), KnownVariant(..)
Expand Down
2 changes: 1 addition & 1 deletion semmc-toy/semmc-toy.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ library
, containers >= 0.5.8
, filepath
, located-base
, text >= 1 && < 2
, text >= 1 && < 2.1
, crucible >= 0.4
, crucible-llvm
, dismantle-tablegen
Expand Down
2 changes: 1 addition & 1 deletion semmc/semmc.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ library
stm,
BoundedChan,
located-base,
text >= 1 && < 2,
text >= 1 && < 2.1,
exceptions >= 0.8 && < 0.11,
s-cargot >= 0.1.4.0 && < 0.2,
s-cargot-letbind >= 0.2.2.0 && < 0.3,
Expand Down
1 change: 1 addition & 0 deletions semmc/src/SemMC/Architecture.hs
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
Expand Down
1 change: 1 addition & 0 deletions semmc/src/SemMC/Architecture/Concrete.hs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module SemMC.Architecture.Concrete (
RegisterizedInstruction(..),
LiteralRef(..),
Expand Down
1 change: 1 addition & 0 deletions semmc/src/SemMC/Architecture/Pseudo.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
-- | Support for "pseudo" archtiectures that wrap other architectures to provide
-- extra operands beyond the native architecture
--
Expand Down
2 changes: 1 addition & 1 deletion submodules/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 submodules/dismantle

0 comments on commit 3606eac

Please sign in to comment.