{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.Simulator.PositionTracking
( positionTrackingFeature
) where
import Control.Lens ((^.), to)
import Control.Monad.IO.Class
import Lang.Crucible.Backend
import Lang.Crucible.Simulator.CallFrame
import Lang.Crucible.Simulator.EvalStmt
import Lang.Crucible.Simulator.ExecutionTree
positionTrackingFeature ::
IsSymInterface sym =>
sym ->
IO (GenericExecutionFeature sym)
positionTrackingFeature :: forall sym.
IsSymInterface sym =>
sym -> IO (GenericExecutionFeature sym)
positionTrackingFeature sym
_sym = GenericExecutionFeature sym -> IO (GenericExecutionFeature sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GenericExecutionFeature sym -> IO (GenericExecutionFeature sym))
-> GenericExecutionFeature sym -> IO (GenericExecutionFeature sym)
forall a b. (a -> b) -> a -> b
$ (forall p ext rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp))
-> GenericExecutionFeature sym
forall sym.
(forall p ext rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp))
-> GenericExecutionFeature sym
GenericExecutionFeature ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall p ext rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall p sym ext rtp.
ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
onStep
where
onStep ::
ExecState p sym ext rtp ->
IO (ExecutionFeatureResult p sym ext rtp)
onStep :: forall p sym ext rtp.
ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
onStep exst :: ExecState p sym ext rtp
exst@(RunningState (RunBlockStart BlockID blocks args
_bid) SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st) =
do let loc :: ProgramLoc
loc = SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
ProgramLoc
(SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
ProgramLoc
-> ProgramLoc
forall s a. s -> Getting a s a -> a
^. ((CallFrame sym ext blocks r args
-> Const ProgramLoc (CallFrame sym ext blocks r args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Const
ProgramLoc
(SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
(r :: CrucibleType) (a :: Ctx CrucibleType)
(a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame((CallFrame sym ext blocks r args
-> Const ProgramLoc (CallFrame sym ext blocks r args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Const
ProgramLoc
(SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> ((ProgramLoc -> Const ProgramLoc ProgramLoc)
-> CallFrame sym ext blocks r args
-> Const ProgramLoc (CallFrame sym ext blocks r args))
-> Getting
ProgramLoc
(SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
ProgramLoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(CallFrame sym ext blocks r args -> ProgramLoc)
-> (ProgramLoc -> Const ProgramLoc ProgramLoc)
-> CallFrame sym ext blocks r args
-> Const ProgramLoc (CallFrame sym ext blocks r args)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to CallFrame sym ext blocks r args -> ProgramLoc
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> ProgramLoc
frameProgramLoc)
let simCtx :: SimContext p sym ext
simCtx = SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
(SimContext p sym ext)
(SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
(SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^. Getting
(SimContext p sym ext)
(SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
(SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
(f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext
IO () -> IO ()
forall a. IO a -> IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ SimContext p sym ext
-> (forall {bak}. IsSymBackend sym bak => bak -> IO ()) -> IO ()
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend SimContext p sym ext
simCtx ((forall {bak}. IsSymBackend sym bak => bak -> IO ()) -> IO ())
-> (forall {bak}. IsSymBackend sym bak => bak -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
bak -> Assumptions sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumptions sym -> IO ()
addAssumptions bak
bak (CrucibleEvent (SymExpr sym) -> Assumptions sym
forall (e :: BaseType -> Type).
CrucibleEvent e -> CrucibleAssumptions e
singleEvent (ProgramLoc -> CrucibleEvent (SymExpr sym)
forall (e :: BaseType -> Type). ProgramLoc -> CrucibleEvent e
LocationReachedEvent ProgramLoc
loc))
ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
ExecutionFeatureModifiedState ExecState p sym ext rtp
exst)
onStep ExecState p sym ext rtp
_ = ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
ExecutionFeatureNoChange