-- |
-- Module           : Lang.Crucible.LLVM.Intrinsics.Libc.Stdio
-- Description      : Override definitions for C @stdio.h@ functions
-- Copyright        : (c) Galois, Inc 2026
-- License          : BSD3
-- Maintainer       : Galois, Inc. <crux@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

module Lang.Crucible.LLVM.Intrinsics.Libc.Stdio
  ( -- * @stdio.h@ overrides
    stdioOverrides
    -- * Override declarations
  , llvmPrintfOverride
  , llvmPrintfChkOverride
  , llvmPutsOverride
  , llvmPutCharOverride
    -- * Implementation functions
  , callPrintf
  , callPutChar
  , callPuts
  , printfOps
  ) where

import           Control.Monad.IO.Class (liftIO)
import           Control.Monad.State (StateT(..), get, put)
import           Control.Monad.Trans.Class (MonadTrans(..))
import qualified Codec.Binary.UTF8.Generic as UTF8
import qualified Data.ByteString as BS
import qualified Data.Vector as V
import           System.IO
import qualified GHC.Stack as GHC

import qualified Data.BitVector.Sized as BV
import           Data.Parameterized.Context (pattern Empty)
import qualified Data.Parameterized.Context as Ctx

import           What4.Interface

import           Lang.Crucible.Backend
import           Lang.Crucible.CFG.Common
import           Lang.Crucible.Simulator (printHandle)
import           Lang.Crucible.Types
import           Lang.Crucible.Simulator.OverrideSim
import           Lang.Crucible.Simulator.RegMap
import           Lang.Crucible.Simulator.SimError

import           Lang.Crucible.LLVM.DataLayout
import           Lang.Crucible.LLVM.MemModel
import qualified Lang.Crucible.LLVM.MemModel.Generic as G
import qualified Lang.Crucible.LLVM.MemModel.Pointer as Ptr
import           Lang.Crucible.LLVM.MemModel.Strings as CStr
import qualified Lang.Crucible.LLVM.MemModel.Type as G
import           Lang.Crucible.LLVM.Printf
import           Lang.Crucible.LLVM.QQ( llvmOvr )

import           Lang.Crucible.LLVM.Intrinsics.Common

-- | All @stdio.h@ overrides
stdioOverrides ::
  ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
  , ?memOpts :: MemOptions ) =>
  [SomeLLVMOverride p sym ext]
stdioOverrides :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
[SomeLLVMOverride p sym ext]
stdioOverrides =
  [ LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> VectorType AnyType)
  (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> VectorType AnyType)
  (BVType 32)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> VectorType AnyType)
  (BVType 32)
llvmPrintfOverride
  , LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> VectorType AnyType)
  (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> VectorType AnyType)
  (BVType 32)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> VectorType AnyType)
  (BVType 32)
llvmPrintfChkOverride
  , LLVMOverride
  p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType 32)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType 32)
llvmPutsOverride
  , LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasPtrWidth wptr) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
llvmPutCharOverride
  ]

------------------------------------------------------------------------
-- ** Declarations

llvmPrintfOverride
  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
     , ?memOpts :: MemOptions )
  => LLVMOverride p sym ext
         (EmptyCtx ::> LLVMPointerType wptr
                   ::> VectorType AnyType)
         (BVType 32)
llvmPrintfOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> VectorType AnyType)
  (BVType 32)
llvmPrintfOverride =
  [llvmOvr| i32 @printf( i8*, ... ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  ((EmptyCtx ::> LLVMPointerType wptr) ::> VectorType AnyType)
args -> CurryAssignment
  ((EmptyCtx ::> LLVMPointerType wptr) ::> VectorType AnyType)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> LLVMPointerType wptr) ::> VectorType AnyType)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 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) ::> VectorType AnyType) f x
-> Assignment
     f ((EmptyCtx ::> LLVMPointerType wptr) ::> VectorType AnyType)
-> x
Ctx.uncurryAssignment (GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (VectorType AnyType)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (VectorType AnyType)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPrintf GlobalVar Mem
memOps) Assignment
  (RegEntry sym)
  ((EmptyCtx ::> LLVMPointerType wptr) ::> VectorType AnyType)
args)

llvmPrintfChkOverride
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?memOpts :: MemOptions )
  => LLVMOverride p sym ext
         (EmptyCtx ::> BVType 32
                   ::> LLVMPointerType wptr
                   ::> VectorType AnyType)
         (BVType 32)
llvmPrintfChkOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> VectorType AnyType)
  (BVType 32)
llvmPrintfChkOverride =
  [llvmOvr| i32 @__printf_chk( i32, i8*, ... ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> VectorType AnyType)
args -> CurryAssignment
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> VectorType AnyType)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> VectorType AnyType)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 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) ::> LLVMPointerType wptr)
   ::> VectorType AnyType)
  f
  x
