From f7a840cf010d62197d6837ad2f165dfcdc7d570e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 7 May 2025 17:21:51 +0000 Subject: [PATCH 1/7] kmir/rt/data.md: factor out functional makeProjectedUpdate --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 162 ++++--------------- 1 file changed, 32 insertions(+), 130 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index e65426e32..a1cf42e3c 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -329,10 +329,12 @@ In contrast to regular write operations, the value does not have to be _mutable_ rule VAL:TypedLocal ~> #markMoved(OLDLOCAL, local(I), PROJECTIONS) ~> CONT => - #projectedUpdate(toLocal(I), OLDLOCAL, PROJECTIONS, Moved, .Contexts, true) + #projectedUpdate(makeProjectedUpdate(toLocal(I), OLDLOCAL, PROJECTIONS, Moved, .Contexts, true, STACK, LOCALS)) ~> VAL ~> CONT + STACK + LOCALS [preserves-definedness] // projections already used when reading ``` @@ -400,13 +402,15 @@ The `#setLocalValue` operation writes a `TypedLocal` value to a given `Place` wi Write operations to places that include (a chain of) projections are handled by a special rewrite symbol `#projectedUpdate`. ```k - syntax KItem ::= #projectedUpdate ( WriteTo , TypedLocal, ProjectionElems, TypedLocal, Contexts , Bool ) + syntax KItem ::= #projectedUpdate ( ProjectedUpdate ) + syntax ProjectedUpdate ::= makeProjectedUpdate(WriteTo, TypedLocal, ProjectionElems, TypedLocal, Contexts, Bool, List, List) [function] // total + | ProjectedUpdate(WriteTo, TypedLocal, TypedLocal, Contexts, Bool) rule #setLocalValue(place(local(I), PROJ), VAL) - => - #projectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, PROJ, VAL, .Contexts, false) + => #projectedUpdate(makeProjectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, PROJ, VAL, .Contexts, false, STACK, LOCALS)) ... + STACK LOCALS requires 0 <=Int I andBool I #buildUpdate(typedValue(Range(ELEMS[I <- VAL]), TY, mutabilityMut), CTXS) [preserves-definedness] // valid list indexing checked upon context construction - rule #projectedUpdate( - DEST, - typedValue(Aggregate(IDX, ARGS), TY, MUT), - projectionElemField(fieldIdx(I), _) PROJS, - UPDATE, - CTXTS, - FORCE - ) => - #projectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, UPDATE, CtxField(TY, IDX, ARGS, I) CTXTS, FORCE) - ... - + rule makeProjectedUpdate(DEST, typedValue(Aggregate(IDX, ARGS), TY, MUT), projectionElemField(fieldIdx(I), _) PROJS, UPDATE, CTXTS, FORCE, STACK, LOCALS) + => makeProjectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, UPDATE, CtxField(TY, IDX, ARGS, I) CTXTS, FORCE, STACK, LOCALS) requires 0 <=Int I andBool I #projectedUpdate( - DEST, - typedValue(Range(ELEMENTS), TY, MUT), - projectionElemIndex(local(LOCAL)) PROJS, - UPDATE, - CTXTS, - FORCE - ) - => - #projectedUpdate( - DEST, - {ELEMENTS[#expectUsize({LOCALS[LOCAL]}:>TypedValue)]}:>TypedValue, - PROJS, - UPDATE, - CtxIndex(TY, ELEMENTS, #expectUsize({LOCALS[LOCAL]}:>TypedValue)) CTXTS, - FORCE) - ... - - LOCALS + rule makeProjectedUpdate(DEST, typedValue(Range(ELEMENTS), TY, MUT), projectionElemIndex(local(LOCAL)) PROJS, UPDATE, CTXTS, FORCE, STACK, LOCALS) + => makeProjectedUpdate(DEST, {ELEMENTS[#expectUsize({LOCALS[LOCAL]}:>TypedValue)]}:>TypedValue, PROJS, UPDATE, CtxIndex(TY, ELEMENTS, #expectUsize({LOCALS[LOCAL]}:>TypedValue)) CTXTS, FORCE, STACK, LOCALS) requires 0 <=Int LOCAL andBool LOCAL #projectedUpdate( - DEST, - typedValue(Range(ELEMENTS), TY, MUT), - projectionElemConstantIndex(OFFSET:Int, _MINLEN, false) PROJS, - UPDATE, - CTXTS, - FORCE - ) - => - #projectedUpdate( - DEST, - {ELEMENTS[OFFSET]}:>TypedValue, - PROJS, - UPDATE, - CtxIndex(TY, ELEMENTS, OFFSET) CTXTS, - FORCE) - ... - + rule makeProjectedUpdate(DEST, typedValue(Range(ELEMENTS), TY, MUT), projectionElemConstantIndex(OFFSET:Int, _MINLEN, false) PROJS, UPDATE, CTXTS, FORCE, STACK, LOCALS) + => makeProjectedUpdate(DEST, {ELEMENTS[OFFSET]}:>TypedValue, PROJS, UPDATE, CtxIndex(TY, ELEMENTS, OFFSET) CTXTS, FORCE, STACK, LOCALS) requires 0 <=Int OFFSET andBool OFFSET #projectedUpdate( - DEST, - typedValue(Range(ELEMENTS), TY, MUT), - projectionElemConstantIndex(OFFSET:Int, MINLEN, true) PROJS, // from end - UPDATE, - CTXTS, - FORCE - ) - => - #projectedUpdate( - DEST, - {ELEMENTS[OFFSET]}:>TypedValue, - PROJS, - UPDATE, - CtxIndex(TY, ELEMENTS, MINLEN -Int OFFSET) CTXTS, - FORCE) - ... - + rule makeProjectedUpdate(DEST, typedValue(Range(ELEMENTS), TY, MUT), projectionElemConstantIndex(OFFSET:Int, MINLEN, true) PROJS, UPDATE, CTXTS, FORCE, STACK, LOCALS) + => makeProjectedUpdate(DEST, {ELEMENTS[OFFSET]}:>TypedValue, PROJS, UPDATE, CtxIndex(TY, ELEMENTS, MINLEN -Int OFFSET) CTXTS, FORCE, STACK, LOCALS) requires 0 #projectedUpdate( - _DEST, - typedValue(Reference(OFFSET, place(LOCAL, PLACEPROJ), MUT), _, _), - projectionElemDeref PROJS, - UPDATE, - _CTXTS, - FORCE - ) - => - #projectedUpdate( - toStack(OFFSET, LOCAL), - #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), - appendP(PLACEPROJ, PROJS), // apply reference projections first, then rest - UPDATE, - .Contexts, // previous contexts obsolete - FORCE - ) - ... - - STACK + rule makeProjectedUpdate(_DEST, typedValue(Reference(OFFSET, place(LOCAL, PLACEPROJ), MUT), _, _), projectionElemDeref PROJS, UPDATE, _CTXTS, FORCE, STACK, LOCALS) + => makeProjectedUpdate(toStack(OFFSET, LOCAL), #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), appendP(PLACEPROJ, PROJS), UPDATE, .Contexts, FORCE, STACK, LOCALS) requires 0 #projectedUpdate( - _DEST, - typedValue(Reference(OFFSET, place(local(I), PLACEPROJ), MUT), _, _), - projectionElemDeref PROJS, - UPDATE, - _CTXTS, - FORCE - ) - => - #projectedUpdate( - toLocal(I), - {LOCALS[I]}:>TypedLocal, - appendP(PLACEPROJ, PROJS), // apply reference projections first, then rest - UPDATE, - .Contexts, // previous contexts obsolete - FORCE - ) - ... - - LOCALS + rule makeProjectedUpdate(_DEST, typedValue(Reference(OFFSET, place(local(I), PLACEPROJ), MUT), _, _), projectionElemDeref PROJS, UPDATE, _CTXTS, FORCE, STACK, LOCALS) + => makeProjectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, appendP(PLACEPROJ, PROJS), UPDATE, .Contexts, FORCE, STACK, LOCALS) requires OFFSET ==Int 0 andBool 0 <=Int I andBool I #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, false) - => - #setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(NEW, CONTEXTS)) + rule makeProjectedUpdate(DEST, TV:TypedValue, .ProjectionElems, NEW, CONTEXTS, FORCE, _, _) + => ProjectedUpdate(DEST, TV, NEW, CONTEXTS, FORCE) + + rule #projectedUpdate(ProjectedUpdate(toLocal(I), _ORIGINAL, NEW, CONTEXTS, false)) + => #setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(NEW, CONTEXTS)) ... - + [preserves-definedness] // valid conmtext ensured upon context construction - rule #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, true) - => - #forceSetLocal(local(I), #buildUpdate(NEW, CONTEXTS)) + rule #projectedUpdate(ProjectedUpdate(toLocal(I), _ORIGINAL, NEW, CONTEXTS, true)) + => #forceSetLocal(local(I), #buildUpdate(NEW, CONTEXTS)) ... - + [preserves-definedness] // valid conmtext ensured upon context construction syntax KItem ::= #forceSetLocal ( Local , TypedLocal ) // #forceSetLocal sets the given value unconditionally (to write Moved values) - rule #forceSetLocal(local(I), VALUE) - => - .K - ... - + rule #forceSetLocal(local(I), VALUE) => .K ... LOCALS => LOCALS[I <- VALUE] requires 0 <=Int I andBool I #projectedUpdate(toStack(FRAME, local(I)), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, _) => .K ... - STACK - => - STACK[(FRAME -Int 1) <- - #updateStackLocal({STACK[FRAME -Int 1]}:>StackFrame, I, #buildUpdate(NEW, CONTEXTS)) - ] - + rule #projectedUpdate(ProjectedUpdate(toStack(FRAME, local(I)), _ORIGINAL, NEW, CONTEXTS, _)) => .K ... + STACK => STACK[(FRAME -Int 1) <- #updateStackLocal({STACK[FRAME -Int 1]}:>StackFrame, I, #buildUpdate(NEW, CONTEXTS)) ] requires 0 Date: Wed, 7 May 2025 17:35:04 +0000 Subject: [PATCH 2/7] kmir/rt/data: remove uneeded state from makeProjectedUpdate function --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 44 ++++++++++---------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index a1cf42e3c..92dcdb1d0 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -329,7 +329,7 @@ In contrast to regular write operations, the value does not have to be _mutable_ rule VAL:TypedLocal ~> #markMoved(OLDLOCAL, local(I), PROJECTIONS) ~> CONT => - #projectedUpdate(makeProjectedUpdate(toLocal(I), OLDLOCAL, PROJECTIONS, Moved, .Contexts, true, STACK, LOCALS)) + #projectedUpdate(makeProjectedUpdate(toLocal(I), OLDLOCAL, PROJECTIONS, .Contexts, true, STACK, LOCALS), Moved) ~> VAL ~> CONT @@ -402,12 +402,12 @@ The `#setLocalValue` operation writes a `TypedLocal` value to a given `Place` wi Write operations to places that include (a chain of) projections are handled by a special rewrite symbol `#projectedUpdate`. ```k - syntax KItem ::= #projectedUpdate ( ProjectedUpdate ) - syntax ProjectedUpdate ::= makeProjectedUpdate(WriteTo, TypedLocal, ProjectionElems, TypedLocal, Contexts, Bool, List, List) [function] // total - | ProjectedUpdate(WriteTo, TypedLocal, TypedLocal, Contexts, Bool) + syntax KItem ::= #projectedUpdate ( ProjectedUpdate , TypedLocal ) + syntax ProjectedUpdate ::= makeProjectedUpdate(WriteTo, TypedLocal, ProjectionElems, Contexts, Bool, List, List) [function] // total + | ProjectedUpdate(WriteTo, Contexts, Bool) rule #setLocalValue(place(local(I), PROJ), VAL) - => #projectedUpdate(makeProjectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, PROJ, VAL, .Contexts, false, STACK, LOCALS)) + => #projectedUpdate(makeProjectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, PROJ, .Contexts, false, STACK, LOCALS), VAL) ... STACK @@ -448,16 +448,16 @@ The solution is to use rewrite operations in a downward pass through the project => #buildUpdate(typedValue(Range(ELEMS[I <- VAL]), TY, mutabilityMut), CTXS) [preserves-definedness] // valid list indexing checked upon context construction - rule makeProjectedUpdate(DEST, typedValue(Aggregate(IDX, ARGS), TY, MUT), projectionElemField(fieldIdx(I), _) PROJS, UPDATE, CTXTS, FORCE, STACK, LOCALS) - => makeProjectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, UPDATE, CtxField(TY, IDX, ARGS, I) CTXTS, FORCE, STACK, LOCALS) + rule makeProjectedUpdate(DEST, typedValue(Aggregate(IDX, ARGS), TY, MUT), projectionElemField(fieldIdx(I), _) PROJS, CTXTS, FORCE, STACK, LOCALS) + => makeProjectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, CtxField(TY, IDX, ARGS, I) CTXTS, FORCE, STACK, LOCALS) requires 0 <=Int I andBool I makeProjectedUpdate(DEST, {ELEMENTS[#expectUsize({LOCALS[LOCAL]}:>TypedValue)]}:>TypedValue, PROJS, UPDATE, CtxIndex(TY, ELEMENTS, #expectUsize({LOCALS[LOCAL]}:>TypedValue)) CTXTS, FORCE, STACK, LOCALS) + rule makeProjectedUpdate(DEST, typedValue(Range(ELEMENTS), TY, MUT), projectionElemIndex(local(LOCAL)) PROJS, CTXTS, FORCE, STACK, LOCALS) + => makeProjectedUpdate(DEST, {ELEMENTS[#expectUsize({LOCALS[LOCAL]}:>TypedValue)]}:>TypedValue, PROJS, CtxIndex(TY, ELEMENTS, #expectUsize({LOCALS[LOCAL]}:>TypedValue)) CTXTS, FORCE, STACK, LOCALS) requires 0 <=Int LOCAL andBool LOCAL makeProjectedUpdate(DEST, {ELEMENTS[OFFSET]}:>TypedValue, PROJS, UPDATE, CtxIndex(TY, ELEMENTS, OFFSET) CTXTS, FORCE, STACK, LOCALS) + rule makeProjectedUpdate(DEST, typedValue(Range(ELEMENTS), TY, MUT), projectionElemConstantIndex(OFFSET:Int, _MINLEN, false) PROJS, CTXTS, FORCE, STACK, LOCALS) + => makeProjectedUpdate(DEST, {ELEMENTS[OFFSET]}:>TypedValue, PROJS, CtxIndex(TY, ELEMENTS, OFFSET) CTXTS, FORCE, STACK, LOCALS) requires 0 <=Int OFFSET andBool OFFSET makeProjectedUpdate(DEST, {ELEMENTS[OFFSET]}:>TypedValue, PROJS, UPDATE, CtxIndex(TY, ELEMENTS, MINLEN -Int OFFSET) CTXTS, FORCE, STACK, LOCALS) + rule makeProjectedUpdate(DEST, typedValue(Range(ELEMENTS), TY, MUT), projectionElemConstantIndex(OFFSET:Int, MINLEN, true) PROJS, CTXTS, FORCE, STACK, LOCALS) + => makeProjectedUpdate(DEST, {ELEMENTS[OFFSET]}:>TypedValue, PROJS, CtxIndex(TY, ELEMENTS, MINLEN -Int OFFSET) CTXTS, FORCE, STACK, LOCALS) requires 0 makeProjectedUpdate(toStack(OFFSET, LOCAL), #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), appendP(PLACEPROJ, PROJS), UPDATE, .Contexts, FORCE, STACK, LOCALS) + rule makeProjectedUpdate(_DEST, typedValue(Reference(OFFSET, place(LOCAL, PLACEPROJ), MUT), _, _), projectionElemDeref PROJS, _CTXTS, FORCE, STACK, LOCALS) + => makeProjectedUpdate(toStack(OFFSET, LOCAL), #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), appendP(PLACEPROJ, PROJS), .Contexts, FORCE, STACK, LOCALS) requires 0 makeProjectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, appendP(PLACEPROJ, PROJS), UPDATE, .Contexts, FORCE, STACK, LOCALS) + rule makeProjectedUpdate(_DEST, typedValue(Reference(OFFSET, place(local(I), PLACEPROJ), MUT), _, _), projectionElemDeref PROJS, _CTXTS, FORCE, STACK, LOCALS) + => makeProjectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, appendP(PLACEPROJ, PROJS), .Contexts, FORCE, STACK, LOCALS) requires OFFSET ==Int 0 andBool 0 <=Int I andBool I ProjectedUpdate(DEST, TV, NEW, CONTEXTS, FORCE) + rule makeProjectedUpdate(DEST, _:TypedValue, .ProjectionElems, CONTEXTS, FORCE, _, _) + => ProjectedUpdate(DEST, CONTEXTS, FORCE) - rule #projectedUpdate(ProjectedUpdate(toLocal(I), _ORIGINAL, NEW, CONTEXTS, false)) + rule #projectedUpdate(ProjectedUpdate(toLocal(I), CONTEXTS, false), NEW) => #setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(NEW, CONTEXTS)) ... [preserves-definedness] // valid conmtext ensured upon context construction - rule #projectedUpdate(ProjectedUpdate(toLocal(I), _ORIGINAL, NEW, CONTEXTS, true)) + rule #projectedUpdate(ProjectedUpdate(toLocal(I), CONTEXTS, true), NEW) => #forceSetLocal(local(I), #buildUpdate(NEW, CONTEXTS)) ... @@ -525,7 +525,7 @@ The solution is to use rewrite operations in a downward pass through the project andBool I #projectedUpdate(ProjectedUpdate(toStack(FRAME, local(I)), _ORIGINAL, NEW, CONTEXTS, _)) => .K ... + rule #projectedUpdate(ProjectedUpdate(toStack(FRAME, local(I)), CONTEXTS, _), NEW) => .K ... STACK => STACK[(FRAME -Int 1) <- #updateStackLocal({STACK[FRAME -Int 1]}:>StackFrame, I, #buildUpdate(NEW, CONTEXTS)) ] requires 0 Date: Wed, 7 May 2025 17:40:53 +0000 Subject: [PATCH 3/7] kmir/rt/data: remove mut checks from makeProjectedUpdate, only for final write --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 50 +++++++++----------- 1 file changed, 22 insertions(+), 28 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 92dcdb1d0..66194e98b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -329,7 +329,7 @@ In contrast to regular write operations, the value does not have to be _mutable_ rule VAL:TypedLocal ~> #markMoved(OLDLOCAL, local(I), PROJECTIONS) ~> CONT => - #projectedUpdate(makeProjectedUpdate(toLocal(I), OLDLOCAL, PROJECTIONS, .Contexts, true, STACK, LOCALS), Moved) + #projectedUpdate(makeProjectedUpdate(toLocal(I), OLDLOCAL, PROJECTIONS, .Contexts, STACK, LOCALS), Moved, true) ~> VAL ~> CONT @@ -402,12 +402,12 @@ The `#setLocalValue` operation writes a `TypedLocal` value to a given `Place` wi Write operations to places that include (a chain of) projections are handled by a special rewrite symbol `#projectedUpdate`. ```k - syntax KItem ::= #projectedUpdate ( ProjectedUpdate , TypedLocal ) - syntax ProjectedUpdate ::= makeProjectedUpdate(WriteTo, TypedLocal, ProjectionElems, Contexts, Bool, List, List) [function] // total - | ProjectedUpdate(WriteTo, Contexts, Bool) + syntax KItem ::= #projectedUpdate ( ProjectedUpdate , TypedLocal , Bool ) + syntax ProjectedUpdate ::= makeProjectedUpdate(WriteTo, TypedLocal, ProjectionElems, Contexts, List, List) [function] // total + | ProjectedUpdate(WriteTo, Contexts) rule #setLocalValue(place(local(I), PROJ), VAL) - => #projectedUpdate(makeProjectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, PROJ, .Contexts, false, STACK, LOCALS), VAL) + => #projectedUpdate(makeProjectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, PROJ, .Contexts, STACK, LOCALS), VAL, false) ... STACK @@ -448,16 +448,15 @@ The solution is to use rewrite operations in a downward pass through the project => #buildUpdate(typedValue(Range(ELEMS[I <- VAL]), TY, mutabilityMut), CTXS) [preserves-definedness] // valid list indexing checked upon context construction - rule makeProjectedUpdate(DEST, typedValue(Aggregate(IDX, ARGS), TY, MUT), projectionElemField(fieldIdx(I), _) PROJS, CTXTS, FORCE, STACK, LOCALS) - => makeProjectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, CtxField(TY, IDX, ARGS, I) CTXTS, FORCE, STACK, LOCALS) + rule makeProjectedUpdate(DEST, typedValue(Aggregate(IDX, ARGS), TY, _), projectionElemField(fieldIdx(I), _) PROJS, CTXTS, STACK, LOCALS) + => makeProjectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, CtxField(TY, IDX, ARGS, I) CTXTS, STACK, LOCALS) requires 0 <=Int I andBool I makeProjectedUpdate(DEST, {ELEMENTS[#expectUsize({LOCALS[LOCAL]}:>TypedValue)]}:>TypedValue, PROJS, CtxIndex(TY, ELEMENTS, #expectUsize({LOCALS[LOCAL]}:>TypedValue)) CTXTS, FORCE, STACK, LOCALS) + rule makeProjectedUpdate(DEST, typedValue(Range(ELEMENTS), TY, _), projectionElemIndex(local(LOCAL)) PROJS, CTXTS, STACK, LOCALS) + => makeProjectedUpdate(DEST, {ELEMENTS[#expectUsize({LOCALS[LOCAL]}:>TypedValue)]}:>TypedValue, PROJS, CtxIndex(TY, ELEMENTS, #expectUsize({LOCALS[LOCAL]}:>TypedValue)) CTXTS, STACK, LOCALS) requires 0 <=Int LOCAL andBool LOCAL TypedValue) andBool #expectUsize({LOCALS[LOCAL]}:>TypedValue) TypedValue)]) - andBool (FORCE orBool MUT ==K mutabilityMut) [preserves-definedness] // index checked, valid Int can be read, ELEMENT indexable and writeable or forced - rule makeProjectedUpdate(DEST, typedValue(Range(ELEMENTS), TY, MUT), projectionElemConstantIndex(OFFSET:Int, _MINLEN, false) PROJS, CTXTS, FORCE, STACK, LOCALS) - => makeProjectedUpdate(DEST, {ELEMENTS[OFFSET]}:>TypedValue, PROJS, CtxIndex(TY, ELEMENTS, OFFSET) CTXTS, FORCE, STACK, LOCALS) + rule makeProjectedUpdate(DEST, typedValue(Range(ELEMENTS), TY, _), projectionElemConstantIndex(OFFSET:Int, _MINLEN, false) PROJS, CTXTS, STACK, LOCALS) + => makeProjectedUpdate(DEST, {ELEMENTS[OFFSET]}:>TypedValue, PROJS, CtxIndex(TY, ELEMENTS, OFFSET) CTXTS, STACK, LOCALS) requires 0 <=Int OFFSET andBool OFFSET makeProjectedUpdate(DEST, {ELEMENTS[OFFSET]}:>TypedValue, PROJS, CtxIndex(TY, ELEMENTS, MINLEN -Int OFFSET) CTXTS, FORCE, STACK, LOCALS) + rule makeProjectedUpdate(DEST, typedValue(Range(ELEMENTS), TY, _), projectionElemConstantIndex(OFFSET:Int, MINLEN, true) PROJS, CTXTS, STACK, LOCALS) + => makeProjectedUpdate(DEST, {ELEMENTS[OFFSET]}:>TypedValue, PROJS, CtxIndex(TY, ELEMENTS, MINLEN -Int OFFSET) CTXTS, STACK, LOCALS) requires 0 makeProjectedUpdate(toStack(OFFSET, LOCAL), #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), appendP(PLACEPROJ, PROJS), .Contexts, FORCE, STACK, LOCALS) + rule makeProjectedUpdate(_DEST, typedValue(Reference(OFFSET, place(LOCAL, PLACEPROJ), _), _, _), projectionElemDeref PROJS, _CTXTS, STACK, LOCALS) + => makeProjectedUpdate(toStack(OFFSET, LOCAL), #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), appendP(PLACEPROJ, PROJS), .Contexts, STACK, LOCALS) requires 0 makeProjectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, appendP(PLACEPROJ, PROJS), .Contexts, FORCE, STACK, LOCALS) + rule makeProjectedUpdate(_DEST, typedValue(Reference(OFFSET, place(local(I), PLACEPROJ), _), _, _), projectionElemDeref PROJS, _CTXTS, STACK, LOCALS) + => makeProjectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, appendP(PLACEPROJ, PROJS), .Contexts, STACK, LOCALS) requires OFFSET ==Int 0 andBool 0 <=Int I andBool I ProjectedUpdate(DEST, CONTEXTS, FORCE) + rule makeProjectedUpdate(DEST, _:TypedValue, .ProjectionElems, CONTEXTS, _, _) + => ProjectedUpdate(DEST, CONTEXTS) - rule #projectedUpdate(ProjectedUpdate(toLocal(I), CONTEXTS, false), NEW) + rule #projectedUpdate(ProjectedUpdate(toLocal(I), CONTEXTS), NEW, false) => #setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(NEW, CONTEXTS)) ... [preserves-definedness] // valid conmtext ensured upon context construction - rule #projectedUpdate(ProjectedUpdate(toLocal(I), CONTEXTS, true), NEW) + rule #projectedUpdate(ProjectedUpdate(toLocal(I), CONTEXTS), NEW, true) => #forceSetLocal(local(I), #buildUpdate(NEW, CONTEXTS)) ... @@ -525,7 +519,7 @@ The solution is to use rewrite operations in a downward pass through the project andBool I #projectedUpdate(ProjectedUpdate(toStack(FRAME, local(I)), CONTEXTS, _), NEW) => .K ... + rule #projectedUpdate(ProjectedUpdate(toStack(FRAME, local(I)), CONTEXTS), NEW, _) => .K ... STACK => STACK[(FRAME -Int 1) <- #updateStackLocal({STACK[FRAME -Int 1]}:>StackFrame, I, #buildUpdate(NEW, CONTEXTS)) ] requires 0 Date: Fri, 9 May 2025 14:41:58 +0000 Subject: [PATCH 4/7] kmir/rt/data: formatting and more compact function definition for readProjection --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 85 ++++++++++++++------ 1 file changed, 61 insertions(+), 24 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 66194e98b..a5d8120a2 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -329,7 +329,7 @@ In contrast to regular write operations, the value does not have to be _mutable_ rule VAL:TypedLocal ~> #markMoved(OLDLOCAL, local(I), PROJECTIONS) ~> CONT => - #projectedUpdate(makeProjectedUpdate(toLocal(I), OLDLOCAL, PROJECTIONS, .Contexts, STACK, LOCALS), Moved, true) + #projectedUpdate(#readProjection(toLocal(I), OLDLOCAL, PROJECTIONS, .Contexts, STACK, LOCALS), Moved, true) ~> VAL ~> CONT @@ -403,11 +403,9 @@ Write operations to places that include (a chain of) projections are handled by ```k syntax KItem ::= #projectedUpdate ( ProjectedUpdate , TypedLocal , Bool ) - syntax ProjectedUpdate ::= makeProjectedUpdate(WriteTo, TypedLocal, ProjectionElems, Contexts, List, List) [function] // total - | ProjectedUpdate(WriteTo, Contexts) rule #setLocalValue(place(local(I), PROJ), VAL) - => #projectedUpdate(makeProjectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, PROJ, .Contexts, STACK, LOCALS), VAL, false) + => #projectedUpdate(#readProjection(toLocal(I), {LOCALS[I]}:>TypedLocal, PROJ, .Contexts, STACK, LOCALS), VAL, false) ... STACK @@ -430,33 +428,48 @@ The solution is to use rewrite operations in a downward pass through the project | toStack ( Int , Local ) // retains information about the value that was deconstructed by a projection - syntax Context ::= CtxField( Ty, VariantIdx, List, Int ) - | CtxIndex( Ty, List , Int ) // array index constant or has been read before + syntax Context ::= CtxField( Ty, VariantIdx, List, Int, Mutability) + | CtxIndex( Ty, List, Int, Mutability) // array index constant or has been read before syntax Contexts ::= List{Context, ""} syntax TypedLocal ::= #buildUpdate ( TypedLocal, Contexts ) [function] - + // ------------------------------------------------------------------- rule #buildUpdate(VAL, .Contexts) => VAL [preserves-definedness] - rule #buildUpdate(VAL, CtxField(TY, IDX, ARGS, I) CTXS) - => #buildUpdate(typedValue(Aggregate(IDX, ARGS[I <- VAL]), TY, mutabilityMut), CTXS) + rule #buildUpdate(VAL, CtxField(TY, IDX, ARGS, I, MUT) CTXS) + => #buildUpdate(typedValue(Aggregate(IDX, ARGS[I <- VAL]), TY, MUT), CTXS) [preserves-definedness] // valid list indexing checked upon context construction - rule #buildUpdate(VAL, CtxIndex(TY, ELEMS, I) CTXS) - => #buildUpdate(typedValue(Range(ELEMS[I <- VAL]), TY, mutabilityMut), CTXS) + rule #buildUpdate(VAL, CtxIndex(TY, ELEMS, I, MUT) CTXS) + => #buildUpdate(typedValue(Range(ELEMS[I <- VAL]), TY, MUT), CTXS) [preserves-definedness] // valid list indexing checked upon context construction - rule makeProjectedUpdate(DEST, typedValue(Aggregate(IDX, ARGS), TY, _), projectionElemField(fieldIdx(I), _) PROJS, CTXTS, STACK, LOCALS) - => makeProjectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, CtxField(TY, IDX, ARGS, I) CTXTS, STACK, LOCALS) + syntax ProjectedUpdate ::= #readProjection(WriteTo, TypedLocal, ProjectionElems, Contexts, List, List) [function] // total + | ProjectedUpdate(WriteTo, Contexts) + // ---------------------------------------------------------- + rule #readProjection( + _DEST, + typedValue(Aggregate(IDX, ARGS), TY, MUT) => {ARGS[I]}:>TypedLocal, + projectionElemField(fieldIdx(I), TY) PROJS => PROJS, + CTXTS => CtxField(TY, IDX, ARGS, I, MUT) CTXTS, + _STACK, + _LOCALS + ) requires 0 <=Int I andBool I makeProjectedUpdate(DEST, {ELEMENTS[#expectUsize({LOCALS[LOCAL]}:>TypedValue)]}:>TypedValue, PROJS, CtxIndex(TY, ELEMENTS, #expectUsize({LOCALS[LOCAL]}:>TypedValue)) CTXTS, STACK, LOCALS) + rule #readProjection( + _DEST, + typedValue(Range(ELEMENTS), TY, MUT) => {ELEMENTS[#expectUsize({LOCALS[LOCAL]}:>TypedValue)]}:>TypedValue, + projectionElemIndex(local(LOCAL)) PROJS => PROJS, + CTXTS => CtxIndex(TY, ELEMENTS, #expectUsize({LOCALS[LOCAL]}:>TypedValue), MUT) CTXTS, + _STACK, + LOCALS + ) requires 0 <=Int LOCAL andBool LOCAL TypedValue)]) [preserves-definedness] // index checked, valid Int can be read, ELEMENT indexable and writeable or forced - rule makeProjectedUpdate(DEST, typedValue(Range(ELEMENTS), TY, _), projectionElemConstantIndex(OFFSET:Int, _MINLEN, false) PROJS, CTXTS, STACK, LOCALS) - => makeProjectedUpdate(DEST, {ELEMENTS[OFFSET]}:>TypedValue, PROJS, CtxIndex(TY, ELEMENTS, OFFSET) CTXTS, STACK, LOCALS) + rule #readProjection( + _DEST, + typedValue(Range(ELEMENTS), TY, MUT) => {ELEMENTS[OFFSET]}:>TypedValue, + projectionElemConstantIndex(OFFSET:Int, _MINLEN, false) PROJS => PROJS, + CTXTS => CtxIndex(TY, ELEMENTS, OFFSET, MUT) CTXTS, + _STACK, + _LOCALS + ) requires 0 <=Int OFFSET andBool OFFSET makeProjectedUpdate(DEST, {ELEMENTS[OFFSET]}:>TypedValue, PROJS, CtxIndex(TY, ELEMENTS, MINLEN -Int OFFSET) CTXTS, STACK, LOCALS) + rule #readProjection( + _DEST, + typedValue(Range(ELEMENTS), TY, MUT) => {ELEMENTS[OFFSET]}:>TypedValue, + projectionElemConstantIndex(OFFSET:Int, MINLEN, true) PROJS => PROJS, + CTXTS => CtxIndex(TY, ELEMENTS, MINLEN -Int OFFSET, MUT) CTXTS, + _STACK, + _LOCALS + ) requires 0 makeProjectedUpdate(toStack(OFFSET, LOCAL), #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, LOCAL, OFFSET), appendP(PLACEPROJ, PROJS), .Contexts, STACK, LOCALS) + rule #readProjection( + _DEST => toStack(OFFSET, LOCAL), + typedValue(Reference(OFFSET, place(LOCAL, PLACEPROJ), _), _, _), + projectionElemDeref PROJS => appendP(PLACEPROJ, PROJS), + _CTXTS => .Contexts, + STACK, + _LOCALS + ) requires 0 makeProjectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, appendP(PLACEPROJ, PROJS), .Contexts, STACK, LOCALS) + rule #readProjection( + _DEST => toLocal(I), + typedValue(Reference(OFFSET, place(local(I), PLACEPROJ), _), _, _) => {LOCALS[I]}:>TypedLocal, + projectionElemDeref PROJS => appendP(PLACEPROJ, PROJS), + _CTXTS => .Contexts, + _STACK, + LOCALS + ) requires OFFSET ==Int 0 andBool 0 <=Int I andBool I ProjectedUpdate(DEST, CONTEXTS) rule #projectedUpdate(ProjectedUpdate(toLocal(I), CONTEXTS), NEW, false) From 77abeec9541fe23555af05448be83761353e481d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 9 May 2025 14:47:04 +0000 Subject: [PATCH 5/7] kmir/rt/data: add back in mutability check on final searched value --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index a5d8120a2..95a1a3d6e 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -447,8 +447,8 @@ The solution is to use rewrite operations in a downward pass through the project [preserves-definedness] // valid list indexing checked upon context construction syntax ProjectedUpdate ::= #readProjection(WriteTo, TypedLocal, ProjectionElems, Contexts, List, List) [function] // total - | ProjectedUpdate(WriteTo, Contexts) - // ---------------------------------------------------------- + | ProjectedUpdate(WriteTo, TypedValue, Contexts) + // ---------------------------------------------------------------------- rule #readProjection( _DEST, typedValue(Aggregate(IDX, ARGS), TY, MUT) => {ARGS[I]}:>TypedLocal, @@ -532,16 +532,16 @@ The solution is to use rewrite operations in a downward pass through the project andBool I ProjectedUpdate(DEST, CONTEXTS) + rule #readProjection(DEST, TV:TypedValue, .ProjectionElems, CONTEXTS, _, _) + => ProjectedUpdate(DEST, TV, CONTEXTS) - rule #projectedUpdate(ProjectedUpdate(toLocal(I), CONTEXTS), NEW, false) + rule #projectedUpdate(ProjectedUpdate(toLocal(I), typedValue(_, _, mutabilityMut), CONTEXTS), NEW, false) => #setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(NEW, CONTEXTS)) ... [preserves-definedness] // valid conmtext ensured upon context construction - rule #projectedUpdate(ProjectedUpdate(toLocal(I), CONTEXTS), NEW, true) + rule #projectedUpdate(ProjectedUpdate(toLocal(I), _, CONTEXTS), NEW, true) => #forceSetLocal(local(I), #buildUpdate(NEW, CONTEXTS)) ... @@ -556,7 +556,7 @@ The solution is to use rewrite operations in a downward pass through the project andBool I #projectedUpdate(ProjectedUpdate(toStack(FRAME, local(I)), CONTEXTS), NEW, _) => .K ... + rule #projectedUpdate(ProjectedUpdate(toStack(FRAME, local(I)), typedValue(_, _, mutabilityMut), CONTEXTS), NEW, _) => .K ... STACK => STACK[(FRAME -Int 1) <- #updateStackLocal({STACK[FRAME -Int 1]}:>StackFrame, I, #buildUpdate(NEW, CONTEXTS)) ] requires 0 Date: Fri, 9 May 2025 15:01:48 +0000 Subject: [PATCH 6/7] kmir/rt/data: refactor #projectedUpdate to not use #setLocalValue recursively --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 95a1a3d6e..82c265772 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -535,16 +535,11 @@ The solution is to use rewrite operations in a downward pass through the project rule #readProjection(DEST, TV:TypedValue, .ProjectionElems, CONTEXTS, _, _) => ProjectedUpdate(DEST, TV, CONTEXTS) - rule #projectedUpdate(ProjectedUpdate(toLocal(I), typedValue(_, _, mutabilityMut), CONTEXTS), NEW, false) - => #setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(NEW, CONTEXTS)) - ... - - [preserves-definedness] // valid conmtext ensured upon context construction - - rule #projectedUpdate(ProjectedUpdate(toLocal(I), _, CONTEXTS), NEW, true) + rule #projectedUpdate(ProjectedUpdate(toLocal(I), typedValue(_, _, MUT), CONTEXTS), NEW, FORCE) => #forceSetLocal(local(I), #buildUpdate(NEW, CONTEXTS)) ... + requires MUT ==K mutabilityMut orBool FORCE [preserves-definedness] // valid conmtext ensured upon context construction syntax KItem ::= #forceSetLocal ( Local , TypedLocal ) From c2be9f7863c28ea0c39885c682996dca08195112 Mon Sep 17 00:00:00 2001 From: devops Date: Sat, 10 May 2025 14:46:45 +0000 Subject: [PATCH 7/7] Set Version: 0.3.158 --- kmir/pyproject.toml | 2 +- kmir/src/kmir/__init__.py | 2 +- kmir/uv.lock | 2 +- package/version | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index a15931f5a..0e334eac2 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kmir" -version = "0.3.157" +version = "0.3.158" description = "" requires-python = "~=3.10" dependencies = [ diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 11b8242a1..e7190a888 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -1,3 +1,3 @@ from typing import Final -VERSION: Final = '0.3.157' +VERSION: Final = '0.3.158' diff --git a/kmir/uv.lock b/kmir/uv.lock index 2b98ee015..ea9e06603 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -488,7 +488,7 @@ wheels = [ [[package]] name = "kmir" -version = "0.3.157" +version = "0.3.158" source = { editable = "." } dependencies = [ { name = "kframework" }, diff --git a/package/version b/package/version index a03f12adb..9f8523ca8 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.157 +0.3.158