--start-symbol for kmir run (#446)

This adds a `<start-symbol>` cell to the configuration with a
configuration variable for the symbol to begin execution from.

It also changes the expected output in the `exec-smir` integration tests
to only check the contents of the K cell. The semantics are going to be
very unstable right now, and without this change we will probably be
spending time updating the test vectors on nearly every pull request.

---------

Co-authored-by: devops <[email protected]>

Author: gtrepta

kmir/Makefile

@@ -90,3 +90,9 @@ SRC_FILES := $(shell find src -type f -name '*.py')
 
 pyupgrade: poetry-install
 	$(POETRY_RUN) pyupgrade --py310-plus $(SRC_FILES)
+
+# Update smir exec tests
+
+.PHONY: update-exec-smir
+update-exec-smir: poetry-install
+	UPDATE_EXEC_SMIR=true $(POETRY_RUN) pytest -k test_exec_smir

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.3.70"
+version = "0.3.71"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.70'
+VERSION: Final = '0.3.71'

kmir/src/kmir/__main__.py

@@ -6,8 +6,6 @@
 from pathlib import Path
 from typing import TYPE_CHECKING
 
-from pyk.kast.inner import KSort, Subst
-
 from kmir.build import semantics
 from kmir.convert_from_definition.v2parser import parse_json
 
@@ -23,6 +21,7 @@ class KMirOpts: ...
 class RunOpts(KMirOpts):
     input_file: Path
     depth: int
+    start_symbol: str
 
 
 def _kmir_run(opts: RunOpts) -> None:
@@ -35,10 +34,7 @@ def _kmir_run(opts: RunOpts) -> None:
 
     kmir_kast, _ = parse_result
 
-    subst = Subst({'$PGM': kmir_kast})
-    init_config = subst.apply(tools.definition.init_config(KSort('GeneratedTopCell')))
-    init_kore = tools.krun.kast_to_kore(init_config, KSort('GeneratedTopCell'))
-    result = tools.krun.run_pattern(init_kore, depth=opts.depth)
+    result = tools.run_parsed(kmir_kast, opts.start_symbol, opts.depth)
 
     print(tools.kprint.kore_to_pretty(result))
 
@@ -60,6 +56,9 @@ def _arg_parser() -> ArgumentParser:
     run_parser = command_parser.add_parser('run', help='run stable MIR programs')
     run_parser.add_argument('input_file', metavar='FILE', help='MIR program to run')
     run_parser.add_argument('--depth', type=int, metavar='DEPTH', help='Depth to execute')
+    run_parser.add_argument(
+        '--start-symbol', type=str, metavar='SYMBOL', default='main', help='Symbol name to begin execution from'
+    )
 
     return parser
 
@@ -69,7 +68,7 @@ def _parse_args(args: Sequence[str]) -> KMirOpts:
 
     match ns.command:
         case 'run':
-            return RunOpts(input_file=Path(ns.input_file).resolve(), depth=ns.depth)
+            return RunOpts(input_file=Path(ns.input_file).resolve(), depth=ns.depth, start_symbol=ns.start_symbol)
         case _:
             raise AssertionError()
 

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

@@ -16,7 +16,7 @@ module KMIR-SYNTAX
   imports INT-SYNTAX
   imports FLOAT-SYNTAX
 
-  syntax KItem ::= #init( Pgm, Symbol )
+  syntax KItem ::= #init( Pgm )
 
 ////////////////////////////////////////////
 // FIXME things below related to memory and
@@ -73,7 +73,7 @@ module KMIR-CONFIGURATION
                                    locals:List)               // return val, args, local variables
 
   configuration <kmir>
-                  <k> #init($PGM:Pgm, symbol("main")) </k>
+                  <k> #init($PGM:Pgm) </k>
                   <retVal> NoValue </retVal>
                   <currentFunc> ty(-1) </currentFunc> // to retrieve caller
                   // unpacking the top frame to avoid frequent stack read/write operations
