Skip to content

Commit

Permalink
Update dependencies (rustc nightly-2023-04-01, viper v-2023-03-29-1448)
Browse files Browse the repository at this point in the history
  • Loading branch information
Aurel300 authored and vakaras committed May 23, 2023
1 parent aa8844c commit cd17b7f
Show file tree
Hide file tree
Showing 99 changed files with 780 additions and 845 deletions.
731 changes: 403 additions & 328 deletions Cargo.lock

Large diffs are not rendered by default.

5 changes: 3 additions & 2 deletions analysis/src/domains/definitely_accessible/state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ use crate::{
};
use log::info;
use prusti_rustc_interface::{
abi::FieldIdx,
data_structures::fx::{FxHashMap, FxHashSet},
middle::{mir, ty, ty::TyCtxt},
span::source_map::SourceMap,
Expand Down Expand Up @@ -237,7 +238,7 @@ fn pretty_print_place<'tcx>(
fn describe_field_from_ty(
tcx: TyCtxt<'_>,
ty: ty::Ty<'_>,
field: mir::Field,
field: FieldIdx,
variant_index: Option<VariantIdx>,
) -> Option<String> {
if ty.is_box() {
Expand All @@ -252,7 +253,7 @@ fn describe_field_from_ty(
} else {
def.non_enum_variant()
};
Some(variant.fields[field.index()].ident(tcx).to_string())
Some(variant.fields[field].ident(tcx).to_string())
}
ty::TyKind::Tuple(_) => Some(field.index().to_string()),
ty::TyKind::Ref(_, ty, _) | ty::TyKind::RawPtr(ty::TypeAndMut { ty, .. }) => {
Expand Down
16 changes: 0 additions & 16 deletions analysis/src/domains/definitely_initialized/state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -270,22 +270,6 @@ impl<'mir, 'tcx: 'mir> DefinitelyInitializedState<'mir, 'tcx> {
res_vec.push((bb, Self::new_top(self.def_id, self.mir, self.tcx)));
}
}
mir::TerminatorKind::DropAndReplace {
place,
ref value,
target,
unwind,
} => {
new_state.set_place_uninitialised(place);
new_state.apply_operand_effect(value, move_out_copy_types);
new_state.set_place_initialised(place);
res_vec.push((target, new_state));

if let Some(bb) = unwind {
// imprecision for error states
res_vec.push((bb, Self::new_top(self.def_id, self.mir, self.tcx)));
}
}
mir::TerminatorKind::Call {
ref func,
ref args,
Expand Down
9 changes: 5 additions & 4 deletions analysis/src/mir_utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
//! copied from prusti-interface/utils
use prusti_rustc_interface::{
abi::FieldIdx,
data_structures::fx::FxHashSet,
infer::infer::TyCtxtInferExt,
middle::{
Expand Down Expand Up @@ -139,7 +140,7 @@ pub fn expand_struct_place<'tcx, P: PlaceImpl<'tcx> + std::marker::Copy>(
.unwrap_or_else(|| def.non_enum_variant());
for (index, field_def) in variant.fields.iter().enumerate() {
if Some(index) != without_field {
let field = mir::Field::from_usize(index);
let field = FieldIdx::from_usize(index);
let field_place =
tcx.mk_place_field(place.to_mir_place(), field, field_def.ty(tcx, substs));
places.push(P::from_mir_place(field_place));
Expand All @@ -149,7 +150,7 @@ pub fn expand_struct_place<'tcx, P: PlaceImpl<'tcx> + std::marker::Copy>(
ty::Tuple(slice) => {
for (index, arg) in slice.iter().enumerate() {
if Some(index) != without_field {
let field = mir::Field::from_usize(index);
let field = FieldIdx::from_usize(index);
let field_place = tcx.mk_place_field(place.to_mir_place(), field, arg);
places.push(P::from_mir_place(field_place));
}
Expand All @@ -158,7 +159,7 @@ pub fn expand_struct_place<'tcx, P: PlaceImpl<'tcx> + std::marker::Copy>(
ty::Closure(_, substs) => {
for (index, subst_ty) in substs.as_closure().upvar_tys().enumerate() {
if Some(index) != without_field {
let field = mir::Field::from_usize(index);
let field = FieldIdx::from_usize(index);
let field_place = tcx.mk_place_field(place.to_mir_place(), field, subst_ty);
places.push(P::from_mir_place(field_place));
}
Expand All @@ -167,7 +168,7 @@ pub fn expand_struct_place<'tcx, P: PlaceImpl<'tcx> + std::marker::Copy>(
ty::Generator(_, substs, _) => {
for (index, subst_ty) in substs.as_generator().upvar_tys().enumerate() {
if Some(index) != without_field {
let field = mir::Field::from_usize(index);
let field = FieldIdx::from_usize(index);
let field_place = tcx.mk_place_field(place.to_mir_place(), field, subst_ty);
places.push(P::from_mir_place(field_place));
}
Expand Down
3 changes: 1 addition & 2 deletions analysis/tests/test_cases/gen_accessibility/create-box.rs
Original file line number Diff line number Diff line change
@@ -1,12 +1,11 @@
#![feature(box_patterns)]
#![feature(box_syntax)]

fn use_box(v: i32) -> Box<i32> {
let x = Box::new(v);
let y = *x;
assert!(v == y);
let z = Box::new(y);
assert!(v == *z);
let result = box *z;
let result = Box::new(*z);
result
}
1 change: 0 additions & 1 deletion analysis/tests/test_cases/gen_accessibility/deref.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
#![feature(box_patterns)]
#![feature(box_syntax)]

struct InfiniteList1 {
next: Box<InfiniteList1>
Expand Down
18 changes: 8 additions & 10 deletions analysis/tests/test_cases/gen_accessibility/loops/tmp-in-guard.rs
Original file line number Diff line number Diff line change
@@ -1,53 +1,51 @@
#![feature(box_syntax)]

fn random() -> u32 {
unimplemented!()
}

fn test1() {
let mut tmp = box box random();
let mut tmp = Box::new(Box::new(random()));
let tmp_ref = &tmp;
let tmp_ref_mut = &mut tmp;

while {
let guard = random() < 55;

let mut tmp = box box random();
let mut tmp = Box::new(Box::new(random()));
let tmp_ref = &tmp;
let tmp_ref_mut = &mut tmp;

guard
} {
let mut tmp = box box random();
let mut tmp = Box::new(Box::new(random()));
let tmp_ref = &tmp;
let tmp_ref_mut = &mut tmp;
}

let mut tmp = box box random();
let mut tmp = Box::new(Box::new(random()));
let tmp_ref = &tmp;
let tmp_ref_mut = &mut tmp;
}

fn test2() {
let mut tmp = box box random();
let mut tmp = Box::new(Box::new(random()));
let tmp_ref = &tmp;
let tmp_ref_mut = &mut tmp;

while {
let guard = random() < 55;

let mut tmp = box box random();
let mut tmp = Box::new(Box::new(random()));
let tmp_ref = &tmp;
let tmp_ref_mut = &mut tmp;

guard
} {
let mut tmp = box box random();
let mut tmp = Box::new(Box::new(random()));
let tmp_ref = &tmp;
let tmp_ref_mut = &mut tmp;
}

let mut tmp = box box random();
let mut tmp = Box::new(Box::new(random()));
let tmp_ref = &tmp;
let tmp_ref_mut = &mut tmp;
}
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
#![feature(box_patterns)]
#![feature(box_syntax)]

use std::borrow::BorrowMut;

Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
//! Example of reassignment
#![feature(box_patterns)]
#![feature(box_syntax)]

struct InfiniteList {
val: i32,
Expand Down
1 change: 0 additions & 1 deletion prusti-common/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@
// file, You can obtain one at http://mozilla.org/MPL/2.0/.

#![feature(box_patterns)]
#![feature(box_syntax)]
#![deny(unused_must_use)]
#![warn(clippy::disallowed_types)]

Expand Down
2 changes: 1 addition & 1 deletion prusti-common/src/vir/optimizations/folding/expressions.rs
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ impl ExprOptimizer {
}

fn restore_unfoldings_boxed(unfolding_map: UnfoldingMap, expr: Box<ast::Expr>) -> Box<ast::Expr> {
box restore_unfoldings(unfolding_map, *expr)
Box::new(restore_unfoldings(unfolding_map, *expr))
}

/// Restore unfoldings on a given expression.
Expand Down
20 changes: 10 additions & 10 deletions prusti-common/src/vir/optimizations/functions/simplifier.rs
Original file line number Diff line number Diff line change
Expand Up @@ -63,8 +63,8 @@ impl ExprSimplifier {
position: pos,
}) => ast::Expr::BinOp(ast::BinOp {
op_kind: ast::BinaryOpKind::NeCmp,
left: box left,
right: box right,
left: Box::new(left),
right: Box::new(right),
position: pos,
}),
ast::Expr::BinOp(ast::BinOp {
Expand Down Expand Up @@ -179,8 +179,8 @@ impl ExprSimplifier {
position: pos,
}) => ast::Expr::BinOp(ast::BinOp {
op_kind: ast::BinaryOpKind::And,
left: box Self::apply_rules(op1),
right: box Self::apply_rules(op2),
left: Box::new(Self::apply_rules(op1)),
right: Box::new(Self::apply_rules(op2)),
position: pos,
}),
r => r,
Expand Down Expand Up @@ -208,22 +208,22 @@ impl ExprFolder for ExprSimplifier {
let result = if simplified_then.is_bool() || simplified_else.is_bool() {
ast::Expr::BinOp(ast::BinOp {
op_kind: ast::BinaryOpKind::And,
left: box ast::Expr::BinOp(ast::BinOp {
left: Box::new(ast::Expr::BinOp(ast::BinOp {
op_kind: ast::BinaryOpKind::Implies,
left: simplified_guard.clone(),
right: simplified_then,
position,
}),
right: box ast::Expr::BinOp(ast::BinOp {
})),
right: Box::new(ast::Expr::BinOp(ast::BinOp {
op_kind: ast::BinaryOpKind::Implies,
left: box ast::Expr::UnaryOp(ast::UnaryOp {
left: Box::new(ast::Expr::UnaryOp(ast::UnaryOp {
op_kind: ast::UnaryOpKind::Not,
argument: simplified_guard,
position,
}),
})),
right: simplified_else,
position,
}),
})),
position,
})
} else {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -111,8 +111,8 @@ impl vir::ExprFolder for Optimizer {
for (expr, variable) in replacer.map.into_iter().sorted_unstable() {
forall = vir::Expr::LetExpr(vir::LetExpr {
variable,
def: box expr,
body: box forall,
def: Box::new(expr),
body: Box::new(forall),
position,
});
}
Expand Down Expand Up @@ -335,7 +335,7 @@ impl vir::ExprFolder for UnfoldingExtractor {
forall = vir::Expr::Unfolding(vir::Unfolding {
predicate: typ,
arguments: args,
base: box forall,
base: Box::new(forall),
permission: perm_amount,
variant,
position,
Expand Down
12 changes: 11 additions & 1 deletion prusti-contracts/prusti-specs/src/lib.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
#![deny(unused_must_use)]
#![feature(drain_filter)]
#![feature(box_patterns)]
#![feature(box_syntax)]
#![feature(proc_macro_span)]
#![feature(if_let_guard)]
#![feature(assert_matches)]
Expand Down Expand Up @@ -645,7 +644,11 @@ pub fn trusted(attr: TokenStream, tokens: TokenStream) -> TokenStream {

let item: syn::DeriveInput = handle_result!(syn::parse2(tokens));
let item_span = item.span();

// clippy false positive (https://github.com/rust-lang/rust-clippy/issues/10577)
#[allow(clippy::redundant_clone)]
let item_ident = item.ident.clone();

let item_name = syn::Ident::new(
&format!("prusti_trusted_item_{item_ident}_{spec_id}"),
item_span,
Expand Down Expand Up @@ -714,7 +717,11 @@ pub fn invariant(attr: TokenStream, tokens: TokenStream) -> TokenStream {

let item: syn::DeriveInput = handle_result!(syn::parse2(tokens));
let item_span = item.span();

// clippy false positive (https://github.com/rust-lang/rust-clippy/issues/10577)
#[allow(clippy::redundant_clone)]
let item_ident = item.ident.clone();

let item_name = syn::Ident::new(
&format!("prusti_invariant_item_{item_ident}_{spec_id}"),
item_span,
Expand All @@ -734,7 +741,10 @@ pub fn invariant(attr: TokenStream, tokens: TokenStream) -> TokenStream {
}
};

// clippy false positive (https://github.com/rust-lang/rust-clippy/issues/10577)
#[allow(clippy::redundant_clone)]
let generics = item.generics.clone();

let generics_idents = generics
.params
.iter()
Expand Down
4 changes: 4 additions & 0 deletions prusti-contracts/prusti-specs/src/print_counterexample.rs
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,11 @@ fn rewrite_internal_struct(
if !args2.empty_or_trailing() {
args2.push_punct(<syn::Token![,]>::default());
}

// clippy false positive (https://github.com/rust-lang/rust-clippy/issues/10577)
#[allow(clippy::redundant_clone)]
let typ = item_struct.ident.clone();

let spec_item = match item_struct.fields {
Fields::Named(_) => {
let spec_item: syn::ItemFn = parse_quote_spanned! {item_span=>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -174,7 +174,7 @@ impl PrustiTokenStream {
(TokenTree::Group(group), _, _, _) => PrustiToken::Group(
group.span(),
group.delimiter(),
box Self::new(group.stream()),
Box::new(Self::new(group.stream())),
),
(token, _, _, _) => PrustiToken::Token(token.clone()),
});
Expand Down
3 changes: 1 addition & 2 deletions prusti-interface/src/environment/mir_body/graphviz.rs
Original file line number Diff line number Diff line change
Expand Up @@ -185,8 +185,7 @@ fn visit_terminator(graph: &mut Graph, bb: mir::BasicBlock, terminator: &mir::Te
TerminatorKind::Unreachable => {
graph.add_exit_edge(bb.to_text(), "unreachable".to_text());
}
TerminatorKind::DropAndReplace { target, unwind, .. }
| TerminatorKind::Drop { target, unwind, .. } => {
TerminatorKind::Drop { target, unwind, .. } => {
graph.add_regular_edge(bb.to_text(), target.to_text());
if let Some(target) = unwind {
graph.add_unwind_edge(bb.to_text(), target.to_text());
Expand Down
4 changes: 2 additions & 2 deletions prusti-interface/src/environment/mir_utils/all_places.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
use prusti_rustc_interface::{
index::vec::Idx,
abi::FieldIdx,
middle::{mir, ty},
};

Expand All @@ -16,7 +16,7 @@ impl<'tcx> AllPlaces<'tcx> for mir::Local {
let ty = mir.local_decls[self].ty;
if let ty::TyKind::Tuple(types) = ty.kind() {
for (i, ty) in types.iter().enumerate() {
let field = mir::Field::new(i);
let field = FieldIdx::from_usize(i);
let place = tcx.mk_place_field(self.into(), field, ty);
places.push(place);
}
Expand Down
3 changes: 1 addition & 2 deletions prusti-interface/src/environment/mir_utils/real_edges.rs
Original file line number Diff line number Diff line change
Expand Up @@ -58,8 +58,7 @@ fn real_targets(terminator: &mir::Terminator) -> Vec<mir::BasicBlock> {
| TerminatorKind::GeneratorDrop
| TerminatorKind::Unreachable => vec![],

TerminatorKind::DropAndReplace { ref target, .. }
| TerminatorKind::Drop { ref target, .. } => vec![*target],
TerminatorKind::Drop { ref target, .. } => vec![*target],

TerminatorKind::Call { target, .. } => match target {
Some(target) => vec![target],
Expand Down
Loading

0 comments on commit cd17b7f

Please sign in to comment.