Skip to content

Commit f484c1b

Browse files
StevengreStevengre
committed
feat(not-ready)
1 parent 3089bb0 commit f484c1b

File tree

3 files changed

+147
-2
lines changed

3 files changed

+147
-2
lines changed

‎kmir/src/kmir/kdist/mir-semantics/kmir.md‎

Lines changed: 127 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -431,11 +431,136 @@ Other terminators that matter at the MIR level "Runtime" are `Drop` and `Unreach
431431
Drops are elaborated to Noops but still define the continuing control flow. Unreachable terminators lead to a program error.
432432

433433
```k
434-
rule [termDrop]: <k> #execTerminator(terminator(terminatorKindDrop(_PLACE, TARGET, _UNWIND), _SPAN))
434+
syntax KItem ::= #applyDrop(MaybeTy)
435+
| #dropValue(Value, MaybeTy)
436+
| #releaseBorrowRefMut(Value)
437+
| #releaseBorrowCell(Value)
438+
| #applyBorrowCell(Int, ProjectionElems)
439+
| #applyBorrowCellStack(Int, Int, ProjectionElems)
440+
441+
rule [termDrop]:
442+
<k> #execTerminator(terminator(terminatorKindDrop(place(local(I), PROJS), TARGET, _UNWIND), _SPAN))
435443
=>
436-
#execBlockIdx(TARGET)
444+
#traverseProjection(toLocal(I), getValue(LOCALS, I), PROJS, .Contexts)
445+
~> #readProjection(true)
446+
~> #applyDrop(getTyOf(tyOfLocal(getLocal(LOCALS, I)), PROJS))
447+
~> #execBlockIdx(TARGET)
437448
...
438449
</k>
450+
<locals> LOCALS </locals>
451+
requires 0 <=Int I
452+
andBool I <Int size(LOCALS)
453+
andBool isTypedLocal(LOCALS[I])
454+
[preserves-definedness] // valid local index checked
455+
456+
rule <k> VAL:Value ~> #applyDrop(MTY) => #dropValue(VAL, MTY) ... </k>
457+
458+
rule #dropValue(_:Value, MTY) => .K
459+
requires notBool #isRefMutTy(#lookupMaybeTy(MTY))
460+
461+
rule <k> #dropValue(Aggregate(_, ARGS), MTY)
462+
=> #releaseBorrowRefMut(getValue(ARGS, 1))
463+
...
464+
</k>
465+
requires #isRefMutTy(#lookupMaybeTy(MTY))
466+
andBool 1 <Int size(ARGS)
467+
468+
rule <k> #releaseBorrowRefMut(Aggregate(_, ListItem(PTR) _))
469+
=> #releaseBorrowCell(PTR)
470+
...
471+
</k>
472+
473+
rule #releaseBorrowRefMut(_) => .K [owise]
474+
475+
rule <k> #releaseBorrowCell(PtrLocal(0, place(local(J), PROJS), _, _))
476+
=>
477+
#traverseProjection(toLocal(J), getValue(LOCALS, J), PROJS, .Contexts)
478+
~> #readProjection(false)
479+
~> #applyBorrowCell(J, PROJS)
480+
...
481+
</k>
482+
<locals> LOCALS </locals>
483+
requires 0 <=Int J
484+
andBool J <Int size(LOCALS)
485+
andBool isTypedValue(LOCALS[J])
486+
[preserves-definedness] // valid pointer target on current stack frame
487+
488+
rule <k> #releaseBorrowCell(Reference(0, place(local(J), PROJS), _, _))
489+
=>
490+
#traverseProjection(toLocal(J), getValue(LOCALS, J), PROJS, .Contexts)
491+
~> #readProjection(false)
492+
~> #applyBorrowCell(J, PROJS)
493+
...
494+
</k>
495+
<locals> LOCALS </locals>
496+
requires 0 <=Int J
497+
andBool J <Int size(LOCALS)
498+
andBool isTypedValue(LOCALS[J])
499+
[preserves-definedness]
500+
501+
rule <k> #releaseBorrowCell(PtrLocal(OFFSET, place(local(J), PROJS), _, _))
502+
=>
503+
#traverseProjection(
504+
toStack(OFFSET, local(J)),
505+
#localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(J), OFFSET),
506+
PROJS,
507+
.Contexts
508+
)
509+
~> #readProjection(false)
510+
~> #applyBorrowCellStack(OFFSET, J, PROJS)
511+
...
512+
</k>
513+
<stack> STACK </stack>
514+
requires 0 <Int OFFSET
515+
andBool OFFSET <=Int size(STACK)
516+
andBool isStackFrame(STACK[OFFSET -Int 1])
517+
[preserves-definedness]
518+
519+
rule <k> #releaseBorrowCell(Reference(OFFSET, place(local(J), PROJS), _, _))
520+
=>
521+
#traverseProjection(
522+
toStack(OFFSET, local(J)),
523+
#localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(J), OFFSET),
524+
PROJS,
525+
.Contexts
526+
)
527+
~> #readProjection(false)
528+
~> #applyBorrowCellStack(OFFSET, J, PROJS)
529+
...
530+
</k>
531+
<stack> STACK </stack>
532+
requires 0 <Int OFFSET
533+
andBool OFFSET <=Int size(STACK)
534+
andBool isStackFrame(STACK[OFFSET -Int 1])
535+
[preserves-definedness]
536+
537+
rule #releaseBorrowCell(_) => .K [owise]
538+
539+
rule <k> CELL:Value ~> #applyBorrowCell(J, PROJS)
540+
=> #setLocalValue(place(local(J), PROJS), #incCellBorrow(CELL))
541+
...
542+
</k>
543+
544+
rule #applyBorrowCell(_, _) => .K [owise]
545+
546+
rule <k> CELL:Value ~> #applyBorrowCellStack(OFFSET, J, PROJS)
547+
=>
548+
#traverseProjection(
549+
toStack(OFFSET, local(J)),
550+
#localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(J), OFFSET),
551+
PROJS,
552+
.Contexts
553+
)
554+
~> #writeProjection(#incCellBorrow(CELL))
555+
...
556+
</k>
557+
<stack> STACK </stack>
558+
requires 0 <Int OFFSET
559+
andBool OFFSET <=Int size(STACK)
560+
andBool isStackFrame(STACK[OFFSET -Int 1])
561+
[preserves-definedness]
562+
563+
rule #applyBorrowCellStack(_, _, _) => .K [owise]
439564
440565
syntax MIRError ::= "ReachedUnreachable"
441566

‎kmir/src/kmir/kdist/mir-semantics/rt/data.md‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -347,6 +347,19 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
347347
andBool isTypedLocal(LOCALS[I])
348348
[preserves-definedness] // valid list indexing and sort checked
349349
350+
syntax Value ::= #incCellBorrow ( Value ) [function, total]
351+
352+
rule #incCellBorrow(Integer(VAL, WIDTH, true))
353+
=> Integer(VAL +Int 1, WIDTH, true)
354+
requires WIDTH ==Int 64
355+
[preserves-definedness]
356+
357+
rule #incCellBorrow(Aggregate(IDX, ListItem(FIRST) REST))
358+
=> Aggregate(IDX, ListItem(#incCellBorrow(FIRST)) REST)
359+
[preserves-definedness]
360+
361+
rule #incCellBorrow(OTHER) => OTHER [owise]
362+
350363
syntax ProjectionElems ::= appendP ( ProjectionElems , ProjectionElems ) [function, total]
351364
rule appendP(.ProjectionElems, TAIL) => TAIL
352365
rule appendP(X:ProjectionElem REST:ProjectionElems, TAIL) => X appendP(REST, TAIL)

‎kmir/src/kmir/kdist/mir-semantics/rt/types.md‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -99,6 +99,13 @@ Pointers to arrays/slices are compatible with pointers to the element type
9999
rule #allowsInteriorMutation(typeInfoStructType(NAME:String, _, _, _))
100100
=> findString(NAME, "UnsafeCell", 0) =/=Int -1
101101
rule #allowsInteriorMutation(_) => false [owise]
102+
103+
syntax Bool ::= #isRefMutTy ( TypeInfo ) [function, total]
104+
105+
rule #isRefMutTy(typeInfoStructType(NAME:String, _, _, _))
106+
=> findString(NAME, "RefMut<", 0) =/=Int -1
107+
rule #isRefMutTy(_)
108+
=> false [owise]
102109
```
103110

104111
## Determining types of places with projection

0 commit comments

Comments
 (0)