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 build SAW with GHC 9.4:

* GHC 9.4 is more conservative about inferring superclass constraints that arise
  from functional dependencies (see [this
  section](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.4?version_id=b60e52482a666d25638d59cd7e86851ddf971dc1#constraints-derived-from-superclasses)
  of the GHC 9.4 Migration Guide), so we must add explicit `m ~ Identity`
  constraints to certain parts of `heapster-saw` to make it compile with GHC
  9.4.
* I raised the upper version bounds on `aeson` and `vector` to allow building
  them with GHC 9.4.
* The following submodule changes were brought in to support building with
  GHC 9.4:
  * `argo`: #193
  * `crucible`: GaloisInc/crucible#1073

    (This also requires bumping the `llvm-pretty`, `llvm-pretty-bc-parser`,
    and `what4` submodules as a side effect)
  * `language-sally`: GaloisInc/language-sally#13
  * `macaw`: GaloisInc/macaw#330
  * `parameterized-utils`: GaloisInc/parameterized-utils#146

Fixes #1852.
  • Loading branch information
@RyanGlScott
RyanGlScott committed May 26, 2023
1 parent 58c2a8a commit 3d83e0d
Show file tree
Hide file tree
Showing 12 changed files with 21 additions and 24 deletions.
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/language-sally
Submodule language-sally updated 1 files
+1 −1 language-sally.cabal
2 changes: 1 addition & 1 deletion deps/llvm-pretty
Submodule llvm-pretty updated from 64d43d to b13493
2 changes: 1 addition & 1 deletion deps/llvm-pretty-bc-parser
Submodule llvm-pretty-bc-parser updated 24 files
+41 −7 .github/workflows/build.yml
+53 −21 .github/workflows/llvm-quick-fuzz.yml
+2 −0 .gitignore
+49 −31 README.md
+286 −129 disasm-test/Main.hs
+9 −0 disasm-test/tests/T189.c
+29 −0 disasm-test/tests/T189.ll
+43 −0 disasm-test/tests/di-arg-list.at-least-llvm13.ll
+4 −0 disasm-test/tests/di-arg-list.c
+3 −0 disasm-test/tests/poison.at-least-llvm12.ll
+14 −0 doc/developing.md
+1 −1 llvm-pretty
+15 −3 llvm-pretty-bc-parser.cabal
+17 −20 regression-test/Main.hs
+134 −42 src/Data/LLVM/BitCode/BitString.hs
+53 −67 src/Data/LLVM/BitCode/Bitstream.hs
+309 −98 src/Data/LLVM/BitCode/GetBits.hs
+3 −1 src/Data/LLVM/BitCode/IR.hs
+82 −40 src/Data/LLVM/BitCode/IR/Constants.hs
+40 −3 src/Data/LLVM/BitCode/IR/Function.hs
+50 −8 src/Data/LLVM/BitCode/IR/Metadata.hs
+8 −2 src/Data/LLVM/BitCode/IR/Module.hs
+7 −7 src/Data/LLVM/BitCode/Record.hs
+10 −0 unit-test/Tests/Instances.hs
2 changes: 1 addition & 1 deletion deps/macaw
Submodule macaw updated 30 files
+12 −4 .github/workflows/ci.yaml
+2 −0 base/macaw-base.cabal
+1 −0 base/src/Data/Macaw/CFG/Core.hs
+5 −2 base/src/Data/Macaw/CFG/Rewriter.hs
+1 −0 base/src/Data/Macaw/Memory.hs
+15 −0 base/src/Data/Macaw/Panic.hs
+34 −34 cabal.project.freeze.ghc-8.10.7
+0 −283 cabal.project.freeze.ghc-8.8.4
+44 −42 cabal.project.freeze.ghc-9.2.7
+61 −59 cabal.project.freeze.ghc-9.4.4
+1 −1 deps/asl-translator
+1 −1 deps/bv-sized
+1 −1 deps/bv-sized-float
+1 −1 deps/crucible
+1 −1 deps/dismantle
+1 −1 deps/grift
+1 −1 deps/llvm-pretty
+1 −1 deps/llvm-pretty-bc-parser
+1 −1 deps/macaw-loader
+1 −1 deps/semmc
+1 −1 deps/what4
+1 −0 macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/Functions.hs
+1 −0 macaw-ppc/src/Data/Macaw/PPC/Disassemble.hs
+1 −0 macaw-ppc/src/Data/Macaw/PPC/Identify.hs
+1 −0 macaw-ppc/tests/PPC64InstructionCoverage.hs
+1 −0 macaw-ppc/tests/PPCTests.hs
+1 −0 macaw-ppc/tests/Shared.hs
+1 −0 macaw-semmc/src/Data/Macaw/SemMC/Operands.hs
+1 −0 macaw-semmc/src/Data/Macaw/SemMC/Simplify.hs
+1 −0 refinement/src/Data/Macaw/Refinement/Solver.hs
2 changes: 1 addition & 1 deletion deps/parameterized-utils
Submodule parameterized-utils updated 9 files
+8 −5 .github/workflows/test.yml
+13 −0 Changelog.md
+8 −7 parameterized-utils.cabal
+1 −1 src/Data/Parameterized/Classes.hs
+1 −1 src/Data/Parameterized/ClassesC.hs
+2 −2 src/Data/Parameterized/Context/Safe.hs
+2 −2 src/Data/Parameterized/Context/Unsafe.hs
+1 −0 src/Data/Parameterized/Fin.hs
+1 −1 src/Data/Parameterized/Some.hs
2 changes: 1 addition & 1 deletion deps/what4
Submodule what4 updated 6 files
+22 −0 what4/doc/arithdomain.cry
+8 −0 what4/src/What4/Expr/Builder.hs
+6 −0 what4/src/What4/Utils/BVDomain.hs
+55 −0 what4/src/What4/Utils/BVDomain/Arith.hs
+3 −0 what4/test/BVDomTests.hs
+1 −1 what4/what4.cabal
2 changes: 1 addition & 1 deletion heapster-saw/heapster-saw.cabal
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ library
filepath,
language-rust,
hobbits ^>= 1.4,
aeson >= 1.5 && < 2.1,
aeson >= 1.5 && < 2.2,
th-abstraction,
template-haskell,
extra
Expand Down
13 changes: 5 additions & 8 deletions heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2972,7 +2972,7 @@ instance (NuMatching a, Substable PermVarSubst a Identity) =>
[nuMP| EqProofCons eqp' eq_step |] ->
EqProofCons <$> genSubst s eqp' <*> genSubst s eq_step

instance SubstVar PermVarSubst m =>
instance m ~ Identity =>
Substable PermVarSubst (SimplImpl ps_in ps_out) m where
genSubst s mb_impl = case mbMatch mb_impl of
[nuMP| SImpl_Drop x p |] ->
Expand Down Expand Up @@ -3251,7 +3251,7 @@ instance SubstVar PermVarSubst m =>
[nuMP| SImpl_ElimAnyToPtr x fp |] ->
SImpl_ElimAnyToPtr <$> genSubst s x <*> genSubst s fp

instance SubstVar PermVarSubst m =>
instance m ~ Identity =>
Substable PermVarSubst (PermImpl1 ps_in ps_out) m where
genSubst s mb_impl = case mbMatch mb_impl of
[nuMP| Impl1_Fail err |] -> Impl1_Fail <$> genSubst s err
Expand Down Expand Up @@ -3291,17 +3291,15 @@ instance SubstVar PermVarSubst m =>
Impl1_TryProveBVProp <$> genSubst s x <*> genSubst s prop <*>
return (mbLift prop_str)

-- FIXME: shouldn't need the SubstVar PermVarSubst m assumption...
instance (NuMatchingAny1 r, SubstVar PermVarSubst m,
instance (NuMatchingAny1 r, m ~ Identity,
Substable1 PermVarSubst r m) =>
Substable PermVarSubst (PermImpl r ps) m where
genSubst s mb_impl = case mbMatch mb_impl of
[nuMP| PermImpl_Done r |] -> PermImpl_Done <$> genSubst1 s r
[nuMP| PermImpl_Step impl1 mb_impls |] ->
PermImpl_Step <$> genSubst s impl1 <*> genSubst s mb_impls

-- FIXME: shouldn't need the SubstVar PermVarSubst m assumption...
instance (NuMatchingAny1 r, SubstVar PermVarSubst m,
instance (NuMatchingAny1 r, m ~ Identity,
Substable1 PermVarSubst r m) =>
Substable PermVarSubst (MbPermImpls r bs_pss) m where
genSubst s mb_impls = case mbMatch mb_impls of
Expand All @@ -3317,8 +3315,7 @@ instance SubstVar s m => Substable s (OrListDisj ps a disj) m where
instance SubstVar s m => Substable1 s (OrListDisj ps a) m where
genSubst1 = genSubst

-- FIXME: shouldn't need the SubstVar PermVarSubst m assumption...
instance SubstVar PermVarSubst m =>
instance m ~ Identity =>
Substable PermVarSubst (LocalPermImpl ps_in ps_out) m where
genSubst s (mbMatch -> [nuMP| LocalPermImpl impl |]) =
LocalPermImpl <$> genSubst s impl
Expand Down
8 changes: 4 additions & 4 deletions heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -809,7 +809,7 @@ instance SubstVar PermVarSubst m =>
[nuMP| TypedRegsCons rs r |] ->
TypedRegsCons <$> genSubst s rs <*> genSubst s r

instance (NuMatchingAny1 r, SubstVar PermVarSubst m,
instance (NuMatchingAny1 r, m ~ Identity,
Substable1 PermVarSubst r m) =>
Substable PermVarSubst (AnnotPermImpl r ps) m where
genSubst s (mbMatch -> [nuMP| AnnotPermImpl err impl |]) =
Expand Down Expand Up @@ -1003,7 +1003,7 @@ instance SubstVar PermVarSubst m =>
Substable1 PermVarSubst (TypedJumpTarget blocks tops) m where
genSubst1 = genSubst

instance SubstVar PermVarSubst m =>
instance m ~ Identity =>
Substable PermVarSubst (TypedTermStmt blocks tops rets ps_in) m where
genSubst s mb_x = case mbMatch mb_x of
[nuMP| TypedJump impl_tgt |] -> TypedJump <$> genSubst s impl_tgt
Expand All @@ -1015,7 +1015,7 @@ instance SubstVar PermVarSubst m =>
[nuMP| TypedErrorStmt str r |] ->
TypedErrorStmt (mbLift str) <$> genSubst s r

instance (PermCheckExtC ext exprExt, SubstVar PermVarSubst m) =>
instance (PermCheckExtC ext exprExt, m ~ Identity) =>
Substable PermVarSubst (TypedStmtSeq ext blocks tops rets ps_in) m where
genSubst s mb_x = case mbMatch mb_x of
[nuMP| TypedImplStmt impl_seq |] ->
Expand All @@ -1027,7 +1027,7 @@ instance (PermCheckExtC ext exprExt, SubstVar PermVarSubst m) =>
TypedTermStmt (mbLift loc) <$> genSubst s term_stmt


instance (PermCheckExtC ext exprExt, SubstVar PermVarSubst m) =>
instance (PermCheckExtC ext exprExt, m ~ Identity) =>
Substable1 PermVarSubst (TypedStmtSeq ext blocks tops rets) m where
genSubst1 = genSubst

Expand Down
6 changes: 3 additions & 3 deletions saw-remote-api/saw-remote-api.cabal
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,8 @@ common errors
-Werror=overlapping-patterns

common deps
build-depends: base >=4.11.1.0 && <4.17,
aeson >= 1.4.2 && < 2.1,
build-depends: base >=4.11.1.0 && <4.18,
aeson >= 1.4.2 && < 2.2,
aig,
argo,
base64-bytestring,
Expand All @@ -60,7 +60,7 @@ common deps
silently,
text,
unordered-containers,
vector >= 0.12 && < 0.13,
vector >= 0.12 && < 0.14,
cryptol-remote-api
default-language: Haskell2010

Expand Down
2 changes: 1 addition & 1 deletion saw-script.cabal
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ library
default-language: Haskell2010
build-depends:
base >= 4.9
, aeson >= 2.0 && < 2.1
, aeson >= 2.0 && < 2.2
, aig
, array
, binary
Expand Down

0 comments on commit 3d83e0d

Please sign in to comment.