1
0
mirror of https://github.com/RPCS3/llvm-mirror.git synced 2024-10-20 11:33:24 +02:00
Commit Graph

8 Commits

Author SHA1 Message Date
Gabor Marton
3b5aa54948 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
2c693415b7 [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
01753e59a7 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
e655727920 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
81dc3f1c2d 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
7db7f7f32f 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
10b7106901 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
dd981b7599 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