Skip to content

Commit

Permalink
Heapster Array Prover Redux (#1617)
Browse files Browse the repository at this point in the history 
* WIP checkin, basic cases of array prover rewrite working.

* Add unit tests for implication prover

* WIP checkin - array implication prover

* Fix bug in skeletonArray range gathering

* Reorg test main

* Add some symbolic tests

* Add some tests over fields

* goo begone

* Some clean up of array reimplementation

* clean up array prover impl

* more testing

* Revert changed examples

* Add comment to last successful case of proveVarLLVMArrayH

* Revert _CoqProject changes

* Revert arrays.saw changes

* WIP checkin, bug fix

* Finish cleanup

* Refactor proveSomeBlockM

* Refactor gatherRangesForArray

* Better docs on SImpl_LLVMArrayBorrowed.

* Fix errors in refactor

* Eliminate array-shaped blocks in `proveVarLLVMArrayH`.

* Check totally-borrowed side condition of SImpl_LLVMArrayBorrowed in `simplImplIn`.

* Make llvmAtomicPermCouldOverlapRange docs more precise

* Missing haddocks

* Remove commented-out code

* Remove unused function.

* Don't throw away rhs borrows.

* Don't depend on ordering when checking an array is completely borrowed

Co-authored-by: Eddy Westbrook <westbrook@galois.com>
  • Loading branch information
@abakst
abakst and Eddy Westbrook authored Mar 28, 2022
1 parent 4ecdc83 commit 5d36808
Show file tree
Hide file tree
Showing 5 changed files with 675 additions and 164 deletions.
22 changes: 22 additions & 0 deletions heapster-saw/heapster-saw.cabal
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,3 +65,25 @@ library
Verifier.SAW.Heapster.Widening
GHC-options: -Wall
default-language: Haskell2010

test-suite prover_tests
type: exitcode-stdio-1.0
hs-source-dirs: proverTests

ghc-options: -Wall -threaded
default-language: Haskell2010

main-is: Main.hs

build-depends: base
, directory
, filemanip
, filepath
, process
, tasty
, tasty-hunit
, tasty-expected-failure
, heapster-saw
, hobbits ^>= 1.4
, crucible
, crucible-llvm
239 changes: 239 additions & 0 deletions heapster-saw/proverTests/Main.hs
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,239 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE IncoherentInstances #-}
{-# OPTIONS_GHC -Wno-type-defaults #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Main where

import Data.Binding.Hobbits
import Data.Binding.Hobbits.NameMap(singleton)
import Test.Tasty
import Verifier.SAW.Heapster.Permissions
import Lang.Crucible.LLVM.Bytes
import Lang.Crucible.LLVM.MemModel (LLVMPointerType)
import Verifier.SAW.Heapster.Implication (proveVarImpl, checkVarImpl)
import Test.Tasty.HUnit
import Lang.Crucible.Types (BVType)
import GHC.TypeLits

infix 5 ===>
infixl 8 \\
infixl 8 \\\
infixl 8 \\\\

(===>) :: (ToConj p1, ToConj p2) => p1 -> p2 -> Bool
xs ===> ys = conj xs `checkImpl` conj ys

(\\) :: LLVMArrayPerm w -> [LLVMArrayBorrow w] -> LLVMArrayPerm w
(\\) a bs = a { llvmArrayBorrows = llvmArrayBorrows a ++ bs }

(\\\) :: (ArrayIndexExpr a1, ArrayIndexExpr a2) => LLVMArrayPerm 64 -> (a1, a2) -> LLVMArrayPerm 64
(\\\) a (i, l) = a \\ [RangeBorrow (BVRange (toIdx i) (toIdx l))]

(\\\\) :: (ArrayIndexExpr a) => LLVMArrayPerm 64 -> a -> LLVMArrayPerm 64
(\\\\) a i = a \\ [FieldBorrow (toIdx i)]

class t ~ LLVMPointerType 64 => ToAtomic a t | a -> t where
atomic :: a -> AtomicPerm t

instance t ~ LLVMPointerType 64 => ToAtomic (AtomicPerm t) t where
atomic = id

instance t ~ LLVMPointerType 64 => ToAtomic (LLVMArrayPerm 64) t where
atomic = Perm_LLVMArray

class ToConj a where
conj :: a -> ValuePerm (LLVMPointerType 64)

instance (ToAtomic p t, t ~ LLVMPointerType 64) => ToConj p where
conj x = ValPerm_Conj1 (atomic x)

instance (ToAtomic p t, t ~ LLVMPointerType 64) => ToConj [p] where
conj = ValPerm_Conj . fmap atomic

instance (t ~ LLVMPointerType 64) => ToConj [AtomicPerm t] where
conj = ValPerm_Conj

class ArrayIndexExpr a where
toIdx :: a -> PermExpr (BVType 64)

instance ArrayIndexExpr (PermExpr (BVType 64)) where
toIdx = id

instance Integral i => ArrayIndexExpr i where
toIdx i = bvInt (toInteger i)

instance t ~ BVType 64 => ArrayIndexExpr (Name t) where
toIdx x = PExpr_Var x

passes :: Bool -> Assertion
passes = assertBool "should succeed"

fails :: Bool -> Assertion
fails = assertBool "should fail" . not

withName :: (Name (BVType 64) -> Bool) -> Bool
withName k = mbLift (nu k)

checkImpl :: ValuePerm (LLVMPointerType 64) -> ValuePerm (LLVMPointerType 64) -> Bool
checkImpl lhs rhs = mbLift (nu $ \x -> checkVarImpl (pset x) (proveVarImpl x perm_rhs))
where
perm_lhs = lhs
perm_rhs = emptyMb rhs
pset x = PermSet { _varPermMap = singleton x perm_lhs, _distPerms = DistPermsNil }

memblockPerm :: (ArrayIndexExpr a1, ArrayIndexExpr a2) =>
a1 -> a2 -> PermExpr (LLVMShapeType 64) -> LLVMBlockPerm 64
memblockPerm off len shape = LLVMBlockPerm
{ llvmBlockRW = PExpr_Write
, llvmBlockLifetime = PExpr_Always
, llvmBlockOffset = toIdx off
, llvmBlockLen = toIdx len
, llvmBlockShape = shape
}

intValuePerm :: (KnownNat sz, 1 <= sz) => ValuePerm (LLVMPointerType sz)
intValuePerm = ValPerm_Exists $ nu $ \x -> ValPerm_Eq (PExpr_LLVMWord (PExpr_Var x))

fieldShape :: (KnownNat sz, 1 <= sz) => ValuePerm (LLVMPointerType sz) -> PermExpr (LLVMShapeType 64)
fieldShape p = PExpr_FieldShape (LLVMFieldShape p)

fieldPerm :: ArrayIndexExpr a => a -> ValuePerm (LLVMPointerType w) -> LLVMFieldPerm 64 w
fieldPerm off contents = LLVMFieldPerm
{ llvmFieldRW = PExpr_Write
, llvmFieldLifetime = PExpr_Always
, llvmFieldOffset = toIdx off
, llvmFieldContents = contents
}

field :: (KnownNat sz, 1 <= sz, ArrayIndexExpr a) =>
a -> ValuePerm (LLVMPointerType sz) -> AtomicPerm (LLVMPointerType 64)
field off contents = Perm_LLVMField (fieldPerm off contents)

memblock_int64field :: (ArrayIndexExpr a) => a -> AtomicPerm (LLVMPointerType 64)
memblock_int64field off = Perm_LLVMBlock $ memblockPerm off 8 (fieldShape (intValuePerm @64))

memblock_int64array :: (ArrayIndexExpr a1, ArrayIndexExpr a2) => a1 -> a2 -> AtomicPerm (LLVMPointerType 64)
memblock_int64array off len = Perm_LLVMBlock $ memblockPerm off (bvMult 8 (toIdx len)) (arrayShape len 8 (fieldShape (intValuePerm @64)))

int64field :: ArrayIndexExpr a => a -> AtomicPerm (LLVMPointerType 64)
int64field off = field off (intValuePerm :: ValuePerm (LLVMPointerType 64))

int64array :: (ArrayIndexExpr a1, ArrayIndexExpr a2) => a1 -> a2 -> AtomicPerm (LLVMPointerType 64)
int64array off len = Perm_LLVMArray (int64ArrayPerm off len)

int32array :: (ArrayIndexExpr a1, ArrayIndexExpr a2) => a1 -> a2 -> AtomicPerm (LLVMPointerType 64)
int32array off len = Perm_LLVMArray (int32ArrayPerm off len)

int64ArrayPerm :: (ArrayIndexExpr a1, ArrayIndexExpr a2) => a1 -> a2 -> LLVMArrayPerm 64
int64ArrayPerm off len = arrayPerm (toIdx off) (toIdx len) 8 (fieldShape (intValuePerm @ 64))

int32ArrayPerm :: (ArrayIndexExpr a1, ArrayIndexExpr a2) => a1 -> a2 -> LLVMArrayPerm 64
int32ArrayPerm off len = arrayPerm (toIdx off) (toIdx len) 4 (fieldShape (intValuePerm @ 32))

arrayPerm ::
PermExpr (BVType w) ->
PermExpr (BVType w) ->
Bytes ->
PermExpr (LLVMShapeType w) ->
LLVMArrayPerm w
arrayPerm off len stride shape = LLVMArrayPerm
{ llvmArrayRW = PExpr_Write
, llvmArrayLifetime = PExpr_Always
, llvmArrayOffset = off
, llvmArrayLen = len
, llvmArrayStride = stride
, llvmArrayCellShape = shape
, llvmArrayBorrows = []
}

arrayShape :: (ArrayIndexExpr a) => a -> Bytes -> PermExpr (LLVMShapeType 64) -> PermExpr (LLVMShapeType 64)
arrayShape len = PExpr_ArrayShape (toIdx len)

arrayTests :: TestTree
arrayTests =
testGroup "arrayTests"
[ testCase "too small" $ fails $ int64array 0 3 ===> int64array 0 6
, testCase "bigger" $ passes $ int64array 0 6 ===> int64array 0 3

, testGroup "sum of two arrays"
[ testCase "exact" $ passes $ [ int64array 0 3, int64array 24 3 ] ===> int64array 0 6
, testCase "larger" $ passes $ [ int64array 0 3, int64array 24 3 ] ===> int64array 0 5
, testCase "not enough" $ fails $ [ int64array 0 3, int64array 24 3 ] ===> int64array 0 7
]

, testGroup "sum of fields"
[ testCase "some fields" $ passes $
[ int64field 0, int64field 8, int64field 16 ] ===> int64array 0 3
, testCase "some extra fields" $ passes $
[ int64field 0, int64field 8, int64field 16 ] ===> int64array 8 2
, testCase "insufficient fields (1)" $ fails $
[ int64field 0, int64field 8, int64field 16 ] ===> int64array 8 3
, testCase "insufficient fields (2)" $ fails $
[ int64field 0, int64field 8, int64field 16 ] ===> int64array 0 4
]

, testGroup "mix of permission types"
[ testCase "memblocks 1:1" $ passes $
memblock_int64field 0 ===> int64array 0 1
, testCase "memblocks insufficient" $ fails $
[ memblock_int64field 0, memblock_int64field 8 ] ===> int64array 0 3
, testCase "memblocks array 1:1" $ passes $
memblock_int64array 0 3 ===> int64array 0 3
, testCase "memblocks array 2:1" $ passes $
[ memblock_int64array 8 3, memblock_int64array 32 4 ] ===> int64array 8 7
]

, testGroup "symbolic"
[ testCase "borrowed concrete field" $ fails $
withName $ \l ->
int64ArrayPerm 0 l \\\\ 0 ===> int64array 0 l
, testCase "borrowed concrete field" $ passes $
withName $ \l ->
[atomic (int64ArrayPerm 0 l \\\\ 0), int64field 0] ===> int64array 0 l
, testCase "borrowed symbolic field" $ passes $
withName $ \l -> withName $ \i ->
[atomic (int64ArrayPerm 0 l \\\\ i), int64field (bvMult 8 (toIdx i))] ===> int64array 0 l
, testCase "symbolic length append" $ passes $
withName $ \l ->
[int64ArrayPerm 0 l, int64ArrayPerm (bvMult 8 (toIdx l)) l] ===> int64array 0 (bvMult 2 (toIdx l))
]

, testGroup "borrows on rhs"
[ testCase "matched borrows" $ passes $
int64ArrayPerm 0 3 \\\ (1,2) ===> int64ArrayPerm 0 3 \\\ (1,2)

, testCase "sum of matched borrows" $ passes $
[ int64ArrayPerm 0 3 \\\ (1,2) , int64ArrayPerm 24 3 ]
===> int64ArrayPerm 0 6 \\\ (1,2)

, testCase "borrowed lhs/rhs offset" $ passes $
[ int64ArrayPerm 24 3,
int64ArrayPerm 48 2 ] ===> int64ArrayPerm 24 5 \\\ (3, 2)

, testCase "rhs borrow intersects two lhs borrows " $ fails $
int64ArrayPerm 0 10 \\\ (1, 3) \\\ (7,3) ===> int64ArrayPerm 0 10 \\\ (2,6)

, testCase "rhs borrow intersects two lhs borrows " $ passes $
[ int64ArrayPerm 0 5 \\\ (1, 3) \\\ (7,3)
, int64ArrayPerm 8 3
, int64ArrayPerm 56 3
] ===> int64ArrayPerm 0 5 \\\ (2,6)

, testCase "too much lhs borrowed" $ fails $ int64ArrayPerm 0 10 \\\ (5,2) ===> int64ArrayPerm 0 10 \\\ (5,1)

, testCase "sum of borrows" $ passes $
[ int64ArrayPerm 0 3 \\\ (1,2) , int64ArrayPerm 24 4 \\\ (1,2) ]
===> int64ArrayPerm 0 7 \\\ (1,2) \\\ (3,3)
]
]

main :: IO ()
main = defaultMain arrayTests
Loading

0 comments on commit 5d36808

Please sign in to comment.