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

martong added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1155-1156 -// TODO: Support SymbolCast. Support IntSymExpr when/if we actually -// start producing them. ASDenysPetrov wrote: > ASDenysPetrov wrote: > >

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

martong updated this revision to Diff 386796. martong marked 7 inline comments as done. martong added a comment. - Rebase on top of parent revisions - Address review comments Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103317/new/

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

vsavchenko added a comment. In D103317#2803238 , @ASDenysPetrov wrote: > @vsavchenko > > I appologize for my immaturity and for the audacity of my infantile > assumptions. I admit any constructive criticism. Thank you for referencing > the theory. I

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

ASDenysPetrov added a comment. @vsavchenko I appologize for my immaturity and for the audacity of my infantile assumptions. I admit any constructive criticism. Thank you for referencing the theory. I will thoroughly study the domain in all. As for the **assignments** and why I brought them

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

vsavchenko added a comment. In D103317#2794099 , @ASDenysPetrov wrote: >> ! In D103317#2793797 , @vsavchenko >> wrote: > > > >> I replied to you earlier that assignments are not producing constraints. >> The

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

martong added a comment. In D103317#2794099 , @ASDenysPetrov wrote: >> ! In D103317#2793797 , @vsavchenko >> wrote: > > > >> I replied to you earlier that assignments are not producing constraints. >> The

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

ASDenysPetrov added a comment. > ! In D103317#2793797 , @vsavchenko > wrote: > I replied to you earlier that assignments are not producing constraints. The > analyzer has some sort of SSA (not really, but anyways), so every time we > reassign the

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

vsavchenko added a comment. In D103317#2793911 , @ASDenysPetrov wrote: > In D103317#2793797 , @vsavchenko > wrote: > >> Hmm, Okay, but what about situations if you have: `a = a1 + a2` and `a = a3 >> + a4 + a5`

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

ASDenysPetrov added a comment. In D103317#2793797 , @vsavchenko wrote: > Hmm, Okay, but what about situations if you have: `a = a1 + a2` and `a = a3 + > a4 + a5` are you going to throw away one of these constraints? And if so, how > do you want to

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

vsavchenko added a comment. In D103317#2793781 , @ASDenysPetrov wrote: > In D103317#2793658 , @vsavchenko > wrote: > >> But the problem it is generally not one-to-one relationship, so `x -> y1 + >> 1`, `x ->

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

ASDenysPetrov added a comment. In D103317#2793658 , @vsavchenko wrote: > But the problem it is generally not one-to-one relationship, so `x -> y1 + > 1`, `x -> y2 + 2`, ... , `x -> yN + N`. In my approach it can't be more then one binding for one

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

vsavchenko added a comment. In D103317#2793557 , @ASDenysPetrov wrote: > Returning to the discussion raised in D102696 > , I'd like to share my vision. > I think we can use much easier approach to use valid constraints

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

ASDenysPetrov added a comment. Returning to the discussion raised in D102696 , I'd like to share my vision. I think we can use much easier approach to use valid constraints at any point of time. The main idea is lazy-reasoning of the ranges. This approach: -

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

ASDenysPetrov added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1155-1156 -// TODO: Support SymbolCast. Support IntSymExpr when/if we actually -// start producing them. ASDenysPetrov wrote: > vsavchenko wrote: > >

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

ASDenysPetrov added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1155-1156 -// TODO: Support SymbolCast. Support IntSymExpr when/if we actually -// start producing them. vsavchenko wrote: > ASDenysPetrov wrote: > >

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

vsavchenko added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1155-1156 -// TODO: Support SymbolCast. Support IntSymExpr when/if we actually -// start producing them. ASDenysPetrov wrote: > vsavchenko wrote: > > Do

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

ASDenysPetrov added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1155-1156 -// TODO: Support SymbolCast. Support IntSymExpr when/if we actually -// start producing them. vsavchenko wrote: > Do we actually produce

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

vsavchenko added a comment. Looking great, thanks! I have a couple of notes below. Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1155-1156 -// TODO: Support SymbolCast. Support IntSymExpr when/if we actually -// start producing them.

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

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: