Unable to run kllvm integration tests

[nwatson22]

When trying to write new integration tests I came across an an issue where some of the tests were failing due to not being able to find a header file.

Steps to reproduce:

1. make test-integration

Expected result:

All integration tests pass

Actual result:

src/tests/integration/kllvm/test_internal_term.py crashes with error:

In file included from /nix/store/s8ban9mix34h309gnbiwbhn8qy34ijxw-llvm-backend-0/lib/kllvm/python_src/ast.cpp:4:
In file included from /home/noah/.cache/pypoetry/virtualenvs/pyk-4YNQRw3p-py3.10/lib/python3.10/site-packages/pybind11/include/pybind11/operators.h:12:
In file included from /home/noah/.cache/pypoetry/virtualenvs/pyk-4YNQRw3p-py3.10/lib/python3.10/site-packages/pybind11/include/pybind11/pybind11.h:13:
In file included from /home/noah/.cache/pypoetry/virtualenvs/pyk-4YNQRw3p-py3.10/lib/python3.10/site-packages/pybind11/include/pybind11/detail/class.h:12:
In file included from /home/noah/.cache/pypoetry/virtualenvs/pyk-4YNQRw3p-py3.10/lib/python3.10/site-packages/pybind11/include/pybind11/detail/../attr.h:13:
In file included from /home/noah/.cache/pypoetry/virtualenvs/pyk-4YNQRw3p-py3.10/lib/python3.10/site-packages/pybind11/include/pybind11/detail/common.h:266:
In file included from /usr/include/python3.10/Python.h:8:
/usr/include/python3.10/pyconfig.h:3:12: fatal error: 'x86_64-linux-gnu/python3.10/pyconfig.h' file not found
#  include <x86_64-linux-gnu/python3.10/pyconfig.h>
           ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1 error generated.

[ehildenb]

As far as I can tell, it only happens with kup-installed K.

[ehildenb]

The error I get:

[tothtamas28]

My guess is this is due to missing headers that on Ubuntu are shipped with python3-dev. @goodlyrottenapple, can you look into this?

[goodlyrottenapple]

@ehildenb i got your error because of missing python3-dev package. Afterwards I get the same error as described in the issue. The offending command

llvm-kompile pythonast --python /home/vagrant/.cache/pypoetry/virtualenvs/pyk-bTZ70AFp-py3.10/bin/python --python-output-dir /tmp/tmpufpmj025

fails when using poetry version of python. When I remove the --python flag, the command seems to work. Spoke to @Baltoli about this and he seems to think we maybe need to be querying some kind of include directory path if the --python flag is passed?

[tothtamas28]

When I remove the --python flag, the command seems to work

Is it possible the Python used with poetry is missing header files? You can check the path to the include directory with

$ poetry run python3 -c 'from distutils.sysconfig import get_python_inc; print(get_python_inc())'

The fact that providing the --python flag changes the result indicates that llvm-kompile is looking for an interpreter-specific include path, which is the right thing to do.

I'll do a few more tests in a clean VM.

[tothtamas28]

I'll do a few more tests in a clean VM.

On Ubuntu Jammy without python3-dev and with a pyenv-installed Python 3.10.

$ pyenv versions
* system (set by /root/.pyenv/version)
  3.10.11

With system Python:

$ rm -rf ~/.cache/pypoetry/
$ poetry env list
$ pyenv local system
$ pyenv versions
* system (set by /pyk/.python-version)
  3.10.11
$ poetry env use python3
Recreating virtualenv pyk-Zk7W7w5m-py3.10 in /root/.cache/pypoetry/virtualenvs/pyk-Zk7W7w5m-py3.10
Using virtualenv: /root/.cache/pypoetry/virtualenvs/pyk-Zk7W7w5m-py3.10
$ poetry run python --version
Python 3.10.6
$ poetry run python3 -c 'from distutils.sysconfig import get_python_inc; print(get_python_inc())'
/usr/include/python3.10
$ ls /usr/include/python3.10
ls: cannot access '/usr/include/python3.10': No such file or directory
$ make test-integration  # fails

Installing python3-dev solves the problem in this setup.

