Safe Haskell	Safe-Inferred
Language	Haskell2010

Lang.Crucible.Syntax.Atoms

Contents

The atom datatype
Individual atoms

Description

Atoms used by the Crucible CFG concrete syntax.

Synopsis

data Atomic
- = Kw !Keyword
- | Lbl !LabelName
- | At !AtomName
- | Rg !RegName
- | Gl !GlobalName
- | Fn !FunName
- | Int !Integer
- | Rat !Rational
- | Bool !Bool
- | StrLit !Text
atom :: Parser Atomic
newtype AtomName = AtomName Text
newtype LabelName = LabelName Text
newtype RegName = RegName Text
newtype FunName = FunName Text
newtype GlobalName = GlobalName Text
data Keyword
- = Defun
- | DefBlock
- | DefGlobal
- | Declare
- | Extern
- | Registers
- | Start
- | SetGlobal
- | SetRef
- | DropRef_
- | Plus
- | Minus
- | Times
- | Div
- | Negate
- | Abs
- | Just_
- | Nothing_
- | FromJust
- | Inj
- | Proj
- | AnyT
- | UnitT
- | BoolT
- | NatT
- | IntegerT
- | RealT
- | ComplexRealT
- | CharT
- | StringT
- | BitvectorT
- | VectorT
- | SequenceT
- | FPT
- | FunT
- | MaybeT
- | VariantT
- | StructT
- | RefT
- | Half_
- | Float_
- | Double_
- | Quad_
- | X86_80_
- | DoubleDouble_
- | Unicode_
- | Char8_
- | Char16_
- | The
- | Equalp
- | Integerp
- | If
- | Not_
- | And_
- | Or_
- | Xor_
- | Mod
- | Lt
- | Le
- | Show
- | StringConcat_
- | StringEmpty_
- | StringLength_
- | ToAny
- | FromAny
- | VectorLit_
- | VectorReplicate_
- | VectorIsEmpty_
- | VectorSize_
- | VectorGetEntry_
- | VectorSetEntry_
- | VectorCons_
- | MkStruct_
- | GetField_
- | SetField_
- | SequenceNil_
- | SequenceCons_
- | SequenceAppend_
- | SequenceIsNil_
- | SequenceLength_
- | SequenceHead_
- | SequenceTail_
- | SequenceUncons_
- | Deref
- | Ref
- | EmptyRef
- | Jump_
- | Return_
- | Branch_
- | MaybeBranch_
- | TailCall_
- | Error_
- | Output_
- | Case
- | Print_
- | PrintLn_
- | Let
- | Fresh
- | Assert_
- | Assume_
- | SetRegister
- | Funcall
- | Breakpoint_
- | BV
- | BVConcat_
- | BVSelect_
- | BVTrunc_
- | BVZext_
- | BVSext_
- | BVNonzero_
- | BoolToBV_
- | BVCarry_
- | BVSCarry_
- | BVSBorrow_
- | BVNot_
- | BVAnd_
- | BVOr_
- | BVXor_
- | BVShl_
- | BVLshr_
- | BVAshr_
- | Sle
- | Slt
- | Sdiv
- | Smod
- | ZeroExt
- | SignExt
- | RNE_
- | RNA_
- | RTP_
- | RTN_
- | RTZ_
- | FPToUBV_
- | FPToSBV_
- | UBVToFP_
- | SBVToFP_
- | BinaryToFP_
- | FPToBinary_
- | FPToReal_
- | RealToFP_

The atom datatype

data Atomic Source #

The atoms of the language

Constructors

Kw !Keyword	Keywords are all the built-in operators and expression formers
Lbl !LabelName	Labels, but not the trailing colon
At !AtomName	Atom names (which look like Scheme symbols)
Rg !RegName	Registers, whose names have a leading single $
Gl !GlobalName	Global variables, whose names have a leading double $$
Fn !FunName	Function names, minus the leading @
Int !Integer	Literal integers
Rat !Rational	Literal rational numbers
Bool !Bool	Literal Booleans
StrLit !Text	Literal strings

Instances

Instances details

Show Atomic Source #
Instance details Defined in Lang.Crucible.Syntax.Atoms Methods showsPrec :: Int -> Atomic -> ShowS # show :: Atomic -> String # showList :: [Atomic] -> ShowS #
IsAtom Atomic Source #
Instance details Defined in Lang.Crucible.Syntax.Atoms Methods showAtom :: Atomic -> Text Source #
Eq Atomic Source #
Instance details Defined in Lang.Crucible.Syntax.Atoms Methods (==) :: Atomic -> Atomic -> Bool # (/=) :: Atomic -> Atomic -> Bool #
Ord Atomic Source #
Instance details Defined in Lang.Crucible.Syntax.Atoms Methods compare :: Atomic -> Atomic -> Ordering # (<) :: Atomic -> Atomic -> Bool # (<=) :: Atomic -> Atomic -> Bool # (>) :: Atomic -> Atomic -> Bool # (>=) :: Atomic -> Atomic -> Bool # max :: Atomic -> Atomic -> Atomic # min :: Atomic -> Atomic -> Atomic #

atom :: Parser Atomic Source #

Parse an atom

Individual atoms

newtype AtomName Source #

The name of an atom (non-keyword identifier)

Constructors

AtomName Text

Instances

Instances details

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

newtype LabelName Source #

The name of a label (identifier followed by colon)

Constructors

LabelName Text

Instances

Instances details

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

newtype RegName Source #

The name of a register (dollar sign followed by identifier)

Constructors

RegName Text

Instances

Instances details

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

newtype FunName Source #

The name of a function (at-sign followed by identifier)

Constructors

FunName Text

Instances

Instances details

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

newtype GlobalName Source #

The name of a global variable (two dollar signs followed by identifier)

Constructors

GlobalName Text

Instances

Instances details

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

data Keyword Source #

Individual language keywords (reserved identifiers)

Constructors

Defun
DefBlock
DefGlobal
Declare
Extern
Registers
Start
SetGlobal
SetRef
DropRef_
Plus
Minus
Times
Div
Negate
Abs
Just_
Nothing_
FromJust
Inj
Proj
AnyT
UnitT
BoolT
NatT
IntegerT
RealT
ComplexRealT
CharT
StringT
BitvectorT
VectorT
SequenceT
FPT
FunT
MaybeT
VariantT
StructT
RefT
Half_
Float_
Double_
Quad_
X86_80_
DoubleDouble_
Unicode_
Char8_
Char16_
The
Equalp
Integerp
If
Not_
And_
Or_
Xor_
Mod
Lt
Le
Show
StringConcat_
StringEmpty_
StringLength_
ToAny
FromAny
VectorLit_
VectorReplicate_
VectorIsEmpty_
VectorSize_
VectorGetEntry_
VectorSetEntry_
VectorCons_
MkStruct_
GetField_
SetField_
SequenceNil_
SequenceCons_
SequenceAppend_
SequenceIsNil_
SequenceLength_
SequenceHead_
SequenceTail_
SequenceUncons_
Deref
Ref
EmptyRef
Jump_
Return_
Branch_
MaybeBranch_
TailCall_
Error_
Output_
Case
Print_
PrintLn_
Let
Fresh
Assert_
Assume_
SetRegister
Funcall
Breakpoint_
BV
BVConcat_
BVSelect_
BVTrunc_
BVZext_
BVSext_
BVNonzero_
BoolToBV_
BVCarry_
BVSCarry_
BVSBorrow_
BVNot_
BVAnd_
BVOr_
BVXor_
BVShl_
BVLshr_
BVAshr_
Sle
Slt
Sdiv
Smod
ZeroExt
SignExt
RNE_
RNA_
RTP_
RTN_
RTZ_
FPToUBV_
FPToSBV_
UBVToFP_
SBVToFP_
BinaryToFP_
FPToBinary_
FPToReal_
RealToFP_

Instances

Instances details

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