Adding multi-crate support through cell map

Makefile

@@ -31,7 +31,7 @@ smir-parse-tests: # build # commented out for CI's sake
 		&& echo -n "smir-ed " \
 		|| report "$$source" "SMIR ERROR!"; \
 	    if [ -s $${target} ]; then \
-		${POETRY_RUN} convert-from-definition $$(realpath $${target}) Pgm > /dev/null \
+		${POETRY_RUN} convert-from-definition $$(realpath $${target}) Crate > /dev/null \
 			&& (echo "and parsed!"; rm $${target}) \
 			|| report "$$source" "PARSE ERROR!"; \
 		fi; \

kmir/src/kmir/__main__.py

@@ -1,32 +1,37 @@
 from __future__ import annotations
 
+import os
 import sys
 from argparse import ArgumentParser
 from dataclasses import dataclass
 from pathlib import Path
 from typing import TYPE_CHECKING
 
 from pyk.cterm import CTerm, cterm_build_claim
-from pyk.kast.inner import Subst
+from pyk.kast.inner import KApply, KSort, Subst
 from pyk.kast.manip import split_config_from
 from pyk.kast.outer import KFlatModule, KImport
 
 from kmir.build import haskell_semantics, llvm_semantics
+from kmir.convert_from_definition.__main__ import parse_mir_klist_json
 from kmir.convert_from_definition.v2parser import parse_json
 
 if TYPE_CHECKING:
     from collections.abc import Sequence
 
+    from pyk.kast.inner import KToken
+
 
 @dataclass
 class KMirOpts: ...
 
 
 @dataclass
 class RunOpts(KMirOpts):
-    input_file: Path
+    input_files: list[Path]
     depth: int
     start_symbol: str
+    start_crate: str
     haskell_backend: bool
 
 
@@ -48,22 +53,43 @@ def __init__(self, input_file: Path, output_file: str | None, start_symbol: str)
 def _kmir_run(opts: RunOpts) -> None:
     tools = haskell_semantics() if opts.haskell_backend else llvm_semantics()
 
-    parse_result = parse_json(tools.definition, opts.input_file, 'Pgm')
-    if parse_result is None:
-        print('Parse error!', file=sys.stderr)
+    # TODO: Same as comment in convert_from_definition::__main__.py - args.sort might not be right
+    results = [parse_json(tools.definition, input_file, 'Crate') for input_file in opts.input_files]
+
+    failed = []
+    passed: list[tuple[KApply | KToken, KSort]] = []
+
+    for index, result in enumerate(results):
+        if result is None:
+            failed.append(opts.input_files[index])
+        else:
+            passed.append(result)
+
+    if failed:
+        for failure in failed:
+            print(f'Parse error! In {failure}', file=sys.stderr)
         sys.exit(1)
 
-    kmir_kast, _ = parse_result
+    terms, _sort = parse_mir_klist_json(passed, KSort('Crate'))
+
+    start_crate = (
+        extract_crate_name(opts.input_files[0]).replace('-', '_') if len(opts.input_files) == 1 else opts.start_crate
+    )
+
+    run_result = tools.run_parsed(terms, opts.start_symbol, start_crate, opts.depth)
 
-    result = tools.run_parsed(kmir_kast, opts.start_symbol, opts.depth)
+    print(tools.kprint.kore_to_pretty(run_result))
 
-    print(tools.kprint.kore_to_pretty(result))
+
+def extract_crate_name(file_path: Path) -> str:
+    filename = os.path.basename(file_path)
+    return filename.removesuffix('.smir.json')
 
 
 def _kmir_gen_spec(opts: GenSpecOpts) -> None:
     tools = haskell_semantics()
 
-    parse_result = parse_json(tools.definition, opts.input_file, 'Pgm')
+    parse_result = parse_json(tools.definition, opts.input_file, 'Crate')
     if parse_result is None:
         print('Parse error!', file=sys.stderr)
         sys.exit(1)
@@ -105,11 +131,14 @@ def _arg_parser() -> ArgumentParser:
     command_parser = parser.add_subparsers(dest='command', required=True)
 
     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('input_file', metavar='FILE', nargs='+', 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'
     )
+    run_parser.add_argument(
+        '--start-crate', type=str, metavar='START_CRATE', default='main', help='Crate name to begin execution from'
+    )
     run_parser.add_argument('--haskell-backend', action='store_true', help='Run with the haskell backend')
 
     gen_spec_parser = command_parser.add_parser('gen-spec', help='Generate a k spec from a SMIR json')
@@ -128,9 +157,10 @@ def _parse_args(args: Sequence[str]) -> KMirOpts:
     match ns.command:
         case 'run':
             return RunOpts(
-                input_file=Path(ns.input_file).resolve(),
+                input_files=[Path(file).resolve() for file in ns.input_file],
                 depth=ns.depth,
                 start_symbol=ns.start_symbol,
+                start_crate=ns.start_crate,
                 haskell_backend=ns.haskell_backend,
             )
         case 'gen-spec':

