Skip to content

Commit

Permalink
Update dependencies (rustc nightly-2023-07-15, viper v-2023-07-05-0730)
Browse files Browse the repository at this point in the history
  • Loading branch information
fpoli authored and vakaras committed Jul 21, 2023
1 parent 5486c19 commit d628217
Show file tree
Hide file tree
Showing 58 changed files with 471 additions and 536 deletions.
199 changes: 102 additions & 97 deletions Cargo.lock

Large diffs are not rendered by default.

9 changes: 7 additions & 2 deletions analysis/src/bin/analysis-driver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,14 +16,15 @@ use prusti_rustc_interface::{
borrowck::consumers::{self, BodyWithBorrowckFacts},
data_structures::fx::FxHashMap,
driver::Compilation,
errors,
hir::def_id::{DefId, LocalDefId},
interface::{interface, Config, Queries},
middle::{
query::{queries::mir_borrowck::ProvidedValue, ExternProviders, Providers},
ty,
},
polonius_engine::{Algorithm, Output},
session::{Attribute, Session},
session::{self, Attribute, EarlyErrorHandler, Session},
};
use std::{cell::RefCell, rc::Rc};

Expand Down Expand Up @@ -146,6 +147,7 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls {

fn after_analysis<'tcx>(
&mut self,
_error_handler: &EarlyErrorHandler,
compiler: &interface::Compiler,
queries: &'tcx Queries<'tcx>,
) -> Compilation {
Expand Down Expand Up @@ -288,7 +290,10 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls {
/// --analysis=ReachingDefsState or --analysis=DefinitelyInitializedAnalysis
fn main() {
env_logger::init();
prusti_rustc_interface::driver::init_rustc_env_logger();
let error_handler = EarlyErrorHandler::new(session::config::ErrorOutputType::HumanReadable(
errors::emitter::HumanReadableErrorType::Default(errors::emitter::ColorConfig::Auto),
));
prusti_rustc_interface::driver::init_rustc_env_logger(&error_handler);
let mut compiler_args = Vec::new();
let mut callback_args = Vec::new();
for arg in std::env::args() {
Expand Down
10 changes: 7 additions & 3 deletions analysis/src/bin/gen-accessibility-driver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,15 +9,15 @@ use prusti_rustc_interface::{
borrowck::consumers::{self, BodyWithBorrowckFacts},
data_structures::fx::FxHashMap,
driver::Compilation,
hir,
errors, hir,
hir::def_id::LocalDefId,
interface::{interface, Config, Queries},
middle::{
query::{queries::mir_borrowck::ProvidedValue, ExternProviders, Providers},
ty,
},
polonius_engine::{Algorithm, Output},
session::Session,
session::{self, EarlyErrorHandler, Session},
span::FileName,
};
use std::{cell::RefCell, path::PathBuf, rc::Rc};
Expand Down Expand Up @@ -99,6 +99,7 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls {

fn after_analysis<'tcx>(
&mut self,
_error_handler: &EarlyErrorHandler,
compiler: &interface::Compiler,
queries: &'tcx Queries<'tcx>,
) -> Compilation {
Expand Down Expand Up @@ -212,7 +213,10 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls {
/// Run an analysis by calling like it rustc
fn main() {
env_logger::init();
prusti_rustc_interface::driver::init_rustc_env_logger();
let error_handler = EarlyErrorHandler::new(session::config::ErrorOutputType::HumanReadable(
errors::emitter::HumanReadableErrorType::Default(errors::emitter::ColorConfig::Auto),
));
prusti_rustc_interface::driver::init_rustc_env_logger(&error_handler);
let mut compiler_args = Vec::new();
let mut callback_args = Vec::new();
for arg in std::env::args() {
Expand Down
8 changes: 7 additions & 1 deletion prusti-common/src/vir/optimizations/methods/purifier.rs
Original file line number Diff line number Diff line change
Expand Up @@ -274,7 +274,13 @@ impl VarPurifier {
}
}
fn get_replacement(&self, expr: &ast::Expr) -> ast::Expr {
let ast::Expr::Local(ast::Local {variable: var, position: pos}) = expr else { unreachable!() };
let ast::Expr::Local(ast::Local {
variable: var,
position: pos,
}) = expr
else {
unreachable!()
};
let replacement = self
.replacements
.get(var)
Expand Down
12 changes: 9 additions & 3 deletions prusti-common/src/vir/to_viper.rs
Original file line number Diff line number Diff line change
Expand Up @@ -316,7 +316,9 @@ impl<'v> ToViper<'v, viper::Stmt<'v>> for Stmt {
)
}
Stmt::ApplyMagicWand(ref wand, ref pos) => {
let Expr::MagicWand(_, _, Some(borrow), _) = wand else { unreachable!() };
let Expr::MagicWand(_, _, Some(borrow), _) = wand else {
unreachable!()
};
let borrow: usize = borrow_id(*borrow);
let borrow: Expr = borrow.into();
let inhale = ast.inhale(
Expand Down Expand Up @@ -618,7 +620,9 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for Expr {
ContainerOpKind::SeqLen => ast.seq_length(left.to_viper(context, ast)),
},
Expr::Seq(ty, elems, _pos) => {
let Type::Seq(box elem_ty) = ty else { unreachable!() };
let Type::Seq(box elem_ty) = ty else {
unreachable!()
};
let viper_elem_ty = elem_ty.to_viper(context, ast);
if elems.is_empty() {
ast.empty_seq(viper_elem_ty)
Expand All @@ -631,7 +635,9 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for Expr {
}
}
Expr::Map(ty, elems, _pos) => {
let Type::Map(box key_ty, box val_ty) = ty else { unreachable!() };
let Type::Map(box key_ty, box val_ty) = ty else {
unreachable!()
};
let viper_key_ty = key_ty.to_viper(context, ast);
let viper_val_ty = val_ty.to_viper(context, ast);
if elems.is_empty() {
Expand Down
18 changes: 13 additions & 5 deletions prusti-contracts/prusti-specs/src/lib.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
#![deny(unused_must_use)]
#![feature(drain_filter)]
#![feature(extract_if)]
#![feature(box_patterns)]
#![feature(proc_macro_span)]
#![feature(if_let_guard)]
Expand Down Expand Up @@ -78,7 +78,9 @@ fn extract_prusti_attributes(
// tokens identical to the ones passed by the native procedural
// macro call.
let mut iter = attr.tokens.into_iter();
let TokenTree::Group(group) = iter.next().unwrap() else { unreachable!() };
let TokenTree::Group(group) = iter.next().unwrap() else {
unreachable!()
};
assert!(iter.next().is_none(), "Unexpected shape of an attribute.");
group.stream()
}
Expand Down Expand Up @@ -597,10 +599,14 @@ pub fn refine_trait_spec(_attr: TokenStream, tokens: TokenStream) -> TokenStream
let parsed_predicate =
handle_result!(predicate::parse_predicate_in_impl(makro.mac.tokens.clone()));

let ParsedPredicate::Impl(predicate) = parsed_predicate else { unreachable!() };
let ParsedPredicate::Impl(predicate) = parsed_predicate else {
unreachable!()
};

// Patch spec function: Rewrite self with _self: <SpecStruct>
let syn::Item::Fn(spec_function) = predicate.spec_function else { unreachable!() };
let syn::Item::Fn(spec_function) = predicate.spec_function else {
unreachable!()
};
generated_spec_items.push(spec_function);

// Add patched predicate function to new items
Expand Down Expand Up @@ -883,7 +889,9 @@ fn extract_prusti_attributes_for_types(
// tokens identical to the ones passed by the native procedural
// macro call.
let mut iter = attr.tokens.into_iter();
let TokenTree::Group(group) = iter.next().unwrap() else { unreachable!() };
let TokenTree::Group(group) = iter.next().unwrap() else {
unreachable!()
};
group.stream()
}
};
Expand Down
8 changes: 4 additions & 4 deletions prusti-contracts/prusti-specs/src/parse_closure_macro.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,16 +16,16 @@ impl Parse for ClosureWithSpec {

// collect and remove any specification attributes
// leave other attributes intact
attrs.drain_filter(|attr| {
attrs.retain(|attr| {
if let Some(id) = attr.path.get_ident() {
match id.to_string().as_ref() {
"requires" => pres.push(syn::parse2(attr.tokens.clone())),
"ensures" => posts.push(syn::parse2(attr.tokens.clone())),
_ => return false,
_ => return true,
}
true
} else {
false
} else {
true
}
});
cl.attrs = attrs;
Expand Down
25 changes: 15 additions & 10 deletions prusti-interface/src/environment/body.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,12 @@ use prusti_rustc_interface::{
macros::{TyDecodable, TyEncodable},
middle::{
mir,
ty::{self, subst::SubstsRef, TyCtxt},
ty::{self, TyCtxt},
},
span::def_id::{DefId, LocalDefId},
};
use rustc_hash::FxHashMap;
use rustc_middle::ty::GenericArgsRef;
use std::{cell::RefCell, collections::hash_map::Entry, rc::Rc};

use crate::environment::{borrowck::facts::BorrowckFacts, mir_storage};
Expand Down Expand Up @@ -80,7 +81,7 @@ impl<'tcx> PreLoadedBodies<'tcx> {
/// - we are encoding an impure function, where the method is encoded only once
/// and calls are performed indirectly via contract exhale/inhale; or
/// - when the caller is unknown, e.g. to check a pure function definition.
type MonomorphKey<'tcx> = (DefId, SubstsRef<'tcx>, Option<DefId>);
type MonomorphKey<'tcx> = (DefId, GenericArgsRef<'tcx>, Option<DefId>);

/// Store for all the `mir::Body` which we've taken out of the compiler
/// or imported from external crates, all of which are indexed by DefId
Expand Down Expand Up @@ -151,7 +152,7 @@ impl<'tcx> EnvBody<'tcx> {
fn get_monomorphised(
&self,
def_id: DefId,
substs: SubstsRef<'tcx>,
substs: GenericArgsRef<'tcx>,
caller_def_id: Option<DefId>,
) -> Option<MirBody<'tcx>> {
self.monomorphised_bodies
Expand All @@ -162,7 +163,7 @@ impl<'tcx> EnvBody<'tcx> {
fn set_monomorphised(
&self,
def_id: DefId,
substs: SubstsRef<'tcx>,
substs: GenericArgsRef<'tcx>,
caller_def_id: Option<DefId>,
body: MirBody<'tcx>,
) -> MirBody<'tcx> {
Expand All @@ -179,7 +180,7 @@ impl<'tcx> EnvBody<'tcx> {
ty::EarlyBinder::bind(body.0),
)
} else {
ty::EarlyBinder::bind(body.0).subst(self.tcx, substs)
ty::EarlyBinder::bind(body.0).instantiate(self.tcx, substs)
};
v.insert(MirBody(monomorphised)).clone()
} else {
Expand All @@ -201,7 +202,11 @@ impl<'tcx> EnvBody<'tcx> {
/// with the given type substitutions.
///
/// FIXME: This function is called only in pure contexts???
pub fn get_impure_fn_body(&self, def_id: LocalDefId, substs: SubstsRef<'tcx>) -> MirBody<'tcx> {
pub fn get_impure_fn_body(
&self,
def_id: LocalDefId,
substs: GenericArgsRef<'tcx>,
) -> MirBody<'tcx> {
if let Some(body) = self.get_monomorphised(def_id.to_def_id(), substs, None) {
return body;
}
Expand Down Expand Up @@ -231,7 +236,7 @@ impl<'tcx> EnvBody<'tcx> {
pub fn get_closure_body(
&self,
def_id: DefId,
substs: SubstsRef<'tcx>,
substs: GenericArgsRef<'tcx>,
caller_def_id: DefId,
) -> MirBody<'tcx> {
if let Some(body) = self.get_monomorphised(def_id, substs, Some(caller_def_id)) {
Expand All @@ -246,7 +251,7 @@ impl<'tcx> EnvBody<'tcx> {
pub fn get_pure_fn_body(
&self,
def_id: DefId,
substs: SubstsRef<'tcx>,
substs: GenericArgsRef<'tcx>,
caller_def_id: DefId,
) -> MirBody<'tcx> {
if let Some(body) = self.get_monomorphised(def_id, substs, Some(caller_def_id)) {
Expand All @@ -261,7 +266,7 @@ impl<'tcx> EnvBody<'tcx> {
pub fn get_expression_body(
&self,
def_id: DefId,
substs: SubstsRef<'tcx>,
substs: GenericArgsRef<'tcx>,
caller_def_id: DefId,
) -> MirBody<'tcx> {
if let Some(body) = self.get_monomorphised(def_id, substs, Some(caller_def_id)) {
Expand All @@ -279,7 +284,7 @@ impl<'tcx> EnvBody<'tcx> {
pub fn get_spec_body(
&self,
def_id: DefId,
substs: SubstsRef<'tcx>,
substs: GenericArgsRef<'tcx>,
caller_def_id: DefId,
) -> MirBody<'tcx> {
if let Some(body) = self.get_monomorphised(def_id, substs, Some(caller_def_id)) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -73,10 +73,8 @@ impl<'tcx> Visitor<'tcx> for CollectPrustiSpecVisitor<'tcx> {
) {
let def_id = self.env_query.as_local_def_id(item.hir_id()).to_def_id();
let adt_def = self.env_query.tcx().adt_def(def_id);
let ty = self
.env_query
.tcx()
.mk_adt(adt_def, self.env_query.identity_substs(def_id));
let tcx = self.env_query.tcx();
let ty = ty::Ty::new_adt(tcx, adt_def, self.env_query.identity_substs(def_id));
self.types.push(ty);
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ impl<'tcx> SplitAggregateAssignment<'tcx> for mir::Statement<'tcx> {
mir::Rvalue::Use(_) | mir::Rvalue::Ref(_, _, _) => vec![(lhs, rhs)],
// slice creation is ok
mir::Rvalue::Cast(
mir::CastKind::Pointer(ty::adjustment::PointerCast::Unsize),
mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize),
_,
cast_ty,
) if cast_ty.is_slice_ref() => vec![(lhs, rhs)],
Expand Down
4 changes: 2 additions & 2 deletions prusti-interface/src/environment/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
//! This module defines the interface provided to a verifier.

use prusti_rustc_interface::middle::ty::{self, TyCtxt};
use rustc_middle::ty::GenericArgsRef;

pub mod body;
pub mod borrowck;
Expand Down Expand Up @@ -45,7 +46,6 @@ use self::{
collect_prusti_spec_visitor::CollectPrustiSpecVisitor,
};
use crate::data::ProcedureDefId;
use rustc_middle::ty::SubstsRef;

/// Facade to the Rust compiler.
pub struct Environment<'tcx> {
Expand Down Expand Up @@ -139,7 +139,7 @@ impl<'tcx> Environment<'tcx> {
&self,
caller_def_id: ProcedureDefId,
called_def_id: ProcedureDefId,
call_substs: SubstsRef<'tcx>,
call_substs: GenericArgsRef<'tcx>,
) -> bool {
if called_def_id == caller_def_id {
true
Expand Down
2 changes: 1 addition & 1 deletion prusti-interface/src/environment/polonius_info.rs
Original file line number Diff line number Diff line change
Expand Up @@ -587,7 +587,7 @@ fn get_borrowed_places<'a, 'tcx: 'a>(

// slice creation involves an unsize pointer cast like &[i32; 3] -> &[i32]
&mir::Rvalue::Cast(
mir::CastKind::Pointer(ty::adjustment::PointerCast::Unsize),
mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize),
ref operand,
ref cast_ty,
) if cast_ty.is_slice_ref() => {
Expand Down
2 changes: 1 addition & 1 deletion prusti-interface/src/environment/procedure.rs
Original file line number Diff line number Diff line change
Expand Up @@ -247,7 +247,7 @@ pub fn get_loop_invariant<'tcx>(
bb_data: &BasicBlockData<'tcx>,
) -> Option<(
ProcedureDefId,
prusti_rustc_interface::middle::ty::subst::SubstsRef<'tcx>,
prusti_rustc_interface::middle::ty::GenericArgsRef<'tcx>,
)> {
for stmt in &bb_data.statements {
if let StatementKind::Assign(box (
Expand Down
Loading

0 comments on commit d628217

Please sign in to comment.