-> Assignment
     f
     (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
      ::> VectorType AnyType)
-> x
Ctx.uncurryAssignment (\RegEntry sym (BVType 32)
_flg -> GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (VectorType AnyType)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (VectorType AnyType)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPrintf GlobalVar Mem
memOps) Assignment
  (RegEntry sym)
  (((EmptyCtx ::> BVType 32) ::> LLVMPointerType wptr)
   ::> VectorType AnyType)
args)


llvmPutCharOverride
  :: (IsSymInterface sym, HasPtrWidth wptr)
  => LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
llvmPutCharOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasPtrWidth wptr) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
llvmPutCharOverride =
  [llvmOvr| i32 @putchar( i32 ) |]
  (\GlobalVar Mem
memOps Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
args -> CurryAssignment
  (EmptyCtx ::> BVType 32)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 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
Ctx.uncurryAssignment (GlobalVar Mem
-> RegEntry sym (BVType 32)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar Mem
-> RegEntry sym (BVType 32)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPutChar GlobalVar Mem
memOps) Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
args)


llvmPutsOverride
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?memOpts :: MemOptions )
  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType 32)
llvmPutsOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
LLVMOverride
  p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType 32)
llvmPutsOverride =
  [llvmOvr| i32 @puts( i8* ) |]
  (\GlobalVar Mem
memOps Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr)
args -> CurryAssignment
  (EmptyCtx ::> LLVMPointerType wptr)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 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) f x
-> Assignment f (EmptyCtx ::> LLVMPointerType wptr) -> x
Ctx.uncurryAssignment (GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPuts GlobalVar Mem
memOps) Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr)
args)

------------------------------------------------------------------------
-- ** Implementations

callPutChar
  :: IsSymInterface sym
  => GlobalVar Mem
  -> RegEntry sym (BVType 32)
  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPutChar :: forall sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar Mem
-> RegEntry sym (BVType 32)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPutChar GlobalVar Mem
_mvar
 (RegEntry sym (BVType 32) -> RegValue sym (BVType 32)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (BVType 32)
ch) = do
    Handle
h <- SimContext p sym ext -> Handle
forall p sym ext. SimContext p sym ext -> Handle
printHandle (SimContext p sym ext -> Handle)
-> OverrideSim p sym ext r args ret (SimContext p sym ext)
-> OverrideSim p sym ext r args ret Handle
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> OverrideSim p sym ext r args ret (SimContext p sym ext)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (SimContext p sym ext)
getContext
    let chval :: Char
chval = Char -> (Integer -> Char) -> Maybe Integer -> Char
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Char
'?' (Int -> Char
forall a. Enum a => Int -> a
toEnum (Int -> Char) -> (Integer -> Int) -> Integer -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a. Num a => Integer -> a
fromInteger) (BV 32 -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned (BV 32 -> Integer) -> Maybe (BV 32) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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)
asBV RegValue sym (BVType 32)
SymExpr sym ('BaseBVType 32)
ch)
    IO () -> OverrideSim p sym ext r args ret ()
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 () -> OverrideSim p sym ext r args ret ())
-> IO () -> OverrideSim p sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ Handle -> Char -> IO ()
hPutChar Handle
h Char
chval
    SymExpr sym ('BaseBVType 32)
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 32))
forall a. a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return RegValue sym (BVType 32)
SymExpr sym ('BaseBVType 32)
ch

callPuts
  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
     , ?memOpts :: MemOptions )
  => GlobalVar Mem
  -> RegEntry sym (LLVMPointerType wptr)
  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPuts :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPuts GlobalVar Mem
mvar
  (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
strPtr) =
    (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
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 (RegValue sym (BVType 32)))
 -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
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
mvar
      [Word8]
str <- 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
-> RegValue sym (LLVMPointerType 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]
CStr.loadString bak
bak MemImpl sym
mem RegValue sym (LLVMPointerType wptr)
strPtr Maybe Int
forall a. Maybe a
Nothing
      Handle
h <- SimContext p sym ext -> Handle
forall p sym ext. SimContext p sym ext -> Handle
printHandle (SimContext p sym ext -> Handle)
-> OverrideSim p sym ext r args ret (SimContext p sym ext)
-> OverrideSim p sym ext r args ret Handle
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> OverrideSim p sym ext r args ret (SimContext p sym ext)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (SimContext p sym ext)
getContext
      IO () -> OverrideSim p sym ext r args ret ()
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 () -> OverrideSim p sym ext r args ret ())
-> IO () -> OverrideSim p sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStrLn Handle
h ([Word8] -> String
forall b s. UTF8Bytes b s => b -> String
UTF8.toString [Word8]
str)
      -- return non-negative value on success
      IO (SymExpr sym ('BaseBVType 32))
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 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 (SymExpr sym ('BaseBVType 32))
 -> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 32)))
-> IO (SymExpr sym ('BaseBVType 32))
-> OverrideSim p sym ext r 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)
bvLit (bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak) NatRepr 32
forall (n :: Natural). KnownNat n => NatRepr n
knownNat (NatRepr 32 -> BV 32
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.one NatRepr 32
forall (n :: Natural). KnownNat n => NatRepr n
knownNat)

callPrintf
  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
     , ?memOpts :: MemOptions )
  => GlobalVar Mem
  -> RegEntry sym (LLVMPointerType wptr)
  -> RegEntry sym (VectorType AnyType)
  -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPrintf :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (VectorType AnyType)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPrintf GlobalVar Mem
mvar
  (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
strPtr)
  (RegEntry sym (VectorType AnyType)
-> RegValue sym (VectorType AnyType)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (VectorType AnyType)
valist) =
    (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
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 (RegValue sym (BVType 32)))
 -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
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
mvar
      [Word8]
formatStr <- 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
-> RegValue sym (LLVMPointerType 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]
CStr.loadString bak
bak MemImpl sym
mem RegValue sym (LLVMPointerType wptr)
strPtr Maybe Int
forall a. Maybe a
Nothing
      case [Word8] -> Either String [PrintfDirective]
parseDirectives [Word8]
formatStr of
        Left String
err -> SimErrorReason
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 32))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (res :: CrucibleType) a.
IsSymInterface sym =>
SimErrorReason -> OverrideSim p sym ext rtp args res a
overrideError (SimErrorReason
 -> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 32)))
-> SimErrorReason
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 32))
forall a b. (a -> b) -> a -> b
$ String -> String -> SimErrorReason
AssertFailureSimError String
"Format string parsing failed" String
err
        Right [PrintfDirective]
ds -> do
          ((ByteString
str, Int
n), MemImpl sym
mem') <- IO ((ByteString, Int), MemImpl sym)
-> OverrideSim
     p sym ext r args ret ((ByteString, Int), MemImpl sym)
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 ((ByteString, Int), MemImpl sym)
 -> OverrideSim
      p sym ext r args ret ((ByteString, Int), MemImpl sym))
-> IO ((ByteString, Int), MemImpl sym)
-> OverrideSim
     p sym ext r args ret ((ByteString, Int), MemImpl sym)
forall a b. (a -> b) -> a -> b
$ StateT (MemImpl sym) IO (ByteString, Int)
-> MemImpl sym -> IO ((ByteString, Int), MemImpl sym)
forall s (m :: Type -> Type) a. StateT s m a -> s -> m (a, s)
runStateT (PrintfOperations (StateT (MemImpl sym) IO)
-> [PrintfDirective] -> StateT (MemImpl sym) IO (ByteString, Int)
forall (m :: Type -> Type).
Monad m =>
PrintfOperations m -> [PrintfDirective] -> m (ByteString, Int)
executeDirectives (bak
-> Vector (AnyValue sym)
-> PrintfOperations (StateT (MemImpl sym) IO)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
bak
-> Vector (AnyValue sym)
-> PrintfOperations (StateT (MemImpl sym) IO)
printfOps bak
bak Vector (AnyValue sym)
RegValue sym (VectorType AnyType)
valist) [PrintfDirective]
ds) MemImpl sym
mem
          GlobalVar Mem
-> RegValue sym Mem -> OverrideSim p sym ext r args ret ()
forall (tp :: CrucibleType) sym p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
GlobalVar tp
-> RegValue sym tp -> OverrideSim p sym ext rtp args ret ()
writeGlobal GlobalVar Mem
mvar RegValue sym Mem
MemImpl sym
mem'
          Handle
h <- SimContext p sym ext -> Handle
forall p sym ext. SimContext p sym ext -> Handle
printHandle (SimContext p sym ext -> Handle)
-> OverrideSim p sym ext r args ret (SimContext p sym ext)
-> OverrideSim p sym ext r args ret Handle
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> OverrideSim p sym ext r args ret (SimContext p sym ext)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (SimContext p sym ext)
getContext
          IO () -> OverrideSim p sym ext r args ret ()
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 () -> OverrideSim p sym ext r args ret ())
-> IO () -> OverrideSim p sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ Handle -> ByteString -> IO ()
BS.hPutStr Handle
h ByteString
str
          IO (SymExpr sym ('BaseBVType 32))
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 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 (SymExpr sym ('BaseBVType 32))
 -> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType 32)))
-> IO (SymExpr sym ('BaseBVType 32))
-> OverrideSim p sym ext r 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)
bvLit (bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak) NatRepr 32
forall (n :: Natural). KnownNat n => NatRepr n
knownNat (NatRepr 32 -> Integer -> BV 32
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr 32
forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n))

printfOps :: ( IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr
             , ?memOpts :: MemOptions )
          => bak
          -> V.Vector (AnyValue sym)
          -> PrintfOperations (StateT (MemImpl sym) IO)
printfOps :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr,
 ?memOpts::MemOptions) =>
