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

[Artem Dergachev via Phabricator via llvm-commits]

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


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D78453