README.md 3.19 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1
# λMC – monadic translation of mini C into HeapLang
Dan Frumin's avatar
Dan Frumin committed
2

Dan Frumin's avatar
Dan Frumin committed
3 4 5 6 7
## Prerequisites

This version is known to compile with

- Coq version 8.8.1
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9
- Development versions of [std++](https://gitlab.mpi-sws.org/iris/stdpp) and
  [Iris](https://gitlab.mpi-sws.org/FP/iris-coq).
Dan Frumin's avatar
Dan Frumin committed
10 11 12 13 14

## Installation instructions

- Install [opam](https://opam.ocaml.org/) version >= 2.0
- Add the Iris opam repository:
Robbert Krebbers's avatar
Robbert Krebbers committed
15 16 17 18
  ```
  opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
  opam update
  ```
Dan Frumin's avatar
Dan Frumin committed
19 20 21 22 23
- Install the Coq development by running `opam install .` in the root
  directory.

## Code structure

Robbert Krebbers's avatar
Robbert Krebbers committed
24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
- [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.
Dan Frumin's avatar
Dan Frumin committed
48 49 50 51


## Differences with the paper

Robbert Krebbers's avatar
Robbert Krebbers committed
52 53 54
- 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.
Dan Frumin's avatar
Dan Frumin committed
55 56 57
- 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"
Robbert Krebbers's avatar
Robbert Krebbers committed
58
  operators, arrays and pointer arithmetic, and mutable local scope variables.
Dan Frumin's avatar
Dan Frumin committed
59 60 61 62

## Notations

The list of notations used in λMC:
Dan Frumin's avatar
Dan Frumin committed
63 64

**Monadic part**
Dan Frumin's avatar
Dan Frumin committed
65
- `x ←ᶜ y ;;ᶜ z` and `x ;;ᶜ z`: monadic bind
Dan Frumin's avatar
Dan Frumin committed
66 67 68
- `e1 |||ᶜ e2`: par

**C translation**
Dan Frumin's avatar
Dan Frumin committed
69 70 71
- `♯ l` and `♯ₗ l`: `return` for literals and locations
- `allocᶜ ( e1 , e2 )`: calloc
- `e1 =ᶜ e2`: assignment
Dan Frumin's avatar
Dan Frumin committed
72
- `∗ᶜ e`: dereference
Dan Frumin's avatar
Dan Frumin committed
73
- `x ←ᶜ e1 ;ᶜ e2` and `e1 ;ᶜ e2`: sequence point bind
Dan Frumin's avatar
Dan Frumin committed
74 75
- `ifᶜ ( e1 ) { e2 } elseᶜ { e3 }`
- `whileᶜ ( e1 ) { e2 }`
Robbert Krebbers's avatar
Robbert Krebbers committed
76
- `callᶜ ( e1 , e2 )`
Dan Frumin's avatar
Dan Frumin committed
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91
- 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`