From 815a8100e02966043a41ae6b366f23feb470e736 Mon Sep 17 00:00:00 2001 From: Balazs Benics Date: Tue, 30 Jun 2020 12:26:50 +0200 Subject: [PATCH] [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 --- llvm/lib/Support/Z3Solver.cpp | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/llvm/lib/Support/Z3Solver.cpp b/llvm/lib/Support/Z3Solver.cpp index 3e0cb49..9485536 100644 --- a/llvm/lib/Support/Z3Solver.cpp +++ b/llvm/lib/Support/Z3Solver.cpp @@ -6,6 +6,7 @@ // //===----------------------------------------------------------------------===// +#include "llvm/ADT/SmallString.h" #include "llvm/ADT/Twine.h" #include "llvm/Config/config.h" #include "llvm/Support/SMTAPI.h" @@ -723,10 +724,25 @@ public: } 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(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 { -- 2.7.4