Add annotations and tweaks to parse a complete smir json (#408)

* read a file in convert-from-definition instead of expecting verbatim json * add more file requires clauses to reflect imports As it turns out, these `requires "my-file.k"` clauses are interpreted _transitively_, but we should add all requirements explicitly to make editing and moving module contents easier. * WIP annotating K productions for parsing, top-down * WIP fixing var-debug-info parsing * teach the parser some more English plurals * fix parser for var_debug_info from panic_example * mir group annotations for all syntax in ty.k * reformat body.k to remove overly long lines * accept strings as single arguments of enum variants * Fix symbol typo, simplify Ty syntax, rename GenericArg * The `Ty` production with a struct was not observed in the wild yet. In addition, the [related rust code](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.Ty.html) seems to not have the modeled structure. * The `GenericArgs` list needs to contain elements of sort `GenericArg`, not `GenericArgKind` (see python list parsing code). * fix MonoItems parsing * Fix `GlobalAllocs` parsing (renamed from `GlobalAllocMap`) * add some details to the parser documentation notes * Set Version: 0.3.38 * Set Version: 0.3.39 * From review: add/correct list symbols as per convention, remove some comments, remove unused `Ty` production --------- Co-authored-by: devops <[email protected]>
runtimeverification · Aug 26, 2024 · 82d3e5e · 82d3e5e
1 parent ca9abac
commit 82d3e5e
Show file tree

Hide file tree

Showing 13 changed files with 535 additions and 339 deletions.
diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.3.38"
+version = "0.3.39"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py
@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.38'
+VERSION: Final = '0.3.39'
diff --git a/kmir/src/kmir/convert_from_definition/__main__.py b/kmir/src/kmir/convert_from_definition/__main__.py
@@ -19,7 +19,9 @@ def main() -> None:
     tools = semantics()
     p = Parser(tools.definition)
 
-    result = p.parse_mir_json(json.loads(args.json), args.sort)
+    with open(args.json, 'r') as f:
+        json_data = json.load(f)
+    result = p.parse_mir_json(json_data, args.sort)
     if result is None:
         print('Parse error!', file=sys.stderr)
         sys.exit(1)

diff --git a/kmir/src/kmir/convert_from_definition/notes.md b/kmir/src/kmir/convert_from_definition/notes.md
@@ -27,10 +27,10 @@ json: a boolean value, e.g., `true`
 
 #### mir-list
 ```
-syntax L ::= List {E, ""} [group(mir-list), ...]
+syntax Elems ::= List {Elem, ""} [group(mir-list), ...]
 ```
-json: a homogeneous list, e.g. `[e1, e2, e3, ...]`
-Note that all elements of the json list `(e1, e2, e3)` should correspond to syntactic productions for the sort E.
+json: a homogeneous list, e.g. `[e1, e2, e3, ...]`, where all elements correspond to syntactic productions for the sort `Elem`.
+As per naming convention, the list sort `Elems` (plural) should contain elements of sort `Elem` (singular). Usual plural formation rules (`Body -> Bodies`, `Branch -> Branches`) are respected.
 
 #### mir-klist-ElementSort
 ```
@@ -41,10 +41,16 @@ Note that all elements of the json list `(e1, e2, e3)` should correspond to synt
 
 #### mir-enum
 ```
-syntax MyEnum ::= myEnumField1(...) [group(mir-enum), ...]
-                | myEnumField2(...) [group(mir-enum), ...]
+syntax MyEnum ::= myEnumCon1(ArgSort)     [group(mir-enum)        , symbol(MyEnum::Con1)]
+                | myEnumCon2(Sort1,Sort2) [group(mir-enum)        , symbol(MyEnum::Con2)]
+                | myEnumCon3(field:...)   [group(mir-enum---field), symbol(MyEnum::Con3)]
+                | "myEnumCon4"            [group(mir-enum)        , symbol(MyEnum::Con4)]
 ```
-json: a dictionary with a single key-value pair. The key should correspond to one of the productions for the `MyEnum` Sort, and the value should be valid json.
+json: a dictionary with a single key-value pair.
+The key should correspond to (symbol for) one of the productions for the `MyEnum` Sort, and the value should be valid json.
+Arguments for variants that do not use field names are encoded as (heterogenous) _lists_ in json.
+Field names can be added after `mir-enum`, separated by `---`.
+Enum variants without arguments are encoded as _json strings_.
 
 #### mir-option
 ```
@@ -63,6 +69,7 @@ syntax MaybeInt::= someInt(Int) [group(mir-option-int)]
 #### mir
 Any remaining production describing MIR syntax.
 
+
 ### Conventions for productions
 - Syntax productions with more than one non terminals should not include sorts `Int`, `Bool`, `String`, but should instead use the sorts `MIRInt`, `MIRBool`, `MIRString`. These are intended to be semantically equivalent, i.e.
 ```

diff --git a/kmir/src/kmir/convert_from_definition/v2parser.py b/kmir/src/kmir/convert_from_definition/v2parser.py
@@ -99,14 +99,19 @@ def _list_symbols(sort: str) -> tuple[str, str]:
 # Given a list Sort, return the element sort.
 def _element_sort(sort: KSort) -> KSort:
     name = sort.name
-    # Dictionary containing irregular plural to singular sort names.
-    element_name = {
-        'Bodies': 'Body',
-        'Branches': 'Branch',
-        'VariantAndFieldIndices': 'VariantAndFieldIndex',
-    }.get(name)
-    if element_name:
-        return KSort(element_name)
+    if name.endswith('ies'):  # Bodies, Entries, ...
+        return KSort(name[:-3] + 'y')
+    elif (  # -es for words ending in 's', 'ch', 'sh', 'ss', 'x' or 'z'
+        name.endswith('ses')
+        or name.endswith('ches')
+        or name.endswith('shes')
+        or name.endswith('sses')
+        or name.endswith('xes')
+        or name.endswith('zes')
+    ):
+        return KSort(name[:-2])
+    elif name.endswith('Indices'):
+        return KSort(name[:-7] + 'Index')
     # If the name is not lsted above, we assume it has a regular plural form.
     # Simply remove trailing 's' to get the singular for element sort name.
     assert name.endswith('s')
@@ -261,7 +266,8 @@ def _parse_mir_enum_json(self, json: JSON, sort: KSort) -> ParseResult:
             # case, the argument needs to be changed to a list, so that its
             # structure is not cosidered a part of the current enumeration.
             if not _has_named_fields(_get_group(prod)) and len(prod.argument_sorts) == 1:
-                assert not isinstance(json_value, Sequence)
+                # str is a Sequence, therefore the extra check
+                assert isinstance(json_value, str) or not isinstance(json_value, Sequence)
                 json_value = [json_value]
             return self._parse_mir_nonterminal_json(json_value, prod)
         else:

diff --git a/kmir/src/kmir/kdist/mir-semantics/abi.md b/kmir/src/kmir/kdist/mir-semantics/abi.md
@@ -1,4 +1,8 @@
 ```k
+requires "lib.md"
+requires "target.md"
+requires "ty.md"
+
 module ABI
   imports LIB-SORTS
   imports TARGET-SORTS
@@ -143,4 +147,4 @@ syntax CallConvention ::= "callConventionC"
                         | "callConventionRiscvInterrupt"
 
 endmodule
-```
+```
diff --git a/kmir/src/kmir/kdist/mir-semantics/alloc.md b/kmir/src/kmir/kdist/mir-semantics/alloc.md
@@ -1,4 +1,7 @@
 ```k
+requires "ty.md"
+requires "mono.md"
+
 module ALLOC-SORTS
 
 syntax AllocId
@@ -27,16 +30,27 @@ module ALLOC
 
 ```k
 syntax BinderForExistentialTraitRef ::= binderForExistentialTraitRef(value: ExistentialTraitRef, boundVars: BoundVariableKindList)
-syntax MaybeBinderForExistentialTraitRef ::= someBinderForExistentialTraitRef(BinderForExistentialTraitRef)
-                                           | "noBinderForExistentialTraitRef"
-syntax GlobalAlloc ::= globalAllocFunction(Instance)
-                     | globalAllocVTable(Ty, MaybeBinderForExistentialTraitRef)
-                     | globalAllocStatic(StaticDef) [symbol(globalAllocStatic)]
-                     | globalAllocMemory(Allocation) [symbol(globalAllocMemory)]
-
-syntax GlobalAllocEntry ::= globalAllocEntry(MIRInt, GlobalAlloc) [symbol(globalAllocEntry)]
-syntax GlobalAllocsMap ::= List {GlobalAllocEntry, ""} [symbol(globalAllocsMap), terminator-symbol(.globalAllocsMap)]
+                                          [group(mir---value--bound-vars)]
+
+syntax MaybeBinderForExistentialTraitRef ::= someBinderForExistentialTraitRef(BinderForExistentialTraitRef) [group(mir-option)]
+                                           | "noBinderForExistentialTraitRef"                               [group(mir-option)]
+
+syntax GlobalAllocKind ::= globalAllocFunction(Instance)
+                             [group(mir-enum), symbol(GlobalAllocKind::Function)]
+                         | globalAllocVTable(Ty, MaybeBinderForExistentialTraitRef)
+                             [group(mir-enum), symbol(GlobalAllocKind::VTable)]
+                         | Static(StaticDef)
+                             [group(mir-enum), symbol(GlobalAllocKind::Static)]
+                         | Memory(Allocation)
+                             [group(mir-enum), symbol(GlobalAllocKind::Memory)]
+
+syntax GlobalAlloc ::= globalAllocEntry(MIRInt, GlobalAllocKind)
+         [symbol(globalAllocEntry), group(mir)]
+
+syntax GlobalAllocs ::= List {GlobalAlloc, ""}
+         [symbol(GlobalAllocs::append), terminator-symbol(GlobalAllocs::empty), group(mir-list)]
+
 syntax AllocId ::= allocId(Int) [symbol(allocId)]
 
 endmodule
-```
+```