-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Simulator.BoundedExec
-- Description      : Support for bounding loop depth
-- Copyright        : (c) Galois, Inc 2018
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
--
-- This module provides an execution feature for bounding the
-- number of iterations that a loop will execute in the simulator.
------------------------------------------------------------------------
{-# 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.BoundedExec
  ( boundedExecFeature
  ) where

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


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

import           Lang.Crucible.Analysis.Fixpoint.Components
import           Lang.Crucible.Backend
import           Lang.Crucible.CFG.Core
import           Lang.Crucible.FunctionHandle
import           Lang.Crucible.Panic
import           Lang.Crucible.Simulator.CallFrame
import           Lang.Crucible.Simulator.ExecutionTree
import           Lang.Crucible.Simulator.GlobalState
import           Lang.Crucible.Simulator.Intrinsics
import           Lang.Crucible.Simulator.EvalStmt
import           Lang.Crucible.Simulator.SimError

import           What4.FunctionName
import           What4.Interface

data FrameBoundData =
  forall args ret.
    FrameBoundData
    { ()
frameBoundHandle :: !(FnHandle args ret)
    , FrameBoundData -> Word64
frameBoundLimit :: !Word64
    , FrameBoundData -> Map Int (Int, Int)
frameWtoMap :: !(Map Int (Int,Int))
    , FrameBoundData -> Seq Word64
frameBoundCounts :: Seq Word64
    }

-- | This function takes weak topological order data and computes
--   a mapping from block ID number to (position, depth) pair.  The
--   position value indicates which the position in the WTO listing
--   in which the block ID appears, and the depth indicates the number
--   of nested components the block ID appears in.  Loop backedges
--   occur exactly at places where control flows from a higher position
--   number to a lower position number.  Jumps that exit inner loops
--   to the next iteration of an outer loop are identified by backedges
--   that pass from higher depths to lower depths.
buildWTOMap :: [WTOComponent (Some (BlockID blocks))] -> Map Int (Int,Int)
buildWTOMap :: forall (blocks :: Ctx (Ctx CrucibleType)).
[WTOComponent (Some (BlockID blocks))] -> Map Int (Int, Int)
buildWTOMap = (Int, Map Int (Int, Int)) -> Map Int (Int, Int)
forall a b. (a, b) -> b
snd ((Int, Map Int (Int, Int)) -> Map Int (Int, Int))
-> ([WTOComponent (Some (BlockID blocks))]
    -> (Int, Map Int (Int, Int)))
-> [WTOComponent (Some (BlockID blocks))]
-> Map Int (Int, Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int
-> Int
-> Map Int (Int, Int)
-> [WTOComponent (Some (BlockID blocks))]
-> (Int, Map Int (Int, Int))
forall (blocks :: Ctx (Ctx CrucibleType)).
Int
-> Int
-> Map Int (Int, Int)
-> [WTOComponent (Some (BlockID blocks))]
-> (Int, Map Int (Int, Int))
go Int
0 Int
0 Map Int (Int, Int)
forall k a. Map k a
Map.empty
 where
 go :: Int -> Int -> Map Int (Int,Int) -> [WTOComponent (Some (BlockID blocks))] -> (Int, Map Int (Int,Int))
 go :: forall (blocks :: Ctx (Ctx CrucibleType)).
Int
-> Int
-> Map Int (Int, Int)
-> [WTOComponent (Some (BlockID blocks))]
-> (Int, Map Int (Int, Int))
go !Int
x !Int
_ Map Int (Int, Int)
m [] = (Int
x,Map Int (Int, Int)
m)
 go !Int
x !Int
d Map Int (Int, Int)
m (Vertex (Some BlockID blocks x
bid) : [WTOComponent (Some (BlockID blocks))]
cs) =
    let m' :: Map Int (Int, Int)
m' = Int -> (Int, Int) -> Map Int (Int, Int) -> Map Int (Int, Int)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Index blocks x -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
Ctx.indexVal (BlockID blocks x -> Index blocks x
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex BlockID blocks x
bid)) (Int
x,Int
d) Map Int (Int, Int)
m
     in Int
-> Int
-> Map Int (Int, Int)
-> [WTOComponent (Some (BlockID blocks))]
-> (Int, Map Int (Int, Int))
forall (blocks :: Ctx (Ctx CrucibleType)).
Int
-> Int
-> Map Int (Int, Int)
-> [WTOComponent (Some (BlockID blocks))]
-> (Int, Map Int (Int, Int))
go (Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int
d Map Int (Int, Int)
m' [WTOComponent (Some (BlockID blocks))]
cs
 go !Int
x !Int
d Map Int (Int, Int)
m (SCC SCC (Some (BlockID blocks))
scc : [WTOComponent (Some (BlockID blocks))]
cs) =
    let m' :: Map Int (Int, Int)
m'  = (forall (tp :: Ctx CrucibleType).
 BlockID blocks tp -> Map Int (Int, Int))
-> Some (BlockID blocks) -> Map Int (Int, Int)
forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome (\BlockID blocks tp
hd -> Int -> (Int, Int) -> Map Int (Int, Int) -> Map Int (Int, Int)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Index blocks tp -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
Ctx.indexVal (BlockID blocks tp -> Index blocks tp
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex BlockID blocks tp
hd)) (Int
x,Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Map Int (Int, Int)
m) (SCC (Some (BlockID blocks)) -> Some (BlockID blocks)
forall n. SCC n -> n
wtoHead SCC (Some (BlockID blocks))
scc)
        (Int
x',Map Int (Int, Int)
m'') = Int
-> Int
-> Map Int (Int, Int)
-> [WTOComponent (Some (BlockID blocks))]
-> (Int, Map Int (Int, Int))
forall (blocks :: Ctx (Ctx CrucibleType)).
Int
-> Int
-> Map Int (Int, Int)
-> [WTOComponent (Some (BlockID blocks))]
-> (Int, Map Int (Int, Int))
go (Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Map Int (Int, Int)
m' ([WTOComponent (Some (BlockID blocks))]
 -> (Int, Map Int (Int, Int)))
-> [WTOComponent (Some (BlockID blocks))]
-> (Int, Map Int (Int, Int))
forall a b. (a -> b) -> a -> b
$ SCC (Some (BlockID blocks))
-> [WTOComponent (Some (BlockID blocks))]
forall n. SCC n -> [WTOComponent n]
wtoComps SCC (Some (BlockID blocks))
scc
     in Int
-> Int
-> Map Int (Int, Int)
-> [WTOComponent (Some (BlockID blocks))]
-> (Int, Map Int (Int, Int))
forall (blocks :: Ctx (Ctx CrucibleType)).
Int
-> Int
-> Map Int (Int, Int)
-> [WTOComponent (Some (BlockID blocks))]
-> (Int, Map Int (Int, Int))
go Int
x' Int
d Map Int (Int, Int)
m'' [WTOComponent (Some (BlockID blocks))]
cs


-- | This function updates the loop bound count at the given depth.
--   Any loop bounds deeper than this are discarded.  If the given
--   sequence is too short to accommodate the given depth, the sequence
--   is extended with 0 counters to the correct depth.
incrementBoundCount :: Seq Word64 -> Int -> (Seq Word64, Word64)
incrementBoundCount :: Seq Word64 -> Int -> (Seq Word64, Word64)
incrementBoundCount Seq Word64
cs Int
depth =
  case Int -> Seq Word64 -> Maybe Word64
forall a. Int -> Seq a -> Maybe a
Seq.lookup Int
depth Seq Word64
cs of
     Just Word64
n ->
       do let n' :: Word64
n' = Word64
nWord64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+Word64
1
          let cs' :: Seq Word64
cs' = Int -> Word64 -> Seq Word64 -> Seq Word64
forall a. Int -> a -> Seq a -> Seq a
Seq.update Int
depth Word64
n' (Seq Word64 -> Seq Word64) -> Seq Word64 -> Seq Word64
forall a b. (a -> b) -> a -> b
$ Int -> Seq Word64 -> Seq Word64
forall a. Int -> Seq a -> Seq a
Seq.take (Int
depthInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Seq Word64
cs
          Word64
n' Word64 -> (Seq Word64, Word64) -> (Seq Word64, Word64)
forall a b. a -> b -> b
`seq` Seq Word64
cs' Seq Word64 -> (Seq Word64, Word64) -> (Seq Word64, Word64)
forall a b. a -> b -> b
`seq` (Seq Word64
cs', Word64
n')
     Maybe Word64
Nothing ->
       do let cs' :: Seq Word64
cs' = Seq Word64
cs Seq Word64 -> Seq Word64 -> Seq Word64
forall a. Semigroup a => a -> a -> a
<> Int -> Word64 -> Seq Word64
forall a. Int -> a -> Seq a
Seq.replicate (Int
depth Int -> Int -> Int
forall a. Num a => a -> a -> a
- Seq Word64 -> Int
forall a. Seq a -> Int
Seq.length Seq Word64
cs) Word64
0 Seq Word64 -> Seq Word64 -> Seq Word64
forall a. Semigroup a => a -> a -> a
<> Word64 -> Seq Word64
forall a. a -> Seq a
Seq.singleton Word64
1
          Seq Word64
cs' Seq Word64 -> (Seq Word64, Word64) -> (Seq Word64, Word64)
forall a b. a -> b -> b
`seq` (Seq Word64
cs', Word64
1)

instance IntrinsicClass sym "BoundedExecFrameData" where
  type Intrinsic sym "BoundedExecFrameData" ctx = [Either FunctionName FrameBoundData]

  muxIntrinsic :: forall (ctx :: Ctx CrucibleType).
sym
-> IntrinsicTypes sym
-> SymbolRepr "BoundedExecFrameData"
-> CtxRepr ctx
-> Pred sym
-> Intrinsic sym "BoundedExecFrameData" ctx
-> Intrinsic sym "BoundedExecFrameData" ctx
-> IO (Intrinsic sym "BoundedExecFrameData" ctx)
muxIntrinsic sym
_sym IntrinsicTypes sym
_iTypes SymbolRepr "BoundedExecFrameData"
_nm CtxRepr ctx
_ Pred sym
_p Intrinsic sym "BoundedExecFrameData" ctx
fd1 Intrinsic sym "BoundedExecFrameData" ctx
fd2 = [Either FunctionName FrameBoundData]
-> [Either FunctionName FrameBoundData]
-> IO [Either FunctionName FrameBoundData]
combineFrameBoundData [Either FunctionName FrameBoundData]
Intrinsic sym "BoundedExecFrameData" ctx
fd1 [Either FunctionName FrameBoundData]
Intrinsic sym "BoundedExecFrameData" ctx
fd2

mergeCounts :: Seq Word64 -> Seq Word64 -> Seq Word64
mergeCounts :: Seq Word64 -> Seq Word64 -> Seq Word64
mergeCounts Seq Word64
cx Seq Word64
cy =
  Int -> (Int -> Word64) -> Seq Word64
forall a. Int -> (Int -> a) -> Seq a
Seq.fromFunction
    (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Seq Word64 -> Int
forall a. Seq a -> Int
Seq.length Seq Word64
cx) (Seq Word64 -> Int
forall a. Seq a -> Int
Seq.length Seq Word64
cy))
    (\Int
i -> Word64 -> Word64 -> Word64
forall a. Ord a => a -> a -> a
max (Word64 -> Maybe Word64 -> Word64
forall a. a -> Maybe a -> a
fromMaybe Word64
0 (Maybe Word64 -> Word64) -> Maybe Word64 -> Word64
forall a b. (a -> b) -> a -> b
$ Int -> Seq Word64 -> Maybe Word64
forall a. Int -> Seq a -> Maybe a
Seq.lookup Int
i Seq Word64
cx)
               (Word64 -> Maybe Word64 -> Word64
forall a. a -> Maybe a -> a
fromMaybe Word64
0 (Maybe Word64 -> Word64) -> Maybe Word64 -> Word64
forall a b. (a -> b) -> a -> b
$ Int -> Seq Word64 -> Maybe Word64
forall a. Int -> Seq a -> Maybe a
Seq.lookup Int
i Seq Word64
cy))

mergeFBD ::
  FrameBoundData ->
  FrameBoundData ->
  IO FrameBoundData
mergeFBD :: FrameBoundData -> FrameBoundData -> IO FrameBoundData
mergeFBD x :: FrameBoundData
x@FrameBoundData{ frameBoundHandle :: ()
frameBoundHandle = FnHandle args ret
hx } y :: FrameBoundData
y@FrameBoundData{ frameBoundHandle :: ()
frameBoundHandle = FnHandle args ret
hy }
  | Just (args ::> ret) :~: (args ::> ret)
_ <- Nonce GlobalNonceGenerator (args ::> ret)
-> Nonce GlobalNonceGenerator (args ::> ret)
-> Maybe ((args ::> ret) :~: (args ::> ret))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx CrucibleType) (b :: Ctx CrucibleType).
Nonce GlobalNonceGenerator a
-> Nonce GlobalNonceGenerator b -> Maybe (a :~: b)
testEquality (FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle args ret
hx) (FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleID FnHandle args ret
hy) =
       FrameBoundData -> IO FrameBoundData
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return FrameBoundData
x{ frameBoundCounts = mergeCounts (frameBoundCounts x) (frameBoundCounts y) }

  | Bool
otherwise =
       [Char] -> [[Char]] -> IO FrameBoundData
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"BoundedExec.mergeFBD"
       [ [Char]
"Attempted to merge frame bound data from different function activations: "
       , [Char]
" ** " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FnHandle args ret -> [Char]
forall a. Show a => a -> [Char]
show FnHandle args ret
hx
       , [Char]
" ** " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FnHandle args ret -> [Char]
forall a. Show a => a -> [Char]
show FnHandle args ret
hy
       ]


combineFrameBoundData ::
  [Either FunctionName FrameBoundData] ->
  [Either FunctionName FrameBoundData] ->
  IO [Either FunctionName FrameBoundData]
combineFrameBoundData :: [Either FunctionName FrameBoundData]
-> [Either FunctionName FrameBoundData]
-> IO [Either FunctionName FrameBoundData]
combineFrameBoundData [] [] = [Either FunctionName FrameBoundData]
-> IO [Either FunctionName FrameBoundData]
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return []

combineFrameBoundData (Left FunctionName
nmx:[Either FunctionName FrameBoundData]
xs) (Left FunctionName
nmy : [Either FunctionName FrameBoundData]
_) | FunctionName
nmx FunctionName -> FunctionName -> Bool
forall a. Eq a => a -> a -> Bool
== FunctionName
nmy
  = [Either FunctionName FrameBoundData]
-> IO [Either FunctionName FrameBoundData]
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (FunctionName -> Either FunctionName FrameBoundData
forall a b. a -> Either a b
Left FunctionName
nmx Either FunctionName FrameBoundData
-> [Either FunctionName FrameBoundData]
-> [Either FunctionName FrameBoundData]
forall a. a -> [a] -> [a]
: [Either FunctionName FrameBoundData]
xs)

combineFrameBoundData (Right FrameBoundData
x:[Either FunctionName FrameBoundData]
xs) (Right FrameBoundData
y:[Either FunctionName FrameBoundData]
_)
  = (\FrameBoundData
x' -> FrameBoundData -> Either FunctionName FrameBoundData
forall a b. b -> Either a b
Right FrameBoundData
x' Either FunctionName FrameBoundData
-> [Either FunctionName FrameBoundData]
-> [Either FunctionName FrameBoundData]
forall a. a -> [a] -> [a]
: [Either FunctionName FrameBoundData]
xs) (FrameBoundData -> [Either FunctionName FrameBoundData])
-> IO FrameBoundData -> IO [Either FunctionName FrameBoundData]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> FrameBoundData -> FrameBoundData -> IO FrameBoundData
mergeFBD FrameBoundData
x FrameBoundData
y

combineFrameBoundData [Either FunctionName FrameBoundData]
xs [Either FunctionName FrameBoundData]
ys
  = [Char] -> [[Char]] -> IO [Either FunctionName FrameBoundData]
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"BoundedExec.combineFrameBoundData"
      [ [Char]
"Attempt to combine incompatible frame bound data: stack shape mismatch:"
      , [Char]
" *** " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
forall a. Show a => a -> [Char]
show ([Either FunctionName FrameBoundData] -> [[Char]]
printStack [Either FunctionName FrameBoundData]
xs)
      , [Char]
" *** " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
forall a. Show a => a -> [Char]
show ([Either FunctionName FrameBoundData] -> [[Char]]
printStack [Either FunctionName FrameBoundData]
ys)
      ]

printStack :: [Either FunctionName FrameBoundData] -> [String]
printStack :: [Either FunctionName FrameBoundData] -> [[Char]]
printStack [] = []
printStack (Left FunctionName
nm :[Either FunctionName FrameBoundData]
xs) = FunctionName -> [Char]
forall a. Show a => a -> [Char]
show FunctionName
nm [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: [Either FunctionName FrameBoundData] -> [[Char]]
printStack [Either FunctionName FrameBoundData]
xs
printStack (Right FrameBoundData{ frameBoundHandle :: ()
frameBoundHandle = FnHandle args ret
h } : [Either FunctionName FrameBoundData]
xs) = FnHandle args ret -> [Char]
forall a. Show a => a -> [Char]
show FnHandle args ret
h [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: [Either FunctionName FrameBoundData] -> [[Char]]
printStack [Either FunctionName FrameBoundData]
xs


type BoundedExecGlobal = GlobalVar (IntrinsicType "BoundedExecFrameData" EmptyCtx)


-- | This execution feature allows users to place a bound on the number
--   of iterations that a loop will execute.  Each time a function is called,
--   the included action is called to determine if the loops in that function
--   should be bounded, and what their iteration bound should be.
--
--   The boolean argument indicates if we should generate proof obligations when
--   we cut off loop execution.  If true, loop cutoffs will generate proof obligations
--   which will be provable only if the loop actually could not have executed that number
--   of iterations.  If false, the execution of loops will be aborted without generating
--   side conditions.
--
--   Note that we compute a weak topological ordering on control flow graphs
--   to determine loop heads and loop nesting structure.  Loop bounds for inner
--   loops are reset on every iteration through an outer loop.
boundedExecFeature ::
  (SomeHandle -> IO (Maybe Word64))
    {- ^ Action for computing loop bounds for functions when they are called -} ->
  Bool {- ^ Produce a proof obligation when resources are exhausted? -} ->
  IO (GenericExecutionFeature sym)
boundedExecFeature :: forall sym.
(SomeHandle -> IO (Maybe Word64))
-> Bool -> IO (GenericExecutionFeature sym)
boundedExecFeature SomeHandle -> IO (Maybe Word64)
getLoopBounds Bool
generateSideConditions =
  do IORef BoundedExecGlobal
gvRef <- BoundedExecGlobal -> IO (IORef BoundedExecGlobal)
forall a. a -> IO (IORef a)
newIORef ([Char] -> BoundedExecGlobal
forall a. HasCallStack => [Char] -> a
error [Char]
"Global variable for BoundedExecFrameData 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 BoundedExecGlobal
-> ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall p sym ext rtp.
IORef BoundedExecGlobal
-> ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
onStep IORef BoundedExecGlobal
gvRef

 where
 buildFrameData :: ResolvedCall p sym ext ret -> IO (Either FunctionName FrameBoundData)
 buildFrameData :: forall p sym ext (ret :: CrucibleType).
ResolvedCall p sym ext ret
-> IO (Either FunctionName FrameBoundData)
buildFrameData (OverrideCall Override p sym ext args ret
ov OverrideFrame sym ret args
_) = Either FunctionName FrameBoundData
-> IO (Either FunctionName FrameBoundData)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (FunctionName -> Either FunctionName FrameBoundData
forall a b. a -> Either a b
Left (Override p sym ext args ret -> FunctionName
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
Override p sym ext args ret -> FunctionName
overrideName Override p sym ext args ret
ov))
 buildFrameData (CrucibleCall BlockID blocks args
_entry CallFrame{ _frameCFG :: ()
_frameCFG = CFG ext blocks initialArgs ret
g }) =
   do let wtoMap :: Map Int (Int, Int)
wtoMap = [WTOComponent (Some (BlockID blocks))] -> Map Int (Int, Int)
forall (blocks :: Ctx (Ctx CrucibleType)).
[WTOComponent (Some (BlockID blocks))] -> Map Int (Int, Int)
buildWTOMap (CFG ext blocks initialArgs ret
-> [WTOComponent (Some (BlockID blocks))]
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> [WTOComponent (Some (BlockID blocks))]
cfgWeakTopologicalOrdering CFG ext blocks initialArgs ret
g)
      Maybe Word64
mn <- SomeHandle -> IO (Maybe Word64)
getLoopBounds (FnHandle initialArgs ret -> SomeHandle
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> SomeHandle
SomeHandle (CFG ext blocks initialArgs ret -> FnHandle initialArgs ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
cfgHandle CFG ext blocks initialArgs ret
g))
      case Maybe Word64
mn of
        Maybe Word64
Nothing -> Either FunctionName FrameBoundData
-> IO (Either FunctionName FrameBoundData)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Either FunctionName FrameBoundData
 -> IO (Either FunctionName FrameBoundData))
-> Either FunctionName FrameBoundData
-> IO (Either FunctionName FrameBoundData)
forall a b. (a -> b) -> a -> b
$ FunctionName -> Either FunctionName FrameBoundData
forall a b. a -> Either a b
Left  (FunctionName -> Either FunctionName FrameBoundData)
-> FunctionName -> Either FunctionName FrameBoundData
forall a b. (a -> b) -> a -> b
$ FnHandle initialArgs ret -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
handleName (CFG ext blocks initialArgs ret -> FnHandle initialArgs ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
cfgHandle CFG ext blocks initialArgs ret
g)
        Just Word64
n  -> Either FunctionName FrameBoundData
-> IO (Either FunctionName FrameBoundData)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Either FunctionName FrameBoundData
 -> IO (Either FunctionName FrameBoundData))
-> Either FunctionName FrameBoundData
-> IO (Either FunctionName FrameBoundData)
forall a b. (a -> b) -> a -> b
$ FrameBoundData -> Either FunctionName FrameBoundData
forall a b. b -> Either a b
Right (FrameBoundData -> Either FunctionName FrameBoundData)
-> FrameBoundData -> Either FunctionName FrameBoundData
forall a b. (a -> b) -> a -> b
$ FrameBoundData
                       { frameBoundHandle :: FnHandle initialArgs ret
frameBoundHandle = CFG ext blocks initialArgs ret -> FnHandle initialArgs ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
cfgHandle CFG ext blocks initialArgs ret
g
                       , frameBoundLimit :: Word64
frameBoundLimit  = Word64
n
                       , frameWtoMap :: Map Int (Int, Int)
frameWtoMap      = Map Int (Int, Int)
wtoMap
                       , frameBoundCounts :: Seq Word64
frameBoundCounts = Seq Word64
forall a. Monoid a => a
mempty
                       }

 checkBackedge ::
   IORef BoundedExecGlobal ->
   Some (BlockID blocks) ->
   BlockID blocks tgt_args ->
   SymGlobalState sym ->
   IO (SymGlobalState sym, Maybe Word64)
 checkBackedge :: forall (blocks :: Ctx (Ctx CrucibleType))
       (tgt_args :: Ctx CrucibleType) sym.
IORef BoundedExecGlobal
-> Some (BlockID blocks)
-> BlockID blocks tgt_args
-> SymGlobalState sym
-> IO (SymGlobalState sym, Maybe Word64)
checkBackedge IORef BoundedExecGlobal
gvRef (Some BlockID blocks x
bid_curr) BlockID blocks tgt_args
bid_tgt SymGlobalState sym
globals =
   do BoundedExecGlobal
gv <- IORef BoundedExecGlobal -> IO BoundedExecGlobal
forall a. IORef a -> IO a
readIORef IORef BoundedExecGlobal
gvRef
      case [Either FunctionName FrameBoundData]
-> Maybe [Either FunctionName FrameBoundData]
-> [Either FunctionName FrameBoundData]
forall a. a -> Maybe a -> a
fromMaybe [] (BoundedExecGlobal
-> SymGlobalState sym
-> Maybe
     (RegValue sym (IntrinsicType "BoundedExecFrameData" EmptyCtx))
forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
lookupGlobal BoundedExecGlobal
gv SymGlobalState sym
globals) of
        ( Right FrameBoundData
fbd : [Either FunctionName FrameBoundData]
rest ) ->
          do let id_curr :: Int
id_curr = Index blocks x -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
Ctx.indexVal (BlockID blocks x -> Index blocks x
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex BlockID blocks x
bid_curr)
             let id_tgt :: Int
id_tgt  = Index blocks tgt_args -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
Ctx.indexVal (BlockID blocks tgt_args -> Index blocks tgt_args
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex BlockID blocks tgt_args
bid_tgt)
             let m :: Map Int (Int, Int)
m = FrameBoundData -> Map Int (Int, Int)
frameWtoMap FrameBoundData
fbd
             case (Int -> Map Int (Int, Int) -> Maybe (Int, Int)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
id_curr Map Int (Int, Int)
m, Int -> Map Int (Int, Int) -> Maybe (Int, Int)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
id_tgt Map Int (Int, Int)
m) of
               (Just (Int
cx, Int
_cd), Just (Int
tx, Int
td)) | Int
tx Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
cx ->
                  do let cs :: Seq Word64
cs       = FrameBoundData -> Seq Word64
frameBoundCounts FrameBoundData
fbd
                     let (Seq Word64
cs', Word64
q) = Seq Word64 -> Int -> (Seq Word64, Word64)
incrementBoundCount Seq Word64
cs Int
td
                     let fbd' :: FrameBoundData
fbd'     = FrameBoundData
fbd{ frameBoundCounts = cs' }
                     let globals' :: SymGlobalState sym
globals' = BoundedExecGlobal
-> RegValue sym (IntrinsicType "BoundedExecFrameData" EmptyCtx)
-> SymGlobalState sym
-> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
insertGlobal BoundedExecGlobal
gv (FrameBoundData -> Either FunctionName FrameBoundData
forall a b. b -> Either a b
Right FrameBoundData
fbd' Either FunctionName FrameBoundData
-> [Either FunctionName FrameBoundData]
-> [Either FunctionName FrameBoundData]
forall a. a -> [a] -> [a]
: [Either FunctionName FrameBoundData]
rest) SymGlobalState sym
globals
                     if Word64
q Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
> FrameBoundData -> Word64
frameBoundLimit FrameBoundData
fbd then
                       (SymGlobalState sym, Maybe Word64)
-> IO (SymGlobalState sym, Maybe Word64)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymGlobalState sym
globals', Word64 -> Maybe Word64
forall a. a -> Maybe a
Just (FrameBoundData -> Word64
frameBoundLimit FrameBoundData
fbd))
                     else
                       (SymGlobalState sym, Maybe Word64)
-> IO (SymGlobalState sym, Maybe Word64)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymGlobalState sym
globals', Maybe Word64
forall a. Maybe a
Nothing)

               (Maybe (Int, Int), Maybe (Int, Int))
_ -> (SymGlobalState sym, Maybe Word64)
-> IO (SymGlobalState sym, Maybe Word64)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymGlobalState sym
globals, Maybe Word64
forall a. Maybe a
Nothing)
        [Either FunctionName FrameBoundData]