bak
-> Vector (AnyValue sym)
-> PrintfOperations (StateT (MemImpl sym) IO)
printfOps bak
bak Vector (AnyValue sym)
valist =
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak in
  PrintfOperations
  { printfUnsupported :: forall a. HasCallStack => String -> StateT (MemImpl sym) IO a
printfUnsupported = \String
x -> IO a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a.
Monad m =>
m a -> StateT (MemImpl sym) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO a -> StateT (MemImpl sym) IO a)
-> IO a -> StateT (MemImpl sym) IO a
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO a
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak
                                   (SimErrorReason -> IO a) -> SimErrorReason -> IO a
forall a b. (a -> b) -> a -> b
$ CallStack -> String -> SimErrorReason
Unsupported CallStack
HasCallStack => CallStack
GHC.callStack String
x

  , printfGetInteger :: Int
-> Bool
-> PrintfLengthModifier
-> StateT (MemImpl sym) IO (Maybe Integer)
printfGetInteger = \Int
i Bool
sgn PrintfLengthModifier
_len ->
     case Vector (AnyValue sym)
valist Vector (AnyValue sym) -> Int -> Maybe (AnyValue sym)
forall a. Vector a -> Int -> Maybe a
V.!? (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) of
       Just (AnyValue (LLVMPointerRepr NatRepr w
w) p :: RegValue sym tp
p@(LLVMPointer SymNat sym
_blk SymBV sym w
bv)) ->
         do SymExpr sym BaseBoolType
isBv <- IO (SymExpr sym BaseBoolType)
-> StateT (MemImpl sym) IO (SymExpr sym BaseBoolType)
forall a. IO a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> LLVMPtr sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> LLVMPtr sym w -> IO (Pred sym)
Ptr.ptrIsBv sym
sym RegValue sym tp
LLVMPtr sym w
p)
            IO () -> StateT (MemImpl sym) IO ()
forall a. IO a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT (MemImpl sym) IO ())
-> IO () -> StateT (MemImpl sym) IO ()
forall a b. (a -> b) -> a -> b
$ bak -> SymExpr sym BaseBoolType -> SimErrorReason -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Pred sym -> SimErrorReason -> IO ()
assert bak
bak SymExpr sym BaseBoolType
isBv (SimErrorReason -> IO ()) -> SimErrorReason -> IO ()
forall a b. (a -> b) -> a -> b
$
              String -> String -> SimErrorReason
AssertFailureSimError
               String
"Passed a pointer to printf where a bitvector was expected"
               String
""
            if Bool
sgn then
              Maybe Integer -> StateT (MemImpl sym) IO (Maybe Integer)
forall a. a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe Integer -> StateT (MemImpl sym) IO (Maybe Integer))
-> Maybe Integer -> StateT (MemImpl sym) IO (Maybe Integer)
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BV w -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned NatRepr w
w (BV w -> Integer) -> Maybe (BV w) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymBV sym w -> Maybe (BV w)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV SymBV sym w
bv
            else
              Maybe Integer -> StateT (MemImpl sym) IO (Maybe Integer)
forall a. a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe Integer -> StateT (MemImpl sym) IO (Maybe Integer))
-> Maybe Integer -> StateT (MemImpl sym) IO (Maybe Integer)
forall a b. (a -> b) -> a -> b
$ BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned (BV w -> Integer) -> Maybe (BV w) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymBV sym w -> Maybe (BV w)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV SymBV sym w
bv
       Just (AnyValue TypeRepr tp
tpr RegValue sym tp
_) ->
         IO (Maybe Integer) -> StateT (MemImpl sym) IO (Maybe Integer)
forall (m :: Type -> Type) a.
Monad m =>
m a -> StateT (MemImpl sym) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Maybe Integer) -> StateT (MemImpl sym) IO (Maybe Integer))
-> IO (Maybe Integer) -> StateT (MemImpl sym) IO (Maybe Integer)
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO (Maybe Integer)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak
              (SimErrorReason -> IO (Maybe Integer))
-> SimErrorReason -> IO (Maybe Integer)
forall a b. (a -> b) -> a -> b
$ String -> String -> SimErrorReason
AssertFailureSimError
                String
"Type mismatch in printf"
                ([String] -> String
unwords [String
"Expected integer, but got:", TypeRepr tp -> String
forall a. Show a => a -> String
show TypeRepr tp
tpr])
       Maybe (AnyValue sym)
Nothing ->
         IO (Maybe Integer) -> StateT (MemImpl sym) IO (Maybe Integer)
