search

llvm / llvm-project

The LLVM Project is a collection of modular and reusable compiler and toolchain technologies.
http://llvm.org
Other
29.36k stars 12.14k forks source link

[Umbrella] Constraint solver improvements. #39492

Open haoNoQ opened 5 years ago

haoNoQ commented 5 years ago
Bugzilla Link 40145
Version trunk
OS All
CC @devincoughlin,@edwintorok

Extended Description

I'll dup false positives and false negatives that can be fixed by better constraint solving to this bug for easier tracking, as an effort to simplify Bugzilla maintenance and make it more useful.

All of the bugs duped here can be addressed with relative ease by integrating a third-party SMT solver such as Z3. Most likely every single one of them can be addressed by improving RangeConstraintManager instead, but addressing a significant portion of them this way boils down to re-inventing an SMT solver.

In some cases Static Analyzer produces simplified symbolic expressions in order to make life easier for RangeConstraintManager. One of the most common examples is the problem of implementing integral casts: they are intentionally incorrect because otherwise symbolic expressions will be too hard for the RangeConstraintManager to deal with, resulting in a net increase in false positives. Such bugs will be duped here as well. Bugs that require other, unrelated improvements to Static Analyzer (eg., better support for pointer casts that requires RegionStore re-modeling) will not be duped here.

haoNoQ commented 3 years ago

mentioned in issue llvm/llvm-bugzilla-archive#51358

haoNoQ commented 3 years ago

mentioned in issue llvm/llvm-bugzilla-archive#45081

haoNoQ commented 3 years ago

llvm/llvm-bugzilla-archive#51358 negation problems.

haoNoQ commented 5 years ago

^ A request for better cast support.

haoNoQ commented 5 years ago

Bug llvm/llvm-project#38486 has been marked as a duplicate of this bug.

haoNoQ commented 5 years ago

^ Relational constraints (x4 dupes).

haoNoQ commented 5 years ago

Bug llvm/llvm-project#2678 has been marked as a duplicate of this bug.

haoNoQ commented 5 years ago

assigned to @haoNoQ