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:
subset
along the CFG :). Link.I prototyped the variant (a couple different ways because of the problems I encountered) — Link to the first version:
vec-push-ref
tests.cycle_unification
and cfg_propagation_required
.flow_sensitive_equality_required
.But this implementation is incorrect:
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:
unnecessary_error
test is not emitting errors, as expected.clap
, it doesn't seem to work yet.I'll keep working on this.
or
or
By clicking below, you agree to our terms of service.
New to HackMD? Sign up
Syntax | Example | Reference | |
---|---|---|---|
# Header | Header | 基本排版 | |
- Unordered List |
|
||
1. Ordered List |
|
||
- [ ] Todo List |
|
||
> Blockquote | Blockquote |
||
**Bold font** | Bold font | ||
*Italics font* | Italics font | ||
~~Strikethrough~~ | |||
19^th^ | 19th | ||
H~2~O | H2O | ||
++Inserted text++ | Inserted text | ||
==Marked text== | Marked text | ||
[link text](https:// "title") | Link | ||
 | Image | ||
`Code` | Code |
在筆記中貼入程式碼 | |
```javascript var i = 0; ``` |
|
||
:smile: | ![]() |
Emoji list | |
{%youtube youtube_id %} | Externals | ||
$L^aT_eX$ | LaTeX | ||
:::info This is a alert area. ::: |
This is a alert area. |
On a scale of 0-10, how likely is it that you would recommend HackMD to your friends, family or business associates?
Please give us some advice and help us improve HackMD.
Syncing