content: -----------------------------------------------------------------------
  -- |
  -- Module           : Lang.Crucible.Simulator.PositionTracking
  -- Description      : Execution feature for tracking program positions
  -- Copyright        : (c) Galois, Inc 2021
  -- License          : BSD3
  -- Maintainer       : Rob Dockins <rdockins@galois.com>
  -- Stability        : provisional
  ------------------------------------------------------------------------
  {-# 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
  
  
  -- | This execution feature adds a @LocationReachedEvent@ to
  --   the backend assumption tracking whenever execution reaches the
  --   head of a basic block.
  positionTrackingFeature ::
    IsSymInterface sym =>
    sym ->
    IO (GenericExecutionFeature sym)
  positionTrackingFeature _sym = return $ GenericExecutionFeature onStep
   where
     onStep ::
       ExecState p sym ext rtp ->
       IO (ExecutionFeatureResult p sym ext rtp)
     onStep exst@(RunningState (RunBlockStart _bid) st) =
       do let loc = st ^. (stateCrucibleFrame.to frameProgramLoc)
          let simCtx = st ^. stateContext
          liftIO $ withBackend simCtx $ \bak ->
            addAssumptions bak (singleEvent (LocationReachedEvent loc))
          return (ExecutionFeatureModifiedState exst)
  
     onStep _ = return ExecutionFeatureNoChange
  