Skip to content

feat(dataflow): sparse fact api#859

Open
axelcool1234 wants to merge 3 commits into
opencompl:mainfrom
axelcool1234:sparse-fact-api
Open

feat(dataflow): sparse fact api#859
axelcool1234 wants to merge 3 commits into
opencompl:mainfrom
axelcool1234:sparse-fact-api

Conversation

@axelcool1234

@axelcool1234 axelcool1234 commented Jun 12, 2026

Copy link
Copy Markdown
Collaborator

The following is a type that builds off of the generic Fact type. You can define "sparse facts" - facts that attach to Values, using this type. It'll handle notifying dependents and subscribed analyses for you when it changes.

@axelcool1234 axelcool1234 marked this pull request as draft June 12, 2026 03:53
@axelcool1234 axelcool1234 force-pushed the sparse-fact-api branch 3 times, most recently from 4bd5d12 to abbbe5e Compare June 12, 2026 06:57
@axelcool1234 axelcool1234 marked this pull request as ready for review June 12, 2026 19:33
@axelcool1234 axelcool1234 requested a review from math-fehr June 12, 2026 19:33
Comment thread Veir/Analysis/DataFlow/Facts.lean Outdated
@axelcool1234 axelcool1234 force-pushed the sparse-fact-api branch 3 times, most recently from 9c78f96 to d642161 Compare June 12, 2026 23:13
Comment on lines +34 to +55
/--
Propagate a sparse lattice update by revisiting dependents and all users of the
updated SSA value for subscribed analyses.
-/
def propagate (state : Fact kind) (anchor : LatticeAnchor)
(dfCtx : DataFlowContext) (irCtx : IRContext OpCode) : DataFlowContext := Id.run do
let mut dfCtx := { dfCtx with workList := state.enqueueDependents dfCtx.workList }
match anchor with
| .ValuePtr ssaValue =>
let mut maybeUse := ssaValue.getFirstUse! irCtx
while let some use := maybeUse do
let user := (use.get! irCtx).owner
for analysisKind in state.subscribers do
match InsertPoint.after? user irCtx with
| some point =>
dfCtx := dfCtx.enqueue (point, analysisKind)
| none =>
pure ()
maybeUse := (use.get! irCtx).nextUse
| _ =>
pure ()
dfCtx

@axelcool1234 axelcool1234 Jun 12, 2026

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

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

@math-fehr Here is an example of subscribers being used. For any fact that attaches to SSA Values, it enqueues into the worklist all of its uses for each subscribed analysis whenever said SSA fact changes. That's because its uses will be affected by that change. Analyses concerned about said change of this fact will be subscribed so that it can run its transfer function on the uses.

@axelcool1234 axelcool1234 marked this pull request as draft June 13, 2026 17:34
@axelcool1234 axelcool1234 marked this pull request as ready for review June 13, 2026 23:55
@axelcool1234

Copy link
Copy Markdown
Collaborator Author

Cc @math-fehr @regehr @ineol this is the first step towards supporting transfer functions on SSA values, which is what John is mostly concerned with. I need some review of this code, thank you 🙏

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.

2 participants