What4.Expr.MATLAB

This module provides an interface that a symbolic backend should implement to support MATLAB intrinsics.

Documentation

data MatlabSolverFn (f :: BaseType -> Type) args ret where

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

BoolOrFn :: MatlabSolverFn f ((EmptyCtx ::> BaseBoolType) ::> BaseBoolType) BaseBoolType

IsIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType

NatLeFn :: MatlabSolverFn f ((EmptyCtx ::> BaseNatType) ::> BaseNatType) BaseBoolType

IntLeFn :: MatlabSolverFn f ((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType) BaseBoolType

BVToNatFn :: 1 <= w => !(NatRepr w) -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseNatType

SBVToIntegerFn :: 1 <= w => !(NatRepr w) -> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType

NatToIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseNatType) BaseIntegerType

IntegerToNatFn :: MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseNatType

IntegerToRealFn :: MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType

RealToIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseIntegerType

PredToIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType

NatSeqFn :: !(f BaseNatType) -> !(f BaseNatType) -> MatlabSolverFn f ((EmptyCtx ::> BaseNatType) ::> BaseNatType) BaseNatType

RealSeqFn :: !(f BaseRealType) -> !(f BaseRealType) -> MatlabSolverFn f ((EmptyCtx ::> BaseNatType) ::> BaseNatType) BaseRealType

IndicesInRange :: !(Assignment OnlyNatRepr (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

Instances

(Hashable (f BaseNatType), Hashable (f BaseRealType), HashableF f) => Hashable (MatlabSolverFn f args tp)

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

Get arg tpyes of solver fn.

matlabSolverReturnType :: MatlabSolverFn f args ret -> BaseTypeRepr ret

Get return type of solver fn.

ppMatlabSolverFn :: IsExpr f => MatlabSolverFn f a r -> Doc

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))

Test MatlabSolverFn values for equality.

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

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)

Create a Matlab solver function from its prototype.

Instances

MatlabSymbolicArrayBuilder (ExprBuilder t st fs)

Defined in What4.Expr.Builder

Methods

mkMatlabSolverFn :: ExprBuilder t st fs -> MatlabSolverFn (SymExpr (ExprBuilder t st fs)) args ret -> IO (SymFn (ExprBuilder t st fs) args ret)

Utilities for definition

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)

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)

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)

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)