Evaluate Profile-Guided Optimization (PGO)

[zamazan4ik]

Hi!

Recently I checked Profile-Guided Optimization (PGO) improvements on multiple projects. The results are here. LLVM-related results are here.

Since PGO showed measurable improvements in compiler-like loads (Clang, Clangd, clang-format, GCC, Rustc, etc.) I think it could be useful to check PGO on IKOS as well.

We need to perform PGO benchmarks on IKOS. And if it shows improvements - add a note about possible improvements in IKOS performance with PGO. Providing an easier way (e.g. a build option) to build scripts with PGO can be useful for the end-users too. Probably trying LLVM BOLT would be a good thing too (but after PGO).

[arthaud]

cf facebook/mariana-trench#137

[ivanperez-keera]

This sounds like a great idea. However, I don't really know what the action item would be on this. I'm moving it to a discussion for now; we can open issues when there's a clear plan of how to complete this.