Merge branch 'master' into jh/fix-thunk-projection

Author: Stevengre

Makefile

@@ -21,6 +21,7 @@ test: test-unit test-integration smir-parse-tests
 stable-mir-json: CARGO_BUILD_OPTS =
 stable-mir-json:
 	cd deps/stable-mir-json && cargo build ${CARGO_BUILD_OPTS}
+	cd deps/stable-mir-json && cargo build --release ${CARGO_BUILD_OPTS}
 	cd deps/stable-mir-json && cargo run --bin cargo_stable_mir_json -- ${TOP_DIR}/deps/stable-mir-json ${TOP_DIR}/deps
 	${TOP_DIR}/deps/.stable-mir-json/release.sh --version || ${TOP_DIR}/deps/.stable-mir-json/debug.sh --version
 

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

@@ -177,21 +177,23 @@ In contrast to regular write operations, the value does not have to be _mutable_
 ### Setting Local Variables
 
 The `#setLocalValue` operation writes a `Value` value to a given `Place` within the `List` of local variables currently on top of the stack.
-This may fail because a local may not be accessible or not mutable.
 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.
 A variant `#forceSetLocal` is provided for setting the local value without checking the mutability of the location.
 
+**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.
+
+TODO: `#forceSetLocal` is now functionally identical to `#setLocalValue` and may be removed.
+
 ```k
   syntax KItem ::= #setLocalValue( Place, Evaluation ) [strict(2)]
                  | #forceSetLocal ( Local , Evaluation ) [strict(2)]
 
   rule <k> #setLocalValue(place(local(I), .ProjectionElems), VAL) => .K ... </k>
        <locals>
-          LOCALS => LOCALS[I <- typedValue(VAL, tyOfLocal(getLocal(LOCALS, I)), mutabilityMut)]
+          LOCALS => LOCALS[I <- typedValue(VAL, tyOfLocal(getLocal(LOCALS, I)), mutabilityOf(getLocal(LOCALS, I)))]
        </locals>
     requires 0 <=Int I andBool I <Int size(LOCALS)
      andBool isTypedValue(LOCALS[I])
-     andBool mutabilityOf(getLocal(LOCALS, I)) ==K mutabilityMut
     [preserves-definedness] // valid list indexing checked
 
   rule <k> #setLocalValue(place(local(I), .ProjectionElems), VAL) => .K ... </k>

kmir/src/tests/integration/data/prove-rs/immutable-local-reassign.rs

@@ -0,0 +1,11 @@
+fn main() {
+    let _ = repro();
+}
+
+fn repro() -> usize {
+    let mut out = [0usize; 2];
+    for i in 0usize..2usize {
+        out[i] = i;
+    }
+    out[1]
+}

kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected

@@ -49,14 +49,15 @@
       │   #execBlockIdx ( basicBlockIdx ( 7 ) ) ~> .K
       │   function: main
       │
-      │  (17 steps)
-      └─ 11 (stuck, leaf)
-          #setLocalValue ( place ( ... local: local ( 1 ) , projection: .ProjectionElems )
-          function: main
-          span: 79
-
+      │  (66 steps)
+      ├─ 11 (terminal)
+      │   #EndProgram ~> .K
+      │   function: main
+      │
+      ┊  constraint: true
+      ┊  subst: ...
+      └─ 2 (leaf, target, terminal)
+          #EndProgram ~> .K
 
-┌─ 2 (root, leaf, target, terminal)
-│   #EndProgram ~> .K