[PATCH] D78453: [llvm][Z3][NFC] Improve mkBitvector performance

Artem Dergachev via Phabricator via llvm-commits llvm-commits at lists.llvm.org
Mon Apr 20 03:11:21 PDT 2020


NoQ added inline comments.


================
Comment at: llvm/lib/Support/Z3Solver.cpp:730
+    // Slow path, when 64 bits are not enough.
+    if (LLVM_UNLIKELY(Int.getBitWidth() > 64u)) {
+      SmallString<40> Buffer;
----------------
ddcc wrote:
> steakhal wrote:
> > xazax.hun wrote:
> > > I am not sure if the unlikely is justified. The likelihood might depend on the analyzed code and it is possible to write code where this is the frequent case. 
> > The analyzer works on code, but in code, we can not have larger integer literals than `long long` which is (probably) not wider than 64 bits.
> > I think the rest of the LLVM users are the concern here.
> > Should I remove then?
> > 
> > Though, we could further improve the performance, since if the literal's value is small enough to fit into 64-bits, the bitwidth of the storage doesn't matter much. Though, I considered this sort of a hack. In this way, the code is more readable IMO.
> Aren't `__int128_t` and `__uint128_t` types support by Clang? I'm not sure how those integer literals would be generated though, unless an intermediate pass merges together two 64-bit literals.
We don't need those to be literals in the code. They can be computed at run-time and the analyzer will simply follow the computations.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D78453/new/

https://reviews.llvm.org/D78453





More information about the llvm-commits mailing list