Skip to content
This repository has been archived by the owner on Aug 22, 2024. It is now read-only.

Update MIRAI to work with latest nightly #1228

Merged
merged 11 commits into from
Jul 29, 2023
Merged

Update MIRAI to work with latest nightly #1228

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
839cb53
nightly-2023-05-16
hermanventer Jul 17, 2023
69250fb
nightly-2023-05-23
hermanventer Jul 17, 2023
913a806
nightly-2023-05-30
hermanventer Jul 17, 2023
0f766d0
nightly-2023-06-06
hermanventer Jul 25, 2023
30bdfca
nightly-2023-06-13
hermanventer Jul 25, 2023
38d92d2
nightly-2023-06-20
hermanventer Jul 25, 2023
d3eed30
nightly-2023-06-27
hermanventer Jul 26, 2023
30f3175
nightly-2023-07-04
hermanventer Jul 26, 2023
d163cf4
nightly-2023-07-11
hermanventer Jul 26, 2023
3787414
nightly-2023-07-18
hermanventer Jul 26, 2023
99e9fc5
nightly-2023-07-28
hermanventer Jul 26, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
325 changes: 125 additions & 200 deletions Cargo.lock
View file
Open in desktop

Large diffs are not rendered by default.

1 change: 1 addition & 0 deletions Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
[workspace]
resolver = "2"

