Docs: update what_charon_translates.md#1080
Docs: update what_charon_translates.md#1080oliver-butterley wants to merge 2 commits intoAeneasVerif:mainfrom
what_charon_translates.md#1080Conversation
|
|
||
| 1. **Transparent** — the item is fully translated. | ||
| 2. **Foreign** — the default for items outside the current crate. Translation depends on normal Rust visibility: for types, translate fully if it's a struct with all-public fields or an enum; for other items this is equivalent to Opaque. | ||
| 3. **Opaque** — only the name and signature are translated, not the contents. For functions and globals, the body is not translated. For types (structs, enums, unions), the fields/variants are not translated. For traits and trait impls, this doesn't change anything. For modules, the contents are not explored (but items referenced from elsewhere are still translated). |
There was a problem hiding this comment.
There's an extra subtlety: for traits and trait impls, opaque means we only translate a default method if it is used somewhere else. E.g. for Iterator that means we always translate next and mostly translate none of its other methods, unless they're mentioned explicitly. (We still ensure that each impl has exactly the same methods as its trait declaration).
|
This is great, thank you so much for taking the time to clean it up :) |
|
|
||
| When both a source annotation and a CLI pattern apply, the more opaque of the two wins (`Transparent < Foreign < Opaque < Invisible`). This means `--include` **cannot** override a `#[charon::opaque]` annotation. | ||
|
|
||
| Note: `#[charon::opaque]` operates at the MIR level, before Charon's item selection. This is necessary when Charon panics during MIR processing of a function body — CLI flags only take effect after MIR is available, so they cannot prevent such panics. |
There was a problem hiding this comment.
I'm not sure I understand what "at the MIR level" means here. The opaque annotation should totally be able to prevent charon from panicking on a function body, do you know a case where it doesn't?
|
|
||
| - **`--start-from <PATTERN>`** — Entry points for translation. Can be specified multiple times. Default: `crate` (the entire current crate). | ||
| - **`--start-from-attribute[=<ATTR>]`** — Use items annotated with a given attribute as entry points. Default attribute if none specified: `verify::start_from`. | ||
| - **`--start-from-pub`** — Use all `pub` items as entry points. |
There was a problem hiding this comment.
| - **`--start-from-pub`** — Use all `pub` items as entry points. | |
| - **`--start-from-pub`** — Use all `pub` items from the current crate as entry points. |
| - **`--opaque <PATTERN>`** — Set matched items to **opaque**. | ||
| - **`--exclude <PATTERN>`** — Set matched items to **invisible**. | ||
| - **`--extract-opaque-bodies`** — Alias for `--include *`. Makes all items transparent. | ||
| - **`--translate-all-methods`** — Include provided trait methods even if unused. |
There was a problem hiding this comment.
| - **`--translate-all-methods`** — Include provided trait methods even if unused. | |
| - **`--translate-all-methods`** — Include provided trait methods even if unused. Equivalent to making all trait declarations transparent. |
| - `crate::module::item` — matches this item and all its subitems | ||
| - `crate::module::item::_` — matches only the subitems (not the item itself) | ||
| - `core::convert::{impl core::convert::Into<_> for _}` — a specific trait impl | ||
| - `_` or `*` — glob, matches any single path segment | ||
|
|
||
| Patterns are **prefix matches**: `crate::foo` matches `crate::foo`, `crate::foo::bar`, `crate::foo::bar::baz`, etc.[^4] |
There was a problem hiding this comment.
I'm unsure about documenting this now because I'm thinking of changing patterns to not be prefix matches. In that world, crate::module::item matches exactly that item, crate::module::item::_ matches the items directly inside it, and crate::module::item::* does a prefix match which includes this item and all its (grand*)children.
The reason for that is that in practice I've found myself often writing --include some_path --opaque some_path::_ to get a single module which seems silly. I'm unsure still, which would you prefer?
|
|
||
| - `crate::module::item` — matches this item and all its subitems | ||
| - `crate::module::item::_` — matches only the subitems (not the item itself) | ||
| - `core::convert::{impl core::convert::Into<_> for _}` — a specific trait impl |
There was a problem hiding this comment.
There's an extra case: {impl core::convert::Into<_> for _} works without the core::convert prefix too: in that case we do a global search for impls.
There was a problem hiding this comment.
Could you also mention that we don't support matching on inherent impl blocks yet? Writing crate::module::_::method is the standard workaround
2 participants
This PR expands the text in the docs to fully describe how Charon selects items and the different ways to control the selection.
To be discussed:
I included footnotes to the source code where behaviour documented here is implemented. This might not be general taste, it's what seems best for me: surely the code will be updated and the doc will be out of date sometime, this is an easy way for readers to quickly notice this when it happens. Also allows agents to easily have the connection from docs to source to help with updates. I can remove these if required.
Fixes #1079