Page MenuHomePhabricator

[analyzer] Move RangeSet related declarations into the RangedConstraintManager header.
ClosedPublic

Authored by mikhail.ramalho on Apr 21 2018, 4:54 AM.

Diff Detail

Repository
rC Clang

Event Timeline

rnkovacs created this revision.Apr 21 2018, 4:54 AM

I could also move RangedConstraintManager.h under include

We probably don't want to do that: currently it can only be imported by files in Core, and we probably should keep it that way

lib/StaticAnalyzer/Core/RangedConstraintManager.h
130

Why not also REGISTER_TRAIT_WITH_PROGRAMSTATE here?

Another approach would be to instead teach RangedConstraintManager to convert it's constraints to Z3. That would be an unwanted dependency, but the change would be much smaller, and the internals of the solver would not have to be exposed. @NoQ thoughts?

NoQ added inline comments.Apr 23 2018, 12:01 PM
lib/StaticAnalyzer/Core/RangedConstraintManager.h
130
33   /// The macro should not be used inside namespaces, or for traits that must
34   /// be accessible from more than one translation unit.
35   #define REGISTER_TRAIT_WITH_PROGRAMSTATE(Name, Type) \
36   ...

I don't remember why.

NoQ added a comment.Apr 23 2018, 12:23 PM

Another approach would be to instead teach RangedConstraintManager to convert it's constraints to Z3. That would be an unwanted dependency, but the change would be much smaller, and the internals of the solver would not have to be exposed. @NoQ thoughts?

Dunno. Obviously, the adaptor code between the constraint manager and the refutation manager (i think the word "solver" is causing confusion now) would have to access internals of both managers, so the situation is quite symmetric.

NoQ accepted this revision.Apr 23 2018, 1:02 PM

I could also move RangedConstraintManager.h under include

We probably don't want to do that: currently it can only be imported by files in Core, and we probably should keep it that way

I believe that many of our warning messages could be improved by presenting ranges to the user. Eg., ArrayBoundChecker could benefit from something like "index is within range [11, 12] and array size is equal to 10", and then a visitor that explains all the places in which the index was constrained to a smaller range. So in long term i'll be in favor of providing a way of explaining constraints to the users, which means partially exposing constraint manager internals to the checkers in a certain way (not necessarily *this* way). So for now i have no opinion on this issue :)

This revision is now accepted and ready to land.Apr 23 2018, 1:02 PM
mikhail.ramalho commandeered this revision.May 10 2018, 10:12 AM
mikhail.ramalho added a reviewer: rnkovacs.
mikhail.ramalho added a subscriber: mikhail.ramalho.

Commandeering the PR because of GSoC.

This revision was automatically updated to reflect the committed changes.