Heapster array permission bug fixes

heapster-saw/examples/arrays.c

@@ -122,3 +122,15 @@ uint64_t even_odd_sums_diff(const uint64_t *arr, size_t len) {
   }
   return sum;
 }
+
+uint64_t alloc_sum_array_test (void) {
+  uint64_t X[8];
+  X[0] = 0; X[1] = 1; X[2] = 2; X[3] = 3;
+  X[4] = 4; X[5] = 5; X[6] = 6; X[7] = 7;
+  /*
+  for (uint64_t i = 0; i < 16; ++i) {
+    X[i] = i;
+  }
+  */
+  return sum_inc_ptr_64 (X, 8);
+}

heapster-saw/examples/arrays.saw

@@ -62,4 +62,6 @@ heapster_typecheck_fun env "even_odd_sums_diff"
   "(l:bv 64). arg0:array(W,0,<2*l,*8,fieldsh(int64<>)), arg1:eq(llvmword(2*l)) -o \
             \ arg0:array(W,0,<2*l,*8,fieldsh(int64<>)), arg1:true, ret:int64<>";
 
+heapster_typecheck_fun env "alloc_sum_array_test" "(). empty -o ret:int64<>";
+
 heapster_export_coq env "arrays_gen.v";

heapster-saw/examples/rust_data.rs

@@ -179,7 +179,7 @@ pub fn extract_from_result_infallible <'a> (r:&'a Result<Infallible,u64>) -> u64
 /* Sum of two types; yes, this is like Result, but defined locally so we can
  * make an impl block on it */
 #[derive(Clone, Debug, PartialEq)]
-#[repr(C)]
+#[repr(C,u64)]
 pub enum Sum<X,Y> {
     Left (X),
     Right (Y)

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

@@ -2659,6 +2659,11 @@ mbLLVMArrayLen = mbMapCl $(mkClosed [| llvmArrayLen |])
 mbLLVMArrayLenBytes :: (1 <= w, KnownNat w) => Mb ctx (LLVMArrayPerm w) -> Mb ctx (PermExpr (BVType w))
 mbLLVMArrayLenBytes = mbMapCl $(mkClosed [| llvmArrayLengthBytes |])
 
+-- | Get the range of offsets of an array permission in binding
+mbLLVMArrayRange :: (1 <= w, KnownNat w) => Mb ctx (LLVMArrayPerm w) ->
+                    Mb ctx (BVRange w)
+mbLLVMArrayRange = mbMapCl $(mkClosed [| llvmArrayRange |])
+
 -- | Get the stride of an array permission in binding
 mbLLVMArrayStride :: Mb ctx (LLVMArrayPerm w) -> Bytes
 mbLLVMArrayStride = mbLift . mbMapCl $(mkClosed [| llvmArrayStride |])
@@ -4957,6 +4962,15 @@ llvmArrayCellsToOffsets :: (1 <= w, KnownNat w) => LLVMArrayPerm w ->
 llvmArrayCellsToOffsets ap (BVRange cell num_cells) =
   BVRange (llvmArrayCellToOffset ap cell) (llvmArrayCellToOffset ap num_cells)
 
+-- | Convert a range of absolute byte offsets to a range of cell numbers in an
+-- array permission, if possible
+llvmArrayAbsOffsetsToCells :: (1 <= w, KnownNat w) => LLVMArrayPerm w ->
+                              BVRange w -> Maybe (BVRange w)
+llvmArrayAbsOffsetsToCells ap rng
+  | Just cell <- matchLLVMArrayCell ap (bvRangeOffset rng) =
+    Just $ BVRange cell (bvDiv (bvRangeLength rng) (llvmArrayStride ap))
+llvmArrayAbsOffsetsToCells _ _ = Nothing
+
 -- | Return the clopen range @[0,len)@ of the cells of an array permission
 llvmArrayCells :: (1 <= w, KnownNat w) => LLVMArrayPerm w -> BVRange w
 llvmArrayCells ap = BVRange (bvInt 0) (llvmArrayLen ap)
@@ -5031,18 +5045,27 @@ permToLLVMArrayBorrow ap p =
 
     _ -> Nothing
 
+-- | Get the range of offsets spanned by a borrow relative to the start of an
+-- array permission
 llvmArrayBorrowRange :: (1 <= w, KnownNat w) =>
                         LLVMArrayPerm w -> LLVMArrayBorrow w -> BVRange w
 llvmArrayBorrowRange ap borrow =
   llvmArrayCellsToOffsets ap (llvmArrayBorrowCells borrow)
 
+-- | Get the "absolute" range of offsets spanned by a borrow relative to the
+-- pointer with this array permission
 llvmArrayAbsBorrowRange :: (1 <= w, KnownNat w) =>
-                        LLVMArrayPerm w -> LLVMArrayBorrow w -> BVRange w
+                           LLVMArrayPerm w -> LLVMArrayBorrow w -> BVRange w
 llvmArrayAbsBorrowRange ap borrow =
   range { bvRangeOffset = bvAdd (llvmArrayOffset ap) (bvRangeOffset range) }
   where
     range = llvmArrayCellsToOffsets ap (llvmArrayBorrowCells borrow)
 
+-- | Get the absolute offset at which an array borrow starts
+llvmArrayBorrowAbsOffset :: (1 <= w, KnownNat w) => LLVMArrayPerm w ->
+                            LLVMArrayBorrow w -> PermExpr (BVType w)
+llvmArrayBorrowAbsOffset ap b = bvRangeOffset $ llvmArrayAbsBorrowRange ap b
+
 -- | Add a borrow to an 'LLVMArrayPerm'
 llvmArrayAddBorrow :: LLVMArrayBorrow w -> LLVMArrayPerm w -> LLVMArrayPerm w
 llvmArrayAddBorrow b ap = ap { llvmArrayBorrows = b : llvmArrayBorrows ap }
@@ -5106,7 +5129,7 @@ llvmArrayBorrowsPermuteTo ap bs =
 -- | Add a cell offset to an 'LLVMArrayBorrow', meaning we change the borrow to
 -- be relative to an array with that many more cells added to the front
 cellOffsetLLVMArrayBorrow :: (1 <= w, KnownNat w) => PermExpr (BVType w) ->
-                              LLVMArrayBorrow w -> LLVMArrayBorrow w
+                             LLVMArrayBorrow w -> LLVMArrayBorrow w
 cellOffsetLLVMArrayBorrow off (FieldBorrow ix) =
   FieldBorrow (bvAdd ix off)
 cellOffsetLLVMArrayBorrow off (RangeBorrow rng) =
@@ -5119,6 +5142,8 @@ llvmArrayBorrowCells :: (KnownNat w, 1 <= w) => LLVMArrayBorrow w -> BVRange w
 llvmArrayBorrowCells (FieldBorrow idx) = bvRangeOfIndex idx
 llvmArrayBorrowCells (RangeBorrow r) = r
 
+-- FIXME: delete? not used, and should be implementable via bvRangeDelete
+{-
 -- | Given a borrow @borrow@ and range (of borrowed indices) @rng@,
 -- delete @rng@ from @borrow@, and return the borrows that describe
 -- the remaining borrowed cells.
@@ -5139,27 +5164,42 @@ llvmArrayBorrowRangeDelete borrow rng =
       , bvEq (bvRangeLength new_range) (bvInt 1) = Just $ FieldBorrow idx
       | 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
+-- | Take in a range @rng@ and a list of ranges @rngs@ and try to find a
+-- sequence of non-overlapping but contiguous ranges in @rngs@ that covers the
+-- desired range @rng@
+gatherCoveringRanges :: (1 <= w, KnownNat w) => BVRange w -> [BVRange w] ->
+                        Maybe [BVRange w]
+gatherCoveringRanges rng _ | bvIsZero (bvRangeLength rng) = Just []
+gatherCoveringRanges rng rngs
+  | Just i <- findIndex (bvInRange (bvRangeOffset rng)) rngs
+  , rng' <- rngs!!i =
+    -- If rng' covers all of rng, then we are done
+    if bvRangeSubset rng rng' then Just [rng'] else
+      (rng' :) <$>
+      gatherCoveringRanges (bvRangeSuffix (bvRangeEnd rng') rng)
+                           (deleteNth i rngs)
+gatherCoveringRanges _ _ = Nothing
+
+-- | Test if the borrows in @ap@ cover a given range of offsets. That is, test
+-- if the ranges of the borrows in @ap@ can be arranged as a sequence of
+-- non-overlapping but contiguous ranges that extends at least as far as @len@
+-- (in the sense of @bvLeq@).
+llvmArrayRangeIsBorrowed :: (HasCallStack, 1 <= w, KnownNat w) =>
+                            LLVMArrayPerm w -> BVRange w -> Bool
+llvmArrayRangeIsBorrowed ap rng =
+  isJust $ gatherCoveringRanges rng $
+  map (llvmArrayBorrowAbsOffsets ap) (llvmArrayBorrows ap)
+
+-- | Test whether the borrows in @ap@ cover the range of cells @[0, len)@. That
+-- is, test if the ranges of the borrows in @ap@ can be arranged as a sequence
+-- of non-overlapping but contiguous ranges 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)
-    go _ _ = False
-
-    permForOff o b = bvCouldEqual o (bvRangeOffset b)
+  llvmArrayRangeIsBorrowed ap (llvmArrayAbsOffsets ap)
 
 -- | Test if a byte offset @o@ statically aligns with a statically-known offset
 -- into some array cell, i.e., whether
@@ -5328,6 +5368,7 @@ llvmMakeSubArray ap off len
   , cell_rng <- BVRange cell len =
     ap { llvmArrayOffset = off, llvmArrayLen = len,
          llvmArrayBorrows =
+           map (cellOffsetLLVMArrayBorrow (bvNegate cell)) $
            filter (not . all bvPropHolds .
                    llvmArrayBorrowsDisjoint (RangeBorrow cell_rng)) $
            llvmArrayBorrows ap }
@@ -5367,23 +5408,42 @@ llvmPermContainsOffsetBool :: (1 <= w, KnownNat w) => PermExpr (BVType w) ->
 llvmPermContainsOffsetBool off p =
   maybe False snd $ llvmPermContainsOffset off p
 
--- | Test if an atomic LLVM permission contains (in the sense of 'bvPropHolds')
--- all offsets in a given range
-llvmAtomicPermContainsRange :: (1 <= w, KnownNat w) => BVRange w ->
-                               AtomicPerm (LLVMPointerType w) -> Bool
-llvmAtomicPermContainsRange rng (Perm_LLVMArray ap)
+-- | Build the propositions stating that an atomic LLVM permission contains all
+-- offsets in a given range
+llvmAtomicPermContainsRangeProps :: (1 <= w, KnownNat w) => BVRange w ->
+                                    AtomicPerm (LLVMPointerType w) ->
+                                    Maybe [BVProp w]
+llvmAtomicPermContainsRangeProps rng (Perm_LLVMArray ap)
   | Just ix1 <- matchLLVMArrayIndex ap (bvRangeOffset rng)
   , Just ix2 <- matchLLVMArrayIndex ap (bvRangeEnd rng)
   , props <- llvmArrayBorrowInArray ap (RangeBorrow $ BVRange
                                         (llvmArrayIndexCell ix1)
                                         (llvmArrayIndexCell ix2)) =
+    Just props
+llvmAtomicPermContainsRangeProps rng (Perm_LLVMField fp) =
+  Just $ bvPropRangeSubset rng (llvmFieldRange fp)
+llvmAtomicPermContainsRangeProps rng (Perm_LLVMBlock bp) =
+  Just $ bvPropRangeSubset rng (llvmBlockRange bp)
+llvmAtomicPermContainsRangeProps _ _ = Nothing
+
+-- | Test if an atomic LLVM permission contains (in the sense of 'bvPropHolds')
+-- all offsets in a given range
+llvmAtomicPermContainsRange :: (1 <= w, KnownNat w) => BVRange w ->
+                               AtomicPerm (LLVMPointerType w) -> Bool
+llvmAtomicPermContainsRange rng p
+  | Just props <- llvmAtomicPermContainsRangeProps rng p =
     all bvPropHolds props
-llvmAtomicPermContainsRange rng (Perm_LLVMField fp) =
-  bvRangeSubset rng (llvmFieldRange fp)
-llvmAtomicPermContainsRange rng (Perm_LLVMBlock bp) =
-  bvRangeSubset rng (llvmBlockRange bp)
 llvmAtomicPermContainsRange _ _ = False
 
+-- | Test if an atomic LLVM permission could contain (in the sense of
+-- 'bvPropCouldHold') all offsets in a given range
+llvmAtomicPermCouldContainRange :: (1 <= w, KnownNat w) => BVRange w ->
+                                   AtomicPerm (LLVMPointerType w) -> Bool
+llvmAtomicPermCouldContainRange rng p
+  | Just props <- llvmAtomicPermContainsRangeProps rng p =
+    all bvPropCouldHold props
+llvmAtomicPermCouldContainRange _ _ = False
+
 -- | Test if an atomic LLVM permission has a range that overlaps with (in the
 -- sense of 'bvPropHolds') the offsets in a given range
 llvmAtomicPermOverlapsRange :: (1 <= w, KnownNat w) => BVRange w ->
@@ -5437,7 +5497,7 @@ llvmArrayToBlocks _ = Nothing
 llvmArrayBorrowOffsets :: (1 <= w, KnownNat w) => LLVMArrayPerm w ->
                           LLVMArrayBorrow w -> BVRange w
 llvmArrayBorrowOffsets ap (FieldBorrow ix) =
-  bvRangeOfIndex $ llvmArrayCellToOffset ap ix
+  BVRange (llvmArrayCellToOffset ap ix) (bvInt $ toInteger $ llvmArrayStride ap)
 llvmArrayBorrowOffsets ap (RangeBorrow r) = llvmArrayCellsToOffsets ap r
 
 -- | Get the range of byte offsets represented by an array borrow relative to