# λMC – monadic translation of mini C into HeapLang
See the overview paper [Semi-automated reasoning about non-determinism in C expressions](http://cs.ru.nl/~dfrumin/wpc/iris-c-monad.pdf).
## Prerequisites
This development has been built and tested with the following dependencies:
- Coq 8.9.0
- A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
- A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
## 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/iris/opam.git
opam update
```
- Install the Coq development by running `opam install .` in the root
directory.
## Code structure
- [theories/lib](theories/lib) contains the auxiliary theories for mutexes (aka
locks), mutable sets, the lockable heap construction, etc.
- [theories/c_translation](theories/c_translation) contains λMC: a definitional
semantics of C and its associated logic.
+ [monad.v](theories/c_translation/monad.v) contains the definitions and
specifications for of monadic combinators.
+ [translation.v](theories/c_translation/translation.v) contains definitions
and specifications of the λMC operators.
+ [proofmode.v](theories/c_translation/proofmode.v) contains the MoSeL tactics
for the logic.
- [theories/vcgen](theories/vcgen) contains everything to do with symbolic
execution and verification condition generation.
+ [dcexpr.v](theories/vcgen/dcexpr.v) contains the reified syntax of the λMC
expressions and values.
+ [reification.v](theories/vcgen/reification.v) contains type classes for the
reification procedure.
+ [denv.v](theories/vcgen/denv.v) contains the representation of and the
operations on symbolic heaps.
+ [forward.v](theories/vcgen/forward.v) contains the symbolic executor and its
correctness proof.
+ [vcg.v](theories/vcgen/vcg.v) contains the vcgen algorithm and its
correctness proof.
+ [proofmode.v](theories/vcgen/proofmode.v) contains the MoSeL `vcgen` tactic.
- [theories/tests](theories/tests) contains a number of tests and example code.
## Differences with the paper
- In the Coq developmenet we do not have a separate (deeply embedded) syntactic
layer for λMC. Instead we define all the λMC operators as macros (as a
shallow embedding) on top of 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`: monadic bind
- `e1 |||ᶜ e2`: par
**C translation**
- `♯ l` and `♯ₗ l`: `return` for literals and locations
- `allocᶜ ( e1 , e2 )`: calloc
- `e1 =ᶜ e2`: assignment
- `∗ᶜ e`: dereference
- `x ←ᶜ e1 ;ᶜ e2` and `e1 ;ᶜ e2`: sequence point bind
- `ifᶜ ( e1 ) { e2 } elseᶜ { e3 }`
- `whileᶜ ( e1 ) { e2 }`
- `callᶜ ( e1 , e2 )`
- Binary and unary operations:
+ `e1 +ᶜ e2`
+ `e1 -ᶜ e2`
+ `e1 *ᶜ e2`
+ `e1 ≤ᶜ e2`
+ `e1 <ᶜ e2`
+ `e1 ==ᶜ e2`
+ `e1 !=ᶜ e2`
+ `~ᶜ e`
- Pointer arithmetic:
+ `e1 +∗ᶜ e2`: addition
+ `e1 <∗ᶜ e2`: comparison
- "Pre" operations:
+ `e1 +=ᶜ e2`
+ `e1 +∗=ᶜ e2`