BinaryAnalysisPlatform / bap

Binary Analysis Platform
MIT License
2.04k stars 272 forks source link

String Theory (SMT-like) support #1590

Open XVilka opened 1 year ago

XVilka commented 1 year ago

Just like SMT it would allow better reasoning about strings: https://microsoft.github.io/z3guide/docs/theories/Strings/

The tricky thing is to decide about encoding, Unicode, handling "wide" characters with zeroes inside, handling grapheme clusters, etc.

ivg commented 1 year ago

The Strings Theory sounds like a good addition, though I am not sure about including it in the Core theory. That's kind of the whole idea of Core that it only includes Core computations (and it is already a little bit overextended to my taste, e.g., compare it with the SMT's Core theory, which is much thinner).

So, maybe the issue should be just "Develop the String Theory"?