[llvm-bugs] [Bug 49490] New: RangeConstraintManager infeasible execution path due to EquivalenceClasses

[via llvm-bugs]

https://bugs.llvm.org/show_bug.cgi?id=49490

            Bug ID: 49490
           Summary: RangeConstraintManager infeasible execution path due
                    to EquivalenceClasses
           Product: clang
           Version: trunk
          Hardware: PC
                OS: All
            Status: NEW
          Severity: enhancement
          Priority: P
         Component: Static Analyzer
          Assignee: dcoughlin at apple.com
          Reporter: balazs.benics at sigmatechnology.se
                CC: dcoughlin at apple.com, llvm-bugs at lists.llvm.org

Created attachment 24605
  --> https://bugs.llvm.org/attachment.cgi?id=24605&action=edit
reproducer

RangeConstraintManager::setConstraint produces a State, where an empty RangeSet
is associated with an EquivalenceClass.
AFAIK that should never happen.
Originally, the Z3 crosscheck visitor crashed on this when it tried to
serialize the range set of a symbol.
Then I realized that this is connected to the `RangeConstraintManager`,
constructing an infeasible execution path.

I attach the trimmed exploded graph segment, where the first state appears with
the empty range-set.

You can add the required assertions to diagnose it by applying the attached
`add-sanity-check-assertions.patch` patch file on top of
b9f169fb7dcd09721a4487801873a61a1e20da7e (current trunk).
It will check if the State returned by `RangeConstraintManager::setConstraint`
has no empty range sets associated with any EquivalenceClasses.

Then run the analysis on the attached code:
./bin/clang --analyze -Xclang -analyzer-display-progress -Xclang
-analyze-function="bar()" -Xclang
-analyzer-checker=core,alpha.security.ArrayBound MemorySSA-preprocessed.cpp


I would fix this myself, but I'm quite busy right now.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-bugs/attachments/20210309/5eca68db/attachment.html>