diff --git a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md index 4fbd84645..7b3d37533 100644 --- a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md +++ b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md @@ -125,6 +125,55 @@ Execution gets stuck (no matching rule) when operands have different types or un rule #extractOperandType(_, _) => TyUnknown [owise] ``` +#### Ptr Offset Computations (`std::intrinsics::ptr_offset_from`, `std::intrinsics::ptr_offset_from_unsigned`) + +The `ptr_offset_from[_unsigned]` calculates the distance between two pointers within the same allocation, +i.e., pointers that refer to the same place and only differ in their offset from a given base. + +Additionally, for `ptr_offset_from_unsigned`, it is _known_ that the first argument has a greater offset than +the second argument, so the returned difference is always positive. + + +```k + rule #execIntrinsic(IntrinsicFunction(symbol("ptr_offset_from")), ARG1:Operand ARG2:Operand .Operands, DEST) + => #ptrOffsetDiff(ARG1, ARG2, true, DEST) + ... + + + rule #execIntrinsic(IntrinsicFunction(symbol("ptr_offset_from_unsigned")), ARG1:Operand ARG2:Operand .Operands, DEST) + => #ptrOffsetDiff(ARG1, ARG2, false, DEST) + ... + + + syntax KItem ::= #ptrOffsetDiff ( Evaluation , Evaluation , Bool , Place ) [seqstrict(1,2)] + + syntax MIRError ::= UBPtrOffsetDiff + + syntax UBPtrOffsetDiff ::= #UBErrorPtrOffsetDiff( Value , Value , Bool ) + + rule + #ptrOffsetDiff( + PtrLocal(HEIGHT, PLACE, _, metadata( _ , OFF1, _)), + PtrLocal(HEIGHT, PLACE, _, metadata( _ , OFF2, _)), + SIGNED_FLAG, + DEST + ) => #setLocalValue(DEST, Integer(OFF1 -Int OFF2, 64, SIGNED_FLAG)) + ... + + requires (SIGNED_FLAG orBool OFF1 >=Int OFF2) + + rule + #ptrOffsetDiff( + PtrLocal(_, _, _, _) #as PTR1, + PtrLocal(_, _, _, _) #as PTR2, + SIGNED_FLAG, + _DEST + ) => #UBErrorPtrOffsetDiff(PTR1, PTR2, SIGNED_FLAG) + ... + + [priority(100)] +``` + ```k endmodule ``` diff --git a/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected b/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected new file mode 100644 index 000000000..72b241b12 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected @@ -0,0 +1,137 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (296 steps) +├─ 3 (split) +│ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 8 ) ) +┃ +┃ (branch) +┣━━┓ subst: .Subst +┃ ┃ constraint: +┃ ┃ 0 ==Int ARG_INT1:Int &Int 18446744073709551615 +┃ │ +┃ ├─ 4 +┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 8 ) ) +┃ │ +┃ │ (582 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ subst: .Subst + ┃ constraint: + ┃ notBool 0 ==Int ARG_INT1:Int &Int 18446744073709551615 + │ + ├─ 5 + │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 8 ) ) + │ + │ (1 step) + ├─ 7 (split) + │ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 7 ) ) + ┃ + ┃ (branch) + ┣━━┓ subst: .Subst + ┃ ┃ constraint: + ┃ ┃ 1 ==Int ARG_INT1:Int &Int 18446744073709551615 + ┃ │ + ┃ ├─ 8 + ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 7 ) ) + ┃ │ + ┃ │ (99 steps) + ┃ └─ 10 (stuck, leaf) + ┃ #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 1 , place ( ... local: local + ┃ + ┗━━┓ subst: .Subst + ┃ constraint: + ┃ notBool 1 ==Int ARG_INT1:Int &Int 18446744073709551615 + │ + ├─ 9 + │ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 7 ) ) + │ + │ (1 step) + ├─ 11 (split) + │ #selectBlock ( switchTargets ( ... branches: branch ( 2 , basicBlockIdx ( 6 ) ) + ┃ + ┃ (branch) + ┣━━┓ subst: .Subst + ┃ ┃ constraint: + ┃ ┃ 2 ==Int ARG_INT1:Int &Int 18446744073709551615 + ┃ │ + ┃ ├─ 12 + ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 2 , basicBlockIdx ( 6 ) ) + ┃ │ + ┃ │ (99 steps) + ┃ └─ 14 (stuck, leaf) + ┃ #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 1 , place ( ... local: local + ┃ + ┗━━┓ subst: .Subst + ┃ constraint: + ┃ notBool 2 ==Int ARG_INT1:Int &Int 18446744073709551615 + │ + ├─ 13 + │ #selectBlock ( switchTargets ( ... branches: branch ( 2 , basicBlockIdx ( 6 ) ) + │ + │ (1 step) + ├─ 15 (split) + │ #selectBlock ( switchTargets ( ... branches: branch ( 3 , basicBlockIdx ( 5 ) ) + ┃ + ┃ (branch) + ┣━━┓ subst: .Subst + ┃ ┃ constraint: + ┃ ┃ 3 ==Int ARG_INT1:Int &Int 18446744073709551615 + ┃ │ + ┃ ├─ 16 + ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 3 , basicBlockIdx ( 5 ) ) + ┃ │ + ┃ │ (16 steps) + ┃ └─ 18 (stuck, leaf) + ┃ #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 0 , place ( ... local: local + ┃ + ┗━━┓ subst: .Subst + ┃ constraint: + ┃ notBool 3 ==Int ARG_INT1:Int &Int 18446744073709551615 + │ + ├─ 17 + │ #selectBlock ( switchTargets ( ... branches: branch ( 3 , basicBlockIdx ( 5 ) ) + │ + │ (1 step) + ├─ 19 (split) + │ #selectBlock ( switchTargets ( ... branches: branch ( 4 , basicBlockIdx ( 4 ) ) + ┃ + ┃ (branch) + ┣━━┓ subst: .Subst + ┃ ┃ constraint: + ┃ ┃ 4 ==Int ARG_INT1:Int &Int 18446744073709551615 + ┃ │ + ┃ ├─ 20 + ┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 4 , basicBlockIdx ( 4 ) ) + ┃ │ + ┃ │ (68 steps) + ┃ └─ 22 (stuck, leaf) + ┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , + ┃ span: 32 + ┃ + ┗━━┓ subst: .Subst + ┃ constraint: + ┃ notBool 4 ==Int ARG_INT1:Int &Int 18446744073709551615 + │ + ├─ 21 + │ #selectBlock ( switchTargets ( ... branches: branch ( 4 , basicBlockIdx ( 4 ) ) + │ + │ (6 steps) + ├─ 23 (terminal) + │ #EndProgram ~> .K + │ + ┊ constraint: true + ┊ subst: ... + └─ 2 (leaf, target, terminal) + #EndProgram ~> .K + + + diff --git a/kmir/src/tests/integration/data/prove-rs/test_offset_from-fail.rs b/kmir/src/tests/integration/data/prove-rs/test_offset_from-fail.rs new file mode 100644 index 000000000..274310eab --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/test_offset_from-fail.rs @@ -0,0 +1,43 @@ +#![feature(core_intrinsics)] +use std::intrinsics::ptr_offset_from_unsigned; // core::ptr variant since 1.87.0, not for us + +fn testing(mode: isize) { + let a = [1, 2, 3, 4, 5]; + let b = [6, 7, 8, 9, 10]; + let a_p = &a as *const i32; + let b_p = &b as *const i32; + let a1: *const i32 = &a[1]; + let a3: *const i32 = &a[3]; + let b1: *const i32 = &b[1]; + + match mode { + 0 => unsafe { // correct and expected operation on pointers with offset + let a1_p = a_p.add(1); + assert_eq!(a1_p.offset_from(a_p), 1); + assert_eq!(a_p.offset_from(a1_p), -1); + assert_eq!(ptr_offset_from_unsigned(a1_p, a_p), 1); + }, + 1 => unsafe { // correct and expected operation on addresses within arrays + assert_eq!(a3.offset_from(a1), 2); + assert_eq!(a1.offset_from(a3), -2); + }, + 2 => unsafe { // different allocation + assert_eq!(a1.offset_from(b1), 0xdeadbeef); // UB + }, + 3 => unsafe { + // violating assumption of a3 > a1 + assert_eq!(ptr_offset_from_unsigned(a1, a3), 0xdeadbeef); // UB + }, + 4 => unsafe { + let unit_p: *const () = &(); + assert_eq!(unit_p.offset_from(unit_p), 0xdeadbeef); // panics + }, + _ => () + } +} + + +fn main() { + testing(0); + testing(4); +} \ No newline at end of file diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 77f181b67..170b4da54 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -37,6 +37,7 @@ 'assume-cheatcode': ['check_assume'], 'assume-cheatcode-conflict-fail': ['check_assume_conflict'], 'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'], + 'test_offset_from-fail': ['testing'], } PROVE_RS_SHOW_SPECS = [ 'local-raw-fail', @@ -59,6 +60,7 @@ 'unions-fail', 'transmute-maybe-uninit-fail', 'iter_next_2-fail', + 'test_offset_from-fail', ]