OSDN Git Service

[llvm][Z3][NFC] Improve mkBitvector performance
authorBalazs Benics <benicsbalazs@gmail.com>
Tue, 30 Jun 2020 10:26:50 +0000 (12:26 +0200)
committerBalazs Benics <benicsbalazs@gmail.com>
Tue, 30 Jun 2020 10:26:50 +0000 (12:26 +0200)
commit815a8100e02966043a41ae6b366f23feb470e736
treea2d8c460e2917f42a920c3d09035cc13a6918bb4
parent84ced55d9b7bade7c9db39f3bcebc6af333dc325
[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