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.

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

Improve message buffer access #153

Merged
merged 2 commits into from
Nov 21, 2023

Conversation

geonnave
Copy link
Collaborator

@geonnave geonnave commented Nov 21, 2023

  • use .as_slice() instead of buffer.content[..buffer.len]
  • use fill_with_slice(slice) instead of buffer[..buffer.len].copy_from_slice(slice)

This introduces some unwrap calls which should not fail, and I hope it could be guaranteed by hax. If not then it can be reworked.

Deliberately not being exhaustive in the calls to .content[] within parsing routines. In this case, we also expect to have proofs from hax.

Note that we are not hax-typechecking ead*, so early
returns are fine there.
@geonnave geonnave force-pushed the refactor-buffer-access branch from c39304d to 780b8de Compare November 21, 2023 10:47
@geonnave geonnave merged commit d63b48a into openwsn-berkeley:main Nov 21, 2023
@geonnave geonnave deleted the refactor-buffer-access branch November 21, 2023 12:51
@chrysn
Copy link
Collaborator

chrysn commented Nov 21, 2023

By the way, the MessageBuffer is at this point pretty much a re-implementation of heapless::Vec. If hacspec grows well, it may be possible to just swap that in at some point. (That'd work best when all direct access to content has been removed, which AIU we currently do for efficiency reasons -- thus, it may take some time until we can do that, for may require placement return).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants