test failure: core-domain-numeric-apron-pkgrid_polyhedra_lin_congruences

[OnlyOneCannolo]

I made a Dockerfile to build for ubuntu:xenial and ubuntu:bionic. The xenial build works fine, but the bionic test suite fails.

      Start 30: core-domain-numeric-apron-pkgrid_polyhedra_lin_congruences
30/61 Test #30: core-domain-numeric-apron-pkgrid_polyhedra_lin_congruences ...***Failed    0.01 sec
Running 17 test cases...
unknown location(0): fatal error: in "is_top_and_bottom": memory access violation at address: 0x00000088: no mapping at fault address
/home/ikos/core/test/unit/domain/numeric/apron/pkgrid_polyhedra_lin_congruences.cpp(71): last checkpoint

*** 1 failure is detected in the test module "test_apron_pkgrid_polyhedra_lin_congruences"

...

98% tests passed, 1 tests failed out of 61

Total Test time (real) =  26.23 sec

The following tests FAILED:
	 30 - core-domain-numeric-apron-pkgrid_polyhedra_lin_congruences (Failed)
Errors while running CTest
CMakeFiles/check.dir/build.make:57: recipe for target 'CMakeFiles/check' failed
make[3]: *** [CMakeFiles/check] Error 8
CMakeFiles/Makefile2:101: recipe for target 'CMakeFiles/check.dir/all' failed
make[2]: *** [CMakeFiles/check.dir/all] Error 2
CMakeFiles/Makefile2:108: recipe for target 'CMakeFiles/check.dir/rule' failed
make[1]: *** [CMakeFiles/check.dir/rule] Error 2
Makefile:188: recipe for target 'check' failed
make: *** [check] Error 2

This is my Dockerfile, which I build with docker build --pull --rm --tag ikos --build-arg ubuntu_version='bionic' . from a directory containinig the Dockerfile.

# ubuntu_version=bionic
# ubuntu_version=xenial
ARG ubuntu_version
FROM ubuntu:$ubuntu_version
ARG ubuntu_version

# - git: to clone the repository directly from github.
# - libapron-dev: to enable the Apron features.
# - wget, gnupg: to add the llvm package repository.
RUN \
    apt-get update -y \
    && apt-get upgrade -y \
    && apt-get install -y \
        gcc \
        g++ \
        cmake \
        libgmp-dev \
        libboost-dev \
        libboost-filesystem-dev \
        libboost-test-dev \
        python \
        python-pygments \
        libsqlite3-dev \
        libz-dev \
        libedit-dev \
        libapron-dev \
        wget \
        gnupg

# - llvm-7-tools: for FileCheck.
# - lld-7: for lld.
RUN \
    echo "deb http://apt.llvm.org/$ubuntu_version/ llvm-toolchain-$ubuntu_version-7 main" | tee -a /etc/apt/sources.list \
    && wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add - \
    && apt-get update -y \
    && apt-get install -y \
        llvm-7 \
        llvm-7-dev \
        clang-7 \
        llvm-7-tools \
        lld-7

WORKDIR /home
RUN \
    apt-get install -y git \
    && git clone https://github.com/NASA-SW-VnV/ikos.git

# Make the install directory.
WORKDIR /home/ikos/install
WORKDIR /home/ikos/build
# Change the default linker to lld to enable some ikos tests.
RUN \
    rm /usr/bin/ld \
    && ln -s /usr/bin/ld.lld-7 /usr/bin/ld \
    && cmake \
        -DCMAKE_INSTALL_PREFIX=/home/ikos/install \
        -DLLVM_CONFIG_EXECUTABLE=/usr/lib/llvm-7/bin/llvm-config \
        -DAPRON_ROOT=/usr \
        .. \
    && make -j$(nproc)

# Increase verbosity on failure.
RUN make CTEST_OUTPUT_ON_FAILURE='ON' check -j$(nproc)

# Prepend utf-8 encoding directive to fix bug that occurs when relocating the installation directory contents.
RUN \
    make install \
    && printf '# coding: utf-8\n%s' "$(cat /home/ikos/install/lib/python2.7/site-packages/ikos/abs_int.py)" > /home/ikos/install/lib/python2.7/site-packages/ikos/abs_int.py

[arthaud]

Hi @OnlyOneCannolo,

This is a bug in the APRON library.

It has been fixed upstream. See https://gforge.inria.fr/scm/viewvc.php/apron?view=revision&revision=594

I opened an issue on the Ubuntu bug tracker a few months ago. I was hoping they could patch the package, but I didn't get any answer. See https://bugs.launchpad.net/ubuntu/+source/apron/+bug/1800041 If you add a comment saying that you are experiencing the same issue, they might take a look at it, who knows..

By the way, APRON is optional in IKOS. This bug only shows up if you try to use ikos -d=apron-pkgrid-polyhedra-lin-cong [...]

[OnlyOneCannolo]

I submitted feedback in the Ubuntu bug tracker, and the status changed to reflect that the bug affects multiple people.

I know that APRON is optional, but I'd like to use it. For now, I'll build it from source.

Thank you for looking into this.

[ivanperez-keera]

I'm following up on this.

libapron has been removed from Ubuntu (see https://packages.ubuntu.com/search?keywords=apron&searchon=names&suite=all&section=all) and Debian (https://packages.debian.org/search?searchon=names&keywords=libapron).

The issue on launchpad remains open and confirmed, but nobody acted on this in years.

There have been further releases of apron (I see that the latest version available is 0.9.14 but the latest in Ubuntu is 0.9.10: https://github.com/antoinemine/apron).

What would be the right course of action here? I see at least two options: a) Tell people to compile libapron by hand. b) Tell Ubuntu to repackage an up-to-date version of libapron.

Also, we might want to point out that ikos needs a version of libapron strictly higher than 0.9.10 to avoid running into this bug.

[arthaud]

I think we could give instructions to build APRON from source.

[ivanperez-keera]

For the record, the library was removed from Debian and consequently Ubuntu. Here was the request:

https://lists.debian.org/debian-ocaml-maint/2021/12/msg00065.html

The person who submitted that request for removal has a point. The last release of Apron included in Debian, 0.9.10, was made in 2009. There's new activity in the repo, though. I've ping the debian people to see what's up with that.

[ivanperez-keera]

Note that we also provide a brew formula for Apron ourselves: https://github.com/NASA-SW-VnV/homebrew-core/blob/master/Formula/apron.rb.

However, that formula picks Apron 0.9.10. We could update it to install a newer release: https://github.com/antoinemine/apron/releases.

[ivanperez-keera]

I've added a draft PR that adds an entry to the TROUBLESHOOTING.md document. I am reticent to add more direct instructions regarding APRON in the README (https://github.com/NASA-SW-VnV/ikos#installation) because those instructions are minimal and I would not want to pollute them too much. Also, if we upgrade the Apron brew formula on our side, then those instructions should still work without changes.