Support for raw pointers #532
Conversation
| // | Ptr( Address, MaybeValue ) // FIXME why maybe? why value? | ||
| // address, metadata for ref/ptr | ||
| | Ptr( Int, Place, Mutability, Int, Int) | ||
| // stack depth (initially zero), place, mutablility, address, offset NOTE: First 3 fields are the same as Reference, last are needed for low level instructions |
There was a problem hiding this comment.
Nit-pick: long line
| // stack depth (initially zero), place, mutablility, address, offset NOTE: First 3 fields are the same as Reference, last are needed for low level instructions | |
| // stack depth (initially zero), place, mutablility, address, offset | |
| // NOTE: First 3 fields are the same as Reference, last are needed for low level instructions |
| rule #compute( | ||
| BOP, | ||
| typedValue(Integer(ARG1, WIDTH, _), _, _), | ||
| typedValue(Integer(ARG2, WIDTH, _), _, _), | ||
| false) // unchecked | ||
| => | ||
| typedValue( | ||
| Integer(onInt(BOP, ARG1, ARG2), WIDTH, false), | ||
| TyUnknown, | ||
| mutabilityNot | ||
| ) |
There was a problem hiding this comment.
Two things to correct:
- Your result is always unsigned but we have to keep the signedness flag from the arguments.
| rule #compute( | |
| BOP, | |
| typedValue(Integer(ARG1, WIDTH, _), _, _), | |
| typedValue(Integer(ARG2, WIDTH, _), _, _), | |
| false) // unchecked | |
| => | |
| typedValue( | |
| Integer(onInt(BOP, ARG1, ARG2), WIDTH, false), | |
| TyUnknown, | |
| mutabilityNot | |
| ) | |
| rule #compute( | |
| BOP, | |
| typedValue(Integer(ARG1, WIDTH, SIGNED), TY, _), | |
| typedValue(Integer(ARG2, WIDTH, SIGNED), TY, _), | |
| false) // unchecked | |
| => | |
| typedValue( | |
| Integer(onInt(BOP, ARG1, ARG2), WIDTH, SIGNED), | |
| TY, | |
| mutabilityNot | |
| ) |
- We have to ensure the
Tyare the same for both arguments (I added the match onTYabove). There are rules that checks this, and the suitability of the operands, for arithmetic operations. Maybe we should add similar rules for bit-oriented ones, to signalTypeMismatchorOperandMismatcherrors
| typedValue(Ptr(_, _, _, ADDRESS, _), _, _), | ||
| typedValue(Integer(VAL, WIDTH, _), _, _), |
There was a problem hiding this comment.
??? Do we really need this rule? I thought the Ptr value gets cast to usize before that, or not?
EDIT after reading the related cast rule: Maybe the cast should just be different and we delete this rule.
| // requires TY_TO #in TYPEMAP | ||
| // requires #is_valid_cast(TY_FROM.layout(), TY_TO.layout()) | ||
|
|
||
| rule <k> #cast( typedValue(VALUE, _TY_FROM, LOCAL_MUT), castKindTransmute, TY_TO) => typedValue(VALUE, TY_TO, LOCAL_MUT) ... </k> |
There was a problem hiding this comment.
Well... this rule is certainly too generic.
Right now we only want to cast raw pointers and return their "Address" (IIUC, or something that is derived from it?), as a usize value that will suit the example program...
| rule <k> #projectedUpdate( | ||
| _DEST, | ||
| typedValue(Ptr(OFFSET, place(LOCAL, PLACEPROJ), MUT, _ADDRESS, _OFFSET2), _, _), | ||
| projectionElemDeref PROJS, |
There was a problem hiding this comment.
There is also #readProjection earlier in this module, which will require the same kind of extension to Deref a pointer.
mir-semantics/kmir/src/kmir/kdist/mir-semantics/rt/data.md
Lines 314 to 322 in 1ee2475
Raw pointers through
AddressOfandAggregateKind::RawPtrare required. Supporting pointers means we are going to have to support or stubAlignmentandLayoutin some manner to handle those MIR rvalues.