[all-commits] [llvm/llvm-project] 815a81: [llvm][Z3][NFC] Improve mkBitvector performance

[Balazs Benics via All-commits]

  Branch: refs/heads/master
  Home:   https://github.com/llvm/llvm-project
  Commit: 815a8100e02966043a41ae6b366f23feb470e736
      https://github.com/llvm/llvm-project/commit/815a8100e02966043a41ae6b366f23feb470e736
  Author: Balazs Benics <benicsbalazs at gmail.com>
  Date:   2020-06-30 (Tue, 30 Jun 2020)

  Changed paths:
    M llvm/lib/Support/Z3Solver.cpp

  Log Message:
  -----------
  [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