diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for crucible-symio + +## 0.1 -- 2024-02-05 + +* First version. Released on an unsuspecting world. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2021-2022 Galois Inc. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in + the documentation and/or other materials provided with the + distribution. + + * Neither the name of Galois, Inc. nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED +TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER +OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/crucible-symio.cabal b/crucible-symio.cabal new file mode 100644 --- /dev/null +++ b/crucible-symio.cabal @@ -0,0 +1,74 @@ +cabal-version: 2.2 +synopsis: An implementation of symbolic I/O primitives for Crucible +description: + This library provides language-independent overrides implementing filesystem + operations (as provided by most operating systems). These primitives support + reading and writing symbolic data. An example use case would be to support verifying + programs that e.g., use configuration files or accept input from files. +name: crucible-symio +version: 0.1 +license: BSD-3-Clause +license-file: LICENSE +author: Daniel Matichuk +maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com +build-type: Simple +category: Language +extra-source-files: CHANGELOG.md + +source-repository head + type: git + location: https://github.com/GaloisInc/crucible + subdir: crucible-symio + +common shared + build-depends: base >=4.12 && <4.19, + aeson, + bv-sized, + bytestring, + crucible, + containers, + directory, + filemanip, + filepath, + IntervalMap, + lens, + mtl, + parameterized-utils, + text, + what4 + +library + import: shared + exposed-modules: + Lang.Crucible.SymIO + Lang.Crucible.SymIO.Loader + other-modules: + Lang.Crucible.SymIO.Types + What4.CachedArray + Data.Parameterized.IntervalsMap + hs-source-dirs: src + default-language: Haskell2010 + ghc-options: -Wall -Wcompat + +test-suite crucible-symio-tests + import: shared + type: exitcode-stdio-1.0 + default-language: Haskell2010 + other-modules: + Data.Parameterized.IntervalsMap + Lang.Crucible.SymIO + Lang.Crucible.SymIO.Loader + Lang.Crucible.SymIO.Types + What4.CachedArray + main-is: TestMain.hs + hs-source-dirs: tests, src + ghc-options: -Wall -Wcompat + build-depends: base >=4.12 && <4.19, + what4, + crucible, + crucible-symio, + parameterized-utils, + tasty, + tasty-hunit + + diff --git a/src/Data/Parameterized/IntervalsMap.hs b/src/Data/Parameterized/IntervalsMap.hs new file mode 100644 --- /dev/null +++ b/src/Data/Parameterized/IntervalsMap.hs @@ -0,0 +1,322 @@ +----------------------------------------------------------------------- +-- | +-- Module : Data.IntervalsMap +-- Description : Nested intervals +-- Copyright : (c) Galois, Inc 2020 +-- License : BSD3 +-- Maintainer : Daniel Matichuk +-- Stability : provisional +------------------------------------------------------------------------ + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE FlexibleInstances, FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE FunctionalDependencies #-} + +module Data.Parameterized.IntervalsMap + ( IntervalF(..) + , mkIntervalF + , Intervals(..) + , IntervalsMap + , intersecting + , unionWith + , unionWithM + , singleton + , insertWith + , insertWithM + , intersectionWith + , mapMIntersecting + , fromList + , toList + , empty + , IM.Interval(..) + , mergeIntervalsF + , mergeWithM + , AsOrd(..) + ) where + + +import Data.Kind ( Type ) +import Data.Maybe (catMaybes) + +import Data.IntervalMap.Strict ( IntervalMap ) +import qualified Data.IntervalMap.Strict as IM +import qualified Data.IntervalMap.Interval as IM +import qualified Data.IntervalMap.Generic.Strict as IMG + +import Data.Parameterized.Classes +import qualified Data.Parameterized.Context as Ctx + +newtype AsOrd f tp where + AsOrd :: { unAsOrd :: f tp } -> AsOrd f tp + +instance TestEquality f => Eq (AsOrd f tp) where + (AsOrd a) == (AsOrd b) = case testEquality a b of + Just Refl -> True + _ -> False + +instance OrdF f => Ord (AsOrd f tp) where + compare (AsOrd a) (AsOrd b) = toOrdering $ compareF a b + +newtype IntervalF f tp where + IntervalF :: IM.Interval (AsOrd f tp) -> IntervalF f tp + +mkIntervalF :: + IM.Interval (f tp) -> IntervalF f tp +mkIntervalF ival = IntervalF $ fmap AsOrd ival + +instance TestEquality f => TestEquality (IntervalF f) where + testEquality (IntervalF i1) (IntervalF i2) = case testEquality (unAsOrd (IM.lowerBound i1)) (unAsOrd (IM.lowerBound i2)) of + Just Refl | i1 == i2 -> Just Refl + _ -> Nothing + +deriving instance TestEquality f => Eq (IntervalF f tp) + +deriving instance OrdF f => Ord (IntervalF f tp) + +newtype Intervals f ctx = Intervals (Ctx.Assignment (IntervalF f) ctx) + +deriving instance TestEquality f => Eq (Intervals f ctx) + +instance OrdF f => Ord (Intervals f ctx) where + compare (Intervals (rest1 Ctx.:> a1)) (Intervals (rest2 Ctx.:> a2)) = + compare a1 a2 <> compare (Intervals rest1) (Intervals rest2) + compare (Intervals Ctx.Empty) (Intervals Ctx.Empty) = EQ + +data IntervalsMap (f :: k -> Type) (ctx :: Ctx.Ctx k) tp where + IntervalsMapCons :: + IntervalMap (AsOrd f idx) (IntervalsMap f ctx tp) -> + IntervalsMap f (ctx Ctx.::> idx) tp + IntervalsMapHead :: tp -> IntervalsMap f Ctx.EmptyCtx tp + +instance Functor (IntervalsMap f ctx) where + fmap f ims = case ims of + IntervalsMapCons ims' -> IntervalsMapCons (fmap (fmap f) ims') + IntervalsMapHead v -> IntervalsMapHead $ f v + +instance Foldable (IntervalsMap f ctx) where + foldMap f (IntervalsMapCons ims') = foldMap (foldMap f) ims' + foldMap f (IntervalsMapHead v) = f v + +instance Traversable (IntervalsMap f ctx) where + traverse f (IntervalsMapCons ims') = IntervalsMapCons <$> traverse (traverse f) ims' + traverse f (IntervalsMapHead v) = IntervalsMapHead <$> f v + +intersecting :: + OrdF f => + IntervalsMap f ctx tp -> + Intervals f ctx -> + IntervalsMap f ctx tp +intersecting (IntervalsMapCons ims) (Intervals (rest Ctx.:> IntervalF k)) = + let + top = IM.intersecting ims k + in IntervalsMapCons $ fmap (\ims' -> intersecting ims' (Intervals rest)) top +intersecting v (Intervals Ctx.Empty) = v + +fromList :: + OrdF f => + [(Intervals f (ctx Ctx.::> a), tp)] -> + IntervalsMap f (ctx Ctx.::> a) tp +fromList es = foldr (unionWith (\l _ -> l)) empty (map (uncurry singleton) es) + +toList :: + IntervalsMap f ctx tp -> + [(Intervals f ctx, tp)] +toList (IntervalsMapCons ims) = + concat $ map (\(k, es) -> addTo k (toList es)) $ (IM.toList ims) + where + addTo :: IM.Interval (AsOrd f a) -> [(Intervals f ctx, tp)] -> [(Intervals f (ctx Ctx.::> a), tp)] + addTo ival = map (\(Intervals ivalf, a) -> (Intervals $ ivalf Ctx.:> IntervalF ival, a)) +toList (IntervalsMapHead v) = [(Intervals Ctx.empty, v)] + +unionWith :: + OrdF f => + (a -> a -> a) -> + IntervalsMap f ctx a -> + IntervalsMap f ctx a -> + IntervalsMap f ctx a +unionWith f (IntervalsMapCons ims1) (IntervalsMapCons ims2) = + IntervalsMapCons $ IM.unionWith (unionWith f) ims1 ims2 +unionWith f (IntervalsMapHead v1) (IntervalsMapHead v2) = IntervalsMapHead $ f v1 v2 + +unionWithM :: + forall f m a ctx. + OrdF f => + Monad m => + (a -> a -> m a) -> + IntervalsMap f ctx a -> + IntervalsMap f ctx a -> + m (IntervalsMap f ctx a) +unionWithM f ims1 ims2 = sequenceA $ unionWith go (fmap return ims1) (fmap return ims2) + where + go :: m a -> m a -> m a + go f1 f2 = do + v1 <- f1 + v2 <- f2 + f v1 v2 + +data MergeResult a b = + MergeLeft a + | MergeRight b + | MergeCombined a b + +mergeWithM :: + forall f m a b c ctx. + OrdF f => + Monad m => + (a -> m c) -> + (b -> m c) -> + (a -> b -> m c) -> + IntervalsMap f ctx a -> + IntervalsMap f ctx b -> + m (IntervalsMap f ctx c) +mergeWithM inLeft inRight combine ims1 ims2 = do + traverse eval $ unionWith go (fmap MergeLeft ims1) (fmap MergeRight ims2) + where + eval :: MergeResult a b -> m c + eval (MergeLeft a) = inLeft a + eval (MergeRight b) = inRight b + eval (MergeCombined a b) = combine a b + + go :: MergeResult a b -> MergeResult a b -> MergeResult a b + go (MergeLeft f1) (MergeRight f2) = MergeCombined f1 f2 + go _ _ = error "mergeWithM: unexpected MergeResult" + + +singleton :: + Intervals f ctx -> + tp -> + IntervalsMap f ctx tp +singleton (Intervals (rest Ctx.:> IntervalF k)) v = IntervalsMapCons $ IM.singleton k (singleton (Intervals rest) v) +singleton (Intervals Ctx.Empty) v = IntervalsMapHead v + +empty :: IntervalsMap f (ctx Ctx.::> a) tp +empty = IntervalsMapCons IM.empty + +insertWith :: + OrdF f => + (tp -> tp -> tp) -> + Intervals f ctx -> + tp -> + IntervalsMap f ctx tp -> + IntervalsMap f ctx tp +insertWith f k v = unionWith f (singleton k v) + + +insertWithM :: + forall m f ctx tp. + Monad m => + OrdF f => + (tp -> tp -> m tp) -> + Intervals f ctx -> + tp -> + IntervalsMap f ctx tp -> + m (IntervalsMap f ctx tp) +insertWithM f k v ims = sequenceA $ insertWith go k (return v) (fmap return ims) + where + go :: m tp -> m tp -> m tp + go f1 f2 = do + v1 <- f1 + v2 <- f2 + f v1 v2 + +intersectionWith :: + OrdF f => + (a -> b -> c) -> + IntervalsMap f ctx a -> + IntervalsMap f ctx b -> + IntervalsMap f ctx c +intersectionWith f (IntervalsMapCons ims1) (IntervalsMapCons ims2) = + IntervalsMapCons $ IM.intersectionWith (intersectionWith f) ims1 ims2 +intersectionWith f (IntervalsMapHead v1) (IntervalsMapHead v2) = IntervalsMapHead $ f v1 v2 + +mapMIntersecting' :: + Monad m => + OrdF f => + Intervals f ctx -> + (tp -> m (Maybe tp)) -> + IntervalsMap f ctx tp -> + m (Maybe (IntervalsMap f ctx tp)) +mapMIntersecting' (Intervals (rest Ctx.:> IntervalF k)) f (IntervalsMapCons ims) = do + ims' <- mapMIntersectingBase k (\_ -> mapMIntersecting' (Intervals rest) f) ims + case IM.size ims' of + 0 -> return Nothing + _ -> return $ Just (IntervalsMapCons ims') +mapMIntersecting' (Intervals Ctx.Empty) f (IntervalsMapHead v) = fmap IntervalsMapHead <$> f v + +-- | Adjust entries which intersect the given interval +mapMIntersecting :: + Monad m => + OrdF f => + Intervals f (ctx Ctx.::> a) -> + (tp -> m (Maybe tp)) -> + IntervalsMap f (ctx Ctx.::> a) tp -> + m (IntervalsMap f (ctx Ctx.::> a) tp) +mapMIntersecting i f ims = mapMIntersecting' i f ims >>= \case + Just ims' -> return ims' + Nothing -> return $ IntervalsMapCons IM.empty + + +mapMIntersectingBase :: + forall k v e m. + Monad m => + IMG.Interval k e => + Ord k => + k -> + (k -> v -> m (Maybe v)) -> + IMG.IntervalMap k v -> + m (IMG.IntervalMap k v) +mapMIntersectingBase k f im = do + let (pref, inter, suf) = IM.splitIntersecting im k + case IM.size inter of + 0 -> return im + _ -> do + im' <- catMaybes <$> mapM go (IM.toAscList inter) + return $ IM.fromDistinctAscList (IM.toAscList pref ++ im' ++ IM.toAscList suf) + where + go :: (k, v) -> m (Maybe (k, v)) + go (k', v) = f k' v >>= \case + Just v' -> return $ Just (k', v') + Nothing -> return Nothing + + +mergeIntervals :: + Ord a => + IM.Interval a -> + IM.Interval a -> + IM.Interval a +mergeIntervals i1 i2 = case (leftClosed, rightClosed) of + (True, True) -> IM.ClosedInterval lower upper + (False, True) -> IM.IntervalOC lower upper + (True, False) -> IM.IntervalCO lower upper + (False, False) -> IM.OpenInterval lower upper + where + leftClosed = (IM.leftClosed i1 && lo1 <= lo2) || (IM.leftClosed i2 && lo2 <= lo1) + rightClosed = (IM.rightClosed i1 && hi2 <= hi1) || (IM.rightClosed i2 && hi1 <= hi2) + lo1 = IM.lowerBound i1 + lo2 = IM.lowerBound i2 + hi1 = IM.upperBound i1 + hi2 = IM.upperBound i2 + lower = min lo1 lo2 + upper = max hi1 hi2 + +mergeIntervalsF :: + OrdF f => + IntervalF f a -> + IntervalF f a -> + IntervalF f a +mergeIntervalsF (IntervalF i1) (IntervalF i2) = IntervalF (mergeIntervals i1 i2) diff --git a/src/Lang/Crucible/SymIO.hs b/src/Lang/Crucible/SymIO.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/SymIO.hs @@ -0,0 +1,823 @@ +----------------------------------------------------------------------- +-- | +-- Module : Lang.Crucible.SymIO +-- Description : Core definitions of the symbolic filesystem model +-- Copyright : (c) Galois, Inc 2020 +-- License : BSD3 +-- Maintainer : Daniel Matichuk +-- Stability : provisional +------------------------------------------------------------------------ + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE FlexibleInstances, FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE FunctionalDependencies #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Lang.Crucible.SymIO + ( + -- * Setup + FDTarget(..) + , TargetDirection + , In + , Out + , fdTargetToText + , InitialFileSystemContents(..) + , emptyInitialFileSystemContents + -- * Filesystem types + -- $filetypes + , FileSystemType + , FileHandle + , FileHandleType + , FilePointer + , FilePointerType + , FileIdent + , DataChunk + , CA.mkArrayChunk + -- ** Reprs + , pattern FileRepr + , pattern FileSystemRepr + -- * Filesystem operations + -- $fileops + , initFS + , openFile + , openFile' + , readByte + , readByte' + , writeByte + , writeByte' + , readChunk + , readChunk' + , writeChunk + , writeChunk' + , closeFileHandle + , closeFileHandle' + , isHandleOpen + , invalidFileHandle + , symIOIntrinsicTypes + , CA.chunkToArray + , CA.arrayToChunk + , CA.evalChunk + -- * Error conditions + , FileIdentError(..) + , FileHandleError(..) + ) where + +import GHC.TypeNats +import GHC.Stack + +import Control.Arrow ( first ) +import Control.Monad.IO.Class ( MonadIO, liftIO ) +import qualified Control.Monad.State as CMS +import qualified Control.Monad.Trans as CMT + +import qualified Data.Text as Text +import qualified Data.Text.Encoding as Text +import qualified Data.Traversable as DT +import qualified Data.Map as Map +import qualified Data.BitVector.Sized as BV +import qualified Data.ByteString as BS + +import qualified Data.Parameterized.Classes as PC +import Data.Parameterized.Context ( pattern (:>), pattern Empty ) +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.NatRepr + +import Lang.Crucible.CFG.Core +import Lang.Crucible.Simulator.RegMap ( RegMap(..), emptyRegMap, RegEntry(..), unconsReg, regMapSize ) +import Lang.Crucible.Simulator.SimError +import qualified Lang.Crucible.Simulator.OverrideSim as C + +import Lang.Crucible.Backend +import Lang.Crucible.Utils.MuxTree +import qualified What4.Interface as W4 +import qualified What4.Concrete as W4C +import What4.Partial + +import qualified What4.CachedArray as CA +import Lang.Crucible.SymIO.Types + +--------------------------------------- +-- Interface + +data TargetDirection = In | Out +type In = 'In +type Out = 'Out + +-- | Files to which concrete or symbolic contents can be assigned +-- +-- This covers both named files and the standard I/O streams. In the future, it +-- could also cover sockets and other file-like entities. Note that the GADT +-- tags are in place to let us restrict the 'InitialFileSystemContents' to only +-- refer to files that can serve as inputs (i.e., write only files cannot have +-- initial contents). +data FDTarget (k :: TargetDirection) where + FileTarget :: FilePath -> FDTarget In + StdinTarget :: FDTarget In + StdoutTarget :: FDTarget Out + StderrTarget :: FDTarget Out + +deriving instance Eq (FDTarget k) +deriving instance Ord (FDTarget k) +deriving instance Show (FDTarget k) +instance PC.ShowF FDTarget where + showF = show + +-- | Convert an 'FDTarget' to 'T.Text' +-- +-- We need to do this because filenames are stored in a Crucible StringMap, so +-- we can't use our custom ADT. We have to do some custom namespacing here to +-- avoid collisions between named files and our special files. +-- +-- We will adopt the convention that /all/ actual files will have absolute paths +-- in the symbolic filesystem. The special files will have names that are not +-- valid absolute paths. +-- +-- FIXME: Add some validation somewhere so that we actually enforce the absolute +-- path property +fdTargetToText :: FDTarget k -> Text.Text +fdTargetToText t = + case t of + FileTarget f -> Text.pack f + StdinTarget -> Text.pack "stdin" + StdoutTarget -> Text.pack "stdout" + StderrTarget -> Text.pack "stderr" + +-- | The initial contents of the symbolic filesystem +-- +-- Note that standard input will be enabled if it is specified as one of the +-- 'FDTarget' keys. +-- +-- Standard output and standard error will be connected if possible and if their +-- respective boolean flags are set to True +data InitialFileSystemContents sym = + InitialFileSystemContents { concreteFiles :: Map.Map (FDTarget In) BS.ByteString + , symbolicFiles :: Map.Map (FDTarget In) [W4.SymBV sym 8] + , useStdout :: Bool + , useStderr :: Bool + } + +-- | An empty initial symbolic filesystem +-- +-- This has no files and also disables stdout and stderr +emptyInitialFileSystemContents :: InitialFileSystemContents sym +emptyInitialFileSystemContents = + InitialFileSystemContents { concreteFiles = Map.empty + , symbolicFiles = Map.empty + , useStdout = False + , useStderr = False + } + +singletonIf :: Bool -> a -> [a] +singletonIf b p = if b then [p] else [] + +-- $fileops +-- Top-level overrides for filesystem operations. + +-- $filetypes +-- The associated crucible types used to interact with the filesystem. + +-- | Create an initial 'FileSystem' based on files with initial symbolic and +-- concrete contents +initFS + :: forall sym wptr + .(1 <= wptr, IsSymInterface sym) + => sym + -- ^ The symbolic backend + -> NatRepr wptr + -- ^ A type-level representative of the pointer width + -> InitialFileSystemContents sym + -- ^ The initial contents of the filesystem + -> IO (FileSystem sym wptr) +initFS sym ptrSize initContents = do + let symContents = fmap (first Some) $ Map.toList (symbolicFiles initContents) + let stdioOutputs = concat [ singletonIf (useStdout initContents) (Some StdoutTarget, BS.empty) + , singletonIf (useStderr initContents) (Some StderrTarget, BS.empty) + ] + let concContents = stdioOutputs ++ fmap (first Some) (Map.toList (concreteFiles initContents)) + symContents' <- DT.forM concContents $ \(name, bytes) -> do + bytes' <- bytesToSym bytes + return (name, bytes') + let + contentsIdx = zip [0..] (symContents ++ symContents') + flatContents = + concat $ map (\(fileIdx, (_, bytes)) -> + map (\(offset, byte) -> (fileIdx, offset, byte)) (zip [0..] bytes)) + contentsIdx + + initArray <- CA.initArrayConcrete sym (W4.BaseBVRepr (knownNat @8)) + (map mkFileEntry flatContents) + + sizes <- DT.forM contentsIdx $ \(fileIdx, (_, bytes)) -> do + size_bv <- W4.bvLit sym ptrSize (BV.mkBV ptrSize (fromIntegral (length bytes))) + return $ (Ctx.empty :> W4C.ConcreteInteger fileIdx, size_bv) + + sizes_arr <- CA.initArrayConcrete sym (W4.BaseBVRepr ptrSize) sizes + + names <- DT.forM contentsIdx $ \(fileIdx, (name, _)) -> do + fileIdx_int <- W4.intLit sym fileIdx + return $ (name, justPartExpr sym (File ptrSize fileIdx_int)) + + return $ FileSystem + { fsPtrSize = ptrSize + , fsFileNames = Map.fromList [ (fdTargetToText name, x) + | (Some name, x) <- names + ] + , fsFileSizes = sizes_arr + , fsSymData = initArray + , fsConstraints = \x -> x + } + + where + bytesToSym :: BS.ByteString -> IO [W4.SymBV sym 8] + bytesToSym bs = mapM (\w -> W4.bvLit sym (knownNat @8) (BV.word8 w)) (BS.unpack bs) + + mkFileEntry :: + -- | file identifier, offset into file, byte value + (Integer, Integer, W4.SymBV sym 8) -> + (Ctx.Assignment W4C.ConcreteVal (EmptyCtx ::> BaseBVType wptr ::> BaseIntegerType), + W4.SymBV sym 8) + mkFileEntry (fileIdent, offset, byte) = + (Ctx.empty :> W4C.ConcreteBV ptrSize (BV.mkBV ptrSize offset) :> W4C.ConcreteInteger fileIdent, byte) + +-- | Close a file by invalidating its file handle + +closeFileHandle :: + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileHandle sym wptr -> + (forall args'. Maybe FileHandleError -> C.OverrideSim p sym arch r args' ret a) -> + C.OverrideSim p sym arch r args ret a +closeFileHandle fvar fhdl cont = runFileMHandleCont fvar fhdl emptyRegMap (\a -> cont (eitherToMaybeL a)) $ \_ fhdl' -> do + sz <- getPtrSz + sym <- getSym + liftOV $ C.writeMuxTreeRef (MaybeRepr (FilePointerRepr sz)) fhdl' (maybePartExpr sym Nothing) + + +-- | Partial version of 'closeFileHandle' that asserts success. +closeFileHandle' :: + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileHandle sym wptr -> + C.OverrideSim p sym arch r args ret () +closeFileHandle' fvar fhdl = closeFileHandle fvar fhdl $ \merr -> + case merr of + Nothing -> return () + Just FileHandleClosed -> + C.ovrWithBackend $ \bak -> + liftIO $ addFailedAssertion bak $ + AssertFailureSimError + "Attempted to close already closed file handle." + "closeFileHandle': Unassigned file handle." + +eitherToMaybeL :: Either a b -> Maybe a +eitherToMaybeL (Left a) = Just a +eitherToMaybeL _ = Nothing + +-- | Open a file by resolving a 'FileIdent' into a 'File' and then allocating a fresh +-- 'FileHandle' pointing to the start of its contents. +openFile :: + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileIdent sym -> + (forall args'. Either FileIdentError (FileHandle sym wptr) -> C.OverrideSim p sym arch r args' ret a) -> + C.OverrideSim p sym arch r args ret a +openFile fsVar ident cont = runFileMIdentCont fsVar ident cont $ \ident' -> do + file <- resolveFileIdent ident' + openResolvedFile file + +-- | Partial version of 'openFile' that asserts success. +openFile' :: + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileIdent sym -> + C.OverrideSim p sym arch r args ret (FileHandle sym wptr) +openFile' fsVar ident = openFile fsVar ident $ \case + Left FileNotFound -> + C.ovrWithBackend $ \bak -> + liftIO $ addFailedAssertion bak $ + AssertFailureSimError + "Could not open file." + ("openFile': Invalid file identifier: " ++ show (W4.printSymExpr ident)) + Right fhdl -> return fhdl + +-- | Write a single byte to the given 'FileHandle' and increment it +writeByte :: + forall p sym arch r args ret wptr a. + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileHandle sym wptr -> + W4.SymBV sym 8 -> + (forall args'. Maybe FileHandleError -> C.OverrideSim p sym arch r args' ret a) -> + C.OverrideSim p sym arch r args ret a +writeByte fsVar fhdl byte cont = do + let args = RegMap (Empty :> RegEntry (BVRepr (knownNat @8)) byte) + runFileMHandleCont fsVar fhdl args (\a -> cont (eitherToMaybeL a)) $ \(RegMap (Empty :> RegEntry _ byte')) fhdl' -> do + ptr <- getHandle fhdl' + writeBytePointer ptr byte' + sym <- getSym + repr <- getPtrSz + one <- liftIO $ W4.bvLit sym repr (BV.mkBV repr 1) + incHandleWrite fhdl' one + +-- | Partial version of 'writeByte' that asserts success. +writeByte' :: + forall p sym arch r args ret wptr. + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileHandle sym wptr -> + W4.SymBV sym 8 -> + C.OverrideSim p sym arch r args ret () +writeByte' fsVar fhdl byte = writeByte fsVar fhdl byte $ \case + Just FileHandleClosed -> + C.ovrWithBackend $ \bak -> + liftIO $ addFailedAssertion bak $ + AssertFailureSimError + "Failed to write byte due to closed file handle." + "writeByte': Closed file handle" + Nothing -> return () + +-- | Write a chunk to the given 'FileHandle' and increment it to the end of +-- the written data. Returns the number of bytes written. +writeChunk :: + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileHandle sym wptr -> + DataChunk sym wptr -> + W4.SymBV sym wptr -> + (forall args'. Either FileHandleError (W4.SymBV sym wptr) -> C.OverrideSim p sym arch r args' ret a) -> + C.OverrideSim p sym arch r args ret a +writeChunk fsVar fhdl chunk sz cont = do + W4.BaseBVRepr ptrSz <- return $ W4.exprType sz + let args = RegMap (Empty :> RegEntry (BVRepr ptrSz) sz) + runFileMHandleCont fsVar fhdl args cont $ \(RegMap (Empty :> RegEntry _ sz')) fhdl' -> do + ptr <- getHandle fhdl' + writeChunkPointer ptr chunk sz' + incHandleWrite fhdl' sz' + +-- | Partial version of 'writeArray' that asserts success. +writeChunk' :: + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileHandle sym wptr -> + DataChunk sym wptr -> + W4.SymBV sym wptr -> + C.OverrideSim p sym arch r args ret (W4.SymBV sym wptr) +writeChunk' fsVar fhdl chunk sz = writeChunk fsVar fhdl chunk sz $ \case + Left FileHandleClosed -> + C.ovrWithBackend $ \bak -> + liftIO $ addFailedAssertion bak $ + AssertFailureSimError + "Failed to write array due to closed file handle." + "writeArray': Closed file handle" + Right sz' -> return sz' + +-- | Read a byte from a given 'FileHandle' and increment it. +-- The partial result is undefined if the read yields no results. +readByte :: + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileHandle sym wptr -> + (forall args'. Either FileHandleError (PartExpr (W4.Pred sym) (W4.SymBV sym 8)) -> C.OverrideSim p sym arch r args' ret a) -> + C.OverrideSim p sym arch r args ret a +readByte fsVar fhdl cont = runFileMHandleCont fsVar fhdl emptyRegMap cont $ \_ fhdl' -> do + ptr <- getHandle fhdl' + v <- readBytePointer ptr + sym <- getSym + repr <- getPtrSz + one <- liftIO $ W4.bvLit sym repr (BV.mkBV repr 1) + readBytes <- incHandleRead fhdl' one + valid <- liftIO $ W4.isEq sym one readBytes + return $ mkPE valid v + +-- | Total version of 'readByte' that asserts success. +readByte' :: + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileHandle sym wptr -> + C.OverrideSim p sym arch r args ret (PartExpr (W4.Pred sym) (W4.SymBV sym 8)) +readByte' fsVar fhdl = readByte fsVar fhdl $ \case + Left FileHandleClosed -> + C.ovrWithBackend $ \bak -> + liftIO $ addFailedAssertion bak $ + AssertFailureSimError + "Failed to read byte due to closed file handle." + "readByte': Closed file handle" + Right r -> return r + +-- | Read a chunk from a given 'FileHandle' of the given size, and increment the +-- handle by the size. Returns a struct containing the array contents, and the number +-- of bytes read. +readChunk :: + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileHandle sym wptr -> + W4.SymBV sym wptr -> + (forall args'. Either FileHandleError (DataChunk sym wptr, W4.SymBV sym wptr) -> C.OverrideSim p sym arch r args' ret a) -> + C.OverrideSim p sym arch r args ret a +readChunk fsVar fhdl sz cont = do + W4.BaseBVRepr ptrSz <- return $ W4.exprType sz + let args = RegMap (Empty :> RegEntry (BVRepr ptrSz) sz) + runFileMHandleCont fsVar fhdl args cont $ \(RegMap (Empty :> RegEntry _ sz')) fhdl' -> do + ptr <- getHandle fhdl' + chunk <- readChunkPointer ptr sz' + readSz <- incHandleRead fhdl' sz' + return (chunk, readSz) + +-- | Partial version of 'readArray' that asserts success. +readChunk' :: + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileHandle sym wptr -> + W4.SymBV sym wptr -> + C.OverrideSim p sym arch r args ret (DataChunk sym wptr, W4.SymBV sym wptr) +readChunk' fsVar fhdl sz = readChunk fsVar fhdl sz $ \case + Left FileHandleClosed -> + C.ovrWithBackend $ \bak -> + liftIO $ addFailedAssertion bak $ + AssertFailureSimError + "Failed to read array due to closed file handle." + "readArray': Closed file handle" + Right arr -> return arr + +-- | Returns a predicate indicating whether or not the file handle is still open. +isHandleOpen :: + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileHandle sym wptr -> + C.OverrideSim p sym arch args r ret (W4.Pred sym) +isHandleOpen fvar fhdl = runFileM fvar $ do + sym <- getSym + repr <- getPtrSz + liftOV (C.readMuxTreeRef (MaybeRepr (FilePointerRepr repr)) fhdl) >>= \case + PE p _ -> return p + Unassigned -> return (W4.falsePred sym) + +-- | Return a file handle that is already closed (i.e. any file operations +-- on it will necessarily fail). +invalidFileHandle :: + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + C.OverrideSim p sym arch args r ret (FileHandle sym wptr) +invalidFileHandle fvar = runFileM fvar $ do + repr <- getPtrSz + sym <- getSym + toMuxTree sym <$> (liftOV $ C.newEmptyRef (MaybeRepr (FilePointerRepr repr))) + + +-- | Returns a predicate indicating whether or not the file identifier +-- represents a valid file. +isFileIdentValid :: + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileIdent sym -> + C.OverrideSim p sym arch args r ret (W4.Pred sym) +isFileIdentValid fvar ident = runFileM fvar $ do + sym <- getSym + m <- CMS.gets fsFileNames + case W4.asString ident of + Just (W4.Char8Literal i') + | Right str <- Text.decodeUtf8' i' + -> case Map.lookup str m of + Just _ -> return $ W4.truePred sym + Nothing -> return $ W4.falsePred sym + _ -> return $ W4.falsePred sym + +----------------------------------------- +-- Internal operations + +-- | This internal monad defines a stateful context in which file operations are executed +-- +-- Operations in this monad have full access to the symbolic filesystem (which +-- is normally carried throughout the symbolic execution). +-- +-- Note that most operations actually use 'FileM' instead, which fixes some +-- useful constraints on top of the monad. +newtype FileM_ p arch r args ret sym wptr a = FileM { _unFM :: CMS.StateT (FileSystem sym wptr) (C.OverrideSim p sym arch r args ret) a } + deriving + ( Applicative + , Functor + , Monad + , MonadIO + , CMS.MonadState (FileSystem sym wptr) + ) + +data FileHandleError = FileHandleClosed +data FileIdentError = FileNotFound + +-- | The monad in which all filesystem operations run +type FileM p arch r args ret sym wptr a = + (IsSymInterface sym, 1 <= wptr) => + FileM_ p arch r args ret sym wptr a + +liftOV :: + C.OverrideSim p sym arch r args ret a -> + FileM p arch r args ret sym wptr a +liftOV f = FileM $ CMT.lift f + +-- | Run a 'FileM_' action in the 'C.OverrideSim' monad +-- +-- This extracts the current filesystem state and threads it appropriately +-- through the 'FileM_' monad context. +runFileM :: + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileM_ p arch r args ret sym wptr a -> + C.OverrideSim p sym arch r args ret a +runFileM fvar (FileM f) = do + fs <- C.readGlobal fvar + (a, fs') <- CMS.runStateT f fs + C.writeGlobal fvar fs' + return a + + +runFileMHandleCont :: + forall p sym arch r args args' ret a b wptr. + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileHandle sym wptr -> + RegMap sym args' -> + (forall args''. Either FileHandleError a -> C.OverrideSim p sym arch r (args <+> args'') ret b) -> + (forall args''. RegMap sym args' -> FileHandle sym wptr -> FileM_ p arch r (args <+> args'') ret sym wptr a) -> + C.OverrideSim p sym arch r args ret b +runFileMHandleCont fvar fhdl (RegMap args') cont f = do + fs <- C.readGlobal fvar + p <- isHandleOpen fvar fhdl + sym <- C.getSymInterface + args <- C.getOverrideArgs + let + cont' = cont @(args' ::> FileHandleType wptr) + args'' = RegMap (args' :> RegEntry (FileHandleRepr (fsPtrSize fs)) fhdl) + resultCase :: C.OverrideSim p sym arch r (args <+> (args' ::> FileHandleType wptr)) ret b + resultCase = do + (args_args', RegEntry _ fhdl') <- unconsReg <$> C.getOverrideArgs + let (_, args'_) = splitRegs (regMapSize args) (Ctx.size args') args_args' + a <- runFileM fvar (f @(args' ::> FileHandleType wptr) args'_ fhdl') + cont' (Right a) + + C.symbolicBranches args'' + [(p, resultCase, Nothing) + ,(W4.truePred sym, cont' (Left FileHandleClosed), Nothing) + ] + +splitRegs :: + Ctx.Size ctx -> + Ctx.Size ctx' -> + RegMap sym (ctx <+> ctx') -> + (RegMap sym ctx, RegMap sym ctx') +splitRegs sz sz' (RegMap m) = (RegMap (Ctx.take sz sz' m), RegMap (Ctx.drop sz sz' m)) + +runFileMIdentCont :: + forall p sym arch r args ret a b wptr. + (IsSymInterface sym, 1 <= wptr) => + GlobalVar (FileSystemType wptr) -> + FileIdent sym -> + (forall args'. Either FileIdentError a -> C.OverrideSim p sym arch r (args <+> args') ret b) -> + (forall args'. FileIdent sym -> FileM_ p arch r (args <+> args') ret sym wptr a) -> + C.OverrideSim p sym arch r args ret b +runFileMIdentCont fvar ident cont f = do + p <- isFileIdentValid fvar ident + sym <- C.getSymInterface + let + cont' = cont @(EmptyCtx ::> FileIdentType) + args' = RegMap (Empty :> RegEntry (StringRepr Char8Repr) ident) + resultCase :: C.OverrideSim p sym arch r (args ::> FileIdentType) ret b + resultCase = do + (_, RegEntry _ fhdl') <- unconsReg <$> C.getOverrideArgs + a <- runFileM fvar (f @(EmptyCtx ::> FileIdentType) fhdl') + cont' (Right a) + + C.symbolicBranches args' + [(p, resultCase, Nothing) + ,(W4.truePred sym, cont' (Left FileNotFound), Nothing) + ] + +getSym :: FileM p arch r args ret sym wptr sym +getSym = liftOV C.getSymInterface + +withBackend :: + (forall bak. IsSymBackend sym bak => bak -> FileM p arch r args ret sym wptr a) -> + FileM p arch r args ret sym wptr a +withBackend k = + FileM $ CMS.StateT $ \st -> + C.ovrWithBackend $ \bak -> + CMS.runStateT (_unFM (k bak)) st + +getPtrSz :: FileM p arch r args ret sym wptr (NatRepr wptr) +getPtrSz = CMS.gets fsPtrSize + +-- | Get the (possibly symbolic) size in bytes of the given file +getFileSize :: FileHandle sym wptr -> FileM p arch r args ret sym wptr (W4.SymBV sym wptr) +getFileSize fhdl = do + (FilePointer (File _ fileid) _, _) <- readHandle fhdl + szArray <- CMS.gets fsFileSizes + sym <- getSym + liftIO $ CA.readSingle sym (Ctx.empty Ctx.:> fileid) szArray + +readHandle :: + FileHandle sym wptr -> + FileM p arch r args ret sym wptr (FilePointer sym wptr, W4.Pred sym) +readHandle fhandle = do + repr <- getPtrSz + liftOV (C.readMuxTreeRef (MaybeRepr (FilePointerRepr repr)) fhandle) >>= \case + PE p v -> return (v, p) + Unassigned -> + withBackend $ \bak -> + liftIO $ addFailedAssertion bak $ + AssertFailureSimError + "Read from closed file handle." + "readHandle: Unassigned file handle." + +-- | Retrieve the pointer that the handle is currently at +getHandle :: + FileHandle sym wptr -> + FileM p arch r args ret sym wptr (FilePointer sym wptr) +getHandle fhandle = do + (v, p) <- readHandle fhandle + withBackend $ \bak -> + liftIO $ assert bak p $ + AssertFailureSimError + "Read from closed file handle." + "getHandle: File handle assertion failed." + return v + + +-- | Resolve a file identifier to a 'File' +-- +-- Note that this adds a failing assertion if: +-- +-- - The file does not exist (or the the filename is symbolic) +-- - The filename is malformed (i.e., not utf8) +resolveFileIdent :: + FileIdent sym -> + FileM p arch r args ret sym wptr (File sym wptr) +resolveFileIdent ident = do + m <- CMS.gets fsFileNames + let missingErr = AssertFailureSimError "missing file" + "resolveFileIdent attempted to lookup a file handle that does not exist" + withBackend $ \bak -> + case W4.asString ident of + Just (W4.Char8Literal i') + | Right str <- Text.decodeUtf8' i' + -> case Map.lookup str m of + Just n -> liftIO $ readPartExpr bak n missingErr + Nothing -> liftIO $ addFailedAssertion bak missingErr + _ -> liftIO $ addFailedAssertion bak $ + Unsupported callStack "Unsupported string in resolveFileIdent" + + +openResolvedFile :: + File sym wptr -> + FileM p arch r args ret sym wptr (FileHandle sym wptr) +openResolvedFile file = do + sym <- getSym + repr <- getPtrSz + zero <- liftIO $ W4.bvLit sym repr (BV.mkBV repr 0) + ref <- toMuxTree sym <$> (liftOV $ C.newEmptyRef (MaybeRepr (FilePointerRepr repr))) + setHandle ref (FilePointer file zero) + return ref + +setHandle :: + FileHandle sym wptr -> + FilePointer sym wptr -> + FileM p arch r args ret sym wptr () +setHandle fhandle ptr = do + repr <- getPtrSz + sym <- getSym + let ptr' = justPartExpr sym ptr + liftOV $ C.writeMuxTreeRef (MaybeRepr (FilePointerRepr repr)) fhandle ptr' + +-- | True if the read remains in bounds, if false, the result is the number of +-- bytes that were overrun +bytesOverrun :: + FileHandle sym wptr -> + FilePointer sym wptr -> + FileM p arch r args ret sym wptr (W4.Pred sym, W4.SymBV sym wptr) +bytesOverrun fhandle (FilePointer _ ptrOff) = do + sz <- getFileSize fhandle + sym <- getSym + inbounds <- liftIO $ W4.bvUle sym ptrOff sz + overrun <- liftIO $ W4.bvSub sym ptrOff sz + return $ (inbounds, overrun) + +-- | Increment the filehandle by the number of bytes read, returning the +-- number of bytes that were actually incremented. This is less than +-- the number requested if the read is over the end of the file. +incHandleRead :: + FileHandle sym wptr -> + W4.SymBV sym wptr -> + FileM p arch r args ret sym wptr (W4.SymBV sym wptr) +incHandleRead fhandle sz = do + sym <- getSym + basePtr <- getHandle fhandle + ptr <- addToPointer sz basePtr + (inbounds, overrun) <- bytesOverrun fhandle ptr + off <- liftIO $ W4.bvSub sym sz overrun + readBytes <- liftIO $ W4.baseTypeIte sym inbounds sz off + ptr' <- addToPointer readBytes basePtr + setHandle fhandle ptr' + return readBytes + +-- | Increment the filehandle by the number of bytes written. Currently +-- this is exactly the given value, since writing has no failure cases. +incHandleWrite :: + FileHandle sym wptr -> + W4.SymBV sym wptr -> + FileM p arch r args ret sym wptr (W4.SymBV sym wptr) +incHandleWrite fhandle sz = do + basePtr <- getHandle fhandle + ptr <- addToPointer sz basePtr + setHandle fhandle ptr + updateFileSize fhandle + return sz + +-- | Update the file size of the given file handle if it now points past +-- the end of the file (i.e. after a successful write). +updateFileSize :: + FileHandle sym wptr -> + FileM p arch r args ret sym wptr () +updateFileSize fhdl = do + (FilePointer (File _ fileid) off, _) <- readHandle fhdl + szArray <- CMS.gets fsFileSizes + sym <- getSym + oldsz <- liftIO $ CA.readSingle sym (Ctx.empty Ctx.:> fileid) szArray + szArray' <- liftIO $ CA.writeSingle sym (Ctx.empty Ctx.:> fileid) off szArray + outbounds <- liftIO $ W4.bvUlt sym oldsz off + szArray'' <- liftIO $ CA.muxArrays sym outbounds szArray' szArray + CMS.modify' $ \arr -> arr { fsFileSizes = szArray'' } + +addToPointer :: + W4.SymBV sym wptr -> + FilePointer sym wptr -> + FileM p arch r args ret sym wptr (FilePointer sym wptr) +addToPointer i (FilePointer n off) = do + sym <- getSym + off' <- liftIO $ W4.bvAdd sym off i + return $ FilePointer n off' + + +writeBytePointer :: + FilePointer sym wptr -> + W4.SymBV sym 8 -> + FileM p arch r args ret sym wptr () +writeBytePointer fptr bv = do + let idx = filePointerIdx fptr + sym <- getSym + dataArr <- CMS.gets fsSymData + dataArr' <- liftIO $ CA.writeSingle sym idx bv dataArr + CMS.modify' $ \fs -> fs { fsSymData = dataArr' } + +readBytePointer :: + FilePointer sym wptr -> + FileM p arch r args ret sym wptr (W4.SymBV sym 8) +readBytePointer fptr = do + sym <- getSym + let idx = filePointerIdx fptr + dataArr <- CMS.gets fsSymData + liftIO $ CA.readSingle sym idx dataArr + + +writeChunkPointer :: + FilePointer sym wptr -> + DataChunk sym wptr -> + W4.SymBV sym wptr -> + FileM p arch r args ret sym wptr () +writeChunkPointer fptr chunk sz = do + let idx = filePointerIdx fptr + sym <- getSym + dataArr <- CMS.gets fsSymData + dataArr' <- liftIO $ CA.writeChunk sym idx sz chunk dataArr + CMS.modify' $ \fs -> fs { fsSymData = dataArr' } + + +readChunkPointer :: + FilePointer sym wptr -> + -- | Number of bytes to read + W4.SymBV sym wptr -> + FileM p arch r args ret sym wptr (DataChunk sym wptr) +readChunkPointer fptr sz = do + let idx = filePointerIdx fptr + sym <- getSym + dataArr <- CMS.gets fsSymData + liftIO $ CA.readChunk sym idx sz dataArr + +filePointerIdx :: + IsSymInterface sym => + FilePointer sym wptr -> + FileSystemIndex sym wptr +filePointerIdx (FilePointer (File _ n) off) = Ctx.empty :> off :> n diff --git a/src/Lang/Crucible/SymIO/Loader.hs b/src/Lang/Crucible/SymIO/Loader.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/SymIO/Loader.hs @@ -0,0 +1,179 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +-- | This module defines a default loader for initial symbolic filesystem contents +-- +-- It uses a simple convention to convert on-disk files and metadata into a +-- 'SymIO.InitialFileSystemContents'. This is not the only way to construct +-- initial filesystem contents, but it is a good default if a tool does not have +-- more specific needs. +-- +-- The caller provides a single input: a path to a directory. The directory +-- contains two things: +-- +-- 1. A subdirectory named @root@ that contains the concrete files in the symbolic filesystem (i.e., the directory mapped to @/@) +-- 2. (Optional) A file named @symbolic-manifest.json@, which describes symbolic files and overlays +-- +-- The symbolic manifest specifies the contents of symbolic files, including +-- constraints on symbolic values. Furthermore, it enables users to specify +-- that concrete files in the provided filesystem have symbolic values overlaid +-- over the concrete values. If an overlay is specified in the symbolic +-- manifest, the referenced concrete file /must/ exist. +-- +-- Note: future versions of this interface could support symbolic filesystems +-- stored in zip or tar files. +module Lang.Crucible.SymIO.Loader ( + loadInitialFiles + , FileSystemLoadError(..) + ) where + +import qualified Control.Exception as X +import qualified Data.Aeson as JSON +import qualified Data.ByteString as BS +import qualified Data.Foldable as F +import qualified Data.List as List +import qualified Data.Map.Strict as Map +import Data.Maybe ( fromMaybe ) +import qualified Data.Parameterized.NatRepr as PN +import qualified Data.Text as T +import qualified Data.Traversable as T +import Data.Word ( Word64 ) +import GHC.Generics ( Generic ) +import qualified System.Directory as SD +import System.FilePath ( () ) +import qualified System.FilePath.Find as SFF +import qualified What4.BaseTypes as WT +import qualified What4.Interface as WI + +import qualified Lang.Crucible.Backend as LCB +import qualified Lang.Crucible.SymIO as SymIO + +data FileSystemLoadError = ErrorDecodingJSON String + | forall k . FileSpecifiedAsSymbolicAndConcrete (SymIO.FDTarget k) + +deriving instance Show FileSystemLoadError + +instance X.Exception FileSystemLoadError + +-- | The specification for the symbolic contents of a file in the symbolic +-- filesystem +-- +-- There will be multiple specifications including: +-- +-- * Complete symbolic file specifications (including concrete regions) +-- * Symbolic overlays on otherwise concrete files +data SymbolicFileContents = + SymbolicContents { symbolicContentSize :: Word64 + } + deriving (Show, Generic) + +instance JSON.FromJSON SymbolicFileContents + +-- | A description of the contents of a symbolic filesystem +-- +-- This includes high-level metadata and the specifications for symbolic files. +-- +-- Note that the file paths are /absolute/ paths within the symbolic filesystem +data SymbolicManifest = + SymbolicManifest { symbolicFiles :: [(FilePath, SymbolicFileContents)] + , useStdout :: Bool + , useStderr :: Bool + } + deriving (Show, Generic) + +instance JSON.FromJSON SymbolicManifest + +-- | A file path that is absolute within the symbolic filesystem we are building +newtype AbsolutePath = AbsolutePath FilePath + deriving (Eq, Ord, Show) + +-- | Create an absolute path *within the symbolic filesystem* based on the root +-- FS path and the absolute path to a file in the real filesystem +-- +-- This effectively strips the real root FS off of the absolute file path, +-- creating an absolute path within the symbolic FS. +toInternalAbsolutePath + :: FilePath + -- ^ The path to the root filesystem in the real (non-symbolic) filesystem + -> FilePath + -- ^ The absolute path to the file in the real (non-symbolic) filesystem + -> AbsolutePath +toInternalAbsolutePath pfx x = AbsolutePath (fromMaybe x (List.stripPrefix pfx x)) + +createSymbolicFile + :: (LCB.IsSymInterface sym) + => sym + -> (FilePath, SymbolicFileContents) + -> IO (SymIO.FDTarget SymIO.In, [WI.SymBV sym 8]) +createSymbolicFile sym (internalAbsPath, symContent) = + case symContent of + SymbolicContents { symbolicContentSize = numBytes } -> do + bytes <- T.forM [0.. numBytes - 1] $ \byteNum -> do + let symName = WI.safeSymbol (internalAbsPath ++ "_" ++ show byteNum) + WI.freshConstant sym symName (WT.BaseBVRepr (PN.knownNat @8)) + return (SymIO.FileTarget internalAbsPath, bytes) + +-- | Load the symbolic filesystem at the given file path +-- +-- Note that this will throw an exception if: +-- +-- * The symbolic manifest declares an overlay for a file that does not exist in the concrete portion of the filesystem +loadInitialFiles + :: (LCB.IsSymInterface sym) + => sym + -> FilePath + -> IO (SymIO.InitialFileSystemContents sym) +loadInitialFiles sym fsRoot = do + -- FIXME: Use the lower-level fold primitive that enables exception handling; + -- this version just spews errors to stderr, which is inappropriate. + let concreteFilesRoot = fsRoot "root" + let isRegular = SFF.fileType SFF.==? SFF.RegularFile + concreteFilePaths <- SFF.find SFF.always isRegular concreteFilesRoot + + -- Check if standard input has been specified as a concrete file + let stdinPath = fsRoot T.unpack (SymIO.fdTargetToText SymIO.StdinTarget) + hasStdin <- SD.doesFileExist stdinPath + + -- Note that all of these paths are absolute *if* @fsRoot@ was absolute. + -- Also, if it has leading .. components, they will be included. We need to + -- normalize these paths so that they have @fsRoot@ stripped off (and thus are + -- absolute in the symbolic filesystem) + let relativePaths = [ (p, toInternalAbsolutePath concreteFilesRoot p) + | p <- concreteFilePaths + ] + concFiles <- mapM (\(p, name) -> (name,) <$> BS.readFile p) relativePaths + let concMap0 = Map.fromList [ (SymIO.FileTarget p, bytes) | (AbsolutePath p, bytes) <- concFiles ] + concMap1 <- + if | hasStdin -> do + stdinBytes <- BS.readFile stdinPath + return (Map.insert SymIO.StdinTarget stdinBytes concMap0) + | otherwise -> return concMap0 + + let manifestFilePath = fsRoot "system-manifest.json" + hasManifest <- SD.doesFileExist manifestFilePath + case hasManifest of + False -> + return SymIO.InitialFileSystemContents { SymIO.concreteFiles = concMap1 + , SymIO.symbolicFiles = Map.empty + , SymIO.useStdout = False + , SymIO.useStderr = False + } + True -> do + manifestBytes <- BS.readFile manifestFilePath + case JSON.eitherDecodeStrict manifestBytes of + Left msg -> X.throwIO (ErrorDecodingJSON msg) + Right symManifest -> do + symFiles <- mapM (createSymbolicFile sym) (symbolicFiles symManifest) + F.forM_ symFiles $ \(fdTarget, _) -> do + case Map.lookup fdTarget concMap1 of + Nothing -> return () + Just _ -> X.throwIO (FileSpecifiedAsSymbolicAndConcrete fdTarget) + return SymIO.InitialFileSystemContents { SymIO.concreteFiles = concMap1 + , SymIO.symbolicFiles = Map.fromList symFiles + , SymIO.useStdout = useStdout symManifest + , SymIO.useStderr = useStderr symManifest + } diff --git a/src/Lang/Crucible/SymIO/Types.hs b/src/Lang/Crucible/SymIO/Types.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/SymIO/Types.hs @@ -0,0 +1,224 @@ +----------------------------------------------------------------------- +-- | +-- Module : Lang.Crucible.SymIO.Types +-- Description : Crucible type definitions related to VFS +-- Copyright : (c) Galois, Inc 2020 +-- License : BSD3 +-- Maintainer : Daniel Matichuk +-- Stability : provisional +------------------------------------------------------------------------ + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeApplications #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Lang.Crucible.SymIO.Types + ( symIOIntrinsicTypes + , FilePointer(..) + , FilePointerType + , pattern FilePointerRepr + , FileHandle + , FileHandleType + , pattern FileHandleRepr + , FileIdent + , FileIdentType + , FileSystem(..) + , muxFileSystem + , FileSystemType + , FileSystemIndex + , pattern FileSystemRepr + , File(..) + , pattern FileRepr + , FileType + , muxFile + , DataChunk + , SizedDataChunk + , SizedDataChunkType + ) +where + +import Data.Typeable +import GHC.TypeNats + +import qualified Data.Parameterized.Map as MapF +import Data.Parameterized.Context +import Data.Parameterized.Classes +import Data.Parameterized.NatRepr + +import Lang.Crucible.Backend +import Lang.Crucible.Simulator.RegValue +import Lang.Crucible.Types +import Lang.Crucible.Simulator.Intrinsics + +import What4.Interface +import qualified What4.CachedArray as CA + +-- | The intrinsic types used in the symbolic filesystem +symIOIntrinsicTypes :: IsSymInterface sym => IntrinsicTypes sym +symIOIntrinsicTypes = id + . MapF.insert (knownSymbol :: SymbolRepr "VFS_filesystem") IntrinsicMuxFn + . MapF.insert (knownSymbol :: SymbolRepr "VFS_file") IntrinsicMuxFn + . MapF.insert (knownSymbol :: SymbolRepr "VFS_filepointer") IntrinsicMuxFn + $ MapF.empty + +-- | An identifier for a file, which must be resolved into a 'File' to access +-- the underlying filesystem. +-- +-- This is a file path +type FileIdent sym = RegValue sym FileIdentType + +-- | The crucible-level type of 'FileIdent' +type FileIdentType = StringType Char8 + +-- | The crucible-level type of 'FileSystem' +type FileSystemType w = IntrinsicType "VFS_filesystem" (EmptyCtx ::> BVType w) + +-- | Defines the current state of a symbolic filesystem. +data FileSystem sym w = + FileSystem + { + fsPtrSize :: NatRepr w + , fsFileNames :: RegValue sym (StringMapType (FileType w)) + -- ^ map from concrete file identifiers to files + , fsFileSizes :: CA.CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType w) + -- ^ a symbolic map from files to their size + , fsSymData :: CA.CachedArray sym (EmptyCtx ::> BaseBVType w ::> BaseIntegerType) (BaseBVType 8) + -- ^ array representing symbolic file contents + , fsConstraints :: forall a. ((IsSymInterface sym, 1 <= w) => a) -> a + } + +-- | A base index into the filesystem, consistent of a file identifier and an offset into that file. +type FileSystemIndex sym w = Assignment (SymExpr sym) (EmptyCtx ::> BaseBVType w ::> BaseIntegerType) + +muxFileSystem :: + IsSymInterface sym => + sym -> + Pred sym -> + FileSystem sym w -> + FileSystem sym w -> + IO (FileSystem sym w) +muxFileSystem sym p fsT fsF = do + symData <- CA.muxArrays sym p (fsSymData fsT) (fsSymData fsF) + symFiles <- muxStringMap sym (muxFile sym) p (fsFileNames fsT) (fsFileNames fsF) + symFileSizes <- CA.muxArrays sym p (fsFileSizes fsT) (fsFileSizes fsF) + return $ fsT { fsSymData = symData, fsFileNames = symFiles, fsFileSizes = symFileSizes } + +instance (IsSymInterface sym) => IntrinsicClass sym "VFS_filesystem" where + type Intrinsic sym "VFS_filesystem" (EmptyCtx ::> BVType w) = FileSystem sym w + + muxIntrinsic sym _iTypes _nm (Empty :> (BVRepr _w)) = muxFileSystem sym + muxIntrinsic _ _ nm ctx = \_ _ _ -> typeError nm ctx + +pattern FileSystemRepr :: () => (1 <= w, ty ~ FileSystemType w) => NatRepr w -> TypeRepr ty +pattern FileSystemRepr w <- IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "VFS_filesystem") -> Just Refl) + (Empty :> BVRepr w) + where + FileSystemRepr w = IntrinsicRepr knownSymbol (Empty :> BVRepr w) + +-- | The crucible type of file handles. +type FileHandleType w = ReferenceType (MaybeType (FilePointerType w)) + +-- | A file handle is a mutable file pointer that increments every time it is read. +type FileHandle sym w = RegValue sym (FileHandleType w) + +-- | A 'File' represents a file in the filesystem independent +-- of any open handles to it +-- +-- The 'NatRepr' records the size of file pointers (in bits) +-- +-- The 'SymInteger' is an index into the underlying array of arrays that represents file contents +data File sym w = File (NatRepr w) (SymInteger sym) + +pattern FileRepr :: () => (1 <= w, ty ~ FileType w) => NatRepr w -> TypeRepr ty +pattern FileRepr w <- IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "VFS_file") -> Just Refl) + (Empty :> BVRepr w) + where + FileRepr w = IntrinsicRepr knownSymbol (Empty :> BVRepr w) + +-- | The crucible-level type of 'File' +type FileType w = IntrinsicType "VFS_file" (EmptyCtx ::> BVType w) + +instance (IsSymInterface sym) => IntrinsicClass sym "VFS_file" where + type Intrinsic sym "VFS_file" (EmptyCtx ::> BVType w) = File sym w + + muxIntrinsic sym _iTypes _nm (Empty :> BVRepr _w) = muxFile sym + muxIntrinsic _ _ nm ctx = typeError nm ctx + +muxFile :: + IsSymInterface sym => + sym -> + Pred sym -> + File sym w -> + File sym w -> + IO (File sym w) +muxFile sym p (File w f1) (File _w f2) = File w <$> baseTypeIte sym p f1 f2 + +-- | A file pointer represents an index into a particular file. +-- +-- The 'File' is similar to an inode, and uniquely identifies a file (as an +-- index into the array of all files). The 'SymBV' is the offset into the file +-- that the file pointer is currently at (i.e., where the next read or write +-- will be from). +data FilePointer sym w = + FilePointer (File sym w) (SymBV sym w) + +-- | The crucible type of 'FilePointer' +type FilePointerType w = IntrinsicType "VFS_filepointer" (EmptyCtx ::> BVType w) + +instance (IsSymInterface sym) => IntrinsicClass sym "VFS_filepointer" where + type Intrinsic sym "VFS_filepointer" (EmptyCtx ::> BVType w) = FilePointer sym w + + muxIntrinsic sym _iTypes _nm (Empty :> (BVRepr _w)) = muxFilePointer sym + muxIntrinsic _ _ nm ctx = typeError nm ctx + +-- | Mux on 'FilePointer' +muxFilePointer :: + (1 <= w) => + IsSymInterface sym => + sym -> + Pred sym -> + FilePointer sym w -> + FilePointer sym w -> + IO (FilePointer sym w) +muxFilePointer sym p (FilePointer f1 off1) (FilePointer f2 off2) = + do b <- muxFile sym p f1 f2 + off <- bvIte sym p off1 off2 + return $ FilePointer b off + + +type DataChunk sym w = CA.ArrayChunk sym (BaseBVType w) (BaseBVType 8) + +type SizedDataChunkType w = SymbolicStructType (EmptyCtx ::> BaseArrayType (EmptyCtx ::> BaseBVType w) (BaseBVType 8) ::> BaseBVType w) +type SizedDataChunk sym w = SymStruct sym (EmptyCtx ::> BaseArrayType (EmptyCtx ::> BaseBVType w) (BaseBVType 8) ::> BaseBVType w) + +-- | A file handle is a reference to an optional file pointer +-- +-- If the file pointer is not present, the file handle is closed. Otherwise, the +-- file pointer is the current pointer into the file (i.e., that will be read +-- from or written to next). +-- +-- Note that this is just the repr and the real file handle value is symbolic +-- and stored in a Crucible reference. +pattern FileHandleRepr :: () => (1 <= w, ty ~ FileHandleType w) => NatRepr w -> TypeRepr ty +pattern FileHandleRepr w = ReferenceRepr (MaybeRepr (FilePointerRepr w)) + +pattern FilePointerRepr :: () => (1 <= w, ty ~ FilePointerType w) => NatRepr w -> TypeRepr ty +pattern FilePointerRepr w <- IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "VFS_filepointer") -> Just Refl) + (Empty :> BVRepr w) + where + FilePointerRepr w = IntrinsicRepr knownSymbol (Empty :> BVRepr w) + + + diff --git a/src/What4/CachedArray.hs b/src/What4/CachedArray.hs new file mode 100644 --- /dev/null +++ b/src/What4/CachedArray.hs @@ -0,0 +1,850 @@ +----------------------------------------------------------------------- +-- | +-- Module : What4.CachedArray +-- Description : What4 array storage with a concrete backing supporting symbolic indexes +-- Copyright : (c) Galois, Inc 2020 +-- License : BSD3 +-- Maintainer : Daniel Matichuk +-- Stability : provisional +-- +-- +-- This module provides a storage structure that supports arrays that have reads +-- from and writes to a mix of concrete and symbolic indexes. It can be thought +-- of as a multi-dimensional array that supports reading and writing contiguous +-- "chunks". It is built on the 'Data.Parameterized.IntervalsMap' structure, +-- which computes an abstract domain over indexes (supporting symbolic +-- reads/writes). +------------------------------------------------------------------------ + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE FlexibleInstances, FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE UndecidableInstances #-} + +module What4.CachedArray + ( + CachedArray + , ArrayChunk + , mkArrayChunk + , evalChunk + , writeChunk + , writeSingle + , readSingle + , readChunk + , arrayToChunk + , chunkToArray + , muxArrays + , initArrayConcrete + , initArray + ) where + +import Control.Lens ( (.~), (&) ) +import Control.Monad ( foldM, join ) +import Control.Monad.Trans ( lift ) +import Data.Functor.Const +import Data.Maybe ( catMaybes ) +import qualified Data.Map as Map +import Data.Maybe (mapMaybe) +import qualified Data.IORef as IO + +import qualified Data.Parameterized.TraversableFC as FC +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.Classes +import Data.Parameterized.NatRepr ( type (<=) ) +import qualified Data.Parameterized.Nonce as PN +import qualified Data.BitVector.Sized as BV + +import qualified Lang.Crucible.Utils.MuxTree as MT + +import qualified What4.Interface as W4 +import qualified What4.Partial as W4 +import qualified What4.Concrete as W4 +import qualified What4.Utils.AbstractDomains as W4 +import qualified What4.Utils.BVDomain as BVD + +import qualified Data.Parameterized.IntervalsMap as IM +import Data.Parameterized.IntervalsMap ( AsOrd(..) ) + +------------------------------------------------ +-- Interface + +-- TODO: add coalescing function for merging adjacent entries + +newtype ArrayChunk sym idx tp = + ArrayChunk { evalChunk :: (W4.SymExpr sym idx -> IO (W4.SymExpr sym tp)) } + +mkArrayChunk :: + forall sym idx tp. + W4.IsSymExprBuilder sym => + sym -> + (W4.SymExpr sym idx -> IO (W4.SymExpr sym tp)) -> + IO (ArrayChunk sym idx tp) +mkArrayChunk _sym f = do + ref <- IO.newIORef Map.empty + let f' idx = do + m <- IO.readIORef ref + case Map.lookup (AsOrd idx) m of + Just v -> return v + Nothing -> do + v <- f idx + IO.modifyIORef ref (Map.insert (AsOrd idx) v) + return v + return $ ArrayChunk f' + +writeChunk :: + forall sym ctx tp. + NonEmptyCtx ctx => + W4.IsSymExprBuilder sym => + sym -> + -- | base address to write to + Ctx.Assignment (W4.SymExpr sym) ctx -> + -- | size of write + W4.SymExpr sym (CtxFirst ctx) -> + -- | symbolic value to write + ArrayChunk sym (CtxFirst ctx) tp -> + CachedArray sym ctx tp -> + IO (CachedArray sym ctx tp) +writeChunk sym loExpr offExpr chunk arr | NonEmptyCtxRepr <- nonEmptyCtxRepr @_ @ctx = + arrConstraints arr $ do + rng <- mkSymRangeOff sym loExpr offExpr + arr' <- invalidateEntries sym rng arr + -- offset the incoming function so that its value at zero becomes the value at + -- the base address + let + off = indexToOffset $ symRangeLo rng + vals :: SymIndex sym ctx -> IO (W4.PartExpr (W4.Pred sym) (W4.SymExpr sym tp)) + vals idx' = do + p <- isInRange sym rng idx' + (SymOffset idxOffsetExpr) <- indexToOffset <$> subSymOffset sym idx' off + v <- evalChunk chunk idxOffsetExpr + return $ W4.mkPE p v + entry <- mkMultiEntry vals + arr'' <- IM.insertWithM (mergeEntriesMux sym (isInRange sym rng)) (symRangeToAbs rng) (toPMuxTree sym entry) (arrMap arr') + incNonce $ arr { arrMap = arr''} + + +writeSingle :: + forall sym ctx tp. + W4.IsSymExprBuilder sym => + sym -> + Ctx.Assignment (W4.SymExpr sym) ctx -> + W4.SymExpr sym tp -> + CachedArray sym ctx tp -> + IO (CachedArray sym ctx tp) +writeSingle sym symIdxExpr val arr = arrConstraints arr $ do + arr' <- invalidateEntries sym (SymRangeSingle symIdx) arr + entry <- mkValEntry sym symIdx val + + arr'' <- IM.insertWithM (mergeEntriesMux sym (isEqIndex sym symIdx)) (symIdxToAbs symIdx) (toPMuxTree sym entry) (arrMap arr') + incNonce $ arr { arrMap = arr'' } + where + symIdx = mkSymIndex symIdxExpr + + +readSingle :: + forall sym idx tp. + W4.IsSymExprBuilder sym => + sym -> + Ctx.Assignment (W4.SymExpr sym) idx -> + CachedArray sym idx tp -> + IO (W4.SymExpr sym tp) +readSingle sym symIdxExpr arr = readArrayBase sym symIdx arr + where + symIdx = SymIndex symIdxExpr Nothing + +readChunk :: + forall sym ctx tp. + NonEmptyCtx ctx => + W4.IsSymExprBuilder sym => + sym -> + -- | base address to read from + Ctx.Assignment (W4.SymExpr sym) ctx -> + -- | size of read + W4.SymExpr sym (CtxFirst ctx) -> + CachedArray sym ctx tp -> + IO (ArrayChunk sym (CtxFirst ctx) tp) +readChunk sym loExpr offExpr arr | NonEmptyCtxRepr <- nonEmptyCtxRepr @_ @ctx = do + rng <- mkSymRangeOff sym loExpr offExpr + let absIdx = symRangeToAbs rng + -- offset the outgoing array so that its value at zero is the value at + -- the base address + return $ ArrayChunk $ \idxExpr -> do + let off = SymOffset idxExpr + offsetIdx <- addSymOffset sym (symRangeLo rng) off + readArrayBase sym (offsetIdx { symIdxAbs = Just absIdx}) arr + +chunkToArray :: + forall sym idx tp. + W4.IsSymExprBuilder sym => + sym -> + W4.BaseTypeRepr idx -> + ArrayChunk sym idx tp -> + IO (W4.SymArray sym (Ctx.EmptyCtx Ctx.::> idx) tp) +chunkToArray sym repr chunk = do + var <- W4.freshBoundVar sym W4.emptySymbol repr + body <- evalChunk chunk (W4.varExpr sym var) + fn <- W4.definedFn sym (W4.safeSymbol "readRange") (Ctx.empty Ctx.:> var) body W4.AlwaysUnfold + W4.arrayFromFn sym fn + +arrayToChunk :: + forall sym idx tp. + W4.IsSymExprBuilder sym => + sym -> + (W4.SymArray sym (Ctx.EmptyCtx Ctx.::> idx) tp) -> + IO (ArrayChunk sym idx tp) +arrayToChunk sym arr = mkArrayChunk sym $ \idx -> W4.arrayLookup sym arr (Ctx.empty Ctx.:> idx) + + +muxArrays :: + forall sym idx tp. + W4.IsSymExprBuilder sym => + sym -> + W4.Pred sym -> + CachedArray sym idx tp -> + CachedArray sym idx tp -> + IO (CachedArray sym idx tp) +muxArrays sym p arr1 arr2 = case arr1 == arr2 of + True -> return arr1 + False -> arrConstraints arr1 $ do + notp <- W4.notPred sym p + arr' <- IM.mergeWithM + (pmuxTreeAddCondition sym p) + (pmuxTreeAddCondition sym notp) + (muxEntries sym p) + (arrMap arr1) + (arrMap arr2) + incNonce $ arr1 { arrMap = arr' } + +-- | Initialize an array with symbolic contents at concrete locations +initArrayConcrete :: + forall sym idx tp idx' tp'. + W4.IsSymExprBuilder sym => + idx ~ (idx' Ctx.::> tp') => + sym -> + W4.BaseTypeRepr tp -> + [(Ctx.Assignment W4.ConcreteVal idx, W4.SymExpr sym tp)] -> + IO (CachedArray sym idx tp) +initArrayConcrete sym repr m = do + nonce <- freshArrayNonce + im <- IM.fromList <$> mapM go m + return $ CachedArray im (\x -> x) repr nonce + where + go :: + (Ctx.Assignment W4.ConcreteVal idx, W4.SymExpr sym tp) -> + IO (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp)) + go (cidx, v) = do + symIdx <- concreteIdxToSym sym cidx + entry <- mkValEntry sym symIdx v + return $ (symIdxToAbs symIdx, toPMuxTree sym entry) + +-- | Initialize an array with symbolic contents at symbolic locations +initArray :: + forall sym idx tp idx' tp'. + W4.IsSymExprBuilder sym => + idx ~ (idx' Ctx.::> tp') => + sym -> + W4.BaseTypeRepr tp -> + [(Ctx.Assignment (W4.SymExpr sym) idx, W4.SymExpr sym tp)] -> + IO (CachedArray sym idx tp) +initArray sym repr m = do + nonce <- freshArrayNonce + im <- IM.fromList <$> mapM go m + return $ CachedArray im (\x -> x) repr nonce + where + go :: + (Ctx.Assignment (W4.SymExpr sym) idx, W4.SymExpr sym tp) -> + IO (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp)) + go (symIdxExpr, v) = do + let + symIdx = SymIndex symIdxExpr Nothing + entry <- mkValEntry sym symIdx v + return $ (symIdxToAbs symIdx, toPMuxTree sym entry) + +--------------------------------------------------- +-- Implementation + +-- | A sentinel nonce that is refreshed every time the array is updated. +newtype ArrayNonce = ArrayNonce (PN.Nonce PN.GlobalNonceGenerator IO) + +instance Eq ArrayNonce where + (ArrayNonce i1) == (ArrayNonce i2) | Just Refl <- testEquality i1 i2 = True + _ == _ = False + +instance Ord ArrayNonce where + compare (ArrayNonce i1) (ArrayNonce i2) = toOrdering $ compareF i1 i2 + +freshArrayNonce :: IO ArrayNonce +freshArrayNonce = ArrayNonce <$> PN.freshNonce PN.globalNonceGenerator + +-- | An array that supports reading from a stack of mixed concrete/symbolic writes efficiently. +-- +-- The primary interface is intended to be 'readChunk' and 'writeChunk', which +-- allow writing contiguous subsequences of data to the array. +-- +-- Note that the equality instances is based on a unique nonce (see +-- 'ArrayNonce') that is incremented each time the array is updated, and is thus +-- an identity test rather than a structural equality test. +data CachedArray sym (ctx :: Ctx.Ctx W4.BaseType) (tp :: W4.BaseType) where + CachedArray :: + { + arrMap :: IM.IntervalsMap AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp)) + , arrConstraints :: forall a. (NonEmptyCtx ctx => a) -> a + , arrTypeRepr :: W4.BaseTypeRepr tp + , _arrNonce :: ArrayNonce + } -> CachedArray sym ctx tp + +instance Eq (CachedArray sym idx tp) where + (CachedArray _ _ _ nonce1) == (CachedArray _ _ _ nonce2) = nonce1 == nonce2 + +incNonce :: + CachedArray sym idx tp -> + IO (CachedArray sym idx tp) +incNonce (CachedArray am ac tr _) = do + nonce <- freshArrayNonce + return $ CachedArray am ac tr nonce + +-- | An array entry defines a set of possible values for a given +-- abstract domain. Entries may overlap, and so as an invariant we +-- preserve the fact that at each logical index, exactly one entry is valid +data ArrayEntry sym ctx tp where + ArrayEntry :: + { -- TODO: should we cache these results? + entryVals :: (SymIndex sym ctx -> IO (W4.PartExpr (W4.Pred sym) (W4.SymExpr sym tp))) + , entryNonce :: ArrayNonce + } -> ArrayEntry sym ctx tp + + +incNonceEntry :: + ArrayEntry sym ctx tp -> + IO (ArrayEntry sym ctx tp) +incNonceEntry (ArrayEntry vals _) = do + nonce <- freshArrayNonce + return $ ArrayEntry vals nonce + +instance Eq (ArrayEntry sym ctx tp) where + e1 == e2 = entryNonce e1 == entryNonce e2 + +instance Ord (ArrayEntry sym ctx tp) where + compare e1 e2 = compare (entryNonce e1) (entryNonce e2) + +-- | A symbolic index into the array. It represents the index for a single array element, +-- although its value may be symbolic +data SymIndex sym ctx = + SymIndex + { -- | the symbolic index + _symIdxExpr :: Ctx.Assignment (W4.SymExpr sym) ctx + -- | an optional override for the abstract domain of the index + , symIdxAbs :: Maybe (AbsIndex ctx) + } + +deriving instance W4.IsSymExprBuilder sym => Eq (SymIndex sym ctx) +deriving instance W4.IsSymExprBuilder sym => Ord (SymIndex sym ctx) + +-- | An offset is an index into the last element of the array index +-- A value range is always representable as a base + offset +newtype SymOffset sym ctx where + SymOffset :: W4.SymExpr sym (CtxFirst ctx) -> SymOffset sym ctx + +newtype FirstIndex ctx where + FirstIndex :: Ctx.Index ctx (CtxFirst ctx) -> FirstIndex ctx + +skipFirst :: + FirstIndex (ctx Ctx.::> tp1) -> FirstIndex (ctx Ctx.::> tp1 Ctx.::> tp2) +skipFirst (FirstIndex idx) = FirstIndex (Ctx.skipIndex idx) + +firstIndex :: + forall ctx. + NonEmptyCtx ctx => + Ctx.Size ctx -> + FirstIndex ctx +firstIndex sz | NonEmptyCtxRepr <- nonEmptyCtxRepr @_ @ctx = + case Ctx.viewSize (Ctx.decSize sz) of + Ctx.ZeroSize -> FirstIndex (Ctx.baseIndex) + Ctx.IncSize _ -> skipFirst (firstIndex (Ctx.decSize sz)) + +indexToOffset :: + forall sym ctx. + NonEmptyCtx ctx => + W4.IsSymExprBuilder sym => + SymIndex sym ctx -> + SymOffset sym ctx +indexToOffset (SymIndex eCtx _) = + let + FirstIndex idx = firstIndex (Ctx.size eCtx) + e = eCtx Ctx.! idx + in SymOffset e + +addSymOffset :: + forall sym ctx. + W4.IsSymExprBuilder sym => + NonEmptyCtx ctx => + sym -> + SymIndex sym ctx -> + SymOffset sym ctx -> + IO (SymIndex sym ctx) +addSymOffset sym (SymIndex eCtx _) (SymOffset off) = do + let + FirstIndex idx = firstIndex (Ctx.size eCtx) + e = eCtx Ctx.! idx + e' <- case W4.exprType off of + W4.BaseIntegerRepr -> W4.intAdd sym e off + W4.BaseBVRepr _ -> W4.bvAdd sym e off + _ -> fail $ "Unsupported type" + return $ SymIndex (eCtx & (ixF idx) .~ e') Nothing + +negateSymOffset :: + W4.IsSymExprBuilder sym => + sym -> + SymOffset sym ctx -> + IO (SymOffset sym ctx) +negateSymOffset sym (SymOffset off) = do + e' <- case W4.exprType off of + W4.BaseIntegerRepr -> W4.intNeg sym off + W4.BaseBVRepr _ -> W4.bvNeg sym off + _ -> fail $ "Unsupported type" + return $ SymOffset e' + +-- | Previous offset from the given one, to create an exclusive upper bound +prevSymOffset :: + W4.IsSymExprBuilder sym => + sym -> + SymOffset sym ctx -> + IO (SymOffset sym ctx) +prevSymOffset sym (SymOffset off) = do + e' <- case W4.exprType off of + W4.BaseIntegerRepr -> do + one <- W4.intLit sym 1 + W4.intSub sym off one + W4.BaseBVRepr w -> do + one <- W4.bvLit sym w (BV.mkBV w 1) + W4.bvSub sym off one + _ -> fail $ "Unsupported type" + return $ SymOffset e' + +subSymOffset :: + W4.IsSymExprBuilder sym => + NonEmptyCtx ctx => + sym -> + SymIndex sym ctx -> + SymOffset sym ctx -> + IO (SymIndex sym ctx) +subSymOffset sym idx off = do + negoff <- negateSymOffset sym off + addSymOffset sym idx negoff + +mkSymIndex :: + forall sym ctx. + Ctx.Assignment (W4.SymExpr sym) ctx -> + SymIndex sym ctx +mkSymIndex e = SymIndex e Nothing + +-- | Represents a symbolic range, where equality and ordering is defined on the +-- abstract domain of the underlying expression +data SymRange sym ctx = + SymRangeSingle (SymIndex sym ctx) + | SymRangeMulti (SymIndex sym ctx) (SymIndex sym ctx) + +symRangeLo :: SymRange sym ctx -> SymIndex sym ctx +symRangeLo (SymRangeSingle symIdx) = symIdx +symRangeLo (SymRangeMulti loIdx _) = loIdx + + +symRangeToAbs :: + W4.IsSymExprBuilder sym => + SymRange sym ctx -> + AbsIndex ctx +symRangeToAbs (SymRangeSingle symIdx) = symIdxToAbs symIdx +symRangeToAbs (SymRangeMulti loIdx hiIdx) = + joinAbsIndex (symIdxToAbs loIdx) (symIdxToAbs hiIdx) + + +-- | Create a range that is exclusive of the given offset +-- i.e. 2 + 4 --> (2, 5) +mkSymRangeOff :: + forall sym ctx . + W4.IsSymExprBuilder sym => + NonEmptyCtx ctx => + sym -> + Ctx.Assignment (W4.SymExpr sym) ctx -> + W4.SymExpr sym (CtxFirst ctx) -> + IO (SymRange sym ctx) +mkSymRangeOff sym loExpr offExpr = do + let + lo = mkSymIndex @sym loExpr + off = SymOffset offExpr + offPrev <- prevSymOffset sym off + hi <- addSymOffset sym lo offPrev + return $ (SymRangeMulti lo hi) + +data NonEmptyCtxRepr (ctx :: Ctx.Ctx k) where + NonEmptyCtxRepr :: NonEmptyCtxRepr (ctx Ctx.::> x) + +type family CtxFirst (ctx :: Ctx.Ctx k) where + CtxFirst (Ctx.EmptyCtx Ctx.::> a) = a + CtxFirst (ctx Ctx.::> _) = CtxFirst ctx + +class NonEmptyCtx (ctx :: Ctx.Ctx k) where + type CtxHead ctx :: k + type CtxTail ctx :: Ctx.Ctx k + + nonEmptyCtxRepr :: NonEmptyCtxRepr ctx + +instance NonEmptyCtx (ctx Ctx.::> tp) where + type CtxHead (ctx Ctx.::> tp) = tp + type CtxTail (ctx Ctx.::> tp) = ctx + nonEmptyCtxRepr = NonEmptyCtxRepr + +data AbsIntervalEnd tp where + AbsIntervalEndInt :: W4.ValueBound Integer -> AbsIntervalEnd W4.BaseIntegerType + AbsIntervalEndBV :: (1 <= w) => W4.NatRepr w -> W4.ValueBound Integer -> AbsIntervalEnd (W4.BaseBVType w) + +instance Ord (AbsIntervalEnd tp) where + compare a1 a2 = toOrdering $ compareF a1 a2 + +instance Eq (AbsIntervalEnd tp) where + a1 == a2 = (compare a1 a2) == EQ + +instance TestEquality AbsIntervalEnd where + testEquality a1 a2 = case compareF a1 a2 of + EQF -> Just Refl + _ -> Nothing + +instance OrdF AbsIntervalEnd where + compareF a1 a2 = case (a1, a2) of + (AbsIntervalEndInt n1, AbsIntervalEndInt n2) -> fromOrdering $ compare n1 n2 + (AbsIntervalEndBV w1 i1, AbsIntervalEndBV w2 i2) -> + lexCompareF w1 w2 $ fromOrdering $ compare i1 i2 + (AbsIntervalEndInt{}, AbsIntervalEndBV{}) -> LTF + (AbsIntervalEndBV{}, AbsIntervalEndInt{}) -> GTF + + +type AbsIndex (idx :: Ctx.Ctx W4.BaseType) = IM.Intervals AbsIntervalEnd idx +type AbsInterval tp = IM.IntervalF AbsIntervalEnd tp + + +bvDomainRange :: + 1 <= w => + W4.NatRepr w -> + BVD.BVDomain w -> + AbsInterval (W4.BaseBVType w) +bvDomainRange w d = case BVD.ubounds d of + (i1, i2) -> IM.mkIntervalF $ IM.ClosedInterval (AbsIntervalEndBV w (W4.Inclusive i1)) (AbsIntervalEndBV w (W4.Inclusive i2)) + +exprToAbsInterval :: + forall sym tp. + W4.IsSymExprBuilder sym => + W4.SymExpr sym tp -> + AbsInterval tp +exprToAbsInterval e = absToInterval (W4.exprType e) (W4.getAbsValue e) + +absToInterval :: + W4.BaseTypeRepr tp -> + W4.AbstractValue tp -> + AbsInterval tp +absToInterval repr v = case repr of + W4.BaseIntegerRepr -> case v of + W4.SingleRange x -> IM.mkIntervalF $ IM.ClosedInterval (AbsIntervalEndInt (W4.Inclusive x)) (AbsIntervalEndInt (W4.Inclusive x)) + W4.MultiRange lo hi -> IM.mkIntervalF $ IM.ClosedInterval (AbsIntervalEndInt lo) (AbsIntervalEndInt hi) + W4.BaseBVRepr w -> bvDomainRange w v + _ -> error "Unsupported type" + + +readArrayBase :: + forall sym idx tp. + W4.IsSymExprBuilder sym => + sym -> + SymIndex sym idx -> + CachedArray sym idx tp -> + IO (W4.SymExpr sym tp) +readArrayBase sym symIdx arr = do + let + intersecting = IM.toList $ IM.intersecting (arrMap arr) (symIdxToAbs symIdx) + entries <- mapM expandEntry $ concat $ map (viewPMuxTree . snd) intersecting + case entries of + [(W4.PE p (AsOrd e), path_cond)] + | Just True <- W4.asConstantPred path_cond + , Just True <- W4.asConstantPred p -> return e + entryExprs -> arrConstraints arr $ do + + muxTree <- mkPMuxTreePartial sym entryExprs + MT.collapseMuxTree sym ite muxTree >>= \case + Just (AsOrd e) -> return e + -- garbage result + Nothing -> W4.freshConstant sym W4.emptySymbol (arrTypeRepr arr) + + where + ite :: + W4.Pred sym -> + Maybe (AsOrd (W4.SymExpr sym) tp) -> + Maybe (AsOrd (W4.SymExpr sym) tp) -> + IO (Maybe (AsOrd (W4.SymExpr sym) tp)) + ite p (Just (AsOrd e1)) (Just (AsOrd e2)) = (Just . AsOrd) <$> W4.baseTypeIte sym p e1 e2 + ite _ Nothing (Just e2) = return $ Just e2 + ite _ (Just e1) Nothing = return $ Just e1 + ite _ Nothing Nothing = return Nothing + + expandEntry :: + (ArrayEntry sym idx tp, W4.Pred sym) -> + IO (W4.PartExpr (W4.Pred sym) (AsOrd (W4.SymExpr sym) tp), W4.Pred sym) + expandEntry (entry, path_cond) = do + val <- entryVals entry symIdx + return $ (fmap AsOrd val, path_cond) + +mkValEntry :: + W4.IsSymExprBuilder sym => + sym -> + SymIndex sym ctx -> + W4.SymExpr sym tp -> + IO (ArrayEntry sym ctx tp) +mkValEntry sym idx v = do + let vals idx' = do + p <- isEqIndex sym idx idx' + return $ W4.mkPE p v + mkMultiEntry vals + +mkMultiEntry :: + (SymIndex sym ctx -> IO (W4.PartExpr (W4.Pred sym) (W4.SymExpr sym tp))) -> + IO (ArrayEntry sym ctx tp) +mkMultiEntry vals = do + nonce <- freshArrayNonce + return $ ArrayEntry vals nonce + +symIdxToAbs :: + forall sym ctx. + W4.IsSymExprBuilder sym => + SymIndex sym ctx -> AbsIndex ctx +symIdxToAbs (SymIndex symIdxExpr Nothing) = IM.Intervals $ FC.fmapFC (exprToAbsInterval @sym) symIdxExpr +symIdxToAbs (SymIndex _ (Just absIdx)) = absIdx + +concreteIdxToSym :: + forall sym ctx. + W4.IsSymExprBuilder sym => + sym -> + Ctx.Assignment W4.ConcreteVal ctx -> + IO (SymIndex sym ctx) +concreteIdxToSym sym conc = do + symIdxExpr <- FC.traverseFC (W4.concreteToSym sym) conc + return $ SymIndex symIdxExpr Nothing + + +-- | Invalidate all entries within the given range +-- TODO: delete entries which are statically invalid +invalidateRange :: + forall sym ctx tp. + W4.IsSymExprBuilder sym => + sym -> + -- | range to invalidate + SymRange sym ctx -> + ArrayEntry sym ctx tp -> + IO (Maybe (ArrayEntry sym ctx tp)) +invalidateRange sym invalid_rng entry = do + let vals symIdx' = do + notThis <- W4.notPred sym =<< isInRange sym invalid_rng symIdx' + val <- entryVals entry symIdx' + W4.runPartialT sym notThis $ W4.returnPartial val + entry' <- incNonceEntry $ entry { entryVals = vals } + return $ Just entry' + + +isInRange :: + forall sym ctx. + W4.IsSymExprBuilder sym => + sym -> + SymRange sym ctx -> + SymIndex sym ctx -> + IO (W4.Pred sym) +isInRange sym rng symIdx2@(SymIndex symIdxExpr _) = case rng of + SymRangeSingle symIdx1 -> isEqIndex sym symIdx1 symIdx2 + SymRangeMulti (SymIndex loIdxExpr _) (SymIndex hiIdxExpr _) -> do + lo <- FC.toListFC getConst <$> Ctx.zipWithM doLe loIdxExpr symIdxExpr + hi <- FC.toListFC getConst <$> Ctx.zipWithM doLe symIdxExpr hiIdxExpr + foldM (W4.andPred sym) (W4.truePred sym) $ lo ++ hi + where + doLe :: + forall tp. + W4.SymExpr sym tp -> + W4.SymExpr sym tp -> + IO (Const (W4.Pred sym) tp) + doLe e1 e2 = Const <$> case W4.exprType e1 of + W4.BaseBVRepr _ -> W4.bvUle sym e1 e2 + W4.BaseIntegerRepr -> W4.intLe sym e1 e2 + _ -> fail "isInRange: unsupported type" + +isEqIndex :: + forall sym ctx. + W4.IsSymExprBuilder sym => + sym -> + SymIndex sym ctx -> + SymIndex sym ctx -> + IO (W4.Pred sym) +isEqIndex sym (SymIndex symIdxExpr1 _) (SymIndex symIdxExpr2 _) = do + preds <- FC.toListFC getConst <$> Ctx.zipWithM (\e1 e2 -> Const <$> W4.isEq sym e1 e2) symIdxExpr1 symIdxExpr2 + foldM (W4.andPred sym) (W4.truePred sym) preds + +-- | Invalidate all existing symbolic entries at exactly this index +invalidateEntries :: + forall sym ctx tp. + W4.IsSymExprBuilder sym => + sym -> + SymRange sym ctx -> + CachedArray sym ctx tp -> + IO (CachedArray sym ctx tp) +invalidateEntries sym symRange arr = arrConstraints arr $ do + NonEmptyCtxRepr <- return $ nonEmptyCtxRepr @_ @ctx + cmap <- IM.mapMIntersecting absIndex (\v -> getMaybe <$> pmuxTreeMaybeOp sym (invalidateRange sym symRange) v) (arrMap arr) + return $ arr { arrMap = cmap } + where + absIndex = symRangeToAbs symRange + getMaybe :: PMuxTree sym (ArrayEntry sym ctx tp) -> Maybe (PMuxTree sym (ArrayEntry sym ctx tp)) + getMaybe mt | isEmptyPMuxTree mt = Nothing + getMaybe mt = Just mt + +buildMuxTree :: (W4.IsExprBuilder sym, Ord a) => sym -> a -> [(a, W4.Pred sym)] -> IO (MT.MuxTree sym a) +buildMuxTree sym a as = + foldM (\mt (a',p) -> MT.mergeMuxTree sym p (MT.toMuxTree sym a') mt) (MT.toMuxTree sym a) as + + +joinAbsIndex :: + AbsIndex ctx -> + AbsIndex ctx -> + AbsIndex ctx +joinAbsIndex (IM.Intervals idx1) (IM.Intervals idx2) = IM.Intervals $ Ctx.zipWith IM.mergeIntervalsF idx1 idx2 + + +muxEntries :: + W4.IsSymExprBuilder sym => + sym -> + W4.Pred sym -> + PMuxTree sym (ArrayEntry sym ctx tp) -> + PMuxTree sym (ArrayEntry sym ctx tp) -> + IO (PMuxTree sym (ArrayEntry sym ctx tp)) +muxEntries sym p mtT mtF = MT.mergeMuxTree sym p mtT mtF + +mergeEntries :: + forall sym ctx tp. + W4.IsSymExprBuilder sym => + NonEmptyCtx ctx => + sym -> + (SymIndex sym ctx -> IO (W4.Pred sym)) -> + ArrayEntry sym ctx tp -> + ArrayEntry sym ctx tp -> + IO (ArrayEntry sym ctx tp) +mergeEntries sym pickLeftFn e1 e2 = do + let vals symIdx' = do + pickLeft <- pickLeftFn symIdx' + val1 <- entryVals e1 symIdx' + val2 <- entryVals e2 symIdx' + W4.mergePartial sym (\p a b -> lift $ W4.baseTypeIte sym p a b) + pickLeft val1 val2 + incNonceEntry $ e1 { entryVals = vals } + +mergeEntriesMux :: + forall sym ctx tp. + W4.IsSymExprBuilder sym => + NonEmptyCtx ctx => + sym -> + (SymIndex sym ctx -> IO (W4.Pred sym)) -> + PMuxTree sym (ArrayEntry sym ctx tp) -> + PMuxTree sym (ArrayEntry sym ctx tp) -> + IO (PMuxTree sym (ArrayEntry sym ctx tp)) +mergeEntriesMux sym pickLeftFn = pmuxTreeBinOp sym (mergeEntries sym pickLeftFn) + +-- | A partial mux tree +type PMuxTree sym tp = MT.MuxTree sym (Maybe tp) + +viewPMuxTree :: forall sym a. PMuxTree sym a -> [(a, W4.Pred sym)] +viewPMuxTree mt = mapMaybe go $ MT.viewMuxTree mt + where + go :: (Maybe a, W4.Pred sym) -> Maybe (a, W4.Pred sym) + go (Just a, p) = Just (a, p) + go _ = Nothing + +isEmptyPMuxTree :: PMuxTree sym tp -> Bool +isEmptyPMuxTree mt = case MT.viewMuxTree mt of + [(Nothing, _)] -> True + _ -> False + +mkPMuxTree :: + (W4.IsExprBuilder sym, Ord a) => + sym -> + [(a, W4.Pred sym)] -> + IO (PMuxTree sym a) +mkPMuxTree sym ls = buildMuxTree sym Nothing (map (\(a, p) -> (Just a, p)) ls) + +mkPMuxTreePartial :: + forall sym a. + (W4.IsExprBuilder sym, Ord a) => + sym -> + [(W4.PartExpr (W4.Pred sym) a, W4.Pred sym)] -> + IO (PMuxTree sym a) +mkPMuxTreePartial sym ls = mkPMuxTree sym =<< (catMaybes <$> mapM go ls) + where + go :: (W4.PartExpr (W4.Pred sym) a, W4.Pred sym) -> IO (Maybe (a, W4.Pred sym)) + go (W4.PE p a, cond) = do + p' <- W4.andPred sym p cond + return $ Just (a, p') + go (W4.Unassigned, _) = return Nothing + +pmuxTreeAddCondition :: + forall sym a. + W4.IsExprBuilder sym => + Ord a => + sym -> + W4.Pred sym -> + PMuxTree sym a -> + IO (PMuxTree sym a) +pmuxTreeAddCondition sym cond mt = mkPMuxTree sym =<< mapM addCond (viewPMuxTree mt) + where + addCond :: (a, W4.Pred sym) -> IO (a, W4.Pred sym) + addCond (a, cond') = do + cond'' <- W4.andPred sym cond cond' + return $ (a, cond'') + + +pmuxTreeMaybeOp :: + (W4.IsExprBuilder sym, Ord a, Ord b) => + sym -> + (a -> IO (Maybe b)) -> + PMuxTree sym a -> + IO (PMuxTree sym b) +pmuxTreeMaybeOp sym f mt = MT.muxTreeUnaryOp sym (\a -> join <$> mapM f a) mt + +_pmuxTreeUnaryOp :: + (W4.IsExprBuilder sym, Ord b) => + sym -> + (a -> IO b) -> + PMuxTree sym a -> + IO (PMuxTree sym b) +_pmuxTreeUnaryOp sym f mt = MT.muxTreeUnaryOp sym (\a -> mapM f a) mt + + +pmuxTreeBinOp :: + forall sym a b c. + (W4.IsExprBuilder sym, Ord c) => + sym -> + (a -> b -> IO c) -> + PMuxTree sym a -> + PMuxTree sym b -> + IO (PMuxTree sym c) +pmuxTreeBinOp sym f mt1 mt2 = MT.muxTreeBinOp sym g mt1 mt2 + where + g :: Maybe a -> Maybe b -> IO (Maybe c) + g (Just a) (Just b) = Just <$> f a b + g _ _ = return Nothing + +toPMuxTree :: W4.IsExprBuilder sym => sym -> a -> PMuxTree sym a +toPMuxTree sym a = MT.toMuxTree sym (Just a) diff --git a/tests/TestMain.hs b/tests/TestMain.hs new file mode 100644 --- /dev/null +++ b/tests/TestMain.hs @@ -0,0 +1,564 @@ +----------------------------------------------------------------------- +-- | +-- Module : TestMain +-- Description : Test module for SymIO +-- Copyright : (c) Galois, Inc 2021 +-- License : BSD3 +-- Maintainer : Daniel Matichuk +-- 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 + + +