Skip to content

Commit 94c1c78

Browse files
jbertholdjberthold
authored
Refactor split RT-DATA into separate modules/files (#515)
* A basic module `rt/value.md` contains the `Value` sort and `TypedLocal` with its subsorts * A `rt/numbers.md` module contains code related to decoding and casting integers, and helper functions * The configuration now lives inside `rt/configuration.md` Most of this is just moving existing code around into new files and adjusting imports. The `RT-DATA-LOW` and `RT-DATA-HIGH` modules were removed, moving code from `HIGH` into `RT-DATA` (`RT-DATA-LOW` was never actually used). ## New module import graph (omitting `domains.md` modules): ![image](https://github.com/user-attachments/assets/a2e6bd8c-79fb-4ea2-9a18-39630ff587c3) We can split `rt/data.md` into more parts, e.g. * [ ] reading/writing locals and projections, * [ ] `Rvalue` evaluation (in general), which could also move to `KMIR-CONTROL-FLOW` inside `kmir.md` * [ ] `BinaryOp`, `UnaryOp` (which are specific `Rvalue`s)
1 parent 827e46b commit 94c1c78

File tree

12 files changed

+706
-785
lines changed

12 files changed

+706
-785
lines changed

‎kmir/pyproject.toml

Lines changed: 1 addition & 1 deletion
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.110"
7+
version = "0.3.111"
88
description = ""
99
authors = [
1010
"Runtime Verification, Inc. <[email protected]>",

‎kmir/src/kmir/__init__.py

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
from typing import Final
22

3-
VERSION: Final = '0.3.110'
3+
VERSION: Final = '0.3.111'

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ module KMIR-AST
1616
imports TARGET
1717
imports TYPES
1818
19+
1920
syntax Pgm ::= Symbol GlobalAllocs FunctionNames MonoItems BaseTypes
2021
[symbol(pgm), group(mir---name--allocs--functions--items--types)]
2122
@@ -32,5 +33,7 @@ module KMIR-AST
3233
3334
syntax BaseTypes ::= List{BaseType, ""} [group(mir-list), symbol(BaseTypes::append), terminator-symbol(BaseTypes::empty)]
3435
36+
syntax KItem ::= #init( Pgm )
37+
3538
endmodule
3639
```

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

Lines changed: 10 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
```k
44
requires "kmir-ast.md"
55
requires "rt/data.md"
6+
requires "rt/configuration.md"
67
requires "lemmas/kmir-lemmas.md"
78
```
89

@@ -12,92 +13,29 @@ The MIR syntax is largely defined in [KMIR-AST](./kmir-ast.md) and its
1213
submodules. The execution is initialised based on a loaded `Pgm` read
1314
from a json format of stable-MIR, and the name of the function to execute.
1415

15-
```k
16-
module KMIR-SYNTAX
17-
imports KMIR-AST
18-
19-
syntax KItem ::= #init( Pgm )
20-
21-
endmodule
22-
```
23-
2416
## (Dynamic) Semantics
2517

2618
### Execution Configuration
2719

28-
The execution (dynamic) semantics of MIR in K is defined based on the
29-
configuration of the running program.
30-
31-
Essential parts of the configuration:
32-
* the `k` cell to control the execution
33-
* a `stack` of `StackFrame`s describing function calls and their data
34-
* `currentFrame`, an unpacked version of the top of `stack`
35-
* the `functions` map to look up function bodies when they are called
36-
* the `memory` cell which abstracts allocated heap data
37-
38-
The entire program's return value (`retVal`) is held in a separate cell.
39-
40-
Besides the `caller` (to return to) and `dest` and `target` to specify where the return value should be written, a `StackFrame` includes information about the `locals` of the currently-executing function/item. Each function's code will only access local values (or heap data referenced by them). Local variables carry type information (see `RT-DATA`).
41-
42-
```k
43-
module KMIR-CONFIGURATION
44-
imports KMIR-SYNTAX
45-
imports INT-SYNTAX
46-
imports BOOL-SYNTAX
47-
imports RT-DATA-HIGH-SYNTAX
48-
49-
syntax RetVal ::= return( Value )
50-
| "noReturn"
51-
52-
syntax StackFrame ::= StackFrame(caller:Ty, // index of caller function
53-
dest:Place, // place to store return value
54-
target:MaybeBasicBlockIdx, // basic block to return to
55-
UnwindAction, // action to perform on panic
56-
locals:List) // return val, args, local variables
57-
58-
configuration <kmir>
59-
<k> #init($PGM:Pgm) </k>
60-
<retVal> noReturn </retVal>
61-
<currentFunc> ty(-1) </currentFunc> // to retrieve caller
62-
// unpacking the top frame to avoid frequent stack read/write operations
63-
<currentFrame>
64-
<currentBody> .List </currentBody>
65-
<caller> ty(-1) </caller>
66-
<dest> place(local(-1), .ProjectionElems)</dest>
67-
<target> noBasicBlockIdx </target>
68-
<unwind> unwindActionUnreachable </unwind>
69-
<locals> .List </locals>
70-
</currentFrame>
71-
// remaining call stack (without top frame)
72-
<stack> .List </stack>
73-
// function store, Ty -> MonoItemFn
74-
<functions> .Map </functions>
75-
// heap
76-
<memory> .Map </memory> // FIXME unclear how to model
77-
// FIXME where do we put the "GlobalAllocs"? in the heap, presumably?
78-
<start-symbol> symbol($STARTSYM:String) </start-symbol>
79-
// static information about the base type interning in the MIR
80-
<basetypes> .Map </basetypes>
81-
</kmir>
82-
83-
endmodule
84-
```
20+
The _configuration_ that this MIR semantics operates on carries the entire state of the running program, including local variables of the current function item, the whole call stack, as well as all code items that may potentially be executed.
8521

22+
See [`rt/configuration.md`](./rt/configuration.md) for a detailed description of the configuration.
8623

8724
### Execution Control Flow
8825

8926
```k
9027
module KMIR-CONTROL-FLOW
91-
imports KMIR-SYNTAX
92-
imports KMIR-CONFIGURATION
93-
imports MONO
94-
imports RT-DATA-HIGH
95-
imports TYPES
96-
9728
imports BOOL
9829
imports LIST
9930
imports MAP
10031
imports K-EQUAL
32+
33+
imports KMIR-AST
34+
imports MONO
35+
imports TYPES
36+
37+
imports KMIR-CONFIGURATION
38+
imports RT-DATA
10139
```
10240

10341
Execution of a program begins by creating a stack frame for the `main`

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,11 @@ requires "../rt/data.md"
1212
requires "../kmir.md"
1313
1414
module KMIR-LEMMAS
15-
imports RT-DATA-HIGH
16-
1715
imports LIST
1816
imports INT-SYMBOLIC
1917
imports BOOL
18+
19+
imports RT-DATA
2020
```
2121
## Simplifications for lists to avoid spurious branching on error cases in control flow
2222

‎kmir/src/kmir/kdist/mir-semantics/rt/configuration.md

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
# KMIR Configuration
2+
3+
This is the configuration of a running program in the MIR semantics.
4+
5+
Essential parts of the configuration:
6+
* the `k` cell to control the execution
7+
* a `stack` of `StackFrame`s describing function calls and their data
8+
* `currentFrame`, an unpacked version of the top of `stack`
9+
* the `functions` map to look up function bodies when they are called
10+
* the `memory` cell which abstracts allocated heap data
11+
12+
The entire program's return value (`retVal`) is held in a separate cell.
13+
14+
Besides the `caller` (to return to) and `dest` and `target` to specify where the return value should be written, a `StackFrame` includes information about the `locals` of the currently-executing function/item. Each function's code will only access local values (or heap data referenced by them). Local variables carry type information (see `RT-DATA`).
15+
16+
```k
17+
requires "./value.md"
18+
19+
module KMIR-CONFIGURATION
20+
imports KMIR-AST
21+
imports INT-SYNTAX
22+
imports BOOL-SYNTAX
23+
imports RT-VALUE-SYNTAX
24+
25+
syntax RetVal ::= return( Value )
26+
| "noReturn"
27+
28+
syntax StackFrame ::= StackFrame(caller:Ty, // index of caller function
29+
dest:Place, // place to store return value
30+
target:MaybeBasicBlockIdx, // basic block to return to
31+
UnwindAction, // action to perform on panic
32+
locals:List) // return val, args, local variables
33+
34+
configuration <kmir>
35+
<k> #init($PGM:Pgm) </k>
36+
<retVal> noReturn </retVal>
37+
<currentFunc> ty(-1) </currentFunc> // to retrieve caller
38+
// unpacking the top frame to avoid frequent stack read/write operations
39+
<currentFrame>
40+
<currentBody> .List </currentBody>
41+
<caller> ty(-1) </caller>
42+
<dest> place(local(-1), .ProjectionElems)</dest>
43+
<target> noBasicBlockIdx </target>
44+
<unwind> unwindActionUnreachable </unwind>
45+
<locals> .List </locals>
46+
</currentFrame>
47+
// remaining call stack (without top frame)
48+
<stack> .List </stack>
49+
// function store, Ty -> MonoItemFn
50+
<functions> .Map </functions>
51+
// heap
52+
<memory> .Map </memory> // FIXME unclear how to model
53+
// FIXME where do we put the "GlobalAllocs"? in the heap, presumably?
54+
<start-symbol> symbol($STARTSYM:String) </start-symbol>
55+
// static information about the base type interning in the MIR
56+
<basetypes> .Map </basetypes>
57+
</kmir>
58+
59+
endmodule
60+
```

0 commit comments

Comments
 (0)