en Copyright 2015 Java http://172.16.0.5:8080/history/llvm-project-15.0.7/clang/test/Analysis/symbol-simplification-fixpoint-iteration-unreachable-code.cpp#806329da [analyzer][solver] Iterate to a fixpoint during symbol simplification with constantsD103314 introduced symbol simplification when a new constant constraint isadded. Currently, we simplify existing equivalence classes by iterating overall existing members of them and trying to simplify each member symbol withsimplifySVal.At the end of such a simplification round we may end up introducing anew constant constraint. Example:``` if (a + b + c != d) return; if (c + b != 0) return; // Simplification starts here. if (b != 0) return;```The `c == 0` constraint is the result of the first simplification iteration.However, we could do another round of simplification to reach the conclusionthat `a == d`. Generally, we could do as many new iterations until we reach afixpoint.We can reach to a fixpoint by recursively calling `State->assume` on thenewly simplified symbol. By calling `State->assume` we re-ignite thewhole assume machinery (along e.g with adjustment handling).Why should we do this? By reaching a fixpoint in simplification we are capableof discovering infeasible states at the moment of the introduction of the**first** constant constraint.Let's modify the previous example just a bit, and consider what happens withoutthe fixpoint iteration.``` if (a + b + c != d) return; if (c + b != 0) return; // Adding a new constraint. if (a == d) return; // This brings in a contradiction. if (b != 0) return; clang_analyzer_warnIfReached(); // This produces a warning. // The path is already infeasible... if (c == 0) // ...but we realize that only when we evaluate `c == 0`. return;```What happens currently, without the fixpoint iteration? As the inline commentssuggest, without the fixpoint iteration we are doomed to realize that we are onan infeasible path only after we are already walking on that. With fixpointiteration we can detect that before stepping on that. With fixpoint iteration,the `clang_analyzer_warnIfReached` does not warn in the above example b/cduring the evaluation of `b == 0` we realize the contradiction. The engine andthe checkers do rely on that either `assume(Cond)` or `assume(!Cond)` should befeasible. This is in fact assured by the so called expensive checks(LLVM_ENABLE_EXPENSIVE_CHECKS). The StdLibraryFuncionsChecker is notably one ofthe checkers that has a very similar assertion.Before this patch, we simply added the simplified symbol to the equivalenceclass. In this patch, after we have added the simplified symbol, we remove theold (more complex) symbol from the members of the equivalence class(`ClassMembers`). Removing the old symbol is beneficial because during the nextiteration of the simplification we don't have to consider again the old symbol.Contrary to how we handle `ClassMembers`, we don't remove the old Sym->Classrelation from the `ClassMap`. This is important for two reasons: Theconstraints of the old symbol can still be found via it's equivalence classthat it used to be the member of (1). We can spare one removal and thus oneadditional tree in the forest of `ClassMap` (2).Performance and complexity: Let us assume that in a State we have N non-trivialequivalence classes and that all constraints and disequality info is related tonon-trivial classes. In the worst case, we can simplify only one symbol of oneclass in each iteration. The number of symbols in one class cannot grow b/c wereplace the old symbol with the simplified one. Also, the number of theequivalence classes can decrease only, b/c the algorithm does a merge operationoptionally. We need N iterations in this case to reach the fixpoint. Thus, thesteps needed to be done in the worst case is proportional to `N*N`. Empiricalresults (attached) show that there is some hardly noticeable run-time and peakmemory discrepancy compared to the baseline. In my opinion, these differencescould be the result of measurement error.This worst case scenario can be extended to that cases when we have trivialclasses in the constraints and in the disequality map are transforming to sucha State where there are only non-trivial classes, b/c the algorithm does mergeoperations. A merge operation on two trivial classes results in one non-trivialclass.Differential Revision: https://reviews.llvm.org/D106823 List of files: /llvm-project-15.0.7/clang/test/Analysis/symbol-simplification-fixpoint-iteration-unreachable-code.cpp Mon, 26 Jul 2021 20:55:44 +0000 Gabor Marton <gabor.marton@ericsson.com>