Skip to content

Commit 00ab196

Browse files
JustusAdamcelinval
JustusAdam
and
celinval
authored
Encapsulate KaniAttributes (rust-lang#2668)
Creates a `KaniAttributes` struct with a low-level API for interacting with all the attributes found on an item. The old `attributes` API exposed functions of the form of `extract_<features>_attribute(tcx: TyCtxt, def_id: DefId)`. These functions would parse the attributes on the item, create an intermediate map of all attributes found and then extract whichever one was relevant. The most used extraction was the `extract_harness_attributes` which builds a whole struct describing all harness attributes for an item. For the time this API was sufficient but in the future we may have to (hint: contracts) interact multiple times with the attributes on a single item. Ideally in this case we would not parse all attributes again and again, but we also would not want to expose the internals of the `attributes` module, because that makes maintenance hard. This PR proposes to encapsulate the intermediate parse result as an opaque `KaniAttributes` structure. This can subsequently be efficiently queried to extract values or check them. Co-authored-by: Celina G. Val <[email protected]>
1 parent ca39285 commit 00ab196

File tree

3 files changed

+199
-155
lines changed

3 files changed

+199
-155
lines changed

‎kani-compiler/src/kani_middle/attributes.rs

Lines changed: 193 additions & 150 deletions
Original file line numberDiff line numberDiff line change
@@ -43,60 +43,206 @@ impl KaniAttributeKind {
4343
}
4444
}
4545

