This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Refactor and simplify SimpleConstraintManager
ClosedPublic

Authored by ddcc on Oct 27 2016, 8:05 PM.

Details

Summary

SimpleConstraintManager is difficult to use, and makes assumptions about capabilities of the constraint manager. This patch refactors out those portions into a new RangedConstraintManager, and also fixes some issues with camel case, formatting, and confusing naming.

Event Timeline

ddcc updated this revision to Diff 76161.Oct 27 2016, 8:05 PM
ddcc retitled this revision from to [analyzer] Refactor and simplify SimpleConstraintManager.
ddcc updated this object.
ddcc added reviewers: zaks.anna, dcoughlin.
ddcc added subscribers: cfe-commits, rgov, NoQ, xazax.hun.
ddcc added a comment.EditedOct 27 2016, 8:32 PM

To summarize, here is a list of changes:

  • General
    • Fixed some issues with formatting (clang-format)
    • Fixed inconsistent capitalization following camel case style guidelines
  • ConstraintManager.h
    • Renamed assumeWithinInclusiveRange*() to assumeInclusiveRange*(), since the range is not necessarily contained within unless Assumption is true, to match assume()
  • RangedConstraintManager.h (inherits SimpleConstraintManager)
    • Moved assumeSym* and canReasonAbout() from SimpleConstraintManager to here
    • Renamed assumeSymbolWithinInclusiveRange/assumeSymbolOutOfInclusiveRange to assumeSymWithinInclusiveRange/assumeSymOutsideInclusiveRange to match the above, and moved to here
    • This is now inherited by RangeConstraintManager, and essentially provides the current interface in SimpleConstraintManager
  • SimpleConstraintManager.h (inherits ConstraintManager)
    • Implemented a new interface that internally converts the DefinedSVal in assume(...) from ConstraintManager.h to NonLoc to SymbolRef. Subclasses only need to override ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, bool Assumption)
    • For inclusive ranges, implemented a new interface that internally converts from NonLoc to SymbolRef. Subclasses only need to override ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)
    • Implemented a new interface that internally handles expressions that fail canReasonAbout() by adding them directly to the constraint manager state. Subclasses only need to expose ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym, BinaryOperator::Opcode op, const llvm::APSInt &Int)
  • RangeConstraintManager.cpp
    • Minor optimization to avoid updating the state if nothing is pruned in removeDeadBindings()
dcoughlin edited edge metadata.Oct 31 2016, 2:48 PM

Thanks for the patch!

Would it be possible to split this up into several patches? I think it is important to separate the interface layering changes from the formatting changes, renaming changes, and minor optimization changes. This will make the patches easier to review.

Also: is this motivated by a different implementation of range constraints? Is this something you plan on upstreaming?

In D26061#581778, @ddcc wrote:

To summarize, here is a list of changes:

  • General
    • Fixed some issues with formatting (clang-format)
    • Fixed inconsistent capitalization following camel case style guidelines
  • ConstraintManager.h
    • Renamed assumeWithinInclusiveRange*() to assumeInclusiveRange*(), since the range is not necessarily contained within unless Assumption is true, to match assume()
  • RangedConstraintManager.h (inherits SimpleConstraintManager)
    • Moved assumeSym* and canReasonAbout() from SimpleConstraintManager to here
    • Renamed assumeSymbolWithinInclusiveRange/assumeSymbolOutOfInclusiveRange to assumeSymWithinInclusiveRange/assumeSymOutsideInclusiveRange to match the above, and moved to here
    • This is now inherited by RangeConstraintManager, and essentially provides the current interface in SimpleConstraintManager

What do you view as the distinction between RangeConstraintMananger and RangedConstraintManager? In other words, if I'm a developer adding new functionality how would you suggest I decide which to add it to? It would be good to document this in the code! Also: the closeness in the names of these classes could be potentially confusing. Are there other, more distinctive, names that still communicate the difference you intend?

  • SimpleConstraintManager.h (inherits ConstraintManager)
    • Implemented a new interface that internally converts the DefinedSVal in assume(...) from ConstraintManager.h to NonLoc to SymbolRef. Subclasses only need to override ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, bool Assumption)
    • For inclusive ranges, implemented a new interface that internally converts from NonLoc to SymbolRef. Subclasses only need to override ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)
    • Implemented a new interface that internally handles expressions that fail canReasonAbout() by adding them directly to the constraint manager state. Subclasses only need to expose ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym, BinaryOperator::Opcode op, const llvm::APSInt &Int)
  • RangeConstraintManager.cpp
    • Minor optimization to avoid updating the state if nothing is pruned in removeDeadBindings()
ddcc added a comment.Nov 1 2016, 10:48 AM

Yes, I've been writing a Z3 solver interface, which motivated this patch. However, this patch has snowballed into something that it's a little too convoluted, so I'll split it up.

I'm not sure whether the RangedConstraintManager interface is useful or not; I preserved it because it's currently in the code, but since RangeConstraintManager is the only user, it is possible to merge the two together and eliminate the interface. In the past, BasicConstraintManager was the other class that used this interface, but that was deleted quite a while back, and I'm not sure if there are plans for anything else?

ddcc updated this revision to Diff 78049.Nov 15 2016, 12:22 PM
ddcc edited edge metadata.

Rebase on recent changes

ddcc updated this revision to Diff 80129.Dec 2 2016, 1:51 PM

Rebase, move assumeSymRel() to RangedConstraintManager, make assumeSymUnsupported pure virtual in SimpleConstraintManager.

ddcc added a comment.Dec 12 2016, 5:52 PM

How does this look now?

ddcc updated this revision to Diff 85136.Jan 20 2017, 7:57 AM

Rebase

ddcc updated this revision to Diff 89054.Feb 18 2017, 8:00 PM

Rebase, incorporate D22862

This revision was automatically updated to reflect the committed changes.