leventerkok / cracknum Goto Github PK

Consider:

$ crackNum -f3+4 0b0000011
Satisfiable. Model:
  DECODED = 0.0938 :: FloatingPoint 3 4
                  6 543 210
                  S E3- S3-
   Binary layout: 0 000 011
      Hex layout: 03
       Precision: 3 exponent bits, 3 significand bits
            Sign: Positive
        Exponent: -2 (Subnormal, with fixed exponent value. Stored: 0, Bias: 3)
  Classification: FP_SUBNORMAL
          Binary: 0b1.1p-4
           Octal: 0o6p-6
         Decimal: 0.0938
             Hex: 0x1.8p-4

This is correct; but extremely confusing! Why, because the decimal value as printed is an "equal" value that maps to this representation. But at first look, one would like to see 0.09375.

Note that 0.0938 isn't incorrect; because it maps to that very same value representationally. And it's probably picked by the underlying FPLib library because it's "shorter."

But this is clearly confusing. I wonder if we can represent the info in a better way to avoid such pitfalls.

cracknum nicely prints floats in hex format: 0xfp-4

It might be nice to also allow for this format to be used in conversion. (i.e., in decoding, not just encoding.)

Thanks for creating the most awesome number converter on the planet. It has helped immensely as I need to convert a lot of binary/hex-/decimal values to their respective hex layout. It is faster then Python and gives all sorts of interesting details as output.

And therein lies the rub: would crackNum be faster when less verbose, skipping other calculations ? Asking because I am converting more and more data and at some piont it might take weeks to convert the data on a dedicated rig. All I need is the hexdecimal layout.

Might not be a big win but I thought it might not hurt to ask. Project's Git

Due to: LeventErkok/sbv#414

Probably move the required functionality directly into 'CrackNum' itself and expose it via the library portion; and then SBV can just use it from here.

Until two weeks ago I could build crackNum straight from github without fail. When building today I was greeted with the following error:

code that is executed is
RUN cd crackNum && stack path --local-bin && stack setup && stack init && stack build && stack install && stack clean && rm -R /crackNum here

It mentiones the returned value is a value, not a string. Any idea here ?

On the stackage build server there was a build failure on the crackNum executable (due to specifying -Werror in Main.hs):

Building executable 'crackNum' for crackNum-3.4..
[1 of 3] Compiling CrackNum.TestSuite
[2 of 3] Compiling Paths_crackNum
[3 of 3] Compiling Main

/Users/dan/scratch/crackNum-3.4/src/CrackNum/Main.hs:340:78: error: [GHC-63394] [-Wx-partial, -Werror=x-partial]
    In the use of ‘tail’
    (imported from Prelude, but defined in GHC.List):
    "This is a partial function, it throws an error on empty lists. Replace it with drop 1, or use pattern matching or Data.List.uncons instead. Consider refactoring to use Data.List.NonEmpty."
    |
340 |                 trim xs | "[" `isPrefixOf` xs && "]" `isSuffixOf` xs = init (tail xs)
    |                                                                              ^^^^

I was able to reproduce this locally like so:

stack unpack crackNum-3.4 && cd crackNum-3.4
edit stack.yaml # add the following stack.yaml
stack build --test --bench --no-run-benchmarks --fast

# stack.yaml
resolver: nightly-2024-01-11
extra-deps:
- sbv-10.3@sha256:d869a49fd8e6303a81f7f704bb8669deff20d000e4644f93ddc64749d4bc0f9a,23712

In light of new SBV support for all floating-point types; I think it's time to rewrite crackNum so it handles all those cases, simply by piggy-backing on what SBV does.

Having SBV as a dependency is rather large for crackNum, but I think we can afford it.

FYI, I will work around this as 20.04 is about to be deprecated