GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-08-16 17:30:27 +03:00
Code Issues Projects Releases Wiki Activity

Initial support for floating point computation

Browse Source
This commit is contained in:
Iavor Diatchki 2020-06-10 17:14:58 -07:00
parent 7caf72abb4
commit 0047eaf77a
57 changed files with 3048 additions and 864 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
.gitmodules vendored
View File

@ -4,3 +4,6 @@
[submodule "dependencies/what4"]
path = dependencies/what4
url = https://github.com/GaloisInc/what4.git
[submodule "dependencies/libBF-hs"]
path = dependencies/libBF-hs
url = git@github.com:GaloisInc/libBF-hs.git

1
cabal.project
View File

@ -1,6 +1,7 @@
packages:
cryptol.cabal
tests
dependencies/libBF-hs
optional-packages:
dependencies/what4/what4

6
cryptol.cabal
View File

@ -56,6 +56,7 @@ library
gitrev >= 1.0,
GraphSCC >= 1.0.4,
heredoc >= 0.2,
libBF,
monad-control >= 1.0,
monadLib >= 3.7.2,
parameterized-utils >= 2.0.2,
@ -157,6 +158,8 @@ library
Cryptol.Eval.Arch,
Cryptol.Eval.Backend,
Cryptol.Eval.Concrete,
Cryptol.Eval.Concrete.Float,
Cryptol.Eval.Concrete.FloatHelpers,
Cryptol.Eval.Concrete.Value,
Cryptol.Eval.Env,
Cryptol.Eval.Generic,
@ -166,6 +169,9 @@ library
Cryptol.Eval.Type,
Cryptol.Eval.Value,
Cryptol.Eval.What4,
Cryptol.Eval.What4.Value,
Cryptol.Eval.What4.Float,
Cryptol.Eval.What4.SFloat,
Cryptol.Testing.Random,

1
dependencies/libBF-hs vendored Submodule

@ -0,0 +1 @@
Subproject commit 20335b895358d81f1f7ad093dac6f80aa6afecf6

16
lib/Cryptol.cry
View File

@ -197,6 +197,22 @@ primitive fromThenTo : {first, next, last, a, len}
, first != next
, lengthFromThenTo first next last == len) => [len]a
// Fractional Literals ---------------------
/** 'FLiteral n d r a' asserts that the type `a' contains the
fraction `n/d`. The flag `r` indicates if we should round (`r >= 1`)
or report an error if the number can't be represented exactly. */
primitive type FLiteral : # -> # -> # -> * -> Prop
/** A fractional literal corresponding to `m/n` */
primitive
fraction : { m, n, r, a } FLiteral m n r a => a
// The Zero class -------------------------------------------------------

155
lib/Float.cry Normal file
View File

