RefinedC merge requestshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests2021-06-24T14:25:03Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/81check range on int to ptr cast2021-06-24T14:25:03ZMichael Sammlercheck range on int to ptr casthttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/80add type_alive2021-06-22T10:39:22ZMichael Sammleradd type_alivehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/79add at_value type2021-06-22T09:36:53ZMichael Sammleradd at_value typehttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/78Notation [&tagged] for owned tagged pointers.2021-06-22T08:39:21ZRodolphe LepigreNotation [&tagged] for owned tagged pointers.This is done by generalising the type parser, to allow type names
starting with '&'.This is done by generalising the type parser, to allow type names
starting with '&'.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/77Make integer to pointer casting rule more realistic2021-06-21T12:08:09ZMichael SammlerMake integer to pointer casting rule more realistichttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/76Change rc_copy_alloc_id to do the cast.2021-06-21T09:14:47ZMichael SammlerChange rc_copy_alloc_id to do the cast.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/74Add a simplification rule for tagged pointers.2021-06-18T13:08:16ZRodolphe LepigreAdd a simplification rule for tagged pointers.The rule turns any value type assigment hypothesis for a tagged pointer
with tag 0 into a value type assigment hypothesis for an owned pointer.
This allows implementing the [untag] function using [tag] in the tagged
pointer example (exam...The rule turns any value type assigment hypothesis for a tagged pointer
with tag 0 into a value type assigment hypothesis for an owned pointer.
This allows implementing the [untag] function using [tag] in the tagged
pointer example (examples/tagged_ptr.c).https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/73require alloc alive on pointer to integer cast2021-06-18T12:17:07ZMichael Sammlerrequire alloc alive on pointer to integer casthttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/72More provenances2021-06-16T12:22:47ZMichael SammlerMore provenanceshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/70add valid_ptr requirement to copy alloc id2021-06-14T17:46:52ZMichael Sammleradd valid_ptr requirement to copy alloc idhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/69Disallow creation of out of bounds pointers2021-06-14T11:39:51ZMichael SammlerDisallow creation of out of bounds pointershttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/68update iris2021-06-14T07:01:14ZMichael Sammlerupdate irishttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/60Example with tagged pointers.2021-06-10T11:57:16ZRodolphe LepigreExample with tagged pointers.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/67Reduce shifts on Z in solve goal, unfold aligned_to and Z.divide in solve_goa...2021-06-10T10:45:21ZMichael SammlerReduce shifts on Z in solve goal, unfold aligned_to and Z.divide in solve_goal and simpl in solve_goalhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/66Update Cerberus version.2021-06-02T17:03:57ZRodolphe LepigreUpdate Cerberus version.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/64Add cast in the definition of rc_copy_alloc_id.2021-05-21T12:44:38ZRodolphe LepigreAdd cast in the definition of rc_copy_alloc_id.There is not change in the generated code (up to some position updates).
However, the macro is now expanded to `((uintptr_t) (from), (to))`, which means that we force the provenance of the pointer from which we copy the provenance is ex...There is not change in the generated code (up to some position updates).
However, the macro is now expanded to `((uintptr_t) (from), (to))`, which means that we force the provenance of the pointer from which we copy the provenance is exposed (following the PNVI-ae-udi semantics).https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/63Preserve different C types in the frontend.2021-05-20T14:56:37ZRodolphe LepigrePreserve different C types in the frontend.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/62Add support for the comma operator.2021-05-19T10:40:46ZRodolphe LepigreAdd support for the comma operator.https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/58Hide the code in RefinedC goals.2021-04-28T14:22:27ZRodolphe LepigreHide the code in RefinedC goals.This PR changes two things:
- the code in goals is hidden (we use a notation `...` for printing),
- the hypotheses with location/case info do not have a definition anymore (this makes them smaller and more readable).This PR changes two things:
- the code in goals is hidden (we use a notation `...` for printing),
- the hypotheses with location/case info do not have a definition anymore (this makes them smaller and more readable).https://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/56Progress towards tracking pointer provenance in integers2021-04-27T07:21:11ZRodolphe LepigreProgress towards tracking pointer provenance in integersThis MR generalises the value representation of integers to preserve pointer provenance after a pointer-to-integer cast. However, this provenance information is lost on any arithmetic operation.
In the type system, this is handled using...This MR generalises the value representation of integers to preserve pointer provenance after a pointer-to-integer cast. However, this provenance information is lost on any arithmetic operation.
In the type system, this is handled using a new `l @ intptr<it>` type (similar to `n @ int<it>` but refined by a location instead of an integer). Elements of this type can be cast back to an owned pointer type (in which case the provenance is preserved) or to a normal `int` type (in which case the provenance information is lost).