diff --git a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md new file mode 100644 index 000000000..f95c90d6a --- /dev/null +++ b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md @@ -0,0 +1,107 @@ +# Rust Intrinsic Functions in K + +```k +// This looks like a circular import but only module KMIR in kmir.md imports KMIR-INTRINSICS +requires "kmir.md" + +module KMIR-INTRINSICS + imports KMIR-CONTROL-FLOW +``` + +### Intrinsic Functions + +Intrinsic functions are built-in functions provided by the compiler that don't have regular MIR bodies. +They are handled specially in the execution semantics through the `#execIntrinsic` mechanism. +When an intrinsic function is called, the execution bypasses the normal function call setup and directly +executes the intrinsic-specific logic. + +#### Black Box (`std::hint::black_box`) + +The `black_box` intrinsic serves as an optimization barrier, preventing the compiler from making assumptions +about the value passed through it. In the semantics, it acts as an identity function that simply passes +its argument to the destination without modification. + +```k + // Black box intrinsic implementation - identity function + rule #execIntrinsic(IntrinsicFunction(symbol("black_box")), ARG:Operand .Operands, DEST) + => #setLocalValue(DEST, ARG) + ... +``` + +#### Cold Path (`std::hint::cold_path`) + +The `cold_path` intrinsic is a compiler hint indicating that the current execution path is unlikely to be taken. +It provides metadata for the optimiser and code generator to improve layout and branch predicition but is +a NO OP for program semantics. `std::intrinsics::likely` and `std::intrinsics::unlikely` are +"normal" `MonoItemFn`s that call the `cold_path` intrinsic. + +```k + rule #execIntrinsic(IntrinsicFunction(symbol("cold_path")), .Operands, _DEST) => .K ... +``` + +#### Prefetch (`std::intrinsics::prefetch_*`) + +The `prefetch_read_data`, `prefetch_write_data`, `prefetch_read_instruction`, and `prefetch_write_instruction` +intrinsics in Rust are performance hints that request the CPU to load or prepare a memory address in cache +before it's used. They have no effect on program semantics, and are implemented as a NO OP in this semantics. + +```k + rule #execIntrinsic(IntrinsicFunction(symbol("prefetch_read_data")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... + rule #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_data")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... + + rule #execIntrinsic(IntrinsicFunction(symbol("prefetch_read_instruction")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... + rule #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_instruction")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... +``` + +#### Raw Eq (`std::intrinsics::raw_eq`) + +The `raw_eq` intrinsic performs byte-by-byte equality comparison of the memory contents pointed to by two references. +It returns a boolean value indicating whether the referenced values are equal. The implementation dereferences the +provided references to access the underlying values, then compares them using K's built-in equality operator. + +**Type Safety:** +The implementation requires operands to have identical types (`TY1 ==K TY2`) before performing the comparison. +Execution gets stuck (no matching rule) when operands have different types or unknown type information. + +```k + // Raw eq: dereference operands, extract types, and delegate to typed comparison + rule #execIntrinsic(IntrinsicFunction(symbol("raw_eq")), ARG1:Operand ARG2:Operand .Operands, PLACE) + => #execRawEqTyped(PLACE, #withDeref(ARG1), #extractOperandType(#withDeref(ARG1), LOCALS), + #withDeref(ARG2), #extractOperandType(#withDeref(ARG2), LOCALS)) + ... + LOCALS + + // Compare values only if types are identical + syntax KItem ::= #execRawEqTyped(Place, Evaluation, MaybeTy, Evaluation, MaybeTy) [seqstrict(2,4)] + rule #execRawEqTyped(DEST, VAL1:Value, TY1:Ty, VAL2:Value, TY2:Ty) + => #setLocalValue(DEST, BoolVal(VAL1 ==K VAL2)) + ... + requires TY1 ==K TY2 + [preserves-definedness] + + // Add deref projection to operands + syntax Operand ::= #withDeref(Operand) [function, total] + rule #withDeref(operandCopy(place(LOCAL, PROJ))) + => operandCopy(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems))) + rule #withDeref(operandMove(place(LOCAL, PROJ))) + => operandCopy(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems))) + // must not overwrite the value, just the reference is moved! + rule #withDeref(OP) => OP [owise] + + // Extract type from operands (locals with projections, constants, fallback to unknown) + syntax MaybeTy ::= #extractOperandType(Operand, List) [function, total] + rule #extractOperandType(operandCopy(place(local(I), PROJS)), LOCALS) + => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) + requires 0 <=Int I andBool I getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) + requires 0 <=Int I andBool I TY + rule #extractOperandType(_, _) => TyUnknown [owise] +``` + +```k +endmodule +``` diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index cedc1382d..8e805eb05 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -6,6 +6,7 @@ requires "rt/data.md" requires "rt/configuration.md" requires "lemmas/kmir-lemmas.md" requires "cheatcodes.md" +requires "intrinsics.md" ``` ## Syntax of MIR in K @@ -560,75 +561,6 @@ Drops are elaborated to Noops but still define the continuing control flow. Unre ``` -### Intrinsic Functions - -Intrinsic functions are built-in functions provided by the compiler that don't have regular MIR bodies. -They are handled specially in the execution semantics through the `#execIntrinsic` mechanism. -When an intrinsic function is called, the execution bypasses the normal function call setup and directly -executes the intrinsic-specific logic. - -#### Black Box (`std::hint::black_box`) - -The `black_box` intrinsic serves as an optimization barrier, preventing the compiler from making assumptions -about the value passed through it. In the semantics, it acts as an identity function that simply passes -its argument to the destination without modification. - -```k - // Black box intrinsic implementation - identity function - rule #execIntrinsic(IntrinsicFunction(symbol("black_box")), ARG:Operand .Operands, DEST) - => #setLocalValue(DEST, ARG) - ... -``` - -#### Raw Eq (`std::intrinsics::raw_eq`) - -The `raw_eq` intrinsic performs byte-by-byte equality comparison of the memory contents pointed to by two references. -It returns a boolean value indicating whether the referenced values are equal. The implementation dereferences the -provided references to access the underlying values, then compares them using K's built-in equality operator. - -**Type Safety:** -The implementation requires operands to have identical types (`TY1 ==K TY2`) before performing the comparison. -Execution gets stuck (no matching rule) when operands have different types or unknown type information. - -```k - // Raw eq: dereference operands, extract types, and delegate to typed comparison - rule #execIntrinsic(IntrinsicFunction(symbol("raw_eq")), ARG1:Operand ARG2:Operand .Operands, PLACE) - => #execRawEqTyped(PLACE, #withDeref(ARG1), #extractOperandType(#withDeref(ARG1), LOCALS), - #withDeref(ARG2), #extractOperandType(#withDeref(ARG2), LOCALS)) - ... - LOCALS - - // Compare values only if types are identical - syntax KItem ::= #execRawEqTyped(Place, Evaluation, MaybeTy, Evaluation, MaybeTy) [seqstrict(2,4)] - rule #execRawEqTyped(DEST, VAL1:Value, TY1:Ty, VAL2:Value, TY2:Ty) - => #setLocalValue(DEST, BoolVal(VAL1 ==K VAL2)) - ... - requires TY1 ==K TY2 - [preserves-definedness] - - // Add deref projection to operands - syntax Operand ::= #withDeref(Operand) [function, total] - rule #withDeref(operandCopy(place(LOCAL, PROJ))) - => operandCopy(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems))) - rule #withDeref(operandMove(place(LOCAL, PROJ))) - => operandCopy(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems))) - // must not overwrite the value, just the reference is moved! - rule #withDeref(OP) => OP [owise] - - // Extract type from operands (locals with projections, constants, fallback to unknown) - syntax MaybeTy ::= #extractOperandType(Operand, List) [function, total] - rule #extractOperandType(operandCopy(place(local(I), PROJS)), LOCALS) - => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) - requires 0 <=Int I andBool I getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS) - requires 0 <=Int I andBool I TY - rule #extractOperandType(_, _) => TyUnknown [owise] -``` - ### Stopping on Program Errors The semantics has a dedicated error sort to stop execution when flawed input or undefined behaviour is detected. @@ -656,5 +588,6 @@ module KMIR imports KMIR-AST // Necessary for the external Python parser imports KMIR-CONTROL-FLOW imports KMIR-CHEATCODES + imports KMIR-INTRINSICS imports KMIR-LEMMAS endmodule diff --git a/kmir/src/tests/integration/data/prove-rs/checked_arithmetic-fail.rs b/kmir/src/tests/integration/data/prove-rs/checked_arithmetic.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/checked_arithmetic-fail.rs rename to kmir/src/tests/integration/data/prove-rs/checked_arithmetic.rs diff --git a/kmir/src/tests/integration/data/prove-rs/intrinsics.rs b/kmir/src/tests/integration/data/prove-rs/intrinsics.rs new file mode 100644 index 000000000..fb8a2d0c1 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/intrinsics.rs @@ -0,0 +1,29 @@ +#![feature(core_intrinsics)] +use std::intrinsics; + +fn main() { + intrinsics::cold_path(); + let b = true; + intrinsics::likely(b); + intrinsics::unlikely(b); + prefetch(); +} + +fn prefetch() { + let mut data = 11; + let ptr = &data as *const i32; + + unsafe { + intrinsics::prefetch_read_instruction::(ptr, 3); + intrinsics::prefetch_read_data::(ptr, 3); + assert_eq!(11, *ptr); + } + + let ptr_mut = &mut data as *mut i32; + unsafe { + intrinsics::prefetch_write_instruction::(ptr_mut, 3); + intrinsics::prefetch_write_data::(ptr_mut, 3); + // (*ptr_mut) = 44; + // assert_eq!(44, *ptr); // FIXME: fails due to thunks on casts + } +} diff --git a/kmir/src/tests/integration/data/prove-rs/raw-ptr-cast-fail.rs b/kmir/src/tests/integration/data/prove-rs/raw-ptr-cast-fail.rs new file mode 100644 index 000000000..cf098c9c3 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/raw-ptr-cast-fail.rs @@ -0,0 +1,10 @@ +fn main() { + let mut data = 11; + let ptr = &data as *const i32; + + let ptr_mut = &mut data as *mut i32; + unsafe { + (*ptr_mut) = 44; + assert_eq!(44, *ptr); // FIXME: fails due to thunks on casts + } +} diff --git a/kmir/src/tests/integration/data/prove-rs/show/checked_arithmetic-fail.checked_add_i32.expected b/kmir/src/tests/integration/data/prove-rs/show/checked_arithmetic-fail.checked_add_i32.expected deleted file mode 100644 index 39a16b517..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/checked_arithmetic-fail.checked_add_i32.expected +++ /dev/null @@ -1,39 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (64 steps) -├─ 3 (split) -│ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 4 ) ) -┃ -┃ (branch) -┣━━┓ subst: .Subst -┃ ┃ constraint: -┃ ┃ ARG_INT1:Int +Int ARG_INT2:Int ==K truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 32 , Signed ) -┃ │ -┃ ├─ 4 -┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 4 ) ) -┃ │ -┃ │ (250 steps) -┃ ├─ 6 (terminal) -┃ │ #EndProgram ~> .K -┃ │ -┃ ┊ constraint: true -┃ ┊ subst: ... -┃ └─ 2 (leaf, target, terminal) -┃ #EndProgram ~> .K -┃ -┗━━┓ subst: .Subst - ┃ constraint: - ┃ notBool truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 32 , Signed ) ==K ARG_INT1:Int +Int ARG_INT2:Int - │ - ├─ 5 - │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 4 ) ) - │ - │ (6 steps) - └─ 7 (stuck, leaf) - #execIntrinsic ( IntrinsicFunction ( symbol ( "cold_path" ) ) , .Operands , plac - - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected new file mode 100644 index 000000000..f7d8e97bb --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected @@ -0,0 +1,40 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (119 steps) +├─ 3 +│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th +│ function: main +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC +┃ │ function: main +┃ │ +┃ │ (1 step) +┃ └─ 6 (stuck, leaf) +┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re +┃ function: main +┃ +┗━━┓ + │ + ├─ 5 + │ #execBlockIdx ( basicBlockIdx ( 3 ) ) ~> .K + │ function: main + │ + │ (124 steps) + ├─ 7 (terminal) + │ #EndProgram ~> .K + │ function: main + │ + ┊ constraint: true + ┊ subst: ... + └─ 2 (leaf, target, terminal) + #EndProgram ~> .K + + + diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index ae02d189d..4bdd55b39 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -52,6 +52,7 @@ 'pointer-cast-length-test-fail', 'niche-enum', 'assume-cheatcode-conflict-fail', + 'raw-ptr-cast-fail', ]