content: {-# LANGUAGE GADTs #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  module Lang.Crucible.LLVM.Eval
    ( llvmExtensionEval
    , callStackFromMemVar
    ) where
  
  import           Control.Lens ((^.), view)
  import           Control.Monad (forM_)
  import qualified Data.List.NonEmpty as NE
  import           Data.Parameterized.TraversableF
  
  import           What4.Interface
  
  import           Lang.Crucible.Backend
  import           Lang.Crucible.CFG.Common (GlobalVar)
  import           Lang.Crucible.Simulator.ExecutionTree (SimState, CrucibleState)
  import           Lang.Crucible.Simulator.ExecutionTree (stateGlobals)
  import           Lang.Crucible.Simulator.GlobalState (lookupGlobal)
  import           Lang.Crucible.Simulator.Intrinsics
  import           Lang.Crucible.Simulator.Evaluation
  import           Lang.Crucible.Simulator.RegValue
  import           Lang.Crucible.Simulator.SimError
  import           Lang.Crucible.Panic (panic)
  
  import qualified Lang.Crucible.LLVM.Arch.X86 as X86
  import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB
  import           Lang.Crucible.LLVM.Extension
  import           Lang.Crucible.LLVM.MemModel (memImplHeap)
  import           Lang.Crucible.LLVM.MemModel.CallStack (CallStack, getCallStack)
  import           Lang.Crucible.LLVM.MemModel.MemLog (memState)
  import           Lang.Crucible.LLVM.MemModel.Partial
  import           Lang.Crucible.LLVM.MemModel.Pointer
  import           Lang.Crucible.LLVM.Types (Mem)
  
  callStackFromMemVar ::
    SimState p sym ext rtp lang args ->
    GlobalVar Mem ->
    CallStack
  callStackFromMemVar state mvar =
    getCallStack . view memState . memImplHeap $
       case lookupGlobal mvar (state ^. stateGlobals) of
         Just v -> v
         Nothing ->
           panic "callStackFromMemVar"
             [ "Global heap value not initialized."
             , "*** Global heap variable: " ++ show mvar
             ]
  
  assertSideCondition ::
    (HasLLVMAnn sym, IsSymBackend sym bak) =>
    bak ->
    CallStack ->
    LLVMSideCondition (RegValue' sym) ->
    IO ()
  assertSideCondition bak callStack (LLVMSideCondition (RV p) ub) =
    do let sym = backendGetSym bak
       p' <- annotateUB sym callStack ub p
       let err = AssertFailureSimError "Undefined behavior encountered" (show (UB.explain ub))
       assert bak p' err
  
  llvmExtensionEval ::
    forall sym bak p ext rtp blocks r ctx.
    (HasLLVMAnn sym, IsSymBackend sym bak) =>
    bak ->
    IntrinsicTypes sym ->
    (Int -> String -> IO ()) ->
    CrucibleState p sym ext rtp blocks r ctx ->
    EvalAppFunc sym LLVMExtensionExpr
  
  llvmExtensionEval bak _iTypes _logFn state eval e =
    let sym = backendGetSym bak in
    case e of
      X86Expr ex -> X86.eval sym eval ex
  
      LLVM_SideConditions mvar _tp conds val ->
        do let callStack = callStackFromMemVar state mvar
           conds' <- traverse (traverseF (\x -> RV @sym <$> eval x)) (NE.toList conds)
           forM_ conds' (assertSideCondition bak callStack)
           eval val
  
      LLVM_PointerExpr _w blk off ->
        do blk' <- eval blk
           off' <- eval off
           return (LLVMPointer blk' off')
  
      LLVM_PointerBlock _w ptr ->
        llvmPointerBlock <$> eval ptr
  
      LLVM_PointerOffset _w ptr ->
        llvmPointerOffset <$> eval ptr
  
      LLVM_PointerIte _w c x y ->
        do cond <- eval c
           LLVMPointer xblk xoff <- eval x
           LLVMPointer yblk yoff <- eval y
           blk <- natIte sym cond xblk yblk
           off <- bvIte sym cond xoff yoff
           return (LLVMPointer blk off)
  