Lang.Crucible.CFG.Expr

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.

App

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

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

TraversableFC (ExprExtension ext) => FoldableFC (App ext :: (CrucibleType -> Type) -> CrucibleType -> Type)

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)

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)

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)

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)

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)

Defined in Lang.Crucible.CFG.Expr

Methods

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

(TestEqualityFC (ExprExtension ext), TestEquality f) => TestEquality (App ext f :: CrucibleType -> Type)

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)

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)

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

Defined in Lang.Crucible.CFG.Expr

Methods

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

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

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

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)

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

Equality on booleans

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

Equality on integers

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

Equality on real numbers.

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

Equality on bitvectors

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

Return first or second value depending on condition.

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

Return first or second value depending on condition.

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

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

Return first or second value depending on condition.

Base terms

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

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

Constructors

BaseTerm

Fields

• baseTermType :: !(BaseTypeRepr tp)
• baseTermVal :: !(f (BaseToType tp))

Instances

FoldableFC BaseTerm

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

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

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

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

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)

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)

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

Enum RoundingMode

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

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

Defined in What4.Utils.FloatHelpers

Methods

showsPrec :: Int -> RoundingMode -> ShowS

show :: RoundingMode -> String

showList :: [RoundingMode] -> ShowS

Eq RoundingMode

Defined in What4.Utils.FloatHelpers

Methods

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

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

Ord RoundingMode

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

Defined in What4.Utils.FloatHelpers

Methods

hashWithSalt :: Int -> RoundingMode -> Int

hash :: RoundingMode -> Int

type Rep RoundingMode

Defined in What4.Utils.FloatHelpers

type Rep RoundingMode = D1 ('MetaData "RoundingMode" "What4.Utils.FloatHelpers" "what4-1.5.1-6GimHtONvd1LMJIg4FyjIh" '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)

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