changed the permIndicesForProvingOffset case that allows imprecise ma…

…tches on the left to check not only for a syntactic array permission, but also for a block permission containing an array shape (#1536)
GaloisInc · Dec 7, 2021 · 18a0cea · 18a0cea
1 parent 96272c0
commit 18a0cea
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 1 deletion.
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -4770,7 +4770,7 @@ permIndicesForProvingOffset ps imprecise_p off =
   let ixs_holdss = flip findMaybeIndices ps $ \p ->
         case llvmPermContainsOffset off p of
           Just (_, True) -> Just True
-          Just _ | isLLVMArrayPerm p && imprecise_p -> Just False
+          Just _ | llvmPermContainsArray p && imprecise_p -> Just False
           _ -> Nothing in
   case find (\(_,holds) -> holds) ixs_holdss of
     Just (i,_) -> [i]

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -3733,6 +3733,19 @@ llvmAtomicPermEndOffset p =
 llvmAtomicPermRange :: AtomicPerm (LLVMPointerType w) -> Maybe (BVRange w)
 llvmAtomicPermRange p = fmap llvmBlockRange $ llvmAtomicPermToBlock p
 
+-- | Test if an LLVM atomic permission contains some range of offsets that have
+-- an array shape
+llvmPermContainsArray :: AtomicPerm (LLVMPointerType w) -> Bool
+llvmPermContainsArray (Perm_LLVMArray _) = True
+llvmPermContainsArray (Perm_LLVMBlock bp) =
+  shapeContainsArray $ llvmBlockShape bp where
+  shapeContainsArray :: PermExpr (LLVMShapeType w) -> Bool
+  shapeContainsArray (PExpr_ArrayShape _ _ _) = True
+  shapeContainsArray (PExpr_SeqShape sh1 sh2) =
+    shapeContainsArray sh1 || shapeContainsArray sh2
+  shapeContainsArray _ = False
+llvmPermContainsArray _ = False
+
 -- | Set the range of an 'LLVMBlock'
 llvmBlockSetRange :: LLVMBlockPerm w -> BVRange w -> LLVMBlockPerm w
 llvmBlockSetRange bp (BVRange off len) =