rebis-dev: Improve safety of atom tables and RawBlock
The safety of the operations defined for Atom and RawBlock relied until now on undocumented and unasserted properties of the inputs and the environment.
For instance, the following (dubious) library prolog code triggers undefined behavior:
dubious_load_library(Path) :- open(Path, read, Stream, []), '$load_library_as_stream'(Stream, _, _).
This PR aims to lessen the chance of someone inadvertently causing undefined behavior from an incorrect usage of Atom or RawBlock, by making the following changes:
- Turn
RawBlockTraits::align()into a constant, to enforce the invariant that it must be constant. This should also slightly improve performance. - Fix
RawBlock::allocnot actually aligning thesizetoT::align(), causing potential UB (all call sites were already aligning the size themselves). - Assert that atom pointers are within the bounds of their atom table and are correctly aligned (makes it so that the previous code sample now panics instead of segfaulting).
- Don't create an invalid, temporary
AtomDatabefore the right metadata for its fat pointer is obtained. - Assert at compile time that
AtomDatahas the expected representation. - Encapsulate accesses to
RawBlock, to reduce the amount of code that needs to uphold its invariants. The raw accesses are replaced with functions with both checked and unchecked variants. - Replace
UnsafeCellwithCellinRawBlock, as the previous code did not need to hand out mutable borrows toptr.RawBlockis still notSync. - Rename
ptrtoheadand store it as an offset frombase, to reduce the number of pointer operations to keep track of. - Document the invariants of
AtomDataandRawBlock. - Informally prove the safety of operations within
AtomDataandRawBlock.
I'm well aware that these are a lot of changes. I split them into multiple commits to make it possible to pull out changes into a future PR if needs be :)
Thank you so much for working on this!
One question I have regarding these changes: Would it be better to apply them directly to the upcoming rebis-dev development branch, so that the future merge is easier?
Please see the announcement and discussion at: https://github.com/mthom/scryer-prolog/discussions/2569
The rebase to rebis-dev shouldn't be too hard
@bakaq: I would greatly appreciate if you could take a look at these impressive changes!
I'm not sure why AndFrame::index behaves like a 1-indexed array, but I've added assertions in stack.rs where they were easy to add, and otherwise added TODOs to come back later to, as I don't want to blow out the complexity of this PR.
I would like to suggest in a subsequent PR a way to make the API of AtomTable fully safe, but those changes will need to be built on top of this PR's changes :)
@adri326: This looks awesome, thank you so much for all these impressive contributions!
Looks like there are some module access restrictions preventing the CI tests from passing.
Those were fixed by #2735 iirc
@adri326 is there a way to rerun the CI tests for this PR? One easy way may be to amend the topmost commit with --date=now and then force-push.
Did a rebase, the one failing test case is fixed in #2759, but you can run the tests locally with --no-fail-fast to let it go through all of the other ones.
I should probably squash those commits down, too.
Mark referred to the CI tests which we see on github at the end of this PR discussion, they still fail:
You can click on the tests to see more information.
@triska that's what I also understood. What I meant earlier was that the CI passing depends on #2759 (as of now, the same error in the CI occurs in rebis-dev), but the changes of this PR are themselves independent.
In the meantime, I've reorganised/squashed the commits for them to not be a mess anymore :)
As proof, you can see that the tests pass if you locally cherry-pick the fix from #2759:
git cherry-pick 2546976
cargo test
# All tests pass
@adri326 Could you please rebase your commits on the latest rebis-dev? I'd like to commit this PR. Thanks
@adri326: If you have time, could you please rebase the changes on the latest rebis-dev? They may help to resolve the remaining problem not yet addressed by #2945. Thank you a lot!