crucible-0.7.2: Crucible is a library for language-agnostic symbolic simulation
Copyright(c) Galois Inc 2014-2016
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Safe HaskellSafe-Inferred
LanguageHaskell2010

Lang.Crucible.CFG.Expr

Description

Define the syntax of Crucible expressions. Expressions represent side-effect free computations that result in terms. The same expression language is used both for registerized CFGs (Lang.Crucible.CFG.Reg) and for the core SSA-form CFGs (Lang.Crucible.CFG.Core).

Evaluation of expressions is defined in module Lang.Crucible.Simulator.Evaluation.

Synopsis

App

data App (ext :: Type) (f :: CrucibleType -> Type) (tp :: CrucibleType) where Source #

The main Crucible expression datastructure, defined as a multisorted algebra. Type App ext f tp encodes the top-level application of a Crucible expression. The parameter ext is used to indicate which syntax extension is being used via the ExprExtension type family. The type parameter tp is a type index that indicates the Crucible type of the values denoted by the given expression form. Parameter f is used everywhere a recursive sub-expression would go. Uses of the App type will tie the knot through this parameter.

Constructors

ExtensionApp :: !(ExprExtension ext f tp) -> App ext f tp 
BaseIsEq :: !(BaseTypeRepr tp) -> !(f (BaseToType tp)) -> !(f (BaseToType tp)) -> App ext f BoolType

Return true if two base types are equal.

BaseIte :: !(BaseTypeRepr tp) -> !(f BoolType) -> !(f (BaseToType tp)) -> !(f (BaseToType tp)) -> App ext f (BaseToType tp)

Select one or other

EmptyApp :: App ext f UnitType 
PackAny :: !(TypeRepr tp) -> !(f tp) -> App ext f AnyType 
UnpackAny :: !(TypeRepr tp) -> !(f AnyType) -> App ext f (MaybeType tp) 
BoolLit :: !Bool -> App ext f BoolType 
Not :: !(f BoolType) -> App ext f BoolType 
And :: !(f BoolType) -> !(f BoolType) -> App ext f BoolType 
Or :: !(f BoolType) -> !(f BoolType) -> App ext f BoolType 
BoolXor :: !(f BoolType) -> !(f BoolType) -> App ext f BoolType 
NatLit :: !Natural -> App ext f NatType 
NatEq :: !(f NatType) -> !(f NatType) -> App ext f BoolType 
NatIte :: !(f BoolType) -> !(f NatType) -> !(f NatType) -> App ext f NatType 
NatLt :: !(f NatType) -> !(f NatType) -> App ext f BoolType 
NatLe :: !(f NatType) -> !(f NatType) -> App ext f BoolType 
NatAdd :: !(f NatType) -> !(f NatType) -> App ext f NatType 
NatSub :: !(f NatType) -> !(f NatType) -> App ext f NatType 
NatMul :: !(f NatType) -> !(f NatType) -> App ext f NatType 
NatDiv :: !(f NatType) -> !(f NatType) -> App ext f NatType 
NatMod :: !(f NatType) -> !(f NatType) -> App ext f NatType 
IntLit :: !Integer -> App ext f IntegerType 
IntLt :: !(f IntegerType) -> !(f IntegerType) -> App ext f BoolType 
IntLe :: !(f IntegerType) -> !(f IntegerType) -> App ext f BoolType 
IntNeg :: !(f IntegerType) -> App ext f IntegerType 
IntAdd :: !(f IntegerType) -> !(f IntegerType) -> App ext f IntegerType 
IntSub :: !(f IntegerType) -> !(f IntegerType) -> App ext f IntegerType 
IntMul :: !(f IntegerType) -> !(f IntegerType) -> App ext f IntegerType 
IntDiv :: !(f IntegerType) -> !(f IntegerType) -> App ext f IntegerType 
IntMod :: !(f IntegerType) -> !(f IntegerType) -> App ext f IntegerType 
IntAbs :: !(f IntegerType) -> App ext f IntegerType 
RationalLit :: !Rational -> App ext f RealValType 
RealLt :: !(f RealValType) -> !(f RealValType) -> App ext f BoolType 
RealLe :: !(f RealValType) -> !(f RealValType) -> App ext f BoolType 
RealNeg :: !(f RealValType) -> App ext f RealValType 
RealAdd :: !(f RealValType) -> !(f RealValType) -> App ext f RealValType 
RealSub :: !(f RealValType) -> !(f RealValType) -> App ext f RealValType 
RealMul :: !(f RealValType) -> !(f RealValType) -> App ext f RealValType 
RealDiv :: !(f RealValType) -> !(f RealValType) -> App ext f RealValType 
RealMod :: !(f RealValType) -> !(f RealValType) -> App ext f RealValType 
RealIsInteger :: !(f RealValType) -> App ext f BoolType 
FloatUndef :: !(FloatInfoRepr fi) -> App ext f (FloatType fi)

