Skip to content

Fix InitialSeeds for IFDS#632

Merged
MMory merged 2 commits into
developmentfrom
f-FixInitialSeedsForIFDS
Jun 18, 2023
Merged

Fix InitialSeeds for IFDS#632
MMory merged 2 commits into
developmentfrom
f-FixInitialSeedsForIFDS

Conversation

@fabianbs96
Copy link
Copy Markdown
Member

@fabianbs96 fabianbs96 commented Jun 17, 2023

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 mentioned this pull request Jun 17, 2023
Closed
@fabianbs96 fabianbs96 added the bug Something isn't working label Jun 17, 2023
@Luweicai
Copy link
Copy Markdown

Luweicai commented Jun 18, 2023

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

MMory
MMory approved these changes Jun 18, 2023
View reviewed changes
Copy link
Copy Markdown
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

Reviewers

@MMory MMory MMory approved these changes

Assignees

@fabianbs96 fabianbs96

Labels

bug Something isn't working

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Possible error in function resultatinLLVMSSA()

3 participants

@fabianbs96 @Luweicai @MMory