Skip to content

Remove alloc decoding from the K definition #729

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 14 commits into from
Oct 9, 2025
Merged

Remove alloc decoding from the K definition #729

merged 14 commits into from
Oct 9, 2025

Conversation

tothtamas28
Copy link
Contributor

No description provided.

@tothtamas28 tothtamas28 self-assigned this Oct 8, 2025
@tothtamas28
Copy link
Contributor Author

The following tests are failing:

FAILED kmir/src/tests/integration/test_integration.py::test_exec_smir[Alloc-enum-two-refs-fail-llvm] - KeyError: 0
FAILED kmir/src/tests/integration/test_integration.py::test_exec_smir[Alloc-enum-two-refs-fail-haskell] - KeyError: 0
FAILED kmir/src/tests/integration/test_integration.py::test_prove_rs[enum-two-refs-fail] - KeyError: 0

The root cause is, type 0 is referred to but is missing from the types map in enum-two-refs-fail.smir.json.

@dkcumming, @jberthold, how was this test file generated?

Is is also possible the linker has / at some point had a bug (i.e. a type reference is missed somewhere in the JSON tree).

@jberthold
Copy link
Member

The following tests are failing:

FAILED kmir/src/tests/integration/test_integration.py::test_exec_smir[Alloc-enum-two-refs-fail-llvm] - KeyError: 0
FAILED kmir/src/tests/integration/test_integration.py::test_exec_smir[Alloc-enum-two-refs-fail-haskell] - KeyError: 0
FAILED kmir/src/tests/integration/test_integration.py::test_prove_rs[enum-two-refs-fail] - KeyError: 0

The root cause is, type 0 is referred to but is missing from the types map in enum-two-refs-fail.smir.json.

@dkcumming, @jberthold, how was this test file generated?

Is is also possible the linker has / at some point had a bug (i.e. a type reference is missed somewhere in the JSON tree).

Interesting...
The SMIR files are checked in together with the *.rs files for these tests, and there is a make target to update them when stable-mir-json changes. We could just update the SMIR JSON and re-test...
However, there is obviously a problem with ty(0) that should be investigated. I'll read through the related code.
The linker is not involved in these single-crate tests so that's not the reason, but it would be good to check the linker code about ty(0), too.

jberthold
jberthold reviewed Oct 8, 2025
View reviewed changes
kmir/src/kmir/kdist/mir-semantics/rt/decoding.md
Comment on lines -356 to -378
```k
syntax Map ::= #decodeAllocs ( GlobalAllocs , Map ) [function, total, symbol("decodeAllocs") ] // AllocId |-> Thing
| #decodeAllocsAux ( Map , GlobalAllocs , Map ) [function, total, symbol("decodeAllocsAux")] // accumulating version
// -----------------------------------------------------------------------------------------------
rule #decodeAllocs(ALLOCS, TYPEMAP) => #decodeAllocsAux(.Map, ALLOCS, TYPEMAP)
rule #decodeAllocsAux(ACCUM, .GlobalAllocs, _TYPEMAP) => ACCUM
rule #decodeAllocsAux(ACCUM, globalAllocEntry(ID, TY, Memory(ALLOC)) ALLOCS, TYPEMAP)
=> #decodeAllocsAux(ACCUM #decodeAlloc(ID, TY, ALLOC, TYPEMAP), ALLOCS, TYPEMAP)
requires TY in_keys(TYPEMAP)
[preserves-definedness]
```

If the type of an alloc cannot be found, or for non-`Memory` allocs, the raw data is stored in a super-sort of `Value`.
This ensures that the function is total (anyway lookups require constraining the sort).

```k
syntax AllocData ::= Value | AllocData ( Ty , GlobalAllocKind )
rule #decodeAllocsAux(ACCUM, globalAllocEntry(ID, TY, OTHER) ALLOCS, TYPEMAP)
=> #decodeAllocsAux(ACCUM ID |-> AllocData(TY, OTHER), ALLOCS, TYPEMAP)
[owise]
```
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The rule here at the bottom previously took care of the case where the type ID is not found in the type map, producing AllocData nodes in the expected output:
https://github.com/runtimeverification/mir-semantics/blob/master/kmir/src/tests/integration/data/exec-smir/allocs/enum-two-refs-fail.state#L87-L90

@jberthold
Copy link
Member

About the question of why we are getting the ty(0), I believe this is a hack or a bug in stable-mir-json.
The file enum-two-refs-fail.smir.json features ty(0) as the (data) type of the four mentioned allocations, but also uses 0 as the ID for function lang_start_internal.

Inspecting the data, I can see that allocs 10-13 are referenced from other allocs (1 references 10 and 11, 2 references 12 and 13), and 1 and 2 are of type Thing<'_> , so 10 and 12 should actually just be i16, 11 and 13 should be u16, but they aren't for some reason.

@jberthold jberthold mentioned this pull request Oct 8, 2025
Open
jberthold
jberthold reviewed Oct 8, 2025
View reviewed changes
@tothtamas28 tothtamas28 marked this pull request as ready for review October 9, 2025 09:33
@tothtamas28 tothtamas28 requested a review from jberthold October 9, 2025 09:33
jberthold
jberthold approved these changes Oct 9, 2025
View reviewed changes
Copy link
Member

@jberthold jberthold left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice! All tests green so let's merge it.

@automergerpr-permission-manager automergerpr-permission-manager bot merged commit 8fba85a into master Oct 9, 2025
7 checks passed
@automergerpr-permission-manager automergerpr-permission-manager bot deleted the remove-k-decoding branch October 9, 2025 10:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jberthold jberthold jberthold approved these changes

Assignees

@tothtamas28 tothtamas28

Labels

automerge

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@tothtamas28 @jberthold