Skip to content

Commit fa9e197

Browse files
StevengreStevengre
committed
feat(not-ready)
1 parent 3c6d6b6 commit fa9e197

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
@@ -444,11 +444,136 @@ Other terminators that matter at the MIR level "Runtime" are `Drop` and `Unreach
444444
Drops are elaborated to Noops but still define the continuing control flow. Unreachable terminators lead to a program error.
445445

446446
```k
447-
rule [termDrop]: <k> #execTerminator(terminator(terminatorKindDrop(_PLACE, TARGET, _UNWIND), _SPAN))
447+
syntax KItem ::= #applyDrop(MaybeTy)
448+
| #dropValue(Value, MaybeTy)
449+
| #releaseBorrowRefMut(Value)
450+
| #releaseBorrowCell(Value)
451+
| #applyBorrowCell(Int, ProjectionElems)
452+
| #applyBorrowCellStack(Int, Int, ProjectionElems)
453+
454+
rule [termDrop]:
455+
<k> #execTerminator(terminator(terminatorKindDrop(place(local(I), PROJS), TARGET, _UNWIND), _SPAN))
448456
=>
449-
#execBlockIdx(TARGET)
457+
#traverseProjection(toLocal(I), getValue(LOCALS, I), PROJS, .Contexts)
458+
~> #readProjection(true)
459+
~> #applyDrop(getTyOf(tyOfLocal(getLocal(LOCALS, I)), PROJS))
460+
~> #execBlockIdx(TARGET)
450461
...
451462
</k>
463+
<locals> LOCALS </locals>
464+
requires 0 <=Int I
465+
andBool I <Int size(LOCALS)
466+
andBool isTypedLocal(LOCALS[I])
467+
[preserves-definedness] // valid local index checked
468+
469+
rule <k> VAL:Value ~> #applyDrop(MTY) => #dropValue(VAL, MTY) ... </k>
470+
471+
rule #dropValue(_:Value, MTY) => .K
472+
requires notBool #isRefMutTy(#lookupMaybeTy(MTY))
473+
474+
rule <k> #dropValue(Aggregate(_, ARGS), MTY)
475+
=> #releaseBorrowRefMut(getValue(ARGS, 1))
476+
...
477+
</k>
478+
requires #isRefMutTy(#lookupMaybeTy(MTY))
479+
andBool 1 <Int size(ARGS)
480+
481+
rule <k> #releaseBorrowRefMut(Aggregate(_, ListItem(PTR) _))
482+
=> #releaseBorrowCell(PTR)
483+
...
484+
</k>
485+
486+
rule #releaseBorrowRefMut(_) => .K [owise]
487+
488+
rule <k> #releaseBorrowCell(PtrLocal(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] // valid pointer target on current stack frame
500+
501+
rule <k> #releaseBorrowCell(Reference(0, place(local(J), PROJS), _, _))
502+
=>
503+
#traverseProjection(toLocal(J), getValue(LOCALS, J), PROJS, .Contexts)
504+
~> #readProjection(false)
505+
~> #applyBorrowCell(J, PROJS)
506+
...
507+
</k>
508+
<locals> LOCALS </locals>
509+
requires 0 <=Int J
510+
andBool J <Int size(LOCALS)
511+
andBool isTypedValue(LOCALS[J])
512+
[preserves-definedness]
513+
514+
rule <k> #releaseBorrowCell(PtrLocal(OFFSET, place(local(J), PROJS), _, _))
515+
=>
516+
#traverseProjection(
517+
toStack(OFFSET, local(J)),
518+
#localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(J), OFFSET),
519+
PROJS,
520+
.Contexts
521+
)
522+
~> #readProjection(false)
523+
~> #applyBorrowCellStack(OFFSET, J, PROJS)
524+
...
525+
</k>
526+
<stack> STACK </stack>
527+
requires 0 <Int OFFSET
528+
andBool OFFSET <=Int size(STACK)
529+
andBool isStackFrame(STACK[OFFSET -Int 1])
530+
[preserves-definedness]
531+
532+
rule <k> #releaseBorrowCell(Reference(OFFSET, place(local(J), PROJS), _, _))
533+
=>
534+
#traverseProjection(
535+
toStack(OFFSET, local(J)),
536+
#localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(J), OFFSET),
537+
PROJS,
538+
.Contexts
539+
)
540+
~> #readProjection(false)
541+
~> #applyBorrowCellStack(OFFSET, J, PROJS)
542+
...
543+
</k>
544+
<stack> STACK </stack>
545+
requires 0 <Int OFFSET
546+
andBool OFFSET <=Int size(STACK)
547+
andBool isStackFrame(STACK[OFFSET -Int 1])
548+
[preserves-definedness]
549+
550+
rule #releaseBorrowCell(_) => .K [owise]
551+
552+
rule <k> CELL:Value ~> #applyBorrowCell(J, PROJS)
553+
=> #setLocalValue(place(local(J), PROJS), #incCellBorrow(CELL))
554+
...
555+
</k>
556+
557+
rule #applyBorrowCell(_, _) => .K [owise]
558+
559+
rule <k> CELL:Value ~> #applyBorrowCellStack(OFFSET, J, PROJS)
560+
=>
561+
#traverseProjection(
562+
toStack(OFFSET, local(J)),
563+
#localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(J), OFFSET),
564+
PROJS,
565+
.Contexts
566+
)
567+
~> #writeProjection(#incCellBorrow(CELL))
568+
...
569+
</k>
570+
<stack> STACK </stack>
571+
requires 0 <Int OFFSET
572+
andBool OFFSET <=Int size(STACK)
573+
andBool isStackFrame(STACK[OFFSET -Int 1])
574+
[preserves-definedness]
575+
576+
rule #applyBorrowCellStack(_, _, _) => .K [owise]
452577
453578
syntax MIRError ::= "ReachedUnreachable"
454579

‎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)