Hotfix avoid deref in refs

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

@@ -299,18 +299,18 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
                    | toStack ( Int , Local )
 
   // retains information about the value that was deconstructed by a projection
-  syntax Context ::= CtxField( VariantIdx, List, Int )
+  syntax Context ::= CtxField( VariantIdx, List, Int , Ty )
                    | CtxIndex( List , Int ) // array index constant or has been read before
                    | CtxSubslice( List , Int , Int ) // start and end always counted from beginning
 
   syntax Contexts ::= List{Context, ""}
 
   syntax Value ::= #buildUpdate ( Value , Contexts ) [function]
-
+  // ----------------------------------------------------------
   rule #buildUpdate(VAL, .Contexts) => VAL
      [preserves-definedness]
 
-  rule #buildUpdate(VAL, CtxField(IDX, ARGS, I) CTXS)
+  rule #buildUpdate(VAL, CtxField(IDX, ARGS, I, _) CTXS)
       => #buildUpdate(Aggregate(IDX, ARGS[I <- VAL]), CTXS)
      [preserves-definedness] // valid list indexing checked upon context construction
 
@@ -387,14 +387,14 @@ This is done without consideration of the validity of the Downcast[^downcast].
   rule <k> #traverseProjection(
              DEST,
              Aggregate(IDX, ARGS),
-             projectionElemField(fieldIdx(I), _) PROJS,
+             projectionElemField(fieldIdx(I), TY) PROJS,
              CTXTS
            )
         => #traverseProjection(
              DEST,
              getValue(ARGS, I),
              PROJS,
-             CtxField(IDX, ARGS, I) CTXTS
+             CtxField(IDX, ARGS, I, TY) CTXTS
            )
         ...
         </k>