$ ls /usr/include/python3.10/
Python.h           compile.h              exports.h             interpreteridobject.h  namespaceobject.h  pyerrors.h     pystrcmp.h      token.h
abstract.h         complexobject.h        fileobject.h          intrcheck.h            object.h           pyexpat.h      pystrhex.h      traceback.h
bltinmodule.h      context.h              fileutils.h           iterobject.h           objimpl.h          pyframe.h      pystrtod.h      tracemalloc.h
boolobject.h       cpython                floatobject.h         listobject.h           opcode.h           pyhash.h       pythonrun.h     tupleobject.h
bytearrayobject.h  datetime.h             frameobject.h         longintrepr.h          osdefs.h           pylifecycle.h  pythread.h      typeslots.h
bytesobject.h      descrobject.h          funcobject.h          longobject.h           osmodule.h         pymacconfig.h  rangeobject.h   unicodeobject.h
cellobject.h       dictobject.h           genericaliasobject.h  marshal.h              patchlevel.h       pymacro.h      setobject.h     warnings.h
ceval.h            dynamic_annotations.h  genobject.h           memoryobject.h         py_curses.h        pymath.h       sliceobject.h   weakrefobject.h
classobject.h      enumobject.h           graminit.h            methodobject.h         pycapsule.h        pymem.h        structmember.h
code.h             errcode.h              import.h              modsupport.h           pyconfig.h         pyport.h       structseq.h
codecs.h           eval.h                 internal              moduleobject.h         pydtrace.h         pystate.h      sysmodule.h
$ make test-integration  # succeeds

With pyenv-installed Python:

$ rm -rf ~/.cache/pypoetry/
$ poetry env list
$ pyenv local 3.10
$ pyenv versions
  system
* 3.10.11 (set by /pyk/.python-version)
$ poetry env use python3
Creating virtualenv pyk-Zk7W7w5m-py3.10 in /root/.cache/pypoetry/virtualenvs
Using virtualenv: /root/.cache/pypoetry/virtualenvs/pyk-Zk7W7w5m-py3.10
$ poetry run python --version
Python 3.10.11
$ poetry run python3 -c 'from distutils.sysconfig import get_python_inc; print(get_python_inc())'
/root/.pyenv/versions/3.10.11/include/python3.10
$ ls /root/.pyenv/versions/3.10.11/include/python3.10
Python.h           compile.h              exports.h              intrcheck.h        object.h      pyexpat.h      pystrhex.h      traceback.h
abstract.h         complexobject.h        fileobject.h           iterobject.h       objimpl.h     pyframe.h      pystrtod.h      tracemalloc.h
bltinmodule.h      context.h              fileutils.h            listobject.h       opcode.h      pyhash.h       pythonrun.h     tupleobject.h
boolobject.h       cpython                floatobject.h          longintrepr.h      osdefs.h      pylifecycle.h  pythread.h      typeslots.h
bytearrayobject.h  datetime.h             frameobject.h          longobject.h       osmodule.h    pymacconfig.h  rangeobject.h   unicodeobject.h
bytesobject.h      descrobject.h          funcobject.h           marshal.h          patchlevel.h  pymacro.h      setobject.h     warnings.h
cellobject.h       dictobject.h           genericaliasobject.h   memoryobject.h     py_curses.h   pymath.h       sliceobject.h   weakrefobject.h
ceval.h            dynamic_annotations.h  genobject.h            methodobject.h     pycapsule.h   pymem.h        structmember.h
classobject.h      enumobject.h           import.h               modsupport.h       pyconfig.h    pyport.h       structseq.h
code.h             errcode.h              internal               moduleobject.h     pydtrace.h    pystate.h      sysmodule.h
codecs.h           eval.h                 interpreteridobject.h  namespaceobject.h  pyerrors.h    pystrcmp.h     token.h
$ make test-integration  # succeeds

So based on this it indeed looks like llvm-kompile looks for the right include folder. The most probable cause for error is header files missing from the right location.

[Baltoli]

I ran into this issue again today, and after some more digging the issue is that poetry projects need to be configured to use the correct version of Python; if they aren't then the various include paths used by the system / pyenv Python are not correct when using the Nix-supplied C++ compiler to build the Python binding modules.

Happily, it seems that Poetry is happy to be told to use the Python interpreter pointed to by the kup-installed K derivation with a command like:

$ poetry env use /nix/store/bc45k1n0pkrdkr3xa6w84w1xhkl1kkyp-python3-3.10.12/bin/python3 --no-cache

We should implement the following fixes:

• Have kup supply some way of telling us what the correct path in the Nix store is for Python.
• Have pyk give a friendlier error message when we see this error; perhaps validate arguments to the function that runs llvm-kompile - if there's nix in the path to the llvm-kompile binary, and not in the path to the supplied Python, and the call fails, suggest running the poetry env ... command above?

[tothtamas28]

Fixed in runtimeverification/k#3823:

$ poetry env use --no-cache $(k-which-python)