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

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

steakhal marked 4 inline comments as done.
steakhal added a comment.

I made my first google benchmark. Yeey.
Yeah, It's probably flawed :|

F11767721: benchmark.patch <https://reviews.llvm.org/F11767721>
F11767720: benchmark-results-before-patch.txt <https://reviews.llvm.org/F11767720>
F11767722: benchmark-results-after-patch.txt <https://reviews.llvm.org/F11767722>

Since the benchmark library does not support 128 bit wide integers, I used the INT64_MIN-INT64_MAX value range for testing instead.
It should not matter much, though.

To be honest I expected a bit more improvement.
F11767707: benchmark-comparison.png <https://reviews.llvm.org/F11767707>

PS: Can someone tell me why does the `uint128` test-case have only two instances?
That case should not differ from the rest of the cases... I'm confused.



================
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:
> steakhal wrote:
> > 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`.
> > at some point, it was a concrete integer
> 
> ```lang=c++
> __uint128_t x = 2;
> __uint128_t y = 2;
> __uint128_t z = x * y; // 'z' is a nonloc::ConcreteInt '4 U128b'
>                        // that is neither a literal nor hardcoded
>                        // in the analyzer.
> ```
You are right.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D78453