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.

Sign up for GitHub

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

Jump to bottom

Introduce backward analysis to dataflow framework. #3370

Merged
merged 22 commits into from
Jun 30, 2020
Merged

Introduce backward analysis to dataflow framework. #3370

merged 22 commits into from
Jun 30, 2020

Conversation

xingweitian
Copy link
Member

@xingweitian xingweitian commented Jun 13, 2020 •
edited
Loading

Refactor dataflow framework. Change Analysis to be an interface, and add AbstractAnalysis,
ForwardAnalysis, ForwardTransferFunction, ForwardAnalysisImpl, BackwardAnalysis, BackwardTransferFunction, and BackwardAnalysisImpl.

Live variable analysis is also added in #3371 to show that the introduced backward analysis can work.

Co-authored-by: Charles Chen Charleszhuochen@gmail.com

@xingweitian @CharlesZ-Chen
Refactor dataflow framework. Introduce backward analysis.
737e03e 
Co-authored-by: Charles Chen <Charleszhuochen@gmail.com>
@xingweitian xingweitian added the Breaking change Breaks some clients. Requires minor version number increase (middle number in the version number). label Jun 13, 2020
This was referenced Jun 13, 2020
Merged
Closed
@smillst smillst self-assigned this Jun 15, 2020
kelloggm
kelloggm requested changes Jun 16, 2020
View reviewed changes
Copy link
Contributor

@kelloggm kelloggm left a comment

Choose a reason for hiding this comment

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

