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

[Balázs Benics via Phabricator via llvm-commits]

steakhal marked an inline comment as done.
steakhal 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;
----------------
NoQ wrote:
> 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.
@ddcc 
> Aren't __int128_t and __uint128_t types support by Clang?
I assume yes, but probably somewhat rare use-case. That is the reason why I marked that path //unlikely//.
But after this discussion I will probably remove that.

@NoQ 
> 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.
AFAIK this function (`mkBitvector`) would be called only for concrete integers. That integer could have been introduced by the analyzer itself, but at some point, it was a concrete integer. As an example, the `ProgramState::assumeInBound` transforms an assumption using a new concrete integer `MIN`.
I'm not expecting the analyzer to use wider integers than the modeled code itself uses. And as the majority of the analyzed code simply uses 32 bit or 64-bit integers, all the integers should be at most 64 bit wide during an analysis.

That was the reasoning behind marking that condition `LLVM_UNLIKELY`.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D78453