{-# 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

-- what4
import qualified What4.Expr.Builder as WEB
import What4.Interface (bvLit, natLit)

-- crucible
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) )


-- crucible-llvm
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

-- crux
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

-- | Create a simulator context for the given architecture.
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)

-- | Parse an LLVM bit-code file.
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

     -- register the callable override functions
     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

     -- register all the functions defined in the LLVM module
     (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 =>
  -- | Path to the LLVM module
  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)
       -- We modify the defaults, which are extremely conservative.  Unless the
       -- user directs otherwise, we default to connecting stdin, stdout, and stderr.
       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
                                   }

-- | Given an LLVM Bitcode file, and a GlobalVar memory, translate the
-- file into the Crucible representation and add the globals and
-- definitions from the file to the GlobalVar memory.

prepLLVMModule :: IsSymBackend sym bak
               => HasLLVMAnn sym
               => Crux.Logs msgs
               => Log.SupportsCruxLLVMLogMessage msgs
               => LLVMOptions
               -> HandleAllocator
               -> bak
               -> FilePath  -- for the LLVM bitcode file
               -> 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)  -- TODO(lb): Suggest uc-crux-llvm?

    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 ()

    -- Simulate a function with the signature @int main(int argc, char* argv[])@.
    -- We do so by behaving as if we are starting from this entrypoint:
    --
    --   int crucible_main() {
    --     int argc = 0;
    --     char *argv[] = {};
    --     return main(argc, argv);
    --   }
    --
    -- @argc@ can easily be created with 'bvLit'. For @argv@, we have to choose
    -- what sort of allocation we want when creating its @LLVMPointer@. We've
    -- opted for 'doAlloca' since the LLVM bitcode to allocate @argv@ will use
    -- the @alloca@ instruction. This means that @argv@ will be
    -- stack-allocated, which is a reasonable choice, given that the @main@
    -- function's @argv@ argument actually lives on the stack in most binaries.
    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

---------------------------------------------------------------------
-- Profiling

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
                    -- Note: These map keys are used by profile.js in
                    -- https://github.com/GaloisInc/sympro-ui and must
                    -- match the names there.
                    [ (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"

----------------------------------------------------------------------

-- arbitrary, we should probably make this limit configurable
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)
               ]