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

Copyright | (c) Galois Inc 2016-2020
License | BSD3
Maintainer | Joe Hendrix <jhendrix@galois.com>
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Expr.MATLAB

Contents

- Utilities for definition

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

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 |

#### Instances

Instances details

TestEquality f => Eq (MatlabSolverFn f args tp) Source # |
Instance details Defined in What4.Expr.MATLAB Methods (==) :: MatlabSolverFn f args tp -> MatlabSolverFn f args tp -> Bool Source # (/=) :: MatlabSolverFn f args tp -> MatlabSolverFn f args tp -> Bool Source #
(Hashable (f BaseRealType), Hashable (f BaseIntegerType), HashableF f, TestEquality f) => Hashable (MatlabSolverFn f args tp) Source # |
Instance details Defined in What4.Expr.MATLAB Methods hashWithSalt :: Int -> MatlabSolverFn f args tp -> Int Source # hash :: MatlabSolverFn f args tp -> Int Source #

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

Instances details

MatlabSymbolicArrayBuilder (ExprBuilder t st fs) Source # |
Instance details 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 #