diff --git a/Makefile b/Makefile index 503257b9b..158e8c831 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/test_integration.py::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/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 > 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/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.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/to_int_unchecked-fail.rs 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.rs @@ -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/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_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/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_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/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_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/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_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/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_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/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/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/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/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/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/data/verify-rust-std/README.md b/kmir/src/tests/integration/data/verify-rust-std/README.md new file mode 100644 index 000000000..21b806dc7 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/README.md @@ -0,0 +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 8c59cce9b..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 @@ -109,6 +109,240 @@ 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', + ], + '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', + ], + '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', + ], + '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', + ], + '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', + ], + 'unchecked_neg': [ + 'unchecked_neg_i8', + 'unchecked_neg_i16', + 'unchecked_neg_i32', + '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', + ], + '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', + ], + 'widening_mul': [ + 'widening_mul_u8', + 'widening_mul_u16', + 'widening_mul_u32', + 'widening_mul_u64', + ], + 'carrying_mul': [ + 'carrying_mul_u8', + 'carrying_mul_u16', + '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', + 'to_int_unchecked_f64_i64', + 'to_int_unchecked_f128_i128', + ], +} +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', +] + + +@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, 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() + + 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) + + 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_opts.start_symbol = start_symbol + apr_proof = kmir.prove_program(prove_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: + 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'))