Skip to content

Commit

Permalink
Allow signaling nans to be presented if we're given the surface reps
Browse files Browse the repository at this point in the history 
To be used by the crackNum executable
  • Loading branch information
@LeventErkok
LeventErkok committed Feb 12, 2024
1 parent 8f87233 commit 4217924
Show file tree
Hide file tree
Showing 6 changed files with 80 additions and 55 deletions.
3 changes: 3 additions & 0 deletions CHANGES.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,9 @@
* Before issuing a get-value, make sure there are no outstanding assert calls.
See: https://github.com/LeventErkok/sbv/issues/682 for details.

* crackNum mode now displays the surface form of NaNs more faithfully, if provided
with the input string. This functionality is used by the crackNum executable.

### Version 10.3, 2024-01-05

* Clean-up GHC extensions required in the cabal file, and changes required to compile cleanly with GHC 9.8 series.
Expand Down
4 changes: 2 additions & 2 deletions Data/SBV.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -503,8 +503,8 @@ import Data.Char (isSpace, isPunctuation)
-- | 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 = s
crack (SBV sv) = show sv
crack (SBV (SVal _ (Left cv))) | Just s <- CN.crackNum cv Nothing = s
crack (SBV sv) = show sv

-- Haddock section documentation
{- $progIntro
Expand Down
43 changes: 22 additions & 21 deletions Data/SBV/Core/Symbolic.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2283,27 +2283,28 @@ data SolverCapabilities = SolverCapabilities {
-- (i.e., SWord and SInt), but also with floats. It is particularly useful with floating-point numbers, as it shows you how they are laid out in
-- memory following the IEEE754 rules.
data SMTConfig = SMTConfig {
verbose :: Bool -- ^ Debug mode
, timing :: Timing -- ^ Print timing information on how long different phases took (construction, solving, etc.)
, printBase :: Int -- ^ Print integral literals in this base (2, 10, and 16 are supported.)
, printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16)
, crackNum :: Bool -- ^ For each numeric value, show it in detail in the model with its bits spliced out. Good for floats.
, satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics.
, allSatMaxModelCount :: Maybe Int -- ^ In a 'Data.SBV.allSat' call, return at most this many models. If nothing, return all.
, allSatPrintAlong :: Bool -- ^ In a 'Data.SBV.allSat' call, print models as they are found.
, allSatTrackUFs :: Bool -- ^ In a 'Data.SBV.allSat' call, should we try to extract values of uninterpreted functions?
, isNonModelVar :: String -> Bool -- ^ When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything)
, validateModel :: Bool -- ^ If set, SBV will attempt to validate the model it gets back from the solver.
, optimizeValidateConstraints :: Bool -- ^ Validate optimization results. NB: Does NOT make sure the model is optimal, just checks they satisfy the constraints.
, transcript :: Maybe FilePath -- ^ If Just, the entire interaction will be recorded as a playable file (for debugging purposes mostly)
, smtLibVersion :: SMTLibVersion -- ^ What version of SMT-lib we use for the tool
, dsatPrecision :: Maybe Double -- ^ Delta-sat precision
, solver :: SMTSolver -- ^ The actual SMT solver.
, extraArgs :: [String] -- ^ Extra command line arguments to pass to the solver.
, roundingMode :: RoundingMode -- ^ Rounding mode to use for floating-point conversions
, solverSetOptions :: [SMTOption] -- ^ Options to set as we start the solver
, ignoreExitCode :: Bool -- ^ If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.
, redirectVerbose :: Maybe FilePath -- ^ Redirect the verbose output to this file if given. If Nothing, stdout is implied.
verbose :: Bool -- ^ Debug mode
, timing :: Timing -- ^ Print timing information on how long different phases took (construction, solving, etc.)
, printBase :: Int -- ^ Print integral literals in this base (2, 10, and 16 are supported.)
, printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16)
, crackNum :: Bool -- ^ For each numeric value, show it in detail in the model with its bits spliced out. Good for floats.
, crackNumSurfaceVals :: [(String, Integer)] -- ^ For crackNum: The surface representation of variables, if available
, satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics.
, allSatMaxModelCount :: Maybe Int -- ^ In a 'Data.SBV.allSat' call, return at most this many models. If nothing, return all.
, allSatPrintAlong :: Bool -- ^ In a 'Data.SBV.allSat' call, print models as they are found.
, allSatTrackUFs :: Bool -- ^ In a 'Data.SBV.allSat' call, should we try to extract values of uninterpreted functions?
, isNonModelVar :: String -> Bool -- ^ When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything)
, validateModel :: Bool -- ^ If set, SBV will attempt to validate the model it gets back from the solver.
, optimizeValidateConstraints :: Bool -- ^ Validate optimization results. NB: Does NOT make sure the model is optimal, just checks they satisfy the constraints.
, transcript :: Maybe FilePath -- ^ If Just, the entire interaction will be recorded as a playable file (for debugging purposes mostly)
, smtLibVersion :: SMTLibVersion -- ^ What version of SMT-lib we use for the tool
, dsatPrecision :: Maybe Double -- ^ Delta-sat precision
, solver :: SMTSolver -- ^ The actual SMT solver.
, extraArgs :: [String] -- ^ Extra command line arguments to pass to the solver.
, roundingMode :: RoundingMode -- ^ Rounding mode to use for floating-point conversions
, solverSetOptions :: [SMTOption] -- ^ Options to set as we start the solver
, ignoreExitCode :: Bool -- ^ If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.
, redirectVerbose :: Maybe FilePath -- ^ Redirect the verbose output to this file if given. If Nothing, stdout is implied.
}

