From 8d5f5c83aec75cdf25ffb6a82b5371ddc31355ce Mon Sep 17 00:00:00 2001
From: Vincent Lafeychine <vincent.lafeychine@proton.me>
Date: Fri, 24 May 2024 18:38:34 +0200
Subject: [PATCH] clippy: Fix partial_pub_fields
---
rr_frontend/.cargo/config.toml | 1 -
rr_frontend/radium/src/code.rs | 2 +
rr_frontend/radium/src/specs.rs | 7 +-
.../src/environment/dump_borrowck_info.rs | 4 +-
.../translation/src/environment/loops.rs | 28 ++++--
.../src/environment/polonius_info.rs | 4 +-
.../translation/src/environment/procedure.rs | 88 +++++++++----------
rr_frontend/translation/src/function_body.rs | 7 +-
rr_frontend/translation/src/lib.rs | 10 +--
.../translation/src/type_translator.rs | 5 +-
10 files changed, 80 insertions(+), 76 deletions(-)
diff --git a/rr_frontend/.cargo/config.toml b/rr_frontend/.cargo/config.toml
index 3a8584f2..cdbd860b 100644
--- a/rr_frontend/.cargo/config.toml
+++ b/rr_frontend/.cargo/config.toml
@@ -34,7 +34,6 @@ rustflags = [
# clippy::restriction
"-Aclippy::non_ascii_literal",
"-Aclippy::panic_in_result_fn",
- "-Aclippy::partial_pub_fields",
"-Aclippy::pub_use",
"-Aclippy::pub_with_shorthand",
"-Aclippy::redundant_type_annotations",
diff --git a/rr_frontend/radium/src/code.rs b/rr_frontend/radium/src/code.rs
index 2830ce10..aec86351 100644
--- a/rr_frontend/radium/src/code.rs
+++ b/rr_frontend/radium/src/code.rs
@@ -757,6 +757,7 @@ struct InvariantMap(HashMap<usize, LoopSpec>);
/// A Caesium function bundles up the Caesium code itself as well as the generated specification
/// for it.
+#[allow(clippy::partial_pub_fields)]
pub struct Function<'def> {
pub code: FunctionCode,
pub spec: FunctionSpec<'def>,
@@ -1077,6 +1078,7 @@ pub struct StaticMeta<'def> {
/// A `CaesiumFunctionBuilder` allows to incrementally construct the functions's code and the spec
/// at the same time. It ensures that both definitions line up in the right way (for instance, by
/// ensuring that other functions are linked up in a consistent way).
+#[allow(clippy::partial_pub_fields)]
pub struct FunctionBuilder<'def> {
pub code: FunctionCodeBuilder,
pub spec: FunctionSpecBuilder<'def>,
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index 25283a76..df24cff9 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -2656,7 +2656,7 @@ pub struct FunctionSpec<'def> {
/// postcondition as a separating conjunction
pub post: IProp,
/// true iff any attributes have been provided
- has_spec: bool,
+ pub has_spec: bool,
}
impl<'def> FunctionSpec<'def> {
@@ -2686,11 +2686,6 @@ impl<'def> FunctionSpec<'def> {
out
}
- #[must_use]
- pub const fn has_spec(&self) -> bool {
- self.has_spec
- }
-
fn uncurry_typed_binders<'a, F>(v: F) -> (coq::Pattern, coq::Type)
where
F: IntoIterator<Item = &'a (coq::Name, coq::Type)>,
diff --git a/rr_frontend/translation/src/environment/dump_borrowck_info.rs b/rr_frontend/translation/src/environment/dump_borrowck_info.rs
index fae37397..315f3819 100644
--- a/rr_frontend/translation/src/environment/dump_borrowck_info.rs
+++ b/rr_frontend/translation/src/environment/dump_borrowck_info.rs
@@ -524,7 +524,7 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> {
fn visit_basic_block(&mut self, bb: mir::BasicBlock) -> Result<(), io::Error> {
write_graph!(self, "\"{:?}\" [ shape = \"record\"", bb);
- if self.loops.loop_heads.contains(&bb) {
+ if self.loops.is_loop_head(bb) {
write_graph!(self, "color=green");
}
write_graph!(self, "label =<<table>");
@@ -579,7 +579,7 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> {
self.visit_terminator(bb, terminator)?;
}
- if !self.loops.loop_heads.contains(&bb) {
+ if !self.loops.is_loop_head(bb) {
return Ok(());
}
diff --git a/rr_frontend/translation/src/environment/loops.rs b/rr_frontend/translation/src/environment/loops.rs
index f4588560..49313a16 100644
--- a/rr_frontend/translation/src/environment/loops.rs
+++ b/rr_frontend/translation/src/environment/loops.rs
@@ -6,7 +6,7 @@
use std::collections::{HashMap, HashSet};
-use log::{debug, trace};
+use log::{debug, info, trace};
use rustc_data_structures::graph::dominators::{dominators, Dominators};
use rustc_index::{Idx, IndexVec};
use rustc_middle::mir;
@@ -207,12 +207,12 @@ fn order_basic_blocks(
#[derive(Clone)]
pub struct ProcedureLoops {
/// A list of basic blocks that are loop heads.
- pub loop_heads: HashSet<BasicBlockIndex>,
+ loop_heads: HashSet<BasicBlockIndex>,
/// The depth of each loop head, starting from one for a simple single loop.
- pub loop_head_depths: HashMap<BasicBlockIndex, usize>,
+ loop_head_depths: HashMap<BasicBlockIndex, usize>,
/// A map from loop heads to the corresponding bodies.
- pub loop_bodies: HashMap<BasicBlockIndex, HashSet<BasicBlockIndex>>,
- pub ordered_loop_bodies: HashMap<BasicBlockIndex, Vec<BasicBlockIndex>>,
+ loop_bodies: HashMap<BasicBlockIndex, HashSet<BasicBlockIndex>>,
+ ordered_loop_bodies: HashMap<BasicBlockIndex, Vec<BasicBlockIndex>>,
/// A map from loop bodies to the ordered vector of enclosing loop heads (from outer to inner).
enclosing_loop_heads: HashMap<BasicBlockIndex, Vec<BasicBlockIndex>>,
/// A map from loop heads to the ordered blocks from which a CFG edge exits from the loop.
@@ -221,11 +221,11 @@ pub struct ProcedureLoops {
/// in any loop iteration).
nonconditional_loop_blocks: HashMap<BasicBlockIndex, HashSet<BasicBlockIndex>>,
/// Back edges.
- pub back_edges: HashSet<(BasicBlockIndex, BasicBlockIndex)>,
+ back_edges: HashSet<(BasicBlockIndex, BasicBlockIndex)>,
/// Dominators graph.
dominators: Dominators<BasicBlockIndex>,
/// The list of basic blocks ordered in the topological order (ignoring back edges).
- pub ordered_blocks: Vec<BasicBlockIndex>,
+ ordered_blocks: Vec<BasicBlockIndex>,
}
impl ProcedureLoops {
@@ -364,6 +364,20 @@ impl ProcedureLoops {
self.loop_heads.len()
}
+ pub fn dump_body_head(&self) {
+ info!("loop heads: {:?}", self.loop_heads);
+ for (head, bodies) in &self.loop_bodies {
+ info!("loop {:?} -> {:?}", head, bodies);
+ }
+ }
+
+ #[must_use]
+ pub const fn get_back_edges(
+ &self,
+ ) -> &HashSet<(rustc_middle::mir::BasicBlock, rustc_middle::mir::BasicBlock)> {
+ &self.back_edges
+ }
+
#[must_use]
pub fn max_loop_nesting(&self) -> usize {
self.loop_head_depths.values().max().copied().unwrap_or(0)
diff --git a/rr_frontend/translation/src/environment/polonius_info.rs b/rr_frontend/translation/src/environment/polonius_info.rs
index ab0b9605..88f8d67e 100644
--- a/rr_frontend/translation/src/environment/polonius_info.rs
+++ b/rr_frontend/translation/src/environment/polonius_info.rs
@@ -308,7 +308,7 @@ pub struct PoloniusInfo<'a, 'tcx: 'a> {
/// Position at which a specific loan was created.
pub(crate) loan_position: HashMap<facts::Loan, mir::Location>,
pub(crate) loan_at_position: HashMap<mir::Location, facts::Loan>,
- pub place_regions: PlaceRegions,
+ pub(crate) place_regions: PlaceRegions,
pub(crate) additional_facts: AdditionalFacts,
/// Loans that are created inside loops. Loan → loop head.
pub(crate) loops: loops::ProcedureLoops,
@@ -488,7 +488,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
let output = Output::compute(&all_facts, Algorithm::Naive, true);
let all_facts_without_back_edges =
- remove_back_edges(*all_facts.clone(), &interner, &loop_info.back_edges);
+ remove_back_edges(*all_facts.clone(), &interner, loop_info.get_back_edges());
let output_without_back_edges =
Output::compute(&all_facts_without_back_edges, Algorithm::Naive, true);
diff --git a/rr_frontend/translation/src/environment/procedure.rs b/rr_frontend/translation/src/environment/procedure.rs
index 69a8a04e..186ef756 100644
--- a/rr_frontend/translation/src/environment/procedure.rs
+++ b/rr_frontend/translation/src/environment/procedure.rs
@@ -116,14 +116,14 @@ impl<'tcx> Procedure<'tcx> {
self.ty_params
}
- /// Get an absolute `def_path`. Note: not preserved across compilations!
- #[must_use]
- pub fn get_def_path(&self) -> String {
- let def_path = self.tcx.def_path(self.proc_def_id);
- let mut crate_name = self.tcx.crate_name(def_path.krate).to_string();
- crate_name.push_str(&def_path.to_string_no_crate_verbose());
- crate_name
- }
+ // /// Get an absolute `def_path`. Note: not preserved across compilations!
+ // #[must_use]
+ // pub fn get_def_path(&self) -> String {
+ // let def_path = self.tcx.def_path(self.proc_def_id);
+ // let mut crate_name = self.tcx.crate_name(def_path.krate).to_string();
+ // crate_name.push_str(&def_path.to_string_no_crate_verbose());
+ // crate_name
+ // }
// /// Get a short name of the procedure
// pub fn get_short_name(&self) -> String {
@@ -135,49 +135,45 @@ impl<'tcx> Procedure<'tcx> {
// self.tcx.absolute_item_path_str(self.proc_def_id)
// }
- /// Get the span of the procedure
- #[must_use]
- pub fn get_span(&self) -> Span {
- self.mir.span
- }
+ // /// Get the span of the procedure
+ // #[must_use]
+ // pub fn get_span(&self) -> Span {
+ // self.mir.span
+ // }
- /// Get the first CFG block
- #[must_use]
- pub fn get_first_cfg_block(&self) -> BasicBlock {
- self.mir.basic_blocks.indices().next().unwrap()
- }
+ // /// Get the first CFG block
+ // #[must_use]
+ // pub fn get_first_cfg_block(&self) -> BasicBlock {
+ // self.mir.basic_blocks.indices().next().unwrap()
+ // }
- /// Iterate over all CFG basic blocks
- #[must_use]
- pub fn get_all_cfg_blocks(&self) -> Vec<BasicBlock> {
- self.loop_info.ordered_blocks.clone()
- }
+ // /// Iterate over all CFG basic blocks
+ // #[must_use]
+ // pub fn get_all_cfg_blocks(&self) -> Vec<BasicBlock> {
+ // self.loop_info.ordered_blocks.clone()
+ // }
- /// Iterate over all reachable CFG basic blocks
- #[must_use]
- pub fn get_reachable_cfg_blocks(&self) -> Vec<BasicBlock> {
- self.get_all_cfg_blocks()
- .into_iter()
- .filter(|bbi| self.is_reachable_block(*bbi))
- .collect()
- }
+ // /// Iterate over all reachable CFG basic blocks
+ // #[must_use]
+ // pub fn get_reachable_cfg_blocks(&self) -> Vec<BasicBlock> {
+ // self.get_all_cfg_blocks()
+ // .into_iter()
+ // .filter(|bbi| self.is_reachable_block(*bbi))
+ // .collect()
+ // }
- /*
- /// Iterate over all reachable CFG basic blocks that are not part of the specification type checking
- pub fn get_reachable_nonspec_cfg_blocks(&self) -> Vec<BasicBlock> {
- self.get_reachable_cfg_blocks()
- .into_iter()
- .filter(|bbi| !self.is_spec_block(*bbi))
- .collect()
- }
- */
+ // /// Iterate over all reachable CFG basic blocks that are not part of the specification type checking
+ // pub fn get_reachable_nonspec_cfg_blocks(&self) -> Vec<BasicBlock> {
+ // self.get_reachable_cfg_blocks()
+ // .into_iter()
+ // .filter(|bbi| !self.is_spec_block(*bbi))
+ // .collect()
+ // }
- /*
- /// Check whether the block is used for typechecking the specification
- pub fn is_spec_block(&self, bbi: BasicBlockIndex) -> bool {
- !self.nonspec_basic_blocks.contains(&bbi)
- }
- */
+ // /// Check whether the block is used for typechecking the specification
+ // pub fn is_spec_block(&self, bbi: BasicBlockIndex) -> bool {
+ // !self.nonspec_basic_blocks.contains(&bbi)
+ // }
/// Check whether the block is reachable
#[must_use]
diff --git a/rr_frontend/translation/src/function_body.rs b/rr_frontend/translation/src/function_body.rs
index f52cd8a3..875c1a2d 100644
--- a/rr_frontend/translation/src/function_body.rs
+++ b/rr_frontend/translation/src/function_body.rs
@@ -1161,10 +1161,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
) -> Result<radium::Function<'def>, TranslationError> {
// add loop info
let loop_info = self.proc.loop_info();
- info!("loop heads: {:?}", loop_info.loop_heads);
- for (head, bodies) in &loop_info.loop_bodies {
- info!("loop {:?} -> {:?}", head, bodies);
- }
+ loop_info.dump_body_head();
// translate the function's basic blocks
let basic_blocks = &self.proc.get_mir().basic_blocks;
@@ -1660,7 +1657,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
/// Find the optional `DefId` of the closure giving the invariant for the loop with head `head_bb`.
fn find_loop_spec_closure(&self, head_bb: BasicBlock) -> Result<Option<DefId>, TranslationError> {
- let bodies = &self.proc.loop_info().ordered_loop_bodies[&head_bb];
+ let bodies = self.proc.loop_info().get_loop_body(head_bb);
let basic_blocks = &self.proc.get_mir().basic_blocks;
// we go in order through the bodies in order to not stumble upon an annotation for a
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index 04a9a37e..17696fff 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -447,7 +447,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
)
.unwrap();
for (_, fun) in self.procedure_registry.iter_code() {
- if fun.spec.has_spec() {
+ if fun.spec.has_spec {
if fun.spec.args.len() != fun.code.get_argument_count() {
warn!("Function specification for {} is missing arguments", fun.name());
}
@@ -463,7 +463,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
// also write only-spec functions specs
for (_, spec) in self.procedure_registry.iter_only_spec() {
- if spec.has_spec() {
+ if spec.has_spec {
spec_file.write(format!("{}", spec).as_bytes()).unwrap();
spec_file.write("\n\n".as_bytes()).unwrap();
} else {
@@ -510,7 +510,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
let mode = self.procedure_registry.lookup_function_mode(*did).unwrap();
- if fun.spec.has_spec() && mode.needs_proof() {
+ if fun.spec.has_spec && mode.needs_proof() {
let mut imports = common_imports.clone();
imports.append(&mut vec![
@@ -547,7 +547,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
write!(template_file, "End proof.\n\n").unwrap();
fun.generate_proof_prelude(&mut template_file).unwrap();
- } else if !fun.spec.has_spec() {
+ } else if !fun.spec.has_spec {
write!(template_file, "(* No specification provided *)").unwrap();
} else {
write!(template_file, "(* Function is trusted *)").unwrap();
@@ -557,7 +557,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
fn check_function_needs_proof(&self, did: DefId, fun: &radium::Function) -> bool {
let mode = self.procedure_registry.lookup_function_mode(did).unwrap();
- fun.spec.has_spec() && mode.needs_proof()
+ fun.spec.has_spec && mode.needs_proof()
}
/// Write proofs for a verification unit.
diff --git a/rr_frontend/translation/src/type_translator.rs b/rr_frontend/translation/src/type_translator.rs
index 98d2fe42..a5b160cb 100644
--- a/rr_frontend/translation/src/type_translator.rs
+++ b/rr_frontend/translation/src/type_translator.rs
@@ -60,11 +60,11 @@ impl AdtUseKey {
#[derive(Debug)]
pub struct TypeTranslationScope<'def> {
/// defid of the current function
- pub(crate) did: DefId,
+ did: DefId,
/// maps generic indices (De Bruijn) to the corresponding Coq names in the current environment
/// the invariant is that they are Literals
- pub generic_scope: Vec<Option<radium::LiteralTyParam>>,
+ pub(crate) generic_scope: Vec<Option<radium::LiteralTyParam>>,
/// maps universal lifetime indices (Polonius) to their names. offset by 1 because 0 = static.
universal_lifetimes: HashMap<ty::RegionVid, String>,
@@ -72,6 +72,7 @@ pub struct TypeTranslationScope<'def> {
// TODO currently, these may contain duplicates
/// collection of tuple types that we use
pub(crate) tuple_uses: Vec<radium::LiteralTypeUse<'def>>,
+
/// Shim uses for the current function
pub(crate) shim_uses: HashMap<AdtUseKey, radium::LiteralTypeUse<'def>>,
}
--
GitLab