Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
c
Commits
70278ab4
Commit
70278ab4
authored
Nov 16, 2018
by
Dan Frumin
Browse files
Update the readme
parent
81137d7c
Changes
1
Hide whitespace changes
Inline
Sidebyside
README.md
View file @
70278ab4
# λ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.mpisws.org/iris/stdpp
)
and
[
Iris
](
https://gitlab.mpisws.org/FP/iriscoq
)
.
## Installation instructions

Install
[
opam
](
https://opam.ocaml.org/
)
version >= 2.0

Add the Iris opam repository:
```
opam repo add irisdev https://gitlab.mpisws.org/FP/opamdev.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**
**Monadic part**

`x ←ᶜ y ;;ᶜ z`
and
`x ;;ᶜ z`
: bind

`x ←ᶜ y ;;ᶜ z`
and
`x ;;ᶜ z`
:
monadic
bind

`e1 ᶜ e2`
: par

`e1 ᶜ e2`
: par
**C translation**
**C translation**

`♯ l`
and
`♯ₗ l`
:
`return`
o
f literals and locations

`♯ l`
and
`♯ₗ l`
:
`return`
f
or
literals and locations

`allocᶜ ( e1 , e2 )`
: alloc

`allocᶜ ( e1 , e2 )`
:
c
alloc

`e1 =ᶜ e2`
: assign

`e1 =ᶜ e2`
: assign
ment

`∗ᶜ e`
: dereference

`∗ᶜ e`
: dereference

`e1 ;ᶜ e2`
sequence point
s

`
x ←ᶜ
e1 ;ᶜ e2`
and
`e1 ;ᶜ e2`
:
sequence point
bind

`ifᶜ ( e1 ) { e2 } elseᶜ { e3 }`

`ifᶜ ( e1 ) { e2 } elseᶜ { e3 }`

`whileᶜ ( e1 ) { e2 }`

`whileᶜ ( e1 ) { e2 }`

`callᶜ ( f , a )`

`callᶜ ( f , a )`
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment