-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Simulator.ExecutionTree
-- Description      : Data structure the execution state of the simulator
-- Copyright        : (c) Galois, Inc 2014-2018
-- License          : BSD3
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
--
-- Execution trees record the state of the simulator as it explores
-- execution paths through a program.  This module defines the
-- collection of datatypes that record the state of a running simulator
-- and basic lenses and accessors for these types. See
-- "Lang.Crucible.Simulator.Operations" for the definitions of operations
-- that manipulate these datastructures to drive them through the simulator
-- state machine.
------------------------------------------------------------------------
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fprint-explicit-kinds -Wall #-}
module Lang.Crucible.Simulator.ExecutionTree
  ( -- * GlobalPair
    GlobalPair(..)
  , gpValue
  , gpGlobals

    -- * TopFrame
  , TopFrame
  , crucibleTopFrame
  , overrideTopFrame

    -- * CrucibleBranchTarget
  , CrucibleBranchTarget(..)
  , ppBranchTarget

    -- * AbortedResult
  , AbortedResult(..)
  , SomeFrame(..)
  , filterCrucibleFrames
  , arFrames
  , ppExceptionContext

    -- * Partial result
  , PartialResult(..)
  , PartialResultFrame
  , partialValue

    -- * Execution states
  , ExecResult(..)
  , ExecState(..)
  , ExecCont
  , RunningStateInfo(..)
  , ResolvedCall(..)
  , resolvedCallHandle
  , execResultContext
  , execStateContext
  , execStateSimState

    -- * Simulator context trees
    -- ** Main context data structures
  , ValueFromValue(..)
  , ValueFromFrame(..)
  , PendingPartialMerges(..)

    -- ** Paused Frames
  , ResolvedJump(..)
  , ControlResumption(..)
  , PausedFrame(..)

    -- ** Sibling paths
  , VFFOtherPath(..)
  , FrameRetType

    -- ** ReturnHandler
  , ReturnHandler(..)

    -- * ActiveTree
  , ActiveTree(..)
  , singletonTree
  , activeFrames
  , actContext
  , actFrame

    -- * Simulator context
    -- ** Function bindings
  , Override(..)
  , FnState(..)
  , FunctionBindings(..)

    -- ** Extensions
  , ExtensionImpl(..)
  , EvalStmtFunc
  , emptyExtensionImpl

    -- ** SimContext record
  , IsSymInterfaceProof
  , SimContext(..)
  , Metric(..)
  , initSimContext
  , withBackend
  , ctxSymInterface
  , functionBindings
  , cruciblePersonality
  , profilingMetrics

    -- * SimState
  , SimState(..)
  , SomeSimState(..)
  , initSimState
  , stateLocation

  , AbortHandler(..)
  , CrucibleState

    -- ** Lenses and accessors
  , stateTree
  , abortHandler
  , stateContext
  , stateCrucibleFrame
  , stateSymInterface
  , stateSolverProof
  , stateIntrinsicTypes
  , stateOverrideFrame
  , stateGlobals
  , stateConfiguration
  ) where

import           Control.Lens
import           Control.Monad.Reader
import           Data.Kind
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Parameterized.Ctx
import qualified Data.Parameterized.Context as Ctx
import           Data.Text (Text)
import           System.Exit (ExitCode)
import           System.IO
import qualified Prettyprinter as PP

import           What4.Config (Config)
import           What4.Interface (Pred, getConfiguration)
import           What4.FunctionName (FunctionName, startFunctionName)
import           What4.ProgramLoc (ProgramLoc, plSourceLoc)

import           Lang.Crucible.Backend
                   ( IsSymInterface, IsSymBackend(..), HasSymInterface(..)
                   , AbortExecReason, SomeBackend(..), FrameIdentifier, Assumptions
                   )
