From 82ff3b794e0f3730323d04a5745513bb208ebb3e Mon Sep 17 00:00:00 2001 From: dkcumming Date: Mon, 10 Nov 2025 23:38:20 +1000 Subject: [PATCH 1/7] Refactored intrinsics --- .../kmir/kdist/mir-semantics/intrinsics.md | 82 +++++++++++++++++++ kmir/src/kmir/kdist/mir-semantics/kmir.md | 71 +--------------- 2 files changed, 84 insertions(+), 69 deletions(-) create mode 100644 kmir/src/kmir/kdist/mir-semantics/intrinsics.md 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..beeda0d5a --- /dev/null +++ b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md @@ -0,0 +1,82 @@ +# 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) + ... +``` + +#### 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 From d4d21020e804d39171ec08a73d8c452020c35c30 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Tue, 11 Nov 2025 00:18:12 +1000 Subject: [PATCH 2/7] Implements `cold_path` instrinics as a no op. This also handles `likely` and `unlikely` "intrinsics` that are actually `MonoItemFn`. --- kmir/src/kmir/kdist/mir-semantics/intrinsics.md | 11 +++++++++++ .../src/tests/integration/data/prove-rs/intrinsics.rs | 9 +++++++++ 2 files changed, 20 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/intrinsics.rs diff --git a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md index beeda0d5a..e02db8fb3 100644 --- a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md +++ b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md @@ -28,6 +28,17 @@ its argument to the destination without modification. ... ``` +#### 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. Related are "intrinsics" `likely`, and `unlikely` are not `Intrinsics` but +are `MonoItemFn` that call the `cold_path` intrinsic. + +```k + rule #execIntrinsic(IntrinsicFunction(symbol("cold_path")), .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. 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..00ce50fe2 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/intrinsics.rs @@ -0,0 +1,9 @@ +#![feature(core_intrinsics)] +use std::intrinsics; + +fn main() { + intrinsics::cold_path(); + let b = true; + intrinsics::likely(b); + intrinsics::unlikely(b); +} From d937ae75868667b1fbb8f10e0392f9887cfa0748 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Tue, 11 Nov 2025 01:41:07 +1000 Subject: [PATCH 3/7] Added `prefetch_read_data` and `prefetch_write_data` intrinsics as NO OP --- .../src/kmir/kdist/mir-semantics/intrinsics.md | 11 +++++++++++ .../integration/data/prove-rs/intrinsics.rs | 18 ++++++++++++++++++ 2 files changed, 29 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md index e02db8fb3..4410cfedb 100644 --- a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md +++ b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md @@ -39,6 +39,17 @@ are `MonoItemFn` that call the `cold_path` intrinsic. rule #execIntrinsic(IntrinsicFunction(symbol("cold_path")), .Operands, _DEST) => .K ... ``` +#### Prefetch (`std::intrinsics::prefetch_*`) + +The `prefetch_read_data` and `prefetch_write_data` 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 ... +``` + #### 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. diff --git a/kmir/src/tests/integration/data/prove-rs/intrinsics.rs b/kmir/src/tests/integration/data/prove-rs/intrinsics.rs index 00ce50fe2..96468abba 100644 --- a/kmir/src/tests/integration/data/prove-rs/intrinsics.rs +++ b/kmir/src/tests/integration/data/prove-rs/intrinsics.rs @@ -6,4 +6,22 @@ fn main() { 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_data::(ptr, 3); + assert_eq!(11, *ptr); + } + + let ptr_mut = &mut data as *mut i32; + unsafe { + intrinsics::prefetch_write_data::(ptr_mut, 3); + // (*ptr_mut) = 44; + // assert_eq!(44, *ptr); // FIXME: fails due to thunks on casts + } } From 711f133e90456d1c175f6d89672b201eefad033f Mon Sep 17 00:00:00 2001 From: dkcumming Date: Tue, 11 Nov 2025 02:35:40 +1000 Subject: [PATCH 4/7] Added simple pointer cast failure test --- .../data/prove-rs/raw-ptr-cast-fail.rs | 10 +++++ .../show/raw-ptr-cast-fail.main.expected | 40 +++++++++++++++++++ .../src/tests/integration/test_integration.py | 1 + 3 files changed, 51 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/raw-ptr-cast-fail.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected 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/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', ] From fe072145ecf8fd38982f5bf8b226298fc943fbd0 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Tue, 11 Nov 2025 02:44:28 +1000 Subject: [PATCH 5/7] Added `prefetch_{read, write}_instruction` as NO OP --- kmir/src/kmir/kdist/mir-semantics/intrinsics.md | 9 ++++++--- kmir/src/tests/integration/data/prove-rs/intrinsics.rs | 2 ++ 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md index 4410cfedb..93179991f 100644 --- a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md +++ b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md @@ -41,13 +41,16 @@ are `MonoItemFn` that call the `cold_path` intrinsic. #### Prefetch (`std::intrinsics::prefetch_*`) -The `prefetch_read_data` and `prefetch_write_data` 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. +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`) diff --git a/kmir/src/tests/integration/data/prove-rs/intrinsics.rs b/kmir/src/tests/integration/data/prove-rs/intrinsics.rs index 96468abba..fb8a2d0c1 100644 --- a/kmir/src/tests/integration/data/prove-rs/intrinsics.rs +++ b/kmir/src/tests/integration/data/prove-rs/intrinsics.rs @@ -14,12 +14,14 @@ fn prefetch() { 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 From 05181ee0a7fb6161ac5cdece0f6d46fc89106632 Mon Sep 17 00:00:00 2001 From: Daniel Cumming <124537596+dkcumming@users.noreply.github.com> Date: Tue, 11 Nov 2025 11:42:16 +1000 Subject: [PATCH 6/7] Update kmir/src/kmir/kdist/mir-semantics/intrinsics.md Co-authored-by: Jost Berthold --- kmir/src/kmir/kdist/mir-semantics/intrinsics.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md index 93179991f..f95c90d6a 100644 --- a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md +++ b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md @@ -32,8 +32,8 @@ its argument to the destination without modification. 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. Related are "intrinsics" `likely`, and `unlikely` are not `Intrinsics` but -are `MonoItemFn` that call the `cold_path` intrinsic. +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 ... From a82ff67584cea7ff37eac777a0e3c18f269d8e42 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Tue, 11 Nov 2025 11:44:12 +1000 Subject: [PATCH 7/7] Moved checked-arithmetic test to passing --- ...ithmetic-fail.rs => checked_arithmetic.rs} | 0 ...d_arithmetic-fail.checked_add_i32.expected | 39 ------------------- 2 files changed, 39 deletions(-) rename kmir/src/tests/integration/data/prove-rs/{checked_arithmetic-fail.rs => checked_arithmetic.rs} (100%) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/checked_arithmetic-fail.checked_add_i32.expected 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/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 - - -