README.md 3.38 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
See the overview paper [Semi-automated reasoning about non-determinism in C expressions](http://cs.ru.nl/~dfrumin/wpc/iris-c-monad.pdf).

Dan Frumin's avatar
Dan Frumin committed
5 6
## Prerequisites

7
This development has been built and tested with the following dependencies:
Dan Frumin's avatar
Dan Frumin committed
8

9
 - Coq 8.9.0
Dan Frumin's avatar
Dan Frumin committed
10
 - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
11
 - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
Dan Frumin's avatar
Dan Frumin committed
12 13 14 15 16

## Installation instructions

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

## Code structure

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


## Differences with the paper

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

## Notations

The list of notations used in λMC:
Dan Frumin's avatar
Dan Frumin committed
65 66

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

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