| Copyright | (c) Galois Inc 2016-2020 |
|---|---|
| License | BSD3 |
| Maintainer | Joe Hendrix <[email protected]> |
| 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 :: Ctx BaseType) (ret :: BaseType) where
- BoolOrFn :: forall (f :: BaseType -> Type). MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBoolType) '::> BaseBoolType) 'BaseBoolType
- IsIntegerFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseBoolType
- IntLeFn :: forall (f :: BaseType -> Type). MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseIntegerType) '::> BaseIntegerType) 'BaseBoolType
- BVToIntegerFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType w) 'BaseIntegerType
- SBVToIntegerFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType w) 'BaseIntegerType
- IntegerToRealFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseIntegerType) 'BaseRealType
- RealToIntegerFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseIntegerType
- PredToIntegerFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBoolType) 'BaseIntegerType
- IntSeqFn :: forall (f :: BaseType -> Type). !(f BaseIntegerType) -> !(f BaseIntegerType) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseIntegerType) '::> BaseIntegerType) 'BaseIntegerType
- RealSeqFn :: forall (f :: BaseType -> Type). !(f BaseRealType) -> !(f BaseRealType) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseIntegerType) '::> BaseIntegerType) 'BaseRealType
- IndicesInRange :: forall (idx :: Ctx BaseType) (itp :: BaseType) (f :: BaseType -> Type). !(Assignment OnlyIntRepr (idx ::> itp)) -> !(Assignment f (idx ::> itp)) -> MatlabSolverFn f (idx '::> itp) 'BaseBoolType
- IsEqFn :: forall (tp :: BaseType) (f :: BaseType -> Type). !(BaseTypeRepr tp) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> tp) '::> tp) 'BaseBoolType
- BVIsNonZeroFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType w) 'BaseBoolType
- ClampedIntNegFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType w) ('BaseBVType w)
- ClampedIntAbsFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType w) ('BaseBVType w)
- ClampedIntAddFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w)
- ClampedIntSubFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w)
- ClampedIntMulFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w)
- ClampedUIntAddFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w)
- ClampedUIntSubFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w)
- ClampedUIntMulFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) '::> BaseBVType w) ('BaseBVType w)
- IntSetWidthFn :: forall (m :: Natural) (n :: Natural) (f :: BaseType -> Type). (1 <= m, 1 <= n) => !(NatRepr m) -> !(NatRepr n) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType m) ('BaseBVType n)
- UIntSetWidthFn :: forall (m :: Natural) (n :: Natural) (f :: BaseType -> Type). (1 <= m, 1 <= n) => !(NatRepr m) -> !(NatRepr n) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType m) ('BaseBVType n)
- UIntToIntFn :: forall (m :: Natural) (n :: Natural) (f :: BaseType -> Type). (1 <= m, 1 <= n) => !(NatRepr m) -> !(NatRepr n) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType m) ('BaseBVType n)
- IntToUIntFn :: forall (m :: Natural) (n :: Natural) (f :: BaseType -> Type). (1 <= m, 1 <= n) => !(NatRepr m) -> !(NatRepr n) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBVType m) ('BaseBVType n)
- RealIsNonZeroFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseBoolType
- RealCosFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseRealType
- RealSinFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseRealType
- RealToSBVFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) ('BaseBVType w)
- RealToUBVFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) ('BaseBVType w)
- PredToBVFn :: forall (w :: Natural) (f :: BaseType -> Type). 1 <= w => !(NatRepr w) -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseBoolType) ('BaseBVType w)
- CplxIsNonZeroFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseBoolType
- CplxIsRealFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseBoolType
- RealToComplexFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseRealType) 'BaseComplexType
- RealPartOfCplxFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseRealType
- ImagPartOfCplxFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseRealType
- CplxNegFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
- CplxAddFn :: forall (f :: BaseType -> Type). MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseComplexType) '::> BaseComplexType) 'BaseComplexType
- CplxSubFn :: forall (f :: BaseType -> Type). MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseComplexType) '::> BaseComplexType) 'BaseComplexType
- CplxMulFn :: forall (f :: BaseType -> Type). MatlabSolverFn f (((EmptyCtx :: Ctx BaseType) ::> BaseComplexType) '::> BaseComplexType) 'BaseComplexType
- CplxRoundFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
- CplxFloorFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
- CplxCeilFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
- CplxMagFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseRealType
- CplxSqrtFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
- CplxExpFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
- CplxLogFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
- CplxLogBaseFn :: forall (f :: BaseType -> Type). !Integer -> MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
- CplxSinFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
- CplxCosFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
- CplxTanFn :: forall (f :: BaseType -> Type). MatlabSolverFn f ((EmptyCtx :: Ctx BaseType) '::> BaseComplexType) 'BaseComplexType
- matlabSolverArgTypes :: forall (f :: BaseType -> Type) (args :: Ctx BaseType) (ret :: BaseType). MatlabSolverFn f args ret -> Assignment BaseTypeRepr args
- matlabSolverReturnType :: forall (f :: BaseType -> Type) (args :: Ctx BaseType) (ret :: BaseType). MatlabSolverFn f args ret -> BaseTypeRepr ret
- ppMatlabSolverFn :: forall (f :: BaseType -> Type) (a :: Ctx BaseType) (r :: BaseType) ann. IsExpr f => MatlabSolverFn f a r -> Doc ann
- evalMatlabSolverFn :: forall sym (args :: Ctx BaseType) (ret :: BaseType). IsExprBuilder sym => MatlabSolverFn (SymExpr sym) args ret -> sym -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret)
- testSolverFnEq :: forall (f :: BaseType -> Type) (ax :: Ctx BaseType) (rx :: BaseType) (ay :: Ctx BaseType) (ry :: BaseType). TestEquality f => MatlabSolverFn f ax rx -> MatlabSolverFn f ay ry -> Maybe ((ax ::> rx) :~: (ay ::> ry))
- traverseMatlabSolverFn :: forall m e f (a :: Ctx BaseType) (r :: BaseType). Applicative m => (forall (tp :: BaseType). e tp -> m (f tp)) -> MatlabSolverFn e a r -> m (MatlabSolverFn f a r)
- class IsSymExprBuilder sym => MatlabSymbolicArrayBuilder sym where
- mkMatlabSolverFn :: forall (args :: Ctx BaseType) (ret :: BaseType). sym -> MatlabSolverFn (SymExpr sym) args ret -> IO (SymFn sym args ret)
- clampedIntAdd :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
- clampedIntSub :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
- clampedIntMul :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
- clampedIntNeg :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)
- clampedIntAbs :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)
- clampedUIntAdd :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
- clampedUIntSub :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
- clampedUIntMul :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
Documentation
data MatlabSolverFn (f :: BaseType -> Type) (args :: Ctx BaseType) (ret :: BaseType) 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
| TestEquality f => Eq (MatlabSolverFn f args tp) Source # | |
Defined in What4.Expr.MATLAB Methods (==) :: MatlabSolverFn f args tp -> MatlabSolverFn f args tp -> Bool # (/=) :: MatlabSolverFn f args tp -> MatlabSolverFn f args tp -> Bool # | |
| (Hashable (f BaseRealType), Hashable (f BaseIntegerType), HashableF f, TestEquality 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 :: forall (f :: BaseType -> Type) (args :: Ctx BaseType) (ret :: BaseType). MatlabSolverFn f args ret -> Assignment BaseTypeRepr args Source #
Get arg tpyes of solver fn.
matlabSolverReturnType :: forall (f :: BaseType -> Type) (args :: Ctx BaseType) (ret :: BaseType). MatlabSolverFn f args ret -> BaseTypeRepr ret Source #
Get return type of solver fn.
ppMatlabSolverFn :: forall (f :: BaseType -> Type) (a :: Ctx BaseType) (r :: BaseType) ann. IsExpr f => MatlabSolverFn f a r -> Doc ann Source #
evalMatlabSolverFn :: forall sym (args :: Ctx BaseType) (ret :: BaseType). IsExprBuilder sym => MatlabSolverFn (SymExpr sym) args ret -> sym -> Assignment (SymExpr sym) args -> IO (SymExpr sym ret) Source #
testSolverFnEq :: forall (f :: BaseType -> Type) (ax :: Ctx BaseType) (rx :: BaseType) (ay :: Ctx BaseType) (ry :: BaseType). TestEquality f => MatlabSolverFn f ax rx -> MatlabSolverFn f ay ry -> Maybe ((ax ::> rx) :~: (ay ::> ry)) Source #
Test MatlabSolverFn values for equality.
traverseMatlabSolverFn :: forall m e f (a :: Ctx BaseType) (r :: BaseType). Applicative m => (forall (tp :: BaseType). 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 :: forall (args :: Ctx BaseType) (ret :: BaseType). 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 :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #
clampedIntSub :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #
clampedIntMul :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #
clampedIntNeg :: forall sym (w :: Natural). (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 :: forall sym (w :: Natural). (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 :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #
clampedUIntSub :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #
clampedUIntMul :: forall sym (w :: Natural). (IsExprBuilder sym, 1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w) Source #