Skip to content

Commit 57345df

Browse files
dkcummingdkcumming
authored
assert_inhabited intrinsic support (#851)
The [assert_inhabited](https://doc.rust-lang.org/std/intrinsics/fn.assert_inhabited.html) intrinsic will (possibly) panic if a type in uninhabited (cannot be instantiated). E.g. ```rust assert_inhabited<!>(); // panics (probably) assert_inhabited<u8>(); // does nothing ``` Despite being an `assert`, panicking is not guaranteed and is dependent on the target and code generation - it is sound to perform a NO OP. Since calling the intrinsic comes from a `TerminatorKind::Call`, there must be a `BasicBlock` to go to after the call. However we observe that for `assert_inhabited<!>()` the execution continues to `noBasicBlockIdx` (which would get stuck). The semantics looks for this case and converts to `#AssertInhabitedFailure`, and otherwise performs a `NO OP`.
1 parent 9127004 commit 57345df

File tree

16 files changed

+94
-19
lines changed

16 files changed

+94
-19
lines changed

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

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,29 @@ before it's used. They have no effect on program semantics, and are implemented
5353
rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_instruction")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
5454
```
5555

56+
#### Assert Inhabited (`std::intrinsics::assert_inhabited`)
57+
58+
The `assert_inhabited` instrinsic asserts that a type is "inhabited" (able to be instantiated). Types such as
59+
`Never` (`!`) cannot be instantiated and are uninhabited types. The target / codegen decides how to handle this
60+
intrinsic, it is not required to panic if the type is not inhabited, it could also perform a NO OP. We have witnessed
61+
in the case that there is an uninhabited type that the following basic block is `noBasicBlockIdx`, and so we
62+
error with `#AssertInhabitedFailure` if we see that following the intrinsic. Otherwise, we perform a NO OP.
63+
64+
```k
65+
syntax MIRError ::= "AssertInhabitedFailure"
66+
rule <k> #execIntrinsic(IntrinsicFunction(symbol("assert_inhabited")), .Operands, _DEST)
67+
~> #continueAt(noBasicBlockIdx)
68+
=> AssertInhabitedFailure
69+
...
70+
</k>
71+
72+
rule <k> #execIntrinsic(IntrinsicFunction(symbol("assert_inhabited")), .Operands, _DEST)
73+
=> .K
74+
...
75+
</k>
76+
[owise]
77+
```
78+
5679
#### Raw Eq (`std::intrinsics::raw_eq`)
5780

5881
The `raw_eq` intrinsic performs byte-by-byte equality comparison of the memory contents pointed to by two references.

‎kmir/src/tests/integration/data/prove-rs/assert-inhabited-fail.rs‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
#![feature(core_intrinsics)]
2+
#![feature(never_type)]
3+
use std::intrinsics::assert_inhabited;
4+
5+
fn main() {
6+
std::hint::black_box(
7+
assert_inhabited::<!>() // Up to compiler/CodegenBackend to panic or NOOP
8+
);
9+
}

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,16 @@
11
#![feature(core_intrinsics)]
2-
use std::intrinsics;
2+
use std::intrinsics::{self, assert_inhabited};
33

44
fn main() {
55
intrinsics::cold_path();
66
let b = true;
77
intrinsics::likely(b);
88
intrinsics::unlikely(b);
99
prefetch();
10+
assert_inhabited::<i32>(); // Up to compiler/CodegenBackend to panic or NOOP
11+
std::hint::black_box(
12+
assert_inhabited::<()>() // Trying to stop being optimised away
13+
);
1014
}
1115

1216
fn prefetch() {

‎kmir/src/tests/integration/data/prove-rs/iterator-simple-fail.rs‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
fn main() {
2+
let arr = [1];
3+
4+
for elem in arr {
5+
assert!(elem != 0);
6+
}
7+
}

‎kmir/src/tests/integration/data/prove-rs/show/assert-inhabited-fail.main.expected‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
2+
┌─ 1 (root, init)
3+
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ span: 0
5+
│
6+
│ (8 steps)
7+
└─ 3 (stuck, leaf)
8+
#ProgramError ( AssertInhabitedFailure ) ~> .K
9+
function: main
10+
11+
12+
┌─ 2 (root, leaf, target, terminal)
13+
│ #EndProgram ~> .K
14+
15+

‎kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
2+
┌─ 1 (root, init)
3+
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ span: 0
5+
│
6+
│ (487 steps)
7+
└─ 3 (stuck, leaf)
8+
#traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place ( ..
9+
span: 219
10+
11+
12+
┌─ 2 (root, leaf, target, terminal)
13+
│ #EndProgram ~> .K
14+
15+

‎kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
<kmir>
22
<k>
3-
#execIntrinsic ( IntrinsicFunction ( symbol ( "assert_inhabited" ) ) , .Operands , place (... local: local ( 23 ) , projection: .ProjectionElems ) ) ~> #continueAt ( someBasicBlockIdx ( basicBlockIdx ( 8 ) ) ) ~> .K
3+
#traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
44
</k>
55
<retVal>
66
noReturn
@@ -57,7 +57,7 @@
5757
ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
5858
ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
5959
ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
60-
ListItem ( newLocal ( ty ( 54 ) , mutabilityMut ) )
60+
ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
6161
ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
6262
ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
6363
</locals>

‎kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
<kmir>
22
<k>
3-
#execIntrinsic ( IntrinsicFunction ( symbol ( "assert_inhabited" ) ) , .Operands , place (... local: local ( 23 ) , projection: .ProjectionElems ) ) ~> #continueAt ( someBasicBlockIdx ( basicBlockIdx ( 8 ) ) ) ~> .K
3+
#traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
44
</k>
55
<retVal>
66
noReturn
@@ -57,7 +57,7 @@
5757
ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
5858
ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
5959
ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
60-
ListItem ( newLocal ( ty ( 54 ) , mutabilityMut ) )
60+
ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
6161
ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
6262
ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
6363
</locals>

‎kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
<kmir>
22
<k>
3-
#execIntrinsic ( IntrinsicFunction ( symbol ( "assert_inhabited" ) ) , .Operands , place (... local: local ( 23 ) , projection: .ProjectionElems ) ) ~> #continueAt ( someBasicBlockIdx ( basicBlockIdx ( 8 ) ) ) ~> .K
3+
#traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
44
</k>
55
<retVal>
66
noReturn
@@ -57,7 +57,7 @@
5757
ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
5858
ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
5959
ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
60-
ListItem ( newLocal ( ty ( 54 ) , mutabilityMut ) )
60+
ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
6161
ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
6262
ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
6363
</locals>

‎kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
<kmir>
22
<k>
3-
#execIntrinsic ( IntrinsicFunction ( symbol ( "assert_inhabited" ) ) , .Operands , place (... local: local ( 23 ) , projection: .ProjectionElems ) ) ~> #continueAt ( someBasicBlockIdx ( basicBlockIdx ( 8 ) ) ) ~> .K
3+
#traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) ) statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) ) statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) ) .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ) .Operands ) ) , span: span ( 301 ) ) statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
44
</k>
55
<retVal>
66
noReturn
@@ -57,7 +57,7 @@
5757
ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
5858
ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
5959
ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
60-
ListItem ( newLocal ( ty ( 54 ) , mutabilityMut ) )
60+
ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
6161
ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
6262
ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) ) .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
6363
</locals>

0 commit comments

Comments
 (0)