From 5e6bbb99b48e97a874d0050b32dd1a5e6507e014 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 11 Mar 2026 21:41:38 +1000 Subject: [PATCH 01/19] Created make target and pytest harness to prove verify-rust-std --- Makefile | 4 + .../0011-floats-ints/unchecked_add.rs | 84 +++++++++++++++++++ .../src/tests/integration/test_integration.py | 42 ++++++++++ 3 files changed, 130 insertions(+) create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add.rs diff --git a/Makefile b/Makefile index 503257b9b..f29cb16bb 100644 --- a/Makefile +++ b/Makefile @@ -56,6 +56,10 @@ test-integration: stable-mir-json build $(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration --maxfail=1 --verbose \ --durations=0 --numprocesses=$(PARALLEL) --dist=worksteal $(TEST_ARGS) +test-verify-rust-std: stable-mir-json build + $(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration -k test_verify_rust_std --maxfail=1 --verbose \ + --durations=0 --numprocesses=$(PARALLEL) --dist=worksteal $(TEST_ARGS) + # Checks and formatting format: autoflake isort black nix-fmt diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add.rs new file mode 100644 index 000000000..ef210d2d0 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add.rs @@ -0,0 +1,84 @@ +#![feature(unchecked_math)] + +fn main() { + unchecked_add_u8(0, 0); + unchecked_add_u16(0, 0); + unchecked_add_u32(0, 0); + unchecked_add_u64(0, 0); + unchecked_add_u128(0, 0); + unchecked_add_i8(0, 0); + unchecked_add_i16(0, 0); + unchecked_add_i32(0, 0); + unchecked_add_i64(0, 0); + unchecked_add_i128(0, 0); +} + +fn unchecked_add_u8(a: u8, b: u8) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_u16(a: u16, b: u16) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_u32(a: u32, b: u32) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_u64(a: u64, b: u64) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_u128(a: u128, b: u128) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_i8(a: i8, b: i8) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_i16(a: i16, b: i16) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_i32(a: i32, b: i32) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_i64(a: i64, b: i64) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_i128(a: i128, b: i128) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 8c59cce9b..2c9aa297c 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -109,6 +109,48 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: assert apr_proof.failed +VERIFY_RUST_STD_DIR = (Path(__file__).parent / 'data' / 'verify-rust-std').resolve(strict=True) +VERIFY_RUST_STD_FILES = list(VERIFY_RUST_STD_DIR.glob('**/*.rs')) +VERIFY_RUST_STD_START_SYMBOLS = { + 'unchecked_add': [ + 'unchecked_add_u8', + 'unchecked_add_u16', + 'unchecked_add_u32', + 'unchecked_add_u64', + 'unchecked_add_u128', + 'unchecked_add_i8', + 'unchecked_add_i16', + 'unchecked_add_i32', + 'unchecked_add_i64', + 'unchecked_add_i128', + ], +} + + +@pytest.mark.parametrize( + 'rs_file', + VERIFY_RUST_STD_FILES, + ids=[spec.stem for spec in VERIFY_RUST_STD_FILES], +) +def test_verify_rust_std(rs_file: Path, kmir: KMIR) -> None: + should_fail = rs_file.stem.endswith('fail') + + prove_rs_opts = ProveRSOpts(rs_file) + + start_symbols = ['main'] + if rs_file.stem in VERIFY_RUST_STD_START_SYMBOLS: + start_symbols = VERIFY_RUST_STD_START_SYMBOLS[rs_file.stem] + + for start_symbol in start_symbols: + prove_rs_opts.start_symbol = start_symbol + apr_proof = kmir.prove_rs(prove_rs_opts) + + if not should_fail: + assert apr_proof.passed + else: + assert apr_proof.failed + + MULTI_CRATE_DIR = (Path(__file__).parent / 'data' / 'crate-tests').resolve(strict=True) MULTI_CRATE_TESTS = list(MULTI_CRATE_DIR.glob('*/main-crate')) From bdb74621304c625208c8e8fc5117ad1ce47dbc9e Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 11 Mar 2026 21:50:09 +1000 Subject: [PATCH 02/19] Updated README with verification requirements --- .../0011-floats-ints/README.md | 35 +++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md new file mode 100644 index 000000000..1c7c4171b --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md @@ -0,0 +1,35 @@ +# Challenge 0011: Safety of Methods for Numeric Primitive Types + +Tests for [verify-rust-std challenge 0011](https://model-checking.github.io/verify-rust-std/challenges/0011-floats-ints.html), which verifies the safety of public unsafe methods for floats and integers in `core::num`. + +## Part 1: Unsafe Integer Methods + +All types: i8, i16, i32, i64, i128, u8, u16, u32, u64, u128 + +- [x] `unchecked_add` +- [ ] `unchecked_sub` +- [ ] `unchecked_mul` +- [ ] `unchecked_shl` +- [ ] `unchecked_shr` + +Signed only: i8, i16, i32, i64, i128 + +- [ ] `unchecked_neg` + +## Part 2: Safe API Verification + +All types: i8, i16, i32, i64, i128, u8, u16, u32, u64, u128 + +- [ ] `wrapping_shl` +- [ ] `wrapping_shr` + +Unsigned only: u8, u16, u32, u64 + +- [ ] `widening_mul` +- [ ] `carrying_mul` + +## Part 3: Float to Integer Conversion + +Types: f16, f32, f64, f128 + +- [ ] `to_int_unchecked` From 10f3dbeec55a94d1c1d0824c7a22ff0ff522e22c Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 11 Mar 2026 22:01:14 +1000 Subject: [PATCH 03/19] `wrapping_sub` passing --- .../0011-floats-ints/README.md | 2 +- .../0011-floats-ints/unchecked_sub.rs | 84 +++++++++++++++++++ .../src/tests/integration/test_integration.py | 12 +++ 3 files changed, 97 insertions(+), 1 deletion(-) create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_sub.rs diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md index 1c7c4171b..34b782417 100644 --- a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md @@ -7,7 +7,7 @@ Tests for [verify-rust-std challenge 0011](https://model-checking.github.io/veri All types: i8, i16, i32, i64, i128, u8, u16, u32, u64, u128 - [x] `unchecked_add` -- [ ] `unchecked_sub` +- [x] `unchecked_sub` - [ ] `unchecked_mul` - [ ] `unchecked_shl` - [ ] `unchecked_shr` diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_sub.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_sub.rs new file mode 100644 index 000000000..8745dd6d3 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_sub.rs @@ -0,0 +1,84 @@ +#![feature(unchecked_math)] + +fn main() { + unchecked_sub_u8(0, 0); + unchecked_sub_u16(0, 0); + unchecked_sub_u32(0, 0); + unchecked_sub_u64(0, 0); + unchecked_sub_u128(0, 0); + unchecked_sub_i8(0, 0); + unchecked_sub_i16(0, 0); + unchecked_sub_i32(0, 0); + unchecked_sub_i64(0, 0); + unchecked_sub_i128(0, 0); +} + +fn unchecked_sub_u8(a: u8, b: u8) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_u16(a: u16, b: u16) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_u32(a: u32, b: u32) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_u64(a: u64, b: u64) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_u128(a: u128, b: u128) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_i8(a: i8, b: i8) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_i16(a: i16, b: i16) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_i32(a: i32, b: i32) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_i64(a: i64, b: i64) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_i128(a: i128, b: i128) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 2c9aa297c..487e2b69a 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -124,6 +124,18 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: 'unchecked_add_i64', 'unchecked_add_i128', ], + 'unchecked_sub': [ + 'unchecked_sub_u8', + 'unchecked_sub_u16', + 'unchecked_sub_u32', + 'unchecked_sub_u64', + 'unchecked_sub_u128', + 'unchecked_sub_i8', + 'unchecked_sub_i16', + 'unchecked_sub_i32', + 'unchecked_sub_i64', + 'unchecked_sub_i128', + ], } From 70654eedc100115bcec4d26ea27b039aafa9f703 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 11 Mar 2026 22:20:08 +1000 Subject: [PATCH 04/19] `unchecked_mul` passing --- .../0011-floats-ints/README.md | 2 +- .../0011-floats-ints/unchecked_mul.rs | 84 +++++++++++++++++++ .../src/tests/integration/test_integration.py | 12 +++ 3 files changed, 97 insertions(+), 1 deletion(-) create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul.rs diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md index 34b782417..5a9c032ec 100644 --- a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md @@ -8,7 +8,7 @@ All types: i8, i16, i32, i64, i128, u8, u16, u32, u64, u128 - [x] `unchecked_add` - [x] `unchecked_sub` -- [ ] `unchecked_mul` +- [x] `unchecked_mul` - [ ] `unchecked_shl` - [ ] `unchecked_shr` diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul.rs new file mode 100644 index 000000000..f364a4d47 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul.rs @@ -0,0 +1,84 @@ +#![feature(unchecked_math)] + +fn main() { + unchecked_mul_u8(0, 0); + unchecked_mul_u16(0, 0); + unchecked_mul_u32(0, 0); + unchecked_mul_u64(0, 0); + unchecked_mul_u128(0, 0); + unchecked_mul_i8(0, 0); + unchecked_mul_i16(0, 0); + unchecked_mul_i32(0, 0); + unchecked_mul_i64(0, 0); + unchecked_mul_i128(0, 0); +} + +fn unchecked_mul_u8(a: u8, b: u8) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_u16(a: u16, b: u16) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_u32(a: u32, b: u32) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_u64(a: u64, b: u64) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_u128(a: u128, b: u128) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_i8(a: i8, b: i8) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_i16(a: i16, b: i16) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_i32(a: i32, b: i32) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_i64(a: i64, b: i64) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_i128(a: i128, b: i128) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 487e2b69a..ed635a202 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -136,6 +136,18 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: 'unchecked_sub_i64', 'unchecked_sub_i128', ], + 'unchecked_mul': [ + 'unchecked_mul_u8', + 'unchecked_mul_u16', + 'unchecked_mul_u32', + 'unchecked_mul_u64', + 'unchecked_mul_u128', + 'unchecked_mul_i8', + 'unchecked_mul_i16', + 'unchecked_mul_i32', + 'unchecked_mul_i64', + 'unchecked_mul_i128', + ], } From 6d61381d160b09d092f3954176c38ccd3d2e121b Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 11 Mar 2026 22:31:39 +1000 Subject: [PATCH 05/19] `unchecked_shl` passing --- .../0011-floats-ints/README.md | 2 +- .../0011-floats-ints/unchecked_shl.rs | 84 +++++++++++++++++++ .../src/tests/integration/test_integration.py | 12 +++ 3 files changed, 97 insertions(+), 1 deletion(-) create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl.rs diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md index 5a9c032ec..f0a3ac49b 100644 --- a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md @@ -9,7 +9,7 @@ All types: i8, i16, i32, i64, i128, u8, u16, u32, u64, u128 - [x] `unchecked_add` - [x] `unchecked_sub` - [x] `unchecked_mul` -- [ ] `unchecked_shl` +- [x] `unchecked_shl` - [ ] `unchecked_shr` Signed only: i8, i16, i32, i64, i128 diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl.rs new file mode 100644 index 000000000..86fde4935 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl.rs @@ -0,0 +1,84 @@ +#![feature(unchecked_shifts)] + +fn main() { + unchecked_shl_u8(0, 0); + unchecked_shl_u16(0, 0); + unchecked_shl_u32(0, 0); + unchecked_shl_u64(0, 0); + unchecked_shl_u128(0, 0); + unchecked_shl_i8(0, 0); + unchecked_shl_i16(0, 0); + unchecked_shl_i32(0, 0); + unchecked_shl_i64(0, 0); + unchecked_shl_i128(0, 0); +} + +fn unchecked_shl_u8(a: u8, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_u16(a: u16, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_u32(a: u32, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_u64(a: u64, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_u128(a: u128, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_i8(a: i8, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_i16(a: i16, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_i32(a: i32, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_i64(a: i64, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_i128(a: i128, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index ed635a202..ec7eee4bb 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -148,6 +148,18 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: 'unchecked_mul_i64', 'unchecked_mul_i128', ], + 'unchecked_shl': [ + 'unchecked_shl_u8', + 'unchecked_shl_u16', + 'unchecked_shl_u32', + 'unchecked_shl_u64', + 'unchecked_shl_u128', + 'unchecked_shl_i8', + 'unchecked_shl_i16', + 'unchecked_shl_i32', + 'unchecked_shl_i64', + 'unchecked_shl_i128', + ], } From a1c657917fba29fdc22adc6a4930af12f8cab51d Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 11 Mar 2026 22:43:19 +1000 Subject: [PATCH 06/19] Restricted `make test-verify-std-rust` to tests in the verify-std-rust/ --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index f29cb16bb..158e8c831 100644 --- a/Makefile +++ b/Makefile @@ -57,7 +57,7 @@ test-integration: stable-mir-json build --durations=0 --numprocesses=$(PARALLEL) --dist=worksteal $(TEST_ARGS) test-verify-rust-std: stable-mir-json build - $(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration -k test_verify_rust_std --maxfail=1 --verbose \ + $(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration/test_integration.py::test_verify_rust_std --maxfail=1 --verbose \ --durations=0 --numprocesses=$(PARALLEL) --dist=worksteal $(TEST_ARGS) # Checks and formatting From 4182d26108e3518a312b0e9ec2f58bf897485a94 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 11 Mar 2026 23:01:18 +1000 Subject: [PATCH 07/19] `unchecked_shr` passing --- .../0011-floats-ints/README.md | 2 +- .../0011-floats-ints/unchecked_shr.rs | 84 +++++++++++++++++++ .../src/tests/integration/test_integration.py | 12 +++ 3 files changed, 97 insertions(+), 1 deletion(-) create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr.rs diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md index f0a3ac49b..76b4469db 100644 --- a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md @@ -10,7 +10,7 @@ All types: i8, i16, i32, i64, i128, u8, u16, u32, u64, u128 - [x] `unchecked_sub` - [x] `unchecked_mul` - [x] `unchecked_shl` -- [ ] `unchecked_shr` +- [x] `unchecked_shr` Signed only: i8, i16, i32, i64, i128 diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr.rs new file mode 100644 index 000000000..13d7f8064 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr.rs @@ -0,0 +1,84 @@ +#![feature(unchecked_shifts)] + +fn main() { + unchecked_shr_u8(0, 0); + unchecked_shr_u16(0, 0); + unchecked_shr_u32(0, 0); + unchecked_shr_u64(0, 0); + unchecked_shr_u128(0, 0); + unchecked_shr_i8(0, 0); + unchecked_shr_i16(0, 0); + unchecked_shr_i32(0, 0); + unchecked_shr_i64(0, 0); + unchecked_shr_i128(0, 0); +} + +fn unchecked_shr_u8(a: u8, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_u16(a: u16, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_u32(a: u32, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_u64(a: u64, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_u128(a: u128, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_i8(a: i8, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_i16(a: i16, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_i32(a: i32, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_i64(a: i64, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_i128(a: i128, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index ec7eee4bb..efa2b7fdb 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -160,6 +160,18 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: 'unchecked_shl_i64', 'unchecked_shl_i128', ], + 'unchecked_shr': [ + 'unchecked_shr_u8', + 'unchecked_shr_u16', + 'unchecked_shr_u32', + 'unchecked_shr_u64', + 'unchecked_shr_u128', + 'unchecked_shr_i8', + 'unchecked_shr_i16', + 'unchecked_shr_i32', + 'unchecked_shr_i64', + 'unchecked_shr_i128', + ], } From d29c959106d352c573600e8a2465b2772aab8cc4 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 11 Mar 2026 23:26:44 +1000 Subject: [PATCH 08/19] `unchecked_neg` passing --- .../0011-floats-ints/README.md | 2 +- .../0011-floats-ints/unchecked_neg.rs | 44 +++++++++++++++++++ .../src/tests/integration/test_integration.py | 7 +++ 3 files changed, 52 insertions(+), 1 deletion(-) create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_neg.rs diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md index 76b4469db..4fa8f508c 100644 --- a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md @@ -14,7 +14,7 @@ All types: i8, i16, i32, i64, i128, u8, u16, u32, u64, u128 Signed only: i8, i16, i32, i64, i128 -- [ ] `unchecked_neg` +- [x] `unchecked_neg` ## Part 2: Safe API Verification diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_neg.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_neg.rs new file mode 100644 index 000000000..b9c70684c --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_neg.rs @@ -0,0 +1,44 @@ +#![feature(unchecked_neg)] + +fn main() { + unchecked_neg_i8(0); + unchecked_neg_i16(0); + unchecked_neg_i32(0); + unchecked_neg_i64(0); + unchecked_neg_i128(0); +} + +fn unchecked_neg_i8(a: i8) { + if let Some(expected) = a.checked_neg() { + let result = unsafe { a.unchecked_neg() }; + assert!(result == expected); + } +} + +fn unchecked_neg_i16(a: i16) { + if let Some(expected) = a.checked_neg() { + let result = unsafe { a.unchecked_neg() }; + assert!(result == expected); + } +} + +fn unchecked_neg_i32(a: i32) { + if let Some(expected) = a.checked_neg() { + let result = unsafe { a.unchecked_neg() }; + assert!(result == expected); + } +} + +fn unchecked_neg_i64(a: i64) { + if let Some(expected) = a.checked_neg() { + let result = unsafe { a.unchecked_neg() }; + assert!(result == expected); + } +} + +fn unchecked_neg_i128(a: i128) { + if let Some(expected) = a.checked_neg() { + let result = unsafe { a.unchecked_neg() }; + assert!(result == expected); + } +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index efa2b7fdb..b59e2a730 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -172,6 +172,13 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: 'unchecked_shr_i64', 'unchecked_shr_i128', ], + 'unchecked_neg': [ + 'unchecked_neg_i8', + 'unchecked_neg_i16', + 'unchecked_neg_i32', + 'unchecked_neg_i64', + 'unchecked_neg_i128', + ], } From efccba7a2bb1929f080232870596ecabdff1113c Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 12 Mar 2026 02:16:59 +1000 Subject: [PATCH 09/19] `wrapping_shl` added but fails with non-det branching --- .../0011-floats-ints/wrapping_shl.rs | 72 +++++++++++++++++++ .../src/tests/integration/test_integration.py | 12 ++++ 2 files changed, 84 insertions(+) create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shl.rs diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shl.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shl.rs new file mode 100644 index 000000000..e28de3376 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shl.rs @@ -0,0 +1,72 @@ +fn main() { + wrapping_shl_u8(0, 0); + wrapping_shl_u16(0, 0); + wrapping_shl_u32(0, 0); + wrapping_shl_u64(0, 0); + wrapping_shl_u128(0, 0); + wrapping_shl_i8(0, 0); + wrapping_shl_i16(0, 0); + wrapping_shl_i32(0, 0); + wrapping_shl_i64(0, 0); + wrapping_shl_i128(0, 0); +} + +fn wrapping_shl_u8(a: u8, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_u16(a: u16, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_u32(a: u32, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_u64(a: u64, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_u128(a: u128, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_i8(a: i8, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_i16(a: i16, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_i32(a: i32, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_i64(a: i64, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_i128(a: i128, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index b59e2a730..bb6daeac2 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -179,6 +179,18 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: 'unchecked_neg_i64', 'unchecked_neg_i128', ], + 'wrapping_shl': [ + 'wrapping_shl_u8', + 'wrapping_shl_u16', + 'wrapping_shl_u32', + 'wrapping_shl_u64', + 'wrapping_shl_u128', + 'wrapping_shl_i8', + 'wrapping_shl_i16', + 'wrapping_shl_i32', + 'wrapping_shl_i64', + 'wrapping_shl_i128', + ], } From e5686447c23b1d7ccc14c6a010171bc54563c047 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 12 Mar 2026 02:18:32 +1000 Subject: [PATCH 10/19] Added lemmas for `wrapping_shl` which is now passing --- .../kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md | 11 +++++++++++ .../data/verify-rust-std/0011-floats-ints/README.md | 2 +- 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md index 525e311a0..121ad10f3 100644 --- a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md +++ b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md @@ -163,6 +163,17 @@ power of two but the semantics will always operate with these particular ones. rule VAL &Int bitmask128 => VAL requires 0 <=Int VAL andBool VAL <=Int bitmask128 [simplification, preserves-definedness, smt-lemma] ``` +Shift operations like `wrapping_shl` mask the shift amount with `BITS - 1` (e.g., `rhs & 7` for `u8`). +When the shift amount is already known to be less than `BITS`, the mask is a no-op. + +```k + rule VAL &Int 7 => VAL requires 0 <=Int VAL andBool VAL VAL requires 0 <=Int VAL andBool VAL VAL requires 0 <=Int VAL andBool VAL VAL requires 0 <=Int VAL andBool VAL VAL requires 0 <=Int VAL andBool VAL Date: Thu, 12 Mar 2026 03:29:27 +1000 Subject: [PATCH 11/19] `wrapping_shr` passing --- .../0011-floats-ints/README.md | 2 +- .../0011-floats-ints/wrapping_shr.rs | 72 +++++++++++++++++++ .../src/tests/integration/test_integration.py | 12 ++++ 3 files changed, 85 insertions(+), 1 deletion(-) create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shr.rs diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md index a5d6626eb..c33b54d60 100644 --- a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md @@ -21,7 +21,7 @@ Signed only: i8, i16, i32, i64, i128 All types: i8, i16, i32, i64, i128, u8, u16, u32, u64, u128 - [x] `wrapping_shl` -- [ ] `wrapping_shr` +- [x] `wrapping_shr` Unsigned only: u8, u16, u32, u64 diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shr.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shr.rs new file mode 100644 index 000000000..ab182baf0 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shr.rs @@ -0,0 +1,72 @@ +fn main() { + wrapping_shr_u8(0, 0); + wrapping_shr_u16(0, 0); + wrapping_shr_u32(0, 0); + wrapping_shr_u64(0, 0); + wrapping_shr_u128(0, 0); + wrapping_shr_i8(0, 0); + wrapping_shr_i16(0, 0); + wrapping_shr_i32(0, 0); + wrapping_shr_i64(0, 0); + wrapping_shr_i128(0, 0); +} + +fn wrapping_shr_u8(a: u8, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_u16(a: u16, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_u32(a: u32, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_u64(a: u64, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_u128(a: u128, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_i8(a: i8, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_i16(a: i16, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_i32(a: i32, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_i64(a: i64, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_i128(a: i128, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index bb6daeac2..d2ccdaf85 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -191,6 +191,18 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: 'wrapping_shl_i64', 'wrapping_shl_i128', ], + 'wrapping_shr': [ + 'wrapping_shr_u8', + 'wrapping_shr_u16', + 'wrapping_shr_u32', + 'wrapping_shr_u64', + 'wrapping_shr_u128', + 'wrapping_shr_i8', + 'wrapping_shr_i16', + 'wrapping_shr_i32', + 'wrapping_shr_i64', + 'wrapping_shr_i128', + ], } From 3de3a679d10354691f5df47f3f368fdb17a45c90 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 12 Mar 2026 04:07:59 +1000 Subject: [PATCH 12/19] `widening_mul` passing --- .../0011-floats-ints/README.md | 2 +- .../0011-floats-ints/widening_mul.rs | 36 +++++++++++++++++++ .../src/tests/integration/test_integration.py | 6 ++++ 3 files changed, 43 insertions(+), 1 deletion(-) create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/widening_mul.rs diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md index c33b54d60..a46bf2a84 100644 --- a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md @@ -25,7 +25,7 @@ All types: i8, i16, i32, i64, i128, u8, u16, u32, u64, u128 Unsigned only: u8, u16, u32, u64 -- [ ] `widening_mul` +- [x] `widening_mul` - [ ] `carrying_mul` ## Part 3: Float to Integer Conversion diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/widening_mul.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/widening_mul.rs new file mode 100644 index 000000000..806c63d3f --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/widening_mul.rs @@ -0,0 +1,36 @@ +#![feature(bigint_helper_methods)] + +fn main() { + widening_mul_u8(0, 0); + widening_mul_u16(0, 0); + widening_mul_u32(0, 0); + widening_mul_u64(0, 0); +} + +fn widening_mul_u8(a: u8, b: u8) { + let (lo, hi) = a.widening_mul(b); + let expected = (a as u16) * (b as u16); + assert!(lo == (expected as u8)); + assert!(hi == ((expected >> u8::BITS) as u8)); +} + +fn widening_mul_u16(a: u16, b: u16) { + let (lo, hi) = a.widening_mul(b); + let expected = (a as u32) * (b as u32); + assert!(lo == (expected as u16)); + assert!(hi == ((expected >> u16::BITS) as u16)); +} + +fn widening_mul_u32(a: u32, b: u32) { + let (lo, hi) = a.widening_mul(b); + let expected = (a as u64) * (b as u64); + assert!(lo == (expected as u32)); + assert!(hi == ((expected >> u32::BITS) as u32)); +} + +fn widening_mul_u64(a: u64, b: u64) { + let (lo, hi) = a.widening_mul(b); + let expected = (a as u128) * (b as u128); + assert!(lo == (expected as u64)); + assert!(hi == ((expected >> u64::BITS) as u64)); +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index d2ccdaf85..11f615aaa 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -203,6 +203,12 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: 'wrapping_shr_i64', 'wrapping_shr_i128', ], + 'widening_mul': [ + 'widening_mul_u8', + 'widening_mul_u16', + 'widening_mul_u32', + 'widening_mul_u64', + ], } From 04c8165fdf03606cf944476d6feb956591502084 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 12 Mar 2026 04:24:01 +1000 Subject: [PATCH 13/19] `carrying_mul` passing --- .../0011-floats-ints/README.md | 2 +- .../0011-floats-ints/carrying_mul.rs | 36 +++++++++++++++++++ .../src/tests/integration/test_integration.py | 6 ++++ 3 files changed, 43 insertions(+), 1 deletion(-) create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/carrying_mul.rs diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md index a46bf2a84..7891e672b 100644 --- a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md @@ -26,7 +26,7 @@ All types: i8, i16, i32, i64, i128, u8, u16, u32, u64, u128 Unsigned only: u8, u16, u32, u64 - [x] `widening_mul` -- [ ] `carrying_mul` +- [x] `carrying_mul` ## Part 3: Float to Integer Conversion diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/carrying_mul.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/carrying_mul.rs new file mode 100644 index 000000000..fbe975d31 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/carrying_mul.rs @@ -0,0 +1,36 @@ +#![feature(bigint_helper_methods)] + +fn main() { + carrying_mul_u8(0, 0, 0); + carrying_mul_u16(0, 0, 0); + carrying_mul_u32(0, 0, 0); + carrying_mul_u64(0, 0, 0); +} + +fn carrying_mul_u8(a: u8, b: u8, c: u8) { + let (lo, hi) = a.carrying_mul(b, c); + let expected = (a as u16) * (b as u16) + (c as u16); + assert!(lo == (expected as u8)); + assert!(hi == ((expected >> u8::BITS) as u8)); +} + +fn carrying_mul_u16(a: u16, b: u16, c: u16) { + let (lo, hi) = a.carrying_mul(b, c); + let expected = (a as u32) * (b as u32) + (c as u32); + assert!(lo == (expected as u16)); + assert!(hi == ((expected >> u16::BITS) as u16)); +} + +fn carrying_mul_u32(a: u32, b: u32, c: u32) { + let (lo, hi) = a.carrying_mul(b, c); + let expected = (a as u64) * (b as u64) + (c as u64); + assert!(lo == (expected as u32)); + assert!(hi == ((expected >> u32::BITS) as u32)); +} + +fn carrying_mul_u64(a: u64, b: u64, c: u64) { + let (lo, hi) = a.carrying_mul(b, c); + let expected = (a as u128) * (b as u128) + (c as u128); + assert!(lo == (expected as u64)); + assert!(hi == ((expected >> u64::BITS) as u64)); +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 11f615aaa..224f594a2 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -209,6 +209,12 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: 'widening_mul_u32', 'widening_mul_u64', ], + 'carrying_mul': [ + 'carrying_mul_u8', + 'carrying_mul_u16', + 'carrying_mul_u32', + 'carrying_mul_u64', + ], } From be11fc544ca89570e8d9e516e1995c9cc0baf963 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Sat, 14 Mar 2026 03:36:16 +1000 Subject: [PATCH 14/19] Added float harnesses under `.txt` as they have many thunks --- .../0011-floats-ints/README.md | 4 ++ .../to_int_unchecked-fail.txt | 37 +++++++++++++++++++ .../src/tests/integration/test_integration.py | 6 +++ 3 files changed, 47 insertions(+) create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/to_int_unchecked-fail.txt diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md index 7891e672b..8a00eb767 100644 --- a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md @@ -30,6 +30,10 @@ Unsigned only: u8, u16, u32, u64 ## Part 3: Float to Integer Conversion +TODO: Currently floats are unsupported. However there the required harnesses are +added to `to_int_unchecked-fail.txt` which should be changed to `.rs` when floats +will not cause thunks and branching + Types: f16, f32, f64, f128 - [ ] `to_int_unchecked` diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/to_int_unchecked-fail.txt b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/to_int_unchecked-fail.txt new file mode 100644 index 000000000..9911fb291 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/to_int_unchecked-fail.txt @@ -0,0 +1,37 @@ +#![feature(f16)] +#![feature(f128)] + +fn main() { + to_int_unchecked_f16_i8(0.0); + to_int_unchecked_f32_i32(0.0); + to_int_unchecked_f64_i64(0.0); + to_int_unchecked_f128_i128(0.0); +} + +fn to_int_unchecked_f16_i8(a: f16) { + if a.is_finite() && a >= i8::MIN as f16 && a < -(i8::MIN as f16) { + let result = unsafe { a.to_int_unchecked::() }; + assert!(result == a as i8); + } +} + +fn to_int_unchecked_f32_i32(a: f32) { + if a.is_finite() && a >= i32::MIN as f32 && a < -(i32::MIN as f32) { + let result = unsafe { a.to_int_unchecked::() }; + assert!(result == a as i32); + } +} + +fn to_int_unchecked_f64_i64(a: f64) { + if a.is_finite() && a >= i64::MIN as f64 && a < -(i64::MIN as f64) { + let result = unsafe { a.to_int_unchecked::() }; + assert!(result == a as i64); + } +} + +fn to_int_unchecked_f128_i128(a: f128) { + if a.is_finite() && a >= i128::MIN as f128 && a < -(i128::MIN as f128) { + let result = unsafe { a.to_int_unchecked::() }; + assert!(result == a as i128); + } +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 224f594a2..04f2e65c0 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -215,6 +215,12 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: 'carrying_mul_u32', 'carrying_mul_u64', ], + 'to_int_unchecked-fail': [ + 'to_int_unchecked_f16_i8', + 'to_int_unchecked_f32_i32', + 'to_int_unchecked_f64_i64', + 'to_int_unchecked_f128_i128', + ], } From 29c9a0dd8cb50e93dc5abc1686dd5d1ebbe88074 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Sat, 14 Mar 2026 03:39:26 +1000 Subject: [PATCH 15/19] Added `show` for expected output on `-fail` tests --- .../src/tests/integration/test_integration.py | 23 ++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 04f2e65c0..51ce21c83 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -222,6 +222,9 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: 'to_int_unchecked_f128_i128', ], } +VERIFY_RUST_STD_SHOW_SPECS = [ + 'to_int_unchecked-fail', +] @pytest.mark.parametrize( @@ -229,10 +232,16 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: VERIFY_RUST_STD_FILES, ids=[spec.stem for spec in VERIFY_RUST_STD_FILES], ) -def test_verify_rust_std(rs_file: Path, kmir: KMIR) -> None: +def test_verify_rust_std(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: should_fail = rs_file.stem.endswith('fail') + should_show = rs_file.stem in VERIFY_RUST_STD_SHOW_SPECS + + if update_expected_output and not should_show: + pytest.skip() prove_rs_opts = ProveRSOpts(rs_file) + printer = PrettyPrinter(kmir.definition) + cterm_show = CTermShow(printer.print) start_symbols = ['main'] if rs_file.stem in VERIFY_RUST_STD_START_SYMBOLS: @@ -242,6 +251,18 @@ def test_verify_rust_std(rs_file: Path, kmir: KMIR) -> None: prove_rs_opts.start_symbol = start_symbol apr_proof = kmir.prove_rs(prove_rs_opts) + if should_show: + display_opts = ShowOpts( + rs_file.parent, apr_proof.id, full_printer=False, smir_info=None, omit_current_body=False + ) + shower = APRProofShow(kmir.definition, node_printer=KMIRAPRNodePrinter(cterm_show, apr_proof, display_opts)) + show_res = '\n'.join(shower.show(apr_proof)) + show_dir = rs_file.parent / 'show' + show_dir.mkdir(exist_ok=True) + assert_or_update_show_output( + show_res, show_dir / f'{rs_file.stem}.{start_symbol}.expected', update=update_expected_output + ) + if not should_fail: assert apr_proof.passed else: From c7259e96345ff3c8fb313a5cd7b80681d26c3bb6 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Sat, 14 Mar 2026 06:49:35 +1000 Subject: [PATCH 16/19] Added README.md for verify-rust-std --- kmir/src/tests/integration/data/verify-rust-std/README.md | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 kmir/src/tests/integration/data/verify-rust-std/README.md diff --git a/kmir/src/tests/integration/data/verify-rust-std/README.md b/kmir/src/tests/integration/data/verify-rust-std/README.md new file mode 100644 index 000000000..71543a821 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/README.md @@ -0,0 +1,3 @@ +# verify-rust-std challenges + +Test harnesses for verify-rust-std ([docs](https://model-checking.github.io/verify-rust-std/) / [github](https://github.com/model-checking/verify-rust-std/)) challenges. Each subdirectory corresponds to a challenge and contains a README.md on progress. From 24681b1dd5cbccf6a6316fe75667efe8680970d7 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Sat, 14 Mar 2026 06:50:44 +1000 Subject: [PATCH 17/19] All proofs are run with `--terminate-on-thunk` This is needed while we still have `thunk` in the semantics to catch UB --- kmir/src/tests/integration/data/verify-rust-std/README.md | 2 ++ kmir/src/tests/integration/test_integration.py | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/kmir/src/tests/integration/data/verify-rust-std/README.md b/kmir/src/tests/integration/data/verify-rust-std/README.md index 71543a821..21b806dc7 100644 --- a/kmir/src/tests/integration/data/verify-rust-std/README.md +++ b/kmir/src/tests/integration/data/verify-rust-std/README.md @@ -1,3 +1,5 @@ # verify-rust-std challenges Test harnesses for verify-rust-std ([docs](https://model-checking.github.io/verify-rust-std/) / [github](https://github.com/model-checking/verify-rust-std/)) challenges. Each subdirectory corresponds to a challenge and contains a README.md on progress. + +All tests are run with `--terminate-on-thunk`, so unresolved symbolic expressions (e.g. from unchecked operations with unmet preconditions) cause the proof to terminate rather than propagate. This means `-fail` tests detect UB by the prover being unable to resolve the unchecked operation on the violating path. diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 51ce21c83..d3cc1db02 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -239,7 +239,7 @@ def test_verify_rust_std(rs_file: Path, kmir: KMIR, update_expected_output: bool if update_expected_output and not should_show: pytest.skip() - prove_rs_opts = ProveRSOpts(rs_file) + prove_rs_opts = ProveRSOpts(rs_file, terminate_on_thunk=True) printer = PrettyPrinter(kmir.definition) cterm_show = CTermShow(printer.print) From a7373174f862f1668028dc13cc8d3804b0b02a76 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Sat, 14 Mar 2026 08:38:21 +1000 Subject: [PATCH 18/19] Added show output for failing tests and moved float test to runable --- .../0011-floats-ints/README.md | 5 +- ...d-fail.to_int_unchecked_f128_i128.expected | 38 ++++++++++ ...cked-fail.to_int_unchecked_f16_i8.expected | 39 ++++++++++ ...ked-fail.to_int_unchecked_f32_i32.expected | 15 ++++ ...ked-fail.to_int_unchecked_f64_i64.expected | 15 ++++ ...ecked_add-fail.unchecked_add_i128.expected | 34 +++++++++ ...hecked_add-fail.unchecked_add_i16.expected | 34 +++++++++ ...hecked_add-fail.unchecked_add_i32.expected | 34 +++++++++ ...hecked_add-fail.unchecked_add_i64.expected | 34 +++++++++ ...checked_add-fail.unchecked_add_i8.expected | 34 +++++++++ ...ecked_add-fail.unchecked_add_u128.expected | 34 +++++++++ ...hecked_add-fail.unchecked_add_u16.expected | 35 +++++++++ ...hecked_add-fail.unchecked_add_u32.expected | 35 +++++++++ ...hecked_add-fail.unchecked_add_u64.expected | 34 +++++++++ ...checked_add-fail.unchecked_add_u8.expected | 35 +++++++++ ...ecked_mul-fail.unchecked_mul_i128.expected | 34 +++++++++ ...hecked_mul-fail.unchecked_mul_i16.expected | 34 +++++++++ ...hecked_mul-fail.unchecked_mul_i32.expected | 34 +++++++++ ...hecked_mul-fail.unchecked_mul_i64.expected | 34 +++++++++ ...checked_mul-fail.unchecked_mul_i8.expected | 34 +++++++++ ...ecked_mul-fail.unchecked_mul_u128.expected | 34 +++++++++ ...hecked_mul-fail.unchecked_mul_u16.expected | 35 +++++++++ ...hecked_mul-fail.unchecked_mul_u32.expected | 35 +++++++++ ...hecked_mul-fail.unchecked_mul_u64.expected | 34 +++++++++ ...checked_mul-fail.unchecked_mul_u8.expected | 35 +++++++++ ...ecked_neg-fail.unchecked_neg_i128.expected | 35 +++++++++ ...hecked_neg-fail.unchecked_neg_i16.expected | 35 +++++++++ ...hecked_neg-fail.unchecked_neg_i32.expected | 35 +++++++++ ...hecked_neg-fail.unchecked_neg_i64.expected | 35 +++++++++ ...checked_neg-fail.unchecked_neg_i8.expected | 35 +++++++++ ...ecked_shl-fail.unchecked_shl_i128.expected | 35 +++++++++ ...hecked_shl-fail.unchecked_shl_i16.expected | 35 +++++++++ ...hecked_shl-fail.unchecked_shl_i32.expected | 35 +++++++++ ...hecked_shl-fail.unchecked_shl_i64.expected | 35 +++++++++ ...checked_shl-fail.unchecked_shl_i8.expected | 35 +++++++++ ...ecked_shl-fail.unchecked_shl_u128.expected | 35 +++++++++ ...hecked_shl-fail.unchecked_shl_u16.expected | 36 +++++++++ ...hecked_shl-fail.unchecked_shl_u32.expected | 36 +++++++++ ...hecked_shl-fail.unchecked_shl_u64.expected | 35 +++++++++ ...checked_shl-fail.unchecked_shl_u8.expected | 36 +++++++++ ...ecked_shr-fail.unchecked_shr_i128.expected | 35 +++++++++ ...hecked_shr-fail.unchecked_shr_i16.expected | 35 +++++++++ ...hecked_shr-fail.unchecked_shr_i32.expected | 35 +++++++++ ...hecked_shr-fail.unchecked_shr_i64.expected | 35 +++++++++ ...checked_shr-fail.unchecked_shr_i8.expected | 35 +++++++++ ...ecked_shr-fail.unchecked_shr_u128.expected | 35 +++++++++ ...hecked_shr-fail.unchecked_shr_u16.expected | 36 +++++++++ ...hecked_shr-fail.unchecked_shr_u32.expected | 36 +++++++++ ...hecked_shr-fail.unchecked_shr_u64.expected | 35 +++++++++ ...checked_shr-fail.unchecked_shr_u8.expected | 36 +++++++++ ...ecked_sub-fail.unchecked_sub_i128.expected | 34 +++++++++ ...hecked_sub-fail.unchecked_sub_i16.expected | 34 +++++++++ ...hecked_sub-fail.unchecked_sub_i32.expected | 34 +++++++++ ...hecked_sub-fail.unchecked_sub_i64.expected | 34 +++++++++ ...checked_sub-fail.unchecked_sub_i8.expected | 34 +++++++++ ...ecked_sub-fail.unchecked_sub_u128.expected | 34 +++++++++ ...hecked_sub-fail.unchecked_sub_u16.expected | 35 +++++++++ ...hecked_sub-fail.unchecked_sub_u32.expected | 35 +++++++++ ...hecked_sub-fail.unchecked_sub_u64.expected | 34 +++++++++ ...checked_sub-fail.unchecked_sub_u8.expected | 35 +++++++++ ...cked-fail.txt => to_int_unchecked-fail.rs} | 0 .../0011-floats-ints/unchecked_add-fail.rs | 64 ++++++++++++++++ .../0011-floats-ints/unchecked_mul-fail.rs | 64 ++++++++++++++++ .../0011-floats-ints/unchecked_neg-fail.rs | 34 +++++++++ .../0011-floats-ints/unchecked_shl-fail.rs | 64 ++++++++++++++++ .../0011-floats-ints/unchecked_shr-fail.rs | 64 ++++++++++++++++ .../0011-floats-ints/unchecked_sub-fail.rs | 64 ++++++++++++++++ .../src/tests/integration/test_integration.py | 73 +++++++++++++++++++ 68 files changed, 2447 insertions(+), 2 deletions(-) create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f128_i128.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f16_i8.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f32_i32.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f64_i64.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i128.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i16.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i32.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i64.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i8.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u128.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u16.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u32.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u64.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u8.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i128.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i16.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i32.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i64.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i8.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u128.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u16.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u32.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u64.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u8.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i128.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i16.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i32.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i64.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i8.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i128.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i16.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i32.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i64.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i8.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u128.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u16.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u32.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u64.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u8.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i128.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i16.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i32.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i64.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i8.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u128.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u16.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u32.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u64.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u8.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i128.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i16.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i32.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i64.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i8.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u128.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u16.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u32.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u64.expected create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u8.expected rename kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/{to_int_unchecked-fail.txt => to_int_unchecked-fail.rs} (100%) create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add-fail.rs create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul-fail.rs create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_neg-fail.rs create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl-fail.rs create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr-fail.rs create mode 100644 kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_sub-fail.rs diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md index 8a00eb767..17f8c3463 100644 --- a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md @@ -31,8 +31,9 @@ Unsigned only: u8, u16, u32, u64 ## Part 3: Float to Integer Conversion TODO: Currently floats are unsupported. However there the required harnesses are -added to `to_int_unchecked-fail.txt` which should be changed to `.rs` when floats -will not cause thunks and branching +added to `to_int_unchecked-fail.rs`, once they are passing this file should be +renamed to `to_int_unchecked.rs` and tests that demonstrate KMIR catching `UB` +should be added to `to_int_unchecked-fail.rs`. Types: f16, f32, f64, f128 diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f128_i128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f128_i128.expected new file mode 100644 index 000000000..b98f22762 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f128_i128.expected @@ -0,0 +1,38 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (31 steps) +├─ 3 +│ #cast ( #adjustRef ( ARG1:Value , 2 ) , castKindTransmute , ty ( 38 ) , ty ( 39 +│ span: 32 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 340282366920938463463374607 +┃ │ span: 32 +┃ │ +┃ │ (29 steps) +┃ ├─ 6 +┃ │ #cast ( Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 3402823669209384634 +┃ │ span: 115 +┃ │ +┃ │ (1 step) +┃ └─ 7 (leaf, terminal) +┃ thunk ( #cast ( Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 34028236692 +┃ span: 115 +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #cast ( #adjustRef ( ARG1:Value , 2 ) , castKindTransmute , ty ( 38 ) , + span: 32 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f16_i8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f16_i8.expected new file mode 100644 index 000000000..dbf6a9636 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f16_i8.expected @@ -0,0 +1,39 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (31 steps) +├─ 3 +│ #cast ( #adjustRef ( ARG1:Value , 2 ) , castKindTransmute , ty ( 22 ) , ty ( 23 +│ span: 32 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 65535 , 16 , false ) +~> #fr +┃ │ span: 32 +┃ │ +┃ │ (29 steps) +┃ ├─ 6 +┃ │ #cast ( Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 65535 &Int 32767 , +┃ │ span: 56 +┃ │ +┃ │ (1 step) +┃ └─ 7 (leaf, terminal) +┃ thunk ( #cast ( Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 65535 &Int +┃ span: 56 +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #cast ( #adjustRef ( ARG1:Value , 2 ) , castKindTransmute , ty ( 22 ) , + span: 32 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f32_i32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f32_i32.expected new file mode 100644 index 000000000..4ec73a403 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f32_i32.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (22 steps) +└─ 3 (stuck, leaf) + #execIntrinsic ( IntrinsicFunction ( symbol ( "fabsf32" ) ) , operandMove ( plac + span: 73 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f64_i64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f64_i64.expected new file mode 100644 index 000000000..39571fec2 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f64_i64.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (22 steps) +└─ 3 (stuck, leaf) + #execIntrinsic ( IntrinsicFunction ( symbol ( "fabsf64" ) ) , operandMove ( plac + span: 90 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i128.expected new file mode 100644 index 000000000..8ebaab361 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i128.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 128 , true ) , Intege +│ span: 301 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 128 , Signed ) , 128 , tru +┃ │ span: 301 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 128 , true ) + span: 301 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i16.expected new file mode 100644 index 000000000..469e3ebff --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i16.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , Integer +│ span: 115 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 16 , Signed ) , 16 , true +┃ │ span: 115 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , + span: 115 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i32.expected new file mode 100644 index 000000000..c23b7ba5e --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i32.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , Integer +│ span: 146 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 32 , Signed ) , 32 , true +┃ │ span: 146 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , + span: 146 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i64.expected new file mode 100644 index 000000000..57dd3469d --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i64.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , Integer +│ span: 177 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 64 , Signed ) , 64 , true +┃ │ span: 177 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , + span: 177 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i8.expected new file mode 100644 index 000000000..16b2aeed4 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i8.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , Integer +│ span: 53 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 8 , Signed ) , 8 , true ) +┃ │ span: 53 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , + span: 53 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u128.expected new file mode 100644 index 000000000..40d83226c --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u128.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 128 , false ) , Inte +│ span: 332 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int &Int 34028236692093846346337460743176 +┃ │ span: 332 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 128 , false + span: 332 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u16.expected new file mode 100644 index 000000000..97948e0a6 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u16.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) , Integ +│ span: 208 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int &Int 65535 , 16 , false ) +~> #freezer +┃ │ span: 208 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) + span: 208 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u32.expected new file mode 100644 index 000000000..1680f4224 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u32.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) , Integ +│ span: 239 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int &Int 4294967295 , 32 , false ) +~> #fr +┃ │ span: 239 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) + span: 239 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u64.expected new file mode 100644 index 000000000..412ad1c08 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u64.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) , Integ +│ span: 270 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int &Int 18446744073709551615 , 64 , fals +┃ │ span: 270 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) + span: 270 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u8.expected new file mode 100644 index 000000000..bd0e55614 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u8.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) , Intege +│ span: 84 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int &Int 255 , 8 , false ) +~> #freezer#se +┃ │ span: 84 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) + span: 84 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i128.expected new file mode 100644 index 000000000..257c4d3c5 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i128.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 128 , true ) , Intege +│ span: 301 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int *Int ARG_INT2:Int , 128 , Signed ) , 128 , tru +┃ │ span: 301 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 128 , true ) + span: 301 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i16.expected new file mode 100644 index 000000000..ac5d7b039 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i16.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , Integer +│ span: 115 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int *Int ARG_INT2:Int , 16 , Signed ) , 16 , true +┃ │ span: 115 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , + span: 115 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i32.expected new file mode 100644 index 000000000..fd2162753 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i32.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , Integer +│ span: 146 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int *Int ARG_INT2:Int , 32 , Signed ) , 32 , true +┃ │ span: 146 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , + span: 146 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i64.expected new file mode 100644 index 000000000..f8395cba5 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i64.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , Integer +│ span: 177 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int *Int ARG_INT2:Int , 64 , Signed ) , 64 , true +┃ │ span: 177 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , + span: 177 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i8.expected new file mode 100644 index 000000000..516befead --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i8.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , Integer +│ span: 53 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int *Int ARG_INT2:Int , 8 , Signed ) , 8 , true ) +┃ │ span: 53 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , + span: 53 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u128.expected new file mode 100644 index 000000000..7bc83384a --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u128.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 128 , false ) , Inte +│ span: 332 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int &Int 34028236692093846346337460743176 +┃ │ span: 332 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 128 , false + span: 332 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u16.expected new file mode 100644 index 000000000..9c8b8fa13 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u16.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) , Integ +│ span: 208 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int &Int 65535 , 16 , false ) +~> #freezer +┃ │ span: 208 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) + span: 208 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u32.expected new file mode 100644 index 000000000..f7153e5f8 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u32.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) , Integ +│ span: 239 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int &Int 4294967295 , 32 , false ) +~> #fr +┃ │ span: 239 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) + span: 239 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u64.expected new file mode 100644 index 000000000..8542f300a --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u64.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) , Integ +│ span: 270 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int &Int 18446744073709551615 , 64 , fals +┃ │ span: 270 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) + span: 270 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u8.expected new file mode 100644 index 000000000..6519b70b7 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u8.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) , Intege +│ span: 84 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int &Int 255 , 8 , false ) +~> #freezer#se +┃ │ span: 84 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) + span: 84 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i128.expected new file mode 100644 index 000000000..fd29da216 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i128.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (50 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 128 , true ) , Integer ( ARG_INT +│ span: 178 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( 0 -Int ARG_INT1:Int , 128 , Signed ) , 128 , true ) +~> #fre +┃ │ span: 178 +┃ │ +┃ │ (67 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 128 , true ) , Integer ( + span: 178 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i16.expected new file mode 100644 index 000000000..72f28e18e --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i16.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (50 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 16 , true ) , Integer ( ARG_INT1 +│ span: 91 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( 0 -Int ARG_INT1:Int , 16 , Signed ) , 16 , true ) +~> #freez +┃ │ span: 91 +┃ │ +┃ │ (67 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 16 , true ) , Integer ( + span: 91 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i32.expected new file mode 100644 index 000000000..1964ce895 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i32.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (50 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 32 , true ) , Integer ( ARG_INT1 +│ span: 120 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( 0 -Int ARG_INT1:Int , 32 , Signed ) , 32 , true ) +~> #freez +┃ │ span: 120 +┃ │ +┃ │ (67 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 32 , true ) , Integer ( + span: 120 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i64.expected new file mode 100644 index 000000000..bd1cbbe06 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i64.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (50 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 64 , true ) , Integer ( ARG_INT1 +│ span: 149 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( 0 -Int ARG_INT1:Int , 64 , Signed ) , 64 , true ) +~> #freez +┃ │ span: 149 +┃ │ +┃ │ (67 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 64 , true ) , Integer ( + span: 149 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i8.expected new file mode 100644 index 000000000..c15a88519 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i8.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (50 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 8 , true ) , Integer ( ARG_INT1: +│ span: 58 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( 0 -Int ARG_INT1:Int , 8 , Signed ) , 8 , true ) +~> #freezer +┃ │ span: 58 +┃ │ +┃ │ (67 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 8 , true ) , Integer ( A + span: 58 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i128.expected new file mode 100644 index 000000000..57eaa182d --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i128.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 128 , true ) , Intege +│ span: 274 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int < .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 128 , true ) + span: 274 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i16.expected new file mode 100644 index 000000000..7d5a42edc --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i16.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , Integer +│ span: 112 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int < .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , + span: 112 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i32.expected new file mode 100644 index 000000000..052ceb2ce --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i32.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , Integer +│ span: 139 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int < .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , + span: 139 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i64.expected new file mode 100644 index 000000000..d2eb45316 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i64.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , Integer +│ span: 166 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int < .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , + span: 166 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i8.expected new file mode 100644 index 000000000..d62c1b8b2 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i8.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , Integer +│ span: 58 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int < .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , + span: 58 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u128.expected new file mode 100644 index 000000000..29fbeb3d1 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u128.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 128 , false ) , Inte +│ span: 301 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int < .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 128 , false + span: 301 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u16.expected new file mode 100644 index 000000000..f188b583b --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u16.expected @@ -0,0 +1,36 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) , Integ +│ span: 193 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int < #free +┃ │ span: 193 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) + span: 193 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u32.expected new file mode 100644 index 000000000..cf5f2c5dd --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u32.expected @@ -0,0 +1,36 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) , Integ +│ span: 220 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int < +┃ │ span: 220 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) + span: 220 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u64.expected new file mode 100644 index 000000000..6ed421f4d --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u64.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) , Integ +│ span: 247 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int < .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) + span: 247 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u8.expected new file mode 100644 index 000000000..1ffb3dc3e --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u8.expected @@ -0,0 +1,36 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) , Intege +│ span: 85 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int < #freezer +┃ │ span: 85 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) + span: 85 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i128.expected new file mode 100644 index 000000000..a84d5aa5b --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i128.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 128 , true ) , Intege +│ span: 274 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int >>Int ARG_UINT2:Int modInt 3402823669209384634 +┃ │ span: 274 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 128 , true ) + span: 274 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i16.expected new file mode 100644 index 000000000..527202efb --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i16.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , Integer +│ span: 112 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int >>Int ARG_UINT2:Int modInt 65536 , 16 , Signed +┃ │ span: 112 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , + span: 112 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i32.expected new file mode 100644 index 000000000..0128d3fa8 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i32.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , Integer +│ span: 139 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int >>Int ARG_UINT2:Int modInt 4294967296 , 32 , S +┃ │ span: 139 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , + span: 139 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i64.expected new file mode 100644 index 000000000..9e7dad859 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i64.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , Integer +│ span: 166 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int >>Int ARG_UINT2:Int modInt 1844674407370955161 +┃ │ span: 166 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , + span: 166 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i8.expected new file mode 100644 index 000000000..a71512a69 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i8.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , Integer +│ span: 58 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int >>Int ARG_UINT2:Int modInt 256 , 8 , Signed ) +┃ │ span: 58 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , + span: 58 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u128.expected new file mode 100644 index 000000000..06c1a5167 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u128.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 128 , false ) , Inte +│ span: 301 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int >>Int ARG_UINT2:Int modInt 34028236692093846346337460743 +┃ │ span: 301 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 128 , false + span: 301 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u16.expected new file mode 100644 index 000000000..01762529e --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u16.expected @@ -0,0 +1,36 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) , Integ +│ span: 193 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int >>Int ARG_UINT2:Int modInt 65536 , 16 , false ) +~> #free +┃ │ span: 193 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) + span: 193 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u32.expected new file mode 100644 index 000000000..00cceb40c --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u32.expected @@ -0,0 +1,36 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) , Integ +│ span: 220 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int >>Int ARG_UINT2:Int modInt 4294967296 , 32 , false ) +~> +┃ │ span: 220 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) + span: 220 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u64.expected new file mode 100644 index 000000000..f700cf0d8 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u64.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) , Integ +│ span: 247 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int >>Int ARG_UINT2:Int modInt 18446744073709551616 , 64 , f +┃ │ span: 247 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) + span: 247 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u8.expected new file mode 100644 index 000000000..9c712f1a3 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u8.expected @@ -0,0 +1,36 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) , Intege +│ span: 85 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int >>Int ARG_UINT2:Int modInt 256 , 8 , false ) +~> #freezer +┃ │ span: 85 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) + span: 85 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i128.expected new file mode 100644 index 000000000..ea78ced21 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i128.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 128 , true ) , Intege +│ span: 301 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int -Int ARG_INT2:Int , 128 , Signed ) , 128 , tru +┃ │ span: 301 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 128 , true ) + span: 301 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i16.expected new file mode 100644 index 000000000..743fd093c --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i16.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , Integer +│ span: 115 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int -Int ARG_INT2:Int , 16 , Signed ) , 16 , true +┃ │ span: 115 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , + span: 115 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i32.expected new file mode 100644 index 000000000..c1a06dce6 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i32.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , Integer +│ span: 146 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int -Int ARG_INT2:Int , 32 , Signed ) , 32 , true +┃ │ span: 146 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , + span: 146 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i64.expected new file mode 100644 index 000000000..b42cde312 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i64.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , Integer +│ span: 177 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int -Int ARG_INT2:Int , 64 , Signed ) , 64 , true +┃ │ span: 177 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , + span: 177 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i8.expected new file mode 100644 index 000000000..0a56f6b97 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i8.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , Integer +│ span: 53 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int -Int ARG_INT2:Int , 8 , Signed ) , 8 , true ) +┃ │ span: 53 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , + span: 53 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u128.expected new file mode 100644 index 000000000..8588fcce4 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u128.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 128 , false ) , Inte +│ span: 332 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int -Int ARG_UINT2:Int &Int 34028236692093846346337460743176 +┃ │ span: 332 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 128 , false + span: 332 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u16.expected new file mode 100644 index 000000000..d8ace363c --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u16.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) , Integ +│ span: 208 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int -Int ARG_UINT2:Int &Int 65535 , 16 , false ) +~> #freezer +┃ │ span: 208 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) + span: 208 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u32.expected new file mode 100644 index 000000000..f800b206f --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u32.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) , Integ +│ span: 239 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int -Int ARG_UINT2:Int &Int 4294967295 , 32 , false ) +~> #fr +┃ │ span: 239 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) + span: 239 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u64.expected new file mode 100644 index 000000000..c0b199507 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u64.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) , Integ +│ span: 270 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int -Int ARG_UINT2:Int &Int 18446744073709551615 , 64 , fals +┃ │ span: 270 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) + span: 270 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u8.expected new file mode 100644 index 000000000..6888f0278 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u8.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) , Intege +│ span: 84 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int -Int ARG_UINT2:Int &Int 255 , 8 , false ) +~> #freezer#se +┃ │ span: 84 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) + span: 84 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/to_int_unchecked-fail.txt b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/to_int_unchecked-fail.rs similarity index 100% rename from kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/to_int_unchecked-fail.txt rename to kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/to_int_unchecked-fail.rs diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add-fail.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add-fail.rs new file mode 100644 index 000000000..85680b316 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add-fail.rs @@ -0,0 +1,64 @@ +#![feature(unchecked_math)] + +fn main() { + unchecked_add_u8(0, 0); + unchecked_add_u16(0, 0); + unchecked_add_u32(0, 0); + unchecked_add_u64(0, 0); + unchecked_add_u128(0, 0); + unchecked_add_i8(0, 0); + unchecked_add_i16(0, 0); + unchecked_add_i32(0, 0); + unchecked_add_i64(0, 0); + unchecked_add_i128(0, 0); +} + +fn unchecked_add_u8(a: u8, b: u8) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_u16(a: u16, b: u16) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_u32(a: u32, b: u32) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_u64(a: u64, b: u64) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_u128(a: u128, b: u128) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_i8(a: i8, b: i8) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_i16(a: i16, b: i16) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_i32(a: i32, b: i32) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_i64(a: i64, b: i64) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_i128(a: i128, b: i128) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul-fail.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul-fail.rs new file mode 100644 index 000000000..1fb9684cd --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul-fail.rs @@ -0,0 +1,64 @@ +#![feature(unchecked_math)] + +fn main() { + unchecked_mul_u8(0, 0); + unchecked_mul_u16(0, 0); + unchecked_mul_u32(0, 0); + unchecked_mul_u64(0, 0); + unchecked_mul_u128(0, 0); + unchecked_mul_i8(0, 0); + unchecked_mul_i16(0, 0); + unchecked_mul_i32(0, 0); + unchecked_mul_i64(0, 0); + unchecked_mul_i128(0, 0); +} + +fn unchecked_mul_u8(a: u8, b: u8) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_u16(a: u16, b: u16) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_u32(a: u32, b: u32) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_u64(a: u64, b: u64) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_u128(a: u128, b: u128) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_i8(a: i8, b: i8) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_i16(a: i16, b: i16) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_i32(a: i32, b: i32) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_i64(a: i64, b: i64) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_i128(a: i128, b: i128) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_neg-fail.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_neg-fail.rs new file mode 100644 index 000000000..35c732a0d --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_neg-fail.rs @@ -0,0 +1,34 @@ +#![feature(unchecked_neg)] + +fn main() { + unchecked_neg_i8(0); + unchecked_neg_i16(0); + unchecked_neg_i32(0); + unchecked_neg_i64(0); + unchecked_neg_i128(0); +} + +fn unchecked_neg_i8(a: i8) { + let result = unsafe { a.unchecked_neg() }; + assert!(result == a.wrapping_neg()); +} + +fn unchecked_neg_i16(a: i16) { + let result = unsafe { a.unchecked_neg() }; + assert!(result == a.wrapping_neg()); +} + +fn unchecked_neg_i32(a: i32) { + let result = unsafe { a.unchecked_neg() }; + assert!(result == a.wrapping_neg()); +} + +fn unchecked_neg_i64(a: i64) { + let result = unsafe { a.unchecked_neg() }; + assert!(result == a.wrapping_neg()); +} + +fn unchecked_neg_i128(a: i128) { + let result = unsafe { a.unchecked_neg() }; + assert!(result == a.wrapping_neg()); +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl-fail.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl-fail.rs new file mode 100644 index 000000000..3d35ab316 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl-fail.rs @@ -0,0 +1,64 @@ +#![feature(unchecked_shifts)] + +fn main() { + unchecked_shl_u8(0, 0); + unchecked_shl_u16(0, 0); + unchecked_shl_u32(0, 0); + unchecked_shl_u64(0, 0); + unchecked_shl_u128(0, 0); + unchecked_shl_i8(0, 0); + unchecked_shl_i16(0, 0); + unchecked_shl_i32(0, 0); + unchecked_shl_i64(0, 0); + unchecked_shl_i128(0, 0); +} + +fn unchecked_shl_u8(a: u8, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_u16(a: u16, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_u32(a: u32, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_u64(a: u64, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_u128(a: u128, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_i8(a: i8, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_i16(a: i16, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_i32(a: i32, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_i64(a: i64, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_i128(a: i128, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr-fail.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr-fail.rs new file mode 100644 index 000000000..c1192257f --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr-fail.rs @@ -0,0 +1,64 @@ +#![feature(unchecked_shifts)] + +fn main() { + unchecked_shr_u8(0, 0); + unchecked_shr_u16(0, 0); + unchecked_shr_u32(0, 0); + unchecked_shr_u64(0, 0); + unchecked_shr_u128(0, 0); + unchecked_shr_i8(0, 0); + unchecked_shr_i16(0, 0); + unchecked_shr_i32(0, 0); + unchecked_shr_i64(0, 0); + unchecked_shr_i128(0, 0); +} + +fn unchecked_shr_u8(a: u8, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_u16(a: u16, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_u32(a: u32, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_u64(a: u64, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_u128(a: u128, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_i8(a: i8, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_i16(a: i16, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_i32(a: i32, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_i64(a: i64, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_i128(a: i128, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_sub-fail.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_sub-fail.rs new file mode 100644 index 000000000..fd27fa0c4 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_sub-fail.rs @@ -0,0 +1,64 @@ +#![feature(unchecked_math)] + +fn main() { + unchecked_sub_u8(0, 0); + unchecked_sub_u16(0, 0); + unchecked_sub_u32(0, 0); + unchecked_sub_u64(0, 0); + unchecked_sub_u128(0, 0); + unchecked_sub_i8(0, 0); + unchecked_sub_i16(0, 0); + unchecked_sub_i32(0, 0); + unchecked_sub_i64(0, 0); + unchecked_sub_i128(0, 0); +} + +fn unchecked_sub_u8(a: u8, b: u8) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_u16(a: u16, b: u16) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_u32(a: u32, b: u32) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_u64(a: u64, b: u64) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_u128(a: u128, b: u128) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_i8(a: i8, b: i8) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_i16(a: i16, b: i16) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_i32(a: i32, b: i32) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_i64(a: i64, b: i64) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_i128(a: i128, b: i128) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index d3cc1db02..1127e9d20 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -215,6 +215,73 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: 'carrying_mul_u32', 'carrying_mul_u64', ], + 'unchecked_add-fail': [ + 'unchecked_add_u8', + 'unchecked_add_u16', + 'unchecked_add_u32', + 'unchecked_add_u64', + 'unchecked_add_u128', + 'unchecked_add_i8', + 'unchecked_add_i16', + 'unchecked_add_i32', + 'unchecked_add_i64', + 'unchecked_add_i128', + ], + 'unchecked_sub-fail': [ + 'unchecked_sub_u8', + 'unchecked_sub_u16', + 'unchecked_sub_u32', + 'unchecked_sub_u64', + 'unchecked_sub_u128', + 'unchecked_sub_i8', + 'unchecked_sub_i16', + 'unchecked_sub_i32', + 'unchecked_sub_i64', + 'unchecked_sub_i128', + ], + 'unchecked_mul-fail': [ + 'unchecked_mul_u8', + 'unchecked_mul_u16', + 'unchecked_mul_u32', + 'unchecked_mul_u64', + 'unchecked_mul_u128', + 'unchecked_mul_i8', + 'unchecked_mul_i16', + 'unchecked_mul_i32', + 'unchecked_mul_i64', + 'unchecked_mul_i128', + ], + 'unchecked_shl-fail': [ + 'unchecked_shl_u8', + 'unchecked_shl_u16', + 'unchecked_shl_u32', + 'unchecked_shl_u64', + 'unchecked_shl_u128', + 'unchecked_shl_i8', + 'unchecked_shl_i16', + 'unchecked_shl_i32', + 'unchecked_shl_i64', + 'unchecked_shl_i128', + ], + 'unchecked_shr-fail': [ + 'unchecked_shr_u8', + 'unchecked_shr_u16', + 'unchecked_shr_u32', + 'unchecked_shr_u64', + 'unchecked_shr_u128', + 'unchecked_shr_i8', + 'unchecked_shr_i16', + 'unchecked_shr_i32', + 'unchecked_shr_i64', + 'unchecked_shr_i128', + ], + 'unchecked_neg-fail': [ + 'unchecked_neg_i8', + 'unchecked_neg_i16', + 'unchecked_neg_i32', + 'unchecked_neg_i64', + 'unchecked_neg_i128', + ], 'to_int_unchecked-fail': [ 'to_int_unchecked_f16_i8', 'to_int_unchecked_f32_i32', @@ -223,6 +290,12 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: ], } VERIFY_RUST_STD_SHOW_SPECS = [ + 'unchecked_add-fail', + 'unchecked_sub-fail', + 'unchecked_mul-fail', + 'unchecked_shl-fail', + 'unchecked_shr-fail', + 'unchecked_neg-fail', 'to_int_unchecked-fail', ] From f54ce95d99a68401e231ab62adb4ba98bbdb8551 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Sun, 15 Mar 2026 20:49:14 +1000 Subject: [PATCH 19/19] Use parsed `.smir.json` to avoid repeated LLVM compilation Tested with `time make test-verify-rust-std TEST_ARGS='-k unchecked_add'` which resulted in a 17.8% reduction in time (110.643 seconds): - Before: 10m22.304s - After: 8m31.661s --- kmir/src/tests/integration/test_integration.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 1127e9d20..8555b8c95 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -12,7 +12,7 @@ from pyk.kast.pretty import PrettyPrinter from pyk.proof.show import APRProofShow -from kmir.cargo import CargoProject +from kmir.cargo import CargoProject, cargo_get_smir_json from kmir.kmir import KMIR, KMIRAPRNodePrinter from kmir.options import ProveOpts, ShowOpts from kmir.parse.parser import Parser @@ -312,7 +312,8 @@ def test_verify_rust_std(rs_file: Path, kmir: KMIR, update_expected_output: bool if update_expected_output and not should_show: pytest.skip() - prove_rs_opts = ProveRSOpts(rs_file, terminate_on_thunk=True) + parsed_smir = cargo_get_smir_json(rs_file) + prove_opts = ProveOpts(rs_file, terminate_on_thunk=True, parsed_smir=parsed_smir) printer = PrettyPrinter(kmir.definition) cterm_show = CTermShow(printer.print) @@ -321,8 +322,8 @@ def test_verify_rust_std(rs_file: Path, kmir: KMIR, update_expected_output: bool start_symbols = VERIFY_RUST_STD_START_SYMBOLS[rs_file.stem] for start_symbol in start_symbols: - prove_rs_opts.start_symbol = start_symbol - apr_proof = kmir.prove_rs(prove_rs_opts) + prove_opts.start_symbol = start_symbol + apr_proof = kmir.prove_program(prove_opts) if should_show: display_opts = ShowOpts(