Skip to content

Latest commit

 

History

History
253 lines (208 loc) · 10.3 KB

BUILD_ORGANIZATION.md

File metadata and controls

253 lines (208 loc) · 10.3 KB
Raw

HOW TO BUILD:

Check compatibility

If you install VST via opam, opam will take care of dependency versions.

Otherwise please check:

  1. Make sure you have the right version of Coq.

    grep ^COQVERSION Makefile

    will tell you which versions are compatible.

  2. Make sure you have the right version of CompCert. VST 2.6 uses CompCert 3.7 for Coq 8.11 or Coq 8.12

Install Method 1: use the Coq Platform

The recommended way to install any library for Coq (including VST) is via the Coq Platform, which is a set of scripts that will do an appropriate opam install for your operating system (Linux, MacOS, Windows). Follow the instructions there (that is, in README.md under Usage) to download the Coq Platform scripts and then follow the OS-specific instructions. After you install via the Coq Platform, you can still use opam commands to adjust your configuration, add more packages, et cetera.

Install Method 2: use opam directly

If you install VST via opam, opam will try to install a suitable version of CompCert, Flocq and other dependencies.

opam install coq  # best to install coq by opam instead of some other method

opam install coq-vst
AND/OR
opam install coq-vst-64

You can install both the 32 bit and the 64 bit versions of VST and CompCert in parallel. They will be installed in different folders. Please note that the 64 bit variants will be installed in non standard locations and must be included explicitly with -Q or -R options:

<opam-root>/lib/coq-variants/vst64/vst/
<opam-root>/lib/coq-variants/compcert64/compcert/
<opam-root>/variants/compcert64/bin/
<opam-root>/variants/compcert64/lib/

Please also note that some opam supplied versions of CompCert use a version of Flocq distributed with CompCert. This is problematic if you want to verify numerical code which uses tools like CoqInterval or Gappa which also use Flocq. The proofs these tools do might then not be compatible with VST and CompCert. For CompCert 3.7 there is an opam version called

coq-compcert.3.7~coq-platform
coq-compcert-64.3.7~coq-platform

which uses the opam supplied version of Flocq. There is also a version

coq-compcert.3.7~coq-platform~open-source
coq-compcert-64.3.7~coq-platform~open-source

which only contains the dual licensed open source part of CompCert. This is sufficient for learning VST using the example C programs provided. If you want to use VST for your own C code, you need at least clightgen, which is not free software. Please clarify the CompCert license conditions if you want to use clightgen. In case you want to use clightgen, please use this install command:

opam install coq-compcert.3.7~coq-platform coq-vst
AND/OR
opam install coq-compcert-64.3.7~coq-platform coq-vst-64

VST can work with various installations of CompCert and this sequence ensures you get the version you want. If you are an industrial user and want to learn CompCert and ensure you only install open source software, please use this install command:

opam install coq-compcert.3.7~coq-platform~open-source coq-vst
AND/OR
opam install coq-compcert-64.3.7~coq-platform~open-source coq-vst-64

Install Method 3: manual make with opam-supplied CompCert

Download the VST sources (by cloning the repo, or by unzipping a release .zip or .tar.gz file).

Then follow this procedure:

  1. Make sure CompCert and Flocq Coq .vo files are installed in 
    <opam-root>/lib/coq/user-contrib/Flocq
<opam-root>/lib/coq/user-contrib/compcert
AND/OR
<root>/lib/coq-variants/compcert64/compcert

This will happen automatically if you use the Coq Platform (or opam directly) to install CompCert.

  1. Make sure CompCert clightgen is installed in

    <opam-root>/bin
AND/OR
<opam-root>/variants/compcert64/bin

  2. In the VST root source directory (the directory containing the file you are reading), execute this command:

    make
OR
make BITSIZE=64

    (or, if you have a multi-core computer, make -j 16). You may add the target floyd to just build VST's core without examples and tests.

Please note that if you give options via the make command line, you should not have a file CONFIGURE in the VST root folder.

Install Method 4: advanced manual make, e.g. with bundled CompCert

Download the VST sources (by cloning the repo, or by unzipping a release .zip or .tar.gz file).

All options described in this section can be given in 3 ways:

  • on the command line of make via <option>=<value>
  • as an environment variable
  • as an assignment in a file CONFIGURE in the VST root folder Please be sure that you don't mix these methods in unintended ways.

