Code to write to array indexes (#552)

This completes the array support for kmir.

Closes #487

---------

Co-authored-by: devops <devops@runtimeverification.com>

Author: jberthold

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kmir"
-version = "0.3.137"
+version = "0.3.138"
 description = ""
 requires-python = "~=3.10"
 dependencies = [

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.137'
+VERSION: Final = '0.3.138'

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

@@ -427,7 +427,7 @@ The solution is to use rewrite operations in a downward pass through the project
 
   // retains information about the value that was deconstructed by a projection
   syntax Context ::= CtxField( Ty, VariantIdx, List, Int )
-                // | array context will be added here
+                   | CtxIndex( Ty, List , Int ) // array index constant or has been read before
 
   syntax Contexts ::= List{Context, ""}
 
@@ -440,6 +440,10 @@ The solution is to use rewrite operations in a downward pass through the project
       => #buildUpdate(typedValue(Aggregate(IDX, ARGS[I <- VAL]), TY, mutabilityMut), 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)
+     [preserves-definedness] // valid list indexing checked upon context construction
+
   rule <k> #projectedUpdate(
               DEST,
               typedValue(Aggregate(IDX, ARGS), TY, MUT),
@@ -457,6 +461,84 @@ The solution is to use rewrite operations in a downward pass through the project
      andBool (FORCE orBool MUT ==K mutabilityMut)
      [preserves-definedness] // valid list indexing checked
 
+  rule <k> #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)
+        ...
+        </k>
+        <locals> LOCALS </locals>
+    requires 0 <=Int LOCAL
+     andBool LOCAL <Int size(LOCALS)
+     andBool isTypedValue(LOCALS[LOCAL])
+     andBool isInt(#expectUsize({LOCALS[LOCAL]}:>TypedValue))
+     andBool 0 <=Int #expectUsize({LOCALS[LOCAL]}:>TypedValue)
+     andBool #expectUsize({LOCALS[LOCAL]}:>TypedValue) <Int size(ELEMENTS)
+     andBool isTypedValue(ELEMENTS[#expectUsize({LOCALS[LOCAL]}:>TypedValue)])
+     andBool (FORCE orBool MUT ==K mutabilityMut)
+    [preserves-definedness] // index checked, valid Int can be read, ELEMENT indexable and writeable or forced
+
+  rule <k> #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)
+        ...
+        </k>
+    requires 0 <=Int OFFSET
+     andBool OFFSET <Int size(ELEMENTS)
+     andBool isTypedValue(ELEMENTS[OFFSET])
+     andBool (FORCE orBool MUT ==K mutabilityMut)
+    [preserves-definedness] // ELEMENT indexable and writeable or forced
+
+  rule <k> #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)
+        ...
+        </k>
+    requires 0 <Int OFFSET
+     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 <k> #projectedUpdate(
             _DEST,
             typedValue(Reference(OFFSET, place(LOCAL, PLACEPROJ), MUT), _, _),

kmir/src/tests/integration/data/exec-smir/arrays/array_write.rs

@@ -0,0 +1,12 @@
+fn main() {
+
+    let mut a: [i16; 4] = [1;4];
+
+    a[0] = 2;
+
+    let b = &mut (a[1]);
+
+    *b = 2;
+
+    assert!(a[0] == a[1]);
+}