This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Moved static Context to class member
ClosedPublic

Authored by mikhail.ramalho on Jul 12 2018, 7:51 AM.

Details

Summary

Although it is a big patch, the changes are simple:

  1. There is one Z3_Context now, member of the SMTConstraintManager class.
  2. Z3Expr, Z3Sort, Z3Model and Z3Solver are constructed with a reference to the Z3_Context in SMTConstraintManager.
  3. All static functions are now members of Z3Solver, e.g, the SMTConstraintManager now calls Solver.fromBoolean(false) instead of Z3Expr::fromBoolean(false).

Most of the patch only move stuff around except:

  1. New method Z3Sort MkSort(const QualType &Ty, unsigned BitWidth), that creates a sort based on the QualType and its width. Used to simplify the fromData method.

Unfortunate consequence of this patch:

  1. getInterpretation was moved from Z3Model class to Z3Solver, because it needs to create a Z3Sort before returning the interpretation. This can be fixed by changing both toAPFloat and toAPSInt by removing the dependency of Z3Sort (it's only used to check which Sort was created and to retrieve the type width).

Diff Detail

Event Timeline

george.karpenkov requested changes to this revision.Jul 12 2018, 10:41 AM
george.karpenkov added inline comments.
lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
944–946

This line is redundant

This revision now requires changes to proceed.Jul 12 2018, 10:41 AM

Removed redundant line.

The code is still crashing. For some reason, SMTConstraintManager's constructor creates a temporary Z3Context and destroys it.

NoQ added a comment.Jul 12 2018, 11:21 AM

SMTContext::getContext() returns the context by value, which means making a copy. It should return by reference.

NoQ added a comment.Jul 12 2018, 11:23 AM

Mm, wait, nvm, it's a pointer.

NoQ added a comment.Jul 12 2018, 11:25 AM

Z3Solver takes Z3Context by value, but then stores a reference. It should take it by reference.

In D49236#1160540, @NoQ wrote:

Z3Solver takes Z3Context by value, but then stores a reference. It should take it by reference.

Yes! Thank you!

Fixed constructor of Z3Expr, Z3Sort, Z3Model and Z3Solver not taking the reference to the Z3Context.

It's still crashing, due to the removal of castAPSInt. Investigating now.

mikhail.ramalho edited the summary of this revision. (Show Details)

Migrated cast methods.

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
938

I'm not sure whether this is a right ownership model.
Constraint manager conceptually represents a solver, right?
Then could we make the Z3Solver non-mutable, have Z3Context live at the level above (one per application) and pass it by reference to the Z3ConstraintManager constructor?

george.karpenkov requested changes to this revision.Jul 17 2018, 10:59 AM
This revision now requires changes to proceed.Jul 17 2018, 10:59 AM
lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
938

I don't know how changing the Z3ConstraintManager constructor would work with the rest of the CSA. The analyzer expects the constraint manager to be created using (Analyses.def:25 ):

std::unique_ptr<ConstraintManager>
ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng)

and it's expected to be in the form (ProgramState.h:42):

typedef std::unique_ptr<ConstraintManager>(*ConstraintManagerCreator)(
    ProgramStateManager &, SubEngine *);

A pointer to the function that creates the constraint manager (CreateZ3ConstraintManager if -analyzer-constraints=z3 or CreateRangeConstraintManager if -analyzer-constraints=range) and eventually gets invoked in ProgramStateManager's constructor:

ProgramStateManager::ProgramStateManager(ASTContext &Ctx,
                                         StoreManagerCreator CreateSMgr,
                                         ConstraintManagerCreator CreateCMgr,
                                         llvm::BumpPtrAllocator &alloc,
                                         SubEngine *SubEng)
  : Eng(SubEng), EnvMgr(alloc), GDMFactory(alloc),
    svalBuilder(createSimpleSValBuilder(alloc, Ctx, *this)),
    CallEventMgr(new CallEventManager(alloc)), Alloc(alloc) {
  StoreMgr = (*CreateSMgr)(*this);
  ConstraintMgr = (*CreateCMgr)(*this, SubEng);
}

Maybe we should keep the idea of one context on hold and focus on the reusable SAT cores for now?

Maybe we should keep the idea of one context on hold and focus on the reusable SAT cores for now?

Unfortunately no, it's crucial to reuse the same context for performance. In fact that's a much easier way to get there.

OK what about this: why not just decouple context and solver classes from constraint manager entirely?
Z3ConstraintManager can then create it's own context/solver.
Your visitor can use Z3Solver directly. Does that sound too complicated?

I mean, conceptually, you are not really using Z3ConstraintManager, as we are not replacing the solver with Z3, we are just using it for cross-checking.

Maybe we should keep the idea of one context on hold and focus on the reusable SAT cores for now?

Unfortunately no, it's crucial to reuse the same context for performance. In fact that's a much easier way to get there.

OK what about this: why not just decouple context and solver classes from constraint manager entirely?

Yeah, actually neither the SMTConstraintManager nor the Z3ConstraintManager need to know about the SMTContext, it can be moved to inside the Z3Solver class (or a generic SMTSolver).

Z3ConstraintManager can then create it's own context/solver.
Your visitor can use Z3Solver directly. Does that sound too complicated?

No, I think that's the way to go.

I mean, conceptually, you are not really using Z3ConstraintManager, as we are not replacing the solver with Z3, we are just using it for cross-checking.

Having a SMTSolver generic class seems like a good idea, specially if we want to implement other solvers in the future.

We can expose it to both the ConstraintManager and the RefutationManager through a createSMTSolver(SolverT ty), where SolverT is a enum of possible solvers. How about that? Obviously, it'll only have Z3 for now.

Updated given changes in D49233

mikhail.ramalho retitled this revision from [analyzer] [WIP] Moved static Context to class member to [analyzer] Moved static Context to class member.

I'm not 100% convinced that reference count is correct everywhere, but I guess OK if it's not crashing.

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
70–71

should be a separate revision, but OK

243

I'm confused why in other move assignments you only decrement reference counts, but in this one you increment as well

This revision is now accepted and ready to land.Jul 20 2018, 10:22 AM
lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
243

Yeah, I'm not quite sure what's the difference, it's there since the beginning.

In any case, we won't need all these constructors when the new API lands. I'll create a revision in the future to remove all the dead code from the backend.

This revision was automatically updated to reflect the committed changes.