forall (m :: Type -> Type) a.
Monad m =>
m a -> StateT (MemImpl sym) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Maybe Integer) -> StateT (MemImpl sym) IO (Maybe Integer))
-> IO (Maybe Integer) -> StateT (MemImpl sym) IO (Maybe Integer)
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO (Maybe Integer)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak
              (SimErrorReason -> IO (Maybe Integer))
-> SimErrorReason -> IO (Maybe Integer)
forall a b. (a -> b) -> a -> b
$ String -> String -> SimErrorReason
AssertFailureSimError
               String
"Out-of-bounds argument access in printf"
               ([String] -> String
unwords [String
"Index:", Int -> String
forall a. Show a => a -> String
show Int
i])

  , printfGetFloat :: Int
-> PrintfLengthModifier -> StateT (MemImpl sym) IO (Maybe Rational)
printfGetFloat = \Int
i PrintfLengthModifier
_len ->
     case Vector (AnyValue sym)
valist Vector (AnyValue sym) -> Int -> Maybe (AnyValue sym)
forall a. Vector a -> Int -> Maybe a
V.!? (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) of
       Just (AnyValue (FloatRepr (FloatInfoRepr flt
_fi :: FloatInfoRepr fi)) RegValue sym tp
x) ->
         do SymExpr sym BaseRealType
xr <- IO (SymExpr sym BaseRealType)
-> StateT (MemImpl sym) IO (SymExpr sym BaseRealType)
forall a. IO a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> SymInterpretedFloat sym fi -> IO (SymReal sym)
iFloatToReal @_ @fi sym
sym RegValue sym tp
SymInterpretedFloat sym flt
x)
            Maybe Rational -> StateT (MemImpl sym) IO (Maybe Rational)
forall a. a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymExpr sym BaseRealType -> Maybe Rational
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseRealType -> Maybe Rational
asRational SymExpr sym BaseRealType
xr)
       Just (AnyValue TypeRepr tp
tpr RegValue sym tp
_) ->
         IO (Maybe Rational) -> StateT (MemImpl sym) IO (Maybe Rational)
forall (m :: Type -> Type) a.
Monad m =>
m a -> StateT (MemImpl sym) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Maybe Rational) -> StateT (MemImpl sym) IO (Maybe Rational))
-> IO (Maybe Rational) -> StateT (MemImpl sym) IO (Maybe Rational)
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO (Maybe Rational)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak
              (SimErrorReason -> IO (Maybe Rational))
-> SimErrorReason -> IO (Maybe Rational)
forall a b. (a -> b) -> a -> b
$ String -> String -> SimErrorReason
AssertFailureSimError
                String
"Type mismatch in printf."
                ([String] -> String
unwords [String
"Expected floating-point, but got:", TypeRepr tp -> String
forall a. Show a => a -> String
show TypeRepr tp
tpr])
       Maybe (AnyValue sym)
Nothing ->
         IO (Maybe Rational) -> StateT (MemImpl sym) IO (Maybe Rational)
forall (m :: Type -> Type) a.
Monad m =>
m a -> StateT (MemImpl sym) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Maybe Rational) -> StateT (MemImpl sym) IO (Maybe Rational))
-> IO (Maybe Rational) -> StateT (MemImpl sym) IO (Maybe Rational)
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO (Maybe Rational)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak
              (SimErrorReason -> IO (Maybe Rational))
-> SimErrorReason -> IO (Maybe Rational)
forall a b. (a -> b) -> a -> b
$ String -> String -> SimErrorReason
AssertFailureSimError
                String
"Out-of-bounds argument access in printf:"
                ([String] -> String
unwords [String
"Index:", Int -> String
forall a. Show a => a -> String
show Int
i])

  , printfGetString :: Int -> Maybe Int -> StateT (MemImpl sym) IO [Word8]
printfGetString  = \Int
i Maybe Int
numchars ->
     case Vector (AnyValue sym)
valist Vector (AnyValue sym) -> Int -> Maybe (AnyValue sym)
forall a. Vector a -> Int -> Maybe a
V.!? (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) of
       Just (AnyValue TypeRepr tp
PtrRepr RegValue sym tp
ptr) ->
           do MemImpl sym
mem <- StateT (MemImpl sym) IO (MemImpl sym)
forall s (m :: Type -> Type). MonadState s m => m s
get
              IO [Word8] -> StateT (MemImpl sym) IO [Word8]
forall a. IO a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO [Word8] -> StateT (MemImpl sym) IO [Word8])
-> IO [Word8] -> StateT (MemImpl sym) IO [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]
CStr.loadString bak
bak MemImpl sym
mem RegValue sym tp
LLVMPtr sym wptr
ptr Maybe Int
numchars
       Just (AnyValue TypeRepr tp
tpr RegValue sym tp
_) ->
         IO [Word8] -> StateT (MemImpl sym) IO [Word8]