Thanks for building this - I think it will be really useful going forward for implementing new kinds of analyses! I have two primary concerns (one of which is more about #3371, which I've also read):

  1. Why doesn't the backwards analysis have support for a widening operator? I don't think one is needed to correctly implement live-variable analysis, but many other interesting dataflow problems that one might want to express as backwards analyses will need one.
  2. The live-variable analysis that Add live variable analysis to dataflow framework. #3371 implements is never tested, so I don't know how you've established that it is actually working. Can you add some tests that show that the live-variable analysis gets the correct results? That will also help us establish confidence that the implementation of backwards analysis here is correct.

I also left some minor comments on documentation and style.

dataflow/src/main/java/org/checkerframework/dataflow/analysis/Analysis.java Outdated Show resolved Hide resolved
dataflow/src/main/java/org/checkerframework/dataflow/analysis/Analysis.java Outdated Show resolved Hide resolved
dataflow/src/main/java/org/checkerframework/dataflow/analysis/Analysis.java Outdated Show resolved Hide resolved
dataflow/src/main/java/org/checkerframework/dataflow/analysis/Analysis.java Outdated Show resolved Hide resolved
dataflow/src/main/java/org/checkerframework/dataflow/analysis/AnalysisResult.java Outdated Show resolved Hide resolved
dataflow/src/main/java/org/checkerframework/dataflow/analysis/ForwardAnalysisImpl.java Show resolved Hide resolved
@smillst smillst assigned xingweitian and unassigned smillst Jun 16, 2020
@xingweitian
Resolve comments.
066c7d3 
Reduce the differences between forward and backward analysis implementation.
@xingweitian
Merge remote-tracking branch 'typetools/master' into typetools-backwa…
720123f 
…rd-analysis
@xingweitian
Remove unused import.
0d8664d
@xingweitian
Copy link
Member Author

@kelloggm Thanks for the review and helpful comments!

Why doesn't the backwards analysis have support for a widening operator? I don't think one is needed to correctly implement live-variable analysis, but many other interesting dataflow problems that one might want to express as backwards analyses will need one.

I agree with you: backward analysis can support widening. In the previous code review of this pull request in opprop, @wmdietl and I decided to support widening for backward analysis in the future: opprop#99 (comment)

The live-variable analysis that #3371 implements is never tested, so I don't know how you've established that it is actually working. Can you add some tests that show that the live-variable analysis gets the correct results? That will also help us establish confidence that the implementation of backwards analysis here is correct.

Currently, I use LiveVariablePlayground to test the correctness of the live variable analysis and backward analysis: run the playground with a java file to generate a control flow graph. Then, I check the live variable information of each block to see whether it is correct.

I discussed with @wmdietl today, I will also try to create some test cases to test with live variable analysis and backward analysis.

@kelloggm
Copy link
Contributor

I agree with you: backward analysis can support widening. In the previous code review of this pull request in opprop, @wmdietl and I decided to support widening for backward analysis in the future: opprop#99 (comment)

Thanks for the context on this. I suspect we will eventually need it, but keeping the first pull request simple is a good idea. Can you document somewhere in the code (probably in the Javadoc for BackwardsAnalysisImpl, but possibly elsewhere) that adding widening support in the same way that the forwards analysis supports widening is future work?

Currently, I use LiveVariablePlayground to test the correctness of the live variable analysis and backward analysis: run the playground with a java file to generate a control flow graph. Then, I check the live variable information of each block to see whether it is correct.
I discussed with @wmdietl today, I will also try to create some test cases to test with live variable analysis and backward analysis.

Adding automated versions of those tests will really improve these PRs.

@xingweitian xingweitian mentioned this pull request Jun 17, 2020
Closed
@xingweitian xingweitian assigned kelloggm and unassigned xingweitian Jun 26, 2020
@xingweitian
Copy link
Member Author

I agree with you: backward analysis can support widening. In the previous code review of this pull request in opprop, @wmdietl and I decided to support widening for backward analysis in the future: opprop#99 (comment)

Thanks for the context on this. I suspect we will eventually need it, but keeping the first pull request simple is a good idea. Can you document somewhere in the code (probably in the Javadoc for BackwardsAnalysisImpl, but possibly elsewhere) that adding widening support in the same way that the forwards analysis supports widening is future work?

Currently, I use LiveVariablePlayground to test the correctness of the live variable analysis and backward analysis: run the playground with a java file to generate a control flow graph. Then, I check the live variable information of each block to see whether it is correct.
I discussed with @wmdietl today, I will also try to create some test cases to test with live variable analysis and backward analysis.

Adding automated versions of those tests will really improve these PRs.

Hi @kelloggm, I have added a test case for live variable analysis in #3371, could you please have a look? Thanks!

kelloggm
kelloggm approved these changes Jun 26, 2020
View reviewed changes
Copy link
Contributor

@kelloggm kelloggm left a comment

Choose a reason for hiding this comment

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

Thanks for these changes and the test case in #3371. I had one minor comment on documentation, but there is no need for me to review this again once that is addressed unless my understanding is wrong.

dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java Outdated Show resolved Hide resolved
@smillst smillst assigned smillst and unassigned kelloggm Jun 29, 2020
@smillst smillst added this to the Critical milestone Jun 29, 2020
smillst
smillst approved these changes Jun 30, 2020
View reviewed changes
Copy link
Member

@smillst smillst left a comment

Choose a reason for hiding this comment

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

I have one minor comment. I also tried to push some minor tweaks, but I did not have permission. Please merge xingweitian#13.

dataflow/src/main/java/org/checkerframework/dataflow/analysis/BackwardAnalysisImpl.java Outdated Show resolved Hide resolved
@smillst smillst assigned xingweitian and unassigned smillst Jun 30, 2020
@xingweitian xingweitian assigned smillst and unassigned xingweitian Jun 30, 2020
@smillst smillst merged commit e8bbd7f into typetools:master Jun 30, 2020
@xingweitian xingweitian deleted the typetools-backward-analysis branch June 30, 2020 19:20
@xingweitian xingweitian mentioned this pull request Jul 1, 2020
Merged
smillst pushed a commit that referenced this pull request Jul 1, 2020
@xingweitian
Add live variable analysis to dataflow framework. (#3371)
7558863 
 This PR added live variable analysis to the dataflow framework aiming to show #3370's backward analysis works properly.

Co-authored-by: Charles Chen Charleszhuochen@gmail.com
smillst pushed a commit that referenced this pull request Jul 23, 2020
@xingweitian
Correct the logic of dataflow framework. (#3414)
bc9a120 
BackwardAnalysis:
1. Add exception block's predecessor exception block to inputs (fix null pointer exception).
2. When running `runAnalysisFor()` with an exception block, pass a copied transfer input to `callTransferFunction()`.

ForwardAnalysis:
1. When running `runAnalysisFor()` with an exception block, pass a copied transfer input to `callTransferFunction()`. In the previous dataflow framework (before #3370), we passed a non-copied transfer input (https://github.com/typetools/checker-framework/pull/3370/files#diff-d4108228a0a5407e00c090c2e97d8b6dL401-L402). This seems a bug existing in the old dataflow framework.

Resolves #3447.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@mernst mernst mernst left review comments

@wmdietl wmdietl wmdietl left review comments

@kelloggm kelloggm kelloggm approved these changes

@smillst smillst smillst approved these changes

Assignees

@smillst smillst

Labels
Breaking change Breaks some clients. Requires minor version number increase (middle number in the version number).
Projects
None yet
Milestone
Critical
Development

Successfully merging this pull request may close these issues.
5 participants
@xingweitian @kelloggm @mernst @wmdietl @smillst