Update submodules

This commit adapts to recent changes in crucible and raises the version bounds
to admit newer versions of what4.

deps/crucible

@@ -1 +1 @@
-Subproject commit 31758d08848f447cb37f03ca14ca04d1e2c25162
+Subproject commit 78a22c4c49a98bb507fad2f4974513feb6c57523

deps/llvm-pretty-bc-parser

@@ -1 +1 @@
-Subproject commit 8d4e4c661e33dfd9b87e45eb6f19d8ed823934cc
+Subproject commit bea158b759d7315cdb4f4c4a364c9fd2c2f9b5a4

deps/macaw-loader

@@ -1 +1 @@
-Subproject commit 777fc7d102794cf898422e51377fc550905edd8f
+Subproject commit dae480507ff731b3e900c7e1e7a5e8c33de28729

deps/what4

@@ -1 +1 @@
-Subproject commit 713526b303306cda67a2bbce0c41a556a564286b
+Subproject commit ce5c0aa937286932f792fe33ad7692495cdd54a6

deps/what4-serialize

@@ -1 +1 @@
-Subproject commit c7e7da52089749cc7c114a6cf89f29a440976039
+Subproject commit 35f2877a3c04d17b133ac640a5e7035e507532a7

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.2
+                       what4 >= 1.1 && < 1.3
   hs-source-dirs:      src
   default-language:    Haskell2010
   ghc-options:         -Wall -Wcompat

refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs

@@ -63,7 +63,6 @@ import qualified What4.ProgramLoc as W
 import qualified What4.Protocol.Online as W
 import qualified What4.SatResult as W
 import qualified What4.BaseTypes as WT
-import qualified What4.LabeledPred as WLP
 
 import qualified Data.Macaw.Refinement.Logging as RL
 import qualified Data.Macaw.Refinement.Path as RP
@@ -203,7 +202,7 @@ smtSolveTransfer ctx slice
               exec_res <- liftIO $
                 C.executeCrucible executionFeatures initialState
 
-              assumptions <- F.toList . fmap (^. WLP.labeledPred) <$> liftIO (CB.collectAssumptions sym)
+              assumptions <- liftIO (CB.assumptionsPred sym =<< (CB.collectAssumptions sym))
 
               case exec_res of
                 C.FinishedResult _ res -> do
@@ -424,7 +423,7 @@ extractIPModels :: forall arch solver m sym t fp
                 => RefinementContext arch
                 -> sym
                 -> W.SolverProcess t solver
-                -> [W.Pred sym]
+                -> W.Pred sym
                 -> W.SymNat sym
                 -> WE.Expr t (WT.BaseBVType (M.ArchAddrWidth arch))
                 -> m (IPModels (MM.MemSegmentOff (M.ArchAddrWidth arch)))
@@ -443,7 +442,7 @@ extractIPModels ctx sym solverProc initialAssumptions res_ip_base res_ip_off = d
       basePred1 <- liftIO $ W.natEq sym natOne res_ip_base
       basePred <- liftIO $ W.orPred sym basePred0 basePred1
 
-      let assumptions = ipConstraint : basePred : initialAssumptions
+      let assumptions = [ipConstraint, basePred, initialAssumptions]
 
       genModels (Proxy @arch) sym solverProc assumptions res_ip_off modelMax
 

symbolic/macaw-symbolic.cabal

@@ -24,7 +24,7 @@ library
     text,
     vector,
     bytestring,
-    what4 >= 1.1 && < 1.2
+    what4 >= 1.1 && < 1.3
 
   hs-source-dirs: src
 

symbolic/src/Data/Macaw/Symbolic/Memory.hs

@@ -361,8 +361,7 @@ populateSegmentChunk _ sym mmc mem symArray seg addr bytes ptrtable = do
         eq_pred <- liftIO $ WI.bvEq sym byte =<< WI.arrayLookup sym symArray (Ctx.singleton index_bv)
         prog_loc <- liftIO $ WI.getCurrentProgramLoc sym
         let desc = "Byte@" ++ show byteAddr
-        liftIO $ CB.addAssumption sym $
-          CB.LabeledPred eq_pred $ CB.AssumptionReason prog_loc desc
+        liftIO $ CB.addAssumption sym (CB.GenericAssumption prog_loc desc eq_pred)
       let symArray2 = symArray
 
       return (symArray2, IM.insert interval mut_flag ptrtable)