forall (m :: Type -> Type) a.
Monad m =>
m a -> StateT (MemImpl sym) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO [Word8] -> StateT (MemImpl sym) IO [Word8])
-> IO [Word8] -> StateT (MemImpl sym) IO [Word8]
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO [Word8]
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak
              (SimErrorReason -> IO [Word8]) -> SimErrorReason -> IO [Word8]
forall a b. (a -> b) -> a -> b
$ String -> String -> SimErrorReason
AssertFailureSimError
                String
"Type mismatch in printf."
                ([String] -> String
unwords [String
"Expected char*, but got:", TypeRepr tp -> String
forall a. Show a => a -> String
show TypeRepr tp
tpr])
       Maybe (AnyValue sym)
Nothing ->
         IO [Word8] -> StateT (MemImpl sym) IO [Word8]
forall (m :: Type -> Type) a.
Monad m =>
m a -> StateT (MemImpl sym) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO [Word8] -> StateT (MemImpl sym) IO [Word8])
-> IO [Word8] -> StateT (MemImpl sym) IO [Word8]
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO [Word8]
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak
              (SimErrorReason -> IO [Word8]) -> SimErrorReason -> IO [Word8]
forall a b. (a -> b) -> a -> b
$ String -> String -> SimErrorReason
AssertFailureSimError
                String
"Out-of-bounds argument access in printf:"
                ([String] -> String
unwords [String
"Index:", Int -> String
forall a. Show a => a -> String
show Int
i])

  , printfGetPointer :: Int -> StateT (MemImpl sym) IO String
printfGetPointer = \Int
i ->
     case Vector (AnyValue sym)
valist Vector (AnyValue sym) -> Int -> Maybe (AnyValue sym)
forall a. Vector a -> Int -> Maybe a
V.!? (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) of
       Just (AnyValue TypeRepr tp
PtrRepr RegValue sym tp
ptr) ->
         String -> StateT (MemImpl sym) IO String
forall a. a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (String -> StateT (MemImpl sym) IO String)
-> String -> StateT (MemImpl sym) IO String
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (LLVMPtr sym wptr -> Doc Any
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
G.ppPtr RegValue sym tp
LLVMPtr sym wptr
ptr)
       Just (AnyValue TypeRepr tp
tpr RegValue sym tp
_) ->
         IO String -> StateT (MemImpl sym) IO String
forall (m :: Type -> Type) a.
Monad m =>
m a -> StateT (MemImpl sym) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO String -> StateT (MemImpl sym) IO String)
-> IO String -> StateT (MemImpl sym) IO String
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO String
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak
              (SimErrorReason -> IO String) -> SimErrorReason -> IO String
forall a b. (a -> b) -> a -> b
$ String -> String -> SimErrorReason
AssertFailureSimError
                String
"Type mismatch in printf."
                ([String] -> String
unwords [String
"Expected void*, but got:", TypeRepr tp -> String
forall a. Show a => a -> String
show TypeRepr tp
tpr])
       Maybe (AnyValue sym)
Nothing ->
         IO String -> StateT (MemImpl sym) IO String
forall (m :: Type -> Type) a.
Monad m =>
m a -> StateT (MemImpl sym) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO String -> StateT (MemImpl sym) IO String)
-> IO String -> StateT (MemImpl sym) IO String
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO String
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak
              (SimErrorReason -> IO String) -> SimErrorReason -> IO String
forall a b. (a -> b) -> a -> b
$ String -> String -> SimErrorReason
AssertFailureSimError
                String
"Out-of-bounds argument access in printf:"
                ([String] -> String
unwords [String
"Index:", Int -> String
forall a. Show a => a -> String
show Int
i])

  , printfSetInteger :: Int -> PrintfLengthModifier -> Int -> StateT (MemImpl sym) IO ()
printfSetInteger = \Int
i PrintfLengthModifier
len Int
v ->
     case Vector (AnyValue sym)
valist Vector (AnyValue sym) -> Int -> Maybe (AnyValue sym)
forall a. Vector a -> Int -> Maybe a
V.!? (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) of
       Just (AnyValue TypeRepr tp
PtrRepr RegValue sym tp
ptr) ->
         do MemImpl sym
mem <- StateT (MemImpl sym) IO (MemImpl sym)
forall s (m :: Type -> Type). MonadState s m => m s
get
            case PrintfLengthModifier
len of
              PrintfLengthModifier
Len_Byte  -> do
                 let w8 :: NatRepr 8
w8 = NatRepr 8
forall (n :: Natural). KnownNat n => NatRepr n
knownNat :: NatRepr 8
                 let tp :: StorageType
tp = Bytes -> StorageType
G.bitvectorType Bytes
1
                 LLVMPointer sym 8
