From 233b1e696ee6d33231d05bbbd03e1e41c39efe44 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 4 Dec 2024 10:45:44 +0100 Subject: [PATCH] Add tests for K definitions (#39) --- .github/workflows/test-pr.yml | 4 +- package/smoke-test.sh | 2 +- src/kimp/__main__.py | 11 +- src/kimp/kimp.py | 58 ++++++++- src/tests/integration/test_expr.py | 147 ++++++++++++++++++++++ src/tests/integration/test_imp.py | 47 +++++++ src/tests/integration/test_integration.py | 2 - 7 files changed, 260 insertions(+), 11 deletions(-) create mode 100644 src/tests/integration/test_expr.py create mode 100644 src/tests/integration/test_imp.py delete mode 100644 src/tests/integration/test_integration.py diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index 6a71050..b817c0c 100644 --- a/.github/workflows/test-pr.yml +++ b/.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() diff --git a/package/smoke-test.sh b/package/smoke-test.sh index 69a4ca1..63cf629 100755 --- a/package/smoke-test.sh +++ b/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 diff --git a/src/kimp/__main__.py b/src/kimp/__main__.py index 5278870..70cd06d 100644 --- a/src/kimp/__main__.py +++ b/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') diff --git a/src/kimp/kimp.py b/src/kimp/kimp.py index ef1441a..9a087c6 100644 --- a/src/kimp/kimp.py +++ b/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,13 +208,19 @@ 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: @@ -217,6 +228,41 @@ def pretty(self, pattern: Pattern, color: bool | None = None) -> str: 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 diff --git a/src/tests/integration/test_expr.py b/src/tests/integration/test_expr.py new file mode 100644 index 0000000..d73ad24 --- /dev/null +++ b/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) diff --git a/src/tests/integration/test_imp.py b/src/tests/integration/test_imp.py new file mode 100644 index 0000000..1d2c95b --- /dev/null +++ b/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 diff --git a/src/tests/integration/test_integration.py b/src/tests/integration/test_integration.py deleted file mode 100644 index c51c3eb..0000000 --- a/src/tests/integration/test_integration.py +++ /dev/null @@ -1,2 +0,0 @@ -def test() -> None: - assert True