Skip to content

Commit 92056cd

Browse files
authored
cleanup(rt): remove redundant #forceSetLocal (#810)
## Summary - remove the redundant `#forceSetLocal` helper now that `#setLocalValue` no longer guards on mutability - route moved-writeback and zero-sized-local initialization through `#setLocalValue` - drop the obsolete interior-mutability fast-path introduced by the old branch state ## Why After rebasing onto current `origin/master`, the original interior-mutability writeback fast-path became obsolete: `#setLocalValue` already permits writes to immutable locals, so the extra helper and its special-case callsites no longer buy any behavior. This PR turns the branch into the cleanup that current master actually needs. ## Validation - `make build` - `cd kmir && uv run pytest src/tests/integration/test_integration.py -v --timeout=600 -k "interior-mut or transmute-maybe-uninit-fail" -x` - 4 passed, 261 deselected - started `make test-integration`; no early failures before stopping due runtime
1 parent b694d02 commit 92056cd

1 file changed

Lines changed: 3 additions & 12 deletions

File tree

  • kmir/src/kmir/kdist/mir-semantics/rt

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

Lines changed: 3 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -178,15 +178,11 @@ In contrast to regular write operations, the value does not have to be _mutable_
178178

179179
The `#setLocalValue` operation writes a `Value` value to a given `Place` within the `List` of local variables currently on top of the stack.
180180
If we are setting a value at a `Place` which has `Projection`s in it, then we must first traverse the projections before setting the value.
181-
A variant `#forceSetLocal` is provided for setting the local value without checking the mutability of the location.
182181

183182
**Note on mutability:** The Rust compiler validates assignment legality and may reuse immutable locals in MIR (e.g., loop variables), so `#setLocalValue` does not guard on mutability.
184183

185-
TODO: `#forceSetLocal` is now functionally identical to `#setLocalValue` and may be removed.
186-
187184
```k
188185
syntax KItem ::= #setLocalValue( Place, Evaluation ) [strict(2)]
189-
| #forceSetLocal ( Local , Evaluation ) [strict(2)]
190186
191187
rule <k> #setLocalValue(place(local(I), .ProjectionElems), VAL) => .K ... </k>
192188
<locals>
@@ -216,11 +212,6 @@ TODO: `#forceSetLocal` is now functionally identical to `#setLocalValue` and may
216212
andBool isTypedValue(LOCALS[I])
217213
[preserves-definedness] // valid list indexing and sort checked
218214
219-
rule <k> #forceSetLocal(local(I), MBVAL:Value) => .K ... </k>
220-
<locals> LOCALS => LOCALS[I <- typedValue(MBVAL, tyOfLocal(getLocal(LOCALS, I)), mutabilityOf(getLocal(LOCALS, I)))] </locals>
221-
requires 0 <=Int I andBool I <Int size(LOCALS)
222-
andBool isTypedLocal(LOCALS[I])
223-
[preserves-definedness] // valid list indexing checked
224215
```
225216

226217
### Traversing Projections for Reads and Writes
@@ -270,7 +261,7 @@ A `Deref` projection in the projections list changes the target of the write ope
270261
271262
rule <k> #traverseProjection(toLocal(I), _ORIGINAL, .ProjectionElems, CONTEXTS)
272263
~> #writeMoved
273-
=> #forceSetLocal(local(I), #buildUpdate(Moved, CONTEXTS)) // TODO retain Ty and Mutability from _ORIGINAL
264+
=> #setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(Moved, CONTEXTS)) // TODO retain Ty and Mutability from _ORIGINAL
274265
...
275266
</k>
276267
[preserves-definedness] // valid context ensured upon context construction
@@ -1238,8 +1229,8 @@ This eliminates any `Deref` projections from the place, and also resolves `Index
12381229
12391230
// Borrowing a zero-sized local that is still `NewLocal`: initialise it, then reuse the regular rule.
12401231
rule <k> rvalueRef(REGION, KIND, place(local(I), PROJS))
1241-
=> #forceSetLocal(
1242-
local(I),
1232+
=> #setLocalValue(
1233+
place(local(I), .ProjectionElems),
12431234
#decodeConstant(
12441235
constantKindZeroSized,
12451236
tyOfLocal(getLocal(LOCALS, I)),

0 commit comments

Comments
 (0)