Skip to content

evaluate_function followed by Term.step causes segmentation fault #943

Open
@tothtamas28

Description

@tothtamas28

https://github.com/runtimeverification/pyk/actions/runs/7272674739/job/19815247058?pr=784

Reproduction script: test_evaluate.py.txt

Copy the file to the pyk repo root, then run

poetry run python3 test_evaluate.py

Output:

INFO:pyk.ktool.kompile:Running: kompile src/tests/integration/k-files/imp.k --emit-json --backend llvm --output-definition /tmp/tmp6hrgm03t/imp-kompiled
INFO:pyk.ktool.kompile:Completed in 5.169s with status 0: kompile src/tests/integration/k-files/imp.k --emit-json --backend llvm --output-definition /tmp/tmp6hrgm03t/imp-kompiled
INFO:pyk.kllvm.compiler:Compiling pythonast extension: _kllvm.cpython-310-x86_64-linux-gnu.so
INFO:pyk.kllvm.compiler:Running: llvm-kompile pythonast --python /home/ttoth/.cache/pypoetry/virtualenvs/pyk-YghnWhM2-py3.10/bin/python3 --python-output-dir /tmp/tmp6hrgm03t/imp-kompiled
INFO:pyk.kllvm.compiler:Completed in 4.834s with status 0: llvm-kompile pythonast --python /home/ttoth/.cache/pypoetry/virtualenvs/pyk-YghnWhM2-py3.10/bin/python3 --python-output-dir /tmp/tmp6hrgm03t/imp-kompiled
INFO:pyk.kllvm.compiler:Compiling python extension: _kllvm_runtime.cpython-310-x86_64-linux-gnu.so
INFO:pyk.kllvm.compiler:Running: llvm-kompile /tmp/tmp6hrgm03t/imp-kompiled/definition.kore /tmp/tmp6hrgm03t/imp-kompiled/dt python --python /home/ttoth/.cache/pypoetry/virtualenvs/pyk-YghnWhM2-py3.10/bin/python3
INFO:pyk.kllvm.compiler:Completed in 3.335s with status 0: llvm-kompile /tmp/tmp6hrgm03t/imp-kompiled/definition.kore /tmp/tmp6hrgm03t/imp-kompiled/dt python --python /home/ttoth/.cache/pypoetry/virtualenvs/pyk-YghnWhM2-py3.10/bin/python3
Fatal Python error: Segmentation fault

Current thread 0x00007fdbf640cb80 (most recent call first):
  File "/home/ttoth/git/pyk/test_evaluate.py", line 59 in <module>
[1]    300671 segmentation fault (core dumped)  poetry run python3 test_evaluate.py

On my machine, decreasing either of the two iteration bounds causes the issue to not surface. Accordingly, the bounds might require tweaking in other environments.

Additionally, evaluate_function, when run in an infinite loop, seems to exhibit the same monotonically increasing memory consumption as simplify_pattern (#922).

Metadata

Metadata

Assignees

No one assigned

    Labels

    bindingsLLVM backend bindings to other languagesbugSomething isn't working

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions