Skip to content

Commit 9937a4c

Browse files
jbertholdjberthold
committed
Merge remote-tracking branch 'origin/master' into array-index-writes
2 parents 62fa82d + 5c284d9 commit 9937a4c

10 files changed

Lines changed: 67 additions & 121 deletions

File tree

‎Makefile‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,14 @@
11
UV := uv --directory kmir
22
UV_RUN := $(UV) run
33

4+
PARALLEL := 4
5+
46
TOP_DIR := $(shell pwd)
57

68
default: check build
79

810
build:
9-
$(UV_RUN) kdist -v build mir-semantics\.* -j4
11+
$(UV_RUN) kdist -v build mir-semantics\.* -j$(PARALLEL)
1012

1113
.PHONY: test
1214
test: test-unit test-integration smir-parse-tests
@@ -46,7 +48,7 @@ test-unit:
4648

4749
test-integration: build
4850
$(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration --maxfail=1 --verbose \
49-
--durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS)
51+
--durations=0 --numprocesses=$(PARALLEL) --dist=worksteal $(TEST_ARGS)
5052

5153
# Checks and formatting
5254

‎kmir/src/kmir/__main__.py‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@
1111
from pyk.proof.reachability import APRProof, APRProver
1212
from pyk.proof.tui import APRProofViewer
1313

14-
from .build import HASKELL_DEF_DIR, LLVM_LIB_DIR, haskell_semantics, llvm_semantics
14+
from .build import HASKELL_DEF_DIR, LLVM_DEF_DIR, LLVM_LIB_DIR
1515
from .kmir import KMIR, KMIRAPRNodePrinter
1616
from .options import GenSpecOpts, ProvePruneOpts, ProveRSOpts, ProveRunOpts, ProveViewOpts, RunOpts
1717
from .parse.parser import parse_json
@@ -29,7 +29,7 @@
2929

3030

3131
def _kmir_run(opts: RunOpts) -> None:
32-
tools = haskell_semantics() if opts.haskell_backend else llvm_semantics()
32+
kmir = KMIR(HASKELL_DEF_DIR) if opts.haskell_backend else KMIR(LLVM_DEF_DIR)
3333

3434
smir_file: Path
3535
if opts.file:
@@ -39,16 +39,16 @@ def _kmir_run(opts: RunOpts) -> None:
3939
target = opts.bin if opts.bin else cargo.default_target
4040
smir_file = cargo.smir_for(target)
4141

42-
parse_result = parse_json(tools.definition, smir_file, 'Pgm')
42+
parse_result = parse_json(kmir.definition, smir_file, 'Pgm')
4343
if parse_result is None:
4444
print('Parse error!', file=sys.stderr)
4545
sys.exit(1)
4646

4747
kmir_kast, _ = parse_result
4848

49-
result = tools.run_parsed(kmir_kast, opts.start_symbol, opts.depth)
49+
result = kmir.run_parsed(kmir_kast, opts.start_symbol, opts.depth)
5050

51-
print(tools.kprint.kore_to_pretty(result))
51+
print(kmir.kore_to_pretty(result))
5252

5353

5454
def _kmir_prove_rs(opts: ProveRSOpts) -> None:

‎kmir/src/kmir/build.py‎

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -4,19 +4,9 @@
44

55
from pyk.kdist import kdist
66

7-
from .tools import Tools
8-
97
if TYPE_CHECKING:
108
from typing import Final
119

1210
LLVM_DEF_DIR: Final = kdist.which('mir-semantics.llvm')
1311
LLVM_LIB_DIR: Final = kdist.which('mir-semantics.llvm-library')
1412
HASKELL_DEF_DIR: Final = kdist.which('mir-semantics.haskell')
15-
16-
17-
def llvm_semantics() -> Tools:
18-
return Tools(LLVM_DEF_DIR)
19-
20-
21-
def haskell_semantics() -> Tools:
22-
return Tools(HASKELL_DEF_DIR)

‎kmir/src/kmir/kmir.py‎

Lines changed: 24 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,9 @@
66

77
from pyk.cli.utils import bug_report_arg
88
from pyk.cterm import CTerm, cterm_symbolic
9-
from pyk.kast.inner import KApply, KInner, KSequence, Subst
9+
from pyk.kast.inner import KApply, KInner, KSequence, KSort, Subst
1010
from pyk.kast.manip import split_config_from
11+
from pyk.kast.prelude.string import stringToken
1112
from pyk.kcfg import KCFG
1213
from pyk.kcfg.explore import KCFGExplore
1314
from pyk.kcfg.semantics import DefaultSemantics
@@ -17,23 +18,24 @@
1718
from pyk.proof.reachability import APRProof, APRProver
1819
from pyk.proof.show import APRProofNodePrinter
1920

21+
from .kparse import KParse
2022
from .parse.parser import Parser
2123
from .rust.cargo import cargo_get_smir_json
22-
from .tools import Tools
2324

2425
if TYPE_CHECKING:
2526
from collections.abc import Iterator
2627
from pathlib import Path
2728
from typing import Final
2829

30+
from pyk.kore.syntax import Pattern
2931
from pyk.utils import BugReport
3032

3133
from .options import ProveRSOpts
3234

3335
_LOGGER: Final = logging.getLogger(__name__)
3436

3537

36-
class KMIR(KProve, KRun):
38+
class KMIR(KProve, KRun, KParse):
3739
llvm_library_dir: Path | None
3840
bug_report: BugReport | None
3941

@@ -43,6 +45,7 @@ def __init__(
4345
self.bug_report = bug_report_arg(bug_report) if bug_report is not None else None
4446
KProve.__init__(self, definition_dir, bug_report=self.bug_report)
4547
KRun.__init__(self, definition_dir, bug_report=self.bug_report)
48+
KParse.__init__(self, definition_dir)
4649
self.llvm_library_dir = llvm_library_dir
4750

4851
class Symbols:
@@ -59,11 +62,27 @@ def kcfg_explore(self, label: str | None = None) -> Iterator[KCFGExplore]:
5962
) as cts:
6063
yield KCFGExplore(cts, kcfg_semantics=KMIRSemantics())
6164

65+
def make_init_config(
66+
self, parsed_smir: KInner, start_symbol: KInner | str = 'main', sort: str = 'GeneratedTopCell'
67+
) -> KInner:
68+
if isinstance(start_symbol, str):
69+
start_symbol = stringToken(start_symbol)
70+
71+
subst = Subst({'$PGM': parsed_smir, '$STARTSYM': start_symbol})
72+
init_config = subst.apply(self.definition.init_config(KSort(sort)))
73+
return init_config
74+
75+
def run_parsed(self, parsed_smir: KInner, start_symbol: KInner | str = 'main', depth: int | None = None) -> Pattern:
76+
init_config = self.make_init_config(parsed_smir, start_symbol)
77+
init_kore = self.kast_to_kore(init_config, KSort('GeneratedTopCell'))
78+
result = self.run_pattern(init_kore, depth=depth)
79+
80+
return result
81+
6282
def apr_proof_from_kast(
6383
self, id: str, kmir_kast: KInner, sort: str = 'GeneratedTopCell', proof_dir: Path | None = None
6484
) -> APRProof:
65-
tools = Tools(self.definition_dir)
66-
config = tools.make_init_config(kmir_kast, 'main', sort=sort)
85+
config = self.make_init_config(kmir_kast, 'main', sort=sort)
6786
config_with_cell_vars, _ = split_config_from(config)
6887

6988
lhs = CTerm(config)

‎kmir/src/kmir/kparse.py‎

Lines changed: 15 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,30 +2,41 @@
22

33
from pathlib import Path
44
from subprocess import CalledProcessError
5-
from typing import TYPE_CHECKING
5+
from typing import TYPE_CHECKING, Callable, Iterable
66

77
if TYPE_CHECKING:
88
from subprocess import CompletedProcess
99
from pyk.kore.syntax import Pattern
1010
from pyk.kast.inner import KInner
11+
from pyk.kast.outer import KFlatModule
12+
from pyk.kast.pretty import SymbolTable
13+
from pyk.utils import BugReport
1114

1215
from pyk.kore.parser import KoreParser
1316
from pyk.ktool.kprint import KPrint
1417
from pyk.utils import run_process
1518

1619

1720
class KParse(KPrint):
18-
command: str
21+
parser: str
1922

2023
def __init__(
2124
self,
2225
definition_dir: Path,
26+
use_directory: Path | None = None,
27+
bug_report: BugReport | None = None,
28+
extra_unparsing_modules: Iterable[KFlatModule] = (),
29+
patch_symbol_table: Callable[[SymbolTable], None] | None = None,
2330
command: str = 'kparse',
2431
):
2532
super().__init__(
2633
definition_dir,
34+
use_directory=use_directory,
35+
bug_report=bug_report,
36+
extra_unparsing_modules=extra_unparsing_modules,
37+
patch_symbol_table=patch_symbol_table,
2738
)
28-
self.command = command
39+
self.parser = command
2940

3041
def parse_process(
3142
self,
@@ -38,7 +49,7 @@ def parse_process(
3849
ntf.flush()
3950

4051
return _kparse(
41-
command=self.command,
52+
command=self.parser,
4253
input_file=Path(ntf.name),
4354
definition_dir=self.definition_dir,
4455
sort=sort,

‎kmir/src/kmir/parse/__main__.py‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@
22
import sys
33
from pathlib import Path
44

5-
from kmir.build import llvm_semantics
6-
5+
from ..build import LLVM_DEF_DIR
6+
from ..kmir import KMIR
77
from .parser import parse_json
88

99

@@ -17,13 +17,13 @@ def parse_args() -> argparse.Namespace:
1717
def main() -> None:
1818
sys.setrecursionlimit(10000000)
1919
args = parse_args()
20-
tools = llvm_semantics()
20+
kmir = KMIR(LLVM_DEF_DIR)
2121

22-
result = parse_json(tools.definition, Path(args.json), args.sort)
22+
result = parse_json(kmir.definition, Path(args.json), args.sort)
2323

2424
if result is None:
2525
print('Parse error!', file=sys.stderr)
2626
sys.exit(1)
2727

2828
term, _ = result
29-
print(tools.krun.pretty_print(term))
29+
print(kmir.pretty_print(term))

‎kmir/src/kmir/testing/__init__.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
from .fixtures import tools
1+

‎kmir/src/kmir/testing/fixtures.py‎

Lines changed: 1 addition & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,10 @@
11
from __future__ import annotations
22

3-
from typing import TYPE_CHECKING
4-
53
import pytest
64

7-
from kmir.build import HASKELL_DEF_DIR, LLVM_LIB_DIR, llvm_semantics
5+
from kmir.build import HASKELL_DEF_DIR, LLVM_LIB_DIR
86
from kmir.kmir import KMIR
97

10-
if TYPE_CHECKING:
11-
from kmir.tools import Tools
12-
13-
14-
@pytest.fixture
15-
def tools() -> Tools:
16-
return llvm_semantics()
17-
188

199
@pytest.fixture
2010
def kmir() -> KMIR:

‎kmir/src/kmir/tools.py‎

Lines changed: 0 additions & 65 deletions
This file was deleted.

0 commit comments

Comments
 (0)