Skip to content

Dataflow Analysis Framework - #264

Merged
math-fehr merged 3 commits into
opencompl:mainfrom
axelcool1234:dataflow-framework
May 19, 2026
Merged

Dataflow Analysis Framework#264
math-fehr merged 3 commits into
opencompl:mainfrom
axelcool1234:dataflow-framework

Conversation

@axelcool1234

@axelcool1234 axelcool1234 commented Mar 3, 2026

Copy link
Copy Markdown
Collaborator

The following is a dataflow analysis framework based off the C++ MLIR implementation.

An analysis I've implemented on top of the framework is SCCP: #456

@axelcool1234
axelcool1234 marked this pull request as draft March 3, 2026 01:53
@axelcool1234 axelcool1234 mentioned this pull request Mar 3, 2026
@axelcool1234
axelcool1234 force-pushed the dataflow-framework branch 3 times, most recently from c864fea to fa278ba Compare March 30, 2026 14:25
@axelcool1234

axelcool1234 commented Mar 30, 2026

Copy link
Copy Markdown
Collaborator Author

Wishlist:

  • A way to check if an op is a "branching" one. Parallel to MLIR's RegionBranchOpInterface
  • A way to check if an op is a callable one. Parallel to MLIR's CallableOpInterface
  • A constant folder
  • replaceAllUsesWith
  • replaceWithConstant

Without the first three, I have to manually write out the ops I know that fits them. I already did so for SparseConstantPropagationAnalysis with manual constant folding.

I need a way to see if an op is region branching or callable to complete DeadCodeAnalysis and SparseForwardDataFlowAnalysis.

These are the last of the hurdles before I have a working SCCP transform :)

Other things I need to investigate:

  • DeadCodeAnalysis deals with symbol tables. Not sure what that's about - our codebase doesn't have any of that. Not sure if it's necessary at this stage.
  • DeadCodeAnalysis stores an analysisScope object. DataFlowAnalysiss are usually without state. Not sure if there's a way around this - need to look more into the purpose of this object.

Other things I have to do:

  • Better documentation (also deal with writing doc comments instead of regular comments)
  • Write a guide for John so he can try implementing KnownBits.

@axelcool1234
axelcool1234 force-pushed the dataflow-framework branch 3 times, most recently from 34bfa9b to b498c68 Compare April 12, 2026 08:09
@axelcool1234 axelcool1234 changed the title Draft: Dataflow Analysis Framework Dataflow Analysis Framework Apr 22, 2026
@axelcool1234
axelcool1234 marked this pull request as ready for review April 22, 2026 23:26
@axelcool1234
axelcool1234 force-pushed the dataflow-framework branch 3 times, most recently from aceaecd to 63c8e4a Compare April 23, 2026 01:14

@math-fehr math-fehr left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Sorry for the delay!
I think what would help a lot reviewing this is adding more documentation on the later part of the Veir/Analysis/DataFlowFramework.lean file.
Maybe adding a markdown documentation (/-! -/) at the beginning of the function to explain the relationship between the different structures?

Otherwise, the main issue I see right now is the structures that are using your Dynamic types. Do you think you can see a way to define them with a mutual somehow? If you don't, we can try to look into it.

Comment thread Veir/Analysis/DataFlowFramework.lean Outdated
Comment thread Veir/Analysis/DataFlowFramework.lean Outdated
Comment thread Veir/Analysis/DataFlowFramework.lean Outdated
Comment thread Veir/Analysis/DataFlowFramework.lean Outdated
Comment thread Veir/Analysis/DataFlowFramework.lean Outdated
Comment thread Veir/Analysis/DataFlowFramework.lean Outdated
Comment thread Veir/Analysis/DataFlowFramework.lean Outdated
Comment thread Veir/Analysis/DataFlowFramework.lean Outdated
Comment thread UnitTest/DataFlowFramework.lean
Comment thread UnitTest/DataFlowFramework.lean
@axelcool1234

axelcool1234 commented Apr 25, 2026

Copy link
Copy Markdown
Collaborator Author

Thank you for the review comments. I'll try to get back to them as soon as I can (my laptop decided to have some hardware issues so it might be a second, but I will get to them). I apologize for the poor documentation (I'm still getting used to collaborating with others - didn't have much of that at this scale in my undergrad unfortunately). I should've done an additional once over my PRs and ensure I've commented on everything for better clarity. I'll make sure to do that as well.

I will also reconsider the structure of the framework as a whole now that I have a strong understanding of how the original MLIR version that this is mirroring works. I have a couple of ideas of some restructuring that should eliminate the strange hacks/workarounds and make this simpler. Once I get my laptop up and working I will work on a proposal for this via an additional commit.

@axelcool1234
axelcool1234 force-pushed the dataflow-framework branch 3 times, most recently from dab903d to 91b99f4 Compare May 4, 2026 05:11
@axelcool1234

axelcool1234 commented May 4, 2026

Copy link
Copy Markdown
Collaborator Author

@math-fehr @ineol I have pushed the changes I've mentioned in our last meeting! This should be cleaner I hope.

I think I need to think about how to organize the Analysis/ folder - I currently have this strange split between DataFlowFramework.lean and Facts.lean (which is a misleading name for the file as it's doing more than just fact related stuff) to prevent import cycles.

@math-fehr math-fehr left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Nice! It looks much much better now!
I just added comments mostly about documentation and naming!

I guess to me the biggest question is wether or not some class should be structure instead, like HasFactKind (which I'm not 100% sure I understand what it does). Other than that, the structure looks good now to me!

Comment thread Veir/Analysis/DataFlow/Facts.lean Outdated
Comment thread Veir/Analysis/DataFlow/Facts.lean Outdated
Comment thread Veir/Analysis/DataFlow/Facts.lean Outdated
Comment thread Veir/Analysis/DataFlow/Facts.lean
Comment thread Veir/Analysis/DataFlow/Facts.lean
Comment thread Veir/Analysis/DataFlowFramework.lean Outdated
Comment thread Veir/Analysis/DataFlowFramework.lean Outdated
Comment thread Veir/Analysis/DataFlowFramework.lean Outdated
Comment thread Veir/Analysis/DataFlowFramework.lean Outdated
Comment thread Veir/Analysis.lean Outdated
Comment thread Veir/Analysis/DataFlow/Facts.lean Outdated
Comment thread Veir/Analysis/DataFlow/Facts.lean Outdated
Comment thread Veir/Analysis/DataFlow/Facts.lean Outdated
@axelcool1234
axelcool1234 force-pushed the dataflow-framework branch 12 times, most recently from bc7a2eb to 6796750 Compare May 8, 2026 06:59

@math-fehr math-fehr left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Okay that looks much much better again, nice!
I added some comments for documentation (mostly places where I feel it is harder to understand what's going on).
I'll wait that @ineol reviews it (probably early next week), and to me that should be probably good to go after that!

Comment thread Veir/Analysis/DataFlow/Domains.lean
Comment thread Veir/Analysis/DataFlow/Facts.lean
Comment thread Veir/Analysis/DataFlowFramework.lean
Comment thread Veir/Analysis/DataFlowFramework.lean
Comment thread Veir/Analysis/DataFlowFramework.lean
Comment thread Veir/Analysis/DataFlowFramework.lean
Comment thread Veir/Analysis/DataFlowFramework.lean
@axelcool1234
axelcool1234 force-pushed the dataflow-framework branch 3 times, most recently from c984f33 to fb158fc Compare May 19, 2026 03:12
Comment thread Veir/Analysis/DataFlowFramework.lean
@math-fehr
math-fehr added this pull request to the merge queue May 19, 2026
Merged via the queue into opencompl:main with commit 39cdb37 May 19, 2026
3 of 4 checks passed
alexanderlhicks added a commit to alexanderlhicks/veir that referenced this pull request May 21, 2026
Brings in 32 upstream commits including the Dataflow Analysis Framework
(opencompl#264), VariableState interpreter fix (opencompl#599), parser improvements,
fieldsInBounds_unchanged hypothesis cleanup (opencompl#539), and VEIR_ROUNDTRIP
infrastructure (opencompl#605).

Toolchain conflict: upstream bumped to nightly-2026-05-17 in opencompl#595;
we keep v4.30.0-rc2 to stay compatible with the Mathlib olean cache
fetched in Phase E.5.

Resolved conflicts:
- lean-toolchain: kept v4.30.0-rc2
- Test/lit.cfg: union (kept LLZK_OPT propagation + %scripts substitution
  from ours; took .c suffix, lit.util feature detection, VEIR_ROUNDTRIP
  substitution from upstream)
- Veir/Parser/AttrParser.lean: adapted FeltConstAttr + felt-type parser
  to upstream's new ParserError type (s/throw/throwString/g for string
  literals, in our LLZK-specific additions)

Post-merge state:
- lake build: clean (2563 jobs)
- lake test: clean (122/122)
- lit (no LLZK_OPT): 347 PASS / 9 UNSUPPORTED / 0 FAIL (356 total)
- lit (LLZK_OPT): 355 PASS / 1 UNSUPPORTED / 0 XFAIL / 0 FAIL
- quality gates: all pass

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
axelcool1234 added a commit to axelcool1234/veir that referenced this pull request May 29, 2026
This implements CFG dominance analysis on top of the dataflow framework:
opencompl#264

This is based off of the Cooper-Harvey-Kennedy algorithm.

---------

Co-authored-by: John Regehr <regehr@cs.utah.edu>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants