diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,14 @@ * Hackage: * GitHub: -* Latest Hackage released version: 10.4, 2024-02-15 +* Latest Hackage released version: 10.5, 2024-02-20 + +### Version 10.5, 2024-02-20 + + * Export svFloatingPointAsSWord through Data.SBV.Internals + + * crackNum: if verbose, alert the user if surface value of a NaN doesn't match its calculated value + due to the redundancy in NaN representations. ### Version 10.4, 2024-02-15 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -502,9 +502,9 @@ -- | Show a value in detailed (cracked) form, if possible. -- This makes most sense with numbers, and especially floating-point types. -crack :: SBV a -> String -crack (SBV (SVal _ (Left cv))) | Just s <- CN.crackNum cv Nothing = s -crack (SBV sv) = show sv +crack :: Bool -> SBV a -> String +crack verb (SBV (SVal _ (Left cv))) | Just s <- CN.crackNum cv verb Nothing = s +crack _ (SBV sv) = show sv -- Haddock section documentation {- $progIntro diff --git a/Data/SBV/Core/Floating.hs b/Data/SBV/Core/Floating.hs --- a/Data/SBV/Core/Floating.hs +++ b/Data/SBV/Core/Floating.hs @@ -28,6 +28,7 @@ , blastSFloat, blastSDouble, blastSFloatingPoint , sFloatAsComparableSWord32, sDoubleAsComparableSWord64, sFloatingPointAsComparableSWord , sComparableSWord32AsSFloat, sComparableSWord64AsSDouble, sComparableSWordAsSFloatingPoint + , svFloatingPointAsSWord ) where import Data.Bits (testBit) diff --git a/Data/SBV/Internals.hs b/Data/SBV/Internals.hs --- a/Data/SBV/Internals.hs +++ b/Data/SBV/Internals.hs @@ -61,6 +61,9 @@ , sFloatAsComparableSWord32, sDoubleAsComparableSWord64, sFloatingPointAsComparableSWord , sComparableSWord32AsSFloat, sComparableSWord64AsSDouble, sComparableSWordAsSFloatingPoint + -- * Generalized floats + , svFloatingPointAsSWord + -- * lambdas and axioms , lambda, lambdaStr, namedLambda, namedLambdaStr, constraint, constraintStr, Lambda(..), Constraint(..) ) where @@ -74,7 +77,7 @@ import Data.SBV.Core.Model (genLiteral, genFromCV, genMkSymVar, liftQRem, liftDMod) import Data.SBV.Core.Symbolic (IStage(..), QueryContext(..), MonadQuery, addSValOptGoal, registerKind, VarContext(..), svToSV, mkNewState, UICodeKind(..)) -import Data.SBV.Core.Floating ( sFloatAsComparableSWord32, sDoubleAsComparableSWord64, sFloatingPointAsComparableSWord) +import Data.SBV.Core.Floating (sFloatAsComparableSWord32, sDoubleAsComparableSWord64, sFloatingPointAsComparableSWord, svFloatingPointAsSWord) import qualified Data.SBV.Core.Floating as CF (sComparableSWord32AsSFloat, sComparableSWord64AsSDouble, sComparableSWordAsSFloatingPoint) diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -634,7 +634,7 @@ -- | Show a constant value, in the user-specified base shCV :: SMTConfig -> String -> CV -> String -shCV SMTConfig{printBase, crackNum, crackNumSurfaceVals} nm cv = cracked (sh printBase cv) +shCV SMTConfig{printBase, crackNum, verbose, crackNumSurfaceVals} nm cv = cracked (sh printBase cv) where sh 2 = binS sh 10 = show sh 16 = hexS @@ -642,7 +642,7 @@ cracked def | not crackNum = def - | True = case CN.crackNum cv (nm `lookup` crackNumSurfaceVals) of + | True = case CN.crackNum cv verbose (nm `lookup` crackNumSurfaceVals) of Nothing -> def Just cs -> def ++ "\n" ++ cs diff --git a/Data/SBV/Utils/CrackNum.hs b/Data/SBV/Utils/CrackNum.hs --- a/Data/SBV/Utils/CrackNum.hs +++ b/Data/SBV/Utils/CrackNum.hs @@ -35,31 +35,31 @@ -- | A class for cracking things deeper, if we know how. class CrackNum a where -- | Convert an item to possibly bit-level description, if possible. - crackNum :: a -> Maybe Integer -> Maybe String + crackNum :: a -> Bool -> Maybe Integer -> Maybe String -- | CVs are easy to crack instance CrackNum CV where - crackNum cv mbIV = case kindOf cv of - -- Maybe one day we'll have a use for these, currently cracking them - -- any further seems overkill - KBool {} -> Nothing - KUnbounded {} -> Nothing - KReal {} -> Nothing - KUserSort {} -> Nothing - KChar {} -> Nothing - KString {} -> Nothing - KList {} -> Nothing - KSet {} -> Nothing - KTuple {} -> Nothing - KMaybe {} -> Nothing - KEither {} -> Nothing - KRational {} -> Nothing + crackNum cv verbose mbIV = case kindOf cv of + -- Maybe one day we'll have a use for these, currently cracking them + -- any further seems overkill + KBool {} -> Nothing + KUnbounded {} -> Nothing + KReal {} -> Nothing + KUserSort {} -> Nothing + KChar {} -> Nothing + KString {} -> Nothing + KList {} -> Nothing + KSet {} -> Nothing + KTuple {} -> Nothing + KMaybe {} -> Nothing + KEither {} -> Nothing + KRational {} -> Nothing - -- Actual crackables - KFloat{} -> Just $ let CFloat f = cvVal cv in float mbIV f - KDouble{} -> Just $ let CDouble d = cvVal cv in float mbIV d - KFP{} -> Just $ let CFP f = cvVal cv in float mbIV f - KBounded sg sz -> Just $ let CInteger i = cvVal cv in int sg sz i + -- Actual crackables + KFloat{} -> Just $ let CFloat f = cvVal cv in float verbose mbIV f + KDouble{} -> Just $ let CDouble d = cvVal cv in float verbose mbIV d + KFP{} -> Just $ let CFP f = cvVal cv in float verbose mbIV f + KBounded sg sz -> Just $ let CInteger i = cvVal cv in int sg sz i -- How far off the screen we want displayed? Somewhat experimentally found. tab :: String @@ -229,8 +229,8 @@ -- | Show a float in detail. mbSurface is the integer equivalent if this is a NaN; so we -- can represent it faithfully to the original given. Used by crackNum executable. -float :: HasFloatData a => Maybe Integer -> a -> String -float mbSurface f = intercalate "\n" $ ruler ++ legend : info +float :: HasFloatData a => Bool -> Maybe Integer -> a -> String +float verbose mbSurface f = intercalate "\n" $ ruler ++ legend : info where fd@FloatData{prec, eb, sb, bits = bitsAsStored, fpKind, fpVals} = getFloatData f nanKind = case fpKind of @@ -240,9 +240,9 @@ Subnormal -> False Normal -> False - (nanClassifier, bits) - | nanKind, Just i <- mbSurface = (extraClassifier i, i) - | True = ("", bitsAsStored) + (nanClassifier, bits, nanChanged) + | nanKind, Just i <- mbSurface = (extraClassifier i, i, i /= bitsAsStored) + | True = ("", bitsAsStored, False) -- Is this surface representation a signaling NaN or a quiet nan? -- The test is that the tip bit of the significand is high: If so, quiet. If top bit is low, then signaling. @@ -262,6 +262,9 @@ allBits :: [Bool] allBits = [bits `testBit` i | i <- reverse [0 .. eb + sb - 1]] + storedBits :: [Bool] + storedBits = [bitsAsStored `testBit` i | i <- reverse [0 .. eb + sb - 1]] + flatHex = concatMap mkHex (split (split4 (eb + sb)) allBits) sign = bits `testBit` (eb+sb-1) @@ -269,12 +272,15 @@ esInfo = "Stored: " ++ show storedExponent ++ ", Bias: " ++ show bias + chunks bs = unwords [concatMap (\b -> if b then "1" else "0") is | is <- split splits bs] + isSubNormal = case fpKind of Subnormal -> True _ -> False - info = [ " Binary layout: " ++ unwords [concatMap (\b -> if b then "1" else "0") is | is <- split splits allBits] - , " Hex layout: " ++ unwords (split (split4 (length flatHex)) flatHex) + info = [ " Binary layout: " ++ chunks allBits] + ++ [ " Calculated bits: " ++ chunks storedBits ++ " (Surface NaN value differs from calculated)" | verbose && nanChanged] + ++ [ " Hex layout: " ++ unwords (split (split4 (length flatHex)) flatHex) , " Precision: " ++ prec , " Sign: " ++ if sign then "Negative" else "Positive" ] diff --git a/SBVTestSuite/GoldFiles/allSat8.gold b/SBVTestSuite/GoldFiles/allSat8.gold --- a/SBVTestSuite/GoldFiles/allSat8.gold +++ b/SBVTestSuite/GoldFiles/allSat8.gold @@ -61,4 +61,4 @@ *** NB. If this is a use case you'd like SBV to support, please get in touch! CallStack (from HasCallStack): - error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.4-inplace:Data.SBV.Control.Utils + error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.5-inplace:Data.SBV.Control.Utils diff --git a/SBVTestSuite/GoldFiles/nested1.gold b/SBVTestSuite/GoldFiles/nested1.gold --- a/SBVTestSuite/GoldFiles/nested1.gold +++ b/SBVTestSuite/GoldFiles/nested1.gold @@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.4-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.5-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/nested2.gold b/SBVTestSuite/GoldFiles/nested2.gold --- a/SBVTestSuite/GoldFiles/nested2.gold +++ b/SBVTestSuite/GoldFiles/nested2.gold @@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.4-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.5-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/nested3.gold b/SBVTestSuite/GoldFiles/nested3.gold --- a/SBVTestSuite/GoldFiles/nested3.gold +++ b/SBVTestSuite/GoldFiles/nested3.gold @@ -37,4 +37,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.4-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.5-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/nested4.gold b/SBVTestSuite/GoldFiles/nested4.gold --- a/SBVTestSuite/GoldFiles/nested4.gold +++ b/SBVTestSuite/GoldFiles/nested4.gold @@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.4-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.5-inplace:Data.SBV.Core.Symbolic diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv -Version : 10.4 +Version : 10.5 Category : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description : Express properties about Haskell programs and automatically prove them using SMT