RefinedC merge requestshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests2021-07-12T15:08:27Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/92Add CheckOwnInContext2021-07-12T15:08:27ZMichael SammlerAdd CheckOwnInContexthttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/93try removing pinning of conf-mpfr2021-07-14T05:05:23ZMichael Sammlertry removing pinning of conf-mpfrhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/94Bitblast: tactics for solving integer equality with bits2021-07-16T11:45:44ZFengmin ZhuBitblast: tactics for solving integer equality with bitshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/95Remove generated files and associated CI checks.2021-07-16T07:21:13ZRodolphe LepigreRemove generated files and associated CI checks.This requires adding an option [--soft] to [refinedc clean] in order
to prevent the [_CoqProject] file to be edited locally when building
or cleaning the examples.
No sure we want to merge that, what do you think @msammler?This requires adding an option [--soft] to [refinedc clean] in order
to prevent the [_CoqProject] file to be edited locally when building
or cleaning the examples.
No sure we want to merge that, what do you think @msammler?https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/96cleanup base.v2021-07-16T10:47:24ZMichael Sammlercleanup base.vhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/97Implement && and || using IfE.2021-07-16T21:31:28ZRodolphe LepigreImplement && and || using IfE.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/99parameterise operators with boolean result by the result integer type2021-07-27T07:25:51ZLennard Gähergaeher@mpi-sws.orgparameterise operators with boolean result by the result integer typeThis is a follow-up to https://gitlab.mpi-sws.org/iris/refinedc/-/merge_requests/98.
This PR parameterises Caesium's operators with a "boolean" result (i.e. the comparison operators as well as the derived && and || operators) by a resul...This is a follow-up to https://gitlab.mpi-sws.org/iris/refinedc/-/merge_requests/98.
This PR parameterises Caesium's operators with a "boolean" result (i.e. the comparison operators as well as the derived && and || operators) by a result integer type (which was hard-coded before to i32) as a step to use Caesium for modelling other C-like languages with different modelling of boolean results (e.g. Rust, which uses single-byte booleans).
Concretely, the changes can be summarised as:
* add a parameter `rit` to the affected operators and use that for the operational semantics of these operators, replacing the `i32` used before.
* adapt the existing notations for these operators to reflect this.
* change the Coq codegen to emit the additional parameter as `i32`,
* adapt the typing proofs to work for the changed operators instantiated to `i32`. Possibly, it might be desirable to support other result types even for C and to generalize the proofs accordingly, but I'm not sure.
The existing examples in the repo compile with these changes, but I haven't tested more exhaustively yet.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/100More support comparing pointers with 0 in the front end + rules for if and as...2021-08-03T07:31:46ZRodolphe LepigreMore support comparing pointers with 0 in the front end + rules for if and assert on pointers.This also includes support for better error positions.This also includes support for better error positions.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/101update to coq 8.13.22021-07-27T09:56:04ZMichael Sammlerupdate to coq 8.13.2https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/103allow opening invariants around typed_read_end and typed_write_end2021-07-30T08:28:54ZMichael Sammlerallow opening invariants around typed_read_end and typed_write_endhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/104Generate [return 0] for main + small refactoring.2021-08-03T09:25:56ZRodolphe LepigreGenerate [return 0] for main + small refactoring.@lgaeher this fixes the problem you mentioned [here](https://gitlab.mpi-sws.org/iris/refinedc/-/issues/30#note_64174).@lgaeher this fixes the problem you mentioned [here](https://gitlab.mpi-sws.org/iris/refinedc/-/issues/30#note_64174).https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/105split out heap_loc_eq2021-08-03T11:18:18ZMichael Sammlersplit out heap_loc_eqhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/106add via_vm_compute2021-08-05T07:07:24ZMichael Sammleradd via_vm_computehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/107Use multisuccess of typeclasses eauto to get rid of n parameter in FindInContext2021-08-05T14:57:38ZMichael SammlerUse multisuccess of typeclasses eauto to get rid of n parameter in FindInContexthttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/108Control better which sideconditions get shelved2021-08-19T06:36:09ZMichael SammlerControl better which sideconditions get shelvedhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/109Bit-wise reasoning2021-08-27T10:39:06ZFengmin ZhuBit-wise reasoning1. Introduce new `bitvec` and `bitvec_raw` types, and their typing rules.
2. Rewriting rules for normalizing bit vectors (by customized constructors).
3. Case study: `pgtable.c`1. Introduce new `bitvec` and `bitvec_raw` types, and their typing rules.
2. Rewriting rules for normalizing bit vectors (by customized constructors).
3. Case study: `pgtable.c`https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/110change implementation of via_vm_compute and add negb simpl instances2021-08-25T07:25:47ZMichael Sammlerchange implementation of via_vm_compute and add negb simpl instanceshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/111Add [cast_to_bool] and factorise "if" rules.2021-09-13T16:26:27ZRodolphe LepigreAdd [cast_to_bool] and factorise "if" rules.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/112Generalize the [boolean] type.2021-09-16T14:32:03ZRodolphe LepigreGeneralize the [boolean] type.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/113Better handling of Coq paths in the frontend.2021-09-20T09:27:23ZRodolphe LepigreBetter handling of Coq paths in the frontend.