Commit d81ae4c4 authored by Robbert Krebbers's avatar Robbert Krebbers

README tweaking.

parent 260a3625
......@@ -5,49 +5,57 @@
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).
- 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
```
```
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
- [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 syntactic layer
for λMC. Instead we define all the λMC operators as macros on the
HeapLang syntax.
- 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.
operators, arrays and pointer arithmetic, and mutable local scope variables.
## Notations
......@@ -65,7 +73,7 @@ The list of notations used in λMC:
- `x ←ᶜ e1 ;ᶜ e2` and `e1 ;ᶜ e2`: sequence point bind
- `ifᶜ ( e1 ) { e2 } elseᶜ { e3 }`
- `whileᶜ ( e1 ) { e2 }`
- `callᶜ ( f , a )`
- `callᶜ ( e1 , e2 )`
- Binary and unary operations:
+ `e1 +ᶜ e2`
+ `e1 -ᶜ e2`
......
......@@ -223,10 +223,9 @@ Definition cbin_op_eval (op : cbin_op) (v1 v2 : val) : option val :=
Definition c_pre_bin_op (op : cbin_op) : val := λ: "x" "y",
(* all binds should be non-sequenced *)
"lv" ←ᶜ ("x" ||| "y");;
c_atomic (λ: <>,
"ov" ←ᶜ ∗ᶜ (c_ret (Fst "lv"));;
c_ret (Fst "lv") = c_bin_op op (c_ret "ov") (c_ret (Snd "lv"));;
c_ret "ov").
"ov" ←ᶜ ∗ᶜ (c_ret (Fst "lv"));;
c_ret (Fst "lv") = c_bin_op op (c_ret "ov") (c_ret (Snd "lv"));;
c_ret "ov".
Notation "e1 +=ᶜ e2" := (c_pre_bin_op (CBinOp PlusOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 +∗=ᶜ e2" := (c_pre_bin_op PtrPlusOp e1%E e2%E) (at level 80) : expr_scope.
......@@ -642,9 +641,7 @@ Section proofs.
cwp_apply (cwp_wp with "He1"); iIntros (a1) "Ha1". cwp_lam; cwp_pures.
iApply cwp_bind. iApply (cwp_par with "Ha1 Ha2"). iNext.
iIntros (v1 v2) "Hv1 Hv2 !>". cwp_pures.
iApply cwp_atomic.
iIntros "$ !>". iDestruct ("HΦ" with "Hv1 Hv2") as (cl v w ->) "(Hl & % & HΦ)".
simplify_eq/=. iExists True%I. iSplit; first done. cwp_pures.
iDestruct ("HΦ" with "Hv1 Hv2") as (cl v w ->) "(Hl & % & HΦ)".
iApply cwp_bind. iApply cwp_load. iApply cwp_ret. iApply wp_value.
iExists cl, v; iFrame. iSplit; first done.
iIntros "Hl". cwp_pures. iApply cwp_bind.
......@@ -656,11 +653,10 @@ Section proofs.
iIntros (? ? -> ->); eauto.
- iIntros (? ? -> ->).
iExists _, _; iFrame. iSplit; first done.
iIntros "?". cwp_seq. iApply cwp_ret; iApply wp_value.
iIntros "_". by iApply "HΦ".
iIntros "?". cwp_seq. iApply cwp_ret; iApply wp_value. by iApply "HΦ".
Qed.
End proofs.
(* Make sure that we only use the provided rules and don't break the abstraction *)
Typeclasses Opaque c_alloc c_store c_load c_un_op c_bin_op c_seq_bind c_if c_while c_call.
Global Opaque c_alloc c_store c_load c_un_op c_bin_op c_seq_bind c_if c_while c_call.
Typeclasses Opaque c_alloc c_store c_load c_un_op c_bin_op c_pre_bin_op c_seq_bind c_if c_while c_call.
Global Opaque c_alloc c_store c_load c_un_op c_bin_op c_pre_bin_op c_seq_bind c_if c_while c_call.
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