what4-1.0: Solver-agnostic symbolic values support for issuing queries

Copyright(c) Galois Inc 2016-2020
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Safe HaskellNone
LanguageHaskell2010

What4.Expr.MATLAB

Contents

Description

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

Synopsis

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

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) Source # 
Instance details

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.

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 # 
Instance details

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