djbsort

djbsort includes tools that, given an array size, automatically verify correctness of djbsort's output for all possible input arrays of that size. These tools have three parts:

The time to run the whole sequence of tools gradually increases with the array size. For array size 1024, running the whole sequence of tools to verify int32/avx2 version 20180729 takes about 143 seconds on one core of bolero, a 1.7GHz Intel Xeon E5-2609 v4 (Broadwell). About 76% of this time is for unroll, 14% for minmax, and 6% for decompose. The remaining time is spent simulating the intermediate programs to double-check that they sort a pseudorandom input.

Internally, the verifier has two components:

How to install angr and verify djbsort

djbsort has contributed various patches (see below) to angr. The following instructions rely on having a recent source version of angr that (1) includes some of the djbsort patches and (2) allows further djbsort patches, so you must install angr from source.

These instructions were tested on a virtual machine (created with xen-create-image) running the latest release ("unstable") of Debian.

As root, install various libraries and development packages:

    dpkg --add-architecture i386
    apt update
    apt dist-upgrade -y
    apt install \
      man wget strace psmisc screen vim time git tig \
      build-essential clang gdb valgrind nasm cmake \
      libffi-dev libssl-dev libxml2-dev libxslt1-dev \
      libreadline-dev libpixman-1-dev libqt4-dev \
      libglib2.0-dev python-dev python2.7-dev pypy \
      python3 python-pip virtualenvwrapper pypy-dev \
      libtool debootstrap debian-archive-keyring \
      binutils-multiarch libc6:i386 libgcc1:i386 \
      libstdc++6:i386 libtinfo5:i386 zlib1g:i386 \
      multiarch-support gcc-multilib \
      -y

As the user that compiled djbsort, install the latest version of angr:

    cd
    git clone https://github.com/angr/angr-dev.git
    cd angr-dev
    mkvirtualenv -p /usr/bin/pypy angr
    workon angr
    setsid -w sh -c ./setup.sh < /dev/null

The angr installation takes under 10 minutes and finishes with a comforting "All done!" announcement.

Apply the latest djbsort patches to angr:

    cd $HOME/angr-dev/claripy
    wget https://sorting.cr.yp.to/angrpatch4.txt
    patch -p1 < angrpatch4.txt

Run the verifymany script to verify sorting for all small sizes:

    workon angr
    pip install pyparsing
    cd
    version=$(cat sorting.cr.yp.to/djbsort-latest-version.txt)
    cd djbsort-$version/verif
    ./verifymany

The verifymany script stops with an error message if it encounters any failures.

The angr patches

Description of the patches contributed by djbsort to angr:


Version: This is version 2018.07.29 of the "Verification" web page.