Skip to content

Commit 6a052ab

Browse files
sskeirikrv-auditor
sskeirik
and
rv-auditor
authored
Fixup circular imports and typos (#347)
* Refactor: fixup import chains to avoid circularities * Cleanup: fix token conversion functions * remove mir-place import * Set Version: 0.2.45 --------- Co-authored-by: devops <devops@runtimeverification.com>
1 parent b215e3f commit 6a052ab

File tree

12 files changed

+163
-170
lines changed

12 files changed

+163
-170
lines changed

‎kmir/k-src/mir-basicblock.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,4 +13,4 @@ module MIR-BASICBLOCK-SYNTAX
1313
syntax BasicBlockBody ::= "{" Statements Terminator ";" "}"
1414
syntax BasicBlockList ::= List {BasicBlock, ""}
1515
endmodule
16-
```
16+
```

‎kmir/k-src/mir-rvalue-syntax.md‎

Lines changed: 146 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,146 @@
1+
```k
2+
requires "mir-operand.md"
3+
```
4+
5+
Syntax of rvalues
6+
-----------------
7+
8+
Rvalues are expression that appear on a right-hand-side of an assignment statement.
9+
10+
```k
11+
module MIR-RVALUE-SYNTAX
12+
imports BOOL
13+
imports UNSIGNED-INT-SYNTAX
14+
imports MIR-TYPE-SYNTAX
15+
imports MIR-OPERAND-SYNTAX
16+
```
17+
18+
### [`RValue`](https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.Rvalue.html)
19+
20+
The various kinds of rvalues that can appear in MIR.
21+
22+
```k
23+
syntax RValue ::= Use
24+
| Repeat
25+
| Ref
26+
// | ThreadLocalRef
27+
| AddressOf
28+
| Len
29+
| Cast
30+
| NullaryOp
31+
| UnaryOp
32+
| BinaryOp
33+
| Discriminant
34+
| Aggregate
35+
| ShallowInitBox
36+
| CopyForDeref
37+
38+
syntax Use ::= Operand
39+
40+
syntax Repeat ::= "[" Operand ";" Constant "]"
41+
| "[" Operand ";" RustExpression "]" [avoid]
42+
syntax Ref // TODO: define
43+
44+
// this seems to be responsible for function pointer assignmetn, e.g. `_1 = fn_name`
45+
// syntax ThreadLocalRef ::= PathExpression
46+
47+
syntax AddressOf ::= "&" PtrModifiers Place
48+
49+
syntax Len ::= "Len" "(" Place ")"
50+
51+
// TODO: this needs additional productions
52+
syntax Cast ::= Operand "as" Type [prefer]
53+
| Operand "as" Type "(" PointerCastArg ")" [prefer]
54+
| PathExpression "as" Type
55+
| PathExpression "as" Type "(" PointerCastArg ")"
56+
57+
syntax PointerCastArg ::= "Pointer" "(" PointerCast ")"
58+
syntax PointerCast ::= "ReifyFnPointer"
59+
| "UnsafeFnPointer"
60+
| "ClosureFnPointer" "(" Unsafety ")"
61+
| "MutToConstPointer"
62+
| "ArrayToPointer"
63+
| "Unsize"
64+
65+
syntax Unsafety ::= "Unsafe" | "Normal"
66+
67+
syntax NullaryOp ::= NullaryOpName "(" Type ")"
68+
syntax NullaryOpName ::= "SizeOf" [token]
69+
| "AlignOf" [token]
70+
71+
syntax UnaryOp ::= UnaryOpName "(" Operand ")"
72+
syntax UnaryOpName ::= "Not" [token]
73+
| "Neg" [token]
74+
75+
syntax BinaryOp ::= BinaryOpName "(" Operand "," Operand ")"
76+
syntax BinaryOpName ::= "Add" [token]
77+
| "Sub" [token]
78+
| "Mul" [token]
79+
| "Div" [token]
80+
| "Rem" [token]
81+
| "BitXor" [token]
82+
| "BitAnd" [token]
83+
| "BitOr" [token]
84+
| "Shl" [token]
85+
| "Shr" [token]
86+
| "Eq" [token]
87+
| "Lt" [token]
88+
| "Le" [token]
89+
| "Ne" [token]
90+
| "Ge" [token]
91+
| "Gt" [token]
92+
| "Offset" [token]
93+
94+
syntax Discriminant ::= "discriminant" "(" Place ")"
95+
96+
syntax CopyForDeref ::= "deref_copy" NonTerminalPlace
97+
98+
syntax Aggregate ::= Array
99+
| Tuple
100+
| Adt
101+
| Closure
102+
| Generator
103+
104+
syntax Array ::= "[" "]"
105+
| "[" Operand "]"
106+
| "[" Operand "," OperandList "]"
107+
108+
syntax Tuple ::= "(" ")"
109+
| "(" Operand "," OperandList ")"
110+
111+
syntax Adt ::= StructConstructor
112+
| EnumConstructor
113+
114+
syntax StructConstructor ::= Type "{" AdtFieldList "}"
115+
// | TypePath "(" OperandList ")" // compiletest-rs/ui/traits/copy-requires-self-wf.mir LINE 17
116+
117+
// `AssertKind` `Eq`, `Ne` conflict with BinaryOp names https://github.com/rust-lang/rust/blob/f562931178ff103f23b9e9a10dc0deb38e0d064f/library/core/src/panicking.rs#L259-L263
118+
syntax EnumConstructor ::= Identifier
119+
| Identifier "(" OperandList ")"
120+
| PathExpression "::" Identifier [avoid]
121+
| PathExpression "::" "Eq"
122+
| PathExpression "::" "Ne"
123+
// | PathExpression "::" "Match" // Match isn't conflicting at the moment but might later
124+
| PathExpression "::" Identifier "(" OperandList ")"
125+
126+
syntax AdtField ::= AdtFieldName ":" Operand
127+
syntax AdtFieldList ::= List{AdtField, ","}
128+
129+
syntax Closure ::= "[" "closure" "@" FilePosition "]"
130+
131+
syntax Generator ::= "[" "generator" "@" FilePosition "(" "#" Int ")" "]"
132+
| "[" "generator" "@" FilePosition "(" "#" Int ")" "]" "{" AdtFieldList "}"
133+
134+
syntax ShallowInitBox ::= "ShallowInitBox" "(" Operand "," Type ")"
135+
136+
syntax OperandList ::= List{Operand, ","}
137+
138+
syntax PtrModifiers ::= "" | "mut" | "raw" "mut" | "raw" "const"
139+
140+
syntax RValue ::= #unwrap(Operand)
141+
```
142+
143+
```k
144+
endmodule
145+
```
146+

‎kmir/k-src/mir-rvalue.md‎

Lines changed: 1 addition & 145 deletions
Original file line numberDiff line numberDiff line change
@@ -1,149 +1,5 @@
11
```k
2-
requires "mir-syntax.md"
32
requires "mir-configuration.md"
4-
requires "mir-operand.md"
5-
```
6-
7-
Syntax of rvalues
8-
-----------------
9-
10-
Rvalues are expression that appear on a right-hand-side of an assignment statement.
11-
12-
```k
13-
module MIR-RVALUE-SYNTAX
14-
imports BOOL
15-
imports UNSIGNED-INT-SYNTAX
16-
imports MIR-TYPE-SYNTAX
17-
imports MIR-OPERAND-SYNTAX
18-
```
19-
20-
### [`RValue`](https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.Rvalue.html)
21-
22-
The various kinds of rvalues that can appear in MIR.
23-
24-
```k
25-
syntax RValue ::= Use
26-
| Repeat
27-
| Ref
28-
// | ThreadLocalRef
29-
| AddressOf
30-
| Len
31-
| Cast
32-
| NullaryOp
33-
| UnaryOp
34-
| BinaryOp
35-
| Discriminant
36-
| Aggregate
37-
| ShallowInitBox
38-
| CopyForDeref
39-
40-
syntax Use ::= Operand
41-
42-
syntax Repeat ::= "[" Operand ";" Constant "]"
43-
| "[" Operand ";" RustExpression "]" [avoid]
44-
syntax Ref // TODO: define
45-
46-
// this seems to be responsible for function pointer assignmetn, e.g. `_1 = fn_name`
47-
// syntax ThreadLocalRef ::= PathExpression
48-
49-
syntax AddressOf ::= "&" PtrModifiers Place
50-
51-
syntax Len ::= "Len" "(" Place ")"
52-
53-
// TODO: this needs additional productions
54-
syntax Cast ::= Operand "as" Type [prefer]
55-
| Operand "as" Type "(" PointerCastArg ")" [prefer]
56-
| PathExpression "as" Type
57-
| PathExpression "as" Type "(" PointerCastArg ")"
58-
59-
syntax PointerCastArg ::= "Pointer" "(" PointerCast ")"
60-
syntax PointerCast ::= "ReifyFnPointer"
61-
| "UnsafeFnPointer"
62-
| "ClosureFnPointer" "(" Unsafety ")"
63-
| "MutToConstPointer"
64-
| "ArrayToPointer"
65-
| "Unsize"
66-
67-
syntax Unsafety ::= "Unsafe" | "Normal"
68-
69-
syntax NullaryOp ::= NullaryOpName "(" Type ")"
70-
syntax NullaryOpName ::= "SizeOf" [token]
71-
| "AlignOf" [token]
72-
73-
syntax UnaryOp ::= UnaryOpName "(" Operand ")"
74-
syntax UnaryOpName ::= "Not" [token]
75-
| "Neg" [token]
76-
77-
syntax BinaryOp ::= BinaryOpName "(" Operand "," Operand ")"
78-
syntax BinaryOpName ::= "Add" [token]
79-
| "Sub" [token]
80-
| "Mul" [token]
81-
| "Div" [token]
82-
| "Rem" [token]
83-
| "BitXor" [token]
84-
| "BitAnd" [token]
85-
| "BitOr" [token]
86-
| "Shl" [token]
87-
| "Shr" [token]
88-
| "Eq" [token]
89-
| "Lt" [token]
90-
| "Le" [token]
91-
| "Ne" [token]
92-
| "Ge" [token]
93-
| "Gt" [token]
94-
| "Offset" [token]
95-
96-
syntax Discriminant ::= "discriminant" "(" Place ")"
97-
98-
syntax CopyForDeref ::= "deref_copy" NonTerminalPlace
99-
100-
syntax Aggregate ::= Array
101-
| Tuple
102-
| Adt
103-
| Closure
104-
| Generator
105-
106-
syntax Array ::= "[" "]"
107-
| "[" Operand "]"
108-
| "[" Operand "," OperandList "]"
109-
110-
syntax Tuple ::= "(" ")"
111-
| "(" Operand "," OperandList ")"
112-
113-
syntax Adt ::= StructConstructor
114-
| EnumConstructor
115-
116-
syntax StructConstructor ::= Type "{" AdtFieldList "}"
117-
// | TypePath "(" OperandList ")" // compiletest-rs/ui/traits/copy-requires-self-wf.mir LINE 17
118-
119-
// `AssertKind` `Eq`, `Ne` conflict with BinaryOp names https://github.com/rust-lang/rust/blob/f562931178ff103f23b9e9a10dc0deb38e0d064f/library/core/src/panicking.rs#L259-L263
120-
syntax EnumConstructor ::= Identifier
121-
| Identifier "(" OperandList ")"
122-
| PathExpression "::" Identifier [avoid]
123-
| PathExpression "::" "Eq"
124-
| PathExpression "::" "Ne"
125-
// | PathExpression "::" "Match" // Match isn't conflicting at the moment but might later
126-
| PathExpression "::" Identifier "(" OperandList ")"
127-
128-
syntax AdtField ::= AdtFieldName ":" Operand
129-
syntax AdtFieldList ::= List{AdtField, ","}
130-
131-
syntax Closure ::= "[" "closure" "@" FilePosition "]"
132-
133-
syntax Generator ::= "[" "generator" "@" FilePosition "(" "#" Int ")" "]"
134-
| "[" "generator" "@" FilePosition "(" "#" Int ")" "]" "{" AdtFieldList "}"
135-
136-
syntax ShallowInitBox ::= "ShallowInitBox" "(" Operand "," Type ")"
137-
138-
syntax OperandList ::= List{Operand, ","}
139-
140-
syntax PtrModifiers ::= "" | "mut" | "raw" "mut" | "raw" "const"
141-
142-
syntax RValue ::= #unwrap(Operand)
143-
```
144-
145-
```k
146-
endmodule
1473
```
1484

1495
Evaluation of rvalues
@@ -242,7 +98,7 @@ Evaluate a syntactic `RValue` into a semantics `RValueResult`. Inspired by [eval
24298
//-------------------------------------------------------------
24399
rule evalConstantValue(VALUE:UnsignedLiteral) => UnsignedLiteral2Int(VALUE)
244100
rule evalConstantValue(VALUE:SignedLiteral) => SignedLiteral2Int(VALUE)
245-
rule evalConstantValue(VALUE:StringLiteral) => StringLitertal2String(VALUE)
101+
rule evalConstantValue(VALUE:StringLiteral) => StringLiteral2String(VALUE)
246102
rule evalConstantValue(( )) => Unit
247103
rule evalConstantValue(VALUE:Bool) => VALUE
248104
rule evalConstantValue(VALUE:ConstEnumConstructor) => evalPrimitiveBound(VALUE)

‎kmir/k-src/mir-statement.md‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
```k
2-
requires "mir-rvalue.md"
3-
requires "mir-place.md"
2+
requires "mir-rvalue-syntax.md"
43
```
54
### [Statements](https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.StatementKind.html) and [Terminators](https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.TerminatorKind.html)
65

‎kmir/k-src/mir-syntax.md‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,4 @@
11
```k
2-
requires "mir-types.md"
3-
requires "mir-place.md"
4-
requires "mir-rvalue.md"
52
requires "mir-basicblock.md"
63
```
74

‎kmir/k-src/mir-terminator.md‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
```k
2-
requires "mir-types.md"
3-
requires "mir-rvalue.md"
2+
requires "mir-rvalue-syntax.md"
43
requires "mir-assert.md"
54
```
65

0 commit comments

Comments
 (0)