bump submodules

GaloisInc · Dec 5, 2023 · 4c7d1aa · 4c7d1aa
1 parent d8041ab
commit 4c7d1aa
Show file tree

Hide file tree

Showing 13 changed files with 49 additions and 16 deletions.
diff --git a/cabal.project.dist b/cabal.project.dist
@@ -2,7 +2,6 @@ packages: .
           submodules/llvm-pretty
           submodules/parameterized-utils
           submodules/what4/what4
-          submodules/what4-serialize
           submodules/crucible/crucible
           submodules/crucible/crucible-symio
           submodules/crucible/crucible-llvm

diff --git a/pate.cabal b/pate.cabal
@@ -40,8 +40,9 @@ common shared
                        elf-edit >= 0.39,
                        IntervalMap >= 0.6 && < 0.7,
                        lens >= 4 && < 6,
-                       hashtables >= 1.2 && < 1.3,
-                       mtl >= 2 && < 2.3,
+                       hashtables >= 1.2 && < 1.3.1,
+                       mtl >= 2 && < 2.4,
+                       monadplus,
                        panic >= 0.4 && < 0.5,
                        lumberjack >= 0.1 && < 1.1,
                        prettyprinter >= 1.7 && < 1.8,
@@ -55,7 +56,6 @@ common shared
                        split >= 0.2,
                        parameterized-utils,
                        what4 >= 1 && < 2,
-                       what4-serialize,
                        crucible,
                        crucible-llvm,
                        macaw-base,
@@ -68,7 +68,7 @@ common shared
                        demangler >= 1.3.0.0,
                        semmc,
                        sayable,
-                       text >= 1 && < 1.3,
+                       text >= 1 && < 2.1,
                        tomland >= 1.3 && < 1.4,
                        transformers,
                        time >= 1 && < 2,
@@ -198,6 +198,25 @@ common shared-test
                  text,
                  pate 
 
+-- just used for loading test modules interactively
+library pate-test-base
+  import: shared-test
+  hs-source-dirs: tests, arch
+  other-modules: Pate.AArch32, Pate.PPC
+  build-depends: semmc-aarch32,
+                 macaw-aarch32,
+                 macaw-aarch32-symbolic,
+                 macaw-loader-aarch32,
+                 macaw-ppc,
+                 macaw-ppc-symbolic,
+                 macaw-loader-ppc,
+                 semmc-ppc,
+                 asl-translator,
+                 what4,
+                 dismantle-arm-xml,
+                 dismantle-ppc,
+                 dismantle-tablegen
+
 test-suite pate-test-loaders
   import: shared-test
   type: exitcode-stdio-1.0
@@ -250,6 +269,20 @@ test-suite pate-test-aarch32
                  what4,
                  dismantle-arm-xml
 
+test-suite pate-test-solver
+  import: shared-test
+  type: exitcode-stdio-1.0
+  main-is: SolverTestMain.hs
+  other-modules: Pate.AArch32
+  hs-source-dirs: tests, arch
+  build-depends: semmc-aarch32,
+                 macaw-aarch32,
+                 macaw-aarch32-symbolic,
+                 macaw-loader-aarch32,
+                 asl-translator,
+                 what4,
+                 dismantle-arm-xml
+
 common shared-exec
   ghc-options: -Wall -Wcompat
   default-language: Haskell2010

diff --git a/submodules/asl-translator b/submodules/asl-translator
diff --git a/submodules/crucible b/submodules/crucible
diff --git a/submodules/dismantle b/submodules/dismantle
diff --git a/submodules/flexdis86 b/submodules/flexdis86
diff --git a/submodules/llvm-pretty b/submodules/llvm-pretty
diff --git a/submodules/macaw b/submodules/macaw
diff --git a/submodules/macaw-loader b/submodules/macaw-loader
diff --git a/submodules/parameterized-utils b/submodules/parameterized-utils
diff --git a/submodules/semmc b/submodules/semmc
diff --git a/submodules/what4 b/submodules/what4
diff --git a/tools/pate-repl/Repl.hs b/tools/pate-repl/Repl.hs
@@ -32,7 +32,8 @@ import qualified System.IO as IO
 import qualified System.IO.Unsafe as IO
 import qualified Data.IORef as IO
 import qualified Control.Concurrent as IO
-import           Control.Monad.State ( MonadState, StateT, modify, gets, runStateT, get, put, forM )
+import           Control.Monad ( forM )
+import           Control.Monad.State ( MonadState, StateT, modify, gets, runStateT, get, put )
 import qualified Control.Monad.IO.Class as IO
 import           Data.Proxy
 import qualified Data.Text.IO as Text
