Rewrite polonius-engine
#183
Conversation
ecstatic-morse
force-pushed
the
new-engine
branch
2 times, most recently
from
495c96f to
bc94adf
Compare
|
I'm not sure what the path is to upstream this. It's too big to review on its own, obviously. I might have to work in my fork for a while. |
Each section ("naive", "initialization", etc.) is now expressed as a
`Computation`, with defined inputs and outputs. Computations are
organized into `Pipeline`s, which execute each computation in turn,
storing the results in a `Db` where they are accessible to later
computations in the pipeline.
`Computation`s can also dump intermediate results using the
creatively-named `Dump` struct. A series of `Dumper`s can be specified
for a pipeline, each which will be given access to a type-erased
version of the dumped data.
Only the location-insensitive variant computes this relation
ecstatic-morse
force-pushed
the
new-engine
branch
from
bc94adf to
6db3908
Compare
| let input = <C::Input<'_>>::load_from_db(db); | ||
| dump.unit_start(name); | ||
| let start_time = Instant::now(); | ||
| let output = computation.compute(input, dump); | ||
| let end_time = Instant::now(); | ||
| dump.unit_end(name); | ||
|
|
||
| output.store_to_db(db, dump); |
There was a problem hiding this comment.
Here's the part that requires GATs. Moving the lifetime parameter for Input to Computation itself and changing the signature to the following gives an error:
fn compute_<C, T>(computation: &C, db: &mut Db<T>, dump: &mut Dump<'_>)
where
for<'db> C: Computation<'db, T>,
for<'db> <C as Computation<'db, T>>::Input: LoadFrom<'db, T>,
for<'db> <C as Computation<'db, T>>::Output: StoreTo<T>,
T: FactTypes,error[E0502]: cannot borrow `*db` as mutable because it is also borrowed as immutable
--> polonius-engine/src/pipeline.rs:213:5
|
206 | let input = <C::Input>::load_from_db(db);
| -- immutable borrow occurs here
...
213 | output.store_to_db(db, dump);
| ^^^^^^^-----------^^^^^^^^^^
| | |
| | immutable borrow later used by call
| mutable borrow occurs here
This is expected since data from db flows from input into computation and then output. It's perhaps more surprising that this works with a GAT on Computation::Input?
There was a problem hiding this comment.
My understanding is that this works with GATs because neither the implementer of Computation nor Computation::Output can name the lifetime used in Computation::Input<'db>. I'm not very confident in this assessment, however. Ironically, this is the kind of complex HRTB case that Polonius cannot handle at the moment.
|
@ecstatic-morse are you still working on this? |
Requires rust-lang/datafrog#50.
Each section ("naive", "initialization", etc.) is now expressed as a
Computation, with defined inputs and outputs. Computations are organized intoPipelines, which execute each computation in turn, storing the results in aDbwhere they are accessible to later computations in the pipeline.Computations can also dump intermediate results using the (creatively named)Dumpstruct. A series ofDumpers can be specified for a pipeline, each which will be given access to a type-erased version of the dumped data.The purpose of this is to support arbitrary configurations of analysis passes, such as skipping move/init analysis by providing an additional "dropped_while_init" input, or the use of alternate solvers (e.g. Soufflé).
For now, I've preserved the existing interface of
polonius-engine(Ouput,AllFactsandAlgorithm). I expect this to be temporary, but I wanted to take advantage of the existing test machinery and keep my changes localized (relatively speaking).This adds some additional dependencies (most of which could be removed) and some nightly features (which cannot be, at least not easily). I'm not sure if compiling under the beta toolchain without
RUSTC_BOOTSTRAPis a hard requirement, or if it could be relaxed.