kmir/src/kmir/convert_from_definition/__main__.py

@@ -1,6 +1,14 @@
+from __future__ import annotations
+
 import argparse
 import sys
 from pathlib import Path
+from typing import TYPE_CHECKING
+
+from pyk.kast.inner import KApply, KSort
+
+if TYPE_CHECKING:
+    from pyk.kast.inner import KToken
 
 from kmir.build import llvm_semantics
 
@@ -9,20 +17,51 @@
 
 def parse_args() -> argparse.Namespace:
     parser = argparse.ArgumentParser()
-    parser.add_argument('json', metavar='JSON', help='JSON data to convert')
-    parser.add_argument('sort', metavar='SORT', help='Expected Sort name for the parsed term', default='pgm')
+    parser.add_argument(
+        'json', metavar='JSON', nargs='+', help='JSON data to convert, add multiple files for cross-crate'
+    )
+    parser.add_argument('sort', metavar='SORT', help='Expected Sort name for the parsed term', default='Crate')
     return parser.parse_args()
 
 
+# This is essentially just a duplicate of `Parser` method `_parse_mir_klist_json`
+def parse_mir_klist_json(crates: list[tuple[KApply | KToken, KSort]], sort: KSort) -> tuple[KApply, KSort]:
+    append_symbol = '_List_'
+    empty_symbol = '.List'
+    list_item_symbol = 'ListItem'
+    list_kapply = KApply(empty_symbol, ())
+    first_iter = True
+    for element_kapply, _ in crates:
+        element_list_item = KApply(list_item_symbol, (element_kapply))
+        if first_iter:
+            list_kapply = element_list_item
+            first_iter = False
+        else:
+            list_kapply = KApply(append_symbol, (list_kapply, element_list_item))
+    return list_kapply, sort
+
+
 def main() -> None:
     args = parse_args()
     tools = llvm_semantics()
 
-    result = parse_json(tools.definition, Path(args.json), args.sort)
+    # TODO: args.sort might not be right
+    results = [parse_json(tools.definition, Path(json), args.sort) for json in args.json]
+
+    failed = []
+    passed: list[tuple[KApply | KToken, KSort]] = []
 
-    if result is None:
-        print('Parse error!', file=sys.stderr)
+    for index, result in enumerate(results):
+        if result is None:
+            failed.append(args.json[index])
+        else:
+            passed.append(result)
+
+    if failed:
+        for failure in failed:
+            print(f'Parse error! In {failure}', file=sys.stderr)
         sys.exit(1)
 
-    term, _ = result
-    print(tools.krun.pretty_print(term))
+    terms, _sort = parse_mir_klist_json(passed, KSort('Crate'))
+
+    print(tools.krun.pretty_print(terms))

kmir/src/kmir/convert_json/convert.py

