-
Notifications
You must be signed in to change notification settings - Fork 99
/
Copy pathannotations.rs
136 lines (128 loc) · 5.1 KB
/
annotations.rs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//! This file contains code for extracting stubbing-related attributes.
use rustc_ast::Attribute;
use rustc_data_structures::fx::FxHashMap;
use rustc_driver::RunCompiler;
use rustc_driver::{Callbacks, Compilation};
use rustc_errors::ErrorGuaranteed;
use rustc_hir::def_id::{DefId, LocalDefId};
use rustc_hir::definitions::DefPathHash;
use rustc_interface::interface::Compiler;
use rustc_interface::Queries;
use rustc_middle::ty::TyCtxt;
use crate::kani_middle::attributes::{extract_path_arguments, partition_kanitool_attributes};
use crate::kani_middle::resolve::resolve_path;
/// Collects the stubs from the harnesses in a crate, running rustc (to
/// expansion) with the supplied arguments `rustc_args`.
pub fn collect_stub_mappings(
rustc_args: &[String],
) -> Result<FxHashMap<String, FxHashMap<DefPathHash, DefPathHash>>, ErrorGuaranteed> {
let mut callbacks = CollectorCallbacks::default();
let compiler = RunCompiler::new(rustc_args, &mut callbacks);
compiler.run().map(|_| callbacks.stub_mapping)
}
/// A rustc callback that is used to collect the stub mappings specified for
/// each harness.
#[derive(Default)]
struct CollectorCallbacks {
stub_mapping: FxHashMap<String, FxHashMap<DefPathHash, DefPathHash>>,
}
impl Callbacks for CollectorCallbacks {
/// The main callback, invoked after the HIR has been created.
fn after_expansion<'tcx>(
&mut self,
_compiler: &Compiler,
queries: &'tcx Queries<'tcx>,
) -> Compilation {
queries.global_ctxt().unwrap().peek_mut().enter(|tcx| {
for item in tcx.hir_crate_items(()).items() {
let local_def_id = item.owner_id.def_id;
let def_id = local_def_id.to_def_id();
let (proof, other) = partition_kanitool_attributes(tcx.get_attrs_unchecked(def_id));
// Ignore anything that is not a harness
if proof.is_empty() {
continue;
}
let mut stub_pairs = FxHashMap::default();
for (name, attr) in other {
if name == "stub" {
update_stub_mapping(tcx, local_def_id, attr, &mut stub_pairs);
}
}
let harness_name = tcx.def_path_str(def_id);
self.stub_mapping.insert(harness_name, stub_pairs);
}
tcx.sess.abort_if_errors();
// We do not need to continue compilation after we've collected the stub mappings
Compilation::Stop
})
}
}
/// Given a `kani::stub` attribute, tries to extract a pair of paths (the
/// original function/method, and its stub). Returns `None` and errors if the
/// attribute's arguments are not two paths.
fn extract_stubbing_pair(
tcx: TyCtxt,
harness: LocalDefId,
attr: &Attribute,
) -> Option<(DefId, DefId)> {
// Extract the attribute arguments
let args = extract_path_arguments(attr);
if args.len() != 2 {
tcx.sess.span_err(
attr.span,
format!("Attribute `kani::stub` takes two path arguments; found {}", args.len()),
);
return None;
}
if args.iter().any(|arg| arg.is_none()) {
tcx.sess.span_err(
attr.span,
"Attribute `kani::stub` takes two path arguments; \
found argument that is not a path",
);
return None;
}
// Resolve the attribute arguments to `DefId`s
let current_module = tcx.parent_module_from_def_id(harness);
let resolve = |name: &str| -> Option<DefId> {
let maybe_resolved = resolve_path(tcx, current_module, name);
if let Some(def_id) = maybe_resolved {
tracing::debug!(?def_id, "Resolved {name} to {}", tcx.def_path_str(def_id));
} else {
tcx.sess.span_err(attr.span, format!("unable to resolve function/method: {name}"));
}
maybe_resolved
};
let orig = resolve(args[0].as_deref().unwrap());
let stub = resolve(args[1].as_deref().unwrap());
Some((orig?, stub?))
}
/// Updates the running map `stub_pairs` that maps a function/method to its
/// stub. Errors if a function/method is mapped more than once.
fn update_stub_mapping(
tcx: TyCtxt,
harness: LocalDefId,
attr: &Attribute,
stub_pairs: &mut FxHashMap<DefPathHash, DefPathHash>,
) {
if let Some((orig_id, stub_id)) = extract_stubbing_pair(tcx, harness, attr) {
let orig_hash = tcx.def_path_hash(orig_id);
let stub_hash = tcx.def_path_hash(stub_id);
let other_opt = stub_pairs.insert(orig_hash, stub_hash);
if let Some(other) = other_opt {
if other != stub_hash {
tcx.sess.span_err(
attr.span,
format!(
"duplicate stub mapping: {} mapped to {} and {}",
tcx.def_path_str(orig_id),
tcx.def_path_str(stub_id),
tcx.def_path_str(tcx.def_path_hash_to_def_id(other, &mut || panic!()))
),
);
}
}
}
}