diff --git a/kmir/src/kmir/decoding.py b/kmir/src/kmir/decoding.py index 4d0dc95fb..27a2dc019 100644 --- a/kmir/src/kmir/decoding.py +++ b/kmir/src/kmir/decoding.py @@ -445,10 +445,12 @@ def _extract_tag(*, data: bytes, tag_offset: MachineSize, tag: Scalar) -> tuple[ case Initialized( value=PrimitiveInt( length=length, - signed=False, + signed=_, ), valid_range=_, ): + # Stable MIR enum discriminants are represented against the raw tag bits. + # Use unsigned decoding even when the scalar metadata marks the tag as signed. tag_data = data[tag_offset.in_bytes : tag_offset.in_bytes + length.value] tag_value = int.from_bytes(tag_data, byteorder='little', signed=False) return tag_value, length diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index ece4c9a3f..5a2b48c65 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -548,8 +548,10 @@ Therefore a heuristics is used here: andBool isTypedValue(LOCALS[TUPLE]) andBool isTupleType(lookupTy(tyOfLocal({LOCALS[TUPLE]}:>TypedLocal))) andBool isTypedLocal(LOCALS[CLOSURE]) - andBool typeInfoVoidType ==K lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)) - // either the closure ref type is missing from type table + andBool ( + typeInfoVoidType ==K lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)) + orBool isFunType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))) + ) [priority(40), preserves-definedness] rule [setupCalleeClosure2]: #setUpCalleeData( @@ -581,16 +583,22 @@ Therefore a heuristics is used here: // or the closure ref type pointee is missing from the type table andBool isRefType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))) andBool isTy(pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))) - andBool lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType + andBool ( + lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType + orBool isFunType(lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty)) + ) [priority(45), preserves-definedness] syntax Bool ::= isTupleType ( TypeInfo ) [function, total] | isRefType ( TypeInfo ) [function, total] + | isFunType ( TypeInfo ) [function, total] // ------------------------------------------------------- rule isTupleType(typeInfoTupleType(_, _)) => true rule isTupleType( _ ) => false [owise] rule isRefType(typeInfoRefType(_)) => true rule isRefType( _ ) => false [owise] + rule isFunType(typeInfoFunType(_)) => true + rule isFunType( _ ) => false [owise] syntax KItem ::= #setTupleArgs ( Int , Value ) | #setTupleArgs ( Int , List ) diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected index 60dbf8403..544958705 100644 --- a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected +++ b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected @@ -2,7 +2,7 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ -│ (740 steps) +│ (737 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ diff --git a/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.expected b/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.expected new file mode 100644 index 000000000..8916e2b4d --- /dev/null +++ b/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.expected @@ -0,0 +1 @@ +Aggregate ( variantIdx ( 1 ) , .List ) diff --git a/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.json b/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.json new file mode 100644 index 000000000..3696e0d04 --- /dev/null +++ b/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.json @@ -0,0 +1,138 @@ +{ + "bytes": [ + 0 + ], + "types": [], + "typeInfo": { + "EnumType": { + "name": "OrderingLike", + "adt_def": 72, + "discriminants": [ + 255, + 0, + 1 + ], + "fields": [ + [], + [], + [] + ], + "layout": { + "fields": { + "Arbitrary": { + "offsets": [ + { + "num_bits": 0 + } + ] + } + }, + "variants": { + "Multiple": { + "tag": { + "Initialized": { + "value": { + "Int": { + "length": "I8", + "signed": true + } + }, + "valid_range": { + "start": 255, + "end": 1 + } + } + }, + "tag_encoding": "Direct", + "tag_field": 0, + "variants": [ + { + "fields": { + "Arbitrary": { + "offsets": [] + } + }, + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Aggregate": { + "sized": true + } + }, + "abi_align": 1, + "size": { + "num_bits": 8 + } + }, + { + "fields": { + "Arbitrary": { + "offsets": [] + } + }, + "variants": { + "Single": { + "index": 1 + } + }, + "abi": { + "Aggregate": { + "sized": true + } + }, + "abi_align": 1, + "size": { + "num_bits": 8 + } + }, + { + "fields": { + "Arbitrary": { + "offsets": [] + } + }, + "variants": { + "Single": { + "index": 2 + } + }, + "abi": { + "Aggregate": { + "sized": true + } + }, + "abi_align": 1, + "size": { + "num_bits": 8 + } + } + ] + } + }, + "abi": { + "Scalar": { + "Initialized": { + "value": { + "Int": { + "length": "I8", + "signed": true + } + }, + "valid_range": { + "start": 255, + "end": 1 + } + } + } + }, + "abi_align": 1, + "size": { + "num_bits": 8 + } + } + } + } +} diff --git a/kmir/src/tests/integration/data/prove-rs/and_then_closure-fail.rs b/kmir/src/tests/integration/data/prove-rs/and_then_closure.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/and_then_closure-fail.rs rename to kmir/src/tests/integration/data/prove-rs/and_then_closure.rs diff --git a/kmir/src/tests/integration/data/prove-rs/closure_access_struct-fail.rs b/kmir/src/tests/integration/data/prove-rs/closure_access_struct.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/closure_access_struct-fail.rs rename to kmir/src/tests/integration/data/prove-rs/closure_access_struct.rs diff --git a/kmir/src/tests/integration/data/prove-rs/closure_fnonce_tuple_arg.rs b/kmir/src/tests/integration/data/prove-rs/closure_fnonce_tuple_arg.rs new file mode 100644 index 000000000..18cfb9c22 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/closure_fnonce_tuple_arg.rs @@ -0,0 +1,8 @@ +fn apply u8>(f: F, a: u8, b: u8) -> u8 { + f(a, b) +} + +fn main() { + let result = apply(|x, y| x + y, 10, 32); + assert_eq!(result, 42); +} diff --git a/kmir/src/tests/integration/data/prove-rs/show/and_then_closure-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/and_then_closure-fail.main.expected deleted file mode 100644 index a6b62b249..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/and_then_closure-fail.main.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (142 steps) -└─ 3 (stuck, leaf) - #traverseProjection ( toLocal ( 2 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( - span: 157 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected deleted file mode 100644 index 8a1aff14b..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (196 steps) -└─ 3 (stuck, leaf) - #traverseProjection ( toLocal ( 2 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( - span: 125 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected deleted file mode 100644 index ce7aaeddb..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (102 steps) -└─ 3 (stuck, leaf) - #traverseProjection ( toLocal ( 2 ) , thunk ( #decodeConstant ( constantKindAllo - span: 153 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed-fail.rs b/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed-fail.rs rename to kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed.rs diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 8b1def7f8..5f36b155d 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -54,7 +54,6 @@ 'assume-cheatcode-conflict-fail', 'raw-ptr-cast-fail', 'transmute-u8-to-enum-fail', - 'transmute-u8-to-enum-changed-discriminant-signed-fail', 'assert-inhabited-fail', 'iterator-simple', 'unions-fail', @@ -63,8 +62,6 @@ 'test_offset_from-fail', 'ref-ptr-cast-elem-fail', 'ref-ptr-cast-elem-offset-fail', - 'and_then_closure-fail', - 'closure_access_struct-fail', ]