+16 −8		.github/workflows/ci-matrix.yml
+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
+6 −9		asl-translator.cabal
+0 −1		cabal.project.newbuild
+23 −25		data/extra_defs.asl
+96,203 −96,203		data/parsed/arm_defs.sexpr
+73 −51		data/parsed/extra_defs.sexpr
+15 −1		data/parsed/support.sexpr
+3 −1		data/support.asl
+16 −16		docs/DESIGN.md
+1 −1		exe/Concrete.hs
+5 −1		exe/Main.hs
+4 −5		lib/Data/Parameterized/AssignTree.hs
+3 −4		lib/Data/Parameterized/CtxFuns.hs
+11 −0		lib/Data/Parameterized/SomeSome.hs
+1 −2		lib/Language/ASL/Crucible.hs
+2 −1		lib/Language/ASL/Formulas.hs
+3 −3		lib/Language/ASL/Formulas/Normalize.hs
+3 −3		lib/Language/ASL/Formulas/Serialize.hs
+1 −0		lib/Language/ASL/Globals.hs
+3 −1		lib/Language/ASL/Globals/Definitions.hs
+0 −1		lib/Language/ASL/StaticExpr.hs
+29 −34		lib/Language/ASL/SyntaxTraverse.hs
+3 −19		lib/Language/ASL/Translation.hs
+20 −17		lib/Language/ASL/Translation/Driver.hs
+0 −1		lib/Language/ASL/Translation/Preprocess.hs
+4 −2		lib/Util/Log.hs
+1 −2		lib/What4/Expr/ExprTree.hs
+1 −1		submodules/arm-asl-parser
+1 −1		submodules/crucible
+1 −1		submodules/dismantle
+1 −1		submodules/what4
+0 −1		submodules/what4-serialize
+1 −1		tests/Translation/Main.hs
+2 −2		.github/workflows/ci.yaml
+0 −103		cabal.project.ghc-8.10.7.freeze
+43 −45		cabal.project.ghc-9.2.8.freeze
+55 −58		cabal.project.ghc-9.4.5.freeze
+98 −0		cabal.project.ghc-9.6.2.freeze
+78 −58		data/optable.xml
+1 −1		deps/elf-edit
+8 −14		flexdis86.cabal
+2 −0		src/Flexdis86/Assembler.hs
+634 −196		src/Flexdis86/Disassembler.hs
+87 −92		src/Flexdis86/InstructionSet.hs
+14 −3		src/Flexdis86/OpTable.hs
+16 −9		src/Flexdis86/Prefixes.hs
+22 −1		src/Flexdis86/Register.hs
+7 −1		src/Flexdis86/Relocation.hs
+7 −1		src/Flexdis86/Segment.hs
+1 −0		tests/Roundtrip.hs
+3 −2		utils/DumpInstr.hs
+18 −9		.github/workflows/ci.yaml
+2 −1		.gitignore
+6 −3		.gitmodules
+3 −2		cabal.project.dist
+13 −3		macaw-loader-aarch32/src/Data/Macaw/BinaryLoader/AArch32.hs
+14 −3		macaw-loader-ppc/src/Data/Macaw/BinaryLoader/PPC.hs
+13 −3		macaw-loader-x86/src/Data/Macaw/BinaryLoader/X86.hs
+1 −0		macaw-loader/src/Data/Macaw/BinaryLoader.hs
+1 −1		submodules/asl-translator
+1 −1		submodules/crucible
+1 −1		submodules/dismantle
+1 −1		submodules/dwarf
+1 −1		submodules/elf-edit
+1 −1		submodules/flexdis86
+1 −0		submodules/llvm-pretty
+1 −0		submodules/llvm-pretty-bc-parser
+1 −1		submodules/macaw
+1 −1		submodules/parameterized-utils
+1 −1		submodules/semmc
+1 −1		submodules/what4
+0 −1		submodules/what4-serialize
+22 −7		.github/workflows/test.yml
+19 −0		Changelog.md
+9 −8		parameterized-utils.cabal
+1 −1		src/Data/Parameterized/Classes.hs
+1 −1		src/Data/Parameterized/ClassesC.hs
+2 −2		src/Data/Parameterized/Context.hs
+5 −4		src/Data/Parameterized/Context/Safe.hs
+4 −3		src/Data/Parameterized/Context/Unsafe.hs
+4 −1		src/Data/Parameterized/DecidableEq.hs
+1 −0		src/Data/Parameterized/Fin.hs
+4 −1		src/Data/Parameterized/Map.hs
+3 −1		src/Data/Parameterized/NatRepr.hs
+3 −0		src/Data/Parameterized/Nonce.hs
+1 −1		src/Data/Parameterized/Some.hs
+1 −1		test/Test/NatRepr.hs
+15 −4		.github/workflows/ci.yml
+0 −3		.gitmodules
+0 −268		cabal.GHC-8.8.4.config
+114 −113		cabal.GHC-9.2.8.config
+128 −128		cabal.GHC-9.4.5.config
+131 −132		cabal.GHC-9.6.2.config
+0 −1		cabal.project.newbuild
+1 −2		semmc-aarch32/semmc-aarch32.cabal
+5 −5		semmc-aarch32/src/SemMC/Architecture/ARM/ASL.hs
+5 −5		semmc-aarch32/src/SemMC/Architecture/ARM/UF.hs
+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
+4 −2		semmc-synthesis/src/SemMC/Synthesis/Cegis/LLVMMem.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
+6 −8		semmc/semmc.cabal
+2 −3		semmc/src/Data/Parameterized/TyMap.hs
+0 −1		semmc/src/Data/Type/List.hs
+11 −9		semmc/src/SemMC/Architecture.hs
+1 −0		semmc/src/SemMC/Architecture/AllocatedOperand.hs
+1 −0		semmc/src/SemMC/Architecture/Concrete.hs
+2 −1		semmc/src/SemMC/Architecture/Pseudo.hs
+1 −0		semmc/src/SemMC/Formula/Equivalence.hs
+1 −2		semmc/src/SemMC/Formula/Parser.hs
+8 −9		semmc/src/SemMC/Formula/Printer.hs
+2 −2		semmc/tests/semstore/ParamFormulaTests.hs
+1 −1		submodules/asl-translator
+1 −1		submodules/crucible
+1 −1		submodules/dismantle
+1 −1		submodules/elf-edit
+1 −1		submodules/llvm-pretty
+1 −1		submodules/what4
+0 −1		submodules/what4-serialize
+6 −3		.github/workflows/gen_matrix.pl
+29 −9		.github/workflows/test.yml
+5 −5		README.md
+1 −1		dependencies/aig
+2 −1		what4-abc/src/What4/Solver/ABC.hs
+1 −2		what4-abc/what4-abc.cabal
+1 −1		what4-blt/what4-blt.cabal
+44 −35		what4-transition-system/src/What4/TransitionSystem.hs
+2 −3		what4-transition-system/what4-transition-system.cabal
+48 −0		what4/CHANGES.md
+1 −1		what4/LICENSE
+7 −0		what4/README.md
+22 −0		what4/doc/arithdomain.cry
+1 −1		what4/doc/implementation.md
+2 −2		what4/src/What4/Config.hs
+2 −0		what4/src/What4/Expr/App.hs
+1 −1		what4/src/What4/Expr/AppTheory.hs
+67 −18		what4/src/What4/Expr/Builder.hs
+3 −2		what4/src/What4/Expr/Simplify.hs
+5 −5		what4/src/What4/Expr/VarIdentification.hs
+1 −1		what4/src/What4/Expr/WeightedSum.hs
+88 −6		what4/src/What4/Interface.hs
+1 −1		what4/src/What4/Partial.hs
+9 −3		what4/src/What4/ProblemFeatures.hs
+47 −0		what4/src/What4/Protocol/Online.hs
+6 −0		what4/src/What4/Protocol/SExp.hs
+456 −18		what4/src/What4/Protocol/SMTLib2.hs
+3 −2		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
+115 −5		what4/src/What4/Protocol/SMTWriter.hs
+1 −0		what4/src/What4/Protocol/VerilogWriter.hs
+3 −1		what4/src/What4/Protocol/VerilogWriter/AST.hs
+2 −1		what4/src/What4/Protocol/VerilogWriter/Backend.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,071 −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
+6 −0		what4/src/What4/Utils/BVDomain.hs
+55 −0		what4/src/What4/Utils/BVDomain/Arith.hs
+1 −0		what4/src/What4/Utils/OnlyIntRepr.hs
+127 −0		what4/src/What4/Utils/Serialize.hs
+0 −6		what4/src/What4/Utils/Versions.hs
+155 −0		what4/test/Abduct.hs
+1 −0		what4/test/AdapterTest.hs
+3 −0		what4/test/BVDomTests.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
+75 −13		what4/what4.cabal