Skip to content
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

Fix InitialSeeds for IFDS #632

Merged
merged 2 commits into from
Jun 18, 2023
Merged

Fix InitialSeeds for IFDS #632

merged 2 commits into from
Jun 18, 2023

Conversation

fabianbs96
Copy link
Member

The default edge value of the InitialSeeds for IFDS analyses is TOP (the bottom value of the binary lattice) indicating "no information". This is incorrect as holding IFDS dataflow facts semantically have to be annotated with the top value of the binary lattice, which is called BOTTOM in phasar.
This issue prevents the IDESolver from computing IFDS results at certain call sites.

This PR solves that problem by correctly assigning the BOTTOM edge value to the initial seeds of IFDS analyses.

Should fix #629.

@fabianbs96 fabianbs96 requested a review from MMory as a code owner June 17, 2023 12:52
@fabianbs96 fabianbs96 self-assigned this Jun 17, 2023
@fabianbs96 fabianbs96 added the bug Something isn't working label Jun 17, 2023
@Luweicai
Copy link

Hi, @fabianbs96. This patch fix the problem that preventing the IDESolver from computing IFDS results at certain call sites.

But it seems casue a new problem: the new generated fact will have the value of TOP at no called position.

%1 = add nsw i32 %0, 1;
%2 = add nsw i32 %1, 1;
call void @tt(i32 %3);
%5 = add nsw i32 %4, 1;

The result is:

N: %1 = add nsw i32 %0, 1;
-----------------------------------------------------
D: @zero_value | V: BOTTOM
D: i32 %0 | V: BOTTOM

N: %2 = add nsw i32 %1, 1;
-----------------------------------------------------
D: @zero_value | V: BOTTOM
D: i32 %0 | V: TOP
%1 = add nsw i32 %0, 1; | V: TOP

N: call void @tt(i32 %3);
-----------------------------------------------------
D: @zero_value | V: BOTTOM
D: i32 %0 | V: BOTTOM
%1 = add nsw i32 %0, 1; | V: BOTTOM

N: %5 = add nsw i32 %4, 1;
-----------------------------------------------------
D: @zero_value | V: BOTTOM
D: i32 %0 | V: TOP
D: %1 = add nsw i32 %0, 1; | V: TOP
D: %2 = add nsw i32 %1, 1; | V: TOP

Copy link
Member

@MMory MMory left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

lgtm, thanks!

@MMory MMory merged commit 6d1ef70 into development Jun 18, 2023
@MMory MMory deleted the f-FixInitialSeedsForIFDS branch June 18, 2023 11:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Possible error in function resultatinLLVMSSA()
3 participants