| Copyright | (c) Galois Inc 2016-2020 |
|---|---|
| License | BSD3 |
| Maintainer | Joe Hendrix <jhendrix@galois.com> |
| Safe Haskell | None |
| Language | Haskell2010 |
What4.Expr.MATLAB
Contents
Description
This module provides an interface that a symbolic backend should implement to support MATLAB intrinsics.
Synopsis
- data MatlabSolverFn (f :: BaseType -> Type) args ret where
- BoolOrFn :: MatlabSolverFn f ((EmptyCtx ::> BaseBoolType) ::> BaseBoolType) BaseBoolType
- IsIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType
- IntLeFn :: MatlabSolverFn f ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType) BaseBoolType
- BVToIntegerFn :: 1 <= w => !(NatRepr w) -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
- SBVToIntegerFn :: 1 <= w => !(NatRepr w) -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
- IntegerToRealFn :: MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType
- RealToIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseIntegerType
- PredToIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType
- IntSeqFn :: !(f BaseIntegerType) -> !(f BaseIntegerType) -> MatlabSolverFn f ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType) BaseIntegerType
- RealSeqFn :: !(f BaseRealType) -> !(f BaseRealType) -> MatlabSolverFn f ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType) BaseRealType
- IndicesInRange :: !(Assignment OnlyIntRepr (idx ::> itp)) -> !(Assignment f (idx ::> itp)) -> MatlabSolverFn f (idx ::> itp) BaseBoolType
- IsEqFn :: !(BaseTypeRepr tp) -> MatlabSolverFn f ((EmptyCtx ::> tp) ::> tp) BaseBoolType
- BVIsNonZeroFn :: 1 <= w => !(NatRepr w) -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseBoolType
- ClampedIntNegFn :: 1 <= w => !(NatRepr w) -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType w)
- ClampedIntAbsFn :: 1 <= w => !(NatRepr w) -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType w)
- ClampedIntAddFn :: 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
- ClampedIntSubFn :: 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
- ClampedIntMulFn :: 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
- ClampedUIntAddFn :: 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
- ClampedUIntSubFn :: 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
- ClampedUIntMulFn :: 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx ::> BaseBVType w) ::> BaseBVType w) (BaseBVType w)
- IntSetWidthFn :: (1 <= m, 1 <= n) => !(NatRepr m) -> !(NatRepr n) -> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)
- UIntSetWidthFn :: (1 <= m, 1 <= n) => !(NatRepr m) -> !(NatRepr n) -> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)
- UIntToIntFn :: (1 <= m, 1 <= n) => !(NatRepr m) -> !(NatRepr n) -> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)
- IntToUIntFn :: (1 <= m, 1 <= n) => !(NatRepr m) -> !(NatRepr n) -> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)
- RealIsNonZeroFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType
- RealCosFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseRealType
- RealSinFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseRealType
- RealToSBVFn :: 1 <= w => !(NatRepr w) -> MatlabSolverFn f (EmptyCtx ::> BaseRealType) (BaseBVType w)
- RealToUBVFn :: 1 <= w => !(NatRepr w) -> MatlabSolverFn f (EmptyCtx ::> BaseRealType) (BaseBVType w)
- PredToBVFn :: 1 <= w => !(NatRepr w) -> MatlabSolverFn f (EmptyCtx ::> BaseBoolType) (BaseBVType w)
- CplxIsNonZeroFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseBoolType
- CplxIsRealFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseBoolType
- RealToComplexFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseComplexType
- RealPartOfCplxFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseRealType
- ImagPartOfCplxFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseRealType
- CplxNegFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
- CplxAddFn :: MatlabSolverFn f ((EmptyCtx ::> BaseComplexType) ::> BaseComplexType) BaseComplexType
- CplxSubFn :: MatlabSolverFn f ((EmptyCtx ::> BaseComplexType) ::> BaseComplexType) BaseComplexType
- CplxMulFn :: MatlabSolverFn f ((EmptyCtx ::> BaseComplexType) ::> BaseComplexType) BaseComplexType
- CplxRoundFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
- CplxFloorFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
- CplxCeilFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
- CplxMagFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseRealType
- CplxSqrtFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
- CplxExpFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
- CplxLogFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
- CplxLogBaseFn :: !Integer -> MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
- CplxSinFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
- CplxCosFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
- CplxTanFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
- matlabSolverArgTypes :: MatlabSolverFn f args ret -> Assignment BaseTypeRepr args
- matlabSolverReturnType :: MatlabSolverFn f args ret -> BaseTypeRepr ret
- ppMatlabSolverFn :: IsExpr f => MatlabSolverFn f a r -> Doc ann
- evalMatlabSolverFn :: forall sym args ret. IsExprBuilder sym => MatlabSolverFn (SymExpr sym) args ret -> sym -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
- testSolverFnEq :: TestEquality f => MatlabSolverFn f ax rx -> MatlabSolverFn f ay ry -> Maybe ((ax ::> rx) :~: (ay ::> ry))
- traverseMatlabSolverFn :: Applicative m => (forall tp. e tp -> m (f tp)) -> MatlabSolverFn e a r -> m (MatlabSolverFn f a r)
- class IsSymExprBuilder sym => MatlabSymbolicArrayBuilder sym where
- mkMatlabSolverFn :: sym -> MatlabSolverFn (SymExpr sym) args ret -> IO (SymFn sym args ret)
- clampedIntAdd :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
- clampedIntSub :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
- clampedIntMul :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
- clampedIntNeg :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)
- clampedIntAbs :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)
- clampedUIntAdd :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
- clampedUIntSub :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
- clampedUIntMul :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
Documentation
data MatlabSolverFn (f :: BaseType -> Type) args ret where Source #
Builtin functions that can be used to generate symbolic functions.
These functions are expected to be total, but the value returned may not be
specified. e.g. IntegerToNatFn must return some natural number for every
integer, but for negative integers, the particular number is unspecified.
Constructors
Instances
| (Hashable (f BaseRealType), Hashable (f BaseIntegerType), HashableF f) => Hashable (MatlabSolverFn f args tp) Source # | |
Defined in What4.Expr.MATLAB Methods hashWithSalt :: Int -> MatlabSolverFn f args tp -> Int # hash :: MatlabSolverFn f args tp -> Int # | |
matlabSolverArgTypes :: MatlabSolverFn f args ret -> Assignment BaseTypeRepr args Source #
Get arg tpyes of solver fn.
matlabSolverReturnType :: MatlabSolverFn f args ret -> BaseTypeRepr ret Source #
Get return type of solver fn.
ppMatlabSolverFn :: IsExpr f => MatlabSolverFn f a r -> Doc ann Source #
evalMatlabSolverFn :: forall sym args ret. IsExprBuilder sym => MatlabSolverFn (SymExpr sym) args ret -> sym -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret) Source #
testSolverFnEq :: TestEquality f => MatlabSolverFn f ax rx -> MatlabSolverFn f ay ry -> Maybe ((ax ::> rx) :~: (ay ::> ry)) Source #
Test MatlabSolverFn values for equality.
traverseMatlabSolverFn :: Applicative m => (forall tp. e tp -> m (f tp)) -> MatlabSolverFn e a r -> m (MatlabSolverFn f a r) Source #
class IsSymExprBuilder sym => MatlabSymbolicArrayBuilder sym where Source #
This class is provides functions needed to implement the symbolic array intrinsic functions
Methods
mkMatlabSolverFn :: sym -> MatlabSolverFn (SymExpr sym) args ret -> IO (SymFn sym args ret) Source #
Create a Matlab solver function from its prototype.
Instances
| MatlabSymbolicArrayBuilder (ExprBuilder t st fs) Source # | |
Defined in What4.Expr.Builder Methods mkMatlabSolverFn :: forall (args :: Ctx BaseType) (ret :: BaseType). ExprBuilder t st fs -> MatlabSolverFn (SymExpr (ExprBuilder t st fs)) args ret -> IO (SymFn (ExprBuilder t st fs) args ret) Source # | |
Utilities for definition
clampedIntAdd :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #
clampedIntSub :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #
clampedIntMul :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #
clampedIntNeg :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w) Source #
Compute the clamped negation of a signed bitvector.
The only difference between this operation and the usual 2's complement negation function is the handling of MIN_INT. The usual 2's complement negation sends MIN_INT to MIN_INT; however, the clamped version instead sends MIN_INT to MAX_INT.
clampedIntAbs :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w) Source #
Compute the clamped absolute value of a signed bitvector.
The only difference between this operation and the usual 2's complement operation is the handling of MIN_INT. The usual 2's complement absolute value function sends MIN_INT to MIN_INT; however, the clamped version instead sends MIN_INT to MAX_INT.
clampedUIntAdd :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #
clampedUIntSub :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #
clampedUIntMul :: (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #