google / google/zerocopy

Support conditional compilation (`#[cfg]`) in Anneal verification targets

Open
#3,017 0 comments 0 reactions 0 assignees View on GitHub
Dominant language
Rust
Stars
2.6k
Forks
179
Avg merge
1d 19h
Merged PRs (30d)
29

Description

### Problem

Anneal currently ignores `#[cfg(...)]` attributes during its AST scan. It parses all items syntactically, regardless of whether they are enabled for the current build target.

If a user annotates an item that is conditionally compiled out (e.g., a function guarded by `#[cfg(windows)]` when running on Linux, or an item requiring a disabled feature), Anneal still identifies it as a verification target. It then invokes `charon`, which performs a real compilation (`cargo check`). Since the item does not exist in the compiled artifact, Charon crashes or fails with an "Item not found" error.

### Goal

Anneal should simulate `rustc`'s conditional compilation logic during the parsing phase. If an item is disabled by the current configuration, Anneal should ignore it entirely: neither extracting it as a target nor traversing into it (in the case of modules).

### Proposed Solutions

#### Solution A: Copy all files; don't bail on missing files

We just need it to be the case that, if a project would have failed to compile normally, then its shadow copy will fail to compile; and if it would have succeeded, then its shadow copy will succeed.

Thus, given a `mod foo;` declaration, we can simply attempt to find a corresponding `foo.rs` or `foo/mod.rs` and copy it. If we succeed and `mod foo;` ends up being cfg'd out, then the file is ignored in the subsequent build, which is fine. If we fail and `mod foo;` is _not_ cfg'd out, then compiling the original source would have failed too, and so it's fine that the shadow crate fails to compile.

It's an open question whether this works with conditional paths. I _think_we can apply the same approach (copy all files we find names for, but fail silently), and the same logic applies for why it's fine, but I'd need to think harder about it.

```rust
#[cfg_attr(a, path = "foo_a.rs")]
#[cfg_attr(b, path = "foo_b.rs")]
mod foo;
```

#### Solution B: Evaluate cfgs

We should implement a evaluate cfgs using the `cfg-expr` crate.

##$## Context gathering

We need to capture the build context to evaluate `cfg` predicates:

* Invoke `rustc --print cfg` to obtain the global target key-value pairs (e.g., `target_os = "linux"`, `unix`, `target_pointer_width = "64"`).
* Extract the list of enabled features for each package from the `cargo metadata` resolution graph.

###$# Conditional parsing

Update the `AnnealVisitor` (`src/parse.rs`) to check for `#[cfg]` attributes before processing any item:

1. When visiting an item (Fn, Mod, Impl, etc.), parse any `#[cfg(...)]` attributes using `cfg-expr`.
2. Check the predicate against the gathered context (Target CFG + Package Features).
3. Then:
* If **false**: Skip the item completely. Do not extract annotations and do not descend into children.
* If **true**: Proceed as normal.

##$## Module resolution

This logic must crucially apply to `mod foo;` declarations. If a module is `#[cfg(false)]`, Anneal must **not** attempt to resolve the file path or parse the file, avoiding "File not found" errors for platform-specific modules.

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.