x <- IO (LLVMPointer sym 8)
-> StateT (MemImpl sym) IO (LLVMPointer sym 8)
forall a. IO a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> SymExpr sym (BaseBVType 8) -> IO (LLVMPtr sym 8)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym (SymExpr sym (BaseBVType 8) -> IO (LLVMPointer sym 8))
-> IO (SymExpr sym (BaseBVType 8)) -> IO (LLVMPointer sym 8)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr 8 -> BV 8 -> IO (SymExpr sym (BaseBVType 8))
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)
bvLit sym
sym NatRepr 8
w8 (NatRepr 8 -> Integer -> BV 8
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr 8
w8 (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
v)))
                 MemImpl sym
mem' <- IO (MemImpl sym) -> StateT (MemImpl sym) IO (MemImpl sym)
forall a. IO a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (MemImpl sym) -> StateT (MemImpl sym) IO (MemImpl sym))
-> IO (MemImpl sym) -> StateT (MemImpl sym) IO (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> TypeRepr (LLVMPointerType 8)
-> StorageType
-> Alignment
-> LLVMPtr sym 8
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural) (tp :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> TypeRepr tp
-> StorageType
-> Alignment
-> RegValue sym tp
-> IO (MemImpl sym)
doStore bak
bak MemImpl sym
mem RegValue sym tp
LLVMPtr sym wptr
ptr (NatRepr 8 -> TypeRepr (LLVMPointerType 8)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr 8
w8) StorageType
tp Alignment
noAlignment LLVMPtr sym 8
LLVMPointer sym 8
x
                 MemImpl sym -> StateT (MemImpl sym) IO ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put MemImpl sym
mem'
              PrintfLengthModifier
Len_Short -> do
                 let w16 :: NatRepr 16
w16 = NatRepr 16
forall (n :: Natural). KnownNat n => NatRepr n
knownNat :: NatRepr 16
                 let tp :: StorageType
tp = Bytes -> StorageType
G.bitvectorType Bytes
2
                 LLVMPointer sym 16
x <- IO (LLVMPointer sym 16)
-> StateT (MemImpl sym) IO (LLVMPointer sym 16)
forall a. IO a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> SymExpr sym (BaseBVType 16) -> IO (LLVMPtr sym 16)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym (SymExpr sym (BaseBVType 16) -> IO (LLVMPointer sym 16))
-> IO (SymExpr sym (BaseBVType 16)) -> IO (LLVMPointer sym 16)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr 16 -> BV 16 -> IO (SymExpr sym (BaseBVType 16))
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)
bvLit sym
sym NatRepr 16
w16 (NatRepr 16 -> Integer -> BV 16
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr 16
w16 (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
v)))
                 MemImpl sym
mem' <- IO (MemImpl sym) -> StateT (MemImpl sym) IO (MemImpl sym)
forall a. IO a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (MemImpl sym) -> StateT (MemImpl sym) IO (MemImpl sym))
-> IO (MemImpl sym) -> StateT (MemImpl sym) IO (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> TypeRepr (LLVMPointerType 16)
-> StorageType
-> Alignment
-> LLVMPtr sym 16
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural) (tp :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> TypeRepr tp
-> StorageType
-> Alignment
-> RegValue sym tp
-> IO (MemImpl sym)
doStore bak
bak MemImpl sym
mem RegValue sym tp
LLVMPtr sym wptr
ptr (NatRepr 16 -> TypeRepr (LLVMPointerType 16)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr 16
w16) StorageType
tp Alignment
noAlignment LLVMPtr sym 16
LLVMPointer sym 16
x
                 MemImpl sym -> StateT (MemImpl sym) IO ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put MemImpl sym
mem'
              PrintfLengthModifier
Len_NoMod -> do
                 let w32 :: NatRepr 32
w32  = NatRepr 32
forall (n :: Natural). KnownNat n => NatRepr n
knownNat :: NatRepr 32
                 let tp :: StorageType
tp = Bytes -> StorageType
G.bitvectorType Bytes
4
                 LLVMPointer sym 32
x <- IO (LLVMPointer sym 32)
-> StateT (MemImpl sym) IO (LLVMPointer sym 32)
forall a. IO a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> SymExpr sym ('BaseBVType 32) -> IO (LLVMPtr sym 32)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym (SymExpr sym ('BaseBVType 32) -> IO (LLVMPointer sym 32))
-> IO (SymExpr sym ('BaseBVType 32)) -> IO (LLVMPointer sym 32)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m 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)
bvLit sym
sym NatRepr 32
w32 (NatRepr 32 -> Integer -> BV 32
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr 32
w32 (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
v)))
                 MemImpl sym
mem' <- IO (MemImpl sym) -> StateT (MemImpl sym) IO (MemImpl sym)
forall a. IO a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (MemImpl sym) -> StateT (MemImpl sym) IO (MemImpl sym))
-> IO (MemImpl sym) -> StateT (MemImpl sym) IO (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> TypeRepr (LLVMPointerType 32)
-> StorageType
-> Alignment
-> LLVMPtr sym 32
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural) (tp :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> TypeRepr tp
-> StorageType
-> Alignment
-> RegValue sym tp
-> IO (MemImpl sym)
doStore bak
bak MemImpl sym
mem RegValue sym tp
LLVMPtr sym wptr
ptr (NatRepr 32 -> TypeRepr (LLVMPointerType 32)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr 32
w32) StorageType
tp Alignment
noAlignment LLVMPtr sym 32
LLVMPointer sym 32
x
                 MemImpl sym -> StateT (MemImpl sym) IO ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put MemImpl sym
mem'
              PrintfLengthModifier
Len_Long  -> do
                 let w64 :: NatRepr 64
w64 = NatRepr 64
forall (n :: Natural). KnownNat n => NatRepr n
knownNat :: NatRepr 64
                 let tp :: StorageType
tp = Bytes -> StorageType
G.bitvectorType Bytes
8
                 LLVMPointer sym 64
x <- IO (LLVMPointer sym 64)
-> StateT (MemImpl sym) IO (LLVMPointer sym 64)
forall a. IO a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> SymExpr sym (BaseBVType 64) -> IO (LLVMPtr sym 64)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym (SymExpr sym (BaseBVType 64) -> IO (LLVMPointer sym 64))
-> IO (SymExpr sym (BaseBVType 64)) -> IO (LLVMPointer sym 64)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr 64 -> BV 64 -> IO (SymExpr sym (BaseBVType 64))
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)
bvLit sym
sym NatRepr 64
w64 (NatRepr 64 -> Integer -> BV 64
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr 64
w64 (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
v)))
                 MemImpl sym
