Skip to content

Commit 1258928

Browse files
jbertholdrv-auditor
jberthold
and
rv-auditor
authored
write-up of MIR semantics (#448)
Co-authored-by: devops <[email protected]>
1 parent 01a575c commit 1258928

File tree

4 files changed

+224
-3
lines changed

4 files changed

+224
-3
lines changed

Diff for: ‎docs/semantics-of-mir.md

+221
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,221 @@
1+
# Top-Down Description of the Semantics of MIR Constructs
2+
3+
## Executing a `Body` (function call)
4+
Every _rust function_ gets compiled into a `Body`. A function body is
5+
broken up into a number of _basic blocks_ (portions of code with
6+
straight-line control flow).
7+
8+
A function _call_ is executed by setting up the arguments and local
9+
variables, and then executing its body. After the function call, the
10+
return value (result) needs to be written back to the _destination_
11+
given in the call, and execution continues with the _target_ basic
12+
block. An _unwind_ property indicates how to proceed when the call
13+
unwinds (i.e., panics).
14+
15+
The _args_, _destination_, _unwind_, and (optional!) _target_ are
16+
supplied by either the `Terminator` kind `Call` (within a program), or
17+
unnecessary (when calling `main`).
18+
19+
The execution of a body consists of
20+
* setting up a stack frame for this call
21+
- with reserved space for all _locals_: return value, arg.s, and local
22+
variables
23+
- with the (caller's) function address to return to (as well as
24+
_destination_, _target_, _unwind_)
25+
- with all _basic blocks_ of the function body
26+
* and then executing block 0 of the _basic blocks_
27+
28+
## Blocks and Control Flow
29+
30+
Executing a block means to execute its contained _statements_ in
31+
order, followed by the _terminator_ action.
32+
33+
### Execution of Terminators (Control Flow)
34+
35+
The _terminator_ can be one of a variety of terminator kinds,
36+
indicating different continuations to the basic block.
37+
38+
Some of these `TerminatorKind`s are only relevant for MIR
39+
transformations while elaborating higher-level operations and
40+
checking, others directly affect the execution control flow.
41+
42+
43+
| Kind | Data | | Action |
44+
|-----------------|-------------|---------------------------|-------------------------------------------|
45+
| Goto | block | | continue with given block |
46+
|-----------------|-------------|---------------------------|-------------------------------------------|
47+
| SwitchInt | discr | value to switch over | evaluate value and follow |
48+
| | targets | alternative continuations | the selected alternative |
49+
|-----------------|-------------|---------------------------|-------------------------------------------|
50+
| ?UnwindResume | | | Continue unwinding after "landing pad"(?) |
51+
|-----------------|-------------|---------------------------|-------------------------------------------|
52+
| UnwindTerminate | Reason | | Terminate after "landing pad"(?) |
53+
|-----------------|-------------|---------------------------|-------------------------------------------|
54+
| Return | | assign _0 to destination | continue with _target_ from call |
55+
| | | | and maybe more, "exact semantics unclear" |
56+
|-----------------|-------------|---------------------------|-------------------------------------------|
57+
| Unreachable | | cannot be reached | undefined behaviour if executed |
58+
|-----------------|-------------|---------------------------|-------------------------------------------|
59+
| Call | func | function address to call | set up stack frame for, load, and call |
60+
| | args | arguments | given function |
61+
| | destination | to store returned value | (will store return value at _destination_ |
62+
| | target | next block to go to | and proceed with _target_ block) |
63+
| | unwind | | |
64+
|-----------------|-------------|---------------------------|-------------------------------------------|
65+
| TailCall | func | function address to call | special version of `Call` for tail calls |
66+
| | args | arguments | replaces the stack frame instead of an |
67+
| | | | duplicating destination and target |
68+
|-----------------|-------------|---------------------------|-------------------------------------------|
69+
| Assert | cond | operand to check (bool) | evaluates _cond_, compares to _expected_ |
70+
| | expected | expected result of check | if equal, continue with _target_ |
71+
| | msg | msg for panic! call | otherwise `panic!` with _msg_ |
72+
| | target | continuation if OK | |
73+
| | unwind | | |
74+
|-----------------|-------------|---------------------------|-------------------------------------------|
75+
| InlineAsm | (for asm) | | executes inline ASM and returns |
76+
| | targets | next blocks, default 1st | to the _targets[1]_ block, UNCLEAR |
77+
|-----------------|-------------|---------------------------|-------------------------------------------|
78+
| **Irrelevant** | | | |
79+
|-----------------|-------------|---------------------------|-------------------------------------------|
80+
| Drop | place | memory to drop | UNCLEAR: noop after "drop elaboration" |
81+
| | target | next block to go to | |
82+
| | unwind | | |
83+
| | replace | | |
84+
|-----------------|-------------|---------------------------|-------------------------------------------|
85+
| Yield | ... | for coroutine blocks only | return a value to caller, resume from |
86+
| | | | given block when called again. |
87+
|-----------------|-------------|---------------------------|-------------------------------------------|
88+
| CoroutineDrop | ... | ? | |
89+
|-----------------|-------------|---------------------------|-------------------------------------------|
90+
| FalseEdge | real target | for borrow checker only | behaves like `Goto` with _real target_ |
91+
| FalseUnwind | real target | for borrow checker only | behaves like `Goto` with _real target_ |
92+
|-----------------|-------------|---------------------------|-------------------------------------------|
93+
94+
### Statements (within a Basic Block)
95+
96+
The list of statements in a basic block is executed sequentially. Each
97+
`Statement` has a certain `StatementKind`. Some `StatementKind`s won't
98+
appear in the MIR that gets executed by the semantics, others do.
99+
100+
| Kind | Data | Action |
101+
|------------------|-----------------------------------------|------------------------------------------|
102+
| Assign | (Place, RValue) | evaluates place and rvalue, assigns |
103+
| ?SetDiscriminant | place, variant_index | write variant discriminant to place |
104+
|------------------|-----------------------------------------|------------------------------------------|
105+
| Deinit | (Place) | writes `uninit` to the place |
106+
| StorageLive | (Local) | allocates memory for the local |
107+
| StorageDead | (Local) | deallocates memory for the local |
108+
|------------------|-----------------------------------------|------------------------------------------|
109+
| ?Retag | (RetagKind, Place) | only for `miri`, puts fresh tag on place |
110+
| Intrinsic | (NonDivergingIntrinsic) | optimised call to intrinsic, saves block |
111+
| PlaceMention | (Place) | (technical, records place access) |
112+
|------------------|-----------------------------------------|------------------------------------------|
113+
| FakeRead | (FakeReadCause, Place) | disallowed after drop elaboration |
114+
| AscribeUserType | ((Place, UserTypeProjection), Variance) | relates types in assign, NOOP at runtime |
115+
| Coverage | (CoverageKind) | CostCtr indication for coverage counters |
116+
| ConstEvalCounter | | counts const eval. cost, NOOP otherwise |
117+
| Nop | | NOOP |
118+
119+
The [code of the constant
120+
interpreter](https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_const_eval/src/interpret/step.rs#L57-L291)
121+
demonstrates the semantics outlined in the table further. For
122+
instance, `Retag` and `PlaceMention` evaluate the given `Place`
123+
(`FakeRead` does not!).
124+
125+
## Memory
126+
127+
Some of the above constructs (statements `Storage{Live,Dead}` and
128+
`Deinit`, terminators `Drop`) are only relevant if memory allocation
129+
is part of the semantic model. In the KMIR semantics (so far), memory
130+
is intended to be modeled at a more abstract level.
131+
132+
The `Assign` statement is where memory is accessed for reading or
133+
writing. An `RValue` is computed, potentially reading some arguments,
134+
and then written to a `Place`.
135+
136+
### `Place`s
137+
A `Place` is a `Local` variable (actually just its index), and
138+
potentially a vector of `ProjectionElem`ents.
139+
- `Deref`erencing references or pointers (or `Box`es allocated in the
140+
heap)
141+
- `Field` access in struct.s and tuples
142+
- `Index`ing into arrays (from front or back)
143+
- Casting values (`OpaqueCast` or `Downcast` - variant narrowing)
144+
145+
146+
### `RValue`s
147+
148+
An `RValue` is an operation that produces a value which can then be assigned to a `Place`.
149+
150+
| RValue | Arguments | Action |
151+
|----------------|-------------------------------------------------|--------------------------------------|
152+
| Use | Operand | use (i.e., copy) operand unmodified |
153+
| Repeat | Operand, Const | create array [Operand;Const] |
154+
| Ref | Region, BorrowKind, Place | create reference to place |
155+
| ThreadLocalRef | DefId | thread-local reference (?) |
156+
| AddressOf | Mutability, Place | creates pointer to place |
157+
| Len | Place | array or slice size |
158+
| Cast | CastKind, Operand, Ty | different kinds of type casts |
159+
|----------------|-------------------------------------------------|--------------------------------------|
160+
| BinaryOp | BinOp, Box<(Operand, Operand)> | different fixed operations |
161+
| NullaryOp | NullOp, Ty | on ints, bool, floats |
162+
| UnaryOp | UnOp, Operand | (see below) |
163+
|----------------|-------------------------------------------------|--------------------------------------|
164+
| Discriminant | Place | discriminant (of sums types) (?) |
165+
| Aggregate | Box<AggregateKind>, IndexVec<FieldIdx, Operand> | disallowed after lowering. DF helper |
166+
| ShallowInitBox | Operand, Ty | ? |
167+
| CopyForDeref | Place | use (copy) contents of `Place` |
168+
169+
See https://github.com/runtimeverification/rust/blob/9131ddf5faba14fab225a7bf8ef5ee5dafe12e3b/compiler/rustc_const_eval/src/interpret/step.rs#L139-L291
170+
171+
### Operations
172+
173+
Operations are described cursorily in the `RValue` descriptions and in
174+
the `BinOp` and `UnaryOp` descriptions. Their exact semantics,
175+
however, must sometimes be retrieved from the compiler code.
176+
177+
The `Operand`s of operations are `Copy` or `Move` from `Place`s, or
178+
`ConstOperand`s allocated in a `Box`.
179+
Both `Copy` and `Move` _load_ the operand from a `Place`.
180+
181+
#### Nullary Operations `NullOp`
182+
183+
| SizeOf | size of a type |
184+
| AlignOf, | minimum alignment of a type |
185+
| OffsetOf(&'tcx List<(VariantIdx, FieldIdx)>), | offset of a field in a struct |
186+
| UbChecks | whether upper-bound checks should be performed |
187+
188+
#### Unary Operations `UnOp`
189+
190+
| Not | logical inversion |
191+
| Neg | arithmetic inversion |
192+
| PtrMetadata | get pointer metadata. Only allowed in MIR:Runtime phase (?) |
193+
194+
#### Binary Operations `BinOp`, operands A and B
195+
196+
| Add | (A + B truncated, bool overflow flag) | int, float | |
197+
| AddUnchecked | A + B | int, float | must have been wrapped in `unsafe` |
198+
| AddWithOverflow | (A + B truncated, bool overflow flag) | int, float | not present in stable MIR |
199+
| Sub | (A - B truncated, bool underflow flag) | int, float | |
200+
| SubUnchecked | A - B | int, float | |
201+
| SubWithOverflow | (A - B truncated, bool underflow flag) | int, float | not present in stable MIR |
202+
| Mul | (A * B truncated, bool overflow flag) | int, float | |
203+
| MulUnchecked | A * B | int, float | |
204+
| MulWithOverflow | (A * B truncated, bool overflow flag) | int, float | not present in stable MIR |
205+
| Div | A / B or A `div` B | int, float | |
206+
| Rem | A `mod` B, rounding towards zero | int | |
207+
| BitXor | A `xor` B | int | |
208+
| BitAnd | A & B | int | |
209+
| BitOr | A \| B | int | |
210+
| Shl | (A << B truncated, bool overflow flag) | int | |
211+
| ShlUnchecked | A << B | int | |
212+
| Shr | (A >> B truncated? | int | |
213+
| ShrUnchecked | A >> B | int | |
214+
| Eq | A == B | int,float,bool | |
215+
| Lt | A < B | int,float | |
216+
| Le | A <= B | int,float | |
217+
| Ne | A /= B | int,float | |
218+
| Ge | A >= B | int,float | |
219+
| Gt | A > B | int,float | |
220+
| Cmp | cmp A B (LT -1, EQ 0, GT 1) | int,float | |
221+
| Offset | offset from a pointer | pointers | |

Diff for: ‎kmir/pyproject.toml

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
44

55
[tool.poetry]
66
name = "kmir"
7-
version = "0.3.71"
7+
version = "0.3.72"
88
description = ""
99
authors = [
1010
"Runtime Verification, Inc. <[email protected]>",

Diff for: ‎kmir/src/kmir/__init__.py

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
from typing import Final
22

3-
VERSION: Final = '0.3.71'
3+
VERSION: Final = '0.3.72'

Diff for: ‎package/version

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
0.3.71
1+
0.3.72

0 commit comments

Comments
 (0)