VST make supports the below options to control which CompCert is used:

  • COMPCERT=platform: (default) choose 32 or 64 bit platform supplied x86 variant, dependent on BITSIZE, ARCH can be left empty or must be x86
  • COMPCERT=bundled: build and use bundled 32 or 64 x86 variant, dependent on BITSIZE, ARCH can be left empty or must be x86
  • COMPCERT=bundled_new: build and use bundled compcert_new 32 or 64 x86 variant, dependent on BITSIZE, ARCH can be left empty or must be x86
  • COMPCERT=src_dir: build and use in source folder COMPCERT_SRC_DIR the variant specified by ARCH and BITSIZE
  • COMPCERT=inst_dir: use prebuilt CompCert in COMPCERT_INST_DIR. BITSIZE and ARCH can be left empty or must match

The above settings for COMPCERT are keywords and not placeholders. If required additional information is given with these variables:

  • COMPCERT_SRC_DIR: absolute or relative CompCert source path
  • COMPCERT_INST_DIR: usually absolute CompCert installation path or source path with in-place build

If CompCert is built from sources, make sure to give at least one of the following options to CompCert's ./configure script: -clightgen, or -install-coqdev, or -coqdevdir, so that CompCert's compcert.config file is produced for VST to read.

The below options can be given in addition in order to chose the architecture. If CompCert is built from sources, this configures CompCert accordingly. If COMPCERT=inst_dir is chosen, the below options must match the specified installation if they are given. If COMPCERT=platform is chosen, BITSIZE can be specified, but the architecture is ignored.

  • BITSIZE=32 (default)
  • BITSIZE=64
  • ARCH=x86: (default) Intel x86, 32 and 64 bit
  • ARCH=aarch64: 64 bit ARM architecture
  • ARCH=powerpc: 32 bit power PC architecture

In case you want to regenerate the clightgen Coq files for the examples, you need to specify an absolute path to a clightgen executable. This is useful in case you want to check the examples for non x86 architectures. Please take care that this matches the given architecture (this is not checked).

  • CLIGHTGEN=<absolute path for given architecture>/clightgen

ORGANIZATION:

The Verified Software Tool-chain is organized into separate sub-projects, each in a separate directory:

  • msl - Mechanized Software Library
  • examples - examples of how to use the msl (not ported to Coq 8.6)
  • compcert - front end of the CompCert compiler, specification of C light
  • zlist - theory of concatenable sublists, and list theory solver
  • sepcomp - the theory and practice of how to specify shared-memory interaction
  • veric - program logic (and soundness proof) for Verifiable C
  • floyd - tactics for applying the separation logic
  • progs - sample programs, with their verifications

The dependencies are:

  • msl: no dependency on other directories
  • examples: msl
  • compcert: no dependency on other directories
  • zlist - no dependency on other directories
  • sepcomp: compcert
  • veric: msl compcert sepcomp
  • floyd: msl sepcomp compcert veric
  • progs: msl sepcomp compcert veric floyd

In general, we Import using -Q (qualified) instead of -R (recursive). This means modules need to be named using qualified names. Thus, in veric/expr.v we write Require Import msl.msl_standard instead of Require Import msl_standard. To make this work, the loadpaths need to be set up properly; the file _CoqProject (built by make _CoqProject) shows what -I includes to use.

USING VST:

To use either of these interactive development environments you will need to have the right load path. This can be done by command-line arguments to coqide or coqtop. The precise command-line arguments to use when running CoqIDE or coqc are constructed automatically when when you do "make", in the following files:

  • _CoqProject-export: For VST users, running the IDE outside the VST directory
  • _CoqProject : For VST developers, running the IDE in the VST directory

WITH COQIDE

From the VST root directory, run ./coqide to run coqide with recommended options. (Read the script for more info.)

WITH PROOF GENERAL

Use the _CoqProject file generated by the Makefile (Yes, we know, normally it's the other way 'round, normally one generates a Makefile from the _CoqProject.)

NEW DIRECTORIES:

If you add a new directory, you will probably want to augment the loadpath so that qualified names work right. Edit the OTHERDIRS or VSTDIRS lines of the Makefile.

EXTERNAL COMPCERT:

The VST imports from the CompCert verified C compiler, the definition of C light syntax and operational semantics. For the convenience of VST users, the VST/compcert directory is a copy (with permission) of the front-end portions of compcert.
You may choose to ignore the VST/compcert directory and have the VST import from a build of compcert that you have installed in another directory, for example, ../CompCert.

This has not been tested recently, as of August 2017.
To do this, create a file CONFIGURE containing a definition such as, COMPCERT=../CompCert
Make sure that you have the right version of CompCert! Check the file VST/compcert/VERSION to be sure.

COMPCERT_NEW:

Starting in July 2018, for a limited period of (we hope) only a few months, there is an experimental alternate CompCert basis in compcert_new. To use this, define a CONFIGURE file containing COMPCERT=compcert_new, and make sure to do a "make depend" and "make clean" before (re)building. WARNING: When using compcert_new, the file veric/Clight_core.v is not active; instead concurrency/shim/Clight_core.v is bound to the module path VST.veric.Clight_core.