Skip to content

Commit

Permalink
Merge pull request #1430 from viperproject/auto-update-nightly-2023-0…
Browse files Browse the repository at this point in the history
…7-15

Update dependencies (rustc nightly-2023-07-15, viper v-2023-07-05-0730)
  • Loading branch information
Aurel300 authored Aug 11, 2023
2 parents b256b42 + f0996cc commit d54e24d
Show file tree
Hide file tree
Showing 78 changed files with 514 additions and 591 deletions.
201 changes: 103 additions & 98 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
2 changes: 1 addition & 1 deletion analysis/tests/test_analysis.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ fn run_tests(mode: &str, path: &str, custom_args: Vec<String>) {
let mut flags = Vec::new();
flags.push("--edition 2018".to_owned());
flags.push(format!("--sysroot {}", find_sysroot()));
flags.extend(custom_args.into_iter());
flags.extend(custom_args);
config.target_rustcflags = Some(flags.join(" "));
config.mode = mode.parse().expect("Invalid mode");
config.rustc_path = find_compiled_executable("analysis-driver");
Expand Down
2 changes: 1 addition & 1 deletion jni-gen/src/generators/module.rs
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ pub fn generate_module(class_names: Vec<&ClassName>) -> String {
})
.unwrap_or_else(|| "// No modules".to_string());

vec![
[
"//! Automatically generated code\n".to_string(),
"#![allow(non_snake_case)]\n".to_string(),
"pub mod builtins;\n".to_string(),
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 @@ -163,7 +163,7 @@ fn check_requirements_conflict(
conflict_set.insert(base1);
} else if base1 == base2 && !place1.has_prefix(place2) && !place2.has_prefix(place1) {
// Check if we have different variants.
for (part1, part2) in components1.into_iter().zip(components2.into_iter()) {
for (part1, part2) in components1.into_iter().zip(components2) {
match (part1, part2) {
(
ast::PlaceComponent::Variant(ast::Field { name: name1, .. }, _),
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
4 changes: 2 additions & 2 deletions prusti-contracts/prusti-contracts-proc-macros/Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[package]
name = "prusti-contracts-proc-macros"
version = "0.1.9"
version = "0.1.10"
authors = ["Prusti Devs <[email protected]>"]
edition = "2021"
license = "MPL-2.0"
Expand All @@ -15,7 +15,7 @@ categories = ["development-tools", "development-tools::testing"]
proc-macro = true

[dependencies]
prusti-specs = { path = "../prusti-specs", version = "0.1.9", optional = true }
prusti-specs = { path = "../prusti-specs", version = "0.1.10", optional = true }
proc-macro2 = { version = "1.0", optional = true }

[features]
Expand Down
4 changes: 2 additions & 2 deletions prusti-contracts/prusti-contracts/Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[package]
name = "prusti-contracts"
version = "0.1.9"
version = "0.1.10"
authors = ["Prusti Devs <[email protected]>"]
edition = "2021"
license = "MPL-2.0"
Expand All @@ -12,7 +12,7 @@ keywords = ["prusti", "contracts", "verification", "formal", "specifications"]
categories = ["development-tools", "development-tools::testing"]

[dependencies]
prusti-contracts-proc-macros = { path = "../prusti-contracts-proc-macros", version = "0.1.9" }
prusti-contracts-proc-macros = { path = "../prusti-contracts-proc-macros", version = "0.1.10" }

[dev-dependencies]
trybuild = "1.0"
Expand Down
2 changes: 1 addition & 1 deletion prusti-contracts/prusti-specs/Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[package]
name = "prusti-specs"
version = "0.1.9"
version = "0.1.10"
authors = ["Prusti Devs <[email protected]>"]
edition = "2021"
license = "MPL-2.0"
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
Original file line number Diff line number Diff line change
Expand Up @@ -221,8 +221,7 @@ impl PrustiTokenStream {
PrustiToken::BinOp(span, PrustiBinaryOp::Rust(op)) => Ok(op.to_tokens(span)),
_ => err(token.span(), "unexpected Prusti syntax"),
})
.collect::<Result<Vec<_>, _>>()?
.into_iter(),
.collect::<Result<Vec<_>, _>>()?,
))
}

Expand Down
4 changes: 2 additions & 2 deletions prusti-contracts/prusti-std/Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[package]
name = "prusti-std"
version = "0.1.9"
version = "0.1.10"
authors = ["Prusti Devs <[email protected]>"]
edition = "2021"
license = "MPL-2.0"
Expand All @@ -12,7 +12,7 @@ keywords = ["prusti", "contracts", "verification", "formal", "specifications"]
categories = ["development-tools", "development-tools::testing"]

[dependencies]
prusti-contracts = { path = "../prusti-contracts", version = "0.1.9" }
prusti-contracts = { path = "../prusti-contracts", version = "0.1.10" }

# Forward "prusti" flag
[features]
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
Loading

0 comments on commit d54e24d

Please sign in to comment.