Generate an "undefined" float value. The semantics of this construct are still under discussion, see crucible#366.

FloatLit :: !Float -> App ext f (FloatType SingleFloat) 
DoubleLit :: !Double -> App ext f (FloatType DoubleFloat) 
X86_80Lit :: !X86_80Val -> App ext f (FloatType X86_80Float) 
FloatNaN :: !(FloatInfoRepr fi) -> App ext f (FloatType fi) 
FloatPInf :: !(FloatInfoRepr fi) -> App ext f (FloatType fi) 
FloatNInf :: !(FloatInfoRepr fi) -> App ext f (FloatType fi) 
FloatPZero :: !(FloatInfoRepr fi) -> App ext f (FloatType fi) 
FloatNZero :: !(FloatInfoRepr fi) -> App ext f (FloatType fi) 
FloatNeg :: !(FloatInfoRepr fi) -> !(f (FloatType fi)) -> App ext f (FloatType fi) 
FloatAbs :: !(FloatInfoRepr fi) -> !(f (FloatType fi)) -> App ext f (FloatType fi) 
FloatSqrt :: !(FloatInfoRepr fi) -> !RoundingMode -> !(f (FloatType fi)) -> App ext f (FloatType fi) 
FloatAdd :: !(FloatInfoRepr fi) -> !RoundingMode -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f (FloatType fi) 
FloatSub :: !(FloatInfoRepr fi) -> !RoundingMode -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f (FloatType fi) 
FloatMul :: !(FloatInfoRepr fi) -> !RoundingMode -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f (FloatType fi) 
FloatDiv :: !(FloatInfoRepr fi) -> !RoundingMode -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f (FloatType fi) 
FloatRem :: !(FloatInfoRepr fi) -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f (FloatType fi) 
FloatMin :: !(FloatInfoRepr fi) -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f (FloatType fi) 
FloatMax :: !(FloatInfoRepr fi) -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f (FloatType fi) 
FloatFMA :: !(FloatInfoRepr fi) -> !RoundingMode -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f (FloatType fi) 
FloatEq :: !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f BoolType 
FloatFpEq :: !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f BoolType 
FloatGt :: !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f BoolType 
FloatGe :: !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f BoolType 
FloatLt :: !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f BoolType 
FloatLe :: !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f BoolType 
FloatNe :: !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f BoolType 
FloatFpApart :: !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f BoolType 
FloatIte :: !(FloatInfoRepr fi) -> !(f BoolType) -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f (FloatType fi) 
FloatCast :: !(FloatInfoRepr fi) -> !RoundingMode -> !(f (FloatType fi')) -> App ext f (FloatType fi) 
FloatFromBinary :: !(FloatInfoRepr fi) -> !(f (BVType (FloatInfoToBitWidth fi))) -> App ext f (FloatType fi) 
FloatToBinary :: 1 <= FloatInfoToBitWidth fi => !(FloatInfoRepr fi) -> !(f (FloatType fi)) -> App ext f (BVType (FloatInfoToBitWidth fi)) 
FloatFromBV :: 1 <= w => !(FloatInfoRepr fi) -> !RoundingMode -> !(f (BVType w)) -> App ext f (FloatType fi) 
FloatFromSBV :: 1 <= w => !(FloatInfoRepr fi) -> !RoundingMode -> !(f (BVType w)) -> App ext f (FloatType fi) 
FloatFromReal :: !(FloatInfoRepr fi) -> !RoundingMode -> !(f RealValType) -> App ext f (FloatType fi) 
FloatToBV :: 1 <= w => !(NatRepr w) -> !RoundingMode -> !(f (FloatType fi)) -> App ext f (BVType w) 
FloatToSBV :: 1 <= w => !(NatRepr w) -> !RoundingMode -> !(f (FloatType fi)) -> App ext f (BVType w) 
FloatToReal :: !(f (FloatType fi)) -> App ext f RealValType 
FloatIsNaN :: !(f (FloatType fi)) -> App ext f BoolType 
FloatIsInfinite :: !(f (FloatType fi)) -> App ext f BoolType 
FloatIsZero :: !(f (FloatType fi)) -> App ext f BoolType 
FloatIsPositive :: !(f (FloatType fi)) -> App ext f BoolType 
FloatIsNegative :: !(f (FloatType fi)) -> App ext f BoolType 
FloatIsSubnormal :: !(f (FloatType fi)) -> App ext f BoolType 
FloatIsNormal :: !(f (FloatType fi)) -> App ext f BoolType 
JustValue :: !(TypeRepr tp) -> !(f tp) -> App ext f (MaybeType tp) 
NothingValue :: !(TypeRepr tp) -> App ext f (MaybeType tp) 
FromJustValue :: !(TypeRepr tp) -> !(f (MaybeType tp)) -> !(f (StringType Unicode)) -> App ext f tp 
RollRecursive :: IsRecursiveType nm => !(SymbolRepr nm) -> !(CtxRepr ctx) -> !(f (UnrollType nm ctx)) -> App ext f (RecursiveType nm ctx) 
UnrollRecursive :: IsRecursiveType nm => !(SymbolRepr nm) -> !(CtxRepr ctx) -> !(f (RecursiveType nm ctx)) -> App ext f (UnrollType nm ctx) 
SequenceNil :: !(TypeRepr tp) -> App ext f (SequenceType tp) 
SequenceCons :: !(TypeRepr tp) -> !(f tp) -> !(f (SequenceType tp)) -> App ext f (SequenceType tp) 
SequenceAppend :: !(TypeRepr tp) -> !(f (SequenceType tp)) -> !(f (SequenceType tp)) -> App ext f (SequenceType tp) 
SequenceIsNil :: !(TypeRepr tp) -> !(f (SequenceType tp)) -> App ext f BoolType 
SequenceLength :: !(TypeRepr tp) -> !(f (SequenceType tp)) -> App ext f NatType 
SequenceHead :: !(TypeRepr tp) -> !(f (SequenceType tp)) -> App ext f (MaybeType tp) 
SequenceTail :: !(TypeRepr tp) -> !(f (SequenceType tp)) -> App ext f (MaybeType (SequenceType tp)) 
SequenceUncons :: !(TypeRepr tp) -> !(f (SequenceType tp)) -> App ext f (MaybeType (StructType ((EmptyCtx ::> tp) ::> SequenceType tp))) 
VectorLit :: !(TypeRepr tp) -> !(Vector (f tp)) -> App ext f (VectorType tp) 
VectorReplicate :: !(TypeRepr tp) -> !(f NatType) -> !(f tp) -> App ext f (VectorType tp) 
VectorIsEmpty :: !(f (VectorType tp)) -> App ext f BoolType 
VectorSize :: !(f (VectorType tp)) -> App ext f NatType 
VectorGetEntry :: !(TypeRepr tp) -> !(f (VectorType tp)) -> !(f NatType) -> App ext f tp 
VectorSetEntry :: !(TypeRepr tp) -> !(f (VectorType tp)) -> !(f NatType) -> !(f tp) -> App ext f (VectorType tp) 
VectorCons :: !(TypeRepr tp) -> !(f tp) -> !(f (VectorType tp)) -> App ext f (VectorType tp) 
HandleLit :: !(FnHandle args ret) -> App ext f (FunctionHandleType args ret) 
Closure :: !(CtxRepr args) -> !(TypeRepr ret) -> !(f (FunctionHandleType (args ::> tp) ret)) -> !(TypeRepr tp) -> !(f tp) -> App ext f (FunctionHandleType args ret) 
NatToInteger :: !(f NatType) -> App ext f IntegerType 
IntegerToReal :: !(f IntegerType) -> App ext f RealValType 
RealRound :: !(f RealValType) -> App ext f IntegerType 
RealFloor :: !(f RealValType) -> App ext f IntegerType 
RealCeil :: !(f RealValType) -> App ext f IntegerType 
IntegerToBV :: 1 <= w => NatRepr w -> !(f IntegerType) -> App ext f (BVType w) 
RealToNat :: !(f RealValType) -> App ext f NatType 
Complex :: !(f RealValType) -> !(f RealValType) -> App ext f ComplexRealType 
RealPart :: !(f ComplexRealType) -> App ext f RealValType 
ImagPart :: !(f ComplexRealType) -> App ext f RealValType 
BVUndef :: 1 <= w => NatRepr w -> App ext f (BVType w)

Generate an "undefined" bitvector value. The semantics of this construct are still under discussion, see crucible#366.

BVLit :: 1 <= w => NatRepr w -> BV w -> App ext f (BVType w) 
BVConcat :: (1 <= u, 1 <= v, 1 <= (u + v)) => !(NatRepr u) -> !(NatRepr v) -> !(f (BVType u)) -> !(f (BVType v)) -> App ext f (BVType (u + v)) 
BVSelect :: (1 <= w, 1 <= len, (idx + len) <= w) => !(NatRepr idx) -> !(NatRepr len) -> !(NatRepr w) -> !(f (BVType w)) -> App ext f (BVType len) 
BVTrunc :: (1 <= r, (r + 1) <= w) => !(NatRepr r) -> !(NatRepr w) -> !(f (BVType w)) -> App ext f (BVType r) 
BVZext :: (1 <= w, 1 <= r, (w + 1) <= r) => !(NatRepr r) -> !(NatRepr w) -> !(f (BVType w)) -> App ext f (BVType r) 
BVSext :: (1 <= w, 1 <= r, (w + 1) <= r) => !(NatRepr r) -> !(NatRepr w) -> !(f (BVType w)) -> App ext f (BVType r) 
BVNot :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f (BVType w) 
BVAnd :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVOr :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVXor :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVNeg :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f (BVType w) 
BVAdd :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVSub :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVMul :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVUdiv :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVSdiv :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w)

This performs signed division. The result is truncated to zero.

TODO: Document semantics when divisor is zero and case of minSigned w / -1 = minSigned w.

BVUrem :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVSrem :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVUle :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f BoolType 
BVUlt :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f BoolType 
BVSle :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f BoolType 
BVSlt :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f BoolType 
BVCarry :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f BoolType 
BVSCarry :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f BoolType 
BVSBorrow :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f BoolType 
BVShl :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVLshr :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVAshr :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVRol :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVRor :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVCountLeadingZeros :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f (BVType w) 
BVCountTrailingZeros :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f (BVType w) 
BVPopcount :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f (BVType w) 
BVUMin :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVUMax :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVSMin :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BVSMax :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f (BVType w) 
BoolToBV :: 1 <= w => !(NatRepr w) -> !(f BoolType) -> App ext f (BVType w) 
BvToInteger :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f IntegerType 
SbvToInteger :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f IntegerType 
BvToNat :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f NatType 
BVNonzero :: 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f BoolType 
EmptyWordMap :: 1 <= w => !(NatRepr w) -> !(BaseTypeRepr tp) -> App ext f (WordMapType w tp) 
InsertWordMap :: 1 <= w => !(NatRepr w) -> !(BaseTypeRepr tp) -> !(f (BVType w)) -> !(f (BaseToType tp)) -> !(f (WordMapType w tp)) -> App ext f (WordMapType w tp) 
LookupWordMap :: 1 <= w => !(BaseTypeRepr tp) -> !(f (BVType w)) -> !(f (WordMapType w tp)) -> App ext f (BaseToType tp) 
LookupWordMapWithDefault :: 1 <= w => !(BaseTypeRepr tp) -> !(f (BVType w)) -> !(f (WordMapType w tp)) -> !(f (BaseToType tp)) -> App ext f (BaseToType tp) 
InjectVariant :: !(CtxRepr ctx) -> !(Index ctx tp) -> !(f tp) -> App ext f (VariantType ctx) 
ProjectVariant :: !(CtxRepr ctx) -> !(Index ctx tp) -> !(f (VariantType ctx)) -> App ext f (MaybeType tp) 
MkStruct :: !(CtxRepr ctx) -> !(Assignment f ctx) -> App ext f (StructType ctx) 
GetStruct :: !(f (StructType ctx)) -> !(Index ctx tp) -> !(TypeRepr tp) -> App ext f tp 
SetStruct :: !(CtxRepr ctx) -> !(f (StructType ctx)) -> !(Index ctx tp) -> !(f tp) -> App ext f (StructType ctx) 
EmptyStringMap :: !(TypeRepr tp) -> App ext f (StringMapType tp) 
LookupStringMapEntry :: !(TypeRepr tp) -> !(f (StringMapType tp)) -> !(f (StringType Unicode)) -> App ext f (MaybeType tp) 
InsertStringMapEntry :: !(TypeRepr tp) -> !(f (StringMapType tp)) -> !(f (StringType Unicode)) -> !(f (MaybeType tp)) -> App ext f (StringMapType tp) 
StringLit :: !(StringLiteral si) -> App ext f (StringType si) 
StringEmpty :: !(StringInfoRepr si) -> App ext f (StringType si) 
StringConcat :: !(StringInfoRepr si) -> !(f (StringType si)) -> !(f (StringType si)) -> App ext f (StringType si) 
StringLength :: !(f (StringType si)) -> App ext f IntegerType 
StringContains :: !(f (StringType si)) -> !(f (StringType si)) -> App ext f BoolType 
StringIsPrefixOf :: !(f (StringType si)) -> !(f (StringType si)) -> App ext f BoolType 
StringIsSuffixOf :: !(f (StringType si)) -> !(f (StringType si)) -> App ext f BoolType 
StringIndexOf :: !(f (StringType si)) -> !(f (StringType si)) -> !(f IntegerType) -> App ext f IntegerType 
StringSubstring :: !(StringInfoRepr si) -> !(f (StringType si)) -> !(f IntegerType) -> !(f IntegerType) -> App ext f (StringType si) 
ShowValue :: !(BaseTypeRepr bt) -> !(f (BaseToType bt)) -> App ext f (StringType Unicode) 
ShowFloat :: !(FloatInfoRepr fi) -> !(f (FloatType fi)) -> App ext f (StringType Unicode) 
SymArrayLookup :: !(BaseTypeRepr b) -> !(f (SymbolicArrayType (idx ::> tp) b)) -> !(Assignment (BaseTerm f) (idx ::> tp)) -> App ext f (BaseToType b) 
SymArrayUpdate :: !(BaseTypeRepr b) -> !(f (SymbolicArrayType (idx ::> itp) b)) -> !(Assignment (BaseTerm f) (idx ::> itp)) -> !(f (BaseToType b)) -> App ext f (SymbolicArrayType (idx ::> itp) b) 
IsConcrete :: !(BaseTypeRepr b) -> f (BaseToType b) -> App ext f BoolType 
ReferenceEq :: !(TypeRepr tp) -> !(f (ReferenceType tp)) -> !(f (ReferenceType tp)) -> App ext f BoolType 

Instances

Instances details
TraversableFC (ExprExtension ext) => FoldableFC (App ext :: (CrucibleType -> Type) -> CrucibleType -> Type) Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

foldMapFC :: forall f m. Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). App ext f x -> m #

foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> App ext f x -> b #

foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> App ext f x -> b #

foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> App ext f x -> b #

foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> App ext f x -> b #

toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). App ext f x -> [a] #

TraversableFC (ExprExtension ext) => FunctorFC (App ext :: (CrucibleType -> Type) -> CrucibleType -> Type) Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: l). App ext f x -> App ext g x #

OrdFC (ExprExtension ext) => OrdFC (App ext :: (CrucibleType -> Type) -> CrucibleType -> Type) Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: l) (y :: l). App ext f x -> App ext f y -> OrderingF x y #

TestEqualityFC (ExprExtension ext) => TestEqualityFC (App ext :: (CrucibleType -> Type) -> CrucibleType -> Type) Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

testEqualityFC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: l) (y :: l). App ext f x -> App ext f y -> Maybe (x :~: y) #

TraversableFC (ExprExtension ext) => TraversableFC (App ext :: (CrucibleType -> Type) -> CrucibleType -> Type) Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

traverseFC :: forall f g m. Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: l). App ext f x -> m (App ext g x) #

PrettyApp (ExprExtension ext) => PrettyApp (App ext :: (CrucibleType -> Type) -> CrucibleType -> Type) Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

ppApp :: (forall (x :: k). f x -> Doc ann) -> forall (x :: k). App ext f x -> Doc ann Source #

