Commit 70278ab4 authored by Dan Frumin's avatar Dan Frumin

Update the readme

parent 81137d7c
# λMC – monadic translation of mini C
# λMC – monadic translation of mini C into HeapLang
Here is the list of notations used in λMC:
## Prerequisites
This version is known to compile with
- Coq version 8.8.1
- Development versions of [std++](https://gitlab.mpi-sws.org/iris/stdpp) and [Iris](https://gitlab.mpi-sws.org/FP/iris-coq).
## Installation instructions
- Install [opam](https://opam.ocaml.org/) version >= 2.0
- Add the Iris opam repository:
```
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
opam update
```
- Install the Coq development by running `opam install .` in the root
directory.
## Code structure
- `lib` contains the auxiliary theories for locks, mutable sets,
lockable heap, etc
- `c_translation` contains the actual translation and the associated
logic
+ `monad.v`: definitions and specifications for the monadic combinators
+ `translation.v`: definitions and specifications for λMC operators
+ `proofmode.v`: MoSeL tactics for the logic
- `vcgen` contains everything to do with symbolic execution and verification condition generation
+ `dcexpr.v`: reified syntax for the expressions and values
+ `reification.v`: type classes for the reification
+ `denv.v`: representation and operations on the symbolic heaps
+ `forward.v`: symbolic execution algorithm and its correctness proof
+ `vcg.v`: vcgen algorithm and its correctness proof
+ `proofmode.v`: vcgen as a MoSeL tactic
- `tests`: tests and example code
- `algebra/level.v`: the lockable level resource algebra
## Differences with the paper
- In the Coq developmenet we do not have a separate syntactic layer
for λMC. Instead we define all the λMC operators as macros on the
HeapLang syntax.
- Due to that, the values have to be embedded explicitly, either using
`c_ret` or `♯ i` for a literal `i`.
- There are additional language features in the code, including "pre"
operators, arrays and pointer arithmetic, and mutable local scope
variables.
## Notations
The list of notations used in λMC:
**Monadic part**
- `x ←ᶜ y ;;ᶜ z` and `x ;;ᶜ z`: bind
- `x ←ᶜ y ;;ᶜ z` and `x ;;ᶜ z`: monadic bind
- `e1 |||ᶜ e2`: par
**C translation**
- `♯ l` and `♯ₗ l`: `return` of literals and locations
- `allocᶜ ( e1 , e2 )`: alloc
- `e1 =ᶜ e2`: assign
- `♯ l` and `♯ₗ l`: `return` for literals and locations
- `allocᶜ ( e1 , e2 )`: calloc
- `e1 =ᶜ e2`: assignment
- `∗ᶜ e`: dereference
- `e1 ;ᶜ e2` sequence points
- `x ←ᶜ e1 ;ᶜ e2` and `e1 ;ᶜ e2`: sequence point bind
- `ifᶜ ( e1 ) { e2 } elseᶜ { e3 }`
- `whileᶜ ( e1 ) { e2 }`
- `callᶜ ( f , a )`
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment