Copyright	(c) Galois Inc 2014-2018
License	BSD3
Maintainer	Joe Hendrix <jhendrix@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

Lang.Crucible.CFG.Generator

Contents

Generator
Positions
Expressions and statements
References
Labels
Block-terminating statements
Defining blocks
Control-flow combinators
Re-exports

Description

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.

Synopsis

data Generator ext s (t :: Type -> Type) (ret :: CrucibleType) (m :: Type -> Type) a
type FunctionDef ext (t :: Type -> Type) (init :: Ctx CrucibleType) (ret :: CrucibleType) (m :: Type -> Type) = forall s. Assignment (Atom s) init -> (t s, Generator ext s t ret m (Expr ext s ret))
defineFunction :: forall m 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])
defineFunctionOpt :: forall m 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])
getPosition :: forall ext s (t :: Type -> Type) (ret :: CrucibleType) (m :: Type -> Type). Generator ext s t ret m Position
setPosition :: forall ext s (t :: Type -> Type) (ret :: CrucibleType) (m :: Type -> Type). Position -> Generator ext s t ret m ()
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
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)
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)
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)
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 ()
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 ()
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 ()
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)
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 ()
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))
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))
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)
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 ()
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 ()
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)
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 ()
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 ()
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 ()
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 ()
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)
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)
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))
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))
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)
newLabel :: forall (m :: Type -> Type) ext s (t :: Type -> Type) (ret :: CrucibleType). Monad m => Generator ext s t ret m (Label s)
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' :: 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)
currentBlockID :: forall ext s (t :: Type -> Type) (ret :: CrucibleType) (m :: Type -> Type). Generator ext s t ret m (BlockID s)
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
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
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
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
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
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
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
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
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 ()
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 ()
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)
recordCFG :: forall ext s (t :: Type -> Type) (ret :: CrucibleType) (m :: Type -> Type). AnyCFG ext -> 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 ()
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)
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 ()
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 ()
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' :: 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_ :: 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 ()
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)
data MatchMaybe j r = MatchMaybe {
- onJust :: j -> r
- onNothing :: 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_ :: 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 ()
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)
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)
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 ()
data Ctx k
- = EmptyCtx
- | (Ctx k) ::> k
data Position
data Stmt ext s
- = SetReg !(Reg s tp) !(Atom s tp)
- | WriteGlobal !(GlobalVar tp) !(Atom s tp)
- | WriteRef !(Atom s (ReferenceType tp)) !(Atom s tp)
- | DropRef !(Atom s (ReferenceType tp))
- | DefineAtom !(Atom s tp) !(AtomValue ext s tp)
- | Print !(Atom s (StringType Unicode))
- | Assert !(Atom s BoolType) !(Atom s (StringType Unicode))
- | Assume !(Atom s BoolType) !(Atom s (StringType Unicode))
- | Breakpoint BreakpointName !(Assignment (Value s) args)
data Expr ext s (tp :: CrucibleType)
- = App !(App ext (Expr ext s) tp)
- | AtomExpr !(Atom s tp)
data Value s (tp :: CrucibleType)
- = RegValue !(Reg s tp)
- | AtomValue !(Atom s tp)
data Atom s (tp :: CrucibleType) = Atom {
- atomPosition :: !Position
- atomId :: !(Nonce s tp)
- atomSource :: !(AtomSource s tp)
- typeOfAtom :: !(TypeRepr tp)
}
newtype Label s = Label {
- labelId :: Nonce s UnitType
}
data CFG ext s (init :: Ctx CrucibleType) (ret :: CrucibleType) = CFG {
- cfgHandle :: !(FnHandle init ret)
- cfgEntryLabel :: !(Label s)
- cfgBlocks :: ![Block ext s ret]
}
exprType :: forall (tp :: CrucibleType). IsExpr e => e tp -> TypeRepr tp
data TermStmt s (ret :: CrucibleType) where
- Jump :: forall s (ret :: CrucibleType). !(Label s) -> TermStmt s ret
- Br :: forall s (ret :: CrucibleType). !(Atom s BoolType) -> !(Label s) -> !(Label s) -> TermStmt s ret
- MaybeBranch :: forall (tp :: CrucibleType) s (ret :: CrucibleType). !(TypeRepr tp) -> !(Atom s (MaybeType tp)) -> !(LambdaLabel s tp) -> !(Label s) -> TermStmt s ret
- VariantElim :: forall (varctx :: Ctx CrucibleType) s (ret :: CrucibleType). !(CtxRepr varctx) -> !(Atom s (VariantType varctx)) -> !(Assignment (LambdaLabel s) varctx) -> TermStmt s ret
- Return :: forall s (ret :: CrucibleType). !(Atom s ret) -> TermStmt s ret
- TailCall :: forall s (args :: Ctx CrucibleType) (ret :: CrucibleType). !(Atom s (FunctionHandleType args ret)) -> !(CtxRepr args) -> !(Assignment (Atom s) args) -> TermStmt s ret
- ErrorStmt :: forall s (ret :: CrucibleType). !(Atom s (StringType Unicode)) -> TermStmt s ret
- Output :: forall s (tp :: CrucibleType) (ret :: CrucibleType). !(LambdaLabel s tp) -> !(Atom s tp) -> TermStmt s ret
data Block ext s (ret :: CrucibleType)
data BlockID s where
- LabelID :: forall s. Label s -> BlockID s
- LambdaID :: forall s (tp :: CrucibleType). LambdaLabel s tp -> BlockID s
data GlobalVar (tp :: CrucibleType) = GlobalVar {
- globalNonce :: !(Nonce GlobalNonceGenerator tp)
- globalName :: !Text
- globalType :: !(TypeRepr tp)
}
freshGlobalVar :: forall (tp :: CrucibleType). HandleAllocator -> Text -> TypeRepr tp -> IO (GlobalVar tp)
newtype BreakpointName = BreakpointName {
- breakpointNameText :: Text
}
data SomeCFG ext (init :: Ctx CrucibleType) (ret :: CrucibleType) = SomeCFG !(CFG ext s init ret)
cfgArgTypes :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType). CFG ext s init ret -> CtxRepr init
cfgReturnType :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType). CFG ext s init ret -> TypeRepr ret
data Reg s (tp :: CrucibleType) = Reg {
- regPosition :: !Position
- regId :: !(Nonce s tp)
- typeOfReg :: !(TypeRepr tp)
}
cfgEntryBlock :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType). CFG ext s init ret -> Block ext s ret
cfgInputTypes :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType). CFG ext s init ret -> CtxRepr init
substCFG :: forall m ext s s' (init :: Ctx CrucibleType) (ret :: CrucibleType). (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> CFG ext s init ret -> m (CFG ext s' init ret)
substLabel :: Functor m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Label s -> m (Label s')
data LambdaLabel s (tp :: CrucibleType) = LambdaLabel {
- lambdaId :: !(Nonce s tp)
- lambdaAtom :: Atom s tp
}
substLambdaLabel :: forall m s s' (tp :: CrucibleType). Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> LambdaLabel s tp -> m (LambdaLabel s' tp)
substBlockID :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> BlockID s -> m (BlockID s')
substReg :: forall m s s' (tp :: CrucibleType). Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Reg s tp -> m (Reg s' tp)
traverseCFG :: forall m ext genv penv s (ret :: CrucibleType) (init :: Ctx CrucibleType). (Monad m, TraverseExt ext) => (genv -> penv -> Block ext s ret -> m (genv, penv)) -> genv -> penv -> Block ext s ret -> CFG ext s init ret -> m genv
substAtom :: forall m s s' (tp :: CrucibleType). Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Atom s tp -> m (Atom s' tp)
data AtomSource s (tp :: CrucibleType)
- = Assigned
- | FnInput
- | LambdaArg !(LambdaLabel s tp)
substAtomSource :: forall m s s' (tp :: CrucibleType). Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> AtomSource s tp -> m (AtomSource s' tp)
mkInputAtoms :: forall m s (init :: Ctx CrucibleType). Monad m => NonceGenerator m s -> Position -> CtxRepr init -> m (Assignment (Atom s) init)
data AtomValue ext s (tp :: CrucibleType) where
- EvalApp :: forall ext s (tp :: CrucibleType). !(App ext (Atom s) tp) -> AtomValue ext s tp
- ReadReg :: forall s (tp :: CrucibleType) ext. !(Reg s tp) -> AtomValue ext s tp
- EvalExt :: forall ext s (tp :: CrucibleType). !(StmtExtension ext (Atom s) tp) -> AtomValue ext s tp
- ReadGlobal :: forall (tp :: CrucibleType) ext s. !(GlobalVar tp) -> AtomValue ext s tp
- ReadRef :: forall s (tp :: CrucibleType) ext. !(Atom s (ReferenceType tp)) -> AtomValue ext s tp
- NewRef :: forall s (tp1 :: CrucibleType) ext. !(Atom s tp1) -> AtomValue ext s ('ReferenceType tp1)
- NewEmptyRef :: forall (tp1 :: CrucibleType) ext s. !(TypeRepr tp1) -> AtomValue ext s ('ReferenceType tp1)
- FreshConstant :: forall (bt :: BaseType) ext s. !(BaseTypeRepr bt) -> !(Maybe SolverSymbol) -> AtomValue ext s ('BaseToType bt)
- FreshFloat :: forall (fi :: FloatInfo) ext s. !(FloatInfoRepr fi) -> !(Maybe SolverSymbol) -> AtomValue ext s ('FloatType fi)
- FreshNat :: forall ext s. !(Maybe SolverSymbol) -> AtomValue ext s 'NatType
- Call :: forall s (args :: Ctx CrucibleType) (tp :: CrucibleType) ext. !(Atom s (FunctionHandleType args tp)) -> !(Assignment (Atom s) args) -> !(TypeRepr tp) -> AtomValue ext s tp
typeOfAtomValue :: forall ext s (tp :: CrucibleType). (TypeApp (StmtExtension ext), TypeApp (ExprExtension ext)) => AtomValue ext s tp -> TypeRepr tp
substAtomValue :: forall m ext s s' (tp :: CrucibleType). (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> AtomValue ext s tp -> m (AtomValue ext s' tp)
typeOfValue :: forall s (tp :: CrucibleType). Value s tp -> TypeRepr tp
substValue :: forall m s s' (tp :: CrucibleType). Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Value s tp -> m (Value s' tp)
type ValueSet s = Set (Some (Value s))
substValueSet :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> ValueSet s -> m (ValueSet s')
mkBlock :: forall ext s (ret :: CrucibleType). TraverseExt ext => BlockID s -> ValueSet s -> Seq (Posd (Stmt ext s)) -> Posd (TermStmt s ret) -> Block ext s ret
substBlock :: forall m ext s s' (ret :: CrucibleType). (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Block ext s ret -> m (Block ext s' ret)
substStmt :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Stmt ext s -> m (Stmt ext s')
substPosdStmt :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Posd (Stmt ext s) -> m (Posd (Stmt ext s'))
mapStmtAtom :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Atom s x -> m (Atom s x)) -> Stmt ext s -> m (Stmt ext s)
termStmtInputs :: forall s (ret :: CrucibleType). TermStmt s ret -> ValueSet s
termNextLabels :: forall s (ret :: CrucibleType). TermStmt s ret -> Maybe [BlockID s]
substTermStmt :: forall m s s' (ret :: CrucibleType). Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> TermStmt s ret -> m (TermStmt s' ret)
substPosdTermStmt :: forall m s s' (ret :: CrucibleType). Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Posd (TermStmt s ret) -> m (Posd (TermStmt s' ret))
foldStmtInputs :: TraverseExt ext => (forall (x :: CrucibleType). Value s x -> b -> b) -> Stmt ext s -> b -> b
substExpr :: forall m ext s s' (tp :: CrucibleType). (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Expr ext s tp -> m (Expr ext s' tp)
module Lang.Crucible.CFG.EarlyMergeLoops

Generator

data Generator ext s (t :: Type -> Type) (ret :: CrucibleType) (m :: Type -> Type) a Source #

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.

Instances

Instances details

Monad m => MonadState (t s) (Generator ext s t ret m) Source #
Instance details Defined in Lang.Crucible.CFG.Generator Methods get :: Generator ext s t ret m (t s) # put :: t s -> Generator ext s t ret m () # state :: (t s -> (a, t s)) -> Generator ext s t ret m a #
MonadTrans (Generator ext s t ret) Source #
Instance details Defined in Lang.Crucible.CFG.Generator Methods lift :: Monad m => m a -> Generator ext s t ret m a #
MonadFail m => MonadFail (Generator ext s t ret m) Source #
Instance details Defined in Lang.Crucible.CFG.Generator Methods fail :: String -> Generator ext s t ret m a #
MonadIO m => MonadIO (Generator ext s t ret m) Source #
Instance details Defined in Lang.Crucible.CFG.Generator Methods liftIO :: IO a -> Generator ext s t ret m a #
Applicative (Generator ext s t ret m) Source #
Instance details Defined in Lang.Crucible.CFG.Generator Methods pure :: a -> Generator ext s t ret m a # (<>) :: Generator ext s t ret m (a -> b) -> Generator ext s t ret m a -> Generator ext s t ret m b # liftA2 :: (a -> b -> c) -> Generator ext s t ret m a -> Generator ext s t ret m b -> Generator ext s t ret m c # (>) :: Generator ext s t ret m a -> Generator ext s t ret m b -> Generator ext s t ret m b # (<*) :: Generator ext s t ret m a -> Generator ext s t ret m b -> Generator ext s t ret m a #
Functor (Generator ext s t ret m) Source #
Instance details Defined in Lang.Crucible.CFG.Generator Methods fmap :: (a -> b) -> Generator ext s t ret m a -> Generator ext s t ret m b # (<$) :: a -> Generator ext s t ret m b -> Generator ext s t ret m a #
Monad m => Monad (Generator ext s t ret m) Source #
Instance details Defined in Lang.Crucible.CFG.Generator Methods (>>=) :: Generator ext s t ret m a -> (a -> Generator ext s t ret m b) -> Generator ext s t ret m b # (>>) :: Generator ext s t ret m a -> Generator ext s t ret m b -> Generator ext s t ret m b # return :: a -> Generator ext s t ret m a #
MonadCatch m => MonadCatch (Generator ext s t ret m) Source #
Instance details Defined in Lang.Crucible.CFG.Generator Methods catch :: (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 #
MonadThrow m => MonadThrow (Generator ext s t ret m) Source #
Instance details Defined in Lang.Crucible.CFG.Generator Methods throwM :: (HasCallStack, Exception e) => e -> Generator ext s t ret m a #

type FunctionDef ext (t :: Type -> Type) (init :: Ctx CrucibleType) (ret :: CrucibleType) (m :: Type -> Type) = forall s. Assignment (Atom s) init -> (t s, Generator ext s t ret m (Expr ext s ret)) Source #

Given the arguments, this returns the initial state, and an action for computing the return value.

defineFunction Source #

Arguments

:: forall m ext (init :: Ctx CrucibleType) (ret :: CrucibleType) (t :: Type -> Type). (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

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.

defineFunctionOpt Source #

Arguments

:: forall m ext (init :: Ctx CrucibleType) (ret :: CrucibleType) (t :: Type -> Type). (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

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)

Positions

getPosition :: forall ext s (t :: Type -> Type) (ret :: CrucibleType) (m :: Type -> Type). Generator ext s t ret m Position Source #

Get the current position.

setPosition :: forall ext s (t :: Type -> Type) (ret :: CrucibleType) (m :: Type -> Type). Position -> Generator ext s t ret m () Source #

Set the current position.

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 Source #

Set the current position temporarily, and reset it afterwards.

Expressions and statements

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) Source #

Generate a new virtual register with the given initial value.

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) Source #

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.

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) Source #

Get the current value of a register.

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 () Source #

Update the value of a register.

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 () Source #

Modify the value of a register.

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 () Source #

Modify the value of a register.

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) Source #

Read a global variable.

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 () Source #

Write to a global variable.

References

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)) Source #

Generate a new reference cell with the given initial contents.

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)) Source #

Generate a new empty reference cell. If an unassigned reference is later read, it will generate a runtime error.

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) Source #

Read the current value of a reference cell.

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 () Source #

Write the given value into the reference cell.

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 () Source #

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.

call Source #

Arguments

:: 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)	function to call
-> Assignment (Expr ext s) args	function arguments
-> Generator ext s t r m (Expr ext s ret)

