Skip to content

Commit 815a810

Browse files
committed
[llvm][Z3][NFC] Improve mkBitvector performance
We convert `APSInt`s 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`. Differential Revision: https://reviews.llvm.org/D78453
1 parent 84ced55 commit 815a810

File tree

1 file changed

+20
-4
lines changed

1 file changed

+20
-4
lines changed

llvm/lib/Support/Z3Solver.cpp

Lines changed: 20 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@
66
//
77
//===----------------------------------------------------------------------===//
88

9+
#include "llvm/ADT/SmallString.h"
910
#include "llvm/ADT/Twine.h"
1011
#include "llvm/Config/config.h"
1112
#include "llvm/Support/SMTAPI.h"
@@ -723,10 +724,25 @@ class Z3Solver : public SMTSolver {
723724
}
724725

725726
SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override {
726-
const SMTSortRef Sort = getBitvectorSort(BitWidth);
727-
return newExprRef(
728-
Z3Expr(Context, Z3_mk_numeral(Context.Context, Int.toString(10).c_str(),
729-
toZ3Sort(*Sort).Sort)));
727+
const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(BitWidth)).Sort;
728+
729+
// Slow path, when 64 bits are not enough.
730+
if (LLVM_UNLIKELY(Int.getBitWidth() > 64u)) {
731+
SmallString<40> Buffer;
732+
Int.toString(Buffer, 10);
733+
return newExprRef(Z3Expr(
734+
Context, Z3_mk_numeral(Context.Context, Buffer.c_str(), Z3Sort)));
735+
}
736+
737+
const int64_t BitReprAsSigned = Int.getExtValue();
738+
const uint64_t BitReprAsUnsigned =
739+
reinterpret_cast<const uint64_t &>(BitReprAsSigned);
740+
741+
Z3_ast Literal =
742+
Int.isSigned()
743+
? Z3_mk_int64(Context.Context, BitReprAsSigned, Z3Sort)
744+
: Z3_mk_unsigned_int64(Context.Context, BitReprAsUnsigned, Z3Sort);
745+
return newExprRef(Z3Expr(Context, Literal));
730746
}
731747

732748
SMTExprRef mkFloat(const llvm::APFloat Float) override {

0 commit comments

Comments
 (0)