This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Create generic SMT Context class
ClosedPublic

Authored by mikhail.ramalho on Jul 12 2018, 6:29 AM.

Details

Summary

This patch creates SMTContext which will wrap a specific SMT context, through SMTSolverContext.

The templated SMTSolverContext class it's a simple wrapper around a SMT specific context (currently only used in the Z3 backend), while Z3Context inherits SMTSolverContext<Z3_context> and implements solver specific operations like initialization and destruction of the context.

This separation was done because:

  1. We might want to keep one single context, shared across different SMTConstraintManagers. It can be achieved by constructing a SMTContext, through a function like CreateSMTContext(Z3), CreateSMTContext(BOOLECTOR), etc. The rest of the CSA only need to know about SMTContext, so maybe it's a good idea moving SMTSolverContext to a separate header in the future.
  1. Any generic SMT operation will only require one SMTSolverContextobject, which can access the specific context by calling getContext().

Diff Detail

Event Timeline

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

Could we remove this method?

78

Let's not do this. This invalidates all Z3 objects, and all future calls to any Z3 objects will segfault.

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

Removed reset method and call to Z3_finalize_memory().

george.karpenkov requested changes to this revision.Jul 13 2018, 1:29 PM
george.karpenkov added inline comments.
include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h
22

What's the point of this base class?

This revision now requires changes to proceed.Jul 13 2018, 1:29 PM
include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h
22

SMTContext will be used around the CSA, since it doesn't know anything about the specific SMT context, e.g., Z3_Context.

SMTSolverContext<Z3_context> will be used in the solver specific implementation.

Simplify SMTContext class

LGTM with a nit

include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h
24

Probably should do =0 to indicate that this is a pure virtual class.

This revision is now accepted and ready to land.Jul 20 2018, 10:24 AM
This revision was automatically updated to reflect the committed changes.