CN: Represent null pointers as an extra constructor #494
+625
−191
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
dc-mak
changed the title
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
dc-mak
added a commit
to dc-mak/cerberus
that referenced
this pull request
Aug 16, 2024
Commit rems-project@2b30e70 introduced a new solver backend for CN. This code included a work-around for Z3 (Z3Prover/z3#7268), which involved calculating free variables for expressions. For `(let ((x term)) body)`, the code correctly looked in `body` but did not look in `term`. This commit fixes that, whilst tidying up some debugging and logging code to make future debugging sessions easier. It does not include a test because this bug was discovered during the development of a different feature (with file `tests/cn/ptr_diff2.c`) rems-project#494 which will be added in separately, later.
dc-mak
added a commit
to dc-mak/cerberus
that referenced
this pull request
Aug 16, 2024
Commit rems-project@2b30e70 introduced a new solver backend for CN. This code included a work-around for Z3 (Z3Prover/z3#7268), which involved calculating free variables for expressions. For `(let ((x term)) body)`, the code correctly looked in `body` but did not look in `term`. This commit fixes that, whilst tidying up some debugging and logging code to make future debugging sessions easier. It does not include a test because this bug was discovered during the development of a different feature (with file `tests/cn/ptr_diff2.c`) rems-project#494 which will be added in separately, later.
dc-mak
added a commit
that referenced
this pull request
Aug 16, 2024
Commit 2b30e70 introduced a new solver backend for CN. This code included a work-around for Z3 (Z3Prover/z3#7268), which involved calculating free variables for expressions. For `(let ((x term)) body)`, the code correctly looked in `body` but did not look in `term`. This commit fixes that, whilst tidying up some debugging and logging code to make future debugging sessions easier. It does not include a test because this bug was discovered during the development of a different feature (with file `tests/cn/ptr_diff2.c`) #494 which will be added in separately, later.
dc-mak
added a commit
to dc-mak/cerberus
that referenced
this pull request
Aug 16, 2024
Commit rems-project@7f4e8d6 added a test for commit rems-project@4e7fcb9 but it wasn't a test which passes once the error was fixed, so this commit deletes the test (since there will be other ones sooon rems-project#494
vzaliva
pushed a commit
that referenced
this pull request
Aug 18, 2024
Commit 2b30e70 introduced a new solver backend for CN. This code included a work-around for Z3 (Z3Prover/z3#7268), which involved calculating free variables for expressions. For `(let ((x term)) body)`, the code correctly looked in `body` but did not look in `term`. This commit fixes that, whilst tidying up some debugging and logging code to make future debugging sessions easier. It does not include a test because this bug was discovered during the development of a different feature (with file `tests/cn/ptr_diff2.c`) #494 which will be added in separately, later.
dc-mak
force-pushed
the
cn-vip-null
branch
2 times, most recently
from
ffc47ca
to
0ba0dd5
Compare
dc-mak
added a commit
to dc-mak/cn-tutorial
that referenced
this pull request
Aug 20, 2024
rems-project/cerberus#494 made this tests fail, but it wasn't quite phrased correctly anyways. It may need further changes for more VIP features later, but this should suffice for now.
dc-mak
added a commit
to rems-project/cn-tutorial
that referenced
this pull request
Aug 20, 2024
rems-project/cerberus#494 made this tests fail, but it wasn't quite phrased correctly anyways. It may need further changes for more VIP features later, but this should suffice for now.
dc-mak
force-pushed
the
cn-vip-null
branch
3 times, most recently
from
f813240
to
5e144e8
Compare
|
Seems to be some sort of issue where the CI gets stuck on |
dc-mak
added a commit
to dc-mak/cn-tutorial
that referenced
this pull request
Aug 26, 2024
rems-project/cerberus#494 exposed an issue in the Z3 which is a bit difficult to work around in the implementation itself and so we have this hacky work-around instead whilst it is fixed upstream Z3Prover/z3#7352
dc-mak
added a commit
to rems-project/cn-tutorial
that referenced
this pull request
Aug 26, 2024
rems-project/cerberus#494 exposed an issue in the Z3 which is a bit difficult to work around in the implementation itself and so we have this hacky work-around instead whilst it is fixed upstream Z3Prover/z3#7352
dc-mak
force-pushed
the
cn-vip-null
branch
4 times, most recently
from
61926c8
to
12b0c78
Compare
This is to more closely match VIP and also probably remove the need to specify `is_null(x) || !addr_eq(x, NULL` which is just silly. This uses match (for future-proofing against the addition of a `funcptr` constructor) and default<loc> for morally partial index terms. It also rejects more programs as a result. HasAllocId is a positive way to check that a pointer is in the `(@i, a)` datatype case rather than not NULL. Whilst the two are equivalent right now, this change is is mainly to future-proof against the addition of `funcptr` constructor for function pointers as in VIP/PNVI-*. The implementation relies on a few design choices: 1. Shifting on NULL is forbidden (implicitly) by the ISO C standard (it requires pointers which point to objects, hence cannot be NULL). Also, we believe real-world code only relies on this idiom for hand-implementing `offsetof`, so we forbid it. This is enforced in the typing rules. 2. It doesn't enforce that NULL is the same as/has address 0, although if need be, the implementation could use this info since no known optimisations/compilers etc. rely on NULL not being 0. Note that casting 0 to a pointer gives NULL, and casting a NULL pointer to an integer gives 0. 3. Shifting NULL in the specification language results in `default<Loc>`. Representing it as an provenance-address pair with an empty provenance would also be fine but would raise further questions on how to represent the empty provenance (an unconstrained variable, or a special value, the latter of which would require constraints on all Owned pointers to not have that special value as their provenance). For any choice here, one could construct a program in which proof and runtime testing diverge. 4. `each (u64 i; ..) { Owned(array_shift(p,i); }` is defined to imply `has_alloc_id(p)`. 5. Addresses of global variables are also constrained with `has_alloc_id(&global)`. It uses SMT functions for a more readable SMT file output. Unfortunately it also triggers: Z3Prover/z3#7352 which is worked-around by using modifying the simplifier and calling it at exactly the right moment (comments in the code). The test for this is added in tests/cn/simplify_array_shift.c
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The current setup may be fine, but departs from the presentation of pointer in VIP and PNVI-ae-udi. It also leads to somewhat ugly
is_null(p) || !addr_eq(p, NULL))(see append.c) which I believe this change should be able to eliminate.