From e05001b7f2e7a6d6fd880ec9c3ee7edd2d351d5b Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 18 Aug 2025 12:58:14 +1000 Subject: [PATCH 1/4] WIP shorting out Derefs when creating references --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 77 ++++++++++++------- .../crate-tests/two-crate-bin/main.expected | 2 +- .../data/exec-smir/references/weirdRefs.state | 2 +- .../show/interior-mut-fail.main.expected | 6 +- .../show/interior-mut2-fail.main.expected | 2 +- ...-length-test-fail.array_cast_test.expected | 26 ++++++- .../symbolic-args-fail.eats_all_args.expected | 4 +- .../show/symbolic-args-fail.main.expected | 2 +- 8 files changed, 79 insertions(+), 42 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index a3c7a031e..2b7407abf 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/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 #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 ) ... @@ -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 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 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)) ... 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 #mkRef( PLACE , MUT, dynamicSize(_), LOCALS) => #mkDynSizeRef(PLACE, MUT, LOCALS, operandCopy(PLACE)) ... - rule #mkRef(place(LOCAL, PROJS), MUT, META , LOCALS) => Reference(0, place(LOCAL, #resolveProjs(PROJS, LOCALS)), MUT, META) ... [priority(60)] + // once traversal is finished, reconstruct the last projections and the reference offset/local, and possibly read the size + rule #traverseProjection(DEST, VAL:Value, .ProjectionElems, CTXTS) ~> #forRef(MUT, META) + => #mkRef(DEST, #projectionsFor(CTXTS), MUT, #maybeDynamicSize(META, VAL)) + ... + - // with dynamic metadata (reading the value) - rule #mkDynSizeRef(place(LOCAL, PROJS), MUT, LOCALS, VAL:Value) => Reference(0, place(LOCAL, #resolveProjs(PROJS, LOCALS)), MUT, metadataFor(VAL)) ... + syntax Value ::= #mkRef( WriteTo , ProjectionElems , Mutability , Metadata ) [function, total] + // ----------------------------------------------------------------------------------------------- + rule #mkRef( toLocal(I) , PROJS, MUT, META) => Reference( 0 , place(local(I), PROJS), MUT, META) + rule #mkRef(toStack(OFFSET, LOCAL), PROJS, MUT, META) => Reference(OFFSET, place( LOCAL , PROJS), MUT, META) - 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 [owise] + 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 OTHER #resolveProjs(REST, LOCALS) [owise] ``` A `CopyForDeref` `RValue` has the semantics of a simple `Use(operandCopy(...))`, @@ -964,6 +971,18 @@ The operation typically creates a pointer with empty metadata. => PtrLocal(0, place(LOCAL, #resolveProjs(PROJS, LOCALS)), MUT, ptrEmulation(dynamicSize(size(ELEMS)))) ... + + // 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 OTHER #resolveProjs(REST, LOCALS) [owise] ``` In practice, the `AddressOf` can often be found applied to references that get dereferenced first, diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/main.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/main.expected index a8ab0c0a3..361b8cd28 100644 --- a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/main.expected +++ b/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) +│ (728 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ function: main diff --git a/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state b/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state index ea184a39d..baddf93a8 100644 --- a/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state +++ b/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 ) ) diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected index 3079968a1..787390001 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected +++ b/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) +│ (155 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) diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected index 06a165f2b..7c130c0f3 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (166 steps) +│ (176 steps) └─ 3 (stuck, leaf) #traverseProjection ( toLocal ( 2 ) , thunk ( #cast ( PtrLocal ( 0 , place ( ... span: 53 diff --git a/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected index cdb020791..bd731386e 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected @@ -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 + ┃ ┃ │ + ┃ ┃ │ (111 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 ┃ ┗━━┓ │ diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected index 34a843166..e287eec95 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected +++ b/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) +┃ │ (135 steps) ┃ ├─ 6 (split) ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) ) ┃ ┃ @@ -78,7 +78,7 @@ ├─ 5 │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 3 ) ) │ - │ (116 steps) + │ (111 steps) ├─ 7 (split) │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) ) ┃ diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected index 9792462e6..eb10a8adc 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected +++ b/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) +│ (553 steps) └─ 3 (stuck, leaf) #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC function: main From 7830f613f32a1d0085f76ac6436566a963eadf9f Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 18 Aug 2025 13:42:41 +1000 Subject: [PATCH 2/4] shorten out Deref when creating pointers with AddressOf --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 42 ++++++------------- .../show/interior-mut2-fail.main.expected | 4 +- .../show/offset-u8-fail.main.expected | 6 +-- 3 files changed, 18 insertions(+), 34 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 2b7407abf..63f1c842a 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -942,9 +942,12 @@ to casts and pointer arithmetic using `BinOp::Offset`. The operation typically creates a pointer with empty metadata. ```k - rule rvalueAddressOf(MUT, place(local(I), PROJS) #as PLACE) + syntax KItem ::= #forPtr ( Mutability, Metadata ) + + rule 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 ... @@ -954,35 +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 #mkPtr( PLACE , MUT, dynamicSize(_), LOCALS) - => #mkDynLengthPtr(PLACE, MUT, LOCALS, operandCopy(PLACE)) - ... - - - rule #mkPtr(place(LOCAL, PROJS), MUT, META , LOCALS) - => PtrLocal(0, place(LOCAL, #resolveProjs(PROJS, LOCALS)), MUT, ptrEmulation(META)) - ... - [priority(60)] - - rule #mkDynLengthPtr(place(LOCAL, PROJS), MUT, LOCALS, Range(ELEMS)) - => PtrLocal(0, place(LOCAL, #resolveProjs(PROJS, LOCALS)), MUT, ptrEmulation(dynamicSize(size(ELEMS)))) + // once traversal is finished, reconstruct the last projections and the reference offset/local, and possibly read the size + rule #traverseProjection(DEST, VAL:Value, .ProjectionElems, CTXTS) ~> #forPtr(MUT, META) + => #mkPtr(DEST, #projectionsFor(CTXTS), MUT, #maybeDynamicSize(META, VAL)) ... - + - // 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 OTHER #resolveProjs(REST, LOCALS) [owise] + syntax Value ::= #mkPtr ( WriteTo, ProjectionElems, Mutability , Metadata ) [function, total] + // ------------------------------------------------------------------------------------------ + rule #mkPtr( toLocal(I) , PROJS, MUT, META) => PtrLocal( 0 , place(local(I), PROJS), MUT, ptrEmulation(META)) + rule #mkPtr(toStack(OFFSET, LOCAL), PROJS, MUT, META) => PtrLocal(OFFSET, place( LOCAL , PROJS), MUT, ptrEmulation(META)) ``` In practice, the `AddressOf` can often be found applied to references that get dereferenced first, diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected index 7c130c0f3..2f9911855 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected +++ b/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 │ -│ (176 steps) +│ (180 steps) └─ 3 (stuck, leaf) - #traverseProjection ( toLocal ( 2 ) , thunk ( #cast ( PtrLocal ( 0 , place ( ... + #traverseProjection ( toLocal ( 2 ) , thunk ( #cast ( PtrLocal ( 3 , place ( ... span: 53 diff --git a/kmir/src/tests/integration/data/prove-rs/show/offset-u8-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/offset-u8-fail.main.expected index 812709d4e..c827518af 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/offset-u8-fail.main.expected +++ b/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) From 8083bafe486d02302fc6b5a275188a610fca9b55 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 18 Aug 2025 17:34:54 +1000 Subject: [PATCH 3/4] Work around memory issues in simbolic-args-fail proof --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 14 +++++++------- kmir/src/kmir/kmir.py | 2 +- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 63f1c842a..a328e7917 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -910,15 +910,15 @@ This eliminates any `Deref` projections from the place, and also resolves `Index ... - syntax Value ::= #mkRef( WriteTo , ProjectionElems , Mutability , Metadata ) [function, total] + syntax Evaluation ::= #mkRef( WriteTo , ProjectionElems , Mutability , Metadata ) // [function, total] // ----------------------------------------------------------------------------------------------- - rule #mkRef( toLocal(I) , PROJS, MUT, META) => Reference( 0 , place(local(I), PROJS), MUT, META) - rule #mkRef(toStack(OFFSET, LOCAL), PROJS, MUT, META) => Reference(OFFSET, place( LOCAL , PROJS), MUT, META) + rule #mkRef( toLocal(I) , PROJS, MUT, META) => Reference( 0 , place(local(I), PROJS), MUT, META) ... + rule #mkRef(toStack(OFFSET, LOCAL), PROJS, MUT, META) => Reference(OFFSET, place( LOCAL , PROJS), MUT, META) ... syntax Metadata ::= #maybeDynamicSize ( Metadata , Value ) [function, total] // ------------------------------------------------------------------------- rule #maybeDynamicSize(dynamicSize(_), Range(LIST)) => dynamicSize(size(LIST)) - rule #maybeDynamicSize(dynamicSize(_), _OTHER ) => noMetadata [owise] + rule #maybeDynamicSize(dynamicSize(_), _OTHER ) => noMetadata [priority(100)] rule #maybeDynamicSize( OTHER_META , _ ) => OTHER_META [owise] syntax Mutability ::= #mutabilityOf ( BorrowKind ) [function, total] @@ -963,10 +963,10 @@ The operation typically creates a pointer with empty metadata. ... - syntax Value ::= #mkPtr ( WriteTo, ProjectionElems, Mutability , Metadata ) [function, total] + syntax Evaluation ::= #mkPtr ( WriteTo, ProjectionElems, Mutability , Metadata ) // [function, total] // ------------------------------------------------------------------------------------------ - rule #mkPtr( toLocal(I) , PROJS, MUT, META) => PtrLocal( 0 , place(local(I), PROJS), MUT, ptrEmulation(META)) - rule #mkPtr(toStack(OFFSET, LOCAL), PROJS, MUT, META) => PtrLocal(OFFSET, place( LOCAL , PROJS), MUT, ptrEmulation(META)) + rule #mkPtr( toLocal(I) , PROJS, MUT, META) => PtrLocal( 0 , place(local(I), PROJS), MUT, ptrEmulation(META)) ... + rule #mkPtr(toStack(OFFSET, LOCAL), PROJS, MUT, META) => PtrLocal(OFFSET, place( LOCAL , PROJS), MUT, ptrEmulation(META)) ... ``` In practice, the `AddressOf` can often be found applied to references that get dereferenced first, diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index d9ef95de1..c2ce185e3 100644 --- a/kmir/src/kmir/kmir.py +++ b/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()) From 88e861eeb0f6652125e2e550c856caef5f8a9ce6 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 18 Aug 2025 18:50:01 +1000 Subject: [PATCH 4/4] adjust step counts after changing from functions to rewrites --- .../integration/data/crate-tests/single-bin/main.expected | 2 +- .../single-lib/testing::test_add_in_range.expected | 2 +- .../integration/data/crate-tests/two-crate-bin/main.expected | 2 +- .../data/prove-rs/show/assert_eq_exp-fail.main.expected | 2 +- .../show/checked_arithmetic-fail.checked_add_i32.expected | 2 +- .../data/prove-rs/show/interior-mut-fail.main.expected | 2 +- .../data/prove-rs/show/interior-mut2-fail.main.expected | 2 +- .../data/prove-rs/show/interior-mut3-fail.main.expected | 2 +- .../data/prove-rs/show/local-raw-fail.main.expected | 2 +- .../pointer-cast-length-test-fail.array_cast_test.expected | 4 ++-- .../prove-rs/show/symbolic-args-fail.eats_all_args.expected | 4 ++-- .../data/prove-rs/show/symbolic-args-fail.main.expected | 2 +- ...rogram.smir.processor::transfer::process_transfer.expected | 2 +- 13 files changed, 15 insertions(+), 15 deletions(-) diff --git a/kmir/src/tests/integration/data/crate-tests/single-bin/main.expected b/kmir/src/tests/integration/data/crate-tests/single-bin/main.expected index 3c9f4f7eb..2bfb3dc5e 100644 --- a/kmir/src/tests/integration/data/crate-tests/single-bin/main.expected +++ b/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 diff --git a/kmir/src/tests/integration/data/crate-tests/single-lib/testing::test_add_in_range.expected b/kmir/src/tests/integration/data/crate-tests/single-lib/testing::test_add_in_range.expected index 8c70db695..b44976181 100644 --- a/kmir/src/tests/integration/data/crate-tests/single-lib/testing::test_add_in_range.expected +++ b/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 │ diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/main.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/main.expected index 361b8cd28..5134d4e68 100644 --- a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/main.expected +++ b/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 │ -│ (728 steps) +│ (730 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ function: main diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp-fail.main.expected index 46296f9a9..8e77c1486 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp-fail.main.expected +++ b/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 diff --git a/kmir/src/tests/integration/data/prove-rs/show/checked_arithmetic-fail.checked_add_i32.expected b/kmir/src/tests/integration/data/prove-rs/show/checked_arithmetic-fail.checked_add_i32.expected index 79e31b1f1..5ba19c60b 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/checked_arithmetic-fail.checked_add_i32.expected +++ b/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 ┃ │ diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected index 787390001..ad2970223 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (155 steps) +│ (158 steps) └─ 3 (stuck, leaf) #traverseProjection ( toStack ( 3 , local ( 1 ) ) , thunk ( #decodeConstant ( co span: 86 diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected index 2f9911855..6ef3112a7 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected @@ -3,7 +3,7 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (180 steps) +│ (185 steps) └─ 3 (stuck, leaf) #traverseProjection ( toLocal ( 2 ) , thunk ( #cast ( PtrLocal ( 3 , place ( ... span: 53 diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected index e87ac1291..d4b0127e7 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected +++ b/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 diff --git a/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected index 2c483b50d..a99c05167 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected +++ b/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 diff --git a/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected index bd731386e..e8790c95d 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected +++ b/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 @@ -51,7 +51,7 @@ ┃ ┃ │ #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( range ( #mapOffset ( ┃ ┃ │ span: 87 ┃ ┃ │ - ┃ ┃ │ (111 steps) + ┃ ┃ │ (113 steps) ┃ ┃ └─ 13 (stuck, leaf) ┃ ┃ #traverseProjection ( toLocal ( 5 ) , Range ( range ( #mapOffset ( ARG_ARRAY1:Li ┃ ┃ span: 97 diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected index e287eec95..4de9755e0 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.eats_all_args.expected +++ b/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 ) ) ┃ │ -┃ │ (135 steps) +┃ │ (136 steps) ┃ ├─ 6 (split) ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) ) ┃ ┃ @@ -78,7 +78,7 @@ ├─ 5 │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 3 ) ) │ - │ (111 steps) + │ (112 steps) ├─ 7 (split) │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) ) ┃ diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected index eb10a8adc..9e40f97cb 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected +++ b/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 │ -│ (553 steps) +│ (562 steps) └─ 3 (stuck, leaf) #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC function: main diff --git a/kmir/src/tests/integration/data/prove-smir/show/pinocchio_token_program.smir.processor::transfer::process_transfer.expected b/kmir/src/tests/integration/data/prove-smir/show/pinocchio_token_program.smir.processor::transfer::process_transfer.expected index 3cb092f8d..7747d8b71 100644 --- a/kmir/src/tests/integration/data/prove-smir/show/pinocchio_token_program.smir.processor::transfer::process_transfer.expected +++ b/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 ) ) ┃