21 Commits

Author SHA1 Message Date
Luke Shingles
fcb3a04858
[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).
2024-08-29 06:09:07 -04:00
Balazs Benics
b3b0d09cce
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)
2024-07-01 16:03:18 +02:00
Balazs Benics
8fc9c03cde
[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.
2024-06-18 14:59:28 +02:00
Balazs Benics
89c26f6c7b
[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
2024-06-18 09:42:29 +02:00
einvbri
f027dd55f3 [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
2023-01-26 12:55:42 -06:00
Fangrui Song
b1df3a2c0b [Support] llvm::Optional => std::optional
https://discourse.llvm.org/t/deprecating-llvm-optional-x-hasvalue-getvalue-getvalueor/63716
2022-12-16 08:49:10 +00:00
Kazu Hirata
1ea9dd3270 [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
2022-12-05 23:50:04 -08:00
Kazu Hirata
6ba4b62af8 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
2022-11-21 19:06:42 -08:00
Balazs Benics
60cb83d549 [analyzer] Fix include typo introduced by e61a1a9 2022-03-11 16:09:25 +01:00
serge-sans-paille
e61a1a9849 Conditional include of missing headers under Z3 2022-03-11 15:52:24 +01:00
serge-sans-paille
efec6b800f Conditional include of Twine.h under Z3 2022-03-11 15:48:06 +01:00
serge-sans-paille
fbbc41f8dd 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
2022-03-11 11:41:32 +01:00
Balazs Benics
815a8100e0 [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
2020-06-30 12:26:50 +02:00
Gabor Marton
5fc05c376a 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: a14c2a3051/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!
2020-05-14 15:46:13 +02:00
Jonas Devlieghere
0eaee545ee [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
2019-08-15 15:54:37 +00:00
Mikhail R. Gadelha
f5f8d27d39 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
2019-03-27 16:54:12 +00:00
Mikhail R. Gadelha
25f9094d89 Moved body of methods dump to .cpp file to fix compilation when modules
are enabled

llvm-svn: 356994
2019-03-26 14:25:12 +00:00
Mikhail R. Gadelha
db695c834f Moved everything SMT-related to LLVM and updated the cmake scripts.
Differential Revision: https://reviews.llvm.org/D54978

llvm-svn: 356929
2019-03-25 17:47:45 +00:00
Mikhail R. Gadelha
3289ccd848 This reverts commit 1440a848a635849b97f7a5cfa0ecc40d37451f5b.
and commit a1853e834c65751f92521f7481b15cf0365e796b.

They broke arm and aarch64

llvm-svn: 353590
2019-02-09 00:46:12 +00:00
Adrian Prantl
e794db8817 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
2019-02-07 21:03:18 +00:00
Mikhail R. Gadelha
eac500f0c3 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
2019-02-07 03:19:45 +00:00