Skip to content

Commit

Permalink
Completion of issue 711 and general code improvements (#1314)
Browse files Browse the repository at this point in the history
* Changing sets and maps to use the same hasher

* Fixed typo

* Change to FxHash

* Refactor code and change to sort_unstable

Changed code from for loops to map + collect to reduce number of vector reallocations.
Changed Vec::sort() to Vec::sort_unstable(), because it is faster and stability is not
needed. Most of the sorted vectors are created from a hashmap, so there are no duplicate
entries whose order could be changed by the sorting.

* Preallocate vector capacity

* Preallocate vector capacity

* Remove unnecessary work

The old code created the viper encodings for all the methods, even
if they get deleted again afterwards if config::verify_only_preamble()
is true. Now it will only do the work if the option is not set to true

* Fixed formating

* Inline variables in format string

* Switch to unstable sort

* Switch to FxHash

* Switch to rustc-hash

* Fix formatting

* Remove unused file

* Reduce error message duplication

* Switch to rustc-hash

* Improve error reporting

* Add clippy lint for disallowed types

* Fix incorrect format string

Co-authored-by: Aurel <[email protected]>

* Disable rustup self update

---------

Co-authored-by: Aurel <[email protected]>
  • Loading branch information
Patrick-6 and Aurel300 authored Feb 6, 2023
1 parent 3dd957c commit 7c3bfa0
Show file tree
Hide file tree
Showing 93 changed files with 344 additions and 550 deletions.
20 changes: 8 additions & 12 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 2 additions & 0 deletions analysis/clippy.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
# use rustc-hash instead: https://crates.io/crates/rustc-hash
disallowed-types = ["std::collections::HashMap", "std::collections::HashSet", "fxhash::FxHashMap", "fxhash::FxHashSet"]
7 changes: 4 additions & 3 deletions analysis/src/bin/analysis-driver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ use analysis::{
use prusti_rustc_interface::{
ast::ast,
borrowck::BodyWithBorrowckFacts,
data_structures::fx::FxHashMap,
driver::Compilation,
hir::def_id::{DefId, LocalDefId},
interface::{interface, Config, Queries},
Expand All @@ -24,7 +25,7 @@ use prusti_rustc_interface::{
polonius_engine::{Algorithm, Output},
session::{Attribute, Session},
};
use std::{cell::RefCell, collections::HashMap, rc::Rc};
use std::{cell::RefCell, rc::Rc};

struct OurCompilerCalls {
args: Vec<String>,
Expand Down Expand Up @@ -83,8 +84,8 @@ mod mir_storage {
// because we cast it back to `'tcx` before using.
thread_local! {
static MIR_BODIES:
RefCell<HashMap<LocalDefId, BodyWithBorrowckFacts<'static>>> =
RefCell::new(HashMap::new());
RefCell<FxHashMap<LocalDefId, BodyWithBorrowckFacts<'static>>> =
RefCell::new(FxHashMap::default());
}

pub unsafe fn store_mir_body<'tcx>(
Expand Down
7 changes: 4 additions & 3 deletions analysis/src/bin/gen-accessibility-driver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
use analysis::domains::DefinitelyAccessibleAnalysis;
use prusti_rustc_interface::{
borrowck::BodyWithBorrowckFacts,
data_structures::fx::FxHashMap,
driver::Compilation,
hir,
hir::def_id::LocalDefId,
Expand All @@ -19,7 +20,7 @@ use prusti_rustc_interface::{
session::Session,
span::FileName,
};
use std::{cell::RefCell, collections::HashMap, path::PathBuf, rc::Rc};
use std::{cell::RefCell, path::PathBuf, rc::Rc};

struct OurCompilerCalls {
args: Vec<String>,
Expand All @@ -36,8 +37,8 @@ mod mir_storage {
// because we cast it back to `'tcx` before using.
thread_local! {
static MIR_BODIES:
RefCell<HashMap<LocalDefId, BodyWithBorrowckFacts<'static>>> =
RefCell::new(HashMap::new());
RefCell<FxHashMap<LocalDefId, BodyWithBorrowckFacts<'static>>> =
RefCell::new(FxHashMap::default());
}

pub unsafe fn store_mir_body<'tcx>(
Expand Down
43 changes: 20 additions & 23 deletions analysis/src/domains/definitely_accessible/state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -51,20 +51,23 @@ impl<'tcx> DefinitelyAccessibleState<'tcx> {
impl<'tcx> Serialize for DefinitelyAccessibleState<'tcx> {
fn serialize<Se: Serializer>(&self, serializer: Se) -> Result<Se::Ok, Se::Error> {
let mut seq = serializer.serialize_map(Some(2))?;

let mut definitely_accessible_set: Vec<_> = self.definitely_accessible.iter().collect();
definitely_accessible_set.sort();
let mut definitely_accessible_strings = vec![];
for &place in definitely_accessible_set {
definitely_accessible_strings.push(format!("{place:?}"));
}
definitely_accessible_set.sort_unstable();
let definitely_accessible_strings: Vec<_> = definitely_accessible_set
.into_iter()
.map(|place| format!("{place:?}"))
.collect();
seq.serialize_entry("accessible", &definitely_accessible_strings)?;

let mut definitely_owned_set: Vec<_> = self.definitely_owned.iter().collect();
definitely_owned_set.sort();
let mut definitely_owned_strings = vec![];
for &place in definitely_owned_set {
definitely_owned_strings.push(format!("{place:?}"));
}
definitely_owned_set.sort_unstable();
let definitely_owned_strings: Vec<_> = definitely_owned_set
.into_iter()
.map(|place| format!("{place:?}"))
.collect();
seq.serialize_entry("owned", &definitely_owned_strings)?;

seq.end()
}
}
Expand Down Expand Up @@ -93,26 +96,23 @@ impl<'mir, 'tcx: 'mir> PointwiseState<'mir, 'tcx, DefinitelyAccessibleState<'tcx
};
let span = self.mir.source_info(location).span;
if span.parent_callsite().is_some() {
info!("Statement {:?} is generated by a macro", location);
info!("Statement {location:?} is generated by a macro");
continue;
}
if source_map.is_multiline(span) {
info!("Statement {:?} is on multiple lines", location);
info!("Statement {location:?} is on multiple lines");
continue;
}
if let Ok(file_lines) = source_map.span_to_lines(span) {
if file_lines.lines.len() == 1 {
let line = file_lines.lines.first().unwrap();
let line_num = line.line_index + 1;
info!(
"Statement {:?} is on a single line at {}",
location, line_num
);
info!("Statement {location:?} is on a single line at {line_num}");
// Check that it parses as a statement
let line_seems_stmt =
syn::parse_str::<syn::Stmt>(&result[line.line_index]).is_ok();
if !line_seems_stmt {
info!("Statement {:?} doesn't parse as a statement", location);
info!("Statement {location:?} doesn't parse as a statement");
continue;
}
// Keep the first span
Expand All @@ -128,17 +128,14 @@ impl<'mir, 'tcx: 'mir> PointwiseState<'mir, 'tcx, DefinitelyAccessibleState<'tcx
}
}
} else {
info!("Statement {:?} has no lines", location);
info!("Statement {location:?} has no lines");
}
}
}
let mut line_locations: Vec<_> = first_location_on_line.iter().collect();
line_locations.sort_by(|left, right| right.0.cmp(left.0)); // From last to first
line_locations.sort_unstable_by(|left, right| right.0.cmp(left.0)); // From last to first
for (&line_num, &location) in line_locations {
info!(
"The first single-line statement on line {} is {:?}",
line_num, location
);
info!("The first single-line statement on line {line_num} is {location:?}",);
let before = "\t\t\t";
let after = " // Check analysis";
let state = self.lookup_before(location).unwrap();
Expand Down
15 changes: 8 additions & 7 deletions analysis/src/domains/definitely_allocated/state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,9 @@ impl<'mir, 'tcx: 'mir> Eq for DefinitelyAllocatedState<'mir, 'tcx> {}
impl<'mir, 'tcx: 'mir> Serialize for DefinitelyAllocatedState<'mir, 'tcx> {
fn serialize<Se: Serializer>(&self, serializer: Se) -> Result<Se::Ok, Se::Error> {
let mut seq = serializer.serialize_seq(Some(self.def_allocated_locals.len()))?;
let oredered_set: BTreeSet<_> = self.def_allocated_locals.iter().collect();
for local in oredered_set {

let ordered_set: BTreeSet<_> = self.def_allocated_locals.iter().collect();
for local in ordered_set {
seq.serialize_element(&format!("{local:?}"))?;
}
seq.end()
Expand Down Expand Up @@ -92,11 +93,11 @@ impl<'mir, 'tcx: 'mir> DefinitelyAllocatedState<'mir, 'tcx> {
&self,
location: mir::Location,
) -> Result<Vec<(mir::BasicBlock, Self)>, AnalysisError> {
let mut res_vec = Vec::new();
let terminator = self.mir[location.block].terminator();
for bb in terminator.successors() {
res_vec.push((bb, self.clone()));
}
let res_vec = self.mir[location.block]
.terminator()
.successors()
.map(|bb| (bb, self.clone()))
.collect();
Ok(res_vec)
}
}
Expand Down
23 changes: 13 additions & 10 deletions analysis/src/domains/framing/state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -65,19 +65,22 @@ impl<'tcx> FramingState<'tcx> {
impl<'tcx> Serialize for FramingState<'tcx> {
fn serialize<Se: Serializer>(&self, serializer: Se) -> Result<Se::Ok, Se::Error> {
let mut seq = serializer.serialize_map(Some(2))?;

let mut definitely_accessible_set: Vec<_> = self.framed_accessible.iter().collect();
definitely_accessible_set.sort();
let mut definitely_accessible_strings = vec![];
for &place in definitely_accessible_set {
definitely_accessible_strings.push(format!("{place:?}"));
}
definitely_accessible_set.sort_unstable();
let definitely_accessible_strings: Vec<_> = definitely_accessible_set
.into_iter()
.map(|place| format!("{place:?}"))
.collect();
seq.serialize_entry("frame_accessible", &definitely_accessible_strings)?;

let mut definitely_owned_set: Vec<_> = self.framed_owned.iter().collect();
definitely_owned_set.sort();
let mut definitely_owned_strings = vec![];
for &place in definitely_owned_set {
definitely_owned_strings.push(format!("{place:?}"));
}
definitely_owned_set.sort_unstable();
let definitely_owned_strings: Vec<_> = definitely_owned_set
.into_iter()
.map(|place| format!("{place:?}"))
.collect();

seq.serialize_entry("frame_owned", &definitely_owned_strings)?;
seq.end()
}
Expand Down
23 changes: 13 additions & 10 deletions analysis/src/domains/maybe_borrowed/state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -27,20 +27,23 @@ impl<'tcx> MaybeBorrowedState<'tcx> {
impl<'tcx> Serialize for MaybeBorrowedState<'tcx> {
fn serialize<Se: Serializer>(&self, serializer: Se) -> Result<Se::Ok, Se::Error> {
let mut seq = serializer.serialize_map(Some(2))?;

let mut maybe_shared_borrowed_set: Vec<_> = self.maybe_shared_borrowed.iter().collect();
maybe_shared_borrowed_set.sort();
let mut maybe_shared_borrowed_strings = vec![];
for &place in maybe_shared_borrowed_set {
maybe_shared_borrowed_strings.push(format!("{place:?}"));
}
maybe_shared_borrowed_set.sort_unstable();
let maybe_shared_borrowed_strings: Vec<_> = maybe_shared_borrowed_set
.into_iter()
.map(|place| format!("{place:?}"))
.collect();
seq.serialize_entry("frozen", &maybe_shared_borrowed_strings)?;

let mut maybe_mut_borrowed_set: Vec<_> = self.maybe_mut_borrowed.iter().collect();
maybe_mut_borrowed_set.sort();
let mut maybe_mut_borrowed_strings = vec![];
for &place in maybe_mut_borrowed_set {
maybe_mut_borrowed_strings.push(format!("{place:?}"));
}
maybe_mut_borrowed_set.sort_unstable();
let maybe_mut_borrowed_strings: Vec<_> = maybe_mut_borrowed_set
.into_iter()
.map(|place| format!("{place:?}"))
.collect();
seq.serialize_entry("blocked", &maybe_mut_borrowed_strings)?;

seq.end()
}
}
2 changes: 1 addition & 1 deletion analysis/src/domains/reaching_definitions/state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ impl<'mir, 'tcx: 'mir> Serialize for ReachingDefsState<'mir, 'tcx> {
let ordered_ass_map: BTreeMap<_, _> = self.reaching_defs.iter().collect();
for (local, location_set) in ordered_ass_map {
let ordered_loc_set: BTreeSet<_> = location_set.iter().collect();
let mut location_vec = Vec::new();
let mut location_vec = Vec::with_capacity(ordered_loc_set.len());
for location in ordered_loc_set {
match location {
DefLocation::Assignment(l) => {
Expand Down
1 change: 1 addition & 0 deletions analysis/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@

#![feature(rustc_private)]
#![feature(box_patterns)]
#![warn(clippy::disallowed_types)]

pub mod abstract_interpretation;
mod analysis_error;
Expand Down
2 changes: 1 addition & 1 deletion analysis/src/pointwise_state.rs
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ impl<'mir, 'tcx: 'mir, S: Serialize> Serialize for PointwiseState<'mir, 'tcx, S>

for bb in self.mir.basic_blocks.indices() {
let mir::BasicBlockData { ref statements, .. } = self.mir[bb];
let mut stmt_vec: Vec<_> = Vec::new();
let mut stmt_vec: Vec<_> = Vec::with_capacity(statements.len());
for (statement_index, stmt) in statements.iter().enumerate() {
let location = mir::Location {
block: bb,
Expand Down
2 changes: 1 addition & 1 deletion analysis/tests/test_accessibility.rs
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,7 @@ fn collect_standalone_test_programs() -> Vec<PathBuf> {
glob_path
);
assert!(!new_programs.is_empty());
new_programs.sort();
new_programs.sort_unstable();
programs.append(&mut new_programs);
}
assert!(programs.len() >= glob_paths.len());
Expand Down
1 change: 1 addition & 0 deletions jni-gen/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -12,3 +12,4 @@ log = { version = "0.4", features = ["release_max_level_info"] }
error-chain = "0.12.0"
jni = { version = "0.20", features = ["invocation"] }
tempfile = "3"
rustc-hash = "1.1.0"
2 changes: 2 additions & 0 deletions jni-gen/clippy.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
# use rustc-hash instead: https://crates.io/crates/rustc-hash
disallowed-types = ["std::collections::HashMap", "std::collections::HashSet", "fxhash::FxHashMap", "fxhash::FxHashSet"]
6 changes: 3 additions & 3 deletions jni-gen/src/generators/constructor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -67,9 +67,6 @@ pub fn generate_constructor(
},
};

let mut parameter_names: Vec<String> = vec![];
let mut parameter_signatures: Vec<String> = vec![];

let parameters = env
.call_method(
constructor,
Expand All @@ -80,6 +77,9 @@ pub fn generate_constructor(
.l()?;
let num_parameters = env.get_array_length(*parameters)?;

let mut parameter_names: Vec<String> = Vec::with_capacity(num_parameters as usize);
let mut parameter_signatures: Vec<String> = Vec::with_capacity(num_parameters as usize);

for parameter_index in 0..num_parameters {
let parameter = env.get_object_array_element(*parameters, parameter_index)?;
let parameter_name = env.get_string(
Expand Down
Loading

0 comments on commit 7c3bfa0

Please sign in to comment.