Polonius experimental "Timeless" variant

1. The (possibly flawed) methodology

To make sure which of our tests showcased persistent flow, I commented out the parts which propagate the subset TC through the CFG — link — to see test failures:

failures:
    test::vec_push_ref_foo1::datafrog_opt
    test::vec_push_ref_foo2::datafrog_opt
    test::vec_push_ref_foo3::datafrog_opt

Surprisingly, they do not deal with mutable references. They obviously do deal with mutable references, in the method call desugaring.

  • vec-push-ref/foo1: the different number of borrow_live_at tuples computed with and without propagation makes the test fail, and not emit the expected error. (18 borrow_live_at tuples versus the expected 28, probably because of the 19 requires/contains/restricts tuples versus the expected 29)
  • vec-push-ref/foo2: found 18 of the expected 34 borrow_live_at, and 19 of the expected 35 requires; resulting in missing the expected error.
  • vec-push-ref/foo3: this test is the same as foo2 but with the erroneous line removed, so has the same numbers of found/expecte facts. It "correctly" produces no error in either variants, and fails in tests because of the difference in borrow_live_at facts.

Then, we also have a few new examples, in the polonius-imprecision dataset:

  1. a case where the current Polonius analysis is imprecise and emits an unnecessary error. Link.
  2. an example of the Timeless "unification" (currently dependent on CFG propagation). Link.
  3. another example which requires persistent flow to find an error (from the last time we talked about not needing to track subset along the CFG :). Link.
  4. a case Polonius accepts and where the Timeless variant is not precise enough: it would emit errors. To detect this is OK, the variant would require flow-sensitive equality of regions. Link.

2. The variant

I prototyped the variant (a couple different ways because of the problems I encountered) — Link to the first version:

  • passes the vec-push-ref tests.
  • has the same behaviour as the Naive variant on cycle_unification and cfg_propagation_required.
  • as expected, emits errors for flow_sensitive_equality_required.

But this implementation is incorrect:

  • it does emit an error for unnecessary_error.
  • clap "doesn't work" yet: it took a very long time, and used a lot of memory so I killed it (whereas the Naive variant terminates in around 30s) after 5 minutes.

I feel I must have made a mistake somewhere, probably in computing the equality relation (maybe related to having both equals(R1, R2) and equals(R2, R1) tuples).

To check if computing this relation this way in datafrog was causing issues, I made the second version to try and have a bit more control over computing equality: by splitting the subset TC and computing equality in rust, before running the rest of the rules as usual. (It's also still as inefficient as the one before).

This time:

  • the unnecessary_error test is not emitting errors, as expected.
  • but no apparent changes to clap, it doesn't seem to work yet.

I'll keep working on this.

Select a repo