cspgen is a command line tool for creating models of software in the Communicating Sequential Processes (CSP) process calculus. The tool accepts both C programs and LLVM IR as input, and writes a corresponding .csp file to disk. The output is compatible with FDR3, the Oxford CSP model checker. FDR may be used to check the model for for general properties, like deadlock freedom, divergence freedom and determinism, or may be compared with specifications written in CSP using refinement. cspgen aims to model the high-level communication behavior of the input code and to abstract data as much as possible to reduce model-checking time. It supports a subset of the pthreads library for multithreading and mutex primitives.
This repository also includes a formally verified Coq implementation of cspgen's core algorithm.
This is prototype, research software.
Usage: cspgen [OPTIONS] FILE
-o FILE --output=FILE Output destination
-l --llvm Take in LLVM IR rather than C
-d --dump Dump the AST representation of the C-Flat code
-c --emit-c Output the parsed C code
-e FILE --externals=FILE External function specifications
-r FILE --runtime=FILE Runtime file
-p STRING --cpp-opts=STRING Options to be passed to cpp
-t --test Run test files
-w --warn Hide warnings
-i --intermediate Show intermediate results
Note: By default, the input is assumed to be a C program. Use the -l flag if supplying LLVM IR instead.
Cspgen is written in Haskell and can be built with cabal, the Haskell package
manager. If you already have cabal installed, simply run cabal install
from
the top-level specgen
directory. The build depends on LLVM 3.4, which may be
available from your operating systems package manager. The cspgen
binary will
be installed to ~/.cabal/bin
. You can add this directory to your path or move
the binary elsewhere.
The examples
directory contains a variety of C and C++ files we use as test
cases and examples. The tests can be run with cabal test
or with cspgen -t
,
which provides more information. Note that some of the LLVM tests are currently
known to fail.
The verif
directory contains a coq verification of the core algorithm.
For information about the organization of the source code, see the ORGANIZATION file in this directory.
Someday there may be some.
Cspgen has been developed primarly by Chris Casinghino and Chinedu Okongwu.
Cspgen is developed by Draper Labs. Contact Chris Casinghino (ccasinghino@draper.com) for additional information.