[PATCH] D82445: [analyzer][solver] Track symbol equivalence

Valeriy Savchenko via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Wed Jun 24 03:12:41 PDT 2020


vsavchenko created this revision.
vsavchenko added reviewers: NoQ, dcoughlin, ASDenysPetrov, xazax.hun, Szelethus.
Herald added subscribers: cfe-commits, martong, Charusso, dkrupp, donat.nagy, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware.
Herald added a project: clang.
vsavchenko added a parent revision: D82381: [analyzer] Introduce small improvements to the solver infra.

For the most cases, we try to reason about symbol either based on the
information we know about that symbol in particular or about its
composite parts.  This is faster and eliminates costly brute force
searches through existing constraints.

However, we do want to support some cases that are widespread enough
and involve reasoning about different existing constraints at once.
These include:

- resoning about 'a - b' based on what we know about 'b - a'
- reasoning about 'a <= b' based on what we know about 'a > b' or 'a < b'

This commit expands on that part by tracking symbols known to be equal
while still avoiding brute force searches.  It changes the way we track
constraints for individual symbols.  If we know for a fact that 'a == b'
then there is no need in tracking constraints for both 'a' and 'b' especially
if these constraints are different.  This additional relationship makes
dead/live logic for constraints harder as we want to maintain as much
information on the equivalence class as possible, but we still won't
carry the information that we don't need anymore.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D82445

Files:
  clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
  clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  clang/test/Analysis/equality_tracking.c

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D82445.272953.patch
Type: text/x-patch
Size: 40282 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20200624/19d4220c/attachment-0001.bin>


More information about the cfe-commits mailing list