members = [
"annotations",
Expand Down
Binary file modified binaries/summary_store.tar
View file
Open in desktop
Binary file not shown.
2 changes: 1 addition & 1 deletion checker/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ shellwords = "*"
sled = "*"
tar = "0.4.38"
tempfile = "*"
z3-sys = { version = "*", git="https://github.com/prove-rs/z3.rs.git", features = ["static-link-z3"], optional = true }
z3-sys = { version = "*", features = ["static-link-z3"], optional = true }

[dev-dependencies]
walkdir = "*"
Expand Down
252 changes: 133 additions & 119 deletions checker/src/block_visitor.rs
View file
Open in desktop

Large diffs are not rendered by default.

90 changes: 51 additions & 39 deletions checker/src/body_visitor.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,7 @@
use rustc_errors::DiagnosticBuilder;
use rustc_hir::def_id::DefId;
use rustc_middle::mir;
use rustc_middle::ty::subst::SubstsRef;
use rustc_middle::ty::{AdtDef, Const, Ty, TyCtxt, TyKind, TypeAndMut, UintTy};
use rustc_middle::ty::{AdtDef, Const, GenericArgsRef, Ty, TyCtxt, TyKind, TypeAndMut, UintTy};

use crate::abstract_value::{self, AbstractValue, AbstractValueTrait, BOTTOM};
use crate::block_visitor::BlockVisitor;
Expand Down Expand Up @@ -295,7 +294,7 @@
let dominators = self.mir.basic_blocks.dominators();
for (location1, callee_defid1) in self.block_to_call.iter() {
for (location2, callee_defid2) in self.block_to_call.iter() {
if location1 != location2 && location1.dominates(*location2, &dominators) {
if location1 != location2 && location1.dominates(*location2, dominators) {
self.cv.call_graph.add_dom(*callee_defid1, *callee_defid2);
}
}
Expand Down Expand Up @@ -634,7 +633,7 @@
if self.active_calls_map.contains_key(&def_id) {
return;
}
let generic_args = self.cv.substs_cache.get(&def_id).cloned();
let generic_args = self.cv.generic_args_cache.get(&def_id).cloned();
let callee_generic_argument_map = if let Some(generic_args) = generic_args {
self.type_visitor()
.get_generic_arguments_map(def_id, generic_args, &[])
Expand Down Expand Up @@ -1723,13 +1722,13 @@
let union_type = self
.type_visitor()
.get_path_rustc_type(qualifier, self.current_span);
if let TyKind::Adt(def, substs) = union_type.kind() {
let substs = self
if let TyKind::Adt(def, args) = union_type.kind() {
let args = self
.type_visitor
.specialize_substs(substs, &self.type_visitor().generic_argument_map);
.specialize_generic_args(args, &self.type_visitor().generic_argument_map);
for (i, field) in def.all_fields().enumerate() {
let target_type = self.type_visitor().specialize_generic_argument_type(
field.ty(self.tcx, substs),
field.ty(self.tcx, args),
&self.type_visitor().generic_argument_map,
);
let target_path = Path::new_union_field(qualifier.clone(), i, *num_cases);
Expand Down Expand Up @@ -1794,7 +1793,7 @@
fn add_leaf_fields_for<'a>(
path: Rc<Path>,
def: &'a AdtDef,
substs: SubstsRef<'a>,
args: GenericArgsRef<'a>,
tcx: TyCtxt<'a>,
accumulator: &mut Vec<(Rc<Path>, Ty<'a>)>,
) {
Expand Down Expand Up @@ -1823,9 +1822,9 @@
let variant = def.variants().iter().next().expect("at least one variant");
for (i, field) in variant.fields.iter().enumerate() {
let field_path = Path::new_field(path.clone(), i);
let field_ty = field.ty(tcx, substs);
if let TyKind::Adt(def, substs) = field_ty.kind() {
add_leaf_fields_for(field_path, def, substs, tcx, accumulator)
let field_ty = field.ty(tcx, args);
if let TyKind::Adt(def, args) = field_ty.kind() {
add_leaf_fields_for(field_path, def, args, tcx, accumulator)
} else {
accumulator.push((field_path, field_ty))
}
Expand Down Expand Up @@ -1860,16 +1859,17 @@
s_path = Path::new_field(s_path, 0);
ty = self.type_visitor().remove_transparent_wrapper(ty);
}
let source_rustc_type = self
.tcx
.mk_ref(*region, rustc_middle::ty::TypeAndMut { ty, mutbl: *mutbl });
let source_rustc_type = Ty::new_ref(
self.tcx,
*region,
rustc_middle::ty::TypeAndMut { ty, mutbl: *mutbl },
);
let s_ref_val = AbstractValue::make_reference(s_path);
let source_path = Path::new_computed(s_ref_val);
if self.type_visitor.is_slice_pointer(source_rustc_type.kind()) {
let pointer_path = Path::new_field(source_path.clone(), 0);
let pointer_type = self
.tcx
.mk_ptr(rustc_middle::ty::TypeAndMut { ty, mutbl: *mutbl });
let pointer_type =
Ty::new_ptr(self.tcx, rustc_middle::ty::TypeAndMut { ty, mutbl: *mutbl });

Check warning on line 1872 in checker/src/body_visitor.rs

View check run for this annotation

Codecov / codecov/patch

checker/src/body_visitor.rs#L1872 

Added line #L1872 was not covered by tests
source_fields.push((pointer_path, pointer_type));
let len_path = Path::new_length(source_path);
source_fields.push((len_path, self.tcx.types.usize));
Expand All @@ -1890,10 +1890,13 @@
_ => {
if self.type_visitor.is_slice_pointer(source_rustc_type.kind()) {
let pointer_path = Path::new_field(source_path.clone(), 0);
let pointer_type = self.tcx.mk_ptr(rustc_middle::ty::TypeAndMut {
ty: self.type_visitor.get_element_type(source_rustc_type),
mutbl: rustc_hir::Mutability::Not,
});
let pointer_type = Ty::new_ptr(
self.tcx,
rustc_middle::ty::TypeAndMut {
ty: self.type_visitor.get_element_type(source_rustc_type),
mutbl: rustc_hir::Mutability::Not,
},
);
source_fields.push((pointer_path, pointer_type));
let len_path = Path::new_length(source_path);
source_fields.push((len_path, self.tcx.types.usize));
Expand Down Expand Up @@ -1932,20 +1935,25 @@
t_path = Path::new_field(t_path, 0);
ty = self.type_visitor().remove_transparent_wrapper(ty);
}
let target_rustc_type = self
.tcx
.mk_ref(*region, rustc_middle::ty::TypeAndMut { ty, mutbl: *mutbl });
let target_rustc_type = Ty::new_ref(
self.tcx,
*region,
rustc_middle::ty::TypeAndMut { ty, mutbl: *mutbl },
);
let t_ref_val = AbstractValue::make_reference(t_path);
let target_path = Path::new_computed(t_ref_val);
if self
.type_visitor()
.is_slice_pointer(target_rustc_type.kind())
{
let pointer_path = Path::new_field(target_path.clone(), 0);
let pointer_type = self.tcx.mk_ptr(rustc_middle::ty::TypeAndMut {
ty: self.type_visitor.get_element_type(target_rustc_type),
mutbl: rustc_hir::Mutability::Not,
});
let pointer_type = Ty::new_ptr(
self.tcx,
rustc_middle::ty::TypeAndMut {
ty: self.type_visitor.get_element_type(target_rustc_type),
mutbl: rustc_hir::Mutability::Not,
},
);
target_fields.push((pointer_path, pointer_type));
let len_path = Path::new_length(target_path);
target_fields.push((len_path, self.tcx.types.usize));
Expand All @@ -1969,10 +1977,13 @@
.is_slice_pointer(target_rustc_type.kind())
{
let pointer_path = Path::new_field(target_path.clone(), 0);
let pointer_type = self.tcx.mk_ptr(rustc_middle::ty::TypeAndMut {
ty: self.type_visitor.get_element_type(target_rustc_type),
mutbl: rustc_hir::Mutability::Not,
});
let pointer_type = Ty::new_ptr(
self.tcx,
rustc_middle::ty::TypeAndMut {
ty: self.type_visitor.get_element_type(target_rustc_type),
mutbl: rustc_hir::Mutability::Not,
},
);
target_fields.push((pointer_path, pointer_type));
let len_path = Path::new_length(target_path);
target_fields.push((len_path, self.tcx.types.usize));
Expand Down Expand Up @@ -2662,18 +2673,19 @@
let union_type = self
.type_visitor()
.get_path_rustc_type(qualifier, self.current_span);
if let TyKind::Adt(def, substs) = union_type.kind() {
let substs = self
.type_visitor
.specialize_substs(substs, &self.type_visitor().generic_argument_map);
if let TyKind::Adt(def, args) = union_type.kind() {
let generic_args = self.type_visitor.specialize_generic_args(
args,
&self.type_visitor().generic_argument_map,
);
let source_field = def.all_fields().nth(*case_index).unwrap();
let source_type = self.type_visitor().specialize_generic_argument_type(
source_field.ty(self.tcx, substs),
source_field.ty(self.tcx, generic_args),
&self.type_visitor().generic_argument_map,
);
for (i, field) in def.all_fields().enumerate() {
let target_type = self.type_visitor().specialize_generic_argument_type(
field.ty(self.tcx, substs),
field.ty(self.tcx, generic_args),
&self.type_visitor().generic_argument_map,
);
let target_path =
Expand Down
Loading