_ -> (SymGlobalState sym, Maybe Word64)
-> IO (SymGlobalState sym, Maybe Word64)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymGlobalState sym
globals, Maybe Word64
forall a. Maybe a
Nothing)

 modifyStackState ::
   IORef BoundedExecGlobal ->
   (SimState p sym ext rtp f args -> ExecState p sym ext rtp) ->
   SimState p sym ext rtp f args ->
   ([Either FunctionName FrameBoundData] -> [Either FunctionName FrameBoundData]) ->
   IO (ExecutionFeatureResult p sym ext rtp)
 modifyStackState :: forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
IORef BoundedExecGlobal
-> (SimState p sym ext rtp f args -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f args
-> ([Either FunctionName FrameBoundData]
    -> [Either FunctionName FrameBoundData])
-> IO (ExecutionFeatureResult p sym ext rtp)
modifyStackState IORef BoundedExecGlobal
gvRef SimState p sym ext rtp f args -> ExecState p sym ext rtp
mkSt SimState p sym ext rtp f args
st [Either FunctionName FrameBoundData]
-> [Either FunctionName FrameBoundData]
f =
   do BoundedExecGlobal
gv <- IORef BoundedExecGlobal -> IO BoundedExecGlobal
forall a. IORef a -> IO a
readIORef IORef BoundedExecGlobal
gvRef
      let xs :: [Either FunctionName FrameBoundData]
xs = case BoundedExecGlobal
-> SymGlobalState sym
-> Maybe
     (RegValue sym (IntrinsicType "BoundedExecFrameData" EmptyCtx))
forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
lookupGlobal BoundedExecGlobal
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 "BoundedExecFrameData" EmptyCtx))
Nothing -> [Char] -> [Either FunctionName FrameBoundData]
forall a. HasCallStack => [Char] -> a
error [Char]
"bounded execution global not defined!"
                 Just RegValue sym (IntrinsicType "BoundedExecFrameData" EmptyCtx)
v  -> [Either FunctionName FrameBoundData]
RegValue sym (IntrinsicType "BoundedExecFrameData" EmptyCtx)
v
      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
%~ BoundedExecGlobal
-> RegValue sym (IntrinsicType "BoundedExecFrameData" EmptyCtx)
-> SymGlobalState sym
-> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
insertGlobal BoundedExecGlobal
gv ([Either FunctionName FrameBoundData]
-> [Either FunctionName FrameBoundData]
f [Either FunctionName FrameBoundData]
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'))

 onTransition ::
   IORef BoundedExecGlobal ->
   BlockID blocks tgt_args ->
   ControlResumption p sym ext rtp (CrucibleLang blocks ret) ->
   SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a) ->
   IO (ExecutionFeatureResult p sym ext rtp)
 onTransition :: forall (blocks :: Ctx (Ctx CrucibleType))
       (tgt_args :: Ctx CrucibleType) p sym ext rtp (ret :: CrucibleType)
       (a :: Ctx CrucibleType).
IORef BoundedExecGlobal
-> BlockID blocks tgt_args
-> ControlResumption p sym ext rtp (CrucibleLang blocks ret)
-> SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
-> IO (ExecutionFeatureResult p sym ext rtp)
onTransition IORef BoundedExecGlobal
gvRef BlockID blocks tgt_args
tgt_id ControlResumption p sym ext rtp (CrucibleLang blocks ret)
res SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
st = SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
-> 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 (CrucibleLang blocks ret) ('Just a)
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 (CrucibleLang blocks ret) ('Just a)
stSimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
-> Getting
     sym
     (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a))
     sym
-> sym
forall s a. s -> Getting a s a -> a
^.Getting
  sym
  (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a))
  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 (CrucibleLang blocks ret) ('Just a)
stSimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a))
     (SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
^.Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a))
  (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
     (SymGlobalState sym
globals', Maybe Word64
overLimit) <- IORef BoundedExecGlobal
-> Some (BlockID blocks)
-> BlockID blocks tgt_args
-> SymGlobalState sym
-> IO (SymGlobalState sym, Maybe Word64)
forall (blocks :: Ctx (Ctx CrucibleType))
       (tgt_args :: Ctx CrucibleType) sym.
IORef BoundedExecGlobal
-> Some (BlockID blocks)
-> BlockID blocks tgt_args
-> SymGlobalState sym
-> IO (SymGlobalState sym, Maybe Word64)
checkBackedge IORef BoundedExecGlobal
gvRef (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
stSimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
-> Getting
     (Some (BlockID blocks))
     (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a))
     (Some (BlockID blocks))
-> Some (BlockID blocks)
forall s a. s -> Getting a s a -> a
^.(CallFrame sym ext blocks ret a
 -> Const (Some (BlockID blocks)) (CallFrame sym ext blocks ret a))
-> SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
-> Const
     (Some (BlockID blocks))
     (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just 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 ret a
  -> Const (Some (BlockID blocks)) (CallFrame sym ext blocks ret a))
 -> SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
 -> Const
      (Some (BlockID blocks))
      (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)))
-> ((Some (BlockID blocks)
     -> Const (Some (BlockID blocks)) (Some (BlockID blocks)))
    -> CallFrame sym ext blocks ret a
    -> Const (Some (BlockID blocks)) (CallFrame sym ext blocks ret a))
-> Getting
     (Some (BlockID blocks))
     (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a))
     (Some (BlockID blocks))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Some (BlockID blocks)
 -> Const (Some (BlockID blocks)) (Some (BlockID blocks)))
-> CallFrame sym ext blocks ret a
-> Const (Some (BlockID blocks)) (CallFrame sym ext blocks ret a)
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) BlockID blocks tgt_args
tgt_id (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
stSimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a))
     (SymGlobalState sym)
-> SymGlobalState sym
forall s a. s -> Getting a s a -> a
^.Getting
  (SymGlobalState sym)
  (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a))
  (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)
     let st' :: SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
st' = SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
st SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
-> (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
    -> SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a))
-> SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
forall a b. a -> (a -> b) -> b
& (SymGlobalState sym -> Identity (SymGlobalState sym))
-> SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
-> Identity
     (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a))
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 (CrucibleLang blocks ret) ('Just a)
 -> Identity
      (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)))
-> SymGlobalState sym
-> SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
-> SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ SymGlobalState sym
globals'
     case Maybe Word64
