Sources for "Verified Functional Programming of an Abstract Interpreter"

This git repository contains the source of the abstract interpreter presented in "Verified Functional Programming of an Abstract Interpreter".

Thanks to nix, our work is entierly reproducible, in no more than two lines of bash:

sh <(curl -L https://nixos.org/nix/install) --daemon
nix-build --attr all

Folder structure 📂

This repository is organized as following.

src contains all the F* source code:
- src/core contains the abstract interpreter itself, every definition presented in the paper lives in this directory;
- src/app contains the command line frontend to the abstract interpreter;
- src/js contains the sources of the web wrapper.
latex contains LaTeX supplementary files, but the paper is written as F* comments directly in the modules available under src/code.
tests contains a set of unit tests for the abstract interpreter.

Note: building the abstract interpreter triggers a build of F* and Z3 from scratch, which requires about 30 minutes on my machine.

How to build the abstract interpreter ⚙

1. Installing the Nix package manager

Install Nix on any Linux distribution, MacOS and Windows (via WSL) via the recommended multi-user installation:

sh <(curl -L https://nixos.org/nix/install) --daemon – Nix website

2. Build everything

The command nix-build --attr all creates the directory result with:

bin/analyser: the binary for the abstract interpretor (./analyser --help explain its usage);
examples: the example programs, make to run every test;
paper.pdf, paper.tex: the paper;
test-report.log: the log report for tests;
typechecking.log: the output of F* typechecking the abstract interpreter.

Get a developpement environment 🧰

All the steps below require nix to be installed (sh <(curl -L https://nixos.org/nix/install) --daemon).

Ready-to-use, preconfigured Emacs

A single line of bash: nix-shell --attr shellNix --run preconfigured-emacs

will open Emacs configured with the correct Z3 and F* binaries in PATH, with fstar-mode configured, and the important modules opened.

Pull the F* version we use

nix-shell --attr shellNix will drop you in a shell with the correct fstar.exe in PATH.

Recompile the analyser

Just run again nix-build --attr analyser.

Try the analyser in your web browser 🌐

Hosted version

Just go to https://demo-abint.netlify.app/

Locally

Compile the analyser to JavaScript and run a server locally:

nix-shell --attr webapp-nix-shell --run httpserver

Then open http://localhost:8251/ in a web browser.

Other build recipies availables 💉

nix-build --attr analyser: builds the binary in ./result/analyser;
nix-build --attr js-analyser: builds the web application version of the analyser in ./result/analyser;
nix-build --attr fstar: builds the version we use of F* in ./result/bin/fstar.exe;
nix-build --attr latex -o paper.tex: builds the latex of the paper as ./paper.tex;
nix-build --attr ocaml: extract the abstract interpreter as OCaml code in ./result/;
nix-build --attr pdf -o paper.pdf: builds the PDF for the paper as paper.pdf;
nix-build --attr tests -o tests.log: run the tests;
nix-build --attr typecheck -o typecheck.log: typecheck all the modules with F*.

Note on reproducability and on Nix ✨

Nix builds packages in isolation from each other. This ensures that they are reproducible and don't have undeclared dependencies, so if a package works on one machine, it will also work on another. – https://nixos.org/

Pointers on Nix

Flakes

The abstract interpreter actually uses the recent Nix Flakes. If you happen to have flakes enabled on your machine, you can:

nix build .#any-of-the-targets-above;
nix run .#emacs;
nix run .#webapp.

README.md