@@ -92,6 +92,7 @@ module KMIR-CONFIGURATION
                   // 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>
                 </kmir>
 endmodule
 ```
@@ -116,11 +117,12 @@ function map and the initial memory have to be set up.
 
 ```k
   // #init step, assuming a singleton in the K cell
-  rule <k> #init(_Name:Symbol _Allocs:GlobalAllocs Functions:FunctionNames Items:MonoItems, FuncName)
+  rule <k> #init(_Name:Symbol _Allocs:GlobalAllocs Functions:FunctionNames Items:MonoItems)
          =>
            #execFunction(#findItem(Items, FuncName), Functions)
        </k>
        <functions> _ => #mkFunctionMap(Functions, Items) </functions>
+       <start-symbol> FuncName </start-symbol>
 ```
 
 The `Map` of `functions` is constructed from the lookup table of `FunctionNames`,

kmir/src/kmir/tools.py

@@ -2,15 +2,19 @@
 
 from typing import TYPE_CHECKING
 
+from pyk.kast.inner import KSort, Subst
 from pyk.kast.outer import read_kast_definition
 from pyk.ktool.krun import KRun
+from pyk.prelude.string import stringToken
 
 from .kparse import KParse
 
 if TYPE_CHECKING:
     from pathlib import Path
 
+    from pyk.kast import KInner
     from pyk.kast.outer import KDefinition
+    from pyk.kore.syntax import Pattern
     from pyk.ktool.kprint import KPrint
 
 
@@ -42,3 +46,14 @@ def krun(self) -> KRun:
     @property
     def definition(self) -> KDefinition:
         return self.__definition
+
+    def run_parsed(self, parsed_smir: KInner, start_symbol: KInner | str = 'main', depth: int | None = None) -> Pattern:
+        if isinstance(start_symbol, str):
+            start_symbol = stringToken(start_symbol)
+
+        subst = Subst({'$PGM': parsed_smir, '$STARTSYM': start_symbol})
+        init_config = subst.apply(self.definition.init_config(KSort('GeneratedTopCell')))
+        init_kore = self.krun.kast_to_kore(init_config, KSort('GeneratedTopCell'))
+        result = self.krun.run_pattern(init_kore, depth=depth)
+
+        return result

kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.15.state

@@ -47,5 +47,7 @@
   <memory>
     .Map
   </memory>
-</kmir>
-
+  <start-symbol>
+    symbol ( "main" )
+  </start-symbol>
+</kmir>

kmir/src/tests/integration/data/exec-smir/main-a-b-c/main-a-b-c.run.state

@@ -46,4 +46,7 @@
   <memory>
     .Map
   </memory>
-</kmir>
+  <start-symbol>
+    symbol ( "main" )
+  </start-symbol>
+</kmir>

kmir/src/tests/integration/test_integration.py

@@ -1,11 +1,12 @@
 from __future__ import annotations
 
 import json
+import os
 from pathlib import Path
 from typing import TYPE_CHECKING
 
 import pytest
-from pyk.kast.inner import KApply, KSort, KToken, Subst
+from pyk.kast.inner import KApply, KSort, KToken
 
 from kmir.convert_from_definition.v2parser import Parser
 
@@ -187,14 +188,15 @@ def test_exec_smir(
     assert parsed is not None
     kmir_kast, _ = parsed
 
-    subst = Subst({'$PGM': kmir_kast})
-    init_config = subst.apply(tools.definition.init_config(KSort('GeneratedTopCell')))
-    init_kore = tools.krun.kast_to_kore(init_config, KSort('GeneratedTopCell'))
-    result = tools.krun.run_pattern(init_kore, depth=depth)
+    result = tools.run_parsed(kmir_kast, depth=depth)
 
     with output_kast.open('r') as f:
         expected = f.read().rstrip()
 
     result_pretty = tools.kprint.kore_to_pretty(result).rstrip()
 
-    assert result_pretty == expected
+    if os.getenv('UPDATE_EXEC_SMIR') is None:
+        assert result_pretty == expected
+    else:
+        with output_kast.open('w') as f:
+            f.write(result_pretty)

package/version

@@ -1 +1 @@
-0.3.70
+0.3.71