Merge pull request #1625 from GaloisInc/heapster/array-borrow-check

Change Borrowed Array input permissions check

Author: mergify[bot]

heapster-saw/src/Verifier/SAW/Heapster/Implication.hs

@@ -1960,21 +1960,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

heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs

@@ -4795,7 +4795,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