Skip to content
This repository was archived by the owner on Apr 1, 2025. It is now read-only.
This repository was archived by the owner on Apr 1, 2025. It is now read-only.

Abstract domains can’t model sequencing #56

@robrix

Description

@robrix

We currently assume that two statements in a sequence are completely unrelated, e.g.:

def foo
  a
  b
end

Here, a and b are indeed orthogonal, but the result of foo isn’t just determined by b, as it would be in a pure language, but rather by the effects performed by both a and b. In other words, treating statement blocks as simply returning their final value means that we’re losing the ability to model important properties using the abstract domain. This has real consequences for us, in that computing the call graph requires us to manually inspect syntax, instead of e.g. representing values as sets of referenced symbols, unioned together.

If our abstract domain had a sequencing operation, akin to the *> method for Applicatives, we could move a lot of out-of-band inspection of syntax into the representation of the domain, resulting in a simpler, more direct implementation for many analyses.

This will additionally be necessary to correctly model type & effect systems.

Metadata

Metadata

Assignees

Labels

analysisgeneral program analysis (e.g. abstract interpretation) issuesbugSomething isn't working

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions