mirror of
https://github.com/llvm/llvm-project.git
synced 2025-04-29 03:56:06 +00:00
f02c5f3478
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 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 different equivalence classes, which is inconsistent. One solution to this problem is to simply avoid removing the original member 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
49 lines
2.2 KiB
C++
49 lines
2.2 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 TWO iterations.
|
|
|
|
void clang_analyzer_printState();
|
|
|
|
void test(int a, int b, int c, int d) {
|
|
if (a + b + c != d)
|
|
return;
|
|
if (c + b != 0)
|
|
return;
|
|
clang_analyzer_printState();
|
|
// CHECK: "constraints": [
|
|
// CHECK-NEXT: { "symbol": "(((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
|
|
// CHECK-NEXT: { "symbol": "(reg_$2<int c>) + (reg_$1<int b>)", "range": "{ [0, 0] }" }
|
|
// CHECK-NEXT: ],
|
|
// CHECK-NEXT: "equivalence_classes": [
|
|
// CHECK-NEXT: [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "reg_$3<int d>" ]
|
|
// 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_$1<int b>)) + (reg_$2<int c>)) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
|
|
// CHECK-NEXT: { "symbol": "((reg_$0<int a>) + (reg_$2<int c>)) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
|
|
// CHECK-NEXT: { "symbol": "(reg_$0<int a>) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
|
|
// CHECK-NEXT: { "symbol": "(reg_$2<int c>) + (reg_$1<int b>)", "range": "{ [0, 0] }" },
|
|
// CHECK-NEXT: { "symbol": "reg_$1<int b>", "range": "{ [0, 0] }" },
|
|
// CHECK-NEXT: { "symbol": "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>)) != (reg_$3<int d>)", "((reg_$0<int a>) + (reg_$2<int c>)) != (reg_$3<int d>)", "(reg_$0<int a>) != (reg_$3<int d>)" ],
|
|
// CHECK-NEXT: [ "((reg_$0<int a>) + (reg_$1<int b>)) + (reg_$2<int c>)", "(reg_$0<int a>) + (reg_$2<int c>)", "reg_$0<int a>", "reg_$3<int d>" ],
|
|
// CHECK-NEXT: [ "(reg_$2<int c>) + (reg_$1<int b>)", "reg_$2<int c>" ]
|
|
// CHECK-NEXT: ],
|
|
// CHECK-NEXT: "disequality_info": null,
|
|
|
|
// Keep the symbols and the constraints! alive.
|
|
(void)(a * b * c * d);
|
|
return;
|
|
}
|