RefinedC merge requestshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests2020-07-16T08:58:40Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/1sync Makefile and CI with Iris2020-07-16T08:58:40ZRalf Jungjung@mpi-sws.orgsync Makefile and CI with Irishttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/2Dune build2020-10-01T06:23:07ZMichael SammlerDune buildThings to do before this can be merged:
Blocker:
- [x] Make CI work
- [x] Make timing runner in CI work
- [ ] Check that CI that tests against iris master still works
- [x] Figure out the right command to build examples in RefinedC repo...Things to do before this can be merged:
Blocker:
- [x] Make CI work
- [x] Make timing runner in CI work
- [ ] Check that CI that tests against iris master still works
- [x] Figure out the right command to build examples in RefinedC repo
- `make && make install && refinedc check example.c`: Probably suboptimal?
- `dune exec -- refinedc check --no-build example.c && dune build`: Rebuilds everything
- `dune exec -- refinedc check --no-build example.c && dune build $(dirname example.c)`: Does this work? No
- Can one add an option to print `output_dir`?
- [x] Figure out if one can get rid of the `dune` files in the directories. Probably not...
- [x] Can manual proof files live in a different folder than the generated files?
- Seems very hard because dune does not allow cycles between modules
- [X] Is there a way to write a .gitignore file that ignores all generated files? Ignore `code.v`, `spec.v` and `proof_*.v`
- [x] Rename `+rc+` to something else
- `proof`? `rc`?
- [x] Make all generated files start with `rc_`?
Nice to have but not important for first version:
- [ ] Make path where generated files land configurable
- Minimal version: Allow user to pick a different directory name than `+rc+`
- Advanced version: Allow the user to give a path where the generates files should live
- if the path starts with `/`, it is relative to the root of the repo, otherwise it is relative to the dir of the file
- the path can contain `{FILENAME}` which gets replaced by the filename of the generated file
- examples:
- `+rc+/{FILENAME}/` current version
- `/generated/{FILENAME}_` (note no trailing slash) all generated files land in the `generated` folder
- [ ] Display the running time after compiling a file (similar to `TIMED=y make`)
Also nice to have, but not so important:
- [ ] Display a message when dune starts running a command (compared to only when the command is done)https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/3adding allocation range ghost state.2020-11-12T14:38:52ZRodolphe Lepigreadding allocation range ghost state.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/4Add simplification instance for list ≠ [], needed for quicksort2020-11-24T14:37:51ZIke MulderAdd simplification instance for list ≠ [], needed for quicksortWhen doing the quicksort exercise, RefinedC would at some point get stuck on a goal of the form `some_list ≠ [] ∧ …`, where `some_list` is a protected evar. This merge request adds an instance simplifying `l ≠ []` into `∃ a l', l = a :: ...When doing the quicksort exercise, RefinedC would at some point get stuck on a goal of the form `some_list ≠ [] ∧ …`, where `some_list` is a protected evar. This merge request adds an instance simplifying `l ≠ []` into `∃ a l', l = a :: l'` whenever `l` is a protected evar.
Additionally, it adds the sorting function to `tutorial/quicksort_solution.c` for which this instance was necessary.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/5Add a good failure state for allocation failure2020-11-27T11:00:37ZRodolphe LepigreAdd a good failure state for allocation failure- [x] Record in the state whether there has been an allocation failure.
- [x] Allocation failure as a new statement value.
- [x] Modification of the step relation to allow allocation failure to propagate to all threads.
- [x] Hide reason...- [x] Record in the state whether there has been an allocation failure.
- [x] Allocation failure as a new statement value.
- [x] Modification of the step relation to allow allocation failure to propagate to all threads.
- [x] Hide reasoning about allocation failure in a lifting lemma.
- [x] Actually add an "allocation failure" reduction step.
- [x] Fix adequacy.Michael SammlerMichael Sammlerhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/6Use separate inductives for allocation (refactoring).2020-12-02T10:24:34ZRodolphe LepigreUse separate inductives for allocation (refactoring).https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/8Intptr2020-12-04T15:22:53ZMichael SammlerIntptrhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/9Upgrade README demo: it_max -> max_int.2020-12-04T16:30:22ZFengmin ZhuUpgrade README demo: it_max -> max_int.Fix README demo.
- `it_max` -> `max_int`
- `<` -> `≤`Fix README demo.
- `it_max` -> `max_int`
- `<` -> `≤`https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/7Add support for macros2020-12-07T07:08:56ZMichael SammlerAdd support for macroshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/10Adding rules for intptr casts.2020-12-09T09:06:09ZRodolphe LepigreAdding rules for intptr casts.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/11Ensure variable names do not clash with Coq keywords.2020-12-11T07:16:50ZRodolphe LepigreEnsure variable names do not clash with Coq keywords.This fixes the third point of #30.This fixes the third point of #30.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/12Add annotation syntax for [global_with_type] constraints.2020-12-14T07:32:23ZRodolphe LepigreAdd annotation syntax for [global_with_type] constraints.This fixes part of #30.This fixes part of #30.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/13Add infrastructure to destruct products in function parameters.2020-12-17T13:09:50ZRodolphe LepigreAdd infrastructure to destruct products in function parameters.This solves yet another point discussed in #30.This solves yet another point discussed in #30.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/15Unfold instantiated evars on each liRStep.2021-01-12T14:45:52ZRodolphe LepigreUnfold instantiated evars on each liRStep.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/14Encode the constrained type into own_constrained.2021-01-14T08:59:30ZRodolphe LepigreEncode the constrained type into own_constrained.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/16Sugar in the front end + Coq pretty printing2021-01-15T13:21:11ZRodolphe LepigreSugar in the front end + Coq pretty printingThis MR introduces several changes intended to make RefinedC more user-friendly.
The first change concern the syntax of constraints in annotations. The following is now allowed:
- `own l : ty` (previously written `l @ &own<ty>`),
- `shr...This MR introduces several changes intended to make RefinedC more user-friendly.
The first change concern the syntax of constraints in annotations. The following is now allowed:
- `own l : ty` (previously written `l @ &own<ty>`),
- `shr l : ty` (previously written `l @ &shr<ty>`),
- `frac β l : ty` (previously written `l @ &frac<β, ty>`).
- The old notation has been removed.
The second change is some renaming around singleton types and layouts:
- `singleton_val` is now called `value`,
- `singleton_place` is now called `place`,
- `LPtr` is now called `void_ptr` and has notation `void*`,
- `LVoid` is now called `void_layout`.
- Additionally, the front end now accepts `void*` as an identifier.
The last change introduces a new Coq scope called `printing_sugar` that is only opened at the beginning of proofs in generated proof files. It defines printing notations intended at making the output of the tool closer to the syntax of the front end. In particular it defines the following notations:
- `own l : ty`, `shr l : ty`, `frac {β} l : ty`,
- `uninit<ly>`, `value<ly, v>`, `place<l>`, `&own<ty>`, ...
- for each user-defined types an associated printing sugar is defined automatically.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/18Make caesium an ectxi language2021-01-26T16:03:39ZMichael SammlerMake caesium an ectxi languagehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/19Performance improvements?2021-01-27T13:51:28ZMichael SammlerPerformance improvements?https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/20Fix inversion of signedness for [uintptr_t] and [intptr_t].2021-01-28T23:34:23ZRodolphe LepigreFix inversion of signedness for [uintptr_t] and [intptr_t].https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/21Infrastructure for [SimpleSubsumeVal].2021-02-01T08:57:32ZRodolphe LepigreInfrastructure for [SimpleSubsumeVal].