runtimeverification / runtimeverification/kontrol
Handle `DefinitionPatternError` gracefully in Kontrol
Nobody has claimed this yet.
- Dominant language
- Python
- Stars
- 122
- Forks
- 16
- PR merge metrics
- No merged PRs in 30d
Description
Running poetry -C kevm-pyk run kontrol prove ... with lemmas that cause DefinitionPatternError in the booster backend throws a PID still exists but it's a zombie error that does not describe the root cause of the issue:
Running functions: ['...']
[Info#proxy] Loading definition from ../test-forge-args/out/kompiled/definition.kore, main module "FOUNDRY-MAIN"
kore-rpc-booster: DefinitionPatternError (Located (Location {file = FileSource "/Users/personal/k/test-forge-args/out/kompiled/requires/lemmas.k", position = Position {line = 132, column = 10}})) (PredicateExpected (KJDV {sort = SortApp {name = Id {getId = "SortBool"}, args = []}, value = "true"}))
CallStack (from HasCallStack):
error, called at tools/booster/Server.hs:115:52 in main:Main
Traceback (most recent call last):
File "/Users/personal/Library/Caches/pypoetry/virtualenvs/kontrol-XPmevNL1-py3.11/lib/python3.11/site-packages/psutil/_psosx.py", line 346, in wrapper
return fun(self, *args, **kwargs)
^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/Users/personal/Library/Caches/pypoetry/virtualenvs/kontrol-XPmevNL1-py3.11/lib/python3.11/site-packages/psutil/_psosx.py", line 503, in connections
rawlist = cext.proc_connections(self.pid, families, types)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
ProcessLookupError: [Errno 3] No such process (originated from proc_pidinfo(PROC_PIDLISTFDS) 1/2)
During handling of the above exception, another exception occurred:
Traceback (most recent call last):
File "<string>", line 1, in <module>
File "/Users/personal/k/kontrol/src/kontrol/__main__.py", line 87, in main
execute(**vars(args))
File "/Users/personal/k/kontrol/src/kontrol/__main__.py", line 254, in exec_prove
results = foundry_prove(
^^^^^^^^^^^^^^
File "/Users/personal/k/kontrol/src/kontrol/prove.py", line 102, in foundry_prove
results = run_prover(setup_method_tests)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/Users/personal/k/kontrol/src/kontrol/prove.py", line 87, in run_prover
return _run_cfg_group(
^^^^^^^^^^^^^^^
File "/Users/personal/k/kontrol/src/kontrol/prove.py", line 229, in _run_cfg_group
apr_proofs.append(init_and_run_proof(test))
^^^^^^^^^^^^^^^^^^^^^^^^
File "/Users/personal/k/kontrol/src/kontrol/prove.py", line 187, in init_and_run_proof
with legacy_explore(
File "/opt/homebrew/Cellar/python@3.11/3.11.6/Frameworks/Python.framework/Versions/3.11/lib/python3.11/contextlib.py", line 137, in __enter__
return next(self.gen)
^^^^^^^^^^^^^^
File "/Users/personal/k/evm-semantics/kevm-pyk/src/kevm_pyk/utils.py", line 318, in legacy_explore
with kore_server(
^^^^^^^^^^^^
File "/Users/personal/Library/Caches/pypoetry/virtualenvs/kontrol-XPmevNL1-py3.11/lib/python3.11/site-packages/pyk/kore/rpc.py", line 1111, in kore_server
return BoosterServer(
^^^^^^^^^^^^^^
File "/Users/personal/Library/Caches/pypoetry/virtualenvs/kontrol-XPmevNL1-py3.11/lib/python3.11/site-packages/pyk/kore/rpc.py", line 1070, in __init__
super().__init__(
File "/Users/personal/Library/Caches/pypoetry/virtualenvs/kontrol-XPmevNL1-py3.11/lib/python3.11/site-packages/pyk/kore/rpc.py", line 961, in __init__
self._host, self._port = self._get_host_and_port(self._pid)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/Users/personal/Library/Caches/pypoetry/virtualenvs/kontrol-XPmevNL1-py3.11/lib/python3.11/site-packages/pyk/kore/rpc.py", line 988, in _get_host_and_port
while not proc.connections():
^^^^^^^^^^^^^^^^^^
File "/Users/personal/Library/Caches/pypoetry/virtualenvs/kontrol-XPmevNL1-py3.11/lib/python3.11/site-packages/psutil/__init__.py", line 1171, in connections
return self._proc.connections(kind)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/Users/personal/Library/Caches/pypoetry/virtualenvs/kontrol-XPmevNL1-py3.11/lib/python3.11/site-packages/psutil/_psosx.py", line 349, in wrapper
raise ZombieProcess(self.pid, self._name, self._ppid)
psutil.ZombieProcess: PID still exists but it's a zombie (pid=98113)
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Reproduce the poetry -C kevm-pyk run kontrol prove ... case, then start from src/kontrol/__main__.py, src/kontrol/prove.py, and the legacy_explore call in kevm_pyk/utils.py. Trace the booster startup path shown in the traceback; done means a DefinitionPatternError reports its root cause instead of surfacing PID still exists but it's a zombie.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- python
- Domain
- backend, cli
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 45/100