-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Simulator.EvalStmt
-- Description      : Provides functions for evaluating statements.
-- Copyright        : (c) Galois, Inc 2013-2018
-- License          : BSD3
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
--
-- This module provides functions for evaluating Crucible statements.
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.Simulator.EvalStmt
  ( -- * High-level evaluation
    singleStepCrucible
  , executeCrucible
  , ExecutionFeature(..)
  , GenericExecutionFeature(..)
  , ExecutionFeatureResult(..)
  , genericToExecutionFeature
  , timeoutFeature

    -- * Lower-level evaluation operations
  , dispatchExecState
  , advanceCrucibleState
  , evalReg
  , evalReg'
  , evalExpr
  , evalArgs
  , evalJumpTarget
  , evalSwitchTarget
  , stepStmt
  , stepTerm
  , stepBasicBlock
  , readRef
  , alterRef
  ) where

import qualified Control.Exception as Ex
import           Control.Lens
import           Control.Monad (foldM, when)
import           Control.Monad.IO.Class (MonadIO(..))
import           Control.Monad.Reader (ReaderT(..), withReaderT)
import           Data.Maybe (fromMaybe)
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.TraversableFC
import qualified Data.Text as Text
import           Data.Time.Clock
import           System.IO
import           System.IO.Error as Ex
import           Prettyprinter

import           What4.Config
import           What4.Interface
import           What4.InterpretedFloatingPoint (freshFloatConstant)
import           What4.Partial
import           What4.ProgramLoc

import           Lang.Crucible.Backend
import           Lang.Crucible.CFG.Core
import           Lang.Crucible.CFG.Extension
import           Lang.Crucible.FunctionHandle
import           Lang.Crucible.Simulator.CallFrame
import           Lang.Crucible.Simulator.Evaluation
import           Lang.Crucible.Simulator.ExecutionTree
import           Lang.Crucible.Simulator.Intrinsics (IntrinsicTypes)
import           Lang.Crucible.Simulator.GlobalState
import           Lang.Crucible.Simulator.Operations
import           Lang.Crucible.Simulator.RegMap
import           Lang.Crucible.Simulator.SimError
import           Lang.Crucible.Utils.MuxTree


-- | Retrieve the value of a register.
evalReg ::
  Monad m =>
  Reg ctx tp ->
  ReaderT (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg :: forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg Reg ctx tp
r = (RegMap sym ctx -> Reg ctx tp -> RegValue sym tp
forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
RegMap sym ctx -> Reg ctx tp -> RegValue sym tp
`regVal` Reg ctx tp
r) (RegMap sym ctx -> RegValue sym tp)
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym ctx)
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting
  (RegMap sym ctx)
  (CrucibleState p sym ext rtp blocks r ctx)
  (RegMap sym ctx)
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym ctx)
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view ((CallFrame sym ext blocks r ctx
 -> Const (RegMap sym ctx) (CallFrame sym ext blocks r ctx))
-> CrucibleState p sym ext rtp blocks r ctx
-> Const
     (RegMap sym ctx) (CrucibleState p sym ext rtp blocks r ctx)
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame((CallFrame sym ext blocks r ctx
  -> Const (RegMap sym ctx) (CallFrame sym ext blocks r ctx))
 -> CrucibleState p sym ext rtp blocks r ctx
 -> Const
      (RegMap sym ctx) (CrucibleState p sym ext rtp blocks r ctx))
-> ((RegMap sym ctx -> Const (RegMap sym ctx) (RegMap sym ctx))
    -> CallFrame sym ext blocks r ctx
    -> Const (RegMap sym ctx) (CallFrame sym ext blocks r ctx))
-> Getting
     (RegMap sym ctx)
     (CrucibleState p sym ext rtp blocks r ctx)
     (RegMap sym ctx)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(RegMap sym ctx -> Const (RegMap sym ctx) (RegMap sym ctx))
-> CallFrame sym ext blocks r ctx
-> Const (RegMap sym ctx) (CallFrame sym ext blocks r ctx)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args))
-> CallFrame sym ext blocks ret args
-> f (CallFrame sym ext blocks ret args)
frameRegs)

-- | Retrieve the value of a register, returning a 'RegEntry'.
evalReg' ::
  Monad m =>
  Reg ctx tp ->
  ReaderT (CrucibleState p sym ext rtp blocks r ctx) m (RegEntry sym tp)
evalReg' :: forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegEntry sym tp)
evalReg' Reg ctx tp
r = (RegMap sym ctx -> Reg ctx tp -> RegEntry sym tp
forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
RegMap sym ctx -> Reg ctx tp -> RegEntry sym tp
`regVal'` Reg ctx tp
r) (RegMap sym ctx -> RegEntry sym tp)
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym ctx)
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegEntry sym tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting
  (RegMap sym ctx)
  (CrucibleState p sym ext rtp blocks r ctx)
  (RegMap sym ctx)
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym ctx)
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view ((CallFrame sym ext blocks r ctx
 -> Const (RegMap sym ctx) (CallFrame sym ext blocks r ctx))
-> CrucibleState p sym ext rtp blocks r ctx
-> Const
     (RegMap sym ctx) (CrucibleState p sym ext rtp blocks r ctx)
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame((CallFrame sym ext blocks r ctx
  -> Const (RegMap sym ctx) (CallFrame sym ext blocks r ctx))
 -> CrucibleState p sym ext rtp blocks r ctx
 -> Const
      (RegMap sym ctx) (CrucibleState p sym ext rtp blocks r ctx))
-> ((RegMap sym ctx -> Const (RegMap sym ctx) (RegMap sym ctx))
    -> CallFrame sym ext blocks r ctx
    -> Const (RegMap sym ctx) (CallFrame sym ext blocks r ctx))
-> Getting
     (RegMap sym ctx)
     (CrucibleState p sym ext rtp blocks r ctx)
     (RegMap sym ctx)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(RegMap sym ctx -> Const (RegMap sym ctx) (RegMap sym ctx))
-> CallFrame sym ext blocks r ctx
-> Const (RegMap sym ctx) (CallFrame sym ext blocks r ctx)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args))
-> CallFrame sym ext blocks ret args
-> f (CallFrame sym ext blocks ret args)
frameRegs)


evalLogFn ::
  Int {- current verbosity -} ->
  CrucibleState p sym ext rtp blocks r ctx ->
  Int {- verbosity level of the message -} ->
  String ->
  IO ()
evalLogFn :: forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (ctx :: Ctx CrucibleType).
Int
-> CrucibleState p sym ext rtp blocks r ctx
-> Int
-> String
-> IO ()
evalLogFn Int
verb CrucibleState p sym ext rtp blocks r ctx
s Int
n String
msg = do
  let h :: Handle
h = CrucibleState p sym ext rtp blocks r ctx
sCrucibleState p sym ext rtp blocks r ctx
-> Getting Handle (CrucibleState p sym ext rtp blocks r ctx) Handle
-> Handle
forall s a. s -> Getting a s a -> a
^.(SimContext p sym ext -> Const Handle (SimContext p sym ext))
-> CrucibleState p sym ext rtp blocks r ctx
-> Const Handle (CrucibleState p sym ext rtp blocks r ctx)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext((SimContext p sym ext -> Const Handle (SimContext p sym ext))
 -> CrucibleState p sym ext rtp blocks r ctx
 -> Const Handle (CrucibleState p sym ext rtp blocks r ctx))
-> ((Handle -> Const Handle Handle)
    -> SimContext p sym ext -> Const Handle (SimContext p sym ext))
-> Getting Handle (CrucibleState p sym ext rtp blocks r ctx) Handle
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(SimContext p sym ext -> Handle)
-> (Handle -> Const Handle Handle)
-> SimContext p sym ext
-> Const Handle (SimContext p sym ext)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to SimContext p sym ext -> Handle
forall personality sym ext.
SimContext personality sym ext -> Handle
printHandle
  if Int
verb Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n then
      do Handle -> String -> IO ()
hPutStr Handle
h String
msg
         Handle -> IO ()
hFlush Handle
h
  else
      () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()

-- | Evaluate an expression.
evalExpr :: forall p sym ext ctx tp rtp blocks r.
  (IsSymInterface sym, IsSyntaxExtension ext) =>
  Int {- ^ current verbosity -} ->
  Expr ext ctx tp ->
  ReaderT (CrucibleState p sym ext rtp blocks r ctx) IO (RegValue sym tp)
evalExpr :: forall p sym ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType) rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
(IsSymInterface sym, IsSyntaxExtension ext) =>
Int
-> Expr ext ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) IO (RegValue sym tp)
evalExpr Int
verb (App App ext (Reg ctx) tp
a) = (CrucibleState p sym ext rtp blocks r ctx -> IO (RegValue sym tp))
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) IO (RegValue sym tp)
forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT ((CrucibleState p sym ext rtp blocks r ctx -> IO (RegValue sym tp))
 -> ReaderT
      (CrucibleState p sym ext rtp blocks r ctx) IO (RegValue sym tp))
-> (CrucibleState p sym ext rtp blocks r ctx
    -> IO (RegValue sym tp))
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) IO (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ \CrucibleState p sym ext rtp blocks r ctx
s ->
  do let iteFns :: IntrinsicTypes sym
iteFns = CrucibleState p sym ext rtp blocks r ctx
sCrucibleState p sym ext rtp blocks r ctx
-> Getting
     (IntrinsicTypes sym)
     (CrucibleState p sym ext rtp blocks r ctx)
     (IntrinsicTypes sym)
-> IntrinsicTypes sym
forall s a. s -> Getting a s a -> a
^.Getting
  (IntrinsicTypes sym)
  (CrucibleState p sym ext rtp blocks r ctx)
  (IntrinsicTypes sym)
forall p sym ext r f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(IntrinsicTypes sym -> f2 (IntrinsicTypes sym))
-> SimState p sym ext r f1 args
-> f2 (SimState p sym ext r f1 args)
stateIntrinsicTypes
     let simCtx :: SimContext p sym ext
simCtx = CrucibleState p sym ext rtp blocks r ctx
sCrucibleState p sym ext rtp blocks r ctx
-> Getting
     (SimContext p sym ext)
     (CrucibleState p sym ext rtp blocks r ctx)
     (SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
  (SimContext p sym ext)
  (CrucibleState p sym ext rtp blocks r ctx)
  (SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext
     let logFn :: Int -> String -> IO ()
logFn = Int
-> CrucibleState p sym ext rtp blocks r ctx
-> Int
-> String
-> IO ()
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (ctx :: Ctx CrucibleType).
Int
-> CrucibleState p sym ext rtp blocks r ctx
-> Int
-> String
-> IO ()
evalLogFn Int
verb CrucibleState p sym ext rtp blocks r ctx
s
     RegValue sym tp
r <- SimContext p sym ext
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (RegValue sym tp))
-> IO (RegValue sym tp)
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend SimContext p sym ext
simCtx ((forall {bak}.
  IsSymBackend sym bak =>
  bak -> IO (RegValue sym tp))
 -> IO (RegValue sym tp))
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (RegValue sym tp))
-> IO (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
            bak
-> IntrinsicTypes sym
-> (Int -> String -> IO ())
-> EvalAppFunc sym (ExprExtension ext)
-> EvalAppFunc sym (App ext)
forall sym bak ext.
IsSymBackend sym bak =>
bak
-> IntrinsicTypes sym
-> (Int -> String -> IO ())
-> EvalAppFunc sym (ExprExtension ext)
-> EvalAppFunc sym (App ext)
evalApp bak
bak IntrinsicTypes sym
iteFns Int -> String -> IO ()
logFn
              (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)
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 (SimContext p sym ext -> ExtensionImpl p sym ext
forall personality sym ext.
SimContext personality sym ext -> ExtensionImpl personality sym ext
extensionImpl (CrucibleState p sym ext rtp blocks r ctx
sCrucibleState p sym ext rtp blocks r ctx
-> Getting
     (SimContext p sym ext)
     (CrucibleState p sym ext rtp blocks r ctx)
     (SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
  (SimContext p sym ext)
  (CrucibleState p sym ext rtp blocks r ctx)
  (SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext)) bak
bak IntrinsicTypes sym
iteFns Int -> String -> IO ()
logFn CrucibleState p sym ext rtp blocks r ctx
s)
              (\Reg ctx tp
r -> ReaderT
  (CrucibleState p sym ext rtp blocks r ctx) IO (RegValue sym tp)
-> CrucibleState p sym ext rtp blocks r ctx -> IO (RegValue sym tp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT (Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) IO (RegValue sym tp)
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg Reg ctx tp
r) CrucibleState p sym ext rtp blocks r ctx
s)
              App ext (Reg ctx) tp
a
     RegValue sym tp -> IO (RegValue sym tp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (RegValue sym tp -> IO (RegValue sym tp))
-> RegValue sym tp -> IO (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$! RegValue sym tp
r

evalArgs' :: forall sym ctx args.
  RegMap sym ctx ->
  Ctx.Assignment (Reg ctx) args ->
  RegMap sym args
evalArgs' :: forall sym (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType).
RegMap sym ctx -> Assignment (Reg ctx) args -> RegMap sym args
evalArgs' RegMap sym ctx
m0 Assignment (Reg ctx) args
args = Assignment (RegEntry sym) args -> RegMap sym args
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap ((forall (x :: CrucibleType). Reg ctx x -> RegEntry sym x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Reg ctx) x -> Assignment (RegEntry sym) x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC (RegMap sym ctx -> Reg ctx x -> RegEntry sym x
forall (tp :: CrucibleType).
RegMap sym ctx -> Reg ctx tp -> RegEntry sym tp
getEntry RegMap sym ctx
m0) Assignment (Reg ctx) args
args)
  where getEntry :: RegMap sym ctx -> Reg ctx tp -> RegEntry sym tp
        getEntry :: forall (tp :: CrucibleType).
RegMap sym ctx -> Reg ctx tp -> RegEntry sym tp
getEntry (RegMap Assignment (RegEntry sym) ctx
m) Reg ctx tp
r = Assignment (RegEntry sym) ctx
m Assignment (RegEntry sym) ctx -> Index ctx tp -> RegEntry sym tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Reg ctx tp -> Index ctx tp
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Index ctx tp
regIndex Reg ctx tp
r
{-# NOINLINE evalArgs' #-}

-- | Evaluate the actual arguments for a function call or block transfer.
evalArgs ::
  Monad m =>
  Ctx.Assignment (Reg ctx) args ->
  ReaderT (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym args)
evalArgs :: forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (args :: Ctx CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Assignment (Reg ctx) args
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym args)
evalArgs Assignment (Reg ctx) args
args = (CrucibleState p sym ext rtp blocks r ctx -> m (RegMap sym args))
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym args)
forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT ((CrucibleState p sym ext rtp blocks r ctx -> m (RegMap sym args))
 -> ReaderT
      (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym args))
-> (CrucibleState p sym ext rtp blocks r ctx
    -> m (RegMap sym args))
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym args)
forall a b. (a -> b) -> a -> b
$ \CrucibleState p sym ext rtp blocks r ctx
s -> RegMap sym args -> m (RegMap sym args)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (RegMap sym args -> m (RegMap sym args))
-> RegMap sym args -> m (RegMap sym args)
forall a b. (a -> b) -> a -> b
$! RegMap sym ctx -> Assignment (Reg ctx) args -> RegMap sym args
forall sym (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType).
RegMap sym ctx -> Assignment (Reg ctx) args -> RegMap sym args
evalArgs' (CrucibleState p sym ext rtp blocks r ctx
sCrucibleState p sym ext rtp blocks r ctx
-> Getting
     (RegMap sym ctx)
     (CrucibleState p sym ext rtp blocks r ctx)
     (RegMap sym ctx)
-> RegMap sym ctx
forall s a. s -> Getting a s a -> a
^.(CallFrame sym ext blocks r ctx
 -> Const (RegMap sym ctx) (CallFrame sym ext blocks r ctx))
-> CrucibleState p sym ext rtp blocks r ctx
-> Const
     (RegMap sym ctx) (CrucibleState p sym ext rtp blocks r ctx)
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame((CallFrame sym ext blocks r ctx
  -> Const (RegMap sym ctx) (CallFrame sym ext blocks r ctx))
 -> CrucibleState p sym ext rtp blocks r ctx
 -> Const
      (RegMap sym ctx) (CrucibleState p sym ext rtp blocks r ctx))
-> ((RegMap sym ctx -> Const (RegMap sym ctx) (RegMap sym ctx))
    -> CallFrame sym ext blocks r ctx
    -> Const (RegMap sym ctx) (CallFrame sym ext blocks r ctx))
-> Getting
     (RegMap sym ctx)
     (CrucibleState p sym ext rtp blocks r ctx)
     (RegMap sym ctx)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(RegMap sym ctx -> Const (RegMap sym ctx) (RegMap sym ctx))
-> CallFrame sym ext blocks r ctx
-> Const (RegMap sym ctx) (CallFrame sym ext blocks r ctx)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args))
-> CallFrame sym ext blocks ret args
-> f (CallFrame sym ext blocks ret args)
frameRegs) Assignment (Reg ctx) args
args
{-# INLINE evalArgs #-}

-- | Resolve the arguments for a jump.
evalJumpTarget ::
  (IsSymInterface sym, Monad m) =>
  JumpTarget blocks ctx {- ^  Jump target to evaluate -} ->
  ReaderT (CrucibleState p sym ext rtp blocks r ctx) m (ResolvedJump sym blocks)
evalJumpTarget :: forall sym (m :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType) p ext rtp (r :: CrucibleType).
(IsSymInterface sym, Monad m) =>
JumpTarget blocks ctx
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx)
     m
     (ResolvedJump sym blocks)
evalJumpTarget (JumpTarget BlockID blocks args
tgt CtxRepr args
_ Assignment (Reg ctx) args
a) = BlockID blocks args -> RegMap sym args -> ResolvedJump sym blocks
forall sym (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
BlockID blocks args -> RegMap sym args -> ResolvedJump sym blocks
ResolvedJump BlockID blocks args
tgt (RegMap sym args -> ResolvedJump sym blocks)
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym args)
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx)
     m
     (ResolvedJump sym blocks)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Assignment (Reg ctx) args
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym args)
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (args :: Ctx CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Assignment (Reg ctx) args
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym args)
evalArgs Assignment (Reg ctx) args
a

