fix(rt): align transparent pointer casts #811
Conversation
Stevengre
force-pushed
the
jh/align-transparent-place
branch
2 times, most recently
from
24c0f88 to
0f140fa
Compare
Stevengre
force-pushed
the
jh/align-transparent-place
branch
2 times, most recently
from
070066e to
195d6f6
Compare
dkcumming
left a comment
dkcumming
left a comment
There was a problem hiding this comment.
@Stevengre I think this is all good, I will approve but I also think @jberthold should take a loook
jberthold
left a comment
jberthold
left a comment
There was a problem hiding this comment.
LGTM overall.
Please clarify why the orBool is used. The missing ) is not too important unless you re-run CI anyway.
| Conversion is especially possible for the case of _Slices_ (of dynamic length) and _Arrays_ (of static length), | ||
| which have the same representation `Value::Range`. | ||
|
|
||
| When the cast crosses transparent wrappers (newtypes that just forward field `0` e.g. `struct Wrapper<T>(T)`, the pointer's |
There was a problem hiding this comment.
(nit-pick)
| When the cast crosses transparent wrappers (newtypes that just forward field `0` e.g. `struct Wrapper<T>(T)`, the pointer's | |
| When the cast crosses transparent wrappers (newtypes that just forward field `0` e.g. `struct Wrapper<T>(T)`), the pointer's |
| rule #typesCompatible(SRC, OTHER) => true | ||
| requires #zeroSizedType(SRC) orBool #zeroSizedType(OTHER) |
There was a problem hiding this comment.
A bit puzzled by the orBool here... I would accept it immediately with andBool (one zero-sized thing is as good as another) but what happens if we cast a pointer to non-zero-sized to a zero-sized one and back, should that be allowed? Or which side is not allowed? (zero to non-zero I would guess)
There was a problem hiding this comment.
I'm investigating this with a new test, but it encounters other ndbranches.
There was a problem hiding this comment.
It needs a cast from pointer to integer. here: #812
There was a problem hiding this comment.
I provided pointer-cast-zst.rs to cover this scenario: it casts a *const Wrapper to *const () (ZST) and back, then asserts the roundtrip preserves the value. Since this test passes, the semantics currently allow non‑zero → zero → non‑zero pointer casts, so we shoud use this orBool to allow this situation.
| │ (111 steps) | ||
| ├─ 7 | ||
| │ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th | ||
| │ function: main | ||
| ┃ | ||
| ┃ (1 step) | ||
| ┣━━┓ | ||
| ┃ │ | ||
| ┃ ├─ 8 | ||
| ┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC | ||
| ┃ │ function: main | ||
| ┃ │ | ||
| ┃ │ (1 step) | ||
| ┃ └─ 10 (stuck, leaf) | ||
| ┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re | ||
| ┃ function: main | ||
| ┃ | ||
| ┗━━┓ | ||
| │ | ||
| ├─ 9 | ||
| │ #execBlockIdx ( basicBlockIdx ( 7 ) ) ~> .K | ||
| │ function: main | ||
| │ | ||
| │ (17 steps) | ||
| └─ 11 (stuck, leaf) | ||
| #setLocalValue ( place ( ... local: local ( 1 ) , projection: .ProjectionElems ) | ||
| function: main |
There was a problem hiding this comment.
FYI This now hits a non-deterministic branch on what looks like a pointer alignment check .
There was a problem hiding this comment.
@jberthold I saw this last night in a previous proof, it comes when the pointer cast is thunked, and then the pointer is branches. I am worried it is happening because it needs to get the address but I haven't looked with details yet. If it needs the address I am not sure what we do
There was a problem hiding this comment.
I think I solved it before in the big pr. Could I introduce an issue for this and solve it later in another pr?
There was a problem hiding this comment.
Yes, we can solve this one later, it should not block this PR
Co-authored-by: Daniel Cumming <[email protected]>
Stevengre
force-pushed
the
jh/align-transparent-place
branch
from
973bd17 to
d55c2e7
Compare
No description provided.