diff --git a/deps/stable-mir-json b/deps/stable-mir-json index 9a7810914..047ca6ac0 160000 --- a/deps/stable-mir-json +++ b/deps/stable-mir-json @@ -1 +1 @@ -Subproject commit 9a7810914a338dfc2533b04bdb14b19c1943fdb8 +Subproject commit 047ca6ac01786e1b616e13a216d70268b9785e17 diff --git a/deps/stable-mir-json_release b/deps/stable-mir-json_release index 52b29c8d2..b3e6006b7 100644 --- a/deps/stable-mir-json_release +++ b/deps/stable-mir-json_release @@ -1 +1 @@ -9a7810914a338dfc2533b04bdb14b19c1943fdb8 +047ca6ac01786e1b616e13a216d70268b9785e17 diff --git a/flake.lock b/flake.lock index 15bd0b3a7..48334eacc 100644 --- a/flake.lock +++ b/flake.lock @@ -213,11 +213,11 @@ }, "nixpkgs-unstable_2": { "locked": { - "lastModified": 1771369470, - "narHash": "sha256-0NBlEBKkN3lufyvFegY4TYv5mCNHbi5OmBDrzihbBMQ=", + "lastModified": 1772433332, + "narHash": "sha256-izhTDFKsg6KeVBxJS9EblGeQ8y+O8eCa6RcW874vxEc=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "0182a361324364ae3f436a63005877674cf45efb", + "rev": "cf59864ef8aa2e178cccedbe2c178185b0365705", "type": "github" }, "original": { @@ -556,17 +556,17 @@ "rv-nix-tools": "rv-nix-tools_4" }, "locked": { - "lastModified": 1771566009, - "narHash": "sha256-qQGfpcHC12ltraBMnvlwSuY0bEgsMMPdNEjaLW9W8yQ=", + "lastModified": 1772509622, + "narHash": "sha256-4xrcFDb+Vy310S9Sli/7/BiCsf0Jfdp/qqEBLHjCOzE=", "owner": "runtimeverification", "repo": "stable-mir-json", - "rev": "9a7810914a338dfc2533b04bdb14b19c1943fdb8", + "rev": "047ca6ac01786e1b616e13a216d70268b9785e17", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "stable-mir-json", - "rev": "9a7810914a338dfc2533b04bdb14b19c1943fdb8", + "rev": "047ca6ac01786e1b616e13a216d70268b9785e17", "type": "github" } }, diff --git a/flake.nix b/flake.nix index 93a32ea74..dd0ff52ec 100644 --- a/flake.nix +++ b/flake.nix @@ -6,7 +6,7 @@ flake-utils.url = "github:numtide/flake-utils"; - stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/9a7810914a338dfc2533b04bdb14b19c1943fdb8"; + stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/047ca6ac01786e1b616e13a216d70268b9785e17"; stable-mir-json-flake = { inputs.nixpkgs.follows = "nixpkgs"; inputs.flake-utils.follows = "flake-utils"; diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 027a05fd8..966d0c2a4 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -2,4 +2,4 @@ from typing import Final __version__: Final = version('kmir') -__smir_version__: Final = '9a7810914a338dfc2533b04bdb14b19c1943fdb8' +__smir_version__: Final = '047ca6ac01786e1b616e13a216d70268b9785e17' diff --git a/kmir/src/kmir/kdist/mir-semantics/ty.md b/kmir/src/kmir/kdist/mir-semantics/ty.md index e66d98bf8..a5efd60ac 100644 --- a/kmir/src/kmir/kdist/mir-semantics/ty.md +++ b/kmir/src/kmir/kdist/mir-semantics/ty.md @@ -280,6 +280,8 @@ syntax ExistentialPredicateBinders ::= List {ExistentialPredicateBinder, ""} | typeInfoRefType(Ty) [symbol(TypeInfo::RefType) , group(mir-enum---pointee-type)] | typeInfoTupleType(types: Tys, layout: MaybeLayoutShape) [symbol(TypeInfo::TupleType) , group(mir-enum---types--layout)] + | TypeInfoDynType(name: MIRString, layout: MaybeLayoutShape) + [symbol(TypeInfo::DynType) , group(mir-enum---name--layout)] | typeInfoFunType(MIRString) [symbol(TypeInfo::FunType) , group(mir-enum)] | "typeInfoVoidType" [symbol(TypeInfo::VoidType) , group(mir-enum)] diff --git a/kmir/src/kmir/ty.py b/kmir/src/kmir/ty.py index 3851ce157..d899d0d36 100644 --- a/kmir/src/kmir/ty.py +++ b/kmir/src/kmir/ty.py @@ -675,6 +675,28 @@ def nbytes(self, types: Mapping[Ty, TypeMetadata]) -> int: return size.in_bytes +@dataclass +class DynT(TypeMetadata): + name: str + layout: LayoutShape | None + + @staticmethod + def from_raw(data: Any) -> DynT: + match data: + case { + 'DynType': { + 'name': name, + 'layout': layout, + } + }: + return DynT( + name=name, + layout=LayoutShape.from_raw(layout) if layout is not None else None, + ) + case _: + raise _cannot_parse_as('DynT', data) + + @dataclass class FunT(TypeMetadata): type_str: str diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected index 9dbc45230..60dbf8403 100644 --- a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected +++ b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected @@ -2,7 +2,7 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ -│ (736 steps) +│ (740 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ diff --git a/kmir/src/tests/integration/data/prove-rs/and_then_closure.rs b/kmir/src/tests/integration/data/prove-rs/and_then_closure-fail.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/and_then_closure.rs rename to kmir/src/tests/integration/data/prove-rs/and_then_closure-fail.rs diff --git a/kmir/src/tests/integration/data/prove-rs/closure_access_struct.rs b/kmir/src/tests/integration/data/prove-rs/closure_access_struct-fail.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/closure_access_struct.rs rename to kmir/src/tests/integration/data/prove-rs/closure_access_struct-fail.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/and_then_closure-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/and_then_closure-fail.main.expected new file mode 100644 index 000000000..a6b62b249 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/and_then_closure-fail.main.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (142 steps) +└─ 3 (stuck, leaf) + #traverseProjection ( toLocal ( 2 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( + span: 157 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected new file mode 100644 index 000000000..8a1aff14b --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (196 steps) +└─ 3 (stuck, leaf) + #traverseProjection ( toLocal ( 2 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( + span: 125 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index f4975bd29..8b1def7f8 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -63,6 +63,8 @@ 'test_offset_from-fail', 'ref-ptr-cast-elem-fail', 'ref-ptr-cast-elem-offset-fail', + 'and_then_closure-fail', + 'closure_access_struct-fail', ] diff --git a/kmir/uv.lock b/kmir/uv.lock index 8ed1b206d..88372f227 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -99,20 +99,20 @@ wheels = [ [[package]] name = "certifi" -version = "2026.1.4" +version = "2026.2.25" source = { registry = "https://pypi.org/simple" } -sdist = { url = "https://files.pythonhosted.org/packages/e0/2d/a891ca51311197f6ad14a7ef42e2399f36cf2f9bd44752b3dc4eab60fdc5/certifi-2026.1.4.tar.gz", hash = "sha256:ac726dd470482006e014ad384921ed6438c457018f4b3d204aea4281258b2120", size = 154268, upload-time = "2026-01-04T02:42:41.825Z" } +sdist = { url = "https://files.pythonhosted.org/packages/af/2d/7bf41579a8986e348fa033a31cdd0e4121114f6bce2457e8876010b092dd/certifi-2026.2.25.tar.gz", hash = "sha256:e887ab5cee78ea814d3472169153c2d12cd43b14bd03329a39a9c6e2e80bfba7", size = 155029, upload-time = "2026-02-25T02:54:17.342Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/e6/ad/3cc14f097111b4de0040c83a525973216457bbeeb63739ef1ed275c1c021/certifi-2026.1.4-py3-none-any.whl", hash = "sha256:9943707519e4add1115f44c2bc244f782c0249876bf51b6599fee1ffbedd685c", size = 152900, upload-time = "2026-01-04T02:42:40.15Z" }, + { url = "https://files.pythonhosted.org/packages/9a/3c/c17fb3ca2d9c3acff52e30b309f538586f9f5b9c9cf454f3845fc9af4881/certifi-2026.2.25-py3-none-any.whl", hash = "sha256:027692e4402ad994f1c42e52a4997a9763c646b73e4096e4d5d6db8af1d6f0fa", size = 153684, upload-time = "2026-02-25T02:54:15.766Z" }, ] [[package]] name = "chardet" -version = "5.2.0" +version = "6.0.0.post1" source = { registry = "https://pypi.org/simple" } -sdist = { url = "https://files.pythonhosted.org/packages/f3/0d/f7b6ab21ec75897ed80c17d79b15951a719226b9fababf1e40ea74d69079/chardet-5.2.0.tar.gz", hash = "sha256:1b3b6ff479a8c414bc3fa2c0852995695c4a026dcd6d0633b2dd092ca39c1cf7", size = 2069618, upload-time = "2023-08-01T19:23:02.662Z" } +sdist = { url = "https://files.pythonhosted.org/packages/7f/42/fb9436c103a881a377e34b9f58d77b5f503461c702ff654ebe86151bcfe9/chardet-6.0.0.post1.tar.gz", hash = "sha256:6b78048c3c97c7b2ed1fbad7a18f76f5a6547f7d34dbab536cc13887c9a92fa4", size = 12521798, upload-time = "2026-02-22T15:09:17.925Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/38/6f/f5fbc992a329ee4e0f288c1fe0e2ad9485ed064cac731ed2fe47dcc38cbf/chardet-5.2.0-py3-none-any.whl", hash = "sha256:e1cf59446890a00105fe7b7912492ea04b6e6f06d4b742b2c788469e34c82970", size = 199385, upload-time = "2023-08-01T19:23:00.661Z" }, + { url = "https://files.pythonhosted.org/packages/66/42/5de54f632c2de53cd3415b3703383d5fff43a94cbc0567ef362515261a21/chardet-6.0.0.post1-py3-none-any.whl", hash = "sha256:c894a36800549adf7bb5f2af47033281b75fdfcd2aa0f0243be0ad22a52e2dcb", size = 627245, upload-time = "2026-02-22T15:09:15.876Z" }, ] [[package]] @@ -248,7 +248,7 @@ wheels = [ [[package]] name = "cookiecutter" -version = "2.6.0" +version = "2.7.0" source = { registry = "https://pypi.org/simple" } dependencies = [ { name = "arrow" }, @@ -260,9 +260,9 @@ dependencies = [ { name = "requests" }, { name = "rich" }, ] -sdist = { url = "https://files.pythonhosted.org/packages/52/17/9f2cd228eb949a91915acd38d3eecdc9d8893dde353b603f0db7e9f6be55/cookiecutter-2.6.0.tar.gz", hash = "sha256:db21f8169ea4f4fdc2408d48ca44859349de2647fbe494a9d6c3edfc0542c21c", size = 158767, upload-time = "2024-02-21T18:02:41.949Z" } +sdist = { url = "https://files.pythonhosted.org/packages/12/f6/c576423931c725c30f3c97e1eb5bdb53419c27ff7538751cfa6ad1a07f82/cookiecutter-2.7.0.tar.gz", hash = "sha256:b0bf50141201ebf022c95e3fa02a760b64e600b3675d6dabf97563425a62a707", size = 142869, upload-time = "2026-03-02T09:14:13.999Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/b6/d9/0137658a353168ffa9d0fc14b812d3834772040858ddd1cb6eeaf09f7a44/cookiecutter-2.6.0-py3-none-any.whl", hash = "sha256:a54a8e37995e4ed963b3e82831072d1ad4b005af736bb17b99c2cbd9d41b6e2d", size = 39177, upload-time = "2024-02-21T18:02:39.569Z" }, + { url = "https://files.pythonhosted.org/packages/94/1f/21c082112609cb53d89f86e34ea4fa160c0a5e63556ffa9495ad70566cf1/cookiecutter-2.7.0-py3-none-any.whl", hash = "sha256:08dc4398e2d8a57771c20703fa10f8d03952e870eddd46bbb832161dc784fa3d", size = 41616, upload-time = "2026-03-02T09:14:12.893Z" }, ] [[package]] @@ -406,11 +406,11 @@ wheels = [ [[package]] name = "filelock" -version = "3.24.3" +version = "3.25.0" source = { registry = "https://pypi.org/simple" } -sdist = { url = "https://files.pythonhosted.org/packages/73/92/a8e2479937ff39185d20dd6a851c1a63e55849e447a55e798cc2e1f49c65/filelock-3.24.3.tar.gz", hash = "sha256:011a5644dc937c22699943ebbfc46e969cdde3e171470a6e40b9533e5a72affa", size = 37935, upload-time = "2026-02-19T00:48:20.543Z" } +sdist = { url = "https://files.pythonhosted.org/packages/77/18/a1fd2231c679dcb9726204645721b12498aeac28e1ad0601038f94b42556/filelock-3.25.0.tar.gz", hash = "sha256:8f00faf3abf9dc730a1ffe9c354ae5c04e079ab7d3a683b7c32da5dd05f26af3", size = 40158, upload-time = "2026-03-01T15:08:45.916Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/9c/0f/5d0c71a1aefeb08efff26272149e07ab922b64f46c63363756224bd6872e/filelock-3.24.3-py3-none-any.whl", hash = "sha256:426e9a4660391f7f8a810d71b0555bce9008b0a1cc342ab1f6947d37639e002d", size = 24331, upload-time = "2026-02-19T00:48:18.465Z" }, + { url = "https://files.pythonhosted.org/packages/f9/0b/de6f54d4a8bedfe8645c41497f3c18d749f0bd3218170c667bf4b81d0cdd/filelock-3.25.0-py3-none-any.whl", hash = "sha256:5ccf8069f7948f494968fc0713c10e5c182a9c9d9eef3a636307a20c2490f047", size = 26427, upload-time = "2026-03-01T15:08:44.593Z" }, ] [[package]] @@ -529,11 +529,11 @@ wheels = [ [[package]] name = "isort" -version = "8.0.0" +version = "8.0.1" source = { registry = "https://pypi.org/simple" } -sdist = { url = "https://files.pythonhosted.org/packages/bf/e3/e72b0b3a85f24cf5fc2cd8e92b996592798f896024c5cdf3709232e6e377/isort-8.0.0.tar.gz", hash = "sha256:fddea59202f231e170e52e71e3510b99c373b6e571b55d9c7b31b679c0fed47c", size = 769482, upload-time = "2026-02-19T16:31:59.716Z" } +sdist = { url = "https://files.pythonhosted.org/packages/ef/7c/ec4ab396d31b3b395e2e999c8f46dec78c5e29209fac49d1f4dace04041d/isort-8.0.1.tar.gz", hash = "sha256:171ac4ff559cdc060bcfff550bc8404a486fee0caab245679c2abe7cb253c78d", size = 769592, upload-time = "2026-02-28T10:08:20.685Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/74/ea/cf3aad99dd12c026e2d6835d559efb6fc50ccfd5b46d42d5fec2608b116a/isort-8.0.0-py3-none-any.whl", hash = "sha256:184916a933041c7cf718787f7e52064f3c06272aff69a5cb4dc46497bd8911d9", size = 89715, upload-time = "2026-02-19T16:31:57.745Z" }, + { url = "https://files.pythonhosted.org/packages/3e/95/c7c34aa53c16353c56d0b802fba48d5f5caa2cdee7958acbcb795c830416/isort-8.0.1-py3-none-any.whl", hash = "sha256:28b89bc70f751b559aeca209e6120393d43fbe2490de0559662be7a9787e3d75", size = 89733, upload-time = "2026-02-28T10:08:19.466Z" }, ] [[package]] @@ -712,14 +712,14 @@ wheels = [ [[package]] name = "linkify-it-py" -version = "2.0.3" +version = "2.1.0" source = { registry = "https://pypi.org/simple" } dependencies = [ { name = "uc-micro-py" }, ] -sdist = { url = "https://files.pythonhosted.org/packages/2a/ae/bb56c6828e4797ba5a4821eec7c43b8bf40f69cda4d4f5f8c8a2810ec96a/linkify-it-py-2.0.3.tar.gz", hash = "sha256:68cda27e162e9215c17d786649d1da0021a451bdc436ef9e0fa0ba5234b9b048", size = 27946, upload-time = "2024-02-04T14:48:04.179Z" } +sdist = { url = "https://files.pythonhosted.org/packages/2e/c9/06ea13676ef354f0af6169587ae292d3e2406e212876a413bf9eece4eb23/linkify_it_py-2.1.0.tar.gz", hash = "sha256:43360231720999c10e9328dc3691160e27a718e280673d444c38d7d3aaa3b98b", size = 29158, upload-time = "2026-03-01T07:48:47.683Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/04/1e/b832de447dee8b582cac175871d2f6c3d5077cc56d5575cadba1fd1cccfa/linkify_it_py-2.0.3-py3-none-any.whl", hash = "sha256:6bcbc417b0ac14323382aef5c5192c0075bf8a9d6b41820a2b66371eac6b6d79", size = 19820, upload-time = "2024-02-04T14:48:02.496Z" }, + { url = "https://files.pythonhosted.org/packages/b4/de/88b3be5c31b22333b3ca2f6ff1de4e863d8fe45aaea7485f591970ec1d3e/linkify_it_py-2.1.0-py3-none-any.whl", hash = "sha256:0d252c1594ecba2ecedc444053db5d3a9b7ec1b0dd929c8f1d74dce89f86c05e", size = 19878, upload-time = "2026-03-01T07:48:46.098Z" }, ] [[package]] @@ -1311,7 +1311,7 @@ wheels = [ [[package]] name = "textual" -version = "8.0.0" +version = "8.0.1" source = { registry = "https://pypi.org/simple" } dependencies = [ { name = "markdown-it-py", extra = ["linkify"] }, @@ -1321,9 +1321,9 @@ dependencies = [ { name = "rich" }, { name = "typing-extensions" }, ] -sdist = { url = "https://files.pythonhosted.org/packages/f7/08/1e1f705825359590ddfaeda57653bd518c4ff7a96bb2c3239ba1b6fc4c51/textual-8.0.0.tar.gz", hash = "sha256:ce48f83a3d686c0fac0e80bf9136e1f8851c653aa6a4502e43293a151df18809", size = 1595895, upload-time = "2026-02-16T17:12:14.215Z" } +sdist = { url = "https://files.pythonhosted.org/packages/fb/e4/0f6b6c22a30d2dc2850b4d09c8684742cc4ab79501d4588ea05269c1de3f/textual-8.0.1.tar.gz", hash = "sha256:fe6544e57651a7c2a8249b90ec542b45fa945ce4560e69b0d563fb440e7c4db3", size = 6099133, upload-time = "2026-03-01T19:15:41.537Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/d3/be/e191c2a15da20530fde03564564e3e4b4220eb9d687d4014957e5c6a5e85/textual-8.0.0-py3-none-any.whl", hash = "sha256:8908f4ebe93a6b4f77ca7262197784a52162bc88b05f4ecf50ac93a92d49bb8f", size = 718904, upload-time = "2026-02-16T17:12:11.962Z" }, + { url = "https://files.pythonhosted.org/packages/a2/23/40e0019fa60d1e83123b72e3201879b32d68a0d6358b3588d23705107921/textual-8.0.1-py3-none-any.whl", hash = "sha256:6b7522c2bc1a3ab90f534144b7e0ca6e25d35c80942ef92ccfb42a54e945d581", size = 719152, upload-time = "2026-03-01T19:15:43.7Z" }, ] [[package]] @@ -1409,11 +1409,11 @@ wheels = [ [[package]] name = "uc-micro-py" -version = "1.0.3" +version = "2.0.0" source = { registry = "https://pypi.org/simple" } -sdist = { url = "https://files.pythonhosted.org/packages/91/7a/146a99696aee0609e3712f2b44c6274566bc368dfe8375191278045186b8/uc-micro-py-1.0.3.tar.gz", hash = "sha256:d321b92cff673ec58027c04015fcaa8bb1e005478643ff4a500882eaab88c48a", size = 6043, upload-time = "2024-02-09T16:52:01.654Z" } +sdist = { url = "https://files.pythonhosted.org/packages/78/67/9a363818028526e2d4579334460df777115bdec1bb77c08f9db88f6389f2/uc_micro_py-2.0.0.tar.gz", hash = "sha256:c53691e495c8db60e16ffc4861a35469b0ba0821fe409a8a7a0a71864d33a811", size = 6611, upload-time = "2026-03-01T06:31:27.526Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/37/87/1f677586e8ac487e29672e4b17455758fce261de06a0d086167bb760361a/uc_micro_py-1.0.3-py3-none-any.whl", hash = "sha256:db1dffff340817673d7b466ec86114a9dc0e9d4d9b5ba229d9d60e5c12600cd5", size = 6229, upload-time = "2024-02-09T16:52:00.371Z" }, + { url = "https://files.pythonhosted.org/packages/61/73/d21edf5b204d1467e06500080a50f79d49ef2b997c79123a536d4a17d97c/uc_micro_py-2.0.0-py3-none-any.whl", hash = "sha256:3603a3859af53e5a39bc7677713c78ea6589ff188d70f4fee165db88e22b242c", size = 6383, upload-time = "2026-03-01T06:31:26.257Z" }, ] [[package]]