Bugs found in BAP float operations

[Heersin]

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]

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