Merge pull request #2226 from GaloisInc/T2223-bump-submodules-BoolMap

Bump `what4` submodule (and friends) to bring in GaloisInc/what4#277 changes
GaloisInc · Feb 17, 2025 · 692d8fb · 692d8fb
2 parents bce996a + a6c47f2
commit 692d8fb
Show file tree

Hide file tree

Showing 7 changed files with 19 additions and 12 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -52,3 +52,6 @@
 [submodule "deps/mir-json"]
 	path = deps/mir-json
 	url = https://github.com/GaloisInc/mir-json.git
+[submodule "deps/macaw-loader"]
+	path = deps/macaw-loader
+	url = https://github.com/GaloisInc/macaw-loader.git
diff --git a/cabal.project b/cabal.project
@@ -36,9 +36,12 @@ packages:
     deps/lmdb/lmdb
     deps/lmdb/lmdb-simple
     deps/macaw/base
+    deps/macaw/macaw-dump
     deps/macaw/symbolic
     deps/macaw/x86
     deps/macaw/x86_symbolic
+    deps/macaw-loader/macaw-loader
+    deps/macaw-loader/macaw-loader-x86
     deps/elf-edit
     deps/dwarf
     deps/argo/argo

diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/macaw b/deps/macaw
diff --git a/deps/macaw-loader b/deps/macaw-loader
diff --git a/deps/what4 b/deps/what4
diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs
@@ -112,7 +112,7 @@ data SAWExpr (bt :: BaseType) where
 getInputs :: SAWCoreState n -> IO (Seq (SC.ExtCns SC.Term))
 getInputs st = readIORef (saw_inputs st)
 
-baseSCType :: 
+baseSCType ::
   sym ->
   SC.SharedContext ->
   BaseTypeRepr tp ->
@@ -600,10 +600,10 @@ evaluateExpr sym st sc cache = f []
           goNeg env x
 
         B.ConjPred xs ->
-          case BM.viewBoolMap xs of
-            BM.BoolMapUnit -> SAWExpr <$> SC.scBool sc True
-            BM.BoolMapDualUnit -> SAWExpr <$> SC.scBool sc False
-            BM.BoolMapTerms (t:|ts) ->
+          case BM.viewConjMap xs of
+            BM.ConjTrue -> SAWExpr <$> SC.scBool sc True
+            BM.ConjFalse -> SAWExpr <$> SC.scBool sc False
+            BM.Conjuncts (t:|ts) ->
               let pol (x,BM.Positive) = f env x
                   pol (x,BM.Negative) = termOfSAWExpr sym sc =<< goNeg env x
               in SAWExpr <$> join (foldM (SC.scAnd sc) <$> pol t <*> mapM pol ts)
@@ -940,10 +940,10 @@ evaluateExpr sym st sc cache = f []
       case expr of
         -- negation of (x /\ y) becomes (~x \/ ~y)
         B.AppExpr (B.appExprApp -> B.ConjPred xs) ->
-          case BM.viewBoolMap xs of
-            BM.BoolMapUnit -> SAWExpr <$> SC.scBool sc False
-            BM.BoolMapDualUnit -> SAWExpr <$> SC.scBool sc True
-            BM.BoolMapTerms (t:|ts) ->
+          case BM.viewConjMap xs of
+            BM.ConjTrue -> SAWExpr <$> SC.scBool sc False
+            BM.ConjFalse -> SAWExpr <$> SC.scBool sc True
+            BM.Conjuncts (t:|ts) ->
               let pol (x, BM.Positive) = termOfSAWExpr sym sc =<< goNegAtom env x
                   pol (x, BM.Negative) = f env x
               in SAWExpr <$> join (foldM (SC.scOr sc) <$> pol t <*> mapM pol ts)
+2 −2		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs
+1 −1		dependencies/what4
+7 −0		what4/CHANGES.md
+26 −23		what4/src/What4/Expr/App.hs
+108 −14		what4/src/What4/Expr/BoolMap.hs
+34 −18		what4/src/What4/Expr/Builder.hs
+1 −10		what4/src/What4/Expr/GroundEval.hs
+5 −5		what4/src/What4/Expr/VarIdentification.hs
+5 −5		what4/src/What4/Protocol/SMTWriter.hs
+1 −1		what4/src/What4/Protocol/VerilogWriter/Backend.hs
+1 −1		what4/src/What4/Serialize/Printer.hs
+295 −0		what4/test/Bool.hs
+62 −0		what4/test/BoolNormalization.hs
+3 −0		what4/test/ExprsTest.hs
+4 −1		what4/test/OnlineSolverTest.hs
+11 −0		what4/what4.cabal