en Copyright 2015 Java http://172.16.0.5:8080/history/llvm-project-15.0.7/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp#20f8733d [Analyzer][solver] Simplification: Do a fixpoint iteration before the eq class mergeThis reverts commit f02c5f3478318075d1a469203900e452ba651421 andaddresses the issue mentioned in D114619 differently.Repeating the issue here:Currently, during symbol simplification we remove the original membersymbol from the equivalence class (`ClassMembers` trait). However, wekeep the reverse link (`ClassMap` trait), in order to be able the querythe related constraints even for the old member. This asymmetry can leadto a problem when we merge equivalence classes:```ClassA: [a, b] // ClassMembers trait,a->a, b->a // ClassMap trait, a is the representative symbol```Now let,s delete `a`:```ClassA: [b]a->a, b->a```Let's merge ClassA into the trivial class `c`:```ClassA: [c, b]c->c, b->c, a->a```Now, after the merge operation, `c` and `a` are actually in differentequivalence classes, which is inconsistent.This issue manifests in a test case (added in D103317):```void recurring_symbol(int b) { if (b * b != b) if ((b * b) * b * b != (b * b) * b) if (b * b == 1)}```Before the simplification we have these equivalence classes:```trivial EQ1: [b * b != b]trivial EQ2: [(b * b) * b * b != (b * b) * b]```During the simplification with `b * b == 1`, EQ1 is merged with `1 != b``EQ1: [b * b != b, 1 != b]` and we remove the complex symbol, so`EQ1: [1 != b]`Then we start to simplify the only symbol in EQ2:`(b * b) * b * b != (b * b) * b --> 1 * b * b != 1 * b --> b * b != b`But `b * b != b` is such a symbol that had been removed previously fromEQ1, thus we reach the above mentioned inconsistency.This patch addresses the issue by making it impossible to synthesise asymbol that had been simplified before. We achieve this by simplifyingthe given symbol to the absolute simplest form.Differential Revision: https://reviews.llvm.org/D114887 List of files: /llvm-project-15.0.7/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp Wed, 01 Dec 2021 15:47:22 +0000 Gabor Marton <gabor.marton@ericsson.com> http://172.16.0.5:8080/history/llvm-project-15.0.7/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp#f02c5f34 [Analyzer][solver] Do not remove the simplified symbol from the eq classCurrently, during symbol simplification we remove the original member symbolfrom the equivalence class (`ClassMembers` trait). However, we keep thereverse link (`ClassMap` trait), in order to be able the query therelated constraints even for the old member. This asymmetry can lead toa problem when we merge equivalence classes:```ClassA: [a, b] // ClassMembers trait,a->a, b->a // ClassMap trait, a is the representative symbol```Now lets delete `a`:```ClassA: [b]a->a, b->a```Let's merge the trivial class `c` into ClassA:```ClassA: [c, b]c->c, b->c, a->a```Now after the merge operation, `c` and `a` are actually in differentequivalence classes, which is inconsistent.One solution to this problem is to simply avoid removing the originalmember and this is what this patch does.Other options I have considered:1) Always merge the trivial class into the non-trivial class. This might work most of the time, however, will fail if we have to merge two non-trivial classes (in that case we no longer can track equivalences precisely).2) In `removeMember`, update the reverse link as well. This would cease the inconsistency, but we'd loose precision since we could not query the constraints for the removed member.Differential Revision: https://reviews.llvm.org/D114619 List of files: /llvm-project-15.0.7/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp Fri, 26 Nov 2021 09:59:09 +0000 Gabor Marton <gabor.marton@ericsson.com> http://172.16.0.5:8080/history/llvm-project-15.0.7/clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.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-two-iterations.cpp Mon, 26 Jul 2021 20:55:44 +0000 Gabor Marton <gabor.marton@ericsson.com>