NO OP rules for compiler hint intrinsics

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 <k> #execIntrinsic(IntrinsicFunction(symbol("black_box")), ARG:Operand .Operands, DEST)
+        => #setLocalValue(DEST, ARG)
+       ... </k>
+```
+
+#### 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 <k> #execIntrinsic(IntrinsicFunction(symbol("cold_path")), .Operands, _DEST) => .K ... </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 <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_read_data")),  _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_data")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
+
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_read_instruction")),  _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_instruction")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </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 <k> #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))
+       ... </k>
+       <locals> LOCALS </locals>
+
+  // Compare values only if types are identical
+  syntax KItem ::= #execRawEqTyped(Place, Evaluation, MaybeTy, Evaluation, MaybeTy) [seqstrict(2,4)]
+  rule <k> #execRawEqTyped(DEST, VAL1:Value, TY1:Ty, VAL2:Value, TY2:Ty)
+        => #setLocalValue(DEST, BoolVal(VAL1 ==K VAL2))
+       ... </k>
+    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 <Int size(LOCALS) andBool isTypedLocal(LOCALS[I])
+    [preserves-definedness]
+  rule #extractOperandType(operandMove(place(local(I), PROJS)), LOCALS)
+       => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
+    requires 0 <=Int I andBool I <Int size(LOCALS) andBool isTypedLocal(LOCALS[I])
+    [preserves-definedness]
+  rule #extractOperandType(operandConstant(constOperand(_, _, mirConst(_, TY, _))), _) => TY
+  rule #extractOperandType(_, _) => TyUnknown [owise]
+```
+
+```k
+endmodule
+```

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
        </k>
 ```
 
-### 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 <k> #execIntrinsic(IntrinsicFunction(symbol("black_box")), ARG:Operand .Operands, DEST)
-        => #setLocalValue(DEST, ARG)
-       ... </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 <k> #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))
-       ... </k>
-       <locals> LOCALS </locals>
-
-  // Compare values only if types are identical
-  syntax KItem ::= #execRawEqTyped(Place, Evaluation, MaybeTy, Evaluation, MaybeTy) [seqstrict(2,4)]
-  rule <k> #execRawEqTyped(DEST, VAL1:Value, TY1:Ty, VAL2:Value, TY2:Ty)
-        => #setLocalValue(DEST, BoolVal(VAL1 ==K VAL2))
-       ... </k>
-    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 <Int size(LOCALS) andBool isTypedLocal(LOCALS[I])
-    [preserves-definedness]
-  rule #extractOperandType(operandMove(place(local(I), PROJS)), LOCALS)
-       => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)
-    requires 0 <=Int I andBool I <Int size(LOCALS) andBool isTypedLocal(LOCALS[I])
-    [preserves-definedness]
-  rule #extractOperandType(operandConstant(constOperand(_, _, mirConst(_, TY, _))), _) => 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

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::<i32>(ptr, 3);
+        intrinsics::prefetch_read_data::<i32>(ptr, 3);
+        assert_eq!(11, *ptr);
+    }
+
+    let ptr_mut = &mut data as *mut i32;
+    unsafe {
+        intrinsics::prefetch_write_instruction::<i32>(ptr_mut, 3);
+        intrinsics::prefetch_write_data::<i32>(ptr_mut, 3);
+        // (*ptr_mut) = 44;
+        // assert_eq!(44, *ptr); // FIXME: fails due to thunks on casts
+    }
+}

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
+    }
+}

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
+
+
+

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',
 ]