-- | Ignore internal names and those the user told us to
Expand Down
1 change: 1 addition & 0 deletions Data/SBV/Provers/Prover.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,7 @@ mkConfig s smtVersion startOpts = SMTConfig { verbose = Fals
, printBase = 10
, printRealPrec = 16
, crackNum = False
, crackNumSurfaceVals = []
, transcript = Nothing
, solver = s
, smtLibVersion = smtVersion
Expand Down
10 changes: 5 additions & 5 deletions Data/SBV/SMT/SMT.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -560,8 +560,8 @@ showModelDictionary warnEmpty includeEverything cfg allVars
| includeEverything = False
| True = mustIgnoreVar cfg (T.unpack s)

shM (s, RegularCV v) = let vs = shCV cfg v in ((length s, s), (vlength vs, vs))
shM (s, other) = let vs = show other in ((length s, s), (vlength vs, vs))
shM (s, RegularCV v) = let vs = shCV cfg s v in ((length s, s), (vlength vs, vs))
shM (s, other) = let vs = show other in ((length s, s), (vlength vs, vs))

display svs = map line svs
where line ((_, s), (_, v)) = " " ++ right (nameWidth - length s) s ++ " = " ++ left (valWidth - lTrimRight (valPart v)) v
Expand Down Expand Up @@ -633,16 +633,16 @@ showModelUI cfg (nm, (isCurried, SBVType ts, interp))
paren _ x = x

-- | Show a constant value, in the user-specified base
shCV :: SMTConfig -> CV -> String
shCV SMTConfig{printBase, crackNum} cv = cracked (sh printBase cv)
shCV :: SMTConfig -> String -> CV -> String
shCV SMTConfig{printBase, crackNum, crackNumSurfaceVals} nm cv = cracked (sh printBase cv)
where sh 2 = binS
sh 10 = show
sh 16 = hexS
sh n = \w -> show w ++ " -- Ignoring unsupported printBase " ++ show n ++ ", use 2, 10, or 16."

cracked def
| not crackNum = def
| True = case CN.crackNum cv of
| True = case CN.crackNum cv (nm `lookup` crackNumSurfaceVals) of
Nothing -> def
Just cs -> def ++ "\n" ++ cs

Expand Down
74 changes: 47 additions & 27 deletions Data/SBV/Utils/CrackNum.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,31 +35,31 @@ import Numeric
-- | 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 String
crackNum :: a -> Maybe Integer -> Maybe String

-- | CVs are easy to crack
instance CrackNum CV where
crackNum cv = 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 f
KDouble{} -> Just $ let CDouble d = cvVal cv in float d
KFP{} -> Just $ let CFP f = cvVal cv in float f
KBounded sg sz -> Just $ let CInteger i = cvVal cv in int sg sz i
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

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

-- How far off the screen we want displayed? Somewhat experimentally found.
tab :: String
Expand Down Expand Up @@ -227,10 +227,30 @@ instance HasFloatData FP where
| bfIsSubnormal opts f = Subnormal
| True = Normal

-- | Show a float in detail
float :: HasFloatData a => a -> String
float f = intercalate "\n" $ ruler ++ legend : info
where fd@FloatData{prec, eb, sb, bits, fpKind, fpVals} = getFloatData f
-- | 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
where fd@FloatData{prec, eb, sb, bits = bitsAsStored, fpKind, fpVals} = getFloatData f

nanKind = case fpKind of
Zero{} -> False
Infty{} -> False
NaN -> True
Subnormal -> False
Normal -> False

(nanClassifier, bits)
| nanKind, Just i <- mbSurface = (extraClassifier i, i)
| True = ("", bitsAsStored)

-- 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.
extraClassifier :: Integer -> String
extraClassifier i
| sb < 2 = "" -- I don't think this can happen, but just in case
| i `testBit` (sb - 2) = " (Quiet)"
| True = " (Signaling)"

splits = [1, eb, sb]
ruler = map (tab ++) $ mkRuler (eb + sb) splits
Expand Down Expand Up @@ -260,7 +280,7 @@ float f = intercalate "\n" $ ruler ++ legend : info
]
++ [ " Exponent: " ++ show exponentVal ++ " (Subnormal, with fixed exponent value. " ++ esInfo ++ ")" | isSubNormal ]
++ [ " Exponent: " ++ show exponentVal ++ " (" ++ esInfo ++ ")" | not isSubNormal]
++ [ " Classification: " ++ show fpKind]
++ [ " Classification: " ++ show fpKind ++ nanClassifier]
++ (case fpVals of
Left val -> [ " Value: " ++ val]
Right (bval, oval, dval, hval) -> [ " Binary: " ++ bval
Expand Down

0 comments on commit 4217924

Please sign in to comment.