Closed amandasystems closed 5 years ago
The current version seems to work, but I am not happy about generating an entire new Relation
for walking the control-flow graph backwards.
I haven't yet written extensive tests, but I think it makes some sort of sense to go ahead with the extensions to rustc to produce the new facts so as to have some sort of ability to generate input data.
Additionally, I am unsure how to handle a possible off by one situation when doing CFG traversal. In particular, is there a difference between considering a variable as dead or alive in the point where the assignment ("death") happens? I am even unsure of what I am doing now, but I think the correct way would be to have the variable die after assignment, while being alive at the assignment, but I don't know enough about Miri to know if this ever becomes a problem. If calculations of values used in assignments always happens in a point before the assignment itself both variants should be equivalent, right? Or are the points mapped to actual Rust lines of code?
This is marked WIP again as I might as well roll the entire region logic into this PR as per #104.
This is a work in progress on issue #104.
Sorry for the poorly named branch; I started it to fix a silly compiler warning and ended up using it for the implementation.