------------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.CFG.Generator
-- Description      : Provides a monadic interface for constructing Crucible
--                    control flow graphs.
-- Copyright        : (c) Galois, Inc 2014-2018
-- License          : BSD3
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
--
-- This module provides a monadic interface for constructing control flow
-- graph expressions.  The goal is to make it easy to convert languages
-- into CFGs.
--
-- The CFGs generated by this interface are similar to, but not quite
-- the same as, the CFGs defined in "Lang.Crucible.CFG.Core". The
-- module "Lang.Crucible.CFG.SSAConversion" contains code that
-- converts the CFGs produced by this interface into Core CFGs in SSA
-- form.
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.CFG.Generator
  ( -- * Generator
    Generator
  , FunctionDef
  , defineFunction
  , defineFunctionOpt
    -- * Positions
  , getPosition
  , setPosition
  , withPosition
    -- * Expressions and statements
  , newReg
  , newUnassignedReg
  , readReg
  , assignReg
  , modifyReg
  , modifyRegM
  , readGlobal
  , writeGlobal
    -- * References
  , newRef
  , newEmptyRef
  , readRef
  , writeRef
  , dropRef
  , call
  , assertExpr
  , assumeExpr
  , addPrintStmt
  , addBreakpointStmt
  , extensionStmt
  , mkAtom
  , mkFresh
  , mkFreshFloat
  , forceEvaluation
    -- * Labels
  , newLabel
  , newLambdaLabel
  , newLambdaLabel'
  , currentBlockID
    -- * Block-terminating statements
    -- $termstmt
  , jump
  , jumpToLambda
  , branch
  , returnFromFunction
  , reportError
  , branchMaybe
  , branchVariant
  , tailCall
    -- * Defining blocks
    -- $define
  , defineBlock
  , defineLambdaBlock
  , defineBlockLabel
  , recordCFG
    -- * Control-flow combinators
  , continue
  , continueLambda
  , whenCond
  , unlessCond
  , ifte
  , ifte'
  , ifte_
  , ifteM
  , MatchMaybe(..)
  , caseMaybe
  , caseMaybe_
  , fromJustExpr
  , assertedJustExpr
  , while
  -- * Re-exports
  , Ctx.Ctx(..)
  , Position
  , module Lang.Crucible.CFG.Reg
  , module Lang.Crucible.CFG.EarlyMergeLoops
  ) where

import           Control.Lens hiding (Index)
import           Control.Monad ((>=>))
import qualified Control.Monad.Fail as F
import           Control.Monad.IO.Class (MonadIO(..))
import           Control.Monad.State.Strict ()
import           Control.Monad.Trans.Class (MonadTrans(..))
import           Control.Monad.Catch
import qualified Data.Foldable as Fold
import           Data.Kind
import           Data.Parameterized.Context as Ctx
import           Data.Parameterized.Nonce
import           Data.Parameterized.Some
import           Data.Parameterized.TraversableFC
import           Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import           Data.Text (Text)
import           Data.Void

import           What4.ProgramLoc
import           What4.Symbol

import           Lang.Crucible.CFG.Core (AnyCFG(..))
import           Lang.Crucible.CFG.Expr(App(..))
import           Lang.Crucible.CFG.Extension
import           Lang.Crucible.CFG.Reg hiding (AnyCFG)
import           Lang.Crucible.CFG.EarlyMergeLoops (earlyMergeLoops)
import           Lang.Crucible.FunctionHandle
import           Lang.Crucible.Types
import           Lang.Crucible.Utils.StateContT

------------------------------------------------------------------------
-- CurrentBlockState

-- | A sequence of statements.
type StmtSeq ext s = Seq (Posd (Stmt ext s))

-- | Information about block being generated in Generator.
data CurrentBlockState ext s
   = CBS { -- | Identifier for current block
           forall ext s. CurrentBlockState ext s -> BlockID s
cbsBlockID       :: !(BlockID s)
         , forall ext s. CurrentBlockState ext s -> ValueSet s
cbsInputValues   :: !(ValueSet s)
         , forall ext s. CurrentBlockState ext s -> StmtSeq ext s
_cbsStmts        :: !(StmtSeq ext s)
         }

initCurrentBlockState :: ValueSet s -> BlockID s -> CurrentBlockState ext s
initCurrentBlockState :: forall s ext. ValueSet s -> BlockID s -> CurrentBlockState ext s
initCurrentBlockState ValueSet s
inputs BlockID s
block_id =
  CBS { cbsBlockID :: BlockID s
cbsBlockID     = BlockID s
block_id
      , cbsInputValues :: ValueSet s
cbsInputValues = ValueSet s
inputs
      , _cbsStmts :: StmtSeq ext s
_cbsStmts      = StmtSeq ext s
forall a. Seq a
Seq.empty
      }

-- | Statements translated so far in this block.
cbsStmts :: Simple Lens (CurrentBlockState ext s) (StmtSeq ext s)
cbsStmts :: forall ext s (f :: Type -> Type).
Functor f =>
(StmtSeq ext s -> f (StmtSeq ext s))
-> CurrentBlockState ext s -> f (CurrentBlockState ext s)
cbsStmts = (CurrentBlockState ext s -> StmtSeq ext s)
-> (CurrentBlockState ext s
    -> StmtSeq ext s -> CurrentBlockState ext s)
-> Lens
     (CurrentBlockState ext s)
     (CurrentBlockState ext s)
     (StmtSeq ext s)
     (StmtSeq ext s)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens CurrentBlockState ext s -> StmtSeq ext s
forall ext s. CurrentBlockState ext s -> StmtSeq ext s
_cbsStmts (\CurrentBlockState ext s
s StmtSeq ext s
v -> CurrentBlockState ext s
s { _cbsStmts = v })

------------------------------------------------------------------------
-- GeneratorState

-- | State for translating within a basic block.
data IxGeneratorState ext s (t :: Type -> Type) ret m i
  = GS { forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> Label s
_gsEntryLabel :: !(Label s)
       , forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> Seq (Block ext s ret)
_gsBlocks    :: !(Seq (Block ext s ret))
       , forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> NonceGenerator m s
_gsNonceGen  :: !(NonceGenerator m s)
       , forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> i
_gsCurrent   :: !i
       , forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> Position
_gsPosition  :: !Position
       , forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> t s
_gsState     :: !(t s)
       , forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> [AnyCFG ext]
_seenFunctions :: ![AnyCFG ext]
       }

type GeneratorState ext s t ret m =
  IxGeneratorState ext s t ret m (CurrentBlockState ext s)

type EndState ext s t ret m =
  IxGeneratorState ext s t ret m ()

-- | Label for entry block.
gsEntryLabel :: Getter (IxGeneratorState ext s t ret m i) (Label s)
gsEntryLabel :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
(Contravariant f, Functor f) =>
(Label s -> f (Label s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsEntryLabel = (IxGeneratorState ext s t ret m i -> Label s)
-> (Label s -> f (Label s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to IxGeneratorState ext s t ret m i -> Label s
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> Label s
_gsEntryLabel

-- | List of previously processed blocks.
gsBlocks :: Simple Lens (IxGeneratorState ext s t ret m i) (Seq (Block ext s ret))
gsBlocks :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Seq (Block ext s ret) -> f (Seq (Block ext s ret)))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsBlocks = (IxGeneratorState ext s t ret m i -> Seq (Block ext s ret))
-> (IxGeneratorState ext s t ret m i
    -> Seq (Block ext s ret) -> IxGeneratorState ext s t ret m i)
-> Lens
     (IxGeneratorState ext s t ret m i)
     (IxGeneratorState ext s t ret m i)
     (Seq (Block ext s ret))
     (Seq (Block ext s ret))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens IxGeneratorState ext s t ret m i -> Seq (Block ext s ret)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> Seq (Block ext s ret)
_gsBlocks (\IxGeneratorState ext s t ret m i
s Seq (Block ext s ret)
v -> IxGeneratorState ext s t ret m i
s { _gsBlocks = v })

gsNonceGen :: Getter (IxGeneratorState ext s t ret m i) (NonceGenerator m s)
gsNonceGen :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
(Contravariant f, Functor f) =>
(NonceGenerator m s -> f (NonceGenerator m s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsNonceGen = (IxGeneratorState ext s t ret m i -> NonceGenerator m s)
-> (NonceGenerator m s -> f (NonceGenerator m s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to IxGeneratorState ext s t ret m i -> NonceGenerator m s
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> NonceGenerator m s
_gsNonceGen

-- | Information about current block.
gsCurrent :: Lens (IxGeneratorState ext s t ret m i) (IxGeneratorState ext s t ret m j) i j
gsCurrent :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent = (IxGeneratorState ext s t ret m i -> i)
-> (IxGeneratorState ext s t ret m i
    -> j -> IxGeneratorState ext s t ret m j)
-> Lens
     (IxGeneratorState ext s t ret m i)
     (IxGeneratorState ext s t ret m j)
     i
     j
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens IxGeneratorState ext s t ret m i -> i
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> i
_gsCurrent (\IxGeneratorState ext s t ret m i
s j
v -> IxGeneratorState ext s t ret m i
s { _gsCurrent = v })

-- | Current source position.
gsPosition :: Simple Lens (IxGeneratorState ext s t ret m i) Position
gsPosition :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Position -> f Position)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsPosition = (IxGeneratorState ext s t ret m i -> Position)
-> (IxGeneratorState ext s t ret m i
    -> Position -> IxGeneratorState ext s t ret m i)
-> Lens
     (IxGeneratorState ext s t ret m i)
     (IxGeneratorState ext s t ret m i)
     Position
     Position
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens IxGeneratorState ext s t ret m i -> Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> Position
_gsPosition (\IxGeneratorState ext s t ret m i
s Position
v -> IxGeneratorState ext s t ret m i
s { _gsPosition = v })

-- | User state for current block. This gets reset between blocks.
gsState :: Simple Lens (IxGeneratorState ext s t ret m i) (t s)
gsState :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(t s -> f (t s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsState = (IxGeneratorState ext s t ret m i -> t s)
-> (IxGeneratorState ext s t ret m i
    -> t s -> IxGeneratorState ext s t ret m i)
-> Lens
     (IxGeneratorState ext s t ret m i)
     (IxGeneratorState ext s t ret m i)
     (t s)
     (t s)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens IxGeneratorState ext s t ret m i -> t s
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> t s
_gsState (\IxGeneratorState ext s t ret m i
s t s
v -> IxGeneratorState ext s t ret m i
s { _gsState = v })

-- | List of functions seen by current generator.
seenFunctions :: Simple Lens (IxGeneratorState ext s t ret m i) [AnyCFG ext]
seenFunctions :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
([AnyCFG ext] -> f [AnyCFG ext])
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
seenFunctions = (IxGeneratorState ext s t ret m i -> [AnyCFG ext])
-> (IxGeneratorState ext s t ret m i
    -> [AnyCFG ext] -> IxGeneratorState ext s t ret m i)
-> Lens
     (IxGeneratorState ext s t ret m i)
     (IxGeneratorState ext s t ret m i)
     [AnyCFG ext]
     [AnyCFG ext]
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens IxGeneratorState ext s t ret m i -> [AnyCFG ext]
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i.
IxGeneratorState ext s t ret m i -> [AnyCFG ext]
_seenFunctions (\IxGeneratorState ext s t ret m i
s [AnyCFG ext]
v -> IxGeneratorState ext s t ret m i
s { _seenFunctions = v })

------------------------------------------------------------------------

startBlock ::
  BlockID s ->
  EndState ext s t ret m ->
  GeneratorState ext s t ret m
startBlock :: forall s ext (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
BlockID s -> EndState ext s t ret m -> GeneratorState ext s t ret m
startBlock BlockID s
l EndState ext s t ret m
gs =
  EndState ext s t ret m
gs EndState ext s t ret m
-> (EndState ext s t ret m -> GeneratorState ext s t ret m)
-> GeneratorState ext s t ret m
forall a b. a -> (a -> b) -> b
& (() -> Identity (CurrentBlockState ext s))
-> EndState ext s t ret m
-> Identity (GeneratorState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent ((() -> Identity (CurrentBlockState ext s))
 -> EndState ext s t ret m
 -> Identity (GeneratorState ext s t ret m))
-> CurrentBlockState ext s
-> EndState ext s t ret m
-> GeneratorState ext s t ret m
forall s t a b. ASetter s t a b -> b -> s -> t
.~ ValueSet s -> BlockID s -> CurrentBlockState ext s
forall s ext. ValueSet s -> BlockID s -> CurrentBlockState ext s
initCurrentBlockState ValueSet s
forall a. Set a
Set.empty BlockID s
l

-- | Define the current block by defining the position and final
-- statement.
terminateBlock ::
  IsSyntaxExtension ext =>
  TermStmt s ret ->
  GeneratorState ext s t ret m ->
  EndState ext s t ret m
terminateBlock :: forall ext s (ret :: CrucibleType) (t :: Type -> Type)
       (m :: Type -> Type).
IsSyntaxExtension ext =>
TermStmt s ret
-> GeneratorState ext s t ret m -> EndState ext s t ret m
terminateBlock TermStmt s ret
term GeneratorState ext s t ret m
gs =
  do let p :: Position
p = GeneratorState ext s t ret m
gsGeneratorState ext s t ret m
-> Getting Position (GeneratorState ext s t ret m) Position
-> Position
forall s a. s -> Getting a s a -> a
^.Getting Position (GeneratorState ext s t ret m) Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Position -> f Position)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsPosition
     let cbs :: CurrentBlockState ext s
cbs = GeneratorState ext s t ret m
gsGeneratorState ext s t ret m
-> Getting
     (CurrentBlockState ext s)
     (GeneratorState ext s t ret m)
     (CurrentBlockState ext s)
-> CurrentBlockState ext s
forall s a. s -> Getting a s a -> a
^.Getting
  (CurrentBlockState ext s)
  (GeneratorState ext s t ret m)
  (CurrentBlockState ext s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent
     -- Define block
     let b :: Block ext s ret
b = BlockID s
-> ValueSet s
-> Seq (Posd (Stmt ext s))
-> Posd (TermStmt s ret)
-> Block ext s ret
forall ext s (ret :: CrucibleType).
TraverseExt ext =>
BlockID s
-> ValueSet s
-> Seq (Posd (Stmt ext s))
-> Posd (TermStmt s ret)
-> Block ext s ret
mkBlock (CurrentBlockState ext s -> BlockID s
forall ext s. CurrentBlockState ext s -> BlockID s
cbsBlockID CurrentBlockState ext s
cbs) (CurrentBlockState ext s -> ValueSet s
forall ext s. CurrentBlockState ext s -> ValueSet s
cbsInputValues CurrentBlockState ext s
cbs) (CurrentBlockState ext s
cbsCurrentBlockState ext s
-> Getting
     (Seq (Posd (Stmt ext s)))
     (CurrentBlockState ext s)
     (Seq (Posd (Stmt ext s)))
-> Seq (Posd (Stmt ext s))
forall s a. s -> Getting a s a -> a
^.Getting
  (Seq (Posd (Stmt ext s)))
  (CurrentBlockState ext s)
  (Seq (Posd (Stmt ext s)))
forall ext s (f :: Type -> Type).
Functor f =>
(StmtSeq ext s -> f (StmtSeq ext s))
-> CurrentBlockState ext s -> f (CurrentBlockState ext s)
cbsStmts) (Position -> TermStmt s ret -> Posd (TermStmt s ret)
forall v. Position -> v -> Posd v
Posd Position
p TermStmt s ret
term)
     -- Store block
     let gs' :: EndState ext s t ret m
gs' = GeneratorState ext s t ret m
gs GeneratorState ext s t ret m
-> (GeneratorState ext s t ret m -> EndState ext s t ret m)
-> EndState ext s t ret m
forall a b. a -> (a -> b) -> b
& (CurrentBlockState ext s -> Identity ())
-> GeneratorState ext s t ret m
-> Identity (EndState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent ((CurrentBlockState ext s -> Identity ())
 -> GeneratorState ext s t ret m
 -> Identity (EndState ext s t ret m))
-> () -> GeneratorState ext s t ret m -> EndState ext s t ret m
forall s t a b. ASetter s t a b -> b -> s -> t
.~ ()
                  EndState ext s t ret m
-> (EndState ext s t ret m -> EndState ext s t ret m)
-> EndState ext s t ret m
forall a b. a -> (a -> b) -> b
& (Seq (Block ext s ret) -> Identity (Seq (Block ext s ret)))
-> EndState ext s t ret m -> Identity (EndState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Seq (Block ext s ret) -> f (Seq (Block ext s ret)))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsBlocks  ((Seq (Block ext s ret) -> Identity (Seq (Block ext s ret)))
 -> EndState ext s t ret m -> Identity (EndState ext s t ret m))
-> (Seq (Block ext s ret) -> Seq (Block ext s ret))
-> EndState ext s t ret m
-> EndState ext s t ret m
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Seq (Block ext s ret) -> Block ext s ret -> Seq (Block ext s ret)
forall a. Seq a -> a -> Seq a
Seq.|> Block ext s ret
b)
     Block ext s ret -> EndState ext s t ret m -> EndState ext s t ret m
forall a b. a -> b -> b
seq Block ext s ret
b EndState ext s t ret m
gs'

------------------------------------------------------------------------
-- Generator

-- | A generator is used for constructing a CFG from a sequence of
-- monadic actions.
--
-- The 'ext' parameter indicates the syntax extension.
-- The 's' parameter is the phantom parameter for CFGs.
-- The 't' parameter is the parameterized type that allows user-defined
-- state.
-- The 'ret' parameter is the return type of the CFG.
-- The 'm' parameter is a monad over which the generator is lifted
-- The 'a' parameter is the value returned by the monad.

newtype Generator ext s (t :: Type -> Type) (ret :: CrucibleType) m a
      = Generator { forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
Generator ext s t ret m a
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
unGenerator :: StateContT (GeneratorState ext s t ret m)
                                              (EndState ext s t ret m)
                                              m
                                              a
                  }
  deriving ( (forall a b.
 (a -> b) -> Generator ext s t ret m a -> Generator ext s t ret m b)
-> (forall a b.
    a -> Generator ext s t ret m b -> Generator ext s t ret m a)
-> Functor (Generator ext s t ret m)
forall a b.
a -> Generator ext s t ret m b -> Generator ext s t ret m a
forall a b.
(a -> b) -> Generator ext s t ret m a -> Generator ext s t ret m b
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a b.
a -> Generator ext s t ret m b -> Generator ext s t ret m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a b.
(a -> b) -> Generator ext s t ret m a -> Generator ext s t ret m b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a b.
(a -> b) -> Generator ext s t ret m a -> Generator ext s t ret m b
fmap :: forall a b.
(a -> b) -> Generator ext s t ret m a -> Generator ext s t ret m b
$c<$ :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a b.
a -> Generator ext s t ret m b -> Generator ext s t ret m a
<$ :: forall a b.
a -> Generator ext s t ret m b -> Generator ext s t ret m a
Functor
           , Functor (Generator ext s t ret m)
Functor (Generator ext s t ret m) =>
(forall a. a -> Generator ext s t ret m a)
-> (forall a b.
    Generator ext s t ret m (a -> b)
    -> Generator ext s t ret m a -> Generator ext s t ret m b)
-> (forall a b c.
    (a -> b -> c)
    -> Generator ext s t ret m a
    -> Generator ext s t ret m b
    -> Generator ext s t ret m c)
-> (forall a b.
    Generator ext s t ret m a
    -> Generator ext s t ret m b -> Generator ext s t ret m b)
-> (forall a b.
    Generator ext s t ret m a
    -> Generator ext s t ret m b -> Generator ext s t ret m a)
-> Applicative (Generator ext s t ret m)
forall a. a -> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
forall a b.
Generator ext s t ret m (a -> b)
-> Generator ext s t ret m a -> Generator ext s t ret m b
forall a b c.
(a -> b -> c)
-> Generator ext s t ret m a
-> Generator ext s t ret m b
-> Generator ext s t ret m c
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Functor (Generator ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
a -> Generator ext s t ret m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a b.
Generator ext s t ret m (a -> b)
-> Generator ext s t ret m a -> Generator ext s t ret m b
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a b c.
(a -> b -> c)
-> Generator ext s t ret m a
-> Generator ext s t ret m b
-> Generator ext s t ret m c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
a -> Generator ext s t ret m a
pure :: forall a. a -> Generator ext s t ret m a
$c<*> :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a b.
Generator ext s t ret m (a -> b)
-> Generator ext s t ret m a -> Generator ext s t ret m b
<*> :: forall a b.
Generator ext s t ret m (a -> b)
-> Generator ext s t ret m a -> Generator ext s t ret m b
$cliftA2 :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a b c.
(a -> b -> c)
-> Generator ext s t ret m a
-> Generator ext s t ret m b
-> Generator ext s t ret m c
liftA2 :: forall a b c.
(a -> b -> c)
-> Generator ext s t ret m a
-> Generator ext s t ret m b
-> Generator ext s t ret m c
$c*> :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
*> :: forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
$c<* :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m a
<* :: forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m a
Applicative
           , Monad (Generator ext s t ret m)
Monad (Generator ext s t ret m) =>
(forall e a.
 (HasCallStack, Exception e) =>
 e -> Generator ext s t ret m a)
-> MonadThrow (Generator ext s t ret m)
forall e a.
(HasCallStack, Exception e) =>
e -> Generator ext s t ret m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
MonadThrow m =>
Monad (Generator ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> Generator ext s t ret m a
forall (m :: Type -> Type).
Monad m =>
(forall e a. (HasCallStack, Exception e) => e -> m a)
-> MonadThrow m
$cthrowM :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) e a.
(MonadThrow m, HasCallStack, Exception e) =>
e -> Generator ext s t ret m a
throwM :: forall e a.
(HasCallStack, Exception e) =>
e -> Generator ext s t ret m a
MonadThrow
           , MonadThrow (Generator ext s t ret m)
MonadThrow (Generator ext s t ret m) =>
(forall e a.
 (HasCallStack, Exception e) =>
 Generator ext s t ret m a
 -> (e -> Generator ext s t ret m a) -> Generator ext s t ret m a)
-> MonadCatch (Generator ext s t ret m)
forall e a.
(HasCallStack, Exception e) =>
Generator ext s t ret m a
-> (e -> Generator ext s t ret m a) -> Generator ext s t ret m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
MonadCatch m =>
MonadThrow (Generator ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) e a.
(MonadCatch m, HasCallStack, Exception e) =>
Generator ext s t ret m a
-> (e -> Generator ext s t ret m a) -> Generator ext s t ret m a
forall (m :: Type -> Type).
MonadThrow m =>
(forall e a.
 (HasCallStack, Exception e) =>
 m a -> (e -> m a) -> m a)
-> MonadCatch m
$ccatch :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) e a.
(MonadCatch m, HasCallStack, Exception e) =>
Generator ext s t ret m a
-> (e -> Generator ext s t ret m a) -> Generator ext s t ret m a
catch :: forall e a.
(HasCallStack, Exception e) =>
Generator ext s t ret m a
-> (e -> Generator ext s t ret m a) -> Generator ext s t ret m a
MonadCatch
           )

instance MonadTrans (Generator ext s t ret) where
  lift :: forall (m :: Type -> Type) a.
Monad m =>
m a -> Generator ext s t ret m a
lift m a
m = StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (m a
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
forall (m :: Type -> Type) a.
Monad m =>
m a
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m a
m)

instance Monad m => Monad (Generator ext s t ret m) where
  Generator ext s t ret m a
x >>= :: forall a b.
Generator ext s t ret m a
-> (a -> Generator ext s t ret m b) -> Generator ext s t ret m b
>>= a -> Generator ext s t ret m b
f = StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m b
-> Generator ext s t ret m b
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (Generator ext s t ret m a
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
Generator ext s t ret m a
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
unGenerator Generator ext s t ret m a
x StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> (a
    -> StateContT
         (GeneratorState ext s t ret m) (EndState ext s t ret m) m b)
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m b
forall a b.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> (a
    -> StateContT
         (GeneratorState ext s t ret m) (EndState ext s t ret m) m b)
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Generator ext s t ret m b
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m b
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
Generator ext s t ret m a
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
unGenerator (Generator ext s t ret m b
 -> StateContT
      (GeneratorState ext s t ret m) (EndState ext s t ret m) m b)
-> (a -> Generator ext s t ret m b)
-> a
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Generator ext s t ret m b
f)

instance F.MonadFail m => F.MonadFail (Generator ext s t ret m) where
  fail :: forall a. String -> Generator ext s t ret m a
fail String
msg = StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
   (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
 -> Generator ext s t ret m a)
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
forall a b. (a -> b) -> a -> b
$ do
     Position
p <- Getting Position (GeneratorState ext s t ret m) Position
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m Position
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting Position (GeneratorState ext s t ret m) Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Position -> f Position)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsPosition
     String
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
forall a.
String
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
 -> StateContT
      (GeneratorState ext s t ret m) (EndState ext s t ret m) m a)
-> String
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [ String
"Failure encountered while generating a Crucible CFG:"
                    , String
"at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Position -> String
forall a. Show a => a -> String
show Position
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg
                    ]

instance Monad m => MonadState (t s) (Generator ext s t ret m) where
  get :: Generator ext s t ret m (t s)
get = StateContT
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  (EndState ext s t ret m)
  m
  (t s)
-> Generator ext s t ret m (t s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
   (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
   (EndState ext s t ret m)
   m
   (t s)
 -> Generator ext s t ret m (t s))
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     (t s)
-> Generator ext s t ret m (t s)
forall a b. (a -> b) -> a -> b
$ Getting
  (t s)
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  (t s)
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     (t s)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
  (t s)
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  (t s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(t s -> f (t s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsState
  put :: t s -> Generator ext s t ret m ()
put t s
v = StateContT
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  (EndState ext s t ret m)
  m
  ()
-> Generator ext s t ret m ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
   (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
   (EndState ext s t ret m)
   m
   ()
 -> Generator ext s t ret m ())
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     ()
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ (t s -> Identity (t s))
-> IxGeneratorState ext s t ret m (CurrentBlockState ext s)
-> Identity
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(t s -> f (t s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsState ((t s -> Identity (t s))
 -> IxGeneratorState ext s t ret m (CurrentBlockState ext s)
 -> Identity
      (IxGeneratorState ext s t ret m (CurrentBlockState ext s)))
-> t s
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= t s
v

instance MonadIO m => MonadIO (Generator ext s t ret m) where
  liftIO :: forall a. IO a -> Generator ext s t ret m a
liftIO IO a
m = m a -> Generator ext s t ret m a
forall (m :: Type -> Type) a.
Monad m =>
m a -> Generator ext s t ret m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO a -> m a
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO IO a
m)

-- This function only works for 'Generator' actions that terminate
-- early, i.e. do not call their continuation. This includes actions
-- that end with block-terminating statements defined with
-- 'terminateEarly'.
runGenerator ::
  Generator ext s t ret m Void ->
  GeneratorState ext s t ret m ->
  m (EndState ext s t ret m)
runGenerator :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Generator ext s t ret m Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
runGenerator Generator ext s t ret m Void
m GeneratorState ext s t ret m
gs = StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m Void
-> (Void
    -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> GeneratorState ext s t ret m
-> m (EndState ext s t ret m)
forall s r (m :: Type -> Type) a.
StateContT s r m a -> (a -> s -> m r) -> s -> m r
runStateContT (Generator ext s t ret m Void
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m Void
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
Generator ext s t ret m a
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
unGenerator Generator ext s t ret m Void
m) Void -> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
forall a. Void -> a
absurd GeneratorState ext s t ret m
gs

-- | Get the current position.
getPosition :: Generator ext s t ret m Position
getPosition :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Generator ext s t ret m Position
getPosition = StateContT
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  (EndState ext s t ret m)
  m
  Position
-> Generator ext s t ret m Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
   (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
   (EndState ext s t ret m)
   m
   Position
 -> Generator ext s t ret m Position)
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     Position
-> Generator ext s t ret m Position
forall a b. (a -> b) -> a -> b
$ Getting
  Position
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  Position
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     Position
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
  Position
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Position -> f Position)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsPosition

-- | Set the current position.
setPosition :: Position -> Generator ext s t ret m ()
setPosition :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Position -> Generator ext s t ret m ()
setPosition Position
p = StateContT
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  (EndState ext s t ret m)
  m
  ()
-> Generator ext s t ret m ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
   (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
   (EndState ext s t ret m)
   m
   ()
 -> Generator ext s t ret m ())
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     ()
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ (Position -> Identity Position)
-> IxGeneratorState ext s t ret m (CurrentBlockState ext s)
-> Identity
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Position -> f Position)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsPosition ((Position -> Identity Position)
 -> IxGeneratorState ext s t ret m (CurrentBlockState ext s)
 -> Identity
      (IxGeneratorState ext s t ret m (CurrentBlockState ext s)))
-> Position
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Position
p

-- | Set the current position temporarily, and reset it afterwards.
withPosition :: Monad m
             => Position
             -> Generator ext s t ret m a
             -> Generator ext s t ret m a
withPosition :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
Monad m =>
Position -> Generator ext s t ret m a -> Generator ext s t ret m a
withPosition Position
p Generator ext s t ret m a
m =
  do Position
old_pos <- Generator ext s t ret m Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Generator ext s t ret m Position
getPosition
     Position -> Generator ext s t ret m ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Position -> Generator ext s t ret m ()
setPosition Position
p
     a
v <- Generator ext s t ret m a
m
     Position -> Generator ext s t ret m ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Position -> Generator ext s t ret m ()
setPosition Position
old_pos
     a -> Generator ext s t ret m a
forall a. a -> Generator ext s t ret m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a
v

mkNonce :: Monad m => Generator ext s t ret m (Nonce s tp)
mkNonce :: forall {k} (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) (tp :: k).
Monad m =>
Generator ext s t ret m (Nonce s tp)
mkNonce =
  do NonceGenerator m s
ng <- StateContT
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  (EndState ext s t ret m)
  m
  (NonceGenerator m s)
-> Generator ext s t ret m (NonceGenerator m s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
   (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
   (EndState ext s t ret m)
   m
   (NonceGenerator m s)
 -> Generator ext s t ret m (NonceGenerator m s))
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     (NonceGenerator m s)
-> Generator ext s t ret m (NonceGenerator m s)
forall a b. (a -> b) -> a -> b
$ Getting
  (NonceGenerator m s)
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  (NonceGenerator m s)
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     (NonceGenerator m s)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
  (NonceGenerator m s)
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  (NonceGenerator m s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
(Contravariant f, Functor f) =>
(NonceGenerator m s -> f (NonceGenerator m s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsNonceGen
     StateContT
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  (EndState ext s t ret m)
  m
  (Nonce s tp)
-> Generator ext s t ret m (Nonce s tp)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
   (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
   (EndState ext s t ret m)
   m
   (Nonce s tp)
 -> Generator ext s t ret m (Nonce s tp))
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     (Nonce s tp)
-> Generator ext s t ret m (Nonce s tp)
forall a b. (a -> b) -> a -> b
$ m (Nonce s tp)
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     (Nonce s tp)
forall (m :: Type -> Type) a.
Monad m =>
m a
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Nonce s tp)
 -> StateContT
      (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
      (EndState ext s t ret m)
      m
      (Nonce s tp))
-> m (Nonce s tp)
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     (Nonce s tp)
forall a b. (a -> b) -> a -> b
$ NonceGenerator m s -> m (Nonce s tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator m s
ng

----------------------------------------------------------------------
-- Expressions and statements

addStmt :: Monad m => Stmt ext s -> Generator ext s t ret m ()
addStmt :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt Stmt ext s
s =
  do Position
p <- Generator ext s t ret m Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Generator ext s t ret m Position
getPosition
     CurrentBlockState ext s
cbs <- StateContT
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  (EndState ext s t ret m)
  m
  (CurrentBlockState ext s)
-> Generator ext s t ret m (CurrentBlockState ext s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
   (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
   (EndState ext s t ret m)
   m
   (CurrentBlockState ext s)
 -> Generator ext s t ret m (CurrentBlockState ext s))
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     (CurrentBlockState ext s)
-> Generator ext s t ret m (CurrentBlockState ext s)
forall a b. (a -> b) -> a -> b
$ Getting
  (CurrentBlockState ext s)
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  (CurrentBlockState ext s)
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     (CurrentBlockState ext s)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
  (CurrentBlockState ext s)
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  (CurrentBlockState ext s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent
     let ps :: Posd (Stmt ext s)
ps = Position -> Stmt ext s -> Posd (Stmt ext s)
forall v. Position -> v -> Posd v
Posd Position
p Stmt ext s
s
     let cbs' :: CurrentBlockState ext s
cbs' = CurrentBlockState ext s
cbs CurrentBlockState ext s
-> (CurrentBlockState ext s -> CurrentBlockState ext s)
-> CurrentBlockState ext s
forall a b. a -> (a -> b) -> b
& (StmtSeq ext s -> Identity (StmtSeq ext s))
-> CurrentBlockState ext s -> Identity (CurrentBlockState ext s)
forall ext s (f :: Type -> Type).
Functor f =>
(StmtSeq ext s -> f (StmtSeq ext s))
-> CurrentBlockState ext s -> f (CurrentBlockState ext s)
cbsStmts ((StmtSeq ext s -> Identity (StmtSeq ext s))
 -> CurrentBlockState ext s -> Identity (CurrentBlockState ext s))
-> (StmtSeq ext s -> StmtSeq ext s)
-> CurrentBlockState ext s
-> CurrentBlockState ext s
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (StmtSeq ext s -> Posd (Stmt ext s) -> StmtSeq ext s
forall a. Seq a -> a -> Seq a
Seq.|> Posd (Stmt ext s)
ps)
     Posd (Stmt ext s)
-> Generator ext s t ret m () -> Generator ext s t ret m ()
forall a b. a -> b -> b
seq Posd (Stmt ext s)
ps (Generator ext s t ret m () -> Generator ext s t ret m ())
-> Generator ext s t ret m () -> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ CurrentBlockState ext s
-> Generator ext s t ret m () -> Generator ext s t ret m ()
forall a b. a -> b -> b
seq CurrentBlockState ext s
cbs' (Generator ext s t ret m () -> Generator ext s t ret m ())
-> Generator ext s t ret m () -> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ StateContT
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  (EndState ext s t ret m)
  m
  ()
-> Generator ext s t ret m ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
   (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
   (EndState ext s t ret m)
   m
   ()
 -> Generator ext s t ret m ())
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     ()
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ (CurrentBlockState ext s -> Identity (CurrentBlockState ext s))
-> IxGeneratorState ext s t ret m (CurrentBlockState ext s)
-> Identity
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent ((CurrentBlockState ext s -> Identity (CurrentBlockState ext s))
 -> IxGeneratorState ext s t ret m (CurrentBlockState ext s)
 -> Identity
      (IxGeneratorState ext s t ret m (CurrentBlockState ext s)))
-> CurrentBlockState ext s
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= CurrentBlockState ext s
cbs'

freshAtom :: (Monad m, IsSyntaxExtension ext) => AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom AtomValue ext s tp
av =
  do Position
p <- Generator ext s t ret m Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Generator ext s t ret m Position
getPosition
     Nonce s tp
n <- Generator ext s t ret m (Nonce s tp)
forall {k} (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) (tp :: k).
Monad m =>
Generator ext s t ret m (Nonce s tp)
mkNonce
     let atom :: Atom s tp
atom = Atom { atomPosition :: Position
atomPosition = Position
p
                     , atomId :: Nonce s tp
atomId = Nonce s tp
n
                     , atomSource :: AtomSource s tp
atomSource = AtomSource s tp
forall s (tp :: CrucibleType). AtomSource s tp
Assigned
                     , typeOfAtom :: TypeRepr tp
typeOfAtom = AtomValue ext s tp -> TypeRepr tp
forall ext s (tp :: CrucibleType).
(TypeApp (StmtExtension ext), TypeApp (ExprExtension ext)) =>
AtomValue ext s tp -> TypeRepr tp
typeOfAtomValue AtomValue ext s tp
av
                     }
     Stmt ext s -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (Atom s tp -> AtomValue ext s tp -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom Atom s tp
atom AtomValue ext s tp
av)
     Atom s tp -> Generator ext s t ret m (Atom s tp)
forall a. a -> Generator ext s t ret m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Atom s tp
atom


mkFresh :: (Monad m, IsSyntaxExtension ext)
        => BaseTypeRepr tp
        -> Maybe SolverSymbol
        -> Generator ext s t ret m (Atom s (BaseToType tp))
mkFresh :: forall (m :: Type -> Type) ext (tp :: BaseType) s
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
BaseTypeRepr tp
-> Maybe SolverSymbol
-> Generator ext s t ret m (Atom s (BaseToType tp))
mkFresh BaseTypeRepr tp
tr Maybe SolverSymbol
symb = AtomValue ext s (BaseToType tp)
-> Generator ext s t ret m (Atom s (BaseToType tp))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (BaseTypeRepr tp
-> Maybe SolverSymbol -> AtomValue ext s (BaseToType tp)
forall (bt :: BaseType) ext s.
BaseTypeRepr bt
-> Maybe SolverSymbol -> AtomValue ext s ('BaseToType bt)
FreshConstant BaseTypeRepr tp
tr Maybe SolverSymbol
symb)

mkFreshFloat :: (Monad m, IsSyntaxExtension ext)
             => FloatInfoRepr fi
             -> Maybe SolverSymbol
             -> Generator ext s t ret m (Atom s (FloatType fi))
mkFreshFloat :: forall (m :: Type -> Type) ext (fi :: FloatInfo) s
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
FloatInfoRepr fi
-> Maybe SolverSymbol
-> Generator ext s t ret m (Atom s (FloatType fi))
mkFreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
symb = AtomValue ext s (FloatType fi)
-> Generator ext s t ret m (Atom s (FloatType fi))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (FloatInfoRepr fi
-> Maybe SolverSymbol -> AtomValue ext s (FloatType fi)
forall (fi :: FloatInfo) ext s.
FloatInfoRepr fi
-> Maybe SolverSymbol -> AtomValue ext s ('FloatType fi)
FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
symb)

-- | Create an atom equivalent to the given expression if it is
-- not already an 'AtomExpr'.
mkAtom :: (Monad m, IsSyntaxExtension ext) => Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom (AtomExpr Atom s tp
a)   = Atom s tp -> Generator ext s t ret m (Atom s tp)
forall a. a -> Generator ext s t ret m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Atom s tp
a
mkAtom (App App ext (Expr ext s) tp
a)        = AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (AtomValue ext s tp -> Generator ext s t ret m (Atom s tp))
-> (App ext (Atom s) tp -> AtomValue ext s tp)
-> App ext (Atom s) tp
-> Generator ext s t ret m (Atom s tp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. App ext (Atom s) tp -> AtomValue ext s tp
forall ext s (tp :: CrucibleType).
App ext (Atom s) tp -> AtomValue ext s tp
EvalApp (App ext (Atom s) tp -> Generator ext s t ret m (Atom s tp))
-> Generator ext s t ret m (App ext (Atom s) tp)
-> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall (x :: CrucibleType).
 Expr ext s x -> Generator ext s t ret m (Atom s x))
-> forall (x :: CrucibleType).
   App ext (Expr ext s) x
   -> Generator ext s t ret m (App ext (Atom s) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType). App ext f x -> m (App ext g x)
traverseFC Expr ext s x -> Generator ext s t ret m (Atom s x)
forall (x :: CrucibleType).
Expr ext s x -> Generator ext s t ret m (Atom s x)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom App ext (Expr ext s) tp
a

-- | Read a global variable.
readGlobal :: (Monad m, IsSyntaxExtension ext) => GlobalVar tp -> Generator ext s t ret m (Expr ext s tp)
readGlobal :: forall (m :: Type -> Type) ext (tp :: CrucibleType) s
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
GlobalVar tp -> Generator ext s t ret m (Expr ext s tp)
readGlobal GlobalVar tp
v = Atom s tp -> Expr ext s tp
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (Atom s tp -> Expr ext s tp)
-> Generator ext s t ret m (Atom s tp)
-> Generator ext s t ret m (Expr ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (GlobalVar tp -> AtomValue ext s tp
forall (tp :: CrucibleType) ext s.
GlobalVar tp -> AtomValue ext s tp
ReadGlobal GlobalVar tp
v)

-- | Write to a global variable.
writeGlobal :: (Monad m, IsSyntaxExtension ext) => GlobalVar tp -> Expr ext s tp -> Generator ext s t ret m ()
writeGlobal :: forall (m :: Type -> Type) ext (tp :: CrucibleType) s
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
GlobalVar tp -> Expr ext s tp -> Generator ext s t ret m ()
writeGlobal GlobalVar tp
v Expr ext s tp
e =
  do Atom s tp
a <- Expr ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s tp
e
     Stmt ext s -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (GlobalVar tp -> Atom s tp -> Stmt ext s
forall ext s (tp :: CrucibleType).
GlobalVar tp -> Atom s tp -> Stmt ext s
WriteGlobal GlobalVar tp
v Atom s tp
a)

-- | Read the current value of a reference cell.
readRef :: (Monad m, IsSyntaxExtension ext) => Expr ext s (ReferenceType tp) -> Generator ext s t ret m (Expr ext s tp)
readRef :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (ReferenceType tp)
-> Generator ext s t ret m (Expr ext s tp)
readRef Expr ext s (ReferenceType tp)
ref =
  do Atom s (ReferenceType tp)
r <- Expr ext s (ReferenceType tp)
-> Generator ext s t ret m (Atom s (ReferenceType tp))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (ReferenceType tp)
ref
     Atom s tp -> Expr ext s tp
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (Atom s tp -> Expr ext s tp)
-> Generator ext s t ret m (Atom s tp)
-> Generator ext s t ret m (Expr ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (Atom s (ReferenceType tp) -> AtomValue ext s tp
forall s (tp :: CrucibleType) ext.
Atom s (ReferenceType tp) -> AtomValue ext s tp
ReadRef Atom s (ReferenceType tp)
r)

-- | Write the given value into the reference cell.
writeRef :: (Monad m, IsSyntaxExtension ext) => Expr ext s (ReferenceType tp) -> Expr ext s tp -> Generator ext s t ret m ()
writeRef :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (ReferenceType tp)
-> Expr ext s tp -> Generator ext s t ret m ()
writeRef Expr ext s (ReferenceType tp)
ref Expr ext s tp
val =
  do Atom s (ReferenceType tp)
r <- Expr ext s (ReferenceType tp)
-> Generator ext s t ret m (Atom s (ReferenceType tp))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (ReferenceType tp)
ref
     Atom s tp
v <- Expr ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s tp
val
     Stmt ext s -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (Atom s (ReferenceType tp) -> Atom s tp -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s (ReferenceType tp) -> Atom s tp -> Stmt ext s
WriteRef Atom s (ReferenceType tp)
r Atom s tp
v)

-- | Deallocate the given reference cell, returning it to an uninialized state.
--   The reference cell can still be used; subsequent writes will succeed,
--   and reads will succeed if some value is written first.
dropRef :: (Monad m, IsSyntaxExtension ext) => Expr ext s (ReferenceType tp) -> Generator ext s t ret m ()
dropRef :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (ReferenceType tp) -> Generator ext s t ret m ()
dropRef Expr ext s (ReferenceType tp)
ref =
  do Atom s (ReferenceType tp)
r <- Expr ext s (ReferenceType tp)
-> Generator ext s t ret m (Atom s (ReferenceType tp))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (ReferenceType tp)
ref
     Stmt ext s -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (Atom s (ReferenceType tp) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s (ReferenceType tp) -> Stmt ext s
DropRef Atom s (ReferenceType tp)
r)

-- | Generate a new reference cell with the given initial contents.
newRef :: (Monad m, IsSyntaxExtension ext) => Expr ext s tp -> Generator ext s t ret m (Expr ext s (ReferenceType tp))
newRef :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp
-> Generator ext s t ret m (Expr ext s (ReferenceType tp))
newRef Expr ext s tp
val =
  do Atom s tp
v <- Expr ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s tp
val
     Atom s (ReferenceType tp) -> Expr ext s (ReferenceType tp)
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (Atom s (ReferenceType tp) -> Expr ext s (ReferenceType tp))
-> Generator ext s t ret m (Atom s (ReferenceType tp))
-> Generator ext s t ret m (Expr ext s (ReferenceType tp))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AtomValue ext s (ReferenceType tp)
-> Generator ext s t ret m (Atom s (ReferenceType tp))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (Atom s tp -> AtomValue ext s (ReferenceType tp)
forall s (tp1 :: CrucibleType) ext.
Atom s tp1 -> AtomValue ext s ('ReferenceType tp1)
NewRef Atom s tp
v)

-- | Generate a new empty reference cell.  If an unassigned reference is later
--   read, it will generate a runtime error.
newEmptyRef :: (Monad m, IsSyntaxExtension ext) => TypeRepr tp -> Generator ext s t ret m (Expr ext s (ReferenceType tp))
newEmptyRef :: forall (m :: Type -> Type) ext (tp :: CrucibleType) s
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
TypeRepr tp
-> Generator ext s t ret m (Expr ext s (ReferenceType tp))
newEmptyRef TypeRepr tp
tp =
  Atom s (ReferenceType tp) -> Expr ext s (ReferenceType tp)
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (Atom s (ReferenceType tp) -> Expr ext s (ReferenceType tp))
-> Generator ext s t ret m (Atom s (ReferenceType tp))
-> Generator ext s t ret m (Expr ext s (ReferenceType tp))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AtomValue ext s (ReferenceType tp)
-> Generator ext s t ret m (Atom s (ReferenceType tp))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (TypeRepr tp -> AtomValue ext s (ReferenceType tp)
forall (tp1 :: CrucibleType) ext s.
TypeRepr tp1 -> AtomValue ext s ('ReferenceType tp1)
NewEmptyRef TypeRepr tp
tp)

-- | Generate a new virtual register with the given initial value.
newReg :: (Monad m, IsSyntaxExtension ext) => Expr ext s tp -> Generator ext s t ret m (Reg s tp)
newReg :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Reg s tp)
newReg Expr ext s tp
e =
  do Reg s tp
r <- TypeRepr tp -> Generator ext s t ret m (Reg s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
       (t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (Reg s tp)
newUnassignedReg (Expr ext s tp -> TypeRepr tp
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s tp
e)
     Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()
assignReg Reg s tp
r Expr ext s tp
e
     Reg s tp -> Generator ext s t ret m (Reg s tp)
forall a. a -> Generator ext s t ret m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Reg s tp
r

-- | Produce a new virtual register without giving it an initial value.
--   NOTE! If you fail to initialize this register with a subsequent
--   call to @assignReg@, errors will arise during SSA conversion.
newUnassignedReg :: Monad m => TypeRepr tp -> Generator ext s t ret m (Reg s tp)
newUnassignedReg :: forall (m :: Type -> Type) (tp :: CrucibleType) ext s
       (t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (Reg s tp)
newUnassignedReg TypeRepr tp
tp =
  do Position
p <- Generator ext s t ret m Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Generator ext s t ret m Position
getPosition
     Nonce s tp
n <- Generator ext s t ret m (Nonce s tp)
forall {k} (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) (tp :: k).
Monad m =>
Generator ext s t ret m (Nonce s tp)
mkNonce
     Reg s tp -> Generator ext s t ret m (Reg s tp)
forall a. a -> Generator ext s t ret m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Reg s tp -> Generator ext s t ret m (Reg s tp))
-> Reg s tp -> Generator ext s t ret m (Reg s tp)
forall a b. (a -> b) -> a -> b
$! Reg { regPosition :: Position
regPosition = Position
p
                   , regId :: Nonce s tp
regId = Nonce s tp
n
                   , typeOfReg :: TypeRepr tp
typeOfReg = TypeRepr tp
tp
                   }

-- | Get the current value of a register.
readReg :: (Monad m, IsSyntaxExtension ext) => Reg s tp -> Generator ext s t ret m (Expr ext s tp)
readReg :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp -> Generator ext s t ret m (Expr ext s tp)
readReg Reg s tp
r = Atom s tp -> Expr ext s tp
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (Atom s tp -> Expr ext s tp)
-> Generator ext s t ret m (Atom s tp)
-> Generator ext s t ret m (Expr ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (Reg s tp -> AtomValue ext s tp
forall s (tp :: CrucibleType) ext. Reg s tp -> AtomValue ext s tp
ReadReg Reg s tp
r)

-- | Update the value of a register.
assignReg :: (Monad m, IsSyntaxExtension ext) => Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()
assignReg :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()
assignReg Reg s tp
r Expr ext s tp
e =
  do Atom s tp
a <- Expr ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s tp
e
     Stmt ext s -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (Reg s tp -> Atom s tp -> Stmt ext s
forall ext s (tp :: CrucibleType).
Reg s tp -> Atom s tp -> Stmt ext s
SetReg Reg s tp
r Atom s tp
a)

-- | Modify the value of a register.
modifyReg :: (Monad m, IsSyntaxExtension ext) => Reg s tp -> (Expr ext s tp -> Expr ext s tp) -> Generator ext s t ret m ()
modifyReg :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp
-> (Expr ext s tp -> Expr ext s tp) -> Generator ext s t ret m ()
modifyReg Reg s tp
r Expr ext s tp -> Expr ext s tp
f =
  do Expr ext s tp
v <- Reg s tp -> Generator ext s t ret m (Expr ext s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp -> Generator ext s t ret m (Expr ext s tp)
readReg Reg s tp
r
     Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()
assignReg Reg s tp
r (Expr ext s tp -> Generator ext s t ret m ())
-> Expr ext s tp -> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$! Expr ext s tp -> Expr ext s tp
f Expr ext s tp
v

-- | Modify the value of a register.
modifyRegM :: (Monad m, IsSyntaxExtension ext)
           => Reg s tp
           -> (Expr ext s tp -> Generator ext s t ret m (Expr ext s tp))
           -> Generator ext s t ret m ()
modifyRegM :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp
-> (Expr ext s tp -> Generator ext s t ret m (Expr ext s tp))
-> Generator ext s t ret m ()
modifyRegM Reg s tp
r Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
f =
  do Expr ext s tp
v <- Reg s tp -> Generator ext s t ret m (Expr ext s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp -> Generator ext s t ret m (Expr ext s tp)
readReg Reg s tp
r
     Expr ext s tp
v' <- Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
f Expr ext s tp
v
     Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp -> Expr ext s tp -> Generator ext s t ret m ()
assignReg Reg s tp
r Expr ext s tp
v'

-- | Add a statement to print a value.
addPrintStmt :: (Monad m, IsSyntaxExtension ext) => Expr ext s (StringType Unicode) -> Generator ext s t ret m ()
addPrintStmt :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m ()
addPrintStmt Expr ext s (StringType Unicode)
e =
  do Atom s (StringType Unicode)
e_a <- Expr ext s (StringType Unicode)
-> Generator ext s t ret m (Atom s (StringType Unicode))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (StringType Unicode)
e
     Stmt ext s -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (Atom s (StringType Unicode) -> Stmt ext s
forall ext s. Atom s (StringType Unicode) -> Stmt ext s
Print Atom s (StringType Unicode)
e_a)

-- | Add a breakpoint.
addBreakpointStmt ::
  (Monad m, IsSyntaxExtension ext) =>
  Text {- ^ breakpoint name -} ->
  Assignment (Value s) args {- ^ breakpoint values -} ->
  Generator ext s t r m ()
addBreakpointStmt :: forall (m :: Type -> Type) ext s (args :: Ctx CrucibleType)
       (t :: Type -> Type) (r :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Text -> Assignment (Value s) args -> Generator ext s t r m ()
addBreakpointStmt Text
nm Assignment (Value s) args
args = Stmt ext s -> Generator ext s t r m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (Stmt ext s -> Generator ext s t r m ())
-> Stmt ext s -> Generator ext s t r m ()
forall a b. (a -> b) -> a -> b
$ BreakpointName -> Assignment (Value s) args -> Stmt ext s
forall ext s (args :: Ctx CrucibleType).
BreakpointName -> Assignment (Value s) args -> Stmt ext s
Breakpoint (Text -> BreakpointName
BreakpointName Text
nm) Assignment (Value s) args
args

-- | Add an assert statement.
assertExpr ::
  (Monad m, IsSyntaxExtension ext) =>
  Expr ext s BoolType {- ^ assertion -} ->
  Expr ext s (StringType Unicode) {- ^ error message -} ->
  Generator ext s t ret m ()
assertExpr :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Expr ext s (StringType Unicode) -> Generator ext s t ret m ()
assertExpr Expr ext s BoolType
b Expr ext s (StringType Unicode)
e =
  do Atom s BoolType
b_a <- Expr ext s BoolType -> Generator ext s t ret m (Atom s BoolType)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s BoolType
b
     Atom s (StringType Unicode)
e_a <- Expr ext s (StringType Unicode)
-> Generator ext s t ret m (Atom s (StringType Unicode))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (StringType Unicode)
e
     Stmt ext s -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s
forall ext s.
Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s
Assert Atom s BoolType
b_a Atom s (StringType Unicode)
e_a)

-- | Add an assume statement.
assumeExpr ::
  (Monad m, IsSyntaxExtension ext) =>
  Expr ext s BoolType {- ^ assumption -} ->
  Expr ext s (StringType Unicode) {- ^ reason message -} ->
  Generator ext s t ret m ()
assumeExpr :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Expr ext s (StringType Unicode) -> Generator ext s t ret m ()
assumeExpr Expr ext s BoolType
b Expr ext s (StringType Unicode)
e =
  do Atom s BoolType
b_a <- Expr ext s BoolType -> Generator ext s t ret m (Atom s BoolType)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s BoolType
b
     Atom s (StringType Unicode)
m_a <- Expr ext s (StringType Unicode)
-> Generator ext s t ret m (Atom s (StringType Unicode))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (StringType Unicode)
e
     Stmt ext s -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Stmt ext s -> Generator ext s t ret m ()
addStmt (Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s
forall ext s.
Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s
Assume Atom s BoolType
b_a Atom s (StringType Unicode)
m_a)


-- | Stash the given CFG away for later retrieval.  This is primarily
--   used when translating inner and anonymous functions in the
--   context of an outer function.
recordCFG :: AnyCFG ext -> Generator ext s t ret m ()
recordCFG :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
AnyCFG ext -> Generator ext s t ret m ()
recordCFG AnyCFG ext
g = StateContT
  (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
  (EndState ext s t ret m)
  m
  ()
-> Generator ext s t ret m ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
   (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
   (EndState ext s t ret m)
   m
   ()
 -> Generator ext s t ret m ())
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     ()
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ ([AnyCFG ext] -> Identity [AnyCFG ext])
-> IxGeneratorState ext s t ret m (CurrentBlockState ext s)
-> Identity
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
([AnyCFG ext] -> f [AnyCFG ext])
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
seenFunctions (([AnyCFG ext] -> Identity [AnyCFG ext])
 -> IxGeneratorState ext s t ret m (CurrentBlockState ext s)
 -> Identity
      (IxGeneratorState ext s t ret m (CurrentBlockState ext s)))
-> ([AnyCFG ext] -> [AnyCFG ext])
-> StateContT
     (IxGeneratorState ext s t ret m (CurrentBlockState ext s))
     (EndState ext s t ret m)
     m
     ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (AnyCFG ext
gAnyCFG ext -> [AnyCFG ext] -> [AnyCFG ext]
forall a. a -> [a] -> [a]
:)

------------------------------------------------------------------------
-- Labels

-- | Create a new block label.
newLabel :: Monad m => Generator ext s t ret m (Label s)
newLabel :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel = Nonce s UnitType -> Label s
forall s. Nonce s UnitType -> Label s
Label (Nonce s UnitType -> Label s)
-> Generator ext s t ret m (Nonce s UnitType)
-> Generator ext s t ret m (Label s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Generator ext s t ret m (Nonce s UnitType)
forall {k} (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) (tp :: k).
Monad m =>
Generator ext s t ret m (Nonce s tp)
mkNonce

-- | Create a new lambda label.
newLambdaLabel :: Monad m => KnownRepr TypeRepr tp => Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel :: forall (m :: Type -> Type) (tp :: CrucibleType) ext s
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, KnownRepr TypeRepr tp) =>
Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel = TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
       (t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

-- | Create a new lambda label, using an explicit 'TypeRepr'.
newLambdaLabel' :: Monad m => TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' :: forall (m :: Type -> Type) (tp :: CrucibleType) ext s
       (t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' TypeRepr tp
tpr =
  do Position
p <- Generator ext s t ret m Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Generator ext s t ret m Position
getPosition
     Nonce s tp
idx <- Generator ext s t ret m (Nonce s tp)
forall {k} (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) (tp :: k).
Monad m =>
Generator ext s t ret m (Nonce s tp)
mkNonce
     Nonce s tp
i <- Generator ext s t ret m (Nonce s tp)
forall {k} (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) (tp :: k).
Monad m =>
Generator ext s t ret m (Nonce s tp)
mkNonce
     let lbl :: LambdaLabel s tp
lbl = Nonce s tp -> Atom s tp -> LambdaLabel s tp
forall s (tp :: CrucibleType).
Nonce s tp -> Atom s tp -> LambdaLabel s tp
LambdaLabel Nonce s tp
idx Atom s tp
a
         a :: Atom s tp
a = Atom { atomPosition :: Position
atomPosition = Position
p
                  , atomId :: Nonce s tp
atomId = Nonce s tp
i
                  , atomSource :: AtomSource s tp
atomSource = LambdaLabel s tp -> AtomSource s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> AtomSource s tp
LambdaArg LambdaLabel s tp
lbl
                  , typeOfAtom :: TypeRepr tp
typeOfAtom = TypeRepr tp
tpr
                  }
     LambdaLabel s tp -> Generator ext s t ret m (LambdaLabel s tp)
forall a. a -> Generator ext s t ret m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LambdaLabel s tp -> Generator ext s t ret m (LambdaLabel s tp))
-> LambdaLabel s tp -> Generator ext s t ret m (LambdaLabel s tp)
forall a b. (a -> b) -> a -> b
$! LambdaLabel s tp
lbl

-- | Return the label of the current basic block.
currentBlockID :: Generator ext s t ret m (BlockID s)
currentBlockID :: forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Generator ext s t ret m (BlockID s)
currentBlockID =
  StateContT
  (GeneratorState ext s t ret m)
  (EndState ext s t ret m)
  m
  (BlockID s)
-> Generator ext s t ret m (BlockID s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
   (GeneratorState ext s t ret m)
   (EndState ext s t ret m)
   m
   (BlockID s)
 -> Generator ext s t ret m (BlockID s))
-> StateContT
     (GeneratorState ext s t ret m)
     (EndState ext s t ret m)
     m
     (BlockID s)
-> Generator ext s t ret m (BlockID s)
forall a b. (a -> b) -> a -> b
$
  (\GeneratorState ext s t ret m
st -> GeneratorState ext s t ret m
st GeneratorState ext s t ret m
-> Getting
     (CurrentBlockState ext s)
     (GeneratorState ext s t ret m)
     (CurrentBlockState ext s)
-> CurrentBlockState ext s
forall s a. s -> Getting a s a -> a
^. Getting
  (CurrentBlockState ext s)
  (GeneratorState ext s t ret m)
  (CurrentBlockState ext s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent CurrentBlockState ext s
-> (CurrentBlockState ext s -> BlockID s) -> BlockID s
forall a b. a -> (a -> b) -> b
& CurrentBlockState ext s -> BlockID s
forall ext s. CurrentBlockState ext s -> BlockID s
cbsBlockID) (GeneratorState ext s t ret m -> BlockID s)
-> StateContT
     (GeneratorState ext s t ret m)
     (EndState ext s t ret m)
     m
     (GeneratorState ext s t ret m)
-> StateContT
     (GeneratorState ext s t ret m)
     (EndState ext s t ret m)
     m
     (BlockID s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> StateContT
  (GeneratorState ext s t ret m)
  (EndState ext s t ret m)
  m
  (GeneratorState ext s t ret m)
forall s (m :: Type -> Type). MonadState s m => m s
get

----------------------------------------------------------------------
-- Defining blocks

-- $define The block-defining commands should be used with a
-- 'Generator' action ending with a block-terminating statement, which
-- gives it a polymorphic type.

-- | End the translation of the current block, and then continue
-- generating a new block with the given label.
continue ::
  (Monad m, IsSyntaxExtension ext) =>
  Label s {- ^ label for new block -} ->
  (forall a. Generator ext s t ret m a) {- ^ action to end current block -} ->
  Generator ext s t ret m ()
continue :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
continue Label s
lbl forall a. Generator ext s t ret m a
action =
  StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
-> Generator ext s t ret m ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
   (GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
 -> Generator ext s t ret m ())
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ ((() -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
 -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((()
   -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
  -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
 -> StateContT
      (GeneratorState ext s t ret m) (EndState ext s t ret m) m ())
-> ((()
     -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
    -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
forall a b. (a -> b) -> a -> b
$ \() -> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
cont GeneratorState ext s t ret m
gs ->
  do EndState ext s t ret m
gs' <- Generator ext s t ret m Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Generator ext s t ret m Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
runGenerator Generator ext s t ret m Void
forall a. Generator ext s t ret m a
action GeneratorState ext s t ret m
gs
     () -> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
cont () (BlockID s -> EndState ext s t ret m -> GeneratorState ext s t ret m
forall s ext (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
BlockID s -> EndState ext s t ret m -> GeneratorState ext s t ret m
startBlock (Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
lbl) EndState ext s t ret m
gs')

-- | End the translation of the current block, and then continue
-- generating a new lambda block with the given label. The return
-- value is the argument to the lambda block.
continueLambda ::
  (Monad m, IsSyntaxExtension ext) =>
  LambdaLabel s tp {- ^ label for new block -} ->
  (forall a. Generator ext s t ret m a) {- ^ action to end current block -} ->
  Generator ext s t ret m (Expr ext s tp)
continueLambda :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s tp)
continueLambda LambdaLabel s tp
lbl forall a. Generator ext s t ret m a
action =
  StateContT
  (GeneratorState ext s t ret m)
  (EndState ext s t ret m)
  m
  (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
   (GeneratorState ext s t ret m)
   (EndState ext s t ret m)
   m
   (Expr ext s tp)
 -> Generator ext s t ret m (Expr ext s tp))
-> StateContT
     (GeneratorState ext s t ret m)
     (EndState ext s t ret m)
     m
     (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
forall a b. (a -> b) -> a -> b
$ ((Expr ext s tp
  -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
 -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
     (GeneratorState ext s t ret m)
     (EndState ext s t ret m)
     m
     (Expr ext s tp)
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((Expr ext s tp
   -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
  -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
 -> StateContT
      (GeneratorState ext s t ret m)
      (EndState ext s t ret m)
      m
      (Expr ext s tp))
-> ((Expr ext s tp
     -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
    -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
     (GeneratorState ext s t ret m)
     (EndState ext s t ret m)
     m
     (Expr ext s tp)
forall a b. (a -> b) -> a -> b
$ \Expr ext s tp
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
cont GeneratorState ext s t ret m
gs ->
  do EndState ext s t ret m
gs' <- Generator ext s t ret m Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Generator ext s t ret m Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
runGenerator Generator ext s t ret m Void
forall a. Generator ext s t ret m a
action GeneratorState ext s t ret m
gs
     Expr ext s tp
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
cont (Atom s tp -> Expr ext s tp
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (LambdaLabel s tp -> Atom s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Atom s tp
lambdaAtom LambdaLabel s tp
lbl)) (BlockID s -> EndState ext s t ret m -> GeneratorState ext s t ret m
forall s ext (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
BlockID s -> EndState ext s t ret m -> GeneratorState ext s t ret m
startBlock (LambdaLabel s tp -> BlockID s
forall s (tp :: CrucibleType). LambdaLabel s tp -> BlockID s
LambdaID LambdaLabel s tp
lbl) EndState ext s t ret m
gs')

defineSomeBlock ::
  (Monad m, IsSyntaxExtension ext) =>
  BlockID s ->
  Generator ext s t ret m Void ->
  Generator ext s t ret m ()
defineSomeBlock :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
BlockID s
-> Generator ext s t ret m Void -> Generator ext s t ret m ()
defineSomeBlock BlockID s
l Generator ext s t ret m Void
next =
  StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
-> Generator ext s t ret m ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
   (GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
 -> Generator ext s t ret m ())
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ ((() -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
 -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((()
   -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
  -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
 -> StateContT
      (GeneratorState ext s t ret m) (EndState ext s t ret m) m ())
-> ((()
     -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
    -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m ()
forall a b. (a -> b) -> a -> b
$ \() -> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
cont GeneratorState ext s t ret m
gs0 ->
  do let gs1 :: GeneratorState ext s t ret m
gs1 = BlockID s -> EndState ext s t ret m -> GeneratorState ext s t ret m
forall s ext (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
BlockID s -> EndState ext s t ret m -> GeneratorState ext s t ret m
startBlock BlockID s
l (GeneratorState ext s t ret m
gs0 GeneratorState ext s t ret m
-> (GeneratorState ext s t ret m -> EndState ext s t ret m)
-> EndState ext s t ret m
forall a b. a -> (a -> b) -> b
& (CurrentBlockState ext s -> Identity ())
-> GeneratorState ext s t ret m
-> Identity (EndState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent ((CurrentBlockState ext s -> Identity ())
 -> GeneratorState ext s t ret m
 -> Identity (EndState ext s t ret m))
-> () -> GeneratorState ext s t ret m -> EndState ext s t ret m
forall s t a b. ASetter s t a b -> b -> s -> t
.~ ())
     EndState ext s t ret m
gs2 <- Generator ext s t ret m Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Generator ext s t ret m Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
runGenerator Generator ext s t ret m Void
next GeneratorState ext s t ret m
gs1
     -- Reset current block and state.
     let gs3 :: GeneratorState ext s t ret m
gs3 = EndState ext s t ret m
gs2 EndState ext s t ret m
-> (EndState ext s t ret m -> EndState ext s t ret m)
-> EndState ext s t ret m
forall a b. a -> (a -> b) -> b
& (Position -> Identity Position)
-> EndState ext s t ret m -> Identity (EndState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Position -> f Position)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsPosition ((Position -> Identity Position)
 -> EndState ext s t ret m -> Identity (EndState ext s t ret m))
-> Position -> EndState ext s t ret m -> EndState ext s t ret m
forall s t a b. ASetter s t a b -> b -> s -> t
.~ GeneratorState ext s t ret m
gs0GeneratorState ext s t ret m
-> Getting Position (GeneratorState ext s t ret m) Position
-> Position
forall s a. s -> Getting a s a -> a
^.Getting Position (GeneratorState ext s t ret m) Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Position -> f Position)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsPosition
                   EndState ext s t ret m
-> (EndState ext s t ret m -> GeneratorState ext s t ret m)
-> GeneratorState ext s t ret m
forall a b. a -> (a -> b) -> b
& (() -> Identity (CurrentBlockState ext s))
-> EndState ext s t ret m
-> Identity (GeneratorState ext s t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent ((() -> Identity (CurrentBlockState ext s))
 -> EndState ext s t ret m
 -> Identity (GeneratorState ext s t ret m))
-> CurrentBlockState ext s
-> EndState ext s t ret m
-> GeneratorState ext s t ret m
forall s t a b. ASetter s t a b -> b -> s -> t
.~ GeneratorState ext s t ret m
gs0GeneratorState ext s t ret m
-> Getting
     (CurrentBlockState ext s)
     (GeneratorState ext s t ret m)
     (CurrentBlockState ext s)
-> CurrentBlockState ext s
forall s a. s -> Getting a s a -> a
^.Getting
  (CurrentBlockState ext s)
  (GeneratorState ext s t ret m)
  (CurrentBlockState ext s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i j (f :: Type -> Type).
Functor f =>
(i -> f j)
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m j)
gsCurrent
     () -> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
cont () GeneratorState ext s t ret m
gs3

-- | Define a block with an ordinary label.
defineBlock ::
  (Monad m, IsSyntaxExtension ext) =>
  Label s ->
  (forall a. Generator ext s t ret m a) ->
  Generator ext s t ret m ()
defineBlock :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineBlock Label s
l forall a. Generator ext s t ret m a
action =
  BlockID s
-> Generator ext s t ret m Void -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
BlockID s
-> Generator ext s t ret m Void -> Generator ext s t ret m ()
defineSomeBlock (Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
l) Generator ext s t ret m Void
forall a. Generator ext s t ret m a
action

-- | Define a block that has a lambda label.
defineLambdaBlock ::
  (Monad m, IsSyntaxExtension ext) =>
  LambdaLabel s tp ->
  (forall a. Expr ext s tp -> Generator ext s t ret m a) ->
  Generator ext s t ret m ()
defineLambdaBlock :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineLambdaBlock LambdaLabel s tp
l forall a. Expr ext s tp -> Generator ext s t ret m a
action =
  BlockID s
-> Generator ext s t ret m Void -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
BlockID s
-> Generator ext s t ret m Void -> Generator ext s t ret m ()
defineSomeBlock (LambdaLabel s tp -> BlockID s
forall s (tp :: CrucibleType). LambdaLabel s tp -> BlockID s
LambdaID LambdaLabel s tp
l) (Expr ext s tp -> Generator ext s t ret m Void
forall a. Expr ext s tp -> Generator ext s t ret m a
action (Atom s tp -> Expr ext s tp
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (LambdaLabel s tp -> Atom s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Atom s tp
lambdaAtom LambdaLabel s tp
l)))

-- | Define a block with a fresh label, returning the label.
defineBlockLabel ::
  (Monad m, IsSyntaxExtension ext) =>
  (forall a. Generator ext s t ret m a) ->
  Generator ext s t ret m (Label s)
defineBlockLabel :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel forall a. Generator ext s t ret m a
action =
  do Label s
l <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
     Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineBlock Label s
l Generator ext s t ret m a
forall a. Generator ext s t ret m a
action
     Label s -> Generator ext s t ret m (Label s)
forall a. a -> Generator ext s t ret m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Label s
l

------------------------------------------------------------------------
-- Generator interface

-- | Evaluate an expression to an 'AtomExpr', so that it can be reused multiple times later.
forceEvaluation :: (Monad m, IsSyntaxExtension ext) => Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
forceEvaluation :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
forceEvaluation Expr ext s tp
e = Atom s tp -> Expr ext s tp
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (Atom s tp -> Expr ext s tp)
-> Generator ext s t ret m (Atom s tp)
-> Generator ext s t ret m (Expr ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s tp
e

-- | Add a statement from the syntax extension to the current basic block.
extensionStmt ::
   (Monad m, IsSyntaxExtension ext) =>
   StmtExtension ext (Expr ext s) tp ->
   Generator ext s t ret m (Expr ext s tp)
extensionStmt :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt StmtExtension ext (Expr ext s) tp
stmt = do
   StmtExtension ext (Atom s) tp
stmt' <- (forall (x :: CrucibleType).
 Expr ext s x -> Generator ext s t ret m (Atom s x))
-> forall (x :: CrucibleType).
   StmtExtension ext (Expr ext s) x
   -> Generator ext s t ret m (StmtExtension ext (Atom s) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType).
   StmtExtension ext f x -> m (StmtExtension ext g x)
traverseFC Expr ext s x -> Generator ext s t ret m (Atom s x)
forall (x :: CrucibleType).
Expr ext s x -> Generator ext s t ret m (Atom s x)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom StmtExtension ext (Expr ext s) tp
stmt
   Atom s tp -> Expr ext s tp
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (Atom s tp -> Expr ext s tp)
-> Generator ext s t ret m (Atom s tp)
-> Generator ext s t ret m (Expr ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (StmtExtension ext (Atom s) tp -> AtomValue ext s tp
forall ext s (tp :: CrucibleType).
StmtExtension ext (Atom s) tp -> AtomValue ext s tp
EvalExt StmtExtension ext (Atom s) tp
stmt')

-- | Call a function.
call :: (Monad m, IsSyntaxExtension ext)
        => Expr ext s (FunctionHandleType args ret) {- ^ function to call -}
        -> Assignment (Expr ext s) args {- ^ function arguments -}
        -> Generator ext s t r m (Expr ext s ret)
call :: forall (m :: Type -> Type) ext s (args :: Ctx CrucibleType)
       (ret :: CrucibleType) (t :: Type -> Type) (r :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (FunctionHandleType args ret)
-> Assignment (Expr ext s) args
-> Generator ext s t r m (Expr ext s ret)
call Expr ext s (FunctionHandleType args ret)
h Assignment (Expr ext s) args
args = Atom s ret -> Expr ext s ret
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (Atom s ret -> Expr ext s ret)
-> Generator ext s t r m (Atom s ret)
-> Generator ext s t r m (Expr ext s ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr ext s (FunctionHandleType args ret)
-> Assignment (Expr ext s) args
-> Generator ext s t r m (Atom s ret)
forall (m :: Type -> Type) ext s (args :: Ctx CrucibleType)
       (ret :: CrucibleType) (t :: Type -> Type) (r :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (FunctionHandleType args ret)
-> Assignment (Expr ext s) args
-> Generator ext s t r m (Atom s ret)
call' Expr ext s (FunctionHandleType args ret)
h Assignment (Expr ext s) args
args

-- | Call a function.
call' :: (Monad m, IsSyntaxExtension ext)
        => Expr ext s (FunctionHandleType args ret)
        -> Assignment (Expr ext s) args
        -> Generator ext s t r m (Atom s ret)
call' :: forall (m :: Type -> Type) ext s (args :: Ctx CrucibleType)
       (ret :: CrucibleType) (t :: Type -> Type) (r :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (FunctionHandleType args ret)
-> Assignment (Expr ext s) args
-> Generator ext s t r m (Atom s ret)
call' Expr ext s (FunctionHandleType args ret)
h Assignment (Expr ext s) args
args = do
  case Expr ext s (FunctionHandleType args ret)
-> TypeRepr (FunctionHandleType args ret)
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s (FunctionHandleType args ret)
h of
    FunctionHandleRepr CtxRepr ctx
_ TypeRepr ret
retType -> do
      Atom s (FunctionHandleType args ret)
h_a <- Expr ext s (FunctionHandleType args ret)
-> Generator ext s t r m (Atom s (FunctionHandleType args ret))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (FunctionHandleType args ret)
h
      Assignment (Atom s) args
args_a <- (forall (x :: CrucibleType).
 Expr ext s x -> Generator ext s t r m (Atom s x))
-> forall (x :: Ctx CrucibleType).
   Assignment (Expr ext s) x
   -> Generator ext s t r m (Assignment (Atom s) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
   Assignment f x -> m (Assignment g x)
traverseFC Expr ext s x -> Generator ext s t r m (Atom s x)
forall (x :: CrucibleType).
Expr ext s x -> Generator ext s t r m (Atom s x)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Assignment (Expr ext s) args
args
      AtomValue ext s ret -> Generator ext s t r m (Atom s ret)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
AtomValue ext s tp -> Generator ext s t ret m (Atom s tp)
freshAtom (AtomValue ext s ret -> Generator ext s t r m (Atom s ret))
-> AtomValue ext s ret -> Generator ext s t r m (Atom s ret)
forall a b. (a -> b) -> a -> b
$ Atom s (FunctionHandleType args ret)
-> Assignment (Atom s) args -> TypeRepr ret -> AtomValue ext s ret
forall s (args :: Ctx CrucibleType) (tp :: CrucibleType) ext.
Atom s (FunctionHandleType args tp)
-> Assignment (Atom s) args -> TypeRepr tp -> AtomValue ext s tp
Call Atom s (FunctionHandleType args ret)
h_a Assignment (Atom s) args
args_a TypeRepr ret
TypeRepr ret
retType

----------------------------------------------------------------------
-- Block-terminating statements

-- $termstmt The following operations produce block-terminating
-- statements, and have early termination behavior in the 'Generator'
-- monad: Like 'fail', they have polymorphic return types and cause
-- any following monadic actions to be skipped.

-- | End the current block with the given terminal statement, and skip
-- the rest of the 'Generator' computation.
terminateEarly ::
  (Monad m, IsSyntaxExtension ext) => TermStmt s ret -> Generator ext s t ret m a
terminateEarly :: forall (m :: Type -> Type) ext s (ret :: CrucibleType)
       (t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly TermStmt s ret
term =
  StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) a.
StateContT
  (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
Generator (StateContT
   (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
 -> Generator ext s t ret m a)
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
-> Generator ext s t ret m a
forall a b. (a -> b) -> a -> b
$ ((a -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
 -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
forall s r (m :: Type -> Type) a.
((a -> s -> m r) -> s -> m r) -> StateContT s r m a
StateContT (((a -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
  -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
 -> StateContT
      (GeneratorState ext s t ret m) (EndState ext s t ret m) m a)
-> ((a
     -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
    -> GeneratorState ext s t ret m -> m (EndState ext s t ret m))
-> StateContT
     (GeneratorState ext s t ret m) (EndState ext s t ret m) m a
forall a b. (a -> b) -> a -> b
$ \a -> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
_cont GeneratorState ext s t ret m
gs ->
  EndState ext s t ret m -> m (EndState ext s t ret m)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (TermStmt s ret
-> GeneratorState ext s t ret m -> EndState ext s t ret m
forall ext s (ret :: CrucibleType) (t :: Type -> Type)
       (m :: Type -> Type).
IsSyntaxExtension ext =>
TermStmt s ret
-> GeneratorState ext s t ret m -> EndState ext s t ret m
terminateBlock TermStmt s ret
term GeneratorState ext s t ret m
gs)

-- | Jump to the given label.
jump :: (Monad m, IsSyntaxExtension ext) => Label s -> Generator ext s t ret m a
jump :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
l = TermStmt s ret -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
       (t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly (Label s -> TermStmt s ret
forall s (ret :: CrucibleType). Label s -> TermStmt s ret
Jump Label s
l)

-- | Jump to the given label with output.
jumpToLambda ::
  (Monad m, IsSyntaxExtension ext) =>
  LambdaLabel s tp ->
  Expr ext s tp ->
  Generator ext s t ret m a
jumpToLambda :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
jumpToLambda LambdaLabel s tp
lbl Expr ext s tp
v = do
  Atom s tp
v_a <- Expr ext s tp -> Generator ext s t ret m (Atom s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s tp
v
  TermStmt s ret -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
       (t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly (LambdaLabel s tp -> Atom s tp -> TermStmt s ret
forall s (tp :: CrucibleType) (ret :: CrucibleType).
LambdaLabel s tp -> Atom s tp -> TermStmt s ret
Output LambdaLabel s tp
lbl Atom s tp
v_a)

-- | Branch between blocks.
branch ::
  (Monad m, IsSyntaxExtension ext) =>
  Expr ext s BoolType {- ^ condition -} ->
  Label s             {- ^ true label -} ->
  Label s             {- ^ false label -} ->
  Generator ext s t ret m a
branch :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
branch (App (Not Expr ext s BoolType
e)) Label s
x_id Label s
y_id = do
  Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
branch Expr ext s BoolType
e Label s
y_id Label s
x_id
branch Expr ext s BoolType
e Label s
x_id Label s
y_id = do
  Atom s BoolType
a <- Expr ext s BoolType -> Generator ext s t ret m (Atom s BoolType)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s BoolType
e
  TermStmt s ret -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
       (t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly (Atom s BoolType -> Label s -> Label s -> TermStmt s ret
forall s (ret :: CrucibleType).
Atom s BoolType -> Label s -> Label s -> TermStmt s ret
Br Atom s BoolType
a Label s
x_id Label s
y_id)

-- | Return from this function with the given return value.
returnFromFunction ::
  (Monad m, IsSyntaxExtension ext) =>
  Expr ext s ret -> Generator ext s t ret m a
returnFromFunction :: forall (m :: Type -> Type) ext s (ret :: CrucibleType)
       (t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s ret -> Generator ext s t ret m a
returnFromFunction Expr ext s ret
e = do
  Atom s ret
e_a <- Expr ext s ret -> Generator ext s t ret m (Atom s ret)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s ret
e
  TermStmt s ret -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
       (t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly (Atom s ret -> TermStmt s ret
forall s (ret :: CrucibleType). Atom s ret -> TermStmt s ret
Return Atom s ret
e_a)

-- | Report an error message.
reportError ::
  (Monad m, IsSyntaxExtension ext) =>
  Expr ext s (StringType Unicode) -> Generator ext s t ret m a
reportError :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m a
reportError Expr ext s (StringType Unicode)
e = do
  Atom s (StringType Unicode)
e_a <- Expr ext s (StringType Unicode)
-> Generator ext s t ret m (Atom s (StringType Unicode))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (StringType Unicode)
e
  TermStmt s ret -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
       (t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly (Atom s (StringType Unicode) -> TermStmt s ret
forall s (ret :: CrucibleType).
Atom s (StringType Unicode) -> TermStmt s ret
ErrorStmt Atom s (StringType Unicode)
e_a)

-- | Branch between blocks based on a @Maybe@ value.
branchMaybe ::
  (Monad m, IsSyntaxExtension ext) =>
  Expr ext s (MaybeType tp) ->
  LambdaLabel s tp {- ^ label for @Just@ -} ->
  Label s          {- ^ label for @Nothing@ -} ->
  Generator ext s t ret m a
branchMaybe :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp)
-> LambdaLabel s tp -> Label s -> Generator ext s t ret m a
branchMaybe Expr ext s (MaybeType tp)
v LambdaLabel s tp
l1 Label s
l2 =
  case Expr ext s (MaybeType tp) -> TypeRepr (MaybeType tp)
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s (MaybeType tp)
v of
    MaybeRepr TypeRepr tp1
etp ->
      do Atom s (MaybeType tp)
v_a <- Expr ext s (MaybeType tp)
-> Generator ext s t ret m (Atom s (MaybeType tp))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (MaybeType tp)
v
         TermStmt s ret -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
       (t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly (TypeRepr tp1
-> Atom s ('MaybeType tp1)
-> LambdaLabel s tp1
-> Label s
-> TermStmt s ret
forall (tp :: CrucibleType) s (ret :: CrucibleType).
TypeRepr tp
-> Atom s (MaybeType tp)
-> LambdaLabel s tp
-> Label s
-> TermStmt s ret
MaybeBranch TypeRepr tp1
etp Atom s (MaybeType tp)
Atom s ('MaybeType tp1)
v_a LambdaLabel s tp
LambdaLabel s tp1
l1 Label s
l2)

-- | Switch on a variant value. Examine the tag of the variant and
-- jump to the appropriate switch target.
branchVariant ::
  (Monad m, IsSyntaxExtension ext) =>
  Expr ext s (VariantType varctx) {- ^ value to scrutinize -} ->
  Assignment (LambdaLabel s) varctx {- ^ target labels -} ->
  Generator ext s t ret m a
branchVariant :: forall (m :: Type -> Type) ext s (varctx :: Ctx CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (VariantType varctx)
-> Assignment (LambdaLabel s) varctx -> Generator ext s t ret m a
branchVariant Expr ext s (VariantType varctx)
v Assignment (LambdaLabel s) varctx
lbls =
  case Expr ext s (VariantType varctx) -> TypeRepr (VariantType varctx)
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s (VariantType varctx)
v of
    VariantRepr CtxRepr ctx
typs ->
      do Atom s (VariantType varctx)
v_a <- Expr ext s (VariantType varctx)
-> Generator ext s t ret m (Atom s (VariantType varctx))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (VariantType varctx)
v
         TermStmt s ret -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
       (t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly (CtxRepr ctx
-> Atom s ('VariantType ctx)
-> Assignment (LambdaLabel s) ctx
-> TermStmt s ret
forall (varctx :: Ctx CrucibleType) s (ret :: CrucibleType).
CtxRepr varctx
-> Atom s (VariantType varctx)
-> Assignment (LambdaLabel s) varctx
-> TermStmt s ret
VariantElim CtxRepr ctx
typs Atom s (VariantType varctx)
Atom s ('VariantType ctx)
v_a Assignment (LambdaLabel s) varctx
Assignment (LambdaLabel s) ctx
lbls)

-- | End a block with a tail call to a function.
tailCall ::
  (Monad m, IsSyntaxExtension ext) =>
  Expr ext s (FunctionHandleType args ret) {- ^ function to call -} ->
  Assignment (Expr ext s) args {- ^ function arguments -} ->
  Generator ext s t ret m a
tailCall :: forall (m :: Type -> Type) ext s (args :: Ctx CrucibleType)
       (ret :: CrucibleType) (t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (FunctionHandleType args ret)
-> Assignment (Expr ext s) args -> Generator ext s t ret m a
tailCall Expr ext s (FunctionHandleType args ret)
h Assignment (Expr ext s) args
args =
  case Expr ext s (FunctionHandleType args ret)
-> TypeRepr (FunctionHandleType args ret)
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s (FunctionHandleType args ret)
h of
    FunctionHandleRepr CtxRepr ctx
argTypes TypeRepr ret
_retType ->
      do Atom s (FunctionHandleType args ret)
h_a <- Expr ext s (FunctionHandleType args ret)
-> Generator ext s t ret m (Atom s (FunctionHandleType args ret))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Expr ext s (FunctionHandleType args ret)
h
         Assignment (Atom s) args
args_a <- (forall (x :: CrucibleType).
 Expr ext s x -> Generator ext s t ret m (Atom s x))
-> forall (x :: Ctx CrucibleType).
   Assignment (Expr ext s) x
   -> Generator ext s t ret m (Assignment (Atom s) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
   Assignment f x -> m (Assignment g x)
traverseFC Expr ext s x -> Generator ext s t ret m (Atom s x)
forall (x :: CrucibleType).
Expr ext s x -> Generator ext s t ret m (Atom s x)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Atom s tp)
mkAtom Assignment (Expr ext s) args
args
         TermStmt s ret -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
       (t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
TermStmt s ret -> Generator ext s t ret m a
terminateEarly (Atom s (FunctionHandleType args ret)
-> CtxRepr args -> Assignment (Atom s) args -> TermStmt s ret
forall s (args :: Ctx CrucibleType) (ret :: CrucibleType).
Atom s (FunctionHandleType args ret)
-> CtxRepr args -> Assignment (Atom s) args -> TermStmt s ret
TailCall Atom s (FunctionHandleType args ret)
h_a CtxRepr args
CtxRepr ctx
argTypes Assignment (Atom s) args
args_a)

------------------------------------------------------------------------
-- Combinators

-- | Expression-level if-then-else.
ifte :: (Monad m, IsSyntaxExtension ext, KnownRepr TypeRepr tp)
     => Expr ext s BoolType
     -> Generator ext s t ret m (Expr ext s tp) -- ^ true branch
     -> Generator ext s t ret m (Expr ext s tp) -- ^ false branch
     -> Generator ext s t ret m (Expr ext s tp)
ifte :: forall (m :: Type -> Type) ext (tp :: CrucibleType) s
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext, KnownRepr TypeRepr tp) =>
Expr ext s BoolType
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
ifte Expr ext s BoolType
e Generator ext s t ret m (Expr ext s tp)
x Generator ext s t ret m (Expr ext s tp)
y = do
  LambdaLabel s tp
c_id <- Generator ext s t ret m (LambdaLabel s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, KnownRepr TypeRepr tp) =>
Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel
  Label s
x_id <- (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel ((forall a. Generator ext s t ret m a)
 -> Generator ext s t ret m (Label s))
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall a b. (a -> b) -> a -> b
$ Generator ext s t ret m (Expr ext s tp)
x Generator ext s t ret m (Expr ext s tp)
-> (Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> (a -> Generator ext s t ret m b) -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
jumpToLambda LambdaLabel s tp
c_id
  Label s
y_id <- (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel ((forall a. Generator ext s t ret m a)
 -> Generator ext s t ret m (Label s))
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall a b. (a -> b) -> a -> b
$ Generator ext s t ret m (Expr ext s tp)
y Generator ext s t ret m (Expr ext s tp)
-> (Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> (a -> Generator ext s t ret m b) -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
jumpToLambda LambdaLabel s tp
c_id
  LambdaLabel s tp
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s tp)
continueLambda LambdaLabel s tp
c_id (Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
branch Expr ext s BoolType
e Label s
x_id Label s
y_id)

ifte' :: (Monad m, IsSyntaxExtension ext)
      => TypeRepr tp
      -> Expr ext s BoolType
      -> Generator ext s t ret m (Expr ext s tp) -- ^ true branch
      -> Generator ext s t ret m (Expr ext s tp) -- ^ false branch
      -> Generator ext s t ret m (Expr ext s tp)
ifte' :: forall (m :: Type -> Type) ext (tp :: CrucibleType) s
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
TypeRepr tp
-> Expr ext s BoolType
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
ifte' TypeRepr tp
repr Expr ext s BoolType
e Generator ext s t ret m (Expr ext s tp)
x Generator ext s t ret m (Expr ext s tp)
y = do
  LambdaLabel s tp
c_id <- TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
       (t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' TypeRepr tp
repr
  Label s
x_id <- (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel ((forall a. Generator ext s t ret m a)
 -> Generator ext s t ret m (Label s))
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall a b. (a -> b) -> a -> b
$ Generator ext s t ret m (Expr ext s tp)
x Generator ext s t ret m (Expr ext s tp)
-> (Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> (a -> Generator ext s t ret m b) -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
jumpToLambda LambdaLabel s tp
c_id
  Label s
y_id <- (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel ((forall a. Generator ext s t ret m a)
 -> Generator ext s t ret m (Label s))
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall a b. (a -> b) -> a -> b
$ Generator ext s t ret m (Expr ext s tp)
y Generator ext s t ret m (Expr ext s tp)
-> (Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> (a -> Generator ext s t ret m b) -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
jumpToLambda LambdaLabel s tp
c_id
  LambdaLabel s tp
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s tp)
continueLambda LambdaLabel s tp
c_id (Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
branch Expr ext s BoolType
e Label s
x_id Label s
y_id)

-- | Statement-level if-then-else.
ifte_ :: (Monad m, IsSyntaxExtension ext)
      => Expr ext s BoolType
      -> Generator ext s t ret m () -- ^ true branch
      -> Generator ext s t ret m () -- ^ false branch
      -> Generator ext s t ret m ()
ifte_ :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Generator ext s t ret m ()
-> Generator ext s t ret m ()
-> Generator ext s t ret m ()
ifte_ Expr ext s BoolType
e Generator ext s t ret m ()
x Generator ext s t ret m ()
y = do
  Label s
c_id <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
  Label s
x_id <- (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel ((forall a. Generator ext s t ret m a)
 -> Generator ext s t ret m (Label s))
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall a b. (a -> b) -> a -> b
$ Generator ext s t ret m ()
x Generator ext s t ret m ()
-> Generator ext s t ret m a -> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
c_id
  Label s
y_id <- (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel ((forall a. Generator ext s t ret m a)
 -> Generator ext s t ret m (Label s))
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall a b. (a -> b) -> a -> b
$ Generator ext s t ret m ()
y Generator ext s t ret m ()
-> Generator ext s t ret m a -> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
c_id
  Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
continue Label s
c_id (Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
branch Expr ext s BoolType
e Label s
x_id Label s
y_id)

-- | Expression-level if-then-else with a monadic condition.
ifteM :: (Monad m, IsSyntaxExtension ext, KnownRepr TypeRepr tp)
     => Generator ext s t ret m (Expr ext s BoolType)
     -> Generator ext s t ret m (Expr ext s tp) -- ^ true branch
     -> Generator ext s t ret m (Expr ext s tp) -- ^ false branch
     -> Generator ext s t ret m (Expr ext s tp)
ifteM :: forall (m :: Type -> Type) ext (tp :: CrucibleType) s
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext, KnownRepr TypeRepr tp) =>
Generator ext s t ret m (Expr ext s BoolType)
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
ifteM Generator ext s t ret m (Expr ext s BoolType)
em Generator ext s t ret m (Expr ext s tp)
x Generator ext s t ret m (Expr ext s tp)
y = do { Expr ext s BoolType
m <- Generator ext s t ret m (Expr ext s BoolType)
em; Expr ext s BoolType
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
forall (m :: Type -> Type) ext (tp :: CrucibleType) s
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext, KnownRepr TypeRepr tp) =>
Expr ext s BoolType
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
-> Generator ext s t ret m (Expr ext s tp)
ifte Expr ext s BoolType
m Generator ext s t ret m (Expr ext s tp)
x Generator ext s t ret m (Expr ext s tp)
y }

-- | Run a computation when a condition is true.
whenCond :: (Monad m, IsSyntaxExtension ext)
         => Expr ext s BoolType
         -> Generator ext s t ret m ()
         -> Generator ext s t ret m ()
whenCond :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Generator ext s t ret m () -> Generator ext s t ret m ()
whenCond Expr ext s BoolType
e Generator ext s t ret m ()
x = do
  Label s
c_id <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
  Label s
t_id <- (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel ((forall a. Generator ext s t ret m a)
 -> Generator ext s t ret m (Label s))
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall a b. (a -> b) -> a -> b
$ Generator ext s t ret m ()
x Generator ext s t ret m ()
-> Generator ext s t ret m a -> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
c_id
  Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
continue Label s
c_id (Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
branch Expr ext s BoolType
e Label s
t_id Label s
c_id)

-- | Run a computation when a condition is false.
unlessCond :: (Monad m, IsSyntaxExtension ext)
           => Expr ext s BoolType
           -> Generator ext s t ret m ()
           -> Generator ext s t ret m ()
unlessCond :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Generator ext s t ret m () -> Generator ext s t ret m ()
unlessCond Expr ext s BoolType
e Generator ext s t ret m ()
x = do
  Label s
c_id <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
  Label s
f_id <- (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
defineBlockLabel ((forall a. Generator ext s t ret m a)
 -> Generator ext s t ret m (Label s))
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Label s)
forall a b. (a -> b) -> a -> b
$ Generator ext s t ret m ()
x Generator ext s t ret m ()
-> Generator ext s t ret m a -> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
c_id
  Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
continue Label s
c_id (Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
branch Expr ext s BoolType
e Label s
c_id Label s
f_id)

data MatchMaybe j r
   = MatchMaybe
   { forall j r. MatchMaybe j r -> j -> r
onJust :: j -> r
   , forall j r. MatchMaybe j r -> r
onNothing :: r
   }

-- | Compute an expression by cases over a @Maybe@ value.
caseMaybe :: (Monad m, IsSyntaxExtension ext)
          => Expr ext s (MaybeType tp) {- ^ expression to scrutinize -}
          -> TypeRepr r {- ^ result type -}
          -> MatchMaybe (Expr ext s tp) (Generator ext s t ret m (Expr ext s r)) {- ^ case branches -}
          -> Generator ext s t ret m (Expr ext s r)
caseMaybe :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (r :: CrucibleType) (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp)
-> TypeRepr r
-> MatchMaybe
     (Expr ext s tp) (Generator ext s t ret m (Expr ext s r))
-> Generator ext s t ret m (Expr ext s r)
caseMaybe Expr ext s (MaybeType tp)
v TypeRepr r
retType MatchMaybe (Expr ext s tp) (Generator ext s t ret m (Expr ext s r))
cases = do
  let etp :: TypeRepr tp
etp = case Expr ext s (MaybeType tp) -> TypeRepr (MaybeType tp)
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s (MaybeType tp)
v of
              MaybeRepr TypeRepr tp1
etp' -> TypeRepr tp
TypeRepr tp1
etp'
  LambdaLabel s tp
j_id <- TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
       (t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' TypeRepr tp
etp
  Label s
n_id <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
  LambdaLabel s r
c_id <- TypeRepr r -> Generator ext s t ret m (LambdaLabel s r)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
       (t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' TypeRepr r
retType
  LambdaLabel s tp
-> (forall {a}. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineLambdaBlock LambdaLabel s tp
j_id ((forall {a}. Expr ext s tp -> Generator ext s t ret m a)
 -> Generator ext s t ret m ())
-> (forall {a}. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ MatchMaybe (Expr ext s tp) (Generator ext s t ret m (Expr ext s r))
-> Expr ext s tp -> Generator ext s t ret m (Expr ext s r)
forall j r. MatchMaybe j r -> j -> r
onJust MatchMaybe (Expr ext s tp) (Generator ext s t ret m (Expr ext s r))
cases (Expr ext s tp -> Generator ext s t ret m (Expr ext s r))
-> (Expr ext s r -> Generator ext s t ret m a)
-> Expr ext s tp
-> Generator ext s t ret m a
forall (m :: Type -> Type) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> LambdaLabel s r -> Expr ext s r -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
jumpToLambda LambdaLabel s r
c_id
  Label s
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineBlock       Label s
n_id ((forall {a}. Generator ext s t ret m a)
 -> Generator ext s t ret m ())
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ MatchMaybe (Expr ext s tp) (Generator ext s t ret m (Expr ext s r))
-> Generator ext s t ret m (Expr ext s r)
forall j r. MatchMaybe j r -> r
onNothing MatchMaybe (Expr ext s tp) (Generator ext s t ret m (Expr ext s r))
cases Generator ext s t ret m (Expr ext s r)
-> (Expr ext s r -> Generator ext s t ret m a)
-> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> (a -> Generator ext s t ret m b) -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= LambdaLabel s r -> Expr ext s r -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
jumpToLambda LambdaLabel s r
c_id
  LambdaLabel s r
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s r)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s tp)
continueLambda LambdaLabel s r
c_id (Expr ext s (MaybeType tp)
-> LambdaLabel s tp -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp)
-> LambdaLabel s tp -> Label s -> Generator ext s t ret m a
branchMaybe Expr ext s (MaybeType tp)
v LambdaLabel s tp
j_id Label s
n_id)

-- | Evaluate different statements by cases over a @Maybe@ value.
caseMaybe_ :: (Monad m, IsSyntaxExtension ext)
           => Expr ext s (MaybeType tp) {- ^ expression to scrutinize -}
           -> MatchMaybe (Expr ext s tp) (Generator ext s t ret m ()) {- ^ case branches -}
           -> Generator ext s t ret m ()
caseMaybe_ :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp)
-> MatchMaybe (Expr ext s tp) (Generator ext s t ret m ())
-> Generator ext s t ret m ()
caseMaybe_ Expr ext s (MaybeType tp)
v MatchMaybe (Expr ext s tp) (Generator ext s t ret m ())
cases = do
  let etp :: TypeRepr tp
etp = case Expr ext s (MaybeType tp) -> TypeRepr (MaybeType tp)
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s (MaybeType tp)
v of
              MaybeRepr TypeRepr tp1
etp' -> TypeRepr tp
TypeRepr tp1
etp'
  LambdaLabel s tp
j_id <- TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
       (t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' TypeRepr tp
etp
  Label s
n_id <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
  Label s
c_id <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
  LambdaLabel s tp
-> (forall {a}. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineLambdaBlock LambdaLabel s tp
j_id ((forall {a}. Expr ext s tp -> Generator ext s t ret m a)
 -> Generator ext s t ret m ())
-> (forall {a}. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ \Expr ext s tp
e -> MatchMaybe (Expr ext s tp) (Generator ext s t ret m ())
-> Expr ext s tp -> Generator ext s t ret m ()
forall j r. MatchMaybe j r -> j -> r
onJust MatchMaybe (Expr ext s tp) (Generator ext s t ret m ())
cases Expr ext s tp
e Generator ext s t ret m ()
-> Generator ext s t ret m a -> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
c_id
  Label s
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineBlock       Label s
n_id ((forall {a}. Generator ext s t ret m a)
 -> Generator ext s t ret m ())
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ MatchMaybe (Expr ext s tp) (Generator ext s t ret m ())
-> Generator ext s t ret m ()
forall j r. MatchMaybe j r -> r
onNothing MatchMaybe (Expr ext s tp) (Generator ext s t ret m ())
cases Generator ext s t ret m ()
-> Generator ext s t ret m a -> Generator ext s t ret m a
forall a b.
Generator ext s t ret m a
-> Generator ext s t ret m b -> Generator ext s t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
c_id
  Label s
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
continue Label s
c_id (Expr ext s (MaybeType tp)
-> LambdaLabel s tp -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp)
-> LambdaLabel s tp -> Label s -> Generator ext s t ret m a
branchMaybe Expr ext s (MaybeType tp)
v LambdaLabel s tp
j_id Label s
n_id)

-- | Return the argument of a @Just@ value, or call 'reportError' if
-- the value is @Nothing@.
fromJustExpr :: (Monad m, IsSyntaxExtension ext)
             => Expr ext s (MaybeType tp)
             -> Expr ext s (StringType Unicode) {- ^ error message -}
             -> Generator ext s t ret m (Expr ext s tp)
fromJustExpr :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp)
-> Expr ext s (StringType Unicode)
-> Generator ext s t ret m (Expr ext s tp)
fromJustExpr Expr ext s (MaybeType tp)
e Expr ext s (StringType Unicode)
msg = do
  let etp :: TypeRepr tp
etp = case Expr ext s (MaybeType tp) -> TypeRepr (MaybeType tp)
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s (MaybeType tp)
e of
              MaybeRepr TypeRepr tp1
etp' -> TypeRepr tp
TypeRepr tp1
etp'
  LambdaLabel s tp
j_id <- TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
       (t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' TypeRepr tp
etp
  Label s
n_id <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
  LambdaLabel s tp
c_id <- TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
       (t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (LambdaLabel s tp)
newLambdaLabel' TypeRepr tp
etp
  LambdaLabel s tp
-> (forall {a}. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineLambdaBlock LambdaLabel s tp
j_id ((forall {a}. Expr ext s tp -> Generator ext s t ret m a)
 -> Generator ext s t ret m ())
-> (forall {a}. Expr ext s tp -> Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp -> Expr ext s tp -> Generator ext s t ret m a
jumpToLambda LambdaLabel s tp
c_id
  Label s
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineBlock       Label s
n_id ((forall {a}. Generator ext s t ret m a)
 -> Generator ext s t ret m ())
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ Expr ext s (StringType Unicode) -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m a
reportError Expr ext s (StringType Unicode)
msg
  LambdaLabel s tp
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
LambdaLabel s tp
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m (Expr ext s tp)
continueLambda LambdaLabel s tp
c_id (Expr ext s (MaybeType tp)
-> LambdaLabel s tp -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp)
-> LambdaLabel s tp -> Label s -> Generator ext s t ret m a
branchMaybe Expr ext s (MaybeType tp)
e LambdaLabel s tp
j_id Label s
n_id)

-- | This asserts that the value in the expression is a @Just@ value, and
-- returns the underlying value.
assertedJustExpr :: (Monad m, IsSyntaxExtension ext)
                 => Expr ext s (MaybeType tp)
                 -> Expr ext s (StringType Unicode) {- ^ error message -}
                 -> Generator ext s t ret m (Expr ext s tp)
assertedJustExpr :: forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (MaybeType tp)
-> Expr ext s (StringType Unicode)
-> Generator ext s t ret m (Expr ext s tp)
assertedJustExpr Expr ext s (MaybeType tp)
e Expr ext s (StringType Unicode)
msg =
  case Expr ext s (MaybeType tp) -> TypeRepr (MaybeType tp)
forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType Expr ext s (MaybeType tp)
e of
    MaybeRepr TypeRepr tp1
tp ->
      Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
forceEvaluation (Expr ext s tp -> Generator ext s t ret m (Expr ext s tp))
-> Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
forall a b. (a -> b) -> a -> b
$! App ext (Expr ext s) tp -> Expr ext s tp
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (TypeRepr tp
-> Expr ext s (MaybeType tp)
-> Expr ext s (StringType Unicode)
-> App ext (Expr ext s) tp
forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext.
TypeRepr tp
-> f (MaybeType tp) -> f (StringType Unicode) -> App ext f tp
FromJustValue TypeRepr tp
TypeRepr tp1
tp Expr ext s (MaybeType tp)
e Expr ext s (StringType Unicode)
msg)

-- | Execute the loop body as long as the test condition is true.
while :: (Monad m, IsSyntaxExtension ext)
      => (Position, Generator ext s t ret m (Expr ext s BoolType)) {- ^ test condition -}
      -> (Position, Generator ext s t ret m ()) {- ^ loop body -}
      -> Generator ext s t ret m ()
while :: forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
(Position, Generator ext s t ret m (Expr ext s BoolType))
-> (Position, Generator ext s t ret m ())
-> Generator ext s t ret m ()
while (Position
pcond,Generator ext s t ret m (Expr ext s BoolType)
cond) (Position
pbody,Generator ext s t ret m ()
body) = do
  Label s
cond_lbl <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
  Label s
loop_lbl <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel
  Label s
exit_lbl <- Generator ext s t ret m (Label s)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
Monad m =>
Generator ext s t ret m (Label s)
newLabel

  Position
-> Generator ext s t ret m () -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
Monad m =>
Position -> Generator ext s t ret m a -> Generator ext s t ret m a
withPosition Position
pcond (Generator ext s t ret m () -> Generator ext s t ret m ())
-> Generator ext s t ret m () -> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$
    Label s
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineBlock Label s
cond_lbl ((forall {a}. Generator ext s t ret m a)
 -> Generator ext s t ret m ())
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ do
      Expr ext s BoolType
b <- Generator ext s t ret m (Expr ext s BoolType)
cond
      Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Label s -> Label s -> Generator ext s t ret m a
branch Expr ext s BoolType
b Label s
loop_lbl Label s
exit_lbl

  Position
-> Generator ext s t ret m () -> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
Monad m =>
Position -> Generator ext s t ret m a -> Generator ext s t ret m a
withPosition Position
pbody (Generator ext s t ret m () -> Generator ext s t ret m ())
-> Generator ext s t ret m () -> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$
    Label s
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineBlock Label s
loop_lbl ((forall {a}. Generator ext s t ret m a)
 -> Generator ext s t ret m ())
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall a b. (a -> b) -> a -> b
$ do
      Generator ext s t ret m ()
body
      Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
cond_lbl

  Label s
-> (forall {a}. Generator ext s t ret m a)
-> Generator ext s t ret m ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
continue Label s
exit_lbl (Label s -> Generator ext s t ret m a
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump Label s
cond_lbl)

------------------------------------------------------------------------
-- CFG

cfgFromGenerator :: FnHandle init ret
                 -> IxGeneratorState ext s t ret m i
                 -> CFG ext s init ret
cfgFromGenerator :: forall (init :: Ctx CrucibleType) (ret :: CrucibleType) ext s
       (t :: Type -> Type) (m :: Type -> Type) i.
FnHandle init ret
-> IxGeneratorState ext s t ret m i -> CFG ext s init ret
cfgFromGenerator FnHandle init ret
h IxGeneratorState ext s t ret m i
s =
  CFG { cfgHandle :: FnHandle init ret
cfgHandle = FnHandle init ret
h
      , cfgEntryLabel :: Label s
cfgEntryLabel = IxGeneratorState ext s t ret m i
sIxGeneratorState ext s t ret m i
-> Getting (Label s) (IxGeneratorState ext s t ret m i) (Label s)
-> Label s
forall s a. s -> Getting a s a -> a
^.Getting (Label s) (IxGeneratorState ext s t ret m i) (Label s)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
(Contravariant f, Functor f) =>
(Label s -> f (Label s))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsEntryLabel
      , cfgBlocks :: [Block ext s ret]
cfgBlocks = Seq (Block ext s ret) -> [Block ext s ret]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
Fold.toList (IxGeneratorState ext s t ret m i
sIxGeneratorState ext s t ret m i
-> Getting
     (Seq (Block ext s ret))
     (IxGeneratorState ext s t ret m i)
     (Seq (Block ext s ret))
-> Seq (Block ext s ret)
forall s a. s -> Getting a s a -> a
^.Getting
  (Seq (Block ext s ret))
  (IxGeneratorState ext s t ret m i)
  (Seq (Block ext s ret))
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
(Seq (Block ext s ret) -> f (Seq (Block ext s ret)))
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
gsBlocks)
      }

-- | Given the arguments, this returns the initial state, and an action for
-- computing the return value.
type FunctionDef ext t init ret m =
  forall s .
  Assignment (Atom s) init ->
  (t s, Generator ext s t ret m (Expr ext s ret))

-- | The given @FunctionDef@ action is run to generate a registerized
--   CFG. The return value of @defineFunction@ is the generated CFG,
--   and a list of CFGs for any other auxiliary function definitions
--   generated along the way (e.g., for anonymous or inner functions).
--
--   This is the same as @defineFunctionOpt@ with the identity
--   transformation.
defineFunction :: (Monad m, IsSyntaxExtension ext)
               => Position                     -- ^ Source position for the function
               -> Some (NonceGenerator m)      -- ^ Nonce generator for internal use
               -> FnHandle init ret            -- ^ Handle for the generated function
               -> FunctionDef ext t init ret m -- ^ Generator action and initial state
               -> m (SomeCFG ext init ret, [AnyCFG ext]) -- ^ Generated CFG and inner function definitions
defineFunction :: forall (m :: Type -> Type) ext (init :: Ctx CrucibleType)
       (ret :: CrucibleType) (t :: Type -> Type).
(Monad m, IsSyntaxExtension ext) =>
Position
-> Some (NonceGenerator m)
-> FnHandle init ret
-> FunctionDef ext t init ret m
-> m (SomeCFG ext init ret, [AnyCFG ext])
defineFunction Position
p Some (NonceGenerator m)
sng FnHandle init ret
h FunctionDef ext t init ret m
f = Position
-> Some (NonceGenerator m)
-> FnHandle init ret
-> FunctionDef ext t init ret m
-> (forall s.
    NonceGenerator m s -> CFG ext s init ret -> m (CFG ext s init ret))
-> m (SomeCFG ext init ret, [AnyCFG ext])
forall (m :: Type -> Type) ext (init :: Ctx CrucibleType)
       (ret :: CrucibleType) (t :: Type -> Type).
(Monad m, IsSyntaxExtension ext) =>
Position
-> Some (NonceGenerator m)
-> FnHandle init ret
-> FunctionDef ext t init ret m
-> (forall s.
    NonceGenerator m s -> CFG ext s init ret -> m (CFG ext s init ret))
-> m (SomeCFG ext init ret, [AnyCFG ext])
defineFunctionOpt Position
p Some (NonceGenerator m)
sng FnHandle init ret
h Assignment (Atom s) init
-> (t s, Generator ext s t ret m (Expr ext s ret))
FunctionDef ext t init ret m
f (\NonceGenerator m s
_ CFG ext s init ret
cfg -> CFG ext s init ret -> m (CFG ext s init ret)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return CFG ext s init ret
cfg)

-- | The main API for generating CFGs for a Crucible function.
--
--   The given @FunctionDef@ action is run to generate a registerized
--   CFG. The return value of @defineFunction@ is the generated CFG,
--   and a list of CFGs for any other auxiliary function definitions
--   generated along the way (e.g., for anonymous or inner functions).
--
--   The caller can supply a transformation to run over the generated CFG
--   (i.e. an optimization pass)
defineFunctionOpt :: (Monad m, IsSyntaxExtension ext)
                  => Position                     -- ^ Source position for the function
                  -> Some (NonceGenerator m)      -- ^ Nonce generator for internal use
                  -> FnHandle init ret            -- ^ Handle for the generated function
                  -> FunctionDef ext t init ret m -- ^ Generator action and initial state
                  -> (forall s. NonceGenerator m s
                             -> CFG ext s init ret
                             -> m (CFG ext s init ret))     -- ^ Transformation pass
                  -> m (SomeCFG ext init ret, [AnyCFG ext]) -- ^ Generated CFG and inner function definitions
defineFunctionOpt :: forall (m :: Type -> Type) ext (init :: Ctx CrucibleType)
       (ret :: CrucibleType) (t :: Type -> Type).
(Monad m, IsSyntaxExtension ext) =>
Position
-> Some (NonceGenerator m)
-> FnHandle init ret
-> FunctionDef ext t init ret m
-> (forall s.
    NonceGenerator m s -> CFG ext s init ret -> m (CFG ext s init ret))
-> m (SomeCFG ext init ret, [AnyCFG ext])
defineFunctionOpt Position
p Some (NonceGenerator m)
sng FnHandle init ret
h FunctionDef ext t init ret m
f forall s.
NonceGenerator m s -> CFG ext s init ret -> m (CFG ext s init ret)
optPass = FnHandle init ret
-> m (SomeCFG ext init ret, [AnyCFG ext])
-> m (SomeCFG ext init ret, [AnyCFG ext])
forall a b. a -> b -> b
seq FnHandle init ret
h (m (SomeCFG ext init ret, [AnyCFG ext])
 -> m (SomeCFG ext init ret, [AnyCFG ext]))
-> m (SomeCFG ext init ret, [AnyCFG ext])
-> m (SomeCFG ext init ret, [AnyCFG ext])
forall a b. (a -> b) -> a -> b
$ do
  let argTypes :: CtxRepr init
argTypes = FnHandle init ret -> CtxRepr init
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> CtxRepr args
handleArgTypes FnHandle init ret
h
  Some NonceGenerator m x
ng <- Some (NonceGenerator m) -> m (Some (NonceGenerator m))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Some (NonceGenerator m)
sng
  Assignment (Atom x) init
inputs <- NonceGenerator m x
-> Position -> CtxRepr init -> m (Assignment (Atom x) init)
forall (m :: Type -> Type) s (init :: Ctx CrucibleType).
Monad m =>
NonceGenerator m s
-> Position -> CtxRepr init -> m (Assignment (Atom s) init)
mkInputAtoms NonceGenerator m x
ng Position
p CtxRepr init
argTypes
  let inputSet :: Set (Some (Value x))
inputSet = [Some (Value x)] -> Set (Some (Value x))
forall a. Ord a => [a] -> Set a
Set.fromList ((forall (x :: CrucibleType). Atom x x -> Some (Value x))
-> forall (x :: Ctx CrucibleType).
   Assignment (Atom x) x -> [Some (Value x)]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: CrucibleType -> Type) a.
(forall (x :: CrucibleType). f x -> a)
-> forall (x :: Ctx CrucibleType). Assignment f x -> [a]
toListFC (Value x x -> Some (Value x)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Value x x -> Some (Value x))
-> (Atom x x -> Value x x) -> Atom x x -> Some (Value x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atom x x -> Value x x
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue) Assignment (Atom x) init
inputs)
  let (t x
init_state, Generator ext x t ret m (Expr ext x ret)
action) = Assignment (Atom x) init
-> (t x, Generator ext x t ret m (Expr ext x ret))
FunctionDef ext t init ret m
f (Assignment (Atom x) init
 -> (t x, Generator ext x t ret m (Expr ext x ret)))
-> Assignment (Atom x) init
-> (t x, Generator ext x t ret m (Expr ext x ret))
forall a b. (a -> b) -> a -> b
$! Assignment (Atom x) init
inputs
  Label x
lbl <- Nonce x UnitType -> Label x
forall s. Nonce s UnitType -> Label s
Label (Nonce x UnitType -> Label x)
-> m (Nonce x UnitType) -> m (Label x)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> NonceGenerator m x -> m (Nonce x UnitType)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator m x
ng
  let cbs :: CurrentBlockState ext x
cbs = Set (Some (Value x)) -> BlockID x -> CurrentBlockState ext x
forall s ext. ValueSet s -> BlockID s -> CurrentBlockState ext s
initCurrentBlockState Set (Some (Value x))
inputSet (Label x -> BlockID x
forall s. Label s -> BlockID s
LabelID Label x
lbl)
  let ts :: IxGeneratorState ext x t ret m (CurrentBlockState ext x)
ts = GS { _gsEntryLabel :: Label x
_gsEntryLabel = Label x
lbl
              , _gsBlocks :: Seq (Block ext x ret)
_gsBlocks = Seq (Block ext x ret)
forall a. Seq a
Seq.empty
              , _gsNonceGen :: NonceGenerator m x
_gsNonceGen = NonceGenerator m x
ng
              , _gsCurrent :: CurrentBlockState ext x
_gsCurrent = CurrentBlockState ext x
cbs
              , _gsPosition :: Position
_gsPosition = Position
p
              , _gsState :: t x
_gsState = t x
init_state
              , _seenFunctions :: [AnyCFG ext]
_seenFunctions = []
              }
  EndState ext x t ret m
ts' <- Generator ext x t ret m Void
-> IxGeneratorState ext x t ret m (CurrentBlockState ext x)
-> m (EndState ext x t ret m)
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Generator ext s t ret m Void
-> GeneratorState ext s t ret m -> m (EndState ext s t ret m)
runGenerator (Generator ext x t ret m (Expr ext x ret)
action Generator ext x t ret m (Expr ext x ret)
-> (Expr ext x ret -> Generator ext x t ret m Void)
-> Generator ext x t ret m Void
forall a b.
Generator ext x t ret m a
-> (a -> Generator ext x t ret m b) -> Generator ext x t ret m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expr ext x ret -> Generator ext x t ret m Void
forall (m :: Type -> Type) ext s (ret :: CrucibleType)
       (t :: Type -> Type) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s ret -> Generator ext s t ret m a
returnFromFunction) (IxGeneratorState ext x t ret m (CurrentBlockState ext x)
 -> m (EndState ext x t ret m))
-> IxGeneratorState ext x t ret m (CurrentBlockState ext x)
-> m (EndState ext x t ret m)
forall a b. (a -> b) -> a -> b
$! IxGeneratorState ext x t ret m (CurrentBlockState ext x)
ts
  CFG ext x init ret
g   <- NonceGenerator m x -> CFG ext x init ret -> m (CFG ext x init ret)
forall s.
NonceGenerator m s -> CFG ext s init ret -> m (CFG ext s init ret)
optPass NonceGenerator m x
ng (FnHandle init ret -> EndState ext x t ret m -> CFG ext x init ret
forall (init :: Ctx CrucibleType) (ret :: CrucibleType) ext s
       (t :: Type -> Type) (m :: Type -> Type) i.
FnHandle init ret
-> IxGeneratorState ext s t ret m i -> CFG ext s init ret
cfgFromGenerator FnHandle init ret
h EndState ext x t ret m
ts')
  (SomeCFG ext init ret, [AnyCFG ext])
-> m (SomeCFG ext init ret, [AnyCFG ext])
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (CFG ext x init ret -> SomeCFG ext init ret
forall ext (init :: Ctx CrucibleType) (ret :: CrucibleType) s.
CFG ext s init ret -> SomeCFG ext init ret
SomeCFG CFG ext x init ret
g, EndState ext x t ret m
ts'EndState ext x t ret m
-> Getting [AnyCFG ext] (EndState ext x t ret m) [AnyCFG ext]
-> [AnyCFG ext]
forall s a. s -> Getting a s a -> a
^.Getting [AnyCFG ext] (EndState ext x t ret m) [AnyCFG ext]
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type) i (f :: Type -> Type).
Functor f =>
([AnyCFG ext] -> f [AnyCFG ext])
-> IxGeneratorState ext s t ret m i
-> f (IxGeneratorState ext s t ret m i)
seenFunctions)