Pull in changes to KEVM since project creation (#43)

* src/{kontrol,tests}: import changes in KEVM since last import * Set Version: 0.1.4 * src/tests/integratiion/test_foundry_prove: bring back upped recursion limit * src/tests/unit/test_solc_to_k: add unit test harness * .github/test-pr: disable failing if any in matrix fails * .github/test-pr: build haskell backend too * Set Version: 0.1.5 * kontrol/cli: update to latest KEVM foundry_test_args * Set Version: 0.1.7 --------- Co-authored-by: devops <[email protected]>
runtimeverification · Sep 26, 2023 · 9d6dbd3 · 9d6dbd3
1 parent a012b23
commit 9d6dbd3
Show file tree

Hide file tree

Showing 13 changed files with 1,424 additions and 212 deletions.
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -63,6 +63,7 @@ jobs:
     name: 'Profiling'
     runs-on: [self-hosted, linux, normal]
     strategy:
+      fail-fast: false
       matrix:
         backend: ['legacy', 'booster']
     timeout-minutes: 30
@@ -94,6 +95,7 @@ jobs:
     name: 'Integration Tests'
     runs-on: [self-hosted, linux, normal]
     strategy:
+      fail-fast: false
       matrix:
         backend: ['legacy', 'booster']
     timeout-minutes: 240
@@ -109,7 +111,7 @@ jobs:
       - name: 'Build KEVM'
         run: |
             docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'poetry install'
-            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kevm-dist --verbose build -j`nproc` plugin foundry'
+            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kevm-dist --verbose build -j`nproc` plugin haskell foundry'
       - name: 'Run integration tests'
         run: |
           TEST_ARGS=

diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.6
+0.1.7
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.6"
+version = "0.1.7"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py
@@ -1,9 +1,7 @@
 from __future__ import annotations
 
-import argparse
 import json
 import logging
-import re
 import sys
 from argparse import ArgumentParser
 from typing import TYPE_CHECKING
@@ -145,7 +143,7 @@ def exec_prove(
     max_depth: int = 1000,
     max_iterations: int | None = None,
     reinit: bool = False,
-    tests: Iterable[tuple[str, str | None]] = (),
+    tests: Iterable[tuple[str, int | None]] = (),
     exclude_tests: Iterable[str] = (),
     workers: int = 1,
     simplify_init: bool = True,
@@ -218,7 +216,7 @@ def exec_prove(
 def exec_show(
     foundry_root: Path,
     test: str,
-    id: str | None,
+    version: int | None,
     nodes: Iterable[NodeIdLike] = (),
     node_deltas: Iterable[tuple[NodeIdLike, NodeIdLike]] = (),
     to_module: bool = False,
@@ -234,7 +232,7 @@ def exec_show(
     output = foundry_show(
         foundry_root=foundry_root,
         test=test,
-        id=id,
+        version=version,
         nodes=nodes,
         node_deltas=node_deltas,
         to_module=to_module,
@@ -249,18 +247,18 @@ def exec_show(
     print(output)
 
 
-def exec_to_dot(foundry_root: Path, test: str, id: str | None, **kwargs: Any) -> None:
-    foundry_to_dot(foundry_root=foundry_root, test=test, id=id)
+def exec_to_dot(foundry_root: Path, test: str, version: int | None, **kwargs: Any) -> None:
+    foundry_to_dot(foundry_root=foundry_root, test=test, version=version)
 
 
 def exec_list(foundry_root: Path, **kwargs: Any) -> None:
     stats = foundry_list(foundry_root=foundry_root)
     print('\n'.join(stats))
 
 
-def exec_view_kcfg(foundry_root: Path, test: str, id: str | None, **kwargs: Any) -> None:
+def exec_view_kcfg(foundry_root: Path, test: str, version: int | None, **kwargs: Any) -> None:
     foundry = Foundry(foundry_root)
-    test_id = foundry.get_test_id(test, id)
+    test_id = foundry.get_test_id(test, version)
     contract_name, _ = test_id.split('.')
     proof = foundry.get_apr_proof(test_id)
 
@@ -275,14 +273,14 @@ def _custom_view(elem: KCFGElem) -> Iterable[str]:
     viewer.run()
 
 
-def exec_remove_node(foundry_root: Path, test: str, node: NodeIdLike, id: str | None, **kwargs: Any) -> None:
-    foundry_remove_node(foundry_root=foundry_root, test=test, id=id, node=node)
+def exec_remove_node(foundry_root: Path, test: str, node: NodeIdLike, version: int | None, **kwargs: Any) -> None:
+    foundry_remove_node(foundry_root=foundry_root, test=test, version=version, node=node)
 
 
 def exec_simplify_node(
     foundry_root: Path,
     test: str,
-    id: str | None,
+    version: int | None,
     node: NodeIdLike,
     replace: bool = False,
     minimize: bool = True,
@@ -301,7 +299,7 @@ def exec_simplify_node(
     pretty_term = foundry_simplify_node(
         foundry_root=foundry_root,
         test=test,
-        id=id,
+        version=version,
         node=node,
         replace=replace,
         minimize=minimize,
@@ -317,7 +315,7 @@ def exec_simplify_node(
 def exec_step_node(
     foundry_root: Path,
     test: str,
-    id: str | None,
+    version: int | None,
     node: NodeIdLike,
     repeat: int = 1,
     depth: int = 1,
@@ -335,7 +333,7 @@ def exec_step_node(
     foundry_step_node(
         foundry_root=foundry_root,
         test=test,
-        id=id,
+        version=version,
         node=node,
         repeat=repeat,
         depth=depth,
@@ -349,17 +347,17 @@ def exec_step_node(
 def exec_merge_nodes(
     foundry_root: Path,
     test: str,
-    id: str | None,
+    version: int | None,
     nodes: Iterable[NodeIdLike],
     **kwargs: Any,
 ) -> None:
-    foundry_merge_nodes(foundry_root=foundry_root, node_ids=nodes, test=test, id=id)
+    foundry_merge_nodes(foundry_root=foundry_root, node_ids=nodes, test=test, version=version)
 
 
 def exec_section_edge(
     foundry_root: Path,
     test: str,
-    id: str | None,
+    version: int | None,
     edge: tuple[str, str],
     sections: int = 2,
     replace: bool = False,
@@ -377,7 +375,7 @@ def exec_section_edge(
     foundry_section_edge(
         foundry_root=foundry_root,
         test=test,
-        id=id,
+        version=version,
         edge=edge,
         sections=sections,
         replace=replace,
@@ -391,7 +389,7 @@ def exec_section_edge(
 def exec_get_model(
     foundry_root: Path,
     test: str,
-    id: str | None,
+    version: int | None,
     nodes: Iterable[NodeIdLike] = (),
     pending: bool = False,
     failing: bool = False,
@@ -400,7 +398,7 @@ def exec_get_model(
     output = foundry_get_model(
         foundry_root=foundry_root,
         test=test,
-        id=id,
+        version=version,
         nodes=nodes,
         pending=pending,
         failing=failing,
@@ -441,15 +439,12 @@ def parse(s: str) -> list[T]:
     solc_to_k_args.add_argument('contract_file', type=file_path, help='Path to contract file.')
     solc_to_k_args.add_argument('contract_name', type=str, help='Name of contract to generate K helpers for.')
 
-    def _parse_test_id_tuple(value: str) -> tuple[str, str | None]:
-        pattern = r'^([^,]+)(?:,\s*(\S+))?$'
-        match = re.match(pattern, value)
-
-        if match:
-            groups = match.groups()
-            return groups[0], groups[1] if groups[1] is not None else None
+    def _parse_test_version_tuple(value: str) -> tuple[str, int | None]:
+        if ':' in value:
+            test, version = value.split(':')
+            return (test, int(version))
         else:
-            raise argparse.ArgumentTypeError("Invalid tuple format. Expected 'test, id' or 'test'")
+            return (value, None)
 
     build = command_parser.add_parser(
         'build',
@@ -494,15 +489,15 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]:
     )
     prove_args.add_argument(
         '--test',
-        type=_parse_test_id_tuple,
+        type=_parse_test_version_tuple,
         dest='tests',
         default=[],
         action='append',
         help='Limit to only listed tests, ContractName.TestName',
     )
     prove_args.add_argument(
         '--exclude-test',
-        type=_parse_test_id_tuple,
+        type=_parse_test_version_tuple,
         dest='exclude_tests',
         default=[],
         action='append',

diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py
@@ -31,7 +31,7 @@ def foundry_args(self) -> ArgumentParser:
     def foundry_test_args(self) -> ArgumentParser:
         args = ArgumentParser(add_help=False)
         args.add_argument('test', type=str, help='Test to run')
-        args.add_argument('--id', type=str, default=None, required=False, help='ID of the test')
+        args.add_argument('--version', type=int, default=None, required=False, help='Version of the test to use')
         return args
 
     @cached_property