Skip to content

Commit eb05f74

Browse files
artemagvanianartemagvanian
committed
Stop using visitor for instrumentation target finding
1 parent ff4862a commit eb05f74

File tree

3 files changed

+373
-165
lines changed

3 files changed

+373
-165
lines changed

‎kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs

+176-25
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,8 @@ use crate::kani_middle::{
1616
};
1717
use rustc_middle::ty::TyCtxt;
1818
use stable_mir::mir::{
19-
mono::Instance,
20-
visit::{Location, PlaceContext},
21-
BasicBlock, MirVisitor, Operand, Place, Rvalue,
19+
mono::Instance, BasicBlock, CopyNonOverlapping, InlineAsmOperand, NonDivergingIntrinsic,
20+
Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind,
2221
};
2322
use std::collections::HashSet;
2423

@@ -33,6 +32,13 @@ pub struct InstrumentationVisitor<'a, 'tcx> {
3332
tcx: TyCtxt<'tcx>,
3433
}
3534

35+
enum PlaceOperation {
36+
Read,
37+
Write,
38+
Deinit,
39+
Noop,
40+
}
41+
3642
impl<'a, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> {
3743
fn find_next(
3844
&mut self,
@@ -44,14 +50,11 @@ impl<'a, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> {
4450
SourceInstruction::Statement { idx, bb } => {
4551
let BasicBlock { statements, .. } = &body.blocks()[bb];
4652
let stmt = &statements[idx];
47-
self.visit_statement(stmt, self.__location_hack_remove_before_merging(stmt.span))
53+
self.check_statement(stmt)
4854
}
4955
SourceInstruction::Terminator { bb } => {
5056
let BasicBlock { terminator, .. } = &body.blocks()[bb];
51-
self.visit_terminator(
52-
terminator,
53-
self.__location_hack_remove_before_merging(terminator.span),
54-
)
57+
self.check_terminator(terminator)
5558
}
5659
}
5760
self.target.clone()
@@ -76,17 +79,152 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> {
7679
}
7780
}
7881

