Bump what4 submodule to version 1.4

The only other changes required are (1) deleting an unused dependency on `what4-serialize`, and (2) raising upper version bounds on `what4`. This brings in submodule changes from the following: * GaloisInc/asl-translator#48, which performed a similar `what4` adaptation. * GaloisInc/semmc#78, which performed a similar `what4` adaptation. * GaloisIns/crucible#1068, which ensures that everything can build against `tasty-sugar >= 2.0` (the version of the library that `what4-1.4` depends on).
GaloisInc · Mar 21, 2023 · e6a3fb0 · e6a3fb0
1 parent 88d0249
commit e6a3fb0
Show file tree

Hide file tree

Showing 9 changed files with 6 additions and 11 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -31,9 +31,6 @@
 [submodule "deps/arm-asl-parser"]
 	path = deps/arm-asl-parser
 	url = https://github.com/GaloisInc/arm-asl-parser.git
-[submodule "deps/what4-serialize"]
-	path = deps/what4-serialize
-	url = https://github.com/GaloisInc/what4-serialize.git
 [submodule "deps/what4"]
 	path = deps/what4
 	url = [email protected]:GaloisInc/what4.git

diff --git a/cabal.project.dist b/cabal.project.dist
@@ -29,7 +29,6 @@ packages: base/
           deps/crucible/crucible-llvm/
           deps/crucible/crucible-symio/
           deps/what4/what4/
-          deps/what4-serialize/
           deps/dwarf/
           deps/elf-edit/
           deps/flexdis86/

diff --git a/deps/asl-translator b/deps/asl-translator
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/semmc b/deps/semmc
diff --git a/deps/what4 b/deps/what4
diff --git a/deps/what4-serialize b/deps/what4-serialize
diff --git a/macaw-semmc/macaw-semmc.cabal b/macaw-semmc/macaw-semmc.cabal
@@ -39,7 +39,7 @@ library
                        semmc,
                        bv-sized >= 1 && < 1.1,
                        libBF >= 0.6 && < 0.7,
-                       what4 >= 1.1 && < 1.4
+                       what4 >= 1.1 && < 1.5
   hs-source-dirs:      src
   default-language:    Haskell2010
   ghc-options:         -Wall -Wcompat
diff --git a/symbolic/macaw-symbolic.cabal b/symbolic/macaw-symbolic.cabal
@@ -27,7 +27,7 @@ library
     text,
     vector,
     bytestring,
-    what4 >= 1.1 && < 1.4
+    what4 >= 1.1 && < 1.5
 
   hs-source-dirs: src
+0 −3		.gitmodules
+3 −4		asl-translator.cabal
+0 −1		cabal.project.newbuild
+16 −16		docs/DESIGN.md
+1 −1		exe/Concrete.hs
+1 −1		exe/Main.hs
+11 −0		lib/Data/Parameterized/SomeSome.hs
+1 −1		lib/Language/ASL/Crucible.hs
+1 −1		lib/Language/ASL/Formulas.hs
+1 −1		lib/Language/ASL/Formulas/Normalize.hs
+3 −3		lib/Language/ASL/Formulas/Serialize.hs
+2 −2		lib/Language/ASL/Translation.hs
+5 −4		lib/Language/ASL/Translation/Driver.hs
+1 −1		lib/Util/Log.hs
+1 −1		submodules/what4
+0 −1		submodules/what4-serialize
+1 −1		tests/Translation/Main.hs
+0 −3		.gitmodules
+89 −90		cabal.GHC-8.10.7.config
+90 −91		cabal.GHC-8.8.4.config
+87 −90		cabal.GHC-9.0.2.config
+87 −90		cabal.GHC-9.2.2.config
+0 −1		cabal.project.newbuild
+1 −2		semmc-aarch32/semmc-aarch32.cabal
+5 −5		semmc-aarch32/src/SemMC/Architecture/ARM/ASL.hs
+1 −3		semmc/semmc.cabal
+1 −2		semmc/src/SemMC/Formula/Parser.hs
+8 −9		semmc/src/SemMC/Formula/Printer.hs
+1 −1		submodules/asl-translator
+1 −1		submodules/crucible
+1 −1		submodules/what4
+0 −1		submodules/what4-serialize
+4 −2		.github/workflows/gen_matrix.pl
+14 −7		.github/workflows/test.yml
+5 −5		README.md
+1 −1		dependencies/aig
+1 −1		what4-abc/what4-abc.cabal
+1 −1		what4-blt/what4-blt.cabal
+43 −34		what4-transition-system/src/What4/TransitionSystem.hs
+2 −2		what4-transition-system/what4-transition-system.cabal
+33 −0		what4/CHANGES.md
+1 −1		what4/LICENSE
+7 −0		what4/README.md
+1 −1		what4/doc/implementation.md
+2 −0		what4/src/What4/Expr/App.hs
+1 −1		what4/src/What4/Expr/AppTheory.hs
+59 −18		what4/src/What4/Expr/Builder.hs
+2 −3		what4/src/What4/Expr/VarIdentification.hs
+88 −6		what4/src/What4/Interface.hs
+9 −3		what4/src/What4/ProblemFeatures.hs
+47 −0		what4/src/What4/Protocol/Online.hs
+6 −0		what4/src/What4/Protocol/SExp.hs
+454 −18		what4/src/What4/Protocol/SMTLib2.hs
+1 −1		what4/src/What4/Protocol/SMTLib2/Parse.hs
+5 −1		what4/src/What4/Protocol/SMTLib2/Response.hs
+52 −3		what4/src/What4/Protocol/SMTLib2/Syntax.hs
+110 −2		what4/src/What4/Protocol/SMTWriter.hs
+1 −0		what4/src/What4/Protocol/VerilogWriter.hs
+184 −0		what4/src/What4/Serialize/FastSExpr.hs
+436 −0		what4/src/What4/Serialize/Log.hs
+162 −0		what4/src/What4/Serialize/Normalize.hs
+1,070 −0		what4/src/What4/Serialize/Parser.hs
+779 −0		what4/src/What4/Serialize/Printer.hs
+259 −0		what4/src/What4/Serialize/SETokens.hs
+12 −0		what4/src/What4/Solver.hs
+3 −2		what4/src/What4/Solver/Boolector.hs
+4 −4		what4/src/What4/Solver/CVC4.hs
+380 −0		what4/src/What4/Solver/CVC5.hs
+15 −0		what4/src/What4/Solver/Yices.hs
+95 −3		what4/src/What4/Solver/Z3.hs
+1 −0		what4/src/What4/Utils/AbstractDomains.hs
+1 −0		what4/src/What4/Utils/OnlyIntRepr.hs
+127 −0		what4/src/What4/Utils/Serialize.hs
+155 −0		what4/test/Abduct.hs
+1 −0		what4/test/AdapterTest.hs
+3 −1		what4/test/ExprBuilderSMTLib2.hs
+58 −0		what4/test/ExprsTest.hs
+153 −0		what4/test/InvariantSynthesis.hs
+6 −2		what4/test/OnlineSolverTest.hs
+58 −0		what4/test/SerializeTestUtils.hs
+20 −0		what4/test/SerializeTests.hs
+1 −1		what4/test/SolverParserTest.hs
+242 −0		what4/test/SymFnTests.hs
+4 −3		what4/test/TestTemplate.hs
+74 −11		what4/what4.cabal