-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.SymIO
-- Description      : Exporting SymbolicIO operations as Override templates
-- Copyright        : (c) Galois, Inc 2020
-- License          : BSD3
-- Maintainer       : Daniel Matichuk <dmatichuk@galois.com>
-- Stability        : provisional
--
--
-- This module wraps the crucible-symio interface suitably for use within the
-- LLVM frontend to crucible. It provides overrides for the following functions:
--
--   * @open@
--   * @read@
--   * @write@
--   * @close@
--
-- as specified by POSIX. Note that it does not yet cover the C stdio functions.
-- This additional layer on top of crucible-symio is necessary to bridge the gap
-- between LLVMPointer arguments and more primitive argument types (including
-- that filenames need to be read from the LLVM memory model before they can be
-- interpreted).
--
-- The limitations of this library are enumerated in the README for crux-llvm,
-- which is the user-facing documentation for this functionality.
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE LambdaCase #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

module Lang.Crucible.LLVM.SymIO
  ( -- * Types
    llvmSymIOIntrinsicTypes
  , LLVMFileSystem(..)
  , SomeOverrideSim(..)
  , initialLLVMFileSystem
  -- * Overrides
  , symio_overrides
  , openFile
  , callOpenFile
  , closeFile
  , callCloseFile
  , readFileHandle
  , callReadFileHandle
  , writeFileHandle
  , callWriteFileHandle
  -- * File-related utilities
  , allocateFileDescriptor
  , lookupFileHandle
  )
  where

import           Control.Monad ( forM, foldM, when )
import           Control.Monad.IO.Class (liftIO)
import qualified Data.BitVector.Sized as BVS
import qualified Data.ByteString as BS
import qualified Data.ByteString.Char8 as BSC
import qualified Data.Foldable as F
import qualified Data.Map as Map
import qualified Data.Parameterized.Classes as PC
import           Data.Parameterized.Context
                   ( pattern (:>), pattern Empty, (::>), EmptyCtx, uncurryAssignment )
import qualified Data.Parameterized.Map as MapF
import qualified Data.Parameterized.NatRepr as PN
import qualified Data.Parameterized.SymbolRepr as PS
import qualified Data.Set as Set
import qualified Data.Text as Text
import qualified Data.Text.Encoding as TextEncoding
import qualified Data.Text.IO as Text.IO
import           GHC.Natural ( Natural )
import           GHC.TypeNats ( type (<=) )
import qualified System.IO as IO

import qualified Lang.Crucible.FunctionHandle as LCF
import           Lang.Crucible.Types ( IntrinsicType, BVType, TypeRepr(..) )
import qualified Lang.Crucible.Utils.MuxTree as CMT
import           Lang.Crucible.CFG.Common
import           Lang.Crucible.Backend as C
import           Lang.Crucible.Simulator.OverrideSim
import           Lang.Crucible.Simulator.Intrinsics
import           Lang.Crucible.Simulator.RegMap
import qualified Lang.Crucible.Simulator.GlobalState as LCSG

import           Lang.Crucible.LLVM.Bytes (toBytes)
import           Lang.Crucible.LLVM.MemModel
import           Lang.Crucible.LLVM.Extension ( ArchWidth )
import           Lang.Crucible.LLVM.DataLayout ( noAlignment )
import           Lang.Crucible.LLVM.Intrinsics
import           Lang.Crucible.LLVM.QQ( llvmOvr )

import qualified What4.Interface as W4
import qualified What4.Partial as W4P

import qualified Lang.Crucible.SymIO as SymIO

-- | A representation of the filesystem for the LLVM frontend
--
-- This contains the underlying SymIO filesystem as well as the infrastructure
-- for allocating fresh file handles
data LLVMFileSystem ptrW =
  LLVMFileSystem
    { forall (ptrW :: Natural).
LLVMFileSystem ptrW -> GlobalVar (FileSystemType ptrW)
llvmFileSystem :: GlobalVar (SymIO.FileSystemType ptrW)
    -- ^ The underlying symbolic filesystem
    , forall (ptrW :: Natural).
LLVMFileSystem ptrW -> GlobalVar (FDescMapType ptrW)
llvmFileDescMap :: GlobalVar (FDescMapType ptrW)
    -- ^ Maintains the mapping from file descriptors to low-level crucible-symio
    -- 'SymIO.FileHandle's
    , forall (ptrW :: Natural). LLVMFileSystem ptrW -> Map Natural Handle
llvmHandles :: Map.Map Natural IO.Handle
    -- ^ Handles that concrete output will be mirrored to; if this is empty, no
    -- mirroring will be performed
    , forall (ptrW :: Natural). LLVMFileSystem ptrW -> NatRepr ptrW
llvmFilePointerRepr :: PN.NatRepr ptrW
    }

-- | Contains the mapping from file descriptors to the underlying 'SymIO.FileHandle'
--
-- This also tracks the next file descriptor to hand out.  See Note [File
-- Descriptor Sequence].
data FDescMap sym ptrW where
  FDescMap ::
    { forall sym (ptrW :: Natural). FDescMap sym ptrW -> Natural
fDescNext :: Natural
    -- ^ The next file descriptor to hand out
    --
    -- Note that these are truncated to 32 bit bitvectors when they are handed
    -- out; we don't have any guards against overflow on that right now
    , forall sym (ptrW :: Natural).
FDescMap sym ptrW
-> Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
fDescMap :: Map.Map Natural (W4P.PartExpr (W4.Pred sym) (SymIO.FileHandle sym ptrW))
    } -> FDescMap sym ptrW

-- | A wrapper around a RankN 'OverrideSim' action
--
-- This enables us to make explicit that all of the type variables are free and
-- can be instantiated at any types since this override action has to be
-- returned from the 'initialLLVMFileSystem' function.
newtype SomeOverrideSim sym a where
  SomeOverrideSim :: (forall p ext rtp args ret . OverrideSim p sym ext rtp args ret a) -> SomeOverrideSim sym a

targetToFD :: SymIO.FDTarget k -> Maybe Natural
targetToFD :: forall (k :: TargetDirection). FDTarget k -> Maybe Natural
targetToFD FDTarget k
t =
  case FDTarget k
t of
    FDTarget k
SymIO.StdinTarget -> Natural -> Maybe Natural
forall a. a -> Maybe a
Just Natural
0
    FDTarget k
SymIO.StdoutTarget -> Natural -> Maybe Natural
forall a. a -> Maybe a
Just Natural
1
    FDTarget k
SymIO.StderrTarget -> Natural -> Maybe Natural
forall a. a -> Maybe a
Just Natural
2
    FDTarget k
_ -> Maybe Natural
forall a. Maybe a
Nothing

-- | Create an initial 'LLVMFileSystem' based on given concrete and symbolic file contents
--
-- Note that this function takes a 'LCSG.SymGlobalState' because it needs to
-- allocate a few distinguished global variables for its own bookkeeping. It
-- adds them to the given global state and returns an updated global state,
-- which must not be discarded.
--
-- The returned 'LLVMFileSystem' is a wrapper around that global state, and is
-- required to initialize the symbolic I/O overrides.
--
-- This function also returns an 'OverrideSim' action (wrapped in a
-- 'SomeOverrideSim') that must be run to initialize any standard IO file
-- descriptors that have been requested.  This action should be run *before* the
-- entry point of the function that is being verified is invoked.
--
-- See Note [Standard IO Setup] for details
initialLLVMFileSystem
  :: forall sym ptrW
   . (HasPtrWidth ptrW, C.IsSymInterface sym)
  => LCF.HandleAllocator
  -> sym
  -> PN.NatRepr ptrW
  -- ^ The pointer width for the platform
  -> SymIO.InitialFileSystemContents sym
  -- ^ The initial contents of the symbolic filesystem
  -> [(SymIO.FDTarget SymIO.Out, IO.Handle)]
  -- ^ A mapping from file targets to handles, to which output should be
  -- mirrored. This is intended to support mirroring symbolic stdout/stderr to
  -- concrete stdout/stderr, but could be more flexible in the future (e.g.,
  -- handling sockets).
  --
  -- Note that the writes to the associated underlying symbolic files are still
  -- recorded in the symbolic filesystem
  -> LCSG.SymGlobalState sym
  -- ^ The current globals, which will be updated with necessary bindings to support the filesystem
  -> IO (LLVMFileSystem ptrW, LCSG.SymGlobalState sym, SomeOverrideSim sym ())
