Refactor evaluation rules to use more specific sorts

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.3.102"
+version = "0.3.103"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.102'
+VERSION: Final = '0.3.103'

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

@@ -308,23 +308,12 @@ these are irrelevant at the MIR level that this semantics is modeling
 will effectively be no-ops at this level).
 
 ```k
-
-  // all memory accesses relegated to another module (to be added)
   rule <k> #execStmt(statement(statementKindAssign(PLACE, RVAL), _SPAN))
          =>
-           RVAL ~> #assign(PLACE)
+          #setLocalValue(PLACE, RVAL) // RVAL evaluation is implemented in rt/data.md
          ...
        </k>
 
-  // RVAL evaluation is implemented in rt/data.md
-
-  syntax KItem ::= #assign ( Place )
-
-  rule <k> VAL:TypedLocal ~> #assign(PLACE) ~> CONT
-        =>
-           VAL ~> #setLocalValue(PLACE) ~> CONT
-        </k>
-
   rule <k> #execStmt(statement(statementKindSetDiscriminant(_PLACE, _VARIDX), _SPAN))
          =>
            .K // FIXME! write variant index to PLACE
@@ -420,13 +409,16 @@ value is the value in local `_0`, and will go to the _destination_ in
 the `LOCALS` of the caller's stack frame. Execution continues with the
 context of the enclosing stack frame, at the _target_.
 
+If the returned value is not initialised ( `NewValue`), the write is skipped.
 If the returned value is a `Reference`, its stack height must be decremented because a stack frame is popped.
 NB that a stack height of `0` cannot occur here, because the compiler prevents local variable references from escaping.
 
 ```k
   rule <k> #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _
          =>
-           #decrementRef(LOCAL0) ~> #setLocalValue(DEST) ~> #execBlockIdx(TARGET) ~> .K
+           #if isLocalValue(LOCAL0) #then #setLocalValue(DEST, #decrementRef({LOCAL0}:>LocalValue)) #else .K #fi
+              ~> #execBlockIdx(TARGET)
+              ~> .K
        </k>
        <currentFunc> _ => CALLER </currentFunc>
        //<currentFrame>
@@ -441,8 +433,7 @@ NB that a stack height of `0` cannot occur here, because the compiler prevents l
        <stack> ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK </stack>
        <functions> FUNCS </functions>
      requires CALLER in_keys(FUNCS)
-      // andBool DEST #within(LOCALS)
-     [preserves-definedness] // CALLER lookup defined, DEST within locals TODO
+     [preserves-definedness] // CALLER lookup defined, DEST within locals checked by write
 
   syntax List ::= #getBlocks(Map, Ty) [function]
                 | #getBlocksAux(MonoItemKind)  [function, total]
@@ -564,35 +555,40 @@ An operand may be a `Reference` (the only way a function could access another fu
            #setArgFromStack(IDX, OP) ~> #setArgsFromStack(IDX +Int 1, MORE) ~> CONT
        </k>
 
-  rule <k> #setArgFromStack(IDX, operandConstant(_) #as CONSTOPERAND)
+  rule <k> #setArgFromStack(IDX, operandConstant(constOperand(_, _, mirConst(KIND, TY, _))))
         =>
-           #readOperand(CONSTOPERAND) ~> #setLocalValue(place(local(IDX), .ProjectionElems))
+           #setLocalValue(
+              place(local(IDX), .ProjectionElems),
+              typedLocal(#decodeConstant(KIND, {TYPEMAP[TY]}:>RigidTy), TY, mutabilityNot)
+            )
         ...
        </k>
+       <basetypes> TYPEMAP </basetypes>
+    requires TY in_keys(TYPEMAP)
+     andBool isRigidTy(TYPEMAP[TY])
+    [preserves-definedness] // valid Map lookup checked
 
   rule <k> #setArgFromStack(IDX, operandCopy(place(local(I), .ProjectionElems)))
         =>
-           #incrementRef({CALLERLOCALS[I]}:>TypedLocal) ~> #setLocalValue(place(local(IDX), .ProjectionElems))
+           #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef({CALLERLOCALS[I]}:>LocalValue))
         ...
        </k>
        <stack> ListItem(StackFrame(_, _, _, _, CALLERLOCALS)) _:List </stack>
     requires 0 <=Int I
      andBool I <Int size(CALLERLOCALS)
-     andBool isTypedLocal(CALLERLOCALS[I])
-     andBool CALLERLOCALS[I] =/=K Moved
+     andBool isLocalValue(CALLERLOCALS[I])
     [preserves-definedness] // valid list indexing checked
 
   rule <k> #setArgFromStack(IDX, operandMove(place(local(I), .ProjectionElems)))
         =>
-           #incrementRef({CALLERLOCALS[I]}:>TypedLocal) ~> #setLocalValue(place(local(IDX), .ProjectionElems))
+           #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef({CALLERLOCALS[I]}:>LocalValue))
         ...
        </k>
        <stack> ListItem(StackFrame(_, _, _, _, CALLERLOCALS => CALLERLOCALS[I <- Moved])) _:List
         </stack>
     requires 0 <=Int I
      andBool I <Int size(CALLERLOCALS)
-     andBool isTypedLocal(CALLERLOCALS[I])
-     andBool CALLERLOCALS[I] =/=K Moved
+     andBool isLocalValue(CALLERLOCALS[I])
     [preserves-definedness] // valid list indexing checked
 ```
 The `Assert` terminator checks that an operand holding a boolean value (which has previously been computed, e.g., an overflow flag for arithmetic operations) has the expected value (e.g., that this overflow flag is `false` - a very common case).

kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md

@@ -26,11 +26,11 @@ The lists used in the semantics are cons-lists, so only rules with a head elemen
 ```k
   rule N <Int size(_LIST:List) => true
     requires N <Int 0
-    [simplification, symbolic(_LIST)]
+    [simplification]
 
   rule N <Int size(ListItem(_) REST:List) => N -Int 1 <Int size(REST)
-    requires 0 <Int N
-    [simplification, symbolic(REST)]
+    requires 0 <=Int N
+    [simplification]
 ```
 
 ## Simplifications related to the `truncate` function