Load SMT array with concrete size.

GaloisInc · Feb 22, 2023 · 6b4dadd · 6b4dadd
1 parent 5452f6d
commit 6b4dadd
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 17 deletions.
diff --git a/deps/crucible b/deps/crucible
diff --git 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