Skip to content

Implement std::intrinsics::raw_eq support in KMIR #665

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 17 commits into
base: master
Choose a base branch
from
Open

Implement std::intrinsics::raw_eq support in KMIR #665

Show file tree
Hide file tree
Changes from 7 commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
0ed9d98
Add raw_eq_simple test for intrinsic raw_eq functionality
Stevengre Aug 27, 2025
e7f3a31
add test to exec_smir
Stevengre Aug 27, 2025
a545912
Implement std::intrinsics::raw_eq support in KMIR
Stevengre Aug 27, 2025
eb64d3e
remove useless \n
Stevengre Aug 27, 2025
28467a0
docs: Add documentation section for raw_eq intrinsic
Stevengre Aug 27, 2025
8f03fd7
docs: Document current limitations of raw_eq implementation
Stevengre Aug 27, 2025
9f66b04
update expected files
Stevengre Aug 27, 2025
95a6b5d
Update kmir/src/kmir/kdist/mir-semantics/kmir.md
Stevengre Aug 27, 2025
54de2b2
Update kmir/src/kmir/kdist/mir-semantics/kmir.md
Stevengre Aug 27, 2025
7eac083
docs: Improve intrinsic development documentation
Stevengre Aug 27, 2025
d05eaa5
update expected files
Stevengre Aug 28, 2025
296e95f
refactor: Keep operands within #execIntrinsic for better indexing
Stevengre Aug 28, 2025
3fb15d5
docs: Remove unnecessary Rust example in intrinsic guide
Stevengre Aug 28, 2025
6d3d53f
docs: Simplify intrinsic implementation examples
Stevengre Aug 28, 2025
1ada2ae
refactor: Simplify black_box intrinsic implementation
Stevengre Aug 28, 2025
105d2aa
docs: Remove redundant code style guideline
Stevengre Aug 28, 2025
e4a9bc0
updated expected
Stevengre Aug 28, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 48 additions & 3 deletions kmir/src/kmir/kdist/mir-semantics/kmir.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -515,7 +515,7 @@ An operand may be a `Reference` (the only way a function could access another fu

// Handle intrinsic functions - execute directly without setting up local stack frame
rule <k> #setUpCalleeData(IntrinsicFunction(INTRINSIC_NAME), ARGS)
=> #execIntrinsic(INTRINSIC_NAME, ARGS, DEST) ~> #execBlockIdx(RETURN_TARGET)
=> #readOperands(ARGS) ~> #execIntrinsic(INTRINSIC_NAME, DEST) ~> #execBlockIdx(RETURN_TARGET)
</k>
<currentFrame>
<dest> DEST </dest>
Expand All @@ -525,7 +525,7 @@ An operand may be a `Reference` (the only way a function could access another fu

syntax KItem ::= #setArgsFromStack ( Int, Operands)
| #setArgFromStack ( Int, Operand)
| #execIntrinsic ( Symbol, Operands, Place )
| #execIntrinsic ( Symbol, Place )
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe we should keep the operands within #execIntrinsic (might be better for indexing).
We can do the argument evaluation (currently done in readOperands) within each intrinsic implementation (where necessary). For the intrinsics we have as of now, black_box and raw_eq, the rules would look like

rule <k> #execIntrinsic(symbol("black_box"), ARG:Operand .Operands, PLACE) 
        => #setLocalValue(PLACE, ARG)  // this evaluates `ARG`
        ... 
        </k>

rule <k> #execIntrinsic(symbol("raw_eq"), ARG1:Operand ARG2:Operand .Operands, PLACE) 
        => #execRawEq(PLACE, #withDeref(ARG1), #withDeref(ARG2))
        ... 
        </k>

The #execRawEq needs two arguments of sort Evaluation, declared [seqstrict(2,3)], and the helper #withDeref would append the Deref projection to any existing ones.

syntax Operand ::= #withDeref(Operand) [function, total]

(constant operands may still use a Deref when the constant is statically allocated, not implemented yet)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you! That's better. One of my yesterday version is something like this. But I changed to this version because of gernalization.

But yes, it's more concise with this design. And thank you for the indexing thing. Let me refactor this.


// once all arguments have been retrieved, execute
rule <k> #setArgsFromStack(_, .Operands) ~> CONT => CONT </k>
Expand Down Expand Up @@ -629,7 +629,52 @@ its argument to the destination without modification.

```k
// Black box intrinsic implementation - identity function
rule <k> #execIntrinsic(symbol("black_box"), ARG .Operands, DEST) => #setLocalValue(DEST, ARG) ... </k>
rule <k> ListItem(ARG:Value) ~> #execIntrinsic(symbol("black_box"), 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.
This intrinsic is typically used for low-level memory comparison operations where type-specific equality methods
are not suitable.

**Current Limitations:**
The current implementation only handles the simple case where References point to values of the same type.
More complex scenarios require additional testing and implementation work:
- References to different types with the same memory representation
- References to composite types (structs, arrays, enums)
- References with different alignments or padding

Handling different types may require converting values to their byte representations before comparison,
which will need to be addressed when such use cases are encountered.

```k
// Raw eq intrinsic - byte-by-byte equality comparison of referenced values

// Handle Reference values by reading the referenced values directly
rule <k> ListItem(Reference(_OFFSET1, place(LOCAL1, PROJ1), _MUT1, _META1):Value)
ListItem(Reference(_OFFSET2, place(LOCAL2, PROJ2), _MUT2, _META2):Value)
~> #execIntrinsic(symbol("raw_eq"), DEST)
=> #readOperands(
operandCopy(place(LOCAL1, PROJ1))
operandCopy(place(LOCAL2, PROJ2))
.Operands
) ~> #execRawEq(DEST)
... </k>
[priority(1)]

// Dedicated raw_eq execution that compares dereferenced values
syntax KItem ::= #execRawEq(Place)
rule <k> ListItem(VAL1:Value) ListItem(VAL2:Value) ~> #execRawEq(DEST)
=> #setLocalValue(DEST, BoolVal(VAL1 ==K VAL2))
Copy link
Member

@jberthold jberthold Aug 28, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is a subtlety here that we have to address at some point: The VAL1 and VAL2 may be "equal" in our Value sort but not actually in Rust's low-level representation. For example, if we have

enum MyEnum {
    A(u64),
    B(i64),
}

and

struct MyStruct(u64);

then A(42) and MyStruct(42) would both be Aggregate(variantIdx(0), ListItem(Integer(42, 64, false))) in kmir but the byte layout has to store a tag for MyEnum to decide which variant it is. (or the other way round, we store a redundant variantIdx(0) for structs that is not needed in rustcs byte layout)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We could compare the layouts (stable-mir-json is extracting them but they are not currently in the MIR-AST in K), but that will become complex.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, what variantIdx(0) is for?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

To distinguish this case, we need to store the original type of the Aggregate? Maybe I can add a test case for this situation.

As I mentioned this issue #666, should we tackle all the features in this PR? What kind of case can be moved to the furture work?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(PS. Apologies. I'm trying to type in English directly without AI rephrasing for faster response. But I may use some wrong grammar and words.)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We could compare the layouts (stable-mir-json is extracting them but they are not currently in the MIR-AST in K), but that will become complex.

Maybe we should have a way to provide python hooks for K?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this feature will be used in p-token, @dkcumming? If not, maybe we should move this to future work.

And for this case, I'm curious about the real ouput of this raw_eq check. If this will return a false, then what's the purpose when they use raw_eq.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As a first version, we could only implement raw_eq for operands whose TypeInfo is the same.
(or maybe not the type ID, but the type when looked up in the type table, but there might be other IDs in that type recursively).
The type ID is stored with the local but we don't have it for values with projection.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems like this issue touches the deep about what our architecture should look like, including:

  1. how to tackle type info? --- If we use @ehildenb 's plan to traverse the types with its real identifier before sending it to the intial state, this problem should be easy to tackle. just store the name of the place that the reference pointed to. And we don't need to handle the type table anymore.
  2. what the reference type should be? --- should we have the information about the place that the reference pointed to, or just deref and check the type?
  3. Is Enum and Struct will be the same structure?

BTW, it looks weird with raw_eq in p-token to me, because it tries to compare things in bytes. Is that a problem caused by the float? (Or just because it uses so many unsafe ...)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the code in p-token compares arrays of bytes ([u8; 8] is how an "amount" is stored). Just guessing here, though.

... </k>

// Generic rule for non-Reference values (commented out for now - unclear what behavior should be)
// rule <k> ListItem(VAL1:Value) ListItem(VAL2:Value) ~> #execIntrinsic(symbol("raw_eq"), DEST)
// => #setLocalValue(DEST, BoolVal(VAL1 ==K VAL2))
// ... </k>
```

### Stopping on Program Errors
Expand Down
19 changes: 19 additions & 0 deletions kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
#![feature(core_intrinsics)]

use std::intrinsics::raw_eq;

// NOTE: This test demonstrates the raw_eq intrinsic implementation.
// Known issue: Haskell backend produces more verbose symbolic execution output
// compared to LLVM backend due to different handling of symbolic branches.
// Both backends correctly implement the intrinsic but output format differs.
Comment on lines +5 to +8
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this true? Then the test should not pass because both HS backend and LLVM backend are tested.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, I just changed the depth to investigate what the problem it is. And the current depth + 1 (or 3) will generate different states from different backends.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This means the LLVM backend is taking one branch and the HS backend explores more than one branch (non-deterministic branching). That should be investigated.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I found that is a switchBranch. Maybe invetigate this in another PR? What do you think?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It could be a problem with one of the new rules. Maybe related to using KItem instead of Evaluation. If it branches a lot we should probably not merge it without understanding why. The p-token proofs would start branching, too


fn main() {
let a = 42;
let b = 42;

// Test raw_eq intrinsic with identical values
let result = unsafe { raw_eq(&a, &b) };

// This assertion should pass as both values are identical
assert!(result);
}
1 change: 1 addition & 0 deletions kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.smir.json
View file
Open in desktop

Large diffs are not rendered by default.

91 changes: 91 additions & 0 deletions kmir/src/tests/integration/data/exec-smir/intrinsic/raw_eq_simple.state
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,91 @@
<kmir>
<k>
#execTerminator ( terminator (... kind: terminatorKindSwitchInt (... discr: operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , targets: switchTargets (... branches: branch ( 0 , basicBlockIdx ( 2 ) ) .Branches , otherwise: basicBlockIdx ( 3 ) ) ) , span: span ( 56 ) ) ) ~> .K
</k>
<retVal>
noReturn
</retVal>
<currentFunc>
ty ( 25 )
</currentFunc>
<currentFrame>
<currentBody>
ListItem ( basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 1 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandConstant ( constOperand (... span: span ( 52 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"*\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 4 ) , mutability: mutabilityMut ) ) , ty: ty ( 16 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 52 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 2 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandConstant ( constOperand (... span: span ( 53 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"*\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 4 ) , mutability: mutabilityMut ) ) , ty: ty ( 16 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 53 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 4 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 1 ) , projection: .ProjectionElems ) ) ) , span: span ( 54 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 2 ) , projection: .ProjectionElems ) ) ) , span: span ( 55 ) ) .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 25 ) , id: mirConstId ( 9 ) ) ) ) , args: operandCopy ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 3 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionUnreachable ) , span: span ( 51 ) ) ) )
ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindSwitchInt (... discr: operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , targets: switchTargets (... branches: branch ( 0 , basicBlockIdx ( 2 ) ) .Branches , otherwise: basicBlockIdx ( 3 ) ) ) , span: span ( 56 ) ) ) )
ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 57 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 26 ) , id: mirConstId ( 11 ) ) ) ) , args: operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00\x18\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: provenanceMapEntry (... provSize: 0 , allocId: allocId ( 0 ) ) .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 12 ) ) ) ) .Operands , destination: place (... local: local ( 6 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 57 ) ) ) )
ListItem ( basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 58 ) ) ) )
</currentBody>
<caller>
ty ( -1 )
</caller>
<dest>
place (... local: local ( 3 ) , projection: .ProjectionElems )
</dest>
<target>
someBasicBlockIdx ( basicBlockIdx ( 1 ) )
</target>
<unwind>
unwindActionUnreachable
</unwind>
<locals>
ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
ListItem ( typedValue ( Integer ( 42 , 32 , true ) , ty ( 16 ) , mutabilityNot ) )
ListItem ( typedValue ( Integer ( 42 , 32 , true ) , ty ( 16 ) , mutabilityNot ) )
ListItem ( typedValue ( BoolVal ( true ) , ty ( 28 ) , mutabilityNot ) )
ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 29 ) , mutabilityNot ) )
ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 2 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 29 ) , mutabilityNot ) )
ListItem ( newLocal ( ty ( 30 ) , mutabilityMut ) )
</locals>
</currentFrame>
<stack>
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
ListItem ( typedValue ( Integer ( 42 , 32 , true ) , ty ( 16 ) , mutabilityNot ) )
ListItem ( typedValue ( Integer ( 42 , 32 , true ) , ty ( 16 ) , mutabilityNot ) )
ListItem ( newLocal ( ty ( 28 ) , mutabilityNot ) )
ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 29 ) , mutabilityNot ) )
ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 2 ) , projection: .ProjectionElems ) , mutabilityNot , noMetadata ) , ty ( 29 ) , mutabilityNot ) )
ListItem ( newLocal ( ty ( 30 ) , mutabilityMut ) ) ) )
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
</stack>
<memory>
.Map
</memory>
<functions>
ty ( 20 ) |-> IntrinsicFunction ( symbol ( "black_box" ) )
ty ( 25 ) |-> IntrinsicFunction ( symbol ( "raw_eq" ) )
ty ( -1 ) |-> monoItemFn (... name: symbol ( "main" ) , id: defId ( 6 ) , body: someBody ( body (... blocks: basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 1 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandConstant ( constOperand (... span: span ( 52 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"*\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 4 ) , mutability: mutabilityMut ) ) , ty: ty ( 16 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 52 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 2 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandConstant ( constOperand (... span: span ( 53 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"*\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 4 ) , mutability: mutabilityMut ) ) , ty: ty ( 16 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 53 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 4 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 1 ) , projection: .ProjectionElems ) ) ) , span: span ( 54 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 2 ) , projection: .ProjectionElems ) ) ) , span: span ( 55 ) ) .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 25 ) , id: mirConstId ( 9 ) ) ) ) , args: operandCopy ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 3 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionUnreachable ) , span: span ( 51 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindSwitchInt (... discr: operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , targets: switchTargets (... branches: branch ( 0 , basicBlockIdx ( 2 ) ) .Branches , otherwise: basicBlockIdx ( 3 ) ) ) , span: span ( 56 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 57 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 26 ) , id: mirConstId ( 11 ) ) ) ) , args: operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00\x18\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: provenanceMapEntry (... provSize: 0 , allocId: allocId ( 0 ) ) .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 12 ) ) ) ) .Operands , destination: place (... local: local ( 6 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 57 ) ) ) basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 58 ) ) ) .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 59 ) , mut: mutabilityMut ) localDecl (... ty: ty ( 16 ) , span: span ( 60 ) , mut: mutabilityNot ) localDecl (... ty: ty ( 16 ) , span: span ( 61 ) , mut: mutabilityNot ) localDecl (... ty: ty ( 28 ) , span: span ( 62 ) , mut: mutabilityNot ) localDecl (... ty: ty ( 29 ) , span: span ( 54 ) , mut: mutabilityNot ) localDecl (... ty: ty ( 29 ) , span: span ( 55 ) , mut: mutabilityNot ) localDecl (... ty: ty ( 30 ) , span: span ( 57 ) , mut: mutabilityMut ) .LocalDecls , argCount: 0 , varDebugInfo: varDebugInfo (... name: symbol ( "a" ) , sourceInfo: sourceInfo (... span: span ( 60 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt ) varDebugInfo (... name: symbol ( "b" ) , sourceInfo: sourceInfo (... span: span ( 61 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt ) varDebugInfo (... name: symbol ( "result" ) , sourceInfo: sourceInfo (... span: span ( 62 ) , scope: sourceScope ( 3 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt ) .VarDebugInfos , spreadArg: noLocal , span: span ( 63 ) ) ) )
</functions>
<start-symbol>
symbol ( "main" )
</start-symbol>
<types>
ty ( 1 ) |-> typeInfoTupleType ( .Tys )
ty ( 5 ) |-> typeInfoRefType ( ty ( 31 ) )
ty ( 6 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyIsize ) )
ty ( 8 ) |-> typeInfoPtrType ( ty ( 32 ) )
ty ( 9 ) |-> typeInfoPrimitiveType ( primTypeUint ( uintTyU8 ) )
ty ( 10 ) |-> typeInfoEnumType ( "std::result::Result<isize, !>" , adtDef ( 12 ) , Discriminant ( 0 ) Discriminant ( 1 ) .Discriminants )
ty ( 11 ) |-> typeInfoRefType ( ty ( 12 ) )
ty ( 15 ) |-> typeInfoStructType ( "std::sys::pal::unix::process::process_common::ExitCode" , adtDef ( 18 ) , ty ( 9 ) .Tys )
ty ( 16 ) |-> typeInfoPrimitiveType ( primTypeInt ( intTyI32 ) )
ty ( 17 ) |-> typeInfoStructType ( "std::process::ExitCode" , adtDef ( 16 ) , ty ( 15 ) .Tys )
ty ( 18 ) |-> typeInfoRefType ( ty ( 15 ) )
ty ( 22 ) |-> typeInfoPtrType ( ty ( 12 ) )
ty ( 24 ) |-> typeInfoRefType ( ty ( 12 ) )
ty ( 27 ) |-> typeInfoRefType ( ty ( 34 ) )
ty ( 28 ) |-> typeInfoPrimitiveType ( primTypeBool )
ty ( 29 ) |-> typeInfoRefType ( ty ( 16 ) )
ty ( 30 ) |-> typeInfoVoidType
ty ( 32 ) |-> typeInfoPtrType ( ty ( 9 ) )
ty ( 33 ) |-> typeInfoRefType ( ty ( 35 ) )
ty ( 34 ) |-> typeInfoPrimitiveType ( primTypeStr )
ty ( 35 ) |-> typeInfoStructType ( "std::panic::Location<'_>" , adtDef ( 22 ) , ty ( 27 ) ty ( 36 ) ty ( 36 ) .Tys )
ty ( 36 ) |-> typeInfoPrimitiveType ( primTypeUint ( uintTyU32 ) )
</types>
<adt-to-ty>
adtDef ( 12 ) |-> ty ( 10 )
adtDef ( 16 ) |-> ty ( 17 )
adtDef ( 18 ) |-> ty ( 15 )
adtDef ( 22 ) |-> ty ( 35 )
</adt-to-ty>
</kmir>
6 changes: 6 additions & 0 deletions kmir/src/tests/integration/test_integration.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -289,6 +289,12 @@ def test_crate_examples(main_crate: Path, kmir: KMIR, update_expected_output: bo
EXEC_DATA_DIR / 'intrinsic' / 'blackbox.state',
1000,
),
(
'raw_eq_simple',
EXEC_DATA_DIR / 'intrinsic' / 'raw_eq_simple.smir.json',
EXEC_DATA_DIR / 'intrinsic' / 'raw_eq_simple.state',
65,
),
]


Expand Down
Loading