what4-1.3: src/What4/Expr/MATLAB.hs
{-|
Module : What4.Expr.MATLAB
Description : Low-level support for MATLAB-style arithmetic operations
Copyright : (c) Galois, Inc, 2016-2020
License : BSD3
Maintainer : Joe Hendrix <jhendrix@galois.com>
This module provides an interface that a symbolic backend should
implement to support MATLAB intrinsics.
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
module What4.Expr.MATLAB
( MatlabSolverFn(..)
, matlabSolverArgTypes
, matlabSolverReturnType
, ppMatlabSolverFn
, evalMatlabSolverFn
, testSolverFnEq
, traverseMatlabSolverFn
, MatlabSymbolicArrayBuilder(..)
-- * Utilities for definition
, clampedIntAdd
, clampedIntSub
, clampedIntMul
, clampedIntNeg
, clampedIntAbs
, clampedUIntAdd
, clampedUIntSub
, clampedUIntMul
) where
import Control.Monad (join)
import qualified Data.BitVector.Sized as BV
import Data.Kind (Type)
import Data.Hashable
import Data.Parameterized.Classes
import Data.Parameterized.Context as Ctx
import Data.Parameterized.TH.GADT
import Data.Parameterized.TraversableFC
import Prettyprinter
import What4.BaseTypes
import What4.Interface
import What4.Utils.Complex
import What4.Utils.OnlyIntRepr
------------------------------------------------------------------------
-- MatlabSolverFn
clampedIntAdd :: (IsExprBuilder sym, 1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
clampedIntAdd sym x y = do
let w = bvWidth x
withAddPrefixLeq w (knownNat :: NatRepr 1) $ do
-- Compute result with 1 additional bit to catch clamping
let w' = incNat w
x' <- bvSext sym w' x
y' <- bvSext sym w' y
-- Compute result.
r' <- bvAdd sym x' y'
-- Check is result is greater than or equal to max value.
too_high <- bvSgt sym r' =<< bvLit sym w' (BV.maxSigned w')
max_int <- bvLit sym w (BV.maxSigned w)
-- Check is result is less than min value.
too_low <- bvSlt sym r' =<< bvLit sym w' (BV.minSigned w')
min_int <- bvLit sym w (BV.minSigned w)
-- Clamp integer range.
r <- bvTrunc sym w r'
r_low <- bvIte sym too_low min_int r
bvIte sym too_high max_int r_low
clampedIntSub :: (IsExprBuilder sym, 1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
clampedIntSub sym x y = do
let w = bvWidth x
(ov, xy) <- subSignedOF sym x y
ysign <- bvIsNeg sym y
minint <- minSignedBV sym w
maxint <- maxSignedBV sym w
ov_val <- bvIte sym ysign maxint minint
bvIte sym ov ov_val xy
clampedIntMul :: (IsExprBuilder sym, 1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
clampedIntMul sym x y = do
let w = bvWidth x
(hi,lo) <- signedWideMultiplyBV sym x y
zro <- bvLit sym w (BV.zero w)
ones <- maxUnsignedBV sym w
ok_pos <- join $ andPred sym <$> (notPred sym =<< bvIsNeg sym lo)
<*> bvEq sym hi zro
ok_neg <- join $ andPred sym <$> bvIsNeg sym lo
<*> bvEq sym hi ones
ov <- notPred sym =<< orPred sym ok_pos ok_neg
minint <- minSignedBV sym w
maxint <- maxSignedBV sym w
hisign <- bvIsNeg sym hi
ov_val <- bvIte sym hisign minint maxint
bvIte sym ov ov_val lo
-- | 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.
clampedIntNeg :: (IsExprBuilder sym, 1 <= w)
=> sym
-> SymBV sym w
-> IO (SymBV sym w)
clampedIntNeg sym x = do
let w = bvWidth x
minint <- minSignedBV sym w
-- return maxint when x == minint, and neg(x) otherwise
p <- bvEq sym x minint
iteM bvIte sym p (maxSignedBV sym w) (bvNeg sym x)
-- | 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.
clampedIntAbs :: (IsExprBuilder sym, 1 <= w)
=> sym
-> SymBV sym w
-> IO (SymBV sym w)
clampedIntAbs sym x = do
isNeg <- bvIsNeg sym x
iteM bvIte sym isNeg (clampedIntNeg sym x) (pure x)
clampedUIntAdd :: (IsExprBuilder sym, 1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
clampedUIntAdd sym x y = do
let w = bvWidth x
(ov, xy) <- addUnsignedOF sym x y
maxint <- maxUnsignedBV sym w
bvIte sym ov maxint xy
clampedUIntSub :: (IsExprBuilder sym, 1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
clampedUIntSub sym x y = do
let w = bvWidth x
no_underflow <- bvUge sym x y
iteM bvIte
sym
no_underflow
(bvSub sym x y) -- Perform subtraction if y >= x
(bvLit sym w (BV.zero w)) -- Otherwise return min int
clampedUIntMul :: (IsExprBuilder sym, 1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
clampedUIntMul sym x y = do
let w = bvWidth x
(hi, lo) <- unsignedWideMultiplyBV sym x y
maxint <- maxUnsignedBV sym w
ov <- bvIsNonzero sym hi
bvIte sym ov maxint lo
------------------------------------------------------------------------
-- MatlabSolverFn
-- | 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.
data MatlabSolverFn (f :: BaseType -> Type) args ret where
-- Or two Boolean variables
BoolOrFn :: MatlabSolverFn f (EmptyCtx ::> BaseBoolType ::> BaseBoolType) BaseBoolType
-- Returns true if the real value is an integer.
IsIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType
-- Return true if first value is less than or equal to second.
IntLeFn :: MatlabSolverFn f (EmptyCtx ::> BaseIntegerType ::> BaseIntegerType) BaseBoolType
-- A function for mapping a unsigned bitvector to an integer.
BVToIntegerFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
-- A function for mapping a signed bitvector to a integer.
SBVToIntegerFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseIntegerType
-- A function for mapping an integer to equivalent real.
IntegerToRealFn :: MatlabSolverFn f (EmptyCtx ::> BaseIntegerType) BaseRealType
-- A function for mapping a real to equivalent integer.
--
-- Function may return any value if input is not an integer.
RealToIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseIntegerType
-- A function that maps Booleans logical value to an integer
-- (either 0 for false, or 1 for true)
PredToIntegerFn :: MatlabSolverFn f (EmptyCtx ::> BaseBoolType) BaseIntegerType
-- 'IntSeqFn base c' denotes the function '\i _ -> base + c*i
IntSeqFn :: !(f BaseIntegerType)
-> !(f BaseIntegerType)
-> MatlabSolverFn f (EmptyCtx ::> BaseIntegerType ::> BaseIntegerType) BaseIntegerType
-- 'RealSeqFn base c' denotes the function '\_ i -> base + c*i
RealSeqFn :: !(f BaseRealType)
-> !(f BaseRealType)
-> MatlabSolverFn f (EmptyCtx ::> BaseIntegerType ::> BaseIntegerType) BaseRealType
-- 'IndicesInRange tps upper_bounds' returns a predicate that is true if all the arguments
-- (which must be natural numbers) are between 1 and the given upper bounds (inclusive).
IndicesInRange :: !(Assignment OnlyIntRepr (idx ::> itp))
-> !(Assignment f (idx ::> itp))
-- Upper bounds on indices
-> MatlabSolverFn f (idx ::> itp) BaseBoolType
IsEqFn :: !(BaseTypeRepr tp)
-> MatlabSolverFn f (EmptyCtx ::> tp ::> tp) BaseBoolType
------------------------------------------------------------------------
-- Bitvector functions
-- Returns true if the bitvector is non-zero.
BVIsNonZeroFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) BaseBoolType
-- Negate a signed bitvector
ClampedIntNegFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType w)
-- Get absolute value of a signed bitvector
ClampedIntAbsFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType w) (BaseBVType w)
-- Add two values without wrapping but rather rounding to
-- 0/max value when the result is out of range.
ClampedIntAddFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f
(EmptyCtx ::> BaseBVType w ::> BaseBVType w)
(BaseBVType w)
-- Subtract one value from another without wrapping but rather rounding to
-- 0/max value when the result is out of range.
ClampedIntSubFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f
(EmptyCtx ::> BaseBVType w ::> BaseBVType w)
(BaseBVType w)
-- Multiple two values without wrapping but rather rounding to
-- 0/max value when the result is out of range.
ClampedIntMulFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f
(EmptyCtx ::> BaseBVType w ::> BaseBVType w)
(BaseBVType w)
-- Add two values without wrapping but rather rounding to
-- 0/max value when the result is out of range.
ClampedUIntAddFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f
(EmptyCtx ::> BaseBVType w ::> BaseBVType w)
(BaseBVType w)
-- Subtract one value from another without wrapping but rather rounding to
-- 0/max value when the result is out of range.
ClampedUIntSubFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f
(EmptyCtx ::> BaseBVType w ::> BaseBVType w)
(BaseBVType w)
-- Multiple two values without wrapping but rather rounding to
-- 0/max value when the result is out of range.
ClampedUIntMulFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f
(EmptyCtx ::> BaseBVType w ::> BaseBVType w)
(BaseBVType w)
-- Convert a signed integer to the nearest signed integer with the
-- given width. This clamps the value to min-int or max int when truncated
-- the width.
IntSetWidthFn :: (1 <= m, 1 <= n)
=> !(NatRepr m)
-> !(NatRepr n)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)
-- Convert a unsigned integer to the nearest unsigned integer with the
-- given width. This clamps the value to min-int or max int when truncated
-- the width.
UIntSetWidthFn :: (1 <= m, 1 <= n)
=> !(NatRepr m)
-> !(NatRepr n)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)
-- Convert a unsigned integer to the nearest signed integer with the
-- given width. This clamps the value to min-int or max int when truncated
-- the width.
UIntToIntFn :: (1 <= m, 1 <= n)
=> !(NatRepr m)
-> !(NatRepr n)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)
-- Convert a signed integer to the nearest unsigned integer with the
-- given width. This clamps the value to min-int or max int when truncated
-- the width.
IntToUIntFn :: (1 <= m, 1 <= n)
=> !(NatRepr m)
-> !(NatRepr n)
-> MatlabSolverFn f (EmptyCtx ::> BaseBVType m) (BaseBVType n)
------------------------------------------------------------------------
-- Real functions
-- Returns true if the complex number is non-zero.
RealIsNonZeroFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseBoolType
RealCosFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseRealType
RealSinFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseRealType
------------------------------------------------------------------------
-- Conversion functions
RealToSBVFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f (EmptyCtx ::> BaseRealType) (BaseBVType w)
RealToUBVFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f (EmptyCtx ::> BaseRealType) (BaseBVType w)
-- Return 1 if the predicate is true; 0 otherwise.
PredToBVFn :: (1 <= w)
=> !(NatRepr w)
-> MatlabSolverFn f (EmptyCtx ::> BaseBoolType) (BaseBVType w)
------------------------------------------------------------------------
-- Complex functions
-- Returns true if the complex number is non-zero.
CplxIsNonZeroFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseBoolType
-- Returns true if the imaginary part of complex number is zero.
CplxIsRealFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseBoolType
-- A function for mapping a real to equivalent complex with imaginary number equals 0.
RealToComplexFn :: MatlabSolverFn f (EmptyCtx ::> BaseRealType) BaseComplexType
-- Returns the real component out of a complex number.
RealPartOfCplxFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseRealType
-- Returns the imag component out of a complex number.
ImagPartOfCplxFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseRealType
-- Return the complex number formed by negating both components.
CplxNegFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
-- Add two complex values.
CplxAddFn :: MatlabSolverFn f
(EmptyCtx ::> BaseComplexType ::> BaseComplexType)
BaseComplexType
-- Subtract one complex value from another.
CplxSubFn :: MatlabSolverFn f
(EmptyCtx ::> BaseComplexType ::> BaseComplexType)
BaseComplexType
-- Multiply two complex values.
CplxMulFn :: MatlabSolverFn f
(EmptyCtx ::> BaseComplexType ::> BaseComplexType)
BaseComplexType
-- Return the complex number formed by rounding both components.
--
-- Rounding is away from zero.
CplxRoundFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
-- Return the complex number formed by taking floor of both components.
CplxFloorFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
-- Return the complex number formed by taking ceiling of both components.
CplxCeilFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
-- Return magningture of complex number.
CplxMagFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseRealType
-- Return the principal square root of a complex number.
CplxSqrtFn :: MatlabSolverFn f (EmptyCtx ::> BaseComplexType) BaseComplexType
-- Returns complex exponential of input
CplxExpFn :: MatlabSolverFn f
(EmptyCtx ::> BaseComplexType)
BaseComplexType
-- Returns complex natural logarithm of input
CplxLogFn :: MatlabSolverFn f
(EmptyCtx ::> BaseComplexType)
BaseComplexType
-- Returns complex natural logarithm of input
CplxLogBaseFn :: !Integer
-> MatlabSolverFn f
(EmptyCtx ::> BaseComplexType)
BaseComplexType
-- Returns complex sine of input
CplxSinFn :: MatlabSolverFn f
(EmptyCtx ::> BaseComplexType)
BaseComplexType
-- Returns complex cosine of input
CplxCosFn :: MatlabSolverFn f
(EmptyCtx ::> BaseComplexType)
BaseComplexType
-- Returns tangent of input.
--
CplxTanFn :: MatlabSolverFn f
(EmptyCtx ::> BaseComplexType)
BaseComplexType
-- Dummy declaration splice to bring App into template haskell scope.
$(return [])
traverseMatlabSolverFn :: Applicative m
=> (forall tp . e tp -> m (f tp))
-> MatlabSolverFn e a r
-> m (MatlabSolverFn f a r)
traverseMatlabSolverFn f fn_id =
case fn_id of
BoolOrFn -> pure $ BoolOrFn
IsIntegerFn -> pure $ IsIntegerFn
IntLeFn -> pure $ IntLeFn
BVToIntegerFn w -> pure $ BVToIntegerFn w
SBVToIntegerFn w -> pure $ SBVToIntegerFn w
IntegerToRealFn -> pure $ IntegerToRealFn
RealToIntegerFn -> pure $ RealToIntegerFn
PredToIntegerFn -> pure $ PredToIntegerFn
IntSeqFn b i -> IntSeqFn <$> f b <*> f i
RealSeqFn b i -> RealSeqFn <$> f b <*> f i
IndicesInRange tps a -> IndicesInRange tps <$> traverseFC f a
IsEqFn tp -> pure $ IsEqFn tp
BVIsNonZeroFn w -> pure $ BVIsNonZeroFn w
ClampedIntNegFn w -> pure $ ClampedIntNegFn w
ClampedIntAbsFn w -> pure $ ClampedIntAbsFn w
ClampedIntAddFn w -> pure $ ClampedIntAddFn w
ClampedIntSubFn w -> pure $ ClampedIntSubFn w
ClampedIntMulFn w -> pure $ ClampedIntMulFn w
ClampedUIntAddFn w -> pure $ ClampedUIntAddFn w
ClampedUIntSubFn w -> pure $ ClampedUIntSubFn w
ClampedUIntMulFn w -> pure $ ClampedUIntMulFn w
IntSetWidthFn i o -> pure $ IntSetWidthFn i o
UIntSetWidthFn i o -> pure $ UIntSetWidthFn i o
UIntToIntFn i o -> pure $ UIntToIntFn i o
IntToUIntFn i o -> pure $ IntToUIntFn i o
RealCosFn -> pure $ RealCosFn
RealSinFn -> pure $ RealSinFn
RealIsNonZeroFn -> pure $ RealIsNonZeroFn
RealToSBVFn w -> pure $ RealToSBVFn w
RealToUBVFn w -> pure $ RealToUBVFn w
PredToBVFn w -> pure $ PredToBVFn w
CplxIsNonZeroFn -> pure $ CplxIsNonZeroFn
CplxIsRealFn -> pure $ CplxIsRealFn
RealToComplexFn -> pure $ RealToComplexFn
RealPartOfCplxFn -> pure $ RealPartOfCplxFn
ImagPartOfCplxFn -> pure $ ImagPartOfCplxFn
CplxNegFn -> pure $ CplxNegFn
CplxAddFn -> pure $ CplxAddFn
CplxSubFn -> pure $ CplxSubFn
CplxMulFn -> pure $ CplxMulFn
CplxRoundFn -> pure $ CplxRoundFn
CplxFloorFn -> pure $ CplxFloorFn
CplxCeilFn -> pure $ CplxCeilFn
CplxMagFn -> pure $ CplxMagFn
CplxSqrtFn -> pure $ CplxSqrtFn
CplxExpFn -> pure $ CplxExpFn
CplxLogFn -> pure $ CplxLogFn
CplxLogBaseFn b -> pure $ CplxLogBaseFn b
CplxSinFn -> pure $ CplxSinFn
CplxCosFn -> pure $ CplxCosFn
CplxTanFn -> pure $ CplxTanFn
-- | Utilities to make a pair with the same value.
binCtx :: BaseTypeRepr tp -> Ctx.Assignment BaseTypeRepr (EmptyCtx ::> tp ::> tp)
binCtx tp = Ctx.empty Ctx.:> tp Ctx.:> tp
-- | Get arg tpyes of solver fn.
matlabSolverArgTypes :: MatlabSolverFn f args ret -> Assignment BaseTypeRepr args
matlabSolverArgTypes f =
case f of
BoolOrFn -> knownRepr
IsIntegerFn -> knownRepr
IntLeFn -> knownRepr
BVToIntegerFn w -> Ctx.singleton (BaseBVRepr w)
SBVToIntegerFn w -> Ctx.singleton (BaseBVRepr w)
IntegerToRealFn -> knownRepr
RealToIntegerFn -> knownRepr
PredToIntegerFn -> knownRepr
IntSeqFn{} -> knownRepr
IndicesInRange tps _ -> fmapFC toBaseTypeRepr tps
RealSeqFn _ _ -> knownRepr
IsEqFn tp -> binCtx tp
BVIsNonZeroFn w -> Ctx.singleton (BaseBVRepr w)
ClampedIntNegFn w -> Ctx.singleton (BaseBVRepr w)
ClampedIntAbsFn w -> Ctx.singleton (BaseBVRepr w)
ClampedIntAddFn w -> binCtx (BaseBVRepr w)
ClampedIntSubFn w -> binCtx (BaseBVRepr w)
ClampedIntMulFn w -> binCtx (BaseBVRepr w)
ClampedUIntAddFn w -> binCtx (BaseBVRepr w)
ClampedUIntSubFn w -> binCtx (BaseBVRepr w)
ClampedUIntMulFn w -> binCtx (BaseBVRepr w)
IntSetWidthFn i _ -> Ctx.singleton (BaseBVRepr i)
UIntSetWidthFn i _ -> Ctx.singleton (BaseBVRepr i)
UIntToIntFn i _ -> Ctx.singleton (BaseBVRepr i)
IntToUIntFn i _ -> Ctx.singleton (BaseBVRepr i)
RealCosFn -> knownRepr
RealSinFn -> knownRepr
RealIsNonZeroFn -> knownRepr
RealToSBVFn _ -> knownRepr
RealToUBVFn _ -> knownRepr
PredToBVFn _ -> knownRepr
CplxIsNonZeroFn -> knownRepr
CplxIsRealFn -> knownRepr
RealToComplexFn -> knownRepr
RealPartOfCplxFn -> knownRepr
ImagPartOfCplxFn -> knownRepr
CplxNegFn -> knownRepr
CplxAddFn -> knownRepr
CplxSubFn -> knownRepr
CplxMulFn -> knownRepr
CplxRoundFn -> knownRepr
CplxFloorFn -> knownRepr
CplxCeilFn -> knownRepr
CplxMagFn -> knownRepr
CplxSqrtFn -> knownRepr
CplxExpFn -> knownRepr
CplxLogFn -> knownRepr
CplxLogBaseFn _ -> knownRepr
CplxSinFn -> knownRepr
CplxCosFn -> knownRepr
CplxTanFn -> knownRepr
-- | Get return type of solver fn.
matlabSolverReturnType :: MatlabSolverFn f args ret -> BaseTypeRepr ret
matlabSolverReturnType f =
case f of
BoolOrFn -> knownRepr
IsIntegerFn -> knownRepr
IntLeFn -> knownRepr
BVToIntegerFn{} -> knownRepr
SBVToIntegerFn{} -> knownRepr
IntegerToRealFn -> knownRepr
RealToIntegerFn -> knownRepr
PredToIntegerFn -> knownRepr
IntSeqFn{} -> knownRepr
IndicesInRange{} -> knownRepr
RealSeqFn _ _ -> knownRepr
IsEqFn{} -> knownRepr
BVIsNonZeroFn _ -> knownRepr
ClampedIntNegFn w -> BaseBVRepr w
ClampedIntAbsFn w -> BaseBVRepr w
ClampedIntAddFn w -> BaseBVRepr w
ClampedIntSubFn w -> BaseBVRepr w
ClampedIntMulFn w -> BaseBVRepr w
ClampedUIntAddFn w -> BaseBVRepr w
ClampedUIntSubFn w -> BaseBVRepr w
ClampedUIntMulFn w -> BaseBVRepr w
IntSetWidthFn _ o -> BaseBVRepr o
UIntSetWidthFn _ o -> BaseBVRepr o
UIntToIntFn _ o -> BaseBVRepr o
IntToUIntFn _ o -> BaseBVRepr o
RealCosFn -> knownRepr
RealSinFn -> knownRepr
RealIsNonZeroFn -> knownRepr
RealToSBVFn w -> BaseBVRepr w
RealToUBVFn w -> BaseBVRepr w
PredToBVFn w -> BaseBVRepr w
CplxIsNonZeroFn -> knownRepr
CplxIsRealFn -> knownRepr
RealToComplexFn -> knownRepr
RealPartOfCplxFn -> knownRepr
ImagPartOfCplxFn -> knownRepr
CplxNegFn -> knownRepr
CplxAddFn -> knownRepr
CplxSubFn -> knownRepr
CplxMulFn -> knownRepr
CplxRoundFn -> knownRepr
CplxFloorFn -> knownRepr
CplxCeilFn -> knownRepr
CplxMagFn -> knownRepr
CplxSqrtFn -> knownRepr
CplxExpFn -> knownRepr
CplxLogFn -> knownRepr
CplxLogBaseFn _ -> knownRepr
CplxSinFn -> knownRepr
CplxCosFn -> knownRepr
CplxTanFn -> knownRepr
ppMatlabSolverFn :: IsExpr f => MatlabSolverFn f a r -> Doc ann
ppMatlabSolverFn f =
case f of
BoolOrFn -> pretty "bool_or"
IsIntegerFn -> pretty "is_integer"
IntLeFn -> pretty "int_le"
BVToIntegerFn w -> parens $ pretty "bv_to_int" <+> ppNatRepr w
SBVToIntegerFn w -> parens $ pretty "sbv_to_int" <+> ppNatRepr w
IntegerToRealFn -> pretty "integer_to_real"
RealToIntegerFn -> pretty "real_to_integer"
PredToIntegerFn -> pretty "pred_to_integer"
IntSeqFn b i -> parens $ pretty "nat_seq" <+> printSymExpr b <+> printSymExpr i
RealSeqFn b i -> parens $ pretty "real_seq" <+> printSymExpr b <+> printSymExpr i
IndicesInRange _ bnds ->
parens (pretty "indices_in_range" <+> sep (toListFC printSymExpr bnds))
IsEqFn{} -> pretty "is_eq"
BVIsNonZeroFn w -> parens $ pretty "bv_is_nonzero" <+> ppNatRepr w
ClampedIntNegFn w -> parens $ pretty "clamped_int_neg" <+> ppNatRepr w
ClampedIntAbsFn w -> parens $ pretty "clamped_neg_abs" <+> ppNatRepr w
ClampedIntAddFn w -> parens $ pretty "clamped_int_add" <+> ppNatRepr w
ClampedIntSubFn w -> parens $ pretty "clamped_int_sub" <+> ppNatRepr w
ClampedIntMulFn w -> parens $ pretty "clamped_int_mul" <+> ppNatRepr w
ClampedUIntAddFn w -> parens $ pretty "clamped_uint_add" <+> ppNatRepr w
ClampedUIntSubFn w -> parens $ pretty "clamped_uint_sub" <+> ppNatRepr w
ClampedUIntMulFn w -> parens $ pretty "clamped_uint_mul" <+> ppNatRepr w
IntSetWidthFn i o -> parens $ pretty "int_set_width" <+> ppNatRepr i <+> ppNatRepr o
UIntSetWidthFn i o -> parens $ pretty "uint_set_width" <+> ppNatRepr i <+> ppNatRepr o
UIntToIntFn i o -> parens $ pretty "uint_to_int" <+> ppNatRepr i <+> ppNatRepr o
IntToUIntFn i o -> parens $ pretty "int_to_uint" <+> ppNatRepr i <+> ppNatRepr o
RealCosFn -> pretty "real_cos"
RealSinFn -> pretty "real_sin"
RealIsNonZeroFn -> pretty "real_is_nonzero"
RealToSBVFn w -> parens $ pretty "real_to_sbv" <+> ppNatRepr w
RealToUBVFn w -> parens $ pretty "real_to_sbv" <+> ppNatRepr w
PredToBVFn w -> parens $ pretty "pred_to_bv" <+> ppNatRepr w
CplxIsNonZeroFn -> pretty "cplx_is_nonzero"
CplxIsRealFn -> pretty "cplx_is_real"
RealToComplexFn -> pretty "real_to_complex"
RealPartOfCplxFn -> pretty "real_part_of_complex"
ImagPartOfCplxFn -> pretty "imag_part_of_complex"
CplxNegFn -> pretty "cplx_neg"
CplxAddFn -> pretty "cplx_add"
CplxSubFn -> pretty "cplx_sub"
CplxMulFn -> pretty "cplx_mul"
CplxRoundFn -> pretty "cplx_round"
CplxFloorFn -> pretty "cplx_floor"
CplxCeilFn -> pretty "cplx_ceil"
CplxMagFn -> pretty "cplx_mag"
CplxSqrtFn -> pretty "cplx_sqrt"
CplxExpFn -> pretty "cplx_exp"
CplxLogFn -> pretty "cplx_log"
CplxLogBaseFn b -> parens $ pretty "cplx_log_base" <+> pretty b
CplxSinFn -> pretty "cplx_sin"
CplxCosFn -> pretty "cplx_cos"
CplxTanFn -> pretty "cplx_tan"
ppNatRepr :: NatRepr w -> Doc ann
ppNatRepr = viaShow
-- | Test 'MatlabSolverFn' values for equality.
testSolverFnEq :: TestEquality f
=> MatlabSolverFn f ax rx
-> MatlabSolverFn f ay ry
-> Maybe ((ax ::> rx) :~: (ay ::> ry))
testSolverFnEq = $(structuralTypeEquality [t|MatlabSolverFn|]
[ ( DataArg 0 `TypeApp` AnyType
, [|testEquality|]
)
, ( ConType [t|NatRepr|] `TypeApp` AnyType
, [|testEquality|]
)
, ( ConType [t|Assignment|] `TypeApp` AnyType `TypeApp` AnyType
, [|testEquality|]
)
, ( ConType [t|BaseTypeRepr|] `TypeApp` AnyType
, [|testEquality|]
)
]
)
instance TestEquality f => Eq (MatlabSolverFn f args tp) where
x == y = isJust (testSolverFnEq x y)
instance ( Hashable (f BaseRealType)
, Hashable (f BaseIntegerType)
, HashableF f
, TestEquality f
)
=> Hashable (MatlabSolverFn f args tp) where
hashWithSalt = $(structuralHashWithSalt [t|MatlabSolverFn|] [])
realIsNonZero :: IsExprBuilder sym => sym -> SymReal sym -> IO (Pred sym)
realIsNonZero sym = realNe sym (realZero sym)
evalMatlabSolverFn :: forall sym args ret
. IsExprBuilder sym
=> MatlabSolverFn (SymExpr sym) args ret
-> sym
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
evalMatlabSolverFn f sym =
case f of
BoolOrFn -> uncurryAssignment $ orPred sym
IsIntegerFn -> uncurryAssignment $ isInteger sym
IntLeFn -> uncurryAssignment $ intLe sym
BVToIntegerFn{} -> uncurryAssignment $ bvToInteger sym
SBVToIntegerFn{} -> uncurryAssignment $ sbvToInteger sym
IntegerToRealFn -> uncurryAssignment $ integerToReal sym
RealToIntegerFn -> uncurryAssignment $ realToInteger sym
PredToIntegerFn -> uncurryAssignment $ \p ->
iteM intIte sym p (intLit sym 1) (intLit sym 0)
IntSeqFn b inc -> uncurryAssignment $ \idx _ -> do
intAdd sym b =<< intMul sym inc idx
RealSeqFn b inc -> uncurryAssignment $ \_ idx -> do
realAdd sym b =<< realMul sym inc =<< integerToReal sym idx
IndicesInRange tps0 bnds0 -> \args ->
Ctx.forIndex (Ctx.size tps0) (g tps0 bnds0 args) (pure (truePred sym))
where g :: Assignment OnlyIntRepr ctx
-> Assignment (SymExpr sym) ctx
-> Assignment (SymExpr sym) ctx
-> IO (Pred sym)
-> Index ctx tp
-> IO (Pred sym)
g tps bnds args m i = do
case tps Ctx.! i of
OnlyIntRepr -> do
let v = args ! i
let bnd = bnds ! i
one <- intLit sym 1
p <- join $ andPred sym <$> intLe sym one v <*> intLe sym v bnd
andPred sym p =<< m
IsEqFn{} -> Ctx.uncurryAssignment $ \x y -> do
isEq sym x y
BVIsNonZeroFn _ -> Ctx.uncurryAssignment $ bvIsNonzero sym
ClampedIntNegFn _ -> Ctx.uncurryAssignment $ clampedIntNeg sym
ClampedIntAbsFn _ -> Ctx.uncurryAssignment $ clampedIntAbs sym
ClampedIntAddFn _ -> Ctx.uncurryAssignment $ clampedIntAdd sym
ClampedIntSubFn _ -> Ctx.uncurryAssignment $ clampedIntSub sym
ClampedIntMulFn _ -> Ctx.uncurryAssignment $ clampedIntMul sym
ClampedUIntAddFn _ -> Ctx.uncurryAssignment $ clampedUIntAdd sym
ClampedUIntSubFn _ -> Ctx.uncurryAssignment $ clampedUIntSub sym
ClampedUIntMulFn _ -> Ctx.uncurryAssignment $ clampedUIntMul sym
IntSetWidthFn _ o -> Ctx.uncurryAssignment $ \v -> intSetWidth sym v o
UIntSetWidthFn _ o -> Ctx.uncurryAssignment $ \v -> uintSetWidth sym v o
UIntToIntFn _ o -> Ctx.uncurryAssignment $ \v -> uintToInt sym v o
IntToUIntFn _ o -> Ctx.uncurryAssignment $ \v -> intToUInt sym v o
RealIsNonZeroFn -> Ctx.uncurryAssignment $ realIsNonZero sym
RealCosFn -> Ctx.uncurryAssignment $ realCos sym
RealSinFn -> Ctx.uncurryAssignment $ realSin sym
RealToSBVFn w -> Ctx.uncurryAssignment $ \v -> realToSBV sym v w
RealToUBVFn w -> Ctx.uncurryAssignment $ \v -> realToBV sym v w
PredToBVFn w -> Ctx.uncurryAssignment $ \v -> predToBV sym v w
CplxIsNonZeroFn -> Ctx.uncurryAssignment $ \x -> do
(real_x :+ imag_x) <- cplxGetParts sym x
join $ orPred sym <$> realIsNonZero sym real_x <*> realIsNonZero sym imag_x
CplxIsRealFn -> Ctx.uncurryAssignment $ isReal sym
RealToComplexFn -> Ctx.uncurryAssignment $ cplxFromReal sym
RealPartOfCplxFn -> Ctx.uncurryAssignment $ getRealPart sym
ImagPartOfCplxFn -> Ctx.uncurryAssignment $ getImagPart sym
CplxNegFn -> Ctx.uncurryAssignment $ cplxNeg sym
CplxAddFn -> Ctx.uncurryAssignment $ cplxAdd sym
CplxSubFn -> Ctx.uncurryAssignment $ cplxSub sym
CplxMulFn -> Ctx.uncurryAssignment $ cplxMul sym
CplxRoundFn -> Ctx.uncurryAssignment $ cplxRound sym
CplxFloorFn -> Ctx.uncurryAssignment $ cplxFloor sym
CplxCeilFn -> Ctx.uncurryAssignment $ cplxCeil sym
CplxMagFn -> Ctx.uncurryAssignment $ cplxMag sym
CplxSqrtFn -> Ctx.uncurryAssignment $ cplxSqrt sym
CplxExpFn -> Ctx.uncurryAssignment $ cplxExp sym
CplxLogFn -> Ctx.uncurryAssignment $ cplxLog sym
CplxLogBaseFn b -> Ctx.uncurryAssignment $ cplxLogBase (toRational b) sym
CplxSinFn -> Ctx.uncurryAssignment $ cplxSin sym
CplxCosFn -> Ctx.uncurryAssignment $ cplxCos sym
CplxTanFn -> Ctx.uncurryAssignment $ cplxTan sym
-- | This class is provides functions needed to implement the symbolic
-- array intrinsic functions
class IsSymExprBuilder sym => MatlabSymbolicArrayBuilder sym where
-- | Create a Matlab solver function from its prototype.
mkMatlabSolverFn :: sym
-> MatlabSolverFn (SymExpr sym) args ret
-> IO (SymFn sym args ret)