Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Kast to kore segfault bug #233

Draft
wants to merge 4 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion package/version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.85
0.1.86
2 changes: 1 addition & 1 deletion poetry.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "kontrol"
version = "0.1.85"
version = "0.1.86"
description = "Foundry integration for KEVM"
authors = [
"Runtime Verification, Inc. <contact@runtimeverification.com>",
Expand Down
2 changes: 1 addition & 1 deletion src/kontrol/__init__.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,4 +5,4 @@
if TYPE_CHECKING:
from typing import Final

VERSION: Final = '0.1.85'
VERSION: Final = '0.1.86'
4 changes: 4 additions & 0 deletions src/kontrol/__main__.py
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
from __future__ import annotations

import faulthandler
import json
import logging
import sys
Expand Down Expand Up @@ -211,6 +212,9 @@ def exec_prove(
maude_port: int | None = None,
**kwargs: Any,
) -> None:

faulthandler.enable()

_ignore_arg(kwargs, 'main_module', f'--main-module: {kwargs["main_module"]}')
_ignore_arg(kwargs, 'syntax_module', f'--syntax-module: {kwargs["syntax_module"]}')
_ignore_arg(kwargs, 'definition_dir', f'--definition: {kwargs["definition_dir"]}')
Expand Down
2 changes: 2 additions & 0 deletions src/tests/integration/test-data/bug.json

Large diffs are not rendered by default.

18 changes: 17 additions & 1 deletion src/tests/integration/test_foundry_prove.py
Original file line number Diff line number Diff line change
Expand Up @@ -3,23 +3,26 @@
import sys
from distutils.dir_util import copy_tree
from typing import TYPE_CHECKING
import json

import pytest
from filelock import FileLock
from pyk.kore.rpc import kore_server
from pyk.proof import APRProof
from pyk.utils import run_process, single
from pyk.kast import KInner
from pyk.konvert import kast_to_kore

from kontrol.foundry import Foundry, foundry_merge_nodes, foundry_remove_node, foundry_show, foundry_step_node
from kontrol.kompile import foundry_kompile
from kontrol.options import ProveOptions, RPCOptions
from kontrol.prove import foundry_prove

from .utils import TEST_DATA_DIR
from pathlib import Path

if TYPE_CHECKING:
from collections.abc import Iterator
from pathlib import Path
from typing import Final

from pyk.kore.rpc import KoreServer
Expand Down Expand Up @@ -489,3 +492,16 @@ def test_foundry_init_code(test: str, foundry: Foundry, bug_report: BugReport |

# Then
assert_pass(test, single(prove_res))


def test_kast_to_kore_bug(
foundry: Foundry,
) -> None:

sys.setrecursionlimit(10**8)

bug_json = json.loads(Path(TEST_DATA_DIR / 'bug.json').read_text())

kast = KInner.from_dict(bug_json)

kore = kast_to_kore(foundry.kevm.definition, foundry.kevm.kompiled_kore, kast)
Loading