c-tree-carver

Carves C source trees into files suitable for verification tools.

This tool performs tree-carving on a C source-tree given some root functions, by retaining only the used declarations.

It is developed to extract and verify progressively larger parts of pKVM, without having to support irrelevant C constructs.

Installation

Prerequisites

• GNU C++ compiler >= 9.4
• LLVM/Clang 12.0.0
• CMake >= 3.16.3
• OCaml & Libraries (see opam file)

Build

opam install .

Usage

c-tree-carve --help

YOU MUST HAVE A compile_commands.json FILE IN YOUR SOURCE DIRECTORY. Futhermore, it must use relative paths.

cd cpp
./test/run_test.py make # make compile_commands.json file
c-tree-carve test/array/array_initialiser.in.c

Option	Meaning
-d	Output program debug info to stderr.
-n num	Choose a command (compile_commands.json can have more than one command per file)
-r func1,..,funcn	Choose traversal root functions from file (defaults to all)

The remaining options are from Clang's CommonOptionParser.

Running Tests

dune runtest && cd cpp && ./test/run_test.py make && ./test/run_test.py for

This makes a compile_commands.json file for all the test inputs and then runs all the tests. Additional options in ./test/run_test.py -h.

To Do

• C constructs required for kvm_pgtable_walk in pgtable.c
• Command line interface and support for compile_commands.json
• Support for reproducing directory structure
• Fix up tests
• Support macro dependencies
• Comment out instead of ommitting irrelevant lines
• Support retaining relevant includes
• Make build system straightforward
• Input validation for top-level decls
• Source locations for comment-simplifier
• Update conf-clang-12.opam.template to handle more distributions
• Input validation for struct/union fields
• End-to-end tests
• Update .travis.yml
• Add licenses/headache for tests?
• Use ASTContext::getTypeInfo to fill in missing struct fields
• Add new tests for new functionality (test/to-add, input validation, buddy allocator)
• Example for README.md

Funding

This software was developed by the University of Cambridge Computer Laboratory as part of the Rigorous Engineering of Mainstream Systems (REMS) project. This project has been partly funded by an EPSRC Doctoral Training studentship. This project has been partly funded by Google. This project has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No 789108, Advanced Grant ELVER).

History

The initial implementation and tests were taken from cpp-simplifier.