VOLPIC, or "Verifier Of Lifted Pascal In Coq," is a platform for lifting FPC-compatible Pascal code into equivalent Gallina code, which can then be verified in the Coq Proof Assistant and extracted into OCaml or Haskell code.
Read the 2024 PLDI SRC extended abstract for an explanation of the project's purpose, structure, and accomplishments.
First build a custom version of FPC based on my branch*. This should look like:
git clone https://gitlab.com/CharlesAverill/source/ fpc-source
cd fpc-source
git checkout volpic_fpc
cd compiler
make cycle -j8
To compile and run the lifter:
cd vp_lifter
make
dune exec vp_lifter -- <path_to_program> -fpc-path "<path-to-custom-fpc-source>/compiler/ppcx64" -fpc-args "-Fu<path-to-custom-fpc-source>/rtl/units/x86_64-linux/"
* These changes are merged into FPC main, but due to the volatility of the parse tree dump format, I've chosen to maintain my own fork of version 3.2.2.