Call a function.

assertExpr Source #

Arguments

:: forall (m :: Type -> Type) ext s (t :: Type -> Type) (ret :: CrucibleType). (Monad m, IsSyntaxExtension ext)
=> Expr ext s BoolType	assertion
-> Expr ext s (StringType Unicode)	error message
-> Generator ext s t ret m ()

Add an assert statement.

assumeExpr Source #

Arguments

:: forall (m :: Type -> Type) ext s (t :: Type -> Type) (ret :: CrucibleType). (Monad m, IsSyntaxExtension ext)
=> Expr ext s BoolType	assumption
-> Expr ext s (StringType Unicode)	reason message
-> Generator ext s t ret m ()

Add an assume statement.

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 () Source #

Add a statement to print a value.

addBreakpointStmt Source #

Arguments

:: forall (m :: Type -> Type) ext s (args :: Ctx CrucibleType) (t :: Type -> Type) (r :: CrucibleType). (Monad m, IsSyntaxExtension ext)
=> Text	breakpoint name
-> Assignment (Value s) args	breakpoint values
-> Generator ext s t r m ()

Add a breakpoint.

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) Source #

Add a statement from the syntax extension to the current basic block.

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) Source #

Create an atom equivalent to the given expression if it is not already an AtomExpr.

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)) Source #

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)) Source #

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) Source #

Evaluate an expression to an AtomExpr, so that it can be reused multiple times later.

Labels

newLabel :: forall (m :: Type -> Type) ext s (t :: Type -> Type) (ret :: CrucibleType). Monad m => Generator ext s t ret m (Label s) Source #

Create a new block label.

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) Source #

Create a new lambda label.

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) Source #

Create a new lambda label, using an explicit TypeRepr.

currentBlockID :: forall ext s (t :: Type -> Type) (ret :: CrucibleType) (m :: Type -> Type). Generator ext s t ret m (BlockID s) Source #

Return the label of the current basic block.

Block-terminating statements

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.

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 Source #

Jump to the given label.

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 Source #

Jump to the given label with output.

branch Source #

Arguments

:: forall (m :: Type -> Type) ext s (t :: Type -> Type) (ret :: CrucibleType) a. (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 between blocks.

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 Source #

Return from this function with the given return value.

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 Source #

Report an error message.

branchMaybe Source #

Arguments

:: 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 for `Just`
-> Label s	label for `Nothing`
-> Generator ext s t ret m a

Branch between blocks based on a Maybe value.

branchVariant Source #

Arguments

:: forall (m :: Type -> Type) ext s (varctx :: Ctx CrucibleType) (t :: Type -> Type) (ret :: CrucibleType) a. (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

Switch on a variant value. Examine the tag of the variant and jump to the appropriate switch target.

tailCall Source #

Arguments

:: 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)	function to call
-> Assignment (Expr ext s) args	function arguments
-> Generator ext s t ret m a

End a block with a tail call to a function.

Defining blocks

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

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 () Source #

Define a block with an ordinary label.

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 () Source #

Define a block that has a lambda label.

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) Source #

Define a block with a fresh label, returning the label.

recordCFG :: forall ext s (t :: Type -> Type) (ret :: CrucibleType) (m :: Type -> Type). AnyCFG ext -> Generator ext s t ret m () Source #

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.

Control-flow combinators

continue Source #

Arguments

:: forall (m :: Type -> Type) ext s (t :: Type -> Type) (ret :: CrucibleType). (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 ()

End the translation of the current block, and then continue generating a new block with the given label.

continueLambda Source #

Arguments

:: forall (m :: Type -> Type) ext s (tp :: CrucibleType) (t :: Type -> Type) (ret :: CrucibleType). (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)

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.

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 () Source #

Run a computation when a condition is true.

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 () Source #

Run a computation when a condition is false.

ifte Source #

Arguments

:: 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)	true branch
-> Generator ext s t ret m (Expr ext s tp)	false branch
-> Generator ext s t ret m (Expr ext s tp)

Expression-level if-then-else.

ifte' Source #

Arguments

:: 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)	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_ Source #

Arguments

:: 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 ()	true branch
-> Generator ext s t ret m ()	false branch
-> Generator ext s t ret m ()

Statement-level if-then-else.

ifteM Source #

Arguments

:: 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)	true branch
-> Generator ext s t ret m (Expr ext s tp)	false branch
-> Generator ext s t ret m (Expr ext s tp)

Expression-level if-then-else with a monadic condition.

data MatchMaybe j r Source #

Constructors

MatchMaybe
Fields onJust :: j -> r onNothing :: r

caseMaybe Source #

Arguments

:: forall (m :: Type -> Type) ext s (tp :: CrucibleType) (r :: CrucibleType) (t :: Type -> Type) (ret :: CrucibleType). (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)

Compute an expression by cases over a Maybe value.

caseMaybe_ Source #

Arguments

:: forall (m :: Type -> Type) ext s (tp :: CrucibleType) (t :: Type -> Type) (ret :: CrucibleType). (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 ()

Evaluate different statements by cases over a Maybe value.

fromJustExpr Source #

Arguments

:: 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)	error message
-> Generator ext s t ret m (Expr ext s tp)

Return the argument of a Just value, or call reportError if the value is Nothing.

assertedJustExpr Source #

Arguments

:: 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)	error message
-> Generator ext s t ret m (Expr ext s tp)

This asserts that the value in the expression is a Just value, and returns the underlying value.

while Source #

Arguments

:: 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))	test condition
-> (Position, Generator ext s t ret m ())	loop body
-> Generator ext s t ret m ()

Execute the loop body as long as the test condition is true.

Re-exports

data Ctx k #

Kind Ctx k comprises lists of types of kind k.

Constructors

EmptyCtx
(Ctx k) ::> k

Instances

Instances details

FoldableFC (Assignment :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Safe Methods foldMapFC :: forall f m. Monoid m => (forall (x :: k). f x -> m) -> forall (x :: Ctx k). Assignment f x -> m # foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b # foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b # foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b # foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b # toListFC :: (forall (x :: k). f x -> a) -> forall (x :: Ctx k). Assignment f x -> [a] #
FoldableFC (Assignment :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods foldMapFC :: forall f m. Monoid m => (forall (x :: k). f x -> m) -> forall (x :: Ctx k). Assignment f x -> m # foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b # foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b # foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b # foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b # toListFC :: (forall (x :: k). f x -> a) -> forall (x :: Ctx k). Assignment f x -> [a] #
FunctorFC (Assignment :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Safe Methods fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: Ctx k). Assignment f x -> Assignment g x #
FunctorFC (Assignment :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: Ctx k). Assignment f x -> Assignment g x #
OrdFC (Assignment :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Safe Methods compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> OrderingF x y #
OrdFC (Assignment :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> OrderingF x y #
TestEqualityFC (Assignment :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Safe Methods testEqualityFC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Maybe (x :~: y) #
TestEqualityFC (Assignment :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods testEqualityFC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Maybe (x :~: y) #
TraversableFC (Assignment :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Safe Methods traverseFC :: forall f g m. Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: Ctx k). Assignment f x -> m (Assignment g x) #
TraversableFC (Assignment :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods traverseFC :: forall f g m. Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: Ctx k). Assignment f x -> m (Assignment g x) #
FoldableFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Safe Methods ifoldMapFC :: forall f m (z :: Ctx k). Monoid m => (forall (x :: k). IndexF (Assignment f z) x -> f x -> m) -> Assignment f z -> m # ifoldrFC :: forall (z :: Ctx k) f b. (forall (x :: k). IndexF (Assignment f z) x -> f x -> b -> b) -> b -> Assignment f z -> b # ifoldlFC :: forall f b (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> b -> f x -> b) -> b -> Assignment f z -> b # ifoldrFC' :: forall f b (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> f x -> b -> b) -> b -> Assignment f z -> b # ifoldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b # itoListFC :: forall f a (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> f x -> a) -> Assignment f z -> [a] #
FoldableFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods ifoldMapFC :: forall f m (z :: Ctx k). Monoid m => (forall (x :: k). IndexF (Assignment f z) x -> f x -> m) -> Assignment f z -> m # ifoldrFC :: forall (z :: Ctx k) f b. (forall (x :: k). IndexF (Assignment f z) x -> f x -> b -> b) -> b -> Assignment f z -> b # ifoldlFC :: forall f b (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> b -> f x -> b) -> b -> Assignment f z -> b # ifoldrFC' :: forall f b (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> f x -> b -> b) -> b -> Assignment f z -> b # ifoldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: Ctx k). b -> Assignment f x -> b # itoListFC :: forall f a (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> f x -> a) -> Assignment f z -> [a] #
FunctorFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Safe Methods imapFC :: forall f g (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> f x -> g x) -> Assignment f z -> Assignment g z #
FunctorFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods imapFC :: forall f g (z :: Ctx k). (forall (x :: k). IndexF (Assignment f z) x -> f x -> g x) -> Assignment f z -> Assignment g z #
TraversableFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Safe Methods itraverseFC :: forall m (z :: Ctx k) f g. Applicative m => (forall (x :: k). IndexF (Assignment f z) x -> f x -> m (g x)) -> Assignment f z -> m (Assignment g z) #
TraversableFCWithIndex (Assignment :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods itraverseFC :: forall m (z :: Ctx k) f g. Applicative m => (forall (x :: k). IndexF (Assignment f z) x -> f x -> m (g x)) -> Assignment f z -> m (Assignment g z) #
OrdFC (BalancedTree h :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: Ctx k) (y :: Ctx k). BalancedTree h f x -> BalancedTree h f y -> OrderingF x y #
OrdFC (BinomialTree h :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: Ctx k) (y :: Ctx k). BinomialTree h f x -> BinomialTree h f y -> OrderingF x y #
TestEqualityFC (BalancedTree h :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods testEqualityFC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: Ctx k) (y :: Ctx k). BalancedTree h f x -> BalancedTree h f y -> Maybe (x :~: y) #
TestEqualityFC (BinomialTree h :: (k -> Type) -> Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods testEqualityFC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: Ctx k) (y :: Ctx k). BinomialTree h f x -> BinomialTree h f y -> Maybe (x :~: y) #
TestEquality SpecialFunction
Instance details Defined in What4.SpecialFunctions Methods testEquality :: forall (a :: Ctx Type) (b :: Ctx Type). SpecialFunction a -> SpecialFunction b -> Maybe (a :~: b) #
HashableF SpecialFunction
Instance details Defined in What4.SpecialFunctions Methods hashWithSaltF :: forall (tp :: Ctx Type). Int -> SpecialFunction tp -> Int # hashF :: forall (tp :: Ctx Type). SpecialFunction tp -> Int #
OrdF SpecialFunction
Instance details Defined in What4.SpecialFunctions Methods compareF :: forall (x :: Ctx Type) (y :: Ctx Type). SpecialFunction x -> SpecialFunction y -> OrderingF x y # leqF :: forall (x :: Ctx Type) (y :: Ctx Type). SpecialFunction x -> SpecialFunction y -> Bool # ltF :: forall (x :: Ctx Type) (y :: Ctx Type). SpecialFunction x -> SpecialFunction y -> Bool # geqF :: forall (x :: Ctx Type) (y :: Ctx Type). SpecialFunction x -> SpecialFunction y -> Bool # gtF :: forall (x :: Ctx Type) (y :: Ctx Type). SpecialFunction x -> SpecialFunction y -> Bool #
Category (Diff :: Ctx k -> Ctx k -> Type)	Implemented with `noDiff` and `addDiff`
Instance details Defined in Data.Parameterized.Context.Safe Methods id :: forall (a :: Ctx k). Diff a a # (.) :: forall (b :: Ctx k) (c :: Ctx k) (a :: Ctx k). Diff b c -> Diff a b -> Diff a c #
Category (Diff :: Ctx k -> Ctx k -> Type)	Implemented with `noDiff` and `addDiff`
Instance details Defined in Data.Parameterized.Context.Unsafe Methods id :: forall (a :: Ctx k). Diff a a # (.) :: forall (b :: Ctx k) (c :: Ctx k) (a :: Ctx k). Diff b c -> Diff a b -> Diff a c #
TestEquality (BlockID blocks :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods testEquality :: forall (a :: Ctx CrucibleType) (b :: Ctx CrucibleType). BlockID blocks a -> BlockID blocks b -> Maybe (a :~: b) #
TestEquality (MatlabFnWrapper t :: Ctx BaseType -> Type)
Instance details Defined in What4.Expr.Builder Methods testEquality :: forall (a :: Ctx BaseType) (b :: Ctx BaseType). MatlabFnWrapper t a -> MatlabFnWrapper t b -> Maybe (a :~: b) #
IsSymFn (SymFn sym) => TestEquality (SymFnWrapper sym :: Ctx BaseType -> Type)
Instance details Defined in What4.Interface Methods testEquality :: forall (a :: Ctx BaseType) (b :: Ctx BaseType). SymFnWrapper sym a -> SymFnWrapper sym b -> Maybe (a :~: b) #
TestEquality (CrucibleBranchTarget f :: Maybe (Ctx CrucibleType) -> Type) Source #
Instance details Defined in Lang.Crucible.Simulator.CallFrame Methods testEquality :: forall (a :: Maybe (Ctx CrucibleType)) (b :: Maybe (Ctx CrucibleType)). CrucibleBranchTarget f a -> CrucibleBranchTarget f b -> Maybe (a :~: b) #
HashableF (MatlabFnWrapper t :: Ctx BaseType -> Type)
Instance details Defined in What4.Expr.Builder Methods hashWithSaltF :: forall (tp :: Ctx BaseType). Int -> MatlabFnWrapper t tp -> Int # hashF :: forall (tp :: Ctx BaseType). MatlabFnWrapper t tp -> Int #
OrdF (BlockID blocks :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods compareF :: forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType). BlockID blocks x -> BlockID blocks y -> OrderingF x y # leqF :: forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType). BlockID blocks x -> BlockID blocks y -> Bool # ltF :: forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType). BlockID blocks x -> BlockID blocks y -> Bool # geqF :: forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType). BlockID blocks x -> BlockID blocks y -> Bool # gtF :: forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType). BlockID blocks x -> BlockID blocks y -> Bool #
IsSymFn (SymFn sym) => OrdF (SymFnWrapper sym :: Ctx BaseType -> Type)
Instance details Defined in What4.Interface Methods compareF :: forall (x :: Ctx BaseType) (y :: Ctx BaseType). SymFnWrapper sym x -> SymFnWrapper sym y -> OrderingF x y # leqF :: forall (x :: Ctx BaseType) (y :: Ctx BaseType). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool # ltF :: forall (x :: Ctx BaseType) (y :: Ctx BaseType). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool # geqF :: forall (x :: Ctx BaseType) (y :: Ctx BaseType). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool # gtF :: forall (x :: Ctx BaseType) (y :: Ctx BaseType). SymFnWrapper sym x -> SymFnWrapper sym y -> Bool #
ShowF (BlockID blocks :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods withShow :: forall p q (tp :: Ctx CrucibleType) a. p (BlockID blocks) -> q tp -> (Show (BlockID blocks tp) => a) -> a # showF :: forall (tp :: Ctx CrucibleType). BlockID blocks tp -> String # showsPrecF :: forall (tp :: Ctx CrucibleType). Int -> BlockID blocks tp -> String -> String #
ShowF (Size :: Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Safe Methods withShow :: forall p q (tp :: Ctx k) a. p (Size :: Ctx k -> Type) -> q tp -> (Show (Size tp) => a) -> a # showF :: forall (tp :: Ctx k). Size tp -> String # showsPrecF :: forall (tp :: Ctx k). Int -> Size tp -> String -> String #
ShowF (Size :: Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods withShow :: forall p q (tp :: Ctx k) a. p (Size :: Ctx k -> Type) -> q tp -> (Show (Size tp) => a) -> a # showF :: forall (tp :: Ctx k). Size tp -> String # showsPrecF :: forall (tp :: Ctx k). Int -> Size tp -> String -> String #
TestEquality f => TestEquality (Assignment f :: Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Safe Methods testEquality :: forall (a :: Ctx k) (b :: Ctx k). Assignment f a -> Assignment f b -> Maybe (a :~: b) #
TestEquality f => TestEquality (Assignment f :: Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: forall (a :: Ctx k) (b :: Ctx k). Assignment f a -> Assignment f b -> Maybe (a :~: b) #
EqF f => EqF (Assignment f :: Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Safe Methods eqF :: forall (a :: Ctx k). Assignment f a -> Assignment f a -> Bool #
EqF f => EqF (Assignment f :: Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods eqF :: forall (a :: Ctx k). Assignment f a -> Assignment f a -> Bool #
(HashableF f, TestEquality f) => HashableF (Assignment f :: Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Safe Methods hashWithSaltF :: forall (tp :: Ctx k). Int -> Assignment f tp -> Int # hashF :: forall (tp :: Ctx k). Assignment f tp -> Int #
(HashableF f, TestEquality f) => HashableF (Assignment f :: Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods hashWithSaltF :: forall (tp :: Ctx k). Int -> Assignment f tp -> Int # hashF :: forall (tp :: Ctx k). Assignment f tp -> Int #
OrdF f => OrdF (Assignment f :: Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Safe Methods compareF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> OrderingF x y # leqF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool # ltF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool # geqF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool # gtF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool #
OrdF f => OrdF (Assignment f :: Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods compareF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> OrderingF x y # leqF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool # ltF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool # geqF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool # gtF :: forall (x :: Ctx k) (y :: Ctx k). Assignment f x -> Assignment f y -> Bool #
ShowF dom => ShowF (PointAbstraction blocks dom :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.Analysis.Fixpoint Methods withShow :: forall p q (tp :: Ctx CrucibleType) a. p (PointAbstraction blocks dom) -> q tp -> (Show (PointAbstraction blocks dom tp) => a) -> a # showF :: forall (tp :: Ctx CrucibleType). PointAbstraction blocks dom tp -> String # showsPrecF :: forall (tp :: Ctx CrucibleType). Int -> PointAbstraction blocks dom tp -> String -> String #
ShowF f => ShowF (Assignment f :: Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Safe Methods withShow :: forall p q (tp :: Ctx k) a. p (Assignment f) -> q tp -> (Show (Assignment f tp) => a) -> a # showF :: forall (tp :: Ctx k). Assignment f tp -> String # showsPrecF :: forall (tp :: Ctx k). Int -> Assignment f tp -> String -> String #
ShowF f => ShowF (Assignment f :: Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods withShow :: forall p q (tp :: Ctx k) a. p (Assignment f) -> q tp -> (Show (Assignment f tp) => a) -> a # showF :: forall (tp :: Ctx k). Assignment f tp -> String # showsPrecF :: forall (tp :: Ctx k). Int -> Assignment f tp -> String -> String #
IsRepr f => IsRepr (Assignment f :: Ctx k -> Type)
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: Ctx k) r. Assignment f a -> (KnownRepr (Assignment f) a => r) -> r #
KnownRepr (Assignment f :: Ctx k -> Type) (EmptyCtx :: Ctx k)
Instance details Defined in Data.Parameterized.Context.Safe Methods knownRepr :: Assignment f (EmptyCtx :: Ctx k) #
KnownRepr (Assignment f :: Ctx k -> Type) (EmptyCtx :: Ctx k)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods knownRepr :: Assignment f (EmptyCtx :: Ctx k) #
(KnownRepr (Assignment f) ctx, KnownRepr f bt) => KnownRepr (Assignment f :: Ctx k -> Type) (ctx ::> bt :: Ctx k)
Instance details Defined in Data.Parameterized.Context.Safe Methods knownRepr :: Assignment f (ctx ::> bt) #
(KnownRepr (Assignment f) ctx, KnownRepr f bt) => KnownRepr (Assignment f :: Ctx k -> Type) (ctx ::> bt :: Ctx k)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods knownRepr :: Assignment f (ctx ::> bt) #
HashableF f => HashableF (BalancedTree h f :: Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods hashWithSaltF :: forall (tp :: Ctx k). Int -> BalancedTree h f tp -> Int # hashF :: forall (tp :: Ctx k). BalancedTree h f tp -> Int #
HashableF f => HashableF (BinomialTree h f :: Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods hashWithSaltF :: forall (tp :: Ctx k). Int -> BinomialTree h f tp -> Int # hashF :: forall (tp :: Ctx k). BinomialTree h f tp -> Int #
PrettyExt ext => ShowF (Block ext blocks ret :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods withShow :: forall p q (tp :: Ctx CrucibleType) a. p (Block ext blocks ret) -> q tp -> (Show (Block ext blocks ret tp) => a) -> a # showF :: forall (tp :: Ctx CrucibleType). Block ext blocks ret tp -> String # showsPrecF :: forall (tp :: Ctx CrucibleType). Int -> Block ext blocks ret tp -> String -> String #
ShowF f => ShowF (BalancedTree h f :: Ctx k -> Type)
Instance details Defined in Data.Parameterized.Context.Unsafe Methods withShow :: forall p q (tp :: Ctx k) a. p (BalancedTree h f) -> q tp -> (Show (BalancedTree h f tp) => a) -> a # showF :: forall (tp :: Ctx k). BalancedTree h f tp -> String # showsPrecF :: forall (tp :: Ctx k). Int -> BalancedTree h f tp -> String -> String #
MonadState (SimState p sym ext rtp (OverrideLang ret) ('Just args)) (OverrideSim p sym ext rtp args ret) Source #
Instance details Defined in Lang.Crucible.Simulator.OverrideSim Methods get :: OverrideSim p sym ext rtp args ret (SimState p sym ext rtp (OverrideLang ret) ('Just args)) # put :: SimState p sym ext rtp (OverrideLang ret) ('Just args) -> OverrideSim p sym ext rtp args ret () # state :: (SimState p sym ext rtp (OverrideLang ret) ('Just args) -> (a, SimState p sym ext rtp (OverrideLang ret) ('Just args))) -> OverrideSim p sym ext rtp args ret a #

data Position #

Instances

Instances details

Show Position
Instance details Defined in What4.ProgramLoc Methods showsPrec :: Int -> Position -> ShowS # show :: Position -> String # showList :: [Position] -> ShowS #
NFData Position
Instance details Defined in What4.ProgramLoc Methods rnf :: Position -> () #
Eq Position
Instance details Defined in What4.ProgramLoc Methods (==) :: Position -> Position -> Bool # (/=) :: Position -> Position -> Bool #
Ord Position
Instance details Defined in What4.ProgramLoc Methods compare :: Position -> Position -> Ordering # (<) :: Position -> Position -> Bool # (<=) :: Position -> Position -> Bool # (>) :: Position -> Position -> Bool # (>=) :: Position -> Position -> Bool # max :: Position -> Position -> Position # min :: Position -> Position -> Position #
Pretty Position
Instance details Defined in What4.ProgramLoc Methods pretty :: Position -> Doc ann # prettyList :: [Position] -> Doc ann #

data Stmt ext s Source #

Statement in control flow graph.

Constructors

SetReg !(Reg s tp) !(Atom s tp)
WriteGlobal !(GlobalVar tp) !(Atom s tp)
WriteRef !(Atom s (ReferenceType tp)) !(Atom s tp)
DropRef !(Atom s (ReferenceType tp))
DefineAtom !(Atom s tp) !(AtomValue ext s tp)
Print !(Atom s (StringType Unicode))
Assert !(Atom s BoolType) !(Atom s (StringType Unicode))	Assert that the given expression is true.
Assume !(Atom s BoolType) !(Atom s (StringType Unicode))	Assume the given expression.
Breakpoint BreakpointName !(Assignment (Value s) args)

Instances

Instances details

PrettyExt ext => Show (Stmt ext s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> Stmt ext s -> ShowS # show :: Stmt ext s -> String # showList :: [Stmt ext s] -> ShowS #
PrettyExt ext => Pretty (Stmt ext s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: Stmt ext s -> Doc ann # prettyList :: [Stmt ext s] -> Doc ann #

data Expr ext s (tp :: CrucibleType) Source #

An expression in RTL representation.

The type arguments are:

ext: the extensions currently in use (use () for no extension)
s: a dummy variable that should almost always be universally quantified
tp: the Crucible type of the expression

Constructors

App !(App ext (Expr ext s) tp)	An application of an expression
AtomExpr !(Atom s tp)	An evaluated expession

Instances

Instances details

PrettyExt ext => ShowF (Expr ext s :: CrucibleType -> Type) Source #

Instance details

Defined in Lang.Crucible.CFG.Reg

Methods

withShow :: forall p q (tp :: CrucibleType) a. p (Expr ext s) -> q tp -> (Show (Expr ext s tp) => a) -> a #

showF :: forall (tp :: CrucibleType). Expr ext s tp -> String #

showsPrecF :: forall (tp :: CrucibleType). Int -> Expr ext s tp -> String -> String #

TypeApp (ExprExtension ext) => IsExpr (Expr ext s) Source #

Instance details

Defined in Lang.Crucible.CFG.Reg

Associated Types

type ExprExt (Expr ext s)
Instance details Defined in Lang.Crucible.CFG.Reg type ExprExt (Expr ext s) = ext

Methods

app :: forall (tp :: CrucibleType). App (ExprExt (Expr ext s)) (Expr ext s) tp -> Expr ext s tp Source #

asApp :: forall (tp :: CrucibleType). Expr ext s tp -> Maybe (App (ExprExt (Expr ext s)) (Expr ext s) tp) Source #

exprType :: forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp Source #

IsString (Expr ext s (StringType Unicode)) Source #

Instance details

Defined in Lang.Crucible.CFG.Reg

Methods

fromString :: String -> Expr ext s (StringType Unicode) #

PrettyExt ext => Show (Expr ext s tp) Source #

Instance details

Defined in Lang.Crucible.CFG.Reg

Methods

showsPrec :: Int -> Expr ext s tp -> ShowS #

show :: Expr ext s tp -> String #

showList :: [Expr ext s tp] -> ShowS #

PrettyExt ext => Pretty (Expr ext s tp) Source #

Instance details

Defined in Lang.Crucible.CFG.Reg

Methods

pretty :: Expr ext s tp -> Doc ann #

prettyList :: [Expr ext s tp] -> Doc ann #

type ExprExt (Expr ext s) Source #

Instance details

Defined in Lang.Crucible.CFG.Reg

type ExprExt (Expr ext s) = ext

data Value s (tp :: CrucibleType) Source #

A value is either a register or an atom.

Constructors

RegValue !(Reg s tp)
AtomValue !(Atom s tp)

Instances

Instances details

TestEquality (Value s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods testEquality :: forall (a :: CrucibleType) (b :: CrucibleType). Value s a -> Value s b -> Maybe (a :~: b) #
OrdF (Value s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compareF :: forall (x :: CrucibleType) (y :: CrucibleType). Value s x -> Value s y -> OrderingF x y # leqF :: forall (x :: CrucibleType) (y :: CrucibleType). Value s x -> Value s y -> Bool # ltF :: forall (x :: CrucibleType) (y :: CrucibleType). Value s x -> Value s y -> Bool # geqF :: forall (x :: CrucibleType) (y :: CrucibleType). Value s x -> Value s y -> Bool # gtF :: forall (x :: CrucibleType) (y :: CrucibleType). Value s x -> Value s y -> Bool #
ShowF (Value s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods withShow :: forall p q (tp :: CrucibleType) a. p (Value s) -> q tp -> (Show (Value s tp) => a) -> a # showF :: forall (tp :: CrucibleType). Value s tp -> String # showsPrecF :: forall (tp :: CrucibleType). Int -> Value s tp -> String -> String #
Pretty (ValueSet s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: ValueSet s -> Doc ann # prettyList :: [ValueSet s] -> Doc ann #
Show (Value s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> Value s tp -> ShowS # show :: Value s tp -> String # showList :: [Value s tp] -> ShowS #
Pretty (Value s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: Value s tp -> Doc ann # prettyList :: [Value s tp] -> Doc ann #

data Atom s (tp :: CrucibleType) Source #

An expression in the control flow graph with a unique identifier. Unlike registers, atoms must be assigned exactly once.

Constructors

Atom
Fields atomPosition :: !Position Position where register was declared (used for debugging). atomId :: !(Nonce s tp) Unique identifier for atom. atomSource :: !(AtomSource s tp) How the atom expression was defined. typeOfAtom :: !(TypeRepr tp)

Instances

Instances details

TestEquality (Atom s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods testEquality :: forall (a :: CrucibleType) (b :: CrucibleType). Atom s a -> Atom s b -> Maybe (a :~: b) #
OrdF (Atom s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compareF :: forall (x :: CrucibleType) (y :: CrucibleType). Atom s x -> Atom s y -> OrderingF x y # leqF :: forall (x :: CrucibleType) (y :: CrucibleType). Atom s x -> Atom s y -> Bool # ltF :: forall (x :: CrucibleType) (y :: CrucibleType). Atom s x -> Atom s y -> Bool # geqF :: forall (x :: CrucibleType) (y :: CrucibleType). Atom s x -> Atom s y -> Bool # gtF :: forall (x :: CrucibleType) (y :: CrucibleType). Atom s x -> Atom s y -> Bool #
Show (Atom s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> Atom s tp -> ShowS # show :: Atom s tp -> String # showList :: [Atom s tp] -> ShowS #
Pretty (Atom s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: Atom s tp -> Doc ann # prettyList :: [Atom s tp] -> Doc ann #

newtype Label s Source #

A label for a block that does not expect an input.

Constructors

Label
Fields labelId :: Nonce s UnitType

Instances

Instances details

Show (Label s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> Label s -> ShowS # show :: Label s -> String # showList :: [Label s] -> ShowS #
Eq (Label s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods (==) :: Label s -> Label s -> Bool # (/=) :: Label s -> Label s -> Bool #
Ord (Label s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compare :: Label s -> Label s -> Ordering # (<) :: Label s -> Label s -> Bool # (<=) :: Label s -> Label s -> Bool # (>) :: Label s -> Label s -> Bool # (>=) :: Label s -> Label s -> Bool # max :: Label s -> Label s -> Label s # min :: Label s -> Label s -> Label s #
Pretty (Label s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: Label s -> Doc ann # prettyList :: [Label s] -> Doc ann #

data CFG ext s (init :: Ctx CrucibleType) (ret :: CrucibleType) Source #

A CFG using registers instead of SSA form.

Parameter ext is the syntax extension, s is a phantom type parameter identifying a particular CFG, init is the list of input types of the CFG, and ret is the return type.

Constructors

CFG
Fields cfgHandle :: !(FnHandle init ret) cfgEntryLabel :: !(Label s) cfgBlocks :: ![Block ext s ret]

Instances

Instances details

PrettyExt ext => Show (CFG ext s init ret) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> CFG ext s init ret -> ShowS # show :: CFG ext s init ret -> String # showList :: [CFG ext s init ret] -> ShowS #
PrettyExt ext => Pretty (CFG ext s init ret) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: CFG ext s init ret -> Doc ann # prettyList :: [CFG ext s init ret] -> Doc ann #

exprType :: forall (tp :: CrucibleType). IsExpr e => e tp -> TypeRepr tp Source #

data TermStmt s (ret :: CrucibleType) where Source #

Statement that terminates a basic block in a control flow graph.

Constructors

Jump :: forall s (ret :: CrucibleType). !(Label s) -> TermStmt s ret
Br :: forall s (ret :: CrucibleType). !(Atom s BoolType) -> !(Label s) -> !(Label s) -> TermStmt s ret
MaybeBranch :: forall (tp :: CrucibleType) s (ret :: CrucibleType). !(TypeRepr tp) -> !(Atom s (MaybeType tp)) -> !(LambdaLabel s tp) -> !(Label s) -> TermStmt s ret
VariantElim :: forall (varctx :: Ctx CrucibleType) s (ret :: CrucibleType). !(CtxRepr varctx) -> !(Atom s (VariantType varctx)) -> !(Assignment (LambdaLabel s) varctx) -> TermStmt s ret
Return :: forall s (ret :: CrucibleType). !(Atom s ret) -> TermStmt s ret
TailCall :: forall s (args :: Ctx CrucibleType) (ret :: CrucibleType). !(Atom s (FunctionHandleType args ret)) -> !(CtxRepr args) -> !(Assignment (Atom s) args) -> TermStmt s ret
ErrorStmt :: forall s (ret :: CrucibleType). !(Atom s (StringType Unicode)) -> TermStmt s ret
Output :: forall s (tp :: CrucibleType) (ret :: CrucibleType). !(LambdaLabel s tp) -> !(Atom s tp) -> TermStmt s ret

Instances

Instances details

Show (TermStmt s ret) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> TermStmt s ret -> ShowS # show :: TermStmt s ret -> String # showList :: [TermStmt s ret] -> ShowS #
Pretty (TermStmt s ret) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: TermStmt s ret -> Doc ann # prettyList :: [TermStmt s ret] -> Doc ann #

data Block ext s (ret :: CrucibleType) Source #

A basic block within a function.

Instances

Instances details

PrettyExt ext => Show (Block ext s ret) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> Block ext s ret -> ShowS # show :: Block ext s ret -> String # showList :: [Block ext s ret] -> ShowS #
Eq (Block ext s ret) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods (==) :: Block ext s ret -> Block ext s ret -> Bool # (/=) :: Block ext s ret -> Block ext s ret -> Bool #
Ord (Block ext s ret) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compare :: Block ext s ret -> Block ext s ret -> Ordering # (<) :: Block ext s ret -> Block ext s ret -> Bool # (<=) :: Block ext s ret -> Block ext s ret -> Bool # (>) :: Block ext s ret -> Block ext s ret -> Bool # (>=) :: Block ext s ret -> Block ext s ret -> Bool # max :: Block ext s ret -> Block ext s ret -> Block ext s ret # min :: Block ext s ret -> Block ext s ret -> Block ext s ret #
PrettyExt ext => Pretty (Block ext s ret) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: Block ext s ret -> Doc ann # prettyList :: [Block ext s ret] -> Doc ann #

data BlockID s where Source #

A label for a block is either a standard label, or a label expecting an input.

Constructors

LabelID :: forall s. Label s -> BlockID s
LambdaID :: forall s (tp :: CrucibleType). LambdaLabel s tp -> BlockID s

Instances

Instances details

Show (BlockID s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> BlockID s -> ShowS # show :: BlockID s -> String # showList :: [BlockID s] -> ShowS #
Eq (BlockID s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods (==) :: BlockID s -> BlockID s -> Bool # (/=) :: BlockID s -> BlockID s -> Bool #
Ord (BlockID s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compare :: BlockID s -> BlockID s -> Ordering # (<) :: BlockID s -> BlockID s -> Bool # (<=) :: BlockID s -> BlockID s -> Bool # (>) :: BlockID s -> BlockID s -> Bool # (>=) :: BlockID s -> BlockID s -> Bool # max :: BlockID s -> BlockID s -> BlockID s # min :: BlockID s -> BlockID s -> BlockID s #

data GlobalVar (tp :: CrucibleType) Source #

A global variable.

Constructors

GlobalVar
Fields globalNonce :: !(Nonce GlobalNonceGenerator tp) globalName :: !Text globalType :: !(TypeRepr tp)

Instances

Instances details

TestEquality GlobalVar Source #
Instance details Defined in Lang.Crucible.CFG.Common Methods testEquality :: forall (a :: CrucibleType) (b :: CrucibleType). GlobalVar a -> GlobalVar b -> Maybe (a :~: b) #
OrdF GlobalVar Source #
Instance details Defined in Lang.Crucible.CFG.Common Methods compareF :: forall (x :: CrucibleType) (y :: CrucibleType). GlobalVar x -> GlobalVar y -> OrderingF x y # leqF :: forall (x :: CrucibleType) (y :: CrucibleType). GlobalVar x -> GlobalVar y -> Bool # ltF :: forall (x :: CrucibleType) (y :: CrucibleType). GlobalVar x -> GlobalVar y -> Bool # geqF :: forall (x :: CrucibleType) (y :: CrucibleType). GlobalVar x -> GlobalVar y -> Bool # gtF :: forall (x :: CrucibleType) (y :: CrucibleType). GlobalVar x -> GlobalVar y -> Bool #
ShowF GlobalVar Source #
Instance details Defined in Lang.Crucible.CFG.Common Methods withShow :: forall p q (tp :: CrucibleType) a. p GlobalVar -> q tp -> (Show (GlobalVar tp) => a) -> a # showF :: forall (tp :: CrucibleType). GlobalVar tp -> String # showsPrecF :: forall (tp :: CrucibleType). Int -> GlobalVar tp -> String -> String #
Show (GlobalVar tp) Source #
Instance details Defined in Lang.Crucible.CFG.Common Methods showsPrec :: Int -> GlobalVar tp -> ShowS # show :: GlobalVar tp -> String # showList :: [GlobalVar tp] -> ShowS #
Pretty (GlobalVar tp) Source #
Instance details Defined in Lang.Crucible.CFG.Common Methods pretty :: GlobalVar tp -> Doc ann # prettyList :: [GlobalVar tp] -> Doc ann #

freshGlobalVar :: forall (tp :: CrucibleType). HandleAllocator -> Text -> TypeRepr tp -> IO (GlobalVar tp) Source #

newtype BreakpointName Source #

Constructors

BreakpointName
Fields breakpointNameText :: Text

Instances

Instances details

Show BreakpointName Source #
Instance details Defined in Lang.Crucible.CFG.Common Methods showsPrec :: Int -> BreakpointName -> ShowS # show :: BreakpointName -> String # showList :: [BreakpointName] -> ShowS #
Eq BreakpointName Source #
Instance details Defined in Lang.Crucible.CFG.Common Methods (==) :: BreakpointName -> BreakpointName -> Bool # (/=) :: BreakpointName -> BreakpointName -> Bool #
Ord BreakpointName Source #
Instance details Defined in Lang.Crucible.CFG.Common Methods compare :: BreakpointName -> BreakpointName -> Ordering # (<) :: BreakpointName -> BreakpointName -> Bool # (<=) :: BreakpointName -> BreakpointName -> Bool # (>) :: BreakpointName -> BreakpointName -> Bool # (>=) :: BreakpointName -> BreakpointName -> Bool # max :: BreakpointName -> BreakpointName -> BreakpointName # min :: BreakpointName -> BreakpointName -> BreakpointName #
Pretty BreakpointName Source #
Instance details Defined in Lang.Crucible.CFG.Common Methods pretty :: BreakpointName -> Doc ann # prettyList :: [BreakpointName] -> Doc ann #

data SomeCFG ext (init :: Ctx CrucibleType) (ret :: CrucibleType) Source #

SomeCFG is a CFG with an arbitrary parameter s.

Constructors

SomeCFG !(CFG ext s init ret)

cfgArgTypes :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType). CFG ext s init ret -> CtxRepr init Source #

cfgReturnType :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType). CFG ext s init ret -> TypeRepr ret Source #

data Reg s (tp :: CrucibleType) Source #

A mutable value in the control flow graph.

Constructors

Reg
Fields regPosition :: !Position Position where register was declared (used for debugging). regId :: !(Nonce s tp) Unique identifier for register. typeOfReg :: !(TypeRepr tp) Type of register.

Instances

Instances details

TestEquality (Reg s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods testEquality :: forall (a :: CrucibleType) (b :: CrucibleType). Reg s a -> Reg s b -> Maybe (a :~: b) #
OrdF (Reg s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compareF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg s x -> Reg s y -> OrderingF x y # leqF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg s x -> Reg s y -> Bool # ltF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg s x -> Reg s y -> Bool # geqF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg s x -> Reg s y -> Bool # gtF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg s x -> Reg s y -> Bool #
ShowF (Reg s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods withShow :: forall p q (tp :: CrucibleType) a. p (Reg s) -> q tp -> (Show (Reg s tp) => a) -> a # showF :: forall (tp :: CrucibleType). Reg s tp -> String # showsPrecF :: forall (tp :: CrucibleType). Int -> Reg s tp -> String -> String #
Show (Reg s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> Reg s tp -> ShowS # show :: Reg s tp -> String # showList :: [Reg s tp] -> ShowS #
Pretty (Reg s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: Reg s tp -> Doc ann # prettyList :: [Reg s tp] -> Doc ann #

cfgEntryBlock :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType). CFG ext s init ret -> Block ext s ret Source #

cfgInputTypes :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType). CFG ext s init ret -> CtxRepr init Source #

Deprecated: Use cfgArgTypes instead

substCFG :: forall m ext s s' (init :: Ctx CrucibleType) (ret :: CrucibleType). (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> CFG ext s init ret -> m (CFG ext s' init ret) Source #

Rename all the atoms, labels, and other named things in the CFG. Useful for rewriting, since the names can be generated from a nonce generator the client controls (and can thus keep using to generate fresh names).

substLabel :: Functor m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Label s -> m (Label s') Source #

data LambdaLabel s (tp :: CrucibleType) Source #

A label for a block that expects an argument of a specific type.

Constructors

LambdaLabel
Fields lambdaId :: !(Nonce s tp) Nonce that uniquely identifies this label within the CFG. lambdaAtom :: Atom s tp The atom to store the output result in. Note. This must be lazy to break a recursive cycle.

Instances

Instances details

TestEquality (LambdaLabel s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods testEquality :: forall (a :: CrucibleType) (b :: CrucibleType). LambdaLabel s a -> LambdaLabel s b -> Maybe (a :~: b) #
OrdF (LambdaLabel s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compareF :: forall (x :: CrucibleType) (y :: CrucibleType). LambdaLabel s x -> LambdaLabel s y -> OrderingF x y # leqF :: forall (x :: CrucibleType) (y :: CrucibleType). LambdaLabel s x -> LambdaLabel s y -> Bool # ltF :: forall (x :: CrucibleType) (y :: CrucibleType). LambdaLabel s x -> LambdaLabel s y -> Bool # geqF :: forall (x :: CrucibleType) (y :: CrucibleType). LambdaLabel s x -> LambdaLabel s y -> Bool # gtF :: forall (x :: CrucibleType) (y :: CrucibleType). LambdaLabel s x -> LambdaLabel s y -> Bool #
Show (LambdaLabel s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> LambdaLabel s tp -> ShowS # show :: LambdaLabel s tp -> String # showList :: [LambdaLabel s tp] -> ShowS #
Pretty (LambdaLabel s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: LambdaLabel s tp -> Doc ann # prettyList :: [LambdaLabel s tp] -> Doc ann #

substLambdaLabel :: forall m s s' (tp :: CrucibleType). Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> LambdaLabel s tp -> m (LambdaLabel s' tp) Source #

substBlockID :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> BlockID s -> m (BlockID s') Source #

substReg :: forall m s s' (tp :: CrucibleType). Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Reg s tp -> m (Reg s' tp) Source #

traverseCFG :: forall m ext genv penv s (ret :: CrucibleType) (init :: Ctx CrucibleType). (Monad m, TraverseExt ext) => (genv -> penv -> Block ext s ret -> m (genv, penv)) -> genv -> penv -> Block ext s ret -> CFG ext s init ret -> m genv Source #

Run a computation along all of the paths in a cfg, without taking backedges.

The computation has access to an environment that is specific to the current path being explored, as well as a global environment that is maintained across the entire computation.

substAtom :: forall m s s' (tp :: CrucibleType). Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Atom s tp -> m (Atom s' tp) Source #

data AtomSource s (tp :: CrucibleType) Source #

Identifies what generated an atom.

Constructors

Assigned
FnInput	Input argument to function. They are ordered before other inputs to a program.
LambdaArg !(LambdaLabel s tp)	Value passed into a lambda label. This must appear after other expressions.

substAtomSource :: forall m s s' (tp :: CrucibleType). Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> AtomSource s tp -> m (AtomSource s' tp) Source #

mkInputAtoms :: forall m s (init :: Ctx CrucibleType). Monad m => NonceGenerator m s -> Position -> CtxRepr init -> m (Assignment (Atom s) init) Source #

data AtomValue ext s (tp :: CrucibleType) where Source #

The value of an assigned atom.

Constructors

EvalApp :: forall ext s (tp :: CrucibleType). !(App ext (Atom s) tp) -> AtomValue ext s tp
ReadReg :: forall s (tp :: CrucibleType) ext. !(Reg s tp) -> AtomValue ext s tp
EvalExt :: forall ext s (tp :: CrucibleType). !(StmtExtension ext (Atom s) tp) -> AtomValue ext s tp
ReadGlobal :: forall (tp :: CrucibleType) ext s. !(GlobalVar tp) -> AtomValue ext s tp
ReadRef :: forall s (tp :: CrucibleType) ext. !(Atom s (ReferenceType tp)) -> AtomValue ext s tp
NewRef :: forall s (tp1 :: CrucibleType) ext. !(Atom s tp1) -> AtomValue ext s ('ReferenceType tp1)
NewEmptyRef :: forall (tp1 :: CrucibleType) ext s. !(TypeRepr tp1) -> AtomValue ext s ('ReferenceType tp1)
FreshConstant :: forall (bt :: BaseType) ext s. !(BaseTypeRepr bt) -> !(Maybe SolverSymbol) -> AtomValue ext s ('BaseToType bt)
FreshFloat :: forall (fi :: FloatInfo) ext s. !(FloatInfoRepr fi) -> !(Maybe SolverSymbol) -> AtomValue ext s ('FloatType fi)
FreshNat :: forall ext s. !(Maybe SolverSymbol) -> AtomValue ext s 'NatType
Call :: forall s (args :: Ctx CrucibleType) (tp :: CrucibleType) ext. !(Atom s (FunctionHandleType args tp)) -> !(Assignment (Atom s) args) -> !(TypeRepr tp) -> AtomValue ext s tp

Instances

Instances details

PrettyExt ext => Show (AtomValue ext s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods showsPrec :: Int -> AtomValue ext s tp -> ShowS # show :: AtomValue ext s tp -> String # showList :: [AtomValue ext s tp] -> ShowS #
PrettyExt ext => Pretty (AtomValue ext s tp) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: AtomValue ext s tp -> Doc ann # prettyList :: [AtomValue ext s tp] -> Doc ann #

typeOfAtomValue :: forall ext s (tp :: CrucibleType). (TypeApp (StmtExtension ext), TypeApp (ExprExtension ext)) => AtomValue ext s tp -> TypeRepr tp Source #

substAtomValue :: forall m ext s s' (tp :: CrucibleType). (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> AtomValue ext s tp -> m (AtomValue ext s' tp) Source #

typeOfValue :: forall s (tp :: CrucibleType). Value s tp -> TypeRepr tp Source #

substValue :: forall m s s' (tp :: CrucibleType). Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Value s tp -> m (Value s' tp) Source #

type ValueSet s = Set (Some (Value s)) Source #

A set of values.

substValueSet :: Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> ValueSet s -> m (ValueSet s') Source #

mkBlock Source #

Arguments

:: forall ext s (ret :: CrucibleType). TraverseExt ext
=> BlockID s
-> ValueSet s	Extra inputs to block (only non-empty for initial block)
-> Seq (Posd (Stmt ext s))
-> Posd (TermStmt s ret)
-> Block ext s ret

substBlock :: forall m ext s s' (ret :: CrucibleType). (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Block ext s ret -> m (Block ext s' ret) Source #

substStmt :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Stmt ext s -> m (Stmt ext s') Source #

substPosdStmt :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Posd (Stmt ext s) -> m (Posd (Stmt ext s')) Source #

mapStmtAtom :: (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Atom s x -> m (Atom s x)) -> Stmt ext s -> m (Stmt ext s) Source #

termStmtInputs :: forall s (ret :: CrucibleType). TermStmt s ret -> ValueSet s Source #

Returns the set of registers appearing as inputs to a terminal statement.

termNextLabels :: forall s (ret :: CrucibleType). TermStmt s ret -> Maybe [BlockID s] Source #

Returns the next labels for the given block. Error statements have no next labels, while return/tail call statements return Nothing.

substTermStmt :: forall m s s' (ret :: CrucibleType). Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> TermStmt s ret -> m (TermStmt s' ret) Source #

substPosdTermStmt :: forall m s s' (ret :: CrucibleType). Applicative m => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Posd (TermStmt s ret) -> m (Posd (TermStmt s' ret)) Source #

foldStmtInputs :: TraverseExt ext => (forall (x :: CrucibleType). Value s x -> b -> b) -> Stmt ext s -> b -> b Source #

Fold all registers that are inputs tostmt.

substExpr :: forall m ext s s' (tp :: CrucibleType). (Applicative m, TraverseExt ext) => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)) -> Expr ext s tp -> m (Expr ext s' tp) Source #

module Lang.Crucible.CFG.EarlyMergeLoops