RefinedC merge requestshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests2021-02-12T17:57:07Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/35Progress on the verification of [early_alloc.c].2021-02-12T17:57:07ZRodolphe LepigreProgress on the verification of [early_alloc.c].https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/34Check generated files on CI2021-02-12T15:10:40ZMichael SammlerCheck generated files on CIhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/33Case study: quick sort2021-02-26T05:06:45ZFengmin ZhuCase study: quick sortA new example for RefinedC: quick sort implemented using C arrays.A new example for RefinedC: quick sort implemented using C arrays.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/32Progress on the verification of [early_alloc.c].2021-02-12T10:59:15ZRodolphe LepigreProgress on the verification of [early_alloc.c].https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/31page_alloc2021-02-12T09:26:08ZMichael Sammlerpage_allochttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/30try new version of unification2021-02-12T07:22:02ZMichael Sammlertry new version of unificationhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/29Add a size to the [ptr] type.2021-02-12T06:16:14ZRodolphe LepigreAdd a size to the [ptr] type.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/28Refactor mpool2021-02-11T08:38:28ZMichael SammlerRefactor mpoolhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/27Refactor rule for arithmetic operators.2021-02-12T09:06:18ZRodolphe LepigreRefactor rule for arithmetic operators.This PR does a bit of refactoring of the rules for binary (arithmetic) operators on integers.
This will probably be useful to @paulzhu, and I needed this first step for the handling of right shifts.
The changes are the following:
- Defin...This PR does a bit of refactoring of the rules for binary (arithmetic) operators on integers.
This will probably be useful to @paulzhu, and I needed this first step for the handling of right shifts.
The changes are the following:
- Define a function `arith_op_result` that, given the two operands and the op computes the result.
- Define a predicate `arith_op_sidecond` that gives the side conditions for a given op.
- Use the above functions in the rule `type_arith_op_int_int`, and factor in the rules for `/` and `%`.
- Give more precise side conditions for the right and left shift operators (this is the goal of this PR). Note that the standard leaves it as implementation-define what is the result of right-shifting a negative number. I thing we should consider that UB.
Some further factoring of code is possible with the operational semantics, but we can do that as a second step.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/26More [loc_in_bounds] infrastructure.2021-02-10T15:48:00ZRodolphe LepigreMore [loc_in_bounds] infrastructure.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/25Make more functions simpl never2021-02-08T14:13:47ZMichael SammlerMake more functions simpl neverhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/24small steps towards improving subsume_list2021-02-04T16:45:33ZMichael Sammlersmall steps towards improving subsume_listhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/23Unfold more definitions in the side condition solver.2021-02-03T08:00:40ZRodolphe LepigreUnfold more definitions in the side condition solver.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/22Strengthen the [LocInBounds] infrastructure.2021-02-02T08:58:49ZRodolphe LepigreStrengthen the [LocInBounds] infrastructure.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/21Infrastructure for [SimpleSubsumeVal].2021-02-01T08:57:32ZRodolphe LepigreInfrastructure for [SimpleSubsumeVal].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/19Performance improvements?2021-01-27T13:51:28ZMichael SammlerPerformance improvements?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/17Fix cast insertion in the front end.2021-01-28T09:22:29ZRodolphe LepigreFix cast insertion in the front end.I'll merge this straight away if CI succeeds.
The point of this change is to always use Cerberus to decide what casts to insert on arithmetic operations.I'll merge this straight away if CI succeeds.
The point of this change is to always use Cerberus to decide what casts to insert on arithmetic operations.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.