[llvm][Z3][NFC] Improve mkBitvector performance

[steakhal]

Summary

We convert APSInts to Z3 Bitvectors in an inefficient way for most cases.
We should not serialize to std::string just to pass an int64 integer.

For the vast majority of cases, we use at most 64-bit width integers (at least
in the Clang Static Analyzer). We should simply call the Z3_mk_unsigned_int64
and Z3_mk_int64 instead of the Z3_mk_numeral as stated in the Z3 docs.
Which says:

It (Z3_mk_unsigned_int64, etc.) is slightly faster than Z3_mk_numeral since
it is not necessary to parse a string.

If the APSInt is wider than 64 bits, we will use the Z3_mk_numeral with a
SmallString instead of a heap-allocated std::string.

[xazax.hun]

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.

llvm/lib/Support/Z3Solver.cpp

730

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.

[steakhal]

In 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.

llvm/lib/Support/Z3Solver.cpp

730

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.

[ddcc]

llvm/lib/Support/Z3Solver.cpp

730

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.

[xazax.hun]

In D78453#1991384, @steakhal wrote:

In 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.

It is interesting to see if using Z3 (not just the crosscheck) on some projects will show any difference. I would start with this as this might be the easiest to set up. If we do not see any difference on two or three projects we can try doing some microbenchmarks instead. In a microbenchmark, you can just call mkBitvector with random values (a good question is how to choose the distribution of the types).

[NoQ]

llvm/lib/Support/Z3Solver.cpp

730

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.

[steakhal]

llvm/lib/Support/Z3Solver.cpp

730

@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.

[NoQ]

llvm/lib/Support/Z3Solver.cpp

730

at some point, it was a concrete integer

__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.

[steakhal]

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

benchmark.patch2 KBDownload

benchmark-results-before-patch.txt8 KBDownload

benchmark-results-after-patch.txt8 KBDownload

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.

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.

llvm/lib/Support/Z3Solver.cpp

730

You are right.

llvm/lib/Support/Z3Solver.cpp

 //== Z3Solver.cpp -----------------------------------------------*- C++ -*--==//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 
+#include "llvm/ADT/SmallString.h"
 #include "llvm/ADT/Twine.h"
 #include "llvm/Config/config.h"
 #include "llvm/Support/SMTAPI.h"
 #include <set>
 
 using namespace llvm;
 
 #if LLVM_WITH_Z3
public:
   }
 
   SMTExprRef mkBoolean(const bool b) override {
     return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)
                                         : Z3_mk_false(Context.Context)));
   }
 
   SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override {
-    const SMTSortRef Sort = getBitvectorSort(BitWidth);
-    return newExprRef(
-        Z3Expr(Context, Z3_mk_numeral(Context.Context, Int.toString(10).c_str(),
-                                      toZ3Sort(*Sort).Sort)));
+    const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(BitWidth)).Sort;
+
+    // Slow path, when 64 bits are not enough.
+    if (LLVM_UNLIKELY(Int.getBitWidth() > 64u)) {
+      SmallString<40> Buffer;
+      Int.toString(Buffer, 10);
+      return newExprRef(Z3Expr(
+          Context, Z3_mk_numeral(Context.Context, Buffer.c_str(), Z3Sort)));
+    }
+
+    const int64_t BitReprAsSigned = Int.getExtValue();
+    const uint64_t BitReprAsUnsigned =
+        reinterpret_cast<const uint64_t &>(BitReprAsSigned);
+
+    Z3_ast Literal =
+        Int.isSigned()
+            ? Z3_mk_int64(Context.Context, BitReprAsSigned, Z3Sort)
+            : Z3_mk_unsigned_int64(Context.Context, BitReprAsUnsigned, Z3Sort);
+    return newExprRef(Z3Expr(Context, Literal));
   }
 
   SMTExprRef mkFloat(const llvm::APFloat Float) override {
     SMTSortRef Sort =
         getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
 
     llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);
     SMTExprRef Z3Int = mkBitvector(Int, Int.getBitWidth());