bern_target_api/
report.rs

1//! The feature contract report of a platform.
2
3use crate::Diagnostic;
4use bern_ir::Application;
5
6/// A feature contract report for one platform: the result of every
7/// feature in every applicable size, and the diagnostics they raise.
8#[derive(Clone, Debug, Default)]
9pub struct FeatureReport {
10    pub diagnostics: Vec<Diagnostic>,
11    /// `(contract, feature, size, result)` rows, in declaration order.
12    pub rows: Vec<(String, String, bern_ir::LayoutSize, bern_ir::FeatureResult)>,
13}
14
15impl FeatureReport {
16    /// One line per row, for terminals.
17    pub fn lines(&self) -> Vec<String> {
18        self.rows
19            .iter()
20            .map(|(contract, feature, size, result)| {
21                let outcome = match result {
22                    bern_ir::FeatureResult::Covered { entries } => {
23                        format!("covered by {}", entries.join(", "))
24                    }
25                    bern_ir::FeatureResult::Guaranteed { entries, reason } => format!(
26                        "NOT PROVEN, manually guaranteed ({reason}); conditional entries {}",
27                        entries.join(", ")
28                    ),
29                    bern_ir::FeatureResult::Exempt { reason } => format!("exempt: {reason}"),
30                    bern_ir::FeatureResult::Missing => "MISSING".into(),
31                    bern_ir::FeatureResult::Unproven { entries } => {
32                        format!("UNPROVEN: only conditional entries {}", entries.join(", "))
33                    }
34                };
35                format!("{contract}::{feature} [{}] {outcome}", size.name())
36            })
37            .collect()
38    }
39}
40
41/// Evaluate every feature contract for `platform`: exemptions apply only
42/// to their platform; missing and unproven features are errors (B201,
43/// B203), manual guarantees warnings (B206) and exemptions notes (B205).
44pub fn feature_report(app: &Application, platform: &str) -> FeatureReport {
45    let mut report = FeatureReport::default();
46    for contract in &app.contracts {
47        for feature in &contract.features {
48            for (size, result) in feature.results(platform) {
49                let name = format!("{}::{}", contract.name, feature.name);
50                let diagnostic = match &result {
51                    bern_ir::FeatureResult::Covered { .. } => None,
52                    bern_ir::FeatureResult::Missing => Some(
53                        Diagnostic::error(format!(
54                            "Feature missing in adaptive layout\nContract: {}\nFeature: {}\n{}: missing",
55                            contract.name,
56                            feature.name,
57                            size.name()
58                        ))
59                        .code("B201"),
60                    ),
61                    bern_ir::FeatureResult::Unproven { entries } => Some(
62                        Diagnostic::error(format!(
63                            "`{name}` is reached in `{}` only under conditions the framework cannot prove ({}); add an unconditional entry, or `#[guaranteed(\"why\")]`",
64                            size.name(),
65                            entries.join(", ")
66                        ))
67                        .code("B203"),
68                    ),
69                    bern_ir::FeatureResult::Exempt { reason } => Some(
70                        Diagnostic::note(format!(
71                            "`{name}` is exempt in `{}` on {platform}: {reason}",
72                            size.name()
73                        ))
74                        .code("B205"),
75                    ),
76                    bern_ir::FeatureResult::Guaranteed { reason, .. } => Some(
77                        Diagnostic::warning(format!(
78                            "`{name}` in `{}` is not proven; accepted by a manual guarantee: {reason}",
79                            size.name()
80                        ))
81                        .code("B206"),
82                    ),
83                };
84                if let Some(diagnostic) = diagnostic {
85                    report
86                        .diagnostics
87                        .push(diagnostic.at(feature.source.clone()));
88                }
89                report
90                    .rows
91                    .push((contract.name.clone(), feature.name.clone(), size, result));
92            }
93        }
94    }
95    report
96}
bern_target_api/report.rs

bern_target_api/
report.rs
