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

Balázs Benics via Phabricator via llvm-commits llvm-commits at lists.llvm.org
Sun Apr 19 14:25:47 PDT 2020


steakhal marked an inline comment as done.
steakhal added a comment.

In D78453#1991294 <https://reviews.llvm.org/D78453#1991294>, @xazax.hun wrote:

> Mostly looks good to me. I do believe that this is an optimization but it would be nice to have a small benchmark :) In case it is too much work, I do not insist though.


I'm curious too.

Though I'm not sure how to accomplish that. AFAIK you measured such.
How should I measure this?
Should I use eg. the Clang SA and analyze different projects? (which, how many, etc)
Wouldn't have this method introduce too much noise?
Or should I measure this by a microbenchmark?

I'm really in favor of the microbenchmark approach.



================
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;
----------------
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.


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