undefined | Better HN

0 pointsRusky2y ago0 comments

Provenance is a dynamic property of pointer values. The actual underlying rules that a program must follow, even when using raw pointers and `unsafe`, are written in terms of provenance. Miri (https://github.com/rust-lang/miri) represents provenance as an actual value stored alongside each pointer's address, so it can check for violations of these rules.

Lifetimes are a static approximation of provenance. They are erased after being validated by the borrow checker, and do not exist in Miri or have any impact on what transformations the optimizer may perform. In other words, the provenance rules allow a superset of what the borrow checker allows.

0 comments

Buttons8402y ago

So this is about solidifying very specific semantics that are of more concern to projects like Miri than it is to regular users?

Speaking of Miri, is the long term goal to say for certain whether or not a program execution encountered UB? (Which is, of course, different than verifying it before execution at compile time.)

RuskyOP2y ago

It is about solidifying semantics, but those semantics are still a concern to regular users who are writing `unsafe` code, not just Miri.

As I understand it, Miri would like to be certain about the presence/absence of the UB of any particular program execution, but there will probably always be some cases it can't catch.

digama02y ago

> Speaking of Miri, is the long term goal to say for certain whether or not a program execution encountered UB? (Which is, of course, different than verifying it before execution at compile time.)

That's more than a long term goal, that's the present behavior, to the extent that the UB rules are defined in the first place. Miri will tell you when it has to make approximating assumptions (e.g. accessing FFI or using nondeterministic operations), and it doesn't happen very often. This is very much the intent of the tool.

j / k navigate · click thread line to collapse