-
Notifications
You must be signed in to change notification settings - Fork 15.1k
[DA] Check for overflow in strong SIV test #166223
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: main
Are you sure you want to change the base?
Changes from all commits
59ce261
f372751
a94c3ed
c1ba53e
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,6 +1,8 @@ | ||
| ; NOTE: Assertions have been autogenerated by utils/update_analyze_test_checks.py UTC_ARGS: --version 5 | ||
| ; RUN: opt < %s -disable-output "-passes=print<da>" -aa-pipeline=basic-aa 2>&1 \ | ||
| ; RUN: | FileCheck %s | ||
| ; RUN: | FileCheck %s --check-prefixes=CHECK,CHECK-ALL | ||
| ; RUN: opt < %s -disable-output "-passes=print<da>" -aa-pipeline=basic-aa -da-enable-dependence-test=strong-siv 2>&1 \ | ||
| ; RUN: | FileCheck %s --check-prefixes=CHECK,CHECK-STRONG-SIV | ||
|
|
||
| target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64-S128" | ||
| target triple = "x86_64-apple-macosx10.6.0" | ||
|
|
@@ -423,19 +425,33 @@ for.end: ; preds = %for.body | |
| ;; *B++ = A[i + 2*n]; | ||
|
|
||
| define void @strong9(ptr %A, ptr %B, i64 %n) nounwind uwtable ssp { | ||
| ; CHECK-LABEL: 'strong9' | ||
| ; CHECK-NEXT: Src: store i32 %conv, ptr %arrayidx, align 4 --> Dst: store i32 %conv, ptr %arrayidx, align 4 | ||
| ; CHECK-NEXT: da analyze - none! | ||
| ; CHECK-NEXT: Src: store i32 %conv, ptr %arrayidx, align 4 --> Dst: %0 = load i32, ptr %arrayidx2, align 4 | ||
| ; CHECK-NEXT: da analyze - none! | ||
| ; CHECK-NEXT: Src: store i32 %conv, ptr %arrayidx, align 4 --> Dst: store i32 %0, ptr %B.addr.02, align 4 | ||
| ; CHECK-NEXT: da analyze - confused! | ||
| ; CHECK-NEXT: Src: %0 = load i32, ptr %arrayidx2, align 4 --> Dst: %0 = load i32, ptr %arrayidx2, align 4 | ||
| ; CHECK-NEXT: da analyze - none! | ||
| ; CHECK-NEXT: Src: %0 = load i32, ptr %arrayidx2, align 4 --> Dst: store i32 %0, ptr %B.addr.02, align 4 | ||
| ; CHECK-NEXT: da analyze - confused! | ||
| ; CHECK-NEXT: Src: store i32 %0, ptr %B.addr.02, align 4 --> Dst: store i32 %0, ptr %B.addr.02, align 4 | ||
| ; CHECK-NEXT: da analyze - none! | ||
| ; CHECK-ALL-LABEL: 'strong9' | ||
| ; CHECK-ALL-NEXT: Src: store i32 %conv, ptr %arrayidx, align 4 --> Dst: store i32 %conv, ptr %arrayidx, align 4 | ||
| ; CHECK-ALL-NEXT: da analyze - none! | ||
| ; CHECK-ALL-NEXT: Src: store i32 %conv, ptr %arrayidx, align 4 --> Dst: %0 = load i32, ptr %arrayidx2, align 4 | ||
| ; CHECK-ALL-NEXT: da analyze - none! | ||
| ; CHECK-ALL-NEXT: Src: store i32 %conv, ptr %arrayidx, align 4 --> Dst: store i32 %0, ptr %B.addr.02, align 4 | ||
| ; CHECK-ALL-NEXT: da analyze - confused! | ||
| ; CHECK-ALL-NEXT: Src: %0 = load i32, ptr %arrayidx2, align 4 --> Dst: %0 = load i32, ptr %arrayidx2, align 4 | ||
| ; CHECK-ALL-NEXT: da analyze - none! | ||
| ; CHECK-ALL-NEXT: Src: %0 = load i32, ptr %arrayidx2, align 4 --> Dst: store i32 %0, ptr %B.addr.02, align 4 | ||
| ; CHECK-ALL-NEXT: da analyze - confused! | ||
| ; CHECK-ALL-NEXT: Src: store i32 %0, ptr %B.addr.02, align 4 --> Dst: store i32 %0, ptr %B.addr.02, align 4 | ||
| ; CHECK-ALL-NEXT: da analyze - none! | ||
| ; | ||
| ; CHECK-STRONG-SIV-LABEL: 'strong9' | ||
| ; CHECK-STRONG-SIV-NEXT: Src: store i32 %conv, ptr %arrayidx, align 4 --> Dst: store i32 %conv, ptr %arrayidx, align 4 | ||
| ; CHECK-STRONG-SIV-NEXT: da analyze - none! | ||
| ; CHECK-STRONG-SIV-NEXT: Src: store i32 %conv, ptr %arrayidx, align 4 --> Dst: %0 = load i32, ptr %arrayidx2, align 4 | ||
| ; CHECK-STRONG-SIV-NEXT: da analyze - flow [*|<]! | ||
| ; CHECK-STRONG-SIV-NEXT: Src: store i32 %conv, ptr %arrayidx, align 4 --> Dst: store i32 %0, ptr %B.addr.02, align 4 | ||
| ; CHECK-STRONG-SIV-NEXT: da analyze - confused! | ||
| ; CHECK-STRONG-SIV-NEXT: Src: %0 = load i32, ptr %arrayidx2, align 4 --> Dst: %0 = load i32, ptr %arrayidx2, align 4 | ||
| ; CHECK-STRONG-SIV-NEXT: da analyze - none! | ||
| ; CHECK-STRONG-SIV-NEXT: Src: %0 = load i32, ptr %arrayidx2, align 4 --> Dst: store i32 %0, ptr %B.addr.02, align 4 | ||
| ; CHECK-STRONG-SIV-NEXT: da analyze - confused! | ||
| ; CHECK-STRONG-SIV-NEXT: Src: store i32 %0, ptr %B.addr.02, align 4 --> Dst: store i32 %0, ptr %B.addr.02, align 4 | ||
| ; CHECK-STRONG-SIV-NEXT: da analyze - none! | ||
| ; | ||
| entry: | ||
| %cmp1 = icmp eq i64 %n, 0 | ||
|
|
@@ -512,3 +528,45 @@ for.body: ; preds = %entry, %for.body | |
| for.end: ; preds = %for.body | ||
| ret void | ||
| } | ||
|
|
||
|
|
||
| ;; for (long unsigned i = 0; i < 9223372036854775806; i++) | ||
| ;; for (long unsigned j = 0; j < 2147483640; j++) | ||
| ;; if (i < 3000000000) | ||
| ;; A[i] = 0; | ||
| ; | ||
| ; FIXME: DependenceAnalysis fails to detect the dependency between A[i] and | ||
| ; itself, while Strong SIV has been able to prove it. | ||
|
Comment on lines
+538
to
+539
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think this comment also needs to be fixed, as Strong SIV doesn't prove the dependency. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Strong SIV is proving the dependency after the fix by this patch. The output of Strong SIV is There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I don't think DA proves the dependency. Returning false in There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. In general you are correct. If a test returns false it just mean that it couldn't prove anything. But in this case it is different. Sometime when StrongSIV is providing a distance or direction, it actually means that StrongSIV has been able to prove a dependency by providing their difference or direction. More specifically, whenever we have This is something I had mentioned before on another discussion. When StrongSIV is successful to prove a dependency, DA does not need to check other tests anymore. Anyway, meanwhile I think StrongSIV is actually capable to prove a dependency, I am fine to change the comment to something like this:
Let me know what you think or suggest. Thanks. |
||
| define void @strong11(ptr %A) nounwind uwtable ssp { | ||
| ; CHECK-ALL-LABEL: 'strong11' | ||
| ; CHECK-ALL-NEXT: Src: store i32 0, ptr %arrayidx, align 4 --> Dst: store i32 0, ptr %arrayidx, align 4 | ||
| ; CHECK-ALL-NEXT: da analyze - none! | ||
| ; | ||
| ; CHECK-STRONG-SIV-LABEL: 'strong11' | ||
| ; CHECK-STRONG-SIV-NEXT: Src: store i32 0, ptr %arrayidx, align 4 --> Dst: store i32 0, ptr %arrayidx, align 4 | ||
| ; CHECK-STRONG-SIV-NEXT: da analyze - consistent output [0 S]! | ||
| ; | ||
| entry: | ||
| br label %for.cond1.preheader | ||
|
|
||
| for.cond1.preheader: ; preds = %entry, %for.cond.cleanup3 | ||
| %i.017 = phi i64 [ 0, %entry ], [ %inc8, %for.cond.cleanup3 ] | ||
| %cmp5 = icmp samesign ult i64 %i.017, 3000000000 | ||
| %arrayidx = getelementptr inbounds nuw i32, ptr %A, i64 %i.017 | ||
| br i1 %cmp5, label %for.body4.us, label %for.cond.cleanup3 | ||
|
|
||
| for.body4.us: ; preds = %for.cond1.preheader, %for.body4.us | ||
| %j.016.us = phi i64 [ %inc.us, %for.body4.us ], [ 0, %for.cond1.preheader ] | ||
| store i32 0, ptr %arrayidx, align 4 | ||
| %inc.us = add nuw nsw i64 %j.016.us, 1 | ||
| %exitcond.not = icmp eq i64 %inc.us, 2147483640 | ||
| br i1 %exitcond.not, label %for.cond.cleanup3, label %for.body4.us | ||
|
|
||
| for.cond.cleanup: ; preds = %for.cond.cleanup3 | ||
| ret void | ||
|
|
||
| for.cond.cleanup3: ; preds = %for.body4.us, %for.cond1.preheader | ||
| %inc8 = add nuw nsw i64 %i.017, 1 | ||
| %exitcond19.not = icmp eq i64 %inc8, 9223372036854775806 | ||
| br i1 %exitcond19.not, label %for.cond.cleanup, label %for.cond1.preheader | ||
| } | ||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -12,19 +12,24 @@ | |
| ; A[2*i - 4] = 2; | ||
| ; } | ||
| ; | ||
| ; FIXME: DependenceAnalysis currently detects no dependency between the two | ||
| ; stores, but it does exist. For example, each store will access A[0] when i | ||
| ; is 1 and 2 respectively. | ||
| ; The root cause is that the product of the BTC and the coefficient | ||
| ; ((1LL << 62) - 1 and 2) overflows in a signed sense. | ||
|
Comment on lines
-15
to
-19
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why did you rewrite this comment? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Because now the issue that has been mentioned in the comment regarding the overflow in the product of the BTC and the coefficient is resolved. By this patch, Strong SIV is generating the expected output There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This test is not the same as There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I am not sure what you mean. Please clarify your comment on this change. No it is not same as There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
But the comment is now saying There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Thanks for noticing. Overlooked it. Now it is fixed. |
||
| ; FIXME: DependenceAnalysis fails to detect the dependency between A[i] and | ||
| ; itself, while Strong SIV has been able to prove it. | ||
| define void @strongsiv_const_ovfl(ptr %A) { | ||
| ; CHECK-LABEL: 'strongsiv_const_ovfl' | ||
| ; CHECK-NEXT: Src: store i8 1, ptr %gep.0, align 1 --> Dst: store i8 1, ptr %gep.0, align 1 | ||
| ; CHECK-NEXT: da analyze - none! | ||
| ; CHECK-NEXT: Src: store i8 1, ptr %gep.0, align 1 --> Dst: store i8 2, ptr %gep.1, align 1 | ||
| ; CHECK-NEXT: da analyze - none! | ||
| ; CHECK-NEXT: Src: store i8 2, ptr %gep.1, align 1 --> Dst: store i8 2, ptr %gep.1, align 1 | ||
| ; CHECK-NEXT: da analyze - none! | ||
| ; CHECK-ALL-LABEL: 'strongsiv_const_ovfl' | ||
| ; CHECK-ALL-NEXT: Src: store i8 1, ptr %gep.0, align 1 --> Dst: store i8 1, ptr %gep.0, align 1 | ||
| ; CHECK-ALL-NEXT: da analyze - none! | ||
| ; CHECK-ALL-NEXT: Src: store i8 1, ptr %gep.0, align 1 --> Dst: store i8 2, ptr %gep.1, align 1 | ||
| ; CHECK-ALL-NEXT: da analyze - none! | ||
| ; CHECK-ALL-NEXT: Src: store i8 2, ptr %gep.1, align 1 --> Dst: store i8 2, ptr %gep.1, align 1 | ||
| ; CHECK-ALL-NEXT: da analyze - none! | ||
| ; | ||
| ; CHECK-STRONG-SIV-LABEL: 'strongsiv_const_ovfl' | ||
| ; CHECK-STRONG-SIV-NEXT: Src: store i8 1, ptr %gep.0, align 1 --> Dst: store i8 1, ptr %gep.0, align 1 | ||
| ; CHECK-STRONG-SIV-NEXT: da analyze - none! | ||
| ; CHECK-STRONG-SIV-NEXT: Src: store i8 1, ptr %gep.0, align 1 --> Dst: store i8 2, ptr %gep.1, align 1 | ||
| ; CHECK-STRONG-SIV-NEXT: da analyze - consistent output [1]! | ||
| ; CHECK-STRONG-SIV-NEXT: Src: store i8 2, ptr %gep.1, align 1 --> Dst: store i8 2, ptr %gep.1, align 1 | ||
| ; CHECK-STRONG-SIV-NEXT: da analyze - none! | ||
| ; | ||
| entry: | ||
| br label %loop.header | ||
|
|
@@ -64,5 +69,4 @@ exit: | |
| ret void | ||
| } | ||
| ;; NOTE: These prefixes are unused and the list is autogenerated. Do not add tests below this line: | ||
| ; CHECK-ALL: {{.*}} | ||
| ; CHECK-STRONG-SIV: {{.*}} | ||
| ; CHECK: {{.*}} | ||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Does
Consistentneed to be set to false?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, otherwise we will add the
Consistentattribute to a few test cases that do not currently have this attribute. As you are also aware, the attributeConsistentseems to not be well defined. If it is true, we may need to try to remove it in other patches.