Skip to content

Commit

Permalink
Merge pull request #773 from viperproject/type-is-copy
Browse files Browse the repository at this point in the history
Fix type_is_copy
  • Loading branch information
fpoli authored Nov 22, 2021
2 parents 3efd1ab + 9ebda62 commit 4dfd34d
Show file tree
Hide file tree
Showing 12 changed files with 417 additions and 139 deletions.
31 changes: 12 additions & 19 deletions analysis/src/domains/definitely_initialized/state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -182,20 +182,13 @@ impl<'mir, 'tcx: 'mir> DefinitelyInitializedState<'mir, 'tcx> {

/// If the operand is move, make the place uninitialised
/// If the place is a Copy type, uninitialise the place iif `move_out_copy_types` is true.
fn apply_operand_effect(
&mut self,
operand: &mir::Operand<'tcx>,
location: mir::Location,
move_out_copy_types: bool,
) {
fn apply_operand_effect(&mut self, operand: &mir::Operand<'tcx>, move_out_copy_types: bool) {
if let mir::Operand::Move(place) = operand {
let mut uninitialise = true;
if !move_out_copy_types {
let ty = place.ty(&self.mir.local_decls, self.tcx).ty;
let span = self.mir.source_info(location).span;
let param_env = self.tcx.param_env(self.def_id);
let is_copy = ty.is_copy_modulo_regions(self.tcx.at(span), param_env);
uninitialise = !is_copy;
uninitialise = !is_copy(self.tcx, ty, param_env);
}
if uninitialise {
self.set_place_uninitialised(*place);
Expand All @@ -217,16 +210,16 @@ impl<'mir, 'tcx: 'mir> DefinitelyInitializedState<'mir, 'tcx> {
| mir::Rvalue::Cast(_, ref operand, _)
| mir::Rvalue::UnaryOp(_, ref operand)
| mir::Rvalue::Use(ref operand) => {
self.apply_operand_effect(operand, location, move_out_copy_types);
self.apply_operand_effect(operand, move_out_copy_types);
}
mir::Rvalue::BinaryOp(_, box (ref operand1, ref operand2))
| mir::Rvalue::CheckedBinaryOp(_, box (ref operand1, ref operand2)) => {
self.apply_operand_effect(operand1, location, move_out_copy_types);
self.apply_operand_effect(operand2, location, move_out_copy_types);
self.apply_operand_effect(operand1, move_out_copy_types);
self.apply_operand_effect(operand2, move_out_copy_types);
}
mir::Rvalue::Aggregate(_, ref operands) => {
for operand in operands.iter() {
self.apply_operand_effect(operand, location, move_out_copy_types);
self.apply_operand_effect(operand, move_out_copy_types);
}
}
_ => {}
Expand Down Expand Up @@ -260,7 +253,7 @@ impl<'mir, 'tcx: 'mir> DefinitelyInitializedState<'mir, 'tcx> {
mir::TerminatorKind::SwitchInt { ref discr, .. } => {
// only operand has an effect on definitely initialized places, all successors
// get the same state
new_state.apply_operand_effect(discr, location, move_out_copy_types);
new_state.apply_operand_effect(discr, move_out_copy_types);

for &bb in terminator.successors() {
res_vec.push((bb, new_state.clone()));
Expand All @@ -286,7 +279,7 @@ impl<'mir, 'tcx: 'mir> DefinitelyInitializedState<'mir, 'tcx> {
unwind,
} => {
new_state.set_place_uninitialised(place);
new_state.apply_operand_effect(value, location, move_out_copy_types);
new_state.apply_operand_effect(value, move_out_copy_types);
new_state.set_place_initialised(place);
res_vec.push((target, new_state));

Expand All @@ -303,9 +296,9 @@ impl<'mir, 'tcx: 'mir> DefinitelyInitializedState<'mir, 'tcx> {
..
} => {
for arg in args.iter() {
new_state.apply_operand_effect(arg, location, move_out_copy_types);
new_state.apply_operand_effect(arg, move_out_copy_types);
}
new_state.apply_operand_effect(func, location, move_out_copy_types);
new_state.apply_operand_effect(func, move_out_copy_types);
if let Some((place, bb)) = destination {
new_state.set_place_initialised(place);
res_vec.push((bb, new_state));
Expand All @@ -322,7 +315,7 @@ impl<'mir, 'tcx: 'mir> DefinitelyInitializedState<'mir, 'tcx> {
cleanup,
..
} => {
new_state.apply_operand_effect(cond, location, move_out_copy_types);
new_state.apply_operand_effect(cond, move_out_copy_types);
res_vec.push((target, new_state));

if let Some(bb) = cleanup {
Expand All @@ -337,7 +330,7 @@ impl<'mir, 'tcx: 'mir> DefinitelyInitializedState<'mir, 'tcx> {
..
} => {
// TODO: resume_arg?
new_state.apply_operand_effect(value, location, move_out_copy_types);
new_state.apply_operand_effect(value, move_out_copy_types);
res_vec.push((resume, new_state));

if let Some(bb) = drop {
Expand Down
2 changes: 2 additions & 0 deletions analysis/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,10 @@ extern crate polonius_engine;
extern crate rustc_borrowck;
extern crate rustc_data_structures;
extern crate rustc_index;
extern crate rustc_infer;
extern crate rustc_middle;
extern crate rustc_span;
extern crate rustc_trait_selection;
extern crate serde;

pub mod abstract_interpretation;
Expand Down
25 changes: 25 additions & 0 deletions analysis/src/mir_utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,12 @@
use log::trace;
use rustc_data_structures::fx::FxHashSet;
use rustc_infer::infer::TyCtxtInferExt;
use rustc_middle::{
mir,
ty::{self, TyCtxt},
};
use rustc_trait_selection::infer::InferCtxtExt;

/// Convert a `location` to a string representing the statement or terminator at that `location`
pub fn location_to_stmt_str(location: mir::Location, mir: &mir::Body) -> String {
Expand Down Expand Up @@ -294,3 +296,26 @@ impl std::fmt::Display for DisplayPlaceRef<'_> {
Ok(())
}
}

pub fn is_copy<'tcx>(
tcx: ty::TyCtxt<'tcx>,
ty: ty::Ty<'tcx>,
param_env: ty::ParamEnv<'tcx>,
) -> bool {
if let Some(copy_trait) = tcx.lang_items().copy_trait() {
// We need this check because `type_implements_trait`
// panics when called on reference types.
if let ty::TyKind::Ref(_, _, mutability) = ty.kind() {
// Shared references are copy, mutable references are not.
matches!(mutability, mir::Mutability::Not)
} else {
tcx.infer_ctxt().enter(|infcx| {
infcx
.type_implements_trait(copy_trait, ty, ty::List::empty(), param_env)
.must_apply_considering_regions()
})
}
} else {
false
}
}
7 changes: 7 additions & 0 deletions analysis/tests/test_cases/definitely_initialized/array.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
#[analyzer::run]
fn main() {
let x = [1, 2, 3];
drop(x);
let y = [Box::new(4)];
drop(y);
}
Loading

0 comments on commit 4dfd34d

Please sign in to comment.