[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp:46 +ConstraintManager::ProgramStatePair +ConstraintManager::assumeDual(ProgramStateRef State, DefinedSVal Cond) { + ProgramStateRef StTrue = assume(State, Cond, true);

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

thakis added a comment. https://github.com/llvm/llvm-project/commit/21feafaeb85aad2847db44aa2208999b166ba4a9 fixed it, thanks! Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D124674/new/ https://reviews.llvm.org/D124674

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

thakis added a comment. One of your 3 commits in https://github.com/llvm/llvm-project/compare/3d888b0491f8...34ac048aef29 broke check-clang on Windows: http://45.33.8.238/win/57870/step_7.txt Please take a look, and revert for now if it takes a while to fix. Repository: rG LLVM Github

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

This revision was automatically updated to reflect the committed changes. Closed by commit rGc4fa05f5f778: [analyzer] Indicate if a parent state is infeasible (authored by martong). Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D124674/new/

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong updated this revision to Diff 427625. martong marked 2 inline comments as done. martong added a comment. - Fix typos in essay Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D124674/new/ https://reviews.llvm.org/D124674 Files:

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong added inline comments. Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:99 + // recognise that a parent is infeasible only *after* a new and more specific + // constraint and its negation is evaluated. + // Yeah, thx,

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

steakhal accepted this revision. steakhal added a comment. only a few typos Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:89-114 + // A state is infeasible if there is a contradiction among the constraints. + // An infeasible state is

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong updated this revision to Diff 427594. martong marked an inline comment as done. martong added a comment. - Add explanatory comment, rename to PosteriorlyOverconstrained Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D124674/new/

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong marked an inline comment as done. martong added a comment. In D124674#3491710 , @NoQ wrote: > Yes, we've discussed this before, and I'm very much in favor of this change. > This is assertion removal, and the assertion has been really useful back

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

NoQ added a comment. Yes, we've discussed this before, and I'm very much in favor of this change. This is assertion removal, and the assertion has been really useful back in the day, but the assertion doesn't seem to be realistic to maintain with all the new logic in the constraint solver

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong added a comment. @NoQ Could you please take a look? This change effects the very core of the analyzer. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D124674/new/ https://reviews.llvm.org/D124674

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong updated this revision to Diff 426785. martong added a comment. - Add LLVM_UNLIKELY Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D124674/new/ https://reviews.llvm.org/D124674 Files:

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp:51 +ProgramStateRef StFalse = assume(State, Cond, false); +if (!StFalse) { // both infeasible + ProgramStateRef Infeasible = State->cloneAsInfeasible();

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong marked an inline comment as done. martong added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp:51 +ProgramStateRef StFalse = assume(State, Cond, false); +if (!StFalse) { // both infeasible + ProgramStateRef Infeasible =

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong marked an inline comment as done. martong added inline comments. Comment at: clang/test/Analysis/sink-infeasible.c:37-48 + /* The BASELINE passes these checks ('wrning' is used to avoid lit to match) + // The parent state is already infeasible, look at this

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp:51 +ProgramStateRef StFalse = assume(State, Cond, false); +if (!StFalse) { // both infeasible + ProgramStateRef Infeasible = State->cloneAsInfeasible();

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong updated this revision to Diff 426715. martong added a comment. - Add a simpler test case Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D124674/new/ https://reviews.llvm.org/D124674 Files:

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

steakhal added a comment. I think I don't have anything left. Let's see the numbers. Comment at: clang/test/Analysis/sink-infeasible.c:37-48 + /* The BASELINE passes these checks ('wrning' is used to avoid lit to match) + // The parent state is already infeasible, look at

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong added a comment. In D124674#3482765 , @steakhal wrote: > Finally, we have this! Thanks for the review. > Can we have this https://godbolt.org/z/oferc6P5Y in addition to the one you > proposed? > I find it more readable. Sure, I find it also

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp:51 +ProgramStateRef StFalse = assume(State, Cond, false); +if (!StFalse) { // both infeasible + ProgramStateRef Infeasible = State->cloneAsInfeasible();

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong updated this revision to Diff 426635. martong marked 6 inline comments as done. martong added a comment. - Update according to review comments Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D124674/new/ https://reviews.llvm.org/D124674

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

steakhal added a comment. Finally, we have this! Can we have this https://godbolt.org/z/oferc6P5Y in addition to the one you proposed? I find it more readable. What performance hit will we suffer from this change? Please do a differential analysis. Comment at:

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong added inline comments. Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:96-97 - -// If StTrue is infeasible, asserting the falseness of Cond is unnecessary -// because the existing constraints already establish this. -if

[PATCH] D124674: [analyzer] Indicate if a parent state is infeasible

martong created this revision. martong added reviewers: NoQ, steakhal, ASDenysPetrov, Szelethus, xazax.hun. Herald added subscribers: manas, gamesh411, dkrupp, donat.nagy, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware. Herald added a project: All. martong requested review of