add unreachable_cfg_select_predicates lint

[folkertdev]

tracking issue: #115585

Split out from #149783. This lint is emitted on branches of a cfg_select! that are statically known to be unreachable. The lint is only emitted when the feature is enabled, so this change specifically does not need an FCP, and the lint will be stabilized alongside the feature (see #149783 (comment)).

[rustbot]

Some changes occurred in compiler/rustc_attr_parsing

cc @jdonszelmann

[rustbot]

r? @WaffleLapkin

rustbot has assigned @WaffleLapkin.
They will have a look at your PR within the next two weeks and either review your PR or reassign to another reviewer.

Use r? to explicitly pick a reviewer

[Urgau]

The proposed name for this lint seems quite unfortunate to me. When I first read it I though it had something to do with the #[cfg] attribute, like detecting #[cfg] predicates that are unreachable.

I think it would be better include the word "arm" or "cfg_select" in it, to clearly disambiguate it from the other places where cfgs can appear.

Maybe unreachable_cfg_arms or unreachable_cfg_select_arms?

[folkertdev]

There is some reasoning for then name at #149783 (comment).

cc @traviscross was there any particular reason for you to leave out the select or arm/branch parts?

[traviscross]

The reasoning was:

For match, we call it unreachable-patterns; i.e. we put the focus on the pattern being unreachable rather than the arm. This makes sense; it's more precise. Notably we don't call it unreachable-match-arm-patterns.

Here that would suggest the name unreachable-cfg-predicates, since the constructs on the LHS of each arm are "configuration predicates" and we abbreviate "cfg".

But we have an existing lint, unexpected-cfgs that already uses cfgs to mean "configuration options" (a subset of cfg predicates), so punning a bit and riffing off that system would suggest the name unreachable-cfgs (though as mentioned, unreachable-cfg-predicates is OK too.)

To your point about detecting cfg attributes that are unreachable, I had the same thought when proposing the name, but expected I'd be OK, if we ever did want to lint other kinds of unreachable configuration predicates, using this same name for that.

---

Sitting with it now, though, I think unreachable-cfg-select-predicates would be OK.

[folkertdev]

I do like unreachable-cfg-select-predicates better, because it is more specific and more accurately reflects where someone might encounter this lint. So, I changed the implementation to use that name now.

[WaffleLapkin]

This doesn't seem to warn, unless there is a wildcard, why so? Does it not warn in case of

cfg_select! {
    unix => true,
    not(unix) => false,
    windows => false,
}

[folkertdev]

That is correct, it's hard to do better than that. we'd need to actually have some sort of logic solver to do so in general, and even then I think it might misfire if there is some sort of feature flag implication that the checker does not know about.

So the current imlementation is basic but reliable.

[WaffleLapkin]

We have similar checks for unreachable match arms, so it can't be that bad, right?

I'm really concerned that this lint in its current form is just misleading. I think a user that sees #![deny(unreachable_cfg_select_predicates) will assume that rust will detect all unreachable predicates (since rust is normally reliable like that), and then will not notice that there is an unreachable predicate.

[folkertdev]

We have similar checks for unreachable match arms, so it can't be that bad, right?

It seems feasible, but it really is adding a SMT solver, so, not straightforward.

https://doc.rust-lang.org/beta/nightly-rustc/rustc_hir/attrs/data_structures/enum.CfgEntry.html

We currently store

pub enum CfgEntry {
    All(ThinVec<CfgEntry>, Span),
    Any(ThinVec<CfgEntry>, Span),
    Not(Box<CfgEntry>, Span),
    Bool(bool, Span),
    NameValue {
        name: Symbol,
        name_span: Span,
        value: Option<(Symbol, Span)>,
        span: Span,
    },
    Version(Option<RustcVersion>, Span),
}

Meaning that e.g. for target_endian we'd need to encode that covering big/little is exhaustive. We need target feature implications to be taken into account, and cargo feature implication to be taken into account. This all seems useful, but it's complex. I'd rather not block cfg_select! on it.

@traviscross do you have more details of what T-lang had in mind here (and whether we want to block cfg_select! itself on that?

[traviscross]

Unfortunately, I do not have more details on hand. I've noted the question, though, and we'll cover this when we pick up the nomination on #149783.

[traviscross]

Question for you. I've been working on a minimal SAT solver that fits in around 600 lines of Rust code (while still being impressively fast). Let's say we had this. How much of the problem is that, and how much of the problem is encoding the needed invariants in CNF? I.e., if we had a good solver, is this still hard due to e.g. not knowing what we need to know in the right place to add the clauses, needing hard circuits such as for string operations, etc.? Or, if we had a solver, would it be straightforward to encode the problem in CNF?

[folkertdev]

I honestly have no idea, this is not really my area of expertise.

The NameValue variant might need some design around when that is exhaustive. Version seems hard, maybe that is just never exhaustive?

[traviscross]

Basically, a solver is going to offer an interface like this:

    /// Adds a clause to the formula.
    ///
    /// Literals are specified in DIMACS style: positive literal for
    /// variable `v` is `(v + 1)`, negative is `-(v + 1)`.  Variables are
    /// 0-indexed internally.
    ///
    /// # Panics
    ///
    /// Panics if any literal refers to a variable outside `[0, num_vars)`.
    pub fn add_clause(&mut self, lits: &[i32]);

That is, we have a set of $N$ boolean variables. We use "literals" to refer to them: literal 1 asserts that a variable is true; literal -1 asserts that it is false.

A clause is a set of literals that are ORed together (e.g., [1, -2] means v1 OR !v2). The solver ensures all added clauses are true.

If the formula is satisfiable (SAT), the solver returns an assignment of each variable. If it's not, it returns UNSAT.

The game is to assert all of the predicates of the earlier cfg_select arms as false (negated) and the predicate of the current arm as true. If it's SAT, then the arm is reachable. If it's UNSAT, then it's not.

We'd need to map every unique atomic cfg predicate (e.g., unix, target_pointer_width="32") to a unique SAT variable index. The tooling with the solver then provides a mechanism for encoding arbitrary boolean trees (e.g. not(all(a, any(b, c)))) into the right form (using a Tseitin transformation).

One design question is whether it'd be straightforward to produce the needed mapping and clauses.

[traviscross]

The NameValue variant might need some design around when that is exhaustive.

Yes, and we'd want to think about what we expect of the interaction with --cfg-check.

Version seems hard, maybe that is just never exhaustive?

Sounds right. We'd give each version a variable, then assert that at most one of these can be true.

[folkertdev]

@rustbot ready