@@ -637,7 +637,7 @@ def from_dict(js: Mapping[str, object]) -> KInner:
             CRATE_ID = id
             functions_map_from_dict(functions)
             return KApply(
-                'pgm',
+                'crate',
                 (
                     string_from_dict(name),
                     global_allocs_from_dict(allocs),

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

@@ -15,9 +15,13 @@ module KMIR-AST
   imports MONO
   imports TARGET
   imports TYPES
+```
 
-  syntax Pgm ::= Symbol GlobalAllocs FunctionNames MonoItems BaseTypes
-                 [symbol(pgm), group(mir---name--allocs--functions--items--types)]
+`Crate` deviates from the Stable MIR definition of crate (which is a struct containing `id: CrateNum`, `name: Symbol`, `is_local: bool`) since this is not rich enough in information for our purposes. 
+```k 
+  syntax Crate ::= ".Crate"
+                 | Symbol GlobalAllocs FunctionNames MonoItems BaseTypes
+                   [symbol(crate), group(mir---name--allocs--functions--items--types)]
 
   syntax FunctionKind ::= functionNormalSym(Symbol) [symbol(FunctionKind::NormalSym), group(mir-enum)]
                         | functionIntrinsic(Symbol) [symbol(FunctionKind::IntrinsicSym), group(mir-enum)]

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

@@ -8,14 +8,15 @@ requires "rt/data.md"
 ## Syntax of MIR in K
 
 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
+submodules. The execution is initialised based on a loaded `Crate` 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 )
+  syntax CrateList ::= List
+  syntax KItem ::= #init( Crate )
 
 endmodule
 ```
@@ -45,6 +46,8 @@ module KMIR-CONFIGURATION
   imports BOOL-SYNTAX
   imports RT-DATA-HIGH-SYNTAX
 
+  syntax KItem ::= "#populate_crate_map" "(" CrateList ")"
+
   syntax RetVal ::= MaybeValue
 
   syntax StackFrame ::= StackFrame(caller:Ty,                 // index of caller function
@@ -54,7 +57,7 @@ module KMIR-CONFIGURATION
                                    locals:List)               // return val, args, local variables
 
   configuration <kmir>
-                  <k> #init($PGM:Pgm) </k>
+                  <k> #populate_crate_map($PGM:CrateList) </k>
                   <retVal> NoValue </retVal>
                   <currentFunc> ty(-1) </currentFunc> // to retrieve caller
                   // unpacking the top frame to avoid frequent stack read/write operations
@@ -74,8 +77,15 @@ module KMIR-CONFIGURATION
                   <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>
+                  <start-crate> symbol($STARTCRATE:String) </start-crate>
                   // static information about the base type interning in the MIR
                   <basetypes> .Map </basetypes>
+                  <crates>
+                    <crate multiplicity="*" type="Map" initial="">
+                      <name> symbol(""):Symbol </name>
+                      <contents> .Crate:Crate </contents>
+                    </crate>
+                  </crates>
                 </kmir>
 
 endmodule
@@ -103,6 +113,32 @@ function and executing its function body. Before execution begins, the
 function map and the initial memory have to be set up.
 
 ```k
+  // TODO: This leave the dummy configuration in the cell map, need to remove it or better yet never add it at all 
+  rule <k> #populate_crate_map( ListItem(NAME:Symbol ALLOCS:GlobalAllocs FUNCTIONS:FunctionNames ITEMS:MonoItems TYPES:BaseTypes) LIST)
+    => #populate_crate_map(LIST) ...</k>
+      <crates>
+        ( .Bag => <crate>
+                    <name> NAME </name>
+                    <contents> NAME ALLOCS FUNCTIONS ITEMS TYPES </contents>
+                  </crate>
+        )
+        ...
+      </crates>
+
+  rule <k> #populate_crate_map( .List ) => #init( #lookup_crate(START_CRATE) ) ...</k>
+        <start-crate> START_CRATE </start-crate>
+
+  syntax Crate ::= "#lookup_crate" "(" Symbol ")" [function]
+
+  rule [[ #lookup_crate( NAME ) => CONTENTS ]]
+    <crates>
+      <crate>
+        <name> NAME </name>
+        <contents> CONTENTS </contents>
+      </crate>
+      ...
+    </crates>
+
   // #init step, assuming a singleton in the K cell
   rule <k> #init(_NAME:Symbol _ALLOCS:GlobalAllocs FUNCTIONS:FunctionNames ITEMS:MonoItems TYPES:BaseTypes)
          =>

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

@@ -26,7 +26,6 @@ syntax ImplTraitDecls ::= List {ImplDef, ""}
 
 syntax CrateItem ::= crateItem(Int) // imported from crate
 syntax CrateNum ::= crateNum(Int)
-syntax Crate ::= crate(id: CrateNum, name: Symbol, isLocal: MIRBool)
 
 syntax ItemKind ::= "itemKindFn" [symbol(itemKindFn)]
                   | "itemKindStatic" [symbol(itemKindStatic)]

kmir/src/kmir/tools.py

@@ -57,17 +57,27 @@ def kmir(self) -> KMIR:
     def definition(self) -> KDefinition:
         return self.__definition
 
-    def run_parsed(self, parsed_smir: KInner, start_symbol: KInner | str = 'main', depth: int | None = None) -> Pattern:
-        init_config = self.make_init_config(parsed_smir, start_symbol)
+    def run_parsed(
+        self,
+        parsed_smir: KInner,
+        start_symbol: KInner | str = 'main',
+        start_crate: KInner | str = 'main',
+        depth: int | None = None,
+    ) -> Pattern:
+        init_config = self.make_init_config(parsed_smir, start_symbol, start_crate)
         init_kore = self.krun.kast_to_kore(init_config, KSort('GeneratedTopCell'))
         result = self.krun.run_pattern(init_kore, depth=depth)
 
         return result
 
-    def make_init_config(self, parsed_smir: KInner, start_symbol: KInner | str = 'main') -> KInner:
+    def make_init_config(
+        self, parsed_smir: KInner, start_symbol: KInner | str = 'main', start_crate: KInner | str = 'main'
+    ) -> KInner:
         if isinstance(start_symbol, str):
             start_symbol = stringToken(start_symbol)
+        if isinstance(start_crate, str):
+            start_crate = stringToken(start_crate)
 
-        subst = Subst({'$PGM': parsed_smir, '$STARTSYM': start_symbol})
+        subst = Subst({'$PGM': parsed_smir, '$STARTSYM': start_symbol, '$STARTCRATE': start_crate})
         init_config = subst.apply(self.definition.init_config(KSort('GeneratedTopCell')))
         return init_config