import           Lang.Crucible.CFG.Core (BlockID, CFG, CFGPostdom, StmtSeq)
import           Lang.Crucible.CFG.Extension (StmtExtension, ExprExtension)
import           Lang.Crucible.FunctionHandle (FnHandleMap, HandleAllocator, mkHandle')
import           Lang.Crucible.Simulator.CallFrame
import           Lang.Crucible.Simulator.Evaluation (EvalAppFunc)
import           Lang.Crucible.Simulator.GlobalState (SymGlobalState)
import           Lang.Crucible.Simulator.Intrinsics (IntrinsicTypes)
import           Lang.Crucible.Simulator.RegMap (RegMap, emptyRegMap, RegValue, RegEntry)
import           Lang.Crucible.Types

------------------------------------------------------------------------
-- GlobalPair

-- | A value of some type 'v' together with a global state.
data GlobalPair sym (v :: Type) =
   GlobalPair
   { forall sym v. GlobalPair sym v -> v
_gpValue :: !v
   , forall sym v. GlobalPair sym v -> SymGlobalState sym
_gpGlobals :: !(SymGlobalState sym)
   }

-- | Access the value stored in the global pair.
gpValue :: Lens (GlobalPair sym u) (GlobalPair sym v) u v
gpValue :: forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue = (GlobalPair sym u -> u)
-> (GlobalPair sym u -> v -> GlobalPair sym v)
-> Lens (GlobalPair sym u) (GlobalPair sym v) u v
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens GlobalPair sym u -> u
forall sym v. GlobalPair sym v -> v
_gpValue (\GlobalPair sym u
s v
v -> GlobalPair sym u
s { _gpValue = v })

-- | Access the globals stored in the global pair.
gpGlobals :: Simple Lens (GlobalPair sym u) (SymGlobalState sym)
gpGlobals :: forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals = (GlobalPair sym u -> SymGlobalState sym)
-> (GlobalPair sym u -> SymGlobalState sym -> GlobalPair sym u)
-> Lens
     (GlobalPair sym u)
     (GlobalPair sym u)
     (SymGlobalState sym)
     (SymGlobalState sym)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens GlobalPair sym u -> SymGlobalState sym
forall sym v. GlobalPair sym v -> SymGlobalState sym
_gpGlobals (\GlobalPair sym u
s SymGlobalState sym
v -> GlobalPair sym u
s { _gpGlobals = v })


------------------------------------------------------------------------
-- TopFrame

-- | The currently-executing frame plus the global state associated with it.
type TopFrame sym ext f a = GlobalPair sym (SimFrame sym ext f a)

-- | Access the Crucible call frame inside a 'TopFrame'.
crucibleTopFrame ::
  Lens (TopFrame sym ext (CrucibleLang blocks r) ('Just args))
       (TopFrame sym ext (CrucibleLang blocks r) ('Just args'))
       (CallFrame sym ext blocks r args)
       (CallFrame sym ext blocks r args')
crucibleTopFrame :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r args
 -> f (CallFrame sym ext blocks r args'))
-> TopFrame
     sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args)
-> f (TopFrame
        sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args'))
crucibleTopFrame = (SimFrame
   sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args)
 -> f (SimFrame
         sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args')))
-> GlobalPair
     sym
     (SimFrame
        sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args))
-> f (GlobalPair
        sym
        (SimFrame
           sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args')))
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue ((SimFrame
    sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args)
  -> f (SimFrame
          sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args')))
 -> GlobalPair
      sym
      (SimFrame
         sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args))
 -> f (GlobalPair
         sym
         (SimFrame
            sym
            ext
            (CrucibleLang blocks r)
            ('Just @(Ctx CrucibleType) args'))))
-> ((CallFrame sym ext blocks r args
     -> f (CallFrame sym ext blocks r args'))
    -> SimFrame
         sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args)
    -> f (SimFrame
            sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args')))
-> (CallFrame sym ext blocks r args
    -> f (CallFrame sym ext blocks r args'))
-> GlobalPair
     sym
     (SimFrame
        sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args))
-> f (GlobalPair
        sym
        (SimFrame
           sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args')))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CallFrame sym ext blocks r args
 -> f (CallFrame sym ext blocks r args'))
-> SimFrame
     sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args)
-> f (SimFrame
        sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args'))
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (args :: Ctx CrucibleType)
       (blocks' :: Ctx (Ctx CrucibleType)) (r' :: CrucibleType)
       (args' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r args
 -> f (CallFrame sym ext blocks' r' args'))
-> SimFrame
     sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args)
-> f (SimFrame
        sym
        ext
        (CrucibleLang blocks' r')
        ('Just @(Ctx CrucibleType) args'))
crucibleSimFrame
{-# INLINE crucibleTopFrame #-}


overrideTopFrame ::
  Lens (TopFrame sym ext (OverrideLang r) ('Just args))
       (TopFrame sym ext (OverrideLang r') ('Just args'))
       (OverrideFrame sym r args)
       (OverrideFrame sym r' args')
overrideTopFrame :: forall sym ext (r :: CrucibleType) (args :: Ctx CrucibleType)
       (r' :: CrucibleType) (args' :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> TopFrame
     sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args)
-> f (TopFrame
        sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args'))
overrideTopFrame = (SimFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args)
 -> f (SimFrame
         sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args')))
-> GlobalPair
     sym
     (SimFrame
        sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args))
-> f (GlobalPair
        sym
        (SimFrame
           sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args')))
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue ((SimFrame
    sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args)
  -> f (SimFrame
          sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args')))
 -> GlobalPair
      sym
      (SimFrame
         sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args))
 -> f (GlobalPair
         sym
         (SimFrame
            sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args'))))
-> ((OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
    -> SimFrame
         sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args)
    -> f (SimFrame
            sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args')))
-> (OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> GlobalPair
     sym
     (SimFrame
        sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args))
-> f (GlobalPair
        sym
        (SimFrame
           sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args')))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> SimFrame
     sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args)
-> f (SimFrame
        sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args'))
forall sym ext (r :: CrucibleType) (args :: Ctx CrucibleType)
       (r' :: CrucibleType) (args' :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> SimFrame
     sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args)
-> f (SimFrame
        sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args'))
overrideSimFrame
{-# INLINE overrideTopFrame #-}

------------------------------------------------------------------------
-- AbortedResult

-- | An execution path that was prematurely aborted.  Note, an abort
--   does not necessarily indicate an error condition.  An execution
--   path might abort because it became infeasible (inconsistent path
--   conditions), because the program called an exit primitive, or
--   because of a true error condition (e.g., a failed assertion).
data AbortedResult sym ext where
  -- | A single aborted execution with the execution state at time of the abort and the reason.
  AbortedExec ::
    !AbortExecReason ->
    !(GlobalPair sym (SimFrame sym ext l args)) ->
    AbortedResult sym ext

  -- | An aborted execution that was ended by a call to 'exit'.
  AbortedExit ::
    !ExitCode ->
    AbortedResult sym ext

  -- | Two separate threads of execution aborted after a symbolic branch,
  --   possibly for different reasons.
  AbortedBranch ::
    !ProgramLoc       {- The source location of the branching control flow -} ->
    !(Pred sym)       {- The symbolic condition -} ->
    !(AbortedResult sym ext) {- The abort that occurred along the 'true' branch -} ->
    !(AbortedResult sym ext) {- The abort that occurred along the 'false' branch -} ->
    AbortedResult sym ext

------------------------------------------------------------------------
-- SomeFrame

-- | This represents an execution frame where its frame type
--   and arguments have been hidden.
data SomeFrame (f :: fk -> argk -> Type) = forall l a . SomeFrame !(f l a)

-- | Return the program locations of all the Crucible frames.
filterCrucibleFrames :: SomeFrame (SimFrame sym ext) -> Maybe ProgramLoc
filterCrucibleFrames :: forall sym ext.
SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> Maybe ProgramLoc
filterCrucibleFrames (SomeFrame (MF CallFrame sym ext blocks ret args1
f)) = ProgramLoc -> Maybe ProgramLoc
forall a. a -> Maybe a
Just (CallFrame sym ext blocks ret args1 -> ProgramLoc
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> ProgramLoc
frameProgramLoc CallFrame sym ext blocks ret args1
f)
filterCrucibleFrames SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
_ = Maybe ProgramLoc
forall a. Maybe a
Nothing

-- | Iterate over frames in the result.
arFrames :: Simple Traversal (AbortedResult sym ext) (SomeFrame (SimFrame sym ext))
arFrames :: forall sym ext (f :: Type -> Type).
Applicative f =>
(SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
 -> f (SomeFrame
         @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)))
-> AbortedResult sym ext -> f (AbortedResult sym ext)
arFrames SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
        @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext))
h (AbortedExec AbortExecReason
e GlobalPair sym (SimFrame sym ext l args)
p) =
  (\(SomeFrame SimFrame sym ext l a
f') -> AbortExecReason
-> GlobalPair sym (SimFrame sym ext l a) -> AbortedResult sym ext
forall sym ext l (args :: Maybe (Ctx CrucibleType)).
AbortExecReason
-> GlobalPair sym (SimFrame sym ext l args)
-> AbortedResult sym ext
AbortedExec AbortExecReason
e (GlobalPair sym (SimFrame sym ext l args)
p GlobalPair sym (SimFrame sym ext l args)
-> (GlobalPair sym (SimFrame sym ext l args)
    -> GlobalPair sym (SimFrame sym ext l a))
-> GlobalPair sym (SimFrame sym ext l a)
forall a b. a -> (a -> b) -> b
& (SimFrame sym ext l args -> Identity (SimFrame sym ext l a))
-> GlobalPair sym (SimFrame sym ext l args)
-> Identity (GlobalPair sym (SimFrame sym ext l a))
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue ((SimFrame sym ext l args -> Identity (SimFrame sym ext l a))
 -> GlobalPair sym (SimFrame sym ext l args)
 -> Identity (GlobalPair sym (SimFrame sym ext l a)))
-> SimFrame sym ext l a
-> GlobalPair sym (SimFrame sym ext l args)
-> GlobalPair sym (SimFrame sym ext l a)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ SimFrame sym ext l a
f'))
     (SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
 -> AbortedResult sym ext)
-> f (SomeFrame
        @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext))
-> f (AbortedResult sym ext)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
        @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext))
h (SimFrame sym ext l args
-> SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
forall fk argk (f :: fk -> argk -> Type) (l :: fk) (a :: argk).
f l a -> SomeFrame @fk @argk f
SomeFrame (GlobalPair sym (SimFrame sym ext l args)
pGlobalPair sym (SimFrame sym ext l args)
-> Getting
     (SimFrame sym ext l args)
     (GlobalPair sym (SimFrame sym ext l args))
     (SimFrame sym ext l args)
-> SimFrame sym ext l args
forall s a. s -> Getting a s a -> a
^.Getting
  (SimFrame sym ext l args)
  (GlobalPair sym (SimFrame sym ext l args))
  (SimFrame sym ext l args)
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue))
arFrames SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
        @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext))
_ (AbortedExit ExitCode
ec) = AbortedResult sym ext -> f (AbortedResult sym ext)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ExitCode -> AbortedResult sym ext
forall sym ext. ExitCode -> AbortedResult sym ext
AbortedExit ExitCode
ec)
arFrames SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
        @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext))
h (AbortedBranch ProgramLoc
predicate Pred sym
loc AbortedResult sym ext
r AbortedResult sym ext
s) =
  ProgramLoc
-> Pred sym
-> AbortedResult sym ext
-> AbortedResult sym ext
-> AbortedResult sym ext
forall sym ext.
ProgramLoc
-> Pred sym
-> AbortedResult sym ext
-> AbortedResult sym ext
-> AbortedResult sym ext
AbortedBranch ProgramLoc
predicate Pred sym
loc (AbortedResult sym ext
 -> AbortedResult sym ext -> AbortedResult sym ext)
-> f (AbortedResult sym ext)
-> f (AbortedResult sym ext -> AbortedResult sym ext)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
 -> f (SomeFrame
         @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)))
-> AbortedResult sym ext -> f (AbortedResult sym ext)
forall sym ext (f :: Type -> Type).
Applicative f =>
(SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
 -> f (SomeFrame
         @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)))
-> AbortedResult sym ext -> f (AbortedResult sym ext)
arFrames SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
        @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext))
h AbortedResult sym ext
r
                              f (AbortedResult sym ext -> AbortedResult sym ext)
-> f (AbortedResult sym ext) -> f (AbortedResult sym ext)
forall a b. f (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
 -> f (SomeFrame
         @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)))
-> AbortedResult sym ext -> f (AbortedResult sym ext)
forall sym ext (f :: Type -> Type).
Applicative f =>
(SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
 -> f (SomeFrame
         @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)))
-> AbortedResult sym ext -> f (AbortedResult sym ext)
arFrames SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> f (SomeFrame
        @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext))
h AbortedResult sym ext
s

-- | Print an exception context
ppExceptionContext :: [SomeFrame (SimFrame sym ext)] -> PP.Doc ann
ppExceptionContext :: forall sym ext ann.
[SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
-> Doc ann
ppExceptionContext [] = Doc ann
forall a. Monoid a => a
mempty
ppExceptionContext [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
frames = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat ((SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
 -> Doc ann)
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
-> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> Doc ann
forall sym ext ann.
SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> Doc ann
pp ([SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall a. HasCallStack => [a] -> [a]
init [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
frames))
 where
   pp :: SomeFrame (SimFrame sym ext) -> PP.Doc ann
   pp :: forall sym ext ann.
SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> Doc ann
pp (SomeFrame (OF OverrideFrame sym ret args1
f)) =
      String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"When calling" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> FunctionName -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow (OverrideFrame sym ret args1
fOverrideFrame sym ret args1
-> Getting FunctionName (OverrideFrame sym ret args1) FunctionName
-> FunctionName
forall s a. s -> Getting a s a -> a
^.Getting FunctionName (OverrideFrame sym ret args1) FunctionName
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(FunctionName -> f FunctionName)
-> OverrideFrame sym ret args -> f (OverrideFrame sym ret args)
override)
   pp (SomeFrame (MF CallFrame sym ext blocks ret args1
f)) =
      String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"In" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> SomeHandle -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow (CallFrame sym ext blocks ret args1 -> SomeHandle
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> SomeHandle
frameHandle CallFrame sym ext blocks ret args1
f) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+>
      String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"at" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Position -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Position -> Doc ann
PP.pretty (ProgramLoc -> Position
plSourceLoc (CallFrame sym ext blocks ret args1 -> ProgramLoc
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> ProgramLoc
frameProgramLoc CallFrame sym ext blocks ret args1
f))
   pp (SomeFrame (RF FunctionName
nm RegEntry sym (FrameRetType l)
_v)) =
      String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"While returning value from" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> FunctionName -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow FunctionName
nm


------------------------------------------------------------------------
-- PartialResult

-- | A 'PartialResult' represents the result of a computation that
--   might be only partially defined.  If the result is a 'TotalResult',
--   the the result is fully defined; however if it is a
--   'PartialResult', then some of the computation paths that led to
--   this result aborted for some reason, and the resulting value is
--   only defined if the associated condition is true.
data PartialResult sym ext (v :: Type)

     {- | A 'TotalRes' indicates that the the global pair is always defined. -}
   = TotalRes !(GlobalPair sym v)

    {- | 'PartialRes' indicates that the global pair may be undefined
        under some circumstances.  The predicate specifies under what
        conditions the 'GlobalPair' is defined.
        The 'AbortedResult' describes the circumstances under which
        the result would be partial.
     -}
   | PartialRes !ProgramLoc               -- location of symbolic branch point
                !(Pred sym)               -- if true, global pair is defined
                !(GlobalPair sym v)       -- the value
                !(AbortedResult sym ext)  -- failure cases (when pred. is false)



-- | Access the value stored in the partial result.
partialValue ::
  Lens (PartialResult sym ext u)
       (PartialResult sym ext v)
       (GlobalPair sym u)
       (GlobalPair sym v)
partialValue :: forall sym ext u v (f :: Type -> Type).
Functor f =>
(GlobalPair sym u -> f (GlobalPair sym v))
-> PartialResult sym ext u -> f (PartialResult sym ext v)
partialValue GlobalPair sym u -> f (GlobalPair sym v)
f (TotalRes GlobalPair sym u
x) = GlobalPair sym v -> PartialResult sym ext v
forall sym ext v. GlobalPair sym v -> PartialResult sym ext v
TotalRes (GlobalPair sym v -> PartialResult sym ext v)
-> f (GlobalPair sym v) -> f (PartialResult sym ext v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> GlobalPair sym u -> f (GlobalPair sym v)
f GlobalPair sym u
x
partialValue GlobalPair sym u -> f (GlobalPair sym v)
f (PartialRes ProgramLoc
loc Pred sym
p GlobalPair sym u
x AbortedResult sym ext
r) = (\GlobalPair sym v
y -> ProgramLoc
-> Pred sym
-> GlobalPair sym v
-> AbortedResult sym ext
-> PartialResult sym ext v
forall sym ext v.
ProgramLoc
-> Pred sym
-> GlobalPair sym v
-> AbortedResult sym ext
-> PartialResult sym ext v
PartialRes ProgramLoc
loc Pred sym
p GlobalPair sym v
y AbortedResult sym ext
r) (GlobalPair sym v -> PartialResult sym ext v)
-> f (GlobalPair sym v) -> f (PartialResult sym ext v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> GlobalPair sym u -> f (GlobalPair sym v)
f GlobalPair sym u
x
{-# INLINE partialValue #-}

-- | The result of resolving a function call.
data ResolvedCall p sym ext ret where
  -- | A resolved function call to an override.
  OverrideCall ::
    !(Override p sym ext args ret) ->
    !(OverrideFrame sym ret args) ->
    ResolvedCall p sym ext ret

  -- | A resolved function call to a Crucible function.
  CrucibleCall ::
    !(BlockID blocks args) ->
    !(CallFrame sym ext blocks ret args) ->
    ResolvedCall p sym ext ret

resolvedCallHandle :: ResolvedCall p sym ext ret -> SomeHandle
resolvedCallHandle :: forall p sym ext (ret :: CrucibleType).
ResolvedCall p sym ext ret -> SomeHandle
resolvedCallHandle (OverrideCall Override p sym ext args ret
_ OverrideFrame sym ret args
frm) = OverrideFrame sym ret args
frm OverrideFrame sym ret args
-> Getting SomeHandle (OverrideFrame sym ret args) SomeHandle
-> SomeHandle
forall s a. s -> Getting a s a -> a
^. Getting SomeHandle (OverrideFrame sym ret args) SomeHandle
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(SomeHandle -> f SomeHandle)
-> OverrideFrame sym ret args -> f (OverrideFrame sym ret args)
overrideHandle
resolvedCallHandle (CrucibleCall BlockID blocks args
_ CallFrame sym ext blocks ret args
frm) = CallFrame sym ext blocks ret args -> SomeHandle
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> SomeHandle
frameHandle CallFrame sym ext blocks ret args
frm


------------------------------------------------------------------------
-- ExecResult

-- | Executions that have completed either due to (partial or total)
--   successful completion or by some abort condition.
data ExecResult p sym ext (r :: Type)
   = -- | At least one execution path resulted in some return result.
     FinishedResult !(SimContext p sym ext) !(PartialResult sym ext r)
     -- | All execution paths resulted in an abort condition, and there is
     --   no result to return.
   | AbortedResult  !(SimContext p sym ext) !(AbortedResult sym ext)
     -- | An execution stopped somewhere in the middle of a run because
     --   a timeout condition occurred.
   | TimeoutResult !(ExecState p sym ext r)


execResultContext :: ExecResult p sym ext r -> SimContext p sym ext
execResultContext :: forall p sym ext r. ExecResult p sym ext r -> SimContext p sym ext
execResultContext (FinishedResult SimContext p sym ext
ctx PartialResult sym ext r
_) = SimContext p sym ext
ctx
execResultContext (AbortedResult SimContext p sym ext
ctx AbortedResult sym ext
_) = SimContext p sym ext
ctx
execResultContext (TimeoutResult ExecState p sym ext r
exst) = ExecState p sym ext r -> SimContext p sym ext
forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
execStateContext ExecState p sym ext r
exst

execStateContext :: ExecState p sym ext r -> SimContext p sym ext
execStateContext :: forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
execStateContext = \case
  ResultState ExecResult p sym ext r
res        -> ExecResult p sym ext r -> SimContext p sym ext
forall p sym ext r. ExecResult p sym ext r -> SimContext p sym ext
execResultContext ExecResult p sym ext r
res
  AbortState AbortExecReason
_ SimState p sym ext r f a
st        -> SimState p sym ext r f a
stSimState p sym ext r f a
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext r f a)
     (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 r f a)
  (SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
  UnwindCallState ValueFromValue p sym ext r r
_ AbortedResult sym ext
_ SimState p sym ext r f a
st -> SimState p sym ext r f a
stSimState p sym ext r f a
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext r f a)
     (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 r f a)
  (SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
  CallState ReturnHandler ret p sym ext r f a
_ ResolvedCall p sym ext ret
_ SimState p sym ext r f a
st       -> SimState p sym ext r f a
stSimState p sym ext r f a
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext r f a)
     (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 r f a)
  (SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
  TailCallState ValueFromValue p sym ext r ret
_ ResolvedCall p sym ext ret
_ SimState p sym ext r f a
st   -> SimState p sym ext r f a
stSimState p sym ext r f a
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext r f a)
     (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 r f a)
  (SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
  ReturnState FunctionName
_ ValueFromValue p sym ext r ret
_ RegEntry sym ret
_ SimState p sym ext r f a
st   -> SimState p sym ext r f a
stSimState p sym ext r f a
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext r f a)
     (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 r f a)
  (SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
  ControlTransferState ControlResumption p sym ext r f
_ SimState p sym ext r f ('Just @(Ctx CrucibleType) a)
st -> SimState p sym ext r f ('Just @(Ctx CrucibleType) a)
stSimState p sym ext r f ('Just @(Ctx CrucibleType) a)
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext r f ('Just @(Ctx CrucibleType) a))
     (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 r f ('Just @(Ctx CrucibleType) a))
  (SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
  RunningState RunningStateInfo blocks args
_ SimState
  p
  sym
  ext
  r
  (CrucibleLang blocks r)
  ('Just @(Ctx CrucibleType) args)
st      -> SimState
  p
  sym
  ext
  r
  (CrucibleLang blocks r)
  ('Just @(Ctx CrucibleType) args)
stSimState
  p
  sym
  ext
  r
  (CrucibleLang blocks r)
  ('Just @(Ctx CrucibleType) args)
-> Getting
     (SimContext p sym ext)
     (SimState
        p
        sym
        ext
        r
        (CrucibleLang blocks r)
        ('Just @(Ctx CrucibleType) 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
     r
     (CrucibleLang blocks r)
     ('Just @(Ctx CrucibleType) args))
  (SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
  SymbolicBranchState Pred sym
_ PausedFrame p sym ext r f
_ PausedFrame p sym ext r f
_ CrucibleBranchTarget f postdom_args
_ SimState p sym ext r f ('Just @(Ctx CrucibleType) args)
st -> SimState p sym ext r f ('Just @(Ctx CrucibleType) args)
stSimState p sym ext r f ('Just @(Ctx CrucibleType) args)
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext r f ('Just @(Ctx CrucibleType) 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 r f ('Just @(Ctx CrucibleType) args))
  (SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
  OverrideState Override p sym ext args ret
_ SimState
  p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) args)
st -> SimState
  p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) args)
stSimState
  p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) args)
-> Getting
     (SimContext p sym ext)
     (SimState
        p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) 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 r (OverrideLang ret) ('Just @(Ctx CrucibleType) args))
  (SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
  BranchMergeState CrucibleBranchTarget f args
_ SimState p sym ext r f args
st -> SimState p sym ext r f args
stSimState p sym ext r f args
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext r f 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 r f args)
  (SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext
  InitialState SimContext p sym ext
stctx SymGlobalState sym
_ AbortHandler p sym ext (RegEntry sym ret)
_ TypeRepr ret
_ ExecCont
  p
  sym
  ext
  (RegEntry sym ret)
  (OverrideLang ret)
  ('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType))
_ -> SimContext p sym ext
stctx

execStateSimState :: ExecState p sym ext r
                  -> Maybe (SomeSimState p sym ext r)
execStateSimState :: forall p sym ext r.
ExecState p sym ext r -> Maybe (SomeSimState p sym ext r)
execStateSimState = \case
  ResultState ExecResult p sym ext r
_                  -> Maybe (SomeSimState p sym ext r)
forall a. Maybe a
Nothing
  AbortState AbortExecReason
_ SimState p sym ext r f a
st                -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState p sym ext r f a -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState p sym ext r f a
st)
  UnwindCallState ValueFromValue p sym ext r r
_ AbortedResult sym ext
_ SimState p sym ext r f a
st         -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState p sym ext r f a -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState p sym ext r f a
st)
  CallState ReturnHandler ret p sym ext r f a
_ ResolvedCall p sym ext ret
_ SimState p sym ext r f a
st               -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState p sym ext r f a -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState p sym ext r f a
st)
  TailCallState ValueFromValue p sym ext r ret
_ ResolvedCall p sym ext ret
_ SimState p sym ext r f a
st           -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState p sym ext r f a -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState p sym ext r f a
st)
  ReturnState FunctionName
_ ValueFromValue p sym ext r ret
_ RegEntry sym ret
_ SimState p sym ext r f a
st           -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState p sym ext r f a -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState p sym ext r f a
st)
  ControlTransferState ControlResumption p sym ext r f
_ SimState p sym ext r f ('Just @(Ctx CrucibleType) a)
st      -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState p sym ext r f ('Just @(Ctx CrucibleType) a)
-> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState p sym ext r f ('Just @(Ctx CrucibleType) a)
st)
  RunningState RunningStateInfo blocks args
_ SimState
  p
  sym
  ext
  r
  (CrucibleLang blocks r)
  ('Just @(Ctx CrucibleType) args)
st              -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState
  p
  sym
  ext
  r
  (CrucibleLang blocks r)
  ('Just @(Ctx CrucibleType) args)
-> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState
  p
  sym
  ext
  r
  (CrucibleLang blocks r)
  ('Just @(Ctx CrucibleType) args)
st)
  SymbolicBranchState Pred sym
_ PausedFrame p sym ext r f
_ PausedFrame p sym ext r f
_ CrucibleBranchTarget f postdom_args
_ SimState p sym ext r f ('Just @(Ctx CrucibleType) args)
st -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState p sym ext r f ('Just @(Ctx CrucibleType) args)
-> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState p sym ext r f ('Just @(Ctx CrucibleType) args)
st)
  OverrideState Override p sym ext args ret
_ SimState
  p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) args)
st             -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState
  p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) args)
-> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState
  p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) args)
st)
  BranchMergeState CrucibleBranchTarget f args
_ SimState p sym ext r f args
st          -> SomeSimState p sym ext r -> Maybe (SomeSimState p sym ext r)
forall a. a -> Maybe a
Just (SimState p sym ext r f args -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
SomeSimState SimState p sym ext r f args
st)
  InitialState SimContext p sym ext
_ SymGlobalState sym
_ AbortHandler p sym ext (RegEntry sym ret)
_ TypeRepr ret
_ ExecCont
  p
  sym
  ext
  (RegEntry sym ret)
  (OverrideLang ret)
  ('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType))
_         -> Maybe (SomeSimState p sym ext r)
forall a. Maybe a
Nothing

-----------------------------------------------------------------------
-- ExecState

-- | An 'ExecState' represents an intermediate state of executing a
--   Crucible program.  The Crucible simulator executes by transitioning
--   between these different states until it results in a 'ResultState',
--   indicating the program has completed.
data ExecState p sym ext (rtp :: Type)
   {- | The 'ResultState' is used to indicate that the program has completed. -}
   = ResultState
       !(ExecResult p sym ext rtp)

   {- | An abort state indicates that the included 'SimState' encountered
        an abort event while executing its next step.  The state needs to
        be unwound to its nearest enclosing branch point and resumed. -}
   | forall f a.
       AbortState
         !AbortExecReason
           {- Description of what abort condition occurred -}
         !(SimState p sym ext rtp f a)
           {- State of the simulator prior to causing the abort condition -}

   {- | An unwind call state occurs when we are about to leave the context of a
        function call because of an abort.  The included @ValueFromValue@ is the
        context of the call site we are about to unwind into, and the @AbortedResult@
        indicates the reason we are aborting.
    -}
   | forall f a r.
       UnwindCallState
         !(ValueFromValue p sym ext rtp r) {- Caller's context -}
         !(AbortedResult sym ext)          {- Abort causing the stack unwind -}
         !(SimState p sym ext rtp f a)

   {- | A call state is entered when we are about to make a function call to
        the included call frame, which has already resolved the implementation
        and arguments to the function.
    -}
   | forall f a ret.
       CallState
         !(ReturnHandler ret p sym ext rtp f a)
         !(ResolvedCall p sym ext ret)
         !(SimState p sym ext rtp f a)

   {- | A tail-call state is entered when we are about to make a function call to
        the included call frame, and this is the last action we need to take in the
        current caller. Note, we can only enter a tail-call state if there are no
        pending merge points in the caller.  This means that sometimes calls
        that appear to be in tail-call position may nonetheless have to be treated
        as ordinary calls.
    -}
   | forall f a ret.
       TailCallState
         !(ValueFromValue p sym ext rtp ret) {- Calling context to return to -}
         !(ResolvedCall p sym ext ret)       {- Function to call -}
         !(SimState p sym ext rtp f a)

   {- | A return state is entered after the final return value of a function
        is computed, and just before we resolve injecting the return value
        back into the caller's context.
    -}
   | forall f a ret.
       ReturnState
         !FunctionName {- Name of the function we are returning from -}
         !(ValueFromValue p sym ext rtp ret) {- Caller's context -}
         !(RegEntry sym ret) {- Return value -}
         !(SimState p sym ext rtp f a)

   {- | A running state indicates the included 'SimState' is ready to enter
        and execute a Crucible basic block, or to resume a basic block
        from a call site. -}
   | forall blocks r args.
       RunningState
         !(RunningStateInfo blocks args)
         !(SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))

   {- | A symbolic branch state indicates that the execution needs to
        branch on a non-trivial symbolic condition.  The included @Pred@
        is the condition to branch on.  The first @PausedFrame@ is
        the path that corresponds to the @Pred@ being true, and the second
        is the false branch.
    -}
   | forall f args postdom_args.
       SymbolicBranchState
         !(Pred sym) {- predicate to branch on -}
         !(PausedFrame p sym ext rtp f) {- true path-}
         !(PausedFrame p sym ext rtp f)  {- false path -}
         !(CrucibleBranchTarget f postdom_args) {- merge point -}
         !(SimState p sym ext rtp f ('Just args))

   {- | A control transfer state is entered just prior to invoking a
        control resumption.  Control resumptions are responsible
        for transitioning from the end of one basic block to another,
        although there are also some intermediate states related to
        resolving switch statements.
    -}
   | forall f a.
       ControlTransferState
         !(ControlResumption p sym ext rtp f)
         !(SimState p sym ext rtp f ('Just a))

   {- | An override state indicates the included 'SimState' is prepared to
        execute a code override. -}
   | forall args ret.
       OverrideState
         !(Override p sym ext args ret)
           {- The override code to execute -}
         !(SimState p sym ext rtp (OverrideLang ret) ('Just args))
           {- State of the simulator prior to activating the override -}

   {- | A branch merge state occurs when the included 'SimState' is
        in the process of transferring control to the included 'CrucibleBranchTarget'.
        We enter a BranchMergeState every time we need to _check_ if there is a
        pending branch, even if no branch is pending. During this process, paths may
        have to be merged.  If several branches must merge at the same control point,
        this state may be entered several times in succession before returning
        to a 'RunningState'. -}
   | forall f args.
       BranchMergeState
         !(CrucibleBranchTarget f args)
           {- Target of the control-flow transfer -}
         !(SimState p sym ext rtp f args)
           {- State of the simulator before merging pending branches -}

   {- | An initial state indicates the state of a simulator just before execution begins.
        It specifies all the initial data necessary to begin simulating.  The given
        @ExecCont@ will be executed in a fresh @SimState@ representing the default starting
        call frame.
    -}
   | forall ret. rtp ~ RegEntry sym ret =>
       InitialState
         !(SimContext p sym ext)
            {- initial 'SimContext' state -}
         !(SymGlobalState sym)
            {- state of Crucible global variables -}
         !(AbortHandler p sym ext (RegEntry sym ret))
            {- initial abort handler -}
         !(TypeRepr ret)
            {- return type repr -}
         !(ExecCont p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx))
            {- Entry continuation -}

-- | An action which will construct an 'ExecState' given a current
--   'SimState'. Such continuations correspond to a single transition
--   of the simulator transition system.
type ExecCont p sym ext r f a =
  ReaderT (SimState p sym ext r f a) IO (ExecState p sym ext r)

-- | Some additional information attached to a @RunningState@
--   that indicates how we got to this running state.
data RunningStateInfo blocks args
    -- | This indicates that we are now in a @RunningState@ because
    --   we transferred execution to the start of a basic block.
  = RunBlockStart !(BlockID blocks args)
    -- | This indicates that we are in a @RunningState@ because we
    --   reached the terminal statement of a basic block.
  | RunBlockEnd !(Some (BlockID blocks))
    -- | This indicates that we are in a @RunningState@ because we
    --   returned from calling the named function.
  | RunReturnFrom !FunctionName
    -- | This indicates that we are now in a @RunningState@ because
    --   we finished branch merging prior to the start of a block.
  | RunPostBranchMerge !(BlockID blocks args)

-- | A 'ResolvedJump' is a block label together with a collection of
--   actual arguments that are expected by that block.  These data
--   are sufficient to actually transfer control to the named label.
data ResolvedJump sym blocks
  = forall args.
      ResolvedJump
        !(BlockID blocks args)
        !(RegMap sym args)

-- | When a path of execution is paused by the symbolic simulator
--   (while it first explores other paths), a 'ControlResumption'
--   indicates what actions must later be taken in order to resume
--   execution of that path.
data ControlResumption p sym ext rtp f where
  {- | When resuming a paused frame with a @ContinueResumption@,
       no special work needs to be done, simply begin executing
       statements of the basic block. -}
  ContinueResumption ::
    !(ResolvedJump sym blocks) ->
    ControlResumption p sym ext rtp (CrucibleLang blocks r)

  {- | When resuming with a @CheckMergeResumption@, we must check
       for the presence of pending merge points before resuming. -}
  CheckMergeResumption ::
    !(ResolvedJump sym blocks) ->
    ControlResumption p sym ext rtp (CrucibleLang blocks r)

  {- | When resuming a paused frame with a @SwitchResumption@, we must
       continue branching to possible alternatives in a variant elimination
       statement.  In other words, we are still in the process of
       transferring control away from the current basic block (which is now
       at a final @VariantElim@ terminal statement). -}
  SwitchResumption ::
    ![(Pred sym, ResolvedJump sym blocks)] {- remaining branches -} ->
    ControlResumption p sym ext rtp (CrucibleLang blocks r)

  {- | When resuming a paused frame with an @OverrideResumption@, we
       simply return control to the included thunk, which represents
       the remaining computation for the override.
   -}
  OverrideResumption ::
    ExecCont p sym ext rtp (OverrideLang r) ('Just args) ->
    !(RegMap sym args) ->
    ControlResumption p sym ext rtp (OverrideLang r)

------------------------------------------------------------------------
-- Paused Frame

-- | A 'PausedFrame' represents a path of execution that has been postponed
--   while other paths are explored.  It consists of a (potentially partial)
--   'SimFrame' together with some information about how to resume execution
--   of that frame.
data PausedFrame p sym ext rtp f
   = forall old_args.
       PausedFrame
       { ()
pausedFrame  :: !(PartialResultFrame sym ext f ('Just old_args))
       , forall p sym ext rtp f.
PausedFrame p sym ext rtp f -> ControlResumption p sym ext rtp f
resume       :: !(ControlResumption p sym ext rtp f)
       , forall p sym ext rtp f.
PausedFrame p sym ext rtp f -> Maybe ProgramLoc
pausedLoc    :: !(Maybe ProgramLoc)
       }

-- | This describes the state of the sibling path at a symbolic branch point.
--   A symbolic branch point starts with the sibling in the 'VFFActivePath'
--   state, which indicates that the sibling path still needs to be executed.
--   After the first path to be explored has reached the merge point, the
--   places of the two paths are exchanged, and the completed path is
--   stored in the 'VFFCompletePath' state until the second path also
--   reaches its merge point.  The two paths will then be merged,
--   and execution will continue beyond the merge point.
data VFFOtherPath p sym ext ret f args

     {- | This corresponds the a path that still needs to be analyzed. -}
   = VFFActivePath
        !(PausedFrame p sym ext ret f)
          {- Other branch we still need to run -}

     {- | This is a completed execution path. -}
   | VFFCompletePath
        !(Assumptions sym)
          {- Assumptions that we collected while analyzing the branch -}
        !(PartialResultFrame sym ext f args)
          {- Result of running the other branch -}



{- | This type contains information about the current state of the exploration
of the branching structure of a program.  The 'ValueFromFrame' states correspond
to the structure of symbolic branching that occurs within a single function call.

The type parameters have the following meanings:

  * @p@ is the personality of the simulator (i.e., custom user state).

  * @sym@ is the simulator backend being used.

  * @ext@ specifies what extensions to the Crucible language are enabled

  * @ret@ is the global return type of the entire execution.

  * @f@ is the type of the top frame.
-}

data ValueFromFrame p sym ext (ret :: Type) (f :: Type)

  {- | We are working on a branch;  this could be the first or the second
       of both branches (see the 'VFFOtherPath' field). -}
  = forall args.
    VFFBranch

      !(ValueFromFrame p sym ext ret f)
      {- The outer context---what to do once we are done with both branches -}

      !FrameIdentifier
      {- This is the frame identifier in the solver before this branch,
         so that when we are done we can pop-off the assumptions we accumulated
         while processing the branch -}

      !ProgramLoc
      {- Program location of the branch point -}

      !(Pred sym)
      {- Assertion of currently-active branch -}

      !(VFFOtherPath p sym ext ret f args)
      {- Info about the state of the other branch.
         If the other branch is "VFFActivePath", then we still
         need to process it;  if it is "VFFCompletePath", then
         it is finished, and so once we are done then we go back to the
         outer context. -}

      !(CrucibleBranchTarget f args)
      {- Identifies the postdominator where the two branches merge back together -}



  {- | We are on a branch where the other branch was aborted before getting
     to the merge point.  -}
  | VFFPartial

      !(ValueFromFrame p sym ext ret f)
      {- The other context--what to do once we are done with this branch -}

      !ProgramLoc
      {- Program location of the branch point -}

      !(Pred sym)
      {- Assertion of currently-active branch -}

      !(AbortedResult sym ext)
      {- What happened on the other branch -}

      !PendingPartialMerges
      {- should we abort the (outer) sibling branch when it merges with us? -}


  {- | When we are finished with this branch we should return from the function. -}
  | VFFEnd

      !(ValueFromValue p sym ext ret (FrameRetType f))


-- | Data about whether the surrounding context is expecting a merge to
--   occur or not.  If the context sill expects a merge, we need to
--   take some actions to indicate that the merge will not occur;
--   otherwise there is no special work to be done.
data PendingPartialMerges =
    {- | Don't indicate an abort condition in the context -}
    NoNeedToAbort

    {- | Indicate an abort condition in the context when we
         get there again. -}
  | NeedsToBeAborted


{- | This type contains information about the current state of the exploration
of the branching structure of a program.  The 'ValueFromValue' states correspond
to stack call frames in a more traditional simulator environment.

The type parameters have the following meanings:

  * @p@ is the personality of the simulator (i.e., custom user state).

  * @sym@ is the simulator backend being used.

  * @ext@ specifies what extensions to the Crucible language are enabled

  * @ret@ is the global return type of the entire computation

  * @top_return@ is the return type of the top-most call on the stack.
-}
data ValueFromValue p sym ext (ret :: Type) (top_return :: CrucibleType)

  {- | 'VFVCall' denotes a call site in the outer context, and represents
       the point to which a function higher on the stack will
       eventually return.  The three arguments are:

         * The context in which the call happened.

         * The frame of the caller

         * How to modify the current sim frame and resume execution
           when we obtain the return value
  -}
  = forall args caller.
    VFVCall

    !(ValueFromFrame p sym ext ret caller)
    -- The context in which the call happened.

    !(SimFrame sym ext caller args)
    -- The frame of the caller.

    !(ReturnHandler top_return p sym ext ret caller args)
    -- How to modify the current sim frame and resume execution
    -- when we obtain the return value

  {- | A partial value.
    The predicate indicates what needs to hold to avoid the partiality.
    The "AbortedResult" describes what could go wrong if the predicate
    does not hold. -}
  | VFVPartial
      !(ValueFromValue p sym ext ret top_return)
      !ProgramLoc
      !(Pred sym)
      !(AbortedResult sym ext)

  {- | The top return value, indicating the program termination point. -}
  | (ret ~ RegEntry sym top_return) => VFVEnd



instance PP.Pretty (ValueFromValue p ext sym root rp) where
  pretty :: forall ann. ValueFromValue p ext sym root rp -> Doc ann
pretty = ValueFromValue p ext sym root rp -> Doc ann
forall p ext sym root (rp :: CrucibleType) ann.
ValueFromValue p ext sym root rp -> Doc ann
ppValueFromValue

instance PP.Pretty (ValueFromFrame p ext sym ret f) where
  pretty :: forall ann. ValueFromFrame p ext sym ret f -> Doc ann
pretty = ValueFromFrame p ext sym ret f -> Doc ann
forall p ext sym ret f ann.
ValueFromFrame p ext sym ret f -> Doc ann
ppValueFromFrame

instance PP.Pretty (VFFOtherPath ctx sym ext r f a) where
  pretty :: forall ann. VFFOtherPath ctx sym ext r f a -> Doc ann
pretty (VFFActivePath PausedFrame ctx sym ext r f
_)   = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"active_path"
  pretty (VFFCompletePath Assumptions sym
_ PartialResultFrame sym ext f a
_) = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"complete_path"

ppValueFromFrame :: ValueFromFrame p sym ext ret f -> PP.Doc ann
ppValueFromFrame :: forall p ext sym ret f ann.
ValueFromFrame p ext sym ret f -> Doc ann
ppValueFromFrame ValueFromFrame p sym ext ret f
vff =
  case ValueFromFrame p sym ext ret f
vff of
    VFFBranch ValueFromFrame p sym ext ret f
ctx FrameIdentifier
_ ProgramLoc
_ Pred sym
_ VFFOtherPath p sym ext ret f args
other CrucibleBranchTarget f args
mp ->
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat
      [ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"intra_branch"
      , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
2 (VFFOtherPath p sym ext ret f args -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. VFFOtherPath p sym ext ret f args -> Doc ann
PP.pretty VFFOtherPath p sym ext ret f args
other)
      , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
2 (String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (CrucibleBranchTarget f args -> String
forall f (args :: Maybe (Ctx CrucibleType)).
CrucibleBranchTarget f args -> String
ppBranchTarget CrucibleBranchTarget f args
mp))
      , ValueFromFrame p sym ext ret f -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ValueFromFrame p sym ext ret f -> Doc ann
PP.pretty ValueFromFrame p sym ext ret f
ctx
      ]
    VFFPartial ValueFromFrame p sym ext ret f
ctx ProgramLoc
_ Pred sym
_ AbortedResult sym ext
_ PendingPartialMerges
_ ->
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat
      [ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"intra_partial"
      , ValueFromFrame p sym ext ret f -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ValueFromFrame p sym ext ret f -> Doc ann
PP.pretty ValueFromFrame p sym ext ret f
ctx
      ]
    VFFEnd ValueFromValue p sym ext ret (FrameRetType f)
ctx ->
      ValueFromValue p sym ext ret (FrameRetType f) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann.
ValueFromValue p sym ext ret (FrameRetType f) -> Doc ann
PP.pretty ValueFromValue p sym ext ret (FrameRetType f)
ctx

ppValueFromValue :: ValueFromValue p sym ext root tp -> PP.Doc ann
ppValueFromValue :: forall p ext sym root (rp :: CrucibleType) ann.
ValueFromValue p ext sym root rp -> Doc ann
ppValueFromValue ValueFromValue p sym ext root tp
vfv =
  case ValueFromValue p sym ext root tp
vfv of
    VFVCall ValueFromFrame p sym ext root caller
ctx SimFrame sym ext caller args
_ ReturnHandler tp p sym ext root caller args
_ ->
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat
      [ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"call"
      , ValueFromFrame p sym ext root caller -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ValueFromFrame p sym ext root caller -> Doc ann
PP.pretty ValueFromFrame p sym ext root caller
ctx
      ]
    VFVPartial ValueFromValue p sym ext root tp
ctx ProgramLoc
_ Pred sym
_ AbortedResult sym ext
_ ->
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat
      [ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"inter_partial"
      , ValueFromValue p sym ext root tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ValueFromValue p sym ext root tp -> Doc ann
PP.pretty ValueFromValue p sym ext root tp
ctx
      ]
    ValueFromValue p sym ext root tp
VFVEnd -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
"root"


-----------------------------------------------------------------------
-- parentFrames

-- | Return parents frames in reverse order.
parentFrames :: ValueFromFrame p sym ext r a -> [SomeFrame (SimFrame sym ext)]
parentFrames :: forall p sym ext r a.
ValueFromFrame p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
parentFrames ValueFromFrame p sym ext r a
c0 =
  case ValueFromFrame p sym ext r a
c0 of
    VFFBranch ValueFromFrame p sym ext r a
c FrameIdentifier
_ ProgramLoc
_ Pred sym
_ VFFOtherPath p sym ext r a args
_ CrucibleBranchTarget a args
_ -> ValueFromFrame p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall p sym ext r a.
ValueFromFrame p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
parentFrames ValueFromFrame p sym ext r a
c
    VFFPartial ValueFromFrame p sym ext r a
c ProgramLoc
_ Pred sym
_ AbortedResult sym ext
_ PendingPartialMerges
_ -> ValueFromFrame p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall p sym ext r a.
ValueFromFrame p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
parentFrames ValueFromFrame p sym ext r a
c
    VFFEnd ValueFromValue p sym ext r (FrameRetType a)
vfv -> ValueFromValue p sym ext r (FrameRetType a)
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall p sym ext r (a :: CrucibleType).
ValueFromValue p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
vfvParents ValueFromValue p sym ext r (FrameRetType a)
vfv

-- | Return parents frames in reverse order.
vfvParents :: ValueFromValue p sym ext r a -> [SomeFrame (SimFrame sym ext)]
vfvParents :: forall p sym ext r (a :: CrucibleType).
ValueFromValue p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
vfvParents ValueFromValue p sym ext r a
c0 =
  case ValueFromValue p sym ext r a
c0 of
    VFVCall ValueFromFrame p sym ext r caller
c SimFrame sym ext caller args
f ReturnHandler a p sym ext r caller args
_ -> SimFrame sym ext caller args
-> SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
forall fk argk (f :: fk -> argk -> Type) (l :: fk) (a :: argk).
f l a -> SomeFrame @fk @argk f
SomeFrame SimFrame sym ext caller args
f SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall a. a -> [a] -> [a]
: ValueFromFrame p sym ext r caller
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall p sym ext r a.
ValueFromFrame p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
parentFrames ValueFromFrame p sym ext r caller
c
    VFVPartial ValueFromValue p sym ext r a
c ProgramLoc
_ Pred sym
_ AbortedResult sym ext
_ -> ValueFromValue p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall p sym ext r (a :: CrucibleType).
ValueFromValue p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
vfvParents ValueFromValue p sym ext r a
c
    ValueFromValue p sym ext r a
VFVEnd -> []

------------------------------------------------------------------------
-- ReturnHandler

{- | A 'ReturnHandler' indicates what actions to take to resume
executing in a caller's context once a function call has completed and
the return value is available.

The type parameters have the following meanings:

  * @ret@ is the type of the return value that is expected.

  * @p@ is the personality of the simulator (i.e., custom user state).

  * @sym@ is the simulator backend being used.

  * @ext@ specifies what extensions to the Crucible language are enabled.

  * @root@ is the global return type of the entire computation.

  * @f@ is the stack type of the caller.

  * @args@ is the type of the local variables in scope prior to the call.
-}
data ReturnHandler (ret :: CrucibleType) p sym ext root f args where
  {- | The 'ReturnToOverride' constructor indicates that the calling
       context is primitive code written directly in Haskell.
   -}
  ReturnToOverride ::
    (RegEntry sym ret -> SimState p sym ext root (OverrideLang r) ('Just args) -> IO (ExecState p sym ext root))
      {- Remaining override code to run when the return value becomes available -} ->
    ReturnHandler ret p sym ext root (OverrideLang r) ('Just args)

  {- | The 'ReturnToCrucible' constructor indicates that the calling context is an
       ordinary function call position from within a Crucible basic block.
       The included 'StmtSeq' is the remaining statements in the basic block to be
       executed following the return.
  -}
  ReturnToCrucible ::
    TypeRepr ret                       {- Type of the return value -} ->
    StmtSeq ext blocks r (ctx ::> ret) {- Remaining statements to execute -} ->
    ReturnHandler ret p sym ext root (CrucibleLang blocks r) ('Just ctx)

  {- | The 'TailReturnToCrucible' constructor indicates that the calling context is a
       tail call position from the end of a Crucible basic block.  Upon receiving
       the return value, that value should be immediately returned in the caller's
       context as well.
  -}
  TailReturnToCrucible ::
    (ret ~ r) =>
    ReturnHandler ret p sym ext root (CrucibleLang blocks r) ctx


------------------------------------------------------------------------
-- ActiveTree

type PartialResultFrame sym ext f args =
  PartialResult sym ext (SimFrame sym ext f args)

{- | An active execution tree contains at least one active execution.
     The data structure is organized so that the current execution
     can be accessed rapidly. -}
data ActiveTree p sym ext root (f :: Type) args
   = ActiveTree
      { forall p sym ext root f (args :: Maybe (Ctx CrucibleType)).
ActiveTree p sym ext root f args -> ValueFromFrame p sym ext root f
_actContext :: !(ValueFromFrame p sym ext root f)
      , forall p sym ext root f (args :: Maybe (Ctx CrucibleType)).
ActiveTree p sym ext root f args
-> PartialResultFrame sym ext f args
_actResult  :: !(PartialResultFrame sym ext f args)
      }

-- | Create a tree with a single top frame.
singletonTree ::
  TopFrame sym ext f args ->
  ActiveTree p sym ext (RegEntry sym (FrameRetType f)) f args
singletonTree :: forall sym ext f (args :: Maybe (Ctx CrucibleType)) p.
TopFrame sym ext f args
-> ActiveTree p sym ext (RegEntry sym (FrameRetType f)) f args
singletonTree TopFrame sym ext f args
f = ActiveTree { _actContext :: ValueFromFrame p sym ext (RegEntry sym (FrameRetType f)) f
_actContext = ValueFromValue
  p sym ext (RegEntry sym (FrameRetType f)) (FrameRetType f)
-> ValueFromFrame p sym ext (RegEntry sym (FrameRetType f)) f
forall p sym ext ret f.
ValueFromValue p sym ext ret (FrameRetType f)
-> ValueFromFrame p sym ext ret f
VFFEnd ValueFromValue
  p sym ext (RegEntry sym (FrameRetType f)) (FrameRetType f)
forall p sym ext ret (top_return :: CrucibleType).
((ret :: Type) ~ (RegEntry sym top_return :: Type)) =>
ValueFromValue p sym ext ret top_return
VFVEnd
                             , _actResult :: PartialResultFrame sym ext f args
_actResult = TopFrame sym ext f args -> PartialResultFrame sym ext f args
forall sym ext v. GlobalPair sym v -> PartialResult sym ext v
TotalRes TopFrame sym ext f args
f
                             }

-- | Access the calling context of the currently-active frame
actContext ::
  Lens (ActiveTree p sym ext root f args)
       (ActiveTree p sym ext root f args)
       (ValueFromFrame p sym ext root f)
       (ValueFromFrame p sym ext root f)
actContext :: forall p sym ext root f (args :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(ValueFromFrame p sym ext root f
 -> f (ValueFromFrame p sym ext root f))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args)
actContext = (ActiveTree p sym ext root f args
 -> ValueFromFrame p sym ext root f)
-> (ActiveTree p sym ext root f args
    -> ValueFromFrame p sym ext root f
    -> ActiveTree p sym ext root f args)
-> Lens
     (ActiveTree p sym ext root f args)
     (ActiveTree p sym ext root f args)
     (ValueFromFrame p sym ext root f)
     (ValueFromFrame p sym ext root f)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens ActiveTree p sym ext root f args -> ValueFromFrame p sym ext root f
forall p sym ext root f (args :: Maybe (Ctx CrucibleType)).
ActiveTree p sym ext root f args -> ValueFromFrame p sym ext root f
_actContext (\ActiveTree p sym ext root f args
s ValueFromFrame p sym ext root f
v -> ActiveTree p sym ext root f args
s { _actContext = v })

actResult ::
  Lens (ActiveTree p sym ext root f args0)
       (ActiveTree p sym ext root f args1)
       (PartialResult sym ext (SimFrame sym ext f args0))
       (PartialResult sym ext (SimFrame sym ext f args1))
actResult :: forall p sym ext root f (args0 :: Maybe (Ctx CrucibleType))
       (args1 :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(PartialResult sym ext (SimFrame sym ext f args0)
 -> f (PartialResult sym ext (SimFrame sym ext f args1)))
-> ActiveTree p sym ext root f args0
-> f (ActiveTree p sym ext root f args1)
actResult = (ActiveTree p sym ext root f args0
 -> PartialResult sym ext (SimFrame sym ext f args0))
-> (ActiveTree p sym ext root f args0
    -> PartialResult sym ext (SimFrame sym ext f args1)
    -> ActiveTree p sym ext root f args1)
-> Lens
     (ActiveTree p sym ext root f args0)
     (ActiveTree p sym ext root f args1)
     (PartialResult sym ext (SimFrame sym ext f args0))
     (PartialResult sym ext (SimFrame sym ext f args1))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens ActiveTree p sym ext root f args0
-> PartialResult sym ext (SimFrame sym ext f args0)
forall p sym ext root f (args :: Maybe (Ctx CrucibleType)).
ActiveTree p sym ext root f args
-> PartialResultFrame sym ext f args
_actResult ActiveTree p sym ext root f args0
-> PartialResult sym ext (SimFrame sym ext f args1)
-> ActiveTree p sym ext root f args1
forall {p} {sym} {ext} {root} {f}
       {args :: Maybe (Ctx CrucibleType)}
       {args :: Maybe (Ctx CrucibleType)}.
ActiveTree p sym ext root f args
-> PartialResultFrame sym ext f args
-> ActiveTree p sym ext root f args
setter
  where setter :: ActiveTree p sym ext root f args
-> PartialResultFrame sym ext f args
-> ActiveTree p sym ext root f args
setter ActiveTree p sym ext root f args
s PartialResultFrame sym ext f args
v = ActiveTree { _actContext :: ValueFromFrame p sym ext root f
_actContext = ActiveTree p sym ext root f args -> ValueFromFrame p sym ext root f
forall p sym ext root f (args :: Maybe (Ctx CrucibleType)).
ActiveTree p sym ext root f args -> ValueFromFrame p sym ext root f
_actContext ActiveTree p sym ext root f args
s
                                , _actResult :: PartialResultFrame sym ext f args
_actResult = PartialResultFrame sym ext f args
v
                                }
{-# INLINE actResult #-}

-- | Access the currently-active frame
actFrame ::
  Lens (ActiveTree p sym ext root f args)
       (ActiveTree p sym ext root f args')
       (TopFrame sym ext f args)
       (TopFrame sym ext f args')
actFrame :: forall p sym ext root f (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(TopFrame sym ext f args -> f (TopFrame sym ext f args'))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args')
actFrame = (PartialResult sym ext (SimFrame sym ext f args)
 -> f (PartialResult sym ext (SimFrame sym ext f args')))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args')
forall p sym ext root f (args0 :: Maybe (Ctx CrucibleType))
       (args1 :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(PartialResult sym ext (SimFrame sym ext f args0)
 -> f (PartialResult sym ext (SimFrame sym ext f args1)))
-> ActiveTree p sym ext root f args0
-> f (ActiveTree p sym ext root f args1)
actResult ((PartialResult sym ext (SimFrame sym ext f args)
  -> f (PartialResult sym ext (SimFrame sym ext f args')))
 -> ActiveTree p sym ext root f args
 -> f (ActiveTree p sym ext root f args'))
-> ((TopFrame sym ext f args -> f (TopFrame sym ext f args'))
    -> PartialResult sym ext (SimFrame sym ext f args)
    -> f (PartialResult sym ext (SimFrame sym ext f args')))
-> (TopFrame sym ext f args -> f (TopFrame sym ext f args'))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext f args -> f (TopFrame sym ext f args'))
-> PartialResult sym ext (SimFrame sym ext f args)
-> f (PartialResult sym ext (SimFrame sym ext f args'))
forall sym ext u v (f :: Type -> Type).
Functor f =>
(GlobalPair sym u -> f (GlobalPair sym v))
-> PartialResult sym ext u -> f (PartialResult sym ext v)
partialValue
{-# INLINE actFrame #-}

-- | Return the call stack of all active frames, in
--   reverse activation order (i.e., with callees
--   appearing before callers).
activeFrames :: ActiveTree ctx sym ext root a args ->
                [SomeFrame (SimFrame sym ext)]
activeFrames :: forall ctx sym ext root a (args :: Maybe (Ctx CrucibleType)).
ActiveTree ctx sym ext root a args
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
activeFrames (ActiveTree ValueFromFrame ctx sym ext root a
ctx PartialResultFrame sym ext a args
ar) =
  SimFrame sym ext a args
-> SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
forall fk argk (f :: fk -> argk -> Type) (l :: fk) (a :: argk).
f l a -> SomeFrame @fk @argk f
SomeFrame (PartialResultFrame sym ext a args
arPartialResultFrame sym ext a args
-> Getting
     (GlobalPair sym (SimFrame sym ext a args))
     (PartialResultFrame sym ext a args)
     (GlobalPair sym (SimFrame sym ext a args))
-> GlobalPair sym (SimFrame sym ext a args)
forall s a. s -> Getting a s a -> a
^.Getting
  (GlobalPair sym (SimFrame sym ext a args))
  (PartialResultFrame sym ext a args)
  (GlobalPair sym (SimFrame sym ext a args))
forall sym ext u v (f :: Type -> Type).
Functor f =>
(GlobalPair sym u -> f (GlobalPair sym v))
-> PartialResult sym ext u -> f (PartialResult sym ext v)
partialValueGlobalPair sym (SimFrame sym ext a args)
-> Getting
     (SimFrame sym ext a args)
     (GlobalPair sym (SimFrame sym ext a args))
     (SimFrame sym ext a args)
-> SimFrame sym ext a args
forall s a. s -> Getting a s a -> a
^.Getting
  (SimFrame sym ext a args)
  (GlobalPair sym (SimFrame sym ext a args))
  (SimFrame sym ext a args)
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue) SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall a. a -> [a] -> [a]
: ValueFromFrame ctx sym ext root a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
forall p sym ext r a.
ValueFromFrame p sym ext r a
-> [SomeFrame @Type @(Maybe (Ctx CrucibleType)) (SimFrame sym ext)]
parentFrames ValueFromFrame ctx sym ext root a
ctx


------------------------------------------------------------------------
-- SimContext

-- | A definition of a function's semantics, given as a Haskell action.
data Override p sym ext (args :: Ctx CrucibleType) ret
   = Override { forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
Override p sym ext args ret -> FunctionName
overrideName    :: FunctionName
              , forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
Override p sym ext args ret
-> forall r.
   ExecCont
     p sym ext r (OverrideLang ret) ('Just @(Ctx CrucibleType) args)
overrideHandler :: forall r. ExecCont p sym ext r (OverrideLang ret) ('Just args)
              }

-- | State used to indicate what to do when function is called.  A function
--   may either be defined by writing a Haskell 'Override' or by giving
--   a Crucible control-flow graph representation.
data FnState p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType)
   = UseOverride !(Override p sym ext args ret)
   | forall blocks . UseCFG !(CFG ext blocks args ret) !(CFGPostdom blocks)

-- | A map from function handles to their semantics.
newtype FunctionBindings p sym ext = FnBindings { forall p sym ext.
FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
fnBindings :: FnHandleMap (FnState p sym ext) }

-- | The type of functions that interpret extension statements.  These
--   have access to the main simulator state, and can make fairly arbitrary
--   changes to it.
type EvalStmtFunc p sym ext =
  forall rtp blocks r ctx tp'.
    StmtExtension ext (RegEntry sym) tp' ->
    CrucibleState p sym ext rtp blocks r ctx ->
    IO (RegValue sym tp', CrucibleState p sym ext rtp blocks r ctx)

-- | In order to start executing a simulator, one must provide an implementation
--   of the extension syntax.  This includes an evaluator for the added
--   expression forms, and an evaluator for the added statement forms.
data ExtensionImpl p sym ext
  = ExtensionImpl
    { forall p sym ext.
ExtensionImpl p sym ext
-> forall bak rtp (blocks :: Ctx (Ctx CrucibleType))
          (r :: CrucibleType) (ctx :: Ctx CrucibleType).
   IsSymBackend sym bak =>
   bak
   -> IntrinsicTypes sym
   -> (Int -> String -> IO ())
   -> CrucibleState p sym ext rtp blocks r ctx
   -> EvalAppFunc sym (ExprExtension ext)
extensionEval ::
        forall bak rtp blocks r ctx.
        IsSymBackend sym bak =>
        bak ->
        IntrinsicTypes sym ->
        (Int -> String -> IO ()) ->
        CrucibleState p sym ext rtp blocks r ctx ->
        EvalAppFunc sym (ExprExtension ext)

    , forall p sym ext. ExtensionImpl p sym ext -> EvalStmtFunc p sym ext
extensionExec :: EvalStmtFunc p sym ext
    }

-- | Trivial implementation for the "empty" extension, which adds no
--   additional syntactic forms.
emptyExtensionImpl :: ExtensionImpl p sym ()
emptyExtensionImpl :: forall p sym. ExtensionImpl p sym ()
emptyExtensionImpl =
  ExtensionImpl
  { extensionEval :: forall bak rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (ctx :: Ctx CrucibleType).
IsSymBackend sym bak =>
bak
-> IntrinsicTypes sym
-> (Int -> String -> IO ())
-> CrucibleState p sym () rtp blocks r ctx
-> EvalAppFunc sym (ExprExtension ())
extensionEval = \bak
_sym IntrinsicTypes sym
_iTypes Int -> String -> IO ()
_log CrucibleState p sym () rtp blocks r ctx
_f forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
_state -> ExprExtension () f tp -> IO (RegValue sym tp)
\case
  , extensionExec :: EvalStmtFunc p sym ()
extensionExec = StmtExtension () (RegEntry sym) tp'
-> CrucibleState p sym () rtp blocks r ctx
-> IO (RegValue sym tp', CrucibleState p sym () rtp blocks r ctx)
EvalStmtFunc p sym ()
\case
  }

type IsSymInterfaceProof sym a = (IsSymInterface sym => a) -> a

newtype Metric p sym ext =
  Metric {
    forall p sym ext.
Metric p sym ext
-> forall rtp f (args :: Maybe (Ctx CrucibleType)).
   SimState p sym ext rtp f args -> IO Integer
runMetric :: forall rtp f args. SimState p sym ext rtp f args -> IO Integer
  }

-- | Top-level state record for the simulator.  The state contained in this record
--   remains persistent across all symbolic simulator actions.  In particular, it
--   is not rolled back when the simulator returns previous program points to
--   explore additional paths, etc.
data SimContext (personality :: Type) (sym :: Type) (ext :: Type)
   = SimContext { forall personality sym ext.
SimContext personality sym ext -> SomeBackend sym
_ctxBackend            :: !(SomeBackend sym)
                  -- | Class dictionary for @'IsSymInterface' sym@
                , forall personality sym ext.
SimContext personality sym ext
-> forall a. IsSymInterfaceProof sym a
ctxSolverProof         :: !(forall a . IsSymInterfaceProof sym a)
                , forall personality sym ext.
SimContext personality sym ext -> IntrinsicTypes sym
ctxIntrinsicTypes      :: !(IntrinsicTypes sym)
                  -- | Allocator for function handles
                , forall personality sym ext.
SimContext personality sym ext -> HandleAllocator
simHandleAllocator     :: !(HandleAllocator)
                  -- | Handle to write messages to.
                , forall personality sym ext.
SimContext personality sym ext -> Handle
printHandle            :: !Handle
                , forall personality sym ext.
SimContext personality sym ext -> ExtensionImpl personality sym ext
extensionImpl          :: ExtensionImpl personality sym ext
                , forall personality sym ext.
SimContext personality sym ext
-> FunctionBindings personality sym ext
_functionBindings      :: !(FunctionBindings personality sym ext)
                , forall personality sym ext.
SimContext personality sym ext -> personality
_cruciblePersonality   :: !personality
                , forall personality sym ext.
SimContext personality sym ext
-> Map Text (Metric personality sym ext)
_profilingMetrics      :: !(Map Text (Metric personality sym ext))
                }

-- | Create a new 'SimContext' with the given bindings.
initSimContext ::
  IsSymBackend sym bak =>
  bak {- ^ Symbolic backend -} ->
  IntrinsicTypes sym {- ^ Implementations of intrinsic types -} ->
  HandleAllocator {- ^ Handle allocator for creating new function handles -} ->
  Handle {- ^ Handle to write output to -} ->
  FunctionBindings personality sym ext {- ^ Initial bindings for function handles -} ->
  ExtensionImpl personality sym ext {- ^ Semantics for extension syntax -} ->
  personality {- ^ Initial value for custom user state -} ->
  SimContext personality sym ext
initSimContext :: forall sym bak personality ext.
IsSymBackend sym bak =>
bak
-> IntrinsicTypes sym
-> HandleAllocator
-> Handle
-> FunctionBindings personality sym ext
-> ExtensionImpl personality sym ext
-> personality
-> SimContext personality sym ext
initSimContext bak
bak IntrinsicTypes sym
muxFns HandleAllocator
halloc Handle
h FunctionBindings personality sym ext
bindings ExtensionImpl personality sym ext
extImpl personality
personality =
  SimContext { _ctxBackend :: SomeBackend sym
_ctxBackend          = bak -> SomeBackend sym
forall sym bak. IsSymBackend sym bak => bak -> SomeBackend sym
SomeBackend bak
bak
             , ctxSolverProof :: forall a. IsSymInterfaceProof sym a
ctxSolverProof       = \IsSymInterface sym => a
a -> a
IsSymInterface sym => a
a
             , ctxIntrinsicTypes :: IntrinsicTypes sym
ctxIntrinsicTypes    = IntrinsicTypes sym
muxFns
             , simHandleAllocator :: HandleAllocator
simHandleAllocator   = HandleAllocator
halloc
             , printHandle :: Handle
printHandle          = Handle
h
             , extensionImpl :: ExtensionImpl personality sym ext
extensionImpl        = ExtensionImpl personality sym ext
extImpl
             , _functionBindings :: FunctionBindings personality sym ext
_functionBindings    = FunctionBindings personality sym ext
bindings
             , _cruciblePersonality :: personality
_cruciblePersonality = personality
personality
             , _profilingMetrics :: Map Text (Metric personality sym ext)
_profilingMetrics    = Map Text (Metric personality sym ext)
forall k a. Map k a
Map.empty
             }

withBackend ::
  SimContext personality sym ext ->
  (forall bak. IsSymBackend sym bak => bak -> a) ->
  a
withBackend :: forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend SimContext personality sym ext
ctx forall bak. IsSymBackend sym bak => bak -> a
f = case SimContext personality sym ext -> SomeBackend sym
forall personality sym ext.
SimContext personality sym ext -> SomeBackend sym
_ctxBackend SimContext personality sym ext
ctx of SomeBackend bak
bak -> bak -> a
forall bak. IsSymBackend sym bak => bak -> a
f bak
bak

-- | Access the symbolic backend inside a 'SimContext'.
ctxSymInterface :: Getter (SimContext p sym ext) sym
ctxSymInterface :: forall p sym ext (f :: Type -> Type).
(Contravariant f, Functor f) =>
(sym -> f sym) -> SimContext p sym ext -> f (SimContext p sym ext)
ctxSymInterface = (SimContext p sym ext -> sym)
-> (sym -> f sym)
-> SimContext p sym ext
-> f (SimContext p sym ext)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' @Type @Type p f s a
to (\SimContext p sym ext
ctx ->
  case SimContext p sym ext -> SomeBackend sym
forall personality sym ext.
SimContext personality sym ext -> SomeBackend sym
_ctxBackend SimContext p sym ext
ctx of
    SomeBackend bak
bak -> bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak)

-- | A map from function handles to their semantics.
functionBindings :: Lens' (SimContext p sym ext) (FunctionBindings p sym ext)
functionBindings :: forall p sym ext (f :: Type -> Type).
Functor f =>
(FunctionBindings p sym ext -> f (FunctionBindings p sym ext))
-> SimContext p sym ext -> f (SimContext p sym ext)
functionBindings = (SimContext p sym ext -> FunctionBindings p sym ext)
-> (SimContext p sym ext
    -> FunctionBindings p sym ext -> SimContext p sym ext)
-> Lens
     (SimContext p sym ext)
     (SimContext p sym ext)
     (FunctionBindings p sym ext)
     (FunctionBindings p sym ext)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens SimContext p sym ext -> FunctionBindings p sym ext
forall personality sym ext.
SimContext personality sym ext
-> FunctionBindings personality sym ext
_functionBindings (\SimContext p sym ext
s FunctionBindings p sym ext
v -> SimContext p sym ext
s { _functionBindings = v })

-- | Access the custom user-state inside the 'SimContext'.
cruciblePersonality :: Lens' (SimContext p sym ext) p
cruciblePersonality :: forall p sym ext (f :: Type -> Type).
Functor f =>
(p -> f p) -> SimContext p sym ext -> f (SimContext p sym ext)
cruciblePersonality = (SimContext p sym ext -> p)
-> (SimContext p sym ext -> p -> SimContext p sym ext)
-> Lens (SimContext p sym ext) (SimContext p sym ext) p p
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens SimContext p sym ext -> p
forall personality sym ext.
SimContext personality sym ext -> personality
_cruciblePersonality (\SimContext p sym ext
s p
v -> SimContext p sym ext
s{ _cruciblePersonality = v })

profilingMetrics :: Lens' (SimContext p sym ext) (Map Text (Metric p sym ext))
profilingMetrics :: forall p sym ext (f :: Type -> Type).
Functor f =>
(Map Text (Metric p sym ext) -> f (Map Text (Metric p sym ext)))
-> SimContext p sym ext -> f (SimContext p sym ext)
profilingMetrics = (SimContext p sym ext -> Map Text (Metric p sym ext))
-> (SimContext p sym ext
    -> Map Text (Metric p sym ext) -> SimContext p sym ext)
-> Lens
     (SimContext p sym ext)
     (SimContext p sym ext)
     (Map Text (Metric p sym ext))
     (Map Text (Metric p sym ext))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens SimContext p sym ext -> Map Text (Metric p sym ext)
forall personality sym ext.
SimContext personality sym ext
-> Map Text (Metric personality sym ext)
_profilingMetrics (\SimContext p sym ext
s Map Text (Metric p sym ext)
v -> SimContext p sym ext
s { _profilingMetrics = v })

------------------------------------------------------------------------
-- SimState


-- | An abort handler indicates to the simulator what actions to take
--   when an abort occurs.  Usually, one should simply use the
--   'defaultAbortHandler' from "Lang.Crucible.Simulator", which
--   unwinds the tree context to the nearest branch point and
--   correctly resumes simulation.  However, for some use cases, it
--   may be desirable to take additional or alternate actions on abort
--   events; in which case, the library user may replace the default
--   abort handler with their own.
newtype AbortHandler p sym ext rtp
      = AH { forall p sym ext rtp.
AbortHandler p sym ext rtp
-> forall l (args :: Maybe (Ctx CrucibleType)).
   AbortExecReason -> ExecCont p sym ext rtp l args
runAH :: forall (l :: Type) args.
                 AbortExecReason ->
                 ExecCont p sym ext rtp l args
           }

-- | A SimState contains the execution context, an error handler, and
--   the current execution tree.  It captures the entire state
--   of the symbolic simulator.
data SimState p sym ext rtp f (args :: Maybe (Ctx.Ctx CrucibleType))
   = SimState { forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SimContext p sym ext
_stateContext      :: !(SimContext p sym ext)
              , forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> AbortHandler p sym ext rtp
_abortHandler      :: !(AbortHandler p sym ext rtp)
              , forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> ActiveTree p sym ext rtp f args
_stateTree         :: !(ActiveTree p sym ext rtp f args)
              }

data SomeSimState p sym ext rtp =
  forall f args. SomeSimState !(SimState p sym ext rtp f args)

-- | A simulator state that is currently executing Crucible instructions.
type CrucibleState p sym ext rtp blocks ret args
   = SimState p sym ext rtp (CrucibleLang blocks ret) ('Just args)

-- | Create an initial 'SimState'
initSimState ::
  SimContext p sym ext {- ^ initial 'SimContext' state -} ->
  SymGlobalState sym  {- ^ state of Crucible global variables -} ->
  AbortHandler p sym ext (RegEntry sym ret) {- ^ initial abort handler -} ->
  TypeRepr ret ->
  IO (SimState p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx))
initSimState :: forall p sym ext (ret :: CrucibleType).
SimContext p sym ext
-> SymGlobalState sym
-> AbortHandler p sym ext (RegEntry sym ret)
-> TypeRepr ret
-> IO
     (SimState
        p
        sym
        ext
        (RegEntry sym ret)
        (OverrideLang ret)
        ('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType)))
initSimState SimContext p sym ext
ctx SymGlobalState sym
globals AbortHandler p sym ext (RegEntry sym ret)
ah TypeRepr ret
ret =
  do let halloc :: HandleAllocator
halloc = SimContext p sym ext -> HandleAllocator
forall personality sym ext.
SimContext personality sym ext -> HandleAllocator
simHandleAllocator SimContext p sym ext
ctx
     FnHandle (EmptyCtx @CrucibleType) ret
h <- HandleAllocator
-> FunctionName
-> Assignment @CrucibleType TypeRepr (EmptyCtx @CrucibleType)
-> TypeRepr ret
-> IO (FnHandle (EmptyCtx @CrucibleType) ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
HandleAllocator
-> FunctionName
-> Assignment @CrucibleType TypeRepr args
-> TypeRepr ret
-> IO (FnHandle args ret)
mkHandle' HandleAllocator
halloc FunctionName
startFunctionName Assignment @CrucibleType TypeRepr (EmptyCtx @CrucibleType)
forall {k} (ctx :: Ctx k) (f :: k -> Type).
((ctx :: Ctx k) ~ (EmptyCtx @k :: Ctx k)) =>
Assignment @k f ctx
Ctx.Empty TypeRepr ret
ret
     let startFrame :: OverrideFrame sym ret (EmptyCtx @CrucibleType)
startFrame = OverrideFrame { _override :: FunctionName
_override = FunctionName
startFunctionName
                                    , _overrideHandle :: SomeHandle
_overrideHandle = FnHandle (EmptyCtx @CrucibleType) ret -> SomeHandle
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> SomeHandle
SomeHandle FnHandle (EmptyCtx @CrucibleType) ret
h
                                    , _overrideRegMap :: RegMap sym (EmptyCtx @CrucibleType)
_overrideRegMap = RegMap sym (EmptyCtx @CrucibleType)
forall sym. RegMap sym (EmptyCtx @CrucibleType)
emptyRegMap
                                    }
     let startGP :: GlobalPair
  sym
  (SimFrame
     sym
     ext
     (OverrideLang ret)
     ('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType)))
startGP = SimFrame
  sym
  ext
  (OverrideLang ret)
  ('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType))
-> SymGlobalState sym
-> GlobalPair
     sym
     (SimFrame
        sym
        ext
        (OverrideLang ret)
        ('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType)))
forall sym v. v -> SymGlobalState sym -> GlobalPair sym v
GlobalPair (OverrideFrame sym ret (EmptyCtx @CrucibleType)
-> SimFrame
     sym
     ext
     (OverrideLang ret)
     ('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType))
forall sym (ret :: CrucibleType) (args1 :: Ctx CrucibleType) ext.
OverrideFrame sym ret args1
-> SimFrame
     sym ext (OverrideLang ret) ('Just @(Ctx CrucibleType) args1)
OF OverrideFrame sym ret (EmptyCtx @CrucibleType)
startFrame) SymGlobalState sym
globals
     SimState
  p
  sym
  ext
  (RegEntry sym ret)
  (OverrideLang ret)
  ('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType))
-> IO
     (SimState
        p
        sym
        ext
        (RegEntry sym ret)
        (OverrideLang ret)
        ('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType)))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return
       SimState
       { _stateContext :: SimContext p sym ext
_stateContext = SimContext p sym ext
ctx
       , _abortHandler :: AbortHandler p sym ext (RegEntry sym ret)
_abortHandler = AbortHandler p sym ext (RegEntry sym ret)
ah
       , _stateTree :: ActiveTree
  p
  sym
  ext
  (RegEntry sym ret)
  (OverrideLang ret)
  ('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType))
_stateTree    = GlobalPair
  sym
  (SimFrame
     sym
     ext
     (OverrideLang ret)
     ('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType)))
-> ActiveTree
     p
     sym
     ext
     (RegEntry sym (FrameRetType (OverrideLang ret)))
     (OverrideLang ret)
     ('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType))
forall sym ext f (args :: Maybe (Ctx CrucibleType)) p.
TopFrame sym ext f args
-> ActiveTree p sym ext (RegEntry sym (FrameRetType f)) f args
singletonTree GlobalPair
  sym
  (SimFrame
     sym
     ext
     (OverrideLang ret)
     ('Just @(Ctx CrucibleType) (EmptyCtx @CrucibleType)))
startGP
       }


stateLocation :: Getter (SimState p sym ext r f a) (Maybe ProgramLoc)
stateLocation :: forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
(Contravariant f, Functor f) =>
(Maybe ProgramLoc -> f (Maybe ProgramLoc))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateLocation = (SimState p sym ext r f a -> Maybe ProgramLoc)
-> (Maybe ProgramLoc -> f (Maybe ProgramLoc))
-> SimState p sym ext r f a
-> f (SimState p sym ext r f a)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' @Type @Type p f s a
to SimState p sym ext r f a -> Maybe ProgramLoc
forall p sym ext r f (a :: Maybe (Ctx CrucibleType)).
SimState p sym ext r f a -> Maybe ProgramLoc
f
 where
 f :: SimState p sym ext r f a -> Maybe ProgramLoc
 f :: forall p sym ext r f (a :: Maybe (Ctx CrucibleType)).
SimState p sym ext r f a -> Maybe ProgramLoc
f SimState p sym ext r f a
st = case SimState p sym ext r f a
stSimState p sym ext r f a
-> Getting
     (SimFrame sym ext f a)
     (SimState p sym ext r f a)
     (SimFrame sym ext f a)
-> SimFrame sym ext f a
forall s a. s -> Getting a s a -> a
^.(ActiveTree p sym ext r f a
 -> Const @Type (SimFrame sym ext f a) (ActiveTree p sym ext r f a))
-> SimState p sym ext r f a
-> Const @Type (SimFrame sym ext f a) (SimState p sym ext r f a)
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(ActiveTree p sym ext rtp f a -> f (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f a -> f (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext r f a
  -> Const @Type (SimFrame sym ext f a) (ActiveTree p sym ext r f a))
 -> SimState p sym ext r f a
 -> Const @Type (SimFrame sym ext f a) (SimState p sym ext r f a))
-> ((SimFrame sym ext f a
     -> Const @Type (SimFrame sym ext f a) (SimFrame sym ext f a))
    -> ActiveTree p sym ext r f a
    -> Const @Type (SimFrame sym ext f a) (ActiveTree p sym ext r f a))
-> Getting
     (SimFrame sym ext f a)
     (SimState p sym ext r f a)
     (SimFrame sym ext f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext f a
 -> Const @Type (SimFrame sym ext f a) (TopFrame sym ext f a))
-> ActiveTree p sym ext r f a
-> Const @Type (SimFrame sym ext f a) (ActiveTree p sym ext r f a)
forall p sym ext root f (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(TopFrame sym ext f args -> f (TopFrame sym ext f args'))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args')
actFrame ((TopFrame sym ext f a
  -> Const @Type (SimFrame sym ext f a) (TopFrame sym ext f a))
 -> ActiveTree p sym ext r f a
 -> Const @Type (SimFrame sym ext f a) (ActiveTree p sym ext r f a))
-> ((SimFrame sym ext f a
     -> Const @Type (SimFrame sym ext f a) (SimFrame sym ext f a))
    -> TopFrame sym ext f a
    -> Const @Type (SimFrame sym ext f a) (TopFrame sym ext f a))
-> (SimFrame sym ext f a
    -> Const @Type (SimFrame sym ext f a) (SimFrame sym ext f a))
-> ActiveTree p sym ext r f a
-> Const @Type (SimFrame sym ext f a) (ActiveTree p sym ext r f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimFrame sym ext f a
 -> Const @Type (SimFrame sym ext f a) (SimFrame sym ext f a))
-> TopFrame sym ext f a
-> Const @Type (SimFrame sym ext f a) (TopFrame sym ext f a)
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue of
          MF CallFrame sym ext blocks ret args1
cf -> ProgramLoc -> Maybe ProgramLoc
forall a. a -> Maybe a
Just (ProgramLoc -> Maybe ProgramLoc) -> ProgramLoc -> Maybe ProgramLoc
forall a b. (a -> b) -> a -> b
$! (CallFrame sym ext blocks ret args1 -> ProgramLoc
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> ProgramLoc
frameProgramLoc CallFrame sym ext blocks ret args1
cf)
          OF OverrideFrame sym ret args1
_ -> Maybe ProgramLoc
forall a. Maybe a
Nothing
          RF FunctionName
_ RegEntry sym (FrameRetType f)
_ -> Maybe ProgramLoc
forall a. Maybe a
Nothing


-- | Access the 'SimContext' inside a 'SimState'
stateContext :: Simple Lens (SimState p sym ext r f a) (SimContext p sym ext)
stateContext :: forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext = (SimState p sym ext r f a -> SimContext p sym ext)
-> (SimState p sym ext r f a
    -> SimContext p sym ext -> SimState p sym ext r f a)
-> Lens
     (SimState p sym ext r f a)
     (SimState p sym ext r f a)
     (SimContext p sym ext)
     (SimContext p sym ext)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens SimState p sym ext r f a -> SimContext p sym ext
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SimContext p sym ext
_stateContext (\SimState p sym ext r f a
s SimContext p sym ext
v -> SimState p sym ext r f a
s { _stateContext = v })
{-# INLINE stateContext #-}

-- | Access the current abort handler of a state.
abortHandler :: Simple Lens (SimState p sym ext r f a) (AbortHandler p sym ext r)
abortHandler :: forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(AbortHandler p sym ext r -> f (AbortHandler p sym ext r))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
abortHandler = (SimState p sym ext r f a -> AbortHandler p sym ext r)
-> (SimState p sym ext r f a
    -> AbortHandler p sym ext r -> SimState p sym ext r f a)
-> Lens
     (SimState p sym ext r f a)
     (SimState p sym ext r f a)
     (AbortHandler p sym ext r)
     (AbortHandler p sym ext r)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens SimState p sym ext r f a -> AbortHandler p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> AbortHandler p sym ext rtp
_abortHandler (\SimState p sym ext r f a
s AbortHandler p sym ext r
v -> SimState p sym ext r f a
s { _abortHandler = v })

-- | Access the active tree associated with a state.
stateTree ::
  Lens (SimState p sym ext rtp f a)
       (SimState p sym ext rtp g b)
       (ActiveTree p sym ext rtp f a)
       (ActiveTree p sym ext rtp g b)
stateTree :: forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(ActiveTree p sym ext rtp f a -> f (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f a -> f (SimState p sym ext rtp g b)
stateTree = (SimState p sym ext rtp f a -> ActiveTree p sym ext rtp f a)
-> (SimState p sym ext rtp f a
    -> ActiveTree p sym ext rtp g b -> SimState p sym ext rtp g b)
-> Lens
     (SimState p sym ext rtp f a)
     (SimState p sym ext rtp g b)
     (ActiveTree p sym ext rtp f a)
     (ActiveTree p sym ext rtp g b)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens SimState p sym ext rtp f a -> ActiveTree p sym ext rtp f a
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> ActiveTree p sym ext rtp f args
_stateTree (\SimState p sym ext rtp f a
s ActiveTree p sym ext rtp g b
v -> SimState p sym ext rtp f a
s { _stateTree = v })
{-# INLINE stateTree #-}

-- | Access the Crucible call frame inside a 'SimState'
stateCrucibleFrame ::
  Lens (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a))
       (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
       (CallFrame sym ext blocks r a)
       (CallFrame sym ext blocks r a')
stateCrucibleFrame :: 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 @(Ctx CrucibleType) a)
-> f (SimState
        p
        sym
        ext
        rtp
        (CrucibleLang blocks r)
        ('Just @(Ctx CrucibleType) a'))
stateCrucibleFrame = (ActiveTree
   p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
 -> f (ActiveTree
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just @(Ctx CrucibleType) a')))
-> SimState
     p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (SimState
        p
        sym
        ext
        rtp
        (CrucibleLang blocks r)
        ('Just @(Ctx CrucibleType) a'))
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(ActiveTree p sym ext rtp f a -> f (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f a -> f (SimState p sym ext rtp g b)
stateTree ((ActiveTree
    p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
  -> f (ActiveTree
          p
          sym
          ext
          rtp
          (CrucibleLang blocks r)
          ('Just @(Ctx CrucibleType) a')))
 -> SimState
      p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
 -> f (SimState
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just @(Ctx CrucibleType) a')))
-> ((CallFrame sym ext blocks r a
     -> f (CallFrame sym ext blocks r a'))
    -> ActiveTree
         p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
    -> f (ActiveTree
            p
            sym
            ext
            rtp
            (CrucibleLang blocks r)
            ('Just @(Ctx CrucibleType) a')))
-> (CallFrame sym ext blocks r a
    -> f (CallFrame sym ext blocks r a'))
-> SimState
     p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (SimState
        p
        sym
        ext
        rtp
        (CrucibleLang blocks r)
        ('Just @(Ctx CrucibleType) a'))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame
   sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
 -> f (TopFrame
         sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a')))
-> ActiveTree
     p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (ActiveTree
        p
        sym
        ext
        rtp
        (CrucibleLang blocks r)
        ('Just @(Ctx CrucibleType) a'))
forall p sym ext root f (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(TopFrame sym ext f args -> f (TopFrame sym ext f args'))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args')
actFrame ((TopFrame
    sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
  -> f (TopFrame
          sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a')))
 -> ActiveTree
      p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
 -> f (ActiveTree
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just @(Ctx CrucibleType) a')))
-> ((CallFrame sym ext blocks r a
     -> f (CallFrame sym ext blocks r a'))
    -> TopFrame
         sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
    -> f (TopFrame
            sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a')))
-> (CallFrame sym ext blocks r a
    -> f (CallFrame sym ext blocks r a'))
-> ActiveTree
     p sym ext rtp (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (ActiveTree
        p
        sym
        ext
        rtp
        (CrucibleLang blocks r)
        ('Just @(Ctx CrucibleType) a'))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> TopFrame
     sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a)
-> f (TopFrame
        sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) a'))
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r args
 -> f (CallFrame sym ext blocks r args'))
-> TopFrame
     sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args)
-> f (TopFrame
        sym ext (CrucibleLang blocks r) ('Just @(Ctx CrucibleType) args'))
crucibleTopFrame
{-# INLINE stateCrucibleFrame #-}

-- | Access the override frame inside a 'SimState'
stateOverrideFrame ::
  Lens
     (SimState p sym ext q (OverrideLang r) ('Just a))
     (SimState p sym ext q (OverrideLang r) ('Just a'))
     (OverrideFrame sym r a)
     (OverrideFrame sym r a')
stateOverrideFrame :: forall p sym ext q (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(OverrideFrame sym r a -> f (OverrideFrame sym r a'))
-> SimState
     p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (SimState
        p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a'))
stateOverrideFrame = (ActiveTree
   p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
 -> f (ActiveTree
         p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> SimState
     p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (SimState
        p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a'))
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(ActiveTree p sym ext rtp f a -> f (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f a -> f (SimState p sym ext rtp g b)
stateTree ((ActiveTree
    p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
  -> f (ActiveTree
          p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
 -> SimState
      p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
 -> f (SimState
         p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> ((OverrideFrame sym r a -> f (OverrideFrame sym r a'))
    -> ActiveTree
         p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
    -> f (ActiveTree
            p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> (OverrideFrame sym r a -> f (OverrideFrame sym r a'))
-> SimState
     p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (SimState
        p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a'))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
 -> f (TopFrame
         sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> ActiveTree
     p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (ActiveTree
        p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a'))
forall p sym ext root f (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(TopFrame sym ext f args -> f (TopFrame sym ext f args'))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args')
actFrame ((TopFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
  -> f (TopFrame
          sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
 -> ActiveTree
      p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
 -> f (ActiveTree
         p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> ((OverrideFrame sym r a -> f (OverrideFrame sym r a'))
    -> TopFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
    -> f (TopFrame
            sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> (OverrideFrame sym r a -> f (OverrideFrame sym r a'))
-> ActiveTree
     p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (ActiveTree
        p sym ext q (OverrideLang r) ('Just @(Ctx CrucibleType) a'))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
 -> f (SimFrame
         sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> TopFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (TopFrame
        sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a'))
forall sym u v (f :: Type -> Type).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue ((SimFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
  -> f (SimFrame
          sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
 -> TopFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
 -> f (TopFrame
         sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> ((OverrideFrame sym r a -> f (OverrideFrame sym r a'))
    -> SimFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
    -> f (SimFrame
            sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a')))
-> (OverrideFrame sym r a -> f (OverrideFrame sym r a'))
-> TopFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (TopFrame
        sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a'))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OverrideFrame sym r a -> f (OverrideFrame sym r a'))
-> SimFrame sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a)
-> f (SimFrame
        sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) a'))
forall sym ext (r :: CrucibleType) (args :: Ctx CrucibleType)
       (r' :: CrucibleType) (args' :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> SimFrame
     sym ext (OverrideLang r) ('Just @(Ctx CrucibleType) args)
-> f (SimFrame
        sym ext (OverrideLang r') ('Just @(Ctx CrucibleType) args'))
overrideSimFrame

-- | Access the globals inside a 'SimState'
stateGlobals :: Simple Lens (SimState p sym ext q f args) (SymGlobalState sym)
stateGlobals :: forall p sym ext q f (args :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> SimState p sym ext q f args -> f (SimState p sym ext q f args)
stateGlobals = (ActiveTree p sym ext q f args
 -> f (ActiveTree p sym ext q f args))
-> SimState p sym ext q f args -> f (SimState p sym ext q f args)
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(ActiveTree p sym ext rtp f a -> f (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f a -> f (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext q f args
  -> f (ActiveTree p sym ext q f args))
 -> SimState p sym ext q f args -> f (SimState p sym ext q f args))
-> ((SymGlobalState sym -> f (SymGlobalState sym))
    -> ActiveTree p sym ext q f args
    -> f (ActiveTree p sym ext q f args))
-> (SymGlobalState sym -> f (SymGlobalState sym))
-> SimState p sym ext q f args
-> f (SimState p sym ext q f args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext f args -> f (TopFrame sym ext f args))
-> ActiveTree p sym ext q f args
-> f (ActiveTree p sym ext q f args)
forall p sym ext root f (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f :: Type -> Type).
Functor f =>
(TopFrame sym ext f args -> f (TopFrame sym ext f args'))
-> ActiveTree p sym ext root f args
-> f (ActiveTree p sym ext root f args')
actFrame ((TopFrame sym ext f args -> f (TopFrame sym ext f args))
 -> ActiveTree p sym ext q f args
 -> f (ActiveTree p sym ext q f args))
-> ((SymGlobalState sym -> f (SymGlobalState sym))
    -> TopFrame sym ext f args -> f (TopFrame sym ext f args))
-> (SymGlobalState sym -> f (SymGlobalState sym))
-> ActiveTree p sym ext q f args
-> f (ActiveTree p sym ext q f args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymGlobalState sym -> f (SymGlobalState sym))
-> TopFrame sym ext f args -> f (TopFrame sym ext f args)
forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals

-- | Get the symbolic interface out of a 'SimState'
stateSymInterface :: Getter (SimState p sym ext r f a) sym
stateSymInterface :: forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
(Contravariant f, Functor f) =>
(sym -> f sym)
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateSymInterface = (SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext ((SimContext p sym ext -> f (SimContext p sym ext))
 -> SimState p sym ext r f a -> f (SimState p sym ext r f a))
-> ((sym -> f sym)
    -> SimContext p sym ext -> f (SimContext p sym ext))
-> (sym -> f sym)
-> SimState p sym ext r f a
-> f (SimState p sym ext r f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (sym -> f sym) -> SimContext p sym ext -> f (SimContext p sym ext)
forall p sym ext (f :: Type -> Type).
(Contravariant f, Functor f) =>
(sym -> f sym) -> SimContext p sym ext -> f (SimContext p sym ext)
ctxSymInterface

-- | Get the intrinsic type map out of a 'SimState'
stateIntrinsicTypes :: Getter (SimState p sym ext r f args) (IntrinsicTypes sym)
stateIntrinsicTypes :: forall p sym ext r f (args :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
(Contravariant f, Functor f) =>
(IntrinsicTypes sym -> f (IntrinsicTypes sym))
-> SimState p sym ext r f args -> f (SimState p sym ext r f args)
stateIntrinsicTypes = (SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f args -> f (SimState p sym ext r f args)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext ((SimContext p sym ext -> f (SimContext p sym ext))
 -> SimState p sym ext r f args -> f (SimState p sym ext r f args))
-> ((IntrinsicTypes sym -> f (IntrinsicTypes sym))
    -> SimContext p sym ext -> f (SimContext p sym ext))
-> (IntrinsicTypes sym -> f (IntrinsicTypes sym))
-> SimState p sym ext r f args
-> f (SimState p sym ext r f args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimContext p sym ext -> IntrinsicTypes sym)
-> (IntrinsicTypes sym -> f (IntrinsicTypes sym))
-> SimContext p sym ext
-> f (SimContext p sym ext)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' @Type @Type p f s a
to SimContext p sym ext -> IntrinsicTypes sym
forall personality sym ext.
SimContext personality sym ext -> IntrinsicTypes sym
ctxIntrinsicTypes

-- | Get the configuration object out of a 'SimState'
stateConfiguration :: Getter (SimState p sym ext r f args) Config
stateConfiguration :: forall p sym ext r f (args :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
(Contravariant f, Functor f) =>
(Config -> f Config)
-> SimState p sym ext r f args -> f (SimState p sym ext r f args)
stateConfiguration = (SimState p sym ext r f args -> Config)
-> (Config -> f Config)
-> SimState p sym ext r f args
-> f (SimState p sym ext r f args)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' @Type @Type p f s a
to (\SimState p sym ext r f args
s -> SimState p sym ext r f args -> forall a. IsSymInterfaceProof sym a
forall p sym ext r f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext r f args -> forall a. IsSymInterfaceProof sym a
stateSolverProof SimState p sym ext r f args
s (sym -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration (SimState p sym ext r f args
sSimState p sym ext r f args
-> Getting sym (SimState p sym ext r f args) sym -> sym
forall s a. s -> Getting a s a -> a
^.Getting sym (SimState p sym ext r f args) sym
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
(Contravariant f, Functor f) =>
(sym -> f sym)
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateSymInterface)))

-- | Provide the 'IsSymInterface' typeclass dictionary from a 'SimState'
stateSolverProof :: SimState p sym ext r f args -> (forall a . IsSymInterfaceProof sym a)
stateSolverProof :: forall p sym ext r f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext r f args -> forall a. IsSymInterfaceProof sym a
stateSolverProof SimState p sym ext r f args
s = SimContext p sym ext -> forall a. IsSymInterfaceProof sym a
forall personality sym ext.
SimContext personality sym ext
-> forall a. IsSymInterfaceProof sym a
ctxSolverProof (SimState p sym ext r f args
sSimState p sym ext r f args
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext r f 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 r f args)
  (SimContext p sym ext)
forall p sym ext r f (a :: Maybe (Ctx CrucibleType))
       (f :: Type -> Type).
Functor f =>
(SimContext p sym ext -> f (SimContext p sym ext))
-> SimState p sym ext r f a -> f (SimState p sym ext r f a)
stateContext)