initialLLVMFileSystem :: forall sym (ptrW :: Natural).
(HasPtrWidth ptrW, IsSymInterface sym) =>
HandleAllocator
-> sym
-> NatRepr ptrW
-> InitialFileSystemContents sym
-> [(FDTarget 'Out, Handle)]
-> SymGlobalState sym
-> IO
     (LLVMFileSystem ptrW, SymGlobalState sym, SomeOverrideSim sym ())
initialLLVMFileSystem HandleAllocator
halloc sym
sym NatRepr ptrW
ptrW InitialFileSystemContents sym
initContents [(FDTarget 'Out, Handle)]
handles SymGlobalState sym
globals0 = do
  FileSystem sym ptrW
fs0 <- sym
-> NatRepr ptrW
-> InitialFileSystemContents sym
-> IO (FileSystem sym ptrW)
forall sym (wptr :: Natural).
(1 <= wptr, IsSymInterface sym) =>
sym
-> NatRepr wptr
-> InitialFileSystemContents sym
-> IO (FileSystem sym wptr)
SymIO.initFS sym
sym NatRepr ptrW
ptrW InitialFileSystemContents sym
initContents
  let fdm0 :: FDescMap sym ptrW
fdm0 = FDescMap { fDescNext :: Natural
fDescNext = Natural
0
                      , fDescMap :: Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
fDescMap = Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
forall k a. Map k a
Map.empty
                      }
  GlobalVar (FileSystemType ptrW)
fsVar <- HandleAllocator
-> Text
-> TypeRepr (FileSystemType ptrW)
-> IO (GlobalVar (FileSystemType ptrW))
forall (tp :: CrucibleType).
HandleAllocator -> Text -> TypeRepr tp -> IO (GlobalVar tp)
freshGlobalVar HandleAllocator
halloc (String -> Text
Text.pack String
"llvmFileSystem_Global") (NatRepr ptrW -> TypeRepr (FileSystemType ptrW)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ FileSystemType w) =>
NatRepr w -> TypeRepr ty
SymIO.FileSystemRepr NatRepr ptrW
ptrW)
  GlobalVar (FDescMapType ptrW)
fdmVar <- HandleAllocator
-> Text
-> TypeRepr (FDescMapType ptrW)
-> IO (GlobalVar (FDescMapType ptrW))
forall (tp :: CrucibleType).
HandleAllocator -> Text -> TypeRepr tp -> IO (GlobalVar tp)
freshGlobalVar HandleAllocator
halloc (String -> Text
Text.pack String
"llvmFileDescMap_Global") (NatRepr ptrW -> TypeRepr (FDescMapType ptrW)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ FDescMapType w) =>
NatRepr w -> TypeRepr ty
FDescMapRepr NatRepr ptrW
ptrW)
  let llfs :: LLVMFileSystem ptrW
llfs = LLVMFileSystem { llvmFileSystem :: GlobalVar (FileSystemType ptrW)
llvmFileSystem = GlobalVar (FileSystemType ptrW)
fsVar
                            , llvmFileDescMap :: GlobalVar (FDescMapType ptrW)
llvmFileDescMap = GlobalVar (FDescMapType ptrW)
fdmVar
                            , llvmFilePointerRepr :: NatRepr ptrW
llvmFilePointerRepr = NatRepr ptrW
ptrW
                            , llvmHandles :: Map Natural Handle
llvmHandles = [(Natural, Handle)] -> Map Natural Handle
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Natural
fd, Handle
hdl)
                                                         | (FDTarget 'Out
tgt, Handle
hdl) <- [(FDTarget 'Out, Handle)]
handles
                                                         , Just Natural
fd <- Maybe Natural -> [Maybe Natural]
forall a. a -> [a]
forall (m :: Type -> Type) a. Monad m => a -> m a
return (FDTarget 'Out -> Maybe Natural
forall (k :: TargetDirection). FDTarget k -> Maybe Natural
targetToFD FDTarget 'Out
tgt)
                                                         ]
                            }
  let globals1 :: SymGlobalState sym
globals1 = GlobalVar (FDescMapType ptrW)
-> RegValue sym (FDescMapType ptrW)
-> SymGlobalState sym
-> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
LCSG.insertGlobal GlobalVar (FDescMapType ptrW)
fdmVar RegValue sym (FDescMapType ptrW)
FDescMap sym ptrW
forall {sym} {ptrW :: Natural}. FDescMap sym ptrW
fdm0 (SymGlobalState sym -> SymGlobalState sym)
-> SymGlobalState sym -> SymGlobalState sym
forall a b. (a -> b) -> a -> b
$ GlobalVar (FileSystemType ptrW)
-> RegValue sym (FileSystemType ptrW)
-> SymGlobalState sym
-> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
LCSG.insertGlobal GlobalVar (FileSystemType ptrW)
fsVar RegValue sym (FileSystemType ptrW)
FileSystem sym ptrW
fs0 SymGlobalState sym
globals0
  let bootstrapStdio :: OverrideSim p sym ext rtp args ret ()
      bootstrapStdio :: forall p ext rtp (args :: Ctx CrucibleType) (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret ()
bootstrapStdio = do
        -- Allocate the file handles for the standard IO streams in order such
        -- that they are in file descriptors 0, 1, and 2 respectively
        --
        -- We discard the actual file descriptors because they are accessed via
        -- literals in the program.  The 'allocateFileDescriptor' function
        -- handles mapping the underlying FileHandle to an int file descriptor
        -- internally.
        let toLit :: FDTarget k -> StringLiteral 'Char8
toLit = ByteString -> StringLiteral 'Char8
W4.Char8Literal (ByteString -> StringLiteral 'Char8)
-> (FDTarget k -> ByteString) -> FDTarget k -> StringLiteral 'Char8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> ByteString
TextEncoding.encodeUtf8 (Text -> ByteString)
-> (FDTarget k -> Text) -> FDTarget k -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FDTarget k -> Text
forall (k :: TargetDirection). FDTarget k -> Text
SymIO.fdTargetToText
        Bool
-> OverrideSim p sym ext rtp args ret ()
-> OverrideSim p sym ext rtp args ret ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (FDTarget 'In -> Map (FDTarget 'In) ByteString -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member FDTarget 'In
SymIO.StdinTarget (InitialFileSystemContents sym -> Map (FDTarget 'In) ByteString
forall sym.
InitialFileSystemContents sym -> Map (FDTarget 'In) ByteString
SymIO.concreteFiles InitialFileSystemContents sym
initContents) Bool -> Bool -> Bool
|| FDTarget 'In -> Map (FDTarget 'In) [SymBV sym 8] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member FDTarget 'In
SymIO.StdinTarget (InitialFileSystemContents sym -> Map (FDTarget 'In) [SymBV sym 8]
forall sym.
InitialFileSystemContents sym -> Map (FDTarget 'In) [SymBV sym 8]
SymIO.symbolicFiles InitialFileSystemContents sym
initContents)) (OverrideSim p sym ext rtp args ret ()
 -> OverrideSim p sym ext rtp args ret ())
-> OverrideSim p sym ext rtp args ret ()
-> OverrideSim p sym ext rtp args ret ()
forall a b. (a -> b) -> a -> b
$ do
          SymExpr sym (BaseStringType 'Char8)
stdinFilename <- IO (SymExpr sym (BaseStringType 'Char8))
-> OverrideSim
     p sym ext rtp args ret (SymExpr sym (BaseStringType 'Char8))
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseStringType 'Char8))
 -> OverrideSim
      p sym ext rtp args ret (SymExpr sym (BaseStringType 'Char8)))
-> IO (SymExpr sym (BaseStringType 'Char8))
-> OverrideSim
     p sym ext rtp args ret (SymExpr sym (BaseStringType 'Char8))
forall a b. (a -> b) -> a -> b
$ sym
-> StringLiteral 'Char8 -> IO (SymExpr sym (BaseStringType 'Char8))
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
forall (si :: StringInfo).
sym -> StringLiteral si -> IO (SymString sym si)
W4.stringLit sym
sym (FDTarget 'In -> StringLiteral 'Char8
forall {k :: TargetDirection}. FDTarget k -> StringLiteral 'Char8
toLit FDTarget 'In
SymIO.StdinTarget)
          SymExpr sym (BaseBVType 32)
_inFD <- GlobalVar (FileSystemType ptrW)
-> FileIdent sym
-> OverrideSim
     p sym ext rtp args ret (RegValue sym (FileHandleType ptrW))
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileIdent sym
-> OverrideSim p sym arch r args ret (FileHandle sym wptr)
SymIO.openFile' GlobalVar (FileSystemType ptrW)
fsVar FileIdent sym
SymExpr sym (BaseStringType 'Char8)
stdinFilename OverrideSim
  p sym ext rtp args ret (RegValue sym (FileHandleType ptrW))
-> (RegValue sym (FileHandleType ptrW)
    -> OverrideSim
         p sym ext rtp args ret (SymExpr sym (BaseBVType 32)))
-> OverrideSim p sym ext rtp args ret (SymExpr sym (BaseBVType 32))
forall a b.
OverrideSim p sym ext rtp args ret a
-> (a -> OverrideSim p sym ext rtp args ret b)
-> OverrideSim p sym ext rtp args ret b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= LLVMFileSystem ptrW
-> RegValue sym (FileHandleType ptrW)
-> OverrideSim p sym ext rtp args ret (SymExpr sym (BaseBVType 32))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
LLVMFileSystem wptr
-> FileHandle sym wptr
-> OverrideSim p sym ext r args ret (SymBV sym 32)
allocateFileDescriptor LLVMFileSystem ptrW
llfs
          () -> OverrideSim p sym ext rtp args ret ()
forall a. a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
        Bool
-> OverrideSim p sym ext rtp args ret ()
-> OverrideSim p sym ext rtp args ret ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (InitialFileSystemContents sym -> Bool
forall sym. InitialFileSystemContents sym -> Bool
SymIO.useStdout InitialFileSystemContents sym
initContents) (OverrideSim p sym ext rtp args ret ()
 -> OverrideSim p sym ext rtp args ret ())
-> OverrideSim p sym ext rtp args ret ()
-> OverrideSim p sym ext rtp args ret ()
forall a b. (a -> b) -> a -> b
$ do
          SymExpr sym (BaseStringType 'Char8)
stdoutFilename <- IO (SymExpr sym (BaseStringType 'Char8))
-> OverrideSim
     p sym ext rtp args ret (SymExpr sym (BaseStringType 'Char8))
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseStringType 'Char8))
 -> OverrideSim
      p sym ext rtp args ret (SymExpr sym (BaseStringType 'Char8)))
-> IO (SymExpr sym (BaseStringType 'Char8))
-> OverrideSim
     p sym ext rtp args ret (SymExpr sym (BaseStringType 'Char8))
forall a b. (a -> b) -> a -> b
$ sym
-> StringLiteral 'Char8 -> IO (SymExpr sym (BaseStringType 'Char8))
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
forall (si :: StringInfo).
sym -> StringLiteral si -> IO (SymString sym si)
W4.stringLit sym
sym (FDTarget 'Out -> StringLiteral 'Char8
forall {k :: TargetDirection}. FDTarget k -> StringLiteral 'Char8
toLit FDTarget 'Out
SymIO.StdoutTarget)
          SymExpr sym (BaseBVType 32)
_outFD <- GlobalVar (FileSystemType ptrW)
-> FileIdent sym
-> OverrideSim
     p sym ext rtp args ret (RegValue sym (FileHandleType ptrW))
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileIdent sym
-> OverrideSim p sym arch r args ret (FileHandle sym wptr)
SymIO.openFile' GlobalVar (FileSystemType ptrW)
fsVar FileIdent sym
SymExpr sym (BaseStringType 'Char8)
stdoutFilename OverrideSim
  p sym ext rtp args ret (RegValue sym (FileHandleType ptrW))
-> (RegValue sym (FileHandleType ptrW)
    -> OverrideSim
         p sym ext rtp args ret (SymExpr sym (BaseBVType 32)))
-> OverrideSim p sym ext rtp args ret (SymExpr sym (BaseBVType 32))
forall a b.
OverrideSim p sym ext rtp args ret a
-> (a -> OverrideSim p sym ext rtp args ret b)
-> OverrideSim p sym ext rtp args ret b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= LLVMFileSystem ptrW
-> RegValue sym (FileHandleType ptrW)
-> OverrideSim p sym ext rtp args ret (SymExpr sym (BaseBVType 32))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
LLVMFileSystem wptr
-> FileHandle sym wptr
-> OverrideSim p sym ext r args ret (SymBV sym 32)
allocateFileDescriptor LLVMFileSystem ptrW
llfs
          () -> OverrideSim p sym ext rtp args ret ()
forall a. a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
        Bool
-> OverrideSim p sym ext rtp args ret ()
-> OverrideSim p sym ext rtp args ret ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (InitialFileSystemContents sym -> Bool
forall sym. InitialFileSystemContents sym -> Bool
SymIO.useStderr InitialFileSystemContents sym
initContents) (OverrideSim p sym ext rtp args ret ()
 -> OverrideSim p sym ext rtp args ret ())
-> OverrideSim p sym ext rtp args ret ()
-> OverrideSim p sym ext rtp args ret ()
forall a b. (a -> b) -> a -> b
$ do
          SymExpr sym (BaseStringType 'Char8)
stderrFilename <- IO (SymExpr sym (BaseStringType 'Char8))
-> OverrideSim
     p sym ext rtp args ret (SymExpr sym (BaseStringType 'Char8))
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseStringType 'Char8))
 -> OverrideSim
      p sym ext rtp args ret (SymExpr sym (BaseStringType 'Char8)))
-> IO (SymExpr sym (BaseStringType 'Char8))
-> OverrideSim
     p sym ext rtp args ret (SymExpr sym (BaseStringType 'Char8))
forall a b. (a -> b) -> a -> b
$ sym
-> StringLiteral 'Char8 -> IO (SymExpr sym (BaseStringType 'Char8))
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
forall (si :: StringInfo).
sym -> StringLiteral si -> IO (SymString sym si)
W4.stringLit sym
sym (FDTarget 'Out -> StringLiteral 'Char8
forall {k :: TargetDirection}. FDTarget k -> StringLiteral 'Char8
toLit FDTarget 'Out
SymIO.StderrTarget)
          SymExpr sym (BaseBVType 32)
_errFD <- GlobalVar (FileSystemType ptrW)
-> FileIdent sym
-> OverrideSim
     p sym ext rtp args ret (RegValue sym (FileHandleType ptrW))
forall sym (wptr :: Natural) p arch r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileIdent sym
-> OverrideSim p sym arch r args ret (FileHandle sym wptr)
SymIO.openFile' GlobalVar (FileSystemType ptrW)
fsVar FileIdent sym
SymExpr sym (BaseStringType 'Char8)
stderrFilename OverrideSim
  p sym ext rtp args ret (RegValue sym (FileHandleType ptrW))
-> (RegValue sym (FileHandleType ptrW)
    -> OverrideSim
         p sym ext rtp args ret (SymExpr sym (BaseBVType 32)))
-> OverrideSim p sym ext rtp args ret (SymExpr sym (BaseBVType 32))
forall a b.
OverrideSim p sym ext rtp args ret a
-> (a -> OverrideSim p sym ext rtp args ret b)
-> OverrideSim p sym ext rtp args ret b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= LLVMFileSystem ptrW
-> RegValue sym (FileHandleType ptrW)
-> OverrideSim p sym ext rtp args ret (SymExpr sym (BaseBVType 32))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
LLVMFileSystem wptr
-> FileHandle sym wptr
-> OverrideSim p sym ext r args ret (SymBV sym 32)
allocateFileDescriptor LLVMFileSystem ptrW
llfs
          () -> OverrideSim p sym ext rtp args ret ()
forall a. a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()

  (LLVMFileSystem ptrW, SymGlobalState sym, SomeOverrideSim sym ())
-> IO
     (LLVMFileSystem ptrW, SymGlobalState sym, SomeOverrideSim sym ())
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMFileSystem ptrW
llfs, SymGlobalState sym
globals1, (forall p ext rtp (args :: Ctx CrucibleType) (ret :: CrucibleType).
 OverrideSim p sym ext rtp args ret ())
-> SomeOverrideSim sym ()
forall sym a.
(forall p ext rtp (args :: Ctx CrucibleType) (ret :: CrucibleType).
 OverrideSim p sym ext rtp args ret a)
-> SomeOverrideSim sym a
SomeOverrideSim OverrideSim p sym ext rtp args ret ()
forall p ext rtp (args :: Ctx CrucibleType) (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret ()
bootstrapStdio)

type FDescMapType w = IntrinsicType "LLVM_fdescmap" (EmptyCtx ::> BVType w)

instance (IsSymInterface sym) => IntrinsicClass sym "LLVM_fdescmap" where
  type Intrinsic sym "LLVM_fdescmap" (EmptyCtx ::> BVType w) = FDescMap sym w

  muxIntrinsic :: forall (ctx :: Ctx CrucibleType).
sym
-> IntrinsicTypes sym
-> SymbolRepr "LLVM_fdescmap"
-> CtxRepr ctx
-> Pred sym
-> Intrinsic sym "LLVM_fdescmap" ctx
-> Intrinsic sym "LLVM_fdescmap" ctx
-> IO (Intrinsic sym "LLVM_fdescmap" ctx)
muxIntrinsic sym
sym IntrinsicTypes sym
_iTypes SymbolRepr "LLVM_fdescmap"
_nm (Assignment TypeRepr ctx
Empty :> (BVRepr NatRepr n
_w)) = sym
-> Pred sym
-> FDescMap sym n
-> FDescMap sym n
-> IO (FDescMap sym n)
forall sym (ptrW :: Natural).
IsSymInterface sym =>
sym
-> Pred sym
-> FDescMap sym ptrW
-> FDescMap sym ptrW
-> IO (FDescMap sym ptrW)
muxFDescMap sym
sym
  muxIntrinsic sym
_ IntrinsicTypes sym
_ SymbolRepr "LLVM_fdescmap"
nm Assignment TypeRepr ctx
ctx = \Pred sym
_ Intrinsic sym "LLVM_fdescmap" ctx
_ Intrinsic sym "LLVM_fdescmap" ctx
_ -> SymbolRepr "LLVM_fdescmap"
-> Assignment TypeRepr ctx
-> IO (Intrinsic sym "LLVM_fdescmap" ctx)
forall (nm :: Symbol) (ctx :: Ctx CrucibleType) b.
HasCallStack =>
SymbolRepr nm -> CtxRepr ctx -> b
typeError SymbolRepr "LLVM_fdescmap"
nm Assignment TypeRepr ctx
ctx

pattern FDescMapRepr :: () => (1 <= w, ty ~ FDescMapType w) => PN.NatRepr w -> TypeRepr ty
pattern $mFDescMapRepr :: forall {r} {ty :: CrucibleType}.
TypeRepr ty
-> (forall {w :: Natural}.
    (1 <= w, ty ~ FDescMapType w) =>
    NatRepr w -> r)
-> ((# #) -> r)
-> r
$bFDescMapRepr :: forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ FDescMapType w) =>
NatRepr w -> TypeRepr ty
FDescMapRepr w <- IntrinsicRepr (PC.testEquality (PS.knownSymbol @"LLVM_fdescmap") -> Just PC.Refl) (Empty :> BVRepr w)
  where
    FDescMapRepr NatRepr w
w = SymbolRepr "LLVM_fdescmap"
-> CtxRepr (EmptyCtx ::> 'BaseToType (BaseBVType w))
-> TypeRepr (FDescMapType w)
forall (nm :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr nm -> CtxRepr ctx -> TypeRepr ('IntrinsicType nm ctx)
IntrinsicRepr SymbolRepr "LLVM_fdescmap"
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
PS.knownSymbol (Assignment TypeRepr EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment TypeRepr EmptyCtx
-> TypeRepr ('BaseToType (BaseBVType w))
-> CtxRepr (EmptyCtx ::> 'BaseToType (BaseBVType w))
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w)

muxFDescMap
  :: IsSymInterface sym
  => sym
  -> W4.Pred sym
  -> FDescMap sym ptrW
  -> FDescMap sym ptrW
  -> IO (FDescMap sym ptrW)
muxFDescMap :: forall sym (ptrW :: Natural).
IsSymInterface sym =>
sym
-> Pred sym
-> FDescMap sym ptrW
-> FDescMap sym ptrW
-> IO (FDescMap sym ptrW)
muxFDescMap sym
sym Pred sym
p (FDescMap Natural
nextT Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
mapT) (FDescMap Natural
nextF Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
mapF) = do
  let
    keys :: [Natural]
keys = Set Natural -> [Natural]
forall a. Set a -> [a]
Set.toList (Set Natural -> [Natural]) -> Set Natural -> [Natural]
forall a b. (a -> b) -> a -> b
$ Set Natural -> Set Natural -> Set Natural
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
-> Set Natural
forall k a. Map k a -> Set k
Map.keysSet Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
mapT) (Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
-> Set Natural
forall k a. Map k a -> Set k
Map.keysSet Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
mapF)
    next :: Natural
next = Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
max Natural
nextT Natural
nextF
  ([(Natural, PartExpr (Pred sym) (FileHandle sym ptrW))]
 -> FDescMap sym ptrW)
-> IO [(Natural, PartExpr (Pred sym) (FileHandle sym ptrW))]
-> IO (FDescMap sym ptrW)
forall a b. (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Natural
-> Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
-> FDescMap sym ptrW
forall sym (ptrW :: Natural).
Natural
-> Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
-> FDescMap sym ptrW
FDescMap Natural
next (Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
 -> FDescMap sym ptrW)
-> ([(Natural, PartExpr (Pred sym) (FileHandle sym ptrW))]
    -> Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW)))
-> [(Natural, PartExpr (Pred sym) (FileHandle sym ptrW))]
-> FDescMap sym ptrW
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Natural, PartExpr (Pred sym) (FileHandle sym ptrW))]
-> Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList) (IO [(Natural, PartExpr (Pred sym) (FileHandle sym ptrW))]
 -> IO (FDescMap sym ptrW))
-> IO [(Natural, PartExpr (Pred sym) (FileHandle sym ptrW))]
-> IO (FDescMap sym ptrW)
forall a b. (a -> b) -> a -> b
$ [Natural]
-> (Natural
    -> IO (Natural, PartExpr (Pred sym) (FileHandle sym ptrW)))
-> IO [(Natural, PartExpr (Pred sym) (FileHandle sym ptrW))]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Natural]
keys ((Natural
  -> IO (Natural, PartExpr (Pred sym) (FileHandle sym ptrW)))
 -> IO [(Natural, PartExpr (Pred sym) (FileHandle sym ptrW))])
-> (Natural
    -> IO (Natural, PartExpr (Pred sym) (FileHandle sym ptrW)))
-> IO [(Natural, PartExpr (Pred sym) (FileHandle sym ptrW))]
forall a b. (a -> b) -> a -> b
$ \Natural
k -> do
    let vT :: PartExpr (Pred sym) (FileHandle sym ptrW)
vT = Maybe (PartExpr (Pred sym) (FileHandle sym ptrW))
-> PartExpr (Pred sym) (FileHandle sym ptrW)
forall p v. Maybe (PartExpr p v) -> PartExpr p v
W4P.joinMaybePE (Natural
-> Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
-> Maybe (PartExpr (Pred sym) (FileHandle sym ptrW))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Natural
k Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
mapT)
    let vF :: PartExpr (Pred sym) (FileHandle sym ptrW)
vF = Maybe (PartExpr (Pred sym) (FileHandle sym ptrW))
-> PartExpr (Pred sym) (FileHandle sym ptrW)
forall p v. Maybe (PartExpr p v) -> PartExpr p v
W4P.joinMaybePE (Natural
-> Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
-> Maybe (PartExpr (Pred sym) (FileHandle sym ptrW))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Natural
k Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
mapF)
    PartExpr
  (Pred sym)
  (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
r <- sym
-> (Pred sym
    -> MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))
    -> MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))
    -> IO (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))))
-> Pred sym
-> PartExpr
     (Pred sym)
     (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
-> PartExpr
     (Pred sym)
     (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
-> IO
     (PartExpr
        (Pred sym)
        (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))))
forall sym v.
IsExprBuilder sym =>
sym
-> (Pred sym -> v -> v -> IO v)
-> Pred sym
-> PartExpr (Pred sym) v
-> PartExpr (Pred sym) v
-> IO (PartExpr (Pred sym) v)
mergePartExpr sym
sym (sym
-> Pred sym
-> MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))
-> MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))
-> IO (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
forall a sym.
(Ord a, IsExprBuilder sym) =>
sym
-> Pred sym -> MuxTree sym a -> MuxTree sym a -> IO (MuxTree sym a)
CMT.mergeMuxTree sym
sym) Pred sym
p PartExpr
  (Pred sym)
  (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
PartExpr (Pred sym) (FileHandle sym ptrW)
vT PartExpr
  (Pred sym)
  (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
PartExpr (Pred sym) (FileHandle sym ptrW)
vF
    (Natural,
 PartExpr
   (Pred sym)
   (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))))
-> IO
     (Natural,
      PartExpr
        (Pred sym)
        (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Natural
k,PartExpr
  (Pred sym)
  (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
r)

-- | The intrinsics supporting symbolic I/O in LLVM
--
-- Note that this includes the base intrinsic types from crucible-symio, so
-- those do not need to be added again.
llvmSymIOIntrinsicTypes :: IsSymInterface sym => IntrinsicTypes sym
llvmSymIOIntrinsicTypes :: forall sym. IsSymInterface sym => IntrinsicTypes sym
llvmSymIOIntrinsicTypes = MapF SymbolRepr (IntrinsicMuxFn sym)
-> MapF SymbolRepr (IntrinsicMuxFn sym)
forall a. a -> a
id
  (MapF SymbolRepr (IntrinsicMuxFn sym)
 -> MapF SymbolRepr (IntrinsicMuxFn sym))
-> (MapF SymbolRepr (IntrinsicMuxFn sym)
    -> MapF SymbolRepr (IntrinsicMuxFn sym))
-> MapF SymbolRepr (IntrinsicMuxFn sym)
-> MapF SymbolRepr (IntrinsicMuxFn sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolRepr "LLVM_fdescmap"
-> IntrinsicMuxFn sym "LLVM_fdescmap"
-> MapF SymbolRepr (IntrinsicMuxFn sym)
-> MapF SymbolRepr (IntrinsicMuxFn sym)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert (SymbolRepr "LLVM_fdescmap"
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
PS.knownSymbol :: PS.SymbolRepr "LLVM_fdescmap") IntrinsicMuxFn sym "LLVM_fdescmap"
forall sym (nm :: Symbol).
IntrinsicClass sym nm =>
IntrinsicMuxFn sym nm
IntrinsicMuxFn
  (MapF SymbolRepr (IntrinsicMuxFn sym)
 -> MapF SymbolRepr (IntrinsicMuxFn sym))
-> MapF SymbolRepr (IntrinsicMuxFn sym)
-> MapF SymbolRepr (IntrinsicMuxFn sym)
forall a b. (a -> b) -> a -> b
$ MapF SymbolRepr (IntrinsicMuxFn sym)
forall sym. IsSymInterface sym => IntrinsicTypes sym
SymIO.symIOIntrinsicTypes

-- | Resolve a symbolic file descriptor to a known allocated file handle.
-- The partial result is undefined if the descriptor is not found in the
-- file handle table.
getHandle
  :: forall sym ptrW
   . IsSymInterface sym
  => sym
  -> W4.SymBV sym 32
  -> FDescMap sym ptrW
  -> IO (W4P.PartExpr (W4.Pred sym) (SymIO.FileHandle sym ptrW))
getHandle :: forall sym (ptrW :: Natural).
IsSymInterface sym =>
sym
-> SymBV sym 32
-> FDescMap sym ptrW
-> IO (PartExpr (Pred sym) (FileHandle sym ptrW))
getHandle sym
sym SymBV sym 32
fdesc (FDescMap Natural
_ Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
m) = case SymBV sym 32 -> Maybe (BV 32)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
W4.asBV SymBV sym 32
fdesc of
  Just BV 32
fdesc_lit | Just PartExpr (Pred sym) (FileHandle sym ptrW)
fhdl <- Natural
-> Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
-> Maybe (PartExpr (Pred sym) (FileHandle sym ptrW))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (BV 32 -> Natural
forall (w :: Natural). BV w -> Natural
BVS.asNatural BV 32
fdesc_lit) Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
m -> PartExpr (Pred sym) (FileHandle sym ptrW)
-> IO (PartExpr (Pred sym) (FileHandle sym ptrW))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return PartExpr (Pred sym) (FileHandle sym ptrW)
fhdl
  Maybe (BV 32)
_ -> do
    [(Pred sym,
  PartExpr
    (Pred sym)
    (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))))]
cases <- ((Natural, PartExpr (Pred sym) (FileHandle sym ptrW))
 -> IO (Pred sym, PartExpr (Pred sym) (FileHandle sym ptrW)))
-> [(Natural, PartExpr (Pred sym) (FileHandle sym ptrW))]
-> IO [(Pred sym, PartExpr (Pred sym) (FileHandle sym ptrW))]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (Natural, PartExpr (Pred sym) (FileHandle sym ptrW))
-> IO (Pred sym, PartExpr (Pred sym) (FileHandle sym ptrW))
go (Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
-> [(Natural, PartExpr (Pred sym) (FileHandle sym ptrW))]
forall k a. Map k a -> [(k, a)]
Map.assocs Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
m)
    (PartExpr
   (Pred sym)
   (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
 -> (Pred sym,
     PartExpr
       (Pred sym)
       (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))))
 -> IO
      (PartExpr
         (Pred sym)
         (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))))
-> PartExpr
     (Pred sym)
     (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
-> [(Pred sym,
     PartExpr
       (Pred sym)
       (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))))]
-> IO
     (PartExpr
        (Pred sym)
        (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))))
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\PartExpr
  (Pred sym)
  (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
a (Pred sym
p, PartExpr
  (Pred sym)
  (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
b) -> sym
-> (Pred sym
    -> MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))
    -> MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))
    -> IO (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))))
-> Pred sym
-> PartExpr
     (Pred sym)
     (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
-> PartExpr
     (Pred sym)
     (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
-> IO
     (PartExpr
        (Pred sym)
        (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))))
forall sym v.
IsExprBuilder sym =>
sym
-> (Pred sym -> v -> v -> IO v)
-> Pred sym
-> PartExpr (Pred sym) v
-> PartExpr (Pred sym) v
-> IO (PartExpr (Pred sym) v)
mergePartExpr sym
sym (sym
-> Pred sym
-> MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))
-> MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))
-> IO (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
forall a sym.
(Ord a, IsExprBuilder sym) =>
sym
-> Pred sym -> MuxTree sym a -> MuxTree sym a -> IO (MuxTree sym a)
CMT.mergeMuxTree sym
sym) Pred sym
p PartExpr
  (Pred sym)
  (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
b PartExpr
  (Pred sym)
  (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
a) PartExpr
  (Pred sym)
  (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
forall p v. PartExpr p v
W4P.Unassigned [(Pred sym,
  PartExpr
    (Pred sym)
    (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))))]
cases
  where
    go :: (Natural, (W4P.PartExpr (W4.Pred sym) (SymIO.FileHandle sym ptrW)))
       -> IO (W4.Pred sym, (W4P.PartExpr (W4.Pred sym) (SymIO.FileHandle sym ptrW)))
    go :: (Natural, PartExpr (Pred sym) (FileHandle sym ptrW))
-> IO (Pred sym, PartExpr (Pred sym) (FileHandle sym ptrW))
go (Natural
n, PartExpr (Pred sym) (FileHandle sym ptrW)
fhdl) = do
      SymBV sym 32
n_sym <- sym -> NatRepr 32 -> BV 32 -> IO (SymBV sym 32)
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym NatRepr 32
forall (n :: Natural). KnownNat n => NatRepr n
PN.knownNat (NatRepr 32 -> Integer -> BV 32
forall (w :: Natural). NatRepr w -> Integer -> BV w
BVS.mkBV NatRepr 32
forall (n :: Natural). KnownNat n => NatRepr n
PN.knownNat (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n))
      Pred sym
fdesc_eq <- sym -> SymBV sym 32 -> SymBV sym 32 -> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvEq sym
sym SymBV sym 32
n_sym SymBV sym 32
fdesc
      (Pred sym,
 PartExpr
   (Pred sym)
   (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))))
-> IO
     (Pred sym,
      PartExpr
        (Pred sym)
        (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Pred sym,
  PartExpr
    (Pred sym)
    (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))))
 -> IO
      (Pred sym,
       PartExpr
         (Pred sym)
         (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))))
-> (Pred sym,
    PartExpr
      (Pred sym)
      (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))))
-> IO
     (Pred sym,
      PartExpr
        (Pred sym)
        (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW)))))
forall a b. (a -> b) -> a -> b
$ (Pred sym
fdesc_eq, PartExpr
  (Pred sym)
  (MuxTree sym (RefCell ('MaybeType (FilePointerType ptrW))))
PartExpr (Pred sym) (FileHandle sym ptrW)
fhdl)

-- | Construct a 'SymIO.DataChunk' from a pointer
--
-- Note that this is a lazy construct that does not load memory immediately. An
-- 'SymIO.DataChunk' is a wrapper around a function to peek memory at a given
-- offset one byte at a time.
chunkFromMemory
  :: forall sym bak wptr
   . (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions)
  => bak
  -> MemImpl sym
  -> LLVMPtr sym wptr
  -> IO (SymIO.DataChunk sym wptr)
chunkFromMemory :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
bak -> MemImpl sym -> LLVMPtr sym wptr -> IO (DataChunk sym wptr)
chunkFromMemory bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr =
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak in
  sym
-> (SymExpr sym (BaseBVType wptr)
    -> IO (SymExpr sym (BaseBVType 8)))
-> IO (ArrayChunk sym (BaseBVType wptr) (BaseBVType 8))
forall sym (idx :: BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> (SymExpr sym idx -> IO (SymExpr sym tp))
-> IO (ArrayChunk sym idx tp)
SymIO.mkArrayChunk sym
sym ((SymExpr sym (BaseBVType wptr) -> IO (SymExpr sym (BaseBVType 8)))
 -> IO (ArrayChunk sym (BaseBVType wptr) (BaseBVType 8)))
-> (SymExpr sym (BaseBVType wptr)
    -> IO (SymExpr sym (BaseBVType 8)))
-> IO (ArrayChunk sym (BaseBVType wptr) (BaseBVType 8))
forall a b. (a -> b) -> a -> b
$ \SymExpr sym (BaseBVType wptr)
offset -> do
    LLVMPointer sym wptr
ptr' <- sym
-> NatRepr wptr
-> LLVMPtr sym wptr
-> SymExpr sym (BaseBVType wptr)
-> IO (LLVMPtr sym wptr)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym
-> NatRepr w -> LLVMPtr sym w -> SymBV sym w -> IO (LLVMPtr sym w)
ptrAdd sym
sym NatRepr wptr
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth LLVMPtr sym wptr
ptr SymExpr sym (BaseBVType wptr)
offset
    LLVMPointer sym 8
llbytes <- bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> TypeRepr (LLVMPointerType 8)
-> Alignment
-> IO (RegValue sym (LLVMPointerType 8))
forall sym bak (wptr :: Natural) (tp :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> TypeRepr tp
-> Alignment
-> IO (RegValue sym tp)
doLoad bak
bak MemImpl sym
mem LLVMPtr sym wptr
LLVMPointer sym wptr
ptr' (Bytes -> StorageType
bitvectorType (Integer -> Bytes
forall a. Integral a => a -> Bytes
toBytes (Integer
1 :: Integer))) (NatRepr 8 -> TypeRepr (LLVMPointerType 8)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr (forall (n :: Natural). KnownNat n => NatRepr n
PN.knownNat @8)) Alignment
noAlignment
    bak
-> RegValue sym (LLVMPointerType 8)
-> IO (SymExpr sym (BaseBVType 8))
forall sym bak (w :: Natural).
IsSymBackend sym bak =>
bak -> LLVMPtr sym w -> IO (SymBV sym w)
projectLLVM_bv bak
bak RegValue sym (LLVMPointerType 8)
LLVMPointer sym 8
llbytes

-- | Retrieve the 'SymIO.FileHandle' that the given descriptor represents,
-- calling the continuation with 'Nothing' if the descriptor does not represent
-- a valid handle. Notably, a successfully resolved handle may itself still be closed.
--
-- Note that the continuation may be called multiple times if it is used within
-- a symbolic branch. As a result, any side effects in the continuation may be
-- performed multiple times.
lookupFileHandle
  :: IsSymInterface sym
  => LLVMFileSystem wptr
  -> W4.SymBV sym 32
  -> RegMap sym args''
  -> (forall args'. Maybe (SymIO.FileHandle sym wptr) -> RegMap sym args'' -> OverrideSim p sym ext r args' ret a)
  -> OverrideSim p sym ext r args ret a
lookupFileHandle :: forall sym (wptr :: Natural) (args'' :: Ctx CrucibleType) p ext r
       (ret :: CrucibleType) a (args :: Ctx CrucibleType).
IsSymInterface sym =>
LLVMFileSystem wptr
-> SymBV sym 32
-> RegMap sym args''
-> (forall (args' :: Ctx CrucibleType).
    Maybe (FileHandle sym wptr)
    -> RegMap sym args'' -> OverrideSim p sym ext r args' ret a)
-> OverrideSim p sym ext r args ret a
lookupFileHandle LLVMFileSystem wptr
fsVars SymBV sym 32
fdesc RegMap sym args''
args forall (args' :: Ctx CrucibleType).
Maybe (FileHandle sym wptr)
-> RegMap sym args'' -> OverrideSim p sym ext r args' ret a
cont = do
  FDescMap sym wptr
descMap <- GlobalVar (FDescMapType wptr)
-> OverrideSim
     p sym ext r args ret (RegValue sym (FDescMapType wptr))
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal (LLVMFileSystem wptr -> GlobalVar (FDescMapType wptr)
forall (ptrW :: Natural).
LLVMFileSystem ptrW -> GlobalVar (FDescMapType ptrW)
llvmFileDescMap LLVMFileSystem wptr
fsVars)
  sym
sym <- OverrideSim p sym ext r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
  (IO
  (PartExpr
     (SymExpr sym BaseBoolType)
     (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))))
-> OverrideSim
     p
     sym
     ext
     r
     args
     ret
     (PartExpr
        (SymExpr sym BaseBoolType)
        (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO
   (PartExpr
      (SymExpr sym BaseBoolType)
      (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))))
 -> OverrideSim
      p
      sym
      ext
      r
      args
      ret
      (PartExpr
         (SymExpr sym BaseBoolType)
         (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr))))))
-> IO
     (PartExpr
        (SymExpr sym BaseBoolType)
        (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))))
-> OverrideSim
     p
     sym
     ext
     r
     args
     ret
     (PartExpr
        (SymExpr sym BaseBoolType)
        (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))))
forall a b. (a -> b) -> a -> b
$ sym
-> SymBV sym 32
-> FDescMap sym wptr
-> IO (PartExpr (SymExpr sym BaseBoolType) (FileHandle sym wptr))
forall sym (ptrW :: Natural).
IsSymInterface sym =>
sym
-> SymBV sym 32
-> FDescMap sym ptrW
-> IO (PartExpr (Pred sym) (FileHandle sym ptrW))
getHandle sym
sym SymBV sym 32
fdesc FDescMap sym wptr
descMap) OverrideSim
  p
  sym
  ext
  r
  args
  ret
  (PartExpr
     (SymExpr sym BaseBoolType)
     (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))))
-> (PartExpr
      (SymExpr sym BaseBoolType)
      (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr))))
    -> OverrideSim p sym ext r args ret a)