mem' <- IO (MemImpl sym) -> StateT (MemImpl sym) IO (MemImpl sym)
forall a. IO a -> StateT (MemImpl sym) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (MemImpl sym) -> StateT (MemImpl sym) IO (MemImpl sym))
-> IO (MemImpl sym) -> StateT (MemImpl sym) IO (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> TypeRepr (LLVMPointerType 64)
-> StorageType
-> Alignment
-> LLVMPtr sym 64
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural) (tp :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> TypeRepr tp
-> StorageType
-> Alignment
-> RegValue sym tp
-> IO (MemImpl sym)
doStore bak
bak MemImpl sym
mem RegValue sym tp
LLVMPtr sym wptr
ptr (NatRepr 64 -> TypeRepr (LLVMPointerType 64)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr 64
w64) StorageType
tp Alignment
noAlignment LLVMPtr sym 64
LLVMPointer sym 64
x
                 MemImpl sym -> StateT (MemImpl sym) IO ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put MemImpl sym
mem'
              PrintfLengthModifier
_ ->
                IO () -> StateT (MemImpl sym) IO ()
forall (m :: Type -> Type) a.
Monad m =>
m a -> StateT (MemImpl sym) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> StateT (MemImpl sym) IO ())
-> IO () -> StateT (MemImpl sym) IO ()
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO ()
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak
                     (SimErrorReason -> IO ()) -> SimErrorReason -> IO ()
forall a b. (a -> b) -> a -> b
$ CallStack -> String -> SimErrorReason
Unsupported CallStack
HasCallStack => CallStack
GHC.callStack
                     (String -> SimErrorReason) -> String -> SimErrorReason
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"Unsupported size modifier in %n conversion:", PrintfLengthModifier -> String
forall a. Show a => a -> String
show PrintfLengthModifier
len]

       Just (AnyValue TypeRepr tp
tpr RegValue sym tp
_) ->
         IO () -> StateT (MemImpl sym) IO ()
forall (m :: Type -> Type) a.
Monad m =>
m a -> StateT (MemImpl sym) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> StateT (MemImpl sym) IO ())
-> IO () -> StateT (MemImpl sym) IO ()
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO ()
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak
              (SimErrorReason -> IO ()) -> SimErrorReason -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> SimErrorReason
AssertFailureSimError
                String
"Type mismatch in printf."
                ([String] -> String
unwords [String
"Expected void*, but got:", TypeRepr tp -> String
forall a. Show a => a -> String
show TypeRepr tp
tpr])

       Maybe (AnyValue sym)
Nothing ->
         IO () -> StateT (MemImpl sym) IO ()
forall (m :: Type -> Type) a.
Monad m =>
m a -> StateT (MemImpl sym) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> StateT (MemImpl sym) IO ())
-> IO () -> StateT (MemImpl sym) IO ()
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO ()
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak
              (SimErrorReason -> IO ()) -> SimErrorReason -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> SimErrorReason
AssertFailureSimError
                String
"Out-of-bounds argument access in printf:"
                ([String] -> String
unwords [String
"Index:", Int -> String
forall a. Show a => a -> String
show Int
i])
  }