Refactor split RT-DATA into separate modules/files

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.3.110"
+version = "0.3.111"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.110'
+VERSION: Final = '0.3.111'

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

@@ -16,6 +16,7 @@ module KMIR-AST
   imports TARGET
   imports TYPES
 
+
   syntax Pgm ::= Symbol GlobalAllocs FunctionNames MonoItems BaseTypes
                  [symbol(pgm), group(mir---name--allocs--functions--items--types)]
 
@@ -32,5 +33,7 @@ module KMIR-AST
 
   syntax BaseTypes ::= List{BaseType, ""} [group(mir-list), symbol(BaseTypes::append), terminator-symbol(BaseTypes::empty)]
 
+  syntax KItem ::= #init( Pgm )
+
 endmodule
 ```

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

@@ -3,6 +3,7 @@
 ```k
 requires "kmir-ast.md"
 requires "rt/data.md"
+requires "rt/configuration.md"
 requires "lemmas/kmir-lemmas.md"
 ```
 
@@ -12,92 +13,29 @@ The MIR syntax is largely defined in [KMIR-AST](./kmir-ast.md) and its
 submodules. The execution is initialised based on a loaded `Pgm` read
 from a json format of stable-MIR, and the name of the function to execute.
 
-```k
-module KMIR-SYNTAX
-  imports KMIR-AST
-
-  syntax KItem ::= #init( Pgm )
-
-endmodule
-```
-
 ## (Dynamic) Semantics
 
 ### Execution Configuration
 
-The execution (dynamic) semantics of MIR in K is defined based on the
-configuration of the running program.
-
-Essential parts of the configuration:
-* the `k` cell to control the execution
-* a `stack` of `StackFrame`s describing function calls and their data
-* `currentFrame`, an unpacked version of the top of `stack`
-* the `functions` map to look up function bodies when they are called
-* the `memory` cell which abstracts allocated heap data
-
-The entire program's return value (`retVal`) is held in a separate cell.
-
-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`).
-
-```k
-module KMIR-CONFIGURATION
-  imports KMIR-SYNTAX
-  imports INT-SYNTAX
-  imports BOOL-SYNTAX
-  imports RT-DATA-HIGH-SYNTAX
-
-  syntax RetVal ::= return( Value )
-                  | "noReturn"
-
-  syntax StackFrame ::= StackFrame(caller:Ty,                 // index of caller function
-                                   dest:Place,                // place to store return value
-                                   target:MaybeBasicBlockIdx, // basic block to return to
-                                   UnwindAction,              // action to perform on panic
-                                   locals:List)               // return val, args, local variables
-
-  configuration <kmir>
-                  <k> #init($PGM:Pgm) </k>
-                  <retVal> noReturn </retVal>
-                  <currentFunc> ty(-1) </currentFunc> // to retrieve caller
-                  // unpacking the top frame to avoid frequent stack read/write operations
-                  <currentFrame>
-                    <currentBody> .List </currentBody>
-                    <caller> ty(-1) </caller>
-                    <dest> place(local(-1), .ProjectionElems)</dest>
-                    <target> noBasicBlockIdx </target>
-                    <unwind> unwindActionUnreachable </unwind>
-                    <locals> .List </locals>
-                  </currentFrame>
-                  // remaining call stack (without top frame)
-                  <stack> .List </stack>
-                  // function store, Ty -> MonoItemFn
-                  <functions> .Map </functions>
-                  // heap
-                  <memory> .Map </memory> // FIXME unclear how to model
-                  // FIXME where do we put the "GlobalAllocs"? in the heap, presumably?
-                  <start-symbol> symbol($STARTSYM:String) </start-symbol>
-                  // static information about the base type interning in the MIR
-                  <basetypes> .Map </basetypes>
-                </kmir>
-
-endmodule
-```
+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.
 
+See [`rt/configuration.md`](./rt/configuration.md) for a detailed description of the configuration.
 
 ### Execution Control Flow
 
 ```k
 module KMIR-CONTROL-FLOW
-  imports KMIR-SYNTAX
-  imports KMIR-CONFIGURATION
-  imports MONO
-  imports RT-DATA-HIGH
-  imports TYPES
-
   imports BOOL
   imports LIST
   imports MAP
   imports K-EQUAL
+
+  imports KMIR-AST
+  imports MONO
+  imports TYPES
+
+  imports KMIR-CONFIGURATION
+  imports RT-DATA
 ```
 
 Execution of a program begins by creating a stack frame for the `main`

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

@@ -12,11 +12,11 @@ requires "../rt/data.md"
 requires "../kmir.md"
 
 module KMIR-LEMMAS
-  imports RT-DATA-HIGH
-
   imports LIST
   imports INT-SYMBOLIC
   imports BOOL
+
+  imports RT-DATA
 ```
 ## Simplifications for lists to avoid spurious branching on error cases in control flow
 

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

@@ -0,0 +1,60 @@
+# KMIR Configuration
+
+This is the configuration of a running program in the MIR semantics.
+
+Essential parts of the configuration:
+* the `k` cell to control the execution
+* a `stack` of `StackFrame`s describing function calls and their data
+* `currentFrame`, an unpacked version of the top of `stack`
+* the `functions` map to look up function bodies when they are called
+* the `memory` cell which abstracts allocated heap data
+
+The entire program's return value (`retVal`) is held in a separate cell.
+
+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`).
+
+```k
+requires "./value.md"
+
+module KMIR-CONFIGURATION
+  imports KMIR-AST
+  imports INT-SYNTAX
+  imports BOOL-SYNTAX
+  imports RT-VALUE-SYNTAX
+
+  syntax RetVal ::= return( Value )
+                  | "noReturn"
+
+  syntax StackFrame ::= StackFrame(caller:Ty,                 // index of caller function
+                                   dest:Place,                // place to store return value
+                                   target:MaybeBasicBlockIdx, // basic block to return to
+                                   UnwindAction,              // action to perform on panic
+                                   locals:List)               // return val, args, local variables
+
+  configuration <kmir>
+                  <k> #init($PGM:Pgm) </k>
+                  <retVal> noReturn </retVal>
+                  <currentFunc> ty(-1) </currentFunc> // to retrieve caller
+                  // unpacking the top frame to avoid frequent stack read/write operations
+                  <currentFrame>
+                    <currentBody> .List </currentBody>
+                    <caller> ty(-1) </caller>
+                    <dest> place(local(-1), .ProjectionElems)</dest>
+                    <target> noBasicBlockIdx </target>
+                    <unwind> unwindActionUnreachable </unwind>
+                    <locals> .List </locals>
+                  </currentFrame>
+                  // remaining call stack (without top frame)
+                  <stack> .List </stack>
+                  // function store, Ty -> MonoItemFn
+                  <functions> .Map </functions>
+                  // heap
+                  <memory> .Map </memory> // FIXME unclear how to model
+                  // FIXME where do we put the "GlobalAllocs"? in the heap, presumably?
+                  <start-symbol> symbol($STARTSYM:String) </start-symbol>
+                  // static information about the base type interning in the MIR
+                  <basetypes> .Map </basetypes>
+                </kmir>
+
+endmodule
+```