From ebe691348bff540936dbb973215b370f0845dab1 Mon Sep 17 00:00:00 2001
From: Alexander Bakst <abakst@galois.com>
Date: Tue, 5 Apr 2022 16:41:57 -0700
Subject: [PATCH] Check an array is totally borrowed by walking the borrowed
 cell ranges.

---
 .../src/Verifier/SAW/Heapster/Implication.hs   | 13 +------------
 .../src/Verifier/SAW/Heapster/Permissions.hs   | 18 ++++++++++++++++++
 2 files changed, 19 insertions(+), 12 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index 0dd85d5fbd..f957a992cd 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -1961,21 +1961,10 @@ simplImplIn (SImpl_LLVMArrayEmpty _ ap) =
 simplImplIn (SImpl_LLVMArrayBorrowed x bp ap) =
   if bvIsZero (llvmArrayLen ap) then
     error "simplImplIn: SImpl_LLVMArrayBorrowed: empty array permission"
-  else if not totallyBorrowed then
+  else if not (llvmArrayIsBorrowed ap) then
     error "simplImplIn: SImpl_LLVMArrayBorrowed: array permission not completely borrowed"
   else
     distPerms1 x (ValPerm_Conj1 $ Perm_LLVMBlock bp)
-  where
-    -- If all the subtractions below could be empty, then we've subtracted the
-    -- whole array
-    totallyBorrowed = all (bvCouldEqual (bvInt 0)) (bvRangeLength <$> remaining)
-
-    remaining =
-      -- iteratively subtract each borrow from the total range of array indices
-      foldr (\b xs -> xs >>= (`bvRangeDelete` llvmArrayBorrowCells b))
-            [llvmArrayCells ap]
-            (llvmArrayBorrows ap)
-
 
 simplImplIn (SImpl_LLVMArrayFromBlock x bp) =
   distPerms1 x $ ValPerm_LLVMBlock bp
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index 27224a5868..75e55ce5ef 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -4738,7 +4738,25 @@ llvmArrayBorrowRangeDelete borrow rng =
       | otherwise =
         error "llvmArrayBorrowRangeDelete: found non unit new_range for FieldBorrow"
 
+-- | Return whether or not the borrows in @ap@ cover the range of cells [0, len). Specifically,
+-- if the borrowed cells (as ranges) can be arranged in as a sequence of non-overlapping but contiguous
+-- ranges (in the sense of @bvCouldEqual@) that extends at least as far as @len@ (in the sense of @bvLeq@)
+llvmArrayIsBorrowed ::
+  (HasCallStack, 1 <= w, KnownNat w) =>
+  LLVMArrayPerm w ->
+  Bool
+llvmArrayIsBorrowed ap =
+  go (bvInt 0) (llvmArrayBorrowCells <$> llvmArrayBorrows ap)
+  where
+    end = bvRangeEnd (llvmArrayCells ap)
+
+    go off borrows
+      | bvLeq end off
+      = True
+      | Just i <- findIndex (permForOff off) borrows
+      = go (bvAdd off (bvRangeLength (borrows!!i))) (deleteNth i borrows)
 
+    permForOff o b = bvCouldEqual o (bvRangeOffset b)
 
 -- | Test if a byte offset @o@ statically aligns with a statically-known offset
 -- into some array cell, i.e., whether