Bump what4 submodule to version 1.4

The only substantial code change required was to delete an unused dependency on `what4-serialize`. This brings in submodule changes from the following: * GaloisInc/asl-translator#48, which performed a similar `what4` adaptation. * GaloisInc/macaw#328, 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 22, 2023 · a615460 · a615460
1 parent 6bedaeb
commit a615460
Show file tree

Hide file tree

Showing 8 changed files with 5 additions and 10 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -16,9 +16,6 @@
 [submodule "submodules/what4"]
 	path = submodules/what4
 	url = [email protected]:GaloisInc/what4.git
-[submodule "submodules/what4-serialize"]
-	path = submodules/what4-serialize
-	url = [email protected]:GaloisInc/what4-serialize.git
 [submodule "submodules/semmc"]
 	path = submodules/semmc
 	url = [email protected]:GaloisInc/semmc.git

diff --git a/cabal.project.dist b/cabal.project.dist
@@ -14,7 +14,6 @@ packages:
     submodules/asl-translator
     submodules/arm-asl-parser
     submodules/what4/what4
-    submodules/what4-serialize
     submodules/semmc/semmc
     submodules/semmc/semmc-synthesis
     submodules/semmc/semmc-learning

diff --git a/submodules/asl-translator b/submodules/asl-translator
diff --git a/submodules/crucible b/submodules/crucible
diff --git a/submodules/macaw b/submodules/macaw
diff --git a/submodules/semmc b/submodules/semmc
diff --git a/submodules/what4 b/submodules/what4
diff --git a/submodules/what4-serialize b/submodules/what4-serialize
+0 −3		.gitmodules
+4 −4		Makefile
+ −		archived/functions-norm-lite.what4.gz
+ −		archived/functions-norm.what4.gz
+ −		archived/instructions-norm-lite.what4.gz
+ −		archived/instructions-norm.what4.gz
+4 −7		asl-translator.cabal
+0 −1		cabal.project.newbuild
+22 −12		data/extra_defs.asl
+89 −15		data/parsed/extra_defs.sexpr
+16 −16		docs/DESIGN.md
+1 −1		exe/Concrete.hs
+5 −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
+3 −7		lib/Language/ASL/SyntaxTraverse.hs
+2 −2		lib/Language/ASL/Translation.hs
+16 −9		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