Basic support for checking raw pointer read/write

[ranjitjhala]

1. Track an int index with the pointer, to track how much is "valid" to write,
2. Check at deref that the associated index is (strictly) positive,
3. Defer tracking provenance etc. to later, perhaps once we have more experience with what is needed.

e.g. the following now works, with an error reported without the preconditions.

#[flux::opts(check_raw_pointer = "checked")]
#[flux::spec(fn (ptr: *mut{v: v > 0} T, value: T))]
fn write<T>(ptr: *mut T, value: T) {
    unsafe {
        *ptr = value;
    }
}

#[flux::opts(check_raw_pointer = "checked")]
#[flux::spec(fn (ptr: *mut{v: v > 0} T, value: T))]
fn write<T>(ptr: *mut T, value: T) {
    unsafe {
        *ptr = value;
    }
}

[ranjitjhala]

@nilehmann ping -- I'd like to merge this one in to do more stuff on core.

[nilehmann]

I'm looking at this now.

[ranjitjhala]

@nilehmann I made the changes we discussed yesterday

[nilehmann]

@ranjitjhala some comments

[nilehmann]

This makes me nervous. Did you add it because as_mut_ptr returns whatever refined type was in the input, and you wanted to keep using it the pointer at that type?

[ranjitjhala]

Sort of -- I was just trying to mirror the story for &mut T here?

The option is to remove subtyping between raw-ptr, but that seemed to be worse, no?

[ranjitjhala]

Or is your point that we IGNORE the refinements for stuff read through raw-ptr so it doesn't matter e.g.
https://github.com/flux-rs/flux/blob/9c27760a7bbbda9c95bceb21f831334bee11408e/crates/flux-refineck/src/checker.rs#L1403-L1404

[ranjitjhala]

@nilehmann I did the changes, except the ptr-subtyping, see discussion above.