Isabelle-LLVM

Isabelle-LLVM is a verification framework for Isabelle/HOL that targets LLVM as backend. The main features are:

Shallowly embedded semantics of fragment of LLVM
Code generator, to export LLVM code
Generation of header files for interfacing the code from C/C++
Separation logic based VCG
Support for stepwise refinement based verification
Support for parallel programs

News

March 2023: added parallel partitioning algorithm
November 2022: ported to Isabelle 2022
June 2022: added support for unions
April 22: added support for floating point numbers
October 2021: added support for parallel programs
July 2021: ISASAT, a fully verified SAT solver that uses Isabelle-LLVM, has won the 2021 EDA Fixed CNF Encoding Race.
June 2021: released version 2.0. New features:
- support of arbitrary structures, and pointers to structure itself (required for, e.g., linked lists)
- faster export_llvm for big code
Updated to work with new Isabelle 2021 version

Getting Started

You can browse the theories or download the files. (The download link won’t work if you are browsing this from inside the downloaded archive!)

Warning: the .thy files in the download are best viewed with the Isabelle/HOL IDE.

Git Repository

The project is hosted on github github.com/lammich/isabelle_llvm/tree/2022

Starting Points for Browsing

Here are some default starting points for browsing the theories

Parallel Paper

Some starting points, structured according to the parallel paper:

NE Monad

M Monad Includes the parallel combinator

Memory Model Including access reports

LLVM Values stored in Memory

LLVM Instructions

Code Generator Including the template for translating llc_par

Separation Logic and VCG A bit more general than described in paper, parameterized over memory model. The general rules are proved in Sep_Generic_Wp.thy, e.g. lemma ht_par for the parallel rule. The instantiated parallel rule is ht_llc_par in Sepref_Parallel.thy.

Sepref Tool Including the parallel setup in Sepref_Parallel.thy.

Interval array data structure

With-Split Combinator, With-Idxs Combinator and its implementation on arrays.

Sorting Algorithms Contains the code export to LLVM, and the final correctness theorem. Our parallel quicksort algorithm is in Sorting_Parsort.thy, the sampling pivot finder is in Sorting_Sample_Partition.thy, and the parallel partitioner is in Sorting_Par_Partition.thy.

Verified Algorithms

Parallel Quicksort

Introsort

PDQ Sort

Knuth Morris Pratt String Search

Binary Search

For the ISA-SAT verified SAT solver, see its own homepage

Isabelle-LLVM

IICF (Isabelle-LLVM + Refinement Framework + Collection Framework)

Shallow Embedding of LLVM Semantics

Prerequisites

To compile the LLVM code: Working installation of LLVM version >= 10.0.0.
To compile the functional code: An MLton compiler version >= 20100608.
To re-check the proofs: Working installation of Isabelle/HOL with the Archive of Formal Proofs installed as as described on https://www.isa-afp.org/using.shtml. We require version = Isabelle-2022, which, at the time of writing, is the current version.
To run the regression tests: Valgrind version >= 3.0.0

Compiling and running benchmarks

To compile and run the benchmarks

cd benchmarks
./bench_bs.sh -r
./bench_kmp.sh -r
cd sorting
make run

This will run the binary search, KMP, and parallel sorting benchmarks. Warning: We have only tested this on a Linux x86_64 platform so far. We do not (yet) know how LLVM will digest our code on other platforms.

Re-Checking the Proofs

To re-check the proofs, run

  cd thys 
  isabelle build -D.

Here, isabelle must refer to /your/path/to/Isabelle2022/bin/isabelle from your Isabelle installation. This will invoke Isabelle to check all proofs and re-generate the exported code.

Regression Test Script

To run a quick regression test script

  cd regression
  make

This will re-check the proofs, export a few example programs, link them with C wrappers, and execute them under Valgrind’s memcheck, to detect ABI problems with header file generation and interfacing exported code from C.