radareorg / radeco

radare2-based decompiler and symbol executor
371 stars 52 forks source link

Use Chalk engine for solving constraints and as a decision engine #182

Open XVilka opened 6 years ago

XVilka commented 6 years ago

https://github.com/rust-lang-nursery/chalk - they are going to use it in Rust compiler itself. Should suit decompiler too.

XVilka commented 5 years ago

Note there is an interesting idea of using Prolog-like (Datalog) query interface to extract knowledge from the program: https://github.com/maurer/thesis/ The named the engine Holmes: "Holmes is a dialect of Datalog, tailored with extensions for the specific use case of analyzing compiled code."

See this Holmes implementation here https://github.com/maurer/mycroft Its license is MIT, so can be reused without any problem.

XVilka commented 5 years ago

See also (Pharos) https://edmcman.github.io/pres/ccs18.pdf + https://edmcman.github.io/papers/ccs18.pdf

XVilka commented 5 years ago

See also https://github.com/GrammaTech/ddisasm/tree/master/src/datalog