@@ -877,9 +877,23 @@ For slices (represented as `Value::Range`), the metadata is the length (as a dyn
 For `struct`s (represented as `Value::Aggregate`), the metadata is that of the _last_ field (for dynamically-sized data).
 Other `Value`s are not expected to have pointer `Metadata` as per their types.
 
+As references are sometimes created by dereferencing other references or pointers, the referenced value is first evaluated (using `#traverseProjection`).
+This eliminates any `Deref` projections from the place, and also resolves `Index` projections to `ConstantIndex` ones.
+
 ```k
-  rule <k> rvalueRef(_REGION, KIND, place(local(I), PROJS) #as PLACE)
-        => #mkRef(PLACE, #mutabilityOf(KIND), #metadata(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS, TYPEMAP), LOCALS)
+  // reconstructs projections stored as context (used for Rvalues Ref and AddressOf )
+  syntax ProjectionElems ::= #projectionsFor( Contexts )                   [function, total]
+                           | #projectionsFor( Contexts , ProjectionElems ) [function, total]
+  // ----------------------------------------------------------------------------------------
+  rule #projectionsFor(CTXS) => #projectionsFor(CTXS, .ProjectionElems)
+  rule #projectionsFor(       .Contexts          , PROJS) => PROJS
+  rule #projectionsFor(CtxField(_, _, I, TY) CTXS, PROJS) => #projectionsFor(CTXS,     projectionElemField(fieldIdx(I), TY) PROJS)
+  rule #projectionsFor(       CtxIndex(_, I) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemConstantIndex(I, 0, false) PROJS)
+  rule #projectionsFor( CtxSubslice(_, I, J) CTXS, PROJS) => #projectionsFor(CTXS,      projectionElemSubslice(I, J, false) PROJS)
+
+  rule <k> rvalueRef(_REGION, KIND, place(local(I), PROJS))
+        => #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJS, .Contexts)
+        ~> #forRef(#mutabilityOf(KIND), #metadata(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS, TYPEMAP))
        ...
        </k>
        <locals> LOCALS </locals>
@@ -888,37 +902,30 @@ Other `Value`s are not expected to have pointer `Metadata` as per their types.
      andBool isTypedValue(LOCALS[I])
     [preserves-definedness] // valid list indexing checked, #metadata should only use static information
 
-  syntax Evaluation ::= #mkRef ( Place , Mutability, Metadata, List)
-                      | #mkDynSizeRef ( Place , Mutability , List , Evaluation ) [strict(4)]
+  syntax KItem ::= #forRef( Mutability , Metadata )
 
-  rule <k> #mkRef(      PLACE        , MUT, dynamicSize(_), LOCALS) => #mkDynSizeRef(PLACE, MUT, LOCALS, operandCopy(PLACE))               ... </k>
-  rule <k> #mkRef(place(LOCAL, PROJS), MUT,    META       , LOCALS) => Reference(0, place(LOCAL, #resolveProjs(PROJS, LOCALS)), MUT, META) ... </k> [priority(60)]
+  // once traversal is finished, reconstruct the last projections and the reference offset/local, and possibly read the size
+  rule <k> #traverseProjection(DEST, VAL:Value, .ProjectionElems, CTXTS) ~> #forRef(MUT, META)
+        => #mkRef(DEST, #projectionsFor(CTXTS), MUT, #maybeDynamicSize(META, VAL))
+        ...
+      </k>
 
-  // with dynamic metadata (reading the value)
-  rule <k> #mkDynSizeRef(place(LOCAL, PROJS), MUT, LOCALS, VAL:Value) => Reference(0, place(LOCAL, #resolveProjs(PROJS, LOCALS)), MUT, metadataFor(VAL)) ... </k>
+  syntax Evaluation ::= #mkRef( WriteTo , ProjectionElems , Mutability , Metadata ) // [function, total]
+  // -----------------------------------------------------------------------------------------------
+  rule <k> #mkRef(       toLocal(I)     , PROJS, MUT, META) => Reference(   0  , place(local(I), PROJS), MUT, META) ... </k>
+  rule <k> #mkRef(toStack(OFFSET, LOCAL), PROJS, MUT, META) => Reference(OFFSET, place(  LOCAL , PROJS), MUT, META) ... </k>
 
-  syntax Metadata ::= metadataFor ( Value ) [function, total]
-  // --------------------------------------------------------
-  rule metadataFor(    Range(LIST)   ) => dynamicSize(size(LIST))
-  rule metadataFor(      _OTHER     ) => noMetadata      [owise]
+  syntax Metadata ::= #maybeDynamicSize ( Metadata , Value ) [function, total]
+  // -------------------------------------------------------------------------
+  rule #maybeDynamicSize(dynamicSize(_), Range(LIST)) => dynamicSize(size(LIST))
+  rule #maybeDynamicSize(dynamicSize(_),   _OTHER   ) => noMetadata              [priority(100)]
+  rule #maybeDynamicSize(   OTHER_META ,     _      ) => OTHER_META              [owise]
 
   syntax Mutability ::= #mutabilityOf ( BorrowKind ) [function, total]
   // -----------------------------------------------------------------
   rule #mutabilityOf(borrowKindShared)  => mutabilityNot
   rule #mutabilityOf(borrowKindFake(_)) => mutabilityNot // Shallow fake borrow disallowed in late stages
   rule #mutabilityOf(borrowKindMut(_))  => mutabilityMut // all mutable kinds behave equally for us
-
-  // turns Index(LOCAL) projections into ConstantIndex(Int)
-  syntax ProjectionElems ::= #resolveProjs ( ProjectionElems , List ) [function, total]
-  // ----------------------------------------------------------------------------------
-  rule #resolveProjs(        .ProjectionElems           , _LOCALS) => .ProjectionElems
-  rule #resolveProjs( projectionElemIndex(local(I)) REST, LOCALS ) => projectionElemConstantIndex(#expectUsize(getValue(LOCALS,I)), 0, false) #resolveProjs(REST, LOCALS)
-    requires 0 <=Int I
-     andBool I <Int size(LOCALS)
-     andBool isTypedValue(LOCALS[I])
-     andBool isInt(#expectUsize(getValue(LOCALS,I)))
-    [preserves-definedness]
-  rule #resolveProjs(     OTHER:ProjectionElem      REST, LOCALS ) => OTHER #resolveProjs(REST, LOCALS) [owise]
 ```
 
 A `CopyForDeref` `RValue` has the semantics of a simple `Use(operandCopy(...))`,
@@ -935,9 +942,12 @@ to casts and pointer arithmetic using `BinOp::Offset`.
 The operation typically creates a pointer with empty metadata.
 
 ```k
-  rule <k> rvalueAddressOf(MUT, place(local(I), PROJS) #as PLACE)
+  syntax KItem ::= #forPtr ( Mutability, Metadata )
+
+  rule <k> rvalueAddressOf(MUT, place(local(I), PROJS))
          =>
-           #mkPtr(PLACE, MUT, #metadata(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS, TYPEMAP), LOCALS)
+           #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJS, .Contexts)
+          ~> #forPtr(MUT, #metadata(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS, TYPEMAP))
            // we should use #alignOf to emulate the address
        ...
        </k>
@@ -947,23 +957,16 @@ The operation typically creates a pointer with empty metadata.
      andBool isTypedValue(LOCALS[I])
     [preserves-definedness] // valid list indexing checked, #metadata should only use static information
 
-  syntax Evaluation ::= #mkPtr ( Place , Mutability , Metadata , List )
-                      | #mkDynLengthPtr ( Place , Mutability , List , Evaluation ) [strict(4)]
-
-  rule <k> #mkPtr(      PLACE        , MUT, dynamicSize(_), LOCALS)
-        => #mkDynLengthPtr(PLACE, MUT, LOCALS, operandCopy(PLACE))
+  // once traversal is finished, reconstruct the last projections and the reference offset/local, and possibly read the size
+  rule <k> #traverseProjection(DEST, VAL:Value, .ProjectionElems, CTXTS) ~> #forPtr(MUT, META)
+        => #mkPtr(DEST, #projectionsFor(CTXTS), MUT, #maybeDynamicSize(META, VAL))
         ...
-       </k>
+      </k>
 
-  rule <k> #mkPtr(place(LOCAL, PROJS), MUT,    META       , LOCALS)
-        => PtrLocal(0, place(LOCAL, #resolveProjs(PROJS, LOCALS)), MUT, ptrEmulation(META))
-        ...
-       </k> [priority(60)]
-
-  rule <k> #mkDynLengthPtr(place(LOCAL, PROJS), MUT, LOCALS, Range(ELEMS))
-        => PtrLocal(0, place(LOCAL, #resolveProjs(PROJS, LOCALS)), MUT, ptrEmulation(dynamicSize(size(ELEMS))))
-        ...
-       </k>
+  syntax Evaluation ::= #mkPtr ( WriteTo, ProjectionElems, Mutability , Metadata ) // [function, total]
+  // ------------------------------------------------------------------------------------------
+  rule <k> #mkPtr(         toLocal(I)   , PROJS, MUT, META) => PtrLocal(    0 , place(local(I), PROJS), MUT, ptrEmulation(META)) ... </k>
+  rule <k> #mkPtr(toStack(OFFSET, LOCAL), PROJS, MUT, META) => PtrLocal(OFFSET, place(  LOCAL , PROJS), MUT, ptrEmulation(META)) ... </k>
 ```
 
 In practice, the `AddressOf` can often be found applied to references that get dereferenced first,

kmir/src/kmir/kmir.py

@@ -64,7 +64,7 @@ def kcfg_explore(self, label: str | None = None) -> Iterator[KCFGExplore]:
             llvm_definition_dir=self.llvm_library_dir,
             bug_report=self.bug_report,
             id=label if self.bug_report is not None else None,  # NB bug report arg.s must be coherent
-            interim_simplification=200,  # working around memory problems in LLVM backend calls
+            interim_simplification=50,  # working around memory problems in LLVM backend calls
         ) as cts:
             yield KCFGExplore(cts, kcfg_semantics=KMIRSemantics())
 

kmir/src/tests/integration/data/crate-tests/single-bin/main.expected

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (223 steps)
+│  (225 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │   function: main

kmir/src/tests/integration/data/crate-tests/single-lib/testing::test_add_in_range.expected

@@ -25,7 +25,7 @@
    ├─ 5
    │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
    │
-   │  (179 steps)
+   │  (181 steps)
    ├─ 7 (terminal)
    │   #EndProgram ~> .K
    │

kmir/src/tests/integration/data/crate-tests/two-crate-bin/main.expected

@@ -2,7 +2,7 @@
 ┌─ 1 (root, init)
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │
-│  (727 steps)
+│  (730 steps)
 ├─ 3 (terminal)
 │   #EndProgram ~> .K
 │   function: main

kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state

@@ -51,7 +51,7 @@
       ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 9 ) , projection: .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 35 ) , mutabilityNot ) )
       ListItem ( typedValue ( Integer ( 43 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 32 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 23 ) , projection: projectionElemDeref  projectionElemField ( fieldIdx ( 2 ) , ty ( 26 ) )  .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 36 ) , mutabilityNot ) )
+      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 2 ) , ty ( 26 ) )  .ProjectionElems ) , mutabilityMut , noMetadata ) , ty ( 36 ) , mutabilityNot ) )
       ListItem ( typedValue ( Moved , ty ( 2 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 25 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 32 ) , mutabilityMut ) )

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

@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (98 steps)
+│  (99 steps)
 └─ 3 (stuck, leaf)
     #traverseProjection ( toLocal ( 6 ) , thunk ( #decodeConstant ( constantKindAllo
     function: main

kmir/src/tests/integration/data/prove-rs/show/checked_arithmetic-fail.checked_add_i32.expected

