wip

crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs

@@ -1638,10 +1638,10 @@ possibleAllocs n mem =
 newtype MemoIO m a = MemoIO (IORef (Either (m a) a))
 
 putMemoIO :: MonadIO m => m a -> m (MemoIO m a)
-putMemoIO comp = MemoIO <$> (liftIO $ newIORef $ Left comp)
+putMemoIO comp = MemoIO <$> liftIO (newIORef $ Left comp)
 
 getMemoIO :: MonadIO m => MemoIO m a -> m a
-getMemoIO (MemoIO ref) = (liftIO $ readIORef ref) >>= \case
+getMemoIO (MemoIO ref) = liftIO (readIORef ref) >>= \case
   Left comp -> do
     res <- comp
     liftIO $ writeIORef ref $ Right res
@@ -1673,6 +1673,7 @@ asMemAllocationArrayStore sym w ptr mem
   , [SomeAlloc _ _ (Just sz) _ _ _] <- List.nub (possibleAllocs blk_no mem)
   , Just Refl <- testEquality w (bvWidth sz) =
      do memo_nothing <- putMemoIO $ return Nothing
+        putStrLn $ "asMemAllocationArrayStore: base=" ++ show blk_no ++ " sz=" ++ show (printSymExpr sz)
         result <- findArrayStore sym w blk_no (BV.zero w) sz memo_nothing $
           memWritesAtConstant blk_no $ memWrites mem
         return $ case result of
@@ -1693,6 +1694,7 @@ asMemMatchingArrayStore sym w ptr sz mem
   | Just blk_no <- asNat (llvmPointerBlock ptr)
   , memMemberArrayBlock (llvmPointerBlock ptr) mem
   , Just off <- asBV (llvmPointerOffset ptr) = do
+    putStrLn $ "asMemMatchingArrayStore: ptr=" ++ show (blk_no, off) ++ " sz=" ++ show (printSymExpr sz)
     memo_nothing <- putMemoIO $ return Nothing
     findArrayStore sym w blk_no off sz memo_nothing $ memWritesAtConstant blk_no $ memWrites mem
   | otherwise = return Nothing
@@ -1709,7 +1711,11 @@ findArrayStore ::
   IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)))
 findArrayStore sym w blk_no off sz memo_cont = \case
   [] -> getMemoIO memo_cont
-  head_mem_write : tail_mem_writes -> case head_mem_write of
+  head_mem_write : tail_mem_writes -> do
+   putStrLn $ "  findArrayStore: ptr=" ++ show (blk_no, off) ++ " sz=" ++ show (printSymExpr sz)
+   putStrLn $ "  findArrayStore: write=" ++ (case head_mem_write of MemWrite{} -> "write"; WriteMerge{} -> "merge")
+
+   case head_mem_write of
     MemWrite write_ptr write_source
       | Just write_blk_no <- asNat (llvmPointerBlock write_ptr)
       , blk_no == write_blk_no