Add Float and Trans theories into RZIL - Githubissues

rizinorg / rizin

UNIX-like reverse engineering framework and command-line toolset.

https://rizin.re

GNU Lesser General Public License v3.0

2.71k stars 363 forks source link

Add Float and Trans theories into RZIL #1461

Open XVilka opened 3 years ago

XVilka commented 3 years ago

Currently only supported theories are:

Bool
Bitvector
Mem (Array)
Effect

The biggest missing chunk is the Float theory

[x] Implement IEE754 types and helper APIs in RzUtil
[x] Implement Fbasic operations https://github.com/rizinorg/rizin/pull/3184
[x] Cover these by unit tests
[ ] Add rounding modes (Rmode) operations
[ ] Add Trans (transcendental) operations

See:

Implementation is at https://github.com/BinaryAnalysisPlatform/bap/blob/master/lib/bap_core_theory/bap_core_theory_definition.ml

Note, I think that Trans theory should be separate from the Float in the code.

http://binaryanalysisplatform.github.io/bap/api/odoc/bap-core-theory/Bap_core_theory/Theory/module-type-Core/index.html

XVilka commented 1 year ago

Better description of the rounding modes is here: http://binaryanalysisplatform.github.io/bap/api/master/bap-core-theory/Bap_core_theory/Theory/module-type-Float/index.html#rounding-modes

@brightprogrammer @Heersin @imbillow