46-
/// Check that all attributes assigned to an item is valid.
47-
/// Errors will be added to the session. Invoke self.tcx.sess.abort_if_errors() to terminate
48-
/// the session and emit all errors found.
49-
pub(super) fn check_attributes(tcx: TyCtxt, def_id: DefId) {
50-
let attributes = extract_kani_attributes(tcx, def_id);
51-
52-
// Check that all attributes are correctly used and well formed.
53-
let is_harness = attributes.contains_key(&KaniAttributeKind::Proof);
54-
for (kind, attrs) in attributes {
55-
if !is_harness && kind.is_harness_only() {
56-
tcx.sess.span_err(
57-
attrs[0].span,
58-
format!(
59-
"the `{}` attribute also requires the `#[kani::proof]` attribute",
60-
kind.as_ref()
61-
),
62-
);
63-
}
64-
match kind {
65-
KaniAttributeKind::ShouldPanic => {
66-
expect_single(tcx, kind, &attrs);
67-
attrs.iter().for_each(|attr| {
68-
expect_no_args(tcx, kind, attr);
69-
})
70-
}
71-
KaniAttributeKind::Solver => {
72-
expect_single(tcx, kind, &attrs);
73-
attrs.iter().for_each(|attr| {
74-
parse_solver(tcx, attr);
75-
})
46+
/// Bundles together common data used when evaluating the attributes of a given
47+
/// function.
48+
#[derive(Clone)]
49+
pub struct KaniAttributes<'tcx> {
50+
/// Rustc type context/queries
51+
tcx: TyCtxt<'tcx>,
52+
/// The function which these attributes decorate.
53+
item: DefId,
54+
/// All attributes we found in raw format.
55+
map: BTreeMap<KaniAttributeKind, Vec<&'tcx Attribute>>,
56+
}
57+
58+
impl<'tcx> std::fmt::Debug for KaniAttributes<'tcx> {
59+
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
60+
f.debug_struct("KaniAttributes")
61+
.field("item", &self.tcx.def_path_debug_str(self.item))
62+
.field("map", &self.map)
63+
.finish()
64+
}
65+
}
66+
67+
impl<'tcx> KaniAttributes<'tcx> {
68+
/// Perform preliminary parsing and checking for the attributes on this
69+
/// function
70+
pub fn for_item(tcx: TyCtxt<'tcx>, def_id: DefId) -> Self {
71+
let all_attributes = tcx.get_attrs_unchecked(def_id);
72+
let map = all_attributes.iter().fold(
73+
<BTreeMap<KaniAttributeKind, Vec<&'tcx Attribute>>>::default(),
74+
|mut result, attribute| {
75+
// Get the string the appears after "kanitool::" in each attribute string.
76+
// Ex - "proof" | "unwind" etc.
77+
if let Some(kind) = attr_kind(tcx, attribute) {
78+
result.entry(kind).or_default().push(attribute)
79+
}
80+
result
81+
},
82+
);
83+
Self { map, tcx, item: def_id }
84+
}
85+
86+
/// Check that all attributes assigned to an item is valid.
87+
/// Errors will be added to the session. Invoke self.tcx.sess.abort_if_errors() to terminate
88+
/// the session and emit all errors found.
89+
pub(super) fn check_attributes(&self) {
90+
// Check that all attributes are correctly used and well formed.
91+
let is_harness = self.is_harness();
92+
for (&kind, attrs) in self.map.iter() {
93+
if !is_harness && kind.is_harness_only() {
94+
self.tcx.sess.span_err(
95+
attrs[0].span,
96+
format!(
97+
"the `{}` attribute also requires the `#[kani::proof]` attribute",
98+
kind.as_ref()
99+
),
100+
);
76101
}
77-
KaniAttributeKind::Stub => {
78-
parse_stubs(tcx, def_id, attrs);
102+
match kind {
103+
KaniAttributeKind::ShouldPanic => {
104+
expect_single(self.tcx, kind, &attrs);
105+
attrs.iter().for_each(|attr| {
106+
expect_no_args(self.tcx, kind, attr);
107+
})
108+
}
109+
KaniAttributeKind::Solver => {
110+
expect_single(self.tcx, kind, &attrs);
111+
attrs.iter().for_each(|attr| {
112+
parse_solver(self.tcx, attr);
113+
})
114+
}
115+
KaniAttributeKind::Stub => {
116+
parse_stubs(self.tcx, self.item, attrs);
117+
}
118+
KaniAttributeKind::Unwind => {
119+
expect_single(self.tcx, kind, &attrs);
120+
attrs.iter().for_each(|attr| {
121+
parse_unwind(self.tcx, attr);
122+
})
123+
}
124+
KaniAttributeKind::Proof => {
125+
expect_single(self.tcx, kind, &attrs);
126+
attrs.iter().for_each(|attr| self.check_proof_attribute(attr))
127+
}
128+
KaniAttributeKind::Unstable => attrs.iter().for_each(|attr| {
129+
let _ = UnstableAttribute::try_from(*attr).map_err(|err| err.report(self.tcx));
130+
}),
79131
}
80-
KaniAttributeKind::Unwind => {
81-
expect_single(tcx, kind, &attrs);
82-
attrs.iter().for_each(|attr| {
83-
parse_unwind(tcx, attr);
84-
})
132+
}
133+
}
134+
135+
/// Check that any unstable API has been enabled. Otherwise, emit an error.
136+
///
137+
/// TODO: Improve error message by printing the span of the harness instead of the definition.
138+
pub fn check_unstable_features(&self, enabled_features: &[String]) {
139+
if !matches!(self.tcx.type_of(self.item).skip_binder().kind(), TyKind::FnDef(..)) {
140+
// Skip closures since it shouldn't be possible to add an unstable attribute to them.
141+
// We have to explicitly skip them though due to an issue with rustc:
142+
// https://github.com/model-checking/kani/pull/2406#issuecomment-1534333862
143+
return;
144+
}
145+
if let Some(unstable_attrs) = self.map.get(&KaniAttributeKind::Unstable) {
146+
for attr in unstable_attrs {
147+
let unstable_attr = UnstableAttribute::try_from(*attr).unwrap();
148+
if !enabled_features.contains(&unstable_attr.feature) {
149+
// Reached an unstable attribute that was not enabled.
150+
self.report_unstable_forbidden(&unstable_attr);
151+
} else {
152+
debug!(enabled=?attr, def_id=?self.item, "check_unstable_features");
153+
}
85154
}
86-
KaniAttributeKind::Proof => {
87-
expect_single(tcx, kind, &attrs);
88-
attrs.iter().for_each(|attr| check_proof_attribute(tcx, def_id, attr))
155+
}
156+
}
157+
158+
/// Report misusage of an unstable feature that was not enabled.
159+
fn report_unstable_forbidden(&self, unstable_attr: &UnstableAttribute) -> ErrorGuaranteed {
160+
let fn_name = self.tcx.def_path_str(self.item);
161+
self.tcx
162+
.sess
163+
.struct_err(format!(
164+
"Use of unstable feature `{}`: {}",
165+
unstable_attr.feature, unstable_attr.reason
166+
))
167+
.span_note(
168+
self.tcx.def_span(self.item),
169+
format!("the function `{fn_name}` is unstable:"),
170+
)
171+
.note(format!("see issue {} for more information", unstable_attr.issue))
172+
.help(format!("use `-Z {}` to enable using this function.", unstable_attr.feature))
173+
.emit()
174+
}
175+
176+
/// Is this item a harness? (either `proof` or `proof_for_contract`
177+
/// attribute are present)
178+
fn is_harness(&self) -> bool {
179+
self.map.get(&KaniAttributeKind::Proof).is_some()
180+
}
181+
182+
/// Extract harness attributes for a given `def_id`.
183+
///
184+
/// We only extract attributes for harnesses that are local to the current crate.
185+
/// Note that all attributes should be valid by now.
186+
pub fn harness_attributes(&self) -> HarnessAttributes {
187+
// Abort if not local.
188+
assert!(self.item.is_local(), "Expected a local item, but got: {:?}", self.item);
189+
trace!(?self, "extract_harness_attributes");
190+
assert!(self.is_harness());
191+
self.map.iter().fold(HarnessAttributes::default(), |mut harness, (kind, attributes)| {
192+
match kind {
193+
KaniAttributeKind::ShouldPanic => harness.should_panic = true,
194+
KaniAttributeKind::Solver => {
195+
harness.solver = parse_solver(self.tcx, attributes[0]);
196+
}
197+
KaniAttributeKind::Stub => {
198+
harness.stubs = parse_stubs(self.tcx, self.item, attributes);
199+
}
200+
KaniAttributeKind::Unwind => {
201+
harness.unwind_value = parse_unwind(self.tcx, attributes[0])
202+
}
203+
KaniAttributeKind::Proof => harness.proof = true,
204+
KaniAttributeKind::Unstable => {
205+
// Internal attribute which shouldn't exist here.
206+
unreachable!()
207+
}
208+
};
209+
harness
210+
})
211+
}
212+
213+
/// Check that if this item is tagged with a proof_attribute, it is a valid harness.
214+
fn check_proof_attribute(&self, proof_attribute: &Attribute) {
215+
let span = proof_attribute.span;
216+
let tcx = self.tcx;
217+
expect_no_args(tcx, KaniAttributeKind::Proof, proof_attribute);
218+
if tcx.def_kind(self.item) != DefKind::Fn {
219+
tcx.sess.span_err(span, "the `proof` attribute can only be applied to functions");
220+
} else if tcx.generics_of(self.item).requires_monomorphization(tcx) {
221+
tcx.sess.span_err(span, "the `proof` attribute cannot be applied to generic functions");
222+
} else {
223+
let instance = Instance::mono(tcx, self.item);
224+
if !super::fn_abi(tcx, instance).args.is_empty() {
225+
tcx.sess.span_err(span, "functions used as harnesses cannot have any arguments");
89226
}
90-
KaniAttributeKind::Unstable => attrs.iter().for_each(|attr| {
91-
let _ = UnstableAttribute::try_from(*attr).map_err(|err| err.report(tcx));
92-
}),
93-
};
227+
}
94228
}
95229
}
96230

231+
/// An efficient check for the existence for a particular [`KaniAttributeKind`].
232+
/// Unlike querying [`KaniAttributes`] this method builds no new heap data
233+
/// structures and has short circuiting.
234+
fn has_kani_attribute<F: Fn(KaniAttributeKind) -> bool>(
235+
tcx: TyCtxt,
236+
def_id: DefId,
237+
predicate: F,
238+
) -> bool {
239+
tcx.get_attrs_unchecked(def_id).iter().filter_map(|a| attr_kind(tcx, a)).any(predicate)
240+
}
241+
242+
/// Same as [`KaniAttributes::is_harness`] but more efficient because less
243+
/// attribute parsing is performed.
97244
pub fn is_proof_harness(tcx: TyCtxt, def_id: DefId) -> bool {
98-
let attributes = extract_kani_attributes(tcx, def_id);
99-
attributes.contains_key(&KaniAttributeKind::Proof)
245+
has_kani_attribute(tcx, def_id, |a| matches!(a, KaniAttributeKind::Proof))
100246
}
101247

102248
/// Does this `def_id` have `#[rustc_test_marker]`?
@@ -112,77 +258,6 @@ pub fn test_harness_name(tcx: TyCtxt, def_id: DefId) -> String {
112258
parse_str_value(&marker).unwrap()
113259
}
114260

115-
/// Extract harness attributes for a given `def_id`.
116-
///
117-
/// We only extract attributes for harnesses that are local to the current crate.
118-
/// Note that all attributes should be valid by now.
119-
pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> HarnessAttributes {
120-
// Abort if not local.
121-
assert!(def_id.is_local(), "Expected a local item, but got: {def_id:?}");
122-
let attributes = extract_kani_attributes(tcx, def_id);
123-
trace!(?def_id, ?attributes, "extract_harness_attributes");
124-
assert!(attributes.contains_key(&KaniAttributeKind::Proof));
125-
attributes.into_iter().fold(HarnessAttributes::default(), |mut harness, (kind, attributes)| {
126-
match kind {
127-
KaniAttributeKind::ShouldPanic => harness.should_panic = true,
128-
KaniAttributeKind::Solver => {
129-
harness.solver = parse_solver(tcx, attributes[0]);
130-
}
131-
KaniAttributeKind::Stub => {
132-
harness.stubs = parse_stubs(tcx, def_id, attributes);
133-
}
134-
KaniAttributeKind::Unwind => harness.unwind_value = parse_unwind(tcx, attributes[0]),
135-
KaniAttributeKind::Proof => harness.proof = true,
136-
KaniAttributeKind::Unstable => {
137-
// Internal attribute which shouldn't exist here.
138-
unreachable!()
139-
}
140-
};
141-
harness
142-
})
143-
}
144-
145-
/// Check that any unstable API has been enabled. Otherwise, emit an error.
146-
///
147-
/// TODO: Improve error message by printing the span of the harness instead of the definition.
148-
pub fn check_unstable_features(tcx: TyCtxt, enabled_features: &[String], def_id: DefId) {
149-
if !matches!(tcx.type_of(def_id).skip_binder().kind(), TyKind::FnDef(..)) {
150-
// skip closures due to an issue with rustc.
151-
// https://github.com/model-checking/kani/pull/2406#issuecomment-1534333862
152-
return;
153-
}
154-
let attributes = extract_kani_attributes(tcx, def_id);
155-
if let Some(unstable_attrs) = attributes.get(&KaniAttributeKind::Unstable) {
156-
for attr in unstable_attrs {
157-
let unstable_attr = UnstableAttribute::try_from(*attr).unwrap();
158-
if !enabled_features.contains(&unstable_attr.feature) {
159-
// Reached an unstable attribute that was not enabled.
160-
report_unstable_forbidden(tcx, def_id, &unstable_attr);
161-
} else {
162-
debug!(enabled=?attr, ?def_id, "check_unstable_features");
163-
}
164-
}
165-
}
166-
}
167-
168-
/// Report misusage of an unstable feature that was not enabled.
169-
fn report_unstable_forbidden(
170-
tcx: TyCtxt,
171-
def_id: DefId,
172-
unstable_attr: &UnstableAttribute,
173-
) -> ErrorGuaranteed {
174-
let fn_name = tcx.def_path_str(def_id);
175-
tcx.sess
176-
.struct_err(format!(
177-
"Use of unstable feature `{}`: {}",
178-
unstable_attr.feature, unstable_attr.reason
179-
))
180-
.span_note(tcx.def_span(def_id), format!("the function `{fn_name}` is unstable:"))
181-
.note(format!("see issue {} for more information", unstable_attr.issue))
182-
.help(format!("use `-Z {}` to enable using this function.", unstable_attr.feature))
183-
.emit()
184-
}
185-
186261
fn expect_single<'a>(
187262
tcx: TyCtxt,
188263
kind: KaniAttributeKind,
@@ -200,38 +275,6 @@ fn expect_single<'a>(
200275
attr
201276
}
202277

203-
/// Check that if an item is tagged with a proof_attribute, it is a valid harness.
204-
fn check_proof_attribute(tcx: TyCtxt, def_id: DefId, proof_attribute: &Attribute) {
205-
let span = proof_attribute.span;
206-
expect_no_args(tcx, KaniAttributeKind::Proof, proof_attribute);
207-
if tcx.def_kind(def_id) != DefKind::Fn {
208-
tcx.sess.span_err(span, "the `proof` attribute can only be applied to functions");
209-
} else if tcx.generics_of(def_id).requires_monomorphization(tcx) {
210-
tcx.sess.span_err(span, "the `proof` attribute cannot be applied to generic functions");
211-
} else {
212-
let instance = Instance::mono(tcx, def_id);
213-
if !super::fn_abi(tcx, instance).args.is_empty() {
214-
tcx.sess.span_err(span, "functions used as harnesses cannot have any arguments");
215-
}
216-
}
217-
}
218-
219-
/// Partition all the attributes according to their kind.
220-
fn extract_kani_attributes(
221-
tcx: TyCtxt,
222-
def_id: DefId,
223-
) -> BTreeMap<KaniAttributeKind, Vec<&Attribute>> {
224-
let all_attributes = tcx.get_attrs_unchecked(def_id);
225-
all_attributes.iter().fold(BTreeMap::default(), |mut result, attribute| {
226-
// Get the string the appears after "kanitool::" in each attribute string.
227-
// Ex - "proof" | "unwind" etc.
228-
if let Some(kind) = attr_kind(tcx, attribute) {
229-
result.entry(kind).or_default().push(attribute)
230-
}
231-
result
232-
})
233-
}
234-
235278
/// Attribute used to mark a Kani lib API unstable.
236279
#[derive(Debug)]
237280
struct UnstableAttribute {
@@ -328,7 +371,7 @@ fn parse_unwind(tcx: TyCtxt, attr: &Attribute) -> Option<u32> {
328371
}
329372
}
330373

331-
fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: Vec<&Attribute>) -> Vec<Stub> {
374+
fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec<Stub> {
332375
let current_module = tcx.parent_module_from_def_id(harness.expect_local());
333376
let check_resolve = |attr: &Attribute, name: &str| {
334377
let result = resolve::resolve_fn(tcx, current_module, name);

‎kani-compiler/src/kani_middle/metadata.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,11 +10,11 @@ use kani_metadata::{ArtifactType, HarnessAttributes, HarnessMetadata};
1010
use rustc_hir::def_id::DefId;
1111
use rustc_middle::ty::{Instance, InstanceDef, TyCtxt};
1212

13-
use super::{attributes::extract_harness_attributes, SourceLocation};
13+
use super::{attributes::KaniAttributes, SourceLocation};
1414

1515
/// Create the harness metadata for a proof harness for a given function.
1616
pub fn gen_proof_metadata(tcx: TyCtxt, def_id: DefId, base_name: &Path) -> HarnessMetadata {
17-
let attributes = extract_harness_attributes(tcx, def_id);
17+
let attributes = KaniAttributes::for_item(tcx, def_id).harness_attributes();
1818
let pretty_name = tcx.def_path_str(def_id);
1919
// Main function a special case in order to support `--function main`
2020
// TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129

0 commit comments

Comments
 (0)