Add tests for K definitions (#39)

Author: tothtamas28

.github/workflows/test-pr.yml

@@ -39,7 +39,9 @@ jobs:
         uses: ./.github/actions/with-docker
         with:
           container-name: ${CONTAINER}
-      - name: 'Build and run integration tests'
+      - name: 'Build K definitions'
+        run: docker exec -u user ${CONTAINER} make kdist
+      - name: 'Run integration tests'
         run: docker exec -u user ${CONTAINER} make cov-integration
       - name: 'Tear down Docker container'
         if: always()

package/smoke-test.sh

@@ -4,7 +4,7 @@ set -euxo pipefail
 
 kimp --help
 
-kimp run --verbose examples/sumto10.imp --env 'x=0,y=1' --env z=2
+kimp run --verbose examples/sumto10.imp --env 'x=0,y=1' --env b1=false --env b2=true
 
 kimp prove --verbose examples/specs/imp-sum-spec.k IMP-SUM-SPEC sum-spec
 

src/kimp/__main__.py

@@ -132,7 +132,16 @@ def create_argument_parser() -> ArgumentParser:
 
     # Run
     def env(s: str) -> list[tuple[str, int]]:
-        return [(var.strip(), int(val)) for var, val in (assign.split('=') for assign in s.split(','))]
+        def parse(s: str) -> int:
+            match s:
+                case 'true':
+                    return True
+                case 'false':
+                    return False
+                case _:
+                    return int(s)
+
+        return [(var.strip(), parse(val)) for var, val in (assign.split('=') for assign in s.split(','))]
 
     run_subparser = command_parser.add_parser('run', help='Run an IMP program', parents=[shared_args])
     run_subparser.add_argument('input_file', metavar='INPUT_FILE', type=file_path, help='Path to .imp file')

src/kimp/kimp.py

@@ -182,15 +182,20 @@ def run(
         return llvm_interpret(definition_dir=self.dist.llvm_dir, pattern=pattern, depth=depth)
 
     def pattern(self, *, pgm: str, env: Mapping[str, int]) -> Pattern:
-        from pyk.kore.prelude import ID, INT, SORT_K_ITEM, inj, map_pattern, top_cell_initializer
+        from pyk.kore.prelude import BOOL, ID, INT, SORT_K_ITEM, bool_dv, inj, int_dv, map_pattern, top_cell_initializer
         from pyk.kore.syntax import DV, SortApp, String
 
+        def inj_dv(val: int) -> Pattern:
+            if isinstance(val, bool):
+                return inj(BOOL, SORT_K_ITEM, bool_dv(val))
+            return inj(INT, SORT_K_ITEM, int_dv(val))
+
         pgm_pattern = self.parse(pgm)
         env_pattern = map_pattern(
             *(
                 (
                     inj(ID, SORT_K_ITEM, DV(ID, String(var))),
-                    inj(INT, SORT_K_ITEM, DV(INT, String(str(val)))),
+                    inj_dv(val),
                 )
                 for var, val in env.items()
             )
@@ -203,20 +208,61 @@ def pattern(self, *, pgm: str, env: Mapping[str, int]) -> Pattern:
         )
 
     def parse(self, pgm: str) -> Pattern:
+        from subprocess import CalledProcessError
+
         from pyk.kore.parser import KoreParser
         from pyk.utils import run_process_2
 
         parser = self.dist.llvm_dir / 'parser_PGM'
         args = [str(parser), '/dev/stdin']
 
-        kore_text = run_process_2(args, input=pgm).stdout
+        try:
+            kore_text = run_process_2(args, input=pgm).stdout
+        except CalledProcessError as err:
+            raise ValueError(err.stderr) from err
+
         return KoreParser(kore_text).pattern()
 
     def pretty(self, pattern: Pattern, color: bool | None = None) -> str:
         from pyk.kore.tools import kore_print
 
         return kore_print(pattern, definition_dir=self.dist.llvm_dir, color=bool(color))
 
+    def env(self, pattern: Pattern) -> dict[str, int]:
+        import pyk.kore.match as km
+        from pyk.kore.prelude import BOOL, INT
+        from pyk.utils import case, chain
+
+        extract = (
+            chain
+            >> km.app("Lbl'-LT-'generatedTop'-GT-'")
+            >> km.arg("Lbl'-LT-'env'-GT-'")
+            >> km.arg(0)
+            >> km.kore_map_of(
+                key=chain >> km.inj >> km.kore_id,
+                value=chain
+                >> km.match_inj
+                >> case(
+                    (
+                        (
+                            lambda inj: inj.sorts[0] == BOOL,
+                            chain >> km.arg(0) >> km.kore_bool,
+                        ),
+                        (
+                            lambda inj: inj.sorts[0] == INT,
+                            chain >> km.arg(0) >> km.kore_int,
+                        ),
+                    )
+                ),
+            )
+        )
+
+        try:
+            return dict(extract(pattern))
+        except Exception as err:
+            pretty_pattern = self.pretty(pattern)
+            raise ValueError(f'Cannot extract environment from pattern:\n{pretty_pattern}') from err
+
     def debug(self, pattern: Pattern) -> Callable[[int | None], None]:
         """Return a closure that enables step-by-step debugging in a REPL.
 
@@ -227,12 +273,12 @@ def debug(self, pattern: Pattern) -> Callable[[int | None], None]:
             step()            # Run a single step
             step(1)           # Run a single step
             step(0)           # Just print the current configuration
-            step(bound=None)  # Run to completion
+            step(depth=None)  # Run to completion
         """
 
-        def step(bound: int | None = 1) -> None:
+        def step(depth: int | None = 1) -> None:
             nonlocal pattern
-            pattern = self.run(pattern, depth=bound)
+            pattern = self.run(pattern, depth=depth)
             print(self.pretty(pattern, color=True))
 
         return step

src/tests/integration/test_expr.py

@@ -0,0 +1,147 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING, Final
+
+import pytest
+from pyk.ktool.krun import llvm_interpret
+
+if TYPE_CHECKING:
+    from pathlib import Path
+
+    from pyk.kore.syntax import Pattern
+
+
+@pytest.fixture(scope='module')
+def definition_dir() -> Path:
+    from pyk.kdist import kdist
+
+    return kdist.get('imp-semantics.expr')
+
+
+TEST_DATA: Final = (
+    ('false', False),
+    ('true', True),
+    ('0', 0),
+    ('-1', -1),
+    ('--1', 1),
+    ('1 + 2', 3),
+    ('3 - 2', 1),
+    ('2 * 3', 6),
+    ('6 / 2', 3),
+    ('1 + 2 - 3', 0),
+    ('2 * 3 / 4', 1),
+    ('1 + 2 * 3', 7),
+    ('(1 + 2) * 3', 9),
+    ('0 == 0', True),
+    ('0 == 1', False),
+    ('true == true', True),
+    ('false == false', True),
+    ('true == false', False),
+    ('false == true', False),
+    ('1 >= 1', True),
+    ('1 > 1', False),
+    ('1 <= 1', True),
+    ('1 < 1', False),
+    ('0 < 1 == 1 < 2', True),
+    ('1 == 1 == true', True),
+    ('!true', False),
+    ('!false', True),
+    ('!!true', True),
+    ('!(1 > 2)', True),
+    ('false && true', False),
+    ('true && true', True),
+    ('true && 1', 1),
+    ('true || false', True),
+    ('false || false', False),
+    ('false || 1', 1),
+    ('1 > 2 && 1 == 1', False),
+    ('1 > 2 || 1 == 1', True),
+    ('true || false == false', True),
+    ('(true || false) == false', False),
+)
+
+
+@pytest.mark.parametrize('text,expected', TEST_DATA, ids=[test_id for test_id, _ in TEST_DATA])
+def test_expr(
+    text: str,
+    expected: int | bool,
+    definition_dir: Path,
+) -> None:
+    # When
+    pgm = parse(definition_dir, text)
+    pattern = config(pgm)
+    result = llvm_interpret(definition_dir, pattern)
+    actual = extract(definition_dir, result)
+
+    # Then
+    assert actual == expected
+
+
+def parse(definition_dir: Path, text: str) -> Pattern:
+    from subprocess import CalledProcessError
+
+    from pyk.kore.parser import KoreParser
+    from pyk.utils import run_process_2
+
+    parser = definition_dir / 'parser_PGM'
+    args = [str(parser), '/dev/stdin']
+
+    try:
+        kore_text = run_process_2(args, input=text).stdout
+    except CalledProcessError as err:
+        raise ValueError(err.stderr) from err
+
+    return KoreParser(kore_text).pattern()
+
+
+def config(pgm: Pattern) -> Pattern:
+    from pyk.kore.prelude import SORT_K_ITEM, inj, top_cell_initializer
+    from pyk.kore.syntax import SortApp
+
+    return top_cell_initializer(
+        {
+            '$PGM': inj(SortApp('SortExpr'), SORT_K_ITEM, pgm),
+        }
+    )
+
+
+def extract(definition_dir: Path, pattern: Pattern) -> int | bool:
+    from pyk.kore.syntax import DV, App, String
+
+    match pattern:
+        case App(
+            "Lbl'-LT-'generatedTop'-GT-'",
+            args=(
+                App(
+                    "Lbl'-LT-'k'-GT-'",
+                    args=(
+                        App(
+                            'kseq',
+                            args=(
+                                App('inj', args=(DV(value=String(res)),)),
+                                App('dotk'),
+                            ),
+                        ),
+                    ),
+                ),
+                *_,
+            ),
+        ):
+            try:
+                return int(res)
+            except Exception:
+                pass
+            match res:
+                case 'true':
+                    return True
+                case 'false':
+                    return False
+
+    pretty_pattern = pretty(definition_dir, pattern)
+    raise ValueError(f'Cannot extract result from pattern:\n{pretty_pattern}')
+
+
+def pretty(definition_dir: Path, pattern: Pattern) -> str:
+    from pyk.kore.tools import kore_print
+
+    return kore_print(pattern, definition_dir=definition_dir)

src/tests/integration/test_imp.py

@@ -0,0 +1,47 @@
+from __future__ import annotations
+
+from itertools import count
+from typing import TYPE_CHECKING
+
+import pytest
+
+from kimp import KImp
+
+if TYPE_CHECKING:
+    from typing import Final
+
+    Env = dict[str, int]
+
+
+TEST_DATA: Final[tuple[tuple[Env, str, Env], ...]] = (
+    ({}, '{}', {}),
+    ({'x': 0}, '{}', {'x': 0}),
+    ({}, 'x = 1;', {'x': 1}),
+    ({}, 'x = 1 + 1;', {'x': 2}),
+    ({'x': 0}, 'x = 1;', {'x': 1}),
+    ({'x': 0, 'y': 1}, 'x = y;', {'x': 1, 'y': 1}),
+    ({'x': 1}, 'x = false;', {'x': False}),
+    ({}, '{ x = 0; }', {'x': 0}),
+    ({}, 'x = 0; x = 1;', {'x': 1}),
+    ({}, 'x = 0; y = 1;', {'x': 0, 'y': 1}),
+    ({'x': 0, 'y': 1}, 'z = x; x = y; y = z;', {'x': 1, 'y': 0, 'z': 0}),
+    ({'b': True}, 'if (b) x = 1;', {'b': True, 'x': 1}),
+    ({'b': False}, 'if (b) x = 1;', {'b': False}),
+    ({'b': True}, 'if (b) x = 1; else x = 2;', {'b': True, 'x': 1}),
+    ({'b': False}, 'if (b) x = 1; else x = 2;', {'b': False, 'x': 2}),
+    ({'x': 2}, 'while (x > 0) x = x - 1;', {'x': 0}),
+)
+
+
+@pytest.mark.parametrize('env,pgm,expected', TEST_DATA, ids=count())
+def test_kimp(env: Env, pgm: str, expected: Env) -> None:
+    # Given
+    kimp = KImp()
+
+    # When
+    pattern = kimp.pattern(pgm=pgm, env=env)
+    result = kimp.run(pattern, depth=1000)
+    actual = kimp.env(result)
+
+    # Then
+    assert actual == expected