-> OverrideSim p sym ext r args ret a
forall a b.
OverrideSim p sym ext r args ret a
-> (a -> OverrideSim p sym ext r args ret b)
-> OverrideSim p sym ext r args ret b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    W4P.PE SymExpr sym BaseBoolType
p MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
fhdl -> do
      SymExpr sym BaseBoolType
-> RegMap sym args''
-> OverrideSim p sym ext r args'' ret a
-> Maybe Position
-> RegMap sym args''
-> OverrideSim p sym ext r args'' ret a
-> Maybe Position
-> OverrideSim p sym ext r args ret a
forall sym (then_args :: Ctx CrucibleType) p ext rtp
       (res :: CrucibleType) a (else_args :: Ctx CrucibleType)
       (args :: Ctx CrucibleType).
IsSymInterface sym =>
Pred sym
-> RegMap sym then_args
-> OverrideSim p sym ext rtp then_args res a
-> Maybe Position
-> RegMap sym else_args
-> OverrideSim p sym ext rtp else_args res a
-> Maybe Position
-> OverrideSim p sym ext rtp args res a
symbolicBranch SymExpr sym BaseBoolType
p
        RegMap sym args''
args (OverrideSim p sym ext r args'' ret (RegMap sym args'')
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (RegMap sym args)
getOverrideArgs OverrideSim p sym ext r args'' ret (RegMap sym args'')
-> (RegMap sym args'' -> OverrideSim p sym ext r args'' ret a)
-> OverrideSim p sym ext r args'' ret a
forall a b.
OverrideSim p sym ext r args'' ret a
-> (a -> OverrideSim p sym ext r args'' ret b)
-> OverrideSim p sym ext r args'' ret b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \RegMap sym args''
args' -> Maybe (FileHandle sym wptr)
-> RegMap sym args'' -> OverrideSim p sym ext r args'' ret a
forall (args' :: Ctx CrucibleType).
Maybe (FileHandle sym wptr)
-> RegMap sym args'' -> OverrideSim p sym ext r args' ret a
cont (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
-> Maybe
     (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr))))
