[PATCH] D103317: [Analyzer][engine][solver] Simplify complex constraints

[Gabor Marton via Phabricator via cfe-commits]

martong created this revision.
martong added reviewers: vsavchenko, NoQ, steakhal.
Herald added subscribers: manas, ASDenysPetrov, gamesh411, dkrupp, donat.nagy, Szelethus, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, xazax.hun, whisperity.
Herald added a reviewer: Szelethus.
martong requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

Add the capability to simplify more complex constraints where there are 3
symbols in the tree. In this change I extend simplifySVal to query constraints
of children sub-symbols in a symbol tree. (The constraint for the parent is
asked in `getKnownValue`.) This change makes the following cases to pass
(notice the 3rd check in each test-case).

This patch is the second step of a sequence of patches, and not intended to be
commited as a standalone change. The sequence of patches (and the plan) is
described here: https://reviews.llvm.org/D102696#2784624

  int test_left_tree_constrained(int x, int y, int z) {
    if (x + y + z != 0)
      return 0;
    if (x + y != 0)
      return 0;
    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
    clang_analyzer_eval(x + y == 0);     // expected-warning{{TRUE}}
    clang_analyzer_eval(z == 0);         // expected-warning{{TRUE}}
    x = y = z = 1;
    return 0;
  }


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D103317

Files:
  clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  clang/test/Analysis/simplify-complex-constraints.cpp

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D103317.348511.patch
Type: text/x-patch
Size: 4012 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20210528/12c0f4f7/attachment-0001.bin>