This repository containts ongoing work on a low-level systems programming language. One piece of the puzzle is a verified compiler targeting RISC-V. The source language itself is also equipped with a simple program logic for proving correctness of the source programs. It is not ready yet, at least for most uses.
This project has similar goals as bedrock, but uses a different design. No code is shared between bedrock and bedrock2.
The source language is a "C-like" language called ExprImp. It is an imperative language with expressions. Currently, the only data type is word (32-bit or 64-bit), and the memory is an array of bytes. "Records" are supported as a notation for memory access with an offset.
The following features will be added soon:
- Input and output
- Functions
- Register allocation (spilling if more local variables are needed than registers are available)
It is a design decision to not support the following features:
- Function pointers
You'll need Coq, version 8.9 or master.
In case you didn't clone with --recursive, use make clone_all to clone the git submodules.
Then simply run make or make -j or make -jN where N is the number of cores to use. This will invoke the Makefiles of each subproject in the correct order, and also pass the -j switch to the recursive make.
The source language (ExprImp) is compiled to FlatImp, which has no expressions, ie. all expressions have to be flattened into one-operation-at-a-time style assignments. FlatImp is compiled to RISC-V (the target language).
Main correctness theorems:
flattenStmt_correct_auxinFlattenExpr.vcompile_stmt_correct_auxinFlatToRiscv.vexprImp2Riscv_correctinPipeline.vcombining the two