diff --git a/rr_frontend/.cargo/config.toml b/rr_frontend/.cargo/config.toml
index b289c02473cf7a8e14c857a89822f9f87f23223d..bb9a309ddbedf11946c46bea2fedef58c0ddaf2e 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::ref_patterns",
"-Aclippy::semicolon_inside_block",
"-Aclippy::str_to_string",
"-Aclippy::string_to_string",
diff --git a/rr_frontend/radium/src/coq.rs b/rr_frontend/radium/src/coq.rs
index b48e26e8d125cb3a6da0e511ec8831803bc1dd48..42476ff37d68153abfe713612b87692147fe7cae 100644
--- a/rr_frontend/radium/src/coq.rs
+++ b/rr_frontend/radium/src/coq.rs
@@ -391,7 +391,7 @@ pub struct Param {
impl Param {
#[must_use]
pub fn new(name: Name, ty: Type, implicit: bool) -> Self {
- let depends_on_sigma = if let Type::Literal(ref lit) = ty { lit.contains('Σ') } else { false };
+ let depends_on_sigma = if let Type::Literal(lit) = &ty { lit.contains('Σ') } else { false };
Self {
name,
@@ -414,13 +414,13 @@ impl Param {
}
if make_implicits {
- if let Name::Named(ref name) = self.name {
+ if let Name::Named(name) = &self.name {
format!("`{{{} : !{}}}", name, self.ty)
} else {
format!("`{{!{}}}", self.ty)
}
} else {
- if let Name::Named(ref name) = self.name {
+ if let Name::Named(name) = &self.name {
format!("`({} : !{})", name, self.ty)
} else {
format!("`(!{})", self.ty)
@@ -560,8 +560,8 @@ pub struct InstanceDecl {
impl Display for InstanceDecl {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
- match self.name {
- Some(ref name) => {
+ match &self.name {
+ Some(name) => {
write!(f, "{} Instance {} {} : {}{}", self.attrs, name, self.params, self.ty, self.body)
},
None => write!(f, "{} Instance {} : {}{}", self.attrs, self.params, self.ty, self.body),
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index df24cff9e96c81d8fbea12368e2b7cf89774de65..bd0ead242111bb33ae35320c32733f2540f76c63 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -1527,8 +1527,8 @@ impl<'def> AbstractStruct<'def> {
/// Get the name of the struct, or an ADT defined on it, if available.
#[must_use]
pub fn public_type_name(&self) -> &str {
- match self.invariant {
- Some(ref inv) => &inv.type_name,
+ match &self.invariant {
+ Some(inv) => &inv.type_name,
None => self.plain_ty_name(),
}
}
@@ -1540,8 +1540,8 @@ impl<'def> AbstractStruct<'def> {
#[must_use]
pub fn public_rt_def_name(&self) -> String {
- match self.invariant {
- Some(ref inv) => inv.rt_def_name(),
+ match &self.invariant {
+ Some(inv) => inv.rt_def_name(),
None => self.plain_rt_def_name().to_string(),
}
}
@@ -1563,7 +1563,7 @@ impl<'def> AbstractStruct<'def> {
/// Generate a Coq definition for the struct type alias.
#[must_use]
pub fn generate_coq_type_def(&self) -> String {
- let extra_context = if let Some(ref inv) = self.invariant { inv.coq_params.as_slice() } else { &[] };
+ let extra_context = if let Some(inv) = &self.invariant { inv.coq_params.as_slice() } else { &[] };
self.variant_def.generate_coq_type_def(&self.ty_params, extra_context)
}
@@ -1847,7 +1847,7 @@ impl<'def> AbstractStructUse<'def> {
}
if !self.is_raw() && def.invariant.is_some() {
- let Some(ref inv) = def.invariant else {
+ let Some(inv) = &def.invariant else {
unreachable!();
};
@@ -2167,7 +2167,7 @@ impl<'def> AbstractEnum<'def> {
}
// write the Coq inductive, if applicable
- if let Some(ref ind) = self.optional_inductive_def {
+ if let Some(ind) = &self.optional_inductive_def {
let mut assertions = coq::TopLevelAssertions::empty();
assertions.push(coq::TopLevelAssertion::Comment(format!(
@@ -2664,7 +2664,7 @@ impl<'def> FunctionSpec<'def> {
let mut out = String::with_capacity(100);
out.push_str("λ Ï, [");
- push_str_list!(out, &self.elctx, ", ", |(ref lft1, ref lft2)| format!("({lft1}, {lft2})"));
+ push_str_list!(out, &self.elctx, ", ", |(lft1, lft2)| format!("({lft1}, {lft2})"));
out.push(']');
out
@@ -2815,7 +2815,7 @@ impl<'def> FunctionSpecBuilder<'def> {
}
fn push_coq_name(&mut self, name: &coq::Name) {
- if let coq::Name::Named(ref name) = name {
+ if let coq::Name::Named(name) = &name {
self.coq_names.insert(name.to_string());
}
}
@@ -2868,7 +2868,7 @@ impl<'def> FunctionSpecBuilder<'def> {
}
fn ensure_coq_not_bound(&self, name: &coq::Name) -> Result<(), String> {
- if let coq::Name::Named(ref name) = name {
+ if let coq::Name::Named(name) = &name {
if self.coq_names.contains(name) {
return Err(format!("Coq name is already bound: {}", name));
}
@@ -2909,10 +2909,10 @@ impl<'def> FunctionSpecBuilder<'def> {
/// Add a new universal lifetime constraint.
pub fn add_lifetime_constraint(&mut self, lft1: UniversalLft, lft2: UniversalLft) -> Result<(), String> {
- if let UniversalLft::Local(ref s) = lft1 {
+ if let UniversalLft::Local(s) = &lft1 {
let _ = self.ensure_coq_bound(s)?;
}
- if let UniversalLft::Local(ref s) = lft2 {
+ if let UniversalLft::Local(s) = &lft2 {
let _ = self.ensure_coq_bound(s)?;
}
self.elctx.push((lft1, lft2));
diff --git a/rr_frontend/rrconfig/src/launch.rs b/rr_frontend/rrconfig/src/launch.rs
index 990cf478bc0471f88a92aeb59bc352270b06ca77..5fc302df76c2e0b158f324c0bc2eeb2daa85187a 100644
--- a/rr_frontend/rrconfig/src/launch.rs
+++ b/rr_frontend/rrconfig/src/launch.rs
@@ -33,7 +33,7 @@ pub fn add_to_loader_path(paths: Vec<PathBuf>, cmd: &mut Command) {
fn env_prepend_path(name: &str, value: Vec<PathBuf>, cmd: &mut Command) {
let old_value = env::var_os(name);
let mut parts = value;
- if let Some(ref v) = old_value {
+ if let Some(v) = &old_value {
parts.extend(env::split_paths(v));
};
match env::join_paths(parts) {
diff --git a/rr_frontend/translation/src/checked_op_analysis.rs b/rr_frontend/translation/src/checked_op_analysis.rs
index be827f5f88d860728c9dee384d97982067c6746c..c88841c03bafb7207cecca4efd80f71bbc711cf7 100644
--- a/rr_frontend/translation/src/checked_op_analysis.rs
+++ b/rr_frontend/translation/src/checked_op_analysis.rs
@@ -52,7 +52,7 @@ impl<'def, 'tcx> CheckedOpLocalAnalysis<'def, 'tcx> {
fn successors_of_bb(bb: &BasicBlockData<'tcx>) -> Vec<BasicBlock> {
let mut v = Vec::new();
- let Some(ref term) = bb.terminator else {
+ let Some(term) = &bb.terminator else {
return v;
};
@@ -66,26 +66,17 @@ impl<'def, 'tcx> CheckedOpLocalAnalysis<'def, 'tcx> {
} => v.push(*target),
TerminatorKind::InlineAsm {
- template: _,
- operands: _,
- options: _,
- line_spans: _,
destination: Some(destination),
- unwind: _,
+ ..
} => v.push(*destination),
- TerminatorKind::SwitchInt { discr: _, targets } => {
+ TerminatorKind::SwitchInt { targets, .. } => {
for target in targets.all_targets() {
v.push(*target);
}
},
- TerminatorKind::Yield {
- value: _,
- resume,
- resume_arg: _,
- drop: _,
- } => v.push(*resume),
+ TerminatorKind::Yield { resume, .. } => v.push(*resume),
_ => (),
}
diff --git a/rr_frontend/translation/src/environment/dump_borrowck_info.rs b/rr_frontend/translation/src/environment/dump_borrowck_info.rs
index 2842d20b383a905db859a2b20f064f1a3dd8299e..b189694d7c3f958a9d220e49a2f81519949c237a 100644
--- a/rr_frontend/translation/src/environment/dump_borrowck_info.rs
+++ b/rr_frontend/translation/src/environment/dump_borrowck_info.rs
@@ -546,14 +546,16 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> {
write_graph!(self, "</th>");
let mir::BasicBlockData {
- ref statements,
- ref terminator,
+ statements,
+ terminator,
..
- } = self.mir[bb];
+ } = &self.mir[bb];
+
let mut location = mir::Location {
block: bb,
statement_index: 0,
};
+
let terminator_index = statements.len();
while location.statement_index < terminator_index {
@@ -575,7 +577,7 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> {
write_graph!(self, "</tr>");
write_graph!(self, "</table>> ];");
- if let Some(ref terminator) = &terminator {
+ if let Some(terminator) = &terminator {
self.visit_terminator(bb, terminator)?;
}
@@ -783,11 +785,11 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> {
fn visit_terminator(&self, bb: mir::BasicBlock, terminator: &mir::Terminator) -> Result<(), io::Error> {
use rustc_middle::mir::TerminatorKind;
- match terminator.kind {
+ match &terminator.kind {
TerminatorKind::Goto { target } => {
write_edge!(self, bb, target);
},
- TerminatorKind::SwitchInt { ref targets, .. } => {
+ TerminatorKind::SwitchInt { targets, .. } => {
for target in targets.all_targets() {
write_edge!(self, bb, target);
}
@@ -802,18 +804,14 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> {
TerminatorKind::UnwindTerminate(_) => {
write_edge!(self, bb, str terminate);
},
- TerminatorKind::Drop {
- ref target, unwind, ..
- } => {
+ TerminatorKind::Drop { target, unwind, .. } => {
write_edge!(self, bb, target);
//if let Some(target) = unwind {
//write_edge!(self, bb, unwind target);
//}
},
- TerminatorKind::Call {
- ref target, unwind, ..
- } => {
- if let Some(target) = *target {
+ TerminatorKind::Call { target, unwind, .. } => {
+ if let Some(target) = target {
write_edge!(self, bb, target);
}
//if let Some(target) = unwind {
@@ -829,8 +827,8 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> {
TerminatorKind::Yield { .. } => unimplemented!(),
TerminatorKind::GeneratorDrop => unimplemented!(),
TerminatorKind::FalseEdge {
- ref real_target,
- ref imaginary_target,
+ real_target,
+ imaginary_target,
} => {
write_edge!(self, bb, real_target);
write_edge!(self, bb, imaginary_target);
diff --git a/rr_frontend/translation/src/environment/mir_utils/real_edges.rs b/rr_frontend/translation/src/environment/mir_utils/real_edges.rs
index 39eb9929a02e026dc40c6fe4eae5c4e055253611..a853c15581b3c51c255df44fd31fbb25227bd329 100644
--- a/rr_frontend/translation/src/environment/mir_utils/real_edges.rs
+++ b/rr_frontend/translation/src/environment/mir_utils/real_edges.rs
@@ -44,12 +44,12 @@ impl RealEdges {
}
fn real_targets(terminator: &mir::Terminator) -> Vec<mir::BasicBlock> {
- match terminator.kind {
- TerminatorKind::Goto { ref target } | TerminatorKind::Assert { ref target, .. } => {
+ match &terminator.kind {
+ TerminatorKind::Goto { target } | TerminatorKind::Assert { target, .. } => {
vec![*target]
},
- TerminatorKind::SwitchInt { ref targets, .. } => targets.all_targets().to_vec(),
+ TerminatorKind::SwitchInt { targets, .. } => targets.all_targets().to_vec(),
TerminatorKind::GeneratorDrop
| TerminatorKind::Return
@@ -57,26 +57,21 @@ fn real_targets(terminator: &mir::Terminator) -> Vec<mir::BasicBlock> {
| TerminatorKind::UnwindResume
| TerminatorKind::UnwindTerminate(_) => vec![],
- TerminatorKind::Drop { ref target, .. } => vec![*target],
+ TerminatorKind::Drop { target, .. } => vec![*target],
- TerminatorKind::Call { ref target, .. } => match *target {
- Some(target) => vec![target],
+ TerminatorKind::Call { target, .. } => match target {
+ Some(target) => vec![*target],
None => vec![],
},
- TerminatorKind::FalseEdge {
- ref real_target, ..
- }
- | TerminatorKind::FalseUnwind {
- ref real_target, ..
- } => vec![*real_target],
+ TerminatorKind::FalseEdge { real_target, .. } | TerminatorKind::FalseUnwind { real_target, .. } => {
+ vec![*real_target]
+ },
- TerminatorKind::Yield { ref resume, .. } => vec![*resume],
+ TerminatorKind::Yield { resume, .. } => vec![*resume],
- TerminatorKind::InlineAsm {
- ref destination, ..
- } => match *destination {
- Some(target) => vec![target],
+ TerminatorKind::InlineAsm { destination, .. } => match destination {
+ Some(target) => vec![*target],
None => vec![],
},
}
diff --git a/rr_frontend/translation/src/environment/mir_utils/statement_as_assign.rs b/rr_frontend/translation/src/environment/mir_utils/statement_as_assign.rs
index b2472a731885d588950d6c8a1ba4b22ee573cd79..54b429624bea552c727e6de2f35d26bd11636593 100644
--- a/rr_frontend/translation/src/environment/mir_utils/statement_as_assign.rs
+++ b/rr_frontend/translation/src/environment/mir_utils/statement_as_assign.rs
@@ -13,6 +13,6 @@ pub trait StatementAsAssign<'tcx> {
impl<'tcx> StatementAsAssign<'tcx> for mir::Statement<'tcx> {
fn as_assign(&self) -> Option<(mir::Place<'tcx>, &mir::Rvalue<'tcx>)> {
- if let mir::StatementKind::Assign(box (lhs, ref rhs)) = self.kind { Some((lhs, rhs)) } else { None }
+ if let mir::StatementKind::Assign(box (lhs, rhs)) = &self.kind { Some((*lhs, rhs)) } else { None }
}
}
diff --git a/rr_frontend/translation/src/environment/polonius_info.rs b/rr_frontend/translation/src/environment/polonius_info.rs
index 5e4bf5d5f323b1a967f5e480c04c6d5486dd5480..177d04eb28eaa72052e110166dc2ab7a0a4d0b38 100644
--- a/rr_frontend/translation/src/environment/polonius_info.rs
+++ b/rr_frontend/translation/src/environment/polonius_info.rs
@@ -361,52 +361,54 @@ fn get_borrowed_places<'a, 'tcx: 'a>(
return Ok(Vec::new());
};
- let mir::BasicBlockData { ref statements, .. } = mir[location.block];
+ let mir::BasicBlockData { statements, .. } = &mir[location.block];
+
if statements.len() == location.statement_index {
return Ok(Vec::new());
}
- let statement = &statements[location.statement_index];
- match statement.kind {
- mir::StatementKind::Assign(box (ref _lhs, ref rhs)) => match *rhs {
- mir::Rvalue::Use(mir::Operand::Copy(ref place) | mir::Operand::Move(ref place))
- | mir::Rvalue::Ref(_, _, ref place)
- | mir::Rvalue::Discriminant(ref place) => Ok(vec![place]),
+ let kind = &statements[location.statement_index].kind;
+ let mir::StatementKind::Assign(box (_, rhs)) = kind else {
+ unreachable!("{:?}", kind);
+ };
- mir::Rvalue::Use(mir::Operand::Constant(_)) => Ok(Vec::new()),
+ match rhs {
+ mir::Rvalue::Use(mir::Operand::Copy(place) | mir::Operand::Move(place))
+ | mir::Rvalue::Ref(_, _, place)
+ | mir::Rvalue::Discriminant(place) => Ok(vec![place]),
- mir::Rvalue::Aggregate(_, ref operands) => Ok(operands
- .iter()
- .filter_map(|operand| match *operand {
- mir::Operand::Copy(ref place) | mir::Operand::Move(ref place) => Some(place),
- mir::Operand::Constant(_) => None,
- })
- .collect()),
-
- // slice creation involves an unsize pointer cast like [i32; 3] -> &[i32]
- mir::Rvalue::Cast(
- mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize),
- ref operand,
- ref ty,
- ) if ty.is_slice() && !ty.is_unsafe_ptr() => {
- trace!("slice: operand={:?}, ty={:?}", operand, ty);
- Ok(match *operand {
- mir::Operand::Copy(ref place) | mir::Operand::Move(ref place) => vec![place],
- mir::Operand::Constant(_) => vec![],
- })
- },
+ mir::Rvalue::Use(mir::Operand::Constant(_)) => Ok(Vec::new()),
- mir::Rvalue::Cast(..) => {
- // all other loan-casts are unsupported
- Err(PoloniusInfoError::LoanInUnsupportedStatement(
- "cast statements that create loans are not supported".to_string(),
- *location,
- ))
- },
+ mir::Rvalue::Aggregate(_, operands) => Ok(operands
+ .iter()
+ .filter_map(|operand| match operand {
+ mir::Operand::Copy(place) | mir::Operand::Move(place) => Some(place),
+ mir::Operand::Constant(_) => None,
+ })
+ .collect()),
+
+ // slice creation involves an unsize pointer cast like [i32; 3] -> &[i32]
+ mir::Rvalue::Cast(
+ mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize),
+ operand,
+ ty,
+ ) if ty.is_slice() && !ty.is_unsafe_ptr() => {
+ trace!("slice: operand={:?}, ty={:?}", operand, ty);
+ Ok(match operand {
+ mir::Operand::Copy(place) | mir::Operand::Move(place) => vec![place],
+ mir::Operand::Constant(_) => vec![],
+ })
+ },
- ref x => unreachable!("{:?}", x),
+ mir::Rvalue::Cast(..) => {
+ // all other loan-casts are unsupported
+ Err(PoloniusInfoError::LoanInUnsupportedStatement(
+ "cast statements that create loans are not supported".to_string(),
+ *location,
+ ))
},
- ref x => unreachable!("{:?}", x),
+
+ x => unreachable!("{:?}", x),
}
}
@@ -1345,85 +1347,93 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
/// Check if the statement is assignment.
fn is_assignment(mir: &mir::Body<'_>, location: mir::Location) -> bool {
- let mir::BasicBlockData { ref statements, .. } = mir[location.block];
+ let mir::BasicBlockData { statements, .. } = &mir[location.block];
+
if statements.len() == location.statement_index {
return false;
}
+
matches!(statements[location.statement_index].kind, mir::StatementKind::Assign { .. })
}
/// Check if the terminator is return.
fn is_return(mir: &mir::Body<'_>, location: mir::Location) -> bool {
let mir::BasicBlockData {
- ref statements,
- ref terminator,
+ statements,
+ terminator,
..
- } = mir[location.block];
+ } = &mir[location.block];
+
if statements.len() != location.statement_index {
return false;
}
+
matches!(terminator.as_ref().unwrap().kind, mir::TerminatorKind::Return)
}
fn is_call(mir: &mir::Body<'_>, location: mir::Location) -> bool {
let mir::BasicBlockData {
- ref statements,
- ref terminator,
+ statements,
+ terminator,
..
- } = mir[location.block];
+ } = &mir[location.block];
+
if statements.len() != location.statement_index {
return false;
}
+
matches!(terminator.as_ref().unwrap().kind, mir::TerminatorKind::Call { .. })
}
/// Extract the call terminator at the location. Otherwise return None.
fn get_call_destination<'tcx>(mir: &mir::Body<'tcx>, location: mir::Location) -> Option<mir::Place<'tcx>> {
let mir::BasicBlockData {
- ref statements,
- ref terminator,
+ statements,
+ terminator,
..
- } = mir[location.block];
+ } = &mir[location.block];
+
if statements.len() != location.statement_index {
return None;
}
- match terminator.as_ref().unwrap().kind {
- mir::TerminatorKind::Call {
- ref destination, ..
- } => Some(*destination),
- ref x => {
- panic!("Expected call, got {:?} at {:?}", x, location);
- },
- }
+
+ let kind = &terminator.as_ref().unwrap().kind;
+ let mir::TerminatorKind::Call { destination, .. } = kind else {
+ panic!("Expected call, got {:?} at {:?}", kind, location);
+ };
+
+ Some(*destination)
}
/// Extract reference-typed arguments of the call at the given location.
fn get_call_arguments(mir: &mir::Body<'_>, location: mir::Location) -> Vec<mir::Local> {
let mir::BasicBlockData {
- ref statements,
- ref terminator,
+ statements,
+ terminator,
..
- } = mir[location.block];
+ } = &mir[location.block];
+
assert!(statements.len() == location.statement_index);
- match terminator.as_ref().unwrap().kind {
- mir::TerminatorKind::Call { ref args, .. } => {
- let mut reference_args = Vec::new();
- for arg in args {
- match arg {
- mir::Operand::Copy(place) | mir::Operand::Move(place) => {
- if place.projection.len() == 0 {
- reference_args.push(place.local);
- }
- },
- mir::Operand::Constant(_) => {},
+
+ let kind = &terminator.as_ref().unwrap().kind;
+ let mir::TerminatorKind::Call { args, .. } = kind else {
+ panic!("Expected call, got {:?} at {:?}", kind, location);
+ };
+
+ let mut reference_args = Vec::new();
+
+ for arg in args {
+ match arg {
+ mir::Operand::Copy(place) | mir::Operand::Move(place) => {
+ if place.projection.len() == 0 {
+ reference_args.push(place.local);
}
- }
- reference_args
- },
- ref x => {
- panic!("Expected call, got {:?} at {:?}", x, location);
- },
+ },
+ mir::Operand::Constant(_) => {},
+ }
}
+
+ reference_args
}
/// Additional facts derived from the borrow checker facts.
diff --git a/rr_frontend/translation/src/environment/procedure.rs b/rr_frontend/translation/src/environment/procedure.rs
index bd37fce7cc119dd3932fd10690464d820cc9af5f..65f8989517a125fb941bf80501e27f2888340cc1 100644
--- a/rr_frontend/translation/src/environment/procedure.rs
+++ b/rr_frontend/translation/src/environment/procedure.rs
@@ -183,29 +183,28 @@ impl<'tcx> Procedure<'tcx> {
#[must_use]
pub fn is_panic_block(&self, bbi: BasicBlockIndex) -> bool {
- if let TerminatorKind::Call {
- args: ref _args,
- destination: ref _destination,
- func:
- mir::Operand::Constant(box mir::Constant {
- literal: mir::ConstantKind::Ty(c),
- ..
- }),
- ..
- } = self.mir[bbi].terminator().kind
- {
- if let ty::TyKind::FnDef(def_id, ..) = c.ty().kind() {
- // let func_proc_name = self.tcx.absolute_item_path_str(def_id);
- let func_proc_name = self.tcx.def_path_str(*def_id);
- &func_proc_name == "std::rt::begin_panic"
- || &func_proc_name == "core::panicking::panic"
- || &func_proc_name == "core::panicking::panic_fmt"
- } else {
- false
- }
- } else {
- false
- }
+ let TerminatorKind::Call { func, .. } = &self.mir[bbi].terminator().kind else {
+ return false;
+ };
+
+ let mir::Operand::Constant(box mir::Constant { literal, .. }) = func else {
+ return false;
+ };
+
+ let mir::ConstantKind::Ty(c) = literal else {
+ return false;
+ };
+
+ let ty::TyKind::FnDef(def_id, ..) = c.ty().kind() else {
+ return false;
+ };
+
+ // let func_proc_name = self.tcx.absolute_item_path_str(def_id);
+ let func_proc_name = self.tcx.def_path_str(*def_id);
+
+ func_proc_name == "std::rt::begin_panic"
+ || func_proc_name == "core::panicking::panic"
+ || func_proc_name == "core::panicking::panic_fmt"
}
/// Get the successors of a basic block.
diff --git a/rr_frontend/translation/src/function_body.rs b/rr_frontend/translation/src/function_body.rs
index 3f150608c3015c5ad4fa3b6bcd8603ee764ec575..16cd3981cb5bbf0bb96a2c206bd3b0ec980b7b17 100644
--- a/rr_frontend/translation/src/function_body.rs
+++ b/rr_frontend/translation/src/function_body.rs
@@ -327,7 +327,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
typ: facts::PointType::Start,
});
- for (ref r1, ref r2, ref p) in &info.borrowck_in_facts.subset_base {
+ for (r1, r2, p) in &info.borrowck_in_facts.subset_base {
if *p == root_point && *r2 == r {
info!("find placeholder region for: {:?} ⊑ {:?} = r = {:?}", r1, r2, r);
return Some(*r1);
@@ -1668,7 +1668,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
// check the statements for an assignment
let data = basic_blocks.get(*body).unwrap();
for stmt in &data.statements {
- if let StatementKind::Assign(box (ref pl, _)) = stmt.kind {
+ if let StatementKind::Assign(box (pl, _)) = stmt.kind {
if let Some(did) = self.is_spec_closure_local(pl.local)? {
return Ok(Some(did));
}
@@ -2093,13 +2093,13 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
loc: Location,
dying_loans: Vec<facts::Loan>,
) -> Result<radium::Stmt, TranslationError> {
- match term.kind {
- TerminatorKind::Goto { target } => self.translate_goto_like(&loc, target),
+ match &term.kind {
+ TerminatorKind::Goto { target } => self.translate_goto_like(&loc, *target),
TerminatorKind::Call {
- ref func,
- ref args,
- ref destination,
+ func,
+ args,
+ destination,
target,
..
} => {
@@ -2109,7 +2109,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
return Ok(radium::Stmt::Stuck);
}
- self.translate_function_call(func, args, destination, target, loc, dying_loans.as_slice())
+ self.translate_function_call(func, args, destination, *target, loc, dying_loans.as_slice())
},
TerminatorKind::Return => {
@@ -2132,10 +2132,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
//res_stmt = radium::Stmt::Stuck;
//res_stmt = self.prepend_endlfts(res_stmt, dying_loans.into_iter());
//},
- TerminatorKind::SwitchInt {
- ref discr,
- ref targets,
- } => {
+ TerminatorKind::SwitchInt { discr, targets } => {
let operand = self.translate_operand(discr, true)?;
let all_targets: &[BasicBlock] = targets.all_targets();
@@ -2197,7 +2194,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
},
TerminatorKind::Assert {
- ref cond,
+ cond,
expected,
target,
..
@@ -2209,10 +2206,10 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
ot1: radium::OpType::BoolOp,
ot2: radium::OpType::BoolOp,
e1: Box::new(cond_translated),
- e2: Box::new(radium::Expr::Literal(radium::Literal::LitBool(expected))),
+ e2: Box::new(radium::Expr::Literal(radium::Literal::LitBool(*expected))),
};
- let stmt = self.translate_goto_like(&loc, target)?;
+ let stmt = self.translate_goto_like(&loc, *target)?;
// TODO: should we really have this?
let stmt = self.prepend_endlfts(stmt, dying_loans.into_iter());
@@ -2223,31 +2220,24 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
})
},
- TerminatorKind::Drop {
- ref place, target, ..
- } => {
+ TerminatorKind::Drop { place, target, .. } => {
let ty = self.get_type_of_place(place);
self.register_drop_shim_for(ty.ty);
let place_translated = self.translate_place(place)?;
let _drope = radium::Expr::DropE(Box::new(place_translated));
- let stmt = self.translate_goto_like(&loc, target)?;
+ let stmt = self.translate_goto_like(&loc, *target)?;
Ok(self.prepend_endlfts(stmt, dying_loans.into_iter()))
//res_stmt = radium::Stmt::ExprS { e: drope, s: Box::new(res_stmt)};
},
- TerminatorKind::FalseEdge { real_target, .. } => {
- // just a goto for our purposes
- self.translate_goto_like(&loc, real_target)
- },
-
- TerminatorKind::FalseUnwind {
- ref real_target, ..
- } => {
- // this is just a virtual edge for the borrowchecker, we can translate this to a normal goto
+ // just a goto for our purposes
+ TerminatorKind::FalseEdge { real_target, .. }
+ // this is just a virtual edge for the borrowchecker, we can translate this to a normal goto
+ | TerminatorKind::FalseUnwind { real_target, .. } => {
self.translate_goto_like(&loc, *real_target)
},
@@ -3399,7 +3389,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
match op {
// In Caesium: typed_place needs deref (not use) for place accesses.
// use is used top-level to convert an lvalue to an rvalue, which is why we use it here.
- Operand::Copy(ref place) | Operand::Move(ref place) => {
+ Operand::Copy(place) | Operand::Move(place) => {
// check if this goes to a temporary of a checked op
let place_kind = if self.checked_op_temporaries.contains_key(&place.local) {
assert!(place.projection.len() == 1);
@@ -3435,7 +3425,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
Ok(translated_place)
}
},
- Operand::Constant(ref constant) => {
+ Operand::Constant(constant) => {
// TODO: possibly need different handling of the rvalue flag
// when this also handles string literals etc.
return self.translate_constant(constant.as_ref());
@@ -3590,7 +3580,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
let const_ty = v.ty();
match v.kind() {
- ConstKind::Value(ref v) => {
+ ConstKind::Value(v) => {
// this doesn't contain the necessary structure anymore. Need to reconstruct using the
// type.
match v.try_to_scalar() {
@@ -3647,8 +3637,8 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
let mut acc_expr = radium::Expr::Var(local_name.to_string());
// iterate in evaluation order
- for ref it in pl.projection {
- match it {
+ for it in pl.projection {
+ match &it {
ProjectionElem::Deref => {
// use the type of the dereferencee
let st = self.ty_translator.translate_type_to_syn_type(cur_ty.ty)?;
@@ -3724,7 +3714,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
},
};
// update cur_ty
- cur_ty = cur_ty.projection_ty(self.env.tcx(), *it);
+ cur_ty = cur_ty.projection_ty(self.env.tcx(), it);
}
info!("translating place {:?} to {:?}", pl, acc_expr);
Ok(acc_expr)
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index bd0ae205d108d0e66f8bb66542ef4425f403ef7d..3f8f94d4d48605fc991ce595682d4ef18e40648d 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -700,7 +700,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
let mut dune_project_file =
io::BufWriter::new(fs::File::create(dune_project_path.as_path()).unwrap());
- let (project_name, dune_project_package) = if let Some(ref dune_package) = self.dune_package {
+ let (project_name, dune_project_package) = if let Some(dune_package) = &self.dune_package {
(dune_package.to_string(), format!("(package (name {dune_package}))\n"))
} else {
(stem.to_string(), format!(""))
@@ -747,7 +747,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
let extra_theories: Vec<String> = extra_theories.into_iter().map(|x| x.to_string()).collect();
- let dune_package = if let Some(ref dune_package) = self.dune_package {
+ let dune_package = if let Some(dune_package) = &self.dune_package {
format!("(package {dune_package})\n")
} else {
format!("")
diff --git a/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs b/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
index e49d374a479c46b23327e59c7f099b2ae4bb3beb..52d46912679bc473ee69b17bb8224a67fe80185b 100644
--- a/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
@@ -251,7 +251,7 @@ where
lit: &LiteralTypeWithRef,
ty: &specs::Type<'def>,
) -> (specs::TypeWithRef<'def>, Option<coq::Type>) {
- if let Some(ref lit_ty) = lit.ty {
+ if let Some(lit_ty) = &lit.ty {
// literal type given, we use this literal type as the RR semantic type
// just use the syntype from the Rust type
let st = ty.get_syn_type();
@@ -321,7 +321,7 @@ where
builder.spec.add_arg(ty);
if let Some(cty) = hint {
// potentially add a typing hint to the refinement
- if let IdentOrTerm::Ident(ref i) = arg.rfn {
+ if let IdentOrTerm::Ident(i) = arg.rfn {
info!("Trying to add a typing hint for {}", i);
builder.spec.add_param_type_annot(&coq::Name::Named(i.clone()), cty)?;
}
diff --git a/rr_frontend/translation/src/type_translator.rs b/rr_frontend/translation/src/type_translator.rs
index d61195f6cc6add26f460d7d23856a3690b17f68f..476d17ef984fbeed2c50127cf5e1066c4b9c7868 100644
--- a/rr_frontend/translation/src/type_translator.rs
+++ b/rr_frontend/translation/src/type_translator.rs
@@ -417,8 +417,8 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
ty::RegionKind::ReStatic => Some("static".to_string()),
ty::RegionKind::ReErased => Some("erased".to_string()),
- ty::RegionKind::ReVar(v) => match translation_state {
- TranslationStateInner::InFunction(ref scope) => {
+ ty::RegionKind::ReVar(v) => match &translation_state {
+ TranslationStateInner::InFunction(scope) => {
let r = scope.lookup_universal_region(v);
info!("Translating region: ReVar {:?} as {:?}", v, r);
r
@@ -614,10 +614,10 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
};
let translated_ty = match state {
- TranslationStateInner::TranslateAdt(ref mut deps) => {
+ TranslationStateInner::TranslateAdt(deps) => {
self.translate_type_with_deps(arg_ty, &mut TranslationStateInner::TranslateAdt(deps))?
},
- TranslationStateInner::InFunction(ref mut scope) => {
+ TranslationStateInner::InFunction(scope) => {
let mut translated_ty =
self.translate_type_with_deps(arg_ty, &mut TranslationStateInner::InFunction(scope))?;
@@ -656,7 +656,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
let params = self.translate_generic_args(args, &mut *state)?;
let key = AdtUseKey::new(variant_id, ¶ms);
- if let TranslationStateInner::InFunction(ref mut scope) = state {
+ if let TranslationStateInner::InFunction(scope) = state {
let lit_uses = &mut scope.shim_uses;
lit_uses
@@ -721,7 +721,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
// TODO: don't generate duplicates
let struct_use = radium::LiteralTypeUse::new(lit, params);
- if let TranslationStateInner::InFunction(ref mut scope) = *state {
+ if let TranslationStateInner::InFunction(scope) = state {
scope.tuple_uses.push(struct_use.clone());
}
@@ -954,7 +954,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
info!("finished variant def: {:?}", struct_def);
// now add the invariant, if one was annotated
- if let Some(ref mut invariant_spec) = invariant_spec {
+ if let Some(invariant_spec) = &mut invariant_spec {
if expect_refinement {
// make a plist out of this
let mut rfn = String::with_capacity(100);
@@ -1316,7 +1316,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
let key = AdtUseKey::new(adt.did(), ¶ms);
let shim_use = radium::LiteralTypeUse::new(shim, params);
- if let TranslationStateInner::InFunction(ref mut scope) = state {
+ if let TranslationStateInner::InFunction(scope) = state {
// track this shim use for the current function
scope.shim_uses.entry(key).or_insert_with(|| shim_use.clone());
}
@@ -1414,7 +1414,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
return Ok(radium::Type::Unit);
}
- if let TranslationStateInner::TranslateAdt(ref mut adt_deps) = *state {
+ if let TranslationStateInner::TranslateAdt(adt_deps) = state {
adt_deps.insert(adt.did());
}
@@ -1452,7 +1452,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
},
TyKind::Param(param_ty) => {
- let TranslationStateInner::InFunction(ref mut scope) = state else {
+ let TranslationStateInner::InFunction(scope) = state else {
info!("using generic type param: {}", param_ty);
return Ok(radium::Type::Var(param_ty.index as usize));
};
@@ -1828,7 +1828,7 @@ impl<'def, 'tcx> TypeTranslator<'def, 'tcx> {
//let struct_use = radium::AbstractStructUse::new(struct_ref, translated_tys,
// radium::TypeIsRaw::Yes);
let struct_use = radium::LiteralTypeUse::new(lit, translated_tys);
- if let TranslationStateInner::InFunction(ref mut scope) = *state {
+ if let TranslationStateInner::InFunction(scope) = state {
scope.tuple_uses.push(struct_use.clone());
}
diff --git a/rr_frontend/translation/src/utils.rs b/rr_frontend/translation/src/utils.rs
index 7bc4080e2d5fa945f4ec13be0f21810d6c56a5f8..6c1038bfd2e11a82999b2fe6fb6369063cee698a 100644
--- a/rr_frontend/translation/src/utils.rs
+++ b/rr_frontend/translation/src/utils.rs
@@ -719,8 +719,8 @@ pub fn has_any_tool_attr(attrs: &[ast::Attribute]) -> bool {
pub fn filter_tool_attrs(attrs: &[ast::Attribute]) -> Vec<&ast::AttrItem> {
attrs
.iter()
- .filter_map(|attr| match attr.kind {
- ast::AttrKind::Normal(ref na) => {
+ .filter_map(|attr| match &attr.kind {
+ ast::AttrKind::Normal(na) => {
let item = &na.item;
let seg = item.path.segments.get(0)?;