feat: solve interior-mut3-fail.rs

Author: Stevengre

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

@@ -180,7 +180,8 @@ A variant `#forceSetLocal` is provided for setting the local value without check
        </locals>
     requires 0 <=Int I andBool I <Int size(LOCALS)
      andBool isTypedValue(LOCALS[I])
-     andBool mutabilityOf(getLocal(LOCALS, I)) ==K mutabilityMut
+     andBool (mutabilityOf(getLocal(LOCALS, I)) ==K mutabilityMut
+       orBool #allowsInteriorMutation(lookupTy(tyOfLocal(getLocal(LOCALS, I)))))
     [preserves-definedness] // valid list indexing checked
 
   rule <k> #setLocalValue(place(local(I), .ProjectionElems), VAL) => .K ... </k>

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

@@ -9,6 +9,7 @@ requires "value.md"
 module RT-TYPES
   imports BOOL
   imports INT
+  imports STRING
   imports MAP
   imports K-EQUAL
 
@@ -90,6 +91,14 @@ Pointers to arrays/slices are compatible with pointers to the element type
 
   rule #structOffsets(someLayoutShape(layoutShape(fieldsShapeArbitrary(mk(OFFSETS)), _, _, _, _))) => OFFSETS
   rule #structOffsets(_) => .MachineSizes [owise]
+
+  syntax Bool ::= #allowsInteriorMutation(TypeInfo) [function, total]
+
+  rule #allowsInteriorMutation(typeInfoStructType(mirString(NAME), _, _, _))
+    => findString(NAME, "UnsafeCell", 0) =/=Int -1
+  rule #allowsInteriorMutation(typeInfoStructType(NAME:String, _, _, _))
+    => findString(NAME, "UnsafeCell", 0) =/=Int -1
+  rule #allowsInteriorMutation(_) => false [owise]
 ```
 
 ## Determining types of places with projection

…tion/data/prove-rs/interior-mut3-fail.rs …tegration/data/prove-rs/interior-mut3.rskmir/src/tests/integration/data/prove-rs/interior-mut3-fail.rs renamed to kmir/src/tests/integration/data/prove-rs/interior-mut3.rs kmir/src/tests/integration/data/prove-rs/interior-mut3-fail.rs renamed to kmir/src/tests/integration/data/prove-rs/interior-mut3.rs

@@ -39,7 +39,6 @@
 }
 PROVE_RS_SHOW_SPECS = [
     'interior-mut-fail',
-    'interior-mut3-fail',
     'interior-mut-refcell-fail',
     'assert_eq_exp',
     'bitwise-not-shift',