From 70d9d29503e8799291aef74cfa6ed48446f7aa6d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 8 May 2025 14:20:06 +0000 Subject: [PATCH 1/3] kmir/rt/data: remove mutability checks in calculated #projectedUpdate --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index fac0115fc..1b7f5f4e4 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -446,7 +446,7 @@ The solution is to use rewrite operations in a downward pass through the project rule #projectedUpdate( DEST, - typedValue(Aggregate(IDX, ARGS), TY, MUT), + typedValue(Aggregate(IDX, ARGS), TY, _), projectionElemField(fieldIdx(I), _) PROJS, UPDATE, CTXTS, @@ -458,12 +458,11 @@ The solution is to use rewrite operations in a downward pass through the project requires 0 <=Int I andBool I #projectedUpdate( DEST, - typedValue(Range(ELEMENTS), TY, MUT), + typedValue(Range(ELEMENTS), TY, _), projectionElemIndex(local(LOCAL)) PROJS, UPDATE, CTXTS, @@ -487,12 +486,11 @@ The solution is to use rewrite operations in a downward pass through the project andBool 0 <=Int #expectUsize({LOCALS[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 #projectedUpdate( DEST, - typedValue(Range(ELEMENTS), TY, MUT), + typedValue(Range(ELEMENTS), TY, _), projectionElemConstantIndex(OFFSET:Int, _MINLEN, false) PROJS, UPDATE, CTXTS, @@ -511,12 +509,11 @@ The solution is to use rewrite operations in a downward pass through the project requires 0 <=Int OFFSET andBool OFFSET #projectedUpdate( DEST, - typedValue(Range(ELEMENTS), TY, MUT), + typedValue(Range(ELEMENTS), TY, _), projectionElemConstantIndex(OFFSET:Int, MINLEN, true) PROJS, // from end UPDATE, CTXTS, @@ -536,12 +533,11 @@ The solution is to use rewrite operations in a downward pass through the project andBool OFFSET <=Int MINLEN andBool MINLEN ==Int size(ELEMENTS) // assumed for valid MIR code andBool isTypedValue(ELEMENTS[MINLEN -Int OFFSET]) - andBool (FORCE orBool MUT ==K mutabilityMut) [preserves-definedness] // ELEMENT indexable and writeable or forced rule #projectedUpdate( _DEST, - typedValue(Reference(OFFSET, place(LOCAL, PLACEPROJ), MUT), _, _), + typedValue(Reference(OFFSET, place(LOCAL, PLACEPROJ), _), _, _), projectionElemDeref PROJS, UPDATE, _CTXTS, @@ -562,12 +558,11 @@ The solution is to use rewrite operations in a downward pass through the project requires 0 #projectedUpdate( _DEST, - typedValue(Reference(OFFSET, place(local(I), PLACEPROJ), MUT), _, _), + typedValue(Reference(OFFSET, place(local(I), PLACEPROJ), _), _, _), projectionElemDeref PROJS, UPDATE, _CTXTS, @@ -588,7 +583,6 @@ The solution is to use rewrite operations in a downward pass through the project requires OFFSET ==Int 0 andBool 0 <=Int I andBool I #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, false) From 25a9c16cd36480ac0007c141cb1bd4f99dea2c51 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 8 May 2025 15:34:00 +0000 Subject: [PATCH 2/3] kmir/rt/data: separate out writing from computing projection --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 92 ++++++++------------ 1 file changed, 37 insertions(+), 55 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 1b7f5f4e4..78d6fe1a5 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(toLocal(I), OLDLOCAL, PROJECTIONS, Moved, .Contexts, true) + #projectedUpdate(toLocal(I), OLDLOCAL, PROJECTIONS, .Contexts) ~> #writeProjectedUpdate(Moved, true) ~> VAL ~> CONT @@ -400,11 +400,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 ( WriteTo , TypedLocal, ProjectionElems, TypedLocal, Contexts , Bool ) + syntax KItem ::= #projectedUpdate ( WriteTo , TypedLocal, ProjectionElems, Contexts ) + | #writeProjectedUpdate ( TypedLocal , Bool ) rule #setLocalValue(place(local(I), PROJ), VAL) => - #projectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, PROJ, VAL, .Contexts, false) + #projectedUpdate(toLocal(I), {LOCALS[I]}:>TypedLocal, PROJ, .Contexts) ~> #writeProjectedUpdate(VAL, false) ... LOCALS @@ -448,11 +449,9 @@ The solution is to use rewrite operations in a downward pass through the project DEST, typedValue(Aggregate(IDX, ARGS), TY, _), projectionElemField(fieldIdx(I), _) PROJS, - UPDATE, - CTXTS, - FORCE + CTXTS ) => - #projectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, UPDATE, CtxField(TY, IDX, ARGS, I) CTXTS, FORCE) + #projectedUpdate(DEST, {ARGS[I]}:>TypedLocal, PROJS, CtxField(TY, IDX, ARGS, I) CTXTS) ... requires 0 <=Int I @@ -464,18 +463,15 @@ The solution is to use rewrite operations in a downward pass through the project DEST, typedValue(Range(ELEMENTS), TY, _), projectionElemIndex(local(LOCAL)) PROJS, - UPDATE, - CTXTS, - FORCE + CTXTS ) => #projectedUpdate( DEST, {ELEMENTS[#expectUsize({LOCALS[LOCAL]}:>TypedValue)]}:>TypedValue, PROJS, - UPDATE, - CtxIndex(TY, ELEMENTS, #expectUsize({LOCALS[LOCAL]}:>TypedValue)) CTXTS, - FORCE) + CtxIndex(TY, ELEMENTS, #expectUsize({LOCALS[LOCAL]}:>TypedValue)) CTXTS + ) ... LOCALS @@ -492,18 +488,15 @@ The solution is to use rewrite operations in a downward pass through the project DEST, typedValue(Range(ELEMENTS), TY, _), projectionElemConstantIndex(OFFSET:Int, _MINLEN, false) PROJS, - UPDATE, - CTXTS, - FORCE + CTXTS ) => #projectedUpdate( DEST, {ELEMENTS[OFFSET]}:>TypedValue, PROJS, - UPDATE, - CtxIndex(TY, ELEMENTS, OFFSET) CTXTS, - FORCE) + CtxIndex(TY, ELEMENTS, OFFSET) CTXTS + ) ... requires 0 <=Int OFFSET @@ -515,18 +508,15 @@ The solution is to use rewrite operations in a downward pass through the project DEST, typedValue(Range(ELEMENTS), TY, _), projectionElemConstantIndex(OFFSET:Int, MINLEN, true) PROJS, // from end - UPDATE, - CTXTS, - FORCE + CTXTS ) => #projectedUpdate( DEST, {ELEMENTS[OFFSET]}:>TypedValue, PROJS, - UPDATE, - CtxIndex(TY, ELEMENTS, MINLEN -Int OFFSET) CTXTS, - FORCE) + CtxIndex(TY, ELEMENTS, MINLEN -Int OFFSET) CTXTS + ) ... requires 0 #projectedUpdate( - _DEST, - typedValue(Reference(OFFSET, place(LOCAL, PLACEPROJ), _), _, _), - projectionElemDeref PROJS, - UPDATE, - _CTXTS, - FORCE - ) + _DEST, + typedValue(Reference(OFFSET, place(LOCAL, PLACEPROJ), _), _, _), + projectionElemDeref PROJS, + _CTXTS + ) => - #projectedUpdate( + #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 - ) + .Contexts // previous contexts obsolete + ) ... STACK @@ -561,22 +547,18 @@ The solution is to use rewrite operations in a downward pass through the project [preserves-definedness] rule #projectedUpdate( - _DEST, - typedValue(Reference(OFFSET, place(local(I), PLACEPROJ), _), _, _), - projectionElemDeref PROJS, - UPDATE, - _CTXTS, - FORCE - ) + _DEST, + typedValue(Reference(OFFSET, place(local(I), PLACEPROJ), _), _, _), + projectionElemDeref PROJS, + _CTXTS + ) => - #projectedUpdate( - toLocal(I), - {LOCALS[I]}:>TypedLocal, - appendP(PLACEPROJ, PROJS), // apply reference projections first, then rest - UPDATE, - .Contexts, // previous contexts obsolete - FORCE - ) + #projectedUpdate( + toLocal(I), + {LOCALS[I]}:>TypedLocal, + appendP(PLACEPROJ, PROJS), // apply reference projections first, then rest + .Contexts // previous contexts obsolete + ) ... LOCALS @@ -585,14 +567,14 @@ The solution is to use rewrite operations in a downward pass through the project andBool I #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, false) + rule #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, CONTEXTS) ~> #writeProjectedUpdate(NEW, 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) + rule #projectedUpdate(toLocal(I), _ORIGINAL, .ProjectionElems, CONTEXTS) ~> #writeProjectedUpdate(NEW, true) => #forceSetLocal(local(I), #buildUpdate(NEW, CONTEXTS)) ... @@ -612,7 +594,7 @@ The solution is to use rewrite operations in a downward pass through the project andBool I #projectedUpdate(toStack(FRAME, local(I)), _ORIGINAL, .ProjectionElems, NEW, CONTEXTS, _) => .K ... + rule #projectedUpdate(toStack(FRAME, local(I)), _ORIGINAL, .ProjectionElems, CONTEXTS) ~> #writeProjectedUpdate(NEW, _) => .K ... STACK => STACK[(FRAME -Int 1) <- From ad409486b9bce4abac78e9d09fb70c0b7c2c5df2 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 8 May 2025 16:22:33 +0000 Subject: [PATCH 3/3] Set Version: 0.3.152 --- 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 f9a956359..8cc9993ef 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kmir" -version = "0.3.151" +version = "0.3.152" description = "" requires-python = "~=3.10" dependencies = [ diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index d691d4e14..6c9d75a9c 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.151' +VERSION: Final = '0.3.152' diff --git a/kmir/uv.lock b/kmir/uv.lock index 46b3192a6..b74a5d05f 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -488,7 +488,7 @@ wheels = [ [[package]] name = "kmir" -version = "0.3.151" +version = "0.3.152" source = { editable = "." } dependencies = [ { name = "kframework" }, diff --git a/package/version b/package/version index c2211bb68..0f5719bf7 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.151 +0.3.152