[analyzer] Add missing include <unordered_map> to llvm/lib/Support/Z3Solver.cpp (#106410)

Resolves #106361. Adding #include <unordered_map> to
llvm/lib/Support/Z3Solver.cpp fixes compilation errors

[analyzer] Add missing include <unordered_map> to llvm/lib/Support/Z3Solver.cpp (#106410)

Resolves #106361. Adding #include <unordered_map> to
llvm/lib/Support/Z3Solver.cpp fixes compilation errors for homebrew
build on macOS with Xcode 14.
https://github.com/Homebrew/homebrew-core/actions/runs/10604291631/job/29390993615?pr=181351
shows that this is resolved when the include is patched in (Linux CI
failure is due to unrelated timeout).

show more ...

Reland "[analyzer][NFC] Reorganize Z3 report refutation" (#97265)

This is exactly as originally landed in #95128,
but now the minimal Z3 version was increased to meet this change in #96682.

http

Reland "[analyzer][NFC] Reorganize Z3 report refutation" (#97265)

This is exactly as originally landed in #95128,
but now the minimal Z3 version was increased to meet this change in #96682.

https://discourse.llvm.org/t/bump-minimal-z3-requirements-from-4-7-1-to-4-8-9/79664/4

---

This change keeps existing behavior, namely that if we hit a Z3 timeout
we will accept the report as "satisfiable".

This prepares for the commit "Harden safeguards for Z3 query times".
https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520

(cherry picked from commit 89c26f6c7b0a6dfa257ec090fcf5b6e6e0c89aab)

show more ...

[analyzer] Revert Z3 changes (#95916)

Requested in:
https://github.com/llvm/llvm-project/pull/95128#issuecomment-2176008007

Revert "[analyzer] Harden safeguards for Z3 query times"
Revert "[ana

[analyzer] Revert Z3 changes (#95916)

Requested in:
https://github.com/llvm/llvm-project/pull/95128#issuecomment-2176008007

Revert "[analyzer] Harden safeguards for Z3 query times"
Revert "[analyzer][NFC] Reorganize Z3 report refutation"

This reverts commit eacc3b3504be061f7334410dd0eb599688ba103a.
This reverts commit 89c26f6c7b0a6dfa257ec090fcf5b6e6e0c89aab.

show more ...

[analyzer][NFC] Reorganize Z3 report refutation

This change keeps existing behavior, namely that if we hit a Z3 timeout
we will accept the report as "satisfiable".

This prepares for the commit "Har

[analyzer][NFC] Reorganize Z3 report refutation

This change keeps existing behavior, namely that if we hit a Z3 timeout
we will accept the report as "satisfiable".

This prepares for the commit "Harden safeguards for Z3 query times".
https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520

Reviewers: NagyDonat, haoNoQ, Xazax-hun, mikhailramalho, Szelethus

Reviewed By: NagyDonat

Pull Request: https://github.com/llvm/llvm-project/pull/95128

show more ...

[analyzer] Fix crash exposed by D140059

Change https://reviews.llvm.org/D140059 exposed the following crash in
Z3Solver, where bit widths were not checked consistently with that
change. This change

[analyzer] Fix crash exposed by D140059

Change https://reviews.llvm.org/D140059 exposed the following crash in
Z3Solver, where bit widths were not checked consistently with that
change. This change makes the check consistent, and fixes the crash.

```
clang: <root>/llvm/include/llvm/ADT/APSInt.h:99:
int64_t llvm::APSInt::getExtValue() const: Assertion
`isRepresentableByInt64() && "Too many bits for int64_t"' failed.
...
Stack dump:
0. Program arguments: clang -cc1 -internal-isystem <root>/lib/clang/16/include
-nostdsysteminc -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection
-analyzer-config crosscheck-with-z3=true -verify reproducer.c

#0 0x00000000045b3476 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int)
<root>/llvm/lib/Support/Unix/Signals.inc:567:22
#1 0x00000000045b3862 PrintStackTraceSignalHandler(void*)
<root>/llvm/lib/Support/Unix/Signals.inc:641:1
#2 0x00000000045b14a5 llvm::sys::RunSignalHandlers()
<root>/llvm/lib/Support/Signals.cpp:104:20
#3 0x00000000045b2eb4 SignalHandler(int)
<root>/llvm/lib/Support/Unix/Signals.inc:412:1
...
#9 0x0000000004be2eb3 llvm::APSInt::getExtValue() const
<root>/llvm/include/llvm/ADT/APSInt.h:99:5
<root>/llvm/lib/Support/Z3Solver.cpp:740:53
clang::ASTContext&, clang::ento::SymExpr const*, llvm::APSInt const&, llvm::APSInt const&, bool)
<root>/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:552:61
```

Reviewed By: steakhal

Differential Revision: https://reviews.llvm.org/D142627

show more ...

[Support] llvm::Optional => std::optional

https://discourse.llvm.org/t/deprecating-llvm-optional-x-hasvalue-getvalue-getvalueor/63716

[llvm] Use std::nullopt instead of llvm::None (NFC)

This is part of an effort to migrate from llvm::Optional to
std::optional:

https://discourse.llvm.org/t/deprecating-llvm-optional-x-hasvalue-getv

[llvm] Use std::nullopt instead of llvm::None (NFC)

This is part of an effort to migrate from llvm::Optional to
std::optional:

https://discourse.llvm.org/t/deprecating-llvm-optional-x-hasvalue-getvalue-getvalueor/63716

show more ...

Return None instead of Optional<T>() (NFC)

This patch replaces:

return Optional<T>();

with:

return None;

to make the migration from llvm::Optional to std::optional easier.
Specifically, I ca

Return None instead of Optional<T>() (NFC)

This patch replaces:

return Optional<T>();

with:

return None;

to make the migration from llvm::Optional to std::optional easier.
Specifically, I can deprecate None (in my source tree, that is) to
identify all the instances of None that should be replaced with
std::nullopt.

Note that "return None" far outnumbers "return Optional<T>();". There
are more than 2000 instances of "return None" in our source tree.

All of the instances in this patch come from functions that return
Optional<T> except Archive::findSym and ASTNodeImporter::import, where
we return Expected<Optional<T>>. Note that we can construct
Expected<Optional<T>> from any parameter convertible to Optional<T>,
which None certainly is.

This is part of an effort to migrate from llvm::Optional to
std::optional:

https://discourse.llvm.org/t/deprecating-llvm-optional-x-hasvalue-getvalue-getvalueor/63716

Differential Revision: https://reviews.llvm.org/D138464

show more ...

[analyzer] Fix include typo introduced by e61a1a9

Conditional include of missing headers under Z3

Conditional include of Twine.h under Z3

Cleanup include: TableGen

This also includes a few cleanup from Support.

Discourse thread: https://discourse.llvm.org/t/include-what-you-use-include-cleanup
Differential Revision: https://reviews.l

Cleanup include: TableGen

This also includes a few cleanup from Support.

Discourse thread: https://discourse.llvm.org/t/include-what-you-use-include-cleanup
Differential Revision: https://reviews.llvm.org/D121331

show more ...

[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

[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

show more ...

Fix Z3 function calls regarding arithmetic operations

Summary:
The order of Z3_mk_fpa_mul, Z3_mk_fpa_div, Z3_mk_fpa_add and Z3_mk_fpa_sub functions' arguments is: context, rounding_mode, ast1, ast2.

Fix Z3 function calls regarding arithmetic operations

Summary:
The order of Z3_mk_fpa_mul, Z3_mk_fpa_div, Z3_mk_fpa_add and Z3_mk_fpa_sub functions' arguments is: context, rounding_mode, ast1, ast2.
See for example: https://github.com/Z3Prover/z3/blob/a14c2a30516003cd1a60f8b7deca029033d11c78/src/api/api_fpa.cpp#L433

At function calls from LLVM the argument order was different: rounding_mode was passed as last argument.

Unfortunately these Z3_ast and other function parameter types are technically like void* which are reinterpret_cast-ed to a specific class type. So there was no type error, but the assertions fail in runtime if something goes wrong. Such a crash happened during Z3 refutation while using StaticAnalyzer.

Reviewers: Szelethus, xazax.hun, baloghadamsoftware, steakhal, martong, mikhail.ramalho

Reviewed By: martong

Subscribers: hiraditya, rnkovacs, mikhail.ramalho, martong, llvm-commits

Tags: #llvm

Differential Revision: https://reviews.llvm.org/D79883

Patch by Tibor Brunner!

show more ...

[llvm] Migrate llvm::make_unique to std::make_unique

Now that we've moved to C++14, we no longer need the llvm::make_unique
implementation from STLExtras.h. This patch is a mechanical replacement
of

[llvm] Migrate llvm::make_unique to std::make_unique

Now that we've moved to C++14, we no longer need the llvm::make_unique
implementation from STLExtras.h. This patch is a mechanical replacement
of (hopefully) all the llvm::make_unique instances across the monorepo.

llvm-svn: 369013

show more ...

New methods to check for under-/overflow in the SMT API

Summary: Added methods to check for under-/overflow in additions, subtractions, signed divisions/modulus, negations, and multiplications.

Rev

New methods to check for under-/overflow in the SMT API

Summary: Added methods to check for under-/overflow in additions, subtractions, signed divisions/modulus, negations, and multiplications.

Reviewers: ddcc, gou4shi1

Reviewed By: ddcc, gou4shi1

Subscribers: hiraditya, llvm-commits

Tags: #llvm

Differential Revision: https://reviews.llvm.org/D59796

llvm-svn: 357088

show more ...

Moved body of methods dump to .cpp file to fix compilation when modules
are enabled

llvm-svn: 356994

Moved everything SMT-related to LLVM and updated the cmake scripts.

Differential Revision: https://reviews.llvm.org/D54978

llvm-svn: 356929

Move SMTSolver dump() methods out-of-line.

This broke modularized non-local-submodule-visibility builds because
the function bodies pulled in extra dependencies.

llvm-svn: 353465

Move the SMT API to LLVM

Moved everything SMT-related to LLVM and updated the cmake scripts.

Differential Revision: https://reviews.llvm.org/D54978

llvm-svn: 353373