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

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

steakhal created this revision.
steakhal added reviewers: mikhail.ramalho, ddcc, NoQ, Szelethus, baloghadamsoftware.
Herald added subscribers: llvm-commits, martong, Charusso, rnkovacs, hiraditya.
Herald added a project: LLVM.

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


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D78453

Files:
  llvm/lib/Support/Z3Solver.cpp


Index: llvm/lib/Support/Z3Solver.cpp
===================================================================
--- llvm/lib/Support/Z3Solver.cpp
+++ 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 @@
   }
 
   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 {


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D78453.258597.patch
Type: text/x-patch
Size: 1574 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20200419/7d057378/attachment.bin>