{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Crux.LLVM.Simulate where
import qualified Data.BitVector.Sized as BV
import Data.String (fromString)
import qualified Data.Map.Strict as Map
import Data.IORef
import qualified Data.List as List
import Data.Maybe ( fromMaybe )
import qualified Data.Parameterized.Map as MapF
import qualified Data.Traversable as T
import Control.Lens ((&), (%~), (%=), (^.), use, view)
import Control.Monad.IO.Class (liftIO)
import Data.Text as Text (Text, pack)
import GHC.Exts ( proxy# )
import System.IO (stdout)
import Data.Parameterized.Some (Some(..))
import Data.Parameterized.Context (pattern Empty, pattern (:>))
import Data.LLVM.BitCode (parseBitCodeFromFile)
import qualified Text.LLVM as LLVM
import Prettyprinter
import qualified What4.Expr.Builder as WEB
import What4.Interface (bvLit, natLit)
import Lang.Crucible.Backend
import Lang.Crucible.Types
import Lang.Crucible.CFG.Core(AnyCFG(..), CFG, cfgArgTypes)
import Lang.Crucible.FunctionHandle(newHandleAllocator,HandleAllocator)
import Lang.Crucible.Simulator
( RegMap(..), assignReg, emptyRegMap
, fnBindingsFromList, runOverrideSim, callCFG
, initSimContext, profilingMetrics
, ExecState( InitialState ), GlobalVar
, SimState, defaultAbortHandler, printHandle
, ppSimError, ovrWithBackend
)
import Lang.Crucible.Simulator.ExecutionTree ( actFrame, gpGlobals, stateGlobals, stateTree )
import Lang.Crucible.Simulator.GlobalState ( insertGlobal, lookupGlobal )
import Lang.Crucible.Simulator.Profiling ( Metric(Metric) )
import Lang.Crucible.LLVM(llvmExtensionImpl, llvmGlobals, registerLazyModule )
import Lang.Crucible.LLVM.Bytes ( bytesToBV )
import Lang.Crucible.LLVM.Globals
( initializeAllMemory, populateAllGlobals )
import Lang.Crucible.LLVM.MemModel
( Mem, MemImpl, mkMemVar, withPtrWidth, memAllocCount, memWriteCount
, MemOptions(..), HasLLVMAnn, LLVMAnnMap
, explainCex, CexExplanation(..), doAlloca
, pattern LLVMPointer, pattern LLVMPointerRepr, LLVMPointerType
, pattern PtrRepr, pattern PtrWidth
)
import Lang.Crucible.LLVM.MemModel.CallStack (ppCallStack)
import Lang.Crucible.LLVM.MemType (MemType(..), SymType(..), i8, memTypeAlign, memTypeSize)
import Lang.Crucible.LLVM.PrettyPrint (ppSymbol)
import Lang.Crucible.LLVM.Translation
( translateModule, ModuleTranslation, globalInitMap
, transContext, getTranslatedCFG, llvmPtrWidth, llvmTypeCtx
, LLVMTranslationWarning(..)
)
import Lang.Crucible.LLVM.Intrinsics
(llvmIntrinsicTypes, register_llvm_overrides )
import Lang.Crucible.LLVM.Errors( ppBB )
import Lang.Crucible.LLVM.Extension( LLVM, ArchWidth )
import Lang.Crucible.LLVM.SymIO
( LLVMFileSystem, llvmSymIOIntrinsicTypes, symio_overrides, initialLLVMFileSystem, SomeOverrideSim(..) )
import Lang.Crucible.LLVM.TypeContext (llvmDataLayout)
import qualified Lang.Crucible.SymIO as SymIO
import qualified Lang.Crucible.SymIO.Loader as SymIO.Loader
import qualified Crux
import Crux.Types
import Crux.Log ( outputHandle )
import Crux.LLVM.Config
import qualified Crux.LLVM.Log as Log
import Crux.LLVM.Overrides
setupSimCtxt ::
(IsSymBackend sym bak, HasLLVMAnn sym) =>
HandleAllocator ->
bak ->
MemOptions ->
GlobalVar Mem ->
SimCtxt Crux sym LLVM
setupSimCtxt :: forall sym bak.
(IsSymBackend sym bak, HasLLVMAnn sym) =>
HandleAllocator
-> bak -> MemOptions -> GlobalVar Mem -> SimCtxt Crux sym LLVM
setupSimCtxt HandleAllocator
halloc bak
bak MemOptions
mo GlobalVar Mem
memVar =
bak
-> IntrinsicTypes sym
-> HandleAllocator
-> Handle
-> FunctionBindings (Crux sym) sym LLVM
-> ExtensionImpl (Crux sym) sym LLVM
-> Crux sym
-> SimContext (Crux sym) sym LLVM
forall sym bak personality ext.
IsSymBackend sym bak =>
bak
-> IntrinsicTypes sym
-> HandleAllocator
-> Handle
-> FunctionBindings personality sym ext
-> ExtensionImpl personality sym ext
-> personality
-> SimContext personality sym ext
initSimContext bak
bak
(IntrinsicTypes sym -> IntrinsicTypes sym -> IntrinsicTypes sym
forall {v} (k :: v -> *) (a :: v -> *).
OrdF k =>
MapF k a -> MapF k a -> MapF k a
MapF.union IntrinsicTypes sym
forall sym. IsSymInterface sym => IntrinsicTypes sym
llvmIntrinsicTypes IntrinsicTypes sym
forall sym. IsSymInterface sym => IntrinsicTypes sym
llvmSymIOIntrinsicTypes)
HandleAllocator
halloc
Handle
stdout
([FnBinding (Crux sym) sym LLVM]
-> FunctionBindings (Crux sym) sym LLVM
forall p sym ext.
[FnBinding p sym ext] -> FunctionBindings p sym ext
fnBindingsFromList [])
(MemOptions -> ExtensionImpl (Crux sym) sym LLVM
forall sym p.
HasLLVMAnn sym =>
MemOptions -> ExtensionImpl p sym LLVM
llvmExtensionImpl MemOptions
mo)
Crux sym
forall sym. Crux sym
CruxPersonality
SimContext (Crux sym) sym LLVM
-> (SimContext (Crux sym) sym LLVM
-> SimContext (Crux sym) sym LLVM)
-> SimContext (Crux sym) sym LLVM
forall a b. a -> (a -> b) -> b
& (Map Text (Metric (Crux sym) sym LLVM)
-> Identity (Map Text (Metric (Crux sym) sym LLVM)))
-> SimContext (Crux sym) sym LLVM
-> Identity (SimContext (Crux sym) sym LLVM)
forall p sym ext (f :: * -> *).
Functor f =>
(Map Text (Metric p sym ext) -> f (Map Text (Metric p sym ext)))
-> SimContext p sym ext -> f (SimContext p sym ext)
profilingMetrics ((Map Text (Metric (Crux sym) sym LLVM)
-> Identity (Map Text (Metric (Crux sym) sym LLVM)))
-> SimContext (Crux sym) sym LLVM
-> Identity (SimContext (Crux sym) sym LLVM))
-> (Map Text (Metric (Crux sym) sym LLVM)
-> Map Text (Metric (Crux sym) sym LLVM))
-> SimContext (Crux sym) sym LLVM
-> SimContext (Crux sym) sym LLVM
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Map Text (Metric (Crux sym) sym LLVM)
-> Map Text (Metric (Crux sym) sym LLVM)
-> Map Text (Metric (Crux sym) sym LLVM)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (GlobalVar Mem -> Map Text (Metric (Crux sym) sym LLVM)
forall p sym ext. GlobalVar Mem -> Map Text (Metric p sym ext)
memMetrics GlobalVar Mem
memVar)
parseLLVM :: FilePath -> IO LLVM.Module
parseLLVM :: FilePath -> IO Module
parseLLVM FilePath
file =
do Either Error Module
ok <- FilePath -> IO (Either Error Module)
parseBitCodeFromFile FilePath
file
case Either Error Module
ok of
Left Error
err -> CError -> IO Module
forall (m :: * -> *) b. MonadIO m => CError -> m b
throwCError (Error -> CError
LLVMParseError Error
err)
Right Module
m -> Module -> IO Module
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Module
m
registerFunctions ::
Crux.Logs msgs =>
Log.SupportsCruxLLVMLogMessage msgs =>
(ArchOk arch, IsSymInterface sym, HasLLVMAnn sym, ptrW ~ ArchWidth arch) =>
LLVMOptions ->
LLVM.Module ->
ModuleTranslation arch ->
Maybe (LLVMFileSystem ptrW) ->
OverM Crux sym LLVM ()
registerFunctions :: forall msgs (arch :: LLVMArch) sym (ptrW :: Nat).
(Logs msgs, SupportsCruxLLVMLogMessage msgs, ArchOk arch,
IsSymInterface sym, HasLLVMAnn sym, ptrW ~ ArchWidth arch) =>
LLVMOptions
-> Module
-> ModuleTranslation arch
-> Maybe (LLVMFileSystem ptrW)
-> OverM Crux sym LLVM ()
registerFunctions LLVMOptions
llvmOpts Module
llvm_module ModuleTranslation arch
mtrans Maybe (LLVMFileSystem ptrW)
fs0 =
do let llvm_ctx :: LLVMContext arch
llvm_ctx = ModuleTranslation arch
mtrans ModuleTranslation arch
-> Getting
(LLVMContext arch) (ModuleTranslation arch) (LLVMContext arch)
-> LLVMContext arch
forall s a. s -> Getting a s a -> a
^. Getting
(LLVMContext arch) (ModuleTranslation arch) (LLVMContext arch)
forall (arch :: LLVMArch) (f :: * -> *).
(Contravariant f, Functor f) =>
(LLVMContext arch -> f (LLVMContext arch))
-> ModuleTranslation arch -> f (ModuleTranslation arch)
transContext
let ?lc = LLVMContext arch
llvm_ctx LLVMContext arch
-> Getting TypeContext (LLVMContext arch) TypeContext
-> TypeContext
forall s a. s -> Getting a s a -> a
^. Getting TypeContext (LLVMContext arch) TypeContext
forall (arch :: LLVMArch) (f :: * -> *).
Functor f =>
(TypeContext -> f TypeContext)
-> LLVMContext arch -> f (LLVMContext arch)
llvmTypeCtx
?intrinsicsOpts = LLVMOptions -> IntrinsicsOptions
intrinsicsOpts LLVMOptions
llvmOpts
?memOpts = LLVMOptions -> MemOptions
memOpts LLVMOptions
llvmOpts
Module
-> [OverrideTemplate (Crux sym) sym arch r args ret]
-> [OverrideTemplate (Crux sym) sym arch r args ret]
-> LLVMContext arch
-> OverrideSim (Crux sym) sym LLVM r args ret ()
forall sym (wptr :: Nat) (arch :: LLVMArch) p rtp
(l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
wptr ~ ArchWidth arch, ?intrinsicsOpts::IntrinsicsOptions,
?memOpts::MemOptions) =>
Module
-> [OverrideTemplate p sym arch rtp l a]
-> [OverrideTemplate p sym arch rtp l a]
-> LLVMContext arch
-> OverrideSim p sym LLVM rtp l a ()
register_llvm_overrides Module
llvm_module []
([[OverrideTemplate (Crux sym) sym arch r args ret]]
-> [OverrideTemplate (Crux sym) sym arch r args ret]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Proxy# arch -> [OverrideTemplate (Crux sym) sym arch r args ret]
forall sym (wptr :: Nat) (arch :: LLVMArch) (personality :: * -> *)
rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
wptr ~ ArchWidth arch, ?lc::TypeContext,
?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
Proxy# arch
-> [OverrideTemplate (personality sym) sym arch rtp l a]
cruxLLVMOverrides Proxy# arch
forall {k} (a :: k). Proxy# a
proxy#
, [OverrideTemplate (Crux sym) sym arch r args ret]
forall sym (wptr :: Nat) (personality :: * -> *) (arch :: LLVMArch)
rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
[OverrideTemplate (personality sym) sym arch rtp l a]
svCompOverrides
, Proxy# arch -> [OverrideTemplate (Crux sym) sym arch r args ret]
forall sym (wptr :: Nat) (arch :: LLVMArch) (personality :: * -> *)
rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
wptr ~ ArchWidth arch, ?lc::TypeContext,
?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
Proxy# arch
-> [OverrideTemplate (personality sym) sym arch rtp l a]
cbmcOverrides Proxy# arch
forall {k} (a :: k). Proxy# a
proxy#
, [OverrideTemplate (Crux sym) sym arch r args ret]
-> (LLVMFileSystem ptrW
-> [OverrideTemplate (Crux sym) sym arch r args ret])
-> Maybe (LLVMFileSystem ptrW)
-> [OverrideTemplate (Crux sym) sym arch r args ret]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] LLVMFileSystem ptrW
-> [OverrideTemplate (Crux sym) sym arch r args ret]
forall sym (wptr :: Nat) (arch :: LLVMArch) p rtp
(l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
wptr ~ ArchWidth arch, ?memOpts::MemOptions) =>
LLVMFileSystem wptr -> [OverrideTemplate p sym arch rtp l a]
symio_overrides Maybe (LLVMFileSystem ptrW)
fs0
])
LLVMContext arch
llvm_ctx
(LLVMTranslationWarning -> IO ())
-> ModuleTranslation arch
-> OverrideSim (Crux sym) sym LLVM r args ret ()
forall (arch :: LLVMArch) sym p rtp (l :: Ctx CrucibleType)
(a :: CrucibleType).
(1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch),
IsSymInterface sym) =>
(LLVMTranslationWarning -> IO ())
-> ModuleTranslation arch -> OverrideSim p sym LLVM rtp l a ()
registerLazyModule LLVMTranslationWarning -> IO ()
forall msgs.
(SupportsCruxLLVMLogMessage msgs, Logs msgs) =>
LLVMTranslationWarning -> IO ()
sayTranslationWarning ModuleTranslation arch
mtrans
simulateLLVMFile ::
Crux.Logs msgs =>
Log.SupportsCruxLLVMLogMessage msgs =>
FilePath ->
LLVMOptions ->
Crux.SimulatorCallbacks msgs Crux.Types.CruxSimulationResult
simulateLLVMFile :: forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
FilePath
-> LLVMOptions -> SimulatorCallbacks msgs CruxSimulationResult
simulateLLVMFile FilePath
llvm_file LLVMOptions
llvmOpts =
(forall sym bak t (st :: * -> *) fs.
(IsSymBackend sym bak, Logs msgs, sym ~ ExprBuilder t st fs) =>
IO (SimulatorHooks sym bak t CruxSimulationResult))
-> SimulatorCallbacks msgs CruxSimulationResult
forall msgs r.
(forall sym bak t (st :: * -> *) fs.
(IsSymBackend sym bak, Logs msgs, sym ~ ExprBuilder t st fs) =>
IO (SimulatorHooks sym bak t r))
-> SimulatorCallbacks msgs r
Crux.SimulatorCallbacks ((forall sym bak t (st :: * -> *) fs.
(IsSymBackend sym bak, Logs msgs, sym ~ ExprBuilder t st fs) =>
IO (SimulatorHooks sym bak t CruxSimulationResult))
-> SimulatorCallbacks msgs CruxSimulationResult)
-> (forall sym bak t (st :: * -> *) fs.
(IsSymBackend sym bak, Logs msgs, sym ~ ExprBuilder t st fs) =>
IO (SimulatorHooks sym bak t CruxSimulationResult))
-> SimulatorCallbacks msgs CruxSimulationResult
forall a b. (a -> b) -> a -> b
$
do IORef (LLVMAnnMap (ExprBuilder t st fs))
bbMapRef <- LLVMAnnMap (ExprBuilder t st fs)
-> IO (IORef (LLVMAnnMap (ExprBuilder t st fs)))
forall a. a -> IO (IORef a)
newIORef (Map (BoolAnn sym) (CallStack, BadBehavior sym)
forall {sym}. Map (BoolAnn sym) (CallStack, BadBehavior sym)
forall k a. Map k a
Map.empty :: LLVMAnnMap sym)
let ?recordLLVMAnnotation =
\CallStack
callStack BoolAnn (ExprBuilder t st fs)
an BadBehavior (ExprBuilder t st fs)
bb ->
IORef (LLVMAnnMap (ExprBuilder t st fs))
-> (LLVMAnnMap (ExprBuilder t st fs)
-> LLVMAnnMap (ExprBuilder t st fs))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef (LLVMAnnMap (ExprBuilder t st fs))
bbMapRef (BoolAnn (ExprBuilder t st fs)
-> (CallStack, BadBehavior (ExprBuilder t st fs))
-> LLVMAnnMap (ExprBuilder t st fs)
-> LLVMAnnMap (ExprBuilder t st fs)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert BoolAnn (ExprBuilder t st fs)
an (CallStack
callStack, BadBehavior (ExprBuilder t st fs)
bb))
SimulatorHooks sym bak t CruxSimulationResult
-> IO (SimulatorHooks sym bak t CruxSimulationResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimulatorHooks sym bak t CruxSimulationResult
-> IO (SimulatorHooks sym bak t CruxSimulationResult))
-> SimulatorHooks sym bak t CruxSimulationResult
-> IO (SimulatorHooks sym bak t CruxSimulationResult)
forall a b. (a -> b) -> a -> b
$
Crux.SimulatorHooks
{ setupHook :: bak -> Maybe (SomeOnlineSolver sym bak) -> IO (RunnableState sym)
Crux.setupHook =
\bak
bak Maybe (SomeOnlineSolver sym bak)
maybeOnline ->
do HandleAllocator
halloc <- IO HandleAllocator
newHandleAllocator
HandleAllocator
-> FilePath
-> LLVMOptions
-> bak
-> Maybe (SomeOnlineSolver sym bak)
-> IO (RunnableState sym)
forall sym bak t (st :: * -> *) fs msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs, IsSymBackend sym bak,
sym ~ ExprBuilder t st fs, HasLLVMAnn sym) =>
HandleAllocator
-> FilePath
-> LLVMOptions
-> bak
-> Maybe (SomeOnlineSolver sym bak)
-> IO (RunnableState sym)
setupFileSim HandleAllocator
halloc FilePath
llvm_file LLVMOptions
llvmOpts bak
bak Maybe (SomeOnlineSolver sym bak)
maybeOnline
, onErrorHook :: bak -> IO (Explainer sym t Void)
Crux.onErrorHook =
\bak
bak -> (Maybe (GroundEvalFn t)
-> LabeledPred (Expr t BaseBoolType) SimError -> IO (Doc Void))
-> IO
(Maybe (GroundEvalFn t)
-> LabeledPred (Expr t BaseBoolType) SimError -> IO (Doc Void))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExprBuilder t st fs
-> IORef (LLVMAnnMap (ExprBuilder t st fs))
-> Explainer (ExprBuilder t st fs) t Void
forall sym t (st :: * -> *) fs ann.
(IsSymInterface sym, sym ~ ExprBuilder t st fs) =>
sym -> IORef (LLVMAnnMap sym) -> Explainer sym t ann
explainFailure (bak -> ExprBuilder t st fs
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak) IORef (LLVMAnnMap (ExprBuilder t st fs))
bbMapRef)
, resultHook :: bak -> CruxSimulationResult -> IO CruxSimulationResult
Crux.resultHook = \bak
_sym CruxSimulationResult
result -> CruxSimulationResult -> IO CruxSimulationResult
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CruxSimulationResult
result
}
setupFileSim :: forall sym bak t st fs msgs
. Crux.Logs msgs
=> Log.SupportsCruxLLVMLogMessage msgs
=> IsSymBackend sym bak
=> sym ~ WEB.ExprBuilder t st fs
=> HasLLVMAnn sym
=> HandleAllocator
-> FilePath
-> LLVMOptions
-> bak
-> Maybe (Crux.SomeOnlineSolver sym bak)
-> IO (Crux.RunnableState sym)
setupFileSim :: forall sym bak t (st :: * -> *) fs msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs, IsSymBackend sym bak,
sym ~ ExprBuilder t st fs, HasLLVMAnn sym) =>
HandleAllocator
-> FilePath
-> LLVMOptions
-> bak
-> Maybe (SomeOnlineSolver sym bak)
-> IO (RunnableState sym)
setupFileSim HandleAllocator
halloc FilePath
llvm_file LLVMOptions
llvmOpts bak
bak Maybe (SomeOnlineSolver sym bak)
_maybeOnline =
do let sym :: ExprBuilder t st fs
sym = bak -> ExprBuilder t st fs
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
GlobalVar Mem
memVar <- Text -> HandleAllocator -> IO (GlobalVar Mem)
mkMemVar Text
"crux:llvm_memory" HandleAllocator
halloc
let simctx :: SimContext (Crux (ExprBuilder t st fs)) (ExprBuilder t st fs) LLVM
simctx = (HandleAllocator
-> bak
-> MemOptions
-> GlobalVar Mem
-> SimContext
(Crux (ExprBuilder t st fs)) (ExprBuilder t st fs) LLVM
forall sym bak.
(IsSymBackend sym bak, HasLLVMAnn sym) =>
HandleAllocator
-> bak -> MemOptions -> GlobalVar Mem -> SimCtxt Crux sym LLVM
setupSimCtxt HandleAllocator
halloc bak
bak (LLVMOptions -> MemOptions
memOpts LLVMOptions
llvmOpts) GlobalVar Mem
memVar)
{ printHandle = view outputHandle ?outputConfig }
PreppedLLVM (ExprBuilder t st fs)
prepped <- LLVMOptions
-> HandleAllocator
-> bak
-> FilePath
-> GlobalVar Mem
-> IO (PreppedLLVM (ExprBuilder t st fs))
forall sym bak msgs.
(IsSymBackend sym bak, HasLLVMAnn sym, Logs msgs,
SupportsCruxLLVMLogMessage msgs) =>
LLVMOptions
-> HandleAllocator
-> bak
-> FilePath
-> GlobalVar Mem
-> IO (PreppedLLVM sym)
prepLLVMModule LLVMOptions
llvmOpts HandleAllocator
halloc bak
bak FilePath
llvm_file GlobalVar Mem
memVar
let globSt :: SymGlobalState (ExprBuilder t st fs)
globSt = GlobalVar Mem
-> MemImpl (ExprBuilder t st fs)
-> SymGlobalState (ExprBuilder t st fs)
forall sym. GlobalVar Mem -> MemImpl sym -> SymGlobalState sym
llvmGlobals GlobalVar Mem
memVar (PreppedLLVM (ExprBuilder t st fs) -> MemImpl (ExprBuilder t st fs)
forall sym. PreppedLLVM sym -> MemImpl sym
prepMem PreppedLLVM (ExprBuilder t st fs)
prepped)
Some ModuleTranslation x
trans <- Some ModuleTranslation -> IO (Some ModuleTranslation)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Some ModuleTranslation -> IO (Some ModuleTranslation))
-> Some ModuleTranslation -> IO (Some ModuleTranslation)
forall a b. (a -> b) -> a -> b
$ PreppedLLVM (ExprBuilder t st fs) -> Some ModuleTranslation
forall sym. PreppedLLVM sym -> Some ModuleTranslation
prepSomeTrans PreppedLLVM (ExprBuilder t st fs)
prepped
LLVMContext x
-> forall a.
((16 <= ArchWidth x) => NatRepr (ArchWidth x) -> a) -> a
forall (arch :: LLVMArch).
LLVMContext arch
-> forall a.
((16 <= ArchWidth arch) => NatRepr (ArchWidth arch) -> a) -> a
llvmPtrWidth (ModuleTranslation x
trans ModuleTranslation x
-> Getting (LLVMContext x) (ModuleTranslation x) (LLVMContext x)
-> LLVMContext x
forall s a. s -> Getting a s a -> a
^. Getting (LLVMContext x) (ModuleTranslation x) (LLVMContext x)
forall (arch :: LLVMArch) (f :: * -> *).
(Contravariant f, Functor f) =>
(LLVMContext arch -> f (LLVMContext arch))
-> ModuleTranslation arch -> f (ModuleTranslation arch)
transContext) (((16 <= ArchWidth x) =>
NatRepr (ArchWidth x) -> IO (RunnableState sym))
-> IO (RunnableState sym))
-> ((16 <= ArchWidth x) =>
NatRepr (ArchWidth x) -> IO (RunnableState sym))
-> IO (RunnableState sym)
forall a b. (a -> b) -> a -> b
$ \NatRepr (ArchWidth x)
ptrW -> NatRepr (ArchWidth x)
-> (HasPtrWidth (ArchWidth x) => IO (RunnableState sym))
-> IO (RunnableState sym)
forall (w :: Nat) a.
(16 <= w) =>
NatRepr w -> (HasPtrWidth w => a) -> a
withPtrWidth NatRepr (ArchWidth x)
ptrW ((HasPtrWidth (ArchWidth x) => IO (RunnableState sym))
-> IO (RunnableState sym))
-> (HasPtrWidth (ArchWidth x) => IO (RunnableState sym))
-> IO (RunnableState sym)
forall a b. (a -> b) -> a -> b
$ do
Maybe (InitialFileSystemContents (ExprBuilder t st fs))
mContents <- (FilePath -> IO (InitialFileSystemContents (ExprBuilder t st fs)))
-> Maybe FilePath
-> IO (Maybe (InitialFileSystemContents (ExprBuilder t st fs)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
T.traverse (ExprBuilder t st fs
-> FilePath -> IO (InitialFileSystemContents (ExprBuilder t st fs))
forall sym.
IsSymInterface sym =>
sym -> FilePath -> IO (InitialFileSystemContents sym)
SymIO.Loader.loadInitialFiles ExprBuilder t st fs
sym) (LLVMOptions -> Maybe FilePath
symFSRoot LLVMOptions
llvmOpts)
let defaultFileContents :: InitialFileSystemContents (ExprBuilder t st fs)
defaultFileContents = (forall sym. InitialFileSystemContents sym
SymIO.emptyInitialFileSystemContents @sym)
{ SymIO.useStderr = True
, SymIO.useStdout = True
, SymIO.concreteFiles = Map.fromList [(SymIO.StdinTarget, mempty)]
}
let fsContents :: InitialFileSystemContents (ExprBuilder t st fs)
fsContents = InitialFileSystemContents (ExprBuilder t st fs)
-> Maybe (InitialFileSystemContents (ExprBuilder t st fs))
-> InitialFileSystemContents (ExprBuilder t st fs)
forall a. a -> Maybe a -> a
fromMaybe InitialFileSystemContents (ExprBuilder t st fs)
defaultFileContents Maybe (InitialFileSystemContents (ExprBuilder t st fs))
mContents
let mirroredOutputs :: [(FDTarget 'Out, Handle)]
mirroredOutputs = [ (FDTarget 'Out
SymIO.StdoutTarget, Logs msgs
OutputConfig msgs
?outputConfig OutputConfig msgs
-> Getting Handle (OutputConfig msgs) Handle -> Handle
forall s a. s -> Getting a s a -> a
^. Getting Handle (OutputConfig msgs) Handle
forall msgs (f :: * -> *).
(Contravariant f, Functor f) =>
(Handle -> f Handle) -> OutputConfig msgs -> f (OutputConfig msgs)
Crux.outputHandle)
, (FDTarget 'Out
SymIO.StderrTarget, Logs msgs
OutputConfig msgs
?outputConfig OutputConfig msgs
-> Getting Handle (OutputConfig msgs) Handle -> Handle
forall s a. s -> Getting a s a -> a
^. Getting Handle (OutputConfig msgs) Handle
forall msgs (f :: * -> *).
(Contravariant f, Functor f) =>
(Handle -> f Handle) -> OutputConfig msgs -> f (OutputConfig msgs)
Crux.outputHandle)
]
(LLVMFileSystem (ArchWidth x)
fs0, SymGlobalState (ExprBuilder t st fs)
globSt', SomeOverrideSim forall p ext rtp (args :: Ctx CrucibleType) (ret :: CrucibleType).
OverrideSim p (ExprBuilder t st fs) ext rtp args ret ()
initFSOverride) <- HandleAllocator
-> ExprBuilder t st fs
-> NatRepr (ArchWidth x)
-> InitialFileSystemContents (ExprBuilder t st fs)
-> [(FDTarget 'Out, Handle)]
-> SymGlobalState (ExprBuilder t st fs)
-> IO
(LLVMFileSystem (ArchWidth x),
SymGlobalState (ExprBuilder t st fs),
SomeOverrideSim (ExprBuilder t st fs) ())
forall sym (ptrW :: Nat).
(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 ExprBuilder t st fs
sym NatRepr (ArchWidth x)
ptrW InitialFileSystemContents (ExprBuilder t st fs)
fsContents [(FDTarget 'Out, Handle)]
mirroredOutputs SymGlobalState (ExprBuilder t st fs)
globSt
RunnableState sym -> IO (RunnableState sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (RunnableState sym -> IO (RunnableState sym))
-> RunnableState sym -> IO (RunnableState sym)
forall a b. (a -> b) -> a -> b
$ ExecState (Crux sym) sym LLVM (RegEntry sym UnitType)
-> RunnableState sym
forall sym ext (personality :: * -> *).
IsSyntaxExtension ext =>
ExecState (personality sym) sym ext (RegEntry sym UnitType)
-> RunnableState sym
Crux.RunnableState (ExecState (Crux sym) sym LLVM (RegEntry sym UnitType)
-> RunnableState sym)
-> ExecState (Crux sym) sym LLVM (RegEntry sym UnitType)
-> RunnableState sym
forall a b. (a -> b) -> a -> b
$
SimContext (Crux sym) sym LLVM
-> SymGlobalState sym
-> AbortHandler (Crux sym) sym LLVM (RegEntry sym UnitType)
-> TypeRepr UnitType
-> ExecCont
(Crux sym)
sym
LLVM
(RegEntry sym UnitType)
(OverrideLang UnitType)
('Just EmptyCtx)
-> ExecState (Crux sym) sym LLVM (RegEntry sym UnitType)
forall p sym ext rtp (ret :: CrucibleType).
(rtp ~ RegEntry sym ret) =>
SimContext p sym ext
-> SymGlobalState sym
-> AbortHandler p sym ext (RegEntry sym ret)
-> TypeRepr ret
-> ExecCont
p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
-> ExecState p sym ext rtp
InitialState SimContext (Crux sym) sym LLVM
SimContext (Crux (ExprBuilder t st fs)) (ExprBuilder t st fs) LLVM
simctx SymGlobalState sym
SymGlobalState (ExprBuilder t st fs)
globSt' AbortHandler (Crux sym) sym LLVM (RegEntry sym UnitType)
forall sym p ext rtp.
IsSymInterface sym =>
AbortHandler p sym ext rtp
defaultAbortHandler TypeRepr UnitType
UnitRepr (ExecCont
(Crux sym)
sym
LLVM
(RegEntry sym UnitType)
(OverrideLang UnitType)
('Just EmptyCtx)
-> ExecState (Crux sym) sym LLVM (RegEntry sym UnitType))
-> ExecCont
(Crux sym)
sym
LLVM
(RegEntry sym UnitType)
(OverrideLang UnitType)
('Just EmptyCtx)
-> ExecState (Crux sym) sym LLVM (RegEntry sym UnitType)
forall a b. (a -> b) -> a -> b
$
TypeRepr UnitType
-> OverrideSim
(Crux sym)
sym
LLVM
(RegEntry sym UnitType)
EmptyCtx
UnitType
(RegValue sym UnitType)
-> ExecCont
(Crux sym)
sym
LLVM
(RegEntry sym UnitType)
(OverrideLang UnitType)
('Just EmptyCtx)
forall (tp :: CrucibleType) p sym ext rtp
(args :: Ctx CrucibleType).
TypeRepr tp
-> OverrideSim p sym ext rtp args tp (RegValue sym tp)
-> ExecCont p sym ext rtp (OverrideLang tp) ('Just args)
runOverrideSim TypeRepr UnitType
UnitRepr (OverrideSim
(Crux sym)
sym
LLVM
(RegEntry sym UnitType)
EmptyCtx
UnitType
(RegValue sym UnitType)
-> ExecCont
(Crux sym)
sym
LLVM
(RegEntry sym UnitType)
(OverrideLang UnitType)
('Just EmptyCtx))
-> OverrideSim
(Crux sym)
sym
LLVM
(RegEntry sym UnitType)
EmptyCtx
UnitType
(RegValue sym UnitType)
-> ExecCont
(Crux sym)
sym
LLVM
(RegEntry sym UnitType)
(OverrideLang UnitType)
('Just EmptyCtx)
forall a b. (a -> b) -> a -> b
$
NatRepr (ArchWidth x)
-> (HasPtrWidth (ArchWidth x) =>
OverrideSim
(Crux sym)
sym
LLVM
(RegEntry sym UnitType)
EmptyCtx
UnitType
(RegValue sym UnitType))
-> OverrideSim
(Crux sym)
sym
LLVM
(RegEntry sym UnitType)
EmptyCtx
UnitType
(RegValue sym UnitType)
forall (w :: Nat) a.
(16 <= w) =>
NatRepr w -> (HasPtrWidth w => a) -> a
withPtrWidth NatRepr (ArchWidth x)
ptrW ((HasPtrWidth (ArchWidth x) =>
OverrideSim
(Crux sym)
sym
LLVM
(RegEntry sym UnitType)
EmptyCtx
UnitType
(RegValue sym UnitType))
-> OverrideSim
(Crux sym)
sym
LLVM
(RegEntry sym UnitType)
EmptyCtx
UnitType
(RegValue sym UnitType))
-> (HasPtrWidth (ArchWidth x) =>
OverrideSim
(Crux sym)
sym
LLVM
(RegEntry sym UnitType)
EmptyCtx
UnitType
(RegValue sym UnitType))
-> OverrideSim
(Crux sym)
sym
LLVM
(RegEntry sym UnitType)
EmptyCtx
UnitType
(RegValue sym UnitType)
forall a b. (a -> b) -> a -> b
$
do LLVMOptions
-> Module
-> ModuleTranslation x
-> Maybe (LLVMFileSystem (ArchWidth x))
-> OverM Crux sym LLVM ()
forall msgs (arch :: LLVMArch) sym (ptrW :: Nat).
(Logs msgs, SupportsCruxLLVMLogMessage msgs, ArchOk arch,
IsSymInterface sym, HasLLVMAnn sym, ptrW ~ ArchWidth arch) =>
LLVMOptions
-> Module
-> ModuleTranslation arch
-> Maybe (LLVMFileSystem ptrW)
-> OverM Crux sym LLVM ()
registerFunctions LLVMOptions
llvmOpts (PreppedLLVM (ExprBuilder t st fs) -> Module
forall sym. PreppedLLVM sym -> Module
prepLLVMMod PreppedLLVM (ExprBuilder t st fs)
prepped) ModuleTranslation x
trans (LLVMFileSystem (ArchWidth x)
-> Maybe (LLVMFileSystem (ArchWidth x))
forall a. a -> Maybe a
Just LLVMFileSystem (ArchWidth x)
fs0)
OverrideSim
(Crux sym) sym LLVM (RegEntry sym UnitType) EmptyCtx UnitType ()
OverrideSim
(Crux sym)
(ExprBuilder t st fs)
LLVM
(RegEntry sym UnitType)
EmptyCtx
UnitType
()
forall p ext rtp (args :: Ctx CrucibleType) (ret :: CrucibleType).
OverrideSim p (ExprBuilder t st fs) ext rtp args ret ()
initFSOverride
LLVMOptions
-> ModuleTranslation x -> GlobalVar Mem -> OverM Crux sym LLVM ()
forall (arch :: LLVMArch) msgs (personality :: * -> *) sym.
(IsSymInterface sym, HasLLVMAnn sym, ArchOk arch, Logs msgs,
SupportsCruxLLVMLogMessage msgs) =>
LLVMOptions
-> ModuleTranslation arch
-> GlobalVar Mem
-> OverM personality sym LLVM ()
checkFun LLVMOptions
llvmOpts ModuleTranslation x
trans GlobalVar Mem
memVar
data PreppedLLVM sym = PreppedLLVM { forall sym. PreppedLLVM sym -> Module
prepLLVMMod :: LLVM.Module
, forall sym. PreppedLLVM sym -> Some ModuleTranslation
prepSomeTrans :: Some ModuleTranslation
, forall sym. PreppedLLVM sym -> GlobalVar Mem
prepMemVar :: GlobalVar Mem
, forall sym. PreppedLLVM sym -> MemImpl sym
prepMem :: MemImpl sym
}
prepLLVMModule :: IsSymBackend sym bak
=> HasLLVMAnn sym
=> Crux.Logs msgs
=> Log.SupportsCruxLLVMLogMessage msgs
=> LLVMOptions
-> HandleAllocator
-> bak
-> FilePath
-> GlobalVar Mem
-> IO (PreppedLLVM sym)
prepLLVMModule :: forall sym bak msgs.
(IsSymBackend sym bak, HasLLVMAnn sym, Logs msgs,
SupportsCruxLLVMLogMessage msgs) =>
LLVMOptions
-> HandleAllocator
-> bak
-> FilePath
-> GlobalVar Mem
-> IO (PreppedLLVM sym)
prepLLVMModule LLVMOptions
llvmOpts HandleAllocator
halloc bak
bak FilePath
bcFile GlobalVar Mem
memVar = do
Module
llvmMod <- FilePath -> IO Module
parseLLVM FilePath
bcFile
Some ModuleTranslation x
trans <-
let ?transOpts = LLVMOptions -> TranslationOptions
transOpts LLVMOptions
llvmOpts
in (?transOpts::TranslationOptions) =>
HandleAllocator
-> GlobalVar Mem -> Module -> IO (Some ModuleTranslation)
HandleAllocator
-> GlobalVar Mem -> Module -> IO (Some ModuleTranslation)
translateModule HandleAllocator
halloc GlobalVar Mem
memVar Module
llvmMod
MemImpl sym
mem <- let llvmCtxt :: LLVMContext x
llvmCtxt = ModuleTranslation x
trans ModuleTranslation x
-> Getting (LLVMContext x) (ModuleTranslation x) (LLVMContext x)
-> LLVMContext x
forall s a. s -> Getting a s a -> a
^. Getting (LLVMContext x) (ModuleTranslation x) (LLVMContext x)
forall (arch :: LLVMArch) (f :: * -> *).
(Contravariant f, Functor f) =>
(LLVMContext arch -> f (LLVMContext arch))
-> ModuleTranslation arch -> f (ModuleTranslation arch)
transContext in
let ?lc = LLVMContext x
llvmCtxt LLVMContext x
-> Getting TypeContext (LLVMContext x) TypeContext -> TypeContext
forall s a. s -> Getting a s a -> a
^. Getting TypeContext (LLVMContext x) TypeContext
forall (arch :: LLVMArch) (f :: * -> *).
Functor f =>
(TypeContext -> f TypeContext)
-> LLVMContext arch -> f (LLVMContext arch)
llvmTypeCtx
?memOpts = LLVMOptions -> MemOptions
memOpts LLVMOptions
llvmOpts
in LLVMContext x
-> forall a.
((16 <= ArchWidth x) => NatRepr (ArchWidth x) -> a) -> a
forall (arch :: LLVMArch).
LLVMContext arch
-> forall a.
((16 <= ArchWidth arch) => NatRepr (ArchWidth arch) -> a) -> a
llvmPtrWidth LLVMContext x
llvmCtxt (((16 <= ArchWidth x) => NatRepr (ArchWidth x) -> IO (MemImpl sym))
-> IO (MemImpl sym))
-> ((16 <= ArchWidth x) =>
NatRepr (ArchWidth x) -> IO (MemImpl sym))
-> IO (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ \NatRepr (ArchWidth x)
ptrW ->
NatRepr (ArchWidth x)
-> (HasPtrWidth (ArchWidth x) => IO (MemImpl sym))
-> IO (MemImpl sym)
forall (w :: Nat) a.
(16 <= w) =>
NatRepr w -> (HasPtrWidth w => a) -> a
withPtrWidth NatRepr (ArchWidth x)
ptrW ((HasPtrWidth (ArchWidth x) => IO (MemImpl sym))
-> IO (MemImpl sym))
-> (HasPtrWidth (ArchWidth x) => IO (MemImpl sym))
-> IO (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ do
CruxLLVMLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
CruxLLVMLogMessage -> IO ()
Log.sayCruxLLVM (Integer -> Text -> CruxLLVMLogMessage
Log.UsingPointerWidthForFile (NatRepr (ArchWidth x) -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr (ArchWidth x)
ptrW) (FilePath -> Text
Text.pack FilePath
bcFile))
bak -> GlobalInitializerMap -> MemImpl sym -> IO (MemImpl sym)
forall (wptr :: Nat) sym bak.
(?lc::TypeContext, ?memOpts::MemOptions, 16 <= wptr,
HasPtrWidth wptr, HasLLVMAnn sym, IsSymBackend sym bak) =>
bak -> GlobalInitializerMap -> MemImpl sym -> IO (MemImpl sym)
populateAllGlobals bak
bak (ModuleTranslation x
trans ModuleTranslation x
-> Getting
GlobalInitializerMap (ModuleTranslation x) GlobalInitializerMap
-> GlobalInitializerMap
forall s a. s -> Getting a s a -> a
^. Getting
GlobalInitializerMap (ModuleTranslation x) GlobalInitializerMap
forall (arch :: LLVMArch) (f :: * -> *).
(Contravariant f, Functor f) =>
(GlobalInitializerMap -> f GlobalInitializerMap)
-> ModuleTranslation arch -> f (ModuleTranslation arch)
globalInitMap)
(MemImpl sym -> IO (MemImpl sym))
-> IO (MemImpl sym) -> IO (MemImpl sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< bak -> LLVMContext x -> Module -> IO (MemImpl sym)
forall sym bak (wptr :: Nat) (arch :: LLVMArch).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
?memOpts::MemOptions) =>
bak -> LLVMContext arch -> Module -> IO (MemImpl sym)
initializeAllMemory bak
bak LLVMContext x
llvmCtxt Module
llvmMod
PreppedLLVM sym -> IO (PreppedLLVM sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (PreppedLLVM sym -> IO (PreppedLLVM sym))
-> PreppedLLVM sym -> IO (PreppedLLVM sym)
forall a b. (a -> b) -> a -> b
$ Module
-> Some ModuleTranslation
-> GlobalVar Mem
-> MemImpl sym
-> PreppedLLVM sym
forall sym.
Module
-> Some ModuleTranslation
-> GlobalVar Mem
-> MemImpl sym
-> PreppedLLVM sym
PreppedLLVM Module
llvmMod (ModuleTranslation x -> Some ModuleTranslation
forall k (f :: k -> *) (x :: k). f x -> Some f
Some ModuleTranslation x
trans) GlobalVar Mem
memVar MemImpl sym
mem
sayTranslationWarning ::
Log.SupportsCruxLLVMLogMessage msgs =>
Crux.Logs msgs =>
LLVMTranslationWarning -> IO ()
sayTranslationWarning :: forall msgs.
(SupportsCruxLLVMLogMessage msgs, Logs msgs) =>
LLVMTranslationWarning -> IO ()
sayTranslationWarning = CruxLLVMLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
CruxLLVMLogMessage -> IO ()
Log.sayCruxLLVM (CruxLLVMLogMessage -> IO ())
-> (LLVMTranslationWarning -> CruxLLVMLogMessage)
-> LLVMTranslationWarning
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LLVMTranslationWarning -> CruxLLVMLogMessage
f
where
f :: LLVMTranslationWarning -> CruxLLVMLogMessage
f (LLVMTranslationWarning Symbol
s Position
p Text
msg) =
Text -> Text -> Text -> CruxLLVMLogMessage
Log.TranslationWarning (FilePath -> Text
Text.pack (Doc -> FilePath
forall a. Show a => a -> FilePath
show (Symbol -> Doc
ppSymbol Symbol
s))) (FilePath -> Text
Text.pack (Position -> FilePath
forall a. Show a => a -> FilePath
show Position
p)) Text
msg
checkFun ::
forall arch msgs personality sym.
IsSymInterface sym =>
HasLLVMAnn sym =>
ArchOk arch =>
Crux.Logs msgs =>
Log.SupportsCruxLLVMLogMessage msgs =>
LLVMOptions ->
ModuleTranslation arch ->
GlobalVar Mem ->
OverM personality sym LLVM ()
checkFun :: forall (arch :: LLVMArch) msgs (personality :: * -> *) sym.
(IsSymInterface sym, HasLLVMAnn sym, ArchOk arch, Logs msgs,
SupportsCruxLLVMLogMessage msgs) =>
LLVMOptions
-> ModuleTranslation arch
-> GlobalVar Mem
-> OverM personality sym LLVM ()
checkFun LLVMOptions
llvmOpts ModuleTranslation arch
trans GlobalVar Mem
memVar =
IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
-> OverrideSim
(personality sym)
sym
LLVM
r
args
ret
(Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
forall a.
IO a -> OverrideSim (personality sym) sym LLVM r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (ModuleTranslation arch
-> Symbol
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
forall (arch :: LLVMArch).
ModuleTranslation arch
-> Symbol
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
getTranslatedCFG ModuleTranslation arch
trans (FilePath -> Symbol
forall a. IsString a => FilePath -> a
fromString FilePath
nm)) OverrideSim
(personality sym)
sym
LLVM
r
args
ret
(Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
-> (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])
-> OverrideSim (personality sym) sym LLVM r args ret ())
-> OverrideSim (personality sym) sym LLVM r args ret ()
forall a b.
OverrideSim (personality sym) sym LLVM r args ret a
-> (a -> OverrideSim (personality sym) sym LLVM r args ret b)
-> OverrideSim (personality sym) sym LLVM r args ret b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just (Declare
_, AnyCFG CFG LLVM blocks init ret
anyCfg, [LLVMTranslationWarning]
warns) ->
do IO () -> OverrideSim (personality sym) sym LLVM r args ret ()
forall a.
IO a -> OverrideSim (personality sym) sym LLVM r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ((LLVMTranslationWarning -> IO ())
-> [LLVMTranslationWarning] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ LLVMTranslationWarning -> IO ()
forall msgs.
(SupportsCruxLLVMLogMessage msgs, Logs msgs) =>
LLVMTranslationWarning -> IO ()
sayTranslationWarning [LLVMTranslationWarning]
warns)
case CFG LLVM blocks init ret -> CtxRepr init
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> CtxRepr init
cfgArgTypes CFG LLVM blocks init ret
anyCfg of
CtxRepr init
Empty -> CFG LLVM blocks init ret
-> RegMap sym init -> OverM personality sym LLVM ()
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
(ret :: CrucibleType).
CFG LLVM blocks ctx ret
-> RegMap sym ctx -> OverM personality sym LLVM ()
simulateFun CFG LLVM blocks init ret
anyCfg RegMap sym init
RegMap sym EmptyCtx
forall sym. RegMap sym EmptyCtx
emptyRegMap
(Assignment TypeRepr ctx
Empty :> LLVMPointerRepr NatRepr w
w :> TypeRepr tp
PtrRepr)
| Bool
isMain, Bool
shouldSupplyMainArguments
, Just w :~: 32
Refl <- NatRepr w -> NatRepr 32 -> Maybe (w :~: 32)
forall (a :: Nat) (b :: Nat).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @32)
-> CFG
LLVM
blocks
((EmptyCtx ::> LLVMPointerType 32)
::> LLVMPointerType (ArchWidth arch))
ret
-> OverM personality sym LLVM ()
forall (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
CFG
LLVM
blocks
((EmptyCtx ::> LLVMPointerType 32)
::> LLVMPointerType (ArchWidth arch))
ret
-> OverM personality sym LLVM ()
checkMainWithArguments CFG LLVM blocks init ret
CFG
LLVM
blocks
((EmptyCtx ::> LLVMPointerType 32)
::> LLVMPointerType (ArchWidth arch))
ret
anyCfg
CtxRepr init
_ -> CError -> OverrideSim (personality sym) sym LLVM r args ret ()
forall (m :: * -> *) b. MonadIO m => CError -> m b
throwCError (FilePath -> Bool -> CError
BadFun FilePath
nm Bool
isMain)
Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])
Nothing -> CError -> OverrideSim (personality sym) sym LLVM r args ret ()
forall (m :: * -> *) b. MonadIO m => CError -> m b
throwCError (FilePath -> CError
MissingFun FilePath
nm)
where
nm :: FilePath
nm = LLVMOptions -> FilePath
entryPoint LLVMOptions
llvmOpts
isMain :: Bool
isMain = FilePath
nm FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
"main"
shouldSupplyMainArguments :: Bool
shouldSupplyMainArguments =
case LLVMOptions -> SupplyMainArguments
supplyMainArguments LLVMOptions
llvmOpts of
SupplyMainArguments
NoArguments -> Bool
False
SupplyMainArguments
EmptyArguments -> Bool
True
simulateFun :: CFG LLVM blocks ctx ret ->
RegMap sym ctx ->
OverM personality sym LLVM ()
simulateFun :: forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
(ret :: CrucibleType).
CFG LLVM blocks ctx ret
-> RegMap sym ctx -> OverM personality sym LLVM ()
simulateFun CFG LLVM blocks ctx ret
anyCfg RegMap sym ctx
args = do
IO () -> OverrideSim (personality sym) sym LLVM r args ret ()
forall a.
IO a -> OverrideSim (personality sym) sym LLVM r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim (personality sym) sym LLVM r args ret ())
-> IO () -> OverrideSim (personality sym) sym LLVM r args ret ()
forall a b. (a -> b) -> a -> b
$ CruxLLVMLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
CruxLLVMLogMessage -> IO ()
Log.sayCruxLLVM (Text -> CruxLLVMLogMessage
Log.SimulatingFunction (FilePath -> Text
Text.pack FilePath
nm))
CFG LLVM blocks ctx ret
-> RegMap sym ctx
-> OverrideSim
(personality sym) sym LLVM r args ret (RegEntry sym ret)
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType) sym p rtp
(a :: Ctx CrucibleType) (r :: CrucibleType).
IsSyntaxExtension ext =>
CFG ext blocks init ret
-> RegMap sym init
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
callCFG CFG LLVM blocks ctx ret
anyCfg RegMap sym ctx
args OverrideSim
(personality sym) sym LLVM r args ret (RegEntry sym ret)
-> OverrideSim (personality sym) sym LLVM r args ret ()
-> OverrideSim (personality sym) sym LLVM r args ret ()
forall a b.
OverrideSim (personality sym) sym LLVM r args ret a
-> OverrideSim (personality sym) sym LLVM r args ret b
-> OverrideSim (personality sym) sym LLVM r args ret b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> OverrideSim (personality sym) sym LLVM r args ret ()
forall a. a -> OverrideSim (personality sym) sym LLVM r args ret a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkMainWithArguments ::
CFG LLVM blocks (EmptyCtx ::> LLVMPointerType 32 ::> TPtr arch) ret ->
OverM personality sym LLVM ()
checkMainWithArguments :: forall (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
CFG
LLVM
blocks
((EmptyCtx ::> LLVMPointerType 32)
::> LLVMPointerType (ArchWidth arch))
ret
-> OverM personality sym LLVM ()
checkMainWithArguments CFG
LLVM
blocks
((EmptyCtx ::> LLVMPointerType 32)
::> LLVMPointerType (ArchWidth arch))
ret
anyCfg = (forall bak.
IsSymBackend sym bak =>
bak -> OverrideSim (personality sym) sym LLVM r args ret ())
-> OverrideSim (personality sym) sym LLVM r args ret ()
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 (personality sym) sym LLVM r args ret ())
-> OverrideSim (personality sym) sym LLVM r args ret ())
-> (forall bak.
IsSymBackend sym bak =>
bak -> OverrideSim (personality sym) sym LLVM r args ret ())
-> OverrideSim (personality sym) sym LLVM r args ret ()
forall a b. (a -> b) -> a -> b
$ \bak
bak -> do
let ?memOpts = LLVMOptions -> MemOptions
memOpts LLVMOptions
llvmOpts
let w :: NatRepr 32
w = forall (n :: Nat). KnownNat n => NatRepr n
knownNat @32
dl :: DataLayout
dl = TypeContext -> DataLayout
llvmDataLayout (ModuleTranslation arch
transModuleTranslation arch
-> Getting TypeContext (ModuleTranslation arch) TypeContext
-> TypeContext
forall s a. s -> Getting a s a -> a
^.(LLVMContext arch -> Const TypeContext (LLVMContext arch))
-> ModuleTranslation arch
-> Const TypeContext (ModuleTranslation arch)
forall (arch :: LLVMArch) (f :: * -> *).
(Contravariant f, Functor f) =>
(LLVMContext arch -> f (LLVMContext arch))
-> ModuleTranslation arch -> f (ModuleTranslation arch)
transContext((LLVMContext arch -> Const TypeContext (LLVMContext arch))
-> ModuleTranslation arch
-> Const TypeContext (ModuleTranslation arch))
-> ((TypeContext -> Const TypeContext TypeContext)
-> LLVMContext arch -> Const TypeContext (LLVMContext arch))
-> Getting TypeContext (ModuleTranslation arch) TypeContext
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(TypeContext -> Const TypeContext TypeContext)
-> LLVMContext arch -> Const TypeContext (LLVMContext arch)
forall (arch :: LLVMArch) (f :: * -> *).
Functor f =>
(TypeContext -> f TypeContext)
-> LLVMContext arch -> f (LLVMContext arch)
llvmTypeCtx)
tp :: MemType
tp = Nat -> MemType -> MemType
ArrayType Nat
0 (SymType -> MemType
PtrType (MemType -> SymType
MemType MemType
i8))
tp_sz :: Bytes
tp_sz = DataLayout -> MemType -> Bytes
memTypeSize DataLayout
dl MemType
tp
alignment :: Alignment
alignment = DataLayout -> MemType -> Alignment
memTypeAlign DataLayout
dl MemType
tp
loc :: FilePath
loc = FilePath
"crux-llvm main(argc, argv) simulation"
sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
SymGlobalState sym
gs <- Getting
(SymGlobalState sym)
(SimState
(personality sym) sym LLVM r (OverrideLang ret) ('Just args))
(SymGlobalState sym)
-> OverrideSim
(personality sym) sym LLVM r args ret (SymGlobalState sym)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use ((ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Const
(SymGlobalState sym)
(ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)))
-> SimState
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Const
(SymGlobalState sym)
(SimState
(personality sym) sym LLVM r (OverrideLang ret) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
(b :: Maybe (Ctx CrucibleType)) (f2 :: * -> *).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
-> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree((ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Const
(SymGlobalState sym)
(ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)))
-> SimState
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Const
(SymGlobalState sym)
(SimState
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym
-> Const (SymGlobalState sym) (SymGlobalState sym))
-> ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Const
(SymGlobalState sym)
(ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)))
-> Getting
(SymGlobalState sym)
(SimState
(personality sym) sym LLVM r (OverrideLang ret) ('Just args))
(SymGlobalState sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(TopFrame sym LLVM (OverrideLang ret) ('Just args)
-> Const
(SymGlobalState sym)
(TopFrame sym LLVM (OverrideLang ret) ('Just args)))
-> ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Const
(SymGlobalState sym)
(ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
(args' :: Maybe (Ctx CrucibleType)) (f2 :: * -> *).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame((TopFrame sym LLVM (OverrideLang ret) ('Just args)
-> Const
(SymGlobalState sym)
(TopFrame sym LLVM (OverrideLang ret) ('Just args)))
-> ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Const
(SymGlobalState sym)
(ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym
-> Const (SymGlobalState sym) (SymGlobalState sym))
-> TopFrame sym LLVM (OverrideLang ret) ('Just args)
-> Const
(SymGlobalState sym)
(TopFrame sym LLVM (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym
-> Const (SymGlobalState sym) (SymGlobalState sym))
-> ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Const
(SymGlobalState sym)
(ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(SymGlobalState sym
-> Const (SymGlobalState sym) (SymGlobalState sym))
-> TopFrame sym LLVM (OverrideLang ret) ('Just args)
-> Const
(SymGlobalState sym)
(TopFrame sym LLVM (OverrideLang ret) ('Just args))
forall sym u (f :: * -> *).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals)
MemImpl sym
mem <- case GlobalVar Mem -> SymGlobalState sym -> Maybe (RegValue sym Mem)
forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
lookupGlobal GlobalVar Mem
memVar SymGlobalState sym
gs of
Just RegValue sym Mem
mem -> MemImpl sym
-> OverrideSim (personality sym) sym LLVM r args ret (MemImpl sym)
forall a. a -> OverrideSim (personality sym) sym LLVM r args ret a
forall (f :: * -> *) a. Applicative f => a -> f a
pure RegValue sym Mem
MemImpl sym
mem
Maybe (RegValue sym Mem)
Nothing -> FilePath
-> OverrideSim (personality sym) sym LLVM r args ret (MemImpl sym)
forall a.
FilePath -> OverrideSim (personality sym) sym LLVM r args ret a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail FilePath
"checkFun.checkMainWithArguments: Memory missing from global vars"
LLVMPointer sym 32
argc <- IO (LLVMPointer sym 32)
-> OverrideSim
(personality sym) sym LLVM r args ret (LLVMPointer sym 32)
forall a.
IO a -> OverrideSim (personality sym) sym LLVM r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (LLVMPointer sym 32)
-> OverrideSim
(personality sym) sym LLVM r args ret (LLVMPointer sym 32))
-> IO (LLVMPointer sym 32)
-> OverrideSim
(personality sym) sym LLVM r args ret (LLVMPointer sym 32)
forall a b. (a -> b) -> a -> b
$ SymNat sym -> SymBV sym 32 -> LLVMPointer sym 32
forall sym (w :: Nat).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer (SymNat sym -> SymBV sym 32 -> LLVMPointer sym 32)
-> IO (SymNat sym) -> IO (SymBV sym 32 -> LLVMPointer sym 32)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
natLit sym
sym Nat
0 IO (SymBV sym 32 -> LLVMPointer sym 32)
-> IO (SymBV sym 32) -> IO (LLVMPointer sym 32)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> sym -> NatRepr 32 -> BV 32 -> IO (SymBV sym 32)
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr 32
w (NatRepr 32 -> BV 32
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr 32
w)
SymExpr sym (BaseBVType (ArchWidth arch))
sz <- IO (SymExpr sym (BaseBVType (ArchWidth arch)))
-> OverrideSim
(personality sym)
sym
LLVM
r
args
ret
(SymExpr sym (BaseBVType (ArchWidth arch)))
forall a.
IO a -> OverrideSim (personality sym) sym LLVM r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (BaseBVType (ArchWidth arch)))
-> OverrideSim
(personality sym)
sym
LLVM
r
args
ret
(SymExpr sym (BaseBVType (ArchWidth arch))))
-> IO (SymExpr sym (BaseBVType (ArchWidth arch)))
-> OverrideSim
(personality sym)
sym
LLVM
r
args
ret
(SymExpr sym (BaseBVType (ArchWidth arch)))
forall a b. (a -> b) -> a -> b
$ sym
-> NatRepr (ArchWidth arch)
-> BV (ArchWidth arch)
-> IO (SymExpr sym (BaseBVType (ArchWidth arch)))
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr (ArchWidth arch)
forall (w :: Nat) (w' :: Nat).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth (BV (ArchWidth arch)
-> IO (SymExpr sym (BaseBVType (ArchWidth arch))))
-> BV (ArchWidth arch)
-> IO (SymExpr sym (BaseBVType (ArchWidth arch)))
forall a b. (a -> b) -> a -> b
$ NatRepr (ArchWidth arch) -> Bytes -> BV (ArchWidth arch)
forall (w :: Nat). NatRepr w -> Bytes -> BV w
bytesToBV NatRepr (ArchWidth arch)
forall (w :: Nat) (w' :: Nat).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth Bytes
tp_sz
(LLVMPointer sym (ArchWidth arch)
argv, MemImpl sym
mem') <- IO (LLVMPointer sym (ArchWidth arch), MemImpl sym)
-> OverrideSim
(personality sym)
sym
LLVM
r
args
ret
(LLVMPointer sym (ArchWidth arch), MemImpl sym)
forall a.
IO a -> OverrideSim (personality sym) sym LLVM r args ret a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (LLVMPointer sym (ArchWidth arch), MemImpl sym)
-> OverrideSim
(personality sym)
sym
LLVM
r
args
ret
(LLVMPointer sym (ArchWidth arch), MemImpl sym))
-> IO (LLVMPointer sym (ArchWidth arch), MemImpl sym)
-> OverrideSim
(personality sym)
sym
LLVM
r
args
ret
(LLVMPointer sym (ArchWidth arch), MemImpl sym)
forall a b. (a -> b) -> a -> b
$ bak
-> MemImpl sym
-> SymExpr sym (BaseBVType (ArchWidth arch))
-> Alignment
-> FilePath
-> IO (LLVMPtr sym (ArchWidth arch), MemImpl sym)
forall sym bak (wptr :: Nat).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> SymBV sym wptr
-> Alignment
-> FilePath
-> IO (LLVMPtr sym wptr, MemImpl sym)
doAlloca bak
bak MemImpl sym
mem SymExpr sym (BaseBVType (ArchWidth arch))
sz Alignment
alignment FilePath
loc
(ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Identity
(ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)))
-> SimState
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Identity
(SimState
(personality sym) sym LLVM r (OverrideLang ret) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
(b :: Maybe (Ctx CrucibleType)) (f2 :: * -> *).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
-> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree((ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Identity
(ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)))
-> SimState
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Identity
(SimState
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
-> ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Identity
(ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Identity
(SimState
(personality sym) sym LLVM r (OverrideLang ret) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(TopFrame sym LLVM (OverrideLang ret) ('Just args)
-> Identity (TopFrame sym LLVM (OverrideLang ret) ('Just args)))
-> ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Identity
(ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
(args' :: Maybe (Ctx CrucibleType)) (f2 :: * -> *).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame((TopFrame sym LLVM (OverrideLang ret) ('Just args)
-> Identity (TopFrame sym LLVM (OverrideLang ret) ('Just args)))
-> ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Identity
(ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
-> TopFrame sym LLVM (OverrideLang ret) ('Just args)
-> Identity (TopFrame sym LLVM (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Identity
(ActiveTree
(personality sym) sym LLVM r (OverrideLang ret) ('Just args))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(SymGlobalState sym -> Identity (SymGlobalState sym))
-> TopFrame sym LLVM (OverrideLang ret) ('Just args)
-> Identity (TopFrame sym LLVM (OverrideLang ret) ('Just args))
forall sym u (f :: * -> *).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)
-> Identity
(SimState
(personality sym) sym LLVM r (OverrideLang ret) ('Just args)))
-> (SymGlobalState sym -> SymGlobalState sym)
-> OverrideSim (personality sym) sym LLVM r args ret ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= GlobalVar Mem
-> RegValue sym Mem -> SymGlobalState sym -> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
insertGlobal GlobalVar Mem
memVar RegValue sym Mem
MemImpl sym
mem'
let args :: RegMap
sym
((EmptyCtx ::> LLVMPointerType 32)
::> LLVMPointerType (ArchWidth arch))
args = TypeRepr (LLVMPointerType (ArchWidth arch))
-> LLVMPtr sym (ArchWidth arch)
-> RegMap sym (EmptyCtx ::> LLVMPointerType 32)
-> RegMap
sym
((EmptyCtx ::> LLVMPointerType 32)
::> LLVMPointerType (ArchWidth arch))
forall (tp :: CrucibleType) sym (ctx :: Ctx CrucibleType).
TypeRepr tp
-> RegValue sym tp -> RegMap sym ctx -> RegMap sym (ctx ::> tp)
assignReg TypeRepr (LLVMPointerType (ArchWidth arch))
forall (wptr :: Nat) (ty :: CrucibleType).
(HasPtrWidth wptr, ty ~ LLVMPointerType wptr) =>
TypeRepr ty
PtrRepr LLVMPtr sym (ArchWidth arch)
LLVMPointer sym (ArchWidth arch)
argv (RegMap sym (EmptyCtx ::> LLVMPointerType 32)
-> RegMap
sym
((EmptyCtx ::> LLVMPointerType 32)
::> LLVMPointerType (ArchWidth arch)))
-> RegMap sym (EmptyCtx ::> LLVMPointerType 32)
-> RegMap
sym
((EmptyCtx ::> LLVMPointerType 32)
::> LLVMPointerType (ArchWidth arch))
forall a b. (a -> b) -> a -> b
$
TypeRepr (LLVMPointerType 32)
-> RegValue sym (LLVMPointerType 32)
-> RegMap sym EmptyCtx
-> RegMap sym (EmptyCtx ::> LLVMPointerType 32)
forall (tp :: CrucibleType) sym (ctx :: Ctx CrucibleType).
TypeRepr tp
-> RegValue sym tp -> RegMap sym ctx -> RegMap sym (ctx ::> tp)
assignReg (NatRepr 32 -> TypeRepr (LLVMPointerType 32)
forall (ty :: CrucibleType) (w :: Nat).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr 32
w) RegValue sym (LLVMPointerType 32)
LLVMPointer sym 32
argc RegMap sym EmptyCtx
forall sym. RegMap sym EmptyCtx
emptyRegMap
CFG
LLVM
blocks
((EmptyCtx ::> LLVMPointerType 32)
::> LLVMPointerType (ArchWidth arch))
ret
-> RegMap
sym
((EmptyCtx ::> LLVMPointerType 32)
::> LLVMPointerType (ArchWidth arch))
-> OverM personality sym LLVM ()
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
(ret :: CrucibleType).
CFG LLVM blocks ctx ret
-> RegMap sym ctx -> OverM personality sym LLVM ()
simulateFun CFG
LLVM
blocks
((EmptyCtx ::> LLVMPointerType 32)
::> LLVMPointerType (ArchWidth arch))
ret
anyCfg RegMap
sym
((EmptyCtx ::> LLVMPointerType 32)
::> LLVMPointerType (ArchWidth arch))
args
memMetrics :: forall p sym ext
. GlobalVar Mem
-> Map.Map Text (Metric p sym ext)
memMetrics :: forall p sym ext. GlobalVar Mem -> Map Text (Metric p sym ext)
memMetrics GlobalVar Mem
memVar = [(Text, Metric p sym ext)] -> Map Text (Metric p sym ext)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
[ (Text
"LLVM.allocs", Metric p sym ext
allocs)
, (Text
"LLVM.writes", Metric p sym ext
writes)
]
where
allocs :: Metric p sym ext
allocs = (forall rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> IO Integer)
-> Metric p sym ext
forall p sym ext.
(forall rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> IO Integer)
-> Metric p sym ext
Metric ((forall rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> IO Integer)
-> Metric p sym ext)
-> (forall rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> IO Integer)
-> Metric p sym ext
forall a b. (a -> b) -> a -> b
$ (MemImpl sym -> Int) -> SimState p sym ext rtp f args -> IO Integer
forall r f (args :: Maybe (Ctx CrucibleType)).
(MemImpl sym -> Int) -> SimState p sym ext r f args -> IO Integer
measureMemBy MemImpl sym -> Int
forall sym. MemImpl sym -> Int
memAllocCount
writes :: Metric p sym ext
writes = (forall rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> IO Integer)
-> Metric p sym ext
forall p sym ext.
(forall rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> IO Integer)
-> Metric p sym ext
Metric ((forall rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> IO Integer)
-> Metric p sym ext)
-> (forall rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> IO Integer)
-> Metric p sym ext
forall a b. (a -> b) -> a -> b
$ (MemImpl sym -> Int) -> SimState p sym ext rtp f args -> IO Integer
forall r f (args :: Maybe (Ctx CrucibleType)).
(MemImpl sym -> Int) -> SimState p sym ext r f args -> IO Integer
measureMemBy MemImpl sym -> Int
forall sym. MemImpl sym -> Int
memWriteCount
measureMemBy :: (MemImpl sym -> Int)
-> SimState p sym ext r f args
-> IO Integer
measureMemBy :: forall r f (args :: Maybe (Ctx CrucibleType)).
(MemImpl sym -> Int) -> SimState p sym ext r f args -> IO Integer
measureMemBy MemImpl sym -> Int
f SimState p sym ext r f args
st = do
let globals :: SymGlobalState sym
globals = SimState p sym ext r f args
st SimState p sym ext r f args
-> Getting
(SymGlobalState sym)
(SimState p sym ext r f args)
(SymGlobalState sym)
-> SymGlobalState sym
forall s a. s -> Getting a s a -> a
^. Getting
(SymGlobalState sym)
(SimState p sym ext r f args)
(SymGlobalState sym)
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
(f2 :: * -> *).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
stateGlobals
case GlobalVar Mem -> SymGlobalState sym -> Maybe (RegValue sym Mem)
forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
lookupGlobal GlobalVar Mem
memVar SymGlobalState sym
globals of
Just RegValue sym Mem
mem -> Integer -> IO Integer
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> IO Integer) -> Integer -> IO Integer
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a. Integral a => a -> Integer
toInteger (MemImpl sym -> Int
f RegValue sym Mem
MemImpl sym
mem)
Maybe (RegValue sym Mem)
Nothing -> FilePath -> IO Integer
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail FilePath
"Memory missing from global vars"
detailLimit :: Int
detailLimit :: Int
detailLimit = Int
10
explainFailure :: IsSymInterface sym
=> sym ~ WEB.ExprBuilder t st fs
=> sym
-> IORef (LLVMAnnMap sym)
-> Crux.Explainer sym t ann
explainFailure :: forall sym t (st :: * -> *) fs ann.
(IsSymInterface sym, sym ~ ExprBuilder t st fs) =>
sym -> IORef (LLVMAnnMap sym) -> Explainer sym t ann
explainFailure sym
sym IORef (LLVMAnnMap sym)
bbMapRef Maybe (GroundEvalFn t)
evalFn LPred sym SimError
gl =
do LLVMAnnMap sym
bb <- IORef (LLVMAnnMap sym) -> IO (LLVMAnnMap sym)
forall a. IORef a -> IO a
readIORef IORef (LLVMAnnMap sym)
bbMapRef
CexExplanation (ExprBuilder t st fs) BaseBoolType
ex <- sym
-> LLVMAnnMap sym
-> Maybe (GroundEvalFn t)
-> IO (Pred sym -> IO (CexExplanation sym BaseBoolType))
forall t (st :: * -> *) fs sym.
(IsSymInterface sym, sym ~ ExprBuilder t st fs) =>
sym
-> LLVMAnnMap sym
-> Maybe (GroundEvalFn t)
-> IO (Pred sym -> IO (CexExplanation sym BaseBoolType))
explainCex sym
sym LLVMAnnMap sym
bb Maybe (GroundEvalFn t)
evalFn IO
(Expr t BaseBoolType
-> IO (CexExplanation (ExprBuilder t st fs) BaseBoolType))
-> ((Expr t BaseBoolType
-> IO (CexExplanation (ExprBuilder t st fs) BaseBoolType))
-> IO (CexExplanation (ExprBuilder t st fs) BaseBoolType))
-> IO (CexExplanation (ExprBuilder t st fs) BaseBoolType)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Expr t BaseBoolType
-> IO (CexExplanation (ExprBuilder t st fs) BaseBoolType)
f -> Expr t BaseBoolType
-> IO (CexExplanation (ExprBuilder t st fs) BaseBoolType)
f (LPred sym SimError
LabeledPred (Expr t BaseBoolType) SimError
gl LabeledPred (Expr t BaseBoolType) SimError
-> Getting
(Expr t BaseBoolType)
(LabeledPred (Expr t BaseBoolType) SimError)
(Expr t BaseBoolType)
-> Expr t BaseBoolType
forall s a. s -> Getting a s a -> a
^. Getting
(Expr t BaseBoolType)
(LabeledPred (Expr t BaseBoolType) SimError)
(Expr t BaseBoolType)
forall pred msg pred' (f :: * -> *).
Functor f =>
(pred -> f pred')
-> LabeledPred pred msg -> f (LabeledPred pred' msg)
labeledPred)
let details :: Doc ann
details =
case CexExplanation (ExprBuilder t st fs) BaseBoolType
ex of
CexExplanation (ExprBuilder t st fs) BaseBoolType
NoExplanation -> Doc ann
forall a. Monoid a => a
mempty
DisjOfFailures [(CallStack, BadBehavior (ExprBuilder t st fs))]
xs ->
case (CallStack, BadBehavior (ExprBuilder t st fs)) -> Doc ann
forall {sym} {ann}.
IsExpr (SymExpr sym) =>
(CallStack, BadBehavior sym) -> Doc ann
ppBBPair ((CallStack, BadBehavior (ExprBuilder t st fs)) -> Doc ann)
-> [(CallStack, BadBehavior (ExprBuilder t st fs))] -> [Doc ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(CallStack, BadBehavior (ExprBuilder t st fs))]
xs of
[] -> Doc ann
forall a. Monoid a => a
mempty
[Doc ann
x] -> Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 Doc ann
x
[Doc ann]
xs' ->
let xs'' :: [Doc ann]
xs'' = Int -> [Doc ann] -> [Doc ann]
forall a. Int -> [a] -> [a]
List.take Int
detailLimit [Doc ann]
xs'
xs'l :: Int
xs'l = [Doc ann] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Doc ann]
xs'
msg1 :: Doc ann
msg1 = Doc ann
"Failing conditions::"
msg2 :: Doc ann
msg2 = if Int
xs'l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
detailLimit
then Doc ann
"[only displaying the first"
Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Int
detailLimit
Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"of" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Int
xs'l
Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"failed conditions]"
else Doc ann
"Total failed conditions:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Int
xs'l
in Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
nest Int
2 (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann
msg1 Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: [Doc ann]
xs'' [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. Semigroup a => a -> a -> a
<> [Doc ann
msg2]
Doc ann -> IO (Doc ann)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc ann -> IO (Doc ann)) -> Doc ann -> IO (Doc ann)
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [ SimError -> Doc ann
forall ann. SimError -> Doc ann
ppSimError (LPred sym SimError
LabeledPred (Expr t BaseBoolType) SimError
glLabeledPred (Expr t BaseBoolType) SimError
-> Getting
SimError (LabeledPred (Expr t BaseBoolType) SimError) SimError
-> SimError
forall s a. s -> Getting a s a -> a
^. Getting
SimError (LabeledPred (Expr t BaseBoolType) SimError) SimError
forall pred msg msg' (f :: * -> *).
Functor f =>
(msg -> f msg')
-> LabeledPred pred msg -> f (LabeledPred pred msg')
labeledPredMsg), Doc ann
details ]
where ppBBPair :: (CallStack, BadBehavior sym) -> Doc ann
ppBBPair (CallStack
callStack, BadBehavior sym
bb) =
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep [ BadBehavior sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
ppBB BadBehavior sym
bb
, Doc ann
"in context:"
, Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (CallStack -> Doc ann
forall ann. CallStack -> Doc ann
ppCallStack CallStack
callStack)
]