-----------------------------------------------------------------------
-- |
-- Module : TestMain
-- Description : Test module for SymIO
-- Copyright : (c) Galois, Inc 2021
-- License : BSD3
-- Maintainer : Daniel Matichuk <dmatichuk@galois.com>
-- Stability : provisional
------------------------------------------------------------------------
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
module Main where
import GHC.TypeNats
import Control.Lens ( (^.) )
import Control.Monad (foldM )
import Control.Monad.IO.Class (liftIO)
import qualified Data.Map as Map
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.Classes
import Data.Parameterized.Some
import qualified Data.Parameterized.Nonce as N
import qualified Data.Parameterized.NatRepr as NR
import qualified Data.ByteString as BS
import qualified Data.BitVector.Sized as BVS
import qualified Test.Tasty as T
import qualified Test.Tasty.HUnit as T
import qualified Lang.Crucible.Backend.Simple as CB
import qualified Lang.Crucible.Backend as CB
import qualified Lang.Crucible.CFG.Core as CC
import qualified Lang.Crucible.Types as CT
import qualified Lang.Crucible.Simulator as CS
import qualified Lang.Crucible.Simulator.OverrideSim as CSO
import qualified Lang.Crucible.FunctionHandle as CFH
import qualified Lang.Crucible.Simulator.GlobalState as CGS
import qualified What4.Interface as W4
import qualified What4.Expr as WE
import qualified What4.Config as W4C
import qualified What4.Solver.Yices as W4Y
import qualified What4.Solver.Adapter as WSA
import qualified What4.SatResult as W4R
import qualified What4.Partial as W4
import qualified What4.CachedArray as CA
import qualified Lang.Crucible.SymIO as SymIO
import qualified System.IO as IO
main :: IO ()
main = T.defaultMain fsTests
fsTests :: T.TestTree
fsTests = T.testGroup "Filesystem Tests"
[ T.testCase "Concrete Reads" (runFSTest testConcReads)
, T.testCase "Overlapping Symbolic Writes" (runFSTest testOverlappingWritesSingle)
, T.testCase "Overlapping Symbolic Write Ranges" (runFSTest testOverlappingWritesRange)
, T.testCase "Unknown File" (runFSTest testUnknownFile)
, T.testCase "End Of File" (runFSTest testEOF)
]
data SymIOTestData t = SymIOTestData
runFSTest :: FSTest wptr -> IO ()
runFSTest fsTest = do
Some gen <- N.newIONonceGenerator
sym <- WE.newExprBuilder WE.FloatRealRepr WE.EmptyExprBuilderState gen
bak <- CB.newSimpleBackend sym
runFSTest' bak fsTest
tobs :: [Integer] -> BS.ByteString
tobs is = BS.pack (map fromIntegral is)
runFSTest' ::
forall sym bak wptr t st fs.
(sym ~ WE.ExprBuilder t st fs) =>
CB.IsSymBackend sym bak =>
ShowF (W4.SymExpr sym) =>
bak ->
FSTest wptr ->
IO ()
runFSTest' bak (FSTest fsTest) = do
let sym = CB.backendGetSym bak
let config = W4.getConfiguration sym
W4C.extendConfig W4Y.yicesOptions config
let
nRepr = NR.knownNat @wptr
let contents = SymIO.InitialFileSystemContents { SymIO.symbolicFiles = Map.empty
, SymIO.concreteFiles =
Map.fromList [ (SymIO.FileTarget "/test0", tobs [0,1,2])
, (SymIO.FileTarget "/test1", tobs [3,4,5,6])
]
, SymIO.useStdout = False
, SymIO.useStderr = False
}
fs <- SymIO.initFS sym nRepr contents
halloc <- CFH.newHandleAllocator
fsvar <- CC.freshGlobalVar halloc "fileSystem" (SymIO.FileSystemRepr nRepr)
let
initCtx = CS.initSimContext bak SymIO.symIOIntrinsicTypes halloc IO.stderr (CSO.fnBindingsFromList []) CS.emptyExtensionImpl ()
globals = CGS.insertGlobal fsvar fs CS.emptyGlobals
cont = CS.runOverrideSim CT.UnitRepr (fsTest fsvar)
initState = CS.InitialState initCtx globals CS.defaultAbortHandler CT.UnitRepr cont
eres <- CS.executeCrucible [] initState
case eres of
CS.TimeoutResult {} -> T.assertFailure "Timed out"
CS.AbortedResult _ ab -> T.assertFailure $ "Aborted: " ++ showAbortedResult ab
CS.FinishedResult _ pres -> case pres of
CS.TotalRes _ -> return ()
CS.PartialRes _ p _ _ -> case W4.asConstantPred p of
Just True -> return ()
_ -> do
putStrLn $ showF p
T.assertFailure "Partial Result"
obligations <- CB.getProofObligations bak
mapM_ (proveGoal sym W4Y.yicesAdapter) (maybe [] CB.goalsToList obligations)
proveGoal ::
(sym ~ WE.ExprBuilder t st fs) =>
CB.IsSymInterface sym =>
sym ->
WSA.SolverAdapter st ->
CB.ProofGoal (CB.Assumptions sym) (CB.Assertion sym) ->
IO ()
proveGoal sym adapter (CB.ProofGoal asms goal) = do
let goalPred = goal ^. CB.labeledPred
asmsPred <- CB.assumptionsPred sym asms
notgoal <- W4.notPred sym goalPred
WSA.solver_adapter_check_sat adapter sym WSA.defaultLogData [notgoal, asmsPred] $ \sr ->
case sr of
W4R.Unsat _ -> return ()
W4R.Unknown -> T.assertFailure "Inconclusive"
W4R.Sat _ -> do
putStrLn (showF asmsPred)
putStrLn (showF goalPred)
T.assertFailure "Assertion Failure"
showAbortedResult :: CS.AbortedResult c d -> String
showAbortedResult ar = case ar of
CS.AbortedExec reason _ -> show reason
CS.AbortedExit code -> show code
CS.AbortedBranch _ _ res' res'' -> "BRANCH: " <> showAbortedResult res' <> "\n" <> showAbortedResult res''
data FSTest (wptr :: Nat) where
FSTest :: (KnownNat wptr, 1 <= wptr) =>
(forall sym. (CB.IsSymInterface sym, ShowF (W4.SymExpr sym)) =>
CS.GlobalVar (SymIO.FileSystemType wptr) ->
CS.OverrideSim () sym () (CS.RegEntry sym CT.UnitType) Ctx.EmptyCtx CT.UnitType ()) ->
FSTest wptr
readOne ::
(CB.IsSymInterface sym, 1 <= wptr) =>
CS.GlobalVar (SymIO.FileSystemType wptr) ->
SymIO.FileHandle sym wptr ->
CS.OverrideSim p sym arch r args ret (W4.SymBV sym 8)
readOne fsVar fhdl = CS.ovrWithBackend $ \bak -> do
mval <- SymIO.readByte' fsVar fhdl
liftIO $ CB.readPartExpr bak mval (CS.AssertFailureSimError "readOne" "readOne")
readFromChunk ::
(CB.IsSymInterface sym, 1 <= wptr) =>
SymIO.DataChunk sym wptr ->
W4.SymBV sym wptr ->
CS.OverrideSim p sym arch r args ret (W4.SymBV sym 8)
readFromChunk chunk bv = liftIO $ CA.evalChunk chunk bv
testConcReads :: FSTest 32
testConcReads = FSTest $ \fsVar -> do
sym <- CS.getSymInterface
test0_name <- liftIO $ W4.stringLit sym (W4.Char8Literal "/test0")
test0FileHandle <- SymIO.openFile' fsVar test0_name
byte0_0 <- readOne fsVar test0FileHandle
byte0_1 <- readOne fsVar test0FileHandle
expect byte0_0 0
expect byte0_1 1
test1_name <- liftIO $ W4.stringLit sym (W4.Char8Literal "/test1")
test1FileHandle <- SymIO.openFile' fsVar test1_name
zero <- mkbv 0
one <- mkbv 1
two <- mkbv 2
three <- mkbv 3
byte1_0 <- readOne fsVar test1FileHandle
(chunk_1_1to3, _) <- SymIO.readChunk' fsVar test1FileHandle three
byte1_1 <- readFromChunk chunk_1_1to3 zero
byte1_2 <- readFromChunk chunk_1_1to3 one
byte1_3 <- readFromChunk chunk_1_1to3 two
expect byte1_0 3
expect byte1_1 4
expect byte1_2 5
expect byte1_3 6
mkCase fsVar "/test1" (3, 4, 5, 6)
expect ::
CB.IsSymInterface sym =>
KnownNat w =>
1 <= w =>
W4.SymBV sym w ->
Integer ->
CS.OverrideSim p sym arch r args ret ()
expect bv i = do
sym <- CS.getSymInterface
expectIf (return $ W4.truePred sym) bv i
expectIf ::
CB.IsSymInterface sym =>
KnownNat w =>
1 <= w =>
IO (W4.Pred sym) ->
W4.SymBV sym w ->
Integer ->
CS.OverrideSim p sym arch r args ret ()
expectIf test bv i = CS.ovrWithBackend $ \bak -> do
let sym = CB.backendGetSym bak
test' <- liftIO $ test
bv' <- liftIO $ W4.bvLit sym W4.knownRepr (BVS.mkBV W4.knownRepr i)
check <- liftIO $ W4.isEq sym bv bv'
check' <- liftIO $ W4.impliesPred sym test' check
liftIO $ CB.assert bak check' (CS.AssertFailureSimError "expect failure" "expect failure")
return ()
expectOne ::
forall p sym arch r args ret.
CB.IsSymInterface sym => W4.SymBV sym 8 -> [Integer] -> CS.OverrideSim p sym arch r args ret ()
expectOne bv is = CS.ovrWithBackend $ \bak -> do
let sym = CB.backendGetSym bak
let mkcheck :: Integer -> CS.OverrideSim p sym arch r args ret (W4.Pred sym)
mkcheck i = do
bv' <- liftIO $ W4.bvLit sym W4.knownRepr (BVS.mkBV W4.knownRepr i)
liftIO $ W4.isEq sym bv bv'
check <- foldM (\p i -> mkcheck i >>= \p' -> liftIO $ W4.orPred sym p p') (W4.falsePred sym) is
liftIO $ CB.assert bak check (CS.AssertFailureSimError "expect failure" "expect failure")
mkbv ::
forall wptr p sym arch r args ret.
CB.IsSymInterface sym =>
(KnownNat wptr, 1 <= wptr) =>
Integer ->
CS.OverrideSim p sym arch r args ret (W4.SymBV sym wptr)
mkbv i = do
sym <- CS.getSymInterface
liftIO $ W4.bvLit sym (W4.knownRepr :: W4.NatRepr wptr) (BVS.mkBV W4.knownRepr i)
maybeSeekOne ::
1 <= wptr =>
CB.IsSymInterface sym =>
CS.GlobalVar (SymIO.FileSystemType wptr) ->
SymIO.FileHandle sym wptr ->
CS.OverrideSim p sym arch r args ret (W4.Pred sym)
maybeSeekOne fsVar fhdl = do
sym <- CS.getSymInterface
b <- liftIO $ W4.freshConstant sym W4.emptySymbol W4.BaseBoolRepr
args <- CS.getOverrideArgs
CS.symbolicBranch b args (SymIO.readByte' fsVar fhdl >> return b) Nothing args (return b) Nothing
-- Nondeterministically seeking, but with a mux join
maybeSeekOne' ::
forall sym wptr p arch r args ret.
1 <= wptr =>
CB.IsSymInterface sym =>
CS.GlobalVar (SymIO.FileSystemType wptr) ->
SymIO.FileHandle sym wptr ->
CS.OverrideSim p sym arch r args ret (W4.Pred sym)
maybeSeekOne' fsVar fhdl = do
halloc <- CS.simHandleAllocator <$> CS.getContext
handle <- liftIO $ CFH.mkHandle halloc "maybeSeekOne"
ov <- return $ CS.mkOverride "maybeSeekOne" (maybeSeekOne fsVar fhdl)
(b :: CS.RegEntry sym CT.BoolType) <- CS.callOverride handle ov (CS.RegMap Ctx.empty)
return $ CS.regValue b
neither ::
CB.IsSymInterface sym =>
sym ->
W4.Pred sym ->
W4.Pred sym ->
IO (W4.Pred sym)
neither sym p1 p2 = do
not_p1 <- W4.notPred sym p1
not_p2 <- W4.notPred sym p2
W4.andPred sym not_p1 not_p2
testOverlappingWritesSingle :: FSTest 32
testOverlappingWritesSingle = FSTest $ \fsVar -> do
sym <- CS.getSymInterface
test1_name <- liftIO $ W4.stringLit sym (W4.Char8Literal "/test1")
test1FileHandle <- SymIO.openFile' fsVar test1_name
seek_1 <- maybeSeekOne' fsVar test1FileHandle
eight <- mkbv 8
SymIO.writeByte' fsVar test1FileHandle eight
test1FileHandle2 <- SymIO.openFile' fsVar test1_name
seek_2 <- maybeSeekOne' fsVar test1FileHandle2
nine <- mkbv 9
SymIO.writeByte' fsVar test1FileHandle2 nine
mkCases2 fsVar "/test1" seek_1 seek_2
(3, 9, 5, 6)
(9, 8, 5, 6)
(8, 9, 5, 6)
(9, 4, 5, 6)
return ()
testOverlappingWritesRange :: FSTest 32
testOverlappingWritesRange = FSTest $ \fsVar -> do
sym <- CS.getSymInterface
test1_name <- liftIO $ W4.stringLit sym (W4.Char8Literal "/test1")
test1FileHandle <- SymIO.openFile' fsVar test1_name
seek_1 <- maybeSeekOne' fsVar test1FileHandle
(chunk_8_9, two) <- mkConcreteChunk [8,9]
_ <- SymIO.writeChunk' fsVar test1FileHandle chunk_8_9 two
mkCases1 fsVar "/test1" seek_1
(3, 8, 9, 6)
(8, 9, 5, 6)
test1FileHandle2 <- SymIO.openFile' fsVar test1_name
(chunk_10_11, _) <- mkConcreteChunk [10,11]
seek_2 <- maybeSeekOne' fsVar test1FileHandle2
_ <- SymIO.writeChunk' fsVar test1FileHandle2 chunk_10_11 two
mkCases2 fsVar "/test1" seek_1 seek_2
(3, 10, 11, 6)
(10, 11, 9, 6)
(8, 10, 11, 6)
(10, 11, 5, 6)
testUnknownFile :: FSTest 32
testUnknownFile = FSTest $ \fsVar -> do
sym <- CS.getSymInterface
fhdl <- getSomeFile' fsVar
byte0 <- readOne fsVar fhdl
byte1 <- readOne fsVar fhdl
expectOne byte0 [0, 3]
zero <- mkbv 0
three <- mkbv 3
expectIf (W4.isEq sym byte0 zero) byte1 1
expectIf (W4.isEq sym byte0 three) byte1 4
testEOF :: FSTest 32
testEOF = FSTest $ \fsVar -> CS.ovrWithBackend $ \bak -> do
let sym = CB.backendGetSym bak
let err = CS.AssertFailureSimError "expect EOF" "expect EOF"
test0_name <- liftIO $ W4.stringLit sym (W4.Char8Literal "/test0")
fhdl <- SymIO.openFile' fsVar test0_name
_ <- readOne fsVar fhdl
_ <- readOne fsVar fhdl
_ <- readOne fsVar fhdl
eof <- SymIO.readByte' fsVar fhdl
assertNone eof err
isOpen <- SymIO.isHandleOpen fsVar fhdl
liftIO $ CB.assert bak isOpen err
fhdl2 <- SymIO.openFile' fsVar test0_name
_ <- readOne fsVar fhdl2
three <- mkbv 3
zero <- mkbv 0
one <- mkbv 1
(chunk_2to3, readBytes) <- SymIO.readChunk' fsVar fhdl2 three
expect readBytes 2
byte_2 <- readFromChunk chunk_2to3 zero
byte_3 <- readFromChunk chunk_2to3 one
expect byte_2 1
expect byte_3 2
(_, readBytes2) <- SymIO.readChunk' fsVar fhdl2 three
expect readBytes2 0
isOpen2 <- SymIO.isHandleOpen fsVar fhdl2
liftIO $ CB.assert bak isOpen2 err
fhdl3 <- SymIO.openFile' fsVar test0_name
SymIO.closeFileHandle' fsVar fhdl3
isOpen3 <- SymIO.isHandleOpen fsVar fhdl3
assertNot isOpen3 err
fhdl4 <- SymIO.openFile' fsVar test0_name
SymIO.writeByte' fsVar fhdl4 =<< mkbv 8
SymIO.writeByte' fsVar fhdl4 =<< mkbv 9
SymIO.writeByte' fsVar fhdl4 =<< mkbv 10
SymIO.writeByte' fsVar fhdl4 =<< mkbv 11
eof' <- SymIO.readByte' fsVar fhdl4
assertNone eof' err
mkCase fsVar "/test0" (8, 9, 10, 11)
assertNot ::
CB.IsSymInterface sym =>
W4.Pred sym ->
CS.SimErrorReason ->
CS.OverrideSim p sym arch r args ret ()
assertNot p er = CS.ovrWithBackend $ \bak -> do
let sym = CB.backendGetSym bak
notp <- liftIO $ W4.notPred sym p
liftIO $ CB.assert bak notp er
assertNone ::
CB.IsSymInterface sym =>
W4.PartExpr (W4.Pred sym) v ->
CS.SimErrorReason ->
CS.OverrideSim p sym arch r args ret ()
assertNone pe er = case pe of
W4.Unassigned -> return ()
W4.PE p _ -> assertNot p er
getSomeFile ::
forall sym wptr p arch r args ret.
1 <= wptr =>
CB.IsSymInterface sym =>
CS.GlobalVar (SymIO.FileSystemType wptr) ->
CS.OverrideSim p sym arch r args ret (SymIO.FileHandle sym wptr)
getSomeFile fsVar = do
sym <- CS.getSymInterface
b <- liftIO $ W4.freshConstant sym W4.emptySymbol W4.BaseBoolRepr
args <- CS.getOverrideArgs
test0_name <- liftIO $ W4.stringLit sym (W4.Char8Literal "/test0")
test1_name <- liftIO $ W4.stringLit sym (W4.Char8Literal "/test1")
CS.symbolicBranch b args (SymIO.openFile' fsVar test0_name) Nothing args (SymIO.openFile' fsVar test1_name) Nothing
getSomeFile' ::
forall sym wptr p arch r args ret.
1 <= wptr =>
KnownNat wptr =>
CB.IsSymInterface sym =>
CS.GlobalVar (SymIO.FileSystemType wptr) ->
CS.OverrideSim p sym arch r args ret (SymIO.FileHandle sym wptr)
getSomeFile' fsVar = do
halloc <- CS.simHandleAllocator <$> CS.getContext
handle <- liftIO $ CFH.mkHandle halloc "getSomeFile"
ov <- return $ CS.mkOverride "getSomeFile" (getSomeFile fsVar)
(b :: CS.RegEntry sym (SymIO.FileHandleType wptr)) <- CS.callOverride handle ov (CS.RegMap Ctx.empty)
return $ CS.regValue b
mkConcreteChunk ::
forall sym wptr p arch r args ret.
KnownNat wptr =>
1 <= wptr =>
CB.IsSymInterface sym =>
[Integer] ->
CS.OverrideSim p sym arch r args ret (SymIO.DataChunk sym wptr, W4.SymBV sym wptr)
mkConcreteChunk bytes = do
sym <- CS.getSymInterface
arr <- liftIO $ W4.freshConstant sym W4.emptySymbol W4.knownRepr
sz <- mkbv (fromIntegral $ length bytes)
arr' <- foldM go arr (zip [0..] bytes)
chunk <- liftIO $ CA.arrayToChunk sym arr'
return (chunk, sz)
where
go ::
W4.SymArray sym (Ctx.EmptyCtx Ctx.::> W4.BaseBVType wptr) (W4.BaseBVType 8) ->
(Integer, Integer) ->
CS.OverrideSim p sym arch r args ret (W4.SymArray sym (Ctx.EmptyCtx Ctx.::> W4.BaseBVType wptr) (W4.BaseBVType 8))
go arr (idx, val) = do
idxbv <- mkbv idx
valbv <- mkbv val
sym <- CS.getSymInterface
liftIO $ W4.arrayUpdate sym arr (Ctx.empty Ctx.:> idxbv) valbv
mkCase ::
forall p sym arch r args ret wptr.
CB.IsSymInterface sym =>
1 <= wptr =>
CS.GlobalVar (SymIO.FileSystemType wptr) ->
BS.ByteString ->
(Integer, Integer, Integer, Integer) ->
CS.OverrideSim p sym arch r args ret ()
mkCase fsVar nm case_ = do
sym <- CS.getSymInterface
mkCases1 fsVar nm (W4.truePred sym) case_ case_
mkCases1 ::
forall p sym arch r args ret wptr.
CB.IsSymInterface sym =>
1 <= wptr =>
CS.GlobalVar (SymIO.FileSystemType wptr) ->
BS.ByteString ->
W4.Pred sym ->
(Integer, Integer, Integer, Integer) ->
(Integer, Integer, Integer, Integer) ->
CS.OverrideSim p sym arch r args ret ()
mkCases1 fsVar nm seek case1 case2 = do
sym <- CS.getSymInterface
mkCases2 fsVar nm seek (W4.truePred sym) case1 case1 case2 case2
mkCases2 ::
forall p sym arch r args ret wptr.
CB.IsSymInterface sym =>
1 <= wptr =>
CS.GlobalVar (SymIO.FileSystemType wptr) ->
BS.ByteString ->
W4.Pred sym ->
W4.Pred sym ->
(Integer, Integer, Integer, Integer) ->
(Integer, Integer, Integer, Integer) ->
(Integer, Integer, Integer, Integer) ->
(Integer, Integer, Integer, Integer) ->
CS.OverrideSim p sym arch r args ret ()
mkCases2 fsVar nm seek_1 seek_2 case1 case2 case3 case4 = do
sym <- CS.getSymInterface
name <- liftIO $ W4.stringLit sym (W4.Char8Literal nm)
fhdl <- SymIO.openFile' fsVar name
byte1 <- readOne fsVar fhdl
byte2 <- readOne fsVar fhdl
byte3 <- readOne fsVar fhdl
byte4 <- readOne fsVar fhdl
let
assertCase ::
(Integer, Integer, Integer, Integer) ->
CS.OverrideSim p sym arch r args ret ()
assertCase (i1, i2, i3, i4) = do
expect byte1 i1
expect byte2 i2
expect byte3 i3
expect byte4 i4
args <- CS.getOverrideArgs
CS.symbolicBranch seek_1 args
(CS.symbolicBranch seek_2 args (assertCase case1) Nothing
args (assertCase case2) Nothing)
Nothing
args
(CS.symbolicBranch seek_2 args (assertCase case3) Nothing
args (assertCase case4) Nothing)
Nothing