Google Git
Sign in
opensecura / 3p / nicta / cogent / refs/heads/master
commit52bb32d7a7d3effede360bcffb04e874c954ba8f[log] [tgz]
authorZilin Chen <Zilin.Chen@data61.csiro.au>Sat Oct 17 01:13:57 2020 +1100
committerZilin Chen <Zilin.Chen@data61.csiro.au>Sat Oct 17 01:13:57 2020 +1100
treebd6c7faf05a0901963eb1b24990420663e92e01f
parent8a35eea7a1f65b9ba9006567c2703aab20dfaf43 [diff]
compiler: check arch-dependent implementation

Array lengths and indices are kept 32-bit no matter what arch is chosen;
pointer types and word sizes are in accordance with the arch chosen.
[skip bamboo]
8 files changed
tree: bd6c7faf05a0901963eb1b24990420663e92e01f
  1. c-refinement/
  2. cogent/
  3. docs/
  4. impl/
  5. isa-parser/
  6. minigent/
  7. regression/
  8. tutorial/
  9. isabelle
  10. z3
  11. .gitignore
  12. .gitmodules
  13. .readthedocs.yaml
  14. .regression-noclean
  15. .travis.yml
  16. BilbyFs_CorresProof.patch
  17. build-env.mk
  18. build-env.sh
  19. config.mk
  20. CONTRIBUTING.md
  21. CONTRIBUTORS.md
  22. LICENSE_BSD2.txt
  23. LICENSE_GPLv2.txt
  24. post-deploy.rb
  25. README.md
  26. ROOTS
  27. run_tests
README.md

Build Status Documentation Status

Cogent: Code and Proof Co-Generation

Project homepage

For general context of this project, motivation, an overview, and published papers, see our project homepage.

Online documentation

https://cogent.readthedocs.io

Installation

Instructions tested on Debian GNU/Linux 9.8 (“stretch”) and Ubuntu 18.04 (“bionic”). Similar distributions may also work.

Install dependencies from the Debian repository.

sudo apt-get install git # git
sudo apt-get install python-lxml python-psutil python-pycparser # regression tester

To install the Cogent compiler, consult file cogent/README.md for details.

The Cogent framework depends on Isabelle-2019. If you already have them on your machine, you can use your local copy. Otherwise you can either obtain it from their website or from the isabelle submodule, via git submodule update --init --recursive -- isabelle.

Add isabelle/bin to your PATH: export PATH="$(pwd)/isabelle/bin:$PATH" If you have an existing Isabelle install, you may want to set ISABELLE_IDENTIFIER instead of PATH.

Initialise Isabelle and install components:

isabelle components -I
isabelle components -a

Consult Isabelle manual for more information.

For more customised settings to run proofs and regression tests, modify build-env.sh.

Note: also see Proofs and Regression tests below.

Compiler

See cogent/README.md for more information.

File systems

See impl/fs/ext2/README and impl/fs/bilby/README for more information on how to build the kernel modules.

Proofs

Firstly, download the AutoCorres release from http://ts.data61.csiro.au/projects/TS/autocorres/, move the extracted folder to this directory, and rename the folder to autocorres.

To build the proofs, it is recommended that your machine (or virtual machine) provides 32G of memory and 4–8 CPU threads.

# Build compilation correctness proof for ext2. (ETA: 120 CPU hours)
(cd impl/fs/ext2/cogent;
 make verification;
 export L4V_ARCH="ARM";
 isabelle build -d plat/verification -d ../../../../cogent/isa -d ../../../../autocorres -b Ext2_AllRefine)

# Build compilation correctness proof for BilbyFs. (ETA: 120 CPU hours)
(cd impl/fs/bilby/cogent;
 make verification;
 patch -d plat/verification < ../../../../BilbyFs_CorresProof.patch;
 export L4V_ARCH="ARM";
 isabelle build -d plat/verification -d ../../../../cogent/isa -d ../../../../autocorres -b -o process_output_limit=999 BilbyFs_AllRefine)

# View end-to-end theorems. Each theory has a "print_theorems" command for this.
# For ext2:
L4V_ARCH="ARM" isabelle jedit -d impl/ext2/cogent/plat/verification -d cogent/isa -d autocorres -l Ext2_CorresProof impl/fs/ext2/cogent/plat/verification/Ext2_AllRefine.thy
# For BilbyFs:
L4V_ARCH="ARM" isabelle jedit -d impl/fs/bilby/cogent/plat/verification -d cogent/isa -d autocorres -l BilbyFs_CorresProof impl/fs/bilby/cogent/plat/verification/BilbyFs_AllRefine.thy

The functional correctness proofs for BilbyFs's sync and iget operations are in impl/fs/bilby/proof/. They are built as part of the regression tests, and can be rebuilt with

regression/run_tests.py -x autocorres -x isabelle -v sync iget

Regression tests (for developers; ETA: 2–3 CPU hours)

For testing the compiler, refer to travis.yml for commands.

Run ./run_tests to test systems implementations and parts of their Isabelle proofs.

For C-refinement proofs, which are excluded from the regression tests because of their size, follow instructions in Proofs section.

Directory

  • cogent: Cogent compiler
  • c-refinement: Isabelle/HOL theories and proof procedures for Cogent-C refinement
    • tests: Cogent test programs for proof procedures
  • isa-parser: Haskell library for parsing and pretty-printing Isabelle/HOL
  • impl: Systems implemented in Cogent
    • fs: File systems
      • bilby: Bilby file system
        • cogent: Cogent code for BilbyFs
        • c: C implementation for BilbyFs
        • proof: Functional correctness specs and proofs for BilbyFs
      • ext2: ext2 file system
        • cogent: Cogent code for ext2
  • regression: Regression test script

The Gencot Tool

Gencot is a tool for translating C code to Cogent. It's developed by our collaborators. The repository is hosted on Github. See the README file and the documentation for more details.