-----------------------------------------------------------------------
-- |
-- 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.Monad.IO.Class
import Lens.Micro ((^.), to)

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 :: 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)
-> SimpleGetter (CallFrame sym ext blocks r args) ProgramLoc
forall s a. (s -> a) -> SimpleGetter 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)
        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
$ SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> (forall {bak}. IsSymBackend sym bak => bak -> IO ()) -> IO ()
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)) a.
SimState p sym ext rtp f args
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withStateBackend SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st ((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