### Building VST Modular Verification Examples Source: https://github.com/princetonuniversity/vst/blob/master/progs/VSUpile/README.md Instructions for compiling the VST modular verification examples. This includes general build commands from the VST root, specific project builds, and configuration steps for building the project independently of the main VST installation. ```Makefile # From the VST root installation directory make -jN # From this directory (progs/pile) make -jN link_pile.vo # To build the fastpile example make -jN fast/link_fastpile.vo # For building outside VST, create a CONFIGURE file with: VST_LOC= path/to/VST COMPCERT_LOC= path/to/CompCert # Then run: make ``` -------------------------------- ### Building VST Verification Examples Source: https://github.com/princetonuniversity/vst/blob/master/progs64/VSUpile/README.md Comprehensive instructions for compiling various VST verification targets, including the main 'pile' program and the 'fastpile' example. These commands utilize 'make' with parallel execution from both the VST root installation directory and specific project subdirectories. ```Makefile make -jN ``` ```Makefile make -jN link_pile.vo ``` ```Makefile make -jN fast/link_fastpile.vo ``` -------------------------------- ### Install VST and Dependencies using opam Source: https://github.com/princetonuniversity/vst/blob/master/BUILD_ORGANIZATION.md The recommended way to install VST is via opam, which automatically handles dependencies like CompCert and Flocq. This snippet provides the basic commands to install Coq itself and then the 32-bit or 64-bit versions of VST. ```sh opam install coq opam install coq-vst AND/OR opam install coq-vst-64 ``` -------------------------------- ### Configure VST for Experimental CompCert Version Source: https://github.com/princetonuniversity/vst/blob/master/BUILD_ORGANIZATION.md To switch VST to an experimental CompCert basis (e.g., `compcert_new`), define the `COMPCERT` variable in your `CONFIGURE` file. After this change, it is crucial to run `make depend` and `make clean` before rebuilding the project to ensure proper dependency resolution and a clean build. Note that `veric/Clight_core.v` is replaced by `concurrency/shim/Clight_core.v` in this setup. ```Shell COMPCERT=compcert_new ``` ```Shell make depend make clean ``` -------------------------------- ### Install and Configure VSTlib Source: https://github.com/princetonuniversity/vst/blob/master/lib/README.md Provides shell commands for installing the VSTlib Coq package via OPAM, along with instructions for configuring C compiler include paths, C source paths, and Coq import statements for integrating VSTlib into projects. ```Shell opam repository add coq-released opam install coq-vst-lib ``` ```C -I $(OPAM_SWITCH_PREFIX)/lib/coq/user-contrib/VSTlib/include ``` ```C $(OPAM_SWITCH_PREFIX)/lib/coq/user-contrib/VSTlib/src ``` ```Coq From VSTlib Require Import spec_malloc. ``` -------------------------------- ### Configure Coq IDE and Load Paths for VST Source: https://github.com/princetonuniversity/vst/blob/master/BUILD_ORGANIZATION.md This section describes how VST manages Coq load paths for interactive development environments like CoqIDE and Proof General. It explains the purpose of the automatically generated `_CoqProject` files and provides instructions for launching CoqIDE with the recommended VST-specific options. ```APIDOC Coq Load Path Configuration: - _CoqProject-export: For VST users, running the IDE outside the VST directory. - _CoqProject: For VST developers, running the IDE in the VST directory. Using with CoqIDE: From the VST root directory, run: ./coqide - Runs coqide with recommended VST options. Using with Proof General: - Use the _CoqProject file generated by the Makefile. ``` -------------------------------- ### Install Specific CompCert Versions for VST via opam Source: https://github.com/princetonuniversity/vst/blob/master/BUILD_ORGANIZATION.md For specific use cases or licensing requirements, you might need to install particular versions of CompCert alongside VST. This command block demonstrates how to install CompCert versions compatible with Coq Platform, including an open-source variant suitable for learning VST without proprietary components like `clightgen`. ```sh opam install coq-compcert.3.7~coq-platform coq-vst AND/OR opam install coq-compcert-64.3.7~coq-platform coq-vst-64 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 ``` -------------------------------- ### Build VST Manually using make Source: https://github.com/princetonuniversity/vst/blob/master/BUILD_ORGANIZATION.md If you prefer to build VST from source, this method allows manual compilation using `make`. It assumes that CompCert and Flocq Coq `.vo` files are already installed in the correct opam directories, and provides options for standard or 64-bit builds, as well as parallel compilation. ```sh make OR make BITSIZE=64 ``` -------------------------------- ### Check Coq Version Compatibility for VST Source: https://github.com/princetonuniversity/vst/blob/master/BUILD_ORGANIZATION.md Before installing VST, it's crucial to verify that your Coq installation is compatible. This command uses `grep` to extract the required Coq version from the VST project's Makefile, ensuring proper dependency alignment. ```sh grep ^COQVERSION Makefile ``` -------------------------------- ### Configure CompCert Integration in VST Make Source: https://github.com/princetonuniversity/vst/blob/master/BUILD_ORGANIZATION.md This section details the `make` options available for configuring how the Verified Software Toolchain (VST) integrates with CompCert. Options control whether to use a platform-supplied, bundled, or pre-installed CompCert, and allow specifying source/installation directories, bit size, and architecture. These options can be set via command line, environment variables, or a `CONFIGURE` file. ```APIDOC VST make options for CompCert integration: COMPCERT= - platform: (default) choose 32 or 64 bit platform supplied x86 variant - bundled: build and use bundled 32 or 64 x86 variant - bundled_new: build and use bundled compcert_new 32 or 64 x86 variant - src_dir: build and use in source folder COMPCERT_SRC_DIR the variant specified by ARCH and BITSIZE - inst_dir: use prebuilt CompCert in COMPCERT_INST_DIR. BITSIZE and ARCH must match if given. Additional variables for COMPCERT=src_dir or COMPCERT=inst_dir: COMPCERT_SRC_DIR: absolute or relative CompCert source path COMPCERT_INST_DIR: usually absolute CompCert installation path or source path with in-place build Architecture and Bit Size Options: BITSIZE= - 32: (default) - 64: ARCH= - x86: (default) Intel x86, 32 and 64 bit - aarch64: 64 bit ARM architecture - powerpc: 32 bit power PC architecture Clightgen Path Option: CLIGHTGEN=/clightgen - Specifies an absolute path to a clightgen executable for regenerating Coq files. ``` -------------------------------- ### Configure VST to Use External CompCert Installation Source: https://github.com/princetonuniversity/vst/blob/master/BUILD_ORGANIZATION.md To integrate VST with an externally installed CompCert, create a `CONFIGURE` file in the project root and specify the path to your CompCert build. Ensure the CompCert version matches the VST requirements as indicated in `VST/compcert/VERSION`. ```Shell COMPCERT=../CompCert ``` -------------------------------- ### Install Coq VST Zlist Library via opam Source: https://github.com/princetonuniversity/vst/blob/master/zlist/README.md Instructions for installing the Coq VST Zlist library independently using the opam package manager. This installation is compatible with the corresponding version of VST when used outside of the VST project. ```Shell opam pin coq-vst-zlist https://github.com/PrincetonUniversity/VST.git ``` -------------------------------- ### VST Project Sub-projects and Module Dependencies Source: https://github.com/princetonuniversity/vst/blob/master/BUILD_ORGANIZATION.md The Verified Software Tool-chain (VST) is organized into several sub-projects, each residing in a separate directory. This documentation outlines the purpose of each sub-project and explicitly lists their inter-dependencies, crucial for understanding the project's modular architecture and for setting up Coq load paths correctly. ```APIDOC VST Sub-projects: - 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 Module Dependencies: - 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 Import Strategy: - Uses qualified imports (`-Q`) instead of recursive (`-R`). - Example: `Require Import msl.msl_standard` instead of `Require Import msl_standard`. ``` -------------------------------- ### Build VST from Root Directory Source: https://github.com/princetonuniversity/vst/blob/master/progs/pile/README.md Instructions to build the VST (Verified Software Toolchain) project from its root installation directory, utilizing parallel compilation. ```Make make -jN ``` -------------------------------- ### Build VST Fastpile Example Source: https://github.com/princetonuniversity/vst/blob/master/progs/pile/README.md Compiles the 'link_fastpile.vo' verification object for the 'fastpile' example, using parallel compilation to speed up the build process. ```Make make -jN fast/link_fastpile.vo ``` -------------------------------- ### Configuring VST Project for External Build Source: https://github.com/princetonuniversity/vst/blob/master/progs64/VSUpile/README.md Instructions for creating a 'CONFIGURE' file, which is necessary when VST project directories are moved outside the standard VST installation. This file specifies the absolute paths to the VST root and the CompCert compiler, enabling successful compilation in a custom environment. ```Configuration File VST_LOC= path/to/VST COMPCERT_LOC= path/to/CompCert ``` -------------------------------- ### Configure Emacs for ProofGeneral on Princeton CS Machines Source: https://github.com/princetonuniversity/vst/blob/master/doc/USE.md This Emacs Lisp snippet, to be added to ".emacs", loads the ProofGeneral site-specific configuration file from the shared VST installation on Princeton CS machines, enabling ProofGeneral functionality. ```Emacs Lisp (load "/n/fs/sml/sharedvst/proofgeneral/generic/proof-site.el") ``` -------------------------------- ### Configure VST Paths for External Build Source: https://github.com/princetonuniversity/vst/blob/master/progs/pile/README.md Defines environment variables for VST and CompCert locations in a 'CONFIGURE' file, enabling the project to be built outside the standard VST installation directory. ```Shell VST_LOC= path/to/VST COMPCERT_LOC= path/to/CompCert ``` -------------------------------- ### Typical VST Workflow Commands (Local) Source: https://github.com/princetonuniversity/vst/blob/master/doc/USE.md This sequence of commands outlines the standard workflow for verifying C programs with VST on a local machine. It involves converting a C file to a Coq ".v" file using "clightgen", compiling the Coq file with "make", and then opening the verification file in ProofGeneral or CoqIDE. ```Bash clightgen myprogram.c make myprogram.vo pg verif_myprogram.v #or coqide ``` -------------------------------- ### Launch CoqIDE with VST and CompCert Libraries (Local) Source: https://github.com/princetonuniversity/vst/blob/master/doc/USE.md This command line instruction launches CoqIDE, specifying the paths to the VST and CompCert libraries. VST is loaded via "-I" and CompCert via "-R", with CompCert aliased as 'compcert' for use within Coq. ```Bash coqide -I /PATHTOVST/VST -R /PATHTOCOMPCERT/CompCert-2.5 -as compcert YOURFILE.v ``` -------------------------------- ### Typical VST Workflow Commands (Princeton CS) Source: https://github.com/princetonuniversity/vst/blob/master/doc/USE.md This sequence of commands outlines the standard workflow for verifying C programs with VST on Princeton CS machines. It involves converting a C file to a Coq ".v" file using "clightgen", compiling the Coq file with "make", and then opening the verification file in ProofGeneral. ```Bash clightgen myprogram.c make myprogram.vo pg verif_myprogram.v ``` -------------------------------- ### Configure ProofGeneral for VST and CompCert (Local) Source: https://github.com/princetonuniversity/vst/blob/master/doc/USE.md This Bash script configures Emacs with ProofGeneral to load VST and CompCert as Coq libraries. It sets the "coq-prog-name" to "coqtop" and specifies the library paths using "-I" for VST and "-R" for CompCert, aliasing CompCert as 'compcert'. ```Bash #!/bin/bash emacs \ --eval "(setq coq-prog-name \"coqtop\")" \ --eval "(setq coq-prog-args \ '(\"-I\" \"/PATHTOVST/VST\" \"-R\" \"/PATHTOCOMPCERT/CompCert-2.5\" \"-as\" \"compcert\" ) )" $@ ``` -------------------------------- ### SSH to Princeton CS Machines with X11 Forwarding Source: https://github.com/princetonuniversity/vst/blob/master/doc/USE.md This command establishes an SSH connection to a Princeton University CS machine, enabling X11 forwarding ("-X" option) for graphical applications like ProofGeneral. ```Bash ssh -X username@cycles.cs.princeton.edu ``` -------------------------------- ### Configure PATH for VST Tools on Princeton CS Machines Source: https://github.com/princetonuniversity/vst/blob/master/doc/USE.md This line, to be added to ".bash_profile" or similar shell configuration, prepends the shared VST tools directory to the system's "PATH" environment variable, making "clightgen" and "pg" commands directly accessible. ```Bash export PATH=/n/fs/sml/sharedvst/bin:$PATH ``` -------------------------------- ### Makefile Configuration for Coq Compilation with VST (Princeton CS) Source: https://github.com/princetonuniversity/vst/blob/master/doc/USE.md This Makefile snippet defines "FLAGS" for Coq compilation, including paths to VST and CompCert libraries specific to the Princeton CS shared environment. It sets up a rule to compile ".v" Coq files into ".vo" compiled objects, using "coqc" with the defined flags. ```Makefile FLAGS=-I /n/fs/sml/sharedvst/VST -R /n/fs/sml/sharedvst/CompCert-2.5 -as compcert all:myprogram.vo %.vo:%.v Makefile coqc $(FLAGS) $< ``` -------------------------------- ### Makefile Configuration for Coq Compilation with VST (Local) Source: https://github.com/princetonuniversity/vst/blob/master/doc/USE.md This Makefile snippet defines "FLAGS" for Coq compilation, including paths to VST and CompCert libraries. It sets up a rule to compile ".v" Coq files into ".vo" compiled objects, using "coqc" with the defined flags. ```Makefile FLAGS=-I /PATHTOVST/VST -R /PATHTOCOMPCERT/CompCert-2.5 -as compcert all:myprogram.vo %.vo:%.v Makefile coqc $(FLAGS) $< ``` -------------------------------- ### Coq VST Zlist Solver Tactics Source: https://github.com/princetonuniversity/vst/blob/master/zlist/README.md Tactics available in the Coq VST Zlist library designed to assist in solving and simplifying goals related to list properties. These tactics leverage the library's internal list solver to automate proofs. ```APIDOC list_solve: Use the list solver to solve the goal. If it fails, you may try list_simplify to see the subgoal that cannot be solved. list_simplify: Reduce the goal using the list solver. It is safe that it does not turn a provable goal into any unprovable goals. ``` -------------------------------- ### Build VST Verification for pile Program Source: https://github.com/princetonuniversity/vst/blob/master/progs/pile/README.md Compiles the 'link_pile.vo' verification object for the 'pile' program from the 'progs/pile' directory, utilizing parallel compilation for efficiency. ```Make make -jN link_pile.vo ``` -------------------------------- ### Coq VST Zlist Function Definitions Source: https://github.com/princetonuniversity/vst/blob/master/zlist/README.md Core function definitions provided by the Coq VST Zlist library for manipulating lists. These functions include operations for determining list length, accessing elements, extracting sublists, and updating specific elements. ```APIDOC Zlength: length of a list. Znth: nth element of a list; returns default when out of bounds. sublist: a slice of a list in the range [lo, hi). upd_Znth: update the nth element of a list. ``` === COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.