-- | Resolve the arguments for a switch target.
evalSwitchTarget ::
  (IsSymInterface sym, Monad m) =>
  SwitchTarget blocks ctx tp {- ^ Switch target to evaluate -} ->
  RegEntry sym tp {- ^ Value inside the variant -}  ->
  ReaderT (CrucibleState p sym ext rtp blocks r ctx) m (ResolvedJump sym blocks)
evalSwitchTarget :: forall sym (m :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType) (tp :: CrucibleType) p ext rtp
       (r :: CrucibleType).
(IsSymInterface sym, Monad m) =>
SwitchTarget blocks ctx tp
-> RegEntry sym tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx)
     m
     (ResolvedJump sym blocks)
evalSwitchTarget (SwitchTarget BlockID blocks (args ::> tp)
tgt CtxRepr args
_tp Assignment (Reg ctx) args
a) RegEntry sym tp
x =
  do RegMap sym args
xs <- Assignment (Reg ctx) args
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym args)
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (args :: Ctx CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Assignment (Reg ctx) args
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym args)
evalArgs Assignment (Reg ctx) args
a
     ResolvedJump sym blocks
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx)
     m
     (ResolvedJump sym blocks)
forall a.
a -> ReaderT (CrucibleState p sym ext rtp blocks r ctx) m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BlockID blocks (args ::> tp)
-> RegMap sym (args ::> tp) -> ResolvedJump sym blocks
forall sym (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
BlockID blocks args -> RegMap sym args -> ResolvedJump sym blocks
ResolvedJump BlockID blocks (args ::> tp)
tgt (RegEntry sym tp -> RegMap sym args -> RegMap sym (args ::> tp)
forall sym (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
RegEntry sym tp -> RegMap sym ctx -> RegMap sym (ctx ::> tp)
assignReg' RegEntry sym tp
x RegMap sym args
xs))

-- | Update a reference cell with a new value. Writing an unassigned
-- value resets the reference cell to an uninitialized state.
alterRef ::
  IsSymInterface sym =>
  sym ->
  IntrinsicTypes sym ->
  TypeRepr tp ->
  MuxTree sym (RefCell tp) ->
  PartExpr (Pred sym) (RegValue sym tp) ->
  SymGlobalState sym ->
  IO (SymGlobalState sym)
alterRef :: forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> MuxTree sym (RefCell tp)
-> PartExpr (Pred sym) (RegValue sym tp)
-> SymGlobalState sym
-> IO (SymGlobalState sym)
alterRef sym
sym IntrinsicTypes sym
iTypes TypeRepr tp
tpr MuxTree sym (RefCell tp)
rs PartExpr (Pred sym) (RegValue sym tp)
newv SymGlobalState sym
globs = (SymGlobalState sym
 -> (RefCell tp, Pred sym) -> IO (SymGlobalState sym))
-> SymGlobalState sym
-> [(RefCell tp, Pred sym)]
-> IO (SymGlobalState sym)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM SymGlobalState sym
-> (RefCell tp, Pred sym) -> IO (SymGlobalState sym)
upd SymGlobalState sym
globs (MuxTree sym (RefCell tp) -> [(RefCell tp, Pred sym)]
forall sym a. MuxTree sym a -> [(a, Pred sym)]
viewMuxTree MuxTree sym (RefCell tp)
rs)
  where
  f :: Pred sym
-> RegValue sym tp
-> RegValue sym tp
-> PartialT sym IO (RegValue sym tp)
f Pred sym
p RegValue sym tp
a RegValue sym tp
b = IO (RegValue sym tp) -> PartialT sym IO (RegValue sym tp)
forall a. IO a -> PartialT sym IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RegValue sym tp) -> PartialT sym IO (RegValue sym tp))
-> IO (RegValue sym tp) -> PartialT sym IO (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxRegForType sym
sym IntrinsicTypes sym
iTypes TypeRepr tp
tpr Pred sym
p RegValue sym tp
a RegValue sym tp
b

  upd :: SymGlobalState sym
-> (RefCell tp, Pred sym) -> IO (SymGlobalState sym)
upd SymGlobalState sym
gs (RefCell tp
r,Pred sym
p) =
    do let oldv :: PartExpr (Pred sym) (RegValue sym tp)
oldv = RefCell tp
-> SymGlobalState sym -> PartExpr (Pred sym) (RegValue sym tp)
forall (tp :: CrucibleType) sym.
RefCell tp
-> SymGlobalState sym -> PartExpr (Pred sym) (RegValue sym tp)
lookupRef RefCell tp
r SymGlobalState sym
globs
       PartExpr (Pred sym) (RegValue sym tp)
z <- sym
-> (Pred sym
    -> RegValue sym tp
    -> RegValue sym tp
    -> PartialT sym IO (RegValue sym tp))
-> Pred sym
-> PartExpr (Pred sym) (RegValue sym tp)
-> PartExpr (Pred sym) (RegValue sym tp)
-> IO (PartExpr (Pred sym) (RegValue sym tp))
forall sym (m :: Type -> Type) a.
(IsExprBuilder sym, MonadIO m) =>
sym
-> (Pred sym -> a -> a -> PartialT sym m a)
-> Pred sym
-> PartExpr (Pred sym) a
-> PartExpr (Pred sym) a
-> m (PartExpr (Pred sym) a)
mergePartial sym
sym Pred sym
-> RegValue sym tp
-> RegValue sym tp
-> PartialT sym IO (RegValue sym tp)
f Pred sym
p PartExpr (Pred sym) (RegValue sym tp)
newv PartExpr (Pred sym) (RegValue sym tp)
oldv
       SymGlobalState sym -> IO (SymGlobalState sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymGlobalState sym
gs SymGlobalState sym
-> (SymGlobalState sym -> SymGlobalState sym) -> SymGlobalState sym
forall a b. a -> (a -> b) -> b
& RefCell tp
-> PartExpr (Pred sym) (RegValue sym tp)
-> SymGlobalState sym
-> SymGlobalState sym
forall (tp :: CrucibleType) sym.
RefCell tp
-> PartExpr (Pred sym) (RegValue sym tp)
-> SymGlobalState sym
-> SymGlobalState sym
updateRef RefCell tp
r PartExpr (Pred sym) (RegValue sym tp)
z)

-- | Read from a reference cell.
readRef ::
  IsSymBackend sym bak =>
  bak ->
  IntrinsicTypes sym ->
  TypeRepr tp ->
  MuxTree sym (RefCell tp) ->
  SymGlobalState sym ->
  IO (RegValue sym tp)
readRef :: forall sym bak (tp :: CrucibleType).
IsSymBackend sym bak =>
bak
-> IntrinsicTypes sym
-> TypeRepr tp
-> MuxTree sym (RefCell tp)
-> SymGlobalState sym
-> IO (RegValue sym tp)
readRef bak
bak IntrinsicTypes sym
iTypes TypeRepr tp
tpr MuxTree sym (RefCell tp)
rs SymGlobalState sym
globs =
  do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
     let vs :: [(SymExpr sym BaseBoolType,
  PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp))]
vs = ((RefCell tp, SymExpr sym BaseBoolType)
 -> (SymExpr sym BaseBoolType,
     PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)))
-> [(RefCell tp, SymExpr sym BaseBoolType)]
-> [(SymExpr sym BaseBoolType,
     PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp))]
forall a b. (a -> b) -> [a] -> [b]
map (\(RefCell tp
r,SymExpr sym BaseBoolType
p) -> (SymExpr sym BaseBoolType
p,RefCell tp
-> SymGlobalState sym
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
forall (tp :: CrucibleType) sym.
RefCell tp
-> SymGlobalState sym -> PartExpr (Pred sym) (RegValue sym tp)
lookupRef RefCell tp
r SymGlobalState sym
globs)) (MuxTree sym (RefCell tp)
-> [(RefCell tp, SymExpr sym BaseBoolType)]
forall sym a. MuxTree sym a -> [(a, Pred sym)]
viewMuxTree MuxTree sym (RefCell tp)
rs)
     let f :: SymExpr sym BaseBoolType
-> RegValue sym tp
-> RegValue sym tp
-> PartialT sym IO (RegValue sym tp)
f SymExpr sym BaseBoolType
p RegValue sym tp
a RegValue sym tp
b = IO (RegValue sym tp) -> PartialT sym IO (RegValue sym tp)
forall a. IO a -> PartialT sym IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RegValue sym tp) -> PartialT sym IO (RegValue sym tp))
-> IO (RegValue sym tp) -> PartialT sym IO (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxRegForType sym
sym IntrinsicTypes sym
iTypes TypeRepr tp
tpr SymExpr sym BaseBoolType
p RegValue sym tp
a RegValue sym tp
b
     PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
pv <- sym
-> (SymExpr sym BaseBoolType
    -> RegValue sym tp
    -> RegValue sym tp
    -> PartialT sym IO (RegValue sym tp))
-> [(SymExpr sym BaseBoolType,
     PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp))]
-> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp))
forall sym (m :: Type -> Type) a.
(IsExprBuilder sym, MonadIO m) =>
sym
-> (Pred sym -> a -> a -> PartialT sym m a)
-> [(Pred sym, PartExpr (Pred sym) a)]
-> m (PartExpr (Pred sym) a)
mergePartials sym
sym SymExpr sym BaseBoolType
-> RegValue sym tp
-> RegValue sym tp
-> PartialT sym IO (RegValue sym tp)
f [(SymExpr sym BaseBoolType,
  PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp))]
vs
     let msg :: SimErrorReason
msg = String -> SimErrorReason
ReadBeforeWriteSimError String
"Attempted to read uninitialized reference cell"
     bak
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
-> SimErrorReason
-> IO (RegValue sym tp)
forall sym bak v.
IsSymBackend sym bak =>
bak -> PartExpr (Pred sym) v -> SimErrorReason -> IO v
readPartExpr bak
bak PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
pv SimErrorReason
msg


-- | Evaluation operation for evaluating a single straight-line
--   statement of the Crucible evaluator.
--
--   This is allowed to throw user exceptions or 'SimError'.
stepStmt :: forall p sym ext rtp blocks r ctx ctx'.
  (IsSymInterface sym, IsSyntaxExtension ext) =>
  Int {- ^ Current verbosity -} ->
  Stmt ext ctx ctx' {- ^ Statement to evaluate -} ->
  StmtSeq ext blocks r ctx' {- ^ Remaining statements in the block -} ->
  ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
stepStmt :: forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (ctx :: Ctx CrucibleType)
       (ctx' :: Ctx CrucibleType).
(IsSymInterface sym, IsSyntaxExtension ext) =>
Int
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks r ctx'
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
stepStmt Int
verb Stmt ext ctx ctx'
stmt StmtSeq ext blocks r ctx'
rest =
  do SimContext p sym ext
ctx <- Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
  (SimContext p sym ext)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (SimContext p sym ext)
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
  (SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext
     let sym :: sym
sym = SimContext p sym ext
ctxSimContext p sym ext
-> Getting sym (SimContext p sym ext) sym -> sym
forall s a. s -> Getting a s a -> a
^.Getting sym (SimContext p sym ext) sym
forall p sym ext (f :: Type -> Type).
(Contravariant f, Functor f) =>
(sym -> f sym) -> SimContext p sym ext -> f (SimContext p sym ext)
ctxSymInterface
     let iTypes :: IntrinsicTypes sym
iTypes = SimContext p sym ext -> IntrinsicTypes sym
forall personality sym ext.
SimContext personality sym ext -> IntrinsicTypes sym
ctxIntrinsicTypes SimContext p sym ext
ctx
     SymGlobalState sym
globals <- Getting
  (SymGlobalState sym)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
  (SymGlobalState sym)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (SymGlobalState sym)
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view ((ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Const
      (SymGlobalState sym)
      (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Const
     (SymGlobalState sym)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree((ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> Const
       (SymGlobalState sym)
       (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Const
      (SymGlobalState sym)
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> ((SymGlobalState sym
     -> Const (SymGlobalState sym) (SymGlobalState sym))
    -> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> Const
         (SymGlobalState sym)
         (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     (SymGlobalState sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)
 -> Const
      (SymGlobalState sym)
      (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)))
-> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Const
     (SymGlobalState sym)
     (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame((TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)
  -> Const
       (SymGlobalState sym)
       (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)))
 -> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Const
      (SymGlobalState sym)
      (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> ((SymGlobalState sym
     -> Const (SymGlobalState sym) (SymGlobalState sym))
    -> TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)
    -> Const
         (SymGlobalState sym)
         (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)))
-> (SymGlobalState sym
    -> Const (SymGlobalState sym) (SymGlobalState sym))
-> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Const
     (SymGlobalState sym)
     (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(SymGlobalState sym
 -> Const (SymGlobalState sym) (SymGlobalState sym))
-> TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)
-> Const
     (SymGlobalState sym)
     (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx))
forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals)

     let continueWith :: forall rtp' blocks' r' c f a.
           (SimState p sym ext rtp' f a -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c)) ->
           ExecCont p sym ext rtp' f a
         continueWith :: forall rtp' (blocks' :: Ctx (Ctx CrucibleType))
       (r' :: CrucibleType) (c :: Ctx CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
(SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ExecCont p sym ext rtp' f a
continueWith SimState p sym ext rtp' f a
-> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c)
f = (SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ReaderT
     (SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
     IO
     (ExecState p sym ext rtp')
-> ReaderT
     (SimState p sym ext rtp' f a) IO (ExecState p sym ext rtp')
forall r' r (m :: Type -> Type) a.
(r' -> r) -> ReaderT r m a -> ReaderT r' m a
withReaderT SimState p sym ext rtp' f a
-> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c)
f (Int
-> ReaderT
     (SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
     IO
     (ExecState p sym ext rtp')
forall sym ext p rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (ctx :: Ctx CrucibleType).
(IsSymInterface sym, IsSyntaxExtension ext) =>
Int -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
checkConsTerm Int
verb)

     SimContext p sym ext
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend SimContext p sym ext
ctx ((forall {bak}.
  IsSymBackend sym bak =>
  bak -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
       case Stmt ext ctx ctx'
stmt of
         NewRefCell TypeRepr tp
tpr Reg ctx tp
x ->
           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
              RegValue sym tp
v <- Reg ctx tp
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym tp)
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg Reg ctx tp
x
              RefCell tp
r <- IO (RefCell tp)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RefCell tp)
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RefCell tp)
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
      IO
      (RefCell tp))
-> IO (RefCell tp)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RefCell tp)
forall a b. (a -> b) -> a -> b
$ HandleAllocator -> TypeRepr tp -> IO (RefCell tp)
forall (tp :: CrucibleType).
HandleAllocator -> TypeRepr tp -> IO (RefCell tp)
freshRefCell HandleAllocator
halloc TypeRepr tp
tpr
              (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState
      p
      sym
      ext
      rtp
      (CrucibleLang blocks r)
      ('Just (ctx '::> ReferenceType tp)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall rtp' (blocks' :: Ctx (Ctx CrucibleType))
       (r' :: CrucibleType) (c :: Ctx CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
(SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ExecCont p sym ext rtp' f a
continueWith ((SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> SimState
       p
       sym
       ext
       rtp
       (CrucibleLang blocks r)
       ('Just (ctx '::> ReferenceType tp)))
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> SimState
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just (ctx '::> ReferenceType tp)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$
                 ((ActiveTree
   p
   sym
   ext
   rtp
   (CrucibleLang blocks r)
   ('Just (ctx '::> ReferenceType tp))
 -> Identity
      (ActiveTree
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just (ctx '::> ReferenceType tp))))
-> SimState
     p
     sym
     ext
     rtp
     (CrucibleLang blocks r)
     ('Just (ctx '::> ReferenceType tp))
-> Identity
     (SimState
        p
        sym
        ext
        rtp
        (CrucibleLang blocks r)
        ('Just (ctx '::> ReferenceType tp)))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree ((ActiveTree
    p
    sym
    ext
    rtp
    (CrucibleLang blocks r)
    ('Just (ctx '::> ReferenceType tp))
  -> Identity
       (ActiveTree
          p
          sym
          ext
          rtp
          (CrucibleLang blocks r)
          ('Just (ctx '::> ReferenceType tp))))
 -> SimState
      p
      sym
      ext
      rtp
      (CrucibleLang blocks r)
      ('Just (ctx '::> ReferenceType tp))
 -> Identity
      (SimState
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just (ctx '::> ReferenceType tp))))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
    -> ActiveTree
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just (ctx '::> ReferenceType tp))
    -> Identity
         (ActiveTree
            p
            sym
            ext
            rtp
            (CrucibleLang blocks r)
            ('Just (ctx '::> ReferenceType tp))))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState
     p
     sym
     ext
     rtp
     (CrucibleLang blocks r)
     ('Just (ctx '::> ReferenceType tp))
-> Identity
     (SimState
        p
        sym
        ext
        rtp
        (CrucibleLang blocks r)
        ('Just (ctx '::> ReferenceType tp)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame
   sym ext (CrucibleLang blocks r) ('Just (ctx '::> ReferenceType tp))
 -> Identity
      (TopFrame
         sym
         ext
         (CrucibleLang blocks r)
         ('Just (ctx '::> ReferenceType tp))))
-> ActiveTree
     p
     sym
     ext
     rtp
     (CrucibleLang blocks r)
     ('Just (ctx '::> ReferenceType tp))
-> Identity
     (ActiveTree
        p
        sym
        ext
        rtp
        (CrucibleLang blocks r)
        ('Just (ctx '::> ReferenceType tp)))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame ((TopFrame
    sym ext (CrucibleLang blocks r) ('Just (ctx '::> ReferenceType tp))
  -> Identity
       (TopFrame
          sym
          ext
          (CrucibleLang blocks r)
          ('Just (ctx '::> ReferenceType tp))))
 -> ActiveTree
      p
      sym
      ext
      rtp
      (CrucibleLang blocks r)
      ('Just (ctx '::> ReferenceType tp))
 -> Identity
      (ActiveTree
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just (ctx '::> ReferenceType tp))))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
    -> TopFrame
         sym ext (CrucibleLang blocks r) ('Just (ctx '::> ReferenceType tp))
    -> Identity
         (TopFrame
            sym
            ext
            (CrucibleLang blocks r)
            ('Just (ctx '::> ReferenceType tp))))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> ActiveTree
     p
     sym
     ext
     rtp
     (CrucibleLang blocks r)
     ('Just (ctx '::> ReferenceType tp))
-> Identity
     (ActiveTree
        p
        sym
        ext
        rtp
        (CrucibleLang blocks r)
        ('Just (ctx '::> ReferenceType tp)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymGlobalState sym -> Identity (SymGlobalState sym))
-> TopFrame
     sym ext (CrucibleLang blocks r) ('Just (ctx '::> ReferenceType tp))
-> Identity
     (TopFrame
        sym
        ext
        (CrucibleLang blocks r)
        ('Just (ctx '::> ReferenceType tp)))
forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
 -> SimState
      p
      sym
      ext
      rtp
      (CrucibleLang blocks r)
      ('Just (ctx '::> ReferenceType tp))
 -> Identity
      (SimState
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just (ctx '::> ReferenceType tp))))
-> (SymGlobalState sym -> SymGlobalState sym)
-> SimState
     p
     sym
     ext
     rtp
     (CrucibleLang blocks r)
     ('Just (ctx '::> ReferenceType tp))
-> SimState
     p
     sym
     ext
     rtp
     (CrucibleLang blocks r)
     ('Just (ctx '::> ReferenceType tp))
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ sym
-> RefCell tp
-> RegValue sym tp
-> SymGlobalState sym
-> SymGlobalState sym
forall sym (tp :: CrucibleType).
IsExprBuilder sym =>
sym
-> RefCell tp
-> RegValue sym tp
-> SymGlobalState sym
-> SymGlobalState sym
insertRef sym
sym RefCell tp
r RegValue sym tp
v) (SimState
   p
   sym
   ext
   rtp
   (CrucibleLang blocks r)
   ('Just (ctx '::> ReferenceType tp))
 -> SimState
      p
      sym
      ext
      rtp
      (CrucibleLang blocks r)
      ('Just (ctx '::> ReferenceType tp)))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> SimState
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just (ctx '::> ReferenceType tp)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState
     p
     sym
     ext
     rtp
     (CrucibleLang blocks r)
     ('Just (ctx '::> ReferenceType tp))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                 ((CallFrame sym ext blocks r ctx
 -> Identity
      (CallFrame sym ext blocks r (ctx '::> ReferenceType tp)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState
        p
        sym
        ext
        rtp
        (CrucibleLang blocks r)
        ('Just (ctx '::> ReferenceType tp)))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame ((CallFrame sym ext blocks r ctx
  -> Identity
       (CallFrame sym ext blocks r (ctx '::> ReferenceType tp)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just (ctx '::> ReferenceType tp))))
-> (CallFrame sym ext blocks r ctx
    -> CallFrame sym ext blocks r (ctx '::> ReferenceType tp))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState
     p
     sym
     ext
     rtp
     (CrucibleLang blocks r)
     ('Just (ctx '::> ReferenceType tp))
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ TypeRepr (ReferenceType tp)
-> RegValue sym (ReferenceType tp)
-> StmtSeq ext blocks r (ctx '::> ReferenceType tp)
-> CallFrame sym ext blocks r ctx
-> CallFrame sym ext blocks r (ctx '::> ReferenceType tp)
forall (tp :: CrucibleType) sym ext
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TypeRepr tp
-> RegValue sym tp
-> StmtSeq ext blocks ret (ctx ::> tp)
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret (ctx ::> tp)
extendFrame (TypeRepr tp -> TypeRepr (ReferenceType tp)
forall (a :: CrucibleType).
TypeRepr a -> TypeRepr ('ReferenceType a)
ReferenceRepr TypeRepr tp
tpr) (sym -> RefCell tp -> MuxTree sym (RefCell tp)
forall sym a. IsExprBuilder sym => sym -> a -> MuxTree sym a
toMuxTree sym
sym RefCell tp
r) StmtSeq ext blocks r ctx'
StmtSeq ext blocks r (ctx '::> ReferenceType tp)
rest)

         NewEmptyRefCell TypeRepr tp
tpr ->
           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
              RefCell tp
r <- IO (RefCell tp)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RefCell tp)
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RefCell tp)
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
      IO
      (RefCell tp))
-> IO (RefCell tp)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RefCell tp)
forall a b. (a -> b) -> a -> b
$ HandleAllocator -> TypeRepr tp -> IO (RefCell tp)
forall (tp :: CrucibleType).
HandleAllocator -> TypeRepr tp -> IO (RefCell tp)
freshRefCell HandleAllocator
halloc TypeRepr tp
tpr
              (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState
      p
      sym
      ext
      rtp
      (CrucibleLang blocks r)
      ('Just (ctx '::> ReferenceType tp)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall rtp' (blocks' :: Ctx (Ctx CrucibleType))
       (r' :: CrucibleType) (c :: Ctx CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
(SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ExecCont p sym ext rtp' f a
continueWith ((SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> SimState
       p
       sym
       ext
       rtp
       (CrucibleLang blocks r)
       ('Just (ctx '::> ReferenceType tp)))
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> SimState
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just (ctx '::> ReferenceType tp)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$
                (CallFrame sym ext blocks r ctx
 -> Identity
      (CallFrame sym ext blocks r (ctx '::> ReferenceType tp)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState
        p
        sym
        ext
        rtp
        (CrucibleLang blocks r)
        ('Just (ctx '::> ReferenceType tp)))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame ((CallFrame sym ext blocks r ctx
  -> Identity
       (CallFrame sym ext blocks r (ctx '::> ReferenceType tp)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just (ctx '::> ReferenceType tp))))
-> (CallFrame sym ext blocks r ctx
    -> CallFrame sym ext blocks r (ctx '::> ReferenceType tp))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState
     p
     sym
     ext
     rtp
     (CrucibleLang blocks r)
     ('Just (ctx '::> ReferenceType tp))
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ TypeRepr (ReferenceType tp)
-> RegValue sym (ReferenceType tp)
-> StmtSeq ext blocks r (ctx '::> ReferenceType tp)
-> CallFrame sym ext blocks r ctx
-> CallFrame sym ext blocks r (ctx '::> ReferenceType tp)
forall (tp :: CrucibleType) sym ext
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TypeRepr tp
-> RegValue sym tp
-> StmtSeq ext blocks ret (ctx ::> tp)
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret (ctx ::> tp)
extendFrame (TypeRepr tp -> TypeRepr (ReferenceType tp)
forall (a :: CrucibleType).
TypeRepr a -> TypeRepr ('ReferenceType a)
ReferenceRepr TypeRepr tp
tpr) (sym -> RefCell tp -> MuxTree sym (RefCell tp)
forall sym a. IsExprBuilder sym => sym -> a -> MuxTree sym a
toMuxTree sym
sym RefCell tp
r) StmtSeq ext blocks r ctx'
StmtSeq ext blocks r (ctx '::> ReferenceType tp)
rest

         ReadRefCell Reg ctx (ReferenceType tp)
x ->
           do RegEntry (ReferenceRepr TypeRepr a
tpr) RegValue sym (ReferenceType tp)
rs <- Reg ctx (ReferenceType tp)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegEntry sym (ReferenceType tp))
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegEntry sym tp)
evalReg' Reg ctx (ReferenceType tp)
x
              RegValue sym tp
v <- IO (RegValue sym tp)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym tp)
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RegValue sym tp)
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
      IO
      (RegValue sym tp))
-> IO (RegValue sym tp)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ bak
-> IntrinsicTypes sym
-> TypeRepr a
-> MuxTree sym (RefCell a)
-> SymGlobalState sym
-> IO (RegValue sym a)
forall sym bak (tp :: CrucibleType).
IsSymBackend sym bak =>
bak
-> IntrinsicTypes sym
-> TypeRepr tp
-> MuxTree sym (RefCell tp)
-> SymGlobalState sym
-> IO (RegValue sym tp)
readRef bak
bak IntrinsicTypes sym
iTypes TypeRepr a
tpr MuxTree sym (RefCell a)
RegValue sym (ReferenceType tp)
rs SymGlobalState sym
globals
              (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState
      p sym ext rtp (CrucibleLang blocks r) ('Just (ctx ::> a)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall rtp' (blocks' :: Ctx (Ctx CrucibleType))
       (r' :: CrucibleType) (c :: Ctx CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
(SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ExecCont p sym ext rtp' f a
continueWith ((SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> SimState
       p sym ext rtp (CrucibleLang blocks r) ('Just (ctx ::> a)))
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> SimState
         p sym ext rtp (CrucibleLang blocks r) ('Just (ctx ::> a)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$
                (CallFrame sym ext blocks r ctx
 -> Identity (CallFrame sym ext blocks r (ctx ::> a)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState
        p sym ext rtp (CrucibleLang blocks r) ('Just (ctx ::> a)))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame ((CallFrame sym ext blocks r ctx
  -> Identity (CallFrame sym ext blocks r (ctx ::> a)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState
         p sym ext rtp (CrucibleLang blocks r) ('Just (ctx ::> a))))
-> (CallFrame sym ext blocks r ctx
    -> CallFrame sym ext blocks r (ctx ::> a))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState
     p sym ext rtp (CrucibleLang blocks r) ('Just (ctx ::> a))
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ TypeRepr a
-> RegValue sym a
-> StmtSeq ext blocks r (ctx ::> a)
-> CallFrame sym ext blocks r ctx
-> CallFrame sym ext blocks r (ctx ::> a)
forall (tp :: CrucibleType) sym ext
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TypeRepr tp
-> RegValue sym tp
-> StmtSeq ext blocks ret (ctx ::> tp)
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret (ctx ::> tp)
extendFrame TypeRepr a
tpr RegValue sym tp
RegValue sym a
v StmtSeq ext blocks r ctx'
StmtSeq ext blocks r (ctx ::> a)
rest

         WriteRefCell Reg ctx (ReferenceType tp)
x Reg ctx tp
y ->
           do RegEntry (ReferenceRepr TypeRepr a
tpr) RegValue sym (ReferenceType tp)
rs <- Reg ctx (ReferenceType tp)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegEntry sym (ReferenceType tp))
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegEntry sym tp)
evalReg' Reg ctx (ReferenceType tp)
x
              PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
newv <- sym
-> RegValue sym tp
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
forall sym v.
IsExprBuilder sym =>
sym -> v -> PartExpr (Pred sym) v
justPartExpr sym
sym (RegValue sym tp
 -> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp))
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym tp)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Reg ctx tp
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym tp)
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg Reg ctx tp
y
              SymGlobalState sym
globals' <- IO (SymGlobalState sym)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (SymGlobalState sym)
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymGlobalState sym)
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
      IO
      (SymGlobalState sym))
-> IO (SymGlobalState sym)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (SymGlobalState sym)
forall a b. (a -> b) -> a -> b
$ sym
-> IntrinsicTypes sym
-> TypeRepr a
-> MuxTree sym (RefCell a)
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym a)
-> SymGlobalState sym
-> IO (SymGlobalState sym)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> MuxTree sym (RefCell tp)
-> PartExpr (Pred sym) (RegValue sym tp)
-> SymGlobalState sym
-> IO (SymGlobalState sym)
alterRef sym
sym IntrinsicTypes sym
iTypes TypeRepr a
tpr MuxTree sym (RefCell a)
RegValue sym (ReferenceType tp)
rs PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
PartExpr (SymExpr sym BaseBoolType) (RegValue sym a)
newv SymGlobalState sym
globals
              (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall rtp' (blocks' :: Ctx (Ctx CrucibleType))
       (r' :: CrucibleType) (c :: Ctx CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
(SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ExecCont p sym ext rtp' f a
continueWith ((SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$
                ((ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> Identity
       (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
    -> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> Identity
         (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)
 -> Identity (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)))
-> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame ((TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)
  -> Identity (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)))
 -> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
    -> TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)
    -> Identity (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymGlobalState sym -> Identity (SymGlobalState sym))
-> TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)
-> Identity (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx))
forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> SymGlobalState sym
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ SymGlobalState sym
globals') (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                ((CallFrame sym ext blocks r ctx
 -> Identity (CallFrame sym ext blocks r ctx))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame  ((CallFrame sym ext blocks r ctx
  -> Identity (CallFrame sym ext blocks r ctx))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> ((StmtSeq ext blocks r ctx
     -> Identity (StmtSeq ext blocks r ctx))
    -> CallFrame sym ext blocks r ctx
    -> Identity (CallFrame sym ext blocks r ctx))
-> (StmtSeq ext blocks r ctx
    -> Identity (StmtSeq ext blocks r ctx))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StmtSeq ext blocks r ctx -> Identity (StmtSeq ext blocks r ctx))
-> CallFrame sym ext blocks r ctx
-> Identity (CallFrame sym ext blocks r ctx)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(StmtSeq ext blocks ret ctx -> f (StmtSeq ext blocks ret ctx))
-> CallFrame sym ext blocks ret ctx
-> f (CallFrame sym ext blocks ret ctx)
frameStmts ((StmtSeq ext blocks r ctx -> Identity (StmtSeq ext blocks r ctx))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> StmtSeq ext blocks r ctx
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ StmtSeq ext blocks r ctx
StmtSeq ext blocks r ctx'
rest)

         DropRefCell Reg ctx (ReferenceType tp)
x ->
           do RegEntry (ReferenceRepr TypeRepr a
tpr) RegValue sym (ReferenceType tp)
rs <- Reg ctx (ReferenceType tp)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegEntry sym (ReferenceType tp))
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegEntry sym tp)
evalReg' Reg ctx (ReferenceType tp)
x
              SymGlobalState sym
globals' <- IO (SymGlobalState sym)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (SymGlobalState sym)
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymGlobalState sym)
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
      IO
      (SymGlobalState sym))
-> IO (SymGlobalState sym)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (SymGlobalState sym)
forall a b. (a -> b) -> a -> b
$ sym
-> IntrinsicTypes sym
-> TypeRepr a
-> MuxTree sym (RefCell a)
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym a)
-> SymGlobalState sym
-> IO (SymGlobalState sym)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> MuxTree sym (RefCell tp)
-> PartExpr (Pred sym) (RegValue sym tp)
-> SymGlobalState sym
-> IO (SymGlobalState sym)
alterRef sym
sym IntrinsicTypes sym
iTypes TypeRepr a
tpr MuxTree sym (RefCell a)
RegValue sym (ReferenceType tp)
rs PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
PartExpr (SymExpr sym BaseBoolType) (RegValue sym a)
forall p v. PartExpr p v
Unassigned SymGlobalState sym
globals
              (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall rtp' (blocks' :: Ctx (Ctx CrucibleType))
       (r' :: CrucibleType) (c :: Ctx CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
(SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ExecCont p sym ext rtp' f a
continueWith ((SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$
                ((ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> Identity
       (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
    -> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> Identity
         (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)
 -> Identity (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)))
-> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame ((TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)
  -> Identity (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)))
 -> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
    -> TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)
    -> Identity (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymGlobalState sym -> Identity (SymGlobalState sym))
-> TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)
-> Identity (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx))
forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> SymGlobalState sym
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ SymGlobalState sym
globals') (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                ((CallFrame sym ext blocks r ctx
 -> Identity (CallFrame sym ext blocks r ctx))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame  ((CallFrame sym ext blocks r ctx
  -> Identity (CallFrame sym ext blocks r ctx))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> ((StmtSeq ext blocks r ctx
     -> Identity (StmtSeq ext blocks r ctx))
    -> CallFrame sym ext blocks r ctx
    -> Identity (CallFrame sym ext blocks r ctx))
-> (StmtSeq ext blocks r ctx
    -> Identity (StmtSeq ext blocks r ctx))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StmtSeq ext blocks r ctx -> Identity (StmtSeq ext blocks r ctx))
-> CallFrame sym ext blocks r ctx
-> Identity (CallFrame sym ext blocks r ctx)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(StmtSeq ext blocks ret ctx -> f (StmtSeq ext blocks ret ctx))
-> CallFrame sym ext blocks ret ctx
-> f (CallFrame sym ext blocks ret ctx)
frameStmts ((StmtSeq ext blocks r ctx -> Identity (StmtSeq ext blocks r ctx))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> StmtSeq ext blocks r ctx
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ StmtSeq ext blocks r ctx
StmtSeq ext blocks r ctx'
rest)

         ReadGlobal GlobalVar tp
global_var -> do
           case GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
lookupGlobal GlobalVar tp
global_var SymGlobalState sym
globals of
             Maybe (RegValue sym tp)
Nothing ->
               do let msg :: SimErrorReason
msg = String -> SimErrorReason
ReadBeforeWriteSimError (String -> SimErrorReason) -> String -> SimErrorReason
forall a b. (a -> b) -> a -> b
$ String
"Attempt to read undefined global " String -> String -> String
forall a. [a] -> [a] -> [a]
++ GlobalVar tp -> String
forall a. Show a => a -> String
show GlobalVar tp
global_var
                  IO (ExecState p sym ext rtp)
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (ExecState p sym ext rtp)
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> IO (ExecState p sym ext rtp)
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$ bak -> SimErrorReason -> IO (ExecState p sym ext rtp)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak SimErrorReason
msg
             Just RegValue sym tp
v ->
               (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState
      p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall rtp' (blocks' :: Ctx (Ctx CrucibleType))
       (r' :: CrucibleType) (c :: Ctx CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
(SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ExecCont p sym ext rtp' f a
continueWith ((SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> SimState
       p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp)))
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> SimState
         p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$
                 ((CallFrame sym ext blocks r ctx
 -> Identity (CallFrame sym ext blocks r (ctx '::> tp)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState
        p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp)))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame ((CallFrame sym ext blocks r ctx
  -> Identity (CallFrame sym ext blocks r (ctx '::> tp)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState
         p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp))))
-> (CallFrame sym ext blocks r ctx
    -> CallFrame sym ext blocks r (ctx '::> tp))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState
     p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp))
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ TypeRepr tp
-> RegValue sym tp
-> StmtSeq ext blocks r (ctx '::> tp)
-> CallFrame sym ext blocks r ctx
-> CallFrame sym ext blocks r (ctx '::> tp)
forall (tp :: CrucibleType) sym ext
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TypeRepr tp
-> RegValue sym tp
-> StmtSeq ext blocks ret (ctx ::> tp)
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret (ctx ::> tp)
extendFrame (GlobalVar tp -> TypeRepr tp
forall (tp :: CrucibleType). GlobalVar tp -> TypeRepr tp
globalType GlobalVar tp
global_var) RegValue sym tp
v StmtSeq ext blocks r ctx'
StmtSeq ext blocks r (ctx '::> tp)
rest)

         WriteGlobal GlobalVar tp
global_var Reg ctx tp
local_reg ->
           do RegValue sym tp
v <- Reg ctx tp
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym tp)
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg Reg ctx tp
local_reg
              (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall rtp' (blocks' :: Ctx (Ctx CrucibleType))
       (r' :: CrucibleType) (c :: Ctx CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
(SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ExecCont p sym ext rtp' f a
continueWith ((SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$
                ((ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree ((ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> Identity
       (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
    -> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> Identity
         (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)
 -> Identity (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)))
-> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
actFrame ((TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)
  -> Identity (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)))
 -> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> ((SymGlobalState sym -> Identity (SymGlobalState sym))
    -> TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)
    -> Identity (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)))
-> (SymGlobalState sym -> Identity (SymGlobalState sym))
-> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymGlobalState sym -> Identity (SymGlobalState sym))
-> TopFrame sym ext (CrucibleLang blocks r) ('Just ctx)
-> Identity (TopFrame sym ext (CrucibleLang blocks r) ('Just ctx))
forall sym u (f :: Type -> Type).
Functor f =>
(SymGlobalState sym -> f (SymGlobalState sym))
-> GlobalPair sym u -> f (GlobalPair sym u)
gpGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> (SymGlobalState sym -> SymGlobalState sym)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
insertGlobal GlobalVar tp
global_var RegValue sym tp
v) (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                ((CallFrame sym ext blocks r ctx
 -> Identity (CallFrame sym ext blocks r ctx))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame ((CallFrame sym ext blocks r ctx
  -> Identity (CallFrame sym ext blocks r ctx))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> ((StmtSeq ext blocks r ctx
     -> Identity (StmtSeq ext blocks r ctx))
    -> CallFrame sym ext blocks r ctx
    -> Identity (CallFrame sym ext blocks r ctx))
-> (StmtSeq ext blocks r ctx
    -> Identity (StmtSeq ext blocks r ctx))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StmtSeq ext blocks r ctx -> Identity (StmtSeq ext blocks r ctx))
-> CallFrame sym ext blocks r ctx
-> Identity (CallFrame sym ext blocks r ctx)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(StmtSeq ext blocks ret ctx -> f (StmtSeq ext blocks ret ctx))
-> CallFrame sym ext blocks ret ctx
-> f (CallFrame sym ext blocks ret ctx)
frameStmts ((StmtSeq ext blocks r ctx -> Identity (StmtSeq ext blocks r ctx))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> StmtSeq ext blocks r ctx
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ StmtSeq ext blocks r ctx
StmtSeq ext blocks r ctx'
rest)

         FreshConstant BaseTypeRepr bt
bt Maybe SolverSymbol
mnm ->
           do let nm :: SolverSymbol
nm = SolverSymbol -> Maybe SolverSymbol -> SolverSymbol
forall a. a -> Maybe a -> a
fromMaybe SolverSymbol
emptySymbol Maybe SolverSymbol
mnm
              SymExpr sym bt
v <- IO (SymExpr sym bt)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (SymExpr sym bt)
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym bt)
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
      IO
      (SymExpr sym bt))
-> IO (SymExpr sym bt)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (SymExpr sym bt)
forall a b. (a -> b) -> a -> b
$ sym -> SolverSymbol -> BaseTypeRepr bt -> IO (SymExpr sym bt)
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshConstant sym
sym SolverSymbol
nm BaseTypeRepr bt
bt
              (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState
      p
      sym
      ext
      rtp
      (CrucibleLang blocks r)
      ('Just (ctx '::> BaseToType bt)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall rtp' (blocks' :: Ctx (Ctx CrucibleType))
       (r' :: CrucibleType) (c :: Ctx CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
(SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ExecCont p sym ext rtp' f a
continueWith ((SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> SimState
       p
       sym
       ext
       rtp
       (CrucibleLang blocks r)
       ('Just (ctx '::> BaseToType bt)))
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> SimState
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just (ctx '::> BaseToType bt)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$ (CallFrame sym ext blocks r ctx
 -> Identity (CallFrame sym ext blocks r (ctx '::> BaseToType bt)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState
        p
        sym
        ext
        rtp
        (CrucibleLang blocks r)
        ('Just (ctx '::> BaseToType bt)))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame ((CallFrame sym ext blocks r ctx
  -> Identity (CallFrame sym ext blocks r (ctx '::> BaseToType bt)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just (ctx '::> BaseToType bt))))
-> (CallFrame sym ext blocks r ctx
    -> CallFrame sym ext blocks r (ctx '::> BaseToType bt))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState
     p
     sym
     ext
     rtp
     (CrucibleLang blocks r)
     ('Just (ctx '::> BaseToType bt))
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ TypeRepr (BaseToType bt)
-> RegValue sym (BaseToType bt)
-> StmtSeq ext blocks r (ctx '::> BaseToType bt)
-> CallFrame sym ext blocks r ctx
-> CallFrame sym ext blocks r (ctx '::> BaseToType bt)
forall (tp :: CrucibleType) sym ext
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TypeRepr tp
-> RegValue sym tp
-> StmtSeq ext blocks ret (ctx ::> tp)
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret (ctx ::> tp)
extendFrame (BaseTypeRepr bt -> TypeRepr (BaseToType bt)
forall (bt :: BaseType).
BaseTypeRepr bt -> TypeRepr (BaseToType bt)
baseToType BaseTypeRepr bt
bt) SymExpr sym bt
RegValue sym (BaseToType bt)
v StmtSeq ext blocks r ctx'
StmtSeq ext blocks r (ctx '::> BaseToType bt)
rest

         FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
mnm ->
           do let nm :: SolverSymbol
nm = SolverSymbol -> Maybe SolverSymbol -> SolverSymbol
forall a. a -> Maybe a -> a
fromMaybe SolverSymbol
emptySymbol Maybe SolverSymbol
mnm
              SymExpr sym (SymInterpretedFloatType sym fi)
v <- IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (SymExpr sym (SymInterpretedFloatType sym fi))
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (SymInterpretedFloatType sym fi))
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
      IO
      (SymExpr sym (SymInterpretedFloatType sym fi)))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (SymExpr sym (SymInterpretedFloatType sym fi))
forall a b. (a -> b) -> a -> b
$ sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall sym (fi :: FloatInfo).
IsInterpretedFloatSymExprBuilder sym =>
sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall (fi :: FloatInfo).
sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
freshFloatConstant sym
sym SolverSymbol
nm FloatInfoRepr fi
fi
              (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState
      p
      sym
      ext
      rtp
      (CrucibleLang blocks r)
      ('Just (ctx '::> FloatType fi)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall rtp' (blocks' :: Ctx (Ctx CrucibleType))
       (r' :: CrucibleType) (c :: Ctx CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
(SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ExecCont p sym ext rtp' f a
continueWith ((SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> SimState
       p
       sym
       ext
       rtp
       (CrucibleLang blocks r)
       ('Just (ctx '::> FloatType fi)))
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> SimState
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just (ctx '::> FloatType fi)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$ (CallFrame sym ext blocks r ctx
 -> Identity (CallFrame sym ext blocks r (ctx '::> FloatType fi)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState
        p
        sym
        ext
        rtp
        (CrucibleLang blocks r)
        ('Just (ctx '::> FloatType fi)))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame ((CallFrame sym ext blocks r ctx
  -> Identity (CallFrame sym ext blocks r (ctx '::> FloatType fi)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState
         p
         sym
         ext
         rtp
         (CrucibleLang blocks r)
         ('Just (ctx '::> FloatType fi))))
-> (CallFrame sym ext blocks r ctx
    -> CallFrame sym ext blocks r (ctx '::> FloatType fi))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState
     p
     sym
     ext
     rtp
     (CrucibleLang blocks r)
     ('Just (ctx '::> FloatType fi))
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ TypeRepr (FloatType fi)
-> RegValue sym (FloatType fi)
-> StmtSeq ext blocks r (ctx '::> FloatType fi)
-> CallFrame sym ext blocks r ctx
-> CallFrame sym ext blocks r (ctx '::> FloatType fi)
forall (tp :: CrucibleType) sym ext
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TypeRepr tp
-> RegValue sym tp
-> StmtSeq ext blocks ret (ctx ::> tp)
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret (ctx ::> tp)
extendFrame (FloatInfoRepr fi -> TypeRepr (FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi) SymExpr sym (SymInterpretedFloatType sym fi)
RegValue sym (FloatType fi)
v StmtSeq ext blocks r ctx'
StmtSeq ext blocks r (ctx '::> FloatType fi)
rest

         FreshNat Maybe SolverSymbol
mnm ->
           do let nm :: SolverSymbol
nm = SolverSymbol -> Maybe SolverSymbol -> SolverSymbol
forall a. a -> Maybe a -> a
fromMaybe SolverSymbol
emptySymbol Maybe SolverSymbol
mnm
              SymNat sym
v <- IO (SymNat sym)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (SymNat sym)
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymNat sym)
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
      IO
      (SymNat sym))
-> IO (SymNat sym)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (SymNat sym)
forall a b. (a -> b) -> a -> b
$ sym -> SolverSymbol -> IO (SymNat sym)
forall sym.
IsSymExprBuilder sym =>
sym -> SolverSymbol -> IO (SymNat sym)
freshNat sym
sym SolverSymbol
nm
              (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState
      p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> NatType)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall rtp' (blocks' :: Ctx (Ctx CrucibleType))
       (r' :: CrucibleType) (c :: Ctx CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
(SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ExecCont p sym ext rtp' f a
continueWith ((SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> SimState
       p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> NatType)))
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> SimState
         p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> NatType)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$ (CallFrame sym ext blocks r ctx
 -> Identity (CallFrame sym ext blocks r (ctx '::> NatType)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState
        p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> NatType)))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame ((CallFrame sym ext blocks r ctx
  -> Identity (CallFrame sym ext blocks r (ctx '::> NatType)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState
         p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> NatType))))
-> (CallFrame sym ext blocks r ctx
    -> CallFrame sym ext blocks r (ctx '::> NatType))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState
     p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> NatType))
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ TypeRepr NatType
-> RegValue sym NatType
-> StmtSeq ext blocks r (ctx '::> NatType)
-> CallFrame sym ext blocks r ctx
-> CallFrame sym ext blocks r (ctx '::> NatType)
forall (tp :: CrucibleType) sym ext
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TypeRepr tp
-> RegValue sym tp
-> StmtSeq ext blocks ret (ctx ::> tp)
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret (ctx ::> tp)
extendFrame TypeRepr NatType
NatRepr SymNat sym
RegValue sym NatType
v StmtSeq ext blocks r ctx'
StmtSeq ext blocks r (ctx '::> NatType)
rest

         SetReg TypeRepr tp
tp Expr ext ctx tp
e ->
           do RegValue sym tp
v <- Int
-> Expr ext ctx tp
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym tp)
forall p sym ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType) rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
(IsSymInterface sym, IsSyntaxExtension ext) =>
Int
-> Expr ext ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) IO (RegValue sym tp)
evalExpr Int
verb Expr ext ctx tp
e
              (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState
      p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall rtp' (blocks' :: Ctx (Ctx CrucibleType))
       (r' :: CrucibleType) (c :: Ctx CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
(SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ExecCont p sym ext rtp' f a
continueWith ((SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> SimState
       p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp)))
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> SimState
         p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$ (CallFrame sym ext blocks r ctx
 -> Identity (CallFrame sym ext blocks r (ctx '::> tp)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState
        p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp)))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame ((CallFrame sym ext blocks r ctx
  -> Identity (CallFrame sym ext blocks r (ctx '::> tp)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState
         p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp))))
-> (CallFrame sym ext blocks r ctx
    -> CallFrame sym ext blocks r (ctx '::> tp))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState
     p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp))
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ TypeRepr tp
-> RegValue sym tp
-> StmtSeq ext blocks r (ctx '::> tp)
-> CallFrame sym ext blocks r ctx
-> CallFrame sym ext blocks r (ctx '::> tp)
forall (tp :: CrucibleType) sym ext
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TypeRepr tp
-> RegValue sym tp
-> StmtSeq ext blocks ret (ctx ::> tp)
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret (ctx ::> tp)
extendFrame TypeRepr tp
tp RegValue sym tp
v StmtSeq ext blocks r ctx'
StmtSeq ext blocks r (ctx '::> tp)
rest

         ExtendAssign StmtExtension ext (Reg ctx) tp
estmt -> do
           do let tp :: TypeRepr tp
tp = StmtExtension ext (Reg ctx) tp -> TypeRepr tp
forall (f :: CrucibleType -> Type) (x :: CrucibleType).
StmtExtension ext f x -> TypeRepr x
forall (app :: (CrucibleType -> Type) -> CrucibleType -> Type)
       (f :: CrucibleType -> Type) (x :: CrucibleType).
TypeApp app =>
app f x -> TypeRepr x
appType StmtExtension ext (Reg ctx) tp
estmt
              StmtExtension ext (RegEntry sym) tp
estmt' <- (forall (x :: CrucibleType).
 Reg ctx x
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
      IO
      (RegEntry sym x))
-> forall (x :: CrucibleType).
   StmtExtension ext (Reg ctx) x
   -> ReaderT
        (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
        IO
        (StmtExtension ext (RegEntry sym) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType).
   StmtExtension ext f x -> m (StmtExtension ext g x)
traverseFC Reg ctx x
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegEntry sym x)
forall (x :: CrucibleType).
Reg ctx x
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegEntry sym x)
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegEntry sym tp)
evalReg' StmtExtension ext (Reg ctx) tp
estmt
              (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> IO (ExecState p sym ext rtp))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall r (m :: Type -> Type) a. (r -> m a) -> ReaderT r m a
ReaderT ((SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> IO (ExecState p sym ext rtp))
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> IO (ExecState p sym ext rtp))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$ \SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
s ->
                do (RegValue sym tp
v,SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
s') <- IO
  (RegValue sym tp,
   SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> IO
     (RegValue sym tp,
      SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall a. IO a -> IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO
   (RegValue sym tp,
    SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
 -> IO
      (RegValue sym tp,
       SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> IO
     (RegValue sym tp,
      SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> IO
     (RegValue sym tp,
      SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall a b. (a -> b) -> a -> b
$ ExtensionImpl p sym ext -> EvalStmtFunc p sym ext
forall p sym ext. ExtensionImpl p sym ext -> EvalStmtFunc p sym ext
extensionExec (SimContext p sym ext -> ExtensionImpl p sym ext
forall personality sym ext.
SimContext personality sym ext -> ExtensionImpl personality sym ext
extensionImpl SimContext p sym ext
ctx) StmtExtension ext (RegEntry sym) tp
estmt' SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
s
                   ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT
                     ((SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState
      p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall rtp' (blocks' :: Ctx (Ctx CrucibleType))
       (r' :: CrucibleType) (c :: Ctx CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
(SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ExecCont p sym ext rtp' f a
continueWith ((SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> SimState
       p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp)))
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> SimState
         p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp)))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$ (CallFrame sym ext blocks r ctx
 -> Identity (CallFrame sym ext blocks r (ctx '::> tp)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState
        p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp)))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame ((CallFrame sym ext blocks r ctx
  -> Identity (CallFrame sym ext blocks r (ctx '::> tp)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState
         p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp))))
-> (CallFrame sym ext blocks r ctx
    -> CallFrame sym ext blocks r (ctx '::> tp))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState
     p sym ext rtp (CrucibleLang blocks r) ('Just (ctx '::> tp))
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ TypeRepr tp
-> RegValue sym tp
-> StmtSeq ext blocks r (ctx '::> tp)
-> CallFrame sym ext blocks r ctx
-> CallFrame sym ext blocks r (ctx '::> tp)
forall (tp :: CrucibleType) sym ext
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TypeRepr tp
-> RegValue sym tp
-> StmtSeq ext blocks ret (ctx ::> tp)
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret (ctx ::> tp)
extendFrame TypeRepr tp
tp RegValue sym tp
v StmtSeq ext blocks r ctx'
StmtSeq ext blocks r (ctx '::> tp)
rest)
                     SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
s'

         CallHandle TypeRepr ret
ret_type Reg ctx (FunctionHandleType args ret)
fnExpr CtxRepr args
_types Assignment (Reg ctx) args
arg_exprs ->
           do FnVal sym args ret
hndl <- Reg ctx (FunctionHandleType args ret)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym (FunctionHandleType args ret))
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg Reg ctx (FunctionHandleType args ret)
fnExpr
              RegMap sym args
args <- Assignment (Reg ctx) args
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegMap sym args)
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (args :: Ctx CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Assignment (Reg ctx) args
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym args)
evalArgs Assignment (Reg ctx) args
arg_exprs
              ProgramLoc
loc <- IO ProgramLoc
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     ProgramLoc
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO ProgramLoc
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
      IO
      ProgramLoc)
-> IO ProgramLoc
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     ProgramLoc
forall a b. (a -> b) -> a -> b
$ sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
              FnVal sym args ret
-> RegMap sym args
-> ReturnHandler
     ret p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> ProgramLoc
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall sym (args :: Ctx CrucibleType) (ret :: CrucibleType) p ext
       rtp f (a :: Maybe (Ctx CrucibleType)).
IsExprBuilder sym =>
FnVal sym args ret
-> RegMap sym args
-> ReturnHandler ret p sym ext rtp f a
-> ProgramLoc
-> ExecCont p sym ext rtp f a
callFunction FnVal sym args ret
hndl RegMap sym args
args (TypeRepr ret
-> StmtSeq ext blocks r (ctx '::> ret)
-> ReturnHandler
     ret p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall (ret :: CrucibleType) ext (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (ctx :: Ctx CrucibleType) p sym root.
TypeRepr ret
-> StmtSeq ext blocks r (ctx ::> ret)
-> ReturnHandler
     ret p sym ext root (CrucibleLang blocks r) ('Just ctx)
ReturnToCrucible TypeRepr ret
ret_type StmtSeq ext blocks r ctx'
StmtSeq ext blocks r (ctx '::> ret)
rest) ProgramLoc
loc

         Print Reg ctx (StringType Unicode)
e ->
           do SymExpr sym (BaseStringType Unicode)
msg <- Reg ctx (StringType Unicode)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym (StringType Unicode))
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg Reg ctx (StringType Unicode)
e
              let msg' :: String
msg' = case SymExpr sym (BaseStringType Unicode)
-> Maybe (StringLiteral Unicode)
forall (si :: StringInfo).
SymExpr sym (BaseStringType si) -> Maybe (StringLiteral si)
forall (e :: BaseType -> Type) (si :: StringInfo).
IsExpr e =>
e (BaseStringType si) -> Maybe (StringLiteral si)
asString SymExpr sym (BaseStringType Unicode)
msg of
                           Just (UnicodeLiteral Text
txt) -> Text -> String
Text.unpack Text
txt
                           Maybe (StringLiteral Unicode)
_ -> Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym (BaseStringType Unicode) -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr SymExpr sym (BaseStringType Unicode)
msg)
              IO ()
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO ()
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO ()
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO ())
-> IO ()
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO ()
forall a b. (a -> b) -> a -> b
$ do
                let h :: Handle
h = SimContext p sym ext -> Handle
forall personality sym ext.
SimContext personality sym ext -> Handle
printHandle SimContext p sym ext
ctx
                Handle -> String -> IO ()
hPutStr Handle
h String
msg'
                Handle -> IO ()
hFlush Handle
h
              (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall rtp' (blocks' :: Ctx (Ctx CrucibleType))
       (r' :: CrucibleType) (c :: Ctx CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
(SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ExecCont p sym ext rtp' f a
continueWith ((CallFrame sym ext blocks r ctx
 -> Identity (CallFrame sym ext blocks r ctx))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame  ((CallFrame sym ext blocks r ctx
  -> Identity (CallFrame sym ext blocks r ctx))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> ((StmtSeq ext blocks r ctx
     -> Identity (StmtSeq ext blocks r ctx))
    -> CallFrame sym ext blocks r ctx
    -> Identity (CallFrame sym ext blocks r ctx))
-> (StmtSeq ext blocks r ctx
    -> Identity (StmtSeq ext blocks r ctx))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StmtSeq ext blocks r ctx -> Identity (StmtSeq ext blocks r ctx))
-> CallFrame sym ext blocks r ctx
-> Identity (CallFrame sym ext blocks r ctx)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(StmtSeq ext blocks ret ctx -> f (StmtSeq ext blocks ret ctx))
-> CallFrame sym ext blocks ret ctx
-> f (CallFrame sym ext blocks ret ctx)
frameStmts ((StmtSeq ext blocks r ctx -> Identity (StmtSeq ext blocks r ctx))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> StmtSeq ext blocks r ctx
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ StmtSeq ext blocks r ctx
StmtSeq ext blocks r ctx'
rest)

         Assert Reg ctx BoolType
c_expr Reg ctx (StringType Unicode)
msg_expr ->
           do SymExpr sym BaseBoolType
c <- Reg ctx BoolType
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym BoolType)
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg Reg ctx BoolType
c_expr
              SymExpr sym (BaseStringType Unicode)
msg <- Reg ctx (StringType Unicode)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym (StringType Unicode))
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg Reg ctx (StringType Unicode)
msg_expr
              let err :: SimErrorReason
err = case SymExpr sym (BaseStringType Unicode)
-> Maybe (StringLiteral Unicode)
forall (si :: StringInfo).
SymExpr sym (BaseStringType si) -> Maybe (StringLiteral si)
forall (e :: BaseType -> Type) (si :: StringInfo).
IsExpr e =>
e (BaseStringType si) -> Maybe (StringLiteral si)
asString SymExpr sym (BaseStringType Unicode)
msg of
                           Just (UnicodeLiteral Text
txt) -> String -> String -> SimErrorReason
AssertFailureSimError (Text -> String
Text.unpack Text
txt) String
""
                           Maybe (StringLiteral Unicode)
_ -> String -> String -> SimErrorReason
AssertFailureSimError String
"Symbolic message" (Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym (BaseStringType Unicode) -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr SymExpr sym (BaseStringType Unicode)
msg))
              IO ()
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO ()
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO ()
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO ())
-> IO ()
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO ()
forall a b. (a -> b) -> a -> b
$ bak -> SymExpr sym BaseBoolType -> SimErrorReason -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Pred sym -> SimErrorReason -> IO ()
assert bak
bak SymExpr sym BaseBoolType
c SimErrorReason
err
              (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall rtp' (blocks' :: Ctx (Ctx CrucibleType))
       (r' :: CrucibleType) (c :: Ctx CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
(SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ExecCont p sym ext rtp' f a
continueWith ((CallFrame sym ext blocks r ctx
 -> Identity (CallFrame sym ext blocks r ctx))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame  ((CallFrame sym ext blocks r ctx
  -> Identity (CallFrame sym ext blocks r ctx))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> ((StmtSeq ext blocks r ctx
     -> Identity (StmtSeq ext blocks r ctx))
    -> CallFrame sym ext blocks r ctx
    -> Identity (CallFrame sym ext blocks r ctx))
-> (StmtSeq ext blocks r ctx
    -> Identity (StmtSeq ext blocks r ctx))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StmtSeq ext blocks r ctx -> Identity (StmtSeq ext blocks r ctx))
-> CallFrame sym ext blocks r ctx
-> Identity (CallFrame sym ext blocks r ctx)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(StmtSeq ext blocks ret ctx -> f (StmtSeq ext blocks ret ctx))
-> CallFrame sym ext blocks ret ctx
-> f (CallFrame sym ext blocks ret ctx)
frameStmts ((StmtSeq ext blocks r ctx -> Identity (StmtSeq ext blocks r ctx))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> StmtSeq ext blocks r ctx
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ StmtSeq ext blocks r ctx
StmtSeq ext blocks r ctx'
rest)

         Assume Reg ctx BoolType
c_expr Reg ctx (StringType Unicode)
msg_expr ->
           do SymExpr sym BaseBoolType
c <- Reg ctx BoolType
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym BoolType)
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg Reg ctx BoolType
c_expr
              SymExpr sym (BaseStringType Unicode)
msg <- Reg ctx (StringType Unicode)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym (StringType Unicode))
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg Reg ctx (StringType Unicode)
msg_expr
              let msg' :: String
msg' = case SymExpr sym (BaseStringType Unicode)
-> Maybe (StringLiteral Unicode)
forall (si :: StringInfo).
SymExpr sym (BaseStringType si) -> Maybe (StringLiteral si)
forall (e :: BaseType -> Type) (si :: StringInfo).
IsExpr e =>
e (BaseStringType si) -> Maybe (StringLiteral si)
asString SymExpr sym (BaseStringType Unicode)
msg of
                           Just (UnicodeLiteral Text
txt) -> Text -> String
Text.unpack Text
txt
                           Maybe (StringLiteral Unicode)
_ -> Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym (BaseStringType Unicode) -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr SymExpr sym (BaseStringType Unicode)
msg)
              IO ()
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO ()
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO ()
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO ())
-> IO ()
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO ()
forall a b. (a -> b) -> a -> b
$
                do ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
                   bak -> Assumption sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
addAssumption bak
bak (ProgramLoc -> String -> SymExpr sym BaseBoolType -> Assumption sym
forall (e :: BaseType -> Type).
ProgramLoc -> String -> e BaseBoolType -> CrucibleAssumption e
GenericAssumption ProgramLoc
loc String
msg' SymExpr sym BaseBoolType
c)

              (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall rtp' (blocks' :: Ctx (Ctx CrucibleType))
       (r' :: CrucibleType) (c :: Ctx CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
(SimState p sym ext rtp' f a
 -> SimState p sym ext rtp' (CrucibleLang blocks' r') ('Just c))
-> ExecCont p sym ext rtp' f a
continueWith ((CallFrame sym ext blocks r ctx
 -> Identity (CallFrame sym ext blocks r ctx))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame  ((CallFrame sym ext blocks r ctx
  -> Identity (CallFrame sym ext blocks r ctx))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> ((StmtSeq ext blocks r ctx
     -> Identity (StmtSeq ext blocks r ctx))
    -> CallFrame sym ext blocks r ctx
    -> Identity (CallFrame sym ext blocks r ctx))
-> (StmtSeq ext blocks r ctx
    -> Identity (StmtSeq ext blocks r ctx))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StmtSeq ext blocks r ctx -> Identity (StmtSeq ext blocks r ctx))
-> CallFrame sym ext blocks r ctx
-> Identity (CallFrame sym ext blocks r ctx)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(StmtSeq ext blocks ret ctx -> f (StmtSeq ext blocks ret ctx))
-> CallFrame sym ext blocks ret ctx
-> f (CallFrame sym ext blocks ret ctx)
frameStmts ((StmtSeq ext blocks r ctx -> Identity (StmtSeq ext blocks r ctx))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> StmtSeq ext blocks r ctx
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ StmtSeq ext blocks r ctx
StmtSeq ext blocks r ctx'
rest)


{-# INLINABLE stepTerm #-}

-- | Evaluation operation for evaluating a single block-terminator
--   statement of the Crucible evaluator.
--
--   This is allowed to throw user exceptions or 'SimError'.
stepTerm :: forall p sym ext rtp blocks r ctx.
  (IsSymInterface sym, IsSyntaxExtension ext) =>
  Int {- ^ Verbosity -} ->
  TermStmt blocks r ctx {- ^ Terminating statement to evaluate -} ->
  ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)

stepTerm :: forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (ctx :: Ctx CrucibleType).
(IsSymInterface sym, IsSyntaxExtension ext) =>
Int
-> TermStmt blocks r ctx
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
stepTerm Int
_ (Jump JumpTarget blocks ctx
tgt) =
  ResolvedJump sym blocks
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall sym (blocks :: Ctx (Ctx CrucibleType)) p ext rtp
       (r :: CrucibleType) (a :: Ctx CrucibleType).
IsSymInterface sym =>
ResolvedJump sym blocks
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just a)
jumpToBlock (ResolvedJump sym blocks
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (ResolvedJump sym blocks)
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< JumpTarget blocks ctx
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (ResolvedJump sym blocks)
forall sym (m :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType) p ext rtp (r :: CrucibleType).
(IsSymInterface sym, Monad m) =>
JumpTarget blocks ctx
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx)
     m
     (ResolvedJump sym blocks)
evalJumpTarget JumpTarget blocks ctx
tgt

stepTerm Int
_ (Return Reg ctx r
arg) =
  RegEntry sym r
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
RegEntry sym (FrameRetType (CrucibleLang blocks r))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
RegEntry sym (FrameRetType f) -> ExecCont p sym ext rtp f args
returnValue (RegEntry sym r
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegEntry sym r)
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Reg ctx r
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegEntry sym r)
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegEntry sym tp)
evalReg' Reg ctx r
arg

stepTerm Int
_ (Br Reg ctx BoolType
c JumpTarget blocks ctx
x JumpTarget blocks ctx
y) =
  do ResolvedJump sym blocks
x_jump <- JumpTarget blocks ctx
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (ResolvedJump sym blocks)
forall sym (m :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType) p ext rtp (r :: CrucibleType).
(IsSymInterface sym, Monad m) =>
JumpTarget blocks ctx
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx)
     m
     (ResolvedJump sym blocks)
evalJumpTarget JumpTarget blocks ctx
x
     ResolvedJump sym blocks
y_jump <- JumpTarget blocks ctx
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (ResolvedJump sym blocks)
forall sym (m :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType) p ext rtp (r :: CrucibleType).
(IsSymInterface sym, Monad m) =>
JumpTarget blocks ctx
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx)
     m
     (ResolvedJump sym blocks)
evalJumpTarget JumpTarget blocks ctx
y
     SymExpr sym BaseBoolType
p <- Reg ctx BoolType
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym BoolType)
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg Reg ctx BoolType
c
     SymExpr sym BaseBoolType
-> ResolvedJump sym blocks
-> ResolvedJump sym blocks
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall sym ext (blocks :: Ctx (Ctx CrucibleType)) p rtp
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
(IsSymInterface sym, IsSyntaxExtension ext) =>
Pred sym
-> ResolvedJump sym blocks
-> ResolvedJump sym blocks
-> ExecCont p sym ext rtp (CrucibleLang blocks ret) ('Just ctx)
conditionalBranch SymExpr sym BaseBoolType
p ResolvedJump sym blocks
x_jump ResolvedJump sym blocks
y_jump

stepTerm Int
_ (MaybeBranch TypeRepr tp
tp Reg ctx (MaybeType tp)
e SwitchTarget blocks ctx tp
j JumpTarget blocks ctx
n) =
  do Reg ctx (MaybeType tp)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym (MaybeType tp))
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg Reg ctx (MaybeType tp)
e ReaderT
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
  IO
  (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp))
-> (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
    -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b.
ReaderT
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
-> (a
    -> ReaderT
         (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO b)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
       PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
Unassigned -> ResolvedJump sym blocks
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall sym (blocks :: Ctx (Ctx CrucibleType)) p ext rtp
       (r :: CrucibleType) (a :: Ctx CrucibleType).
IsSymInterface sym =>
ResolvedJump sym blocks
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just a)
jumpToBlock (ResolvedJump sym blocks
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (ResolvedJump sym blocks)
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< JumpTarget blocks ctx
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (ResolvedJump sym blocks)
forall sym (m :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType) p ext rtp (r :: CrucibleType).
(IsSymInterface sym, Monad m) =>
JumpTarget blocks ctx
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx)
     m
     (ResolvedJump sym blocks)
evalJumpTarget JumpTarget blocks ctx
n
       PE SymExpr sym BaseBoolType
p RegValue sym tp
v ->
         do ResolvedJump sym blocks
j_jump <- SwitchTarget blocks ctx tp
-> RegEntry sym tp
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (ResolvedJump sym blocks)
forall sym (m :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType) (tp :: CrucibleType) p ext rtp
       (r :: CrucibleType).
(IsSymInterface sym, Monad m) =>
SwitchTarget blocks ctx tp
-> RegEntry sym tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx)
     m
     (ResolvedJump sym blocks)
evalSwitchTarget SwitchTarget blocks ctx tp
j (TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr tp
tp RegValue sym tp
v)
            ResolvedJump sym blocks
n_jump <- JumpTarget blocks ctx
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (ResolvedJump sym blocks)
forall sym (m :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType) p ext rtp (r :: CrucibleType).
(IsSymInterface sym, Monad m) =>
JumpTarget blocks ctx
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx)
     m
     (ResolvedJump sym blocks)
evalJumpTarget JumpTarget blocks ctx
n
            SymExpr sym BaseBoolType
-> ResolvedJump sym blocks
-> ResolvedJump sym blocks
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall sym ext (blocks :: Ctx (Ctx CrucibleType)) p rtp
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
(IsSymInterface sym, IsSyntaxExtension ext) =>
Pred sym
-> ResolvedJump sym blocks
-> ResolvedJump sym blocks
-> ExecCont p sym ext rtp (CrucibleLang blocks ret) ('Just ctx)
conditionalBranch SymExpr sym BaseBoolType
p ResolvedJump sym blocks
j_jump ResolvedJump sym blocks
n_jump

stepTerm Int
_ (VariantElim CtxRepr varctx
ctx Reg ctx (VariantType varctx)
e Assignment (SwitchTarget blocks ctx) varctx
cases) =
  do Assignment (VariantBranch sym) varctx
vs <- Reg ctx (VariantType varctx)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym (VariantType varctx))
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg Reg ctx (VariantType varctx)
e
     [(SymExpr sym BaseBoolType, ResolvedJump sym blocks)]
jmps <- CtxRepr varctx
ctx CtxRepr varctx
-> (CtxRepr varctx
    -> ReaderT
         (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
         IO
         [(SymExpr sym BaseBoolType, ResolvedJump sym blocks)])
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     [(SymExpr sym BaseBoolType, ResolvedJump sym blocks)]
forall a b. a -> (a -> b) -> b
& (forall (tp :: CrucibleType).
 Index varctx tp
 -> TypeRepr tp
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
      IO
      [(SymExpr sym BaseBoolType, ResolvedJump sym blocks)])
-> CtxRepr varctx
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     [(SymExpr sym BaseBoolType, ResolvedJump sym blocks)]
forall {k} w (m :: Type -> Type) (ctx :: Ctx k) (f :: k -> Type).
(Monoid w, Applicative m) =>
(forall (tp :: k). Index ctx tp -> f tp -> m w)
-> Assignment f ctx -> m w
Ctx.traverseAndCollect (\Index varctx tp
i TypeRepr tp
tp ->
                case Assignment (VariantBranch sym) varctx
vs Assignment (VariantBranch sym) varctx
-> Index varctx tp -> VariantBranch sym tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index varctx tp
i of
                  VB PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
Unassigned ->
                    [(SymExpr sym BaseBoolType, ResolvedJump sym blocks)]
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     [(SymExpr sym BaseBoolType, ResolvedJump sym blocks)]
forall a.
a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return []
                  VB (PE SymExpr sym BaseBoolType
p RegValue sym tp
v) ->
                    do ResolvedJump sym blocks
jmp <- SwitchTarget blocks ctx tp
-> RegEntry sym tp
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (ResolvedJump sym blocks)
forall sym (m :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType) (tp :: CrucibleType) p ext rtp
       (r :: CrucibleType).
(IsSymInterface sym, Monad m) =>
SwitchTarget blocks ctx tp
-> RegEntry sym tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx)
     m
     (ResolvedJump sym blocks)
evalSwitchTarget (Assignment (SwitchTarget blocks ctx) varctx
cases Assignment (SwitchTarget blocks ctx) varctx
-> Index varctx tp -> SwitchTarget blocks ctx tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index varctx tp
i) (TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr tp
tp RegValue sym tp
v)
                       [(SymExpr sym BaseBoolType, ResolvedJump sym blocks)]
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     [(SymExpr sym BaseBoolType, ResolvedJump sym blocks)]
forall a.
a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return [(SymExpr sym BaseBoolType
p,ResolvedJump sym blocks
jmp)])

     [(SymExpr sym BaseBoolType, ResolvedJump sym blocks)]
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall sym (blocks :: Ctx (Ctx CrucibleType)) p ext rtp
       (r :: CrucibleType) (ctx :: Ctx CrucibleType).
IsSymInterface sym =>
[(Pred sym, ResolvedJump sym blocks)]
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
variantCases [(SymExpr sym BaseBoolType, ResolvedJump sym blocks)]
jmps

-- When we make a tail call, we first try to unwind our calling context
-- and replace the currently-active frame with the frame of the new called
-- function.  However, this is only successful if there are no pending
-- symbolic merges.
--
-- If there _are_ pending merges we instead treat the tail call as normal
-- call-then-return sequence, pushing a new call frame on the top of our
-- current context (rather than replacing it).  The TailReturnToCrucible
-- return handler tells the simulator to immediately invoke another return
-- in the caller, which is still present on the stack in this scenario.
stepTerm Int
_ (TailCall Reg ctx (FunctionHandleType args r)
fnExpr CtxRepr args
_types Assignment (Reg ctx) args
arg_exprs) =
  do FnVal sym args r
cl   <- Reg ctx (FunctionHandleType args r)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym (FunctionHandleType args r))
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg Reg ctx (FunctionHandleType args r)
fnExpr
     RegMap sym args
args <- Assignment (Reg ctx) args
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegMap sym args)
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (args :: Ctx CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Assignment (Reg ctx) args
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegMap sym args)
evalArgs Assignment (Reg ctx) args
arg_exprs
     ValueFromFrame p sym ext rtp (CrucibleLang blocks r)
ctx <- Getting
  (ValueFromFrame p sym ext rtp (CrucibleLang blocks r))
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
  (ValueFromFrame p sym ext rtp (CrucibleLang blocks r))
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (ValueFromFrame p sym ext rtp (CrucibleLang blocks r))
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view ((ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Const
      (ValueFromFrame p sym ext rtp (CrucibleLang blocks r))
      (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Const
     (ValueFromFrame p sym ext rtp (CrucibleLang blocks r))
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
stateTree((ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  -> Const
       (ValueFromFrame p sym ext rtp (CrucibleLang blocks r))
       (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
 -> Const
      (ValueFromFrame p sym ext rtp (CrucibleLang blocks r))
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> ((ValueFromFrame p sym ext rtp (CrucibleLang blocks r)
     -> Const
          (ValueFromFrame p sym ext rtp (CrucibleLang blocks r))
          (ValueFromFrame p sym ext rtp (CrucibleLang blocks r)))
    -> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
    -> Const
         (ValueFromFrame p sym ext rtp (CrucibleLang blocks r))
         (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)))
-> Getting
     (ValueFromFrame p sym ext rtp (CrucibleLang blocks r))
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     (ValueFromFrame p sym ext rtp (CrucibleLang blocks r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(ValueFromFrame p sym ext rtp (CrucibleLang blocks r)
 -> Const
      (ValueFromFrame p sym ext rtp (CrucibleLang blocks r))
      (ValueFromFrame p sym ext rtp (CrucibleLang blocks r)))
-> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> Const
     (ValueFromFrame p sym ext rtp (CrucibleLang blocks r))
     (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(ValueFromFrame p sym ext root f1
 -> f2 (ValueFromFrame p sym ext root f1))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args)
actContext)
     sym
sym <- Getting
  sym
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
  sym
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO sym
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting
  sym
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
  sym
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(sym -> f2 sym)
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateSymInterface
     ProgramLoc
loc <- IO ProgramLoc
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     ProgramLoc
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO ProgramLoc
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
      IO
      ProgramLoc)
-> IO ProgramLoc
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     ProgramLoc
forall a b. (a -> b) -> a -> b
$ sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
     case ValueFromFrame p sym ext rtp (CrucibleLang blocks r)
-> Maybe
     (ValueFromValue
        p sym ext rtp (FrameRetType (CrucibleLang blocks r)))
forall p sym ext root f.
ValueFromFrame p sym ext root f
-> Maybe (ValueFromValue p sym ext root (FrameRetType f))
unwindContext ValueFromFrame p sym ext rtp (CrucibleLang blocks r)
ctx of
       Just ValueFromValue p sym ext rtp (FrameRetType (CrucibleLang blocks r))
vfv -> FnVal sym args r
-> RegMap sym args
-> ValueFromValue p sym ext rtp r
-> ProgramLoc
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall f (ret :: CrucibleType) sym (args :: Ctx CrucibleType) p ext
       rtp (a :: Maybe (Ctx CrucibleType)).
(FrameRetType f ~ ret) =>
FnVal sym args ret
-> RegMap sym args
-> ValueFromValue p sym ext rtp ret
-> ProgramLoc
-> ExecCont p sym ext rtp f a
tailCallFunction FnVal sym args r
cl RegMap sym args
args ValueFromValue p sym ext rtp r
ValueFromValue p sym ext rtp (FrameRetType (CrucibleLang blocks r))
vfv ProgramLoc
loc
       Maybe
  (ValueFromValue
     p sym ext rtp (FrameRetType (CrucibleLang blocks r)))
Nothing  -> FnVal sym args r
-> RegMap sym args
-> ReturnHandler
     r p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
-> ProgramLoc
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall sym (args :: Ctx CrucibleType) (ret :: CrucibleType) p ext
       rtp f (a :: Maybe (Ctx CrucibleType)).
IsExprBuilder sym =>
FnVal sym args ret
-> RegMap sym args
-> ReturnHandler ret p sym ext rtp f a
-> ProgramLoc
-> ExecCont p sym ext rtp f a
callFunction FnVal sym args r
cl RegMap sym args
args ReturnHandler r p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall (ret :: CrucibleType) (r :: CrucibleType) p sym ext root
       (blocks :: Ctx (Ctx CrucibleType))
       (args :: Maybe (Ctx CrucibleType)).
(ret ~ r) =>
ReturnHandler ret p sym ext root (CrucibleLang blocks r) args
TailReturnToCrucible ProgramLoc
loc

stepTerm Int
_ (ErrorStmt Reg ctx (StringType Unicode)
msg) =
  do SymExpr sym (BaseStringType Unicode)
msg' <- Reg ctx (StringType Unicode)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (RegValue sym (StringType Unicode))
forall (m :: Type -> Type) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) p sym ext rtp
       (blocks :: Ctx (Ctx CrucibleType)) (r :: CrucibleType).
Monad m =>
Reg ctx tp
-> ReaderT
     (CrucibleState p sym ext rtp blocks r ctx) m (RegValue sym tp)
evalReg Reg ctx (StringType Unicode)
msg
     SimContext p sym ext
simCtx <- Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
  (SimContext p sym ext)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (SimContext p sym ext)
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
  (SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext
     SimContext p sym ext
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend SimContext p sym ext
simCtx ((forall {bak}.
  IsSymBackend sym bak =>
  bak -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$ \bak
bak -> IO (ExecState p sym ext rtp)
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (ExecState p sym ext rtp)
 -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
-> IO (ExecState p sym ext rtp)
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall a b. (a -> b) -> a -> b
$
       case SymExpr sym (BaseStringType Unicode)
-> Maybe (StringLiteral Unicode)
forall (si :: StringInfo).
SymExpr sym (BaseStringType si) -> Maybe (StringLiteral si)
forall (e :: BaseType -> Type) (si :: StringInfo).
IsExpr e =>
e (BaseStringType si) -> Maybe (StringLiteral si)
asString SymExpr sym (BaseStringType Unicode)
msg' of
         Just (UnicodeLiteral Text
txt) ->
                     bak -> SimErrorReason -> IO (ExecState p sym ext rtp)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak
                        (SimErrorReason -> IO (ExecState p sym ext rtp))
-> SimErrorReason -> IO (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ String -> SimErrorReason
GenericSimError (String -> SimErrorReason) -> String -> SimErrorReason
forall a b. (a -> b) -> a -> b
$ Text -> String
Text.unpack Text
txt
         Maybe (StringLiteral Unicode)
Nothing  -> bak -> SimErrorReason -> IO (ExecState p sym ext rtp)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak
                        (SimErrorReason -> IO (ExecState p sym ext rtp))
-> SimErrorReason -> IO (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ String -> SimErrorReason
GenericSimError (String -> SimErrorReason) -> String -> SimErrorReason
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym (BaseStringType Unicode) -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr SymExpr sym (BaseStringType Unicode)
msg')


-- | Checks whether the StmtSeq is a Cons or a Term,
--   to give callers another chance to jump into Crucible's control flow
checkConsTerm ::
  (IsSymInterface sym, IsSyntaxExtension ext) =>
  Int {- ^ Current verbosity -} ->
  ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
checkConsTerm :: forall sym ext p rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (ctx :: Ctx CrucibleType).
(IsSymInterface sym, IsSyntaxExtension ext) =>
Int -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
checkConsTerm Int
verb =
     do CallFrame sym ext blocks r ctx
cf <- Getting
  (CallFrame sym ext blocks r ctx)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
  (CallFrame sym ext blocks r ctx)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (CallFrame sym ext blocks r ctx)
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting
  (CallFrame sym ext blocks r ctx)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
  (CallFrame sym ext blocks r ctx)
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame

        case CallFrame sym ext blocks r ctx
cfCallFrame sym ext blocks r ctx
-> Getting
     (StmtSeq ext blocks r ctx)
     (CallFrame sym ext blocks r ctx)
     (StmtSeq ext blocks r ctx)
-> StmtSeq ext blocks r ctx
forall s a. s -> Getting a s a -> a
^.Getting
  (StmtSeq ext blocks r ctx)
  (CallFrame sym ext blocks r ctx)
  (StmtSeq ext blocks r ctx)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(StmtSeq ext blocks ret ctx -> f (StmtSeq ext blocks ret ctx))
-> CallFrame sym ext blocks ret ctx
-> f (CallFrame sym ext blocks ret ctx)
frameStmts of
          ConsStmt ProgramLoc
_ Stmt ext ctx ctx'
_ StmtSeq ext blocks r ctx'
_ -> Int -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall sym ext p rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (ctx :: Ctx CrucibleType).
(IsSymInterface sym, IsSyntaxExtension ext) =>
Int -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
stepBasicBlock Int
verb
          TermStmt ProgramLoc
_ TermStmt blocks r ctx
_ -> RunningStateInfo blocks ctx
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall (blocks :: Ctx (Ctx CrucibleType)) (a :: Ctx CrucibleType) p
       sym ext rtp (r :: CrucibleType).
RunningStateInfo blocks a
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just a)
continue (Some (BlockID blocks) -> RunningStateInfo blocks ctx
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
Some (BlockID blocks) -> RunningStateInfo blocks args
RunBlockEnd (CallFrame sym ext blocks r ctx
cfCallFrame sym ext blocks r ctx
-> Getting
     (Some (BlockID blocks))
     (CallFrame sym ext blocks r ctx)
     (Some (BlockID blocks))
-> Some (BlockID blocks)
forall s a. s -> Getting a s a -> a
^.Getting
  (Some (BlockID blocks))
  (CallFrame sym ext blocks r ctx)
  (Some (BlockID blocks))
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(Some (BlockID blocks) -> f (Some (BlockID blocks)))
-> CallFrame sym ext blocks ret ctx
-> f (CallFrame sym ext blocks ret ctx)
frameBlockID))

-- | Main evaluation operation for running a single step of
--   basic block evaluation.
--
--   This is allowed to throw user exceptions or 'SimError'.
stepBasicBlock ::
  (IsSymInterface sym, IsSyntaxExtension ext) =>
  Int {- ^ Current verbosity -} ->
  ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
stepBasicBlock :: forall sym ext p rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (ctx :: Ctx CrucibleType).
(IsSymInterface sym, IsSyntaxExtension ext) =>
Int -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
stepBasicBlock Int
verb =
  do SimContext p sym ext
ctx <- Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
  (SimContext p sym ext)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (SimContext p sym ext)
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
  (SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext
     let sym :: sym
sym = SimContext p sym ext
ctxSimContext p sym ext
-> Getting sym (SimContext p sym ext) sym -> sym
forall s a. s -> Getting a s a -> a
^.Getting sym (SimContext p sym ext) sym
forall p sym ext (f :: Type -> Type).
(Contravariant f, Functor f) =>
(sym -> f sym) -> SimContext p sym ext -> f (SimContext p sym ext)
ctxSymInterface
     let h :: Handle
h = SimContext p sym ext -> Handle
forall personality sym ext.
SimContext personality sym ext -> Handle
printHandle SimContext p sym ext
ctx
     CallFrame sym ext blocks r ctx
cf <- Getting
  (CallFrame sym ext blocks r ctx)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
  (CallFrame sym ext blocks r ctx)
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
     IO
     (CallFrame sym ext blocks r ctx)
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting
  (CallFrame sym ext blocks r ctx)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx))
  (CallFrame sym ext blocks r ctx)
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
stateCrucibleFrame

     case CallFrame sym ext blocks r ctx
cfCallFrame sym ext blocks r ctx
-> Getting
     (StmtSeq ext blocks r ctx)
     (CallFrame sym ext blocks r ctx)
     (StmtSeq ext blocks r ctx)
-> StmtSeq ext blocks r ctx
forall s a. s -> Getting a s a -> a
^.Getting
  (StmtSeq ext blocks r ctx)
  (CallFrame sym ext blocks r ctx)
  (StmtSeq ext blocks r ctx)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(StmtSeq ext blocks ret ctx -> f (StmtSeq ext blocks ret ctx))
-> CallFrame sym ext blocks ret ctx
-> f (CallFrame sym ext blocks ret ctx)
frameStmts of
       ConsStmt ProgramLoc
pl Stmt ext ctx ctx'
stmt StmtSeq ext blocks r ctx'
rest ->
         do IO ()
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO ()
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO ()
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO ())
-> IO ()
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO ()
forall a b. (a -> b) -> a -> b
$
              do sym -> ProgramLoc -> IO ()
forall sym. IsExprBuilder sym => sym -> ProgramLoc -> IO ()
setCurrentProgramLoc sym
sym ProgramLoc
pl
                 let sz :: Size ctx
sz = RegMap sym ctx -> Size ctx
forall sym (ctx :: Ctx CrucibleType). RegMap sym ctx -> Size ctx
regMapSize (CallFrame sym ext blocks r ctx
cfCallFrame sym ext blocks r ctx
-> Getting
     (RegMap sym ctx) (CallFrame sym ext blocks r ctx) (RegMap sym ctx)
-> RegMap sym ctx
forall s a. s -> Getting a s a -> a
^.Getting
  (RegMap sym ctx) (CallFrame sym ext blocks r ctx) (RegMap sym ctx)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args))
-> CallFrame sym ext blocks ret args
-> f (CallFrame sym ext blocks ret args)
frameRegs)
                 Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Int
verb Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
4) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Handle -> SomeHandle -> ProgramLoc -> Doc Any -> IO ()
forall ann. Handle -> SomeHandle -> ProgramLoc -> Doc ann -> IO ()
ppStmtAndLoc Handle
h (CallFrame sym ext blocks r ctx -> 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 r ctx
cf) ProgramLoc
pl (Size ctx -> Stmt ext ctx ctx' -> Doc Any
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       ann.
PrettyExt ext =>
Size ctx -> Stmt ext ctx ctx' -> Doc ann
ppStmt Size ctx
sz Stmt ext ctx ctx'
stmt)
            Int
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks r ctx'
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (ctx :: Ctx CrucibleType)
       (ctx' :: Ctx CrucibleType).
(IsSymInterface sym, IsSyntaxExtension ext) =>
Int
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks r ctx'
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
stepStmt Int
verb Stmt ext ctx ctx'
stmt StmtSeq ext blocks r ctx'
rest

       TermStmt ProgramLoc
pl TermStmt blocks r ctx
termStmt -> do
         do IO ()
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO ()
forall a.
IO a
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO ()
 -> ReaderT
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO ())
-> IO ()
-> ReaderT
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just ctx)) IO ()
forall a b. (a -> b) -> a -> b
$
              do sym -> ProgramLoc -> IO ()
forall sym. IsExprBuilder sym => sym -> ProgramLoc -> IO ()
setCurrentProgramLoc sym
sym ProgramLoc
pl
                 Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Int
verb Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
4) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Handle -> SomeHandle -> ProgramLoc -> Doc Any -> IO ()
forall ann. Handle -> SomeHandle -> ProgramLoc -> Doc ann -> IO ()
ppStmtAndLoc Handle
h (CallFrame sym ext blocks r ctx -> 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 r ctx
cf) ProgramLoc
pl (TermStmt blocks r ctx -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. TermStmt blocks r ctx -> Doc ann
pretty TermStmt blocks r ctx
termStmt)
            Int
-> TermStmt blocks r ctx
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (ctx :: Ctx CrucibleType).
(IsSymInterface sym, IsSyntaxExtension ext) =>
Int
-> TermStmt blocks r ctx
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
stepTerm Int
verb TermStmt blocks r ctx
termStmt

ppStmtAndLoc :: Handle -> SomeHandle -> ProgramLoc -> Doc ann -> IO ()
ppStmtAndLoc :: forall ann. Handle -> SomeHandle -> ProgramLoc -> Doc ann -> IO ()
ppStmtAndLoc Handle
h SomeHandle
sh ProgramLoc
pl Doc ann
stmt = do
  Handle -> Doc ann -> IO ()
forall a. Show a => Handle -> a -> IO ()
hPrint Handle
h (Doc ann -> IO ()) -> Doc ann -> IO ()
forall a b. (a -> b) -> a -> b
$
    [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [ SomeHandle -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow SomeHandle
sh Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
':'
         , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc ann
stmt Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"%" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Position -> Doc ann
forall ann. Position -> Doc ann
ppNoFileName (ProgramLoc -> Position
plSourceLoc ProgramLoc
pl)) ]
  Handle -> IO ()
hFlush Handle
h

performStateRun ::
  (IsSymInterface sym, IsSyntaxExtension ext) =>
  RunningStateInfo blocks ctx ->
  Int {- ^ Current verbosity -} ->
  ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
performStateRun :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType) p rtp (r :: CrucibleType).
(IsSymInterface sym, IsSyntaxExtension ext) =>
RunningStateInfo blocks ctx
-> Int
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
performStateRun RunningStateInfo blocks ctx
info Int
verb = case RunningStateInfo blocks ctx
info of
  RunPostBranchMerge BlockID blocks ctx
bid -> RunningStateInfo blocks ctx
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall (blocks :: Ctx (Ctx CrucibleType)) (a :: Ctx CrucibleType) p
       sym ext rtp (r :: CrucibleType).
RunningStateInfo blocks a
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just a)
continue (BlockID blocks ctx -> RunningStateInfo blocks ctx
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
BlockID blocks args -> RunningStateInfo blocks args
RunBlockStart BlockID blocks ctx
bid)
  RunningStateInfo blocks ctx
_ -> Int -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
forall sym ext p rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (ctx :: Ctx CrucibleType).
(IsSymInterface sym, IsSyntaxExtension ext) =>
Int -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
stepBasicBlock Int
verb


----------------------------------------------------------------------
-- ExecState manipulations


-- | Given an 'ExecState', examine it and either enter the continuation
--   for final results, or construct the appropriate 'ExecCont' for
--   continuing the computation and enter the provided intermediate continuation.
dispatchExecState ::
  (IsSymInterface sym, IsSyntaxExtension ext) =>
  IO Int {- ^ Action to query the current verbosity -} ->
  ExecState p sym ext rtp {- ^ Current execution state of the simulator -} ->
  (ExecResult p sym ext rtp -> IO z) {- ^ Final continuation for results -} ->
  (forall f a. ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z)
    {- ^ Intermediate continuation for running states -} ->
  IO z
dispatchExecState :: forall sym ext p rtp z.
(IsSymInterface sym, IsSyntaxExtension ext) =>
IO Int
-> ExecState p sym ext rtp
-> (ExecResult p sym ext rtp -> IO z)
-> (forall f (a :: Maybe (Ctx CrucibleType)).
    ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z)
-> IO z
dispatchExecState IO Int
getVerb ExecState p sym ext rtp
exst ExecResult p sym ext rtp -> IO z
kresult forall f (a :: Maybe (Ctx CrucibleType)).
ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
k =
  case ExecState p sym ext rtp
exst of
    ResultState ExecResult p sym ext rtp
res ->
      ExecResult p sym ext rtp -> IO z
kresult ExecResult p sym ext rtp
res

    InitialState SimContext p sym ext
simctx SymGlobalState sym
globals AbortHandler p sym ext (RegEntry sym ret)
ah TypeRepr ret
ret ExecCont
  p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
cont ->
      do SimState
  p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
st <- 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 EmptyCtx))
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 EmptyCtx))
initSimState SimContext p sym ext
simctx SymGlobalState sym
globals AbortHandler p sym ext (RegEntry sym ret)
ah TypeRepr ret
ret
         ExecCont p sym ext rtp (OverrideLang ret) ('Just EmptyCtx)
-> SimState p sym ext rtp (OverrideLang ret) ('Just EmptyCtx)
-> IO z
forall f (a :: Maybe (Ctx CrucibleType)).
ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
k ExecCont p sym ext rtp (OverrideLang ret) ('Just EmptyCtx)
ExecCont
  p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
cont SimState p sym ext rtp (OverrideLang ret) ('Just EmptyCtx)
SimState
  p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
st

    AbortState AbortExecReason
rsn SimState p sym ext rtp f a
st ->
      let (AH forall l (args :: Maybe (Ctx CrucibleType)).
AbortExecReason -> ExecCont p sym ext rtp l args
handler) = SimState p sym ext rtp f a
stSimState p sym ext rtp f a
-> Getting
     (AbortHandler p sym ext rtp)
     (SimState p sym ext rtp f a)
     (AbortHandler p sym ext rtp)
-> AbortHandler p sym ext rtp
forall s a. s -> Getting a s a -> a
^.Getting
  (AbortHandler p sym ext rtp)
  (SimState p sym ext rtp f a)
  (AbortHandler p sym ext rtp)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(AbortHandler p sym ext r -> f2 (AbortHandler p sym ext r))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
abortHandler in
      ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
forall f (a :: Maybe (Ctx CrucibleType)).
ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
k (AbortExecReason -> ExecCont p sym ext rtp f a
forall l (args :: Maybe (Ctx CrucibleType)).
AbortExecReason -> ExecCont p sym ext rtp l args
handler AbortExecReason
rsn) SimState p sym ext rtp f a
st

    OverrideState Override p sym ext args ret
ovr SimState p sym ext rtp (OverrideLang ret) ('Just args)
st ->
      ExecCont p sym ext rtp (OverrideLang ret) ('Just args)
-> SimState p sym ext rtp (OverrideLang ret) ('Just args) -> IO z
forall f (a :: Maybe (Ctx CrucibleType)).
ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
k (Override p sym ext args ret
-> forall r. ExecCont p sym ext r (OverrideLang ret) ('Just args)
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 args)
overrideHandler Override p sym ext args ret
ovr) SimState p sym ext rtp (OverrideLang ret) ('Just args)
st

    SymbolicBranchState Pred sym
p PausedFrame p sym ext rtp f
a_frame PausedFrame p sym ext rtp f
o_frame CrucibleBranchTarget f postdom_args
tgt SimState p sym ext rtp f ('Just args)
st ->
      ExecCont p sym ext rtp f ('Just args)
-> SimState p sym ext rtp f ('Just args) -> IO z
forall f (a :: Maybe (Ctx CrucibleType)).
ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
k (Pred sym
-> PausedFrame p sym ext rtp f
-> PausedFrame p sym ext rtp f
-> CrucibleBranchTarget f postdom_args
-> ExecCont p sym ext rtp f ('Just args)
forall sym p ext rtp f (args :: Maybe (Ctx CrucibleType))
       (dc_args :: Ctx CrucibleType).
IsSymInterface sym =>
Pred sym
-> PausedFrame p sym ext rtp f
-> PausedFrame p sym ext rtp f
-> CrucibleBranchTarget f args
-> ExecCont p sym ext rtp f ('Just dc_args)
performIntraFrameSplit Pred sym
p PausedFrame p sym ext rtp f
a_frame PausedFrame p sym ext rtp f
o_frame CrucibleBranchTarget f postdom_args
tgt) SimState p sym ext rtp f ('Just args)
st

    ControlTransferState ControlResumption p sym ext rtp f
resumption SimState p sym ext rtp f ('Just a)
st ->
      ExecCont p sym ext rtp f ('Just a)
-> SimState p sym ext rtp f ('Just a) -> IO z
forall f (a :: Maybe (Ctx CrucibleType)).
ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
k (ControlResumption p sym ext rtp f
-> ExecCont p sym ext rtp f ('Just a)
forall sym p ext rtp f (a :: Ctx CrucibleType).
IsSymInterface sym =>
ControlResumption p sym ext rtp f
-> ExecCont p sym ext rtp f ('Just a)
performControlTransfer ControlResumption p sym ext rtp f
resumption) SimState p sym ext rtp f ('Just a)
st

    BranchMergeState CrucibleBranchTarget f args
tgt SimState p sym ext rtp f args
st ->
      ExecCont p sym ext rtp f args
-> SimState p sym ext rtp f args -> IO z
forall f (a :: Maybe (Ctx CrucibleType)).
ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
k (CrucibleBranchTarget f args -> ExecCont p sym ext rtp f args
forall sym f (args :: Maybe (Ctx CrucibleType)) p ext root.
IsSymInterface sym =>
CrucibleBranchTarget f args -> ExecCont p sym ext root f args
performIntraFrameMerge CrucibleBranchTarget f args
tgt) SimState p sym ext rtp f args
st

    UnwindCallState ValueFromValue p sym ext rtp r
vfv AbortedResult sym ext
ar SimState p sym ext rtp f a
st ->
      ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
forall f (a :: Maybe (Ctx CrucibleType)).
ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
k (ValueFromValue p sym ext rtp r
-> AbortedResult sym ext -> ExecCont p sym ext rtp f a
forall sym p ext r (ret' :: CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
IsSymInterface sym =>
ValueFromValue p sym ext r ret'
-> AbortedResult sym ext -> ExecCont p sym ext r f a
resumeValueFromValueAbort ValueFromValue p sym ext rtp r
vfv AbortedResult sym ext
ar) SimState p sym ext rtp f a
st

    CallState ReturnHandler ret p sym ext rtp f a
retHandler ResolvedCall p sym ext ret
frm SimState p sym ext rtp f a
st ->
      ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
forall f (a :: Maybe (Ctx CrucibleType)).
ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
k (ReturnHandler ret p sym ext rtp f a
-> ResolvedCall p sym ext ret -> ExecCont p sym ext rtp f a
forall sym (ret :: CrucibleType) p ext rtp outer_frame
       (outer_args :: Maybe (Ctx CrucibleType)).
IsSymInterface sym =>
ReturnHandler ret p sym ext rtp outer_frame outer_args
-> ResolvedCall p sym ext ret
-> ExecCont p sym ext rtp outer_frame outer_args
performFunctionCall ReturnHandler ret p sym ext rtp f a
retHandler ResolvedCall p sym ext ret
frm) SimState p sym ext rtp f a
st

    TailCallState ValueFromValue p sym ext rtp ret
vfv ResolvedCall p sym ext ret
frm SimState p sym ext rtp f a
st ->
      ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
forall f (a :: Maybe (Ctx CrucibleType)).
ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
k (ValueFromValue p sym ext rtp ret
-> ResolvedCall p sym ext ret -> ExecCont p sym ext rtp f a
forall sym p ext rtp (ret :: CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
IsSymInterface sym =>
ValueFromValue p sym ext rtp ret
-> ResolvedCall p sym ext ret -> ExecCont p sym ext rtp f a
performTailCall ValueFromValue p sym ext rtp ret
vfv ResolvedCall p sym ext ret
frm) SimState p sym ext rtp f a
st

    ReturnState FunctionName
fnm ValueFromValue p sym ext rtp ret
vfv RegEntry sym ret
ret SimState p sym ext rtp f a
st ->
      ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
forall f (a :: Maybe (Ctx CrucibleType)).
ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
k (FunctionName
-> ValueFromValue p sym ext rtp ret
-> RegEntry sym ret
-> ExecCont p sym ext rtp f a
forall sym p ext r (ret :: CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
IsSymInterface sym =>
FunctionName
-> ValueFromValue p sym ext r ret
-> RegEntry sym ret
-> ExecCont p sym ext r f a
performReturn FunctionName
fnm ValueFromValue p sym ext rtp ret
vfv RegEntry sym ret
ret) SimState p sym ext rtp f a
st

    RunningState RunningStateInfo blocks args
info SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st ->
      do Int
v <- IO Int
getVerb
         ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> IO z
forall f (a :: Maybe (Ctx CrucibleType)).
ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z
k (RunningStateInfo blocks args
-> Int
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just args)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType) p rtp (r :: CrucibleType).
(IsSymInterface sym, IsSyntaxExtension ext) =>
RunningStateInfo blocks ctx
-> Int
-> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
performStateRun RunningStateInfo blocks args
info Int
v) SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
st
{-# INLINE dispatchExecState #-}


-- | Run the given @ExecCont@ on the given @SimState@,
--   being careful to catch any simulator abort exceptions
--   that are thrown and dispatch them to the abort handler.
advanceCrucibleState ::
  (IsSymInterface sym, IsSyntaxExtension ext) =>
  ExecCont p sym ext rtp f a ->
  SimState p sym ext rtp f a ->
  IO (ExecState p sym ext rtp)
advanceCrucibleState :: forall sym ext p rtp f (a :: Maybe (Ctx CrucibleType)).
(IsSymInterface sym, IsSyntaxExtension ext) =>
ExecCont p sym ext rtp f a
-> SimState p sym ext rtp f a -> IO (ExecState p sym ext rtp)
advanceCrucibleState ExecCont p sym ext rtp f a
m SimState p sym ext rtp f a
st =
     IO (ExecState p sym ext rtp)
-> [Handler (ExecState p sym ext rtp)]
-> IO (ExecState p sym ext rtp)
forall a. IO a -> [Handler a] -> IO a
Ex.catches (ExecCont p sym ext rtp f a
-> SimState p sym ext rtp f a -> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT ExecCont p sym ext rtp f a
m SimState p sym ext rtp f a
st)
                [ (AbortExecReason -> IO (ExecState p sym ext rtp))
-> Handler (ExecState p sym ext rtp)
forall a e. Exception e => (e -> IO a) -> Handler a
Ex.Handler ((AbortExecReason -> IO (ExecState p sym ext rtp))
 -> Handler (ExecState p sym ext rtp))
-> (AbortExecReason -> IO (ExecState p sym ext rtp))
-> Handler (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ \(AbortExecReason
e::AbortExecReason) ->
                    AbortExecReason
-> SimState p sym ext rtp f a -> IO (ExecState p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
AbortExecReason
-> SimState p sym ext rtp f args -> IO (ExecState p sym ext rtp)
runAbortHandler AbortExecReason
e SimState p sym ext rtp f a
st
                , (IOException -> IO (ExecState p sym ext rtp))
-> Handler (ExecState p sym ext rtp)
forall a e. Exception e => (e -> IO a) -> Handler a
Ex.Handler ((IOException -> IO (ExecState p sym ext rtp))
 -> Handler (ExecState p sym ext rtp))
-> (IOException -> IO (ExecState p sym ext rtp))
-> Handler (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ \(IOException
e::Ex.IOException) ->
                    if IOException -> Bool
Ex.isUserError IOException
e then
                      String
-> SimState p sym ext rtp f a -> IO (ExecState p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
String
-> SimState p sym ext rtp f args -> IO (ExecState p sym ext rtp)
runGenericErrorHandler (IOException -> String
Ex.ioeGetErrorString IOException
e) SimState p sym ext rtp f a
st
                    else
                      IOException -> IO (ExecState p sym ext rtp)
forall e a. Exception e => e -> IO a
Ex.throwIO IOException
e
                ]


-- | Run a single step of the Crucible symbolic simulator.
singleStepCrucible ::
  (IsSymInterface sym, IsSyntaxExtension ext) =>
  Int {- ^ Current verbosity -} ->
  ExecState p sym ext rtp ->
  IO (ExecState p sym ext rtp)
singleStepCrucible :: forall sym ext p rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
Int -> ExecState p sym ext rtp -> IO (ExecState p sym ext rtp)
singleStepCrucible Int
verb ExecState p sym ext rtp
exst =
  IO Int
-> ExecState p sym ext rtp
-> (ExecResult p sym ext rtp -> IO (ExecState p sym ext rtp))
-> (forall f (a :: Maybe (Ctx CrucibleType)).
    ExecCont p sym ext rtp f a
    -> SimState p sym ext rtp f a -> IO (ExecState p sym ext rtp))
-> IO (ExecState p sym ext rtp)
forall sym ext p rtp z.
(IsSymInterface sym, IsSyntaxExtension ext) =>
IO Int
-> ExecState p sym ext rtp
-> (ExecResult p sym ext rtp -> IO z)
-> (forall f (a :: Maybe (Ctx CrucibleType)).
    ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z)
-> IO z
dispatchExecState
    (Int -> IO Int
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Int
verb)
    ExecState p sym ext rtp
exst
    (ExecState p sym ext rtp -> IO (ExecState p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecState p sym ext rtp -> IO (ExecState p sym ext rtp))
-> (ExecResult p sym ext rtp -> ExecState p sym ext rtp)
-> ExecResult p sym ext rtp
-> IO (ExecState p sym ext rtp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExecResult p sym ext rtp -> ExecState p sym ext rtp
forall p sym ext rtp.
ExecResult p sym ext rtp -> ExecState p sym ext rtp
ResultState)
    ExecCont p sym ext rtp f a
-> SimState p sym ext rtp f a -> IO (ExecState p sym ext rtp)
forall f (a :: Maybe (Ctx CrucibleType)).
ExecCont p sym ext rtp f a
-> SimState p sym ext rtp f a -> IO (ExecState p sym ext rtp)
forall sym ext p rtp f (a :: Maybe (Ctx CrucibleType)).
(IsSymInterface sym, IsSyntaxExtension ext) =>
ExecCont p sym ext rtp f a
-> SimState p sym ext rtp f a -> IO (ExecState p sym ext rtp)
advanceCrucibleState


-- | This datatype indicates the possible results that an execution feature
--   can have.
data ExecutionFeatureResult p sym ext rtp where
  -- | This execution feature result indicates that no state changes were
  --   made.
  ExecutionFeatureNoChange       :: ExecutionFeatureResult p sym ext rtp

  -- | This execution feature indicates that the state was modified but
  --   not changed in an "essential" way.  For example, internal bookkeeping
  --   datastructures for the execution feature might be modified, but the
  --   state is not transitioned to a fundamentally different state.
  --
  --   When this result is returned, later execution features in the
  --   installed stack will be executed, until the main simulator loop
  --   is encountered.  Contrast with the \"new state\" result.
  ExecutionFeatureModifiedState ::
     ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp

  -- | This execution feature result indicates that the state was modified
  --   in an essential way that transforms it into new state altogether.
  --   When this result is returned, it preempts any later execution
  --   features and the main simulator loop and instead returns to the head
  --   of the execution feature stack.
  --
  --   NOTE: In particular, the execution feature will encounter the
  --   state again before the simulator loop.  It is therefore very
  --   important that the execution feature be prepared to immediately
  --   encounter the same state again and make significant execution
  --   progress on it, or ignore it so it makes it to the main simulator
  --   loop.  Otherwise, the execution feature will loop back to itself
  --   infinitely, starving out useful work.
  ExecutionFeatureNewState ::
     ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp


-- | An execution feature represents a computation that is allowed to intercept
--   the processing of execution states to perform additional processing at
--   each intermediate state.  A list of execution features is accepted by
--   `executeCrucible`.  After each step of the simulator, the execution features
--   are consulted, each in turn.  After all the execution features have run,
--   the main simulator code is executed to advance the simulator one step.
--
--   If an execution feature wishes to make changes to the execution
--   state before further execution happens, the return value can be
--   used to return a modified state.  If this happens, the current
--   stack of execution features is abandoned and a fresh step starts
--   over immediately from the top of the execution features.  In
--   essence, each execution feature can preempt all following
--   execution features and the main simulator loop. In other words,
--   the main simulator only gets reached if every execution feature
--   returns @Nothing@.  It is important, therefore, that execution
--   features make only a bounded number of modification in a row, or
--   the main simulator loop will be starved out.
newtype ExecutionFeature p sym ext rtp =
  ExecutionFeature
  { forall p sym ext rtp.
ExecutionFeature p sym ext rtp
-> ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
runExecutionFeature :: ExecState p sym ext rtp -> IO (ExecutionFeatureResult p sym ext rtp)
  }

-- | A generic execution feature is an execution feature that is
--   agnostic to the execution environment, and is therefore
--   polymorphic over the @p@, @ext@ and @rtp@ variables.
newtype GenericExecutionFeature sym =
  GenericExecutionFeature
  { forall sym.
GenericExecutionFeature sym
-> forall p ext rtp.
   (IsSymInterface sym, IsSyntaxExtension ext) =>
   ExecState p sym ext rtp
   -> IO (ExecutionFeatureResult p sym ext rtp)
runGenericExecutionFeature :: forall p ext rtp.
      (IsSymInterface sym, IsSyntaxExtension ext) =>
        ExecState p sym ext rtp -> IO (ExecutionFeatureResult p sym ext rtp)
  }

genericToExecutionFeature ::
  (IsSymInterface sym, IsSyntaxExtension ext) =>
  GenericExecutionFeature sym -> ExecutionFeature p sym ext rtp
genericToExecutionFeature :: forall sym ext p rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
GenericExecutionFeature sym -> ExecutionFeature p sym ext rtp
genericToExecutionFeature (GenericExecutionFeature forall p ext rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
f) = (ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
forall p sym ext rtp.
(ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
ExecutionFeature ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall p ext rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
f


-- | Given a 'SimState' and an execution continuation,
--   apply the continuation and execute the resulting
--   computation until completion.
--
--   This function is responsible for catching
--   'AbortExecReason' exceptions and 'UserError'
--   exceptions and invoking the 'errorHandler'
--   contained in the state.
executeCrucible :: forall p sym ext rtp.
  ( IsSymInterface sym
  , IsSyntaxExtension ext
  ) =>
  [ ExecutionFeature p sym ext rtp ] {- ^ Execution features to install -} ->
  ExecState p sym ext rtp   {- ^ Execution state to begin executing -} ->
  IO (ExecResult p sym ext rtp)
executeCrucible :: forall p sym ext rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
[ExecutionFeature p sym ext rtp]
-> ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp)
executeCrucible [ExecutionFeature p sym ext rtp]
execFeatures ExecState p sym ext rtp
exst0 =
  do let cfg :: Config
cfg = sym -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration (sym -> Config)
-> (ExecState p sym ext rtp -> sym)
-> ExecState p sym ext rtp
-> Config
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting sym (SimContext p sym ext) sym
-> SimContext p sym ext -> sym
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting sym (SimContext p sym ext) sym
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)
-> (ExecState p sym ext rtp -> SimContext p sym ext)
-> ExecState p sym ext rtp
-> sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExecState p sym ext rtp -> SimContext p sym ext
forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
execStateContext (ExecState p sym ext rtp -> Config)
-> ExecState p sym ext rtp -> Config
forall a b. (a -> b) -> a -> b
$ ExecState p sym ext rtp
exst0
     OptionSetting BaseIntegerType
verbOpt <- ConfigOption BaseIntegerType
-> Config -> IO (OptionSetting BaseIntegerType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseIntegerType
verbosity Config
cfg

     let loop :: ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp)
loop ExecState p sym ext rtp
exst =
           IO Int
-> ExecState p sym ext rtp
-> (ExecResult p sym ext rtp -> IO (ExecResult p sym ext rtp))
-> (forall f (a :: Maybe (Ctx CrucibleType)).
    ExecCont p sym ext rtp f a
    -> SimState p sym ext rtp f a -> IO (ExecResult p sym ext rtp))
-> IO (ExecResult p sym ext rtp)
forall sym ext p rtp z.
(IsSymInterface sym, IsSyntaxExtension ext) =>
IO Int
-> ExecState p sym ext rtp
-> (ExecResult p sym ext rtp -> IO z)
-> (forall f (a :: Maybe (Ctx CrucibleType)).
    ExecCont p sym ext rtp f a -> SimState p sym ext rtp f a -> IO z)
-> IO z
dispatchExecState
             (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> IO Integer -> IO Int
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> OptionSetting BaseIntegerType -> IO Integer
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt OptionSetting BaseIntegerType
verbOpt)
             ExecState p sym ext rtp
exst
             ExecResult p sym ext rtp -> IO (ExecResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return
             (\ExecCont p sym ext rtp f a
m SimState p sym ext rtp f a
st -> ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp)
knext (ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp))
-> IO (ExecState p sym ext rtp) -> IO (ExecResult p sym ext rtp)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExecCont p sym ext rtp f a
-> SimState p sym ext rtp f a -> IO (ExecState p sym ext rtp)
forall sym ext p rtp f (a :: Maybe (Ctx CrucibleType)).
(IsSymInterface sym, IsSyntaxExtension ext) =>
ExecCont p sym ext rtp f a
-> SimState p sym ext rtp f a -> IO (ExecState p sym ext rtp)
advanceCrucibleState ExecCont p sym ext rtp f a
m SimState p sym ext rtp f a
st)

         applyExecutionFeature :: ExecutionFeature p sym ext rtp
-> (ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp))
-> ExecState p sym ext rtp
-> IO (ExecResult p sym ext rtp)
applyExecutionFeature ExecutionFeature p sym ext rtp
feat ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp)
m = \ExecState p sym ext rtp
exst ->
             ExecutionFeature p sym ext rtp
-> ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall p sym ext rtp.
ExecutionFeature p sym ext rtp
-> ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
runExecutionFeature ExecutionFeature p sym ext rtp
feat ExecState p sym ext rtp
exst IO (ExecutionFeatureResult p sym ext rtp)
-> (ExecutionFeatureResult p sym ext rtp
    -> IO (ExecResult p sym ext rtp))
-> IO (ExecResult p sym ext rtp)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                  ExecutionFeatureResult p sym ext rtp
ExecutionFeatureNoChange            -> ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp)
m ExecState p sym ext rtp
exst
                  ExecutionFeatureModifiedState ExecState p sym ext rtp
exst' -> ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp)
m ExecState p sym ext rtp
exst'
                  ExecutionFeatureNewState ExecState p sym ext rtp
exst'      -> ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp)
knext ExecState p sym ext rtp
exst'

         knext :: ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp)
knext = (ExecutionFeature p sym ext rtp
 -> (ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp))
 -> ExecState p sym ext rtp
 -> IO (ExecResult p sym ext rtp))
-> (ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp))
-> [ExecutionFeature p sym ext rtp]
-> ExecState p sym ext rtp
-> IO (ExecResult p sym ext rtp)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ExecutionFeature p sym ext rtp
-> (ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp))
-> ExecState p sym ext rtp
-> IO (ExecResult p sym ext rtp)
applyExecutionFeature ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp)
loop [ExecutionFeature p sym ext rtp]
execFeatures

     ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp)
knext ExecState p sym ext rtp
exst0


-- | This feature will terminate the execution of a crucible simulator
--   with a @TimeoutResult@ after a given interval of wall-clock time
--   has elapsed.
timeoutFeature ::
  NominalDiffTime ->
  IO (GenericExecutionFeature sym)
timeoutFeature :: forall sym. NominalDiffTime -> IO (GenericExecutionFeature sym)
timeoutFeature NominalDiffTime
timeout =
  do UTCTime
startTime <- IO UTCTime
getCurrentTime
     let deadline :: UTCTime
deadline = NominalDiffTime -> UTCTime -> UTCTime
addUTCTime NominalDiffTime
timeout UTCTime
startTime
     GenericExecutionFeature sym -> IO (GenericExecutionFeature sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GenericExecutionFeature sym -> IO (GenericExecutionFeature sym))
-> GenericExecutionFeature sym -> IO (GenericExecutionFeature sym)
forall a b. (a -> b) -> a -> b
$ (forall p ext rtp.
 (IsSymInterface sym, IsSyntaxExtension ext) =>
 ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> GenericExecutionFeature sym
forall sym.
(forall p ext rtp.
 (IsSymInterface sym, IsSyntaxExtension ext) =>
 ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> GenericExecutionFeature sym
GenericExecutionFeature ((forall p ext rtp.
  (IsSymInterface sym, IsSyntaxExtension ext) =>
  ExecState p sym ext rtp
  -> IO (ExecutionFeatureResult p sym ext rtp))
 -> GenericExecutionFeature sym)
-> (forall p ext rtp.
    (IsSymInterface sym, IsSyntaxExtension ext) =>
    ExecState p sym ext rtp
    -> IO (ExecutionFeatureResult p sym ext rtp))
-> GenericExecutionFeature sym
forall a b. (a -> b) -> a -> b
$ \ExecState p sym ext rtp
exst ->
       case ExecState p sym ext rtp
exst of
         ResultState ExecResult p sym ext rtp
_ -> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
ExecutionFeatureNoChange
         ExecState p sym ext rtp
_ ->
            do UTCTime
now <- IO UTCTime
getCurrentTime
               if UTCTime
deadline UTCTime -> UTCTime -> Bool
forall a. Ord a => a -> a -> Bool
>= UTCTime
now then
                 ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
ExecutionFeatureNoChange
               else
                 ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
ExecutionFeatureNewState (ExecResult p sym ext rtp -> ExecState p sym ext rtp
forall p sym ext rtp.
ExecResult p sym ext rtp -> ExecState p sym ext rtp
ResultState (ExecState p sym ext rtp -> ExecResult p sym ext rtp
forall p sym ext r. ExecState p sym ext r -> ExecResult p sym ext r
TimeoutResult ExecState p sym ext rtp
exst)))