20f8733d4b
This reverts commit f02c5f3478 and
addresses the issue mentioned in D114619 differently.
Repeating the issue here:
Currently, during symbol simplification we remove the original member
symbol from the equivalence class (`ClassMembers` trait). However, we
keep the reverse link (`ClassMap` trait), in order to be able the query
the related constraints even for the old member. This asymmetry can lead
to 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 different
equivalence 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 from
EQ1, thus we reach the above mentioned inconsistency.
This patch addresses the issue by making it impossible to synthesise a
symbol that had been simplified before. We achieve this by simplifying
the given symbol to the absolute simplest form.
Differential Revision: https://reviews.llvm.org/D114887
41 lines
1.4 KiB
C++
41 lines
1.4 KiB
C++
// RUN: %clang_analyze_cc1 %s \
|
|
// RUN: -analyzer-checker=core \
|
|
// RUN: -analyzer-checker=debug.ExprInspection \
|
|
// RUN: 2>&1 | FileCheck %s
|
|
|
|
// In this test we check whether the solver's symbol simplification mechanism
|
|
// is capable of reaching a fixpoint. This should be done after one iteration.
|
|
|
|
void clang_analyzer_printState();
|
|
|
|
void test(int a, int b, int c) {
|
|
if (a + b != c)
|
|
return;
|
|
clang_analyzer_printState();
|
|
// CHECK: "constraints": [
|
|
// CHECK-NEXT: { "symbol": "((reg_$0<int a>) + (reg_$1<int b>)) != (reg_$2<int c>)", "range": "{ [0, 0] }" }
|
|
// CHECK-NEXT: ],
|
|
// CHECK-NEXT: "equivalence_classes": [
|
|
// CHECK-NEXT: [ "(reg_$0<int a>) + (reg_$1<int b>)", "reg_$2<int c>" ]
|
|
// CHECK-NEXT: ],
|
|
// CHECK-NEXT: "disequality_info": null,
|
|
|
|
// Simplification starts here.
|
|
if (b != 0)
|
|
return;
|
|
clang_analyzer_printState();
|
|
// CHECK: "constraints": [
|
|
// CHECK-NEXT: { "symbol": "(reg_$0<int a>) != (reg_$2<int c>)", "range": "{ [0, 0] }" },
|
|
// CHECK-NEXT: { "symbol": "reg_$1<int b>", "range": "{ [0, 0] }" }
|
|
// CHECK-NEXT: ],
|
|
// CHECK-NEXT: "equivalence_classes": [
|
|
// CHECK-NEXT: [ "(reg_$0<int a>) != (reg_$2<int c>)" ],
|
|
// CHECK-NEXT: [ "reg_$0<int a>", "reg_$2<int c>" ]
|
|
// CHECK-NEXT: ],
|
|
// CHECK-NEXT: "disequality_info": null,
|
|
|
|
// Keep the symbols and the constraints! alive.
|
|
(void)(a * b * c);
|
|
return;
|
|
}
|