forall a. a -> Maybe a
Just MuxTree sym (RefCell ('MaybeType (FilePointerType wptr)))
fhdl) RegMap sym args''
args') Maybe Position
forall a. Maybe a
Nothing
        RegMap sym args''
args (OverrideSim p sym ext r args'' ret (RegMap sym args'')
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (RegMap sym args)
getOverrideArgs OverrideSim p sym ext r args'' ret (RegMap sym args'')
-> (RegMap sym args'' -> OverrideSim p sym ext r args'' ret a)
-> OverrideSim p sym ext r args'' ret a
forall a b.
OverrideSim p sym ext r args'' ret a
-> (a -> OverrideSim p sym ext r args'' ret b)
-> OverrideSim p sym ext r args'' ret b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \RegMap sym args''
args' -> Maybe (FileHandle sym wptr)
-> RegMap sym args'' -> OverrideSim p sym ext r args'' ret a
forall (args' :: Ctx CrucibleType).
Maybe (FileHandle sym wptr)
-> RegMap sym args'' -> OverrideSim p sym ext r args' ret a
cont Maybe (FileHandle sym wptr)
forall a. Maybe a
Nothing RegMap sym args''
args') Maybe Position
forall a. Maybe a
Nothing
    PartExpr
  (SymExpr sym BaseBoolType)
  (MuxTree sym (RefCell ('MaybeType (FilePointerType wptr))))
W4P.Unassigned -> Maybe (FileHandle sym wptr)
-> RegMap sym args'' -> OverrideSim p sym ext r args ret a
forall (args' :: Ctx CrucibleType).
Maybe (FileHandle sym wptr)
-> RegMap sym args'' -> OverrideSim p sym ext r args' ret a
cont Maybe (FileHandle sym wptr)
forall a. Maybe a
Nothing RegMap sym args''
args


-- | Allocate a fresh (integer/bitvector(32)) file descriptor that is associated with the given 'SymIO.FileHandle'
--
-- NOTE that this is a file descriptor in the POSIX sense, rather than a @FILE*@
-- or the underlying 'SymIO.FileHandle'.
--
-- NOTE that we truncate the file descriptor source to 32 bits in this function;
-- it could in theory overflow.
--
-- NOTE that the file descriptor counter is incremented monotonically as the
-- simulator hits calls to @open@; this means that calls to @open@ in parallel
-- control flow branches would get sequential file descriptor values whereas the
-- real program would likely allocate the same file descriptor value on both
-- branches. This could be relevant for some bug finding scenarios.
--
-- TODO It would be interesting if we could add a symbolic offset to these
-- values so that we can't make any concrete assertions about them. It isn't
-- clear if that ever happens in real code. If we do that, we need an escape
-- hatch to let us allocate file descriptors 0, 1, and 2 if needed.
allocateFileDescriptor
  :: (IsSymInterface sym, HasPtrWidth wptr)
  => LLVMFileSystem wptr
  -> SymIO.FileHandle sym wptr
  -> OverrideSim p sym ext r args ret (W4.SymBV sym 32)
allocateFileDescriptor :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
LLVMFileSystem wptr
-> FileHandle sym wptr
-> OverrideSim p sym ext r args ret (SymBV sym 32)
allocateFileDescriptor LLVMFileSystem wptr
fsVars FileHandle sym wptr
fh = do
  sym
sym <- OverrideSim p sym ext r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
  GlobalVar (FDescMapType wptr)
-> (RegValue sym (FDescMapType wptr)
    -> OverrideSim
         p
         sym
         ext
         r
         args
         ret
         (SymBV sym 32, RegValue sym (FDescMapType wptr)))
-> OverrideSim p sym ext r args ret (SymBV sym 32)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal (LLVMFileSystem wptr -> GlobalVar (FDescMapType wptr)
forall (ptrW :: Natural).
LLVMFileSystem ptrW -> GlobalVar (FDescMapType ptrW)
llvmFileDescMap LLVMFileSystem wptr
fsVars) ((RegValue sym (FDescMapType wptr)
  -> OverrideSim
       p
       sym
       ext
       r
       args
       ret
       (SymBV sym 32, RegValue sym (FDescMapType wptr)))
 -> OverrideSim p sym ext r args ret (SymBV sym 32))
-> (RegValue sym (FDescMapType wptr)
    -> OverrideSim
         p
         sym
         ext
         r
         args
         ret
         (SymBV sym 32, RegValue sym (FDescMapType wptr)))
-> OverrideSim p sym ext r args ret (SymBV sym 32)
forall a b. (a -> b) -> a -> b
$ \(FDescMap Natural
next Map Natural (PartExpr (Pred sym) (FileHandle sym wptr))
descMap) -> do
    SymBV sym 32
fdesc <-  IO (SymBV sym 32)
-> OverrideSim p sym ext r args ret (SymBV sym 32)
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymBV sym 32)
 -> OverrideSim p sym ext r args ret (SymBV sym 32))
-> IO (SymBV sym 32)
-> OverrideSim p sym ext r args ret (SymBV sym 32)
forall a b. (a -> b) -> a -> b
$ sym -> NatRepr 32 -> BV 32 -> IO (SymBV sym 32)
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym (forall (n :: Natural). KnownNat n => NatRepr n
PN.knownNat @32) (NatRepr 32 -> Integer -> BV 32
forall (w :: Natural). NatRepr w -> Integer -> BV w
BVS.mkBV (forall (n :: Natural). KnownNat n => NatRepr n
PN.knownNat @32) (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
next))
    let ptrMap' :: Map Natural (PartExpr (Pred sym) (FileHandle sym wptr))
ptrMap' = Natural
-> PartExpr (Pred sym) (FileHandle sym wptr)
-> Map Natural (PartExpr (Pred sym) (FileHandle sym wptr))
-> Map Natural (PartExpr (Pred sym) (FileHandle sym wptr))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Natural
next (sym
-> FileHandle sym wptr -> PartExpr (Pred sym) (FileHandle sym wptr)
forall sym v.
IsExprBuilder sym =>
sym -> v -> PartExpr (Pred sym) v
W4P.justPartExpr sym
sym FileHandle sym wptr
fh) Map Natural (PartExpr (Pred sym) (FileHandle sym wptr))
descMap
    (SymBV sym 32, FDescMap sym wptr)
-> OverrideSim
     p sym ext r args ret (SymBV sym 32, FDescMap sym wptr)
forall a. a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymBV sym 32
fdesc, Natural
-> Map Natural (PartExpr (Pred sym) (FileHandle sym wptr))
-> FDescMap sym wptr
forall sym (ptrW :: Natural).
Natural
-> Map Natural (PartExpr (Pred sym) (FileHandle sym ptrW))
-> FDescMap sym ptrW
FDescMap (Natural
next Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
1) Map Natural (PartExpr (Pred sym) (FileHandle sym wptr))
ptrMap')

loadFileIdent
  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions)
  => GlobalVar Mem
  -> LLVMPtr sym wptr
  -> OverrideSim p sym ext r args ret (SymIO.FileIdent sym)
loadFileIdent :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> LLVMPtr sym wptr
-> OverrideSim p sym ext r args ret (FileIdent sym)
loadFileIdent GlobalVar Mem
memOps LLVMPtr sym wptr
filename_ptr =
  (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext r args ret (FileIdent sym))
-> OverrideSim p sym ext r args ret (FileIdent sym)
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym ext r args ret (FileIdent sym))
 -> OverrideSim p sym ext r args ret (FileIdent sym))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext r args ret (FileIdent sym))
-> OverrideSim p sym ext r args ret (FileIdent sym)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
   do MemImpl sym
mem <- GlobalVar Mem
-> OverrideSim p sym ext r args ret (RegValue sym Mem)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal GlobalVar Mem
memOps
      [Word8]
filename_bytes <- IO [Word8] -> OverrideSim p sym ext r args ret [Word8]
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO [Word8] -> OverrideSim p sym ext r args ret [Word8])
-> IO [Word8] -> OverrideSim p sym ext r args ret [Word8]
forall a b. (a -> b) -> a -> b
$ bak -> MemImpl sym -> LLVMPtr sym wptr -> Maybe Int -> IO [Word8]
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, HasCallStack) =>
bak -> MemImpl sym -> LLVMPtr sym wptr -> Maybe Int -> IO [Word8]
loadString bak
bak MemImpl sym
mem LLVMPtr sym wptr
filename_ptr Maybe Int
forall a. Maybe a
Nothing
      IO (SymExpr sym (BaseStringType 'Char8))
-> OverrideSim
     p sym ext r args ret (SymExpr sym (BaseStringType 'Char8))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseStringType 'Char8))
 -> OverrideSim
      p sym ext r args ret (SymExpr sym (BaseStringType 'Char8)))
-> IO (SymExpr sym (BaseStringType 'Char8))
-> OverrideSim
     p sym ext r args ret (SymExpr sym (BaseStringType 'Char8))
forall a b. (a -> b) -> a -> b
$ sym
-> StringLiteral 'Char8 -> IO (SymExpr sym (BaseStringType 'Char8))
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
forall (si :: StringInfo).
sym -> StringLiteral si -> IO (SymString sym si)
W4.stringLit (bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak) (ByteString -> StringLiteral 'Char8
W4.Char8Literal ([Word8] -> ByteString
BS.pack [Word8]
filename_bytes))

returnIOError32
  :: IsSymInterface sym
  => OverrideSim p sym ext r args ret (W4.SymBV sym 32)
returnIOError32 :: forall sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
OverrideSim p sym ext r args ret (SymBV sym 32)
returnIOError32 = do
  sym
sym <- OverrideSim p sym ext r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
  IO (SymBV sym 32)
-> OverrideSim p sym ext r args ret (SymBV sym 32)
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymBV sym 32)
 -> OverrideSim p sym ext r args ret (SymBV sym 32))
-> IO (SymBV sym 32)
-> OverrideSim p sym ext r args ret (SymBV sym 32)
forall a b. (a -> b) -> a -> b
$ sym -> NatRepr 32 -> BV 32 -> IO (SymBV sym 32)
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym (forall (n :: Natural). KnownNat n => NatRepr n
PN.knownNat @32) (NatRepr 32 -> Integer -> BV 32
forall (w :: Natural). NatRepr w -> Integer -> BV w
BVS.mkBV (forall (n :: Natural). KnownNat n => NatRepr n
PN.knownNat @32) (-Integer
1))

returnIOError
  :: forall wptr p sym ext r args ret
  . (IsSymInterface sym, HasPtrWidth wptr)
  => OverrideSim p sym ext r args ret (W4.SymBV sym wptr)
returnIOError :: forall (wptr :: Natural) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
OverrideSim p sym ext r args ret (SymBV sym wptr)
returnIOError = do
  sym
sym <- OverrideSim p sym ext r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
  IO (SymBV sym wptr)
-> OverrideSim p sym ext r args ret (SymBV sym wptr)
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymBV sym wptr)
 -> OverrideSim p sym ext r args ret (SymBV sym wptr))
-> IO (SymBV sym wptr)
-> OverrideSim p sym ext r args ret (SymBV sym wptr)
forall a b. (a -> b) -> a -> b
$ sym -> NatRepr wptr -> BV wptr -> IO (SymBV sym wptr)
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym NatRepr wptr
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BVS.mkBV NatRepr wptr
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth (-Integer
1))

openFile
  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions)
  => LLVMFileSystem wptr
  -> LLVMOverride p sym ext
           (EmptyCtx ::> LLVMPointerType wptr
                     ::> BVType 32)
           (BVType 32)
