------------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.SSAConversion
-- Description      : Allows converting from RTL to SSA representation.
-- Copyright        : (c) Galois, Inc 2014
-- License          : BSD3
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
--
-- This module provides a function for converting from the RTL to SSA
-- Crucible representation.
------------------------------------------------------------------------
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module Lang.Crucible.CFG.SSAConversion
  ( toSSA
  ) where

import           Control.Exception (assert)
import           Control.Lens ((&))
import           Control.Monad.State.Strict
import           Data.Bimap (Bimap)
import qualified Data.Bimap as Bimap
import qualified Data.Foldable as Fold
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Maybe (isJust, fromMaybe)
import           Data.Parameterized.Some
import           Data.Parameterized.TraversableFC
import           Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.Type.Equality
import qualified Prettyprinter as Pretty

import           What4.FunctionName (FunctionName)
import           What4.ProgramLoc

import           Lang.Crucible.Analysis.Reachable
import qualified Lang.Crucible.CFG.Core as C
import qualified Lang.Crucible.CFG.Expr as C
import           Lang.Crucible.CFG.Reg
import           Lang.Crucible.FunctionHandle
import           Lang.Crucible.Panic (panic)

#ifdef UNSAFE_OPS
-- We deliberately import Context.Unsafe as it is the only one that supports
-- the unsafe coerces between an index and its extension.
import           Data.Parameterized.Context.Unsafe as Ctx (Assignment)
import           Data.Parameterized.Context as Ctx hiding (Assignment)
import           Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
import           Unsafe.Coerce
#else
import           Data.Parameterized.Context as Ctx
#endif

------------------------------------------------------------------------
-- Utilities

-- | Given a list of pairs returns a map that maps each value appearing
-- in the first element to the second element in the set of pairs
-- containing it.
nextSetMap :: (Ord x, Ord y) => [(x,y)] -> Map x (Set y)
nextSetMap :: forall x y. (Ord x, Ord y) => [(x, y)] -> Map x (Set y)
nextSetMap [(x, y)]
l = State (Map x (Set y)) [()] -> Map x (Set y) -> Map x (Set y)
forall s a. State s a -> s -> s
execState (((x, y) -> StateT (Map x (Set y)) Identity ())
-> [(x, y)] -> State (Map x (Set y)) [()]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (x, y) -> StateT (Map x (Set y)) Identity ()
forall {k} {a} {m :: Type -> Type}.
(MonadState (Map k (Set a)) m, Ord k, Ord a) =>
(k, a) -> m ()
go [(x, y)]
l) Map x (Set y)
forall k a. Map k a
Map.empty
  where go :: (k, a) -> m ()
go (k
x,a
y) = (Map k (Set a) -> Map k (Set a)) -> m ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify ((Map k (Set a) -> Map k (Set a)) -> m ())
-> (Map k (Set a) -> Map k (Set a)) -> m ()
forall a b. (a -> b) -> a -> b
$ (Set a -> Set a -> Set a)
-> k -> Set a -> Map k (Set a) -> Map k (Set a)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union k
x (a -> Set a
forall a. a -> Set a
Set.singleton a
y)

------------------------------------------------------------------------
-- Input

-- | An input is a wrapper around a value that also knows if the
-- value was obtained as the output from a previous block.
--
-- * The first argument is true if the value was created from a previous block
-- * The second is the value itself.
data Input s
   = Input { forall s. Input s -> Bool
inputGeneratedPrev :: !Bool
             -- ^ Stores true if the value was created from a previous block.
           , forall s. Input s -> Some (Value s)
inputValue :: !(Some (Value s))
           }

instance Show (Input s) where
  showsPrec :: Int -> Input s -> ShowS
showsPrec Int
p Input s
r = Int -> Some (Value s) -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Input s -> Some (Value s)
forall s. Input s -> Some (Value s)
inputValue Input s
r)

instance Eq (Input s) where
  Input s
x == :: Input s -> Input s -> Bool
== Input s
y = Input s -> Some (Value s)
forall s. Input s -> Some (Value s)
inputValue Input s
x Some (Value s) -> Some (Value s) -> Bool
forall a. Eq a => a -> a -> Bool
== Input s -> Some (Value s)
forall s. Input s -> Some (Value s)
inputValue Input s
y

isOutputFromBlock :: BlockID s -> Some (Value s) -> Bool
isOutputFromBlock :: forall s. BlockID s -> Some (Value s) -> Bool
isOutputFromBlock (LambdaID LambdaLabel s tp
l) (Some (AtomValue Atom s x
a))
  | LambdaArg LambdaLabel s x
l' <- Atom s x -> AtomSource s x
forall s (tp :: CrucibleType). Atom s tp -> AtomSource s tp
atomSource Atom s x
a = Maybe (tp :~: x) -> Bool
forall a. Maybe a -> Bool
isJust (LambdaLabel s tp -> LambdaLabel s x -> Maybe (tp :~: x)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
LambdaLabel s a -> LambdaLabel s b -> Maybe (a :~: b)
testEquality LambdaLabel s tp
l LambdaLabel s x
l')
isOutputFromBlock BlockID s
_ Some (Value s)
_ = Bool
False

mkInput :: BlockID s -> Some (Value s) -> Input s
mkInput :: forall s. BlockID s -> Some (Value s) -> Input s
mkInput BlockID s
b Some (Value s)
v = Input { inputGeneratedPrev :: Bool
inputGeneratedPrev = BlockID s -> Some (Value s) -> Bool
forall s. BlockID s -> Some (Value s) -> Bool
isOutputFromBlock BlockID s
b Some (Value s)
v
                    , inputValue :: Some (Value s)
inputValue = Some (Value s)
v
                    }

instance Ord (Input s) where
  -- LambdaArg introduced in this block should be last.
  compare :: Input s -> Input s -> Ordering
compare Input s
x Input s
y =
    case (Input s -> Bool
forall s. Input s -> Bool
inputGeneratedPrev Input s
x, Input s -> Bool
forall s. Input s -> Bool
inputGeneratedPrev Input s
y) of
      (Bool
True,  Bool
True ) -> Bool -> Ordering -> Ordering
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Input s -> Some (Value s)
forall s. Input s -> Some (Value s)
inputValue Input s
x Some (Value s) -> Some (Value s) -> Bool
forall a. Eq a => a -> a -> Bool
== Input s -> Some (Value s)
forall s. Input s -> Some (Value s)
inputValue Input s
y) Ordering
EQ
      (Bool
True,  Bool
False) -> Ordering
GT
      (Bool
False, Bool
True ) -> Ordering
LT
      (Bool
False, Bool
False) -> Some (Value s) -> Some (Value s) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Input s -> Some (Value s)
forall s. Input s -> Some (Value s)
inputValue Input s
x) (Input s -> Some (Value s)
forall s. Input s -> Some (Value s)
inputValue Input s
y)

------------------------------------------------------------------------
-- BlockInput

data BlockInput ext s blocks ret args
  = BInput { forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType).
BlockInput ext s blocks ret args -> BlockID blocks args
binputID         :: !(C.BlockID blocks args)
             -- | Arguments expected by block.
           , forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType).
BlockInput ext s blocks ret args -> Assignment (Value s) args
binputArgs       :: !(Assignment (Value s) args)
           , forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType).
BlockInput ext s blocks ret args -> Seq (Posd (Stmt ext s))
binputStmts      :: !(Seq (Posd (Stmt ext s)))
           , forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType).
BlockInput ext s blocks ret args
-> Posd (ExtendedTermStmt s blocks ret)
binputTerm       :: !(Posd (ExtendedTermStmt s blocks ret))
           }

-- The Breakpoint non-terminator statement becomes a jump during SSA conversion.
-- This datatype temporarily adds breakpoint as a terminator statement.
data ExtendedTermStmt s blocks ret where
  BaseTermStmt :: TermStmt s ret -> ExtendedTermStmt s blocks ret
  BreakStmt :: JumpInfo s blocks -> ExtendedTermStmt s blocks ret

type BlockInputAssignment ext s blocks ret
   = Assignment (BlockInput ext s blocks ret)

extBlockInputAssignment ::
  BlockInputAssignment ext s blocks ret a ->
  BlockInputAssignment ext s (blocks ::> tp) ret a
extBlockInput ::
  BlockInput ext s blocks ret args ->
  BlockInput ext s (blocks ::> tp) ret arg
extBreakpoints ::
  Bimap BreakpointName (Some (C.BlockID blocks)) ->
  Bimap BreakpointName (Some (C.BlockID (blocks ::> tp)))
#ifdef UNSAFE_OPS
extBlockInputAssignment :: forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (a :: Ctx (Ctx CrucibleType))
       (tp :: Ctx CrucibleType).
BlockInputAssignment ext s blocks ret a
-> BlockInputAssignment ext s (blocks ::> tp) ret a
extBlockInputAssignment = BlockInputAssignment ext s blocks ret a
-> BlockInputAssignment ext s (blocks ::> tp) ret a
forall a b. a -> b
unsafeCoerce

extBlockInput :: forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (tp :: Ctx CrucibleType) (arg :: Ctx CrucibleType).
BlockInput ext s blocks ret args
-> BlockInput ext s (blocks ::> tp) ret arg
extBlockInput = BlockInput ext s blocks ret args
-> BlockInput ext s (blocks ::> tp) ret arg
forall a b. a -> b
unsafeCoerce

extBreakpoints :: forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Bimap BreakpointName (Some (BlockID blocks))
-> Bimap BreakpointName (Some (BlockID (blocks ::> tp)))
extBreakpoints = Bimap BreakpointName (Some (BlockID blocks))
-> Bimap BreakpointName (Some (BlockID (blocks ::> tp)))
forall a b. a -> b
unsafeCoerce
#else
extBlockInputAssignment = fmapFC extBlockInput

extBlockInput bi = bi { binputID = C.extendBlockID (binputID bi) }

extBreakpoints = Bimap.mapR (mapSome C.extendBlockID)
#endif

------------------------------------------------------------------------
-- inferRegAssignment

inferRegAssignment :: Set (Input s)
                   -> Some (Assignment (Value s))
inferRegAssignment :: forall s. Set (Input s) -> Some (Assignment (Value s))
inferRegAssignment Set (Input s)
s = [Some (Value s)] -> Some (Assignment (Value s))
forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
Ctx.fromList (Input s -> Some (Value s)
forall s. Input s -> Some (Value s)
inputValue (Input s -> Some (Value s)) -> [Input s] -> [Some (Value s)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (Input s) -> [Input s]
forall a. Set a -> [a]
Set.toList Set (Input s)
s)

------------------------------------------------------------------------
-- JumpInfo

data JumpInfo s blocks where
  JumpInfo :: C.BlockID blocks types
           -> C.CtxRepr types
           -> Assignment (Value s) types
           -> JumpInfo s blocks


emptyJumpInfoMap :: JumpInfoMap s blocks
lookupJumpInfo :: Label s -> JumpInfoMap s blocks -> Maybe (JumpInfo s blocks)
insertJumpInfo :: Label s -> JumpInfo s blocks -> JumpInfoMap s blocks -> JumpInfoMap s blocks

#ifdef UNSAFE_OPS
type JumpInfoMap s blocks = Map (Label s) (JumpInfo s blocks)

extJumpInfoMap :: JumpInfoMap s blocks -> JumpInfoMap s (blocks ::> args)
extJumpInfoMap :: forall s (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
JumpInfoMap s blocks -> JumpInfoMap s (blocks ::> args)
extJumpInfoMap = JumpInfoMap s blocks -> JumpInfoMap s (blocks ::> args)
forall a b. a -> b
unsafeCoerce


emptyJumpInfoMap :: forall s (blocks :: Ctx (Ctx CrucibleType)). JumpInfoMap s blocks
emptyJumpInfoMap = Map (Label s) (JumpInfo s blocks)
forall k a. Map k a
Map.empty
lookupJumpInfo :: forall s (blocks :: Ctx (Ctx CrucibleType)).
Label s -> JumpInfoMap s blocks -> Maybe (JumpInfo s blocks)
lookupJumpInfo = Label s
-> Map (Label s) (JumpInfo s blocks) -> Maybe (JumpInfo s blocks)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup
insertJumpInfo :: forall s (blocks :: Ctx (Ctx CrucibleType)).
Label s
-> JumpInfo s blocks
-> JumpInfoMap s blocks
-> JumpInfoMap s blocks
insertJumpInfo = Label s
-> JumpInfo s blocks
-> Map (Label s) (JumpInfo s blocks)
-> Map (Label s) (JumpInfo s blocks)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert

#else
data JumpInfoMap s blocks
  = forall blocks'.
     JumpInfoMap
     { _jimDiff :: !(Diff blocks' blocks)
     , _jimMap  :: !(Map (Label s) (JumpInfo s blocks'))
     , _jimThunk :: Map (Label s) (JumpInfo s blocks) -- NB! don't make this strict
     }

emptyJumpInfoMap = JumpInfoMap noDiff Map.empty Map.empty

extJumpInfoMap :: JumpInfoMap s blocks -> JumpInfoMap s (blocks ::> args)
extJumpInfoMap (JumpInfoMap diff mp _) =
  let diff' = extendRight diff
   in JumpInfoMap diff' mp (fmap (extJumpInfo diff') mp)

lookupJumpInfo l (JumpInfoMap diff mp _) = fmap (extJumpInfo diff) (Map.lookup l mp)
--lookupJumpInfo l mp = Map.lookup l (jimThunk mp)

insertJumpInfo l ji (JumpInfoMap _ _ thk) =
    let mp = Map.insert l ji thk
     in JumpInfoMap noDiff mp mp

-- | Extend jump target
extJumpInfo :: Diff blocks' blocks -> JumpInfo s blocks' -> JumpInfo s blocks
extJumpInfo diff (JumpInfo b typs a) = JumpInfo (C.extendBlockID' diff b) typs a
#endif


------------------------------------------------------------------------
-- SwitchInfo

data SwitchInfo s blocks tp where
  SwitchInfo :: C.BlockID blocks (args ::> tp)
             -> C.CtxRepr args
             -> Assignment (Value s) args
             -> SwitchInfo s blocks tp

emptySwitchInfoMap :: SwitchInfoMap s blocks

insertSwitchInfo   :: LambdaLabel s tp
                   -> SwitchInfo s blocks tp
                   -> SwitchInfoMap s blocks
                   -> SwitchInfoMap s blocks
lookupSwitchInfo   :: LambdaLabel s tp -> SwitchInfoMap s blocks -> Maybe (SwitchInfo s blocks tp)

#ifdef UNSAFE_OPS
{-
instance CoercibleF (SwitchInfo s blocks) where
  coerceF x = Data.Coerce.coerce x
-}

newtype SwitchInfoMap s blocks = SwitchInfoMap (MapF (LambdaLabel s) (SwitchInfo s blocks))

emptySwitchInfoMap :: forall s (blocks :: Ctx (Ctx CrucibleType)). SwitchInfoMap s blocks
emptySwitchInfoMap = MapF (LambdaLabel s) (SwitchInfo s blocks)
-> SwitchInfoMap s blocks
forall s (blocks :: Ctx (Ctx CrucibleType)).
MapF (LambdaLabel s) (SwitchInfo s blocks)
-> SwitchInfoMap s blocks
SwitchInfoMap MapF (LambdaLabel s) (SwitchInfo s blocks)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty

extSwitchInfoMap   :: SwitchInfoMap s blocks
                   -> SwitchInfoMap s (blocks ::> args)
extSwitchInfoMap :: forall s (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
SwitchInfoMap s blocks -> SwitchInfoMap s (blocks ::> args)
extSwitchInfoMap = SwitchInfoMap s blocks -> SwitchInfoMap s (blocks ::> args)
forall a b. a -> b
unsafeCoerce

insertSwitchInfo :: forall s (tp :: CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
LambdaLabel s tp
-> SwitchInfo s blocks tp
-> SwitchInfoMap s blocks
-> SwitchInfoMap s blocks
insertSwitchInfo LambdaLabel s tp
l SwitchInfo s blocks tp
si (SwitchInfoMap MapF (LambdaLabel s) (SwitchInfo s blocks)
m) = MapF (LambdaLabel s) (SwitchInfo s blocks)
-> SwitchInfoMap s blocks
forall s (blocks :: Ctx (Ctx CrucibleType)).
MapF (LambdaLabel s) (SwitchInfo s blocks)
-> SwitchInfoMap s blocks
SwitchInfoMap (LambdaLabel s tp
-> SwitchInfo s blocks tp
-> MapF (LambdaLabel s) (SwitchInfo s blocks)
-> MapF (LambdaLabel s) (SwitchInfo s blocks)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert LambdaLabel s tp
l SwitchInfo s blocks tp
si MapF (LambdaLabel s) (SwitchInfo s blocks)
m)
lookupSwitchInfo :: forall s (tp :: CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
LambdaLabel s tp
-> SwitchInfoMap s blocks -> Maybe (SwitchInfo s blocks tp)
lookupSwitchInfo LambdaLabel s tp
l (SwitchInfoMap MapF (LambdaLabel s) (SwitchInfo s blocks)
m) = LambdaLabel s tp
-> MapF (LambdaLabel s) (SwitchInfo s blocks)
-> Maybe (SwitchInfo s blocks tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup LambdaLabel s tp
l MapF (LambdaLabel s) (SwitchInfo s blocks)
m

#else
newtype SwitchInfoMap s blocks =
  SwitchInfoMap (Map (Some (LambdaLabel s)) (SomeSwitchInfo s blocks))
data SomeSwitchInfo s blocks = forall tp. SomeSwitchInfo (C.TypeRepr tp) (SwitchInfo s blocks tp)

mapSomeSI :: (forall tp. SwitchInfo s b tp -> SwitchInfo s b' tp) -> SomeSwitchInfo s b -> SomeSwitchInfo s b'
mapSomeSI f (SomeSwitchInfo tp si) = SomeSwitchInfo tp (f si)

emptySwitchInfoMap = SwitchInfoMap Map.empty

extSwitchInfoMap   :: SwitchInfoMap s blocks
                   -> SwitchInfoMap s (blocks ::> args)
extSwitchInfoMap (SwitchInfoMap m) =
   SwitchInfoMap $ fmap (mapSomeSI extSwitchInfo) m

insertSwitchInfo l si (SwitchInfoMap m) =
   SwitchInfoMap $ Map.insert (Some l) (SomeSwitchInfo (typeOfAtom (lambdaAtom l)) si) m

lookupSwitchInfo l (SwitchInfoMap m) =
   case Map.lookup (Some l) m of
      Nothing -> Nothing
      Just (SomeSwitchInfo tr si) -> Just $
         case testEquality tr (typeOfAtom (lambdaAtom l)) of
             Just Refl -> si
             Nothing   -> error "Lang.Crucible.SSAConversion.lookupSwitchInfo: type mismatch!"

-- | Extend switch target
extSwitchInfo :: SwitchInfo s blocks tp -> SwitchInfo s (blocks::>args) tp
extSwitchInfo (SwitchInfo b typs a) = SwitchInfo (C.extendBlockID b) typs a
#endif

extBlockInfo ::
  BlockInfo ext s ret blocks ->
  BlockInput ext s (blocks ::> args) ret args ->
  BlockInfo ext s ret (blocks ::> args)
extBlockInfo :: forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (args :: Ctx CrucibleType).
BlockInfo ext s ret blocks
-> BlockInput ext s (blocks ::> args) ret args
-> BlockInfo ext s ret (blocks ::> args)
extBlockInfo BlockInfo ext s ret blocks
bi BlockInput ext s (blocks ::> args) ret args
binput = do
  let blocks' :: BlockInputAssignment ext s (blocks ::> args) ret blocks
blocks' = BlockInputAssignment ext s blocks ret blocks
-> BlockInputAssignment ext s (blocks ::> args) ret blocks
forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (a :: Ctx (Ctx CrucibleType))
       (tp :: Ctx CrucibleType).
BlockInputAssignment ext s blocks ret a
-> BlockInputAssignment ext s (blocks ::> tp) ret a
extBlockInputAssignment (BlockInputAssignment ext s blocks ret blocks
 -> BlockInputAssignment ext s (blocks ::> args) ret blocks)
-> BlockInputAssignment ext s blocks ret blocks
-> BlockInputAssignment ext s (blocks ::> args) ret blocks
forall a b. (a -> b) -> a -> b
$ BlockInfo ext s ret blocks
-> BlockInputAssignment ext s blocks ret blocks
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> Assignment (BlockInput ext s blocks ret) blocks
biBlocks BlockInfo ext s ret blocks
bi
  let jump_info' :: JumpInfoMap s (blocks ::> args)
jump_info' = JumpInfoMap s blocks -> JumpInfoMap s (blocks ::> args)
forall s (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
JumpInfoMap s blocks -> JumpInfoMap s (blocks ::> args)
extJumpInfoMap (JumpInfoMap s blocks -> JumpInfoMap s (blocks ::> args))
-> JumpInfoMap s blocks -> JumpInfoMap s (blocks ::> args)
forall a b. (a -> b) -> a -> b
$ BlockInfo ext s ret blocks -> JumpInfoMap s blocks
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks -> JumpInfoMap s blocks
biJumpInfo BlockInfo ext s ret blocks
bi
  let switch_info' :: SwitchInfoMap s (blocks ::> args)
switch_info' = SwitchInfoMap s blocks -> SwitchInfoMap s (blocks ::> args)
forall s (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
SwitchInfoMap s blocks -> SwitchInfoMap s (blocks ::> args)
extSwitchInfoMap (SwitchInfoMap s blocks -> SwitchInfoMap s (blocks ::> args))
-> SwitchInfoMap s blocks -> SwitchInfoMap s (blocks ::> args)
forall a b. (a -> b) -> a -> b
$ BlockInfo ext s ret blocks -> SwitchInfoMap s blocks
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks -> SwitchInfoMap s blocks
biSwitchInfo BlockInfo ext s ret blocks
bi
  let breakpoints' :: Bimap BreakpointName (Some (BlockID (blocks ::> args)))
breakpoints' = Bimap BreakpointName (Some (BlockID blocks))
-> Bimap BreakpointName (Some (BlockID (blocks ::> args)))
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Bimap BreakpointName (Some (BlockID blocks))
-> Bimap BreakpointName (Some (BlockID (blocks ::> tp)))
extBreakpoints (Bimap BreakpointName (Some (BlockID blocks))
 -> Bimap BreakpointName (Some (BlockID (blocks ::> args))))
-> Bimap BreakpointName (Some (BlockID blocks))
-> Bimap BreakpointName (Some (BlockID (blocks ::> args)))
forall a b. (a -> b) -> a -> b
$ BlockInfo ext s ret blocks
-> Bimap BreakpointName (Some (BlockID blocks))
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> Bimap BreakpointName (Some (BlockID blocks))
biBreakpoints BlockInfo ext s ret blocks
bi
  BI { biBlocks :: Assignment
  (BlockInput ext s (blocks ::> args) ret) (blocks ::> args)
biBlocks = BlockInputAssignment ext s (blocks ::> args) ret blocks
-> BlockInput ext s (blocks ::> args) ret args
-> Assignment
     (BlockInput ext s (blocks ::> args) ret) (blocks ::> args)
forall {k} (f :: k -> Type) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
extend BlockInputAssignment ext s (blocks ::> args) ret blocks
blocks' BlockInput ext s (blocks ::> args) ret args
binput
     , biJumpInfo :: JumpInfoMap s (blocks ::> args)
biJumpInfo = JumpInfoMap s (blocks ::> args)
jump_info'
     , biSwitchInfo :: SwitchInfoMap s (blocks ::> args)
biSwitchInfo = SwitchInfoMap s (blocks ::> args)
switch_info'
     , biBreakpoints :: Bimap BreakpointName (Some (BlockID (blocks ::> args)))
biBreakpoints = Bimap BreakpointName (Some (BlockID (blocks ::> args)))
breakpoints'
     }

------------------------------------------------------------------------
-- PredMap

newtype PredMap ext s ret = PredMap (Map (BlockID s) [Block ext s ret])

instance Show (PredMap ext s ret) where
  show :: PredMap ext s ret -> String
show (PredMap Map (BlockID s) [Block ext s ret]
m) = Map (BlockID s) [BlockID s] -> String
forall a. Show a => a -> String
show ((Block ext s ret -> BlockID s) -> [Block ext s ret] -> [BlockID s]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID ([Block ext s ret] -> [BlockID s])
-> Map (BlockID s) [Block ext s ret] -> Map (BlockID s) [BlockID s]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (BlockID s) [Block ext s ret]
m)

-- | Return labels that may jump to given label.
getPredecessorLabels :: BlockID s -> PredMap ext s ret -> [Block ext s ret]
getPredecessorLabels :: forall s ext (ret :: CrucibleType).
BlockID s -> PredMap ext s ret -> [Block ext s ret]
getPredecessorLabels BlockID s
l (PredMap Map (BlockID s) [Block ext s ret]
m) = [Block ext s ret] -> Maybe [Block ext s ret] -> [Block ext s ret]
forall a. a -> Maybe a -> a
fromMaybe [] (BlockID s
-> Map (BlockID s) [Block ext s ret] -> Maybe [Block ext s ret]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BlockID s
l Map (BlockID s) [Block ext s ret]
m)

-- | Maps each block to the set of blocks that jump to it.
blockPredMap :: [Block ext s ret] -> PredMap ext s ret
blockPredMap :: forall ext s (ret :: CrucibleType).
[Block ext s ret] -> PredMap ext s ret
blockPredMap [Block ext s ret]
l = Map (BlockID s) [Block ext s ret] -> PredMap ext s ret
forall ext s (ret :: CrucibleType).
Map (BlockID s) [Block ext s ret] -> PredMap ext s ret
PredMap (Set (Block ext s ret) -> [Block ext s ret]
forall a. Set a -> [a]
Set.toList (Set (Block ext s ret) -> [Block ext s ret])
-> Map (BlockID s) (Set (Block ext s ret))
-> Map (BlockID s) [Block ext s ret]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(BlockID s, Block ext s ret)]
-> Map (BlockID s) (Set (Block ext s ret))
forall x y. (Ord x, Ord y) => [(x, y)] -> Map x (Set y)
nextSetMap [(BlockID s, Block ext s ret)]
pairs)
  where pairs :: [(BlockID s, Block ext s ret)]
pairs = [ (BlockID s
n, Block ext s ret
b)
                | Block ext s ret
b <- [Block ext s ret]
l
                , BlockID s
n <- [BlockID s] -> Maybe [BlockID s] -> [BlockID s]
forall a. a -> Maybe a -> a
fromMaybe [] (TermStmt s ret -> Maybe [BlockID s]
forall s (ret :: CrucibleType). TermStmt s ret -> Maybe [BlockID s]
termNextLabels (Posd (TermStmt s ret) -> TermStmt s ret
forall v. Posd v -> v
pos_val (Block ext s ret -> Posd (TermStmt s ret)
forall ext s (ret :: CrucibleType).
Block ext s ret -> Posd (TermStmt s ret)
blockTerm Block ext s ret
b)))
                ]

------------------------------------------------------------------------
-- BlockInputMap

type BlockInputMap s = Map (BlockID s) (Set (Input s))

-- | Return inputs expected by block.
inputsForBlock :: Block ext s ret
               -> Set (Input s)
inputsForBlock :: forall ext s (ret :: CrucibleType).
Block ext s ret -> Set (Input s)
inputsForBlock Block ext s ret
b = (Some (Value s) -> Input s)
-> Set (Some (Value s)) -> Set (Input s)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (BlockID s -> Some (Value s) -> Input s
forall s. BlockID s -> Some (Value s) -> Input s
mkInput (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
b)) (Block ext s ret -> Set (Some (Value s))
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockKnownInputs Block ext s ret
b)

-- | Define map that maps labels to the set of registers they need.
initialInputMap :: [Block ext s ret] -> BlockInputMap s
initialInputMap :: forall ext s (ret :: CrucibleType).
[Block ext s ret] -> BlockInputMap s
initialInputMap [Block ext s ret]
blocks = [(BlockID s, Set (Input s))] -> Map (BlockID s) (Set (Input s))
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(BlockID s, Set (Input s))] -> Map (BlockID s) (Set (Input s)))
-> [(BlockID s, Set (Input s))] -> Map (BlockID s) (Set (Input s))
forall a b. (a -> b) -> a -> b
$
  [ (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
b, Block ext s ret -> Set (Input s)
forall ext s (ret :: CrucibleType).
Block ext s ret -> Set (Input s)
inputsForBlock Block ext s ret
b)
  | Block ext s ret
b <- [Block ext s ret]
blocks
  ]

-- | Return map that stores arguments needed by each block.
completeInputs :: forall ext s ret . [Block ext s ret] -> BlockInputMap s
completeInputs :: forall ext s (ret :: CrucibleType).
[Block ext s ret] -> BlockInputMap s
completeInputs [Block ext s ret]
blocks = do
  let block_map :: Map (BlockID s) (Block ext s ret)
block_map =  [(BlockID s, Block ext s ret)] -> Map (BlockID s) (Block ext s ret)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
b, Block ext s ret
b) | Block ext s ret
b <- [Block ext s ret]
blocks ]
  -- pred_map maps each label to its predecessors.
  let pred_map :: PredMap ext s ret
pred_map = [Block ext s ret] -> PredMap ext s ret
forall ext s (ret :: CrucibleType).
[Block ext s ret] -> PredMap ext s ret
blockPredMap [Block ext s ret]
blocks
  let go :: Set (BlockID s) -- Set of blocks to revisit.
         -> BlockInputMap s
            -- Map from block labels to arguments corresponding block needs at end.
         -> BlockInputMap s
      go :: Set (BlockID s) -> BlockInputMap s -> BlockInputMap s
go Set (BlockID s)
s0 BlockInputMap s
input_map =
        case Set (BlockID s) -> Maybe (BlockID s, Set (BlockID s))
forall a. Set a -> Maybe (a, Set a)
Set.maxView Set (BlockID s)
s0 of
          Maybe (BlockID s, Set (BlockID s))
Nothing -> BlockInputMap s
input_map
          Just (BlockID s
next_label, Set (BlockID s)
rest_labels) -> do
            let inputs :: Set (Input s)
inputs = case BlockID s -> BlockInputMap s -> Maybe (Set (Input s))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BlockID s
next_label BlockInputMap s
input_map of
                           Just Set (Input s)
i -> Set (Input s)
i
                           Maybe (Set (Input s))
Nothing -> String -> [String] -> Set (Input s)
forall a. (?callStack::CallStack) => String -> [String] -> a
panic String
"Crucible.CFG.SSAConversion"
                                      [ String
"Unable to get label from input map" ]

            let resolve_pred :: [Block ext s ret]
                             -> Set (BlockID s)
                             -> BlockInputMap s
                             -> BlockInputMap s
                resolve_pred :: [Block ext s ret]
-> Set (BlockID s) -> BlockInputMap s -> BlockInputMap s
resolve_pred [] Set (BlockID s)
s BlockInputMap s
m = Set (BlockID s) -> BlockInputMap s -> BlockInputMap s
go Set (BlockID s)
s BlockInputMap s
m
                resolve_pred (Block ext s ret
prev_block:[Block ext s ret]
r) Set (BlockID s)
s BlockInputMap s
m = do
                  let prev_label :: BlockID s
prev_label = Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
prev_block
                  -- Get list of inputs already computed for block.
                  let prev_inputs :: Set (Input s)
prev_inputs = case BlockID s -> BlockInputMap s -> Maybe (Set (Input s))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BlockID s
prev_label BlockInputMap s
m of
                                      Just Set (Input s)
previ -> Set (Input s)
previ
                                      Maybe (Set (Input s))
Nothing -> String -> [String] -> Set (Input s)
forall a. (?callStack::CallStack) => String -> [String] -> a
panic String
"Crucible.CFG.SSAConversion"
                                                 [ String
"Unable to get prev_label from input map" ]
                  -- Compute the inputs needed at the start of prev_block
                  let new_inputs :: Set (Input s)
new_inputs = (Some (Value s) -> Input s)
-> Set (Some (Value s)) -> Set (Input s)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (BlockID s -> Some (Value s) -> Input s
forall s. BlockID s -> Some (Value s) -> Input s
mkInput (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
prev_block))
                                 (Set (Some (Value s)) -> Set (Input s))
-> Set (Some (Value s)) -> Set (Input s)
forall a b. (a -> b) -> a -> b
$ (Set (Some (Value s))
-> Set (Some (Value s)) -> Set (Some (Value s))
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Block ext s ret -> Set (Some (Value s))
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockAssignedValues Block ext s ret
prev_block)
                                 (Set (Some (Value s)) -> Set (Some (Value s)))
-> Set (Some (Value s)) -> Set (Some (Value s))
forall a b. (a -> b) -> a -> b
$ (Input s -> Some (Value s))
-> Set (Input s) -> Set (Some (Value s))
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Input s -> Some (Value s)
forall s. Input s -> Some (Value s)
inputValue Set (Input s)
inputs
                  let all_inputs :: Set (Input s)
all_inputs = Set (Input s) -> Set (Input s) -> Set (Input s)
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (Input s)
prev_inputs Set (Input s)
new_inputs
                  if Set (Input s) -> Set (Input s) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set (Input s)
new_inputs Set (Input s)
prev_inputs then
                    [Block ext s ret]
-> Set (BlockID s) -> BlockInputMap s -> BlockInputMap s
resolve_pred [Block ext s ret]
r Set (BlockID s)
s BlockInputMap s
m
                  else do
                    let m' :: BlockInputMap s
m' = BlockID s -> Set (Input s) -> BlockInputMap s -> BlockInputMap s
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert BlockID s
prev_label Set (Input s)
all_inputs BlockInputMap s
m
                    [Block ext s ret]
-> Set (BlockID s) -> BlockInputMap s -> BlockInputMap s
resolve_pred [Block ext s ret]
r (BlockID s -> Set (BlockID s) -> Set (BlockID s)
forall a. Ord a => a -> Set a -> Set a
Set.insert BlockID s
prev_label Set (BlockID s)
s)  BlockInputMap s
m'
            let prev_blocks :: [Block ext s ret]
prev_blocks = BlockID s -> PredMap ext s ret -> [Block ext s ret]
forall s ext (ret :: CrucibleType).
BlockID s -> PredMap ext s ret -> [Block ext s ret]
getPredecessorLabels BlockID s
next_label PredMap ext s ret
pred_map
            [Block ext s ret]
-> Set (BlockID s) -> BlockInputMap s -> BlockInputMap s
resolve_pred [Block ext s ret]
prev_blocks Set (BlockID s)
rest_labels BlockInputMap s
input_map
  -- Compute arguments to each block.
  Set (BlockID s) -> BlockInputMap s -> BlockInputMap s
go (Map (BlockID s) (Block ext s ret) -> Set (BlockID s)
forall k a. Map k a -> Set k
Map.keysSet Map (BlockID s) (Block ext s ret)
block_map) ([Block ext s ret] -> BlockInputMap s
forall ext s (ret :: CrucibleType).
[Block ext s ret] -> BlockInputMap s
initialInputMap [Block ext s ret]
blocks)

------------------------------------------------------------------------
-- Infer information about SSA.

-- | Information that is statically inferred from the block structure.
data BlockInfo ext s ret blocks
   = BI { forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> Assignment (BlockInput ext s blocks ret) blocks
biBlocks      :: !(Assignment (BlockInput ext s blocks ret) blocks)
        , forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks -> JumpInfoMap s blocks
biJumpInfo    :: !(JumpInfoMap s blocks)
        , forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks -> SwitchInfoMap s blocks
biSwitchInfo  :: !(SwitchInfoMap s blocks)
        , forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> Bimap BreakpointName (Some (BlockID blocks))
biBreakpoints :: !(Bimap BreakpointName (Some (C.BlockID blocks)))
        }

-- | This infers the information given a set of blocks.
inferBlockInfo :: forall ext s ret . [Block ext s ret] -> Some (BlockInfo ext s ret)
inferBlockInfo :: forall ext s (ret :: CrucibleType).
[Block ext s ret] -> Some (BlockInfo ext s ret)
inferBlockInfo [Block ext s ret]
blocks = BlockInputMap s
-> Some (BlockInfo ext s ret) -> Some (BlockInfo ext s ret)
forall a b. a -> b -> b
seq BlockInputMap s
input_map (Some (BlockInfo ext s ret) -> Some (BlockInfo ext s ret))
-> Some (BlockInfo ext s ret) -> Some (BlockInfo ext s ret)
forall a b. (a -> b) -> a -> b
$ BlockInfo ext s ret EmptyCtx
-> [Block ext s ret] -> Some (BlockInfo ext s ret)
forall (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> [Block ext s ret] -> Some (BlockInfo ext s ret)
resolveBlocks BlockInfo ext s ret EmptyCtx
forall {ext} {s} {ret :: CrucibleType}.
BlockInfo ext s ret EmptyCtx
bi0 [Block ext s ret]
blocks
  where input_map :: BlockInputMap s
input_map = [Block ext s ret] -> BlockInputMap s
forall ext s (ret :: CrucibleType).
[Block ext s ret] -> BlockInputMap s
completeInputs [Block ext s ret]
blocks
        bi0 :: BlockInfo ext s ret EmptyCtx
bi0 = BI { biBlocks :: Assignment (BlockInput ext s EmptyCtx ret) EmptyCtx
biBlocks = Assignment (BlockInput ext s EmptyCtx ret) EmptyCtx
forall {k} (f :: k -> Type). Assignment f EmptyCtx
empty
                 , biJumpInfo :: JumpInfoMap s EmptyCtx
biJumpInfo = JumpInfoMap s EmptyCtx
forall s (blocks :: Ctx (Ctx CrucibleType)). JumpInfoMap s blocks
emptyJumpInfoMap
                 , biSwitchInfo :: SwitchInfoMap s EmptyCtx
biSwitchInfo = SwitchInfoMap s EmptyCtx
forall s (blocks :: Ctx (Ctx CrucibleType)). SwitchInfoMap s blocks
emptySwitchInfoMap
                 , biBreakpoints :: Bimap BreakpointName (Some (BlockID EmptyCtx))
biBreakpoints = Bimap BreakpointName (Some (BlockID EmptyCtx))
forall a b. Bimap a b
Bimap.empty
                 }
        resolveBlocks ::
          BlockInfo ext s ret blocks ->
          [Block ext s ret] ->
          Some (BlockInfo ext s ret)
        resolveBlocks :: forall (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> [Block ext s ret] -> Some (BlockInfo ext s ret)
resolveBlocks BlockInfo ext s ret blocks
bi [] = BlockInfo ext s ret blocks -> Some (BlockInfo ext s ret)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockInfo ext s ret blocks
bi
        resolveBlocks BlockInfo ext s ret blocks
bi (Block ext s ret
b:[Block ext s ret]
rest) = do
          let sz :: Size blocks
sz = Assignment (BlockInput ext s blocks ret) blocks -> Size blocks
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size (BlockInfo ext s ret blocks
-> Assignment (BlockInput ext s blocks ret) blocks
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> Assignment (BlockInput ext s blocks ret) blocks
biBlocks BlockInfo ext s ret blocks
bi)
          let untyped_id :: BlockID s
untyped_id = Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
b
          let inputs :: Set (Input s)
inputs = case BlockID s -> BlockInputMap s -> Maybe (Set (Input s))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BlockID s
untyped_id BlockInputMap s
input_map of
                         Just Set (Input s)
i -> Set (Input s)
i
                         Maybe (Set (Input s))
Nothing -> String -> [String] -> Set (Input s)
forall a. (?callStack::CallStack) => String -> [String] -> a
panic String
"Crucible.CFG.SSAConversion.inferBlockInfo"
                                    [ String
"Unable to get untyped_id from input map" ]
          case Set (Input s) -> Some (Assignment (Value s))
forall s. Set (Input s) -> Some (Assignment (Value s))
inferRegAssignment Set (Input s)
inputs of
            Some Assignment (Value s) x
ra -> do
              let crepr :: Assignment TypeRepr x
crepr = (forall (x :: CrucibleType). Value s x -> TypeRepr x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Value s) x -> Assignment TypeRepr 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 Value s x -> TypeRepr x
forall s (tp :: CrucibleType). Value s tp -> TypeRepr tp
forall (x :: CrucibleType). Value s x -> TypeRepr x
typeOfValue Assignment (Value s) x
ra
              case BlockID s
untyped_id of
                LabelID Label s
l -> do
                  let block_id :: BlockID (blocks ::> x) x
block_id = Index (blocks ::> x) x -> BlockID (blocks ::> x) x
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Index blocks tp -> BlockID blocks tp
C.BlockID (Size blocks -> Index (blocks ::> x) x
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size blocks
sz)
                  let block_term :: Posd (ExtendedTermStmt s (blocks ::> x) ret)
block_term = (Block ext s ret -> Posd (TermStmt s ret)
forall ext s (ret :: CrucibleType).
Block ext s ret -> Posd (TermStmt s ret)
blockTerm Block ext s ret
b) { pos_val = BaseTermStmt $ pos_val $ blockTerm b }
                  let binput :: BlockInput ext s (blocks ::> x) ret x
binput = BInput { binputID :: BlockID (blocks ::> x) x
binputID = BlockID (blocks ::> x) x
block_id
                                      , binputArgs :: Assignment (Value s) x
binputArgs    = Assignment (Value s) x
ra
                                      , binputStmts :: Seq (Posd (Stmt ext s))
binputStmts   = Block ext s ret -> Seq (Posd (Stmt ext s))
forall ext s (ret :: CrucibleType).
Block ext s ret -> Seq (Posd (Stmt ext s))
blockStmts Block ext s ret
b
                                      , binputTerm :: Posd (ExtendedTermStmt s (blocks ::> x) ret)
binputTerm    = Posd (ExtendedTermStmt s (blocks ::> x) ret)
block_term
                                      }
                  let bi' :: BlockInfo ext s ret (blocks ::> x)
bi' = BlockInfo ext s ret blocks
-> BlockInput ext s (blocks ::> x) ret x
-> BlockInfo ext s ret (blocks ::> x)
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (args :: Ctx CrucibleType).
BlockInfo ext s ret blocks
-> BlockInput ext s (blocks ::> args) ret args
-> BlockInfo ext s ret (blocks ::> args)
extBlockInfo BlockInfo ext s ret blocks
bi BlockInput ext s (blocks ::> x) ret x
binput
                  let ji :: JumpInfo s (blocks ::> x)
ji = BlockID (blocks ::> x) x
-> Assignment TypeRepr x
-> Assignment (Value s) x
-> JumpInfo s (blocks ::> x)
forall (blocks :: Ctx (Ctx CrucibleType))
       (blocks :: Ctx CrucibleType) s.
BlockID blocks blocks
-> CtxRepr blocks
-> Assignment (Value s) blocks
-> JumpInfo s blocks
JumpInfo BlockID (blocks ::> x) x
block_id Assignment TypeRepr x
crepr Assignment (Value s) x
ra
                  let bi'' :: BlockInfo ext s ret (blocks ::> x)
bi'' = BlockInfo ext s ret (blocks ::> x)
bi' { biJumpInfo = insertJumpInfo l ji (biJumpInfo bi') }
                  BlockInfo ext s ret (blocks ::> x)
-> [Block ext s ret] -> Some (BlockInfo ext s ret)
forall (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> [Block ext s ret] -> Some (BlockInfo ext s ret)
splitLastBlockInputOnBreakpoints BlockInfo ext s ret (blocks ::> x)
bi'' [Block ext s ret]
rest
                LambdaID LambdaLabel s tp
l -> do
                  let block_id :: BlockID (blocks ::> (x ::> tp)) (x ::> tp)
block_id = Index (blocks ::> (x ::> tp)) (x ::> tp)
-> BlockID (blocks ::> (x ::> tp)) (x ::> tp)
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Index blocks tp -> BlockID blocks tp
C.BlockID (Size blocks -> Index (blocks ::> (x ::> tp)) (x ::> tp)
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size blocks
sz)
                  let lastArg :: Value s tp
lastArg = Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue (LambdaLabel s tp -> Atom s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Atom s tp
lambdaAtom LambdaLabel s tp
l)
                  let block_term :: Posd (ExtendedTermStmt s (blocks ::> (x ::> tp)) ret)
block_term = (Block ext s ret -> Posd (TermStmt s ret)
forall ext s (ret :: CrucibleType).
Block ext s ret -> Posd (TermStmt s ret)
blockTerm Block ext s ret
b) { pos_val = BaseTermStmt $ pos_val $ blockTerm b }
                  let binput :: BlockInput ext s (blocks ::> (x ::> tp)) ret (x ::> tp)
binput = BInput { binputID :: BlockID (blocks ::> (x ::> tp)) (x ::> tp)
binputID = BlockID (blocks ::> (x ::> tp)) (x ::> tp)
block_id
                                      , binputArgs :: Assignment (Value s) (x ::> tp)
binputArgs = Assignment (Value s) x
ra Assignment (Value s) x
-> Value s tp -> Assignment (Value s) (x ::> tp)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> Value s tp
lastArg
                                      , binputStmts :: Seq (Posd (Stmt ext s))
binputStmts = Block ext s ret -> Seq (Posd (Stmt ext s))
forall ext s (ret :: CrucibleType).
Block ext s ret -> Seq (Posd (Stmt ext s))
blockStmts Block ext s ret
b
                                      , binputTerm :: Posd (ExtendedTermStmt s (blocks ::> (x ::> tp)) ret)
binputTerm = Posd (ExtendedTermStmt s (blocks ::> (x ::> tp)) ret)
block_term
                                      }
                  let bi' :: BlockInfo ext s ret (blocks ::> (x ::> tp))
bi' = BlockInfo ext s ret blocks
-> BlockInput ext s (blocks ::> (x ::> tp)) ret (x ::> tp)
-> BlockInfo ext s ret (blocks ::> (x ::> tp))
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (args :: Ctx CrucibleType).
BlockInfo ext s ret blocks
-> BlockInput ext s (blocks ::> args) ret args
-> BlockInfo ext s ret (blocks ::> args)
extBlockInfo BlockInfo ext s ret blocks
bi BlockInput ext s (blocks ::> (x ::> tp)) ret (x ::> tp)
binput
                  let si :: SwitchInfo s (blocks ::> (x ::> tp)) tp
si = BlockID (blocks ::> (x ::> tp)) (x ::> tp)
-> Assignment TypeRepr x
-> Assignment (Value s) x
-> SwitchInfo s (blocks ::> (x ::> tp)) tp
forall (blocks :: Ctx (Ctx CrucibleType))
       (blocks :: Ctx CrucibleType) (tp :: CrucibleType) s.
BlockID blocks (blocks ::> tp)
-> CtxRepr blocks
-> Assignment (Value s) blocks
-> SwitchInfo s blocks tp
SwitchInfo BlockID (blocks ::> (x ::> tp)) (x ::> tp)
block_id Assignment TypeRepr x
crepr Assignment (Value s) x
ra
                  let bi'' :: BlockInfo ext s ret (blocks ::> (x ::> tp))
bi'' = BlockInfo ext s ret (blocks ::> (x ::> tp))
bi' { biSwitchInfo = insertSwitchInfo l si (biSwitchInfo bi') }
                  BlockInfo ext s ret (blocks ::> (x ::> tp))
-> [Block ext s ret] -> Some (BlockInfo ext s ret)
forall (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> [Block ext s ret] -> Some (BlockInfo ext s ret)
splitLastBlockInputOnBreakpoints BlockInfo ext s ret (blocks ::> (x ::> tp))
bi'' [Block ext s ret]
rest
        splitLastBlockInputOnBreakpoints ::
          BlockInfo ext s ret blocks ->
          [Block ext s ret] ->
          Some (BlockInfo ext s ret)
        splitLastBlockInputOnBreakpoints :: forall (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> [Block ext s ret] -> Some (BlockInfo ext s ret)
splitLastBlockInputOnBreakpoints BlockInfo ext s ret blocks
bi [Block ext s ret]
rest
          | Assignment (BlockInput ext s blocks ret) ctx
first_binputs :> BlockInput ext s blocks ret tp
last_binput <- BlockInfo ext s ret blocks
-> Assignment (BlockInput ext s blocks ret) blocks
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> Assignment (BlockInput ext s blocks ret) blocks
biBlocks BlockInfo ext s ret blocks
bi
          , (Seq (Posd (Stmt ext s))
first_stmts, Posd (Stmt ext s)
break_stmt Seq.:<| Seq (Posd (Stmt ext s))
last_stmts) <-
              (Posd (Stmt ext s) -> Bool)
-> Seq (Posd (Stmt ext s))
-> (Seq (Posd (Stmt ext s)), Seq (Posd (Stmt ext s)))
forall a. (a -> Bool) -> Seq a -> (Seq a, Seq a)
Seq.breakl Posd (Stmt ext s) -> Bool
isBreakpoint (BlockInput ext s blocks ret tp -> Seq (Posd (Stmt ext s))
forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType).
BlockInput ext s blocks ret args -> Seq (Posd (Stmt ext s))
binputStmts BlockInput ext s blocks ret tp
last_binput)
          , Breakpoint BreakpointName
nm Assignment (Value s) args
args <- Posd (Stmt ext s) -> Stmt ext s
forall v. Posd v -> v
pos_val Posd (Stmt ext s)
break_stmt = do
            let block_id :: BlockID (blocks ::> args) args
block_id = Index (blocks ::> args) args -> BlockID (blocks ::> args) args
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Index blocks tp -> BlockID blocks tp
C.BlockID (Index (blocks ::> args) args -> BlockID (blocks ::> args) args)
-> Index (blocks ::> args) args -> BlockID (blocks ::> args) args
forall a b. (a -> b) -> a -> b
$ Size blocks -> Index (blocks ::> args) args
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex (Size blocks -> Index (blocks ::> args) args)
-> Size blocks -> Index (blocks ::> args) args
forall a b. (a -> b) -> a -> b
$ Assignment (BlockInput ext s blocks ret) blocks -> Size blocks
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size (Assignment (BlockInput ext s blocks ret) blocks -> Size blocks)
-> Assignment (BlockInput ext s blocks ret) blocks -> Size blocks
forall a b. (a -> b) -> a -> b
$ BlockInfo ext s ret blocks
-> Assignment (BlockInput ext s blocks ret) blocks
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> Assignment (BlockInput ext s blocks ret) blocks
biBlocks BlockInfo ext s ret blocks
bi

            let first_binputs' :: BlockInputAssignment ext s (blocks ::> args) ret ctx
first_binputs' = Assignment (BlockInput ext s blocks ret) ctx
-> BlockInputAssignment ext s (blocks ::> args) ret ctx
forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (a :: Ctx (Ctx CrucibleType))
       (tp :: Ctx CrucibleType).
BlockInputAssignment ext s blocks ret a
-> BlockInputAssignment ext s (blocks ::> tp) ret a
extBlockInputAssignment (Assignment (BlockInput ext s blocks ret) ctx
 -> BlockInputAssignment ext s (blocks ::> args) ret ctx)
-> Assignment (BlockInput ext s blocks ret) ctx
-> BlockInputAssignment ext s (blocks ::> args) ret ctx
forall a b. (a -> b) -> a -> b
$ Assignment (BlockInput ext s blocks ret) ctx
first_binputs

            let jump_info :: JumpInfo s (blocks ::> args)
jump_info = BlockID (blocks ::> args) args
-> CtxRepr args
-> Assignment (Value s) args
-> JumpInfo s (blocks ::> args)
forall (blocks :: Ctx (Ctx CrucibleType))
       (blocks :: Ctx CrucibleType) s.
BlockID blocks blocks
-> CtxRepr blocks
-> Assignment (Value s) blocks
-> JumpInfo s blocks
JumpInfo BlockID (blocks ::> args) args
block_id ((forall (x :: CrucibleType). Value s x -> TypeRepr x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Value s) x -> Assignment TypeRepr 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 Value s x -> TypeRepr x
forall s (tp :: CrucibleType). Value s tp -> TypeRepr tp
forall (x :: CrucibleType). Value s x -> TypeRepr x
typeOfValue Assignment (Value s) args
args) Assignment (Value s) args
args
            let last_binput' :: BlockInput ext s (blocks ::> args) ret tp
last_binput' = (BlockInput ext s blocks ret tp
-> BlockInput ext s (blocks ::> args) ret tp
forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (tp :: Ctx CrucibleType) (arg :: Ctx CrucibleType).
BlockInput ext s blocks ret args
-> BlockInput ext s (blocks ::> tp) ret arg
extBlockInput BlockInput ext s blocks ret tp
last_binput)
                  { binputStmts = first_stmts
                  , binputTerm = break_stmt { pos_val = BreakStmt jump_info }
                  }

            let new_binput :: BlockInput ext s (blocks ::> args) ret args
new_binput = (BlockInput ext s blocks ret tp
-> BlockInput ext s (blocks ::> args) ret Any
forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (tp :: Ctx CrucibleType) (arg :: Ctx CrucibleType).
BlockInput ext s blocks ret args
-> BlockInput ext s (blocks ::> tp) ret arg
extBlockInput BlockInput ext s blocks ret tp
last_binput)
                  { binputID = block_id
                  , binputArgs = args
                  , binputStmts = last_stmts
                  }

            let new_breakpoints :: Bimap BreakpointName (Some (BlockID (blocks ::> args)))
new_breakpoints = do
                  let try_new_breakpoints :: Bimap BreakpointName (Some (BlockID (blocks ::> args)))
try_new_breakpoints = BreakpointName
-> Some (BlockID (blocks ::> args))
-> Bimap BreakpointName (Some (BlockID (blocks ::> args)))
-> Bimap BreakpointName (Some (BlockID (blocks ::> args)))
forall a b. (Ord a, Ord b) => a -> b -> Bimap a b -> Bimap a b
Bimap.tryInsert BreakpointName
nm (BlockID (blocks ::> args) args -> Some (BlockID (blocks ::> args))
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID (blocks ::> args) args
block_id) (Bimap BreakpointName (Some (BlockID (blocks ::> args)))
 -> Bimap BreakpointName (Some (BlockID (blocks ::> args))))
-> Bimap BreakpointName (Some (BlockID (blocks ::> args)))
-> Bimap BreakpointName (Some (BlockID (blocks ::> args)))
forall a b. (a -> b) -> a -> b
$
                        Bimap BreakpointName (Some (BlockID blocks))
-> Bimap BreakpointName (Some (BlockID (blocks ::> args)))
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Bimap BreakpointName (Some (BlockID blocks))
-> Bimap BreakpointName (Some (BlockID (blocks ::> tp)))
extBreakpoints (Bimap BreakpointName (Some (BlockID blocks))
 -> Bimap BreakpointName (Some (BlockID (blocks ::> args))))
-> Bimap BreakpointName (Some (BlockID blocks))
-> Bimap BreakpointName (Some (BlockID (blocks ::> args)))
forall a b. (a -> b) -> a -> b
$ BlockInfo ext s ret blocks
-> Bimap BreakpointName (Some (BlockID blocks))
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> Bimap BreakpointName (Some (BlockID blocks))
biBreakpoints BlockInfo ext s ret blocks
bi
                  if (BreakpointName, Some (BlockID (blocks ::> args)))
-> Bimap BreakpointName (Some (BlockID (blocks ::> args))) -> Bool
forall a b. (Ord a, Ord b) => (a, b) -> Bimap a b -> Bool
Bimap.pairMember (BreakpointName
nm, (BlockID (blocks ::> args) args -> Some (BlockID (blocks ::> args))
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID (blocks ::> args) args
block_id)) Bimap BreakpointName (Some (BlockID (blocks ::> args)))
try_new_breakpoints
                    then Bimap BreakpointName (Some (BlockID (blocks ::> args)))
try_new_breakpoints
                    else String -> Bimap BreakpointName (Some (BlockID (blocks ::> args)))
forall a. (?callStack::CallStack) => String -> a
error (String -> Bimap BreakpointName (Some (BlockID (blocks ::> args))))
-> String
-> Bimap BreakpointName (Some (BlockID (blocks ::> args)))
forall a b. (a -> b) -> a -> b
$ String
"Duplicate breakpoint: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BreakpointName -> String
forall a. Show a => a -> String
show BreakpointName
nm
            let bi' :: BlockInfo ext s ret (blocks ::> args)
bi' = BI
                  { biBlocks :: Assignment
  (BlockInput ext s (blocks ::> args) ret) (blocks ::> args)
biBlocks = BlockInputAssignment ext s (blocks ::> args) ret ctx
first_binputs' BlockInputAssignment ext s (blocks ::> args) ret ctx
-> BlockInput ext s (blocks ::> args) ret tp
-> Assignment (BlockInput ext s (blocks ::> args) ret) (ctx ::> tp)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BlockInput ext s (blocks ::> args) ret tp
last_binput' Assignment (BlockInput ext s (blocks ::> args) ret) (ctx ::> tp)
-> BlockInput ext s (blocks ::> args) ret args
-> Assignment
     (BlockInput ext s (blocks ::> args) ret) (blocks ::> args)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BlockInput ext s (blocks ::> args) ret args
new_binput
                  , biJumpInfo :: JumpInfoMap s (blocks ::> args)
biJumpInfo = JumpInfoMap s blocks -> JumpInfoMap s (blocks ::> args)
forall s (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
JumpInfoMap s blocks -> JumpInfoMap s (blocks ::> args)
extJumpInfoMap (JumpInfoMap s blocks -> JumpInfoMap s (blocks ::> args))
-> JumpInfoMap s blocks -> JumpInfoMap s (blocks ::> args)
forall a b. (a -> b) -> a -> b
$ BlockInfo ext s ret blocks -> JumpInfoMap s blocks
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks -> JumpInfoMap s blocks
biJumpInfo BlockInfo ext s ret blocks
bi
                  , biSwitchInfo :: SwitchInfoMap s (blocks ::> args)
biSwitchInfo = SwitchInfoMap s blocks -> SwitchInfoMap s (blocks ::> args)
forall s (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
SwitchInfoMap s blocks -> SwitchInfoMap s (blocks ::> args)
extSwitchInfoMap (SwitchInfoMap s blocks -> SwitchInfoMap s (blocks ::> args))
-> SwitchInfoMap s blocks -> SwitchInfoMap s (blocks ::> args)
forall a b. (a -> b) -> a -> b
$ BlockInfo ext s ret blocks -> SwitchInfoMap s blocks
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks -> SwitchInfoMap s blocks
biSwitchInfo BlockInfo ext s ret blocks
bi
                  , biBreakpoints :: Bimap BreakpointName (Some (BlockID (blocks ::> args)))
biBreakpoints = Bimap BreakpointName (Some (BlockID (blocks ::> args)))
new_breakpoints
                  }
            BlockInfo ext s ret (blocks ::> args)
-> [Block ext s ret] -> Some (BlockInfo ext s ret)
forall (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> [Block ext s ret] -> Some (BlockInfo ext s ret)
splitLastBlockInputOnBreakpoints BlockInfo ext s ret (blocks ::> args)
bi' [Block ext s ret]
rest
        splitLastBlockInputOnBreakpoints BlockInfo ext s ret blocks
bi [Block ext s ret]
rest = BlockInfo ext s ret blocks
-> [Block ext s ret] -> Some (BlockInfo ext s ret)
forall (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> [Block ext s ret] -> Some (BlockInfo ext s ret)
resolveBlocks BlockInfo ext s ret blocks
bi [Block ext s ret]
rest
        isBreakpoint :: Posd (Stmt ext s) -> Bool
        isBreakpoint :: Posd (Stmt ext s) -> Bool
isBreakpoint = \case
          Posd Position
_ Breakpoint{} -> Bool
True
          Posd (Stmt ext s)
_ -> Bool
False


------------------------------------------------------------------------
-- Translates from RTL with inference information to SSA.

data MaybeF f tp where
  JustF :: f tp -> MaybeF f tp
  NothingF :: MaybeF f tp

-- | Map each core SSA binding to the expression that generated it if it
-- was generated by an expression.
type RegExprs ext ctx = Assignment (MaybeF (C.Expr ext ctx)) ctx

#ifdef UNSAFE_OPS

extendRegExprs :: MaybeF (C.Expr ext ctx) tp -> RegExprs ext ctx -> RegExprs ext (ctx ::> tp)
extendRegExprs :: forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
MaybeF (Expr ext ctx) tp
-> RegExprs ext ctx -> RegExprs ext (ctx ::> tp)
extendRegExprs MaybeF (Expr ext ctx) tp
r RegExprs ext ctx
e = Assignment (MaybeF (Expr ext ctx)) (ctx ::> tp)
-> RegExprs ext (ctx ::> tp)
forall a b. a -> b
unsafeCoerce (RegExprs ext ctx
e RegExprs ext ctx
-> MaybeF (Expr ext ctx) tp
-> Assignment (MaybeF (Expr ext ctx)) (ctx ::> tp)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> MaybeF (Expr ext ctx) tp
r)

-- | Maps values in mutable representation to the current value in the SSA form.
newtype TypedRegMap s ctx = TypedRegMap { forall s (ctx :: Ctx CrucibleType).
TypedRegMap s ctx -> MapF (Value s) (Reg ctx)
_typedRegMap :: MapF (Value s) (C.Reg ctx) }

-- | Resolve a register
resolveReg :: TypedRegMap s ctx -> Value s tp -> C.Reg ctx tp
resolveReg :: forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Value s tp -> Reg ctx tp
resolveReg (TypedRegMap MapF (Value s) (Reg ctx)
m) Value s tp
r = Reg ctx tp -> Maybe (Reg ctx tp) -> Reg ctx tp
forall a. a -> Maybe a -> a
fromMaybe (String -> Reg ctx tp
forall a. (?callStack::CallStack) => String -> a
error String
msg) (Value s tp -> MapF (Value s) (Reg ctx) -> Maybe (Reg ctx tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup Value s tp
r MapF (Value s) (Reg ctx)
m)
  where msg :: String
msg = String
"Cannot find (unsafe) reg value " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value s tp -> String
forall a. Show a => a -> String
show Value s tp
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
              String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"in TypedRegMap: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (MapF (Value s) (Reg ctx) -> String
forall a. Show a => a -> String
show MapF (Value s) (Reg ctx)
m)

-- | Resolve an atom
resolveAtom :: TypedRegMap s ctx -> Atom s tp -> C.Reg ctx tp
resolveAtom :: forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom (TypedRegMap MapF (Value s) (Reg ctx)
m) Atom s tp
r = Reg ctx tp -> Maybe (Reg ctx tp) -> Reg ctx tp
forall a. a -> Maybe a -> a
fromMaybe (String -> Reg ctx tp
forall a. (?callStack::CallStack) => String -> a
error String
msg) (Value s tp -> MapF (Value s) (Reg ctx) -> Maybe (Reg ctx tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
r) MapF (Value s) (Reg ctx)
m)
  where msg :: String
msg = String
"Cannot find (unsafe) atom value " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Atom s tp -> String
forall a. Show a => a -> String
show Atom s tp
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."

regMapFromAssignment :: forall s args
                      . Assignment (Value s) args
                     -> TypedRegMap s args
regMapFromAssignment :: forall s (args :: Ctx CrucibleType).
Assignment (Value s) args -> TypedRegMap s args
regMapFromAssignment Assignment (Value s) args
a = MapF (Value s) (Reg args) -> TypedRegMap s args
forall s (ctx :: Ctx CrucibleType).
MapF (Value s) (Reg ctx) -> TypedRegMap s ctx
TypedRegMap (MapF (Value s) (Reg args) -> TypedRegMap s args)
-> MapF (Value s) (Reg args) -> TypedRegMap s args
forall a b. (a -> b) -> a -> b
$ Size args
-> (forall (tp :: CrucibleType).
    MapF (Value s) (Reg args)
    -> Index args tp -> MapF (Value s) (Reg args))
-> MapF (Value s) (Reg args)
-> MapF (Value s) (Reg args)
forall {k} (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
forIndex (Assignment (Value s) args -> Size args
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size Assignment (Value s) args
a) MapF (Value s) (Reg args)
-> Index args tp -> MapF (Value s) (Reg args)
forall (tp :: CrucibleType).
MapF (Value s) (Reg args)
-> Index args tp -> MapF (Value s) (Reg args)
go MapF (Value s) (Reg args)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
  where go :: MapF (Value s) (C.Reg args)
           -> Index args tp
           -> MapF (Value s) (C.Reg args)
        go :: forall (tp :: CrucibleType).
MapF (Value s) (Reg args)
-> Index args tp -> MapF (Value s) (Reg args)
go MapF (Value s) (Reg args)
m Index args tp
i = Value s tp
-> Reg args tp
-> MapF (Value s) (Reg args)
-> MapF (Value s) (Reg args)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert (Assignment (Value s) args
a Assignment (Value s) args -> Index args tp -> Value s tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Index args tp
i) (Index args tp -> Reg args tp
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Index ctx tp -> Reg ctx tp
C.Reg Index args tp
i) MapF (Value s) (Reg args)
m

extendRegMap :: TypedRegMap s ctx
             -> TypedRegMap s (ctx ::> tp)
extendRegMap :: forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> TypedRegMap s (ctx ::> tp)
extendRegMap = TypedRegMap s ctx -> TypedRegMap s (ctx ::> tp)
forall a b. a -> b
unsafeCoerce

-- | Assign existing register to atom in typed RegMap.
bindValueReg
    :: Value s tp
    -> C.Reg ctx tp
    -> TypedRegMap s ctx
    -> TypedRegMap s ctx
bindValueReg :: forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp -> Reg ctx tp -> TypedRegMap s ctx -> TypedRegMap s ctx
bindValueReg Value s tp
r Reg ctx tp
cr (TypedRegMap MapF (Value s) (Reg ctx)
m) = MapF (Value s) (Reg ctx) -> TypedRegMap s ctx
forall s (ctx :: Ctx CrucibleType).
MapF (Value s) (Reg ctx) -> TypedRegMap s ctx
TypedRegMap (MapF (Value s) (Reg ctx) -> TypedRegMap s ctx)
-> MapF (Value s) (Reg ctx) -> TypedRegMap s ctx
forall a b. (a -> b) -> a -> b
$ Value s tp
-> Reg ctx tp
-> MapF (Value s) (Reg ctx)
-> MapF (Value s) (Reg ctx)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert Value s tp
r Reg ctx tp
cr MapF (Value s) (Reg ctx)
m

#else

extendRegExprs :: MaybeF (C.Expr ext ctx) tp -> RegExprs ext ctx -> RegExprs ext (ctx ::> tp)
extendRegExprs r e = fmapFC ext e :> ext r
 where ext :: MaybeF (C.Expr ctx) tp' -> MaybeF (C.Expr (ctx ::> tp)) tp'
       ext NothingF  = NothingF
       ext (JustF (C.App app)) = JustF (C.App (C.mapApp C.extendReg app))

data SomeReg ctx where
   SomeReg :: C.TypeRepr tp -> C.Reg ctx tp -> SomeReg ctx

newtype TypedRegMap s ctx = TypedRegMap { _typedRegMap :: Map (Some (Value s)) (SomeReg ctx) }

-- | Resolve a register
resolveReg :: TypedRegMap s ctx -> Value s tp -> C.Reg ctx tp
resolveReg (TypedRegMap m) r = creg
  where creg = case Map.lookup (Some r) m of
                 Nothing -> error msg
                 Just (SomeReg tr r') ->
                    case testEquality tr (typeOfValue r) of
                       Nothing -> error msg
                       Just Refl -> r'

        msg = "Cannot find (safe) reg value " ++ show r

-- | Resolve an atom
resolveAtom :: TypedRegMap s ctx -> Atom s tp -> C.Reg ctx tp
resolveAtom m a = resolveReg m (AtomValue a)

regMapFromAssignment :: forall s args
                      . Assignment (Value s) args
                     -> TypedRegMap s args
regMapFromAssignment a = TypedRegMap $ forIndex (size a) go Map.empty
  where go :: Map (Some (Value s)) (SomeReg args)
           -> Index args tp
           -> Map (Some (Value s)) (SomeReg args)
        go m i =
             let r = a ! i
              in Map.insert (Some r) (SomeReg (typeOfValue r) (C.Reg i)) m

extendRegMap :: TypedRegMap s ctx
             -> TypedRegMap s (ctx ::> tp)
extendRegMap (TypedRegMap m) =
  TypedRegMap $ fmap (\(SomeReg tr x) -> SomeReg tr (C.extendReg x)) m

-- | Assign existing register to atom in typed RegMap.
bindValueReg
    :: Value s tp
    -> C.Reg ctx tp
    -> TypedRegMap s ctx
    -> TypedRegMap s ctx
bindValueReg r cr (TypedRegMap m) =
  TypedRegMap $ Map.insert (Some r) (SomeReg (typeOfValue r) cr) m

#endif

-- | Assign new register to value in typed reg map.
assignRegister
    :: Value s tp
    -> Size ctx
    -> TypedRegMap s ctx
    -> TypedRegMap s (ctx ::> tp)
assignRegister :: forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx ::> tp)
assignRegister Value s tp
r Size ctx
sz TypedRegMap s ctx
m =
  Value s tp
-> Reg (ctx ::> tp) tp
-> TypedRegMap s (ctx ::> tp)
-> TypedRegMap s (ctx ::> tp)
forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp -> Reg ctx tp -> TypedRegMap s ctx -> TypedRegMap s ctx
bindValueReg Value s tp
r (Index (ctx ::> tp) tp -> Reg (ctx ::> tp) tp
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Index ctx tp -> Reg ctx tp
C.Reg (Size ctx -> Index (ctx ::> tp) tp
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size ctx
sz)) (TypedRegMap s ctx -> TypedRegMap s (ctx ::> tp)
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> TypedRegMap s (ctx ::> tp)
extendRegMap TypedRegMap s ctx
m)

copyValue
    :: Value s tp -- ^ Assign
    -> Value s tp
    -> TypedRegMap s ctx
    -> TypedRegMap s ctx
copyValue :: forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp -> Value s tp -> TypedRegMap s ctx -> TypedRegMap s ctx
copyValue Value s tp
r Value s tp
r' TypedRegMap s ctx
m = Value s tp -> Reg ctx tp -> TypedRegMap s ctx -> TypedRegMap s ctx
forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp -> Reg ctx tp -> TypedRegMap s ctx -> TypedRegMap s ctx
bindValueReg Value s tp
r (TypedRegMap s ctx -> Value s tp -> Reg ctx tp
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Value s tp -> Reg ctx tp
resolveReg TypedRegMap s ctx
m Value s tp
r') TypedRegMap s ctx
m


resolveJumpTarget :: BlockInfo ext s ret blocks
                  -> TypedRegMap s ctx
                  -> Label s
                  -> C.JumpTarget blocks ctx
resolveJumpTarget :: forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx -> Label s -> JumpTarget blocks ctx
resolveJumpTarget BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map Label s
next_lbl = do
  case Label s -> JumpInfoMap s blocks -> Maybe (JumpInfo s blocks)
forall s (blocks :: Ctx (Ctx CrucibleType)).
Label s -> JumpInfoMap s blocks -> Maybe (JumpInfo s blocks)
lookupJumpInfo Label s
next_lbl (BlockInfo ext s ret blocks -> JumpInfoMap s blocks
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks -> JumpInfoMap s blocks
biJumpInfo BlockInfo ext s ret blocks
bi) of
    Maybe (JumpInfo s blocks)
Nothing -> String -> JumpTarget blocks ctx
forall a. (?callStack::CallStack) => String -> a
error String
"Could not find label in resolveJumpTarget"
    Just (JumpInfo BlockID blocks types
next_id CtxRepr types
types Assignment (Value s) types
inputs) -> do
      let args :: Assignment (Reg ctx) types
args = (forall (x :: CrucibleType). Value s x -> Reg ctx x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Value s) x -> Assignment (Reg ctx) 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 (TypedRegMap s ctx -> Value s x -> Reg ctx x
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Value s tp -> Reg ctx tp
resolveReg TypedRegMap s ctx
reg_map) Assignment (Value s) types
inputs
      BlockID blocks types
-> CtxRepr types
-> Assignment (Reg ctx) types
-> JumpTarget blocks ctx
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) (ctx :: Ctx CrucibleType).
BlockID blocks args
-> CtxRepr args
-> Assignment (Reg ctx) args
-> JumpTarget blocks ctx
C.JumpTarget BlockID blocks types
next_id CtxRepr types
types Assignment (Reg ctx) types
args

-- | Resolve a lambda label into a typed jump target.
resolveLambdaAsJump :: BlockInfo ext s ret blocks
                    -> TypedRegMap s ctx
                    -> LambdaLabel s tp
                    -> C.Reg ctx tp
                    -> C.JumpTarget blocks ctx
resolveLambdaAsJump :: forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx
-> LambdaLabel s tp
-> Reg ctx tp
-> JumpTarget blocks ctx
resolveLambdaAsJump BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map LambdaLabel s tp
next_lbl Reg ctx tp
output =
  case LambdaLabel s tp
-> SwitchInfoMap s blocks -> Maybe (SwitchInfo s blocks tp)
forall s (tp :: CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
LambdaLabel s tp
-> SwitchInfoMap s blocks -> Maybe (SwitchInfo s blocks tp)
lookupSwitchInfo LambdaLabel s tp
next_lbl (BlockInfo ext s ret blocks -> SwitchInfoMap s blocks
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks -> SwitchInfoMap s blocks
biSwitchInfo BlockInfo ext s ret blocks
bi) of
    Maybe (SwitchInfo s blocks tp)
Nothing -> String -> JumpTarget blocks ctx
forall a. (?callStack::CallStack) => String -> a
error String
"Could not find label in resolveLambdaAsJump"
    Just (SwitchInfo BlockID blocks (args ::> tp)
block_id CtxRepr args
types Assignment (Value s) args
inputs) -> do
      let types' :: Assignment TypeRepr (args ::> tp)
types' = CtxRepr args
types CtxRepr args -> TypeRepr tp -> Assignment TypeRepr (args ::> tp)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom (LambdaLabel s tp -> Atom s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Atom s tp
lambdaAtom LambdaLabel s tp
next_lbl)
      let args :: Assignment (Reg ctx) args
args = (forall (x :: CrucibleType). Value s x -> Reg ctx x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Value s) x -> Assignment (Reg ctx) 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 (TypedRegMap s ctx -> Value s x -> Reg ctx x
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Value s tp -> Reg ctx tp
resolveReg TypedRegMap s ctx
reg_map) Assignment (Value s) args
inputs
      let args' :: Assignment (Reg ctx) (args ::> tp)
args' = Assignment (Reg ctx) args
args Assignment (Reg ctx) args
-> Reg ctx tp -> Assignment (Reg ctx) (args ::> tp)
forall {k} (f :: k -> Type) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
`extend` Reg ctx tp
output
      BlockID blocks (args ::> tp)
-> Assignment TypeRepr (args ::> tp)
-> Assignment (Reg ctx) (args ::> tp)
-> JumpTarget blocks ctx
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) (ctx :: Ctx CrucibleType).
BlockID blocks args
-> CtxRepr args
-> Assignment (Reg ctx) args
-> JumpTarget blocks ctx
C.JumpTarget BlockID blocks (args ::> tp)
block_id Assignment TypeRepr (args ::> tp)
types' Assignment (Reg ctx) (args ::> tp)
args'

-- | Resolve a lambda label into a typed switch target.
resolveLambdaAsSwitch :: BlockInfo ext s ret blocks
                      -> TypedRegMap s ctx
                      -> LambdaLabel s tp
                      -> C.SwitchTarget blocks ctx tp
resolveLambdaAsSwitch :: forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx
-> LambdaLabel s tp
-> SwitchTarget blocks ctx tp
resolveLambdaAsSwitch BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map LambdaLabel s tp
next_lbl =
  case LambdaLabel s tp
-> SwitchInfoMap s blocks -> Maybe (SwitchInfo s blocks tp)
forall s (tp :: CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
LambdaLabel s tp
-> SwitchInfoMap s blocks -> Maybe (SwitchInfo s blocks tp)
lookupSwitchInfo LambdaLabel s tp
next_lbl (BlockInfo ext s ret blocks -> SwitchInfoMap s blocks
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks -> SwitchInfoMap s blocks
biSwitchInfo BlockInfo ext s ret blocks
bi) of
    Maybe (SwitchInfo s blocks tp)
Nothing -> String -> SwitchTarget blocks ctx tp
forall a. (?callStack::CallStack) => String -> a
error String
"Could not find label in resolveLambdaAsSwitch"
    Just (SwitchInfo BlockID blocks (args ::> tp)
block_id CtxRepr args
types Assignment (Value s) args
inputs) -> do
      let args :: Assignment (Reg ctx) args
args = (forall (x :: CrucibleType). Value s x -> Reg ctx x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Value s) x -> Assignment (Reg ctx) 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 (TypedRegMap s ctx -> Value s x -> Reg ctx x
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Value s tp -> Reg ctx tp
resolveReg TypedRegMap s ctx
reg_map) Assignment (Value s) args
inputs
      BlockID blocks (args ::> tp)
-> CtxRepr args
-> Assignment (Reg ctx) args
-> SwitchTarget blocks ctx tp
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) (tp :: CrucibleType)
       (ctx :: Ctx CrucibleType).
BlockID blocks (args ::> tp)
-> CtxRepr args
-> Assignment (Reg ctx) args
-> SwitchTarget blocks ctx tp
C.SwitchTarget BlockID blocks (args ::> tp)
block_id CtxRepr args
types Assignment (Reg ctx) args
args

-- | Resolve an untyped terminal statement to a typed one.
resolveTermStmt :: BlockInfo ext s ret blocks
                -> TypedRegMap s ctx
                -> RegExprs ext ctx
                   -- ^ Maps registers to associated expressions.
                -> ExtendedTermStmt s blocks ret
                -> C.TermStmt blocks ret ctx
resolveTermStmt :: forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> ExtendedTermStmt s blocks ret
-> TermStmt blocks ret ctx
resolveTermStmt BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map RegExprs ext ctx
bindings (BaseTermStmt TermStmt s ret
t0) =
  case TermStmt s ret
t0 of
    Jump Label s
l -> JumpTarget blocks ctx -> TermStmt blocks ret ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (ret :: CrucibleType).
JumpTarget blocks ctx -> TermStmt blocks ret ctx
C.Jump (BlockInfo ext s ret blocks
-> TypedRegMap s ctx -> Label s -> JumpTarget blocks ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx -> Label s -> JumpTarget blocks ctx
resolveJumpTarget BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map Label s
l)

    Br Atom s BoolType
c Label s
x Label s
y -> do
      let c_r :: Reg ctx BoolType
c_r = TypedRegMap s ctx -> Atom s BoolType -> Reg ctx BoolType
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s BoolType
c
      case RegExprs ext ctx
bindings RegExprs ext ctx
-> Index ctx BoolType -> MaybeF (Expr ext ctx) BoolType
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Reg ctx BoolType -> Index ctx BoolType
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Index ctx tp
C.regIndex Reg ctx BoolType
c_r of
        JustF (C.App (C.BoolLit Bool
True))  -> JumpTarget blocks ctx -> TermStmt blocks ret ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (ret :: CrucibleType).
JumpTarget blocks ctx -> TermStmt blocks ret ctx
C.Jump (BlockInfo ext s ret blocks
-> TypedRegMap s ctx -> Label s -> JumpTarget blocks ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx -> Label s -> JumpTarget blocks ctx
resolveJumpTarget BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map Label s
x)
        JustF (C.App (C.BoolLit Bool
False)) -> JumpTarget blocks ctx -> TermStmt blocks ret ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (ret :: CrucibleType).
JumpTarget blocks ctx -> TermStmt blocks ret ctx
C.Jump (BlockInfo ext s ret blocks
-> TypedRegMap s ctx -> Label s -> JumpTarget blocks ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx -> Label s -> JumpTarget blocks ctx
resolveJumpTarget BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map Label s
y)
        MaybeF (Expr ext ctx) BoolType
_ -> Reg ctx BoolType
-> JumpTarget blocks ctx
-> JumpTarget blocks ctx
-> TermStmt blocks ret ctx
forall (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
Reg ctx BoolType
-> JumpTarget blocks ctx
-> JumpTarget blocks ctx
-> TermStmt blocks ret ctx
C.Br Reg ctx BoolType
c_r
                  (BlockInfo ext s ret blocks
-> TypedRegMap s ctx -> Label s -> JumpTarget blocks ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx -> Label s -> JumpTarget blocks ctx
resolveJumpTarget BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map Label s
x)
                  (BlockInfo ext s ret blocks
-> TypedRegMap s ctx -> Label s -> JumpTarget blocks ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx -> Label s -> JumpTarget blocks ctx
resolveJumpTarget BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map Label s
y)
    MaybeBranch TypeRepr tp
tp Atom s (MaybeType tp)
e LambdaLabel s tp
j Label s
n -> do
      let e_r :: Reg ctx (MaybeType tp)
e_r = TypedRegMap s ctx
-> Atom s (MaybeType tp) -> Reg ctx (MaybeType tp)
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s (MaybeType tp)
e
      case RegExprs ext ctx
bindings RegExprs ext ctx
-> Index ctx (MaybeType tp) -> MaybeF (Expr ext ctx) (MaybeType tp)
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Reg ctx (MaybeType tp) -> Index ctx (MaybeType tp)
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Index ctx tp
C.regIndex Reg ctx (MaybeType tp)
e_r of
        JustF (C.App (C.JustValue TypeRepr tp1
_ Reg ctx tp1
je)) -> JumpTarget blocks ctx -> TermStmt blocks ret ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (ret :: CrucibleType).
JumpTarget blocks ctx -> TermStmt blocks ret ctx
C.Jump (BlockInfo ext s ret blocks
-> TypedRegMap s ctx
-> LambdaLabel s tp
-> Reg ctx tp
-> JumpTarget blocks ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx
-> LambdaLabel s tp
-> Reg ctx tp
-> JumpTarget blocks ctx
resolveLambdaAsJump BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map LambdaLabel s tp
j Reg ctx tp
Reg ctx tp1
je)
        JustF (C.App (C.NothingValue TypeRepr tp1
_)) -> JumpTarget blocks ctx -> TermStmt blocks ret ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (ret :: CrucibleType).
JumpTarget blocks ctx -> TermStmt blocks ret ctx
C.Jump (BlockInfo ext s ret blocks
-> TypedRegMap s ctx -> Label s -> JumpTarget blocks ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx -> Label s -> JumpTarget blocks ctx
resolveJumpTarget BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map Label s
n)
        MaybeF (Expr ext ctx) (MaybeType tp)
_ -> TypeRepr tp
-> Reg ctx (MaybeType tp)
-> SwitchTarget blocks ctx tp
-> JumpTarget blocks ctx
-> TermStmt blocks ret ctx
forall (tp :: CrucibleType) (ctx :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
TypeRepr tp
-> Reg ctx (MaybeType tp)
-> SwitchTarget blocks ctx tp
-> JumpTarget blocks ctx
-> TermStmt blocks ret ctx
C.MaybeBranch TypeRepr tp
tp
                           Reg ctx (MaybeType tp)
e_r
                           (BlockInfo ext s ret blocks
-> TypedRegMap s ctx
-> LambdaLabel s tp
-> SwitchTarget blocks ctx tp
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx
-> LambdaLabel s tp
-> SwitchTarget blocks ctx tp
resolveLambdaAsSwitch BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map LambdaLabel s tp
j)
                           (BlockInfo ext s ret blocks
-> TypedRegMap s ctx -> Label s -> JumpTarget blocks ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx -> Label s -> JumpTarget blocks ctx
resolveJumpTarget BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map Label s
n)

    VariantElim CtxRepr varctx
ctx Atom s (VariantType varctx)
e Assignment (LambdaLabel s) varctx
s -> do
      let e_r :: Reg ctx (VariantType varctx)
e_r = TypedRegMap s ctx
-> Atom s (VariantType varctx) -> Reg ctx (VariantType varctx)
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s (VariantType varctx)
e
      case RegExprs ext ctx
bindings RegExprs ext ctx
-> Index ctx (VariantType varctx)
-> MaybeF (Expr ext ctx) (VariantType varctx)
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Reg ctx (VariantType varctx) -> Index ctx (VariantType varctx)
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Index ctx tp
C.regIndex Reg ctx (VariantType varctx)
e_r of
        JustF (C.App (C.InjectVariant CtxRepr ctx
_ Index ctx tp1
idx Reg ctx tp1
x)) ->
          JumpTarget blocks ctx -> TermStmt blocks ret ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (ret :: CrucibleType).
JumpTarget blocks ctx -> TermStmt blocks ret ctx
C.Jump (BlockInfo ext s ret blocks
-> TypedRegMap s ctx
-> LambdaLabel s tp1
-> Reg ctx tp1
-> JumpTarget blocks ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx
-> LambdaLabel s tp
-> Reg ctx tp
-> JumpTarget blocks ctx
resolveLambdaAsJump BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map (Assignment (LambdaLabel s) varctx
s Assignment (LambdaLabel s) varctx
-> Index varctx tp1 -> LambdaLabel s tp1
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index varctx tp1
Index ctx tp1
idx) Reg ctx tp1
x)
        MaybeF (Expr ext ctx) (VariantType varctx)
_ -> CtxRepr varctx
-> Reg ctx (VariantType varctx)
-> Assignment (SwitchTarget blocks ctx) varctx
-> TermStmt blocks ret ctx
forall (varctx :: Ctx CrucibleType) (ctx :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
CtxRepr varctx
-> Reg ctx (VariantType varctx)
-> Assignment (SwitchTarget blocks ctx) varctx
-> TermStmt blocks ret ctx
C.VariantElim CtxRepr varctx
ctx Reg ctx (VariantType varctx)
e_r ((forall (x :: CrucibleType).
 LambdaLabel s x -> SwitchTarget blocks ctx x)
-> forall (x :: Ctx CrucibleType).
   Assignment (LambdaLabel s) x
   -> Assignment (SwitchTarget blocks ctx) 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 (BlockInfo ext s ret blocks
-> TypedRegMap s ctx
-> LambdaLabel s x
-> SwitchTarget blocks ctx x
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx
-> LambdaLabel s tp
-> SwitchTarget blocks ctx tp
resolveLambdaAsSwitch BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map) Assignment (LambdaLabel s) varctx
s)

    Return Atom s ret
e -> Reg ctx ret -> TermStmt blocks ret ctx
forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
Reg ctx ret -> TermStmt blocks ret ctx
C.Return (TypedRegMap s ctx -> Atom s ret -> Reg ctx ret
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s ret
e)
    TailCall Atom s (FunctionHandleType args ret)
f CtxRepr args
ctx Assignment (Atom s) args
args -> do
      Reg ctx (FunctionHandleType args ret)
-> CtxRepr args
-> Assignment (Reg ctx) args
-> TermStmt blocks ret ctx
forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType)
       (ret :: CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
Reg ctx (FunctionHandleType args ret)
-> CtxRepr args
-> Assignment (Reg ctx) args
-> TermStmt blocks ret ctx
C.TailCall (TypedRegMap s ctx
-> Atom s (FunctionHandleType args ret)
-> Reg ctx (FunctionHandleType args ret)
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s (FunctionHandleType args ret)
f) CtxRepr args
ctx ((forall (x :: CrucibleType). Atom s x -> Reg ctx x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Atom s) x -> Assignment (Reg ctx) 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 (TypedRegMap s ctx -> Atom s x -> Reg ctx x
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map) Assignment (Atom s) args
args)
    ErrorStmt Atom s (StringType Unicode)
e -> Reg ctx (StringType Unicode) -> TermStmt blocks ret ctx
forall (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
Reg ctx (StringType Unicode) -> TermStmt blocks ret ctx
C.ErrorStmt (TypedRegMap s ctx
-> Atom s (StringType Unicode) -> Reg ctx (StringType Unicode)
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s (StringType Unicode)
e)

    Output LambdaLabel s tp
l Atom s tp
e -> JumpTarget blocks ctx -> TermStmt blocks ret ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (ret :: CrucibleType).
JumpTarget blocks ctx -> TermStmt blocks ret ctx
C.Jump (BlockInfo ext s ret blocks
-> TypedRegMap s ctx
-> LambdaLabel s tp
-> Reg ctx tp
-> JumpTarget blocks ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx
-> LambdaLabel s tp
-> Reg ctx tp
-> JumpTarget blocks ctx
resolveLambdaAsJump BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map LambdaLabel s tp
l (TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s tp
e))
resolveTermStmt BlockInfo ext s ret blocks
_ TypedRegMap s ctx
reg_map RegExprs ext ctx
_ (BreakStmt (JumpInfo BlockID blocks types
next_id CtxRepr types
types Assignment (Value s) types
inputs)) = do
  let args :: Assignment (Reg ctx) types
args = (forall (x :: CrucibleType). Value s x -> Reg ctx x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Value s) x -> Assignment (Reg ctx) 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 (TypedRegMap s ctx -> Value s x -> Reg ctx x
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Value s tp -> Reg ctx tp
resolveReg TypedRegMap s ctx
reg_map) Assignment (Value s) types
inputs
  JumpTarget blocks ctx -> TermStmt blocks ret ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (ret :: CrucibleType).
JumpTarget blocks ctx -> TermStmt blocks ret ctx
C.Jump (JumpTarget blocks ctx -> TermStmt blocks ret ctx)
-> JumpTarget blocks ctx -> TermStmt blocks ret ctx
forall a b. (a -> b) -> a -> b
$ BlockID blocks types
-> CtxRepr types
-> Assignment (Reg ctx) types
-> JumpTarget blocks ctx
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) (ctx :: Ctx CrucibleType).
BlockID blocks args
-> CtxRepr args
-> Assignment (Reg ctx) args
-> JumpTarget blocks ctx
C.JumpTarget BlockID blocks types
next_id CtxRepr types
types Assignment (Reg ctx) types
args

#ifdef UNSAFE_OPS
type AppRegMap ext ctx = MapF (C.App ext (C.Reg ctx)) (C.Reg ctx)

appRegMap_extend :: AppRegMap ext ctx -> AppRegMap ext (ctx ::> tp)
appRegMap_extend :: forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
AppRegMap ext ctx -> AppRegMap ext (ctx ::> tp)
appRegMap_extend = AppRegMap ext ctx -> AppRegMap ext (ctx ::> tp)
forall a b. a -> b
unsafeCoerce

appRegMap_insert :: ( TraversableFC (C.ExprExtension ext)
                    , OrdFC (C.ExprExtension ext)
                    )
                 => C.App ext (C.Reg ctx) tp
                 -> C.Reg (ctx ::> tp) tp
                 -> AppRegMap ext ctx
                 -> AppRegMap ext (ctx ::> tp)
appRegMap_insert :: forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
(TraversableFC (ExprExtension ext), OrdFC (ExprExtension ext)) =>
App ext (Reg ctx) tp
-> Reg (ctx ::> tp) tp
-> AppRegMap ext ctx
-> AppRegMap ext (ctx ::> tp)
appRegMap_insert App ext (Reg ctx) tp
k Reg (ctx ::> tp) tp
v AppRegMap ext ctx
m = App ext (Reg (ctx ::> tp)) tp
-> Reg (ctx ::> tp) tp
-> MapF (App ext (Reg (ctx ::> tp))) (Reg (ctx ::> tp))
-> MapF (App ext (Reg (ctx ::> tp))) (Reg (ctx ::> tp))
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert ((forall (x :: CrucibleType). Reg ctx x -> Reg (ctx ::> tp) x)
-> forall (x :: CrucibleType).
   App ext (Reg ctx) x -> App ext (Reg (ctx ::> tp)) 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 :: CrucibleType). App ext f x -> App ext g x
fmapFC Reg ctx x -> Reg (ctx ::> tp) x
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType)
       (r :: CrucibleType).
Reg ctx tp -> Reg (ctx ::> r) tp
forall (x :: CrucibleType). Reg ctx x -> Reg (ctx ::> tp) x
C.extendReg App ext (Reg ctx) tp
k) Reg (ctx ::> tp) tp
v (AppRegMap ext ctx
-> MapF (App ext (Reg (ctx ::> tp))) (Reg (ctx ::> tp))
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
AppRegMap ext ctx -> AppRegMap ext (ctx ::> tp)
appRegMap_extend AppRegMap ext ctx
m)

appRegMap_lookup :: ( OrdFC (C.ExprExtension ext)
                    )
                 => C.App ext (C.Reg ctx) tp
                 -> AppRegMap ext ctx
                 -> Maybe (C.Reg ctx tp)
appRegMap_lookup :: forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
OrdFC (ExprExtension ext) =>
App ext (Reg ctx) tp -> AppRegMap ext ctx -> Maybe (Reg ctx tp)
appRegMap_lookup = App ext (Reg ctx) tp
-> MapF (App ext (Reg ctx)) (Reg ctx) -> Maybe (Reg ctx tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup

appRegMap_empty :: AppRegMap ext ctx
appRegMap_empty :: forall ext (ctx :: Ctx CrucibleType). AppRegMap ext ctx
appRegMap_empty = MapF (App ext (Reg ctx)) (Reg ctx)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
#else
type AppRegMap ext ctx = Map (Some (C.App ext (C.Reg ctx))) (SomeReg ctx)

appRegMap_extend :: AppRegMap ext ctx -> AppRegMap ext (ctx ::> tp)
appRegMap_extend = Map.fromList . fmap f . Map.toList
 where f (Some app, SomeReg tp reg) = (Some (C.mapApp C.extendReg app), SomeReg tp (C.extendReg reg))

appRegMap_insert :: OrdFC (C.ExprExtension ext)
                 => C.App ext (C.Reg ctx) tp
                 -> C.Reg (ctx::>tp) tp
                 -> AppRegMap ext ctx
                 -> AppRegMap ext (ctx ::> tp)
appRegMap_insert k v m =
  Map.insert (Some (C.mapApp C.extendReg k)) (SomeReg (C.appType k) v) (appRegMap_extend m)

appRegMap_lookup :: C.App ext (C.Reg ctx) tp
                 -> AppRegMap ext ctx
                 -> Maybe (C.Reg ctx tp)
appRegMap_lookup app m =
  case Map.lookup (Some app) m of
     Nothing -> Nothing
     Just (SomeReg tp r)
        | Just Refl <- testEquality tp (C.appType app) -> Just r
     _ -> error "appRegMap_lookup: impossible!"


appRegMap_empty :: AppRegMap ext ctx
appRegMap_empty = Map.empty

#endif

-- | Resolve a list of statements to a typed list.
resolveStmts :: C.IsSyntaxExtension ext
             => FunctionName
             -> BlockInfo ext s ret blocks
             -> Size ctx
             -> TypedRegMap s ctx
             -> RegExprs ext ctx
                -- ^ Maps registers back to the expression that generated them (if any)
             -> AppRegMap ext ctx
                -- ^ Maps applications to register that stores their value.
                -- Used to eliminate redundant operations.
             -> [Posd (Stmt ext s)]
             -> Posd (ExtendedTermStmt s blocks ret)
             -> C.StmtSeq ext blocks ret ctx
resolveStmts :: forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size ctx
_ TypedRegMap s ctx
reg_map RegExprs ext ctx
bindings AppRegMap ext ctx
_ [] (Posd Position
p ExtendedTermStmt s blocks ret
t) = do
  ProgramLoc -> TermStmt blocks ret ctx -> StmtSeq ext blocks ret ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType) ext.
ProgramLoc -> TermStmt blocks ret ctx -> StmtSeq ext blocks ret ctx
C.TermStmt (FunctionName -> Position -> ProgramLoc
mkProgramLoc FunctionName
nm Position
p)
             (BlockInfo ext s ret blocks
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> ExtendedTermStmt s blocks ret
-> TermStmt blocks ret ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
BlockInfo ext s ret blocks
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> ExtendedTermStmt s blocks ret
-> TermStmt blocks ret ctx
resolveTermStmt BlockInfo ext s ret blocks
bi TypedRegMap s ctx
reg_map RegExprs ext ctx
bindings ExtendedTermStmt s blocks ret
t)
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size ctx
sz TypedRegMap s ctx
reg_map RegExprs ext ctx
bindings AppRegMap ext ctx
appMap (Posd Position
p Stmt ext s
s0:[Posd (Stmt ext s)]
rest) Posd (ExtendedTermStmt s blocks ret)
t = do
  let pl :: ProgramLoc
pl = FunctionName -> Position -> ProgramLoc
mkProgramLoc FunctionName
nm Position
p
  case Stmt ext s
s0 of
    SetReg Reg s tp
r Atom s tp
a -> do
      let reg_map' :: TypedRegMap s ctx
reg_map' = TypedRegMap s ctx
reg_map TypedRegMap s ctx
-> (TypedRegMap s ctx -> TypedRegMap s ctx) -> TypedRegMap s ctx
forall a b. a -> (a -> b) -> b
& Value s tp -> Value s tp -> TypedRegMap s ctx -> TypedRegMap s ctx
forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp -> Value s tp -> TypedRegMap s ctx -> TypedRegMap s ctx
copyValue (Reg s tp -> Value s tp
forall s (tp :: CrucibleType). Reg s tp -> Value s tp
RegValue Reg s tp
r) (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a)
      FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size ctx
sz TypedRegMap s ctx
reg_map' RegExprs ext ctx
bindings AppRegMap ext ctx
appMap [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t
    WriteGlobal GlobalVar tp
v Atom s tp
a -> do
      ProgramLoc
-> Stmt ext ctx ctx
-> StmtSeq ext blocks ret ctx
-> StmtSeq ext blocks ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
C.ConsStmt ProgramLoc
pl
                 (GlobalVar tp -> Reg ctx tp -> Stmt ext ctx ctx
forall (tp :: CrucibleType) (ctx :: Ctx CrucibleType) ext.
GlobalVar tp -> Reg ctx tp -> Stmt ext ctx ctx
C.WriteGlobal GlobalVar tp
v (TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s tp
a))
                 (FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size ctx
sz TypedRegMap s ctx
reg_map RegExprs ext ctx
bindings AppRegMap ext ctx
appMap [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t)
    WriteRef Atom s (ReferenceType tp)
r Atom s tp
a -> do
      ProgramLoc
-> Stmt ext ctx ctx
-> StmtSeq ext blocks ret ctx
-> StmtSeq ext blocks ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
C.ConsStmt ProgramLoc
pl
                 (Reg ctx (ReferenceType tp) -> Reg ctx tp -> Stmt ext ctx ctx
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType) ext.
Reg ctx (ReferenceType tp) -> Reg ctx tp -> Stmt ext ctx ctx
C.WriteRefCell (TypedRegMap s ctx
-> Atom s (ReferenceType tp) -> Reg ctx (ReferenceType tp)
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s (ReferenceType tp)
r) (TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s tp
a))
                 (FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size ctx
sz TypedRegMap s ctx
reg_map RegExprs ext ctx
bindings AppRegMap ext ctx
appMap [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t)
    DropRef Atom s (ReferenceType tp)
r -> do
      ProgramLoc
-> Stmt ext ctx ctx
-> StmtSeq ext blocks ret ctx
-> StmtSeq ext blocks ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
C.ConsStmt ProgramLoc
pl
                 (Reg ctx (ReferenceType tp) -> Stmt ext ctx ctx
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType) ext.
Reg ctx (ReferenceType tp) -> Stmt ext ctx ctx
C.DropRefCell (TypedRegMap s ctx
-> Atom s (ReferenceType tp) -> Reg ctx (ReferenceType tp)
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s (ReferenceType tp)
r))
                 (FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size ctx
sz TypedRegMap s ctx
reg_map RegExprs ext ctx
bindings AppRegMap ext ctx
appMap [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t)
    DefineAtom Atom s tp
a AtomValue ext s tp
av -> do
      case AtomValue ext s tp
av of
        ReadReg Reg s tp
r -> do
          let reg_map' :: TypedRegMap s ctx
reg_map' = TypedRegMap s ctx
reg_map TypedRegMap s ctx
-> (TypedRegMap s ctx -> TypedRegMap s ctx) -> TypedRegMap s ctx
forall a b. a -> (a -> b) -> b
& Value s tp -> Value s tp -> TypedRegMap s ctx -> TypedRegMap s ctx
forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp -> Value s tp -> TypedRegMap s ctx -> TypedRegMap s ctx
copyValue (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) (Reg s tp -> Value s tp
forall s (tp :: CrucibleType). Reg s tp -> Value s tp
RegValue Reg s tp
r)
          FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size ctx
sz TypedRegMap s ctx
reg_map' RegExprs ext ctx
bindings AppRegMap ext ctx
appMap [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t
        EvalExt StmtExtension ext (Atom s) tp
estmt -> do
          let estmt' :: StmtExtension ext (Reg ctx) tp
estmt' = (forall (x :: CrucibleType). Atom s x -> Reg ctx x)
-> forall (x :: CrucibleType).
   StmtExtension ext (Atom s) x -> StmtExtension ext (Reg ctx) 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 :: CrucibleType).
   StmtExtension ext f x -> StmtExtension ext g x
fmapFC (TypedRegMap s ctx -> Atom s x -> Reg ctx x
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map) StmtExtension ext (Atom s) tp
estmt
          let sz' :: Size (ctx '::> tp)
sz' = Size ctx -> Size (ctx '::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
sz
          let reg_map' :: TypedRegMap s (ctx '::> tp)
reg_map'  = TypedRegMap s ctx
reg_map TypedRegMap s ctx
-> (TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp))
-> TypedRegMap s (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp)
forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx ::> tp)
assignRegister (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) Size ctx
sz
          -- No expression to associate with this value.
          let bindings' :: RegExprs ext (ctx '::> tp)
bindings' = RegExprs ext ctx
bindings RegExprs ext ctx
-> (RegExprs ext ctx -> RegExprs ext (ctx '::> tp))
-> RegExprs ext (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& MaybeF (Expr ext ctx) tp
-> RegExprs ext ctx -> RegExprs ext (ctx '::> tp)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
MaybeF (Expr ext ctx) tp
-> RegExprs ext ctx -> RegExprs ext (ctx ::> tp)
extendRegExprs MaybeF (Expr ext ctx) tp
forall {k} (f :: k -> Type) (tp :: k). MaybeF f tp
NothingF
          -- No App to memoize in this case.
          let appMap' :: AppRegMap ext (ctx '::> tp)
appMap'   = AppRegMap ext ctx
appMap   AppRegMap ext ctx
-> (AppRegMap ext ctx -> AppRegMap ext (ctx '::> tp))
-> AppRegMap ext (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& AppRegMap ext ctx -> AppRegMap ext (ctx '::> tp)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
AppRegMap ext ctx -> AppRegMap ext (ctx ::> tp)
appRegMap_extend
          ProgramLoc
-> Stmt ext ctx (ctx '::> tp)
-> StmtSeq ext blocks ret (ctx '::> tp)
-> StmtSeq ext blocks ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
C.ConsStmt ProgramLoc
pl
                     (StmtExtension ext (Reg ctx) tp -> Stmt ext ctx (ctx '::> tp)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
StmtExtension ext (Reg ctx) tp -> Stmt ext ctx (ctx '::> tp)
C.ExtendAssign StmtExtension ext (Reg ctx) tp
estmt')
                     (FunctionName
-> BlockInfo ext s ret blocks
-> Size (ctx '::> tp)
-> TypedRegMap s (ctx '::> tp)
-> RegExprs ext (ctx '::> tp)
-> AppRegMap ext (ctx '::> tp)
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret (ctx '::> tp)
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size (ctx '::> tp)
sz' TypedRegMap s (ctx '::> tp)
reg_map' RegExprs ext (ctx '::> tp)
bindings' AppRegMap ext (ctx '::> tp)
appMap' [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t)
        ReadGlobal GlobalVar tp
v -> do
          let sz' :: Size (ctx '::> tp)
sz' = Size ctx -> Size (ctx '::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
sz
          let reg_map' :: TypedRegMap s (ctx '::> tp)
reg_map'  = TypedRegMap s ctx
reg_map  TypedRegMap s ctx
-> (TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp))
-> TypedRegMap s (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp)
forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx ::> tp)
assignRegister (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) Size ctx
sz
          -- No expression to associate with this value.
          let bindings' :: RegExprs ext (ctx '::> tp)
bindings' = RegExprs ext ctx
bindings RegExprs ext ctx
-> (RegExprs ext ctx -> RegExprs ext (ctx '::> tp))
-> RegExprs ext (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& MaybeF (Expr ext ctx) tp
-> RegExprs ext ctx -> RegExprs ext (ctx '::> tp)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
MaybeF (Expr ext ctx) tp
-> RegExprs ext ctx -> RegExprs ext (ctx ::> tp)
extendRegExprs MaybeF (Expr ext ctx) tp
forall {k} (f :: k -> Type) (tp :: k). MaybeF f tp
NothingF
          -- No App to memoize in this case.
          let appMap' :: AppRegMap ext (ctx '::> tp)
appMap'   = AppRegMap ext ctx
appMap   AppRegMap ext ctx
-> (AppRegMap ext ctx -> AppRegMap ext (ctx '::> tp))
-> AppRegMap ext (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& AppRegMap ext ctx -> AppRegMap ext (ctx '::> tp)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
AppRegMap ext ctx -> AppRegMap ext (ctx ::> tp)
appRegMap_extend
          ProgramLoc
-> Stmt ext ctx (ctx '::> tp)
-> StmtSeq ext blocks ret (ctx '::> tp)
-> StmtSeq ext blocks ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
C.ConsStmt ProgramLoc
pl
                     (GlobalVar tp -> Stmt ext ctx (ctx '::> tp)
forall (tp :: CrucibleType) ext (ctx :: Ctx CrucibleType).
GlobalVar tp -> Stmt ext ctx (ctx '::> tp)
C.ReadGlobal GlobalVar tp
v)
                     (FunctionName
-> BlockInfo ext s ret blocks
-> Size (ctx '::> tp)
-> TypedRegMap s (ctx '::> tp)
-> RegExprs ext (ctx '::> tp)
-> AppRegMap ext (ctx '::> tp)
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret (ctx '::> tp)
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size (ctx '::> tp)
sz' TypedRegMap s (ctx '::> tp)
reg_map' RegExprs ext (ctx '::> tp)
bindings' AppRegMap ext (ctx '::> tp)
appMap' [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t)
        NewRef Atom s tp1
v -> do
          let sz' :: Size (ctx '::> 'ReferenceType tp1)
sz' = Size ctx -> Size (ctx '::> 'ReferenceType tp1)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
sz
          let reg_map' :: TypedRegMap s (ctx '::> tp)
reg_map'  = TypedRegMap s ctx
reg_map  TypedRegMap s ctx
-> (TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp))
-> TypedRegMap s (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp)
forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx ::> tp)
assignRegister (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) Size ctx
sz
          -- No expression to associate with this value.
          let bindings' :: RegExprs ext (ctx '::> 'ReferenceType tp1)
bindings' = RegExprs ext ctx
bindings RegExprs ext ctx
-> (RegExprs ext ctx -> RegExprs ext (ctx '::> 'ReferenceType tp1))
-> RegExprs ext (ctx '::> 'ReferenceType tp1)
forall a b. a -> (a -> b) -> b
& MaybeF (Expr ext ctx) ('ReferenceType tp1)
-> RegExprs ext ctx -> RegExprs ext (ctx '::> 'ReferenceType tp1)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
MaybeF (Expr ext ctx) tp
-> RegExprs ext ctx -> RegExprs ext (ctx ::> tp)
extendRegExprs MaybeF (Expr ext ctx) ('ReferenceType tp1)
forall {k} (f :: k -> Type) (tp :: k). MaybeF f tp
NothingF
          -- No App to memoize in this case.
          let appMap' :: AppRegMap ext (ctx '::> 'ReferenceType tp1)
appMap'   = AppRegMap ext ctx
appMap   AppRegMap ext ctx
-> (AppRegMap ext ctx
    -> AppRegMap ext (ctx '::> 'ReferenceType tp1))
-> AppRegMap ext (ctx '::> 'ReferenceType tp1)
forall a b. a -> (a -> b) -> b
& AppRegMap ext ctx -> AppRegMap ext (ctx '::> 'ReferenceType tp1)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
AppRegMap ext ctx -> AppRegMap ext (ctx ::> tp)
appRegMap_extend
          -- Resolve the atom
          let v' :: Reg ctx tp1
v' = TypedRegMap s ctx -> Atom s tp1 -> Reg ctx tp1
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s tp1
v
          ProgramLoc
-> Stmt ext ctx (ctx '::> 'ReferenceType tp1)
-> StmtSeq ext blocks ret (ctx '::> 'ReferenceType tp1)
-> StmtSeq ext blocks ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
C.ConsStmt ProgramLoc
pl
                     (TypeRepr tp1
-> Reg ctx tp1 -> Stmt ext ctx (ctx '::> 'ReferenceType tp1)
forall (tp :: CrucibleType) (ctx :: Ctx CrucibleType) ext.
TypeRepr tp
-> Reg ctx tp -> Stmt ext ctx (ctx '::> ReferenceType tp)
C.NewRefCell (Atom s tp1 -> TypeRepr tp1
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp1
v) Reg ctx tp1
v')
                     (FunctionName
-> BlockInfo ext s ret blocks
-> Size (ctx '::> 'ReferenceType tp1)
-> TypedRegMap s (ctx '::> 'ReferenceType tp1)
-> RegExprs ext (ctx '::> 'ReferenceType tp1)
-> AppRegMap ext (ctx '::> 'ReferenceType tp1)
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret (ctx '::> 'ReferenceType tp1)
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size (ctx '::> 'ReferenceType tp1)
sz' TypedRegMap s (ctx '::> tp)
TypedRegMap s (ctx '::> 'ReferenceType tp1)
reg_map' RegExprs ext (ctx '::> 'ReferenceType tp1)
bindings' AppRegMap ext (ctx '::> 'ReferenceType tp1)
appMap' [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t)
        NewEmptyRef TypeRepr tp1
tp -> do
          let sz' :: Size (ctx '::> 'ReferenceType tp1)
sz' = Size ctx -> Size (ctx '::> 'ReferenceType tp1)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
sz
          let reg_map' :: TypedRegMap s (ctx '::> tp)
reg_map'  = TypedRegMap s ctx
reg_map  TypedRegMap s ctx
-> (TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp))
-> TypedRegMap s (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp)
forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx ::> tp)
assignRegister (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) Size ctx
sz
          -- No expression to associate with this value.
          let bindings' :: RegExprs ext (ctx '::> 'ReferenceType tp1)
bindings' = RegExprs ext ctx
bindings RegExprs ext ctx
-> (RegExprs ext ctx -> RegExprs ext (ctx '::> 'ReferenceType tp1))
-> RegExprs ext (ctx '::> 'ReferenceType tp1)
forall a b. a -> (a -> b) -> b
& MaybeF (Expr ext ctx) ('ReferenceType tp1)
-> RegExprs ext ctx -> RegExprs ext (ctx '::> 'ReferenceType tp1)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
MaybeF (Expr ext ctx) tp
-> RegExprs ext ctx -> RegExprs ext (ctx ::> tp)
extendRegExprs MaybeF (Expr ext ctx) ('ReferenceType tp1)
forall {k} (f :: k -> Type) (tp :: k). MaybeF f tp
NothingF
          -- No App to memoize in this case.
          let appMap' :: AppRegMap ext (ctx '::> 'ReferenceType tp1)
appMap'   = AppRegMap ext ctx
appMap   AppRegMap ext ctx
-> (AppRegMap ext ctx
    -> AppRegMap ext (ctx '::> 'ReferenceType tp1))
-> AppRegMap ext (ctx '::> 'ReferenceType tp1)
forall a b. a -> (a -> b) -> b
& AppRegMap ext ctx -> AppRegMap ext (ctx '::> 'ReferenceType tp1)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
AppRegMap ext ctx -> AppRegMap ext (ctx ::> tp)
appRegMap_extend
          -- Resolve the atom
          ProgramLoc
-> Stmt ext ctx (ctx '::> 'ReferenceType tp1)
-> StmtSeq ext blocks ret (ctx '::> 'ReferenceType tp1)
-> StmtSeq ext blocks ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
C.ConsStmt ProgramLoc
pl
                     (TypeRepr tp1 -> Stmt ext ctx (ctx '::> 'ReferenceType tp1)
forall (tp :: CrucibleType) ext (ctx :: Ctx CrucibleType).
TypeRepr tp -> Stmt ext ctx (ctx '::> ReferenceType tp)
C.NewEmptyRefCell TypeRepr tp1
tp)
                     (FunctionName
-> BlockInfo ext s ret blocks
-> Size (ctx '::> 'ReferenceType tp1)
-> TypedRegMap s (ctx '::> 'ReferenceType tp1)
-> RegExprs ext (ctx '::> 'ReferenceType tp1)
-> AppRegMap ext (ctx '::> 'ReferenceType tp1)
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret (ctx '::> 'ReferenceType tp1)
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size (ctx '::> 'ReferenceType tp1)
sz' TypedRegMap s (ctx '::> tp)
TypedRegMap s (ctx '::> 'ReferenceType tp1)
reg_map' RegExprs ext (ctx '::> 'ReferenceType tp1)
bindings' AppRegMap ext (ctx '::> 'ReferenceType tp1)
appMap' [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t)
        ReadRef Atom s (ReferenceType tp)
r -> do
          let sz' :: Size (ctx '::> tp)
sz' = Size ctx -> Size (ctx '::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
sz
          let reg_map' :: TypedRegMap s (ctx '::> tp)
reg_map'  = TypedRegMap s ctx
reg_map  TypedRegMap s ctx
-> (TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp))
-> TypedRegMap s (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp)
forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx ::> tp)
assignRegister (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) Size ctx
sz
          -- No expression to associate with this value.
          let bindings' :: RegExprs ext (ctx '::> tp)
bindings' = RegExprs ext ctx
bindings RegExprs ext ctx
-> (RegExprs ext ctx -> RegExprs ext (ctx '::> tp))
-> RegExprs ext (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& MaybeF (Expr ext ctx) tp
-> RegExprs ext ctx -> RegExprs ext (ctx '::> tp)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
MaybeF (Expr ext ctx) tp
-> RegExprs ext ctx -> RegExprs ext (ctx ::> tp)
extendRegExprs MaybeF (Expr ext ctx) tp
forall {k} (f :: k -> Type) (tp :: k). MaybeF f tp
NothingF
          -- No App to memoize in this case.
          let appMap' :: AppRegMap ext (ctx '::> tp)
appMap'   = AppRegMap ext ctx
appMap   AppRegMap ext ctx
-> (AppRegMap ext ctx -> AppRegMap ext (ctx '::> tp))
-> AppRegMap ext (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& AppRegMap ext ctx -> AppRegMap ext (ctx '::> tp)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
AppRegMap ext ctx -> AppRegMap ext (ctx ::> tp)
appRegMap_extend
          -- Resolve the atom
          let r' :: Reg ctx (ReferenceType tp)
r' = TypedRegMap s ctx
-> Atom s (ReferenceType tp) -> Reg ctx (ReferenceType tp)
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s (ReferenceType tp)
r
          ProgramLoc
-> Stmt ext ctx (ctx '::> tp)
-> StmtSeq ext blocks ret (ctx '::> tp)
-> StmtSeq ext blocks ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
C.ConsStmt ProgramLoc
pl
                     (Reg ctx (ReferenceType tp) -> Stmt ext ctx (ctx '::> tp)
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType) ext.
Reg ctx (ReferenceType tp) -> Stmt ext ctx (ctx '::> tp)
C.ReadRefCell Reg ctx (ReferenceType tp)
r')
                     (FunctionName
-> BlockInfo ext s ret blocks
-> Size (ctx '::> tp)
-> TypedRegMap s (ctx '::> tp)
-> RegExprs ext (ctx '::> tp)
-> AppRegMap ext (ctx '::> tp)
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret (ctx '::> tp)
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size (ctx '::> tp)
sz' TypedRegMap s (ctx '::> tp)
reg_map' RegExprs ext (ctx '::> tp)
bindings' AppRegMap ext (ctx '::> tp)
appMap' [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t)
        EvalApp ((forall (x :: CrucibleType). Atom s x -> Reg ctx x)
-> forall (x :: CrucibleType).
   App ext (Atom s) x -> App ext (Reg ctx) 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 :: CrucibleType). App ext f x -> App ext g x
fmapFC (TypedRegMap s ctx -> Atom s x -> Reg ctx x
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map) -> App ext (Reg ctx) tp
e)
          | Just Reg ctx tp
cr <- App ext (Reg ctx) tp -> AppRegMap ext ctx -> Maybe (Reg ctx tp)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
OrdFC (ExprExtension ext) =>
App ext (Reg ctx) tp -> AppRegMap ext ctx -> Maybe (Reg ctx tp)
appRegMap_lookup App ext (Reg ctx) tp
e AppRegMap ext ctx
appMap -> do
            let reg_map' :: TypedRegMap s ctx
reg_map' = Value s tp -> Reg ctx tp -> TypedRegMap s ctx -> TypedRegMap s ctx
forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp -> Reg ctx tp -> TypedRegMap s ctx -> TypedRegMap s ctx
bindValueReg (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) Reg ctx tp
cr TypedRegMap s ctx
reg_map
            FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size ctx
sz TypedRegMap s ctx
reg_map' RegExprs ext ctx
bindings AppRegMap ext ctx
appMap [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t
          | Bool
otherwise -> do
            let e' :: Expr ext ctx tp
e' = App ext (Reg ctx) tp -> Expr ext ctx tp
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
App ext (Reg ctx) tp -> Expr ext ctx tp
C.App App ext (Reg ctx) tp
e
            let sz' :: Size (ctx '::> tp)
sz' = Size ctx -> Size (ctx '::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
sz
            let reg_map' :: TypedRegMap s (ctx '::> tp)
reg_map'  = TypedRegMap s ctx
reg_map  TypedRegMap s ctx
-> (TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp))
-> TypedRegMap s (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp)
forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx ::> tp)
assignRegister (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) Size ctx
sz
            let bindings' :: RegExprs ext (ctx '::> tp)
bindings' = RegExprs ext ctx
bindings RegExprs ext ctx
-> (RegExprs ext ctx -> RegExprs ext (ctx '::> tp))
-> RegExprs ext (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& MaybeF (Expr ext ctx) tp
-> RegExprs ext ctx -> RegExprs ext (ctx '::> tp)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
MaybeF (Expr ext ctx) tp
-> RegExprs ext ctx -> RegExprs ext (ctx ::> tp)
extendRegExprs (Expr ext ctx tp -> MaybeF (Expr ext ctx) tp
forall {k} (f :: k -> Type) (tp :: k). f tp -> MaybeF f tp
JustF Expr ext ctx tp
e')
            let appMap' :: AppRegMap ext (ctx '::> tp)
appMap'   = AppRegMap ext ctx
appMap   AppRegMap ext ctx
-> (AppRegMap ext ctx -> AppRegMap ext (ctx '::> tp))
-> AppRegMap ext (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& App ext (Reg ctx) tp
-> Reg (ctx '::> tp) tp
-> AppRegMap ext ctx
-> AppRegMap ext (ctx '::> tp)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
(TraversableFC (ExprExtension ext), OrdFC (ExprExtension ext)) =>
App ext (Reg ctx) tp
-> Reg (ctx ::> tp) tp
-> AppRegMap ext ctx
-> AppRegMap ext (ctx ::> tp)
appRegMap_insert App ext (Reg ctx) tp
e (Index (ctx '::> tp) tp -> Reg (ctx '::> tp) tp
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Index ctx tp -> Reg ctx tp
C.Reg (Size ctx -> Index (ctx '::> tp) tp
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size ctx
sz))
            let stmt :: Stmt ext ctx (ctx '::> tp)
stmt = TypeRepr tp -> Expr ext ctx tp -> Stmt ext ctx (ctx '::> tp)
forall (tp :: CrucibleType) ext (ctx :: Ctx CrucibleType).
TypeRepr tp -> Expr ext ctx tp -> Stmt ext ctx (ctx '::> tp)
C.SetReg (Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp
a) Expr ext ctx tp
e'
            ProgramLoc
-> Stmt ext ctx (ctx '::> tp)
-> StmtSeq ext blocks ret (ctx '::> tp)
-> StmtSeq ext blocks ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
C.ConsStmt ProgramLoc
pl Stmt ext ctx (ctx '::> tp)
stmt (FunctionName
-> BlockInfo ext s ret blocks
-> Size (ctx '::> tp)
-> TypedRegMap s (ctx '::> tp)
-> RegExprs ext (ctx '::> tp)
-> AppRegMap ext (ctx '::> tp)
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret (ctx '::> tp)
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size (ctx '::> tp)
sz' TypedRegMap s (ctx '::> tp)
reg_map' RegExprs ext (ctx '::> tp)
bindings' AppRegMap ext (ctx '::> tp)
appMap' [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t)

        FreshConstant BaseTypeRepr bt
bt Maybe SolverSymbol
cnm -> do
          let sz' :: Size (ctx '::> 'BaseToType bt)
sz' = Size ctx -> Size (ctx '::> 'BaseToType bt)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
sz
          let reg_map' :: TypedRegMap s (ctx '::> tp)
reg_map'  = TypedRegMap s ctx
reg_map  TypedRegMap s ctx
-> (TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp))
-> TypedRegMap s (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp)
forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx ::> tp)
assignRegister (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) Size ctx
sz
          let bindings' :: RegExprs ext (ctx '::> 'BaseToType bt)
bindings' = RegExprs ext ctx
bindings RegExprs ext ctx
-> (RegExprs ext ctx -> RegExprs ext (ctx '::> 'BaseToType bt))
-> RegExprs ext (ctx '::> 'BaseToType bt)
forall a b. a -> (a -> b) -> b
& MaybeF (Expr ext ctx) ('BaseToType bt)
-> RegExprs ext ctx -> RegExprs ext (ctx '::> 'BaseToType bt)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
MaybeF (Expr ext ctx) tp
-> RegExprs ext ctx -> RegExprs ext (ctx ::> tp)
extendRegExprs MaybeF (Expr ext ctx) ('BaseToType bt)
forall {k} (f :: k -> Type) (tp :: k). MaybeF f tp
NothingF
          let appMap' :: AppRegMap ext (ctx '::> 'BaseToType bt)
appMap'   = AppRegMap ext ctx
appMap   AppRegMap ext ctx
-> (AppRegMap ext ctx -> AppRegMap ext (ctx '::> 'BaseToType bt))
-> AppRegMap ext (ctx '::> 'BaseToType bt)
forall a b. a -> (a -> b) -> b
& AppRegMap ext ctx -> AppRegMap ext (ctx '::> 'BaseToType bt)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
AppRegMap ext ctx -> AppRegMap ext (ctx ::> tp)
appRegMap_extend
          let stmt :: Stmt ext ctx (ctx '::> 'BaseToType bt)
stmt = BaseTypeRepr bt
-> Maybe SolverSymbol -> Stmt ext ctx (ctx '::> 'BaseToType bt)
forall (bt :: BaseType) ext (ctx :: Ctx CrucibleType).
BaseTypeRepr bt
-> Maybe SolverSymbol -> Stmt ext ctx (ctx '::> BaseToType bt)
C.FreshConstant BaseTypeRepr bt
bt Maybe SolverSymbol
cnm
          ProgramLoc
-> Stmt ext ctx (ctx '::> 'BaseToType bt)
-> StmtSeq ext blocks ret (ctx '::> 'BaseToType bt)
-> StmtSeq ext blocks ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
C.ConsStmt ProgramLoc
pl Stmt ext ctx (ctx '::> 'BaseToType bt)
stmt (FunctionName
-> BlockInfo ext s ret blocks
-> Size (ctx '::> 'BaseToType bt)
-> TypedRegMap s (ctx '::> 'BaseToType bt)
-> RegExprs ext (ctx '::> 'BaseToType bt)
-> AppRegMap ext (ctx '::> 'BaseToType bt)
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret (ctx '::> 'BaseToType bt)
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size (ctx '::> 'BaseToType bt)
sz' TypedRegMap s (ctx '::> tp)
TypedRegMap s (ctx '::> 'BaseToType bt)
reg_map' RegExprs ext (ctx '::> 'BaseToType bt)
bindings' AppRegMap ext (ctx '::> 'BaseToType bt)
appMap' [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t)

        FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
cnm -> do
          let sz' :: Size (ctx '::> 'FloatType fi)
sz' = Size ctx -> Size (ctx '::> 'FloatType fi)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
sz
          let reg_map' :: TypedRegMap s (ctx '::> tp)
reg_map'  = TypedRegMap s ctx
reg_map  TypedRegMap s ctx
-> (TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp))
-> TypedRegMap s (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp)
forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx ::> tp)
assignRegister (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) Size ctx
sz
          let bindings' :: RegExprs ext (ctx '::> 'FloatType fi)
bindings' = RegExprs ext ctx
bindings RegExprs ext ctx
-> (RegExprs ext ctx -> RegExprs ext (ctx '::> 'FloatType fi))
-> RegExprs ext (ctx '::> 'FloatType fi)
forall a b. a -> (a -> b) -> b
& MaybeF (Expr ext ctx) ('FloatType fi)
-> RegExprs ext ctx -> RegExprs ext (ctx '::> 'FloatType fi)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
MaybeF (Expr ext ctx) tp
-> RegExprs ext ctx -> RegExprs ext (ctx ::> tp)
extendRegExprs MaybeF (Expr ext ctx) ('FloatType fi)
forall {k} (f :: k -> Type) (tp :: k). MaybeF f tp
NothingF
          let appMap' :: AppRegMap ext (ctx '::> 'FloatType fi)
appMap'   = AppRegMap ext ctx
appMap   AppRegMap ext ctx
-> (AppRegMap ext ctx -> AppRegMap ext (ctx '::> 'FloatType fi))
-> AppRegMap ext (ctx '::> 'FloatType fi)
forall a b. a -> (a -> b) -> b
& AppRegMap ext ctx -> AppRegMap ext (ctx '::> 'FloatType fi)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
AppRegMap ext ctx -> AppRegMap ext (ctx ::> tp)
appRegMap_extend
          let stmt :: Stmt ext ctx (ctx '::> 'FloatType fi)
stmt = FloatInfoRepr fi
-> Maybe SolverSymbol -> Stmt ext ctx (ctx '::> 'FloatType fi)
forall (fi :: FloatInfo) ext (ctx :: Ctx CrucibleType).
FloatInfoRepr fi
-> Maybe SolverSymbol -> Stmt ext ctx (ctx '::> FloatType fi)
C.FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
cnm
          ProgramLoc
-> Stmt ext ctx (ctx '::> 'FloatType fi)
-> StmtSeq ext blocks ret (ctx '::> 'FloatType fi)
-> StmtSeq ext blocks ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
C.ConsStmt ProgramLoc
pl Stmt ext ctx (ctx '::> 'FloatType fi)
stmt (FunctionName
-> BlockInfo ext s ret blocks
-> Size (ctx '::> 'FloatType fi)
-> TypedRegMap s (ctx '::> 'FloatType fi)
-> RegExprs ext (ctx '::> 'FloatType fi)
-> AppRegMap ext (ctx '::> 'FloatType fi)
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret (ctx '::> 'FloatType fi)
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size (ctx '::> 'FloatType fi)
sz' TypedRegMap s (ctx '::> tp)
TypedRegMap s (ctx '::> 'FloatType fi)
reg_map' RegExprs ext (ctx '::> 'FloatType fi)
bindings' AppRegMap ext (ctx '::> 'FloatType fi)
appMap' [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t)

        FreshNat Maybe SolverSymbol
cnm -> do
          let sz' :: Size (ctx '::> 'NatType)
sz' = Size ctx -> Size (ctx '::> 'NatType)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
sz
          let reg_map' :: TypedRegMap s (ctx '::> tp)
reg_map'  = TypedRegMap s ctx
reg_map  TypedRegMap s ctx
-> (TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp))
-> TypedRegMap s (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp)
forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx ::> tp)
assignRegister (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) Size ctx
sz
          let bindings' :: RegExprs ext (ctx '::> 'NatType)
bindings' = RegExprs ext ctx
bindings RegExprs ext ctx
-> (RegExprs ext ctx -> RegExprs ext (ctx '::> 'NatType))
-> RegExprs ext (ctx '::> 'NatType)
forall a b. a -> (a -> b) -> b
& MaybeF (Expr ext ctx) 'NatType
-> RegExprs ext ctx -> RegExprs ext (ctx '::> 'NatType)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
MaybeF (Expr ext ctx) tp
-> RegExprs ext ctx -> RegExprs ext (ctx ::> tp)
extendRegExprs MaybeF (Expr ext ctx) 'NatType
forall {k} (f :: k -> Type) (tp :: k). MaybeF f tp
NothingF
          let appMap' :: AppRegMap ext (ctx '::> 'NatType)
appMap'   = AppRegMap ext ctx
appMap   AppRegMap ext ctx
-> (AppRegMap ext ctx -> AppRegMap ext (ctx '::> 'NatType))
-> AppRegMap ext (ctx '::> 'NatType)
forall a b. a -> (a -> b) -> b
& AppRegMap ext ctx -> AppRegMap ext (ctx '::> 'NatType)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
AppRegMap ext ctx -> AppRegMap ext (ctx ::> tp)
appRegMap_extend
          let stmt :: Stmt ext ctx (ctx '::> 'NatType)
stmt = Maybe SolverSymbol -> Stmt ext ctx (ctx '::> 'NatType)
forall ext (ctx :: Ctx CrucibleType).
Maybe SolverSymbol -> Stmt ext ctx (ctx '::> 'NatType)
C.FreshNat Maybe SolverSymbol
cnm
          ProgramLoc
-> Stmt ext ctx (ctx '::> 'NatType)
-> StmtSeq ext blocks ret (ctx '::> 'NatType)
-> StmtSeq ext blocks ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
C.ConsStmt ProgramLoc
pl Stmt ext ctx (ctx '::> 'NatType)
stmt (FunctionName
-> BlockInfo ext s ret blocks
-> Size (ctx '::> 'NatType)
-> TypedRegMap s (ctx '::> 'NatType)
-> RegExprs ext (ctx '::> 'NatType)
-> AppRegMap ext (ctx '::> 'NatType)
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret (ctx '::> 'NatType)
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size (ctx '::> 'NatType)
sz' TypedRegMap s (ctx '::> tp)
TypedRegMap s (ctx '::> 'NatType)
reg_map' RegExprs ext (ctx '::> 'NatType)
bindings' AppRegMap ext (ctx '::> 'NatType)
appMap' [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t)

        Call Atom s (FunctionHandleType args tp)
h Assignment (Atom s) args
args TypeRepr tp
_ -> do
          let return_type :: TypeRepr tp
return_type = Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp
a
          let h' :: Reg ctx (FunctionHandleType args tp)
h' = TypedRegMap s ctx
-> Atom s (FunctionHandleType args tp)
-> Reg ctx (FunctionHandleType args tp)
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s (FunctionHandleType args tp)
h
          let arg_types :: Assignment TypeRepr args
arg_types = (forall (x :: CrucibleType). Atom s x -> TypeRepr x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Atom s) x -> Assignment TypeRepr 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 Atom s x -> TypeRepr x
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
forall (x :: CrucibleType). Atom s x -> TypeRepr x
typeOfAtom Assignment (Atom s) args
args
          let args' :: Assignment (Reg ctx) args
args' = (forall (x :: CrucibleType). Atom s x -> Reg ctx x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Atom s) x -> Assignment (Reg ctx) 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 (TypedRegMap s ctx -> Atom s x -> Reg ctx x
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map) Assignment (Atom s) args
args
          let stmt :: Stmt ext ctx (ctx '::> tp)
stmt = TypeRepr tp
-> Reg ctx (FunctionHandleType args tp)
-> Assignment TypeRepr args
-> Assignment (Reg ctx) args
-> Stmt ext ctx (ctx '::> tp)
forall (ret :: CrucibleType) (ctx :: Ctx CrucibleType)
       (args :: Ctx CrucibleType) ext.
TypeRepr ret
-> Reg ctx (FunctionHandleType args ret)
-> CtxRepr args
-> Assignment (Reg ctx) args
-> Stmt ext ctx (ctx '::> ret)
C.CallHandle TypeRepr tp
return_type Reg ctx (FunctionHandleType args tp)
h' Assignment TypeRepr args
arg_types Assignment (Reg ctx) args
args'
          let sz' :: Size (ctx '::> tp)
sz' = Size ctx -> Size (ctx '::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
sz
          let reg_map' :: TypedRegMap s (ctx '::> tp)
reg_map'  = TypedRegMap s ctx
reg_map  TypedRegMap s ctx
-> (TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp))
-> TypedRegMap s (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx '::> tp)
forall s (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
Value s tp
-> Size ctx -> TypedRegMap s ctx -> TypedRegMap s (ctx ::> tp)
assignRegister (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) Size ctx
sz
          let bindings' :: RegExprs ext (ctx '::> tp)
bindings' = RegExprs ext ctx
bindings RegExprs ext ctx
-> (RegExprs ext ctx -> RegExprs ext (ctx '::> tp))
-> RegExprs ext (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& MaybeF (Expr ext ctx) tp
-> RegExprs ext ctx -> RegExprs ext (ctx '::> tp)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
MaybeF (Expr ext ctx) tp
-> RegExprs ext ctx -> RegExprs ext (ctx ::> tp)
extendRegExprs MaybeF (Expr ext ctx) tp
forall {k} (f :: k -> Type) (tp :: k). MaybeF f tp
NothingF
          let appMap' :: AppRegMap ext (ctx '::> tp)
appMap'   = AppRegMap ext ctx
appMap   AppRegMap ext ctx
-> (AppRegMap ext ctx -> AppRegMap ext (ctx '::> tp))
-> AppRegMap ext (ctx '::> tp)
forall a b. a -> (a -> b) -> b
& AppRegMap ext ctx -> AppRegMap ext (ctx '::> tp)
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
AppRegMap ext ctx -> AppRegMap ext (ctx ::> tp)
appRegMap_extend
          ProgramLoc
-> Stmt ext ctx (ctx '::> tp)
-> StmtSeq ext blocks ret (ctx '::> tp)
-> StmtSeq ext blocks ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
C.ConsStmt ProgramLoc
pl Stmt ext ctx (ctx '::> tp)
stmt (FunctionName
-> BlockInfo ext s ret blocks
-> Size (ctx '::> tp)
-> TypedRegMap s (ctx '::> tp)
-> RegExprs ext (ctx '::> tp)
-> AppRegMap ext (ctx '::> tp)
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret (ctx '::> tp)
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size (ctx '::> tp)
sz' TypedRegMap s (ctx '::> tp)
reg_map' RegExprs ext (ctx '::> tp)
bindings' AppRegMap ext (ctx '::> tp)
appMap' [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t)

    Print Atom s (StringType Unicode)
e -> do
      ProgramLoc
-> Stmt ext ctx ctx
-> StmtSeq ext blocks ret ctx
-> StmtSeq ext blocks ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
C.ConsStmt ProgramLoc
pl
                 (Reg ctx (StringType Unicode) -> Stmt ext ctx ctx
forall (ctx :: Ctx CrucibleType) ext.
Reg ctx (StringType Unicode) -> Stmt ext ctx ctx
C.Print (TypedRegMap s ctx
-> Atom s (StringType Unicode) -> Reg ctx (StringType Unicode)
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s (StringType Unicode)
e))
                 (FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size ctx
sz TypedRegMap s ctx
reg_map RegExprs ext ctx
bindings AppRegMap ext ctx
appMap [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t)
    Assert Atom s BoolType
c Atom s (StringType Unicode)
m ->
      ProgramLoc
-> Stmt ext ctx ctx
-> StmtSeq ext blocks ret ctx
-> StmtSeq ext blocks ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
C.ConsStmt ProgramLoc
pl
                 (Reg ctx BoolType
-> Reg ctx (StringType Unicode) -> Stmt ext ctx ctx
forall (ctx :: Ctx CrucibleType) ext.
Reg ctx BoolType
-> Reg ctx (StringType Unicode) -> Stmt ext ctx ctx
C.Assert (TypedRegMap s ctx -> Atom s BoolType -> Reg ctx BoolType
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s BoolType
c)
                           (TypedRegMap s ctx
-> Atom s (StringType Unicode) -> Reg ctx (StringType Unicode)
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s (StringType Unicode)
m))
                 (FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size ctx
sz TypedRegMap s ctx
reg_map RegExprs ext ctx
bindings AppRegMap ext ctx
appMap [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t)

    Assume Atom s BoolType
c Atom s (StringType Unicode)
m ->
      ProgramLoc
-> Stmt ext ctx ctx
-> StmtSeq ext blocks ret ctx
-> StmtSeq ext blocks ret ctx
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
C.ConsStmt ProgramLoc
pl
                 (Reg ctx BoolType
-> Reg ctx (StringType Unicode) -> Stmt ext ctx ctx
forall (ctx :: Ctx CrucibleType) ext.
Reg ctx BoolType
-> Reg ctx (StringType Unicode) -> Stmt ext ctx ctx
C.Assume (TypedRegMap s ctx -> Atom s BoolType -> Reg ctx BoolType
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s BoolType
c)
                           (TypedRegMap s ctx
-> Atom s (StringType Unicode) -> Reg ctx (StringType Unicode)
forall s (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypedRegMap s ctx -> Atom s tp -> Reg ctx tp
resolveAtom TypedRegMap s ctx
reg_map Atom s (StringType Unicode)
m))
                 (FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size ctx
sz TypedRegMap s ctx
reg_map RegExprs ext ctx
bindings AppRegMap ext ctx
appMap [Posd (Stmt ext s)]
rest Posd (ExtendedTermStmt s blocks ret)
t)

    -- breakpoint statements are eliminated during the inferBlockInfo phase
    Breakpoint{} -> String -> StmtSeq ext blocks ret ctx
forall a. (?callStack::CallStack) => String -> a
error (String -> StmtSeq ext blocks ret ctx)
-> String -> StmtSeq ext blocks ret ctx
forall a b. (a -> b) -> a -> b
$
      String
"Unexpected breakpoint at position " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Position -> String
forall a. Show a => a -> String
show Position
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (Stmt ext s -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Stmt ext s -> Doc ann
Pretty.pretty Stmt ext s
s0)

data SomeBlockMap ext ret where
  SomeBlockMap ::
    Ctx.Index blocks tp ->
    Bimap BreakpointName (Some (C.BlockID blocks)) ->
    C.BlockMap ext blocks ret ->
    SomeBlockMap ext ret

resolveBlockMap :: forall ext s ret
                 . C.IsSyntaxExtension ext
                => FunctionName
                -> Label s
                -> [Block ext s ret]
                -> SomeBlockMap ext ret
resolveBlockMap :: forall ext s (ret :: CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> Label s -> [Block ext s ret] -> SomeBlockMap ext ret
resolveBlockMap FunctionName
nm Label s
entry [Block ext s ret]
blocks = do
  let resolveBlock :: BlockInfo ext s ret blocks
                   -> BlockInput ext s blocks ret args
                   -> C.Block ext blocks ret args
      resolveBlock :: forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
BlockInfo ext s ret blocks
-> BlockInput ext s blocks ret args -> Block ext blocks ret args
resolveBlock BlockInfo ext s ret blocks
bi BlockInput ext s blocks ret args
bin = do
        let sz :: Size args
sz = Assignment (Value s) args -> Size args
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size (BlockInput ext s blocks ret args -> Assignment (Value s) args
forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType).
BlockInput ext s blocks ret args -> Assignment (Value s) args
binputArgs BlockInput ext s blocks ret args
bin)
        let regs :: TypedRegMap s args
regs = Assignment (Value s) args -> TypedRegMap s args
forall s (args :: Ctx CrucibleType).
Assignment (Value s) args -> TypedRegMap s args
regMapFromAssignment (BlockInput ext s blocks ret args -> Assignment (Value s) args
forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType).
BlockInput ext s blocks ret args -> Assignment (Value s) args
binputArgs BlockInput ext s blocks ret args
bin)
        let regExprs :: Assignment (MaybeF (Expr ext args)) args
regExprs = Size args
-> (forall (tp :: CrucibleType). MaybeF (Expr ext args) tp)
-> Assignment (MaybeF (Expr ext args)) args
forall {k} (ctx :: Ctx k) (f :: k -> Type).
Size ctx -> (forall (tp :: k). f tp) -> Assignment f ctx
Ctx.replicate Size args
sz MaybeF (Expr ext args) tp
forall {k} (f :: k -> Type) (tp :: k). MaybeF f tp
forall (tp :: CrucibleType). MaybeF (Expr ext args) tp
NothingF
        let appMap :: AppRegMap ext ctx
appMap = AppRegMap ext ctx
forall ext (ctx :: Ctx CrucibleType). AppRegMap ext ctx
appRegMap_empty
        let stmts :: [Posd (Stmt ext s)]
stmts = Seq (Posd (Stmt ext s)) -> [Posd (Stmt ext s)]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
Fold.toList (Seq (Posd (Stmt ext s)) -> [Posd (Stmt ext s)])
-> Seq (Posd (Stmt ext s)) -> [Posd (Stmt ext s)]
forall a b. (a -> b) -> a -> b
$ BlockInput ext s blocks ret args -> Seq (Posd (Stmt ext s))
forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType).
BlockInput ext s blocks ret args -> Seq (Posd (Stmt ext s))
binputStmts BlockInput ext s blocks ret args
bin
        let term :: Posd (ExtendedTermStmt s blocks ret)
term = BlockInput ext s blocks ret args
-> Posd (ExtendedTermStmt s blocks ret)
forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType).
BlockInput ext s blocks ret args
-> Posd (ExtendedTermStmt s blocks ret)
binputTerm BlockInput ext s blocks ret args
bin
        C.Block { blockID :: BlockID blocks args
C.blockID = BlockInput ext s blocks ret args -> BlockID blocks args
forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType).
BlockInput ext s blocks ret args -> BlockID blocks args
binputID BlockInput ext s blocks ret args
bin
                , blockInputs :: CtxRepr args
C.blockInputs = (forall (x :: CrucibleType). Value s x -> TypeRepr x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Value s) x -> Assignment TypeRepr 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 Value s x -> TypeRepr x
forall s (tp :: CrucibleType). Value s tp -> TypeRepr tp
forall (x :: CrucibleType). Value s x -> TypeRepr x
typeOfValue (BlockInput ext s blocks ret args -> Assignment (Value s) args
forall ext s (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType).
BlockInput ext s blocks ret args -> Assignment (Value s) args
binputArgs BlockInput ext s blocks ret args
bin)
                , _blockStmts :: StmtSeq ext blocks ret args
C._blockStmts = FunctionName
-> BlockInfo ext s ret blocks
-> Size args
-> TypedRegMap s args
-> Assignment (MaybeF (Expr ext args)) args
-> AppRegMap ext args
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret args
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> BlockInfo ext s ret blocks
-> Size ctx
-> TypedRegMap s ctx
-> RegExprs ext ctx
-> AppRegMap ext ctx
-> [Posd (Stmt ext s)]
-> Posd (ExtendedTermStmt s blocks ret)
-> StmtSeq ext blocks ret ctx
resolveStmts FunctionName
nm BlockInfo ext s ret blocks
bi Size args
sz TypedRegMap s args
regs Assignment (MaybeF (Expr ext args)) args
regExprs AppRegMap ext args
forall ext (ctx :: Ctx CrucibleType). AppRegMap ext ctx
appMap [Posd (Stmt ext s)]
stmts Posd (ExtendedTermStmt s blocks ret)
term
                }
  case [Block ext s ret] -> Some (BlockInfo ext s ret)
forall ext s (ret :: CrucibleType).
[Block ext s ret] -> Some (BlockInfo ext s ret)
inferBlockInfo [Block ext s ret]
blocks of
    Some BlockInfo ext s ret x
bi ->
      case Label s -> JumpInfoMap s x -> Maybe (JumpInfo s x)
forall s (blocks :: Ctx (Ctx CrucibleType)).
Label s -> JumpInfoMap s blocks -> Maybe (JumpInfo s blocks)
lookupJumpInfo Label s
entry (BlockInfo ext s ret x -> JumpInfoMap s x
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks -> JumpInfoMap s blocks
biJumpInfo BlockInfo ext s ret x
bi) of
        Maybe (JumpInfo s x)
Nothing -> String -> SomeBlockMap ext ret
forall a. (?callStack::CallStack) => String -> a
error String
"Missing initial block."
        Just (JumpInfo (C.BlockID Index x types
idx) CtxRepr types
_ Assignment (Value s) types
_) ->
          Index x types
-> Bimap BreakpointName (Some (BlockID x))
-> BlockMap ext x ret
-> SomeBlockMap ext ret
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType)
       ext (ret :: CrucibleType).
Index blocks tp
-> Bimap BreakpointName (Some (BlockID blocks))
-> BlockMap ext blocks ret
-> SomeBlockMap ext ret
SomeBlockMap Index x types
idx (BlockInfo ext s ret x -> Bimap BreakpointName (Some (BlockID x))
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> Bimap BreakpointName (Some (BlockID blocks))
biBreakpoints BlockInfo ext s ret x
bi) (BlockMap ext x ret -> SomeBlockMap ext ret)
-> BlockMap ext x ret -> SomeBlockMap ext ret
forall a b. (a -> b) -> a -> b
$
            (forall (x :: Ctx CrucibleType).
 BlockInput ext s x ret x -> Block ext x ret x)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment (BlockInput ext s x ret) x
   -> Assignment (Block ext x ret) 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 :: Ctx CrucibleType -> Type)
       (g :: Ctx CrucibleType -> Type).
(forall (x :: Ctx CrucibleType). f x -> g x)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment f x -> Assignment g x
fmapFC (BlockInfo ext s ret x
-> BlockInput ext s x ret x -> Block ext x ret x
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
BlockInfo ext s ret blocks
-> BlockInput ext s blocks ret args -> Block ext blocks ret args
resolveBlock BlockInfo ext s ret x
bi) (BlockInfo ext s ret x -> Assignment (BlockInput ext s x ret) x
forall ext s (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
BlockInfo ext s ret blocks
-> Assignment (BlockInput ext s blocks ret) blocks
biBlocks BlockInfo ext s ret x
bi)

------------------------------------------------------------------------
-- SomeCFG

-- | Convert a CFG in RTL form into a Core CFG in SSA form.
--
-- This prunes the CFG so that only reachable blocks are returned.
toSSA :: C.IsSyntaxExtension ext
      => CFG ext s init ret
      -> C.SomeCFG ext init ret
toSSA :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
IsSyntaxExtension ext =>
CFG ext s init ret -> SomeCFG ext init ret
toSSA CFG ext s init ret
g = do
  let h :: FnHandle init ret
h = CFG ext s init ret -> FnHandle init ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> FnHandle init ret
cfgHandle CFG ext s init ret
g
  let initTypes :: CtxRepr init
initTypes = CFG ext s init ret -> CtxRepr init
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> CtxRepr init
cfgArgTypes CFG ext s init ret
g
  let entry :: Label s
entry = CFG ext s init ret -> Label s
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> Label s
cfgEntryLabel CFG ext s init ret
g
  let blocks :: [Block ext s ret]
blocks = CFG ext s init ret -> [Block ext s ret]
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> [Block ext s ret]
cfgBlocks CFG ext s init ret
g
  case FunctionName
-> Label s -> [Block ext s ret] -> SomeBlockMap ext ret
forall ext s (ret :: CrucibleType).
IsSyntaxExtension ext =>
FunctionName
-> Label s -> [Block ext s ret] -> SomeBlockMap ext ret
resolveBlockMap (FnHandle init ret -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
handleName FnHandle init ret
h) Label s
entry [Block ext s ret]
blocks of
    SomeBlockMap Index blocks tp
idx Bimap BreakpointName (Some (BlockID blocks))
breakpoints BlockMap ext blocks ret
block_map -> do
          let b :: Block ext blocks ret tp
b = BlockMap ext blocks ret
block_map BlockMap ext blocks ret
-> Index blocks tp -> Block ext blocks ret tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Index blocks tp
idx
          case Block ext blocks ret tp -> CtxRepr tp
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
C.blockInputs Block ext blocks ret tp
b CtxRepr tp -> CtxRepr init -> Maybe (tp :~: init)
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).
Assignment TypeRepr a -> Assignment TypeRepr b -> Maybe (a :~: b)
`testEquality` CtxRepr init
initTypes of
            Maybe (tp :~: init)
Nothing -> String -> SomeCFG ext init ret
forall a. (?callStack::CallStack) => String -> a
error (String -> SomeCFG ext init ret) -> String -> SomeCFG ext init ret
forall a b. (a -> b) -> a -> b
$
              String
"Input block type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CtxRepr tp -> String
forall a. Show a => a -> String
show (Block ext blocks ret tp -> CtxRepr tp
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
C.blockInputs Block ext blocks ret tp
b)
              String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" does not match expected " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CtxRepr init -> String
forall a. Show a => a -> String
show CtxRepr init
initTypes
              String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":\nwhile SSA converting function " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FnHandle init ret -> String
forall a. Show a => a -> String
show FnHandle init ret
h
            Just tp :~: init
Refl -> do
              let g' :: CFG ext blocks init ret
g' = C.CFG { cfgHandle :: FnHandle init ret
C.cfgHandle = FnHandle init ret
h
                             , cfgBlockMap :: BlockMap ext blocks ret
C.cfgBlockMap = BlockMap ext blocks ret
block_map
                             , cfgEntryBlockID :: BlockID blocks init
C.cfgEntryBlockID = Index blocks init -> BlockID blocks init
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Index blocks tp -> BlockID blocks tp
C.BlockID Index blocks init
Index blocks tp
idx
                             , cfgBreakpoints :: Bimap BreakpointName (Some (BlockID blocks))
C.cfgBreakpoints = Bimap BreakpointName (Some (BlockID blocks))
breakpoints
                             }
              CFG ext blocks init ret -> SomeCFG ext init ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> SomeCFG ext init ret
reachableCFG CFG ext blocks init ret
g'