Basic support for control flow (calls and returns without data) (#445)

* Various adaptations to `kmir.md` so that we can look up functions by
their type `Ty`
  - `functions` table is now keyed on `Ty` instead of `DefId`
  - `caller` and `currentFunc` fields likewise contain a `Ty`
- the `main` function is added to the functions table with `ty(-1)` key
to work around a shortfall of stable-mir-json:
runtimeverification/stable-mir-json#42
- various other adaptations and stub code to write function call
arguments to resp. local values
* A basic program where `main()` calls `a()`, which calls `b()`, which
calls `c()` is added as a first integration test
* The `#init` function is adapted to support executing functions other
than `main` (not tested yet)

---------

Co-authored-by: Guy Repta <[email protected]>

Author: jberthold

kmir/pyproject.toml

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

kmir/src/kmir/__init__.py

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

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

@@ -23,7 +23,7 @@ module KMIR-AST
                         | functionIntrinsic(Symbol) [symbol(FunctionKind::IntrinsicSym), group(mir-enum)]
                         | functionNoop(Symbol)      [symbol(FunctionKind::NoOpSym), group(mir-enum)]
 
-  syntax FunctionName ::= functionName(MIRInt, FunctionKind)
+  syntax FunctionName ::= functionName(Ty, FunctionKind)
                           [symbol(functionName), group(mir)]
 
   syntax FunctionNames ::= List [group(mir-klist-FunctionName)]

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

@@ -0,0 +1,19 @@
+Small tests for MIR execution
+-----------------------------
+
+The tests below this directory are intended to be run with `kmir run`, comparing the pretty-printed output to an expectation file.
+
+# To add a new test
+
+* Write a Rust test program `NAME.rs`
+* Generate stable-mir JSON `NAME.smir.json` for the test program (using `deps/stable-mir-pretty`)
+* run the program once to generate the expected output state
+  ```
+  /mir-semantics $ poetry -C kmir run -- kmir run path/to/NAME.smir.json > <path>/<to>/<NAME>.run.state
+  ```
+* check that the output is as expected
+* add test to `EXEC_DATA` array in `kmir/src/tests/integration/test_integration.py`
+* Several tests can be run from the same `NAME.smir.json` by varying the `--depth` parameter.
+
+
+Ideally, we should also keep the original `NAME.rs` program so we can later update the tests when/if the JSON format changes.

kmir/src/tests/integration/data/exec-smir/README.md

@@ -0,0 +1,11 @@
+fn main() {
+    a()
+}
+fn a() {
+    b()
+}
+fn b() {
+    c()
+}
+fn c() {
+}

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

@@ -0,0 +1 @@
+{"name":"main_a_b_c","crate_id":2129868149476588123,"allocs":[],"functions":[[14,{"NormalSym":"_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17he57786f330055d2dE"}],[25,{"NormalSym":"_ZN10main_a_b_c1a17hf96e7944faad0bd0E"}],[0,{"NormalSym":"_ZN3std2rt19lang_start_internal17h018b8394ba015d86E"}],[26,{"NormalSym":"_ZN10main_a_b_c1b17hbedf65f2538ce3adE"}],[23,{"NormalSym":"_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h88c62a39fb1b342bE"}],[21,{"NormalSym":"_ZN4core3ops8function6FnOnce9call_once17h5775674bf1184c46E"}],[27,{"NormalSym":"_ZN10main_a_b_c1c17h59101d2318335bbdE"}],[28,{"NoOpSym":""}],[19,{"NormalSym":"_ZN4core3ops8function6FnOnce9call_once17hde47e0bf03682721E"}],[20,{"IntrinsicSym":"black_box"}],[13,{"NormalSym":"_ZN3std3sys9backtrace28__rust_begin_short_backtrace17h98accbb0a20ea4f5E"}]],"uneval_consts":[],"items":[{"symbol_name":"_ZN10main_a_b_c1a17hf96e7944faad0bd0E","mono_item_kind":{"MonoItemFn":{"name":"a","id":7,"body":[{"blocks":[{"statements":[],"terminator":{"kind":{"Call":{"func":{"Constant":{"span":55,"user_ty":null,"const_":{"kind":"ZeroSized","ty":26,"id":10}}},"args":[],"destination":{"local":0,"projection":[]},"target":1,"unwind":"Continue"}},"span":56}},{"statements":[],"terminator":{"kind":"Return","span":57}}],"locals":[{"ty":1,"span":58,"mutability":"Mut"}],"arg_count":0,"var_debug_info":[],"spread_arg":null,"span":59}]}},"details":null},{"symbol_name":"_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17he57786f330055d2dE","mono_item_kind":{"MonoItemFn":{"name":"<() as std::process::Termination>::report","id":5,"body":[{"blocks":[{"statements":[{"kind":{"Assign":[{"local":0,"projection":[]},{"Use":{"Constant":{"span":46,"user_ty":null,"const_":{"kind":{"Allocated":{"bytes":[0],"provenance":{"ptrs":[]},"align":1,"mutability":"Mut"}},"ty":17,"id":8}}}}]},"span":46}],"terminator":{"kind":"Return","span":45}}],"locals":[{"ty":17,"span":47,"mutability":"Mut"},{"ty":1,"span":48,"mutability":"Not"}],"arg_count":1,"var_debug_info":[{"name":"self","source_info":{"span":48,"scope":0},"composite":null,"value":{"Const":{"span":32,"user_ty":null,"const_":{"kind":"ZeroSized","ty":1,"id":4}}},"argument_index":1}],"spread_arg":null,"span":49}]}},"details":null},{"symbol_name":"_ZN4core3ops8function6FnOnce40call_once$u7b$$u7b$vtable.shim$u7d$$u7d$17hba596ab1e21f4dfaE","mono_item_kind":{"MonoItemFn":{"name":"<{closure@std::rt::lang_start<()>::{closure#0}} as std::ops::FnOnce<()>>::call_once","id":3,"body":[{"blocks":[{"statements":[],"terminator":{"kind":{"Call":{"func":{"Constant":{"span":43,"user_ty":null,"const_":{"kind":"ZeroSized","ty":21,"id":6}}},"args":[{"Move":{"local":1,"projection":["Deref"]}},{"Move":{"local":2,"projection":[]}}],"destination":{"local":0,"projection":[]},"target":1,"unwind":"Continue"}},"span":43}},{"statements":[],"terminator":{"kind":"Return","span":43}}],"locals":[{"ty":16,"span":43,"mutability":"Mut"},{"ty":22,"span":43,"mutability":"Not"},{"ty":1,"span":43,"mutability":"Not"}],"arg_count":2,"var_debug_info":[],"spread_arg":2,"span":43}]}},"details":null},{"symbol_name":"_ZN3std3sys9backtrace28__rust_begin_short_backtrace17h98accbb0a20ea4f5E","mono_item_kind":{"MonoItemFn":{"name":"std::sys::backtrace::__rust_begin_short_backtrace::<fn(), ()>","id":2,"body":[{"blocks":[{"statements":[],"terminator":{"kind":{"Call":{"func":{"Constant":{"span":31,"user_ty":null,"const_":{"kind":"ZeroSized","ty":19,"id":3}}},"args":[{"Move":{"local":1,"projection":[]}},{"Constant":{"span":32,"user_ty":null,"const_":{"kind":"ZeroSized","ty":1,"id":4}}}],"destination":{"local":0,"projection":[]},"target":1,"unwind":"Continue"}},"span":33}},{"statements":[],"terminator":{"kind":{"Call":{"func":{"Constant":{"span":34,"user_ty":null,"const_":{"kind":"ZeroSized","ty":20,"id":5}}},"args":[{"Constant":{"span":32,"user_ty":null,"const_":{"kind":"ZeroSized","ty":1,"id":4}}}],"destination":{"local":2,"projection":[]},"target":2,"unwind":"Unreachable"}},"span":35}},{"statements":[],"terminator":{"kind":"Return","span":36}}],"locals":[{"ty":1,"span":37,"mutability":"Mut"},{"ty":7,"span":38,"mutability":"Not"},{"ty":1,"span":39,"mutability":"Not"}],"arg_count":1,"var_debug_info":[{"name":"f","source_info":{"span":38,"scope":0},"composite":null,"value":{"Place":{"local":1,"projection":[]}},"argument_index":1},{"name":"result","source_info":{"span":40,"scope":1},"composite":null,"value":{"Place":{"local":0,"projection":[]}},"argument_index":null},{"name":"dummy","source_info":{"span":41,"scope":2},"composite":null,"value":{"Const":{"span":32,"user_ty":null,"const_":{"kind":"ZeroSized","ty":1,"id":4}}},"argument_index":1}],"spread_arg":null,"span":42}]}},"details":null},{"symbol_name":"_ZN10main_a_b_c1c17h59101d2318335bbdE","mono_item_kind":{"MonoItemFn":{"name":"c","id":9,"body":[{"blocks":[{"statements":[],"terminator":{"kind":"Return","span":65}}],"locals":[{"ty":1,"span":66,"mutability":"Mut"}],"arg_count":0,"var_debug_info":[],"spread_arg":null,"span":67}]}},"details":null},{"symbol_name":"_ZN10main_a_b_c1b17hbedf65f2538ce3adE","mono_item_kind":{"MonoItemFn":{"name":"b","id":8,"body":[{"blocks":[{"statements":[],"terminator":{"kind":{"Call":{"func":{"Constant":{"span":60,"user_ty":null,"const_":{"kind":"ZeroSized","ty":27,"id":11}}},"args":[],"destination":{"local":0,"projection":[]},"target":1,"unwind":"Continue"}},"span":61}},{"statements":[],"terminator":{"kind":"Return","span":62}}],"locals":[{"ty":1,"span":63,"mutability":"Mut"}],"arg_count":0,"var_debug_info":[],"spread_arg":null,"span":64}]}},"details":null},{"symbol_name":"_ZN4core3ops8function6FnOnce9call_once17h5775674bf1184c46E","mono_item_kind":{"MonoItemFn":{"name":"<{closure@std::rt::lang_start<()>::{closure#0}} as std::ops::FnOnce<()>>::call_once","id":3,"body":[{"blocks":[{"statements":[{"kind":{"Assign":[{"local":3,"projection":[]},{"Ref":[{"kind":"ReErased"},{"Mut":{"kind":"Default"}},{"local":1,"projection":[]}]}]},"span":43}],"terminator":{"kind":{"Call":{"func":{"Constant":{"span":43,"user_ty":null,"const_":{"kind":"ZeroSized","ty":23,"id":7}}},"args":[{"Move":{"local":3,"projection":[]}},{"Move":{"local":2,"projection":[]}}],"destination":{"local":0,"projection":[]},"target":1,"unwind":{"Cleanup":3}}},"span":43}},{"statements":[],"terminator":{"kind":{"Drop":{"place":{"local":1,"projection":[]},"target":2,"unwind":"Continue"}},"span":43}},{"statements":[],"terminator":{"kind":"Return","span":43}},{"statements":[],"terminator":{"kind":{"Drop":{"place":{"local":1,"projection":[]},"target":4,"unwind":"Terminate"}},"span":43}},{"statements":[],"terminator":{"kind":"Resume","span":43}}],"locals":[{"ty":16,"span":43,"mutability":"Mut"},{"ty":12,"span":43,"mutability":"Not"},{"ty":1,"span":43,"mutability":"Not"},{"ty":24,"span":43,"mutability":"Not"}],"arg_count":2,"var_debug_info":[],"spread_arg":2,"span":43}]}},"details":null},{"symbol_name":"_ZN4core3ops8function6FnOnce9call_once17hde47e0bf03682721E","mono_item_kind":{"MonoItemFn":{"name":"<fn() as std::ops::FnOnce<()>>::call_once","id":3,"body":[{"blocks":[{"statements":[],"terminator":{"kind":{"Call":{"func":{"Move":{"local":1,"projection":[]}},"args":[],"destination":{"local":0,"projection":[]},"target":1,"unwind":"Continue"}},"span":43}},{"statements":[],"terminator":{"kind":"Return","span":43}}],"locals":[{"ty":1,"span":43,"mutability":"Mut"},{"ty":7,"span":43,"mutability":"Not"},{"ty":1,"span":43,"mutability":"Not"}],"arg_count":2,"var_debug_info":[],"spread_arg":2,"span":43}]}},"details":null},{"symbol_name":"_ZN3std2rt10lang_start17he509fe31442a28c4E","mono_item_kind":{"MonoItemFn":{"name":"std::rt::lang_start::<()>","id":0,"body":[{"blocks":[{"statements":[{"kind":{"StorageLive":5},"span":1},{"kind":{"StorageLive":6},"span":2},{"kind":{"StorageLive":8},"span":3},{"kind":{"Assign":[{"local":8,"projection":[]},{"Aggregate":[{"Closure":[1,[{"Type":1},{"Type":2},{"Type":3},{"Type":4}]]},[{"Copy":{"local":1,"projection":[]}}]]}]},"span":3},{"kind":{"Assign":[{"local":7,"projection":[]},{"Ref":[{"kind":"ReErased"},"Shared",{"local":8,"projection":[]}]}]},"span":2},{"kind":{"Assign":[{"local":6,"projection":[]},{"Cast":[{"PointerCoercion":"Unsize"},{"Copy":{"local":7,"projection":[]}},5]}]},"span":2}],"terminator":{"kind":{"Call":{"func":{"Constant":{"span":0,"user_ty":null,"const_":{"kind":"ZeroSized","ty":0,"id":0}}},"args":[{"Move":{"local":6,"projection":[]}},{"Move":{"local":2,"projection":[]}},{"Move":{"local":3,"projection":[]}},{"Move":{"local":4,"projection":[]}}],"destination":{"local":5,"projection":[]},"target":1,"unwind":"Continue"}},"span":1}},{"statements":[{"kind":{"StorageDead":6},"span":5},{"kind":{"Assign":[{"local":0,"projection":[]},{"Use":{"Copy":{"local":5,"projection":[{"Downcast":0},{"Field":[0,6]}]}}}]},"span":6},{"kind":{"StorageDead":8},"span":7},{"kind":{"StorageDead":5},"span":7}],"terminator":{"kind":"Return","span":4}}],"locals":[{"ty":6,"span":8,"mutability":"Mut"},{"ty":7,"span":9,"mutability":"Not"},{"ty":6,"span":10,"mutability":"Not"},{"ty":8,"span":11,"mutability":"Not"},{"ty":9,"span":12,"mutability":"Not"},{"ty":10,"span":1,"mutability":"Mut"},{"ty":5,"span":2,"mutability":"Mut"},{"ty":11,"span":2,"mutability":"Not"},{"ty":12,"span":3,"mutability":"Not"}],"arg_count":4,"var_debug_info":[{"name":"main","source_info":{"span":9,"scope":0},"composite":null,"value":{"Place":{"local":1,"projection":[]}},"argument_index":1},{"name":"argc","source_info":{"span":10,"scope":0},"composite":null,"value":{"Place":{"local":2,"projection":[]}},"argument_index":2},{"name":"argv","source_info":{"span":11,"scope":0},"composite":null,"value":{"Place":{"local":3,"projection":[]}},"argument_index":3},{"name":"sigpipe","source_info":{"span":12,"scope":0},"composite":null,"value":{"Place":{"local":4,"projection":[]}},"argument_index":4},{"name":"v","source_info":{"span":6,"scope":1},"composite":null,"value":{"Place":{"local":0,"projection":[]}},"argument_index":null}],"spread_arg":null,"span":13}]}},"details":null},{"symbol_name":"_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h88c62a39fb1b342bE","mono_item_kind":{"MonoItemFn":{"name":"std::rt::lang_start::<()>::{closure#0}","id":1,"body":[{"blocks":[{"statements":[{"kind":{"StorageLive":2},"span":16},{"kind":{"StorageLive":3},"span":15},{"kind":{"StorageLive":4},"span":17},{"kind":{"Assign":[{"local":4,"projection":[]},{"Use":{"Copy":{"local":1,"projection":["Deref",{"Field":[0,7]}]}}}]},"span":17}],"terminator":{"kind":{"Call":{"func":{"Constant":{"span":14,"user_ty":null,"const_":{"kind":"ZeroSized","ty":13,"id":1}}},"args":[{"Move":{"local":4,"projection":[]}}],"destination":{"local":3,"projection":[]},"target":1,"unwind":"Continue"}},"span":15}},{"statements":[{"kind":{"StorageDead":4},"span":19}],"terminator":{"kind":{"Call":{"func":{"Constant":{"span":18,"user_ty":null,"const_":{"kind":"ZeroSized","ty":14,"id":2}}},"args":[{"Move":{"local":3,"projection":[]}}],"destination":{"local":2,"projection":[]},"target":2,"unwind":"Continue"}},"span":16}},{"statements":[{"kind":{"StorageDead":3},"span":21},{"kind":{"StorageLive":5},"span":22},{"kind":{"Assign":[{"local":5,"projection":[]},{"Ref":[{"kind":"ReErased"},"Shared",{"local":2,"projection":[{"Field":[0,15]}]}]}]},"span":22},{"kind":{"StorageLive":6},"span":23},{"kind":{"Assign":[{"local":6,"projection":[]},{"Use":{"Copy":{"local":2,"projection":[{"Field":[0,15]},{"Field":[0,9]}]}}}]},"span":23},{"kind":{"Assign":[{"local":0,"projection":[]},{"Cast":["IntToInt",{"Move":{"local":6,"projection":[]}},16]}]},"span":24},{"kind":{"StorageDead":6},"span":25},{"kind":{"StorageDead":5},"span":26},{"kind":{"StorageDead":2},"span":27}],"terminator":{"kind":"Return","span":20}}],"locals":[{"ty":16,"span":28,"mutability":"Mut"},{"ty":11,"span":3,"mutability":"Mut"},{"ty":17,"span":16,"mutability":"Mut"},{"ty":1,"span":15,"mutability":"Mut"},{"ty":7,"span":17,"mutability":"Mut"},{"ty":18,"span":22,"mutability":"Mut"},{"ty":9,"span":23,"mutability":"Mut"}],"arg_count":1,"var_debug_info":[{"name":"main","source_info":{"span":9,"scope":0},"composite":null,"value":{"Place":{"local":1,"projection":["Deref",{"Field":[0,7]}]}},"argument_index":null},{"name":"self","source_info":{"span":29,"scope":1},"composite":null,"value":{"Place":{"local":2,"projection":[]}},"argument_index":1},{"name":"self","source_info":{"span":30,"scope":2},"composite":null,"value":{"Place":{"local":5,"projection":[]}},"argument_index":1}],"spread_arg":null,"span":3}]}},"details":null},{"symbol_name":"_ZN10main_a_b_c4main17hcaca459da1b06b9fE","mono_item_kind":{"MonoItemFn":{"name":"main","id":6,"body":[{"blocks":[{"statements":[],"terminator":{"kind":{"Call":{"func":{"Constant":{"span":50,"user_ty":null,"const_":{"kind":"ZeroSized","ty":25,"id":9}}},"args":[],"destination":{"local":0,"projection":[]},"target":1,"unwind":"Continue"}},"span":51}},{"statements":[],"terminator":{"kind":"Return","span":52}}],"locals":[{"ty":1,"span":53,"mutability":"Mut"}],"arg_count":0,"var_debug_info":[],"spread_arg":null,"span":54}]}},"details":null},{"symbol_name":"_ZN4core3ptr85drop_in_place$LT$std..rt..lang_start$LT$$LP$$RP$$GT$..$u7b$$u7b$closure$u7d$$u7d$$GT$17h651e2df3ec0dc2ccE","mono_item_kind":{"MonoItemFn":{"name":"std::ptr::drop_in_place::<{closure@std::rt::lang_start<()>::{closure#0}}>","id":4,"body":[{"blocks":[{"statements":[],"terminator":{"kind":"Return","span":44}}],"locals":[{"ty":1,"span":44,"mutability":"Mut"},{"ty":22,"span":44,"mutability":"Not"}],"arg_count":1,"var_debug_info":[],"spread_arg":null,"span":44}]}},"details":null}],"debug":null}

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

@@ -1,42 +1,42 @@
 ListItem(
   functionName(
-    114,
+    ty(114),
     functionNormalSym(symbol("_ZN4core3ptr42drop_in_place$LT$alloc..string..String$GT$17h1018ac0f9e0b0734E"))
   )
 )
 ListItem(
   functionName(
-    102,
+    ty(102),
     functionNoop(symbol(""))
   )
 )
 ListItem(
   functionName(
-    19,
+    ty(19),
     functionNormalSym(symbol("_ZN4core3ops8function6FnOnce9call_once17ha726c80bc9e6a2adE"))
   )
 )
 ListItem(
   functionName(
-    100,
+    ty(100),
     functionNormalSym(symbol("__rust_dealloc"))
   )
 )
 ListItem(
   functionName(
-    78,
+    ty(78),
     functionIntrinsic(symbol("volatile_load"))
   )
 )
 ListItem(
   functionName(
-    27,
+    ty(27),
     functionIntrinsic(symbol("ctpop"))
   )
 )
 ListItem(
   functionName(
-    109,
+    ty(109),
     functionNormalSym(symbol("_ZN10mainfoobar3bar17hc9f701b05bebc012E"))
   )
 )

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

@@ -5,7 +5,7 @@
 from typing import TYPE_CHECKING
 
 import pytest
-from pyk.kast.inner import KApply, KSort, KToken
+from pyk.kast.inner import KApply, KSort, KToken, Subst
 
 from kmir.convert_from_definition.v2parser import Parser
 
@@ -148,3 +148,53 @@ def test_schema_kapply_parse(
     json_data, expected_term, expected_sort = test_case
 
     assert parser.parse_mir_json(json_data, expected_sort.name) == (expected_term, expected_sort)
+
+
+EXEC_DATA_DIR = (Path(__file__).parent / 'data' / 'exec-smir').resolve(strict=True)
+EXEC_DATA = [
+    (
+        'main-a-b-c',
+        EXEC_DATA_DIR / 'main-a-b-c' / 'main-a-b-c.smir.json',
+        EXEC_DATA_DIR / 'main-a-b-c' / 'main-a-b-c.run.state',
+        None,
+    ),
+    (
+        'main-a-b-c --depth 15',
+        EXEC_DATA_DIR / 'main-a-b-c' / 'main-a-b-c.smir.json',
+        EXEC_DATA_DIR / 'main-a-b-c' / 'main-a-b-c.15.state',
+        15,
+    ),
+]
+
+
+@pytest.mark.parametrize(
+    'test_case',
+    EXEC_DATA,
+    ids=[name for (name, _, _, _) in EXEC_DATA],
+)
+def test_exec_smir(
+    test_case: tuple[str, Path, Path, int],
+    tools: Tools,
+) -> None:
+
+    (_, input_json, output_kast, depth) = test_case
+
+    parser = Parser(tools.definition)
+
+    with input_json.open('r') as f:
+        json_data = json.load(f)
+    parsed = parser.parse_mir_json(json_data, 'Pgm')
+    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)
+
+    with output_kast.open('r') as f:
+        expected = f.read().rstrip()
+
+    result_pretty = tools.kprint.kore_to_pretty(result).rstrip()
+
+    assert result_pretty == expected

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

@@ -1 +1 @@
-0.3.69
+0.3.70