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