(TestEqualityFC (ExprExtension ext), TestEquality f) => TestEquality (App ext f :: CrucibleType -> Type) Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

testEquality :: forall (a :: k) (b :: k). App ext f a -> App ext f b -> Maybe (a :~: b) #

(OrdFC (ExprExtension ext), OrdF f) => OrdF (App ext f :: CrucibleType -> Type) Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

compareF :: forall (x :: k) (y :: k). App ext f x -> App ext f y -> OrderingF x y #

leqF :: forall (x :: k) (y :: k). App ext f x -> App ext f y -> Bool #

ltF :: forall (x :: k) (y :: k). App ext f x -> App ext f y -> Bool #

geqF :: forall (x :: k) (y :: k). App ext f x -> App ext f y -> Bool #

gtF :: forall (x :: k) (y :: k). App ext f x -> App ext f y -> Bool #

TypeApp (ExprExtension ext) => TypeApp (App ext) Source #

Compute a run-time representation of the type of an application.

Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

appType :: forall (f :: CrucibleType -> Type) (x :: CrucibleType). App ext f x -> TypeRepr x Source #

mapApp :: TraversableFC (ExprExtension ext) => (forall u. f u -> g u) -> App ext f tp -> App ext g tp Source #

Map a Crucible-type-preserving function over the immediate subterms of an application.

foldApp :: TraversableFC (ExprExtension ext) => (forall x. f x -> r -> r) -> r -> App ext f tp -> r Source #

Fold over an application.

traverseApp :: forall ext m f g tp. (TraversableFC (ExprExtension ext), Applicative m) => (forall u. f u -> m (g u)) -> App ext f tp -> m (App ext g tp) Source #

Traversal that performs the given action on each immediate subterm of an application. Used for the TraversableFC instance.

pattern BoolEq :: () => tp ~ BoolType => f BoolType -> f BoolType -> App ext f tp Source #

Equality on booleans

pattern IntEq :: () => tp ~ BoolType => f IntegerType -> f IntegerType -> App ext f tp Source #

Equality on integers

pattern RealEq :: () => tp ~ BoolType => f RealValType -> f RealValType -> App ext f tp Source #

Equality on real numbers.

pattern BVEq :: () => (1 <= w, tp ~ BoolType) => NatRepr w -> f (BVType w) -> f (BVType w) -> App ext f tp Source #

Equality on bitvectors

pattern BoolIte :: () => tp ~ BoolType => f BoolType -> f tp -> f tp -> App ext f tp Source #

Return first or second value depending on condition.

pattern IntIte :: () => tp ~ IntegerType => f BoolType -> f tp -> f tp -> App ext f tp Source #

