evaluate_function followed by Term.step causes segmentation fault

[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).

[Baltoli]

First note is that the GC fix in #945 addresses the monotonic memory consumption issue when the function evaluator is run in an infinite loop (if a call to free_all_gc_memory is added after the function is evaluated, similarly to the simplification routines).

[Baltoli]

The second note is that I can reproduce the issue with the exact same depth bounds on my machine; this suggests there's something consistently odd going on in the backend that - fortunately - isn't architecture or OS-specific. I'm going to work on turning the Python example into a C++ one that can be more easily debugged.