RefinedC merge requestshttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests2021-06-21T08:09:29Zhttps://gitlab.rts.mpi-sws.org/iris/refinedc/-/merge_requests/75Change rc_copy_alloc_id to do the cast.2021-06-21T08:09:29ZRodolphe LepigreChange 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/71More provenance2021-06-16T11:13:21ZMichael SammlerMore provenancehttps://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/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/65Remove the layout argument of [free_block].2021-09-20T09:28:04ZRodolphe LepigreRemove the layout argument of [free_block].This information is already contained in the allocation map. Removing
makes it easier to relate to the Cerberus memory model interface.This information is already contained in the allocation map. Removing
makes it easier to relate to the Cerberus memory model interface.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/61Add support for the comma operator.2021-05-19T10:22:57ZRodolphe LepigreAdd support for the comma operator.https://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/59Learn side-conditions in the continuation.2021-09-20T09:29:06ZRodolphe LepigreLearn side-conditions in the continuation.This seems to cause some performance penalty. Not sure how significant.This seems to cause some performance penalty. Not sure how significant.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/57Refactor the [int] type to use [val_to_Z]..2021-04-19T10:18:53ZRodolphe LepigreRefactor the [int] type to use [val_to_Z]..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).