RFC: custom type lattice and more generic abstract interpreter #40992
Comments
|
Another use case is verifying array shapes for numerical/ML programming, and offloading to restricted accelerators like TPUs. Prior art: https://arxiv.org/abs/2102.13254 |
aviatesk
added a commit
to aviatesk/JET.jl
that referenced
this issue
Jun 3, 2021
This is an alternative for #204, and will supersedes it. This PR setups both `ReportPass` and `AbstractAnalyzer` interfaces. The former allow us to extensibly customize JET's default analysis (error detection), and the latter enables us to implement arbitrary pluggable analysis. By using `ReportPass` interface, now users can set up new report construction logic, ignore existing reports, etc., by implementing a new report pass. By default, JET implements `BasicPass<:ReportPass` and `SoundPass<:ReportPass`, which I believe their names are enough descriptive, but the latter is still in very WIP. The `AbstractAnalyzer` interface allows more extensive customization, and enables pluggable analysis as requested #169. Now we can implement arbitrary new analyzer, which may implement its own abstract interpretation based analysis, while still utilizing JET's report cache logic and top-level analysis logic, etc. The example plugin analyzers are kept in `/examples` directory, and also included into the documentation. One limitation to notice is that we still can't implement our own lattice logic, and thus the `AbstractAnalyzer` interface can't analyze stuff that can't be expressed by the lattice implementation designed for type inference and optimization performed by Julia compiler. This should be addressed in upstream, especially as requested at <JuliaLang/julia#40992> --- The changes are kinda really big, and so I focused on coding in this PR and leave documentation update and more example implementations to another PR. Also now TOML based configuration won't fit given the overload-based customizations enabled by this PR, so we will move to Julia format based configuration support in the future. --- * fix #203, setup report passes, enable customized report strategies * fix #169, implement experimental pluggable analysis interface (#209) * fix #169, implement experimental pluggable analysis interface * example: find_unstable_api.jl * wip: include plugins documentation * setup `JETInterfaces`, which allows to use the pluggable analysis framework more easily * API docs * add simple tests for the pluggable-analysis framework
|
i'd also like this: i can see a future where symbolics.jl and julia's compiler slowly converge to allow for really impressive symbolic programming basically built in to the language. also being able to write a bunch of pluggable type checkers would be the next level of linting. being able to add herbie would be killer |
|
I played with this a bit. Core.Compiler changes are on the kf/customlattice branch and the user code is in |
Keno
added a commit
that referenced
this issue
Aug 29, 2022
There's been two threads of work involving the compiler's notion of the inference lattice. One is that the lattice has gotten to complicated and with too many internal constraints that are not manifest in the type system. #42596 attempted to address this, but it's quite disruptive as it changes the lattice types and all the signatures of the lattice operations, which are used quite extensively throughout the ecosystem (despite being internal), so that change is quite disruptive (and something we'd ideally only make the ecosystem do once). The other thread of work is that people would like to experiment with a variety of extended lattices outside of base (either to prototype potential additions to the lattice in base or to do custom abstract interpretation over the julia code). At the moment, the lattice is quite closely interwoven with the rest of the abstract interpreter. In response to this request in #40992, I had proposed a `CustomLattice` element with callbacks, but this doesn't compose particularly well, is cumbersome and imposes overhead on some of the hottest parts of the compiler, so it's a bit of a tough sell to merge into Base. In this PR, I'd like to propose a refactoring that is relatively non-invasive to non-Base users, but I think would allow easier experimentation with changes to the lattice for these two use cases. In essence, we're splitting the lattice into a ladder of 5 different lattices, each containing the previous lattice as a sub-lattice. These 5 lattices are: - JLTypeLattice (Anything that's a `Type`) - ConstsLattice ( + `Const`, `PartialTypeVar`) - PartialsLattice ( + `PartialStruct` ) - ConditionalsLattice ( + `Conditional` ) - InferenceLattice ( + `LimitedAccuracy`, `MaybeUndef` ) The idea is that where a lattice element contains another lattice element (e.g. in `PartialStruct` or `Conditional`), the element contained may only be from a wider lattice. In this PR, this is not enforced by the type system. This is quite deliberate, as I want to retain the types and object layouts of the lattice elements, but of course a future #42596-like change could add such type enforcement. Of particular note is that the `PartialsLattice` and `ConditionalsLattice` is parameterized and additional layers may be added in the stack. For example, in #40992, I had proposed a lattice element that refines `Int` and tracks symbolic expressions. In this setup, this could be accomplished by adding an appropriate lattice in between the `ConstsLattice` and the `PartialsLattice` (of course, additional hooks would be required to make the tfuncs work, but that is outside the scope of this PR). I don't think this is a full solution, but I think it'll help us play with some of these extended lattice options over the next 6-12 months in the packages that want to do this sort of thing. Presumably once we know what all the potential lattice extensions look like, we will want to take another look at this (likely together with whatever solution we come up with for the AbstractInterpreter composability problem and a rebase of #42596). WIP because I didn't bother updating and plumbing through the lattice in all the call sites yet, but that's mostly mechanical, so if we like this direction, I will make that change and hope to merge this in short order (because otherwise it'll accumulate massive merge conflicts).
Keno
added a commit
that referenced
this issue
Aug 31, 2022
There's been two threads of work involving the compiler's notion of the inference lattice. One is that the lattice has gotten to complicated and with too many internal constraints that are not manifest in the type system. #42596 attempted to address this, but it's quite disruptive as it changes the lattice types and all the signatures of the lattice operations, which are used quite extensively throughout the ecosystem (despite being internal), so that change is quite disruptive (and something we'd ideally only make the ecosystem do once). The other thread of work is that people would like to experiment with a variety of extended lattices outside of base (either to prototype potential additions to the lattice in base or to do custom abstract interpretation over the julia code). At the moment, the lattice is quite closely interwoven with the rest of the abstract interpreter. In response to this request in #40992, I had proposed a `CustomLattice` element with callbacks, but this doesn't compose particularly well, is cumbersome and imposes overhead on some of the hottest parts of the compiler, so it's a bit of a tough sell to merge into Base. In this PR, I'd like to propose a refactoring that is relatively non-invasive to non-Base users, but I think would allow easier experimentation with changes to the lattice for these two use cases. In essence, we're splitting the lattice into a ladder of 5 different lattices, each containing the previous lattice as a sub-lattice. These 5 lattices are: - JLTypeLattice (Anything that's a `Type`) - ConstsLattice ( + `Const`, `PartialTypeVar`) - PartialsLattice ( + `PartialStruct` ) - ConditionalsLattice ( + `Conditional` ) - InferenceLattice ( + `LimitedAccuracy`, `MaybeUndef` ) The idea is that where a lattice element contains another lattice element (e.g. in `PartialStruct` or `Conditional`), the element contained may only be from a wider lattice. In this PR, this is not enforced by the type system. This is quite deliberate, as I want to retain the types and object layouts of the lattice elements, but of course a future #42596-like change could add such type enforcement. Of particular note is that the `PartialsLattice` and `ConditionalsLattice` is parameterized and additional layers may be added in the stack. For example, in #40992, I had proposed a lattice element that refines `Int` and tracks symbolic expressions. In this setup, this could be accomplished by adding an appropriate lattice in between the `ConstsLattice` and the `PartialsLattice` (of course, additional hooks would be required to make the tfuncs work, but that is outside the scope of this PR). I don't think this is a full solution, but I think it'll help us play with some of these extended lattice options over the next 6-12 months in the packages that want to do this sort of thing. Presumably once we know what all the potential lattice extensions look like, we will want to take another look at this (likely together with whatever solution we come up with for the AbstractInterpreter composability problem and a rebase of #42596). WIP because I didn't bother updating and plumbing through the lattice in all the call sites yet, but that's mostly mechanical, so if we like this direction, I will make that change and hope to merge this in short order (because otherwise it'll accumulate massive merge conflicts).
Keno
added a commit
that referenced
this issue
Aug 31, 2022
There's been two threads of work involving the compiler's notion of the inference lattice. One is that the lattice has gotten to complicated and with too many internal constraints that are not manifest in the type system. #42596 attempted to address this, but it's quite disruptive as it changes the lattice types and all the signatures of the lattice operations, which are used quite extensively throughout the ecosystem (despite being internal), so that change is quite disruptive (and something we'd ideally only make the ecosystem do once). The other thread of work is that people would like to experiment with a variety of extended lattices outside of base (either to prototype potential additions to the lattice in base or to do custom abstract interpretation over the julia code). At the moment, the lattice is quite closely interwoven with the rest of the abstract interpreter. In response to this request in #40992, I had proposed a `CustomLattice` element with callbacks, but this doesn't compose particularly well, is cumbersome and imposes overhead on some of the hottest parts of the compiler, so it's a bit of a tough sell to merge into Base. In this PR, I'd like to propose a refactoring that is relatively non-invasive to non-Base users, but I think would allow easier experimentation with changes to the lattice for these two use cases. In essence, we're splitting the lattice into a ladder of 5 different lattices, each containing the previous lattice as a sub-lattice. These 5 lattices are: - JLTypeLattice (Anything that's a `Type`) - ConstsLattice ( + `Const`, `PartialTypeVar`) - PartialsLattice ( + `PartialStruct` ) - ConditionalsLattice ( + `Conditional` ) - InferenceLattice ( + `LimitedAccuracy`, `MaybeUndef` ) The idea is that where a lattice element contains another lattice element (e.g. in `PartialStruct` or `Conditional`), the element contained may only be from a wider lattice. In this PR, this is not enforced by the type system. This is quite deliberate, as I want to retain the types and object layouts of the lattice elements, but of course a future #42596-like change could add such type enforcement. Of particular note is that the `PartialsLattice` and `ConditionalsLattice` is parameterized and additional layers may be added in the stack. For example, in #40992, I had proposed a lattice element that refines `Int` and tracks symbolic expressions. In this setup, this could be accomplished by adding an appropriate lattice in between the `ConstsLattice` and the `PartialsLattice` (of course, additional hooks would be required to make the tfuncs work, but that is outside the scope of this PR). I don't think this is a full solution, but I think it'll help us play with some of these extended lattice options over the next 6-12 months in the packages that want to do this sort of thing. Presumably once we know what all the potential lattice extensions look like, we will want to take another look at this (likely together with whatever solution we come up with for the AbstractInterpreter composability problem and a rebase of #42596). WIP because I didn't bother updating and plumbing through the lattice in all the call sites yet, but that's mostly mechanical, so if we like this direction, I will make that change and hope to merge this in short order (because otherwise it'll accumulate massive merge conflicts).
Keno
added a commit
that referenced
this issue
Aug 31, 2022
There's been two threads of work involving the compiler's notion of the inference lattice. One is that the lattice has gotten to complicated and with too many internal constraints that are not manifest in the type system. #42596 attempted to address this, but it's quite disruptive as it changes the lattice types and all the signatures of the lattice operations, which are used quite extensively throughout the ecosystem (despite being internal), so that change is quite disruptive (and something we'd ideally only make the ecosystem do once). The other thread of work is that people would like to experiment with a variety of extended lattices outside of base (either to prototype potential additions to the lattice in base or to do custom abstract interpretation over the julia code). At the moment, the lattice is quite closely interwoven with the rest of the abstract interpreter. In response to this request in #40992, I had proposed a `CustomLattice` element with callbacks, but this doesn't compose particularly well, is cumbersome and imposes overhead on some of the hottest parts of the compiler, so it's a bit of a tough sell to merge into Base. In this PR, I'd like to propose a refactoring that is relatively non-invasive to non-Base users, but I think would allow easier experimentation with changes to the lattice for these two use cases. In essence, we're splitting the lattice into a ladder of 5 different lattices, each containing the previous lattice as a sub-lattice. These 5 lattices are: - JLTypeLattice (Anything that's a `Type`) - ConstsLattice ( + `Const`, `PartialTypeVar`) - PartialsLattice ( + `PartialStruct` ) - ConditionalsLattice ( + `Conditional` ) - InferenceLattice ( + `LimitedAccuracy`, `MaybeUndef` ) The idea is that where a lattice element contains another lattice element (e.g. in `PartialStruct` or `Conditional`), the element contained may only be from a wider lattice. In this PR, this is not enforced by the type system. This is quite deliberate, as I want to retain the types and object layouts of the lattice elements, but of course a future #42596-like change could add such type enforcement. Of particular note is that the `PartialsLattice` and `ConditionalsLattice` is parameterized and additional layers may be added in the stack. For example, in #40992, I had proposed a lattice element that refines `Int` and tracks symbolic expressions. In this setup, this could be accomplished by adding an appropriate lattice in between the `ConstsLattice` and the `PartialsLattice` (of course, additional hooks would be required to make the tfuncs work, but that is outside the scope of this PR). I don't think this is a full solution, but I think it'll help us play with some of these extended lattice options over the next 6-12 months in the packages that want to do this sort of thing. Presumably once we know what all the potential lattice extensions look like, we will want to take another look at this (likely together with whatever solution we come up with for the AbstractInterpreter composability problem and a rebase of #42596). WIP because I didn't bother updating and plumbing through the lattice in all the call sites yet, but that's mostly mechanical, so if we like this direction, I will make that change and hope to merge this in short order (because otherwise it'll accumulate massive merge conflicts).
Keno
added a commit
that referenced
this issue
Aug 31, 2022
There's been two threads of work involving the compiler's notion of the inference lattice. One is that the lattice has gotten to complicated and with too many internal constraints that are not manifest in the type system. #42596 attempted to address this, but it's quite disruptive as it changes the lattice types and all the signatures of the lattice operations, which are used quite extensively throughout the ecosystem (despite being internal), so that change is quite disruptive (and something we'd ideally only make the ecosystem do once). The other thread of work is that people would like to experiment with a variety of extended lattices outside of base (either to prototype potential additions to the lattice in base or to do custom abstract interpretation over the julia code). At the moment, the lattice is quite closely interwoven with the rest of the abstract interpreter. In response to this request in #40992, I had proposed a `CustomLattice` element with callbacks, but this doesn't compose particularly well, is cumbersome and imposes overhead on some of the hottest parts of the compiler, so it's a bit of a tough sell to merge into Base. In this PR, I'd like to propose a refactoring that is relatively non-invasive to non-Base users, but I think would allow easier experimentation with changes to the lattice for these two use cases. In essence, we're splitting the lattice into a ladder of 5 different lattices, each containing the previous lattice as a sub-lattice. These 5 lattices are: - JLTypeLattice (Anything that's a `Type`) - ConstsLattice ( + `Const`, `PartialTypeVar`) - PartialsLattice ( + `PartialStruct` ) - ConditionalsLattice ( + `Conditional` ) - InferenceLattice ( + `LimitedAccuracy`, `MaybeUndef` ) The idea is that where a lattice element contains another lattice element (e.g. in `PartialStruct` or `Conditional`), the element contained may only be from a wider lattice. In this PR, this is not enforced by the type system. This is quite deliberate, as I want to retain the types and object layouts of the lattice elements, but of course a future #42596-like change could add such type enforcement. Of particular note is that the `PartialsLattice` and `ConditionalsLattice` is parameterized and additional layers may be added in the stack. For example, in #40992, I had proposed a lattice element that refines `Int` and tracks symbolic expressions. In this setup, this could be accomplished by adding an appropriate lattice in between the `ConstsLattice` and the `PartialsLattice` (of course, additional hooks would be required to make the tfuncs work, but that is outside the scope of this PR). I don't think this is a full solution, but I think it'll help us play with some of these extended lattice options over the next 6-12 months in the packages that want to do this sort of thing. Presumably once we know what all the potential lattice extensions look like, we will want to take another look at this (likely together with whatever solution we come up with for the AbstractInterpreter composability problem and a rebase of #42596). WIP because I didn't bother updating and plumbing through the lattice in all the call sites yet, but that's mostly mechanical, so if we like this direction, I will make that change and hope to merge this in short order (because otherwise it'll accumulate massive merge conflicts).
Keno
added a commit
that referenced
this issue
Aug 31, 2022
There's been two threads of work involving the compiler's notion of the inference lattice. One is that the lattice has gotten to complicated and with too many internal constraints that are not manifest in the type system. #42596 attempted to address this, but it's quite disruptive as it changes the lattice types and all the signatures of the lattice operations, which are used quite extensively throughout the ecosystem (despite being internal), so that change is quite disruptive (and something we'd ideally only make the ecosystem do once). The other thread of work is that people would like to experiment with a variety of extended lattices outside of base (either to prototype potential additions to the lattice in base or to do custom abstract interpretation over the julia code). At the moment, the lattice is quite closely interwoven with the rest of the abstract interpreter. In response to this request in #40992, I had proposed a `CustomLattice` element with callbacks, but this doesn't compose particularly well, is cumbersome and imposes overhead on some of the hottest parts of the compiler, so it's a bit of a tough sell to merge into Base. In this PR, I'd like to propose a refactoring that is relatively non-invasive to non-Base users, but I think would allow easier experimentation with changes to the lattice for these two use cases. In essence, we're splitting the lattice into a ladder of 5 different lattices, each containing the previous lattice as a sub-lattice. These 5 lattices are: - JLTypeLattice (Anything that's a `Type`) - ConstsLattice ( + `Const`, `PartialTypeVar`) - PartialsLattice ( + `PartialStruct` ) - ConditionalsLattice ( + `Conditional` ) - InferenceLattice ( + `LimitedAccuracy`, `MaybeUndef` ) The idea is that where a lattice element contains another lattice element (e.g. in `PartialStruct` or `Conditional`), the element contained may only be from a wider lattice. In this PR, this is not enforced by the type system. This is quite deliberate, as I want to retain the types and object layouts of the lattice elements, but of course a future #42596-like change could add such type enforcement. Of particular note is that the `PartialsLattice` and `ConditionalsLattice` is parameterized and additional layers may be added in the stack. For example, in #40992, I had proposed a lattice element that refines `Int` and tracks symbolic expressions. In this setup, this could be accomplished by adding an appropriate lattice in between the `ConstsLattice` and the `PartialsLattice` (of course, additional hooks would be required to make the tfuncs work, but that is outside the scope of this PR). I don't think this is a full solution, but I think it'll help us play with some of these extended lattice options over the next 6-12 months in the packages that want to do this sort of thing. Presumably once we know what all the potential lattice extensions look like, we will want to take another look at this (likely together with whatever solution we come up with for the AbstractInterpreter composability problem and a rebase of #42596). WIP because I didn't bother updating and plumbing through the lattice in all the call sites yet, but that's mostly mechanical, so if we like this direction, I will make that change and hope to merge this in short order (because otherwise it'll accumulate massive merge conflicts).
Keno
added a commit
that referenced
this issue
Aug 31, 2022
There's been two threads of work involving the compiler's notion of the inference lattice. One is that the lattice has gotten to complicated and with too many internal constraints that are not manifest in the type system. #42596 attempted to address this, but it's quite disruptive as it changes the lattice types and all the signatures of the lattice operations, which are used quite extensively throughout the ecosystem (despite being internal), so that change is quite disruptive (and something we'd ideally only make the ecosystem do once). The other thread of work is that people would like to experiment with a variety of extended lattices outside of base (either to prototype potential additions to the lattice in base or to do custom abstract interpretation over the julia code). At the moment, the lattice is quite closely interwoven with the rest of the abstract interpreter. In response to this request in #40992, I had proposed a `CustomLattice` element with callbacks, but this doesn't compose particularly well, is cumbersome and imposes overhead on some of the hottest parts of the compiler, so it's a bit of a tough sell to merge into Base. In this PR, I'd like to propose a refactoring that is relatively non-invasive to non-Base users, but I think would allow easier experimentation with changes to the lattice for these two use cases. In essence, we're splitting the lattice into a ladder of 5 different lattices, each containing the previous lattice as a sub-lattice. These 5 lattices are: - JLTypeLattice (Anything that's a `Type`) - ConstsLattice ( + `Const`, `PartialTypeVar`) - PartialsLattice ( + `PartialStruct` ) - ConditionalsLattice ( + `Conditional` ) - InferenceLattice ( + `LimitedAccuracy`, `MaybeUndef` ) The idea is that where a lattice element contains another lattice element (e.g. in `PartialStruct` or `Conditional`), the element contained may only be from a wider lattice. In this PR, this is not enforced by the type system. This is quite deliberate, as I want to retain the types and object layouts of the lattice elements, but of course a future #42596-like change could add such type enforcement. Of particular note is that the `PartialsLattice` and `ConditionalsLattice` is parameterized and additional layers may be added in the stack. For example, in #40992, I had proposed a lattice element that refines `Int` and tracks symbolic expressions. In this setup, this could be accomplished by adding an appropriate lattice in between the `ConstsLattice` and the `PartialsLattice` (of course, additional hooks would be required to make the tfuncs work, but that is outside the scope of this PR). I don't think this is a full solution, but I think it'll help us play with some of these extended lattice options over the next 6-12 months in the packages that want to do this sort of thing. Presumably once we know what all the potential lattice extensions look like, we will want to take another look at this (likely together with whatever solution we come up with for the AbstractInterpreter composability problem and a rebase of #42596). WIP because I didn't bother updating and plumbing through the lattice in all the call sites yet, but that's mostly mechanical, so if we like this direction, I will make that change and hope to merge this in short order (because otherwise it'll accumulate massive merge conflicts).
Keno
added a commit
that referenced
this issue
Aug 31, 2022
There's been two threads of work involving the compiler's notion of the inference lattice. One is that the lattice has gotten to complicated and with too many internal constraints that are not manifest in the type system. #42596 attempted to address this, but it's quite disruptive as it changes the lattice types and all the signatures of the lattice operations, which are used quite extensively throughout the ecosystem (despite being internal), so that change is quite disruptive (and something we'd ideally only make the ecosystem do once). The other thread of work is that people would like to experiment with a variety of extended lattices outside of base (either to prototype potential additions to the lattice in base or to do custom abstract interpretation over the julia code). At the moment, the lattice is quite closely interwoven with the rest of the abstract interpreter. In response to this request in #40992, I had proposed a `CustomLattice` element with callbacks, but this doesn't compose particularly well, is cumbersome and imposes overhead on some of the hottest parts of the compiler, so it's a bit of a tough sell to merge into Base. In this PR, I'd like to propose a refactoring that is relatively non-invasive to non-Base users, but I think would allow easier experimentation with changes to the lattice for these two use cases. In essence, we're splitting the lattice into a ladder of 5 different lattices, each containing the previous lattice as a sub-lattice. These 5 lattices are: - JLTypeLattice (Anything that's a `Type`) - ConstsLattice ( + `Const`, `PartialTypeVar`) - PartialsLattice ( + `PartialStruct` ) - ConditionalsLattice ( + `Conditional` ) - InferenceLattice ( + `LimitedAccuracy`, `MaybeUndef` ) The idea is that where a lattice element contains another lattice element (e.g. in `PartialStruct` or `Conditional`), the element contained may only be from a wider lattice. In this PR, this is not enforced by the type system. This is quite deliberate, as I want to retain the types and object layouts of the lattice elements, but of course a future #42596-like change could add such type enforcement. Of particular note is that the `PartialsLattice` and `ConditionalsLattice` is parameterized and additional layers may be added in the stack. For example, in #40992, I had proposed a lattice element that refines `Int` and tracks symbolic expressions. In this setup, this could be accomplished by adding an appropriate lattice in between the `ConstsLattice` and the `PartialsLattice` (of course, additional hooks would be required to make the tfuncs work, but that is outside the scope of this PR). I don't think this is a full solution, but I think it'll help us play with some of these extended lattice options over the next 6-12 months in the packages that want to do this sort of thing. Presumably once we know what all the potential lattice extensions look like, we will want to take another look at this (likely together with whatever solution we come up with for the AbstractInterpreter composability problem and a rebase of #42596). WIP because I didn't bother updating and plumbing through the lattice in all the call sites yet, but that's mostly mechanical, so if we like this direction, I will make that change and hope to merge this in short order (because otherwise it'll accumulate massive merge conflicts).
aviatesk
pushed a commit
that referenced
this issue
Sep 1, 2022
There's been two threads of work involving the compiler's notion of the inference lattice. One is that the lattice has gotten to complicated and with too many internal constraints that are not manifest in the type system. #42596 attempted to address this, but it's quite disruptive as it changes the lattice types and all the signatures of the lattice operations, which are used quite extensively throughout the ecosystem (despite being internal), so that change is quite disruptive (and something we'd ideally only make the ecosystem do once). The other thread of work is that people would like to experiment with a variety of extended lattices outside of base (either to prototype potential additions to the lattice in base or to do custom abstract interpretation over the Julia code). At the moment, the lattice is quite closely interwoven with the rest of the abstract interpreter. In response to this request in #40992, I had proposed a `CustomLattice` element with callbacks, but this doesn't compose particularly well, is cumbersome and imposes overhead on some of the hottest parts of the compiler, so it's a bit of a tough sell to merge into `Base`. In this PR, I'd like to propose a refactoring that is relatively non-invasive to non-Base users, but I think would allow easier experimentation with changes to the lattice for these two use cases. In essence, we're splitting the lattice into a ladder of 5 different lattices, each containing the previous lattice as a sub-lattice. These 5 lattices are: - `JLTypeLattice` (Anything that's a `Type`) - `ConstsLattice` ( + `Const`, `PartialTypeVar`) - `PartialsLattice` ( + `PartialStruct`, `PartialOpaque` ) - `ConditionalsLattice` ( + `Conditional` ) - `InferenceLattice` ( + `LimitedAccuracy` ) - `OptimizerLattice` ( + `MaybeUndef` ) The idea is that where a lattice element contains another lattice element (e.g. in `PartialStruct` or `Conditional`), the element contained may only be from a wider lattice. In this PR, this is not enforced by the type system. This is quite deliberate, as I want to retain the types and object layouts of the lattice elements, but of course a future #42596-like change could add such type enforcement. Of particular note is that the `PartialsLattice` and `ConditionalsLattice` is parameterized and additional layers may be added in the stack. For example, in #40992, I had proposed a lattice element that refines `Int` and tracks symbolic expressions. In this setup, this could be accomplished by adding an appropriate lattice in between the `ConstsLattice` and the `PartialsLattice` (of course, additional hooks would be required to make the tfuncs work, but that is outside the scope of this PR). I don't think this is a full solution, but I think it'll help us play with some of these extended lattice options over the next 6-12 months in the packages that want to do this sort of thing. Presumably once we know what all the potential lattice extensions look like, we will want to take another look at this (likely together with whatever solution we come up with for the AbstractInterpreter composability problem and a rebase of #42596). WIP because I didn't bother updating and plumbing through the lattice in all the call sites yet, but that's mostly mechanical, so if we like this direction, I will make that change and hope to merge this in short order (because otherwise it'll accumulate massive merge conflicts).
aviatesk
pushed a commit
that referenced
this issue
Sep 1, 2022
There's been two threads of work involving the compiler's notion of the inference lattice. One is that the lattice has gotten to complicated and with too many internal constraints that are not manifest in the type system. #42596 attempted to address this, but it's quite disruptive as it changes the lattice types and all the signatures of the lattice operations, which are used quite extensively throughout the ecosystem (despite being internal), so that change is quite disruptive (and something we'd ideally only make the ecosystem do once). The other thread of work is that people would like to experiment with a variety of extended lattices outside of base (either to prototype potential additions to the lattice in base or to do custom abstract interpretation over the Julia code). At the moment, the lattice is quite closely interwoven with the rest of the abstract interpreter. In response to this request in #40992, I had proposed a `CustomLattice` element with callbacks, but this doesn't compose particularly well, is cumbersome and imposes overhead on some of the hottest parts of the compiler, so it's a bit of a tough sell to merge into `Base`. In this PR, I'd like to propose a refactoring that is relatively non-invasive to non-Base users, but I think would allow easier experimentation with changes to the lattice for these two use cases. In essence, we're splitting the lattice into a ladder of 5 different lattices, each containing the previous lattice as a sub-lattice. These 5 lattices are: - `JLTypeLattice` (Anything that's a `Type`) - `ConstsLattice` ( + `Const`, `PartialTypeVar`) - `PartialsLattice` ( + `PartialStruct`, `PartialOpaque` ) - `ConditionalsLattice` ( + `Conditional` ) - `InferenceLattice` ( + `LimitedAccuracy` ) - `OptimizerLattice` ( + `MaybeUndef` ) The idea is that where a lattice element contains another lattice element (e.g. in `PartialStruct` or `Conditional`), the element contained may only be from a wider lattice. In this PR, this is not enforced by the type system. This is quite deliberate, as I want to retain the types and object layouts of the lattice elements, but of course a future #42596-like change could add such type enforcement. Of particular note is that the `PartialsLattice` and `ConditionalsLattice` is parameterized and additional layers may be added in the stack. For example, in #40992, I had proposed a lattice element that refines `Int` and tracks symbolic expressions. In this setup, this could be accomplished by adding an appropriate lattice in between the `ConstsLattice` and the `PartialsLattice` (of course, additional hooks would be required to make the tfuncs work, but that is outside the scope of this PR). I don't think this is a full solution, but I think it'll help us play with some of these extended lattice options over the next 6-12 months in the packages that want to do this sort of thing. Presumably once we know what all the potential lattice extensions look like, we will want to take another look at this (likely together with whatever solution we come up with for the AbstractInterpreter composability problem and a rebase of #42596). WIP because I didn't bother updating and plumbing through the lattice in all the call sites yet, but that's mostly mechanical, so if we like this direction, I will make that change and hope to merge this in short order (because otherwise it'll accumulate massive merge conflicts).
Keno
added a commit
that referenced
this issue
Sep 1, 2022
There's been two threads of work involving the compiler's notion of the inference lattice. One is that the lattice has gotten to complicated and with too many internal constraints that are not manifest in the type system. #42596 attempted to address this, but it's quite disruptive as it changes the lattice types and all the signatures of the lattice operations, which are used quite extensively throughout the ecosystem (despite being internal), so that change is quite disruptive (and something we'd ideally only make the ecosystem do once). The other thread of work is that people would like to experiment with a variety of extended lattices outside of base (either to prototype potential additions to the lattice in base or to do custom abstract interpretation over the Julia code). At the moment, the lattice is quite closely interwoven with the rest of the abstract interpreter. In response to this request in #40992, I had proposed a `CustomLattice` element with callbacks, but this doesn't compose particularly well, is cumbersome and imposes overhead on some of the hottest parts of the compiler, so it's a bit of a tough sell to merge into `Base`. In this PR, I'd like to propose a refactoring that is relatively non-invasive to non-Base users, but I think would allow easier experimentation with changes to the lattice for these two use cases. In essence, we're splitting the lattice into a ladder of 5 different lattices, each containing the previous lattice as a sub-lattice. These 5 lattices are: - `JLTypeLattice` (Anything that's a `Type`) - `ConstsLattice` ( + `Const`, `PartialTypeVar`) - `PartialsLattice` ( + `PartialStruct`, `PartialOpaque` ) - `ConditionalsLattice` ( + `Conditional` ) - `InferenceLattice` ( + `LimitedAccuracy` ) - `OptimizerLattice` ( + `MaybeUndef` ) The idea is that where a lattice element contains another lattice element (e.g. in `PartialStruct` or `Conditional`), the element contained may only be from a wider lattice. In this PR, this is not enforced by the type system. This is quite deliberate, as I want to retain the types and object layouts of the lattice elements, but of course a future #42596-like change could add such type enforcement. Of particular note is that the `PartialsLattice` and `ConditionalsLattice` is parameterized and additional layers may be added in the stack. For example, in #40992, I had proposed a lattice element that refines `Int` and tracks symbolic expressions. In this setup, this could be accomplished by adding an appropriate lattice in between the `ConstsLattice` and the `PartialsLattice` (of course, additional hooks would be required to make the tfuncs work, but that is outside the scope of this PR). I don't think this is a full solution, but I think it'll help us play with some of these extended lattice options over the next 6-12 months in the packages that want to do this sort of thing. Presumably once we know what all the potential lattice extensions look like, we will want to take another look at this (likely together with whatever solution we come up with for the AbstractInterpreter composability problem and a rebase of #42596). WIP because I didn't bother updating and plumbing through the lattice in all the call sites yet, but that's mostly mechanical, so if we like this direction, I will make that change and hope to merge this in short order (because otherwise it'll accumulate massive merge conflicts).
Keno
added a commit
that referenced
this issue
Sep 2, 2022
…46526) There's been two threads of work involving the compiler's notion of the inference lattice. One is that the lattice has gotten to complicated and with too many internal constraints that are not manifest in the type system. #42596 attempted to address this, but it's quite disruptive as it changes the lattice types and all the signatures of the lattice operations, which are used quite extensively throughout the ecosystem (despite being internal), so that change is quite disruptive (and something we'd ideally only make the ecosystem do once). The other thread of work is that people would like to experiment with a variety of extended lattices outside of base (either to prototype potential additions to the lattice in base or to do custom abstract interpretation over the Julia code). At the moment, the lattice is quite closely interwoven with the rest of the abstract interpreter. In response to this request in #40992, I had proposed a `CustomLattice` element with callbacks, but this doesn't compose particularly well, is cumbersome and imposes overhead on some of the hottest parts of the compiler, so it's a bit of a tough sell to merge into `Base`. In this PR, I'd like to propose a refactoring that is relatively non-invasive to non-Base users, but I think would allow easier experimentation with changes to the lattice for these two use cases. In essence, we're splitting the lattice into a ladder of 5 different lattices, each containing the previous lattice as a sub-lattice. These 5 lattices are: - `JLTypeLattice` (Anything that's a `Type`) - `ConstsLattice` ( + `Const`, `PartialTypeVar`) - `PartialsLattice` ( + `PartialStruct`, `PartialOpaque` ) - `ConditionalsLattice` ( + `Conditional` ) - `InferenceLattice` ( + `LimitedAccuracy` ) - `OptimizerLattice` ( + `MaybeUndef` ) The idea is that where a lattice element contains another lattice element (e.g. in `PartialStruct` or `Conditional`), the element contained may only be from a wider lattice. In this PR, this is not enforced by the type system. This is quite deliberate, as I want to retain the types and object layouts of the lattice elements, but of course a future #42596-like change could add such type enforcement. Of particular note is that the `PartialsLattice` and `ConditionalsLattice` is parameterized and additional layers may be added in the stack. For example, in #40992, I had proposed a lattice element that refines `Int` and tracks symbolic expressions. In this setup, this could be accomplished by adding an appropriate lattice in between the `ConstsLattice` and the `PartialsLattice` (of course, additional hooks would be required to make the tfuncs work, but that is outside the scope of this PR). I don't think this is a full solution, but I think it'll help us play with some of these extended lattice options over the next 6-12 months in the packages that want to do this sort of thing. Presumably once we know what all the potential lattice extensions look like, we will want to take another look at this (likely together with whatever solution we come up with for the AbstractInterpreter composability problem and a rebase of #42596). WIP because I didn't bother updating and plumbing through the lattice in all the call sites yet, but that's mostly mechanical, so if we like this direction, I will make that change and hope to merge this in short order (because otherwise it'll accumulate massive merge conflicts).
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Hi, I'm just starting this issue to keep track of some useful discussion happened in various places about custom type lattice and more generic abstract interpreter.
recently a few people including find that we might need custom type lattice (or insert custom type lattice into existing Julia ones) to enhance inference. So I think it
would be better to collect these scatter thoughts together here.
(please feel free to update the following)
use cases
quantum compilation (YaoCompiler.jl)
The recent progress of quantum hardware raise the need of high level eDSL that help people program this type of hardware, and compiler optimization
on such programs also opens a few new questions on the implementation. We recently find that by inferring if a number is multiple of pi, or pi/2 etc. Temporary
workaround can be defining a custom type for pi and overload everything, but this sounds like a huge engineering work.
we will be able to optimize hybrid (quantum + normal) programs better, and by inferring the measurement result type we can check if some of the non-cloning
errors by using abstract interpreter. However, this seems to require custom lattice type. For reference of how would the type lattices look like in other implementations,
one could refer to the Silq paper: https://files.sri.inf.ethz.ch/website/papers/pldi20-silq.pdf
On the other hand, there is a new paper about quantum abstract
interpretation (which is the distinguished paper in PLDI 2021): http://web.cs.ucla.edu/~palsberg/paper/pldi21-quantum.pdf
It might be a use case for generalizing the Julia abstract interpreter API (or at least make it possible to work with an indepdent eDSL abstract interpreter?)
Static Linter (JET.jl)
I posted an idea about checking numerical error a while ago here (aviatesk/JET.jl#141) and @aviatesk mentioned to support this
type of error we will also need custom lattice type to enhance the checking. Some of the detailed use cases and required elements have been disscussed in that issue.
On the other hand, previously there is https://github.com/FluxML/Mjolnir.jl that kinda implements some customized inference, I think some of them is still hard to implement with the current
abstract interpreter API.
I think @femtomc has some more use cases, but I'm not sure, please feel free to add.
cc: @femtomc @Keno @aviatesk @Keno
The text was updated successfully, but these errors were encountered: