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*. Note, building the compiler requires an existing installation of FPC. Check out the official installation guide. Building my custom FPC should look like:
git clone https://gitlab.com/CharlesAverill/source/ fpc-source
cd fpc-source
git checkout volpic_fpc
cd compiler
make cycle -j8The build will have completed if three binaries ppc1, ppc2, and ppc3 have been generated, as well as the final compiler build, denoted by the architecture you built for (ex. ppcx64)
To compile and run the lifter:
git clone https://github.com/CharlesAverill/volpic
cd volpic/vp_lifter
opam install . --deps-only
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.