ccomp-simd - SIMD extensions for CompCert

This is a prototype of the ccomp-simd tool -- an extension of the CompCert - a certified compiler for C (http://compcert.inria.fr) supporting vector instructions on the x64 architecture. Please refer to the original CompCert's README and its manual for addition information on CompCert and on its copyright/usage instructions.

The current prototype includes also an intrinsics-aware constant-time checker, based on a fine-grained type system that assigns security types to each location (register or memory location) at each program point and calling context.

---

Installation

The original version of this development have been completed in 2016, and hence relies on fairly old versions of the supporting tools¹. Specifically, it depends on the following packages/versions:

• Python3
• Ocaml functional language (version 4.02.3)
• Coq proof assistant (version 8.4.6)
• coq-contrib/containers (coq v8.4 contribs)
• Menhir parser generator (version 20171222)
• SsReflect Ssreflect/MathComp (version 1.6.1)

Alternative #1: use Docker

The simplest way of experimenting with ccomp-simd is by resorting to a Docker container that includes all the mentioned packages. A Dockerfile is provided for it:

docker build https://raw.githubusercontent.com/haslab/ccomp-simd/master/scripts/Dockerfile

The build process creates a docker container with all the required packages and the (compiled) ccomp_simd tool.

Alternative #2: manual installation

step 1: install dependencies

Otherwise, one should install the dependencies manually. Most of the packages are available through the OPAM (Ocaml Package Manager), namelly:

opam install coq.8.4.6
opam install menhir.20171222
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-algebra.1.6.1

(obs: the containers coq plugin should be compiled/installed from the github link given above).

step 2: clone the repository and fetch the compcert compiler

$ git clone https://github.com/haslab/ccomp-simd.git
$ wget http://compcert.inria.fr/release/compcert-2.2.tgz
$ cd ccomp_simd
$ tar xvzf ../compcert-2.2.tgz

step 3: prepare the build directory and compile the tool

The tool is compiled in a dedicated build directory that only has links to both CompCert's and ccomp-simd's source files. The toplevel Makefile includes a target to setup the build directory.

$ make clean_setup_build_dir
$ cd build
$ ./configure ia32-$OS
$ make depend
$ make

where $OS is either macosx or linux.

---

Summary of Changes

component	files affected	modified/added lines
backend	26	795
cfrontend	12	166
common	6	76
cparser	11	191
driver	5	159
extraction	1	13
lib	2	28
ia32	22	4886
taintanalysis	27	8859
tools	2	3311

---

1: The port of the development to the current versions of the supporting tools is in progress.