openFile :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMFileSystem wptr
-> LLVMOverride
     p
     sym
     ext
     ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
     (BVType 32)
openFile LLVMFileSystem wptr
fsVars =
  [llvmOvr| i32 @open( i8*, i32 ) |]
  -- TODO add mode support by making this a varargs function
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym) ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
args -> CurryAssignment
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
  (RegEntry sym)
  (OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32)))
-> Assignment
     (RegEntry sym) ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32) f x
-> Assignment f ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
-> x
uncurryAssignment (GlobalVar Mem
-> LLVMFileSystem wptr
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType 32)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall sym (wptr :: Natural) p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> LLVMFileSystem wptr
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType 32)
-> OverrideSim p sym ext rtp args ret (RegValue sym (BVType 32))
callOpenFile GlobalVar Mem
memOps LLVMFileSystem wptr
fsVars) Assignment
  (RegEntry sym) ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
args)

callOpenFile ::
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) =>
  GlobalVar Mem ->
  LLVMFileSystem wptr ->
  RegEntry sym (LLVMPointerType wptr) ->
  RegEntry sym (BVType 32) ->
  OverrideSim p sym ext rtp args ret (RegValue sym (BVType 32))
callOpenFile :: forall sym (wptr :: Natural) p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> LLVMFileSystem wptr
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType 32)
-> OverrideSim p sym ext rtp args ret (RegValue sym (BVType 32))
callOpenFile GlobalVar Mem
memOps LLVMFileSystem wptr
fsVars RegEntry sym (LLVMPointerType wptr)
filename_ptr RegEntry sym (BVType 32)
_flags =
  do SymExpr sym (BaseStringType 'Char8)
fileIdent <- GlobalVar Mem
-> LLVMPtr sym wptr
-> OverrideSim p sym ext rtp args ret (FileIdent sym)
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> LLVMPtr sym wptr
-> OverrideSim p sym ext r args ret (FileIdent sym)
loadFileIdent GlobalVar Mem
memOps (RegEntry sym (LLVMPointerType wptr) -> LLVMPtr sym wptr
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym (LLVMPointerType wptr)
filename_ptr)
     GlobalVar (FileSystemType wptr)
-> FileIdent sym
-> (forall {args' :: Ctx CrucibleType}.
    Either FileIdentError (FileHandle sym wptr)
    -> OverrideSim
         p sym ext rtp args' ret (SymExpr sym (BaseBVType 32)))
-> OverrideSim p sym ext rtp args ret (SymExpr sym (BaseBVType 32))
forall sym (wptr :: Natural) p arch r (ret :: CrucibleType) a
       (args :: Ctx CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileIdent sym
-> (forall (args' :: Ctx CrucibleType).
    Either FileIdentError (FileHandle sym wptr)
    -> OverrideSim p sym arch r args' ret a)
-> OverrideSim p sym arch r args ret a
SymIO.openFile (LLVMFileSystem wptr -> GlobalVar (FileSystemType wptr)
forall (ptrW :: Natural).
LLVMFileSystem ptrW -> GlobalVar (FileSystemType ptrW)
llvmFileSystem LLVMFileSystem wptr
fsVars) FileIdent sym
SymExpr sym (BaseStringType 'Char8)
fileIdent ((forall {args' :: Ctx CrucibleType}.
  Either FileIdentError (FileHandle sym wptr)
  -> OverrideSim
       p sym ext rtp args' ret (SymExpr sym (BaseBVType 32)))
 -> OverrideSim
      p sym ext rtp args ret (SymExpr sym (BaseBVType 32)))
-> (forall {args' :: Ctx CrucibleType}.
    Either FileIdentError (FileHandle sym wptr)
    -> OverrideSim
         p sym ext rtp args' ret (SymExpr sym (BaseBVType 32)))
-> OverrideSim p sym ext rtp args ret (SymExpr sym (BaseBVType 32))
forall a b. (a -> b) -> a -> b
$ \case
       Left FileIdentError
SymIO.FileNotFound -> OverrideSim p sym ext rtp args' ret (SymExpr sym (BaseBVType 32))
forall sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
OverrideSim p sym ext r args ret (SymBV sym 32)
returnIOError32
       Right FileHandle sym wptr
fileHandle -> LLVMFileSystem wptr
-> FileHandle sym wptr
-> OverrideSim
     p sym ext rtp args' ret (SymExpr sym (BaseBVType 32))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
LLVMFileSystem wptr
-> FileHandle sym wptr
-> OverrideSim p sym ext r args ret (SymBV sym 32)
allocateFileDescriptor LLVMFileSystem wptr
fsVars FileHandle sym wptr
fileHandle

closeFile
  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
  => LLVMFileSystem wptr
  -> LLVMOverride p sym ext
           (EmptyCtx ::> BVType 32)
           (BVType 32)
closeFile :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMFileSystem wptr
-> LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
closeFile LLVMFileSystem wptr
fsVars =
  [llvmOvr| i32 @close( i32 ) |]
  (\GlobalVar Mem
memOps Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
args -> CurryAssignment
  (EmptyCtx ::> BVType 32)
  (RegEntry sym)
  (OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32)))
-> Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> BVType 32) f x
-> Assignment f (EmptyCtx ::> BVType 32) -> x
uncurryAssignment (GlobalVar Mem
-> LLVMFileSystem wptr
-> RegEntry sym (BVType 32)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall sym (wptr :: Natural) p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
GlobalVar Mem
-> LLVMFileSystem wptr
-> RegEntry sym (BVType 32)
-> OverrideSim p sym ext rtp args ret (RegValue sym (BVType 32))
callCloseFile GlobalVar Mem
memOps LLVMFileSystem wptr
fsVars) Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
args)

callCloseFile ::
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
  GlobalVar Mem ->
  LLVMFileSystem wptr ->
  RegEntry sym (BVType 32) ->
  OverrideSim p sym ext rtp args ret (RegValue sym (BVType 32))
callCloseFile :: forall sym (wptr :: Natural) p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
GlobalVar Mem
-> LLVMFileSystem wptr
-> RegEntry sym (BVType 32)
-> OverrideSim p sym ext rtp args ret (RegValue sym (BVType 32))
callCloseFile GlobalVar Mem
_memOps LLVMFileSystem wptr
fsVars RegEntry sym (BVType 32)
filedesc =
  do sym
sym <- OverrideSim p sym ext rtp args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
     LLVMFileSystem wptr
-> SymExpr sym (BaseBVType 32)
-> RegMap sym EmptyCtx
-> (forall {args' :: Ctx CrucibleType}.
    Maybe (FileHandle sym wptr)
    -> RegMap sym EmptyCtx
    -> OverrideSim
         p sym ext rtp args' ret (SymExpr sym (BaseBVType 32)))
-> OverrideSim p sym ext rtp args ret (SymExpr sym (BaseBVType 32))
forall sym (wptr :: Natural) (args'' :: Ctx CrucibleType) p ext r
       (ret :: CrucibleType) a (args :: Ctx CrucibleType).
IsSymInterface sym =>
LLVMFileSystem wptr
-> SymBV sym 32
-> RegMap sym args''
-> (forall (args' :: Ctx CrucibleType).
    Maybe (FileHandle sym wptr)
    -> RegMap sym args'' -> OverrideSim p sym ext r args' ret a)
-> OverrideSim p sym ext r args ret a
lookupFileHandle LLVMFileSystem wptr
fsVars (RegEntry sym (BVType 32) -> RegValue sym (BVType 32)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym (BVType 32)
filedesc) RegMap sym EmptyCtx
forall sym. RegMap sym EmptyCtx
emptyRegMap ((forall {args' :: Ctx CrucibleType}.
  Maybe (FileHandle sym wptr)
  -> RegMap sym EmptyCtx
  -> OverrideSim
       p sym ext rtp args' ret (SymExpr sym (BaseBVType 32)))
 -> OverrideSim
      p sym ext rtp args ret (SymExpr sym (BaseBVType 32)))
-> (forall {args' :: Ctx CrucibleType}.
    Maybe (FileHandle sym wptr)
    -> RegMap sym EmptyCtx
    -> OverrideSim
         p sym ext rtp args' ret (SymExpr sym (BaseBVType 32)))
-> OverrideSim p sym ext rtp args ret (SymExpr sym (BaseBVType 32))
forall a b. (a -> b) -> a -> b
$ \case
       Just FileHandle sym wptr
fileHandle -> \RegMap sym EmptyCtx
_ ->
         GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> (forall {args' :: Ctx CrucibleType}.
    Maybe FileHandleError
    -> OverrideSim
         p sym ext rtp args' ret (SymExpr sym (BaseBVType 32)))
-> OverrideSim
     p sym ext rtp args' ret (SymExpr sym (BaseBVType 32))
forall sym (wptr :: Natural) p arch r (ret :: CrucibleType) a
       (args :: Ctx CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> (forall (args' :: Ctx CrucibleType).
    Maybe FileHandleError -> OverrideSim p sym arch r args' ret a)
-> OverrideSim p sym arch r args ret a
SymIO.closeFileHandle (LLVMFileSystem wptr -> GlobalVar (FileSystemType wptr)
forall (ptrW :: Natural).
LLVMFileSystem ptrW -> GlobalVar (FileSystemType ptrW)
llvmFileSystem LLVMFileSystem wptr
fsVars) FileHandle sym wptr
fileHandle ((forall {args' :: Ctx CrucibleType}.
  Maybe FileHandleError
  -> OverrideSim
       p sym ext rtp args' ret (SymExpr sym (BaseBVType 32)))
 -> OverrideSim
      p sym ext rtp args' ret (SymExpr sym (BaseBVType 32)))
-> (forall {args' :: Ctx CrucibleType}.
    Maybe FileHandleError
    -> OverrideSim
         p sym ext rtp args' ret (SymExpr sym (BaseBVType 32)))
-> OverrideSim
     p sym ext rtp args' ret (SymExpr sym (BaseBVType 32))
forall a b. (a -> b) -> a -> b
$ \case
           Just FileHandleError
SymIO.FileHandleClosed -> OverrideSim p sym ext rtp args' ret (SymExpr sym (BaseBVType 32))
forall sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
OverrideSim p sym ext r args ret (SymBV sym 32)
returnIOError32
           Maybe FileHandleError
Nothing -> IO (SymExpr sym (BaseBVType 32))
-> OverrideSim
     p sym ext rtp args' ret (SymExpr sym (BaseBVType 32))
forall a. IO a -> OverrideSim p sym ext rtp args' ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseBVType 32))
 -> OverrideSim
      p sym ext rtp args' ret (SymExpr sym (BaseBVType 32)))
-> IO (SymExpr sym (BaseBVType 32))
-> OverrideSim
     p sym ext rtp args' ret (SymExpr sym (BaseBVType 32))
forall a b. (a -> b) -> a -> b
$ sym -> NatRepr 32 -> BV 32 -> IO (SymExpr sym (BaseBVType 32))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym (forall (n :: Natural). KnownNat n => NatRepr n
PN.knownNat @32) (NatRepr 32 -> Integer -> BV 32
forall (w :: Natural). NatRepr w -> Integer -> BV w
BVS.mkBV (forall (n :: Natural). KnownNat n => NatRepr n
PN.knownNat @32) Integer
0)
       Maybe (FileHandle sym wptr)
Nothing -> \RegMap sym EmptyCtx
_ -> OverrideSim p sym ext rtp args' ret (SymExpr sym (BaseBVType 32))
forall sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
OverrideSim p sym ext r args ret (SymBV sym 32)
returnIOError32

readFileHandle
  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
  => LLVMFileSystem wptr
  -> LLVMOverride p sym ext
           (EmptyCtx ::> BVType 32
                     ::> LLVMPointerType wptr
                     ::> BVType wptr)
           (BVType wptr)
readFileHandle :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMFileSystem wptr
-> LLVMOverride
     p
     sym
     ext
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
     (BVType wptr)
readFileHandle LLVMFileSystem wptr
fsVars =
  [llvmOvr| ssize_t @read( i32, i8*, size_t ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args -> CurryAssignment
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (RegEntry sym)
  (OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType wptr)))
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (BVType wptr))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  f
  x
-> Assignment
     f
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
-> x
uncurryAssignment (GlobalVar Mem
-> LLVMFileSystem wptr
-> RegEntry sym (BVType 32)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (BVType wptr))
forall sym (wptr :: Natural) p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
GlobalVar Mem
-> LLVMFileSystem wptr
-> RegEntry sym (BVType 32)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext rtp args ret (RegValue sym (BVType wptr))
callReadFileHandle GlobalVar Mem
memOps LLVMFileSystem wptr
fsVars) Assignment
  (RegEntry sym)
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args)

callReadFileHandle ::
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
  GlobalVar Mem ->
  LLVMFileSystem wptr ->
  RegEntry sym (BVType 32) ->
  RegEntry sym (LLVMPointerType wptr) ->
  RegEntry sym (BVType wptr) ->
  OverrideSim p sym ext rtp args ret (RegValue sym (BVType wptr))
callReadFileHandle :: forall sym (wptr :: Natural) p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
GlobalVar Mem
-> LLVMFileSystem wptr
-> RegEntry sym (BVType 32)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext rtp args ret (RegValue sym (BVType wptr))
callReadFileHandle GlobalVar Mem
memOps LLVMFileSystem wptr
fsVars RegEntry sym (BVType 32)
filedesc RegEntry sym (LLVMPointerType wptr)
buf RegEntry sym (BVType wptr)
count =
  do sym
sym <- OverrideSim p sym ext rtp args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
     let args :: Assignment
  (RegEntry sym)
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args = Assignment (RegEntry sym) EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment (RegEntry sym) EmptyCtx
-> RegEntry sym (BVType 32)
-> Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RegEntry sym (BVType 32)
filedesc Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
-> RegEntry sym (LLVMPointerType wptr)
-> Assignment
     (RegEntry sym) ((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RegEntry sym (LLVMPointerType wptr)
buf Assignment
  (RegEntry sym) ((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RegEntry sym (BVType wptr)
count
     LLVMFileSystem wptr
-> SymBV sym 32
-> RegMap
     sym
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
-> (forall {args' :: Ctx CrucibleType}.
    Maybe (FileHandle sym wptr)
    -> RegMap
         sym
         (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
          ::> BVType wptr)
    -> OverrideSim
         p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
-> OverrideSim
     p sym ext rtp args ret (SymExpr sym ('BaseBVType wptr))
forall sym (wptr :: Natural) (args'' :: Ctx CrucibleType) p ext r
       (ret :: CrucibleType) a (args :: Ctx CrucibleType).
IsSymInterface sym =>
LLVMFileSystem wptr
-> SymBV sym 32
-> RegMap sym args''
-> (forall (args' :: Ctx CrucibleType).
    Maybe (FileHandle sym wptr)
    -> RegMap sym args'' -> OverrideSim p sym ext r args' ret a)
-> OverrideSim p sym ext r args ret a
lookupFileHandle LLVMFileSystem wptr
fsVars (RegEntry sym (BVType 32) -> RegValue sym (BVType 32)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym (BVType 32)
filedesc) (Assignment
  (RegEntry sym)
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
-> RegMap
     sym
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap Assignment
  (RegEntry sym)
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args) ((forall {args' :: Ctx CrucibleType}.
  Maybe (FileHandle sym wptr)
  -> RegMap
       sym
       (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
        ::> BVType wptr)
  -> OverrideSim
       p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
 -> OverrideSim
      p sym ext rtp args ret (SymExpr sym ('BaseBVType wptr)))
-> (forall {args' :: Ctx CrucibleType}.
    Maybe (FileHandle sym wptr)
    -> RegMap
         sym
         (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
          ::> BVType wptr)
    -> OverrideSim
         p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
-> OverrideSim
     p sym ext rtp args ret (SymExpr sym ('BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ \case
       Just FileHandle sym wptr
fileHandle -> \(RegMap (Assignment (RegEntry sym) ctx
Empty :> RegEntry sym tp
_ :> RegEntry sym tp
buffer_ptr :> RegEntry sym tp
size)) ->
         GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> SymExpr sym ('BaseBVType wptr)
-> (forall {args' :: Ctx CrucibleType}.
    Either
      FileHandleError
      (DataChunk sym wptr, SymExpr sym ('BaseBVType wptr))
    -> OverrideSim
         p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
-> OverrideSim
     p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr))
forall sym (wptr :: Natural) p arch r (ret :: CrucibleType) a
       (args :: Ctx CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> SymBV sym wptr
-> (forall (args' :: Ctx CrucibleType).
    Either FileHandleError (DataChunk sym wptr, SymBV sym wptr)
    -> OverrideSim p sym arch r args' ret a)
-> OverrideSim p sym arch r args ret a
SymIO.readChunk (LLVMFileSystem wptr -> GlobalVar (FileSystemType wptr)
forall (ptrW :: Natural).
LLVMFileSystem ptrW -> GlobalVar (FileSystemType ptrW)
llvmFileSystem LLVMFileSystem wptr
fsVars) FileHandle sym wptr
fileHandle (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
size) ((forall {args' :: Ctx CrucibleType}.
  Either
    FileHandleError
    (DataChunk sym wptr, SymExpr sym ('BaseBVType wptr))
  -> OverrideSim
       p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
 -> OverrideSim
      p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
-> (forall {args' :: Ctx CrucibleType}.
    Either
      FileHandleError
      (DataChunk sym wptr, SymExpr sym ('BaseBVType wptr))
    -> OverrideSim
         p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
-> OverrideSim
     p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ \case
           Left FileHandleError
SymIO.FileHandleClosed -> OverrideSim
  p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr))
forall (wptr :: Natural) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
OverrideSim p sym ext r args ret (SymBV sym wptr)
returnIOError
           Right (DataChunk sym wptr
chunk, SymExpr sym ('BaseBVType wptr)
bytesRead) -> do
             (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim
      p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
-> OverrideSim
     p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim
       p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
 -> OverrideSim
      p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
-> OverrideSim
     p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
               GlobalVar Mem
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         rtp
         args'
         ret
         (SymExpr sym ('BaseBVType wptr), RegValue sym Mem))
-> OverrideSim
     p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr))
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal GlobalVar Mem
memOps ((RegValue sym Mem
  -> OverrideSim
       p
       sym
       ext
       rtp
       args'
       ret
       (SymExpr sym ('BaseBVType wptr), RegValue sym Mem))
 -> OverrideSim
      p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         rtp
         args'
         ret
         (SymExpr sym ('BaseBVType wptr), RegValue sym Mem))
-> OverrideSim
     p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ \RegValue sym Mem
mem -> IO (SymExpr sym ('BaseBVType wptr), RegValue sym Mem)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret
     (SymExpr sym ('BaseBVType wptr), RegValue sym Mem)
forall a. IO a -> OverrideSim p sym ext rtp args' ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym ('BaseBVType wptr), RegValue sym Mem)
 -> OverrideSim
      p
      sym
      ext
      rtp
      args'
      ret
      (SymExpr sym ('BaseBVType wptr), RegValue sym Mem))
-> IO (SymExpr sym ('BaseBVType wptr), RegValue sym Mem)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret
     (SymExpr sym ('BaseBVType wptr), RegValue sym Mem)
forall a b. (a -> b) -> a -> b
$ do
                 SymExpr
  sym (BaseArrayType (EmptyCtx ::> 'BaseBVType wptr) (BaseBVType 8))
chunkArray <- sym
-> BaseTypeRepr ('BaseBVType wptr)
-> DataChunk sym wptr
-> IO
     (SymExpr
        sym (BaseArrayType (EmptyCtx ::> 'BaseBVType wptr) (BaseBVType 8)))
forall sym (idx :: BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> BaseTypeRepr idx
-> ArrayChunk sym idx tp
-> IO (SymArray sym (EmptyCtx ::> idx) tp)
SymIO.chunkToArray sym
sym (NatRepr wptr -> BaseTypeRepr ('BaseBVType wptr)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr NatRepr wptr
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth) DataChunk sym wptr
chunk
                 MemImpl sym
mem' <- bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> Alignment
-> SymExpr
     sym (BaseArrayType (EmptyCtx ::> 'BaseBVType wptr) (BaseBVType 8))
-> SymExpr sym ('BaseBVType wptr)
-> IO (MemImpl sym)
forall sym bak (w :: Natural).
(IsSymBackend sym bak, HasPtrWidth w, HasLLVMAnn sym) =>
bak
-> MemImpl sym
-> LLVMPtr sym w
-> Alignment
-> SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
-> SymBV sym w
-> IO (MemImpl sym)
doArrayStore bak
bak RegValue sym Mem
MemImpl sym
mem (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
buffer_ptr) Alignment
noAlignment SymExpr
  sym (BaseArrayType (EmptyCtx ::> 'BaseBVType wptr) (BaseBVType 8))
chunkArray SymExpr sym ('BaseBVType wptr)
bytesRead
                 (SymExpr sym ('BaseBVType wptr), MemImpl sym)
-> IO (SymExpr sym ('BaseBVType wptr), MemImpl sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymExpr sym ('BaseBVType wptr)
bytesRead, MemImpl sym
mem')
       Maybe (FileHandle sym wptr)
Nothing -> \RegMap
  sym
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
_ -> OverrideSim
  p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr))
forall (wptr :: Natural) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
OverrideSim p sym ext r args ret (SymBV sym wptr)
returnIOError

-- | If the write is to a concrete FD for which we have an associated 'IO.Handle', mirror the write to that Handle
--
-- This is intended to support mirroring stdout/stderr in a user-visible way
-- (noting that symbolic IO can be repeated due to the simulator branching).
-- Note also that only writes of a concrete length are mirrored reasonably;
-- writes with symbolic length are denoted with a substitute token. Likewise
-- individual symbolic bytes are printed as @?@ characters.
doConcreteWrite
  :: (IsSymInterface sym, HasPtrWidth wptr)
  => PN.NatRepr wptr
  -> Map.Map Natural IO.Handle
  -> RegValue sym (BVType 32)
  -> SymIO.DataChunk sym wptr
  -> RegEntry sym (BVType wptr)
  -> OverrideSim p sym ext rtp args ret ()
doConcreteWrite :: forall sym (wptr :: Natural) p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
NatRepr wptr
-> Map Natural Handle
-> RegValue sym (BVType 32)
-> DataChunk sym wptr
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext rtp args ret ()
doConcreteWrite NatRepr wptr
ptrw Map Natural Handle
handles RegValue sym (BVType 32)
symFD DataChunk sym wptr
chunk RegEntry sym (BVType wptr)
size =
  case SymExpr sym (BaseBVType 32) -> Maybe (BV 32)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
W4.asBV RegValue sym (BVType 32)
SymExpr sym (BaseBVType 32)
symFD of
    Just (BV 32 -> Natural
forall (w :: Natural). BV w -> Natural
BVS.asNatural -> Natural
fd)
      | Just Handle
hdl <- Natural -> Map Natural Handle -> Maybe Handle
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Natural
fd Map Natural Handle
handles
      , Just Integer
numBytes <- BV wptr -> Integer
forall (w :: Natural). BV w -> Integer
BVS.asUnsigned (BV wptr -> Integer) -> Maybe (BV wptr) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymExpr sym (BaseBVType wptr) -> Maybe (BV wptr)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
W4.asBV (RegEntry sym (BVType wptr) -> RegValue sym (BVType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym (BVType wptr)
size) -> do
          -- We have a concrete size of the write and an IO Handle to write
          -- to. Write each byte that is concrete, or replace it with a '?'
          sym
sym <- OverrideSim p sym ext rtp args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
          [Integer]
-> (Integer -> OverrideSim p sym ext rtp args ret ())
-> OverrideSim p sym ext rtp args ret ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
F.forM_ [Integer
0..Integer
numBytes Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1] ((Integer -> OverrideSim p sym ext rtp args ret ())
 -> OverrideSim p sym ext rtp args ret ())
-> (Integer -> OverrideSim p sym ext rtp args ret ())
-> OverrideSim p sym ext rtp args ret ()
forall a b. (a -> b) -> a -> b
$ \Integer
idx -> do
            SymExpr sym (BaseBVType wptr)
idxBV <- IO (SymExpr sym (BaseBVType wptr))
-> OverrideSim
     p sym ext rtp args ret (SymExpr sym (BaseBVType wptr))
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseBVType wptr))
 -> OverrideSim
      p sym ext rtp args ret (SymExpr sym (BaseBVType wptr)))
-> IO (SymExpr sym (BaseBVType wptr))
-> OverrideSim
     p sym ext rtp args ret (SymExpr sym (BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ sym
-> NatRepr wptr -> BV wptr -> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit sym
sym NatRepr wptr
ptrw (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BVS.mkBV NatRepr wptr
ptrw Integer
idx)
            SymExpr sym (BaseBVType 8)
byteVal <- IO (SymExpr sym (BaseBVType 8))
-> OverrideSim p sym ext rtp args ret (SymExpr sym (BaseBVType 8))
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseBVType 8))
 -> OverrideSim p sym ext rtp args ret (SymExpr sym (BaseBVType 8)))
-> IO (SymExpr sym (BaseBVType 8))
-> OverrideSim p sym ext rtp args ret (SymExpr sym (BaseBVType 8))
forall a b. (a -> b) -> a -> b
$ DataChunk sym wptr
-> SymExpr sym (BaseBVType wptr) -> IO (SymExpr sym (BaseBVType 8))
forall sym (idx :: BaseType) (tp :: BaseType).
ArrayChunk sym idx tp -> SymExpr sym idx -> IO (SymExpr sym tp)
SymIO.evalChunk DataChunk sym wptr
chunk SymExpr sym (BaseBVType wptr)
idxBV
            case SymExpr sym (BaseBVType 8) -> Maybe (BV 8)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
W4.asBV SymExpr sym (BaseBVType 8)
byteVal of
              Just (BV 8 -> Integer
forall (w :: Natural). BV w -> Integer
BVS.asUnsigned -> Integer
concByte) -> IO () -> OverrideSim p sym ext rtp args ret ()
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim p sym ext rtp args ret ())
-> IO () -> OverrideSim p sym ext rtp args ret ()
forall a b. (a -> b) -> a -> b
$ Handle -> ByteString -> IO ()
BS.hPut Handle
hdl ([Word8] -> ByteString
BS.pack [Integer -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
concByte])
              Maybe (BV 8)
Nothing -> IO () -> OverrideSim p sym ext rtp args ret ()
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim p sym ext rtp args ret ())
-> IO () -> OverrideSim p sym ext rtp args ret ()
forall a b. (a -> b) -> a -> b
$ Handle -> ByteString -> IO ()
BS.hPut Handle
hdl (String -> ByteString
BSC.pack [Char
'?'])
      | Just Handle
hdl <- Natural -> Map Natural Handle -> Maybe Handle
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Natural
fd Map Natural Handle
handles -> do
          -- In this case, we have a write of symbolic size.  We can't really
          -- write that out, but do our best
          IO () -> OverrideSim p sym ext rtp args ret ()
forall a. IO a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim p sym ext rtp args ret ())
-> IO () -> OverrideSim p sym ext rtp args ret ()
forall a b. (a -> b) -> a -> b
$ Handle -> Text -> IO ()
Text.IO.hPutStr Handle
hdl (String -> Text
Text.pack String
"[‽]")
    Maybe (BV 32)
_ -> () -> OverrideSim p sym ext rtp args ret ()
forall a. a -> OverrideSim p sym ext rtp args ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()

writeFileHandle
  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions)
  => LLVMFileSystem wptr
  -> LLVMOverride p sym ext
           (EmptyCtx ::> BVType 32
                     ::> LLVMPointerType wptr
                     ::> BVType wptr)
           (BVType wptr)
writeFileHandle :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMFileSystem wptr
-> LLVMOverride
     p
     sym
     ext
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
     (BVType wptr)
writeFileHandle LLVMFileSystem wptr
fsVars =
  [llvmOvr| ssize_t @write( i32, i8*, size_t ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args -> CurryAssignment
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (RegEntry sym)
  (OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType wptr)))
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (BVType wptr))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  f
  x
-> Assignment
     f
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
-> x
uncurryAssignment (GlobalVar Mem
-> LLVMFileSystem wptr
-> RegEntry sym (BVType 32)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (BVType wptr))
forall sym (wptr :: Natural) p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> LLVMFileSystem wptr
-> RegEntry sym (BVType 32)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext rtp args ret (RegValue sym (BVType wptr))
callWriteFileHandle GlobalVar Mem
memOps LLVMFileSystem wptr
fsVars) Assignment
  (RegEntry sym)
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args)

callWriteFileHandle ::
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, ?memOpts :: MemOptions) =>
  GlobalVar Mem ->
  LLVMFileSystem wptr ->
  RegEntry sym (BVType 32) ->
  RegEntry sym (LLVMPointerType wptr) ->
  RegEntry sym (BVType wptr) ->
  OverrideSim p sym ext rtp args ret (RegValue sym (BVType wptr))
callWriteFileHandle :: forall sym (wptr :: Natural) p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> LLVMFileSystem wptr
-> RegEntry sym (BVType 32)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext rtp args ret (RegValue sym (BVType wptr))
callWriteFileHandle GlobalVar Mem
memOps LLVMFileSystem wptr
fsVars RegEntry sym (BVType 32)
filedesc RegEntry sym (LLVMPointerType wptr)
buf RegEntry sym (BVType wptr)
count =
  do let args :: Assignment
  (RegEntry sym)
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args = Assignment (RegEntry sym) EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment (RegEntry sym) EmptyCtx
-> RegEntry sym (BVType 32)
-> Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RegEntry sym (BVType 32)
filedesc Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
-> RegEntry sym (LLVMPointerType wptr)
-> Assignment
     (RegEntry sym) ((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RegEntry sym (LLVMPointerType wptr)
buf Assignment
  (RegEntry sym) ((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RegEntry sym (BVType wptr)
count
     LLVMFileSystem wptr
-> SymBV sym 32
-> RegMap
     sym
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
-> (forall {args' :: Ctx CrucibleType}.
    Maybe (FileHandle sym wptr)
    -> RegMap
         sym
         (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
          ::> BVType wptr)
    -> OverrideSim
         p sym ext rtp args' ret (RegValue sym (BVType wptr)))
-> OverrideSim p sym ext rtp args ret (RegValue sym (BVType wptr))
forall sym (wptr :: Natural) (args'' :: Ctx CrucibleType) p ext r
       (ret :: CrucibleType) a (args :: Ctx CrucibleType).
IsSymInterface sym =>
LLVMFileSystem wptr
-> SymBV sym 32
-> RegMap sym args''
-> (forall (args' :: Ctx CrucibleType).
    Maybe (FileHandle sym wptr)
    -> RegMap sym args'' -> OverrideSim p sym ext r args' ret a)
-> OverrideSim p sym ext r args ret a
lookupFileHandle LLVMFileSystem wptr
fsVars (RegEntry sym (BVType 32) -> RegValue sym (BVType 32)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym (BVType 32)
filedesc) (Assignment
  (RegEntry sym)
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
-> RegMap
     sym
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap Assignment
  (RegEntry sym)
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
args) ((forall {args' :: Ctx CrucibleType}.
  Maybe (FileHandle sym wptr)
  -> RegMap
       sym
       (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
        ::> BVType wptr)
  -> OverrideSim
       p sym ext rtp args' ret (RegValue sym (BVType wptr)))
 -> OverrideSim p sym ext rtp args ret (RegValue sym (BVType wptr)))
-> (forall {args' :: Ctx CrucibleType}.
    Maybe (FileHandle sym wptr)
    -> RegMap
         sym
         (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
          ::> BVType wptr)
    -> OverrideSim
         p sym ext rtp args' ret (RegValue sym (BVType wptr)))
-> OverrideSim p sym ext rtp args ret (RegValue sym (BVType wptr))
forall a b. (a -> b) -> a -> b
$ \case
       Just FileHandle sym wptr
fileHandle -> \(RegMap (Assignment (RegEntry sym) ctx
Empty :> RegEntry sym tp
_ :> RegEntry sym tp
buffer_ptr :> RegEntry sym tp
size)) -> do
         MemImpl sym
mem <- GlobalVar Mem
-> OverrideSim p sym ext rtp args' ret (RegValue sym Mem)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal GlobalVar Mem
memOps
         (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim
      p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
-> OverrideSim
     p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim
       p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
 -> OverrideSim
      p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
-> OverrideSim
     p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ \bak
bak -> do
           DataChunk sym wptr
chunk <- IO (DataChunk sym wptr)
-> OverrideSim p sym ext rtp args' ret (DataChunk sym wptr)
forall a. IO a -> OverrideSim p sym ext rtp args' ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (DataChunk sym wptr)
 -> OverrideSim p sym ext rtp args' ret (DataChunk sym wptr))
-> IO (DataChunk sym wptr)
-> OverrideSim p sym ext rtp args' ret (DataChunk sym wptr)
forall a b. (a -> b) -> a -> b
$ bak -> MemImpl sym -> LLVMPtr sym wptr -> IO (DataChunk sym wptr)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
bak -> MemImpl sym -> LLVMPtr sym wptr -> IO (DataChunk sym wptr)
chunkFromMemory bak
bak MemImpl sym
mem (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
buffer_ptr)
           NatRepr wptr
-> Map Natural Handle
-> RegValue sym (BVType 32)
-> DataChunk sym wptr
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext rtp args' ret ()
forall sym (wptr :: Natural) p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
NatRepr wptr
-> Map Natural Handle
-> RegValue sym (BVType 32)
-> DataChunk sym wptr
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext rtp args ret ()
doConcreteWrite (LLVMFileSystem wptr -> NatRepr wptr
forall (ptrW :: Natural). LLVMFileSystem ptrW -> NatRepr ptrW
llvmFilePointerRepr LLVMFileSystem wptr
fsVars) (LLVMFileSystem wptr -> Map Natural Handle
forall (ptrW :: Natural). LLVMFileSystem ptrW -> Map Natural Handle
llvmHandles LLVMFileSystem wptr
fsVars) (RegEntry sym (BVType 32) -> RegValue sym (BVType 32)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym (BVType 32)
filedesc) DataChunk sym wptr
chunk RegEntry sym tp
RegEntry sym (BVType wptr)
size
           GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> DataChunk sym wptr
-> SymExpr sym ('BaseBVType wptr)
-> (forall {args' :: Ctx CrucibleType}.
    Either FileHandleError (SymExpr sym ('BaseBVType wptr))
    -> OverrideSim
         p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
-> OverrideSim
     p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr))
forall sym (wptr :: Natural) p arch r (ret :: CrucibleType) a
       (args :: Ctx CrucibleType).
(IsSymInterface sym, 1 <= wptr) =>
GlobalVar (FileSystemType wptr)
-> FileHandle sym wptr
-> DataChunk sym wptr
-> SymBV sym wptr
-> (forall (args' :: Ctx CrucibleType).
    Either FileHandleError (SymBV sym wptr)
    -> OverrideSim p sym arch r args' ret a)
-> OverrideSim p sym arch r args ret a
SymIO.writeChunk (LLVMFileSystem wptr -> GlobalVar (FileSystemType wptr)
forall (ptrW :: Natural).
LLVMFileSystem ptrW -> GlobalVar (FileSystemType ptrW)
llvmFileSystem LLVMFileSystem wptr
fsVars) FileHandle sym wptr
fileHandle DataChunk sym wptr
chunk (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
size) ((forall {args' :: Ctx CrucibleType}.
  Either FileHandleError (SymExpr sym ('BaseBVType wptr))
  -> OverrideSim
       p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
 -> OverrideSim
      p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
-> (forall {args' :: Ctx CrucibleType}.
    Either FileHandleError (SymExpr sym ('BaseBVType wptr))
    -> OverrideSim
         p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr)))
-> OverrideSim
     p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr))
forall a b. (a -> b) -> a -> b
$ \case
             Left FileHandleError
SymIO.FileHandleClosed -> OverrideSim
  p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr))
forall (wptr :: Natural) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
OverrideSim p sym ext r args ret (SymBV sym wptr)
returnIOError
             Right SymExpr sym ('BaseBVType wptr)
bytesWritten -> SymExpr sym ('BaseBVType wptr)
-> OverrideSim
     p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr))
forall a. a -> OverrideSim p sym ext rtp args' ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return SymExpr sym ('BaseBVType wptr)
bytesWritten
       Maybe (FileHandle sym wptr)
Nothing -> \RegMap
  sym
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
_ -> OverrideSim p sym ext rtp args' ret (RegValue sym (BVType wptr))
OverrideSim
  p sym ext rtp args' ret (SymExpr sym ('BaseBVType wptr))
forall (wptr :: Natural) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
OverrideSim p sym ext r args ret (SymBV sym wptr)
returnIOError

-- | The file handling overrides
--
-- See the 'initialLLVMFileSystem' function for creating the initial filesystem state
symio_overrides
  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch, ?memOpts :: MemOptions)
  => LLVMFileSystem wptr
  -> [OverrideTemplate p sym ext arch]
symio_overrides :: forall sym (wptr :: Natural) (arch :: LLVMArch) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 wptr ~ ArchWidth arch, ?memOpts::MemOptions) =>
LLVMFileSystem wptr -> [OverrideTemplate p sym ext arch]
symio_overrides LLVMFileSystem wptr
fs =
  [ LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
  (BVType 32)
-> OverrideTemplate p sym ext arch
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym ext
       (arch :: LLVMArch) (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym ext args ret -> OverrideTemplate p sym ext arch
basic_llvm_override (LLVMOverride
   p
   sym
   ext
   ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
   (BVType 32)
 -> OverrideTemplate p sym ext arch)
-> LLVMOverride
     p
     sym
     ext
     ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
     (BVType 32)
-> OverrideTemplate p sym ext arch
forall a b. (a -> b) -> a -> b
$ LLVMFileSystem wptr
-> LLVMOverride
     p
     sym
     ext
     ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
     (BVType 32)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMFileSystem wptr
-> LLVMOverride
     p
     sym
     ext
     ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType 32)
     (BVType 32)
openFile LLVMFileSystem wptr
fs
  , LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
-> OverrideTemplate p sym ext arch
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym ext
       (arch :: LLVMArch) (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym ext args ret -> OverrideTemplate p sym ext arch
basic_llvm_override (LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
 -> OverrideTemplate p sym ext arch)
-> LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
-> OverrideTemplate p sym ext arch
forall a b. (a -> b) -> a -> b
$ LLVMFileSystem wptr
-> LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMFileSystem wptr
-> LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
closeFile LLVMFileSystem wptr
fs
  , LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (BVType wptr)
-> OverrideTemplate p sym ext arch
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym ext
       (arch :: LLVMArch) (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym ext args ret -> OverrideTemplate p sym ext arch
basic_llvm_override (LLVMOverride
   p
   sym
   ext
   (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   (BVType wptr)
 -> OverrideTemplate p sym ext arch)
-> LLVMOverride
     p
     sym
     ext
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
     (BVType wptr)
-> OverrideTemplate p sym ext arch
forall a b. (a -> b) -> a -> b
$ LLVMFileSystem wptr
-> LLVMOverride
     p
     sym
     ext
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
     (BVType wptr)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMFileSystem wptr
-> LLVMOverride
     p
     sym
     ext
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
     (BVType wptr)
readFileHandle LLVMFileSystem wptr
fs
  , LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> BVType wptr)
  (BVType wptr)
-> OverrideTemplate p sym ext arch
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym ext
       (arch :: LLVMArch) (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym ext args ret -> OverrideTemplate p sym ext arch
basic_llvm_override (LLVMOverride
   p
   sym
   ext
   (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
    ::> BVType wptr)
   (BVType wptr)
 -> OverrideTemplate p sym ext arch)
-> LLVMOverride
     p
     sym
     ext
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
     (BVType wptr)
-> OverrideTemplate p sym ext arch
forall a b. (a -> b) -> a -> b
$ LLVMFileSystem wptr
-> LLVMOverride
     p
     sym
     ext
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
     (BVType wptr)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMFileSystem wptr
-> LLVMOverride
     p
     sym
     ext
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> BVType wptr)
     (BVType wptr)
writeFileHandle LLVMFileSystem wptr
fs
  ]

{- Note [Standard IO Setup]

The underlying symbolic IO library hands out abstract 'FileHande's, which are an
internal type that do not correspond to any source-level data values.  Frontends
must map them to something from the target programming language.  In this
module, that means we must map them to POSIX file descriptors (represented as C
ints).

In particular, when setting up the symbolic execution engine, we want to be able
to map standard input, standard output, and standard error to their prescribed
file descriptors (0, 1, and 2 respectively).  We can do that by simply
allocating them in order, as we start the file descriptor counter at 0 (see
'FDescMap').  Note that we just reuse the existing infrastructure to allocate
file descriptors (in particular, 'allocateFileDescriptor'). Note that we do
*not* use the 'openFile' function defined in this module because it expects the
filename to be stored in the LLVM memory, which our magic names for the standard
streams are not.

Note that if we start the symbolic execution engine without standard
in/out/error, we could potentially hand out file descriptors at these usually
reserved numbers. That isn't necessarily a problem, but it could be. We could
one day provide a method for forcing file descriptors to start at 3 even if
these special files are not allocated (i.e., start off closed).  We should
investigate the behavior of the OS and mimic it (or make it an option).

As a note on file names, the standard IO streams do not have prescribed names
that can be opened. We use synthetic names defined in the underlying
architecture-independent symbolic IO library.  We do not need to know what they
are here, but they are arranged to not collide with any valid names for actual
files in the symbolic filesystem.

-}

{- Note [File Descriptor Sequence]

This code uses a global counter to provide the next file descriptor to hand out
when a file is opened.  This can lead to a subtle difference in behavior
compared to a real program.

Consider the case where a program contains a symbolic branch where both branches
open files.  The symbolic I/O system will allocate each of the opened files a
different file descriptor.  In contrast, a real system would only assign one of
those file descriptors because it would only see one branch.  This means that
later opened files would differ from the real program.

This should only be observable if the program makes control decisions based on
the values in file descriptors, which it really should not. However, it is
possible in the real world.

-}