Return first or second value depending on condition.

pattern RealIte :: () => tp ~ RealValType => f BoolType -> f tp -> f tp -> App ext f tp Source #

Return first or second number depending on condition.

pattern BVIte :: () => (1 <= w, tp ~ BVType w) => f BoolType -> NatRepr w -> f tp -> f tp -> App ext f tp Source #

Return first or second value depending on condition.

Base terms

data BaseTerm (f :: CrucibleType -> Type) tp Source #

Base terms represent the subset of expressions of base types, packaged together with a run-time representation of their type.

Constructors

BaseTerm 

Fields

Instances

Instances details
FoldableFC BaseTerm Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

foldMapFC :: forall f m. Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). BaseTerm f x -> m #

foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> BaseTerm f x -> b #

foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> BaseTerm f x -> b #

foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> BaseTerm f x -> b #

foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> BaseTerm f x -> b #

toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). BaseTerm f x -> [a] #

FunctorFC BaseTerm Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: l). BaseTerm f x -> BaseTerm g x #

OrdFC BaseTerm Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: l) (y :: l). BaseTerm f x -> BaseTerm f y -> OrderingF x y #

TestEqualityFC BaseTerm Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

testEqualityFC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: l) (y :: l). BaseTerm f x -> BaseTerm f y -> Maybe (x :~: y) #

TraversableFC BaseTerm Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

traverseFC :: forall f g m. Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: l). BaseTerm f x -> m (BaseTerm g x) #

TestEquality f => TestEquality (BaseTerm f :: BaseType -> Type) Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

testEquality :: forall (a :: k) (b :: k). BaseTerm f a -> BaseTerm f b -> Maybe (a :~: b) #

OrdF f => OrdF (BaseTerm f :: BaseType -> Type) Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

compareF :: forall (x :: k) (y :: k). BaseTerm f x -> BaseTerm f y -> OrderingF x y #

leqF :: forall (x :: k) (y :: k). BaseTerm f x -> BaseTerm f y -> Bool #

ltF :: forall (x :: k) (y :: k). BaseTerm f x -> BaseTerm f y -> Bool #

geqF :: forall (x :: k) (y :: k). BaseTerm f x -> BaseTerm f y -> Bool #

gtF :: forall (x :: k) (y :: k). BaseTerm f x -> BaseTerm f y -> Bool #

module Lang.Crucible.CFG.Extension

data RoundingMode #

Rounding modes for IEEE-754 floating point operations.

Constructors

RNE

Round to nearest even.

RNA

Round to nearest away.

RTP

Round toward plus Infinity.

RTN

Round toward minus Infinity.

RTZ

Round toward zero.

Instances

Instances details
Enum RoundingMode 
Instance details

Defined in What4.Utils.FloatHelpers

Methods

succ :: RoundingMode -> RoundingMode #

pred :: RoundingMode -> RoundingMode #

toEnum :: Int -> RoundingMode #

fromEnum :: RoundingMode -> Int #

enumFrom :: RoundingMode -> [RoundingMode] #

enumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode] #

enumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode] #

enumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode] #

Generic RoundingMode 
Instance details

Defined in What4.Utils.FloatHelpers

Associated Types

type Rep RoundingMode :: Type -> Type #

Methods

from :: RoundingMode -> Rep RoundingMode x #

to :: Rep RoundingMode x -> RoundingMode #

Show RoundingMode 
Instance details

Defined in What4.Utils.FloatHelpers

Methods

showsPrec :: Int -> RoundingMode -> ShowS #

show :: RoundingMode -> String #

showList :: [RoundingMode] -> ShowS #

Eq RoundingMode 
Instance details

Defined in What4.Utils.FloatHelpers

Methods

(==) :: RoundingMode -> RoundingMode -> Bool #

(/=) :: RoundingMode -> RoundingMode -> Bool #

Ord RoundingMode 
Instance details

Defined in What4.Utils.FloatHelpers

Methods

compare :: RoundingMode -> RoundingMode -> Ordering #

(<) :: RoundingMode -> RoundingMode -> Bool #

(<=) :: RoundingMode -> RoundingMode -> Bool #

(>) :: RoundingMode -> RoundingMode -> Bool #

(>=) :: RoundingMode -> RoundingMode -> Bool #

max :: RoundingMode -> RoundingMode -> RoundingMode #

min :: RoundingMode -> RoundingMode -> RoundingMode #

Hashable RoundingMode 
Instance details

Defined in What4.Utils.FloatHelpers

Methods

hashWithSalt :: Int -> RoundingMode -> Int #

hash :: RoundingMode -> Int #

type Rep RoundingMode 
Instance details

Defined in What4.Utils.FloatHelpers

type Rep RoundingMode = D1 ('MetaData "RoundingMode" "What4.Utils.FloatHelpers" "what4-1.7-5R8ssY552NP21GNgdZ6Cou" 'False) ((C1 ('MetaCons "RNE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RNA" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RTP" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "RTN" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RTZ" 'PrefixI 'False) (U1 :: Type -> Type))))

testVector :: (forall x y. f x -> f y -> Maybe (x :~: y)) -> Vector (f tp) -> Vector (f tp) -> Maybe (Int :~: Int) Source #

compareVector :: forall f tp. (forall x y. f x -> f y -> OrderingF x y) -> Vector (f tp) -> Vector (f tp) -> OrderingF Int Int Source #