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

PCC: add basic "memory types". #7219

Merged
merged 4 commits into from
Oct 12, 2023
Merged

Conversation

cfallin
Copy link
Member

@cfallin cfallin commented Oct 11, 2023

This PR adds a notion of "memory types" to the PCC (proof-carrying code) framework. To borrow a doc-comment:

A memory type is a struct-like definition -- fields with offsets, each field having a type and possibly an attached fact -- that we can use in proof-carrying code to validate accesses to structs and propagate facts onto the loaded values as well.

Memory types are meant to be rich enough to describe the layout of values in memory, but do not necessarily need to embody higher-level features such as subtyping directly. Rather, they should encode an implementation of a type or object system.

Note also that it is a non-goal for now for this type system to be "complete" or fully orthogonal: we have some restrictions now (e.g., struct fields are only primitives) because this is all we need for existing PCC applications, and it keeps the implementation simpler.

While developing this, we originally sketched out a more complete type-system that had arrays, allowed struct fields to be memory types themselves, and was in general more flexible. However, the possibility of cycles, non-statically-sized types, etc., was getting overly complex and I decided to YAGNI-simplify a bit for now. The Doc-comment on the module does sketch out what other types will be needed, and I think those plus a GV-bounded max fact will be enough to express PCC facts for all static and dynamic memories and table accesses in Wasmtime. (A partial further development of the more complete system, with some more validator checks for cycles, etc., is on this WIP branch.)

Part of this change was

Co-authored-by: Nick Fitzgerald fitzgen@gmail.com

@cfallin cfallin requested review from a team as code owners October 11, 2023 18:17
@cfallin cfallin requested review from elliottt and fitzgen and removed request for a team and elliottt October 11, 2023 18:17
@github-actions github-actions bot added cranelift Issues related to the Cranelift code generator cranelift:area:machinst Issues related to instruction selection and the new MachInst backend. cranelift:area:aarch64 Issues related to AArch64 backend. labels Oct 11, 2023
Copy link
Member

@fitzgen fitzgen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

r=me with nitpick-y suggestions that you can take or leave but also a more important point about a git submodule that should definitely be addressed before landing

cranelift/codegen/src/ir/memtype.rs Show resolved Hide resolved
cranelift/codegen/src/ir/pcc.rs Show resolved Hide resolved
cranelift/filetests/filetests/pcc/fail/simple.clif Outdated Show resolved Hide resolved
crates/wasi-nn/spec Outdated Show resolved Hide resolved
@cfallin cfallin added this pull request to the merge queue Oct 12, 2023
Merged via the queue into bytecodealliance:main with commit 1ced3e8 Oct 12, 2023
18 checks passed
@cfallin cfallin deleted the pcc-memcap branch October 12, 2023 00:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
cranelift:area:aarch64 Issues related to AArch64 backend. cranelift:area:machinst Issues related to instruction selection and the new MachInst backend. cranelift Issues related to the Cranelift code generator
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants