Safe Haskell	Safe-Inferred
Language	Haskell2010

Lang.Crucible.Syntax.Concrete

Contents

Errors
Parsing and Results
Low level parsing operations
Rules for pretty-printing language syntax

Synopsis

data ExprErr s where
- TrivialErr :: Position -> ExprErr s
- Errs :: ExprErr s -> ExprErr s -> ExprErr s
- DuplicateAtom :: Position -> AtomName -> ExprErr s
- DuplicateLabel :: Position -> LabelName -> ExprErr s
- EmptyBlock :: Position -> ExprErr s
- NotGlobal :: Position -> AST s -> ExprErr s
- InvalidRegister :: Position -> AST s -> ExprErr s
- SyntaxParseError :: SyntaxError Atomic -> ExprErr s
data ParserHooks ext = ParserHooks {
- extensionTypeParser :: forall m. MonadSyntax Atomic m => m (Some TypeRepr)
- extensionParser :: forall s m. (MonadSyntax Atomic m, MonadWriter [Posd (Stmt ext s)] m, MonadState (SyntaxState s) m, MonadIO m, IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) => m (Some (Atom s))
}
data ParsedProgram ext = ParsedProgram {
- parsedProgGlobals :: Map GlobalName (Some GlobalVar)
- parsedProgExterns :: Map GlobalName (Some GlobalVar)
- parsedProgCFGs :: [AnyCFG ext]
- parsedProgForwardDecs :: Map FunctionName SomeHandle
}
defaultParserHooks :: ParserHooks ()
top :: NonceGenerator IO s -> HandleAllocator -> [(SomeHandle, Position)] -> TopParser s a -> IO (Either (ExprErr s) a)
cfgs :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) => [AST s] -> TopParser s [AnyCFG ext]
prog :: (TraverseExt ext, IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) => [AST s] -> TopParser s (ParsedProgram ext)
data SyntaxState s = SyntaxState {
- _stxLabels :: Map LabelName (LabelInfo s)
- _stxAtoms :: Map AtomName (Some (Atom s))
- _stxRegisters :: Map RegName (Some (Reg s))
- _stxNonceGen :: NonceGenerator IO s
- _stxProgState :: ProgramState s
}
atomName :: MonadSyntax Atomic m => m AtomName
freshAtom :: (MonadWriter [Posd (Stmt ext s)] m, MonadState (SyntaxState s) m, MonadIO m, IsSyntaxExtension ext) => Position -> AtomValue ext s t -> m (Atom s t)
nat :: MonadSyntax Atomic m => m Natural
string :: MonadSyntax Atomic m => m Text
isType :: (?parserHooks :: ParserHooks ext, MonadSyntax Atomic m) => m (Some TypeRepr)
operands :: forall s ext m tps. (MonadState (SyntaxState s) m, MonadWriter [Posd (Stmt ext s)] m, MonadIO m, MonadSyntax Atomic m, IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) => Assignment TypeRepr tps -> m (Assignment (Atom s) tps)
data BoundedNat bnd = forall w.bnd <= w => BoundedNat (NatRepr w)
type PosNat = BoundedNat 1
posNat :: MonadSyntax Atomic m => m PosNat
someAssign :: forall m ext a. (MonadSyntax Atomic m, ?parserHooks :: ParserHooks ext) => Text -> m (Some a) -> m (Some (Assignment a))
printExpr :: AST s -> Text

Errors

data ExprErr s where Source #

Constructors

TrivialErr :: Position -> ExprErr s
Errs :: ExprErr s -> ExprErr s -> ExprErr s
DuplicateAtom :: Position -> AtomName -> ExprErr s
DuplicateLabel :: Position -> LabelName -> ExprErr s
EmptyBlock :: Position -> ExprErr s
NotGlobal :: Position -> AST s -> ExprErr s
InvalidRegister :: Position -> AST s -> ExprErr s
SyntaxParseError :: SyntaxError Atomic -> ExprErr s

Instances

Instances details

Monoid (ExprErr s) Source #
Instance details Defined in Lang.Crucible.Syntax.Concrete Methods mempty :: ExprErr s # mappend :: ExprErr s -> ExprErr s -> ExprErr s # mconcat :: [ExprErr s] -> ExprErr s #
Semigroup (ExprErr s) Source #
Instance details Defined in Lang.Crucible.Syntax.Concrete Methods (<>) :: ExprErr s -> ExprErr s -> ExprErr s # sconcat :: NonEmpty (ExprErr s) -> ExprErr s # stimes :: Integral b => b -> ExprErr s -> ExprErr s #
Show (ExprErr s) Source #
Instance details Defined in Lang.Crucible.Syntax.Concrete Methods showsPrec :: Int -> ExprErr s -> ShowS # show :: ExprErr s -> String # showList :: [ExprErr s] -> ShowS #
Pretty (ExprErr s) Source #
Instance details Defined in Lang.Crucible.Syntax.Concrete Methods pretty :: ExprErr s -> Doc ann # prettyList :: [ExprErr s] -> Doc ann #

Parsing and Results

data ParserHooks ext Source #

ParserHooks enables support for arbitrary syntax extensions by allowing users to supply their own parsers for types and syntax extensions.

Constructors

ParserHooks

Fields

extensionTypeParser :: forall m. MonadSyntax Atomic m => m (Some TypeRepr)
extensionTypeParser is called for all type specifications and enables the addition of new types to crucible-syntax.
extensionParser :: forall s m. (MonadSyntax Atomic m, MonadWriter [Posd (Stmt ext s)] m, MonadState (SyntaxState s) m, MonadIO m, IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) => m (Some (Atom s))
extensionParser is called when parsing statements and let bindings (everywhere function calls are supported) and enables the addition of syntax extensions to crucible-syntax.

data ParsedProgram ext Source #

The results of parsing a program.

Constructors

ParsedProgram

Fields

parsedProgGlobals :: Map GlobalName (Some GlobalVar)
The parsed defglobals.
parsedProgExterns :: Map GlobalName (Some GlobalVar)
For each parsed extern, map its name to its global variable. It is the responsibility of the caller to insert each global variable into the SymGlobalState alongside an appropriate RegValue.
parsedProgCFGs :: [AnyCFG ext]
The CFGs for each parsed defun.
parsedProgForwardDecs :: Map FunctionName SomeHandle
For each parsed declare, map its name to its function handle. It is the responsibility of the caller to register each handle with an appropriate FnState.

defaultParserHooks :: ParserHooks () Source #

A ParserHooks instance that adds no extensions to the crucible-syntax language.

top :: NonceGenerator IO s -> HandleAllocator -> [(SomeHandle, Position)] -> TopParser s a -> IO (Either (ExprErr s) a) Source #

cfgs :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) => [AST s] -> TopParser s [AnyCFG ext] Source #

prog :: (TraverseExt ext, IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) => [AST s] -> TopParser s (ParsedProgram ext) Source #

Low level parsing operations

data SyntaxState s Source #

Constructors

SyntaxState
Fields _stxLabels :: Map LabelName (LabelInfo s) _stxAtoms :: Map AtomName (Some (Atom s)) _stxRegisters :: Map RegName (Some (Reg s)) _stxNonceGen :: NonceGenerator IO s _stxProgState :: ProgramState s

atomName :: MonadSyntax Atomic m => m AtomName Source #

freshAtom :: (MonadWriter [Posd (Stmt ext s)] m, MonadState (SyntaxState s) m, MonadIO m, IsSyntaxExtension ext) => Position -> AtomValue ext s t -> m (Atom s t) Source #

nat :: MonadSyntax Atomic m => m Natural Source #

string :: MonadSyntax Atomic m => m Text Source #

isType :: (?parserHooks :: ParserHooks ext, MonadSyntax Atomic m) => m (Some TypeRepr) Source #

operands Source #

Arguments

:: forall s ext m tps. (MonadState (SyntaxState s) m, MonadWriter [Posd (Stmt ext s)] m, MonadIO m, MonadSyntax Atomic m, IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext)
=> Assignment TypeRepr tps	Types of the operands
-> m (Assignment (Atom s) tps)	Atoms for the operands

Parse a list of operands (for example, the arguments to a function)

data BoundedNat bnd Source #

Constructors

forall w.bnd <= w => BoundedNat (NatRepr w)

type PosNat = BoundedNat 1 Source #

posNat :: MonadSyntax Atomic m => m PosNat Source #

someAssign :: forall m ext a. (MonadSyntax Atomic m, ?parserHooks :: ParserHooks ext) => Text -> m (Some a) -> m (Some (Assignment a)) Source #

Rules for pretty-printing language syntax

printExpr :: AST s -> Text Source #