Add profile test for kbuild (#487)

Measures profiling data for kompilation and rekompilation.

---------

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

Author: tothtamas28

.github/workflows/test-pr.yml

@@ -58,16 +58,28 @@ jobs:
   profile:
     needs: code-quality-checks
     name: 'Profiling'
-    runs-on: ubuntu-latest
+    runs-on: [self-hosted, linux, normal-ephemeral]
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
+      - name: 'Install Python'
+        uses: actions/setup-python@v4
+        with:
+          python-version: '3.10'
       - name: 'Install Poetry'
         uses: Gr1N/setup-poetry@v8
+      - name: 'Install K'
+        run: |
+          K_VERSION=$(cat deps/k_release)
+          DEB_PACKAGE_NAME=kframework_${K_VERSION}_amd64_ubuntu_jammy.deb
+          wget https://github.com/runtimeverification/k/releases/download/v${K_VERSION}/${DEB_PACKAGE_NAME}
+          sudo apt-get update
+          sudo apt-get -y install ./${DEB_PACKAGE_NAME}
+          kompile --version
       - name: 'Run profiling'
         run: |
           make profile
-          find /tmp/pytest-of-${USER}/pytest-current/ -type f | sort | xargs tail -n +1
+          find /tmp/pytest-of-${USER}/pytest-current/ -type f -name '*.prof' | sort | xargs tail -n +1
 
   integration-tests:
     needs: code-quality-checks

package/version

@@ -1 +1 @@
-0.1.329
+0.1.330

pyproject.toml

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

src/pyk/testing/_profiler.py

@@ -19,7 +19,7 @@ def __init__(self, tmp_path: Path):
     @contextmanager
     def __call__(
         self,
-        file_name: str = 'profile.txt',
+        file_name: str = 'profile.prof',
         *,
         sort_keys: Iterable[str | SortKey] = (),
         patterns: Iterable[str] = (),

src/tests/profiling/profile_kast_json.py

@@ -17,8 +17,8 @@ def test_kast_json(profile: Profiler) -> None:
     with json_file.open() as f:
         json_data = json.load(f)
 
-    with profile('profile-json-kast.txt', sort_keys=('cumtime',), limit=20):
+    with profile('json-to-kast.prof', sort_keys=('cumtime',), limit=20):
         kast: KAst = kast_term(json_data)
 
-    with profile('profile-kast-json.txt', sort_keys=('cumtime',), limit=20):
+    with profile('kast-to-json.prof', sort_keys=('cumtime',), limit=20):
         kast.to_dict()

src/tests/profiling/profile_kast_to_kore.py

@@ -22,18 +22,18 @@ def test_kast_to_kore(profile: Profiler) -> None:
 
     sys.setrecursionlimit(10**8)
 
-    with profile('init-kast-defn.txt', sort_keys=('cumtime',), limit=50):
+    with profile('init-kast-defn.prof', sort_keys=('cumtime',), limit=50):
         kast_defn = read_kast_definition(kast_defn_file)
 
-    with profile('init-kore-defn.txt', sort_keys=('cumtime',), limit=50):
+    with profile('init-kore-defn.prof', sort_keys=('cumtime',), limit=50):
         kore_defn = KompiledKore(kast_to_kore_dir)
         kore_defn.definition
 
     kast = KInner.from_json(kinner_file.read_text())
 
-    for file_name in ['kast-to-kore-1.txt', 'kast-to-kore-2.txt']:
+    for file_name in ['kast-to-kore-1.prof', 'kast-to-kore-2.prof']:
         with profile(file_name, sort_keys=('cumtime',), limit=25):
             kore = kast_to_kore(kast_defn, kore_defn, kast, sort=KSort('GeneratedTopCell'))
 
-    with profile('kore-to-kast.txt', sort_keys=('cumtime',), limit=25):
+    with profile('kore-to-kast.prof', sort_keys=('cumtime',), limit=25):
         kore_to_kast(kast_defn, kore)

src/tests/profiling/profile_kbuild.py

@@ -0,0 +1,33 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING
+
+import pytest
+
+from pyk.kbuild import KBuild, Package
+
+from .utils import TEST_DATA_DIR
+
+if TYPE_CHECKING:
+    from pathlib import Path
+    from typing import Final
+
+    from pyk.testing import Profiler
+
+
+A_SEMANTICS_DIR: Final = TEST_DATA_DIR / 'kbuild/a-semantics'
+
+
+@pytest.fixture
+def kbuild(tmp_path: Path) -> KBuild:
+    return KBuild(tmp_path / 'kbuild')
+
+
+def test_kbuild(kbuild: KBuild, profile: Profiler) -> None:
+    with profile('kompile.prof', sort_keys=('cumtime', 'tottime'), limit=35):
+        package = Package.create(A_SEMANTICS_DIR / 'kbuild.toml')
+        kbuild.kompile(package, 'llvm')
+
+    with profile('rekompile.prof', sort_keys=('cumtime', 'tottime'), limit=35):
+        package = Package.create(A_SEMANTICS_DIR / 'kbuild.toml')
+        kbuild.kompile(package, 'llvm')

src/tests/profiling/profile_kore_parse.py

@@ -18,5 +18,5 @@ def test_kore_parse(profile: Profiler) -> None:
 
     sys.setrecursionlimit(10**8)
 
-    with profile(sort_keys=('cumtime',), limit=50):
+    with profile('parse_kore.prof', sort_keys=('cumtime',), limit=50):
         parser.definition()

src/tests/profiling/test-data/kbuild/a-semantics/a.k

@@ -0,0 +1,10 @@
+requires "b-semantics/b.k"
+requires "c-semantics/c.k"
+
+module A-SYNTAX
+endmodule
+
+module A
+    imports B
+    imports C
+endmodule

src/tests/profiling/test-data/kbuild/a-semantics/kbuild.toml

@@ -0,0 +1,12 @@
+[project]
+name = "a-semantics"
+version = "0.1.0"
+source = "."
+
+[dependencies]
+b-semantics = { path = "../b-semantics" }
+c-semantics = { path = "../c-semantics" }
+
+[targets.llvm]
+main-file = 'a.k'
+backend='llvm'

src/tests/profiling/test-data/kbuild/b-semantics/b.k

@@ -0,0 +1,5 @@
+module B-SYNTAX
+endmodule
+
+module B
+endmodule

src/tests/profiling/test-data/kbuild/b-semantics/kbuild.toml

@@ -0,0 +1,4 @@
+[project]
+name = "b-semantics"
+version = "0.1.0"
+source = "."

src/tests/profiling/test-data/kbuild/c-semantics/c.k

@@ -0,0 +1,5 @@
+module C-SYNTAX
+endmodule
+
+module C
+endmodule

src/tests/profiling/test-data/kbuild/c-semantics/kbuild.toml

@@ -0,0 +1,4 @@
+[project]
+name = "c-semantics"
+version = "0.1.0"
+source = "."