Commit Graph

9 Commits

Author SHA1 Message Date
Jonas Devlieghere 2b3d49b610 [Clang] 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.

Differential revision: https://reviews.llvm.org/D66259

llvm-svn: 368942
2019-08-14 23:04:18 +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
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
Mikhail R. Gadelha b0670d349c [analyzer] Templatefy SMTConstraintManager so more generic code can be moved from solver specific implementations. NFC.
Summary:
By making SMTConstraintManager a template and passing the SMT constraint type and expr, we can further move code from the Z3ConstraintManager class to the generic SMT constraint Manager.

Now, each SMT specific constraint manager only needs to implement the method `bool canReasonAbout(SVal X) const`.

Reviewers: NoQ, george.karpenkov

Reviewed By: george.karpenkov

Subscribers: mgorny, xazax.hun, szepet, a.sidorin, Szelethus

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

llvm-svn: 340533
2018-08-23 13:21:00 +00:00
Mikhail R. Gadelha 3c94b65cb0 [analyzer] Update SMT API documentation and methods
Summary:
Update the documentation of all the classes introduced with the new generic SMT API, most of them were referencing Z3 and how previous operations were being done (like including the context as parameter in a few methods).

Renamed the following methods, so it's clear that the operate on bitvectors:
*`mkSignExt` -> `mkBVSignExt`
*`mkZeroExt` -> `mkBVZeroExt`
*`mkExtract` -> `mkBVExtract`
*`mkConcat` -> `mkBVConcat`

Removed the unecessary methods:
* `getDataExpr`: it was an one line method that called `fromData`
* `mkBitvector(const llvm::APSInt Int)`: it was not being used anywhere

Reviewers: NoQ, george.karpenkov

Reviewed By: george.karpenkov

Subscribers: xazax.hun, szepet, a.sidorin

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

llvm-svn: 337954
2018-07-25 19:34:48 +00:00
Mikhail R. Gadelha 5c3d032e70 [analyzer] Removed API used by the Refutation Manager from SMTConstraintManager and replace by proper calls to SMTSolver
Summary:
Third patch in the refactoring series, to decouple the SMT Solver from the Refutation Manager (1st: D49668, 2nd: D49767).

The refutation API in the `SMTConstraintManager` was a hack to allow us to create an SMT solver and verify the constraints; it was conceptually wrong from the start. Now, we don't actually need to use the `SMTConstraintManager` and can create an SMT object directly, add the constraints and check them.

While updating the Falsification visitor, I inlined the two functions that were used to collect the constraints and add them to the solver.

As a result of this patch, we could move the SMT API elsewhere and as it's not really dependent on the CSA anymore. Maybe we can create a new dir (utils/smt) for Z3 and future solvers?

Reviewers: NoQ, george.karpenkov

Reviewed By: george.karpenkov

Subscribers: xazax.hun, szepet, a.sidorin

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

llvm-svn: 337922
2018-07-25 12:49:43 +00:00
Mikhail R. Gadelha 8628e2cd54 [analyzer] Moved code from SMTConstraintManager to SMTSolver
Summary:
This is the second part of D49668, and moves all the code that's not specific to a ConstraintManager to SMTSolver.

No functional change intended.

Reviewers: NoQ, george.karpenkov

Reviewed By: george.karpenkov

Subscribers: xazax.hun, szepet, a.sidorin

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

llvm-svn: 337921
2018-07-25 12:49:37 +00:00
Mikhail R. Gadelha 456ecffe11 [analyzer] Moved non solver specific code from Z3ConstraintManager to SMTConstraintManager
Summary:
This patch moves a lot of code from `Z3ConstraintManager` to `SMTConstraintManager`, leaving only the necessary:
* `canReasonAbout` which returns if a Solver can handle a given `SVal` (should be moved to `SMTSolver` in the future).
* `removeDeadBindings`, `assumeExpr` and `print`: methods that need to use `ConstraintZ3Ty`, can probably be moved to `SMTConstraintManager` in the future.

The patch creates a new file, `SMTConstraintManager.cpp` with the moved code. Conceptually, this is move in the right direction and needs further improvements: `SMTConstraintManager` still does a lot of things that are not required by a `ConstraintManager`.

We ought to move the unrelated to `SMTSolver` and remove everything that's not related to a `ConstraintManager`. In particular, we could remove `addRangeConstraints` and `isModelFeasible`, and make the refutation manager create an Z3Solver directly.

Reviewers: NoQ, george.karpenkov

Reviewed By: george.karpenkov

Subscribers: mgorny, xazax.hun, szepet, a.sidorin

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

llvm-svn: 337919
2018-07-25 12:49:29 +00:00