Skip to content

Commit 8ef12df

Browse files
dkcummingjberthold
dkcumming
and
jberthold
authored
NO OP rules for compiler hint intrinsics (#828)
Some instrinsics do not affect the semantics of the compiled program but are hints to the compiler. In our semantics these intrinsics are NO OPs where the call is ignored and current continuation (`<k>` cell) moves onto the next term in the sequence. In particular there are rules implemented for these intrinsics: - `cold_path` - `prefetch_read_data` - `prefetch_write_data` - `prefetch_read_instruction` - `prefetch_write_instruction` By handling `cold_path` we also support `likely` and `unlikely` which are `MonoItemFn` that call the `cold_path` instrinic. This PR also refactors the intrinsics into their only file `intrinsics.md`. closes #802 --------- Co-authored-by: Jost Berthold <jost.berthold@gmail.com>
1 parent 2266b60 commit 8ef12df

File tree

8 files changed

+189
-108
lines changed

8 files changed

+189
-108
lines changed

‎kmir/src/kmir/kdist/mir-semantics/intrinsics.md‎

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
# Rust Intrinsic Functions in K
2+
3+
```k
4+
// This looks like a circular import but only module KMIR in kmir.md imports KMIR-INTRINSICS
5+
requires "kmir.md"
6+
7+
module KMIR-INTRINSICS
8+
imports KMIR-CONTROL-FLOW
9+
```
10+
11+
### Intrinsic Functions
12+
13+
Intrinsic functions are built-in functions provided by the compiler that don't have regular MIR bodies.
14+
They are handled specially in the execution semantics through the `#execIntrinsic` mechanism.
15+
When an intrinsic function is called, the execution bypasses the normal function call setup and directly
16+
executes the intrinsic-specific logic.
17+
18+
#### Black Box (`std::hint::black_box`)
19+
20+
The `black_box` intrinsic serves as an optimization barrier, preventing the compiler from making assumptions
21+
about the value passed through it. In the semantics, it acts as an identity function that simply passes
22+
its argument to the destination without modification.
23+
24+
```k
25+
// Black box intrinsic implementation - identity function
26+
rule <k> #execIntrinsic(IntrinsicFunction(symbol("black_box")), ARG:Operand .Operands, DEST)
27+
=> #setLocalValue(DEST, ARG)
28+
... </k>
29+
```
30+
31+
#### Cold Path (`std::hint::cold_path`)
32+
33+
The `cold_path` intrinsic is a compiler hint indicating that the current execution path is unlikely to be taken.
34+
It provides metadata for the optimiser and code generator to improve layout and branch predicition but is
35+
a NO OP for program semantics. `std::intrinsics::likely` and `std::intrinsics::unlikely` are
36+
"normal" `MonoItemFn`s that call the `cold_path` intrinsic.
37+
38+
```k
39+
rule <k> #execIntrinsic(IntrinsicFunction(symbol("cold_path")), .Operands, _DEST) => .K ... </k>
40+
```
41+
42+
#### Prefetch (`std::intrinsics::prefetch_*`)
43+
44+
The `prefetch_read_data`, `prefetch_write_data`, `prefetch_read_instruction`, and `prefetch_write_instruction`
45+
intrinsics in Rust are performance hints that request the CPU to load or prepare a memory address in cache
46+
before it's used. They have no effect on program semantics, and are implemented as a NO OP in this semantics.
47+
48+
```k
49+
rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_read_data")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
50+
rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_data")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
51+
52+
rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_read_instruction")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
53+
rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_instruction")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
54+
```
55+
56+
#### Raw Eq (`std::intrinsics::raw_eq`)
57+
58+
The `raw_eq` intrinsic performs byte-by-byte equality comparison of the memory contents pointed to by two references.
59+
It returns a boolean value indicating whether the referenced values are equal. The implementation dereferences the
60+
provided references to access the underlying values, then compares them using K's built-in equality operator.
61+
62+
**Type Safety:**
63+
The implementation requires operands to have identical types (`TY1 ==K TY2`) before performing the comparison.
64+
Execution gets stuck (no matching rule) when operands have different types or unknown type information.
65+
66+
```k
67+
// Raw eq: dereference operands, extract types, and delegate to typed comparison
68+
rule <k> #execIntrinsic(IntrinsicFunction(symbol("raw_eq")), ARG1:Operand ARG2:Operand .Operands, PLACE)
69+
=> #execRawEqTyped(PLACE, #withDeref(ARG1), #extractOperandType(#withDeref(ARG1), LOCALS),
70+
#withDeref(ARG2), #extractOperandType(#withDeref(ARG2), LOCALS))
71+
... </k>
72+
<locals> LOCALS </locals>
73+
74+
// Compare values only if types are identical
75+
syntax KItem ::= #execRawEqTyped(Place, Evaluation, MaybeTy, Evaluation, MaybeTy) [seqstrict(2,4)]
76+
rule <k> #execRawEqTyped(DEST, VAL1:Value, TY1:Ty, VAL2:Value, TY2:Ty)
77+
=> #setLocalValue(DEST, BoolVal(VAL1 ==K VAL2))
78+
... </k>
79+
requires TY1 ==K TY2
80+
[preserves-definedness]
81+
82+
// Add deref projection to operands
83+
syntax Operand ::= #withDeref(Operand) [function, total]
84+
rule #withDeref(operandCopy(place(LOCAL, PROJ)))
85+
=> operandCopy(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems)))
86+
rule #withDeref(operandMove(place(LOCAL, PROJ)))
87+
=> operandCopy(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems)))
88+
// must not overwrite the value, just the reference is moved!
89+
rule #withDeref(OP) => OP [owise]
90+
91+
// Extract type from operands (locals with projections, constants, fallback to unknown)
92+
syntax MaybeTy ::= #extractOperandType(Operand, List) [function, total]
93+
rule #extractOperandType(operandCopy(place(local(I), PROJS)), LOCALS)
94+
=> getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
95+
requires 0 <=Int I andBool I <Int size(LOCALS) andBool isTypedLocal(LOCALS[I])
96+
[preserves-definedness]
97+
rule #extractOperandType(operandMove(place(local(I), PROJS)), LOCALS)
98+
=> getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
99+
requires 0 <=Int I andBool I <Int size(LOCALS) andBool isTypedLocal(LOCALS[I])
100+
[preserves-definedness]
101+
rule #extractOperandType(operandConstant(constOperand(_, _, mirConst(_, TY, _))), _) => TY
102+
rule #extractOperandType(_, _) => TyUnknown [owise]
103+
```
104+
105+
```k
106+
endmodule
107+
```

‎kmir/src/kmir/kdist/mir-semantics/kmir.md‎

Lines changed: 2 additions & 69 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ requires "rt/data.md"
66
requires "rt/configuration.md"
77
requires "lemmas/kmir-lemmas.md"
88
requires "cheatcodes.md"
9+
requires "intrinsics.md"
910
```
1011

1112
## Syntax of MIR in K
@@ -560,75 +561,6 @@ Drops are elaborated to Noops but still define the continuing control flow. Unre
560561
</k>
561562
```
562563

563-
### Intrinsic Functions
564-
565-
Intrinsic functions are built-in functions provided by the compiler that don't have regular MIR bodies.
566-
They are handled specially in the execution semantics through the `#execIntrinsic` mechanism.
567-
When an intrinsic function is called, the execution bypasses the normal function call setup and directly
568-
executes the intrinsic-specific logic.
569-
570-
#### Black Box (`std::hint::black_box`)
571-
572-
The `black_box` intrinsic serves as an optimization barrier, preventing the compiler from making assumptions
573-
about the value passed through it. In the semantics, it acts as an identity function that simply passes
574-
its argument to the destination without modification.
575-
576-
```k
577-
// Black box intrinsic implementation - identity function
578-
rule <k> #execIntrinsic(IntrinsicFunction(symbol("black_box")), ARG:Operand .Operands, DEST)
579-
=> #setLocalValue(DEST, ARG)
580-
... </k>
581-
```
582-
583-
#### Raw Eq (`std::intrinsics::raw_eq`)
584-
585-
The `raw_eq` intrinsic performs byte-by-byte equality comparison of the memory contents pointed to by two references.
586-
It returns a boolean value indicating whether the referenced values are equal. The implementation dereferences the
587-
provided references to access the underlying values, then compares them using K's built-in equality operator.
588-
589-
**Type Safety:**
590-
The implementation requires operands to have identical types (`TY1 ==K TY2`) before performing the comparison.
591-
Execution gets stuck (no matching rule) when operands have different types or unknown type information.
592-
593-
```k
594-
// Raw eq: dereference operands, extract types, and delegate to typed comparison
595-
rule <k> #execIntrinsic(IntrinsicFunction(symbol("raw_eq")), ARG1:Operand ARG2:Operand .Operands, PLACE)
596-
=> #execRawEqTyped(PLACE, #withDeref(ARG1), #extractOperandType(#withDeref(ARG1), LOCALS),
597-
#withDeref(ARG2), #extractOperandType(#withDeref(ARG2), LOCALS))
598-
... </k>
599-
<locals> LOCALS </locals>
600-
601-
// Compare values only if types are identical
602-
syntax KItem ::= #execRawEqTyped(Place, Evaluation, MaybeTy, Evaluation, MaybeTy) [seqstrict(2,4)]
603-
rule <k> #execRawEqTyped(DEST, VAL1:Value, TY1:Ty, VAL2:Value, TY2:Ty)
604-
=> #setLocalValue(DEST, BoolVal(VAL1 ==K VAL2))
605-
... </k>
606-
requires TY1 ==K TY2
607-
[preserves-definedness]
608-
609-
// Add deref projection to operands
610-
syntax Operand ::= #withDeref(Operand) [function, total]
611-
rule #withDeref(operandCopy(place(LOCAL, PROJ)))
612-
=> operandCopy(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems)))
613-
rule #withDeref(operandMove(place(LOCAL, PROJ)))
614-
=> operandCopy(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems)))
615-
// must not overwrite the value, just the reference is moved!
616-
rule #withDeref(OP) => OP [owise]
617-
618-
// Extract type from operands (locals with projections, constants, fallback to unknown)
619-
syntax MaybeTy ::= #extractOperandType(Operand, List) [function, total]
620-
rule #extractOperandType(operandCopy(place(local(I), PROJS)), LOCALS)
621-
=> getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
622-
requires 0 <=Int I andBool I <Int size(LOCALS) andBool isTypedLocal(LOCALS[I])
623-
[preserves-definedness]
624-
rule #extractOperandType(operandMove(place(local(I), PROJS)), LOCALS)
625-
=> getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
626-
requires 0 <=Int I andBool I <Int size(LOCALS) andBool isTypedLocal(LOCALS[I])
627-
[preserves-definedness]
628-
rule #extractOperandType(operandConstant(constOperand(_, _, mirConst(_, TY, _))), _) => TY
629-
rule #extractOperandType(_, _) => TyUnknown [owise]
630-
```
631-
632564
### Stopping on Program Errors
633565

634566
The semantics has a dedicated error sort to stop execution when flawed input or undefined behaviour is detected.
@@ -656,5 +588,6 @@ module KMIR
656588
imports KMIR-AST // Necessary for the external Python parser
657589
imports KMIR-CONTROL-FLOW
658590
imports KMIR-CHEATCODES
591+
imports KMIR-INTRINSICS
659592
imports KMIR-LEMMAS
660593
endmodule

‎kmir/src/tests/integration/data/prove-rs/checked_arithmetic-fail.rs‎ renamed to ‎kmir/src/tests/integration/data/prove-rs/checked_arithmetic.rs‎

File renamed without changes.

‎kmir/src/tests/integration/data/prove-rs/intrinsics.rs‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
#![feature(core_intrinsics)]
2+
use std::intrinsics;
3+
4+
fn main() {
5+
intrinsics::cold_path();
6+
let b = true;
7+
intrinsics::likely(b);
8+
intrinsics::unlikely(b);
9+
prefetch();
10+
}
11+
12+
fn prefetch() {
13+
let mut data = 11;
14+
let ptr = &data as *const i32;
15+
16+
unsafe {
17+
intrinsics::prefetch_read_instruction::<i32>(ptr, 3);
18+
intrinsics::prefetch_read_data::<i32>(ptr, 3);
19+
assert_eq!(11, *ptr);
20+
}
21+
22+
let ptr_mut = &mut data as *mut i32;
23+
unsafe {
24+
intrinsics::prefetch_write_instruction::<i32>(ptr_mut, 3);
25+
intrinsics::prefetch_write_data::<i32>(ptr_mut, 3);
26+
// (*ptr_mut) = 44;
27+
// assert_eq!(44, *ptr); // FIXME: fails due to thunks on casts
28+
}
29+
}

‎kmir/src/tests/integration/data/prove-rs/raw-ptr-cast-fail.rs‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
fn main() {
2+
let mut data = 11;
3+
let ptr = &data as *const i32;
4+
5+
let ptr_mut = &mut data as *mut i32;
6+
unsafe {
7+
(*ptr_mut) = 44;
8+
assert_eq!(44, *ptr); // FIXME: fails due to thunks on casts
9+
}
10+
}

‎kmir/src/tests/integration/data/prove-rs/show/checked_arithmetic-fail.checked_add_i32.expected‎

Lines changed: 0 additions & 39 deletions
This file was deleted.

‎kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
2+
┌─ 1 (root, init)
3+
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ span: 0
5+
│
6+
│ (119 steps)
7+
├─ 3
8+
│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
9+
│ function: main
10+
┃
11+
┃ (1 step)
12+
┣━━┓
13+
┃ │
14+
┃ ├─ 4
15+
┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
16+
┃ │ function: main
17+
┃ │
18+
┃ │ (1 step)
19+
┃ └─ 6 (stuck, leaf)
20+
┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
21+
┃ function: main
22+
┃
23+
┗━━┓
24+
│
25+
├─ 5
26+
│ #execBlockIdx ( basicBlockIdx ( 3 ) ) ~> .K
27+
│ function: main
28+
│
29+
│ (124 steps)
30+
├─ 7 (terminal)
31+
│ #EndProgram ~> .K
32+
│ function: main
33+
│
34+
┊ constraint: true
35+
┊ subst: ...
36+
└─ 2 (leaf, target, terminal)
37+
#EndProgram ~> .K
38+
39+
40+

‎kmir/src/tests/integration/test_integration.py‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,7 @@
5252
'pointer-cast-length-test-fail',
5353
'niche-enum',
5454
'assume-cheatcode-conflict-fail',
55+
'raw-ptr-cast-fail',
5556
]
5657

5758

0 commit comments

Comments
 (0)