overLimit of
       Just Word64
n ->
         do let msg :: [Char]
msg = [Char]
"reached maximum number of loop iterations (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Word64 -> [Char]
forall a. Show a => a -> [Char]
show Word64
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
            let loc :: ProgramLoc
loc = SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
stSimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
-> Getting
     ProgramLoc
     (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a))
     ProgramLoc
-> ProgramLoc
forall s a. s -> Getting a s a -> a
^.(CallFrame sym ext blocks ret a
 -> Const ProgramLoc (CallFrame sym ext blocks ret a))
-> SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
-> Const
     ProgramLoc
     (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just 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 ret a
  -> Const ProgramLoc (CallFrame sym ext blocks ret a))
 -> SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
 -> Const
      ProgramLoc
      (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)))
-> ((ProgramLoc -> Const ProgramLoc ProgramLoc)
    -> CallFrame sym ext blocks ret a
    -> Const ProgramLoc (CallFrame sym ext blocks ret a))
-> Getting
     ProgramLoc
     (SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a))
     ProgramLoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(CallFrame sym ext blocks ret a -> ProgramLoc)
-> (ProgramLoc -> Const ProgramLoc ProgramLoc)
-> CallFrame sym ext blocks ret a
-> Const ProgramLoc (CallFrame sym ext blocks ret a)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to CallFrame sym ext blocks ret a -> ProgramLoc
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> ProgramLoc
frameProgramLoc
            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 (CrucibleLang blocks ret) ('Just a)
-> 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 (CrucibleLang blocks ret) ('Just a)
st'))
       Maybe Word64
Nothing -> 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 (ControlResumption p sym ext rtp (CrucibleLang blocks ret)
-> SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
-> ExecState p sym ext rtp
forall p sym ext rtp f (a :: Ctx CrucibleType).
ControlResumption p sym ext rtp f
-> SimState p sym ext rtp f ('Just a) -> ExecState p sym ext rtp
ControlTransferState ControlResumption p sym ext rtp (CrucibleLang blocks ret)
res SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
st'))

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

 onStep :: forall p sym ext rtp.
IORef BoundedExecGlobal
-> ExecState p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
onStep IORef BoundedExecGlobal
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
        BoundedExecGlobal
gv <- HandleAllocator
-> Text
-> TypeRepr (IntrinsicType "BoundedExecFrameData" EmptyCtx)
-> IO BoundedExecGlobal
forall (tp :: CrucibleType).
HandleAllocator -> Text -> TypeRepr tp -> IO (GlobalVar tp)
freshGlobalVar HandleAllocator
halloc ([Char] -> Text
Text.pack [Char]
"BoundedExecFrameData") TypeRepr (IntrinsicType "BoundedExecFrameData" EmptyCtx)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
        IORef BoundedExecGlobal -> BoundedExecGlobal -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef BoundedExecGlobal
gvRef BoundedExecGlobal
gv
        let globals' :: SymGlobalState sym
globals' = BoundedExecGlobal
-> RegValue sym (IntrinsicType "BoundedExecFrameData" EmptyCtx)
-> SymGlobalState sym
-> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
insertGlobal BoundedExecGlobal
gv [FunctionName -> Either FunctionName FrameBoundData
forall a b. a -> Either a b
Left FunctionName
"_init"] SymGlobalState sym
globals
        let simctx' :: SimContext p sym ext
simctx' = SimContext p sym ext
simctx{ ctxIntrinsicTypes = MapF.insert (knownSymbol @"BoundedExecFrameData") IntrinsicMuxFn (ctxIntrinsicTypes simctx) }
        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 ->
     do Either FunctionName FrameBoundData
boundData <- ResolvedCall p sym ext ret
-> IO (Either FunctionName FrameBoundData)
forall p sym ext (ret :: CrucibleType).
ResolvedCall p sym ext ret
-> IO (Either FunctionName FrameBoundData)
buildFrameData ResolvedCall p sym ext ret
call
        IORef BoundedExecGlobal
-> (SimState p sym ext rtp f a -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f a
-> ([Either FunctionName FrameBoundData]
    -> [Either FunctionName FrameBoundData])
-> IO (ExecutionFeatureResult p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
IORef BoundedExecGlobal
-> (SimState p sym ext rtp f args -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f args
-> ([Either FunctionName FrameBoundData]
    -> [Either FunctionName FrameBoundData])
-> IO (ExecutionFeatureResult p sym ext rtp)
modifyStackState IORef BoundedExecGlobal
gvRef (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 (Either FunctionName FrameBoundData
boundDataEither FunctionName FrameBoundData
-> [Either FunctionName FrameBoundData]
-> [Either FunctionName FrameBoundData]
forall a. a -> [a] -> [a]
:)

   TailCallState ValueFromValue p sym ext rtp ret
vfv ResolvedCall p sym ext ret
call SimState p sym ext rtp f a
st ->
     do Either FunctionName FrameBoundData
boundData <- ResolvedCall p sym ext ret
-> IO (Either FunctionName FrameBoundData)
forall p sym ext (ret :: CrucibleType).
ResolvedCall p sym ext ret
-> IO (Either FunctionName FrameBoundData)
buildFrameData ResolvedCall p sym ext ret
call
        IORef BoundedExecGlobal
-> (SimState p sym ext rtp f a -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f a
-> ([Either FunctionName FrameBoundData]
    -> [Either FunctionName FrameBoundData])
-> IO (ExecutionFeatureResult p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
IORef BoundedExecGlobal
-> (SimState p sym ext rtp f args -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f args
-> ([Either FunctionName FrameBoundData]
    -> [Either FunctionName FrameBoundData])
-> IO (ExecutionFeatureResult p sym ext rtp)
modifyStackState IORef BoundedExecGlobal
gvRef (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 ((Either FunctionName FrameBoundData
boundDataEither FunctionName FrameBoundData
-> [Either FunctionName FrameBoundData]
-> [Either FunctionName FrameBoundData]
forall a. a -> [a] -> [a]
:) ([Either FunctionName FrameBoundData]
 -> [Either FunctionName FrameBoundData])
-> ([Either FunctionName FrameBoundData]
    -> [Either FunctionName FrameBoundData])
-> [Either FunctionName FrameBoundData]
-> [Either FunctionName FrameBoundData]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int
-> [Either FunctionName FrameBoundData]
-> [Either FunctionName FrameBoundData]
forall a. Int -> [a] -> [a]
drop Int
1)

   ReturnState FunctionName
nm ValueFromValue p sym ext rtp ret
vfv RegEntry sym ret
pr SimState p sym ext rtp f a
st ->
        IORef BoundedExecGlobal
-> (SimState p sym ext rtp f a -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f a
-> ([Either FunctionName FrameBoundData]
    -> [Either FunctionName FrameBoundData])
-> IO (ExecutionFeatureResult p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
IORef BoundedExecGlobal
-> (SimState p sym ext rtp f args -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f args
-> ([Either FunctionName FrameBoundData]
    -> [Either FunctionName FrameBoundData])
-> IO (ExecutionFeatureResult p sym ext rtp)
modifyStackState IORef BoundedExecGlobal
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 (Int
-> [Either FunctionName FrameBoundData]
-> [Either FunctionName FrameBoundData]
forall a. Int -> [a] -> [a]
drop Int
1)

   UnwindCallState ValueFromValue p sym ext rtp r
vfv AbortedResult sym ext
ar SimState p sym ext rtp f a
st ->
        IORef BoundedExecGlobal
-> (SimState p sym ext rtp f a -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f a
-> ([Either FunctionName FrameBoundData]
    -> [Either FunctionName FrameBoundData])
-> IO (ExecutionFeatureResult p sym ext rtp)
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
IORef BoundedExecGlobal
-> (SimState p sym ext rtp f args -> ExecState p sym ext rtp)
-> SimState p sym ext rtp f args
-> ([Either FunctionName FrameBoundData]
    -> [Either FunctionName FrameBoundData])
-> IO (ExecutionFeatureResult p sym ext rtp)
modifyStackState IORef BoundedExecGlobal
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 (Int
-> [Either FunctionName FrameBoundData]
-> [Either FunctionName FrameBoundData]
forall a. Int -> [a] -> [a]
drop Int
1)

   ControlTransferState ControlResumption p sym ext rtp f
res SimState p sym ext rtp f ('Just a)
st ->
     case ControlResumption p sym ext rtp f
res of
       ContinueResumption (ResolvedJump BlockID blocks args
tgt_id RegMap sym args
_)  ->  IORef BoundedExecGlobal
-> BlockID blocks args
-> ControlResumption p sym ext rtp (CrucibleLang blocks r)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> IO (ExecutionFeatureResult p sym ext rtp)
forall (blocks :: Ctx (Ctx CrucibleType))
       (tgt_args :: Ctx CrucibleType) p sym ext rtp (ret :: CrucibleType)
       (a :: Ctx CrucibleType).
IORef BoundedExecGlobal
-> BlockID blocks tgt_args
-> ControlResumption p sym ext rtp (CrucibleLang blocks ret)
-> SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
-> IO (ExecutionFeatureResult p sym ext rtp)
onTransition IORef BoundedExecGlobal
gvRef BlockID blocks args
tgt_id ControlResumption p sym ext rtp f
ControlResumption p sym ext rtp (CrucibleLang blocks r)
res SimState p sym ext rtp f ('Just a)
SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
st
       CheckMergeResumption (ResolvedJump BlockID blocks args
tgt_id RegMap sym args
_) -> IORef BoundedExecGlobal
-> BlockID blocks args
-> ControlResumption p sym ext rtp (CrucibleLang blocks r)
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> IO (ExecutionFeatureResult p sym ext rtp)
forall (blocks :: Ctx (Ctx CrucibleType))
       (tgt_args :: Ctx CrucibleType) p sym ext rtp (ret :: CrucibleType)
       (a :: Ctx CrucibleType).
IORef BoundedExecGlobal
-> BlockID blocks tgt_args
-> ControlResumption p sym ext rtp (CrucibleLang blocks ret)
-> SimState p sym ext rtp (CrucibleLang blocks ret) ('Just a)
-> IO (ExecutionFeatureResult p sym ext rtp)
onTransition IORef BoundedExecGlobal
gvRef BlockID blocks args
tgt_id ControlResumption p sym ext rtp f
ControlResumption p sym ext rtp (CrucibleLang blocks r)
res SimState p sym ext rtp f ('Just a)
SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
st
       ControlResumption p sym ext rtp f
_ -> 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
_ -> 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