Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[CN] Extract should (allow user to) be more specific #311

Open
dc-mak opened this issue Jun 7, 2024 · 2 comments · May be fixed by #921
Open

[CN] Extract should (allow user to) be more specific #311

dc-mak opened this issue Jun 7, 2024 · 2 comments · May be fixed by #921
Assignees
@dc-mak
Labels
cn language Related to design of the CN language resource reasoning Related to reasources in specs

Comments

@dc-mak
Copy link
Collaborator

dc-mak commented Jun 7, 2024

If a program has

void f(int *p, int *q)
/*@ 
requires
   take X = each (u64 i; i < 10u64) { Owned(array_shift(p, i)) }; 
   take Y = each (u64 i; i < 10u64) { Owned(array_shift(q,i)) };
{
  /*@ extract Owned<int>, 5; @*/
...

The current CN can move the ownership of either p[5] or q[5] out the quantified predicate. This may be harmless, or confusing, or even erroneous (though we don't have a concrete example yet). We might like to make it specific, by specifying the base pointer, but it's not obvious how this would work if we managed #303.
@dc-mak dc-mak added the cn label Jun 7, 2024
@dc-mak dc-mak mentioned this issue Jun 7, 2024
Open
@septract septract mentioned this issue Aug 7, 2024
Open
@dc-mak dc-mak changed the title [CN] Extract should (allow user to) be more specific [CN] Extract should (allow user to) be more specific (take base pointer) Aug 19, 2024
This was referenced Aug 19, 2024
Open
Open
@dc-mak
Copy link
Collaborator Author

dc-mak commented Aug 19, 2024

Related #256

This was referenced Aug 19, 2024
Closed
Open
Closed
@dc-mak dc-mak added ui/ux Issue with presentation or user experience resource reasoning Related to reasources in specs language Related to design of the CN language and removed ui/ux Issue with presentation or user experience labels Nov 4, 2024
@dc-mak dc-mak changed the title [CN] Extract should (allow user to) be more specific (take base pointer) [CN] Extract should (allow user to) be more specific Nov 12, 2024
@dc-mak
Copy link
Collaborator Author

dc-mak commented Nov 12, 2024 •
edited
Loading

A new idea of naming resources, whilst chatting with Christopher:
For any take var = Pred(foo); we have syntax resourceof(var) to refer to the resource

Why would we need this?

Currently the extract is not specific enough to say from which each (..) one is intending to extract from, and this leads to confusing behaviour/poor error messages.
Specifically, if the provided index is incompatible with index ranges or quantifier basetypes, CN just skips over it, assuming the intended resource would have a matching basetype.

Why not use the base pointer of the quantified resource?

We also want to move away from the restriction of requiring a pointer in the arguments of a predicate, so the "obvious" solution of using the "base pointer" as a way to disambiguate is not general enough.

Why resourceof?

Seems similar enough to sizeof and typeof to not be too intimidating to C programmers. I've tried to come up with cute notational hacks before, but they're too cute and hence confusing.

Limitations

Programmers might want to do resourceof on arbitrary expressions. We should forbid this as a parse error and only allow it on variables on bound in a loop, pre or post.
To support resourceof outside of loops, pre or post, (e.g. halfway through a function, multi-dimensional arrays), we should support /*@ take var = Pred(..); @*/ as a CN statement, which is a long-standing existing request anyways ("resource assertions").

@dc-mak dc-mak mentioned this issue Dec 17, 2024
Open
@dc-mak dc-mak mentioned this issue Dec 27, 2024
Open
dc-mak added a commit to dc-mak/cerberus that referenced this issue Mar 7, 2025
@dc-mak
CN: Add frontend plumbing to name resources
d93664d 
This commit is the first in a series to address rems-project#311, by allowing users
to name the (quantified) resource they want to focus on.

The precise syntax will probably change in response to user feedback,
but right now it is `take <sym> = <resource> as <sym'>;` where "as" is a
new keyword and "<sym'>" is a symbol. At this point, the latter part
is optional, to preserve backwards compatibility.

Only quantified predicates really _need_ names, but to forbid names on
regular resources grammatically seems overly restrictive, so we shall
see how that plays out.

A tentative plan for how names evolve is:

|--------------------------|-----------|
| Owned<struct s>(..) as H | H.<field> |
| Owned<ct[10]> as H       | H[<index> |
| focus H[<var>];          | H[<var>]  |
| focus H[<expr>] as H'    | H'        |
| partial consumption      | H         |
| unfold a user-def pred   | H.<names> |

Also need a way of naming the ensures of a function call.

I believe there is no need to consider generating names for predicate
folds because that will only happen on demand at an ensures or preceding
a function call.

Perhaps the "names" of the resources in the context actually need to be
terms, e.g. to deal smoothly with H[<expr>].
@dc-mak dc-mak linked a pull request Mar 7, 2025 that will close this issue
Draft
@dc-mak dc-mak self-assigned this Mar 8, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@dc-mak dc-mak

Labels
cn language Related to design of the CN language resource reasoning Related to reasources in specs
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

CN: Add the ability to refer to resources by name dc-mak/cerberus
1 participant
@dc-mak