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