BinaryAnalysisPlatform / bap

Binary Analysis Platform
MIT License
2.07k stars 273 forks source link

Bugs found in BAP float operations #1577

Open Heersin opened 1 year ago

Heersin commented 1 year ago

This issue records some bugs found in bap fbasic, plan to fix them in a pull request.

  1. A mismatched description in http://binaryanalysisplatform.github.io/bap/api/master/bap-core-theory/Bap_core_theory/Theory/module-type-Float/index.html#val-fsucc. looks like rounding is no more need in these two operations.

  2. Bug about the semantics of fsucc and fpred. In short, for any float number x, the relationship fpred(x) < x < fsucc(x) should hold. while in the following Primus Lisp script, when x is negative it breaks the relationship:

    (defun pos ()
    (set ST0 (cast-sfloat :rne 64 1)))
    
    (defun psucc ()
    (set ST1 (+1 (cast-sfloat :rne 64 1))))
    
    (defun ppred ()
    (set ST2 (-1 (cast-sfloat :rne 64 1))))
    
    (defun neg ()
    (set ST0 (cast-sfloat :rne 64 -1)))
    
    (defun nsucc ()
    (set ST1 (+1 (cast-sfloat :rne 64 -1))))
    
    (defun npred ()
    (set ST2 (-1 (cast-sfloat :rne 64 -1))))

    output:

    pos:
    "{
     ST0 := 0x3FF0000000000000
    }"
    psucc:
    "{
     ST1 := 0x3FF0000000000001
    }"
    ppred:
    "{
     ST2 := 0x3FEFFFFFFFFFFFFF
    }"
    neg:
    "{
     ST0 := 0xBFF0000000000000
    }"
    nsucc:
    "{
     ST1 := 0xBFF0000000000001
    }"
    npred:
    "{
     ST2 := 0xBFEFFFFFFFFFFFFF
    }"

    it shows ppred < pos < psucc which is correct, and npred > neg > nsucc which is confused.

  3. Bug about the semantic of cast_float. cast_float interprets the given bitvector as an unsigned one, so cast_float x always return a non-negative float. cast-float -1234567 == cast-float 18446744073708317049 and finally got a float 0x43EFFFFFFFFFFDA5. But cast_float -1234567 and cast_sfloat -1234567 have the following output:

    ❯ bap show e{0,1} --primus-lisp-load=demo -tx86_64 -obap:bil                              ─╯
    e0:
    "{
     RAX := 0xC132D68700000000
    }"
    e1:
    "{
     RAX := 0xC132D68700000000
    }"
XVilka commented 1 year ago

@ivg could you please take a look? It's very important for trace-checking binaries with floating point instructions which we are working on right now.