From 6b4dadd47c70a5a3ed3d7261f23be884906e9419 Mon Sep 17 00:00:00 2001
From: Andrei Stefanescu <andrei@stefanescu.io>
Date: Wed, 22 Feb 2023 13:28:42 +0000
Subject: [PATCH] Load SMT array with concrete size.

---
 deps/crucible                           |  2 +-
 src/SAWScript/Crucible/LLVM/Override.hs | 24 ++++++++----------------
 2 files changed, 9 insertions(+), 17 deletions(-)

diff --git a/deps/crucible b/deps/crucible
index 6d3b277e10..e6c15f14bc 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit 6d3b277e101bba51a44ecd0c6bf576722df359ad
+Subproject commit e6c15f14bcec02de11f6f612f24ebb09c3b9f638
diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
index 8e72d45085..37b7d25c12 100644
--- a/src/SAWScript/Crucible/LLVM/Override.hs
+++ b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -1688,31 +1688,23 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val =
                             W4.bvLit sym Crucible.PtrWidth $ BV.mkBV Crucible.PtrWidth $ fromIntegral sz_nat
                           maybe_matching_array <- liftIO $
                             Crucible.asMemMatchingArrayStore sym Crucible.PtrWidth ptr sz_bv (Crucible.memImplHeap mem)
-                          case maybe_matching_array of
-                            Just (ok, arr) ->
+                          res <- case maybe_matching_array of
+                            Just (ok, arr) -> return $ Right (ok, arr)
+                            Nothing -> liftIO $ Crucible.loadArrayConcreteSizeRaw sym mem ptr sz_nat alignment
+
+                          case res of
+                            Right (ok, arr) ->
                               do addAssert ok md $ Crucible.SimError loc $ Crucible.GenericSimError $ show errMsg
                                  st <- liftIO (sawCoreState sym)
                                  arr_tm <- liftIO $ toSC sym st arr
                                  instantiateExtMatchTerm sc cc md prepost arr_tm $ ttTerm expected_arr_tm
                                  return Nothing
 
-                            Nothing
-                              | sz_nat == 0 ->
-                                do off_type_tm <- liftIO $ scBitvector sc $ natValue ?ptrWidth
-                                   byte_width_tm <- liftIO $ scNat sc 8
-                                   byte_type_tm <- liftIO $ scBitvector sc 8
-
-                                   zero_byte_tm <- liftIO $ scBvNat sc byte_width_tm =<< scNat sc 0
-                                   zero_arr_const_tm <- liftIO $ scArrayConstant sc off_type_tm byte_type_tm zero_byte_tm
-
-                                   instantiateExtMatchTerm sc cc md prepost zero_arr_const_tm $ ttTerm expected_arr_tm
-
-                                   return Nothing
-
-                              | otherwise -> return $ Just errMsg
+                            Left{} -> return $ Just errMsg
 
                      Nothing -> return $ Just errMsg
 
+
 -- | Like 'matchPointsToValue', but specifically geared towards the needs
 -- of fields within bitfields. In particular, this performs all of the
 -- necessary bit-twiddling on the LHS (a bitfield) to extract the necessary