@ -0,0 +1,155 @@
module Float where
primitive type ValidFloat : # -> # -> Prop
/** IEEE-754 floating point numbers. */
primitive type { exponent : #, precision : #}
ValidFloat exponent precision => Float exponent precision : *
/** An abbreviation for common 16-bit floating point numbers. */
type Float16 = Float 5 11
/** An abbreviation for common 32-bit floating point numbers. */
type Float32 = Float 8 24
/** An abbreviation for common 64-bit floating point numbers. */
type Float64 = Float 11 53
/** An abbreviation for common 128-bit floating point numbers. */
type Float128 = Float 15 113
/** An abbreviation for common 256-bit floating point numbers. */
type Float256 = Float 19 237
/* ----------------------------------------------------------------------
* Rounding modes (this should be an enumeration type, when we add these)
*---------------------------------------------------------------------- */
type RoundingMode = [3]
/** Round toward nearest, ties go to even. */
roundNearestEven, rne : RoundingMode
roundNearestEven = 0
rne = roundNearestEven
/** Round toward nearest, ties away from zero. */
roundNearestAway, rna : RoundingMode
roundNearestAway = 1
rna = roundNearestAway
/** Round toward positive infinity. */
roundPositive, rtp : RoundingMode
roundPositive = 2
rtp = roundPositive
/** Round toward negative infinity. */
roundNegative, rtn : RoundingMode
roundNegative = 3
rtn = roundNegative
/** Round toward zero. */
roundZero, rtz : RoundingMode
roundZero = 4
rtz = roundZero
/* ----------------------------------------------------------------------
* Constants
* ---------------------------------------------------------------------- */
/** Not a number. */
primitive
fpNaN : {e,p} ValidFloat e p => Float e p
/** Positive infinity. */
primitive
fpPosInf : {e,p} ValidFloat e p => Float e p
fpNegInf : {e,p} ValidFloat e p => Float e p
fpNegInf = - fpPosInf
/** Positive zero. */
fpPosZero : {e,p} ValidFloat e p => Float e p
fpPosZero = zero
/** Negative zero. */
fpNegZero : {e,p} ValidFloat e p => Float e p
fpNegZero = - fpPosZero
// Binary representations
/** A floating point number using the exact bit pattern,
in IEEE interchange format with layout:
(sign : [1]) # (biased_exponent : [e]) # (significand : [p-1])
*/
primitive
fpFromBits : {e,p} ValidFloat e p => [e + p] -> Float e p
/** Export a floating point number in IEEE interchange format with layout:
(sign : [1]) # (biased_exponent : [e]) # (significand : [p-1])
NaN is represented as:
* positive: sign == 0
* quiet with no info: significand == 0b1 # 0
*/
primitive
fpToBits : {e,p} ValidFloat e p => Float e p -> [e + p]
/* ----------------------------------------------------------------------
* Predicates
* ----------------------------------------------------------------------
*/
// Operations in `Cmp` use IEEE reasoning.
/** Check if two floating point numbers are representationally the same.
In particular, the following hold:
* NaN =.= NaN
* ~ (pfNegZero =.= fpPosZero)
*/
primitive
(=.=) : {e,p} ValidFloat e p => Float e p -> Float e p -> Bool
infix 20 =.=
/* ----------------------------------------------------------------------
* Arithmetic
* ---------------------------------------------------------------------- */
/** Add floating point numbers using the given rounding mode. */
primitive
fpAdd : {e,p} ValidFloat e p =>
RoundingMode -> Float e p -> Float e p -> Float e p
/** Subtract floating point numbers using the given rounding mode. */
primitive
fpSub : {e,p} ValidFloat e p =>
RoundingMode -> Float e p -> Float e p -> Float e p
/** Multiply floating point numbers using the given rounding mode. */
primitive
fpMul : {e,p} ValidFloat e p =>
RoundingMode -> Float e p -> Float e p -> Float e p
/** Divide floating point numbers using the given rounding mode. */
primitive
fpDiv : {e,p} ValidFloat e p =>
RoundingMode -> Float e p -> Float e p -> Float e p

5
src/Cryptol/Eval.hs
View File

@ -63,10 +63,10 @@ import Prelude.Compat
type EvalEnv = GenEvalEnv Concrete
type EvalPrims sym =
( Backend sym, ?evalPrim :: Ident -> Maybe (GenValue sym) )
( Backend sym, ?evalPrim :: PrimIdent -> Maybe (GenValue sym) )
type ConcPrims =
?evalPrim :: Ident -> Maybe (GenValue Concrete)
?evalPrim :: PrimIdent -> Maybe (GenValue Concrete)
-- Expression Evaluation -------------------------------------------------------
@ -426,6 +426,7 @@ etaDelay sym msg env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0
case tp of
TVBit -> v
TVInteger -> v
TVFloat {} -> v
TVIntMod _ -> v
TVRational -> v
TVArray{} -> v

48
src/Cryptol/Eval/Backend.hs
View File

@ -6,6 +6,7 @@ module Cryptol.Eval.Backend
, invalidIndex
, cryUserError
, cryNoPrimError
, FPArith2
-- * Rationals
, SRational(..)
@ -213,6 +214,7 @@ class MonadIO (SEval sym) => Backend sym where
type SBit sym :: Type
type SWord sym :: Type
type SInteger sym :: Type
type SFloat sym :: Type
type SEval sym :: Type -> Type
-- ==== Evaluation monad operations ====
@ -260,6 +262,10 @@ class MonadIO (SEval sym) => Backend sym where
-- | Pretty-print an integer value
ppInteger :: sym -> PPOpts -> SInteger sym -> Doc
-- | Pretty-print a floating-point value
ppFloat :: sym -> PPOpts -> SFloat sym -> Doc
-- ==== Identifying literal values ====
-- | Determine if this symbolic bit is a boolean literal
@ -297,6 +303,14 @@ class MonadIO (SEval sym) => Backend sym where
Integer {- ^ Value -} ->
SEval sym (SInteger sym)
-- | Construct a floating point value from the given rational.
fpLit ::
sym ->
Integer {- ^ exponent bits -} ->
Integer {- ^ precision bits -} ->
Rational {- ^ The rational -} ->
SEval sym (SFloat sym)
-- ==== If/then/else operations ====
iteBit :: sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
iteWord :: sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
@ -650,3 +664,37 @@ class MonadIO (SEval sym) => Backend sym where
SInteger sym ->
SInteger sym ->
SEval sym (SBit sym)
-- == Float Operations ==
fpEq :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
fpLessThan :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
fpGreaterThan :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
fpPlus, fpMinus, fpMult, fpDiv :: FPArith2 sym
fpNeg :: sym -> SFloat sym -> SEval sym (SFloat sym)
fpToInteger ::
sym ->
String {- ^ Name of the function for error reporting -} ->
SWord sym {-^ Rounding mode -} ->
SFloat sym -> SEval sym (SInteger sym)
fpFromInteger ::
sym ->
Integer {- exp width -} ->
Integer {- prec width -} ->
SWord sym {- ^ rounding mode -} ->
SInteger sym {- ^ the integeer to use -} ->
SEval sym (SFloat sym)
type FPArith2 sym =
sym ->
SWord sym ->
SFloat sym ->
SFloat sym ->
SEval sym (SFloat sym)

43
src/Cryptol/Eval/Concrete.hs
View File

@ -9,6 +9,7 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE RecordWildCards #-}
@ -27,13 +28,16 @@ import Control.Monad (join,guard,zipWithM)
import Data.List(sortBy)
import Data.Ord(comparing)
import Data.Bits (Bits(..))
import Data.Ratio(numerator,denominator)
import MonadLib( ChoiceT, findOne, lift )
import qualified LibBF as FP
import qualified Data.Map.Strict as Map
import qualified Data.Text as T
import Cryptol.TypeCheck.Solver.InfNat (Nat'(..))
import Cryptol.Eval.Backend
import Cryptol.Eval.Concrete.Float(floatPrims)
import Cryptol.Eval.Concrete.FloatHelpers(bfValue)
import Cryptol.Eval.Concrete.Value
import Cryptol.Eval.Generic hiding (logicShift)
import Cryptol.Eval.Monad
@ -43,7 +47,7 @@ import Cryptol.ModuleSystem.Name
import Cryptol.Testing.Random (randomV)
import Cryptol.TypeCheck.AST as AST
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.Ident (Ident,mkIdent)
import Cryptol.Utils.Ident (PrimIdent,prelPrim,floatPrim)
import Cryptol.Utils.PP
import Cryptol.Utils.Logger(logPrint)
@ -59,7 +63,8 @@ toExpr :: PrimMap -> AST.Type -> Value -> Eval (Maybe AST.Expr)
toExpr prims t0 v0 = findOne (go t0 v0)
where
prim n = ePrim prims (mkIdent (T.pack n))
prim n = ePrim prims (prelPrim n)
go :: AST.Type -> Value -> ChoiceT Eval Expr
go ty val = case (tNoUser ty, val) of
@ -81,6 +86,9 @@ toExpr prims t0 v0 = findOne (go t0 v0)
do let n' = ETApp (ETApp (prim "number") (tNum n)) (TCon (TC TCInteger) [])
d' = ETApp (ETApp (prim "number") (tNum d)) (TCon (TC TCInteger) [])
return $ EApp (EApp (prim "ratio") n') d'
(TCon (TC TCFloat) [eT,pT], VFloat i) ->
pure (floatToExpr prims eT pT (bfValue i))
(TCon (TC TCSeq) [a,b], VSeq 0 _) -> do
guard (a == tZero)
return $ EList [] b
@ -102,15 +110,36 @@ toExpr prims t0 v0 = findOne (go t0 v0)
, render doc
]
floatToExpr :: PrimMap -> AST.Type -> AST.Type -> FP.BigFloat -> AST.Expr
floatToExpr prims eT pT f =
case FP.bfToRep f of
FP.BFNaN -> mkP "fpNaN"
FP.BFRep sign num ->
case (sign,num) of
(FP.Pos, FP.Zero) -> mkP "fpPosZero"
(FP.Neg, FP.Zero) -> mkP "fpNegZero"
(FP.Pos, FP.Inf) -> mkP "fpPosInf"
(FP.Neg, FP.Inf) -> mkP "fpNegInf"
(_, FP.Num m e) ->
let r = toRational m * (2 ^^ e)
in EProofApp $ ePrim prims (prelPrim "fraction")
`ETApp` tNum (numerator r)
`ETApp` tNum (denominator r)
`ETApp` tNum (0 :: Int)
`ETApp` tFloat eT pT
where
mkP n = EProofApp $ ePrim prims (floatPrim n) `ETApp` eT `ETApp` pT
-- Primitives ------------------------------------------------------------------
evalPrim :: Ident -> Maybe Value
evalPrim :: PrimIdent -> Maybe Value
evalPrim prim = Map.lookup prim primTable
primTable :: Map.Map Ident Value
primTable :: Map.Map PrimIdent Value
primTable = let sym = Concrete in
Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
Map.union (floatPrims sym) $
Map.fromList $ map (\(n, v) -> (prelPrim n, v))
[ -- Literals
("True" , VBit (bitLit sym True))
, ("False" , VBit (bitLit sym False))
@ -118,6 +147,8 @@ primTable = let sym = Concrete in
ecNumberV sym)
, ("ratio" , {-# SCC "Prelude::ratio" #-}
ratioV sym)
, ("fraction" , ecFractionV sym)
-- Zero
, ("zero" , {-# SCC "Prelude::zero" #-}

147
src/Cryptol/Eval/Concrete/Float.hs Normal file
View File

@ -0,0 +1,147 @@
{-# Language BlockArguments #-}
{-# Language OverloadedStrings #-}
{-# Language BangPatterns #-}
-- | Concrete evaluations for floating point primitives.
module Cryptol.Eval.Concrete.Float where
import Data.Map(Map)
import Data.Bits(testBit,setBit,shiftL,shiftR,(.&.),(.|.))
import Data.Int(Int64)
import qualified Data.Map as Map
import LibBF
import Cryptol.Utils.Ident(PrimIdent, floatPrim)
import Cryptol.Utils.Panic(panic)
import Cryptol.Eval.Value
import Cryptol.Eval.Generic
import Cryptol.Eval.Concrete.Value
import Cryptol.Eval.Concrete.FloatHelpers
floatPrims :: Concrete -> Map PrimIdent Value
floatPrims sym = Map.fromList [ (floatPrim i,v) | (i,v) <- nonInfixTable ]
where
(~>) = (,)
nonInfixTable =
[ "fpNaN" ~> ilam \e -> ilam \p ->
VFloat BF { bfValue = bfNaN
, bfExpWidth = e, bfPrecWidth = p }
, "fpPosInf" ~> ilam \e -> ilam \p ->
VFloat BF { bfValue = bfPosInf
, bfExpWidth = e, bfPrecWidth = p }
, "fpFromBits" ~> ilam \e -> ilam \p -> wlam sym \bv ->
pure $ VFloat $ floatFromBits e p $ bvVal bv
, "fpToBits" ~> ilam \e -> ilam \p -> flam \x ->
pure $ word sym (e + p)
$ floatToBits e p
$ bfValue x
, "=.=" ~> ilam \_ -> ilam \_ -> flam \x -> pure $ flam \y ->
pure $ VBit
$ bitLit sym
$ bfCompare (bfValue x) (bfValue y) == EQ
-- From Backend class
, "fpAdd" ~> fpBinArithV sym fpPlus
, "fpSub" ~> fpBinArithV sym fpMinus
, "fpMul" ~> fpBinArithV sym fpMult
, "fpDiv" ~> fpBinArithV sym fpDiv
]
floatFromBits ::
Integer {- ^ Exponent width -} ->
Integer {- ^ Precision widht -} ->
Integer {- ^ Raw bits -} ->
BF
floatFromBits e p bv = BF { bfValue = floatFromBits' e p bv
, bfExpWidth = e, bfPrecWidth = p }
-- | Make a float using "raw" bits.
floatFromBits' ::
Integer {- ^ Exponent width -} ->
Integer {- ^ Precision widht -} ->
Integer {- ^ Raw bits -} ->
BigFloat
floatFromBits' e p bits
| expoBiased == 0 && mant == 0 = -- zero
if isNeg then bfNegZero else bfPosZero
| expoBiased == eMask && mant == 0 = -- infinity
if isNeg then bfNegInf else bfPosInf
| expoBiased == eMask = bfNaN -- NaN
| expoBiased == 0 = -- Subnormal
case bfMul2Exp opts (bfFromInteger mant) (expoVal + 1) of
(num,Ok) -> if isNeg then bfNeg num else num
(_,s) -> panic "floatFromBits" [ "Unexpected status: " ++ show s ]
| otherwise = -- Normal
case bfMul2Exp opts (bfFromInteger mantVal) expoVal of
(num,Ok) -> if isNeg then bfNeg num else num
(_,s) -> panic "floatFromBits" [ "Unexpected status: " ++ show s ]
where
opts = expBits e' <> precBits (p' + 1) <> allowSubnormal
e' = fromInteger e :: Int
p' = fromInteger p - 1 :: Int
eMask = (1 `shiftL` e') - 1 :: Int64
pMask = (1 `shiftL` p') - 1 :: Integer
isNeg = testBit bits (e' + p')
mant = pMask .&. bits :: Integer
mantVal = mant `setBit` p' :: Integer
-- accounts for the implicit 1 bit
expoBiased = eMask .&. fromInteger (bits `shiftR` p') :: Int64
bias = eMask `shiftR` 1 :: Int64
expoVal = expoBiased - bias - fromIntegral p' :: Int64
-- | Turn a float into raw bits.
-- @NaN@ is represented as a positive "quiet" @NaN@
-- (most significant bit in the significand is set, the rest of it is 0)
floatToBits :: Integer -> Integer -> BigFloat -> Integer
floatToBits e p bf = (isNeg `shiftL` (e' + p'))
.|. (expBiased `shiftL` p')
.|. (mant `shiftL` 0)
where
e' = fromInteger e :: Int
p' = fromInteger p - 1 :: Int
eMask = (1 `shiftL` e') - 1 :: Integer
pMask = (1 `shiftL` p') - 1 :: Integer
(isNeg, expBiased, mant) =
case bfToRep bf of
BFNaN -> (0, eMask, 1 `shiftL` (p' - 1))
BFRep s num -> (sign, be, ma)
where
sign = case s of
Neg -> 1
Pos -> 0
(be,ma) =
case num of
Zero -> (0,0)
Num i ev
| ex == 0 -> (0, i `shiftL` (p' - m -1))
| otherwise -> (ex, (i `shiftL` (p' - m)) .&. pMask)
where
m = msb 0 i - 1
bias = eMask `shiftR` 1
ex = toInteger ev + bias + toInteger m
Inf -> (eMask,0)
msb !n j = if j == 0 then n else msb (n+1) (j `shiftR` 1)

138
src/Cryptol/Eval/Concrete/FloatHelpers.hs Normal file
View File

@ -0,0 +1,138 @@
{-# Language BlockArguments #-}
module Cryptol.Eval.Concrete.FloatHelpers where
import Data.Ratio
import LibBF
import Cryptol.Utils.PP
import Cryptol.Utils.Panic(panic)
import Cryptol.Eval.Backend
import Cryptol.Eval.Monad( EvalError(..)
, PPOpts(..), PPFloatFormat(..), PPFloatExp(..)
)
data BF = BF
{ bfExpWidth :: Integer
, bfPrecWidth :: Integer
, bfValue :: BigFloat
}
-- | Make LibBF options for the given precision and rounding mode.
fpOpts ::
Backend sym =>
sym {- ^ backend -} ->
Integer {- ^ expoinent bits -} ->
Integer {- ^ precision bits -} ->
Integer {- ^ rounding mode, as defined in `Float.cry` -} ->
SEval sym BFOpts
fpOpts sym e p r =
case ok of
Just opts -> case fpRound r of
Just m -> pure (rnd m <> opts)
Nothing -> raiseError sym (BadRoundingMode r)
Nothing -> panic "floatOpts" [ "Invalid Float size"
, "exponent: " ++ show e
, "precision: " ++ show p
]
where
ok =
do eb <- rng expBits expBitsMin expBitsMax e
pb <- rng precBits precBitsMin precBitsMax p
pure (eb <> pb <> allowSubnormal)
rng f a b x = if toInteger a <= x && x <= toInteger b
then Just (f (fromInteger x))
else Nothing
-- | Mapping from the rounding modes defined in the `Float.cry` to
-- the rounding modes of `LibBF`.
fpRound :: Integer -> Maybe RoundMode
fpRound n =
case n of
0 -> Just NearEven
1 -> Just NearAway
2 -> Just ToPosInf
3 -> Just ToNegInf
4 -> Just ToZero
_ -> Nothing
-- | Check that we didn't get an unexpected status.
fpCheckStatus :: Backend sym => sym -> (BigFloat,Status) -> SEval sym BigFloat
fpCheckStatus _sym (r,s) =
case s of
MemError -> panic "checkStatus" [ "libBF: Memory error" ]
_ -> pure r
-- | Pretty print a float
fpPP :: PPOpts -> BF -> Doc
fpPP opts bf = text $ bfToString base fmt num
where
num = bfValue bf
precW = bfPrecWidth bf
base = useFPBase opts
withExp :: PPFloatExp -> ShowFmt -> ShowFmt
withExp e f = case e of
AutoExponent -> f
ForceExponent -> f <> forceExp
fmt = addPrefix <> showRnd NearEven <>
case useFPFormat opts of
FloatFree e -> withExp e $ showFreeMin
$ Just $ fromInteger precW
FloatFixed n e -> withExp e $ showFixed $ fromIntegral n
FloatFrac n -> showFrac $ fromIntegral n
-- | Make a literal
fpLit ::
Backend sym =>
sym ->
Integer {- ^ Exponent width -} ->
Integer {- ^ Precision width -} ->
Rational ->
SEval sym BF
fpLit sym e p r =
do opts <- fpOpts sym e p 0 -- round to nearest even
let num = bfFromInteger (numerator r)
res
| denominator r == 1 = bfRoundFloat opts num
| otherwise = bfDiv opts num (bfFromInteger (denominator r))
v <- fpCheckStatus sym res
pure BF { bfExpWidth = e, bfPrecWidth = p, bfValue = v }
fpToI :: RoundMode -> BigFloat -> Maybe Integer
fpToI r flt =
case bfToRep flt of
BFNaN -> Nothing
BFRep s num ->
case num of
Zero -> pure 0
Inf -> Nothing
Num i ev ->
pure
case r of
NearEven -> round $ addSign rat
NearAway -> addSign $ ceiling rat
ToPosInf -> ceiling $ addSign rat
ToNegInf -> floor $ addSign rat
ToZero -> truncate rat
_ -> panic "fpCvtToInteger"
["Unexpected rounding mode", show r]
where
rat = fromInteger i * 2 ^^ ev :: Rational
addSign :: Num a => a -> a
addSign = case s of
Pos -> id
Neg -> negate

63
src/Cryptol/Eval/Concrete/Value.hs
View File

@ -1,4 +1,4 @@
-- |
-- |fpToInteger r e p f
-- Module : Cryptol.Eval.Concrete.Value
-- Copyright : (c) 2013-2020 Galois, Inc.
-- License : BSD3
@ -7,6 +7,7 @@
-- Portability : portable
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PatternGuards #-}
@ -32,13 +33,16 @@ module Cryptol.Eval.Concrete.Value
, Value
, Concrete(..)
, liftBinIntMod
, fpBinArith
) where
import qualified Control.Exception as X
import Data.Bits
import Numeric (showIntAtBase)
import qualified LibBF as FP
import qualified Cryptol.Eval.Arch as Arch
import qualified Cryptol.Eval.Concrete.FloatHelpers as FP
import Cryptol.Eval.Monad
import Cryptol.Eval.Value
import Cryptol.TypeCheck.Solver.InfNat (genLog)
@ -131,6 +135,7 @@ instance Backend Concrete where
type SBit Concrete = Bool
type SWord Concrete = BV
type SInteger Concrete = Integer
type SFloat Concrete = FP.BF
type SEval Concrete = Eval
raiseError _ err = io (X.throwIO err)
@ -164,6 +169,8 @@ instance Backend Concrete where
ppInteger _ _opts i = integer i
ppFloat _ = FP.fpPP
bitLit _ b = b
bitAsLit _ b = Just b
@ -313,9 +320,63 @@ instance Backend Concrete where
znNegate _ 0 _ = evalPanic "znNegate" ["0 modulus not allowed"]
znNegate _ m x = pure $! (negate x) `mod` m
------------------------------------------------------------------------
-- Floating Point
fpLit = FP.fpLit
fpEq _sym x y = pure (FP.bfValue x == FP.bfValue y)
fpLessThan _sym x y = pure (FP.bfValue x < FP.bfValue y)
fpGreaterThan _sym x y = pure (FP.bfValue x > FP.bfValue y)
fpPlus = fpBinArith FP.bfAdd
fpMinus = fpBinArith FP.bfSub
fpMult = fpBinArith FP.bfMul
fpDiv = fpBinArith FP.bfDiv
fpNeg _ x = pure x { FP.bfValue = FP.bfNeg (FP.bfValue x) }
fpFromInteger sym e p r x =
do opts <- FP.fpOpts sym e p (bvVal r)
v <- FP.fpCheckStatus sym (FP.bfRoundInt opts (FP.bfFromInteger x))
pure FP.BF { FP.bfExpWidth = e, FP.bfPrecWidth = p, FP.bfValue = v }
fpToInteger = fpCvtToInteger
{-# INLINE liftBinIntMod #-}
liftBinIntMod :: Monad m =>
(Integer -> Integer -> Integer) -> Integer -> Integer -> Integer -> m Integer
liftBinIntMod op m x y
| m == 0 = evalPanic "znArithmetic" ["0 modulus not allowed"]
| otherwise = pure $ (op x y) `mod` m
{-# INLINE fpBinArith #-}
fpBinArith ::
(FP.BFOpts -> FP.BigFloat -> FP.BigFloat -> (FP.BigFloat, FP.Status)) ->
Concrete ->
SWord Concrete {- ^ Rouding mode -} ->
SFloat Concrete ->
SFloat Concrete ->
SEval Concrete (SFloat Concrete)
fpBinArith fun = \sym r x y ->
do opts <- FP.fpOpts sym (FP.bfExpWidth x) (FP.bfPrecWidth x) (bvVal r)
v <- FP.fpCheckStatus sym (fun opts (FP.bfValue x) (FP.bfValue y))
pure x { FP.bfValue = v }
fpCvtToInteger ::
Concrete ->
String ->
SWord Concrete {- ^ Rounding mode -} ->
SFloat Concrete ->
SEval Concrete (SInteger Concrete)
fpCvtToInteger sym fun (bvVal -> rnd) (FP.bfValue -> flt) =
case FP.fpRound rnd of
Nothing -> raiseError sym (BadRoundingMode rnd)
Just mode ->
case FP.fpToI mode flt of
Just i -> pure i
Nothing -> raiseError sym (BadValue fun)

152
src/Cryptol/Eval/Generic.hs
View File

@ -7,6 +7,7 @@
-- Portability : portable
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE MultiParamTypeClasses #-}
@ -26,6 +27,7 @@ import Control.Monad (join, unless)
import Data.Bits (testBit)
import Data.Maybe (fromMaybe)
import Data.Ratio ((%))
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),nMul,widthInteger)
@ -52,6 +54,7 @@ mkLit sym ty i =
TVIntMod m
| m == 0 -> evalPanic "mkLit" ["0 modulus not allowed"]
| otherwise -> VInteger <$> integerLit sym (i `mod` m)
TVFloat e p -> VFloat <$> fpLit sym e p (fromInteger i)
TVSeq w TVBit -> pure $ word sym w i
TVRational -> VRational <$> (intToRational sym =<< integerLit sym i)
_ -> evalPanic "Cryptol.Eval.Prim.evalConst"
@ -74,11 +77,12 @@ ecNumberV sym =
]
{-# SPECIALIZE intV :: Concrete -> Integer -> TValue -> Eval (GenValue Concrete)
#-}
intV :: Backend sym => sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)
intV sym i = ringNullary sym (\w -> wordFromInt sym w i) (pure i) (\m -> intToZn sym m i) (intToRational sym i)
(\e p -> fpRndMode sym >>= \r -> fpFromInteger sym e p r i)
{-# SPECIALIZE ratioV :: Concrete -> GenValue Concrete #-}
ratioV :: Backend sym => sym -> GenValue sym
@ -89,6 +93,26 @@ ratioV sym =
y' <- fromVInteger <$> y
VRational <$> ratio sym x' y'
{-# SPECIALIZE ecFractionV :: Concrete -> GenValue Concrete
#-}
ecFractionV :: Backend sym => sym -> GenValue sym
ecFractionV sym =
ilam \n ->
ilam \d ->
ilam \_r ->
VPoly \ty ->
case ty of
TVFloat e p -> VFloat <$> fpLit sym e p (n % d)
TVRational ->
do x <- integerLit sym n
y <- integerLit sym d
VRational <$> ratio sym x y
_ -> evalPanic "ecFractionV"
[ "Unexpected `FLiteral` type: " ++ show ty ]
{-# SPECIALIZE fromZV :: Concrete -> GenValue Concrete #-}
fromZV :: Backend sym => sym -> GenValue sym
fromZV sym =
@ -124,6 +148,7 @@ type BinWord sym = Integer -> SWord sym -> SWord sym -> SEval sym (SWord sym)
(SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
(Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
(SRational Concrete -> SRational Concrete -> SEval Concrete (SRational Concrete)) ->
(SFloat Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete)) ->
Binary Concrete
#-}
@ -134,8 +159,9 @@ ringBinary :: forall sym.
(SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->
(Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->
(SRational sym -> SRational sym -> SEval sym (SRational sym)) ->
(SFloat sym -> SFloat sym -> SEval sym (SFloat sym)) ->
Binary sym
ringBinary sym opw opi opz opq = loop
ringBinary sym opw opi opz opq opfp = loop
where
loop' :: TValue
-> SEval sym (GenValue sym)
@ -157,6 +183,9 @@ ringBinary sym opw opi opz opq = loop
TVIntMod n ->
VInteger <$> opz n (fromVInteger l) (fromVInteger r)
TVFloat {} ->
VFloat <$> opfp (fromVFloat l) (fromVFloat r)
TVRational ->
VRational <$> opq (fromVRational l) (fromVRational r)
@ -209,6 +238,7 @@ type UnaryWord sym = Integer -> SWord sym -> SEval sym (SWord sym)
(SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
(Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
(SRational Concrete -> SEval Concrete (SRational Concrete)) ->
(SFloat Concrete -> SEval Concrete (SFloat Concrete)) ->
Unary Concrete
#-}
ringUnary :: forall sym.
@ -218,8 +248,9 @@ ringUnary :: forall sym.
(SInteger sym -> SEval sym (SInteger sym)) ->
(Integer -> SInteger sym -> SEval sym (SInteger sym)) ->
(SRational sym -> SEval sym (SRational sym)) ->
(SFloat sym -> SEval sym (SFloat sym)) ->
Unary sym
ringUnary sym opw opi opz opq = loop
ringUnary sym opw opi opz opq opfp = loop
where
loop' :: TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
loop' ty v = loop ty =<< v
@ -236,6 +267,9 @@ ringUnary sym opw opi opz opq = loop
TVIntMod n ->
VInteger <$> opz n (fromVInteger v)
TVFloat {} ->
VFloat <$> opfp (fromVFloat v)
TVRational ->
VRational <$> opq (fromVRational v)
@ -277,6 +311,7 @@ ringUnary sym opw opi opz opq = loop
SEval Concrete (SInteger Concrete) ->
(Integer -> SEval Concrete (SInteger Concrete)) ->
SEval Concrete (SRational Concrete) ->
(Integer -> Integer -> SEval Concrete (SFloat Concrete)) ->
TValue ->
SEval Concrete (GenValue Concrete)
#-}
@ -288,9 +323,10 @@ ringNullary :: forall sym.
SEval sym (SInteger sym) ->
(Integer -> SEval sym (SInteger sym)) ->
SEval sym (SRational sym) ->
(Integer -> Integer -> SEval sym (SFloat sym)) ->
TValue ->
SEval sym (GenValue sym)
ringNullary sym opw opi opz opq = loop
ringNullary sym opw opi opz opq opfp = loop
where
loop :: TValue -> SEval sym (GenValue sym)
loop ty =
@ -301,6 +337,8 @@ ringNullary sym opw opi opz opq = loop
TVIntMod n -> VInteger <$> opz n
TVFloat e p -> VFloat <$> opfp e p
TVRational -> VRational <$> opq
TVArray{} -> evalPanic "arithNullary" ["Array not in class Ring"]
@ -374,39 +412,43 @@ fromIntegerV sym =
{-# INLINE addV #-}
addV :: Backend sym => sym -> Binary sym
addV sym = ringBinary sym opw opi opz opq
addV sym = ringBinary sym opw opi opz opq opfp
where
opw _w x y = wordPlus sym x y
opi x y = intPlus sym x y
opz m x y = znPlus sym m x y
opq x y = rationalAdd sym x y
opfp x y = fpRndMode sym >>= \r -> fpPlus sym r x y
{-# INLINE subV #-}
subV :: Backend sym => sym -> Binary sym
subV sym = ringBinary sym opw opi opz opq
subV sym = ringBinary sym opw opi opz opq opfp
where
opw _w x y = wordMinus sym x y
opi x y = intMinus sym x y
opz m x y = znMinus sym m x y
opq x y = rationalSub sym x y
opfp x y = fpRndMode sym >>= \r -> fpMinus sym r x y
{-# INLINE negateV #-}
negateV :: Backend sym => sym -> Unary sym
negateV sym = ringUnary sym opw opi opz opq
negateV sym = ringUnary sym opw opi opz opq opfp
where
opw _w x = wordNegate sym x
opi x = intNegate sym x
opz m x = znNegate sym m x
opq x = rationalNegate sym x
opfp x = fpNeg sym x
{-# INLINE mulV #-}
mulV :: Backend sym => sym -> Binary sym
mulV sym = ringBinary sym opw opi opz opq
mulV sym = ringBinary sym opw opi opz opq opfp
where
opw _w x y = wordMult sym x y
opi x y = intMult sym x y
opz m x y = znMult sym m x y
opq x y = rationalMul sym x y
opfp x y = fpRndMode sym >>= \r -> fpMult sym r x y
--------------------------------------------------
-- Integral
@ -504,6 +546,12 @@ recipV sym =
lam $ \x ->
case a of
TVRational -> VRational <$> (rationalRecip sym . fromVRational =<< x)
TVFloat e p ->
do one <- fpLit sym e p 1
r <- fpRndMode sym
xv <- fromVFloat <$> x
VFloat <$> fpDiv sym r one xv
_ -> evalPanic "recip" [show a ++ "is not a Field"]
{-# SPECIALIZE fieldDivideV :: Concrete -> GenValue Concrete #-}
@ -517,6 +565,11 @@ fieldDivideV sym =
do x' <- fromVRational <$> x
y' <- fromVRational <$> y
VRational <$> rationalDivide sym x' y'
TVFloat _e _p ->
do xv <- fromVFloat <$> x
yv <- fromVFloat <$> y
r <- fpRndMode sym
VFloat <$> fpDiv sym r xv yv
_ -> evalPanic "recip" [show a ++ "is not a Field"]
--------------------------------------------------------------
@ -526,43 +579,56 @@ fieldDivideV sym =
Concrete ->
String ->
(SRational Concrete -> SEval Concrete (SInteger Concrete)) ->
(SFloat Concrete -> SEval Concrete (SInteger Concrete)) ->
Unary Concrete #-}
roundOp :: Backend sym => sym -> String -> (SRational sym -> SEval sym (SInteger sym)) -> Unary sym
roundOp _sym nm qop ty v =
roundOp ::
Backend sym =>
sym ->
String ->
(SRational sym -> SEval sym (SInteger sym)) ->
(SFloat sym -> SEval sym (SInteger sym)) ->
Unary sym
roundOp _sym nm qop opfp ty v =
case ty of
TVRational -> VInteger <$> (qop (fromVRational v))
TVRational -> VInteger <$> (qop (fromVRational v))
TVFloat _ _ -> VInteger <$> opfp (fromVFloat v)
_ -> evalPanic nm [show ty ++ " is not a Field"]
{-# INLINE floorV #-}
floorV :: Backend sym => sym -> Unary sym
floorV sym = roundOp sym "floor" opq
floorV sym = roundOp sym "floor" opq opfp
where
opq = rationalFloor sym
opfp = \x -> fpRndRTN sym >>= \r -> fpToInteger sym "floor" r x
{-# INLINE ceilingV #-}
ceilingV :: Backend sym => sym -> Unary sym
ceilingV sym = roundOp sym "ceiling" opq
ceilingV sym = roundOp sym "ceiling" opq opfp
where
opq = rationalCeiling sym
opfp = \x -> fpRndRTP sym >>= \r -> fpToInteger sym "ceiling" r x
{-# INLINE truncV #-}
truncV :: Backend sym => sym -> Unary sym
truncV sym = roundOp sym "trunc" opq
truncV sym = roundOp sym "trunc" opq opfp
where
opq = rationalTrunc sym
opfp = \x -> fpRndRTZ sym >>= \r -> fpToInteger sym "trunc" r x
{-# INLINE roundAwayV #-}
roundAwayV :: Backend sym => sym -> Unary sym
roundAwayV sym = roundOp sym "roundAway" opq
roundAwayV sym = roundOp sym "roundAway" opq opfp
where
opq = rationalRoundAway sym
opfp = \x -> fpRndRNA sym >>= \r -> fpToInteger sym "roundAway" r x
{-# INLINE roundToEvenV #-}
roundToEvenV :: Backend sym => sym -> Unary sym
roundToEvenV sym = roundOp sym "roundToEven" opq
roundToEvenV sym = roundOp sym "roundToEven" opq opfp
where
opq = rationalRoundToEven sym
opfp = \x -> fpRndRNE sym >>= \r -> fpToInteger sym "roundToEven" r x
--------------------------------------------------------------
-- Logic
@ -617,6 +683,7 @@ smodV sym =
(SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) ->
(Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) ->
(SRational Concrete -> SRational Concrete -> SEval Concrete a -> SEval Concrete a) ->
(SFloat Concrete -> SFloat Concrete -> SEval Concrete a -> SEval Concrete a) ->
(TValue -> GenValue Concrete -> GenValue Concrete -> SEval Concrete a -> SEval Concrete a)
#-}
@ -628,13 +695,15 @@ cmpValue ::
(SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) ->
(Integer -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) ->
(SRational sym -> SRational sym -> SEval sym a -> SEval sym a) ->
(SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a) ->
(TValue -> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a)
cmpValue sym fb fw fi fz fq = cmp
cmpValue sym fb fw fi fz fq ff = cmp
where
cmp ty v1 v2 k =
case ty of
TVBit -> fb (fromVBit v1) (fromVBit v2) k
TVInteger -> fi (fromVInteger v1) (fromVInteger v2) k
TVFloat _ _ -> ff (fromVFloat v1) (fromVFloat v2) k
TVIntMod n -> fz n (fromVInteger v1) (fromVInteger v2) k
TVRational -> fq (fromVRational v1) (fromVRational v2) k
TVArray{} -> panic "Cryptol.Prims.Value.cmpValue"
@ -679,35 +748,38 @@ bitGreaterThan sym x y = bitLessThan sym y x
{-# INLINE valEq #-}
valEq :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)
valEq sym ty v1 v2 = cmpValue sym fb fw fi fz fq ty v1 v2 (pure $ bitLit sym True)
valEq sym ty v1 v2 = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure $ bitLit sym True)
where
fb x y k = eqCombine sym (bitEq sym x y) k
fw x y k = eqCombine sym (wordEq sym x y) k
fi x y k = eqCombine sym (intEq sym x y) k
fz m x y k = eqCombine sym (znEq sym m x y) k
fq x y k = eqCombine sym (rationalEq sym x y) k
ff x y k = eqCombine sym (fpEq sym x y) k
{-# INLINE valLt #-}
valLt :: Backend sym =>
sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)
valLt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq ty v1 v2 (pure final)
valLt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure final)
where
fb x y k = lexCombine sym (bitLessThan sym x y) (bitEq sym x y) k
fw x y k = lexCombine sym (wordLessThan sym x y) (wordEq sym x y) k
fi x y k = lexCombine sym (intLessThan sym x y) (intEq sym x y) k
fz _ _ _ _ = panic "valLt" ["Z_n is not in `Cmp`"]
fq x y k = lexCombine sym (rationalLessThan sym x y) (rationalEq sym x y) k
ff x y k = lexCombine sym (fpLessThan sym x y) (fpEq sym x y) k
{-# INLINE valGt #-}
valGt :: Backend sym =>
sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)
valGt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq ty v1 v2 (pure final)
valGt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure final)
where
fb x y k = lexCombine sym (bitGreaterThan sym x y) (bitEq sym x y) k
fw x y k = lexCombine sym (wordGreaterThan sym x y) (wordEq sym x y) k
fi x y k = lexCombine sym (intGreaterThan sym x y) (intEq sym x y) k
fz _ _ _ _ = panic "valGt" ["Z_n is not in `Cmp`"]
fq x y k = lexCombine sym (rationalGreaterThan sym x y) (rationalEq sym x y) k
ff x y k = lexCombine sym (fpGreaterThan sym x y) (fpEq sym x y) k
{-# INLINE eqCombine #-}
eqCombine :: Backend sym =>
@ -755,13 +827,14 @@ greaterThanEqV sym ty v1 v2 = VBit <$> valGt sym ty v1 v2 (bitLit sym True)
{-# INLINE signedLessThanV #-}
signedLessThanV :: Backend sym => sym -> Binary sym
signedLessThanV sym ty v1 v2 = VBit <$> cmpValue sym fb fw fi fz fq ty v1 v2 (pure $ bitLit sym False)
signedLessThanV sym ty v1 v2 = VBit <$> cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure $ bitLit sym False)
where
fb _ _ _ = panic "signedLessThan" ["Attempted to perform signed comparison on bit type"]
fw x y k = lexCombine sym (wordSignedLessThan sym x y) (wordEq sym x y) k
fi _ _ _ = panic "signedLessThan" ["Attempted to perform signed comparison on Integer type"]
fz m _ _ _ = panic "signedLessThan" ["Attempted to perform signed comparison on Z_" ++ show m ++ " type"]
fq _ _ _ = panic "signedLessThan" ["Attempted to perform signed comparison on Rational type"]
ff _ _ _ = panic "signedLessThan" ["Attempted to perform signed comparison on Float"]
@ -794,6 +867,10 @@ zeroV sym ty = case ty of
TVArray{} -> evalPanic "zeroV" ["Array not in class Zero"]
-- floating point
TVFloat e p ->
VFloat <$> fpLit sym e p 0
-- sequences
TVSeq w ety
| isTBit ety -> pure $ word sym w 0
@ -1199,6 +1276,7 @@ logicBinary sym opb opw = loop
TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]
TVArray{} -> evalPanic "logicBinary" ["Array not in class Logic"]
TVFloat {} -> evalPanic "logicBinary" ["Float not in class Logic"]
TVSeq w aty
-- words
| isTBit aty
@ -1274,6 +1352,7 @@ logicUnary sym opb opw = loop
TVInteger -> evalPanic "logicUnary" ["Integer not in class Logic"]
TVIntMod _ -> evalPanic "logicUnary" ["Z not in class Logic"]
TVFloat {} -> evalPanic "logicUnary" ["Float not in class Logic"]
TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]
TVArray{} -> evalPanic "logicUnary" ["Array not in class Logic"]
@ -1719,6 +1798,7 @@ errorV sym ty msg = case ty of
TVIntMod _ -> cryUserError sym msg
TVRational -> cryUserError sym msg
TVArray{} -> cryUserError sym msg
TVFloat {} -> cryUserError sym msg
-- sequences
TVSeq w ety
@ -1837,3 +1917,33 @@ mergeSeqMap :: Backend sym =>
mergeSeqMap sym c x y =
IndexSeqMap $ \i ->
iteValue sym c (lookupSeqMap x i) (lookupSeqMap y i)
--------------------------------------------------------------------------------
-- Floating Point Operations
-- | Make a Cryptol value for a binary arithmetic function.
fpBinArithV :: Backend sym => sym -> FPArith2 sym -> GenValue sym
fpBinArithV sym fun =
ilam \_ ->
ilam \_ ->
wlam sym \r ->
pure $ flam \x ->
pure $ flam \y ->
VFloat <$> fun sym r x y
-- | Rounding mode used in FP operations that do not specify it explicitly.
fpRndMode, fpRndRNE, fpRndRNA, fpRndRTP, fpRndRTN, fpRndRTZ ::
Backend sym => sym -> SEval sym (SWord sym)
fpRndMode = fpRndRNE
fpRndRNE sym = wordLit sym 3 0 {- to nearest, ties to even -}
fpRndRNA sym = wordLit sym 3 1 {- to nearest, ties to away from 0 -}
fpRndRTP sym = wordLit sym 3 2 {- to +inf -}
fpRndRTN sym = wordLit sym 3 3 {- to -inf -}
fpRndRTZ sym = wordLit sym 3 4 {- to 0 -}

24
src/Cryptol/Eval/Monad.hs
View File

@ -9,6 +9,7 @@
{-# LANGUAGE Safe #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE OverloadedStrings #-}
module Cryptol.Eval.Monad
( -- * Evaluation monad
@ -17,6 +18,8 @@ module Cryptol.Eval.Monad
, EvalOpts(..)
, getEvalOpts
, PPOpts(..)
, PPFloatFormat(..)
, PPFloatExp(..)
, defaultPPOpts
, io
, delayFill
@ -54,10 +57,25 @@ data PPOpts = PPOpts
{ useAscii :: Bool
, useBase :: Int
, useInfLength :: Int
, useFPBase :: Int
, useFPFormat :: PPFloatFormat
}
data PPFloatFormat =
FloatFixed Int PPFloatExp -- ^ Use this many significant digis
| FloatFrac Int -- ^ Show this many digits after floating point
| FloatFree PPFloatExp -- ^ Use the correct number of digits
data PPFloatExp = ForceExponent -- ^ Always show an exponent
| AutoExponent -- ^ Only show exponent when needed
defaultPPOpts :: PPOpts
defaultPPOpts = PPOpts { useAscii = False, useBase = 10, useInfLength = 5 }
defaultPPOpts = PPOpts { useAscii = False, useBase = 10, useInfLength = 5
, useFPBase = 16
, useFPFormat = FloatFree AutoExponent
}
-- | Some options for evalutaion
data EvalOpts = EvalOpts
@ -194,6 +212,8 @@ data EvalError
| UserError String -- ^ Call to the Cryptol @error@ primitive
| LoopError String -- ^ Detectable nontermination
| NoPrim Name -- ^ Primitive with no implementation
| BadRoundingMode Integer -- ^ Invalid rounding mode
| BadValue String -- ^ Value outside the domain of a partial function.
deriving (Typeable,Show)
instance PP EvalError where
@ -208,6 +228,8 @@ instance PP EvalError where
text "word too wide for memory:" <+> integer w <+> text "bits"
UserError x -> text "Run-time error:" <+> text x
LoopError x -> text "<<loop>>" <+> text x
BadRoundingMode r -> "invalid rounding mode" <+> integer r
BadValue x -> "invalid input for" <+> backticks (text x)
NoPrim x -> text "unimplemented primitive:" <+> pp x
instance X.Exception EvalError

268
src/Cryptol/Eval/Reference.lhs
View File

@ -8,6 +8,7 @@
> -- Portability : portable
>
> {-# LANGUAGE PatternGuards #-}
> {-# LANGUAGE BlockArguments #-}
>
> module Cryptol.Eval.Reference
> ( Value(..)
@ -19,6 +20,7 @@
>
> import Control.Applicative (liftA2)
> import Data.Bits
> import Data.Ratio((%))
> import Data.List
> (genericDrop, genericIndex, genericLength, genericReplicate, genericSplitAt,
> genericTake, sortBy)
@ -26,6 +28,8 @@
> import Data.Map (Map)
> import qualified Data.Map as Map
> import qualified Data.Text as T (pack)
> import LibBF (BigFloat)
> import qualified LibBF as FP
>
> import Cryptol.ModuleSystem.Name (asPrim)
> import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul)
@ -33,7 +37,9 @@
> import Cryptol.Eval.Monad (EvalError(..), PPOpts(..))
> import Cryptol.Eval.Type (TValue(..), isTBit, evalValType, evalNumType, tvSeq)
> import Cryptol.Eval.Concrete (mkBv, ppBV, lg2)
> import Cryptol.Utils.Ident (Ident, mkIdent)
> import Cryptol.Eval.Concrete.FloatHelpers(fpPP,fpToI,BF(..),fpRound)
> import Cryptol.Eval.Concrete.Float(floatFromBits,floatToBits)
> import Cryptol.Utils.Ident (Ident,PrimIdent, prelPrim, floatPrim)
> import Cryptol.Utils.Panic (panic)
> import Cryptol.Utils.PP
>
@ -68,6 +74,7 @@ are as follows:
| `Integer` | integers | `TVInteger` |
| `Z n` | integers modulo n | `TVIntMod n` |
| `Rational` | rationals | `TVRational` |
| `Float e p` | floating point | `TVFloat` |
| `Array` | arrays | `TVArray` |
| `[n]a` | finite lists | `TVSeq n a` |
| `[inf]a` | infinite lists | `TVStream a` |
@ -123,6 +130,7 @@ terms by providing an evaluator to an appropriate `Value` type.
> = VBit (Either EvalError Bool) -- ^ @ Bit @ booleans
> | VInteger (Either EvalError Integer) -- ^ @ Integer @ or @Z n@ integers
> | VRational (Either EvalError Rational) -- ^ @ Rational @ rationals
> | VFloat (Either EvalError BF) -- ^ Floating point numbers
> | VList Nat' [Value] -- ^ @ [n]a @ finite or infinite lists
> | VTuple [Value] -- ^ @ ( .. ) @ tuples
> | VRecord [(Ident, Value)] -- ^ @ { .. } @ records
@ -177,6 +185,7 @@ cpo that represents any given schema.
> TVInteger -> VInteger (fromVInteger val)
> TVIntMod _ -> VInteger (fromVInteger val)
> TVRational -> VRational (fromVRational val)
> TVFloat _ _ -> VFloat (fromVFloat' val)
> TVArray{} -> evalPanic "copyByTValue" ["Unsupported Array type"]
> TVSeq w ety -> VList (Nat w) (map (go ety) (copyList w (fromVList val)))
> TVStream ety -> VList Inf (map (go ety) (copyStream (fromVList val)))
@ -209,6 +218,19 @@ Operations on Values
> fromVRational :: Value -> Either EvalError Rational
> fromVRational (VRational i) = i
> fromVRational _ = evalPanic "fromVRational" ["Expected a rational"]
>
> fromVFloat :: Value -> Either EvalError BigFloat
> fromVFloat = fmap bfValue . fromVFloat'
> fromVFloat' :: Value -> Either EvalError BF
> fromVFloat' v =
> case v of
> VFloat f -> f
> _ -> evalPanic "fromVFloat" [ "Expected a floating point value." ]
>
> -- | Destructor for @VList@.
> fromVList :: Value -> [Value]
@ -410,6 +432,7 @@ down to the individual bits.
> VBit b -> VBit (condBit c b (fromVBit r))
> VInteger i -> VInteger (condBit c i (fromVInteger r))
> VRational x -> VRational (condBit c x (fromVRational r))
> VFloat x -> VFloat (condBit c x (fromVFloat' r))
> VList n vs -> VList n (zipWith (condValue c) vs (fromVList r))
> VTuple vs -> VTuple (zipWith (condValue c) vs (fromVTuple r))
> VRecord fs -> VRecord [ (f, condValue c v (lookupRecord f r)) | (f, v) <- fs ]
@ -572,8 +595,14 @@ by corresponding typeclasses
* Miscellaneous: `error`, `random`, `trace`
> primTable :: Map Ident Value
> primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
> primTable :: Map PrimIdent Value
> primTable = Map.unions
> [ cryptolPrimTable
> , floatPrimTable
> ]
> cryptolPrimTable :: Map PrimIdent Value
> cryptolPrimTable = Map.fromList $ map (\(n, v) -> (prelPrim (T.pack n), v))
>
> -- Literals
> [ ("True" , VBit (Right True))
@ -581,6 +610,10 @@ by corresponding typeclasses
> , ("number" , vFinPoly $ \val ->
> VPoly $ \a ->
> literal val a)
> , ("fraction" , vFinPoly \top ->
> vFinPoly \bot ->
> vFinPoly \rnd ->
> VPoly \a -> fraction top bot rnd a)
> -- Zero
> , ("zero" , VPoly zero)
>
@ -591,13 +624,26 @@ by corresponding typeclasses
> , ("complement" , unary (logicUnary not))
>
> -- Ring
> , ("+" , binary (ringBinary (\x y -> Right (x + y)) (\x y -> Right (x + y))) )
> , ("-" , binary (ringBinary (\x y -> Right (x - y)) (\x y -> Right (x - y))) )
> , ("*" , binary (ringBinary (\x y -> Right (x * y)) (\x y -> Right (x * y))) )
> , ("negate" , unary (ringUnary (\x -> Right (- x)) (\x -> Right (- x))))
> , ("+" , binary (ringBinary
> (\x y -> Right (x + y))
> (\x y -> Right (x + y))
> (fpBin FP.bfAdd fpImplicitRound)
> ))
> , ("-" , binary (ringBinary
> (\x y -> Right (x - y))
> (\x y -> Right (x - y))
> (fpBin FP.bfSub fpImplicitRound)
> ))
> , ("*" , binary ringMul)
> , ("negate" , unary (ringUnary (\x -> Right (- x))
> (\x -> Right (- x))
> (\_ _ x -> Right (FP.bfNeg x))))
> , ("fromInteger", VPoly $ \a ->
> VFun $ \x ->
> ringNullary (fromVInteger x) (fromInteger <$> fromVInteger x) a)
> ringNullary (fromVInteger x)
> (fromInteger <$> fromVInteger x)
> (\e p -> fpFromInteger e p <$> fromVInteger x)
> a)
>
> -- Integral
> , ("toInteger" , VPoly $ \a ->
@ -612,15 +658,28 @@ by corresponding typeclasses
> ringExp aty a (cryToInteger ety e))
>
> -- Field
> , ("/." , binary (fieldBinary ratDiv))
> , ("recip" , unary (fieldUnary ratRecip))
> , ("/." , binary (fieldBinary ratDiv
> (fpBin FP.bfDiv fpImplicitRound)
> ))
> , ("recip" , unary (fieldUnary ratRecip fpRecip))
>
> -- Round
> , ("floor" , unary (roundUnary floor))
> , ("ceiling" , unary (roundUnary ceiling))
> , ("trunc" , unary (roundUnary truncate))
> , ("roundAway" , unary (roundUnary roundAwayRat))
> , ("roundToEven", unary (roundUnary round))
> , ("floor" , unary (roundUnary floor
> (fpToInteger "floor" FP.ToNegInf)
> ))
> , ("ceiling" , unary (roundUnary ceiling
> (fpToInteger "ceiling" FP.ToPosInf)
> ))
> , ("trunc" , unary (roundUnary truncate
> (fpToInteger "trunc" FP.ToZero)
> ))
> , ("roundAway", unary (roundUnary roundAwayRat
> (fpToInteger "roundAway" FP.Away)
> ))
> , ("roundToEven", unary (roundUnary round
> (fpToInteger "roundToEven" FP.NearEven)
> ))
>
> -- Comparison
> , ("<" , binary (cmpOrder (\o -> o == LT)))
@ -759,6 +818,8 @@ by corresponding typeclasses
> VFun $ \_x ->
> VFun $ \y -> y)
> ]
>
>
> unary :: (TValue -> Value -> Value) -> Value
> unary f = VPoly $ \ty -> VFun $ \x -> f ty x
@ -824,6 +885,7 @@ where the given error is "pushed down" into the leaf types.
> cryError e TVInteger = VInteger (Left e)
> cryError e TVIntMod{} = VInteger (Left e)
> cryError e TVRational = VRational (Left e)
> cryError e TVFloat{} = VFloat (Left e)
> cryError _ TVArray{} = evalPanic "error" ["Array type not supported in `error`"]
> cryError e (TVSeq n ety) = VList (Nat n) (genericReplicate n (cryError e ety))
> cryError e (TVStream ety) = VList Inf (repeat (cryError e ety))
@ -849,6 +911,7 @@ For functions, `zero` returns the constant function that returns
> zero TVInteger = VInteger (Right 0)
> zero TVIntMod{} = VInteger (Right 0)
> zero TVRational = VRational (Right 0)
> zero (TVFloat e p) = VFloat (Right (fpToBF e p FP.bfPosZero))
> zero TVArray{} = evalPanic "zero" ["Array type not in `Zero`"]
> zero (TVSeq n ety) = VList (Nat n) (genericReplicate n (zero ety))
> zero (TVStream ety) = VList Inf (repeat (zero ety))
@ -876,6 +939,22 @@ Given a literal integer, construct a value of a type that can represent that lit
> go ty = evalPanic "literal" [show ty ++ " cannot represent literals"]
Given a fraction, construct a value of a type that can represent that literal.
The rounding flag determines the behavior if the literal cannot be represented
exactly: 0 means report and error, other numbers round to the nearest
representable value.
> fraction :: Integer -> Integer -> Integer -> TValue -> Value
> fraction top btm _rnd ty =
> case ty of
> TVRational -> VRational (Right (top % btm))
> TVFloat e p -> VFloat $ Right $ fpToBF e p $ fpCheckStatus val
> where val = FP.bfDiv opts (FP.bfFromInteger top) (FP.bfFromInteger btm)
> opts = fpOpts e p fpImplicitRound
> _ -> evalPanic "fraction" [show ty ++ " cannot represent " ++
> show top ++ "/" ++ show btm]
Logic
-----
@ -902,6 +981,7 @@ at the same positions.
> TVIntMod _ -> evalPanic "logicUnary" ["Z not in class Logic"]
> TVArray{} -> evalPanic "logicUnary" ["Array not in class Logic"]
> TVRational -> evalPanic "logicUnary" ["Rational not in class Logic"]
> TVFloat{} -> evalPanic "logicUnary" ["Float not in class Logic"]
> TVAbstract{} -> evalPanic "logicUnary" ["Abstract type not in `Logic`"]
> logicBinary :: (Bool -> Bool -> Bool) -> TValue -> Value -> Value -> Value
@ -921,6 +1001,7 @@ at the same positions.
> TVIntMod _ -> evalPanic "logicBinary" ["Z not in class Logic"]
> TVArray{} -> evalPanic "logicBinary" ["Array not in class Logic"]
> TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]
> TVFloat{} -> evalPanic "logicBinary" ["Float not in class Logic"]
> TVAbstract{} -> evalPanic "logicBinary" ["Abstract type not in `Logic`"]
@ -937,8 +1018,9 @@ False]`, but to `[error "foo", error "foo"]`.
> ringNullary ::
> Either EvalError Integer ->
> Either EvalError Rational ->
> (Integer -> Integer -> Either EvalError BigFloat) ->
> TValue -> Value
> ringNullary i q = go
> ringNullary i q fl = go
> where
> go :: TValue -> Value
> go ty =
@ -951,6 +1033,8 @@ False]`, but to `[error "foo", error "foo"]`.
> VInteger (flip mod n <$> i)
> TVRational ->
> VRational q
> TVFloat e p ->
> VFloat (fpToBF e p <$> fl e p)
> TVArray{} ->
> evalPanic "arithNullary" ["Array not in class Ring"]
> TVSeq w a
@ -970,8 +1054,9 @@ False]`, but to `[error "foo", error "foo"]`.
> ringUnary ::
> (Integer -> Either EvalError Integer) ->
> (Rational -> Either EvalError Rational) ->
> (Integer -> Integer -> BigFloat -> Either EvalError BigFloat) ->
> TValue -> Value -> Value
> ringUnary iop qop = go
> ringUnary iop qop flop = go
> where
> go :: TValue -> Value -> Value
> go ty val =
@ -986,6 +1071,8 @@ False]`, but to `[error "foo", error "foo"]`.
> VInteger $ appOp1 (\i -> flip mod n <$> iop i) (fromVInteger val)
> TVRational ->
> VRational $ appOp1 qop (fromVRational val)
> TVFloat e p ->
> VFloat (fpToBF e p <$> appOp1 (flop e p) (fromVFloat val))
> TVSeq w a
> | isTBit a -> vWord w (iop =<< fromVWord val)
> | otherwise -> VList (Nat w) (map (go a) (fromVList val))
@ -1003,8 +1090,9 @@ False]`, but to `[error "foo", error "foo"]`.
> ringBinary ::
> (Integer -> Integer -> Either EvalError Integer) ->
> (Rational -> Rational -> Either EvalError Rational) ->
> (Integer -> Integer -> BigFloat -> BigFloat -> Either EvalError BigFloat) ->
> TValue -> Value -> Value -> Value
> ringBinary iop qop = go
> ringBinary iop qop flop = go
> where
> go :: TValue -> Value -> Value -> Value
> go ty l r =
@ -1017,6 +1105,8 @@ False]`, but to `[error "foo", error "foo"]`.
> VInteger $ appOp2 (\i j -> flip mod n <$> iop i j) (fromVInteger l) (fromVInteger r)
> TVRational ->
> VRational $ appOp2 qop (fromVRational l) (fromVRational r)
> TVFloat e p ->
> VFloat $ fpToBF e p <$> appOp2 (flop e p) (fromVFloat l) (fromVFloat r)
> TVArray{} ->
> evalPanic "arithBinary" ["Array not in class Ring"]
> TVSeq w a
@ -1056,9 +1146,12 @@ Integral
>
> ringExp :: TValue -> Value -> Either EvalError Integer -> Value
> ringExp a _ (Left e) = cryError e a
> ringExp a v (Right i) = foldl mul (literal 1 a) (genericReplicate i v)
> where
> mul = ringBinary (\x y -> Right (x * y)) (\x y -> Right (x * y)) a
> ringExp a v (Right i) = foldl (ringMul a) (literal 1 a) (genericReplicate i v)
>
> ringMul :: TValue -> Value -> Value -> Value
> ringMul = ringBinary (\x y -> Right (x * y))
> (\x y -> Right (x * y))
> (fpBin FP.bfMul fpImplicitRound)
Signed bitvector division (`/$`) and remainder (`%$`) are defined so
@ -1085,16 +1178,22 @@ Types that represent fields are have, in addition to the ring operations
a recipricol operator and a field division operator (not to be
confused with integral division).
> fieldUnary :: (Rational -> Either EvalError Rational) -> TValue -> Value -> Value
> fieldUnary qop ty v = case ty of
> TVRational -> VRational $ appOp1 qop (fromVRational v)
> fieldUnary :: (Rational -> Either EvalError Rational) ->
> (Integer -> Integer -> BigFloat -> Either EvalError BigFloat) ->
> TValue -> Value -> Value
> fieldUnary qop flop ty v = case ty of
> TVRational -> VRational $ appOp1 qop (fromVRational v)
> TVFloat e p -> VFloat $ fpToBF e p <$> appOp1 (flop e p) (fromVFloat v)
> _ -> evalPanic "fieldUnary" [show ty ++ " is not a Field type"]
>
> fieldBinary ::
> (Rational -> Rational -> Either EvalError Rational) ->
> (Integer -> Integer -> BigFloat -> BigFloat -> Either EvalError BigFloat) ->
> TValue -> Value -> Value -> Value
> fieldBinary qop ty l r = case ty of
> fieldBinary qop flop ty l r = case ty of
> TVRational -> VRational $ appOp2 qop (fromVRational l) (fromVRational r)
> TVFloat e p -> VFloat $ fpToBF e p <$> appOp2 (flop e p)
> (fromVFloat l) (fromVFloat r)
> _ -> evalPanic "fieldBinary" [show ty ++ " is not a Field type"]
>
> ratDiv :: Rational -> Rational -> Either EvalError Rational
@ -1109,9 +1208,12 @@ confused with integral division).
Round
-----
> roundUnary :: (Rational -> Integer) -> TValue -> Value -> Value
> roundUnary op ty v = case ty of
> roundUnary :: (Rational -> Integer) ->
> (Integer -> Integer -> BigFloat -> Either EvalError Integer) ->
> TValue -> Value -> Value
> roundUnary op flop ty v = case ty of
> TVRational -> VInteger (op <$> fromVRational v)
> TVFloat e p -> VInteger (flop e p =<< fromVFloat v)
> _ -> evalPanic "roundUnary" [show ty ++ " is not a Round type"]
>
@ -1162,6 +1264,8 @@ bits to the *left* of that position are equal.
> compare <$> fromVInteger l <*> fromVInteger r
> TVRational ->
> compare <$> fromVRational l <*> fromVRational r
> TVFloat{} ->
> compare <$> fromVFloat l <*> fromVFloat r
> TVArray{} ->
> evalPanic "lexCompare" ["invalid type"]
> TVSeq _w ety ->
@ -1209,6 +1313,8 @@ fields are compared in alphabetical order.
> evalPanic "lexSignedCompare" ["invalid type"]
> TVRational ->
> evalPanic "lexSignedCompare" ["invalid type"]
> TVFloat{} ->
> evalPanic "lexSignedCompare" ["invalid type"]
> TVArray{} ->
> evalPanic "lexSignedCompare" ["invalid type"]
> TVSeq _w ety
@ -1389,6 +1495,113 @@ length of the list produces a run-time error.
> updateAt (x : xs) i y = x : updateAt xs (i - 1) y
Floating Point Numbers
----------------------
Whenever we do operations that do not have an explicit rounding mode,
we round towards the closest number, with ties resolved to the even one.
> fpImplicitRound :: FP.RoundMode
> fpImplicitRound = FP.NearEven
The function `fpOpts` deifnes an object specifying the precision and rounding
mode to be used during a floating point computation. We assume that its
aruments are known to be within the limits imposed by the concrete
library used to perform the computation.
> fpOpts :: Integer -> Integer -> FP.RoundMode -> FP.BFOpts
> fpOpts e p r = FP.expBits (fromInteger e) <>
> FP.precBits (fromInteger p) <>
> FP.rnd r
Most floating point computations produce a result and some additional
information about what happened while computing. The function
`fpCheckStatus` examines this status and reports erorrs in unusual situations.
> fpCheckStatus :: (FP.BigFloat, FP.Status) -> FP.BigFloat
> fpCheckStatus (r,s) =
> case s of
> FP.MemError -> panic "fpCheckStatus" [ "Out of memory" ]
> _ -> r
We annotate floating point values with their precision. This is only used
when pretty printing values.
> fpToBF :: Integer -> Integer -> BigFloat -> BF
> fpToBF e p x = BF { bfValue = x, bfExpWidth = e, bfPrecWidth = p }
The following two functions convert between floaitng point numbers
and integers.
> fpFromInteger :: Integer -> Integer -> Integer -> BigFloat
> fpFromInteger e p = fpCheckStatus . FP.bfRoundFloat opts . FP.bfFromInteger
> where opts = fpOpts e p fpImplicitRound
> fpToInteger ::
> String -> FP.RoundMode ->
> Integer -> Integer ->
> BigFloat -> Either EvalError Integer
> fpToInteger fun r _ _ f =
> case fpToI r f of
> Nothing -> Left (BadValue fun)
> Just i -> Right i
This just captures a common pattern for binary floating point primitives.
> fpBin :: (FP.BFOpts -> BigFloat -> BigFloat -> (BigFloat,FP.Status)) ->
> FP.RoundMode -> Integer -> Integer ->
> BigFloat -> BigFloat -> Either EvalError BigFloat
> fpBin f r e p x y = Right (fpCheckStatus (f (fpOpts e p r) x y))
Computes the reciprocal of a floating point number via division.
This assumes that 1 can be represented exactly, which should be
true for all supported precisions.
> fpRecip :: Integer -> Integer -> BigFloat -> Either EvalError BigFloat
> fpRecip e p x = Right (fpCheckStatus (FP.bfDiv opts (FP.bfFromInteger 1) x))
> where opts = fpOpts e p fpImplicitRound
> floatPrimTable :: Map PrimIdent Value
> floatPrimTable = Map.fromList $ map (\(n, v) -> (floatPrim (T.pack n), v))
> [ "fpNaN" ~> vFinPoly \e -> vFinPoly \p ->
> VFloat $ Right $ fpToBF e p FP.bfNaN
>
> , "fpPosInf" ~> vFinPoly \e -> vFinPoly \p ->
> VFloat $ Right $ fpToBF e p FP.bfPosInf
>
> , "fpFromBits" ~> vFinPoly \e -> vFinPoly \p -> VFun \bvv ->
> VFloat (floatFromBits e p <$> fromVWord bvv)
>
> , "fpToBits" ~> vFinPoly \e -> vFinPoly \p -> VFun \fpv ->
> vWord (e + p) (floatToBits e p <$> fromVFloat fpv)
>
> , "=.=" ~> vFinPoly \_ -> vFinPoly \_ -> VFun \xv -> VFun \yv ->
> VBit do x <- fromVFloat xv
> y <- fromVFloat yv
> pure (FP.bfCompare x y == EQ)
>
> , "fpAdd" ~> fpArith FP.bfAdd
> , "fpSub" ~> fpArith FP.bfSub
> , "fpMul" ~> fpArith FP.bfMul
> , "fpDiv" ~> fpArith FP.bfDiv
> ]
> where
> (~>) = (,)
> fpArith f = vFinPoly \e -> vFinPoly \p ->
> VFun \vr -> VFun \xv -> VFun \yv ->
> VFloat do r <- fromVWord vr
> rnd <- case fpRound r of
> Just r' -> pure r'
> Nothing -> Left (BadRoundingMode r)
> x <- fromVFloat xv
> y <- fromVFloat yv
> fpToBF e p <$> fpBin f rnd e p x y
Error Handling
--------------
@ -1409,6 +1622,7 @@ Pretty Printing
> VBit b -> text (either show show b)
> VInteger i -> text (either show show i)
> VRational q -> text (either show show q)
> VFloat fl -> text (either show (show . fpPP opts) fl)
> VList l vs ->
> case l of
> Inf -> ppList (map (ppValue opts) (take (useInfLength opts) vs) ++ [text "..."])

27
src/Cryptol/Eval/SBV.hs
View File

@ -141,7 +141,7 @@ instance Backend SBV where
type SBit SBV = SVal
type SWord SBV = SVal
type SInteger SBV = SVal
type SFloat SBV = () -- XXX: not implemented
type SEval SBV = SBVEval
raiseError _ err = SBVEval (pure (SBVError err))
@ -312,6 +312,23 @@ instance Backend SBV where
znMult _ m a b = sModMult m a b
znNegate _ m a = sModNegate m a
ppFloat _ _ _ = text "[?]"
fpLit _ _ _ _ = unsupported "fpLit"
fpEq _ _ _ = unsupported "fpEq"
fpLessThan _ _ _ = unsupported "fpLessThan"
fpGreaterThan _ _ _ = unsupported "fpGreaterThan"
fpPlus _ _ _ _ = unsupported "fpPlus"
fpMinus _ _ _ _ = unsupported "fpMinus"
fpMult _ _ _ _ = unsupported "fpMult"
fpDiv _ _ _ _ = unsupported "fpDiv"
fpNeg _ _ = unsupported "fpNeg"
fpFromInteger _ _ _ _ _ = unsupported "fpFromInteger"
fpToInteger _ _ _ _ = unsupported "fpToInteger"
unsupported :: String -> SEval SBV a
unsupported x = liftIO (X.throw (UnsupportedSymbolicOp x))
svToInteger :: SWord SBV -> SInteger SBV
svToInteger w =
case svAsInteger w of
@ -333,18 +350,20 @@ evalPanic cxt = panic ("[Symbolic]" ++ cxt)
-- Primitives ------------------------------------------------------------------
evalPrim :: Ident -> Maybe Value
evalPrim :: PrimIdent -> Maybe Value
evalPrim prim = Map.lookup prim primTable
-- See also Cryptol.Eval.Concrete.primTable
primTable :: Map.Map Ident Value
primTable :: Map.Map PrimIdent Value
primTable = let sym = SBV in
Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
Map.fromList $ map (\(n, v) -> (prelPrim (T.pack n), v))
[ -- Literals
("True" , VBit (bitLit sym True))
, ("False" , VBit (bitLit sym False))
, ("number" , ecNumberV sym) -- Converts a numeric type into its corresponding value.
-- { val, rep } (Literal val rep) => rep
, ("fraction" , ecFractionV sym)
, ("ratio" , ratioV sym)
-- Zero

7
src/Cryptol/Eval/Type.hs
View File

@ -29,6 +29,7 @@ import Control.DeepSeq
data TValue
= TVBit -- ^ @ Bit @
| TVInteger -- ^ @ Integer @
| TVFloat Integer Integer -- ^ @ Float e p @
| TVIntMod Integer -- ^ @ Z n @
| TVRational -- ^ @Rational@
| TVArray TValue TValue -- ^ @ Array a b @
@ -46,6 +47,7 @@ tValTy tv =
case tv of
TVBit -> tBit
TVInteger -> tInteger
TVFloat e p -> tFloat (tNum e) (tNum p)
TVIntMod n -> tIntMod (tNum n)
TVRational -> tRational
TVArray a b -> tArray (tValTy a) (tValTy b)
@ -107,6 +109,7 @@ evalType env ty =
(TCBit, []) -> Right $ TVBit
(TCInteger, []) -> Right $ TVInteger
(TCRational, []) -> Right $ TVRational
(TCFloat, [e,p])-> Right $ TVFloat (inum e) (inum p)
(TCIntMod, [n]) -> case num n of
Inf -> evalPanic "evalType" ["invalid type Z inf"]
Nat m -> Right $ TVIntMod m
@ -134,6 +137,10 @@ evalType env ty =
where
val = evalValType env
num = evalNumType env
inum x = case num x of
Nat i -> i
Inf -> evalPanic "evalType"
["Expecting a finite size, but got `inf`"]
-- | Evaluation for value types (kind *).
evalValType :: HasCallStack => TypeEnv -> Type -> TValue

27
src/Cryptol/Eval/Value.hs
View File

@ -34,8 +34,10 @@ module Cryptol.Eval.Value
, word
, lam
, wlam
, flam
, tlam
, nlam
, ilam
, toStream
, toFinSeq
, toSeq
@ -44,6 +46,7 @@ module Cryptol.Eval.Value
, fromVBit
, fromVInteger
, fromVRational
, fromVFloat
, fromVSeq
, fromSeq
, fromWordVal
@ -102,6 +105,7 @@ import Cryptol.Eval.Type
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
import Cryptol.Utils.Ident (Ident)
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.PP
import Data.List(genericIndex)
@ -298,6 +302,7 @@ data GenValue sym
| VBit !(SBit sym) -- ^ @ Bit @
| VInteger !(SInteger sym) -- ^ @ Integer @ or @ Z n @
| VRational !(SRational sym) -- ^ @ Rational @
| VFloat !(SFloat sym)
| VSeq !Integer !(SeqMap sym) -- ^ @ [n]a @
-- Invariant: VSeq is never a sequence of bits
| VWord !Integer !(SEval sym (WordValue sym)) -- ^ @ [n]Bit @
@ -322,6 +327,7 @@ forceValue v = case v of
VBit b -> seq b (return ())
VInteger i -> seq i (return ())
VRational q -> seq q (return ())
VFloat f -> seq f (return ())
VWord _ wv -> forceWordValue =<< wv
VStream _ -> return ()
VFun _ -> return ()
@ -336,6 +342,7 @@ instance Backend sym => Show (GenValue sym) where
VBit _ -> "bit"
VInteger _ -> "integer"
VRational _ -> "rational"
VFloat _ -> "float"
VSeq n _ -> "seq:" ++ show n
VWord n _ -> "word:" ++ show n
VStream _ -> "stream"
@ -365,6 +372,7 @@ ppValue x opts = loop
VBit b -> return $ ppBit x b
VInteger i -> return $ ppInteger x opts i
VRational q -> return $ ppRational x opts q
VFloat i -> return $ ppFloat x opts i
VSeq sz vals -> ppWordSeq sz vals
VWord _ wv -> ppWordVal =<< wv
VStream vals -> do vals' <- traverse (>>=loop) $ enumerateSeqMap (useInfLength opts) vals
@ -413,6 +421,13 @@ lam = VFun
wlam :: Backend sym => sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam sym f = VFun (\arg -> arg >>= fromVWord sym "wlam" >>= f)
-- | Functions that assume floating point inputs
flam :: Backend sym =>
(SFloat sym -> SEval sym (GenValue sym)) -> GenValue sym
flam f = VFun (\arg -> arg >>= f . fromVFloat)
-- | A type lambda that expects a 'Type'.
tlam :: Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam f = VPoly (return . f)
@ -421,6 +436,12 @@ tlam f = VPoly (return . f)
nlam :: Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam f = VNumPoly (return . f)
-- | A type lambda that expects a funite numeric type.
ilam :: Backend sym => (Integer -> GenValue sym) -> GenValue sym
ilam f = nlam (\n -> case n of
Nat i -> f i
Inf -> panic "ilam" [ "Unexpected `inf`" ])
-- | Generate a stream.
toStream :: Backend sym => [GenValue sym] -> SEval sym (GenValue sym)
toStream vs =
@ -546,6 +567,12 @@ fromVRecord val = case val of
VRecord fs -> fs
_ -> evalPanic "fromVRecord" ["not a record"]
fromVFloat :: GenValue sym -> SFloat sym
fromVFloat val =
case val of
VFloat x -> x
_ -> evalPanic "fromVFloat" ["not a Float"]
-- | Lookup a field in a record.
lookupRecord :: Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord f val =

747
src/Cryptol/Eval/What4.hs
View File

@ -4,17 +4,8 @@
-- License : BSD3
-- Maintainer : cryptol@galois.com
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE OverloadedStrings #-}
module Cryptol.Eval.What4
( What4(..)
, W4Result(..)
@ -24,383 +15,36 @@ module Cryptol.Eval.What4
) where
import qualified Control.Exception as X
import Control.Monad (foldM, join)
import Control.Monad.IO.Class
import Data.Bits (bit, shiftR, shiftL, testBit)
import qualified Data.BitVector.Sized as BV
import Data.List
import Control.Monad (join)
import qualified Data.Map as Map
import Data.Parameterized.NatRepr
import Data.Parameterized.Some
import qualified Data.Text as T
import qualified What4.Interface as W4
import qualified What4.SWord as SW
import qualified What4.Utils.AbstractDomains as W4
import Cryptol.Eval.Backend
import Cryptol.Eval.Concrete.Value( BV(..), ppBV )
import Cryptol.Eval.Generic
import Cryptol.Eval.Monad (Eval(..), EvalError(..), Unsupported(..), io, delayFill, blackhole)
import Cryptol.Eval.Type (TValue(..), finNat')
import Cryptol.Eval.Type (finNat')
import Cryptol.Eval.Value
import Cryptol.Eval.What4.Value
import Cryptol.Eval.What4.Float(floatPrims)
import Cryptol.Testing.Random( randomV )
import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), widthInteger)
import Cryptol.Utils.Ident
import Cryptol.Utils.Panic
import Cryptol.Utils.PP
data What4 sym = What4 sym
type Value sym = GenValue (What4 sym)
data W4Result sym a
= W4Error !EvalError
| W4Result !(W4.Pred sym) !a -- safety predicate and result
instance Functor (W4Result sym) where
fmap _ (W4Error err) = W4Error err
fmap f (W4Result p x) = W4Result p (f x)
total :: W4.IsExprBuilder sym => sym -> a -> W4Result sym a
total sym = W4Result (W4.backendPred sym True)
-- TODO? Reorganize this to use PartialT ?
newtype W4Eval sym a = W4Eval{ w4Eval :: sym -> Eval (W4Result sym a) }
deriving (Functor)
instance W4.IsExprBuilder sym => Applicative (W4Eval sym) where
pure x = W4Eval $ \sym -> pure (total sym x)
mf <*> mx = mf >>= \f -> mx >>= \x -> pure (f x)
instance W4.IsExprBuilder sym => Monad (W4Eval sym) where
return = pure
x >>= f = W4Eval $ \sym ->
w4Eval x sym >>= \case
W4Error err -> pure (W4Error err)
W4Result px x' ->
w4Eval (f x') sym >>= \case
W4Error err -> pure (W4Error err)
W4Result pz z ->
do p <- io (W4.andPred sym px pz)
pure (W4Result p z)
instance W4.IsExprBuilder sym => MonadIO (W4Eval sym) where
liftIO m = W4Eval $ \sym -> fmap (total sym) (liftIO m)
assertBVDivisor :: W4.IsExprBuilder sym => sym -> SW.SWord sym -> W4Eval sym ()
assertBVDivisor sym x =
do p <- liftIO (SW.bvIsNonzero sym x)
assertSideCondition (What4 sym) p DivideByZero
assertIntDivisor :: W4.IsExprBuilder sym => sym -> W4.SymInteger sym -> W4Eval sym ()
assertIntDivisor sym x =
do p <- liftIO (W4.notPred sym =<< W4.intEq sym x =<< W4.intLit sym 0)
assertSideCondition (What4 sym) p DivideByZero
instance W4.IsExprBuilder sym => Backend (What4 sym) where
type SBit (What4 sym) = W4.Pred sym
type SWord (What4 sym) = SW.SWord sym
type SInteger (What4 sym) = W4.SymInteger sym
type SEval (What4 sym) = W4Eval sym
raiseError _ err = W4Eval (\_ -> pure (W4Error err))
assertSideCondition _ cond err
| Just False <- W4.asConstantPred cond = W4Eval (\_ -> pure (W4Error err))
| otherwise = W4Eval (\_ -> pure (W4Result cond ()))
isReady (What4 sym) m =
case w4Eval m sym of
Ready _ -> True
_ -> False
sDelayFill _ m retry = W4Eval $ \sym ->
do m' <- delayFill (w4Eval m sym) (w4Eval retry sym)
pure (total sym (W4Eval (const m')))
sDeclareHole _ msg = W4Eval $ \sym ->
do (hole, fill) <- blackhole msg
pure (total sym ( W4Eval (const hole), \m -> W4Eval (\sym' -> fmap (total sym') (fill (w4Eval m sym'))) ))
mergeEval _sym f c mx my = W4Eval $ \sym ->
do rx <- w4Eval mx sym
ry <- w4Eval my sym
case (rx, ry) of
(W4Error err, W4Error _) ->
pure $ W4Error err -- arbitrarily choose left error to report
(W4Error _, W4Result p y) ->
do p' <- io (W4.andPred sym p =<< W4.notPred sym c)
pure $ W4Result p' y
(W4Result p x, W4Error _) ->
do p' <- io (W4.andPred sym p c)
pure $ W4Result p' x
(W4Result px x, W4Result py y) ->
do zr <- w4Eval (f c x y) sym
case zr of
W4Error err -> pure $ W4Error err
W4Result pz z ->
do p' <- io (W4.andPred sym pz =<< W4.itePred sym c px py)
pure $ W4Result p' z
wordAsChar _ bv
| SW.bvWidth bv == 8 = toEnum . fromInteger <$> SW.bvAsUnsignedInteger bv
| otherwise = Nothing
wordLen _ bv = SW.bvWidth bv
bitLit (What4 sym) b = W4.backendPred sym b
bitAsLit _ v = W4.asConstantPred v
wordLit (What4 sym) intw i
| Just (Some w) <- someNat intw
= case isPosNat w of
Nothing -> pure $ SW.ZBV
Just LeqProof -> SW.DBV <$> liftIO (W4.bvLit sym w (BV.mkBV w i))
| otherwise = panic "what4: wordLit" ["invalid bit width:", show intw ]
wordAsLit _ v
| Just x <- SW.bvAsUnsignedInteger v = Just (SW.bvWidth v, x)
| otherwise = Nothing
integerLit (What4 sym) i = liftIO (W4.intLit sym i)
integerAsLit _ v = W4.asInteger v
ppBit _ v
| Just b <- W4.asConstantPred v = text $! if b then "True" else "False"
| otherwise = text "?"
ppWord _ opts v
| Just x <- SW.bvAsUnsignedInteger v
= ppBV opts (BV (SW.bvWidth v) x)
| otherwise = text "[?]"
ppInteger _ _opts v
| Just x <- W4.asInteger v = integer x
| otherwise = text "[?]"
iteBit (What4 sym) c x y = liftIO (W4.itePred sym c x y)
iteWord (What4 sym) c x y = liftIO (SW.bvIte sym c x y)
iteInteger (What4 sym) c x y = liftIO (W4.intIte sym c x y)
bitEq (What4 sym) x y = liftIO (W4.eqPred sym x y)
bitAnd (What4 sym) x y = liftIO (W4.andPred sym x y)
bitOr (What4 sym) x y = liftIO (W4.orPred sym x y)
bitXor (What4 sym) x y = liftIO (W4.xorPred sym x y)
bitComplement (What4 sym) x = liftIO (W4.notPred sym x)
wordBit (What4 sym) bv idx = liftIO (SW.bvAtBE sym bv idx)
wordUpdate (What4 sym) bv idx b = liftIO (SW.bvSetBE sym bv idx b)
packWord sym bs =
do z <- wordLit sym (genericLength bs) 0
let f w (idx,b) = wordUpdate sym w idx b
foldM f z (zip [0..] bs)
unpackWord (What4 sym) bv = liftIO $
mapM (SW.bvAtBE sym bv) [0 .. SW.bvWidth bv-1]
joinWord (What4 sym) x y = liftIO $ SW.bvJoin sym x y
splitWord _sym 0 _ bv = pure (SW.ZBV, bv)
splitWord _sym _ 0 bv = pure (bv, SW.ZBV)
splitWord (What4 sym) lw rw bv = liftIO $
do l <- SW.bvSliceBE sym 0 lw bv
r <- SW.bvSliceBE sym lw rw bv
return (l, r)
extractWord (What4 sym) bits idx bv =
liftIO $ SW.bvSliceBE sym idx bits bv
wordEq (What4 sym) x y = liftIO (SW.bvEq sym x y)
wordLessThan (What4 sym) x y = liftIO (SW.bvult sym x y)
wordGreaterThan (What4 sym) x y = liftIO (SW.bvugt sym x y)
wordSignedLessThan (What4 sym) x y = liftIO (SW.bvslt sym x y)
wordOr (What4 sym) x y = liftIO (SW.bvOr sym x y)
wordAnd (What4 sym) x y = liftIO (SW.bvAnd sym x y)
wordXor (What4 sym) x y = liftIO (SW.bvXor sym x y)
wordComplement (What4 sym) x = liftIO (SW.bvNot sym x)
wordPlus (What4 sym) x y = liftIO (SW.bvAdd sym x y)
wordMinus (What4 sym) x y = liftIO (SW.bvSub sym x y)
wordMult (What4 sym) x y = liftIO (SW.bvMul sym x y)
wordNegate (What4 sym) x = liftIO (SW.bvNeg sym x)
wordLg2 (What4 sym) x = sLg2 sym x
wordDiv (What4 sym) x y =
do assertBVDivisor sym y
liftIO (SW.bvUDiv sym x y)
wordMod (What4 sym) x y =
do assertBVDivisor sym y
liftIO (SW.bvURem sym x y)
wordSignedDiv (What4 sym) x y =
do assertBVDivisor sym y
liftIO (SW.bvSDiv sym x y)
wordSignedMod (What4 sym) x y =
do assertBVDivisor sym y
liftIO (SW.bvSRem sym x y)
wordToInt (What4 sym) x = liftIO (SW.bvToInteger sym x)
wordFromInt (What4 sym) width i = liftIO (SW.integerToBV sym i width)
intPlus (What4 sym) x y = liftIO $ W4.intAdd sym x y
intMinus (What4 sym) x y = liftIO $ W4.intSub sym x y
intMult (What4 sym) x y = liftIO $ W4.intMul sym x y
intNegate (What4 sym) x = liftIO $ W4.intNeg sym x
-- NB: What4's division operation provides SMTLib's euclidean division,
-- which doesn't match the round-to-neg-infinity semantics of Cryptol,
-- so we have to do some work to get the desired semantics.
intDiv (What4 sym) x y =
do assertIntDivisor sym y
liftIO $ do
neg <- liftIO (W4.intLt sym y =<< W4.intLit sym 0)
case W4.asConstantPred neg of
Just False -> W4.intDiv sym x y
Just True ->
do xneg <- W4.intNeg sym x
yneg <- W4.intNeg sym y
W4.intDiv sym xneg yneg
Nothing ->
do xneg <- W4.intNeg sym x
yneg <- W4.intNeg sym y
zneg <- W4.intDiv sym xneg yneg
z <- W4.intDiv sym x y
W4.intIte sym neg zneg z
-- NB: What4's division operation provides SMTLib's euclidean division,
-- which doesn't match the round-to-neg-infinity semantics of Cryptol,
-- so we have to do some work to get the desired semantics.
intMod (What4 sym) x y =
do assertIntDivisor sym y
liftIO $ do
neg <- liftIO (W4.intLt sym y =<< W4.intLit sym 0)
case W4.asConstantPred neg of
Just False -> W4.intMod sym x y
Just True ->
do xneg <- W4.intNeg sym x
yneg <- W4.intNeg sym y
W4.intNeg sym =<< W4.intMod sym xneg yneg
Nothing ->
do xneg <- W4.intNeg sym x
yneg <- W4.intNeg sym y
z <- W4.intMod sym x y
zneg <- W4.intNeg sym =<< W4.intMod sym xneg yneg
W4.intIte sym neg zneg z
intEq (What4 sym) x y = liftIO $ W4.intEq sym x y
intLessThan (What4 sym) x y = liftIO $ W4.intLt sym x y
intGreaterThan (What4 sym) x y = liftIO $ W4.intLt sym y x
-- NB, we don't do reduction here on symbolic values
intToZn (What4 sym) m x
| Just xi <- W4.asInteger x
= liftIO $ W4.intLit sym (xi `mod` m)
| otherwise
= pure x
znToInt _ 0 _ = evalPanic "znToInt" ["0 modulus not allowed"]
znToInt (What4 sym) m x = liftIO (W4.intMod sym x =<< W4.intLit sym m)
znEq _ 0 _ _ = evalPanic "znEq" ["0 modulus not allowed"]
znEq (What4 sym) m x y = liftIO $
do diff <- W4.intSub sym x y
W4.intDivisible sym diff (fromInteger m)
znPlus (What4 sym) m x y = liftIO $ sModAdd sym m x y
znMinus (What4 sym) m x y = liftIO $ sModSub sym m x y
znMult (What4 sym) m x y = liftIO $ sModMult sym m x y
znNegate (What4 sym) m x = liftIO $ sModNegate sym m x
sModAdd :: W4.IsExprBuilder sym =>
sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModAdd _sym 0 _ _ = evalPanic "sModAdd" ["0 modulus not allowed"]
sModAdd sym m x y
| Just xi <- W4.asInteger x
, Just yi <- W4.asInteger y
= W4.intLit sym ((xi+yi) `mod` m)
| otherwise
= W4.intAdd sym x y
sModSub :: W4.IsExprBuilder sym =>
sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModSub _sym 0 _ _ = evalPanic "sModSub" ["0 modulus not allowed"]
sModSub sym m x y
| Just xi <- W4.asInteger x
, Just yi <- W4.asInteger y
= W4.intLit sym ((xi-yi) `mod` m)
| otherwise
= W4.intSub sym x y
sModMult :: W4.IsExprBuilder sym =>
sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModMult _sym 0 _ _ = evalPanic "sModMult" ["0 modulus not allowed"]
sModMult sym m x y
| Just xi <- W4.asInteger x
, Just yi <- W4.asInteger y
= W4.intLit sym ((xi*yi) `mod` m)
| otherwise
= W4.intMul sym x y
sModNegate :: W4.IsExprBuilder sym =>
sym -> Integer -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModNegate _sym 0 _ = evalPanic "sModMult" ["0 modulus not allowed"]
sModNegate sym m x
| Just xi <- W4.asInteger x
= W4.intLit sym ((negate xi) `mod` m)
| otherwise
= W4.intNeg sym x
-- | Try successive powers of 2 to find the first that dominates the input.
-- We could perhaps reduce to using CLZ instead...
sLg2 :: W4.IsExprBuilder sym => sym -> SW.SWord sym -> SEval (What4 sym) (SW.SWord sym)
sLg2 sym x = liftIO $ go 0
where
w = SW.bvWidth x
lit n = SW.bvLit sym w (toInteger n)
go i | toInteger i < w =
do p <- SW.bvule sym x =<< lit (bit i)
lazyIte (SW.bvIte sym) p (lit i) (go (i+1))
-- base case, should only happen when i = w
go i = lit i
-- Errors ----------------------------------------------------------------------
evalPanic :: String -> [String] -> a
evalPanic cxt = panic ("[What4 Symbolic]" ++ cxt)
-- Primitives ------------------------------------------------------------------
evalPrim :: W4.IsExprBuilder sym => sym -> Ident -> Maybe (Value sym)
evalPrim :: W4.IsExprBuilder sym => sym -> PrimIdent -> Maybe (Value sym)
evalPrim sym prim = Map.lookup prim (primTable sym)
-- See also Cryptol.Prims.Eval.primTable
primTable :: W4.IsExprBuilder sym => sym -> Map.Map Ident (Value sym)
primTable :: W4.IsExprBuilder sym => sym -> Map.Map PrimIdent (Value sym)
primTable w4sym = let sym = What4 w4sym in
Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
Map.union (floatPrims sym) $
Map.fromList $ map (\(n, v) -> (prelPrim n, v))
[ -- Literals
("True" , VBit (bitLit sym True))
, ("False" , VBit (bitLit sym False))
, ("number" , ecNumberV sym) -- Converts a numeric type into its corresponding value.
-- { val, rep } (Literal val rep) => rep
, ("fraction" , ecFractionV sym)
, ("ratio" , ratioV sym)
-- Zero
@ -547,372 +191,3 @@ primTable w4sym = let sym = What4 w4sym in
lazyIte ::
(W4.IsExpr p, Monad m) =>
(p W4.BaseBoolType -> a -> a -> m a) ->
p W4.BaseBoolType ->
m a ->
m a ->
m a
lazyIte f c mx my
| Just b <- W4.asConstantPred c = if b then mx else my
| otherwise =
do x <- mx
y <- my
f c x y
indexFront_int ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) ->
TValue ->
SInteger (What4 sym) ->
SEval (What4 sym) (Value sym)
indexFront_int sym mblen _a xs ix idx
| Just i <- W4.asInteger idx
= lookupSeqMap xs i
| (lo, Just hi) <- bounds
= foldr f def [lo .. hi]
| otherwise
= liftIO (X.throw (UnsupportedSymbolicOp "unbounded integer indexing"))
where
def = raiseError (What4 sym) (InvalidIndex Nothing)
f n y =
do p <- liftIO (W4.intEq sym idx =<< W4.intLit sym n)
iteValue (What4 sym) p (lookupSeqMap xs n) y
bounds =
(case W4.rangeLowBound (W4.integerBounds idx) of
W4.Inclusive l -> max l 0
_ -> 0
, case (maxIdx, W4.rangeHiBound (W4.integerBounds idx)) of
(Just n, W4.Inclusive h) -> Just (min n h)
(Just n, _) -> Just n
_ -> Nothing
)
-- Maximum possible in-bounds index given `Z m`
-- type information and the length
-- of the sequence. If the sequences is infinite and the
-- integer is unbounded, there isn't much we can do.
maxIdx =
case (mblen, ix) of
(Nat n, TVIntMod m) -> Just (min (toInteger n) (toInteger m))
(Nat n, _) -> Just n
(_ , TVIntMod m) -> Just m
_ -> Nothing
indexBack_int ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) ->
TValue ->
SInteger (What4 sym) ->
SEval (What4 sym) (Value sym)
indexBack_int sym (Nat n) a xs ix idx = indexFront_int sym (Nat n) a (reverseSeqMap n xs) ix idx
indexBack_int _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["indexBack_int"]
indexFront_word ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) ->
TValue ->
SWord (What4 sym) ->
SEval (What4 sym) (Value sym)
indexFront_word sym mblen _a xs _ix idx
| Just i <- SW.bvAsUnsignedInteger idx
= lookupSeqMap xs i
| otherwise
= foldr f def idxs
where
w = SW.bvWidth idx
def = raiseError (What4 sym) (InvalidIndex Nothing)
f n y =
do p <- liftIO (SW.bvEq sym idx =<< SW.bvLit sym w n)
iteValue (What4 sym) p (lookupSeqMap xs n) y
-- maximum possible in-bounds index given the bitwidth
-- of the index value and the length of the sequence
maxIdx =
case mblen of
Nat n | n < 2^w -> n-1
_ -> 2^w - 1
-- concrete indices to consider, intersection of the
-- range of values the index value might take with
-- the legal values
idxs =
case SW.unsignedBVBounds idx of
Just (lo, hi) -> [lo .. min hi maxIdx]
_ -> [0 .. maxIdx]
indexBack_word ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) ->
TValue ->
SWord (What4 sym) ->
SEval (What4 sym) (Value sym)
indexBack_word sym (Nat n) a xs ix idx = indexFront_word sym (Nat n) a (reverseSeqMap n xs) ix idx
indexBack_word _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["indexBack_word"]
indexFront_bits :: forall sym.
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) ->
TValue ->
[SBit (What4 sym)] ->
SEval (What4 sym) (Value sym)
indexFront_bits sym mblen _a xs _ix bits0 = go 0 (length bits0) bits0
where
go :: Integer -> Int -> [W4.Pred sym] -> W4Eval sym (Value sym)
go i _k []
-- For indices out of range, fail
| Nat n <- mblen
, i >= n
= raiseError (What4 sym) (InvalidIndex (Just i))
| otherwise
= lookupSeqMap xs i
go i k (b:bs)
-- Fail early when all possible indices we could compute from here
-- are out of bounds
| Nat n <- mblen
, (i `shiftL` k) >= n
= raiseError (What4 sym) (InvalidIndex Nothing)
| otherwise
= iteValue (What4 sym) b
(go ((i `shiftL` 1) + 1) (k-1) bs)
(go (i `shiftL` 1) (k-1) bs)
indexBack_bits ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) ->
TValue ->
[SBit (What4 sym)] ->
SEval (What4 sym) (Value sym)
indexBack_bits sym (Nat n) a xs ix idx = indexFront_bits sym (Nat n) a (reverseSeqMap n xs) ix idx
indexBack_bits _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["indexBack_bits"]
-- | Compare a symbolic word value with a concrete integer.
wordValueEqualsInteger :: forall sym.
W4.IsExprBuilder sym =>
sym ->
WordValue (What4 sym) ->
Integer ->
W4Eval sym (W4.Pred sym)
wordValueEqualsInteger sym wv i
| wordValueSize (What4 sym) wv < widthInteger i = return (W4.falsePred sym)
| otherwise =
case wv of
WordVal w -> liftIO (SW.bvEq sym w =<< SW.bvLit sym (SW.bvWidth w) i)
_ -> liftIO . bitsAre i =<< enumerateWordValueRev (What4 sym) wv -- little-endian
where
bitsAre :: Integer -> [W4.Pred sym] -> IO (W4.Pred sym)
bitsAre n [] = pure (W4.backendPred sym (n == 0))
bitsAre n (b : bs) =
do pb <- bitIs (testBit n 0) b
pbs <- bitsAre (n `shiftR` 1) bs
W4.andPred sym pb pbs
bitIs :: Bool -> W4.Pred sym -> IO (W4.Pred sym)
bitIs b x = if b then pure x else W4.notPred sym x
updateFrontSym ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) ->
Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
SEval (What4 sym) (Value sym) ->
SEval (What4 sym) (SeqMap (What4 sym))
updateFrontSym sym _len _eltTy vs (Left idx) val =
case W4.asInteger idx of
Just i -> return $ updateSeqMap vs i val
Nothing -> return $ IndexSeqMap $ \i ->
do b <- intEq (What4 sym) idx =<< integerLit (What4 sym) i
iteValue (What4 sym) b val (lookupSeqMap vs i)
updateFrontSym sym _len _eltTy vs (Right wv) val =
case wv of
WordVal w | Just j <- SW.bvAsUnsignedInteger w ->
return $ updateSeqMap vs j val
_ ->
memoMap $ IndexSeqMap $ \i ->
do b <- wordValueEqualsInteger sym wv i
iteValue (What4 sym) b val (lookupSeqMap vs i)
updateBackSym ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) ->
Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
SEval (What4 sym) (Value sym) ->
SEval (What4 sym) (SeqMap (What4 sym))
updateBackSym _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateBackSym"]
updateBackSym sym (Nat n) _eltTy vs (Left idx) val =
case W4.asInteger idx of
Just i -> return $ updateSeqMap vs (n - 1 - i) val
Nothing -> return $ IndexSeqMap $ \i ->
do b <- intEq (What4 sym) idx =<< integerLit (What4 sym) (n - 1 - i)
iteValue (What4 sym) b val (lookupSeqMap vs i)
updateBackSym sym (Nat n) _eltTy vs (Right wv) val =
case wv of
WordVal w | Just j <- SW.bvAsUnsignedInteger w ->
return $ updateSeqMap vs (n - 1 - j) val
_ ->
memoMap $ IndexSeqMap $ \i ->
do b <- wordValueEqualsInteger sym wv (n - 1 - i)
iteValue (What4 sym) b val (lookupSeqMap vs i)
updateFrontSym_word ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
WordValue (What4 sym) ->
Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
SEval (What4 sym) (GenValue (What4 sym)) ->
SEval (What4 sym) (WordValue (What4 sym))
updateFrontSym_word _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateFrontSym_word"]
updateFrontSym_word sym (Nat _) eltTy (LargeBitsVal n bv) idx val =
LargeBitsVal n <$> updateFrontSym sym (Nat n) eltTy bv idx val
updateFrontSym_word sym (Nat n) eltTy (WordVal bv) (Left idx) val =
do idx' <- wordFromInt (What4 sym) n idx
updateFrontSym_word sym (Nat n) eltTy (WordVal bv) (Right (WordVal idx')) val
updateFrontSym_word sym (Nat n) eltTy bv (Right wv) val =
case wv of
WordVal idx
| Just j <- SW.bvAsUnsignedInteger idx ->
updateWordValue (What4 sym) bv j (fromVBit <$> val)
| WordVal bw <- bv ->
WordVal <$>
do b <- fromVBit <$> val
let sz = SW.bvWidth bw
highbit <- liftIO (SW.bvLit sym sz (bit (fromInteger (sz-1))))
msk <- w4bvLshr sym highbit idx
liftIO $
case W4.asConstantPred b of
Just True -> SW.bvOr sym bw msk
Just False -> SW.bvAnd sym bw =<< SW.bvNot sym msk
Nothing ->
do q <- SW.bvFill sym sz b
bw' <- SW.bvAnd sym bw =<< SW.bvNot sym msk
SW.bvXor sym bw' =<< SW.bvAnd sym q msk
_ -> LargeBitsVal (wordValueSize (What4 sym) wv) <$>
updateFrontSym sym (Nat n) eltTy (asBitsMap (What4 sym) bv) (Right wv) val
updateBackSym_word ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
WordValue (What4 sym) ->
Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
SEval (What4 sym) (GenValue (What4 sym)) ->
SEval (What4 sym) (WordValue (What4 sym))
updateBackSym_word _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateBackSym_word"]
updateBackSym_word sym (Nat _) eltTy (LargeBitsVal n bv) idx val =
LargeBitsVal n <$> updateBackSym sym (Nat n) eltTy bv idx val
updateBackSym_word sym (Nat n) eltTy (WordVal bv) (Left idx) val =
do idx' <- wordFromInt (What4 sym) n idx
updateBackSym_word sym (Nat n) eltTy (WordVal bv) (Right (WordVal idx')) val
updateBackSym_word sym (Nat n) eltTy bv (Right wv) val =
case wv of
WordVal idx
| Just j <- SW.bvAsUnsignedInteger idx ->
updateWordValue (What4 sym) bv (n - 1 - j) (fromVBit <$> val)
| WordVal bw <- bv ->
WordVal <$>
do b <- fromVBit <$> val
let sz = SW.bvWidth bw
lowbit <- liftIO (SW.bvLit sym sz 1)
msk <- w4bvShl sym lowbit idx
liftIO $
case W4.asConstantPred b of
Just True -> SW.bvOr sym bw msk
Just False -> SW.bvAnd sym bw =<< SW.bvNot sym msk
Nothing ->
do q <- SW.bvFill sym sz b
bw' <- SW.bvAnd sym bw =<< SW.bvNot sym msk
SW.bvXor sym bw' =<< SW.bvAnd sym q msk
_ -> LargeBitsVal (wordValueSize (What4 sym) wv) <$>
updateBackSym sym (Nat n) eltTy (asBitsMap (What4 sym) bv) (Right wv) val
sshrV :: W4.IsExprBuilder sym => sym -> Value sym
sshrV sym =
nlam $ \(Nat n) ->
tlam $ \ix ->
wlam (What4 sym) $ \x -> return $
lam $ \y ->
y >>= asIndex (What4 sym) ">>$" ix >>= \case
Left i ->
do pneg <- intLessThan (What4 sym) i =<< integerLit (What4 sym) 0
zneg <- do i' <- shiftShrink (What4 sym) (Nat n) ix =<< intNegate (What4 sym) i
amt <- wordFromInt (What4 sym) n i'
w4bvShl sym x amt
zpos <- do i' <- shiftShrink (What4 sym) (Nat n) ix i
amt <- wordFromInt (What4 sym) n i'
w4bvAshr sym x amt
return (VWord (SW.bvWidth x) (WordVal <$> iteWord (What4 sym) pneg zneg zpos))
Right wv ->
do amt <- asWordVal (What4 sym) wv
return (VWord (SW.bvWidth x) (WordVal <$> w4bvAshr sym x amt))
w4bvShl :: W4.IsExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvShl sym x y = liftIO $ SW.bvShl sym x y
w4bvLshr :: W4.IsExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvLshr sym x y = liftIO $ SW.bvLshr sym x y
w4bvAshr :: W4.IsExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvAshr sym x y = liftIO $ SW.bvAshr sym x y
w4bvRol :: W4.IsExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvRol sym x y = liftIO $ SW.bvRol sym x y
w4bvRor :: W4.IsExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvRor sym x y = liftIO $ SW.bvRor sym x y

54
src/Cryptol/Eval/What4/Float.hs Normal file
View File

@ -0,0 +1,54 @@
{-# Language BlockArguments #-}
{-# Language OverloadedStrings #-}
-- | Floating point primitives for the What4 backend.
module Cryptol.Eval.What4.Float (floatPrims) where
import Data.Map(Map)
import qualified Data.Map as Map
import qualified What4.Interface as W4
import Control.Monad.IO.Class
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
import Cryptol.Eval.Value
import Cryptol.Eval.Generic
import Cryptol.Eval.What4.Value
import qualified Cryptol.Eval.What4.SFloat as W4
import Cryptol.Utils.Ident(PrimIdent, floatPrim)
-- | Table of floating point primitives
floatPrims :: W4.IsExprBuilder sym => What4 sym -> Map PrimIdent (Value sym)
floatPrims sym4@(What4 sym) =
Map.fromList [ (floatPrim i,v) | (i,v) <- nonInfixTable ]
where
(~>) = (,)
nonInfixTable =
[ "fpNaN" ~> fpConst (W4.fpNaN sym)
, "fpPosInf" ~> fpConst (W4.fpPosInf sym)
, "fpFromBits" ~> ilam \e -> ilam \p -> wlam sym4 \w ->
VFloat <$> liftIO (W4.fpFromBinary sym e p w)
, "fpToBits" ~> ilam \e -> ilam \p -> flam \x ->
pure $ VWord (e+p)
$ WordVal <$> liftIO (W4.fpToBinary sym x)
, "=.=" ~> ilam \_ -> ilam \_ -> flam \x -> pure $ flam \y ->
VBit <$> liftIO (W4.fpEq sym x y)
, "fpAdd" ~> fpBinArithV sym4 fpPlus
, "fpSub" ~> fpBinArithV sym4 fpMinus
, "fpMul" ~> fpBinArithV sym4 fpMult
, "fpDiv" ~> fpBinArithV sym4 fpDiv
]
-- | A helper for definitng floating point constants.
fpConst ::
W4.IsExprBuilder sym =>
(Integer -> Integer -> IO (W4.SFloat sym)) ->
Value sym
fpConst mk =
ilam \ e ->
VNumPoly \ ~(Nat p) ->
VFloat <$> liftIO (mk e p)

328
src/Cryptol/Eval/What4/SFloat.hs Normal file
View File

@ -0,0 +1,328 @@
{-# Language DataKinds #-}
{-# Language FlexibleContexts #-}
{-# Language GADTs #-}
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language TypeOperators #-}
-- | Working with floats of dynamic sizes.
-- This should probably be moved to What4 one day.
module Cryptol.Eval.What4.SFloat
( -- * Interface
SFloat(..)
, fpReprOf
, fpSize
-- * Constants
, fpFresh
, fpNaN
, fpPosInf
, fpFromRational
-- * Interchange formats
, fpFromBinary
, fpToBinary
-- * Relations
, SFloatRel
, fpEq
, fpEqIEEE
, fpLtIEEE
, fpGtIEEE
-- * Arithmetic
, SFloatBinArith
, fpNeg
, fpAdd
, fpSub
, fpMul
, fpDiv
-- * Conversions
, fpRound
, fpToReal
, fpFromReal
, fpFromInteger
-- * Queries
, fpIsInf, fpIsNaN
-- * Exceptions
, UnsupportedFloat(..)
, FPTypeError(..)
) where
import Control.Exception
import Data.Parameterized.Some
import Data.Parameterized.NatRepr
import What4.BaseTypes
import What4.Panic(panic)
import What4.SWord
import What4.Interface
-- | Symbolic floating point numbers.
data SFloat sym where
SFloat :: IsExpr (SymExpr sym) => SymFloat sym fpp -> SFloat sym
--------------------------------------------------------------------------------
-- | This exception is thrown if the operations try to create a
-- floating point value we do not support
data UnsupportedFloat =
UnsupportedFloat { fpWho :: String, exponentBits, precisionBits :: Integer }
deriving Show
-- | Throw 'UnsupportedFloat' exception
unsupported ::
String {- ^ Label -} ->
Integer {- ^ Exponent width -} ->
Integer {- ^ Precision width -} ->
IO a
unsupported l e p =
throwIO UnsupportedFloat { fpWho = l
, exponentBits = e
, precisionBits = p }
instance Exception UnsupportedFloat
-- | This exceptoin is throws if the types don't match.
data FPTypeError =
FPTypeError { fpExpected :: Some BaseTypeRepr
, fpActual :: Some BaseTypeRepr
}
deriving Show
instance Exception FPTypeError
fpTypeMismatch :: BaseTypeRepr t1 -> BaseTypeRepr t2 -> IO a
fpTypeMismatch expect actual =
throwIO FPTypeError { fpExpected = Some expect
, fpActual = Some actual
}
fpTypeError :: FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
fpTypeError t1 t2 =
fpTypeMismatch (BaseFloatRepr t1) (BaseFloatRepr t2)
--------------------------------------------------------------------------------
-- | Construct the 'FloatPrecisionRepr' with the given parameters.
fpRepr ::
Integer {- ^ Exponent width -} ->
Integer {- ^ Precision width -} ->
Maybe (Some FloatPrecisionRepr)
fpRepr iE iP =
do Some e <- someNat iE
LeqProof <- testLeq (knownNat @2) e
Some p <- someNat iP
LeqProof <- testLeq (knownNat @2) p
pure (Some (FloatingPointPrecisionRepr e p))
fpReprOf ::
IsExpr (SymExpr sym) => sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
fpReprOf _ e =
case exprType e of
BaseFloatRepr r -> r
fpSize :: SFloat sym -> (Integer,Integer)
fpSize (SFloat f) =
case exprType f of
BaseFloatRepr (FloatingPointPrecisionRepr e p) -> (intValue e, intValue p)
--------------------------------------------------------------------------------
-- Constants
-- | A fresh variable of the given type.
fpFresh ::
IsSymExprBuilder sym =>
sym ->
Integer ->
Integer ->
IO (SFloat sym)
fpFresh sym e p
| Just (Some fpp) <- fpRepr e p =
SFloat <$> freshConstant sym emptySymbol (BaseFloatRepr fpp)
| otherwise = unsupported "fpFresh" e p
-- | Not a number
fpNaN ::
IsExprBuilder sym =>
sym ->
Integer {- ^ Exponent width -} ->
Integer {- ^ Precision width -} ->
IO (SFloat sym)
fpNaN sym e p
| Just (Some fpp) <- fpRepr e p = SFloat <$> floatNaN sym fpp
| otherwise = unsupported "fpNaN" e p
-- | Positive infinity
fpPosInf ::
IsExprBuilder sym =>
sym ->
Integer {- ^ Exponent width -} ->
Integer {- ^ Precision width -} ->
IO (SFloat sym)
fpPosInf sym e p
| Just (Some fpp) <- fpRepr e p = SFloat <$> floatPInf sym fpp
| otherwise = unsupported "fpPosInf" e p
-- | A floating point number corresponding to the given rations.
fpFromRational ::
IsExprBuilder sym =>
sym ->
Integer {- ^ Exponent width -} ->
Integer {- ^ Precision width -} ->
Rational ->
IO (SFloat sym)
fpFromRational sym e p r
| Just (Some fpp) <- fpRepr e p = SFloat <$> floatLit sym fpp r
| otherwise = unsupported "fpFromRational" e p
-- | Make a floating point number with the given bit representation.
fpFromBinary ::
IsExprBuilder sym =>
sym ->
Integer {- ^ Exponent width -} ->
Integer {- ^ Precision width -} ->
SWord sym ->
IO (SFloat sym)
fpFromBinary sym e p swe
| DBV sw <- swe
, Just (Some fpp) <- fpRepr e p
, FloatingPointPrecisionRepr ew pw <- fpp
, let expectW = addNat ew pw
, actual@(BaseBVRepr actualW) <- exprType sw =
case testEquality expectW actualW of
Just Refl -> SFloat <$> floatFromBinary sym fpp sw
Nothing -- we want to report type correct type errors! :-)
| Just LeqProof <- testLeq (knownNat @1) expectW ->
fpTypeMismatch (BaseBVRepr expectW) actual
| otherwise -> panic "fpFromBits" [ "1 >= 2" ]
| otherwise = unsupported "fpFromBits" e p
fpToBinary :: IsExprBuilder sym => sym -> SFloat sym -> IO (SWord sym)
fpToBinary sym (SFloat f)
| FloatingPointPrecisionRepr e p <- fpReprOf sym f
, Just LeqProof <- testLeq (knownNat @1) (addNat e p)
= DBV <$> floatToBinary sym f
| otherwise = panic "fpToBinary" [ "we messed up the types" ]
--------------------------------------------------------------------------------
-- Arithmetic
fpNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym)
fpNeg sym (SFloat fl) = SFloat <$> floatNeg sym fl
fpBinArith ::
IsExprBuilder sym =>
(forall t.
sym ->
RoundingMode ->
SymFloat sym t ->
SymFloat sym t ->
IO (SymFloat sym t)
) ->
sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym)
fpBinArith fun sym r (SFloat x) (SFloat y) =
let t1 = sym `fpReprOf` x
t2 = sym `fpReprOf` y
in
case testEquality t1 t2 of
Just Refl -> SFloat <$> fun sym r x y
_ -> fpTypeError t1 t2
type SFloatBinArith sym =
sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym)
fpAdd :: IsExprBuilder sym => SFloatBinArith sym
fpAdd = fpBinArith floatAdd
fpSub :: IsExprBuilder sym => SFloatBinArith sym
fpSub = fpBinArith floatSub
fpMul :: IsExprBuilder sym => SFloatBinArith sym
fpMul = fpBinArith floatMul
fpDiv :: IsExprBuilder sym => SFloatBinArith sym
fpDiv = fpBinArith floatDiv
--------------------------------------------------------------------------------
fpRel ::
IsExprBuilder sym =>
(forall t.
sym ->
SymFloat sym t ->
SymFloat sym t ->
IO (Pred sym)
) ->
sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
fpRel fun sym (SFloat x) (SFloat y) =
let t1 = sym `fpReprOf` x
t2 = sym `fpReprOf` y
in
case testEquality t1 t2 of
Just Refl -> fun sym x y
_ -> fpTypeError t1 t2
type SFloatRel sym =
sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
fpEq :: IsExprBuilder sym => SFloatRel sym
fpEq = fpRel floatEq
fpEqIEEE :: IsExprBuilder sym => SFloatRel sym
fpEqIEEE = fpRel floatFpEq
fpLtIEEE :: IsExprBuilder sym => SFloatRel sym
fpLtIEEE = fpRel floatLt
fpGtIEEE :: IsExprBuilder sym => SFloatRel sym
fpGtIEEE = fpRel floatGt
--------------------------------------------------------------------------------
fpRound ::
IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
fpRound sym r (SFloat x) = SFloat <$> floatRound sym r x
-- | This is undefined on "special" values (NaN,infinity)
fpToReal :: IsExprBuilder sym => sym -> SFloat sym -> IO (SymReal sym)
fpToReal sym (SFloat x) = floatToReal sym x
fpFromReal ::
IsExprBuilder sym =>
sym -> Integer -> Integer -> RoundingMode -> SymReal sym -> IO (SFloat sym)
fpFromReal sym e p r x
| Just (Some repr) <- fpRepr e p = SFloat <$> realToFloat sym repr r x
| otherwise = unsupported "fpFromReal" e p
fpFromInteger ::
IsExprBuilder sym =>
sym -> Integer -> Integer -> RoundingMode -> SymInteger sym -> IO (SFloat sym)
fpFromInteger sym e p r x = fpFromReal sym e p r =<< integerToReal sym x
--------------------------------------------------------------------------------
fpIsInf :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsInf sym (SFloat x) = floatIsInf sym x
fpIsNaN :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsNaN sym (SFloat x) = floatIsNaN sym x

820
src/Cryptol/Eval/What4/Value.hs Normal file
View File

@ -0,0 +1,820 @@
-- |
-- Module : Cryptol.Eval.What4
-- Copyright : (c) 2020 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.Eval.What4.Value where
import qualified Control.Exception as X
import Control.Monad (foldM)
import Control.Monad.IO.Class
import Data.Bits (bit, shiftR, shiftL, testBit)
import qualified Data.BitVector.Sized as BV
import Data.List
import Data.Parameterized.NatRepr
import Data.Parameterized.Some
import qualified What4.Interface as W4
import qualified What4.SWord as SW
import qualified Cryptol.Eval.What4.SFloat as FP
import qualified What4.Utils.AbstractDomains as W4
import Cryptol.Eval.Backend
import Cryptol.Eval.Concrete.Value( BV(..), ppBV )
import Cryptol.Eval.Generic
import Cryptol.Eval.Monad (Eval(..), EvalError(..), Unsupported(..), io, delayFill, blackhole)
import Cryptol.Eval.Type (TValue(..))
import Cryptol.Eval.Value
import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), widthInteger)
import Cryptol.Utils.Panic
import Cryptol.Utils.PP
data What4 sym = What4 sym
type Value sym = GenValue (What4 sym)
data W4Result sym a
= W4Error !EvalError
| W4Result !(W4.Pred sym) !a -- safety predicate and result
instance Functor (W4Result sym) where
fmap _ (W4Error err) = W4Error err
fmap f (W4Result p x) = W4Result p (f x)
total :: W4.IsExprBuilder sym => sym -> a -> W4Result sym a
total sym = W4Result (W4.backendPred sym True)
-- TODO? Reorganize this to use PartialT ?
newtype W4Eval sym a = W4Eval{ w4Eval :: sym -> Eval (W4Result sym a) }
deriving (Functor)
instance W4.IsExprBuilder sym => Applicative (W4Eval sym) where
pure x = W4Eval $ \sym -> pure (total sym x)
mf <*> mx = mf >>= \f -> mx >>= \x -> pure (f x)
instance W4.IsExprBuilder sym => Monad (W4Eval sym) where
return = pure
x >>= f = W4Eval $ \sym ->
w4Eval x sym >>= \case
W4Error err -> pure (W4Error err)
W4Result px x' ->
w4Eval (f x') sym >>= \case
W4Error err -> pure (W4Error err)
W4Result pz z ->
do p <- io (W4.andPred sym px pz)
pure (W4Result p z)
instance W4.IsExprBuilder sym => MonadIO (W4Eval sym) where
liftIO m = W4Eval $ \sym -> fmap (total sym) (liftIO m)
assertBVDivisor :: W4.IsExprBuilder sym => sym -> SW.SWord sym -> W4Eval sym ()
assertBVDivisor sym x =
do p <- liftIO (SW.bvIsNonzero sym x)
assertSideCondition (What4 sym) p DivideByZero
assertIntDivisor :: W4.IsExprBuilder sym => sym -> W4.SymInteger sym -> W4Eval sym ()
assertIntDivisor sym x =
do p <- liftIO (W4.notPred sym =<< W4.intEq sym x =<< W4.intLit sym 0)
assertSideCondition (What4 sym) p DivideByZero
instance W4.IsExprBuilder sym => Backend (What4 sym) where
type SBit (What4 sym) = W4.Pred sym
type SWord (What4 sym) = SW.SWord sym
type SInteger (What4 sym) = W4.SymInteger sym
type SFloat (What4 sym) = FP.SFloat sym
type SEval (What4 sym) = W4Eval sym
raiseError _ err = W4Eval (\_ -> pure (W4Error err))
assertSideCondition _ cond err
| Just False <- W4.asConstantPred cond = W4Eval (\_ -> pure (W4Error err))
| otherwise = W4Eval (\_ -> pure (W4Result cond ()))
isReady (What4 sym) m =
case w4Eval m sym of
Ready _ -> True
_ -> False
sDelayFill _ m retry = W4Eval $ \sym ->
do m' <- delayFill (w4Eval m sym) (w4Eval retry sym)
pure (total sym (W4Eval (const m')))
sDeclareHole _ msg = W4Eval $ \sym ->
do (hole, fill) <- blackhole msg
pure (total sym ( W4Eval (const hole), \m -> W4Eval (\sym' -> fmap (total sym') (fill (w4Eval m sym'))) ))
mergeEval _sym f c mx my = W4Eval $ \sym ->
do rx <- w4Eval mx sym
ry <- w4Eval my sym
case (rx, ry) of
(W4Error err, W4Error _) ->
pure $ W4Error err -- arbitrarily choose left error to report
(W4Error _, W4Result p y) ->
do p' <- io (W4.andPred sym p =<< W4.notPred sym c)
pure $ W4Result p' y
(W4Result p x, W4Error _) ->
do p' <- io (W4.andPred sym p c)
pure $ W4Result p' x
(W4Result px x, W4Result py y) ->
do zr <- w4Eval (f c x y) sym
case zr of
W4Error err -> pure $ W4Error err
W4Result pz z ->
do p' <- io (W4.andPred sym pz =<< W4.itePred sym c px py)
pure $ W4Result p' z
wordAsChar _ bv
| SW.bvWidth bv == 8 = toEnum . fromInteger <$> SW.bvAsUnsignedInteger bv
| otherwise = Nothing
wordLen _ bv = SW.bvWidth bv
bitLit (What4 sym) b = W4.backendPred sym b
bitAsLit _ v = W4.asConstantPred v
wordLit (What4 sym) intw i
| Just (Some w) <- someNat intw
= case isPosNat w of
Nothing -> pure $ SW.ZBV
Just LeqProof -> SW.DBV <$> liftIO (W4.bvLit sym w (BV.mkBV w i))
| otherwise = panic "what4: wordLit" ["invalid bit width:", show intw ]
wordAsLit _ v
| Just x <- SW.bvAsUnsignedInteger v = Just (SW.bvWidth v, x)
| otherwise = Nothing
integerLit (What4 sym) i = liftIO (W4.intLit sym i)
integerAsLit _ v = W4.asInteger v
ppBit _ v
| Just b <- W4.asConstantPred v = text $! if b then "True" else "False"
| otherwise = text "?"
ppWord _ opts v
| Just x <- SW.bvAsUnsignedInteger v
= ppBV opts (BV (SW.bvWidth v) x)
| otherwise = text "[?]"
ppInteger _ _opts v
| Just x <- W4.asInteger v = integer x
| otherwise = text "[?]"
ppFloat _ _opts _ = text "[?]"
iteBit (What4 sym) c x y = liftIO (W4.itePred sym c x y)
iteWord (What4 sym) c x y = liftIO (SW.bvIte sym c x y)
iteInteger (What4 sym) c x y = liftIO (W4.intIte sym c x y)
bitEq (What4 sym) x y = liftIO (W4.eqPred sym x y)
bitAnd (What4 sym) x y = liftIO (W4.andPred sym x y)
bitOr (What4 sym) x y = liftIO (W4.orPred sym x y)
bitXor (What4 sym) x y = liftIO (W4.xorPred sym x y)
bitComplement (What4 sym) x = liftIO (W4.notPred sym x)
wordBit (What4 sym) bv idx = liftIO (SW.bvAtBE sym bv idx)
wordUpdate (What4 sym) bv idx b = liftIO (SW.bvSetBE sym bv idx b)
packWord sym bs =
do z <- wordLit sym (genericLength bs) 0
let f w (idx,b) = wordUpdate sym w idx b
foldM f z (zip [0..] bs)
unpackWord (What4 sym) bv = liftIO $
mapM (SW.bvAtBE sym bv) [0 .. SW.bvWidth bv-1]
joinWord (What4 sym) x y = liftIO $ SW.bvJoin sym x y
splitWord _sym 0 _ bv = pure (SW.ZBV, bv)
splitWord _sym _ 0 bv = pure (bv, SW.ZBV)
splitWord (What4 sym) lw rw bv = liftIO $
do l <- SW.bvSliceBE sym 0 lw bv
r <- SW.bvSliceBE sym lw rw bv
return (l, r)
extractWord (What4 sym) bits idx bv =
liftIO $ SW.bvSliceBE sym idx bits bv
wordEq (What4 sym) x y = liftIO (SW.bvEq sym x y)
wordLessThan (What4 sym) x y = liftIO (SW.bvult sym x y)
wordGreaterThan (What4 sym) x y = liftIO (SW.bvugt sym x y)
wordSignedLessThan (What4 sym) x y = liftIO (SW.bvslt sym x y)
wordOr (What4 sym) x y = liftIO (SW.bvOr sym x y)
wordAnd (What4 sym) x y = liftIO (SW.bvAnd sym x y)
wordXor (What4 sym) x y = liftIO (SW.bvXor sym x y)
wordComplement (What4 sym) x = liftIO (SW.bvNot sym x)
wordPlus (What4 sym) x y = liftIO (SW.bvAdd sym x y)
wordMinus (What4 sym) x y = liftIO (SW.bvSub sym x y)
wordMult (What4 sym) x y = liftIO (SW.bvMul sym x y)
wordNegate (What4 sym) x = liftIO (SW.bvNeg sym x)
wordLg2 (What4 sym) x = sLg2 sym x
wordDiv (What4 sym) x y =
do assertBVDivisor sym y
liftIO (SW.bvUDiv sym x y)
wordMod (What4 sym) x y =
do assertBVDivisor sym y
liftIO (SW.bvURem sym x y)
wordSignedDiv (What4 sym) x y =
do assertBVDivisor sym y
liftIO (SW.bvSDiv sym x y)
wordSignedMod (What4 sym) x y =
do assertBVDivisor sym y
liftIO (SW.bvSRem sym x y)
wordToInt (What4 sym) x = liftIO (SW.bvToInteger sym x)
wordFromInt (What4 sym) width i = liftIO (SW.integerToBV sym i width)
intPlus (What4 sym) x y = liftIO $ W4.intAdd sym x y
intMinus (What4 sym) x y = liftIO $ W4.intSub sym x y
intMult (What4 sym) x y = liftIO $ W4.intMul sym x y
intNegate (What4 sym) x = liftIO $ W4.intNeg sym x
-- NB: What4's division operation provides SMTLib's euclidean division,
-- which doesn't match the round-to-neg-infinity semantics of Cryptol,
-- so we have to do some work to get the desired semantics.
intDiv (What4 sym) x y =
do assertIntDivisor sym y
liftIO $ do
neg <- liftIO (W4.intLt sym y =<< W4.intLit sym 0)
case W4.asConstantPred neg of
Just False -> W4.intDiv sym x y
Just True ->
do xneg <- W4.intNeg sym x
yneg <- W4.intNeg sym y
W4.intDiv sym xneg yneg
Nothing ->
do xneg <- W4.intNeg sym x
yneg <- W4.intNeg sym y
zneg <- W4.intDiv sym xneg yneg
z <- W4.intDiv sym x y
W4.intIte sym neg zneg z
-- NB: What4's division operation provides SMTLib's euclidean division,
-- which doesn't match the round-to-neg-infinity semantics of Cryptol,
-- so we have to do some work to get the desired semantics.
intMod (What4 sym) x y =
do assertIntDivisor sym y
liftIO $ do
neg <- liftIO (W4.intLt sym y =<< W4.intLit sym 0)
case W4.asConstantPred neg of
Just False -> W4.intMod sym x y
Just True ->
do xneg <- W4.intNeg sym x
yneg <- W4.intNeg sym y
W4.intNeg sym =<< W4.intMod sym xneg yneg
Nothing ->
do xneg <- W4.intNeg sym x
yneg <- W4.intNeg sym y
z <- W4.intMod sym x y
zneg <- W4.intNeg sym =<< W4.intMod sym xneg yneg
W4.intIte sym neg zneg z
intEq (What4 sym) x y = liftIO $ W4.intEq sym x y
intLessThan (What4 sym) x y = liftIO $ W4.intLt sym x y
intGreaterThan (What4 sym) x y = liftIO $ W4.intLt sym y x
-- NB, we don't do reduction here on symbolic values
intToZn (What4 sym) m x
| Just xi <- W4.asInteger x
= liftIO $ W4.intLit sym (xi `mod` m)
| otherwise
= pure x
znToInt _ 0 _ = evalPanic "znToInt" ["0 modulus not allowed"]
znToInt (What4 sym) m x = liftIO (W4.intMod sym x =<< W4.intLit sym m)
znEq _ 0 _ _ = evalPanic "znEq" ["0 modulus not allowed"]
znEq (What4 sym) m x y = liftIO $
do diff <- W4.intSub sym x y
W4.intDivisible sym diff (fromInteger m)
znPlus (What4 sym) m x y = liftIO $ sModAdd sym m x y
znMinus (What4 sym) m x y = liftIO $ sModSub sym m x y
znMult (What4 sym) m x y = liftIO $ sModMult sym m x y
znNegate (What4 sym) m x = liftIO $ sModNegate sym m x
--------------------------------------------------------------
fpLit (What4 sym) e p r = liftIO $ FP.fpFromRational sym e p r
fpEq (What4 sym) x y = liftIO $ FP.fpEqIEEE sym x y
fpLessThan (What4 sym) x y = liftIO $ FP.fpLtIEEE sym x y
fpGreaterThan (What4 sym) x y = liftIO $ FP.fpGtIEEE sym x y
fpPlus = fpBinArith FP.fpAdd
fpMinus = fpBinArith FP.fpSub
fpMult = fpBinArith FP.fpMul
fpDiv = fpBinArith FP.fpDiv
fpNeg (What4 sym) x = liftIO $ FP.fpNeg sym x
fpFromInteger sym@(What4 sy) e p r x =
do rm <- fpRoundingMode sym r
liftIO $ FP.fpFromInteger sy e p rm x
fpToInteger = fpCvtToInteger
sModAdd :: W4.IsExprBuilder sym =>
sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModAdd _sym 0 _ _ = evalPanic "sModAdd" ["0 modulus not allowed"]
sModAdd sym m x y
| Just xi <- W4.asInteger x
, Just yi <- W4.asInteger y
= W4.intLit sym ((xi+yi) `mod` m)
| otherwise
= W4.intAdd sym x y
sModSub :: W4.IsExprBuilder sym =>
sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModSub _sym 0 _ _ = evalPanic "sModSub" ["0 modulus not allowed"]
sModSub sym m x y
| Just xi <- W4.asInteger x
, Just yi <- W4.asInteger y
= W4.intLit sym ((xi-yi) `mod` m)
| otherwise
= W4.intSub sym x y
sModMult :: W4.IsExprBuilder sym =>
sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModMult _sym 0 _ _ = evalPanic "sModMult" ["0 modulus not allowed"]
sModMult sym m x y
| Just xi <- W4.asInteger x
, Just yi <- W4.asInteger y
= W4.intLit sym ((xi*yi) `mod` m)
| otherwise
= W4.intMul sym x y
sModNegate :: W4.IsExprBuilder sym =>
sym -> Integer -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModNegate _sym 0 _ = evalPanic "sModMult" ["0 modulus not allowed"]
sModNegate sym m x
| Just xi <- W4.asInteger x
= W4.intLit sym ((negate xi) `mod` m)
| otherwise
= W4.intNeg sym x
-- | Try successive powers of 2 to find the first that dominates the input.
-- We could perhaps reduce to using CLZ instead...
sLg2 :: W4.IsExprBuilder sym => sym -> SW.SWord sym -> SEval (What4 sym) (SW.SWord sym)
sLg2 sym x = liftIO $ go 0
where
w = SW.bvWidth x
lit n = SW.bvLit sym w (toInteger n)
go i | toInteger i < w =
do p <- SW.bvule sym x =<< lit (bit i)
lazyIte (SW.bvIte sym) p (lit i) (go (i+1))
-- base case, should only happen when i = w
go i = lit i
-- Errors ----------------------------------------------------------------------
evalPanic :: String -> [String] -> a
evalPanic cxt = panic ("[What4 Symbolic]" ++ cxt)
lazyIte ::
(W4.IsExpr p, Monad m) =>
(p W4.BaseBoolType -> a -> a -> m a) ->
p W4.BaseBoolType ->
m a ->
m a ->
m a
lazyIte f c mx my
| Just b <- W4.asConstantPred c = if b then mx else my
| otherwise =
do x <- mx
y <- my
f c x y
indexFront_int ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) ->
TValue ->
SInteger (What4 sym) ->
SEval (What4 sym) (Value sym)
indexFront_int sym mblen _a xs ix idx
| Just i <- W4.asInteger idx
= lookupSeqMap xs i
| (lo, Just hi) <- bounds
= foldr f def [lo .. hi]
| otherwise
= liftIO (X.throw (UnsupportedSymbolicOp "unbounded integer indexing"))
where
def = raiseError (What4 sym) (InvalidIndex Nothing)
f n y =
do p <- liftIO (W4.intEq sym idx =<< W4.intLit sym n)
iteValue (What4 sym) p (lookupSeqMap xs n) y
bounds =
(case W4.rangeLowBound (W4.integerBounds idx) of
W4.Inclusive l -> max l 0
_ -> 0
, case (maxIdx, W4.rangeHiBound (W4.integerBounds idx)) of
(Just n, W4.Inclusive h) -> Just (min n h)
(Just n, _) -> Just n
_ -> Nothing
)
-- Maximum possible in-bounds index given `Z m`
-- type information and the length
-- of the sequence. If the sequences is infinite and the
-- integer is unbounded, there isn't much we can do.
maxIdx =
case (mblen, ix) of
(Nat n, TVIntMod m) -> Just (min (toInteger n) (toInteger m))
(Nat n, _) -> Just n
(_ , TVIntMod m) -> Just m
_ -> Nothing
indexBack_int ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) ->
TValue ->
SInteger (What4 sym) ->
SEval (What4 sym) (Value sym)
indexBack_int sym (Nat n) a xs ix idx = indexFront_int sym (Nat n) a (reverseSeqMap n xs) ix idx
indexBack_int _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["indexBack_int"]
indexFront_word ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) ->
TValue ->
SWord (What4 sym) ->
SEval (What4 sym) (Value sym)
indexFront_word sym mblen _a xs _ix idx
| Just i <- SW.bvAsUnsignedInteger idx
= lookupSeqMap xs i
| otherwise
= foldr f def idxs
where
w = SW.bvWidth idx
def = raiseError (What4 sym) (InvalidIndex Nothing)
f n y =
do p <- liftIO (SW.bvEq sym idx =<< SW.bvLit sym w n)
iteValue (What4 sym) p (lookupSeqMap xs n) y
-- maximum possible in-bounds index given the bitwidth
-- of the index value and the length of the sequence
maxIdx =
case mblen of
Nat n | n < 2^w -> n-1
_ -> 2^w - 1
-- concrete indices to consider, intersection of the
-- range of values the index value might take with
-- the legal values
idxs =
case SW.unsignedBVBounds idx of
Just (lo, hi) -> [lo .. min hi maxIdx]
_ -> [0 .. maxIdx]
indexBack_word ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) ->
TValue ->
SWord (What4 sym) ->
SEval (What4 sym) (Value sym)
indexBack_word sym (Nat n) a xs ix idx = indexFront_word sym (Nat n) a (reverseSeqMap n xs) ix idx
indexBack_word _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["indexBack_word"]
indexFront_bits :: forall sym.
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) ->
TValue ->
[SBit (What4 sym)] ->
SEval (What4 sym) (Value sym)
indexFront_bits sym mblen _a xs _ix bits0 = go 0 (length bits0) bits0
where
go :: Integer -> Int -> [W4.Pred sym] -> W4Eval sym (Value sym)
go i _k []
-- For indices out of range, fail
| Nat n <- mblen
, i >= n
= raiseError (What4 sym) (InvalidIndex (Just i))
| otherwise
= lookupSeqMap xs i
go i k (b:bs)
-- Fail early when all possible indices we could compute from here
-- are out of bounds
| Nat n <- mblen
, (i `shiftL` k) >= n
= raiseError (What4 sym) (InvalidIndex Nothing)
| otherwise
= iteValue (What4 sym) b
(go ((i `shiftL` 1) + 1) (k-1) bs)
(go (i `shiftL` 1) (k-1) bs)
indexBack_bits ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) ->
TValue ->
[SBit (What4 sym)] ->
SEval (What4 sym) (Value sym)
indexBack_bits sym (Nat n) a xs ix idx = indexFront_bits sym (Nat n) a (reverseSeqMap n xs) ix idx
indexBack_bits _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["indexBack_bits"]
-- | Compare a symbolic word value with a concrete integer.
wordValueEqualsInteger :: forall sym.
W4.IsExprBuilder sym =>
sym ->
WordValue (What4 sym) ->
Integer ->
W4Eval sym (W4.Pred sym)
wordValueEqualsInteger sym wv i
| wordValueSize (What4 sym) wv < widthInteger i = return (W4.falsePred sym)
| otherwise =
case wv of
WordVal w -> liftIO (SW.bvEq sym w =<< SW.bvLit sym (SW.bvWidth w) i)
_ -> liftIO . bitsAre i =<< enumerateWordValueRev (What4 sym) wv -- little-endian
where
bitsAre :: Integer -> [W4.Pred sym] -> IO (W4.Pred sym)
bitsAre n [] = pure (W4.backendPred sym (n == 0))
bitsAre n (b : bs) =
do pb <- bitIs (testBit n 0) b
pbs <- bitsAre (n `shiftR` 1) bs
W4.andPred sym pb pbs
bitIs :: Bool -> W4.Pred sym -> IO (W4.Pred sym)
bitIs b x = if b then pure x else W4.notPred sym x
updateFrontSym ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) ->
Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
SEval (What4 sym) (Value sym) ->
SEval (What4 sym) (SeqMap (What4 sym))
updateFrontSym sym _len _eltTy vs (Left idx) val =
case W4.asInteger idx of
Just i -> return $ updateSeqMap vs i val
Nothing -> return $ IndexSeqMap $ \i ->
do b <- intEq (What4 sym) idx =<< integerLit (What4 sym) i
iteValue (What4 sym) b val (lookupSeqMap vs i)
updateFrontSym sym _len _eltTy vs (Right wv) val =
case wv of
WordVal w | Just j <- SW.bvAsUnsignedInteger w ->
return $ updateSeqMap vs j val
_ ->
memoMap $ IndexSeqMap $ \i ->
do b <- wordValueEqualsInteger sym wv i
iteValue (What4 sym) b val (lookupSeqMap vs i)
updateBackSym ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) ->
Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
SEval (What4 sym) (Value sym) ->
SEval (What4 sym) (SeqMap (What4 sym))
updateBackSym _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateBackSym"]
updateBackSym sym (Nat n) _eltTy vs (Left idx) val =
case W4.asInteger idx of
Just i -> return $ updateSeqMap vs (n - 1 - i) val
Nothing -> return $ IndexSeqMap $ \i ->
do b <- intEq (What4 sym) idx =<< integerLit (What4 sym) (n - 1 - i)
iteValue (What4 sym) b val (lookupSeqMap vs i)
updateBackSym sym (Nat n) _eltTy vs (Right wv) val =
case wv of
WordVal w | Just j <- SW.bvAsUnsignedInteger w ->
return $ updateSeqMap vs (n - 1 - j) val
_ ->
memoMap $ IndexSeqMap $ \i ->
do b <- wordValueEqualsInteger sym wv (n - 1 - i)
iteValue (What4 sym) b val (lookupSeqMap vs i)
updateFrontSym_word ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
WordValue (What4 sym) ->
Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
SEval (What4 sym) (GenValue (What4 sym)) ->
SEval (What4 sym) (WordValue (What4 sym))
updateFrontSym_word _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateFrontSym_word"]
updateFrontSym_word sym (Nat _) eltTy (LargeBitsVal n bv) idx val =
LargeBitsVal n <$> updateFrontSym sym (Nat n) eltTy bv idx val
updateFrontSym_word sym (Nat n) eltTy (WordVal bv) (Left idx) val =
do idx' <- wordFromInt (What4 sym) n idx
updateFrontSym_word sym (Nat n) eltTy (WordVal bv) (Right (WordVal idx')) val
updateFrontSym_word sym (Nat n) eltTy bv (Right wv) val =
case wv of
WordVal idx
| Just j <- SW.bvAsUnsignedInteger idx ->
updateWordValue (What4 sym) bv j (fromVBit <$> val)
| WordVal bw <- bv ->
WordVal <$>
do b <- fromVBit <$> val
let sz = SW.bvWidth bw
highbit <- liftIO (SW.bvLit sym sz (bit (fromInteger (sz-1))))
msk <- w4bvLshr sym highbit idx
liftIO $
case W4.asConstantPred b of
Just True -> SW.bvOr sym bw msk
Just False -> SW.bvAnd sym bw =<< SW.bvNot sym msk
Nothing ->
do q <- SW.bvFill sym sz b
bw' <- SW.bvAnd sym bw =<< SW.bvNot sym msk
SW.bvXor sym bw' =<< SW.bvAnd sym q msk
_ -> LargeBitsVal (wordValueSize (What4 sym) wv) <$>
updateFrontSym sym (Nat n) eltTy (asBitsMap (What4 sym) bv) (Right wv) val
updateBackSym_word ::
W4.IsExprBuilder sym =>
sym ->
Nat' ->
TValue ->
WordValue (What4 sym) ->
Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
SEval (What4 sym) (GenValue (What4 sym)) ->
SEval (What4 sym) (WordValue (What4 sym))
updateBackSym_word _ Inf _ _ _ _ = evalPanic "Expected finite sequence" ["updateBackSym_word"]
updateBackSym_word sym (Nat _) eltTy (LargeBitsVal n bv) idx val =
LargeBitsVal n <$> updateBackSym sym (Nat n) eltTy bv idx val
updateBackSym_word sym (Nat n) eltTy (WordVal bv) (Left idx) val =
do idx' <- wordFromInt (What4 sym) n idx
updateBackSym_word sym (Nat n) eltTy (WordVal bv) (Right (WordVal idx')) val
updateBackSym_word sym (Nat n) eltTy bv (Right wv) val =
case wv of
WordVal idx
| Just j <- SW.bvAsUnsignedInteger idx ->
updateWordValue (What4 sym) bv (n - 1 - j) (fromVBit <$> val)
| WordVal bw <- bv ->
WordVal <$>
do b <- fromVBit <$> val
let sz = SW.bvWidth bw
lowbit <- liftIO (SW.bvLit sym sz 1)
msk <- w4bvShl sym lowbit idx
liftIO $
case W4.asConstantPred b of
Just True -> SW.bvOr sym bw msk
Just False -> SW.bvAnd sym bw =<< SW.bvNot sym msk
Nothing ->
do q <- SW.bvFill sym sz b
bw' <- SW.bvAnd sym bw =<< SW.bvNot sym msk
SW.bvXor sym bw' =<< SW.bvAnd sym q msk
_ -> LargeBitsVal (wordValueSize (What4 sym) wv) <$>
updateBackSym sym (Nat n) eltTy (asBitsMap (What4 sym) bv) (Right wv) val
sshrV :: W4.IsExprBuilder sym => sym -> Value sym
sshrV sym =
nlam $ \(Nat n) ->
tlam $ \ix ->
wlam (What4 sym) $ \x -> return $
lam $ \y ->
y >>= asIndex (What4 sym) ">>$" ix >>= \case
Left i ->
do pneg <- intLessThan (What4 sym) i =<< integerLit (What4 sym) 0
zneg <- do i' <- shiftShrink (What4 sym) (Nat n) ix =<< intNegate (What4 sym) i
amt <- wordFromInt (What4 sym) n i'
w4bvShl sym x amt
zpos <- do i' <- shiftShrink (What4 sym) (Nat n) ix i
amt <- wordFromInt (What4 sym) n i'
w4bvAshr sym x amt
return (VWord (SW.bvWidth x) (WordVal <$> iteWord (What4 sym) pneg zneg zpos))
Right wv ->
do amt <- asWordVal (What4 sym) wv
return (VWord (SW.bvWidth x) (WordVal <$> w4bvAshr sym x amt))
w4bvShl :: W4.IsExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvShl sym x y = liftIO $ SW.bvShl sym x y
w4bvLshr :: W4.IsExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvLshr sym x y = liftIO $ SW.bvLshr sym x y
w4bvAshr :: W4.IsExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvAshr sym x y = liftIO $ SW.bvAshr sym x y
w4bvRol :: W4.IsExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvRol sym x y = liftIO $ SW.bvRol sym x y
w4bvRor :: W4.IsExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvRor sym x y = liftIO $ SW.bvRor sym x y
fpRoundingMode ::
W4.IsExprBuilder sym =>
What4 sym -> SWord (What4 sym) -> SEval (What4 sym) W4.RoundingMode
fpRoundingMode sym@(What4 sy) v =
case wordAsLit sym v of
Just (_w,i) ->
case i of
0 -> pure W4.RNE
1 -> pure W4.RNA
2 -> pure W4.RTP
3 -> pure W4.RTN
4 -> pure W4.RTZ
x -> do let err = BadRoundingMode x
assertSideCondition sym (W4.falsePred sy) err
raiseError sym err
_ -> liftIO $ X.throwIO $ UnsupportedSymbolicOp "rounding mode"
fpBinArith ::
W4.IsExprBuilder sym =>
FP.SFloatBinArith sym ->
What4 sym ->
SWord (What4 sym) ->
SFloat (What4 sym) ->
SFloat (What4 sym) ->
SEval (What4 sym) (SFloat (What4 sym))
fpBinArith fun = \sym@(What4 s) r x y ->
do m <- fpRoundingMode sym r
liftIO (fun s m x y)
fpCvtToInteger ::
(W4.IsExprBuilder sy, sym ~ What4 sy) =>
sym -> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpCvtToInteger sym@(What4 sy) fun r x =
do grd <- liftIO
do bad1 <- FP.fpIsInf sy x
bad2 <- FP.fpIsNaN sy x
W4.notPred sy =<< W4.orPred sy bad1 bad2
assertSideCondition sym grd (BadValue fun)
rnd <- fpRoundingMode sym r
liftIO
do y <- FP.fpToReal sy x
case rnd of
W4.RNE -> undefined -- XXX
W4.RNA -> W4.realRound sy y
W4.RTP -> W4.realCeil sy y
W4.RTN -> W4.realFloor sy y
W4.RTZ -> undefined -- XXX

14
src/Cryptol/ModuleSystem/Base.hs
View File

@ -42,14 +42,14 @@ import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.PP as T
import qualified Cryptol.TypeCheck.Sanity as TcSanity
import Cryptol.Transform.AddModParams (addModParams)
import Cryptol.Utils.Ident (preludeName, arrayName, interactiveName
import Cryptol.Utils.Ident (preludeName, floatName, arrayName, interactiveName
, modNameChunks, notParamInstModName
, isParamInstModName )
import Cryptol.Utils.PP (pretty)
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.Logger(logPutStrLn, logPrint)
import Cryptol.Prelude (preludeContents, arrayContents)
import Cryptol.Prelude (preludeContents, floatContents, arrayContents)
import Cryptol.Transform.MonoValues (rewModule)
@ -259,6 +259,7 @@ findModule n = do
handleNotFound =
case n of
m | m == preludeName -> pure (InMem "Cryptol" preludeContents)
| m == floatName -> pure (InMem "Float" floatContents)
| m == arrayName -> pure (InMem "Array" arrayContents)
_ -> moduleNotFound n =<< getSearchPath
@ -369,8 +370,15 @@ checkDecls ds = do
getPrimMap :: ModuleM PrimMap
getPrimMap =
do env <- getModuleEnv
let mkPrims = ifacePrimMap . lmInterface
mp `alsoPrimFrom` m =
case lookupModule m env of
Nothing -> mp
Just lm -> mkPrims lm <> mp
case lookupModule preludeName env of
Just lm -> return (ifacePrimMap (lmInterface lm))
Just prel -> return $ mkPrims prel
`alsoPrimFrom` floatName
Nothing -> panic "Cryptol.ModuleSystem.Base.getPrimMap"
[ "Unable to find the prelude" ]

14
src/Cryptol/ModuleSystem/Interface.hs
View File

@ -27,6 +27,7 @@ module Cryptol.ModuleSystem.Interface (
import Cryptol.ModuleSystem.Name
import Cryptol.TypeCheck.AST
import Cryptol.Utils.Ident (ModName)
import Cryptol.Utils.Panic(panic)
import Cryptol.Parser.Position(Located)
import qualified Data.Map as Map
@ -177,6 +178,13 @@ ifaceDeclsPrimMap IfaceDecls { .. } =
, primTypes = Map.fromList (newtypes ++ types)
}
where
exprs = [ (nameIdent n, n) | n <- Map.keys ifDecls ]
newtypes = [ (nameIdent n, n) | n <- Map.keys ifNewtypes ]
types = [ (nameIdent n, n) | n <- Map.keys ifTySyns ]
entry n = case asPrim n of
Just pid -> (pid,n)
Nothing ->
panic "ifaceDeclsPrimMap"
[ "Top level name not declared in a module?"
, show n ]
exprs = map entry (Map.keys ifDecls)
newtypes = map entry (Map.keys ifNewtypes)
types = map entry (Map.keys ifTySyns)

21
src/Cryptol/ModuleSystem/Name.hs
View File

@ -13,7 +13,6 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
-- for the instances of RunM and BaseM
{-# LANGUAGE UndecidableInstances #-}
@ -219,14 +218,11 @@ nameFixity :: Name -> Maybe Fixity
nameFixity = nFixity
asPrim :: Name -> Maybe Ident
asPrim :: Name -> Maybe PrimIdent
asPrim Name { .. } =
case nInfo of
Declared p _
| p == preludeName -> Just nIdent
| p == arrayName ->
Just $ mkIdent $ modNameToText p <> "::" <> identText nIdent
_ -> Nothing
Declared p _ -> Just $ PrimIdent p $ identText nIdent
_ -> Nothing
toParamInstName :: Name -> Name
toParamInstName n =
@ -351,11 +347,16 @@ paramModRecParam = Name { nInfo = Parameter
-- Prim Maps -------------------------------------------------------------------
-- | A mapping from an identifier defined in some module to its real name.
data PrimMap = PrimMap { primDecls :: Map.Map Ident Name
, primTypes :: Map.Map Ident Name
data PrimMap = PrimMap { primDecls :: Map.Map PrimIdent Name
, primTypes :: Map.Map PrimIdent Name
} deriving (Show, Generic, NFData)
lookupPrimDecl, lookupPrimType :: Ident -> PrimMap -> Name
instance Semigroup PrimMap where
x <> y = PrimMap { primDecls = Map.union (primDecls x) (primDecls y)
, primTypes = Map.union (primTypes x) (primTypes y)
}
lookupPrimDecl, lookupPrimType :: PrimIdent -> PrimMap -> Name
-- | It's assumed that we're looking things up that we know already exist, so
-- this will panic if it doesn't find the name.

15
src/Cryptol/ModuleSystem/NamingEnv.hs
View File

@ -87,14 +87,19 @@ merge :: [Name] -> [Name] -> [Name]
merge xs ys | xs == ys = xs
| otherwise = nub (xs ++ ys)
-- | Generate a mapping from 'Ident' to 'Name' for a given naming environment.
-- | Generate a mapping from 'PrimIdent' to 'Name' for a
-- given naming environment.
toPrimMap :: NamingEnv -> PrimMap
toPrimMap NamingEnv { .. } = PrimMap { .. }
where
primDecls = Map.fromList [ (nameIdent n,n) | ns <- Map.elems neExprs
, n <- ns ]
primTypes = Map.fromList [ (nameIdent n,n) | ns <- Map.elems neTypes
, n <- ns ]
entry n = case asPrim n of
Just p -> (p,n)
Nothing -> panic "toPrimMap" [ "Not a declared name?"
, show n
]
primDecls = Map.fromList [ entry n | ns <- Map.elems neExprs, n <- ns ]
primTypes = Map.fromList [ entry n | ns <- Map.elems neTypes, n <- ns ]
-- | Generate a display format based on a naming environment.
toNameDisp :: NamingEnv -> NameDisp

2
src/Cryptol/Parser.y
View File

@ -52,6 +52,7 @@ import Paths_cryptol
%token
NUM { $$@(Located _ (Token (Num {}) _))}
FRAC { $$@(Located _ (Token (Frac {}) _))}
STRLIT { $$@(Located _ (Token (StrLit {}) _))}
CHARLIT { $$@(Located _ (Token (ChrLit {}) _))}
@ -483,6 +484,7 @@ no_sel_aexpr :: { Expr PName }
: qname { at $1 $ EVar (thing $1) }
| NUM { at $1 $ numLit (tokenType (thing $1)) }
| FRAC { at $1 $ fracLit (tokenType (thing $1)) }
| STRLIT { at $1 $ ELit $ ECString $ getStr $1 }
| CHARLIT { at $1 $ ELit $ ECChar $ getChr $1 }
| '_' { at $1 $ EVar $ mkUnqual $ mkIdent "_" }

24
src/Cryptol/Parser/AST.hs
View File

@ -61,7 +61,7 @@ module Cryptol.Parser.AST
-- * Expressions
, Expr(..)
, Literal(..), NumInfo(..)
, Literal(..), NumInfo(..), FracInfo(..)
, Match(..)
, Pattern(..)
, Selector(..)
@ -88,7 +88,8 @@ import Cryptol.Utils.PP
import Data.List(intersperse)
import Data.Bits(shiftR)
import Data.Maybe (catMaybes)
import Numeric(showIntAtBase)
import Data.Ratio(numerator,denominator)
import Numeric(showIntAtBase,showFloat,showHFloat)
import GHC.Generics (Generic)
import Control.DeepSeq
@ -280,9 +281,15 @@ data NumInfo = BinLit Int -- ^ n-digit binary literal
| PolyLit Int -- ^ polynomial literal
deriving (Eq, Show, Generic, NFData)
-- | Information about fractional literals.
data FracInfo = DecFrac
| HexFrac
deriving (Eq,Show,Generic,NFData)
-- | Literals.
data Literal = ECNum Integer NumInfo -- ^ @0x10@ (HexLit 2)
| ECChar Char -- ^ @'a'@
| ECFrac Rational FracInfo -- ^ @1.2e3@
| ECString String -- ^ @\"hello\"@
deriving (Eq, Show, Generic, NFData)
@ -624,8 +631,21 @@ instance PP Literal where
case lit of
ECNum n i -> ppNumLit n i
ECChar c -> text (show c)
ECFrac n i -> ppFracLit n i
ECString s -> text (show s)
ppFracLit :: Rational -> FracInfo -> Doc
ppFracLit x i
| toRational dbl == x =
case i of
DecFrac -> text (showFloat dbl "")
HexFrac -> text (showHFloat dbl "")
| otherwise =
"fraction`" <.> braces
(commaSep (map integer [ numerator x, denominator x ]))
where
dbl = fromRational x :: Double
ppNumLit :: Integer -> NumInfo -> Doc
ppNumLit n info =

9
src/Cryptol/Parser/Lexer.x
View File

@ -48,7 +48,10 @@ $unitick = \x7
@num2 = "0b" (_*[0-1])+
@num8 = "0o" (_*[0-7])+
@num10 = [0-9](_*[0-9])*
@num16 = "0x" (_*[0-9A-Fa-f])+
@digits16 = (_*[0-9A-Fa-f])+
@num16 = "0x" @digits16
@fnum10 = @num10 "." @num10 ([eE] [\+\-]? @num10)?
@fnum16 = @num16 "." @digits16 ([pP] [\+\-]? @num10)?
@strPart = [^\\\"]+
@chrPart = [^\\\']+
@ -127,6 +130,10 @@ $white+ { emit $ White Space }
@num8 { emitS (numToken 8 . Text.drop 2) }
@num10 { emitS (numToken 10 . Text.drop 0) }
@num16 { emitS (numToken 16 . Text.drop 2) }
@fnum10 { emitS (fnumToken 10 . Text.drop 0) }
@fnum16 { emitS (fnumToken 16 . Text.drop 2) }
"_" { emit $ Sym Underscore }
@id { mkIdent }

35
src/Cryptol/Parser/LexerUtils.hs
View File

@ -225,6 +225,40 @@ fromDigit x'
| otherwise = toInteger (fromEnum x - fromEnum '0')
where x = toLower x'
-- XXX: For now we just keep the number as a rational.
-- It might be better to keep the exponent representation,
-- to avoid making huge numbers, and using up all the memory though...
fnumToken :: Int -> Text -> TokenT
fnumToken rad ds = Frac ((wholenNum + fracNum) * (eBase ^^ expNum)) rad
where
radI = fromIntegral rad :: Integer
radR = fromIntegral rad :: Rational
(whole,rest) = T.break (== '.') ds
digits = T.filter (/= '_')
expSym e = if rad == 10 then toLower e == 'e' else toLower e == 'p'
(frac,mbExp) = T.break expSym (T.drop 1 rest)
wholenNum = fromInteger
$ T.foldl' (\x c -> radI * x + fromDigit c) 0
$ digits whole
fracNum = T.foldl' (\x c -> (x + fromInteger (fromDigit c)) / radR) 0
$ T.reverse $ digits frac
expNum = case T.uncons mbExp of
Nothing -> 0 :: Integer
Just (_,es) ->
case T.uncons es of
Just ('+', more) -> read $ T.unpack more
_ -> read $ T.unpack es
eBase = if rad == 10 then 10 else 2 :: Rational
-------------------------------------------------------------------------------
data AlexInput = Inp { alexPos :: !Position
@ -431,6 +465,7 @@ data TokenErr = UnterminatedComment
deriving (Eq, Show, Generic, NFData)
data TokenT = Num !Integer !Int !Int -- ^ value, base, number of digits
| Frac !Rational !Int -- ^ value, base.
| ChrLit !Char -- ^ character literal
| Ident ![T.Text] !T.Text -- ^ (qualified) identifier
| StrLit !String -- ^ string literal

9
src/Cryptol/Parser/ParserUtils.hs
View File

@ -209,6 +209,15 @@ numLit (Num x base digs)
numLit x = panic "[Parser] numLit" ["invalid numeric literal", show x]
fracLit :: TokenT -> Expr PName
fracLit tok =
case tok of
Frac x base
| base == 10 -> ELit $ ECFrac x DecFrac
| base == 16 -> ELit $ ECFrac x HexFrac
_ -> panic "[Parser] fracLit" [ "Invalid fraction", show tok ]
intVal :: Located Token -> ParseM Integer
intVal tok =
case tokenType (thing tok) of

1
src/Cryptol/Parser/Utils.hs
View File

@ -55,4 +55,5 @@ translateExprToNumT expr =
cvtLit (ECNum n _) = return (TNum n)
cvtLit (ECChar c) = return (TChar c)
cvtLit (ECFrac {}) = Nothing
cvtLit (ECString _) = Nothing

4
src/Cryptol/Prelude.hs
View File

@ -15,6 +15,7 @@
module Cryptol.Prelude
( preludeContents
, floatContents
, arrayContents
, cryptolTcContents
) where
@ -27,6 +28,9 @@ import Text.Heredoc (there)
preludeContents :: ByteString
preludeContents = B.pack [there|lib/Cryptol.cry|]
floatContents :: ByteString
floatContents = B.pack [there|lib/Float.cry|]
arrayContents :: ByteString
arrayContents = B.pack [there|lib/Array.cry|]

18
src/Cryptol/REPL/Command.hs
View File

@ -277,9 +277,19 @@ getPPValOpts =
do base <- getKnownUser "base"
ascii <- getKnownUser "ascii"
infLength <- getKnownUser "infLength"
fpBase <- getKnownUser "fp-base"
fpFmtTxt <- getKnownUser "fp-format"
let fpFmt = case parsePPFloatFormat fpFmtTxt of
Just f -> f
Nothing -> panic "getPPValOpts"
[ "Failed to parse fp-format" ]
return E.PPOpts { E.useBase = base
, E.useAscii = ascii
, E.useInfLength = infLength
, E.useFPBase = fpBase
, E.useFPFormat = fpFmt
}
getEvalOpts :: REPL E.EvalOpts
@ -788,8 +798,8 @@ mkSolverResult thing result earg =
Left ts -> mkArgs (map addError ts)
Right tes -> mkArgs tes
eTrue = T.ePrim prims (M.packIdent "True")
eFalse = T.ePrim prims (M.packIdent "False")
eTrue = T.ePrim prims (M.prelPrim "True")
eFalse = T.ePrim prims (M.prelPrim "False")
resultE = if result then eTrue else eFalse
rty = T.TRec $ [(rIdent, T.tBit )] ++ map fst argF
@ -857,8 +867,8 @@ readFileCmd fp = do
do pm <- getPrimMap
let val = byteStringToInteger bs
let len = BS.length bs
let split = T.ePrim pm (M.packIdent "split")
let number = T.ePrim pm (M.packIdent "number")
let split = T.ePrim pm (M.prelPrim "split")
let number = T.ePrim pm (M.prelPrim "number")
let f = T.EProofApp (foldl T.ETApp split [T.tNum len, T.tNum (8::Integer), T.tBit])
let t = T.tWord (T.tNum (toInteger len * 8))
let x = T.EProofApp (T.ETApp (T.ETApp number (T.tNum val)) t)

38
src/Cryptol/REPL/Monad.hs
View File

@ -63,6 +63,7 @@ module Cryptol.REPL.Monad (
, getUserSatNum
, getUserShowProverStats
, getUserProverValidate
, parsePPFloatFormat
-- ** Configurable Output
, getPutStr
@ -97,6 +98,7 @@ import qualified Cryptol.Parser.AST as P
import Cryptol.Symbolic (SatNum(..))
import qualified Cryptol.Symbolic.SBV as SBV (proverNames, checkProverInstallation)
import qualified Cryptol.Symbolic.What4 as W4 (proverNames)
import Cryptol.Eval.Monad(PPFloatFormat(..),PPFloatExp(..))
import Control.Monad (ap,unless,when)
import Control.Monad.Base
@ -797,11 +799,47 @@ userOptions = mkOptionMap
, simpleOpt "show-examples" (EnvBool True) noCheck
"Print the (counter) example after :sat or :prove"
, simpleOpt "fp-base" (EnvNum 16) checkBase
"The base to display floating point numbers at (2, 8, 10, or 16)."
, simpleOpt "fp-format" (EnvString "free") checkPPFloatFormat
$ unlines
[ "Specifies the format to use when showing floating point numbers:"
, " * free show using as many digits as needed"
, " * free+exp like `free` but always show exponent"
, " * .NUM show NUM (>=1) digits after floating point"
, " * NUM show using NUM (>=1) significant digits"
, " * NUM+exp like NUM but always show exponent"
]
, simpleOpt "ignore-safety" (EnvBool False) noCheck
"Ignore safety predicates when performing :sat or :prove checks"
]
parsePPFloatFormat :: String -> Maybe PPFloatFormat
parsePPFloatFormat s =
case s of
"free" -> Just $ FloatFree AutoExponent
"free+exp" -> Just $ FloatFree ForceExponent
'.' : xs -> FloatFrac <$> readMaybe xs
_ | (as,res) <- break (== '+') s
, Just n <- readMaybe as
, Just e <- case res of
"+exp" -> Just ForceExponent
"" -> Just AutoExponent
_ -> Nothing
-> Just (FloatFixed n e)
_ -> Nothing
checkPPFloatFormat :: Checker
checkPPFloatFormat val =
case val of
EnvString s | Just _ <- parsePPFloatFormat s -> noWarns Nothing
_ -> noWarns $ Just "Failed to parse `fp-format`"
-- | Check the value to the `base` option.
checkBase :: Checker
checkBase val = case val of

3
src/Cryptol/Symbolic.hs
View File

@ -120,6 +120,7 @@ data FinType
| FTInteger
| FTIntMod Integer
| FTRational
| FTFloat Integer Integer
| FTSeq Int FinType
| FTTuple [FinType]
| FTRecord (Map.Map Ident FinType)
@ -139,6 +140,7 @@ finType ty =
TVInteger -> Just FTInteger
TVIntMod n -> Just (FTIntMod n)
TVRational -> Just FTRational
TVFloat e p -> Just (FTFloat e p)
TVSeq n t -> FTSeq <$> numType n <*> finType t
TVTuple ts -> FTTuple <$> traverse finType ts
TVRec fields -> FTRecord . Map.fromList <$> traverse (traverseSnd finType) fields
@ -152,6 +154,7 @@ unFinType fty =
FTInteger -> tInteger
FTIntMod n -> tIntMod (tNum n)
FTRational -> tRational
FTFloat e p -> tFloat (tNum e) (tNum p)
FTSeq l ety -> tSeq (tNum l) (unFinType ety)
FTTuple ftys -> tTuple (unFinType <$> ftys)
FTRecord fs -> tRec (Map.toList (fmap unFinType fs))

13
src/Cryptol/Symbolic/SBV.hs
View File

@ -32,6 +32,8 @@ import Data.Maybe (fromMaybe)
import qualified Data.Map as Map
import qualified Control.Exception as X
import LibBF(bfNaN)
import qualified Data.SBV as SBV (sObserve)
import qualified Data.SBV.Internals as SBV (SBV(..))
import qualified Data.SBV.Dynamic as SBV
@ -48,6 +50,7 @@ import qualified Cryptol.Eval.Backend as Eval
import qualified Cryptol.Eval as Eval
import qualified Cryptol.Eval.Concrete as Concrete
import Cryptol.Eval.Concrete (Concrete(..))
import qualified Cryptol.Eval.Concrete.FloatHelpers as Concrete
import qualified Cryptol.Eval.Monad as Eval
import qualified Cryptol.Eval.Value as Eval
@ -429,6 +432,14 @@ parseValue (FTTuple ts) cvs = (Eval.VTuple (map Eval.ready vs), cvs')
parseValue (FTRecord fs) cvs = (Eval.VRecord (Map.fromList (zip ns (map Eval.ready vs))), cvs')
where (ns, ts) = unzip (Map.toList fs)
(vs, cvs') = parseValues ts cvs
parseValue (FTFloat e p) cvs =
(Eval.VFloat Concrete.BF { Concrete.bfValue = bfNaN
, Concrete.bfExpWidth = e
, Concrete.bfPrecWidth = p
}
, cvs
)
-- XXX: NOT IMPLEMENTED
inBoundsIntMod :: Integer -> Eval.SInteger SBV -> Eval.SBit SBV
inBoundsIntMod n x =
@ -447,6 +458,7 @@ forallFinType ty =
let z = SBV.svInteger SBV.KUnbounded 0
tell [SBV.svLessThan z d]
return (Eval.VRational (Eval.SRational n d))
FTFloat {} -> pure (Eval.VFloat ()) -- XXX: NOT IMPLEMENTED
FTIntMod n -> do x <- lift forallSInteger_
tell [inBoundsIntMod n x]
return (Eval.VInteger x)
@ -468,6 +480,7 @@ existsFinType ty =
let z = SBV.svInteger SBV.KUnbounded 0
tell [SBV.svLessThan z d]
return (Eval.VRational (Eval.SRational n d))
FTFloat {} -> pure $ Eval.VFloat () -- XXX: NOT IMPLEMENTED
FTIntMod n -> do x <- lift existsSInteger_
tell [inBoundsIntMod n x]
return (Eval.VInteger x)

22
src/Cryptol/Symbolic/What4.hs
View File

@ -39,10 +39,12 @@ import qualified Cryptol.ModuleSystem.Monad as M
import qualified Cryptol.Eval as Eval
import qualified Cryptol.Eval.Concrete as Concrete
import qualified Cryptol.Eval.Concrete.Float as Concrete
import qualified Cryptol.Eval.Backend as Eval
import qualified Cryptol.Eval.Value as Eval
import Cryptol.Eval.What4
import qualified Cryptol.Eval.What4.SFloat as W4
import Cryptol.Symbolic
import Cryptol.TypeCheck.AST
import Cryptol.Utils.Ident (Ident)
@ -358,6 +360,18 @@ varBlockingPred sym evalFn v =
VarWord (SW.DBV w) ->
do wlit <- W4.groundEval evalFn w
W4.notPred sym =<< W4.bvEq sym w =<< W4.bvLit sym (W4.bvWidth w) wlit
VarFloat (W4.SFloat f)
| fr@(W4.FloatingPointPrecisionRepr e p) <- sym `W4.fpReprOf` f
, let wid = W4.addNat e p
, Just W4.LeqProof <- W4.isPosNat wid ->
do bits <- W4.groundEval evalFn f
bv <- W4.bvLit sym wid bits
constF <- W4.floatFromBinary sym fr bv
-- NOTE: we are using logical equality here
W4.notPred sym =<< W4.floatEq sym f constF
| otherwise -> panic "varBlockingPred" [ "1 >= 2 ???" ]
VarFinSeq _n vs -> computeBlockingPred sym evalFn vs
VarTuple vs -> computeBlockingPred sym evalFn vs
VarRecord fs -> computeBlockingPred sym evalFn (map snd (Map.toList fs))
@ -385,6 +399,7 @@ data VarShape sym
= VarBit (W4.Pred sym)
| VarInteger (W4.SymInteger sym)
| VarRational (W4.SymInteger sym) (W4.SymInteger sym)
| VarFloat (W4.SFloat sym)
| VarWord (SW.SWord sym)
| VarFinSeq Int [VarShape sym]
| VarTuple [VarShape sym]
@ -400,6 +415,7 @@ freshVariable sym ty =
<*> W4.freshBoundedInt sym W4.emptySymbol (Just 1) Nothing
FTIntMod 0 -> panic "freshVariable" ["0 modulus not allowed"]
FTIntMod n -> VarInteger <$> W4.freshBoundedInt sym W4.emptySymbol (Just 0) (Just (n-1))
FTFloat e p -> VarFloat <$> W4.fpFresh sym e p
FTSeq n FTBit -> VarWord <$> SW.freshBV sym W4.emptySymbol (toInteger n)
FTSeq n t -> VarFinSeq n <$> sequence (replicate n (freshVariable sym t))
FTTuple ts -> VarTuple <$> mapM (freshVariable sym) ts
@ -412,6 +428,7 @@ varToSymValue sym var =
VarInteger i -> Eval.VInteger i
VarRational n d -> Eval.VRational (Eval.SRational n d)
VarWord w -> Eval.VWord (SW.bvWidth w) (return (Eval.WordVal w))
VarFloat f -> Eval.VFloat f
VarFinSeq n vs -> Eval.VSeq (toInteger n) (Eval.finiteSeqMap (What4 sym) (map (pure . varToSymValue sym) vs))
VarTuple vs -> Eval.VTuple (map (pure . varToSymValue sym) vs)
VarRecord fs -> Eval.VRecord (fmap (pure . varToSymValue sym) fs)
@ -431,6 +448,11 @@ varToConcreteValue evalFn v =
VarWord (SW.DBV x) ->
do let w = W4.intValue (W4.bvWidth x)
Eval.VWord w . pure . Eval.WordVal . Concrete.mkBv w . BV.asUnsigned <$> W4.groundEval evalFn x
VarFloat fv@(W4.SFloat f) ->
do let (e,p) = W4.fpSize fv
bits <- W4.groundEval evalFn f
pure $ Eval.VFloat $ Concrete.floatFromBits e p $ BV.asUnsigned bits
VarFinSeq n vs ->
do vs' <- mapM (varToConcreteValue evalFn) vs
pure (Eval.VSeq (toInteger n) (Eval.finiteSeqMap Concrete.Concrete (map pure vs')))

29
src/Cryptol/Testing/Random.hs
View File

@ -17,6 +17,7 @@ module Cryptol.Testing.Random where
import qualified Control.Exception as X
import Control.Monad (join, liftM2)
import Data.Ratio ((%))
import Data.Bits ( (.&.), shiftR )
import Data.List (unfoldr, genericTake, genericIndex, genericReplicate)
import Data.Map (Map)
@ -33,7 +34,8 @@ import Cryptol.Eval.Type (TValue(..), tValTy)
import Cryptol.Eval.Value (GenValue(..),SeqMap(..), WordValue(..),
ppValue, defaultPPOpts, finiteSeqMap)
import Cryptol.Eval.Generic (zeroV)
import Cryptol.TypeCheck.AST (Type(..), TCon(..), TC(..), tNoUser, tIsFun)
import Cryptol.TypeCheck.AST (Type(..), TCon(..), TC(..), tNoUser, tIsFun
, tIsNum )
import Cryptol.TypeCheck.SimpType(tRebuild')
import Cryptol.Utils.Ident (Ident)
@ -149,6 +151,9 @@ randomValue sym ty =
(TC TCIntMod, [TCon (TC (TCNum n)) []]) ->
do return (randomIntMod sym n)
(TC TCFloat, [e',p']) | Just e <- tIsNum e', Just p <- tIsNum p' ->
return (randomFloat sym e p)
(TC TCSeq, [TCon (TC TCInf) [], el]) ->
do mk <- randomValue sym el
return (randomStream mk)
@ -269,6 +274,26 @@ randomRecord gens sz g0 =
let (v, g') = gen sz g
in seq v (g', v)
randomFloat ::
(Backend sym, RandomGen g) =>
sym ->
Integer {- ^ Exponent width -} ->
Integer {- ^ Precision width -} ->
Gen g sym
randomFloat sym e p w g =
( VFloat <$> fpLit sym e p (nu % de)
, g3
)
where
-- XXX: we never generat NaN
-- XXX: Not sure that we need such big integers, we should probably
-- use `e` and `p` as a guide.
(n, g1) = if w < 100 then (fromInteger w, g) else randomSize 8 100 g
(nu, g2) = randomR (- 256^n, 256^n) g1
(de, g3) = randomR (1, 256^n) g2
-- Random Values ---------------------------------------------------------------
@ -363,6 +388,7 @@ typeSize ty =
TCon (TC (TCNum n)) _ -> Just n
_ -> Nothing
(TCIntMod, _) -> Nothing
(TCFloat {}, _) -> Nothing
(TCArray, _) -> Nothing
(TCSeq, [sz,el]) -> case tNoUser sz of
TCon (TC (TCNum n)) _ -> (^ n) <$> typeSize el
@ -398,6 +424,7 @@ typeValues ty =
[ TCon (TC (TCNum n)) _ ] | 0 < n ->
[ VInteger x | x <- [ 0 .. n - 1 ] ]
_ -> []
TCFloat {} -> []
TCArray -> []
TCSeq ->
case map tNoUser ts of

11
src/Cryptol/TypeCheck/AST.hs
View File

@ -36,7 +36,7 @@ import Cryptol.ModuleSystem.Exports(ExportSpec(..)
import Cryptol.Parser.AST ( Selector(..),Pragma(..)
, Import(..), ImportSpec(..), ExportType(..)
, Fixity(..))
import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,packIdent)
import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,PrimIdent,prelPrim)
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Type
@ -176,22 +176,21 @@ data DeclDef = DPrim
--------------------------------------------------------------------------------
-- | Construct a primitive, given a map to the unique names of the Cryptol
-- module.
ePrim :: PrimMap -> Ident -> Expr
-- | Construct a primitive, given a map to the unique primitive name.
ePrim :: PrimMap -> PrimIdent -> Expr
ePrim pm n = EVar (lookupPrimDecl n pm)
-- | Make an expression that is @error@ pre-applied to a type and a message.
eError :: PrimMap -> Type -> String -> Expr
eError prims t str =
EApp (ETApp (ETApp (ePrim prims (packIdent "error")) t)
EApp (ETApp (ETApp (ePrim prims (prelPrim "error")) t)
(tNum (length str))) (eString prims str)
eString :: PrimMap -> String -> Expr
eString prims str = EList (map (eChar prims) str) tChar
eChar :: PrimMap -> Char -> Expr
eChar prims c = ETApp (ETApp (ePrim prims (packIdent "number")) (tNum v)) (tWord (tNum w))
eChar prims c = ETApp (ETApp (ePrim prims (prelPrim "number")) (tNum v)) (tWord (tNum w))
where v = fromEnum c
w = 8 :: Int

20
src/Cryptol/TypeCheck/Infer.hs
View File

@ -23,6 +23,9 @@ module Cryptol.TypeCheck.Infer
)
where
import qualified Data.Text as Text
import Cryptol.ModuleSystem.Name (asPrim,lookupPrimDecl,nameLoc)
import Cryptol.Parser.Position
import qualified Cryptol.Parser.AST as P
@ -53,6 +56,7 @@ import Data.Either(partitionEithers)
import Data.Maybe(mapMaybe,isJust, fromMaybe)
import Data.List(partition,find)
import Data.Graph(SCC(..))
import Data.Ratio(numerator,denominator)
import Data.Traversable(forM)
import Control.Monad(zipWithM,unless,foldM)
@ -85,17 +89,17 @@ inferModule m =
-- | Construct a primitive in the parsed AST.
-- | Construct a Prelude primitive in the parsed AST.
mkPrim :: String -> InferM (P.Expr Name)
mkPrim str =
do nm <- mkPrim' str
return (P.EVar nm)
-- | Construct a primitive in the parsed AST.
-- | Construct a Prelude primitive in the parsed AST.
mkPrim' :: String -> InferM Name
mkPrim' str =
do prims <- getPrimMap
return (lookupPrimDecl (packIdent str) prims)
return (lookupPrimDecl (prelPrim (Text.pack str)) prims)
@ -103,6 +107,7 @@ desugarLiteral :: Bool -> P.Literal -> InferM (P.Expr Name)
desugarLiteral fixDec lit =
do l <- curRange
numberPrim <- mkPrim "number"
fracPrim <- mkPrim "fraction"
let named (x,y) = P.NamedInst
P.Named { name = Located l (packIdent x), value = y }
number fs = P.EAppT numberPrim (map named fs)
@ -124,6 +129,13 @@ desugarLiteral fixDec lit =
| otherwise -> [ ]
P.PolyLit _n -> [ ("rep", P.TSeq P.TWild P.TBit) ]
P.ECFrac fr info ->
let arg f = P.PosInst (P.TNum (f fr))
rnd = P.PosInst (P.TNum (case info of
P.DecFrac -> 0
P.HexFrac -> 1))
in P.EAppT fracPrim [ arg numerator, arg denominator, rnd ]
P.ECChar c ->
number [ ("val", P.TNum (toInteger (fromEnum c)))
, ("rep", tBits (8 :: Integer)) ]
@ -325,7 +337,7 @@ checkE expr tGoal =
P.EApp fun@(dropLoc -> P.EApp (dropLoc -> P.EVar c) _)
arg@(dropLoc -> P.ELit l)
| Just n <- asPrim c
, n `elem` map packIdent [ "<<", ">>", "<<<", ">>>" , "@", "!" ] ->
, n `elem` map prelPrim [ "<<", ">>", "<<<", ">>>" , "@", "!" ] ->
do newArg <- do l1 <- desugarLiteral True l
return $ case arg of
P.ELocated _ pos -> P.ELocated l1 pos

20
src/Cryptol/TypeCheck/InferTypes.hs
View File

@ -18,6 +18,8 @@
{-# LANGUAGE ViewPatterns #-}
module Cryptol.TypeCheck.InferTypes where
import Control.Monad(guard)
import Cryptol.Parser.Position
import Cryptol.ModuleSystem.Name (asPrim,nameLoc)
import Cryptol.TypeCheck.AST
@ -25,7 +27,7 @@ import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Subst
import Cryptol.TypeCheck.TypePat
import Cryptol.TypeCheck.SimpType(tMax)
import Cryptol.Utils.Ident (ModName, identText)
import Cryptol.Utils.Ident (ModName, PrimIdent(..), preludeName)
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Misc(anyJust)
@ -302,13 +304,17 @@ instance PP ConstraintSource where
ppUse :: Expr -> Doc
ppUse expr =
case expr of
EVar (asPrim -> Just prim)
| identText prim == "number" -> "literal or demoted expression"
| identText prim == "infFrom" -> "infinite enumeration"
| identText prim == "infFromThen" -> "infinite enumeration (with step)"
| identText prim == "fromTo" -> "finite enumeration"
| identText prim == "fromThenTo" -> "finite enumeration"
EVar (isPrelPrim -> Just prim)
| prim == "number" -> "literal or demoted expression"
| prim == "infFrom" -> "infinite enumeration"
| prim == "infFromThen" -> "infinite enumeration (with step)"
| prim == "fromTo" -> "finite enumeration"
| prim == "fromThenTo" -> "finite enumeration"
_ -> "expression" <+> pp expr
where
isPrelPrim x = do PrimIdent p i <- asPrim x
guard (p == preludeName)
pure i
instance PP (WithNames Goal) where
ppPrec _ (WithNames g names) =

7
src/Cryptol/TypeCheck/SimpleSolver.hs
View File

@ -10,7 +10,9 @@ import Cryptol.TypeCheck.Solver.Class
( solveZeroInst, solveLogicInst, solveRingInst
, solveIntegralInst, solveFieldInst, solveRoundInst
, solveEqInst, solveCmpInst, solveSignedCmpInst
, solveLiteralInst )
, solveLiteralInst
, solveValidFloat, solveFLiteralInst
)
import Cryptol.Utils.Debug(ppTrace)
import Cryptol.TypeCheck.PP
@ -51,8 +53,9 @@ simplifyStep ctxt prop =
TCon (PC PCmp) [ty] -> solveCmpInst ty
TCon (PC PSignedCmp) [ty] -> solveSignedCmpInst ty
TCon (PC PLiteral) [t1,t2] -> solveLiteralInst t1 t2
TCon (PC PFLiteral) [t1,t2,t3,t4] -> solveFLiteralInst t1 t2 t3 t4
TCon (PC PValidFloat) [t1,t2] -> solveValidFloat t1 t2
TCon (PC PFin) [ty] -> cryIsFinType ctxt ty
TCon (PC PEqual) [t1,t2] -> cryIsEqual ctxt t1 t2

96
src/Cryptol/TypeCheck/Solver/Class.hs
View File

@ -20,14 +20,50 @@ module Cryptol.TypeCheck.Solver.Class
, solveCmpInst
, solveSignedCmpInst
, solveLiteralInst
, solveFLiteralInst
, solveValidFloat
) where
import qualified LibBF as FP
import Cryptol.TypeCheck.Type
import Cryptol.TypeCheck.SimpType (tAdd,tWidth)
import Cryptol.TypeCheck.Solver.Types
import Cryptol.TypeCheck.PP
{- | This places constraints on the floating point numbers that
we can work with. This is a bit of an odd check, as it is really
a limitiation of the backend, and not the language itself.
On the other hand, it helps us give sane results if one accidentally
types a polymorphic float at the REPL. Hopefully, most users will
stick to particular FP sizes, so this should be quite transparent.
-}
solveValidFloat :: Type -> Type -> Solved
solveValidFloat e p
| Just _ <- knownSupportedFloat e p = SolvedIf []
| otherwise = Unsolved
-- | Check that the type parameters correspond to a float that
-- we support, and if so make the precision settings for the BigFloat library.
knownSupportedFloat :: Type -> Type -> Maybe FP.BFOpts
knownSupportedFloat et pt
| Just e <- tIsNum et, Just p <- tIsNum pt
, minExp <= e && e <= maxExp && minPrec <= p && p <= maxPrec =
Just (FP.expBits (fromInteger e) <> FP.precBits (fromInteger p)
<> FP.allowSubnormal)
| otherwise = Nothing
where
minExp = max 2 (toInteger FP.expBitsMin)
maxExp = toInteger FP.expBitsMax
minPrec = max 2 (toInteger FP.precBitsMin)
maxPrec = toInteger FP.precBitsMax
-- | Solve a Zero constraint by instance, if possible.
solveZeroInst :: Type -> Solved
solveZeroInst ty = case tNoUser ty of
@ -45,11 +81,13 @@ solveZeroInst ty = case tNoUser ty of
TCon (TC TCIntMod) [n] -> SolvedIf [ pFin n, n >== tOne ]
-- Zero Real
-- Zero Float
-- Zero Rational
TCon (TC TCRational) [] -> SolvedIf []
-- ValidVloat e p => Zero (Float e p)
TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
-- Zero a => Zero [n]a
TCon (TC TCSeq) [_, a] -> SolvedIf [ pZero a ]
@ -117,6 +155,9 @@ solveRingInst ty = case tNoUser ty of
-- Ring Rational
TCon (TC TCRational) [] -> SolvedIf []
-- ValidFloat e p => Ring (Float e p)
TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
-- (Ring a, Ring b) => Ring { x1 : a, x2 : b }
TRec fs -> SolvedIf [ pRing ety | (_,ety) <- fs ]
@ -181,8 +222,10 @@ solveFieldInst ty = case tNoUser ty of
-- Field Rational
TCon (TC TCRational) [] -> SolvedIf []
-- ValidFloat e p => Field (Float e p)
TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
-- Field Real
-- Field Float
-- Field (Z n)
-- TCon (TC TCIntMod) [n] -> SolvedIf [ pFin n, n >== tOne, pPrime n ]
@ -199,8 +242,10 @@ solveRoundInst ty = case tNoUser ty of
-- Round Rational
TCon (TC TCRational) [] -> SolvedIf []
-- ValidFloat e p => Round (Float e p)
TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
-- Round Real
-- Round Float
_ -> Unsolved
@ -222,6 +267,9 @@ solveEqInst ty = case tNoUser ty of
-- Eq Rational
TCon (TC TCRational) [] -> SolvedIf []
-- ValidFloat e p => Eq (Float e p)
TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
-- Eq (Z n)
TCon (TC TCIntMod) [n] -> SolvedIf [ pFin n, n >== tOne ]
@ -261,6 +309,9 @@ solveCmpInst ty = case tNoUser ty of
TCon (TC TCIntMod) [_] ->
Unsolvable $ TCErrorMessage "Values of Z_n type cannot be compared for order"
-- ValidFloat e p => Cmp (Float e p)
TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
-- (fin n, Cmp a) => Cmp [n]a
TCon (TC TCSeq) [n,a] -> SolvedIf [ pFin n, pCmp a ]
@ -318,6 +369,42 @@ solveSignedCmpInst ty = case tNoUser ty of
_ -> Unsolved
-- | Solving fractional literal constraints.
solveFLiteralInst :: Type -> Type -> Type -> Type -> Solved
solveFLiteralInst numT denT rndT ty
| TCon (TError _ e) _ <- tNoUser numT = Unsolvable e
| TCon (TError _ e) _ <- tNoUser denT = Unsolvable e
| tIsInf numT || tIsInf denT || tIsInf rndT =
Unsolvable $ TCErrorMessage $ "Fractions may not use `inf`"
| Just 0 <- tIsNum denT =
Unsolvable $ TCErrorMessage
$ "Fractions may not have 0 as the denominator."
| otherwise =
case tNoUser ty of
TVar {} -> Unsolved
TCon (TError _ e) _ -> Unsolvable e
TCon (TC TCRational) [] -> SolvedIf []
TCon (TC TCFloat) [e,p]
| Just 0 <- tIsNum rndT -> SolvedIf [ pValidFloat e p ]
| Just _ <- tIsNum rndT
, Just opts <- knownSupportedFloat e p
, Just n <- tIsNum numT
, Just d <- tIsNum denT
-> case FP.bfDiv opts (FP.bfFromInteger n) (FP.bfFromInteger d) of
(_, FP.Ok) -> SolvedIf []
_ -> Unsolvable $ TCErrorMessage
$ show n ++ "/" ++ show d ++ " cannot be " ++
"represented in " ++ show (pp ty)
| otherwise -> Unsolved
_ -> Unsolvable $ TCErrorMessage $ show
$ "Type" <+> quotes (pp ty) <+> "does not support fractional literals."
-- | Solve Literal constraints.
solveLiteralInst :: Type -> Type -> Solved
solveLiteralInst val ty
@ -348,5 +435,6 @@ solveLiteralInst val ty
TVar _ -> Unsolved
_ -> Unsolvable $ TCErrorMessage $ show
$ "Type" <+> quotes (pp ty) <+> "does not support literals."
$ "Type" <+> quotes (pp ty) <+> "does not support integer literals."

8
src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs
View File

@ -138,6 +138,14 @@ propInterval varInts prop = catMaybes
return (x, Interval { iLower = Nat 0, iUpper = ub })
, do (e,_) <- pIsValidFloat prop
x <- tIsVar e
pure (x, iAnyFin)
, do (_,p) <- pIsValidFloat prop
x <- tIsVar p
pure (x, iAnyFin)
]

20
src/Cryptol/TypeCheck/TCon.hs
View File

@ -42,12 +42,20 @@ builtInType nm =
case M.nameInfo nm of
M.Declared m _
| m == preludeName -> Map.lookup (M.nameIdent nm) builtInTypes
| m == floatName -> Map.lookup (M.nameIdent nm) builtInFloat
| m == arrayName -> Map.lookup (M.nameIdent nm) builtInArray
_ -> Nothing
where
x ~> y = (packIdent x, y)
-- Built-in types from Float.cry
builtInFloat = Map.fromList
[ "Float" ~> TC TCFloat
, "ValidFloat" ~> PC PValidFloat
]
-- Built-in types from Cryptol.cry
builtInTypes = Map.fromList
[ -- Types
"inf" ~> TC TCInf
@ -71,6 +79,7 @@ builtInType nm =
, "Cmp" ~> PC PCmp
, "SignedCmp" ~> PC PSignedCmp
, "Literal" ~> PC PLiteral
, "FLiteral" ~> PC PFLiteral
-- Type functions
, "+" ~> TF TCAdd
@ -126,6 +135,7 @@ instance HasKind TC where
TCBit -> KType
TCInteger -> KType
TCRational -> KType
TCFloat -> KNum :-> KNum :-> KType
TCIntMod -> KNum :-> KType
TCArray -> KType :-> KType :-> KType
TCSeq -> KNum :-> KType :-> KType
@ -152,6 +162,8 @@ instance HasKind PC where
PCmp -> KType :-> KProp
PSignedCmp -> KType :-> KProp
PLiteral -> KNum :-> KType :-> KProp
PFLiteral -> KNum :-> KNum :-> KNum :-> KType :-> KProp
PValidFloat -> KNum :-> KNum :-> KProp
PAnd -> KProp :-> KProp :-> KProp
PTrue -> KProp
@ -199,6 +211,10 @@ data PC = PEqual -- ^ @_ == _@
| PCmp -- ^ @Cmp _@
| PSignedCmp -- ^ @SignedCmp _@
| PLiteral -- ^ @Literal _ _@
| PFLiteral -- ^ @FLiteral _ _ _@
| PValidFloat -- ^ @ValidFloat _ _@ constraints on supported
-- floating point representaitons
| PAnd -- ^ This is useful when simplifying things in place
| PTrue -- ^ Ditto
@ -210,6 +226,7 @@ data TC = TCNum Integer -- ^ Numbers
| TCInf -- ^ Inf
| TCBit -- ^ Bit
| TCInteger -- ^ Integer
| TCFloat -- ^ Float
| TCIntMod -- ^ @Z _@
| TCRational -- ^ @Rational@
| TCArray -- ^ @Array _ _@
@ -302,6 +319,8 @@ instance PP PC where
PCmp -> text "Cmp"
PSignedCmp -> text "SignedCmp"
PLiteral -> text "Literal"
PFLiteral -> text "FLiteral"
PValidFloat -> text "ValidFloat"
PTrue -> text "True"
PAnd -> text "(&&)"
@ -315,6 +334,7 @@ instance PP TC where
TCIntMod -> text "Z"
TCRational -> text "Rational"
TCArray -> text "Array"
TCFloat -> text "Float"
TCSeq -> text "[]"
TCFun -> text "(->)"
TCTuple 0 -> text "()"

13
src/Cryptol/TypeCheck/Type.hs
View File

@ -495,6 +495,11 @@ pIsWidth ty = case tNoUser ty of
TCon (TF TCWidth) [t1] -> Just t1
_ -> Nothing
pIsValidFloat :: Prop -> Maybe (Type,Type)
pIsValidFloat ty = case tNoUser ty of
TCon (PC PValidFloat) [a,b] -> Just (a,b)
_ -> Nothing
--------------------------------------------------------------------------------
@ -530,6 +535,9 @@ tInteger = TCon (TC TCInteger) []
tRational :: Type
tRational = TCon (TC TCRational) []
tFloat :: Type -> Type -> Type
tFloat e p = TCon (TC TCFloat) [ e, p ]
tIntMod :: Type -> Type
tIntMod n = TCon (TC TCIntMod) [n]
@ -700,6 +708,9 @@ pFin ty =
TCon (TC TCInf) _ -> pError (TCErrorMessage "`inf` is not finite.")
_ -> TCon (PC PFin) [ty]
pValidFloat :: Type -> Type -> Type
pValidFloat e p = TCon (PC PValidFloat) [e,p]
-- | Make a malformed property.
pError :: TCErrorMessage -> Prop
pError msg = TCon (TError KProp msg) []
@ -858,7 +869,7 @@ instance PP (WithNames Type) where
(TCTuple _, fs) -> parens $ fsep $ punctuate comma $ map (go 0) fs
(_, _) -> pp tc <+> fsep (map (go 4) ts)
(_, _) -> pp tc <+> fsep (map (go 5) ts)
TCon (PC pc) ts ->
case (pc,ts) of

28
src/Cryptol/Utils/Ident.hs
View File

@ -16,6 +16,7 @@ module Cryptol.Utils.Ident
, modNameChunks
, packModName
, preludeName
, floatName
, arrayName
, interactiveName
, noModuleName
@ -37,6 +38,11 @@ module Cryptol.Utils.Ident
, identText
, modParamIdent
-- * Identifiers for primitived
, PrimIdent(..)
, prelPrim
, floatPrim
) where
import Control.DeepSeq (NFData)
@ -101,6 +107,9 @@ modInstPref = "`"
preludeName :: ModName
preludeName = packModName ["Cryptol"]
floatName :: ModName
floatName = packModName ["Float"]
arrayName :: ModName
arrayName = packModName ["Array"]
@ -162,4 +171,23 @@ modParamIdent :: Ident -> Ident
modParamIdent (Ident x t) = Ident x (T.append (T.pack "module parameter ") t)
--------------------------------------------------------------------------------
{- | A way to identify primitives: we used to use just 'Ident', but this
isn't good anymore as now we have primitives in multiple modules.
This is used as a key when we need to lookup details about a speicif
primitive. Also, this is intended to mostly be used internally, so
we don't store the fixity flag of the `Ident` -}
data PrimIdent = PrimIdent ModName T.Text
deriving (Eq,Ord,Show,Generic)
-- | A shortcut to make (non-infix) primitives in the prelude.
prelPrim :: T.Text -> PrimIdent
prelPrim = PrimIdent preludeName
floatPrim :: T.Text -> PrimIdent
floatPrim = PrimIdent floatName
instance NFData PrimIdent

16
tests/issues/T146.icry.stdout
View File

@ -3,14 +3,14 @@ Loading module Cryptol
Loading module Main
[error] at T146.cry:1:18--6:10:
The type ?fv`951 is not sufficiently polymorphic.
It cannot depend on quantified variables: fv`935
The type ?fv`955 is not sufficiently polymorphic.
It cannot depend on quantified variables: fv`939
where
?fv`951 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
fv`935 is signature variable 'fv' at T146.cry:11:10--11:12
?fv`955 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
fv`939 is signature variable 'fv' at T146.cry:11:10--11:12
[error] at T146.cry:5:19--5:24:
The type ?fv`953 is not sufficiently polymorphic.
It cannot depend on quantified variables: fv`935
The type ?fv`957 is not sufficiently polymorphic.
It cannot depend on quantified variables: fv`939
where
?fv`953 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
fv`935 is signature variable 'fv' at T146.cry:11:10--11:12
?fv`957 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
fv`939 is signature variable 'fv' at T146.cry:11:10--11:12

2
tests/issues/issue226.icry.stdout
View File

@ -44,6 +44,7 @@ Primitive Types
Bit : *
Cmp : * -> Prop
Eq : * -> Prop
FLiteral : # -> # -> # -> * -> Prop
Field : * -> Prop
fin : # -> Prop
Integer : *
@ -129,6 +130,7 @@ Symbols
floor : {a} (Round a) => a -> Integer
foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
fraction : {m, n, r, a} (FLiteral m n r a) => a
fromInteger : {a} (Ring a) => Integer -> a
fromThenTo :
{first, next, last, a, len} (fin first, fin next, fin last,

4
tests/issues/issue290v2.icry.stdout
View File

@ -4,9 +4,9 @@ Loading module Main
[error] at issue290v2.cry:2:1--2:19:
Unsolved constraints:
• n`932 == 1
• n`936 == 1
arising from
checking a pattern: type of 1st argument of Main::minMax
at issue290v2.cry:2:8--2:11
where
n`932 is signature variable 'n' at issue290v2.cry:1:11--1:12
n`936 is signature variable 'n' at issue290v2.cry:1:11--1:12

4
tests/issues/issue723.icry.stdout
View File

@ -12,9 +12,9 @@ Loading module Main
assuming
• fin k
the following constraints hold:
• k >= n`932
• k >= n`936
arising from
matching types
at issue723.cry:7:17--7:19
where
n`932 is signature variable 'n' at issue723.cry:1:6--1:7
n`936 is signature variable 'n' at issue723.cry:1:6--1:7

2
tests/mono-binds/test04.icry.stdout
View File

@ -18,4 +18,4 @@ Loading module Cryptol
Loading module test04
[error] at test04.cry:1:1--5:14:
Type '()' does not support literals.
Type '()' does not support integer literals.

29
tests/regression/FloatTests.cry Normal file
View File

@ -0,0 +1,29 @@
module FloatTests where
import Float
section : {n} fin n => [n][8] -> [78][8]
section x = "-- " # take`{min 60 n} x # repeat '-'
type Small = Float 3 2
type Medium = Float64
type Large = Float 60 5000
property roundTrip x = fpFromBits (fpToBits x) =.= x
roundTrip2 : {e : #, p : #} (fin e, fin p, ValidFloat e p) => [e + p] -> Bool
property roundTrip2 x = fpToBits num == x \/ num =.= fpNaN
where num = fpFromBits x : Float e p
property eqRefl1 x = x =.= x
property eqRefl2 x = x == x \/ x =.= fpNaN
property eqProp x y = ~(x == y) \/
(x =.= y \/ x =.= fpNaN
\/ y =.= fpNaN
\/ (x =.= 0.0 /\ y =.= -0.0)
\/ (x =.= -0.0 /\ y =.= 0.0)
)
property leqRefl x = x <= x \/ x =.= fpNaN

134
tests/regression/float.icry Normal file
View File

@ -0,0 +1,134 @@
:module FloatTests
:set ascii=on
section "Float Formatting"
:help :set fp-base
:help :set fp-format
:set fp-base=2
10.25 : Medium
:set fp-base=8
10.25 : Medium
:set fp-base=10
10.25 : Medium
1.0 /. 3.0 : Small
0.4 : Small
:set fp-base=16
10.25 : Medium
1.0 /. 3.0 : Small
:set fp-base=16
:set fp-format=free+exp
0x12.34 : Medium
:set fp-format=.1
0x12.34 : Medium
:set fp-format=2
0x12.34 : Medium
:set fp-format=2+exp
0x12.34 : Medium
section "Float Type"
:help Float
zero : Float 0 0 // Too small
zero : Float 80 1000 // Too large
zero : Small
zero : Medium
zero : Large
section "Literals"
:set fp-base=10
1.0 : Medium
1.25 : Medium
1.25e2 : Medium
:set fp-base=16
0x1.25 : Medium
0xFF.FFp3 : Medium
0xFF.FFp-4 : Medium
0xFF.FFe3 : Medium // This is NOT AN EXPONENT
5.0 : Small // Not checked
0x5.0 : Small // Checked
1.2 : Medium
0x0.2 : Small // Subnormal
fpFromBits 1 : Small // Subnormal
section "NaN"
:help fpNaN
fpNaN : Medium
:set base=2
fpToBits (fpNaN : Small)
fpToBits (fpNaN : Medium)
roundTrip (fpNaN : Large)
eqRefl1 (fpNaN : Medium)
eqRefl2 (fpNaN : Medium)
leqRefl (fpNaN : Medium)
section "Arithmetic"
:set fp-base=10
1.0 + 1.0 : Medium
1.0 - 1.0 : Medium
3.0 * 2.0 : Medium
3.0 /. 2.0 : Medium
1.0 /. 0.0 : Medium
-1.0 /. 0.0 : Medium
-0.0 /. 0.0 : Medium
1.0 /. -0.0 : Medium
-1.0 /. -0.0 : Medium
-0.0 /. -0.0 : Medium
2.0 + 3.0 : Small
2.0 + 8.0 : Small
fpAdd rne 2.0 3.0 : Small
fpAdd rne 2.0 8.0 : Small
fpAdd rne (-2.0) (-3.0) : Small
fpAdd rne (-2.0) (-8.0) : Small
fpAdd rna 2.0 3.0 : Small
fpAdd rna 2.0 8.0 : Small
fpAdd rna (-2.0) (-3.0) : Small
fpAdd rna (-2.0) (-8.0) : Small
fpAdd rtp 2.0 3.0 : Small
fpAdd rtp 2.0 8.0 : Small
fpAdd rtp (-2.0) (-3.0) : Small
fpAdd rtp (-2.0) (-8.0) : Small
fpAdd rtn 2.0 3.0 : Small
fpAdd rtn 2.0 8.0 : Small
fpAdd rtn (-2.0) (-3.0) : Small
fpAdd rtn (-2.0) (-8.0) : Small
fpAdd rtz 2.0 3.0 : Small
fpAdd rtz 2.0 8.0 : Small
fpAdd rtz (-2.0) (-3.0) : Small
fpAdd rtz (-2.0) (-8.0) : Small
section "Proofs"
:set prover=w4-z3
:set show-examples = off
:prove \(x : Medium) -> x == 0.0 \/ x =.= fpNaN // False
:set show-examples = on
:prove \(x : Medium) -> x == x // False
:prove \(x : Medium) -> eqRefl1 x
:prove \(x : Medium) -> eqRefl2 x
:prove \(x : Medium) -> roundTrip x
:prove roundTrip2`{3,2}
:prove roundTrip2`{11,53}
:prove \(x : Medium) -> leqRefl x
:prove \(x : Medium) y -> eqProp x y
section "Random Testing"
:check \(x : Medium) -> eqRefl1 x
:check \(x : Medium) -> eqRefl2 x
:check \(x : Medium) -> roundTrip x
:prove roundTrip2`{3,2}
:prove roundTrip2`{11,53}
:check \(x : Medium) -> leqRefl x
:check \(x : Medium) y -> eqProp x y

146
tests/regression/float.icry.stdout Normal file
View File

@ -0,0 +1,146 @@
Loading module Cryptol
Loading module Float
Loading module FloatTests
"-- Float Formatting-----------------------------------------------------------"
fp-base = 16
Default value: 16
The base to display floating point numbers at (2, 8, 10, or 16).
fp-format = free
Default value: free
Specifies the format to use when showing floating point numbers:
* free show using as many digits as needed
* free+exp like `free` but always show exponent
* .NUM show NUM (>=1) digits after floating point
* NUM show using NUM (>=1) significant digits
* NUM+exp like NUM but always show exponent
0b1010.01
0o12.2
10.25
0.4
0.4
0xa.4
0x0.6
0x1.234p4
0x12.3
0x12
0x1.2p4
"-- Float Type-----------------------------------------------------------------"
primitive type Float : # -> # -> *
`Float exponent precision` requires:
• ValidFloat exponent precision
IEEE-754 floating point numbers.
[error] at <interactive>:1:1--1:17:
Unsolved constraints:
• ValidFloat 0 0
arising from
use of partial type function Float
at <interactive>:1:1--1:17
[error] at <interactive>:1:1--1:21:
Unsolved constraints:
• ValidFloat 80 1000
arising from
use of partial type function Float
at <interactive>:1:1--1:21
0x0.0p0
0x0.0p0
0x0.0p0
"-- Literals-------------------------------------------------------------------"
1.0e0
1.2e0
1.2e2
0x1.2p0
0x8.0p8
0x1.0p4
0x1.0p8
0x4.0p0
[error] at <interactive>:1:1--1:20:
5/1 cannot be represented in FloatTests::Small
0x1.3p0
0x2.0p-4
0x2.0p-4
"-- NaN------------------------------------------------------------------------"
fpNaN : {e, p} (ValidFloat e p) => Float e p
Not a number.
NaN
0b01111
0b0111111111111000000000000000000000000000000000000000000000000000
True
True
True
True
"-- Arithmetic-----------------------------------------------------------------"
2.0e0
0.0e0
6.0e0
1.5e0
Inf
-Inf
NaN
-Inf
Inf
NaN
4.0e0
8.0e0
4.0e0
8.0e0
-4.0e0
-8.0e0
6.0e0
1.2e1
-6.0e0
-1.2e1
6.0e0
1.2e1
-4.0e0
-8.0e0
4.0e0
8.0e0
-6.0e0
-1.2e1
4.0e0
8.0e0
-4.0e0
-8.0e0
"-- Proofs---------------------------------------------------------------------"
Counterexample
Counterexample
(\(x : Medium) -> x == x) NaN = False
Q.E.D.
Q.E.D.
Q.E.D.
Q.E.D.
Q.E.D.
Q.E.D.
Q.E.D.
"-- Random Testing-------------------------------------------------------------"
Using random testing.
Testing... Passed 100 tests.
Using random testing.
Testing... Passed 100 tests.
Using random testing.
Testing... Passed 100 tests.
Q.E.D.
Q.E.D.
Using random testing.
Testing... Passed 100 tests.
Using random testing.
Testing... Passed 100 tests.

1
utils/CryHtml.hs
View File

@ -52,6 +52,7 @@ cl :: TokenT -> AttributeValue
cl tok =
case tok of
Num {} -> "number"
Frac {} -> "number"
Ident {} -> "identifier"
KW {} -> "keyword"
Op {} -> "operator"