crucible-0.8.0.0: Crucible is a library for language-agnostic symbolic simulation
Copyright(c) Galois Inc 2014-2016
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Safe HaskellNone
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 (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 :: forall ext (f :: CrucibleType -> Type) (tp :: CrucibleType). !(ExprExtension ext f tp) -> App ext f tp 
BaseIsEq :: forall (tp1 :: BaseType) (f :: CrucibleType -> Type) ext. !(BaseTypeRepr tp1) -> !(f (BaseToType tp1)) -> !(f (BaseToType tp1)) -> App ext f ('BaseToType BaseBoolType)

Return true if two base types are equal.

BaseIte :: forall (tp1 :: BaseType) (f :: CrucibleType -> Type) ext. !(BaseTypeRepr tp1) -> !(f BoolType) -> !(f (BaseToType tp1)) -> !(f (BaseToType tp1)) -> App ext f ('BaseToType tp1)

Select one or other

EmptyApp :: forall ext (f :: CrucibleType -> Type). App ext f 'UnitType 
PackAny :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(f tp1) -> App ext f 'AnyType 
UnpackAny :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(f AnyType) -> App ext f ('MaybeType tp1) 
BoolLit :: forall ext (f :: CrucibleType -> Type). !Bool -> App ext f ('BaseToType BaseBoolType) 
Not :: forall (f :: CrucibleType -> Type) ext. !(f BoolType) -> App ext f ('BaseToType BaseBoolType) 
And :: forall (f :: CrucibleType -> Type) ext. !(f BoolType) -> !(f BoolType) -> App ext f ('BaseToType BaseBoolType) 
Or :: forall (f :: CrucibleType -> Type) ext. !(f BoolType) -> !(f BoolType) -> App ext f ('BaseToType BaseBoolType) 
BoolXor :: forall (f :: CrucibleType -> Type) ext. !(f BoolType) -> !(f BoolType) -> App ext f ('BaseToType BaseBoolType) 
NatLit :: forall ext (f :: CrucibleType -> Type). !Natural -> App ext f 'NatType 
NatEq :: forall (f :: CrucibleType -> Type) ext. !(f NatType) -> !(f NatType) -> App ext f ('BaseToType BaseBoolType) 
NatIte :: forall (f :: CrucibleType -> Type) ext. !(f BoolType) -> !(f NatType) -> !(f NatType) -> App ext f 'NatType 
NatLt :: forall (f :: CrucibleType -> Type) ext. !(f NatType) -> !(f NatType) -> App ext f ('BaseToType BaseBoolType) 
NatLe :: forall (f :: CrucibleType -> Type) ext. !(f NatType) -> !(f NatType) -> App ext f ('BaseToType BaseBoolType) 
NatAdd :: forall (f :: CrucibleType -> Type) ext. !(f NatType) -> !(f NatType) -> App ext f 'NatType 
NatSub :: forall (f :: CrucibleType -> Type) ext. !(f NatType) -> !(f NatType) -> App ext f 'NatType 
NatMul :: forall (f :: CrucibleType -> Type) ext. !(f NatType) -> !(f NatType) -> App ext f 'NatType 
NatDiv :: forall (f :: CrucibleType -> Type) ext. !(f NatType) -> !(f NatType) -> App ext f 'NatType 
NatMod :: forall (f :: CrucibleType -> Type) ext. !(f NatType) -> !(f NatType) -> App ext f 'NatType 
IntLit :: forall ext (f :: CrucibleType -> Type). !Integer -> App ext f ('BaseToType BaseIntegerType) 
IntLt :: forall (f :: CrucibleType -> Type) ext. !(f IntegerType) -> !(f IntegerType) -> App ext f ('BaseToType BaseBoolType) 
IntLe :: forall (f :: CrucibleType -> Type) ext. !(f IntegerType) -> !(f IntegerType) -> App ext f ('BaseToType BaseBoolType) 
IntNeg :: forall (f :: CrucibleType -> Type) ext. !(f IntegerType) -> App ext f ('BaseToType BaseIntegerType) 
IntAdd :: forall (f :: CrucibleType -> Type) ext. !(f IntegerType) -> !(f IntegerType) -> App ext f ('BaseToType BaseIntegerType) 
IntSub :: forall (f :: CrucibleType -> Type) ext. !(f IntegerType) -> !(f IntegerType) -> App ext f ('BaseToType BaseIntegerType) 
IntMul :: forall (f :: CrucibleType -> Type) ext. !(f IntegerType) -> !(f IntegerType) -> App ext f ('BaseToType BaseIntegerType) 
IntDiv :: forall (f :: CrucibleType -> Type) ext. !(f IntegerType) -> !(f IntegerType) -> App ext f ('BaseToType BaseIntegerType) 
IntMod :: forall (f :: CrucibleType -> Type) ext. !(f IntegerType) -> !(f IntegerType) -> App ext f ('BaseToType BaseIntegerType) 
IntAbs :: forall (f :: CrucibleType -> Type) ext. !(f IntegerType) -> App ext f ('BaseToType BaseIntegerType) 
RationalLit :: forall ext (f :: CrucibleType -> Type). !Rational -> App ext f ('BaseToType BaseRealType) 
RealLt :: forall (f :: CrucibleType -> Type) ext. !(f RealValType) -> !(f RealValType) -> App ext f ('BaseToType BaseBoolType) 
RealLe :: forall (f :: CrucibleType -> Type) ext. !(f RealValType) -> !(f RealValType) -> App ext f ('BaseToType BaseBoolType) 
RealNeg :: forall (f :: CrucibleType -> Type) ext. !(f RealValType) -> App ext f ('BaseToType BaseRealType) 
RealAdd :: forall (f :: CrucibleType -> Type) ext. !(f RealValType) -> !(f RealValType) -> App ext f ('BaseToType BaseRealType) 
RealSub :: forall (f :: CrucibleType -> Type) ext. !(f RealValType) -> !(f RealValType) -> App ext f ('BaseToType BaseRealType) 
RealMul :: forall (f :: CrucibleType -> Type) ext. !(f RealValType) -> !(f RealValType) -> App ext f ('BaseToType BaseRealType) 
RealDiv :: forall (f :: CrucibleType -> Type) ext. !(f RealValType) -> !(f RealValType) -> App ext f ('BaseToType BaseRealType) 
RealMod :: forall (f :: CrucibleType -> Type) ext. !(f RealValType) -> !(f RealValType) -> App ext f ('BaseToType BaseRealType) 
RealIsInteger :: forall (f :: CrucibleType -> Type) ext. !(f RealValType) -> App ext f ('BaseToType BaseBoolType) 
FloatUndef :: forall (fi :: FloatInfo) ext (f :: CrucibleType -> Type). !(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 :: forall ext (f :: CrucibleType -> Type). !Float -> App ext f ('FloatType SingleFloat) 
DoubleLit :: forall ext (f :: CrucibleType -> Type). !Double -> App ext f ('FloatType DoubleFloat) 
X86_80Lit :: forall ext (f :: CrucibleType -> Type). !X86_80Val -> App ext f ('FloatType X86_80Float) 
FloatNaN :: forall (fi :: FloatInfo) ext (f :: CrucibleType -> Type). !(FloatInfoRepr fi) -> App ext f ('FloatType fi) 
FloatPInf :: forall (fi :: FloatInfo) ext (f :: CrucibleType -> Type). !(FloatInfoRepr fi) -> App ext f ('FloatType fi) 
FloatNInf :: forall (fi :: FloatInfo) ext (f :: CrucibleType -> Type). !(FloatInfoRepr fi) -> App ext f ('FloatType fi) 
FloatPZero :: forall (fi :: FloatInfo) ext (f :: CrucibleType -> Type). !(FloatInfoRepr fi) -> App ext f ('FloatType fi) 
FloatNZero :: forall (fi :: FloatInfo) ext (f :: CrucibleType -> Type). !(FloatInfoRepr fi) -> App ext f ('FloatType fi) 
FloatNeg :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. !(FloatInfoRepr fi) -> !(f (FloatType fi)) -> App ext f ('FloatType fi) 
FloatAbs :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. !(FloatInfoRepr fi) -> !(f (FloatType fi)) -> App ext f ('FloatType fi) 
FloatSqrt :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. !(FloatInfoRepr fi) -> !RoundingMode -> !(f (FloatType fi)) -> App ext f ('FloatType fi) 
FloatAdd :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. !(FloatInfoRepr fi) -> !RoundingMode -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('FloatType fi) 
FloatSub :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. !(FloatInfoRepr fi) -> !RoundingMode -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('FloatType fi) 
FloatMul :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. !(FloatInfoRepr fi) -> !RoundingMode -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('FloatType fi) 
FloatDiv :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. !(FloatInfoRepr fi) -> !RoundingMode -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('FloatType fi) 
FloatRem :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. !(FloatInfoRepr fi) -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('FloatType fi) 
FloatMin :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. !(FloatInfoRepr fi) -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('FloatType fi) 
FloatMax :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. !(FloatInfoRepr fi) -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('FloatType fi) 
FloatFMA :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. !(FloatInfoRepr fi) -> !RoundingMode -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('FloatType fi) 
FloatEq :: forall (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('BaseToType BaseBoolType) 
FloatFpEq :: forall (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('BaseToType BaseBoolType) 
FloatGt :: forall (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('BaseToType BaseBoolType) 
FloatGe :: forall (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('BaseToType BaseBoolType) 
FloatLt :: forall (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('BaseToType BaseBoolType) 
FloatLe :: forall (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('BaseToType BaseBoolType) 
FloatNe :: forall (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('BaseToType BaseBoolType) 
FloatFpApart :: forall (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('BaseToType BaseBoolType) 
FloatIte :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. !(FloatInfoRepr fi) -> !(f BoolType) -> !(f (FloatType fi)) -> !(f (FloatType fi)) -> App ext f ('FloatType fi) 
FloatCast :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) (fi' :: FloatInfo) ext. !(FloatInfoRepr fi) -> !RoundingMode -> !(f (FloatType fi')) -> App ext f ('FloatType fi) 
FloatFromBinary :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. !(FloatInfoRepr fi) -> !(f (BVType (FloatInfoToBitWidth fi))) -> App ext f ('FloatType fi) 
FloatToBinary :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. 1 <= FloatInfoToBitWidth fi => !(FloatInfoRepr fi) -> !(f (FloatType fi)) -> App ext f ('BaseToType (BaseBVType (FloatInfoToBitWidth fi))) 
FloatFromBV :: forall (w :: Natural) (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. 1 <= w => !(FloatInfoRepr fi) -> !RoundingMode -> !(f (BVType w)) -> App ext f ('FloatType fi) 
FloatFromSBV :: forall (w :: Natural) (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. 1 <= w => !(FloatInfoRepr fi) -> !RoundingMode -> !(f (BVType w)) -> App ext f ('FloatType fi) 
FloatFromReal :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. !(FloatInfoRepr fi) -> !RoundingMode -> !(f RealValType) -> App ext f ('FloatType fi) 
FloatToBV :: forall (w :: Natural) (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. 1 <= w => !(NatRepr w) -> !RoundingMode -> !(f (FloatType fi)) -> App ext f ('BaseToType (BaseBVType w)) 
FloatToSBV :: forall (w :: Natural) (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. 1 <= w => !(NatRepr w) -> !RoundingMode -> !(f (FloatType fi)) -> App ext f ('BaseToType (BaseBVType w)) 
FloatToReal :: forall (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. !(f (FloatType fi)) -> App ext f ('BaseToType BaseRealType) 
FloatIsNaN :: forall (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. !(f (FloatType fi)) -> App ext f ('BaseToType BaseBoolType) 
FloatIsInfinite :: forall (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. !(f (FloatType fi)) -> App ext f ('BaseToType BaseBoolType) 
FloatIsZero :: forall (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. !(f (FloatType fi)) -> App ext f ('BaseToType BaseBoolType) 
FloatIsPositive :: forall (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. !(f (FloatType fi)) -> App ext f ('BaseToType BaseBoolType) 
FloatIsNegative :: forall (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. !(f (FloatType fi)) -> App ext f ('BaseToType BaseBoolType) 
FloatIsSubnormal :: forall (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. !(f (FloatType fi)) -> App ext f ('BaseToType BaseBoolType) 
FloatIsNormal :: forall (f :: CrucibleType -> Type) (fi :: FloatInfo) ext. !(f (FloatType fi)) -> App ext f ('BaseToType BaseBoolType) 
JustValue :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(f tp1) -> App ext f ('MaybeType tp1) 
NothingValue :: forall (tp1 :: CrucibleType) ext (f :: CrucibleType -> Type). !(TypeRepr tp1) -> App ext f ('MaybeType tp1) 
FromJustValue :: forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp) -> !(f (MaybeType tp)) -> !(f (StringType Unicode)) -> App ext f tp 
RollRecursive :: forall (nm :: Symbol) (ctx :: Ctx CrucibleType) (f :: CrucibleType -> Type) ext. IsRecursiveType nm => !(SymbolRepr nm) -> !(CtxRepr ctx) -> !(f (UnrollType nm ctx)) -> App ext f ('RecursiveType nm ctx) 
UnrollRecursive :: forall (nm :: Symbol) (ctx :: Ctx CrucibleType) (f :: CrucibleType -> Type) ext. IsRecursiveType nm => !(SymbolRepr nm) -> !(CtxRepr ctx) -> !(f (RecursiveType nm ctx)) -> App ext f (UnrollType nm ctx) 
SequenceNil :: forall (tp1 :: CrucibleType) ext (f :: CrucibleType -> Type). !(TypeRepr tp1) -> App ext f ('SequenceType tp1) 
SequenceCons :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(f tp1) -> !(f (SequenceType tp1)) -> App ext f ('SequenceType tp1) 
SequenceAppend :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(f (SequenceType tp1)) -> !(f (SequenceType tp1)) -> App ext f ('SequenceType tp1) 
SequenceIsNil :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(f (SequenceType tp1)) -> App ext f ('BaseToType BaseBoolType) 
SequenceLength :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(f (SequenceType tp1)) -> App ext f 'NatType 
SequenceHead :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(f (SequenceType tp1)) -> App ext f ('MaybeType tp1) 
SequenceTail :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(f (SequenceType tp1)) -> App ext f ('MaybeType (SequenceType tp1)) 
SequenceUncons :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(f (SequenceType tp1)) -> App ext f ('MaybeType (StructType (((EmptyCtx :: Ctx CrucibleType) ::> tp1) ::> SequenceType tp1))) 
VectorLit :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(Vector (f tp1)) -> App ext f ('VectorType tp1) 
VectorReplicate :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(f NatType) -> !(f tp1) -> App ext f ('VectorType tp1) 
VectorIsEmpty :: forall (f :: CrucibleType -> Type) (tp1 :: CrucibleType) ext. !(f (VectorType tp1)) -> App ext f ('BaseToType BaseBoolType) 
VectorSize :: forall (f :: CrucibleType -> Type) (tp1 :: CrucibleType) ext. !(f (VectorType tp1)) -> App ext f 'NatType 
VectorGetEntry :: forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp) -> !(f (VectorType tp)) -> !(f NatType) -> App ext f tp 
VectorSetEntry :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(f (VectorType tp1)) -> !(f NatType) -> !(f tp1) -> App ext f ('VectorType tp1) 
VectorCons :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(f tp1) -> !(f (VectorType tp1)) -> App ext f ('VectorType tp1) 
HandleLit :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType) ext (f :: CrucibleType -> Type). !(FnHandle args ret) -> App ext f ('FunctionHandleType args ret) 
Closure :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType) (f :: CrucibleType -> Type) (tp1 :: CrucibleType) ext. !(CtxRepr args) -> !(TypeRepr ret) -> !(f (FunctionHandleType (args ::> tp1) ret)) -> !(TypeRepr tp1) -> !(f tp1) -> App ext f ('FunctionHandleType args ret) 
NatToInteger :: forall (f :: CrucibleType -> Type) ext. !(f NatType) -> App ext f ('BaseToType BaseIntegerType) 
IntegerToReal :: forall (f :: CrucibleType -> Type) ext. !(f IntegerType) -> App ext f ('BaseToType BaseRealType) 
RealRound :: forall (f :: CrucibleType -> Type) ext. !(f RealValType) -> App ext f ('BaseToType BaseIntegerType) 
RealFloor :: forall (f :: CrucibleType -> Type) ext. !(f RealValType) -> App ext f ('BaseToType BaseIntegerType) 
RealCeil :: forall (f :: CrucibleType -> Type) ext. !(f RealValType) -> App ext f ('BaseToType BaseIntegerType) 
IntegerToBV :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => NatRepr w -> !(f IntegerType) -> App ext f ('BaseToType (BaseBVType w)) 
RealToNat :: forall (f :: CrucibleType -> Type) ext. !(f RealValType) -> App ext f 'NatType 
Complex :: forall (f :: CrucibleType -> Type) ext. !(f RealValType) -> !(f RealValType) -> App ext f ('BaseToType BaseComplexType) 
RealPart :: forall (f :: CrucibleType -> Type) ext. !(f ComplexRealType) -> App ext f ('BaseToType BaseRealType) 
ImagPart :: forall (f :: CrucibleType -> Type) ext. !(f ComplexRealType) -> App ext f ('BaseToType BaseRealType) 
BVUndef :: forall (w :: Natural) ext (f :: CrucibleType -> Type). 1 <= w => NatRepr w -> App ext f ('BaseToType (BaseBVType w))

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

BVLit :: forall (w :: Natural) ext (f :: CrucibleType -> Type). 1 <= w => NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w)) 
BVConcat :: forall (u :: Natural) (v :: Natural) (f :: CrucibleType -> Type) ext. (1 <= u, 1 <= v, 1 <= (u + v)) => !(NatRepr u) -> !(NatRepr v) -> !(f (BVType u)) -> !(f (BVType v)) -> App ext f ('BaseToType (BaseBVType (u + v))) 
BVSelect :: forall (w :: Natural) (len :: Natural) (idx :: Natural) (f :: CrucibleType -> Type) ext. (1 <= w, 1 <= len, (idx + len) <= w) => !(NatRepr idx) -> !(NatRepr len) -> !(NatRepr w) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType len)) 
BVTrunc :: forall (r :: Natural) (w :: Natural) (f :: CrucibleType -> Type) ext. (1 <= r, (r + 1) <= w) => !(NatRepr r) -> !(NatRepr w) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType r)) 
BVZext :: forall (w :: Natural) (r :: Natural) (f :: CrucibleType -> Type) ext. (1 <= w, 1 <= r, (w + 1) <= r) => !(NatRepr r) -> !(NatRepr w) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType r)) 
BVSext :: forall (w :: Natural) (r :: Natural) (f :: CrucibleType -> Type) ext. (1 <= w, 1 <= r, (w + 1) <= r) => !(NatRepr r) -> !(NatRepr w) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType r)) 
BVNot :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVAnd :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVOr :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVXor :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVNeg :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVAdd :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVSub :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVMul :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVUdiv :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVSdiv :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType 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 :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVSrem :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVUle :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType BaseBoolType) 
BVUlt :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType BaseBoolType) 
BVSle :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType BaseBoolType) 
BVSlt :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType BaseBoolType) 
BVCarry :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType BaseBoolType) 
BVSCarry :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType BaseBoolType) 
BVSBorrow :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType BaseBoolType) 
BVShl :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVLshr :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVAshr :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVRol :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVRor :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVCountLeadingZeros :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVCountTrailingZeros :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVPopcount :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVUMin :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVUMax :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVSMin :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BVSMax :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> !(f (BVType w)) -> App ext f ('BaseToType (BaseBVType w)) 
BoolToBV :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f BoolType) -> App ext f ('BaseToType (BaseBVType w)) 
BvToInteger :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f ('BaseToType BaseIntegerType) 
SbvToInteger :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f ('BaseToType BaseIntegerType) 
BvToNat :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f 'NatType 
BVNonzero :: forall (w :: Natural) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(f (BVType w)) -> App ext f ('BaseToType BaseBoolType) 
EmptyWordMap :: forall (w :: Natural) (tp1 :: BaseType) ext (f :: CrucibleType -> Type). 1 <= w => !(NatRepr w) -> !(BaseTypeRepr tp1) -> App ext f ('WordMapType w tp1) 
InsertWordMap :: forall (w :: Natural) (tp1 :: BaseType) (f :: CrucibleType -> Type) ext. 1 <= w => !(NatRepr w) -> !(BaseTypeRepr tp1) -> !(f (BVType w)) -> !(f (BaseToType tp1)) -> !(f (WordMapType w tp1)) -> App ext f ('WordMapType w tp1) 
LookupWordMap :: forall (w :: Natural) (tp1 :: BaseType) (f :: CrucibleType -> Type) ext. 1 <= w => !(BaseTypeRepr tp1) -> !(f (BVType w)) -> !(f (WordMapType w tp1)) -> App ext f ('BaseToType tp1) 
LookupWordMapWithDefault :: forall (w :: Natural) (tp1 :: BaseType) (f :: CrucibleType -> Type) ext. 1 <= w => !(BaseTypeRepr tp1) -> !(f (BVType w)) -> !(f (WordMapType w tp1)) -> !(f (BaseToType tp1)) -> App ext f ('BaseToType tp1) 
InjectVariant :: forall (ctx :: Ctx CrucibleType) (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(CtxRepr ctx) -> !(Index ctx tp1) -> !(f tp1) -> App ext f ('VariantType ctx) 
ProjectVariant :: forall (ctx :: Ctx CrucibleType) (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(CtxRepr ctx) -> !(Index ctx tp1) -> !(f (VariantType ctx)) -> App ext f ('MaybeType tp1) 
MkStruct :: forall (ctx :: Ctx CrucibleType) (f :: CrucibleType -> Type) ext. !(CtxRepr ctx) -> !(Assignment f ctx) -> App ext f ('StructType ctx) 
GetStruct :: forall (f :: CrucibleType -> Type) (ctx :: Ctx CrucibleType) (tp :: CrucibleType) ext. !(f (StructType ctx)) -> !(Index ctx tp) -> !(TypeRepr tp) -> App ext f tp 
SetStruct :: forall (ctx :: Ctx CrucibleType) (f :: CrucibleType -> Type) (tp1 :: CrucibleType) ext. !(CtxRepr ctx) -> !(f (StructType ctx)) -> !(Index ctx tp1) -> !(f tp1) -> App ext f ('StructType ctx) 
EmptyStringMap :: forall (tp1 :: CrucibleType) ext (f :: CrucibleType -> Type). !(TypeRepr tp1) -> App ext f ('StringMapType tp1) 
LookupStringMapEntry :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(f (StringMapType tp1)) -> !(f (StringType Unicode)) -> App ext f ('MaybeType tp1) 
InsertStringMapEntry :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(f (StringMapType tp1)) -> !(f (StringType Unicode)) -> !(f (MaybeType tp1)) -> App ext f ('StringMapType tp1) 
StringLit :: forall (si :: StringInfo) ext (f :: CrucibleType -> Type). !(StringLiteral si) -> App ext f ('BaseToType (BaseStringType si)) 
StringEmpty :: forall (si :: StringInfo) ext (f :: CrucibleType -> Type). !(StringInfoRepr si) -> App ext f ('BaseToType (BaseStringType si)) 
StringConcat :: forall (si :: StringInfo) (f :: CrucibleType -> Type) ext. !(StringInfoRepr si) -> !(f (StringType si)) -> !(f (StringType si)) -> App ext f ('BaseToType (BaseStringType si)) 
StringLength :: forall (f :: CrucibleType -> Type) (si :: StringInfo) ext. !(f (StringType si)) -> App ext f ('BaseToType BaseIntegerType) 
StringContains :: forall (f :: CrucibleType -> Type) (si :: StringInfo) ext. !(f (StringType si)) -> !(f (StringType si)) -> App ext f ('BaseToType BaseBoolType) 
StringIsPrefixOf :: forall (f :: CrucibleType -> Type) (si :: StringInfo) ext. !(f (StringType si)) -> !(f (StringType si)) -> App ext f ('BaseToType BaseBoolType) 
StringIsSuffixOf :: forall (f :: CrucibleType -> Type) (si :: StringInfo) ext. !(f (StringType si)) -> !(f (StringType si)) -> App ext f ('BaseToType BaseBoolType) 
StringIndexOf :: forall (f :: CrucibleType -> Type) (si :: StringInfo) ext. !(f (StringType si)) -> !(f (StringType si)) -> !(f IntegerType) -> App ext f ('BaseToType BaseIntegerType) 
StringSubstring :: forall (si :: StringInfo) (f :: CrucibleType -> Type) ext. !(StringInfoRepr si) -> !(f (StringType si)) -> !(f IntegerType) -> !(f IntegerType) -> App ext f ('BaseToType (BaseStringType si)) 
ShowValue :: forall (bt :: BaseType) (f :: CrucibleType -> Type) ext. !(BaseTypeRepr bt) -> !(f (BaseToType bt)) -> App ext f ('BaseToType (BaseStringType Unicode)) 
ShowFloat :: forall (fi :: FloatInfo) (f :: CrucibleType -> Type) ext. !(FloatInfoRepr fi) -> !(f (FloatType fi)) -> App ext f ('BaseToType (BaseStringType Unicode)) 
SymArrayLookup :: forall (b :: BaseType) (f :: CrucibleType -> Type) (idx :: Ctx BaseType) (tp1 :: BaseType) ext. !(BaseTypeRepr b) -> !(f (SymbolicArrayType (idx ::> tp1) b)) -> !(Assignment (BaseTerm f) (idx ::> tp1)) -> App ext f ('BaseToType b) 
SymArrayUpdate :: forall (b :: BaseType) (f :: CrucibleType -> Type) (idx :: Ctx BaseType) (itp :: BaseType) ext. !(BaseTypeRepr b) -> !(f (SymbolicArrayType (idx ::> itp) b)) -> !(Assignment (BaseTerm f) (idx ::> itp)) -> !(f (BaseToType b)) -> App ext f ('BaseToType (BaseArrayType (idx ::> itp) b)) 
IsConcrete :: forall (b :: BaseType) (f :: CrucibleType -> Type) ext. !(BaseTypeRepr b) -> f (BaseToType b) -> App ext f ('BaseToType BaseBoolType) 
ReferenceEq :: forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext. !(TypeRepr tp1) -> !(f (ReferenceType tp1)) -> !(f (ReferenceType tp1)) -> App ext f ('BaseToType BaseBoolType) 

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 :: CrucibleType). f x -> m) -> forall (x :: CrucibleType). App ext f x -> m #

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

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

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

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

toListFC :: (forall (x :: CrucibleType). f x -> a) -> forall (x :: CrucibleType). 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 :: CrucibleType). f x -> g x) -> forall (x :: CrucibleType). 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 :: CrucibleType) (y :: CrucibleType). f x -> f y -> OrderingF x y) -> forall (x :: CrucibleType) (y :: CrucibleType). 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 :: CrucibleType) (y :: CrucibleType). f x -> f y -> Maybe (x :~: y)) -> forall (x :: CrucibleType) (y :: CrucibleType). 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 :: CrucibleType). f x -> m (g x)) -> forall (x :: CrucibleType). 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 :: CrucibleType). f x -> Doc ann) -> forall (x :: CrucibleType). 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 :: CrucibleType) (b :: CrucibleType). 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 :: CrucibleType) (y :: CrucibleType). App ext f x -> App ext f y -> OrderingF x y #

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

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

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

gtF :: forall (x :: CrucibleType) (y :: CrucibleType). 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 :: forall ext f g (tp :: CrucibleType). TraversableFC (ExprExtension ext) => (forall (u :: CrucibleType). 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 :: forall ext f r (tp :: CrucibleType). TraversableFC (ExprExtension ext) => (forall (x :: CrucibleType). f x -> r -> r) -> r -> App ext f tp -> r Source #

Fold over an application.

traverseApp :: forall ext m f g (tp :: CrucibleType). (TraversableFC (ExprExtension ext), Applicative m) => (forall (u :: CrucibleType). 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 :: forall tp f ext. () => tp ~ BoolType => f BoolType -> f BoolType -> App ext f tp Source #

Equality on booleans

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

Equality on integers

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

Equality on real numbers.

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

Equality on bitvectors

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

Return first or second value depending on condition.

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

Return first or second value depending on condition.

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

Return first or second number depending on condition.

pattern BVIte :: forall tp f ext (w :: Natural). () => (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 :: BaseType) 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 :: CrucibleType). f x -> m) -> forall (x :: BaseType). BaseTerm f x -> m #

foldrFC :: (forall (x :: CrucibleType). f x -> b -> b) -> forall (x :: BaseType). b -> BaseTerm f x -> b #

foldlFC :: forall f b. (forall (x :: CrucibleType). b -> f x -> b) -> forall (x :: BaseType). b -> BaseTerm f x -> b #

foldrFC' :: (forall (x :: CrucibleType). f x -> b -> b) -> forall (x :: BaseType). b -> BaseTerm f x -> b #

foldlFC' :: forall f b. (forall (x :: CrucibleType). b -> f x -> b) -> forall (x :: BaseType). b -> BaseTerm f x -> b #

toListFC :: (forall (x :: CrucibleType). f x -> a) -> forall (x :: BaseType). BaseTerm f x -> [a] #

FunctorFC BaseTerm Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

fmapFC :: (forall (x :: CrucibleType). f x -> g x) -> forall (x :: BaseType). BaseTerm f x -> BaseTerm g x #

OrdFC BaseTerm Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

compareFC :: (forall (x :: CrucibleType) (y :: CrucibleType). f x -> f y -> OrderingF x y) -> forall (x :: BaseType) (y :: BaseType). BaseTerm f x -> BaseTerm f y -> OrderingF x y #

TestEqualityFC BaseTerm Source # 
Instance details

Defined in Lang.Crucible.CFG.Expr

Methods

testEqualityFC :: (forall (x :: CrucibleType) (y :: CrucibleType). f x -> f y -> Maybe (x :~: y)) -> forall (x :: BaseType) (y :: BaseType). 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 :: CrucibleType). f x -> m (g x)) -> forall (x :: BaseType). 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 :: BaseType) (b :: BaseType). 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 :: BaseType) (y :: BaseType). BaseTerm f x -> BaseTerm f y -> OrderingF x y #

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

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

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

gtF :: forall (x :: BaseType) (y :: BaseType). 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 
Instance details

Defined in What4.Utils.FloatHelpers

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

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.1.0-KrjMxsEbDaT7jOAWCf7ZTf" '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 {k} f (tp :: k). (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> Vector (f tp) -> Vector (f tp) -> Maybe (Int :~: Int) Source #

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