Crux.LLVM.Simulate

Documentation

setupSimCtxt :: (IsSymBackend sym bak, HasLLVMAnn sym) => HandleAllocator -> bak -> MemOptions -> GlobalVar Mem -> SimCtxt Crux sym LLVM

Create a simulator context for the given architecture.

parseLLVM :: FilePath -> IO Module

Parse an LLVM bit-code file.

registerFunctions :: Logs msgs => SupportsCruxLLVMLogMessage msgs => (ArchOk arch, IsSymInterface sym, HasLLVMAnn sym, ptrW ~ ArchWidth arch) => LLVMOptions -> Module -> ModuleTranslation arch -> Maybe (LLVMFileSystem ptrW) -> OverM Crux sym LLVM ()

simulateLLVMFile

Arguments

:: Logs msgs

=> SupportsCruxLLVMLogMessage msgs

=> FilePath

Path to the LLVM module

-> LLVMOptions

-> SimulatorCallbacks msgs CruxSimulationResult

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)

data PreppedLLVM sym

Constructors

PreppedLLVM

Fields

• prepLLVMMod :: Module
• prepSomeTrans :: Some ModuleTranslation
• prepMemVar :: GlobalVar Mem
• prepMem :: MemImpl sym

prepLLVMModule :: IsSymBackend sym bak => HasLLVMAnn sym => Logs msgs => SupportsCruxLLVMLogMessage msgs => LLVMOptions -> HandleAllocator -> bak -> FilePath -> GlobalVar Mem -> IO (PreppedLLVM 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.

sayTranslationWarning :: SupportsCruxLLVMLogMessage msgs => Logs msgs => LLVMTranslationWarning -> IO ()

checkFun :: forall arch msgs personality sym. IsSymInterface sym => HasLLVMAnn sym => ArchOk arch => Logs msgs => SupportsCruxLLVMLogMessage msgs => LLVMOptions -> ModuleTranslation arch -> GlobalVar Mem -> OverM personality sym LLVM ()

memMetrics :: forall p sym ext. GlobalVar Mem -> Map Text (Metric p sym ext)

detailLimit :: Int

explainFailure :: IsSymInterface sym => sym ~ ExprBuilder t st fs => sym -> IORef (LLVMAnnMap sym) -> Explainer sym t ann