RefinedC merge requestshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests2021-12-01T12:57:58Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/114Add boolean op-type + [builtin_boolean] type.2021-12-01T12:57:58ZRodolphe LepigreAdd boolean op-type + [builtin_boolean] type.Fixes #45Fixes #45https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/115remove constraints on z3 in gitlab-ci.yml2021-09-22T06:10:13ZMichael Sammlerremove constraints on z3 in gitlab-ci.ymlhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/116dynamic alloc/free2021-10-06T08:26:17ZLennard Gähergaeher@mpi-sws.orgdynamic alloc/freeThis MR adds dynamic memory allocation to the core language. We require this for RefinedRust, but RefinedC can just keep on not using it.
This is implemented in terms of a fairly canonical `Alloc` expression and `Free` statement, using t...This MR adds dynamic memory allocation to the core language. We require this for RefinedRust, but RefinedC can just keep on not using it.
This is implemented in terms of a fairly canonical `Alloc` expression and `Free` statement, using the existing `free_block` and `alloc_new_block` definitions.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/117add SimplExist and SimplForall2021-10-13T15:07:27ZMichael Sammleradd SimplExist and SimplForallhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/118More simpl instances for bf_cons2021-10-15T07:15:34ZFengmin ZhuMore simpl instances for bf_cons1. Instances for a singleton `bf_cons` compare with 0
2. Instance for solving equality of two `bf_cons` with the same shape (field indices)
3. Case study `pgtable.c` is updated accordingly, removing usages of the heuristic tactic `simpl_...1. Instances for a singleton `bf_cons` compare with 0
2. Instance for solving equality of two `bf_cons` with the same shape (field indices)
3. Case study `pgtable.c` is updated accordingly, removing usages of the heuristic tactic `simpl_bool_hyp`https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/119upgrade to coq 8.14.02021-10-19T12:39:05ZMichael Sammlerupgrade to coq 8.14.0https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/120enable record update2021-10-21T16:07:17ZFengmin Zhuenable record update1. Add dependency: coq-record-update
2. Use this library to simplify annotations for `pgtable.c`1. Add dependency: coq-record-update
2. Use this library to simplify annotations for `pgtable.c`https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/122bail out early for trivial hyps2021-11-17T09:43:49ZMichael Sammlerbail out early for trivial hypshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/123bail out early for trivial sideconditions2021-11-17T10:16:51ZMichael Sammlerbail out early for trivial sideconditionshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/124improve liWand performance2021-11-23T15:06:35ZMichael Sammlerimprove liWand performancehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/125Clean up letbinding infrastructure2021-11-24T12:42:59ZMichael SammlerClean up letbinding infrastructurehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/126Remove Movable typeclass2021-12-03T15:31:54ZMichael SammlerRemove Movable typeclasshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/127Add notation for tyexists2021-12-06T15:17:10ZMichael SammlerAdd notation for tyexistshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/128Add VerifyThis2021 solutions2021-12-09T13:31:50ZMichael SammlerAdd VerifyThis2021 solutionshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/129Create a separate coq-lithium package2022-02-28T08:45:47ZMichael SammlerCreate a separate coq-lithium packageThis MR creates a separate coq-lithium packages such that one can install Lithium without needing to pull in the full RefinedC (especially without needing to compile cerberus). Sadly, we need a hack to remove `lithium` from the refinedc ...This MR creates a separate coq-lithium packages such that one can install Lithium without needing to pull in the full RefinedC (especially without needing to compile cerberus). Sadly, we need a hack to remove `lithium` from the refinedc `dune` files before installing, since otherwise `dune` gets confused.
@lepigre any thoughts on this?https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/130fix some typos in the tutorial2022-02-17T13:33:21ZKimaya Bedarkarfix some typos in the tutorialFixed some typos I found in t00 and t01.Fixed some typos I found in t00 and t01.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/131Fix res_ty for rc_annot2022-02-23T16:02:16ZMichael SammlerFix res_ty for rc_annotWithout this MR code like
```
u16 rateval = rc_bitfield_init(u16, "rate_sig");
```
generates
```
f_code := (
<[ "#0" :=
"rateval" <-{ IntOp u16 }
LocInfoE loc_708 (UnOp (CastOp $ IntOp u16) (IntOp i32) (LocInfoE l...Without this MR code like
```
u16 rateval = rc_bitfield_init(u16, "rate_sig");
```
generates
```
f_code := (
<[ "#0" :=
"rateval" <-{ IntOp u16 }
LocInfoE loc_708 (UnOp (CastOp $ IntOp u16) (IntOp i32) (LocInfoE loc_708 (AnnotExpr 1%nat (BitfieldInitAnnot (rate_sig)) (LocInfoE loc_709 (UnOp (CastOp $ IntOp u16) (IntOp i32) (LocInfoE loc_710 (i2v 0 i32))))))) ;
```
Note that this contains a cast too much.
This MR fixes this issue and a similar issue for the ternary operator.
@lepigre Does this fix make sense?https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/133example scheduler2022-05-11T21:10:25ZMichael Sammlerexample schedulerhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/135add and verify simpler bitmap implementation2022-05-03T12:02:49ZKimaya Bedarkaradd and verify simpler bitmap implementationThis MR introduces the file `priority_modified.h`. This file contains an alternate implementation of the bitmap that only supports 64 priorities and is, therefore, easier to verify. This alternate implementation of the bitmap is fully ve...This MR introduces the file `priority_modified.h`. This file contains an alternate implementation of the bitmap that only supports 64 priorities and is, therefore, easier to verify. This alternate implementation of the bitmap is fully verified.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/136update Iris2022-05-13T16:15:28ZMichael Sammlerupdate Iris