This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Removed API used by the Refutation Manager from SMTConstraintManager and replace by proper calls to SMTSolver
ClosedPublic

Authored by mikhail.ramalho on Jul 24 2018, 4:31 PM.

Details

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?

Diff Detail

Repository
rC Clang

Event Timeline

george.karpenkov accepted this revision.Jul 24 2018, 4:47 PM
george.karpenkov added inline comments.
lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
1053

not sure whether it makes sense to return nullptr vs. crashing.

This revision is now accepted and ready to land.Jul 24 2018, 4:47 PM
lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
1053

True, I got it from CreateZ3ConstraintManager. Should I remove it from both?

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
1053

if it was there before, let's leave it for now

This revision was automatically updated to reflect the committed changes.