79-
impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> {
80-
fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) {
82+
impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> {
83+
fn check_statement(&mut self, stmt: &Statement) {
84+
let Statement { kind, .. } = stmt;
85+
match kind {
86+
StatementKind::Assign(place, rvalue) => {
87+
self.check_place(place, PlaceOperation::Write);
88+
self.check_rvalue(rvalue);
89+
}
90+
StatementKind::FakeRead(_, place) => {
91+
// According to the compiler docs, "When executed at runtime this is a nop." For
92+
// more info, see
93+
// https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.FakeRead,
94+
self.check_place(place, PlaceOperation::Noop);
95+
}
96+
StatementKind::SetDiscriminant { place, .. } => {
97+
self.check_place(place, PlaceOperation::Write);
98+
}
99+
StatementKind::Deinit(place) => {
100+
self.check_place(place, PlaceOperation::Deinit);
101+
}
102+
StatementKind::Retag(_, place) => {
103+
// According to the compiler docs, "These statements are currently only interpreted
104+
// by miri and only generated when -Z mir-emit-retag is passed." For more info, see
105+
// https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.Retag,
106+
self.check_place(place, PlaceOperation::Noop);
107+
}
108+
StatementKind::PlaceMention(place) => {
109+
// According to the compiler docs, "When executed at runtime, this computes the
110+
// given place, but then discards it without doing a load." For more info, see
111+
// https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.PlaceMention,
112+
self.check_place(place, PlaceOperation::Noop);
113+
}
114+
StatementKind::AscribeUserType { place, .. } => {
115+
// According to the compiler docs, "When executed at runtime this is a nop." For
116+
// more info, see
117+
// https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.AscribeUserType,
118+
self.check_place(place, PlaceOperation::Noop);
119+
}
120+
121+
StatementKind::Intrinsic(intrisic) => match intrisic {
122+
NonDivergingIntrinsic::Assume(operand) => {
123+
self.check_operand(operand);
124+
}
125+
NonDivergingIntrinsic::CopyNonOverlapping(CopyNonOverlapping {
126+
src,
127+
dst,
128+
count,
129+
}) => {
130+
self.check_operand(src);
131+
self.check_operand(dst);
132+
self.check_operand(count);
133+
}
134+
},
135+
StatementKind::StorageLive(_)
136+
| StatementKind::StorageDead(_)
137+
| StatementKind::Coverage(_)
138+
| StatementKind::ConstEvalCounter
139+
| StatementKind::Nop => {}
140+
}
141+
}
142+
143+
fn check_terminator(&mut self, term: &Terminator) {
144+
let Terminator { kind, .. } = term;
145+
match kind {
146+
TerminatorKind::Goto { .. }
147+
| TerminatorKind::Resume
148+
| TerminatorKind::Abort
149+
| TerminatorKind::Unreachable
150+
| TerminatorKind::Return => {}
151+
TerminatorKind::Assert { cond, .. } => {
152+
self.check_operand(cond);
153+
}
154+
TerminatorKind::Drop { place, .. } => {
155+
// According to the documentation, "After drop elaboration: Drop terminators are a
156+
// complete nop for types that have no drop glue. For other types, Drop terminators
157+
// behave exactly like a call to core::mem::drop_in_place with a pointer to the
158+
// given place." Since we check arguments when instrumenting function calls, perhaps
159+
// we need to check that one, too. For more info, see:
160+
// https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.TerminatorKind.html#variant.Drop
161+
self.check_place(place, PlaceOperation::Read);
162+
}
163+
TerminatorKind::Call { func, args, destination, target: _, unwind: _ } => {
164+
self.check_operand(func);
165+
for arg in args {
166+
self.check_operand(arg);
167+
}
168+
self.check_place(destination, PlaceOperation::Write);
169+
}
170+
TerminatorKind::InlineAsm { operands, .. } => {
171+
for op in operands {
172+
let InlineAsmOperand { in_value, out_place, raw_rpr: _ } = op;
173+
if let Some(input) = in_value {
174+
self.check_operand(input);
175+
}
176+
if let Some(output) = out_place {
177+
self.check_place(output, PlaceOperation::Write);
178+
}
179+
}
180+
}
181+
TerminatorKind::SwitchInt { discr, .. } => {
182+
self.check_operand(discr);
183+
}
184+
}
185+
}
186+
187+
fn check_rvalue(&mut self, rvalue: &Rvalue) {
81188
match rvalue {
82-
Rvalue::AddressOf(..) | Rvalue::Ref(..) => {
83-
// These operations are always legitimate for us.
189+
Rvalue::AddressOf(_, place) | Rvalue::Ref(_, _, place) => {
190+
self.check_place(place, PlaceOperation::Noop);
191+
}
192+
Rvalue::Aggregate(_, operands) => {
193+
for op in operands {
194+
self.check_operand(op);
195+
}
196+
}
197+
Rvalue::BinaryOp(_, lhs, rhs) | Rvalue::CheckedBinaryOp(_, lhs, rhs) => {
198+
self.check_operand(lhs);
199+
self.check_operand(rhs);
200+
}
201+
Rvalue::Cast(_, op, _)
202+
| Rvalue::Repeat(op, _)
203+
| Rvalue::ShallowInitBox(op, ..)
204+
| Rvalue::UnaryOp(_, op)
205+
| Rvalue::Use(op) => {
206+
self.check_operand(op);
207+
}
208+
Rvalue::CopyForDeref(place) | Rvalue::Discriminant(place) | Rvalue::Len(place) => {
209+
self.check_place(place, PlaceOperation::Read);
210+
}
211+
Rvalue::ThreadLocalRef(..) | Rvalue::NullaryOp(..) => {}
212+
}
213+
}
214+
215+
fn check_operand(&mut self, operand: &Operand) {
216+
match operand {
217+
Operand::Copy(place) | Operand::Move(place) => {
218+
self.check_place(place, PlaceOperation::Read)
219+
}
220+
Operand::Constant(_) => {
221+
// Those should be safe to skip, as they are either constants or statics. In the
222+
// latter case, we handle them in regular uninit visior
84223
}
85-
_ => self.super_rvalue(rvalue, location),
86224
}
87225
}
88226

89-
fn visit_place(&mut self, place: &Place, ptx: PlaceContext, location: Location) {
227+
fn check_place(&mut self, place: &Place, place_operation: PlaceOperation) {
90228
// Match the place by whatever it is pointing to and find an intersection with the targets.
91229
if self
92230
.points_to
@@ -95,18 +233,31 @@ impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> {
95233
.next()
96234
.is_some()
97235
{
98-
// If we are mutating the place, initialize it.
99-
if ptx.is_mutating() {
100-
self.push_target(MemoryInitOp::SetRef {
101-
operand: Operand::Copy(place.clone()),
102-
value: true,
103-
position: InsertPosition::After,
104-
});
105-
} else {
106-
// Otherwise, check its initialization.
107-
self.push_target(MemoryInitOp::CheckRef { operand: Operand::Copy(place.clone()) });
236+
match place_operation {
237+
PlaceOperation::Write => {
238+
// If we are mutating the place, initialize it.
239+
self.push_target(MemoryInitOp::SetRef {
240+
operand: Operand::Copy(place.clone()),
241+
value: true,
242+
position: InsertPosition::After,
243+
})
244+
}
245+
PlaceOperation::Deinit => {
246+
// If we are mutating the place, initialize it.
247+
self.push_target(MemoryInitOp::SetRef {
248+
operand: Operand::Copy(place.clone()),
249+
value: false,
250+
position: InsertPosition::After,
251+
})
252+
}
253+
PlaceOperation::Read => {
254+
// Otherwise, check its initialization.
255+
self.push_target(MemoryInitOp::CheckRef {
256+
operand: Operand::Copy(place.clone()),
257+
});
258+
}
259+
PlaceOperation::Noop => {}
108260
}
109261
}
110-
self.super_place(place, ptx, location)
111262
}
112263
}

‎kani-compiler/src/kani_middle/transform/check_uninit/mod.rs

+3-11
Original file line numberDiff line numberDiff line change
@@ -13,12 +13,10 @@ use rustc_middle::ty::TyCtxt;
1313
use rustc_smir::rustc_internal;
1414
use stable_mir::{
1515
mir::{
16-
mono::Instance, visit::Location, AggregateKind, BasicBlock, Body, ConstOperand, Mutability,
17-
Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction,
18-
},
19-
ty::{
20-
FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Span, Ty, TyConst, TyKind, UintTy,
16+
mono::Instance, AggregateKind, BasicBlock, Body, ConstOperand, Mutability, Operand, Place,
17+
Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction,
2118
},
19+
ty::{FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyConst, TyKind, UintTy},
2220
CrateDef,
2321
};
2422
use std::collections::HashMap;
@@ -39,12 +37,6 @@ pub trait TargetFinder {
3937
body: &MutableBody,
4038
source: &SourceInstruction,
4139
) -> Option<InitRelevantInstruction>;
42-
43-
/// TODO: This is just a temporary fix to unblock me because I couldn't create Location
44-
/// directly. Perhaps we need to make a change in StableMIR to allow creating Location.
45-
fn __location_hack_remove_before_merging(&self, span: Span) -> Location {
46-
unsafe { std::mem::transmute(span) }
47-
}
4840
}
4941

5042
// Function bodies of those functions will not be instrumented as not to cause infinite recursion.

0 commit comments

Comments
 (0)