@@ -15,7 +15,7 @@
 ┃  ├─ 4
 ┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 4 ) )
 ┃  │
-┃  │  (249 steps)
+┃  │  (250 steps)
 ┃  ├─ 6 (terminal)
 ┃  │   #EndProgram ~> .K
 ┃  │

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

@@ -3,10 +3,10 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (176 steps)
+│  (158 steps)
 └─ 3 (stuck, leaf)
-    #traverseProjection ( toLocal ( 11 ) , thunk ( #cast ( PtrLocal ( 0 , place ( ..
-    span: 91
+    #traverseProjection ( toStack ( 3 , local ( 1 ) ) , thunk ( #decodeConstant ( co
+    span: 86
 
 
 ┌─ 2 (root, leaf, target, terminal)

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

@@ -3,9 +3,9 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (166 steps)
+│  (185 steps)
 └─ 3 (stuck, leaf)
-    #traverseProjection ( toLocal ( 2 ) , thunk ( #cast ( PtrLocal ( 0 , place ( ...
+    #traverseProjection ( toLocal ( 2 ) , thunk ( #cast ( PtrLocal ( 3 , place ( ...
     span: 53
 
 

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

@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (150 steps)
+│  (151 steps)
 ├─ 3
 │   #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
 │   function: main

kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected

@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (104 steps)
+│  (105 steps)
 ├─ 3
 │   #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
 │   function: main

kmir/src/tests/integration/data/prove-rs/show/offset-u8-fail.main.expected

@@ -3,10 +3,10 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (74 steps)
+│  (31 steps)
 └─ 3 (stuck, leaf)
-    #traverseProjection ( toLocal ( 5 ) , thunk ( #applyBinOp ( binOpOffset , thunk
-    span: 70
+    #traverseProjection ( toLocal ( 1 ) , thunk ( #decodeConstant ( constantKindAllo
+    span: 48
 
 
 ┌─ 2 (root, leaf, target, terminal)

kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected

@@ -27,7 +27,7 @@
    ├─ 5
    │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) )
    │
-   │  (208 steps)
+   │  (209 steps)
    ├─ 7
    │   #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( range ( #mapOffset (
    │   span: 87
@@ -39,10 +39,28 @@
    ┃  │   #traverseProjection ( toStack ( 1 , local ( 2 ) ) , project:Value ( range ( #map
    ┃  │   span: 87
    ┃  │
-   ┃  │  (116 steps)
-   ┃  └─ 10 (stuck, leaf)
-   ┃      #traverseProjection ( toLocal ( 5 ) , Range ( range ( #mapOffset ( ARG_ARRAY1:Li
-   ┃      span: 97
+   ┃  │  (6 steps)
+   ┃  ├─ 10
+   ┃  │   #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( #mapOffset ( range (
+   ┃  │   span: 87
+   ┃  ┃
+   ┃  ┃ (1 step)
+   ┃  ┣━━┓
+   ┃  ┃  │
+   ┃  ┃  ├─ 11
+   ┃  ┃  │   #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( range ( #mapOffset (
+   ┃  ┃  │   span: 87
+   ┃  ┃  │
+   ┃  ┃  │  (113 steps)
+   ┃  ┃  └─ 13 (stuck, leaf)
+   ┃  ┃      #traverseProjection ( toLocal ( 5 ) , Range ( range ( #mapOffset ( ARG_ARRAY1:Li
+   ┃  ┃      span: 97
+   ┃  ┃
+   ┃  ┗━━┓
+   ┃     │
+   ┃     └─ 12 (stuck, leaf)
+   ┃         #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( #mapOffset ( range (
+   ┃         span: 87
    ┃
    ┗━━┓
       │

kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected

@@ -15,7 +15,7 @@
 ┃  ├─ 4
 ┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 3 ) )
 ┃  │
-┃  │  (140 steps)
+┃  │  (136 steps)
 ┃  ├─ 6 (split)
 ┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) )
 ┃  ┃
@@ -78,7 +78,7 @@
    ├─ 5
    │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 3 ) )
    │
-   │  (116 steps)
+   │  (112 steps)
    ├─ 7 (split)
    │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) )
    ┃

kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected

@@ -3,7 +3,7 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (558 steps)
+│  (562 steps)
 └─ 3 (stuck, leaf)
     #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
     function: main

kmir/src/tests/integration/data/prove-smir/show/pinocchio_token_program.smir.processor::transfer::process_transfer.expected

@@ -31,7 +31,7 @@
    ├─ 5
    │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) )
    │
-   │  (417 steps)
+   │  (418 steps)
    ├─ 7 (split)
    │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 6 ) )
    ┃