{-# 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 :: forall p sym ext rtp lang (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp lang args -> GlobalVar Mem -> CallStack
callStackFromMemVar SimState p sym ext rtp lang args
state GlobalVar Mem
mvar =
  MemState sym -> CallStack
forall sym. MemState sym -> CallStack
getCallStack (MemState sym -> CallStack)
-> (MemImpl sym -> MemState sym) -> MemImpl sym -> CallStack
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (MemState sym) (Mem sym) (MemState sym)
-> Mem sym -> MemState sym
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting (MemState sym) (Mem sym) (MemState sym)
forall sym (f :: Type -> Type).
Functor f =>
(MemState sym -> f (MemState sym)) -> Mem sym -> f (Mem sym)
memState (Mem sym -> MemState sym)
-> (MemImpl sym -> Mem sym) -> MemImpl sym -> MemState sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MemImpl sym -> Mem sym
forall sym. MemImpl sym -> Mem sym
memImplHeap (MemImpl sym -> CallStack) -> MemImpl sym -> CallStack
forall a b. (a -> b) -> a -> b
$
     case GlobalVar Mem -> SymGlobalState sym -> Maybe (RegValue sym Mem)
forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
lookupGlobal GlobalVar Mem
mvar (SimState p sym ext rtp lang args
state SimState p sym ext rtp lang args
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext rtp lang args)
     (SymGlobalState sym)
-> SymGlobalState sym
forall s a. s -> Getting a s a -> a
^. Getting
  (SymGlobalState sym)
  (SimState p sym ext rtp lang args)
  (SymGlobalState sym)
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
stateGlobals) of
       Just RegValue sym Mem
v -> RegValue sym Mem
MemImpl sym
v
       Maybe (RegValue sym Mem)
Nothing ->
         String -> [String] -> MemImpl sym
forall a. HasCallStack => String -> [String] -> a
panic String
"callStackFromMemVar"
           [ String
"Global heap value not initialized."
           , String
"*** Global heap variable: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ GlobalVar Mem -> String
forall a. Show a => a -> String
show GlobalVar Mem
mvar
           ]

assertSideCondition ::
  (HasLLVMAnn sym, IsSymBackend sym bak) =>
  bak ->
  CallStack ->
  LLVMSideCondition (RegValue' sym) ->
  IO ()
assertSideCondition :: forall sym bak.
(HasLLVMAnn sym, IsSymBackend sym bak) =>
bak -> CallStack -> LLVMSideCondition (RegValue' sym) -> IO ()
assertSideCondition bak
bak CallStack
callStack (LLVMSideCondition (RV RegValue sym BoolType
p) UndefinedBehavior (RegValue' sym)
ub) =
  do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
     SymExpr sym BaseBoolType
p' <- sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
(IsSymInterface sym, HasLLVMAnn sym) =>
sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
annotateUB sym
sym CallStack
callStack UndefinedBehavior (RegValue' sym)
ub RegValue sym BoolType
SymExpr sym BaseBoolType
p
     let err :: SimErrorReason
err = String -> String -> SimErrorReason
AssertFailureSimError String
"Undefined behavior encountered" (Doc Any -> String
forall a. Show a => a -> String
show (UndefinedBehavior (RegValue' sym) -> Doc Any
forall (e :: CrucibleType -> Type) ann.
UndefinedBehavior e -> Doc ann
UB.explain UndefinedBehavior (RegValue' sym)
ub))
     bak -> SymExpr sym BaseBoolType -> SimErrorReason -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Pred sym -> SimErrorReason -> IO ()
assert bak
bak SymExpr sym BaseBoolType
p' SimErrorReason
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 :: forall sym bak p ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (ctx :: Ctx CrucibleType).
(HasLLVMAnn sym, IsSymBackend sym bak) =>
bak
-> IntrinsicTypes sym
-> (Int -> String -> IO ())
-> CrucibleState p sym ext rtp blocks r ctx
-> EvalAppFunc sym LLVMExtensionExpr
llvmExtensionEval bak
bak IntrinsicTypes sym
_iTypes Int -> String -> IO ()
_logFn CrucibleState p sym ext rtp blocks r ctx
state forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
eval LLVMExtensionExpr f tp
e =
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak in
  case LLVMExtensionExpr f tp
e of
    X86Expr ExtX86 f tp
ex -> sym
-> (forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp))
-> ExtX86 f tp
-> IO (RegValue sym tp)
forall sym (f :: CrucibleType -> Type) (tp :: CrucibleType).
IsSymExprBuilder sym =>
sym
-> (forall (subT :: CrucibleType).
    f subT -> IO (RegValue sym subT))
-> ExtX86 f tp
-> IO (RegValue sym tp)
X86.eval sym
sym f subT -> IO (RegValue sym subT)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
eval ExtX86 f tp
ex

    LLVM_SideConditions GlobalVar Mem
mvar TypeRepr tp
_tp NonEmpty (LLVMSideCondition f)
conds f tp
val ->
      do let callStack :: CallStack
callStack = CrucibleState p sym ext rtp blocks r ctx
-> GlobalVar Mem -> CallStack
forall p sym ext rtp lang (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp lang args -> GlobalVar Mem -> CallStack
callStackFromMemVar CrucibleState p sym ext rtp blocks r ctx
state GlobalVar Mem
mvar
         [LLVMSideCondition (RegValue' sym)]
conds' <- (LLVMSideCondition f -> IO (LLVMSideCondition (RegValue' sym)))
-> [LLVMSideCondition f] -> IO [LLVMSideCondition (RegValue' sym)]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((forall (s :: CrucibleType). f s -> IO (RegValue' sym s))
-> LLVMSideCondition f -> IO (LLVMSideCondition (RegValue' sym))
forall {k} (t :: (k -> Type) -> Type) (m :: Type -> Type)
       (e :: k -> Type) (f :: k -> Type).
(TraversableF t, Applicative m) =>
(forall (s :: k). e s -> m (f s)) -> t e -> m (t f)
forall (m :: Type -> Type) (e :: CrucibleType -> Type)
       (f :: CrucibleType -> Type).
Applicative m =>
(forall (s :: CrucibleType). e s -> m (f s))
-> LLVMSideCondition e -> m (LLVMSideCondition f)
traverseF (\f s
x -> forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV @sym (RegValue sym s -> RegValue' sym s)
-> IO (RegValue sym s) -> IO (RegValue' sym s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f s -> IO (RegValue sym s)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
eval f s
x)) (NonEmpty (LLVMSideCondition f) -> [LLVMSideCondition f]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (LLVMSideCondition f)
conds)
         [LLVMSideCondition (RegValue' sym)]
-> (LLVMSideCondition (RegValue' sym) -> IO ()) -> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [LLVMSideCondition (RegValue' sym)]
conds' (bak -> CallStack -> LLVMSideCondition (RegValue' sym) -> IO ()
forall sym bak.
(HasLLVMAnn sym, IsSymBackend sym bak) =>
bak -> CallStack -> LLVMSideCondition (RegValue' sym) -> IO ()
assertSideCondition bak
bak CallStack
callStack)
         f tp -> IO (RegValue sym tp)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
eval f tp
val

    LLVM_PointerExpr NatRepr w
_w f NatType
blk f (BVType w)
off ->
      do SymNat sym
blk' <- f NatType -> IO (RegValue sym NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
eval f NatType
blk
         SymExpr sym ('BaseBVType w)
off' <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
eval f (BVType w)
off
         LLVMPointer sym w -> IO (LLVMPointer sym w)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymNat sym -> SymExpr sym ('BaseBVType w) -> LLVMPointer sym w
forall sym (w :: Natural).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
blk' SymExpr sym ('BaseBVType w)
off')

    LLVM_PointerBlock NatRepr w
_w f (LLVMPointerType w)
ptr ->
      LLVMPtr sym w -> SymNat sym
LLVMPointer sym w -> SymNat sym
forall sym (w :: Natural). LLVMPtr sym w -> SymNat sym
llvmPointerBlock (LLVMPointer sym w -> SymNat sym)
-> IO (LLVMPointer sym w) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f (LLVMPointerType w) -> IO (LLVMPtr sym w)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
eval f (LLVMPointerType w)
ptr

    LLVM_PointerOffset NatRepr w
_w f (LLVMPointerType w)
ptr ->
      LLVMPtr sym w -> SymBV sym w
LLVMPointer sym w -> SymBV sym w
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
llvmPointerOffset (LLVMPointer sym w -> SymBV sym w)
-> IO (LLVMPointer sym w) -> IO (SymBV sym w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f (LLVMPointerType w) -> IO (LLVMPtr sym w)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
eval f (LLVMPointerType w)
ptr

    LLVM_PointerIte NatRepr w
_w f BoolType
c f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w))
x f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w))
y ->
      do SymExpr sym BaseBoolType
cond <- f BoolType -> IO (RegValue sym BoolType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
eval f BoolType
c
         LLVMPointer SymNat sym
xblk SymBV sym w
xoff <- f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w))
-> IO
     (RegValue
        sym ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
eval f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w))
x
         LLVMPointer SymNat sym
yblk SymBV sym w
yoff <- f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w))
-> IO
     (RegValue
        sym ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
eval f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w))
y
         SymNat sym
blk <- sym
-> SymExpr sym BaseBoolType
-> SymNat sym
-> SymNat sym
-> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natIte sym
sym SymExpr sym BaseBoolType
cond SymNat sym
xblk SymNat sym
yblk
         SymBV sym w
off <- sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall (w :: Natural).
(1 <= w) =>
sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
cond SymBV sym w
xoff SymBV sym w
yoff
         LLVMPointer sym w -> IO (LLVMPointer sym w)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymNat sym -> SymBV sym w -> LLVMPointer sym w
forall sym (w :: Natural).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
blk SymBV sym w
off)