Abstract Interpreters: a Monadic Approach to Modular Verification

This is a research project about verifying abstract interpreters modularly by using monadic semantics.

We provide a library exposing reusable component for the simultaneous construction of monadic concrete and abstract interpreters, with a proof of soundness. We illustrate the use of the library on two illustrative examples: a structured, imperative, "Imp" language; and an assembly-like, control-flow-graph-based, "asm" language. The proof effort is minimal, with extensive code and proof reuse.

Meta

• Author(s):
  • Sébastien Michelland
  • Laure Gonnord
  • Yannick Zakowski
• License: GPLv3
• Coq namespace: ITreeAI

How to reproduce results from the ICFP24 paper

To reproduce results directly on an x86_64 machine, no questions asked, download the compressed Docker image and run the following commands.

Download the image from Zenodo at: https://zenodo.org/records/11470739

% xz -d --stdout icfp24-monadic-ai.tar.xz | sudo docker load
% sudo docker run -it localhost/icfp24-monadic-ai
root@(container):~# dune build
# (proofs go through)
# (shows Eqdep.Eq_rect_eq.eq_rect_eq as the only axiom for both IMP and ASM)
# (inconsequential warning about extraction)
root@(container):~# dune runtest
# (observe that analysis results match the Section 3 example from the paper)

This is a standard build of a Coq project using dune. The dune runtest targets executes the program in extract/test.ml which simply dumps the output of the extracted analyzer on a simple test cases.

We claim that the artifact supports the paper in the following ways:

• The definitions and theorems match the paper. Here's where to find definitions from the paper in the theories/ folder:

  Where	What	In theories/	Note
  Figure 6	mirroring of ast2itree and ast2aflow	Core.SurfaceDSL.sound_ast2itree_ast2aflow
  Figure 6	preservation of sound' through handling	Core.Soundness.interp_sound_{idT,stateT,failT}
  Figure 6	unfolding of sound' into sound	Core.Soundness.sound_unfold
  Figure 7	sequence and do-loop combinators	Combinators.Seq, Combinators.Do
  Figure 8	definition of the aflow monad	Core.AflowMonad.aflow
  Figure 10	event handlers	Core.AflowMonad.aflow_interp_{state,fail}
  Figure 10	unfolding function	Core.AflowMonad.unfold
  Figure 11	surface AST definition	Core.SurfaceDSL.SurfaceAST
  Figure 12	sequence combinator	Combinators.Seq.{seqᵒ,seqˣ}	¹
  Figure 12	do-loop combinator	Combinators.Do.{doᵒ,doˣ}	¹
  Figure 12	while-loop macro	Core.SurfaceDSL.AST_While
  Figure 14	all theorems about IMP	examples.ImpArithFail.*
  Section 3	ast2itree and ast2aflow functions	Core.SurfaceDSL.{ast2itree,ast2aflow}
  Section 6	sound predicate	Core.AflowMonad.sound
  Section 6.1	sound' predicate	Core.Soundness.sound'
  Section 6.1	preservation of sound' through handling	Core.Soundness.interp_sound_{idT,stateT,failT}
  Section 6.1	sequence combinator soundness	Combinators.Seq.sound_seq
  Section 6.1	unfolding of sound' into sound	Core.Soundness.sound_unfold

  ¹: Figure 12 shows simplified versions of the sequence and do-loop combinators where all the parameter-related definitions have been unfolded.

• The theorems only rely on standard axioms

  • We depend on eq_rect_eq for some dependent inversions
  • dune build prints the axioms for the final theorems for IMP and ASM due to Print Assumptions statements at the end of each (see theories/examples/{Asm.v,ImpArithFail.v}

• The analyzer produces the results showcased by the paper

  • The Section 3 example is second-to-last in the output of dune runtest

There are some presentation differences between the paper and artifact:

• Where the paper says "event handling", the code often says (monadic) "interpretation". The latter is the correct term, but the paper avoids using it because it's already overloaded to mean both concrete execution and static analysis.
• The code adds a ᵒ after the name of concrete combinators because the raw name is often a reserved keyword (e.g. if).

Structure

Internal library in theories/

• Combinators/: control flow combinators. Each combinator comes with a concrete and abstract version (Section 5.3), proof of stability by handling, and modular proof of soundness.
  • Return.v: pure computations (rarely used)
  • Seq.v: sequence
  • If.v: conditional
  • Do.v: loop
  • TailMRec.v: mutually tail-recursive collection of computations; includes the CFG combinator as a particular instance
• Core/: main elements for the theory.
  • Events.v: Definition of the class of "Galois Connection for events" (Section 4.1)
  • AflowMonad.v: Definition of the aflow monad (Fig. 8), its effectful handling and unfolding (Fig. 10), and the semantic soundness sound (Section 6)
  • Soundness.v: Definition of the sound' predicate, proof of lifting of the soundness of handlers, and proof of sound_unfold (Section 6.1)
  • SurfaceDSL.v: Definition of the surface DSL (Section 3 and 5.2) and its two compilation functions. Definition of While as a macro (Fig. 12)
• Domains/: interface for numeric and memory domains, i.e. lattices with numeric- or memory-like properties (second half of Fig. 4).
• Lattices/: lattice theory and instances.
  • Lattice.v: Typeclasses for Lattice and GaloisConnection (first half of Fig. 4). Some trivial instances.
  • Lattice*.v: Non-trivial concrete instances of lattices.
• Util/: utilities.

Case studies in theories/examples

• Imp.v: Minimalist "Imp"
• ImpArithFail.v: "Imp" with asserts, built in three layers of interpretation
• Asm.v: Assembly-like language

Illustration of executability extract/

• Extraction.v: Setting up the extraction of the abstract interpreter for ImpArithFail on intervals
• test.ml: Minimal infrastructure to run the example and pretty print the output

Obtaining the project

git clone git@gitlab.inria.fr:sebmiche/itree-ai.git
cd itree-ai

Building the project

Dependencies

This artifact has been packaged with the following exact dependencies. It is likely to build against other versions, but we cannot guarantee it.

• dune 3.15.0
• coq 8.19.1
• coq-ext-lib 0.12.1
• coq-equations 1.3+8.19
• coq-itree 5.2.0
• coq-paco 4.2.0

These dependencies can be manually installed, or using at the root of this folder:

% opam install --deps-only .

Building the project

dune build

Running the extracted abstract interpreters on toy examples

% dune runtest

The example program from Section 3 should report as follows.

=== Abstract test ===
Program:
| x := 2;
| y := 0;
| while x
|   y := 1;
|   x := (x) - (1);
| z := 5;
| assert(y);
| z := 6;
Expected:
  x=[-inf:2] y=[0:1] z=[5:6]
Final state:
  ret = ttˣ
  err = ttˣ
  mem = TopExcept x=[-inf:2], y=[0:1], z=[5:6]
Success

Generating the Docker image

The Docker image for this project is generated from the source files in this repository (including unstaged changes).

% podman build -t icfp24-monadic-ai .

One way to export the image is then to save it and compress it.

% podman save icfp24-monadic-ai:latest > icfp24-monadic-ai.tar
% xz -vk -T0 icfp24-monadic-ai.tar

License

Some files related to base abstract domains are inspired from Xavier Leroy's IMP Abstract Interpreter (LPGL v2.1). The concrete semantics for the two example languages draw heavy inspiration from the tutorial for the Interaction Trees library (MIT). For now this code is licensed under GPLv3 (see LICENSE).