Skip to content

Commit c558fe6

Browse files
yanliu18yanliu18
committed
Alternative implementation of builtin function syntax
1 parent e0d53af commit c558fe6

File tree

4 files changed

+52
-182
lines changed

4 files changed

+52
-182
lines changed

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

Lines changed: 30 additions & 90 deletions
Original file line numberDiff line numberDiff line change
@@ -77,12 +77,33 @@ The various kinds of rvalues that can appear in MIR.
7777
7878
syntax Unsafety ::= "Unsafe" | "Normal"
7979
80-
syntax NullaryOp ::= Identifier "(" Type ")"
81-
82-
syntax UnaryOp ::= Identifier "(" Operand ")"
80+
syntax NullaryOp ::= NullaryOpName "(" Type ")"
81+
syntax NullaryOpName ::= "SizeOf" [token]
82+
| "AlignOf" [token]
8383
84-
syntax BinaryOp ::= Identifier "(" Operand "," Operand ")"
84+
syntax UnaryOp ::= UnaryOpName "(" Operand ")"
85+
syntax UnaryOpName ::= "Not" [token]
86+
| "Neg" [token]
8587
88+
syntax BinaryOp ::= BinaryOpName "(" Operand "," Operand ")"
89+
syntax BinaryOpName ::= "Add" [token]
90+
| "Sub" [token]
91+
| "Mul" [token]
92+
| "Div" [token]
93+
| "Rem" [token]
94+
| "BitXor" [token]
95+
| "BitAnd" [token]
96+
| "BitOr" [token]
97+
| "Shl" [token]
98+
| "Shr" [token]
99+
| "Eq" [token]
100+
| "Lt" [token]
101+
| "Le" [token]
102+
| "Ne" [token]
103+
| "Ge" [token]
104+
| "Gt" [token]
105+
| "Offset" [token]
106+
86107
syntax Discriminant ::= "discriminant" "(" Place ")"
87108
88109
syntax CopyForDeref ::= "deref_copy" NonTerminalPlace
@@ -176,93 +197,12 @@ TODO: these sorts may need refactoring to closer match the `rustc` implementatio
176197
endmodule
177198
```
178199

179-
### Build-in operations
180-
181-
```k
182-
module MIR-BUILTINS-SYNTAX
183-
imports BOOL
184-
imports STRING
185-
186-
syntax MirBuiltInToken ::= NullaryOpName
187-
| UnaryOpName
188-
| BinaryOpName
189-
| CheckedBinaryOpName
190-
191-
syntax MirBuiltInToken ::= String2MirBuiltInToken(MirBuiltInToken) [function, hook(STRING.token2string)]
192-
193-
syntax NullaryOpName ::= "SizeOf" [token]
194-
| "AlignOf" [token]
195-
196-
syntax UnaryOpName ::= String2UnaryOpName(String) [function, hook(STRING.string2token)]
197-
198-
syntax UnaryOpName ::= "Not" [token]
199-
| "Neg" [token]
200-
201-
syntax BinaryOpName ::= String2BinaryOpName(String) [function, hook(STRING.string2token)]
202-
203-
syntax BinaryOpName ::= "Add" [token]
204-
| "Sub" [token]
205-
| "Mul" [token]
206-
| "Div" [token]
207-
| "Rem" [token]
208-
| "BitXor" [token]
209-
| "BitAnd" [token]
210-
| "BitOr" [token]
211-
| "Shl" [token]
212-
| "Shr" [token]
213-
| "Eq" [token]
214-
| "Lt" [token]
215-
| "Le" [token]
216-
| "Ne" [token]
217-
| "Ge" [token]
218-
| "Gt" [token]
219-
| "Offset" [token]
220-
221-
syntax Bool ::= isUnOp(String) [function, total]
222-
//----------------------------------------------
223-
rule isUnOp(OP_NAME) => true
224-
requires OP_NAME ==String "Not"
225-
orBool OP_NAME ==String "Neg"
226-
rule isUnOp(_) => false [owise]
227-
228-
syntax Bool ::= isBinOp(String) [function, total]
229-
//-----------------------------------------------
230-
rule isBinOp(OP_NAME) => true
231-
requires OP_NAME ==String "Add"
232-
orBool OP_NAME ==String "Sub"
233-
orBool OP_NAME ==String "Mul"
234-
orBool OP_NAME ==String "Div"
235-
orBool OP_NAME ==String "Rem"
236-
orBool OP_NAME ==String "BitXor"
237-
orBool OP_NAME ==String "BitAnd"
238-
orBool OP_NAME ==String "BitOr"
239-
orBool OP_NAME ==String "Shl"
240-
orBool OP_NAME ==String "Shr"
241-
orBool OP_NAME ==String "Eq"
242-
orBool OP_NAME ==String "Lt"
243-
orBool OP_NAME ==String "Le"
244-
orBool OP_NAME ==String "Ne"
245-
orBool OP_NAME ==String "Ge"
246-
orBool OP_NAME ==String "Gt"
247-
orBool OP_NAME ==String "Offset"
248-
rule isBinOp(_) => false [owise]
249-
250-
syntax CheckedBinaryOpName ::= "CheckedAdd"
251-
| "CheckedSub"
252-
| "CheckedMul"
253-
| "CheckedShl"
254-
| "CheckedShr"
255-
256-
endmodule
257-
```
258-
259200
Evaluation of rvalues
260201
---------------------
261202

262203
```k
263204
module MIR-RVALUE
264205
imports MIR-RVALUE-SYNTAX
265-
imports MIR-BUILTINS-SYNTAX
266206
imports MIR-TYPES
267207
imports MIR-CONFIGURATION
268208
```
@@ -293,8 +233,8 @@ Evaluate a syntactic `RValue` into a semantics `RValueResult`. Inspired by [eval
293233
```k
294234
syntax MIRValue ::= evalUnaryOp(FunctionLikeKey, UnaryOp) [function]
295235
//------------------------------------------------------------------
296-
rule evalUnaryOp(FN_KEY, NAME:IdentifierToken (X:Operand)) =>
297-
evalUnaryOpImpl(FN_KEY, String2UnaryOpName(IdentifierToken2String(NAME)), X)
236+
rule evalUnaryOp(FN_KEY, NAME:UnaryOpName (X:Operand)) =>
237+
evalUnaryOpImpl(FN_KEY, NAME, X)
298238
299239
syntax MIRValue ::= evalUnaryOpImpl(FunctionLikeKey, UnaryOpName, Operand) [function]
300240
//-----------------------------------------------------------------------------------
@@ -307,8 +247,8 @@ Evaluate a syntactic `RValue` into a semantics `RValueResult`. Inspired by [eval
307247
```k
308248
syntax MIRValue ::= evalBinaryOp(FunctionLikeKey, BinaryOp) [function]
309249
//--------------------------------------------------------------------
310-
rule evalBinaryOp(FN_KEY, NAME:IdentifierToken (X:Operand, Y:Operand)) =>
311-
evalBinaryOpImpl(FN_KEY, String2BinaryOpName(IdentifierToken2String(NAME)), X, Y)
250+
rule evalBinaryOp(FN_KEY, NAME:BinaryOpName (X:Operand, Y:Operand)) =>
251+
evalBinaryOpImpl(FN_KEY, NAME, X, Y)
312252
313253
syntax MIRValue ::= evalBinaryOpImpl(FunctionLikeKey, BinaryOpName, Operand, Operand) [function]
314254
//-----------------------------------------------------------------------
@@ -328,7 +268,7 @@ Evaluate a syntactic `RValue` into a semantics `RValueResult`. Inspired by [eval
328268
rule evalBinaryOpImpl(FN_KEY, Ne, X, Y) => {evalOperand(FN_KEY, X)}:>Int =/=Int {evalOperand(FN_KEY, Y)}:>Int
329269
rule evalBinaryOpImpl(FN_KEY, Ge, X, Y) => {evalOperand(FN_KEY, X)}:>Int >=Int {evalOperand(FN_KEY, Y)}:>Int
330270
rule evalBinaryOpImpl(FN_KEY, Gt, X, Y) => {evalOperand(FN_KEY, X)}:>Int >Int {evalOperand(FN_KEY, Y)}:>Int
331-
// rule evalBinaryOpImpl("Offset", X, Y) => "not implemented"
271+
// rule evalBinaryOpImpl(FN_KEY, _, X, Y) => "not supported" [owise]
332272
```
333273

334274
### Constant evaluation.

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

Lines changed: 0 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -173,64 +173,3 @@ module MIR-PARSER-SYNTAX
173173
174174
endmodule
175175
```
176-
177-
MIR syntax disambiguation
178-
-------------------------
179-
180-
Some of MIR constructs are ambiguous as parsing time. The `MIR-AMBIGUITIES` module contains rewrite rules that disambiguate these constructs.
181-
These rules are applied at `Initialization` phase, see the `MIR` module in "mir.md" for more information on when these rules are used.
182-
183-
```k
184-
module MIR-AMBIGUITIES
185-
imports MIR-SYNTAX
186-
imports MIR-LEXER-SYNTAX
187-
imports MIR-BUILTINS-SYNTAX
188-
imports K-AMBIGUITIES
189-
```
190-
191-
```k
192-
syntax BasicBlockBody ::= disambiguateBasicBlockBody(BasicBlockBody) [function]
193-
//-----------------------------------------------------------------------------
194-
rule disambiguateBasicBlockBody({ STATEMENTS:Statements TERMINATOR:Terminator ; }:BasicBlockBody) =>
195-
({ disambiguateStatements(STATEMENTS) disambiguateTerminator(TERMINATOR) ; })
196-
197-
syntax Statements ::= disambiguateStatements(Statements) [function]
198-
//--------------------------------------------------------------------------
199-
rule disambiguateStatements(.Statements) => .Statements
200-
rule disambiguateStatements(X ; XS) => disambiguateStatement(X) ; disambiguateStatements(XS)
201-
202-
syntax StatementKind ::= disambiguateStatement(StatementKind) [function]
203-
//--------------------------------------------------------------
204-
rule disambiguateStatement((PLACE:Place = VALUE:RValue):Assign) => (PLACE:Place = disambiguateRValue(VALUE:RValue)):Assign
205-
rule disambiguateStatement(S) => S [owise]
206-
207-
syntax Terminator ::= disambiguateTerminator(Terminator) [function]
208-
//-----------------------------------------------------------------
209-
rule disambiguateTerminator(T) => T
210-
```
211-
212-
The actual disambiguation starts here: we need to distinguish certain rvalues:
213-
* enum constructors
214-
* primitive unary and binary operations
215-
216-
```k
217-
syntax RValue ::= disambiguateRValue(RValue) [function]
218-
//-----------------------------------------------------
219-
rule disambiguateRValue(
220-
amb((NAME:IdentifierToken (AGR_1:Operand, ARG_2:Operand, .OperandList))::EnumConstructor,
221-
(NAME:IdentifierToken (AGR_1:Operand, ARG_2:Operand))::BinaryOp
222-
)) =>
223-
(NAME::IdentifierToken (AGR_1:Operand, ARG_2:Operand))::BinaryOp
224-
requires isBinOp(IdentifierToken2String(NAME))
225-
rule disambiguateRValue(
226-
amb((NAME:IdentifierToken (AGR_1:Operand, .OperandList))::EnumConstructor,
227-
(NAME:IdentifierToken (AGR_1:Operand))::UnaryOp
228-
)) =>
229-
(NAME::IdentifierToken (AGR_1:Operand))::UnaryOp
230-
requires isUnOp(IdentifierToken2String(NAME))
231-
rule disambiguateRValue(X) => X [owise]
232-
```
233-
234-
```k
235-
endmodule
236-
```

‎kmir/k-src/mir.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ with the Haskell backend at the moment.
7474
module MIR-INITIALIZATION
7575
imports MIR-CONFIGURATION
7676
imports PANICS
77-
imports MIR-AMBIGUITIES
77+
//imports MIR-AMBIGUITIES
7878
```
7979

8080
### Function definition processing
@@ -273,7 +273,7 @@ This rule panics if it encounters a duplicate block.
273273
<basicBlocks>
274274
(.Bag => <basicBlock>
275275
<bbName> BBName2Int(NAME) </bbName>
276-
<bbBody> disambiguateBasicBlockBody(BODY) </bbBody>
276+
<bbBody> BODY</bbBody>
277277
</basicBlock>
278278
)
279279
...

‎kmir/src/tests/unit/add.mir‎

Lines changed: 20 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -1,55 +1,46 @@
11
// WARNING: This output format is intended for human consumers only
22
// and is subject to change without notice. Knock yourself out.
33
fn add() -> i32 {
4-
let mut _0: i32; // return place in scope 0 at add.rs:1:13: 1:16
5-
let _1: i32; // in scope 0 at add.rs:2:9: 2:10
4+
let mut _0: i32;
5+
let _1: i32;
66
scope 1 {
7-
debug x => _1; // in scope 1 at add.rs:2:9: 2:10
8-
let _2: i32; // in scope 1 at add.rs:3:9: 3:10
7+
debug x => _1;
8+
let _2: i32;
99
scope 2 {
10-
debug y => _2; // in scope 2 at add.rs:3:9: 3:10
10+
debug y => _2;
1111
}
1212
}
1313

1414
bb0: {
15-
_1 = const 1_i32; // scope 0 at add.rs:2:13: 2:14
16-
_2 = const 2_i32; // scope 1 at add.rs:3:13: 3:14
17-
_0 = const 3_i32; // scope 2 at add.rs:4:5: 4:10
18-
return; // scope 0 at add.rs:5:2: 5:2
15+
_1 = const 1_i32;
16+
_2 = const 2_i32;
17+
_0 = Add(_1, _2);
18+
return;
1919
}
2020
}
2121

2222
fn main() -> () {
23-
let mut _0: (); // return place in scope 0 at add.rs:7:15: 7:15
24-
let mut _1: bool; // in scope 0 at add.rs:8:5: 8:24
25-
let mut _2: bool; // in scope 0 at add.rs:8:13: 8:23
26-
let mut _3: i32; // in scope 0 at add.rs:8:13: 8:18
27-
let mut _4: !; // in scope 0 at add.rs:8:5: 8:24
23+
let mut _0: ();
24+
let mut _1: bool;
25+
let mut _2: bool;
26+
let mut _3: i32;
27+
let mut _4: !;
2828

2929
bb0: {
30-
_3 = add() -> bb1; // scope 0 at add.rs:8:13: 8:18
31-
// mir::Constant
32-
// + span: add.rs:8:13: 8:16
33-
// + literal: Const { ty: fn() -> i32 {add}, val: Value(<ZST>) }
30+
_3 = add() -> bb1;
3431
}
3532

3633
bb1: {
37-
_2 = Eq(move _3, const 3_i32); // scope 0 at add.rs:8:13: 8:23
38-
_1 = Not(move _2); // scope 0 at add.rs:8:5: 8:24
39-
switchInt(move _1) -> [0: bb3, otherwise: bb2]; // scope 0 at add.rs:8:5: 8:24
34+
_2 = Eq(move _3, const 3_i32);
35+
_1 = Not(move _2);
36+
switchInt(move _1) -> [0: bb3, otherwise: bb2];
4037
}
4138

4239
bb2: {
43-
_4 = core::panicking::panic(const "assertion failed: add() == 3"); // scope 0 at add.rs:8:5: 8:24
44-
// mir::Constant
45-
// + span: add.rs:8:5: 8:24
46-
// + literal: Const { ty: fn(&'static str) -> ! {core::panicking::panic}, val: Value(<ZST>) }
47-
// mir::Constant
48-
// + span: no-location
49-
// + literal: Const { ty: &str, val: Value(Slice(..)) }
40+
_4 = core::panicking::panic(const "assertion failed: add() == 3");
5041
}
5142

5243
bb3: {
53-
return; // scope 0 at add.rs:10:2: 10:2
44+
return;
5445
}
5546
}

0 commit comments

Comments
 (0)