-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Simulator.BoundedRecursion
-- Description      : Support for bounding function recursion depth
-- Copyright        : (c) Galois, Inc 2019
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
--
-- This module provides an execution feature for bounding recursion.
-- Essentially, we bound the number of times any particular function
-- is allowed to have active frames on the call stack.
------------------------------------------------------------------------

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

{-# OPTIONS_GHC -Wno-orphans #-}
module Lang.Crucible.Simulator.BoundedRecursion
  ( boundedRecursionFeature
  ) where

import           Control.Lens ( (^.), (&), (%~) )
import           Control.Monad (when)
import           Data.IORef
import           Data.Maybe
import qualified Data.Text as Text
import           Data.Word
import qualified Data.Map.Strict as Map

import           Data.Parameterized.Ctx
import qualified Data.Parameterized.Map as MapF

import           What4.Interface

import           Lang.Crucible.Backend
import           Lang.Crucible.CFG.Common
import           Lang.Crucible.FunctionHandle
import           Lang.Crucible.Panic
import           Lang.Crucible.Simulator.SimError
import           Lang.Crucible.Simulator.ExecutionTree
import           Lang.Crucible.Simulator.EvalStmt
import           Lang.Crucible.Simulator.Intrinsics
import           Lang.Crucible.Simulator.GlobalState
import           Lang.Crucible.Types

type BoundedRecursionMap = Map.Map SomeHandle Word64

instance IntrinsicClass sym "BoundedRecursionData" where
  type Intrinsic sym "BoundedRecursionData" ctx = [BoundedRecursionMap]
  muxIntrinsic :: forall (ctx :: Ctx CrucibleType).
sym
-> IntrinsicTypes sym
-> SymbolRepr "BoundedRecursionData"
-> CtxRepr ctx
-> Pred sym
-> Intrinsic sym "BoundedRecursionData" ctx
-> Intrinsic sym "BoundedRecursionData" ctx
-> IO (Intrinsic sym "BoundedRecursionData" ctx)
muxIntrinsic sym
_sym IntrinsicTypes sym
_iTypes SymbolRepr "BoundedRecursionData"
_nm CtxRepr ctx
_ Pred sym
_p Intrinsic sym "BoundedRecursionData" ctx
x Intrinsic sym "BoundedRecursionData" ctx
_y = [BoundedRecursionMap] -> IO [BoundedRecursionMap]
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return [BoundedRecursionMap]
Intrinsic sym "BoundedRecursionData" ctx
x

type BoundedRecursionGlobal = GlobalVar (IntrinsicType "BoundedRecursionData" EmptyCtx)

-- | This execution feature allows users to place a bound on the number of
--   recursive calls that a function can execute.  Each time a function is
--   called, the number of activations of the functions is incremented, and
--   the path is aborted if the bound is exceeded.
--
--   The boolean argument indicates if we should generate proof obligations when
--   we cut off recursion.  If true, recursion cutoffs will generate proof obligations
--   which will be provable only if the function actually could not have executed that number
--   of times.  If false, the execution of recursive functions will be aborted without
--   generating side conditions.
boundedRecursionFeature ::
  (SomeHandle -> IO (Maybe Word64))
    {- ^ Action for computing what recursion depth to allow for the given function -}  ->
  Bool {- ^ Produce a proof obligation when resources are exhausted? -} ->
  IO (GenericExecutionFeature sym)

boundedRecursionFeature :: forall sym.
(SomeHandle -> IO (Maybe Word64))
-> Bool -> IO (GenericExecutionFeature sym)
boundedRecursionFeature SomeHandle -> IO (Maybe Word64)
getRecursionBound Bool
generateSideConditions =
  do IORef BoundedRecursionGlobal
gvRef <- BoundedRecursionGlobal -> IO (IORef BoundedRecursionGlobal)
forall a. a -> IO (IORef a)
newIORef ([Char] -> BoundedRecursionGlobal
forall a. HasCallStack => [Char] -> a
error [Char]
"Global variable for BoundedRecursionData not initialized")
     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
$ IORef BoundedRecursionGlobal
-> ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall p sym ext rtp.
IORef BoundedRecursionGlobal
-> ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
onStep IORef BoundedRecursionGlobal
gvRef

 where
 popFrame ::
   IORef BoundedRecursionGlobal ->
   (SimState p sym ext rtp f args -> ExecState p sym ext rtp) ->
   SimState p sym ext rtp f args ->
   IO (ExecutionFeatureResult p sym ext rtp)
 popFrame :: forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
IORef BoundedRecursionGlobal
-> (SimState p sym ext rtp f args -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f args
-> IO (ExecutionFeatureResult p sym ext rtp)
popFrame IORef BoundedRecursionGlobal
gvRef SimState p sym ext rtp f args -> ExecState p sym ext rtp
mkSt SimState p sym ext rtp f args
st =
   do BoundedRecursionGlobal
gv <- IORef BoundedRecursionGlobal -> IO BoundedRecursionGlobal
forall a. IORef a -> IO a
readIORef IORef BoundedRecursionGlobal
gvRef
      case BoundedRecursionGlobal
-> SymGlobalState sym
-> Maybe
     (RegValue sym (IntrinsicType "BoundedRecursionData" EmptyCtx))
forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
lookupGlobal BoundedRecursionGlobal
gv (SimState p sym ext rtp f args
st SimState p sym ext rtp f args
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext rtp f args)
     (SymGlobalState sym)
-> SymGlobalState sym
forall s a. s -> Getting a s a -> a
^. Getting
  (SymGlobalState sym)
  (SimState p sym ext rtp f args)
  (SymGlobalState sym)
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
stateGlobals) of
        Maybe
  (RegValue sym (IntrinsicType "BoundedRecursionData" EmptyCtx))
Nothing -> [Char] -> [[Char]] -> IO (ExecutionFeatureResult p sym ext rtp)
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"bounded recursion" [[Char]
"global not defined!"]
        Just [] -> [Char] -> [[Char]] -> IO (ExecutionFeatureResult p sym ext rtp)
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"bounded recursion" [[Char]
"pop on empty stack!"]
        Just (BoundedRecursionMap
_:[BoundedRecursionMap]
xs) ->
          do let st' :: SimState p sym ext rtp f args
st' = SimState p sym ext rtp f args
st SimState p sym ext rtp f args
-> (SimState p sym ext rtp f args -> SimState p sym ext rtp f args)
-> SimState p sym ext rtp f args
forall a b. a -> (a -> b) -> b
& (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState p sym ext rtp f args
-> Identity (SimState p sym ext rtp f args)
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
stateGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
 -> SimState p sym ext rtp f args
 -> Identity (SimState p sym ext rtp f args))
-> (SymGlobalState sym -> SymGlobalState sym)
-> SimState p sym ext rtp f args
-> SimState p sym ext rtp f args
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ BoundedRecursionGlobal
-> RegValue sym (IntrinsicType "BoundedRecursionData" EmptyCtx)
-> SymGlobalState sym
-> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
insertGlobal BoundedRecursionGlobal
gv [BoundedRecursionMap]
RegValue sym (IntrinsicType "BoundedRecursionData" EmptyCtx)
xs
             ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
ExecutionFeatureModifiedState (SimState p sym ext rtp f args -> ExecState p sym ext rtp
mkSt SimState p sym ext rtp f args
st'))

 pushFrame ::
   IORef BoundedRecursionGlobal ->
   (BoundedRecursionMap -> BoundedRecursionMap -> [BoundedRecursionMap] -> [BoundedRecursionMap]) ->
   SomeHandle ->
   (SimState p sym ext rtp f args -> ExecState p sym ext rtp) ->
   SimState p sym ext rtp f args ->
   IO (ExecutionFeatureResult p sym ext rtp)
 pushFrame :: forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
IORef BoundedRecursionGlobal
-> (BoundedRecursionMap
    -> BoundedRecursionMap
    -> [BoundedRecursionMap]
    -> [BoundedRecursionMap])
-> SomeHandle
-> (SimState p sym ext rtp f args -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f args
-> IO (ExecutionFeatureResult p sym ext rtp)
pushFrame IORef BoundedRecursionGlobal
gvRef BoundedRecursionMap
-> BoundedRecursionMap
-> [BoundedRecursionMap]
-> [BoundedRecursionMap]
rebuildStack SomeHandle
h SimState p sym ext rtp f args -> ExecState p sym ext rtp
mkSt SimState p sym ext rtp f args
st = SimState p sym ext rtp f args
-> forall a. IsSymInterfaceProof sym a
forall p sym ext r f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext r f args -> forall a. IsSymInterfaceProof sym a
stateSolverProof SimState p sym ext rtp f args
st IsSymInterfaceProof sym (IO (ExecutionFeatureResult p sym ext rtp))
-> IsSymInterfaceProof
     sym (IO (ExecutionFeatureResult p sym ext rtp))
forall a b. (a -> b) -> a -> b
$
     do let sym :: sym
sym = SimState p sym ext rtp f args
stSimState p sym ext rtp f args
-> Getting sym (SimState p sym ext rtp f args) sym -> sym
forall s a. s -> Getting a s a -> a
^.Getting sym (SimState p sym ext rtp f args) 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
        let simCtx :: SimContext p sym ext
simCtx = SimState p sym ext rtp f args
stSimState p sym ext rtp f args
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext rtp f args)
     (SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp f args)
  (SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext
        BoundedRecursionGlobal
gv <- IORef BoundedRecursionGlobal -> IO BoundedRecursionGlobal
forall a. IORef a -> IO a
readIORef IORef BoundedRecursionGlobal
gvRef
        case BoundedRecursionGlobal
-> SymGlobalState sym
-> Maybe
     (RegValue sym (IntrinsicType "BoundedRecursionData" EmptyCtx))
forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
lookupGlobal BoundedRecursionGlobal
gv (SimState p sym ext rtp f args
st SimState p sym ext rtp f args
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext rtp f args)
     (SymGlobalState sym)
-> SymGlobalState sym
forall s a. s -> Getting a s a -> a
^. Getting
  (SymGlobalState sym)
  (SimState p sym ext rtp f args)
  (SymGlobalState sym)
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
stateGlobals) of
          Maybe
  (RegValue sym (IntrinsicType "BoundedRecursionData" EmptyCtx))
Nothing -> [Char] -> [[Char]] -> IO (ExecutionFeatureResult p sym ext rtp)
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"bounded recursion" [[Char]
"global not defined!"]
          Just [] -> [Char] -> [[Char]] -> IO (ExecutionFeatureResult p sym ext rtp)
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"bounded recursion" [[Char]
"empty stack!"]
          Just (BoundedRecursionMap
x:[BoundedRecursionMap]
xs) ->
            do Maybe Word64
mb <- SomeHandle -> IO (Maybe Word64)
getRecursionBound SomeHandle
h
               let v :: Word64
v = Word64
1 Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64 -> Maybe Word64 -> Word64
forall a. a -> Maybe a -> a
fromMaybe Word64
0 (SomeHandle -> BoundedRecursionMap -> Maybe Word64
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SomeHandle
h BoundedRecursionMap
x)
               case Maybe Word64
mb of
                 Just Word64
b | Word64
v Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
> Word64
b ->
                   do ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
                      let msg :: [Char]
msg = ([Char]
"reached maximum number of recursive calls to function " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SomeHandle -> [Char]
forall a. Show a => a -> [Char]
show SomeHandle
h [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Word64 -> [Char]
forall a. Show a => a -> [Char]
show Word64
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")")
                      let err :: SimError
err = ProgramLoc -> SimErrorReason -> SimError
SimError ProgramLoc
loc ([Char] -> SimErrorReason
ResourceExhausted [Char]
msg)
                      Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when Bool
generateSideConditions (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ SimContext p sym ext
-> (forall {bak}. IsSymBackend sym bak => bak -> IO ()) -> IO ()
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend SimContext p sym ext
simCtx ((forall {bak}. IsSymBackend sym bak => bak -> IO ()) -> IO ())
-> (forall {bak}. IsSymBackend sym bak => bak -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
                        bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addProofObligation bak
bak (SymExpr sym BaseBoolType -> SimError -> Assertion sym
forall pred msg. pred -> msg -> LabeledPred pred msg
LabeledPred (sym -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) SimError
err)
                      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 (AbortExecReason
-> SimState p sym ext rtp f args -> ExecState p sym ext rtp
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType)).
AbortExecReason
-> SimState p sym ext rtp f a -> ExecState p sym ext rtp
AbortState (SimError -> AbortExecReason
AssertionFailure SimError
err) SimState p sym ext rtp f args
st))
                 Maybe Word64
_ ->
                   do let x' :: BoundedRecursionMap
x'  = SomeHandle -> Word64 -> BoundedRecursionMap -> BoundedRecursionMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SomeHandle
h Word64
v BoundedRecursionMap
x
                      let st' :: SimState p sym ext rtp f args
st' = SimState p sym ext rtp f args
st SimState p sym ext rtp f args
-> (SimState p sym ext rtp f args -> SimState p sym ext rtp f args)
-> SimState p sym ext rtp f args
forall a b. a -> (a -> b) -> b
& (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState p sym ext rtp f args
-> Identity (SimState p sym ext rtp f args)
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
stateGlobals ((SymGlobalState sym -> Identity (SymGlobalState sym))
 -> SimState p sym ext rtp f args
 -> Identity (SimState p sym ext rtp f args))
-> (SymGlobalState sym -> SymGlobalState sym)
-> SimState p sym ext rtp f args
-> SimState p sym ext rtp f args
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ BoundedRecursionGlobal
-> RegValue sym (IntrinsicType "BoundedRecursionData" EmptyCtx)
-> SymGlobalState sym
-> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
insertGlobal BoundedRecursionGlobal
gv (BoundedRecursionMap
-> BoundedRecursionMap
-> [BoundedRecursionMap]
-> [BoundedRecursionMap]
rebuildStack BoundedRecursionMap
x' BoundedRecursionMap
x [BoundedRecursionMap]
xs)
                      BoundedRecursionMap
x' BoundedRecursionMap
-> IO (ExecutionFeatureResult p sym ext rtp)
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. a -> b -> b
`seq` ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
ExecutionFeatureModifiedState (SimState p sym ext rtp f args -> ExecState p sym ext rtp
mkSt SimState p sym ext rtp f args
st'))

 onStep ::
   IORef BoundedRecursionGlobal ->
   ExecState p sym ext rtp ->
   IO (ExecutionFeatureResult p sym ext rtp)

 onStep :: forall p sym ext rtp.
IORef BoundedRecursionGlobal
-> ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
onStep IORef BoundedRecursionGlobal
gvRef = \case

   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 let halloc :: HandleAllocator
halloc = SimContext p sym ext -> HandleAllocator
forall personality sym ext.
SimContext personality sym ext -> HandleAllocator
simHandleAllocator SimContext p sym ext
simctx
        BoundedRecursionGlobal
gv <- HandleAllocator
-> Text
-> TypeRepr (IntrinsicType "BoundedRecursionData" EmptyCtx)
-> IO BoundedRecursionGlobal
forall (tp :: CrucibleType).
HandleAllocator -> Text -> TypeRepr tp -> IO (GlobalVar tp)
freshGlobalVar HandleAllocator
halloc ([Char] -> Text
Text.pack [Char]
"BoundedRecursionData") TypeRepr (IntrinsicType "BoundedRecursionData" EmptyCtx)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
        IORef BoundedRecursionGlobal -> BoundedRecursionGlobal -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef BoundedRecursionGlobal
gvRef BoundedRecursionGlobal
gv
        let simctx' :: SimContext p sym ext
simctx'  = SimContext p sym ext
simctx{ ctxIntrinsicTypes = MapF.insert
                                   (knownSymbol @"BoundedRecursionData")
                                   IntrinsicMuxFn
                                   (ctxIntrinsicTypes simctx) }
        let globals' :: SymGlobalState sym
globals' = BoundedRecursionGlobal
-> RegValue sym (IntrinsicType "BoundedRecursionData" EmptyCtx)
-> SymGlobalState sym
-> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
insertGlobal BoundedRecursionGlobal
gv [BoundedRecursionMap
forall a. Monoid a => a
mempty] SymGlobalState sym
globals
        ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
ExecutionFeatureModifiedState (SimContext p sym ext
-> SymGlobalState sym
-> AbortHandler p sym ext (RegEntry sym ret)
-> TypeRepr ret
-> ExecCont
     p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
-> ExecState p sym ext rtp
forall p sym ext rtp (ret :: CrucibleType).
(rtp ~ RegEntry sym ret) =>
SimContext p sym ext
-> SymGlobalState sym
-> AbortHandler p sym ext (RegEntry sym ret)
-> TypeRepr ret
-> ExecCont
     p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
-> ExecState p sym ext rtp
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))

   CallState ReturnHandler ret p sym ext rtp f a
rh ResolvedCall p sym ext ret
call SimState p sym ext rtp f a
st ->
     IORef BoundedRecursionGlobal
-> (BoundedRecursionMap
    -> BoundedRecursionMap
    -> [BoundedRecursionMap]
    -> [BoundedRecursionMap])
-> SomeHandle
-> (SimState p sym ext rtp f a -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f a
-> IO (ExecutionFeatureResult p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
IORef BoundedRecursionGlobal
-> (BoundedRecursionMap
    -> BoundedRecursionMap
    -> [BoundedRecursionMap]
    -> [BoundedRecursionMap])
-> SomeHandle
-> (SimState p sym ext rtp f args -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f args
-> IO (ExecutionFeatureResult p sym ext rtp)
pushFrame IORef BoundedRecursionGlobal
gvRef (\BoundedRecursionMap
a BoundedRecursionMap
b [BoundedRecursionMap]
xs -> BoundedRecursionMap
aBoundedRecursionMap
-> [BoundedRecursionMap] -> [BoundedRecursionMap]
forall a. a -> [a] -> [a]
:BoundedRecursionMap
bBoundedRecursionMap
-> [BoundedRecursionMap] -> [BoundedRecursionMap]
forall a. a -> [a] -> [a]
:[BoundedRecursionMap]
xs) (ResolvedCall p sym ext ret -> SomeHandle
forall p sym ext (ret :: CrucibleType).
ResolvedCall p sym ext ret -> SomeHandle
resolvedCallHandle ResolvedCall p sym ext ret
call) (ReturnHandler ret p sym ext rtp f a
-> ResolvedCall p sym ext ret
-> SimState p sym ext rtp f a
-> ExecState p sym ext rtp
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType))
       (ret :: CrucibleType).
ReturnHandler ret p sym ext rtp f a
-> ResolvedCall p sym ext ret
-> SimState p sym ext rtp f a
-> ExecState p sym ext rtp
CallState ReturnHandler ret p sym ext rtp f a
rh ResolvedCall p sym ext ret
call) SimState p sym ext rtp f a
st

   TailCallState ValueFromValue p sym ext rtp ret
vfv ResolvedCall p sym ext ret
call SimState p sym ext rtp f a
st ->
     IORef BoundedRecursionGlobal
-> (BoundedRecursionMap
    -> BoundedRecursionMap
    -> [BoundedRecursionMap]
    -> [BoundedRecursionMap])
-> SomeHandle
-> (SimState p sym ext rtp f a -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f a
-> IO (ExecutionFeatureResult p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
IORef BoundedRecursionGlobal
-> (BoundedRecursionMap
    -> BoundedRecursionMap
    -> [BoundedRecursionMap]
    -> [BoundedRecursionMap])
-> SomeHandle
-> (SimState p sym ext rtp f args -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f args
-> IO (ExecutionFeatureResult p sym ext rtp)
pushFrame IORef BoundedRecursionGlobal
gvRef (\BoundedRecursionMap
a BoundedRecursionMap
_ [BoundedRecursionMap]
xs -> BoundedRecursionMap
aBoundedRecursionMap
-> [BoundedRecursionMap] -> [BoundedRecursionMap]
forall a. a -> [a] -> [a]
:[BoundedRecursionMap]
xs) (ResolvedCall p sym ext ret -> SomeHandle
forall p sym ext (ret :: CrucibleType).
ResolvedCall p sym ext ret -> SomeHandle
resolvedCallHandle ResolvedCall p sym ext ret
call) (ValueFromValue p sym ext rtp ret
-> ResolvedCall p sym ext ret
-> SimState p sym ext rtp f a
-> ExecState p sym ext rtp
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType))
       (ret :: CrucibleType).
ValueFromValue p sym ext rtp ret
-> ResolvedCall p sym ext ret
-> SimState p sym ext rtp f a
-> ExecState p sym ext rtp
TailCallState ValueFromValue p sym ext rtp ret
vfv ResolvedCall p sym ext ret
call) SimState p sym ext rtp f a
st

   ReturnState FunctionName
nm ValueFromValue p sym ext rtp ret
vfv RegEntry sym ret
pr SimState p sym ext rtp f a
st ->
     IORef BoundedRecursionGlobal
-> (SimState p sym ext rtp f a -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f a
-> IO (ExecutionFeatureResult p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
IORef BoundedRecursionGlobal
-> (SimState p sym ext rtp f args -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f args
-> IO (ExecutionFeatureResult p sym ext rtp)
popFrame IORef BoundedRecursionGlobal
gvRef (FunctionName
-> ValueFromValue p sym ext rtp ret
-> RegEntry sym ret
-> SimState p sym ext rtp f a
-> ExecState p sym ext rtp
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType))
       (ret :: CrucibleType).
FunctionName
-> ValueFromValue p sym ext rtp ret
-> RegEntry sym ret
-> SimState p sym ext rtp f a
-> ExecState p sym ext rtp
ReturnState FunctionName
nm ValueFromValue p sym ext rtp ret
vfv RegEntry sym ret
pr) SimState p sym ext rtp f a
st

   UnwindCallState ValueFromValue p sym ext rtp r
vfv AbortedResult sym ext
ar SimState p sym ext rtp f a
st ->
     IORef BoundedRecursionGlobal
-> (SimState p sym ext rtp f a -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f a
-> IO (ExecutionFeatureResult p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
IORef BoundedRecursionGlobal
-> (SimState p sym ext rtp f args -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f args
-> IO (ExecutionFeatureResult p sym ext rtp)
popFrame IORef BoundedRecursionGlobal
gvRef (ValueFromValue p sym ext rtp r
-> AbortedResult sym ext
-> SimState p sym ext rtp f a
-> ExecState p sym ext rtp
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType))
       (r :: CrucibleType).
ValueFromValue p sym ext rtp r
-> AbortedResult sym ext
-> SimState p sym ext rtp f a
-> ExecState p sym ext rtp
UnwindCallState ValueFromValue p sym ext rtp r
vfv AbortedResult sym ext
ar) SimState p sym ext rtp f a
st

   ExecState p sym ext rtp
_ -> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
ExecutionFeatureNoChange