From 64c128756d4e61f2660fd8f81ce73cae22fe3236 Mon Sep 17 00:00:00 2001
From: Vincent Lafeychine <vincent.lafeychine@proton.me>
Date: Thu, 2 May 2024 20:22:35 +0200
Subject: [PATCH] clippy: Fix must_use_candidate
---
rr_frontend/.cargo/config.toml | 1 -
rr_frontend/attribute_parse/src/parse.rs | 12 +++
rr_frontend/radium/src/code.rs | 12 +++
rr_frontend/radium/src/coq.rs | 5 ++
rr_frontend/radium/src/specs.rs | 86 +++++++++++++++++++
rr_frontend/rrconfig/src/launch.rs | 1 +
rr_frontend/rrconfig/src/lib.rs | 25 ++++++
.../src/environment/borrowck/facts.rs | 4 +
.../src/environment/borrowck/regions.rs | 1 +
.../translation/src/environment/loops.rs | 12 +++
.../mir_analyses/initialization.rs | 3 +
.../src/environment/mir_sets/local_set.rs | 2 +
.../src/environment/mir_sets/place_set.rs | 5 ++
.../src/environment/mir_utils/real_edges.rs | 2 +
.../translation/src/environment/mod.rs | 1 +
.../src/environment/polonius_info.rs | 30 +++++++
.../translation/src/environment/procedure.rs | 15 ++++
17 files changed, 216 insertions(+), 1 deletion(-)
diff --git a/rr_frontend/.cargo/config.toml b/rr_frontend/.cargo/config.toml
index d8cc38de..60f51a34 100644
--- a/rr_frontend/.cargo/config.toml
+++ b/rr_frontend/.cargo/config.toml
@@ -32,7 +32,6 @@ rustflags = [
"-Aclippy::string_lit_as_bytes",
# clippy::pedantic
- "-Aclippy::must_use_candidate",
"-Aclippy::needless_continue",
"-Aclippy::needless_pass_by_value",
"-Aclippy::redundant_closure_for_method_calls",
diff --git a/rr_frontend/attribute_parse/src/parse.rs b/rr_frontend/attribute_parse/src/parse.rs
index aee9f8a1..056ae9b3 100644
--- a/rr_frontend/attribute_parse/src/parse.rs
+++ b/rr_frontend/attribute_parse/src/parse.rs
@@ -119,6 +119,7 @@ pub struct ParseBuffer {
}
impl ParseBuffer {
+ #[must_use]
pub fn new(stream: &rustc_ast::tokenstream::TokenStream) -> Self {
// TODO; maybe avoid the cloning
let trees: Vec<TokenTree> = stream.trees().cloned().collect();
@@ -441,6 +442,7 @@ pub struct LitStr {
}
impl LitStr {
+ #[must_use]
pub fn value(&self) -> String {
self.sym.to_string()
}
@@ -478,6 +480,7 @@ where
}
impl Ident {
+ #[must_use]
pub fn value(&self) -> String {
self.sym.to_string()
}
@@ -625,6 +628,7 @@ mod value {
}
}
+#[must_use]
pub fn xid_ok(symbol: &str) -> bool {
let mut chars = symbol.chars();
let first = chars.next().unwrap();
@@ -647,6 +651,7 @@ pub struct BigInt {
}
impl BigInt {
+ #[must_use]
pub const fn new() -> Self {
Self { digits: Vec::new() }
}
@@ -716,6 +721,7 @@ pub struct Punctuated<T, P> {
impl<T, P> Punctuated<T, P> {
/// Creates an empty punctuated sequence.
+ #[must_use]
pub const fn new() -> Self {
Self {
inner: Vec::new(),
@@ -725,6 +731,7 @@ impl<T, P> Punctuated<T, P> {
/// Determines whether this punctuated sequence is empty, meaning it
/// contains no syntax tree nodes or punctuation.
+ #[must_use]
pub fn is_empty(&self) -> bool {
self.inner.len() == 0 && self.last.is_none()
}
@@ -733,11 +740,13 @@ impl<T, P> Punctuated<T, P> {
///
/// This is the number of nodes of type `T`, not counting the punctuation of
/// type `P`.
+ #[must_use]
pub fn len(&self) -> usize {
self.inner.len() + usize::from(self.last.is_some())
}
/// Borrows the first element in this sequence.
+ #[must_use]
pub fn first(&self) -> Option<&T> {
self.iter().next()
}
@@ -748,6 +757,7 @@ impl<T, P> Punctuated<T, P> {
//}
/// Borrows the last element in this sequence.
+ #[must_use]
pub fn last(&self) -> Option<&T> {
self.iter().next_back()
}
@@ -850,6 +860,7 @@ impl<T, P> Punctuated<T, P> {
/// Determines whether this punctuated sequence ends with a trailing
/// punctuation.
+ #[must_use]
pub fn trailing_punct(&self) -> bool {
self.last.is_none() && !self.is_empty()
}
@@ -858,6 +869,7 @@ impl<T, P> Punctuated<T, P> {
/// punctuation.
///
/// Equivalent to `punctuated.is_empty() || punctuated.trailing_punct()`.
+ #[must_use]
pub const fn empty_or_trailing(&self) -> bool {
self.last.is_none()
}
diff --git a/rr_frontend/radium/src/code.rs b/rr_frontend/radium/src/code.rs
index cc007ab5..bfb132f7 100644
--- a/rr_frontend/radium/src/code.rs
+++ b/rr_frontend/radium/src/code.rs
@@ -95,6 +95,7 @@ impl Display for RustType {
}
impl RustType {
+ #[must_use]
pub fn of_type(ty: &Type<'_>, env: &[Option<LiteralTyParam>]) -> Self {
info!("Translating rustType: {:?}", ty);
match ty {
@@ -297,6 +298,7 @@ pub enum Expr {
}
impl Expr {
+ #[must_use]
pub fn with_optional_annotation(e: Self, a: Option<Annotation>, why: Option<String>) -> Self {
match a {
Some(a) => Self::Annot {
@@ -624,6 +626,7 @@ impl Stmt {
}
/// Annotate a statement with a list of annotations
+ #[must_use]
pub fn with_annotations(mut s: Self, a: Vec<Annotation>, why: Option<String>) -> Self {
for annot in a {
s = Self::Annot {
@@ -753,6 +756,7 @@ fn make_lft_map_string(els: Vec<(String, String)>) -> String {
impl FunctionCode {
const INITIAL_BB: usize = 0;
+ #[must_use]
pub fn caesium_fmt(&self) -> String {
// format args
let format_stack_layout = |layout: std::slice::Iter<'_, (String, SynType)>| {
@@ -825,6 +829,7 @@ impl FunctionCode {
}
/// Get the number of arguments of the function.
+ #[must_use]
pub fn get_argument_count(&self) -> usize {
self.stack_layout.iter_args().len()
}
@@ -840,6 +845,7 @@ pub struct StackMap {
}
impl StackMap {
+ #[must_use]
pub fn new() -> Self {
Self {
arg_map: Vec::new(),
@@ -866,6 +872,7 @@ impl StackMap {
true
}
+ #[must_use]
pub fn lookup_binding(&self, name: &str) -> Option<&SynType> {
if !self.used_names.contains(name) {
return None;
@@ -899,6 +906,7 @@ pub struct FunctionCodeBuilder {
}
impl FunctionCodeBuilder {
+ #[must_use]
pub fn new() -> Self {
Self {
stack_layout: StackMap::new(),
@@ -956,6 +964,7 @@ pub struct Function<'def> {
impl<'def> Function<'def> {
/// Get the name of the function.
+ #[must_use]
pub fn name(&self) -> &str {
&self.code.name
}
@@ -1283,6 +1292,7 @@ pub struct FunctionBuilder<'def> {
}
impl<'def> FunctionBuilder<'def> {
+ #[must_use]
pub fn new(name: &str, spec_name: &str) -> Self {
let code_builder = FunctionCodeBuilder::new();
let spec_builder = FunctionSpecBuilder::new();
@@ -1344,11 +1354,13 @@ impl<'def> FunctionBuilder<'def> {
}
/// Get the type parameters.
+ #[must_use]
pub fn get_ty_params(&self) -> &[LiteralTyParam] {
&self.generic_types
}
/// Get the universal lifetimes.
+ #[must_use]
pub fn get_lfts(&self) -> Vec<(Option<String>, Lft)> {
self.generic_lifetimes.clone()
}
diff --git a/rr_frontend/radium/src/coq.rs b/rr_frontend/radium/src/coq.rs
index 00e123c8..3a16d26d 100644
--- a/rr_frontend/radium/src/coq.rs
+++ b/rr_frontend/radium/src/coq.rs
@@ -171,6 +171,7 @@ impl Display for CoqType {
impl CoqType {
/// Check if the `CoqType` contains a free variable `Var(i)`.
+ #[must_use]
pub fn is_closed(&self) -> bool {
match self {
Self::Bool
@@ -251,6 +252,7 @@ impl CoqType {
pub struct CoqParamList(pub Vec<(CoqName, CoqType)>);
impl CoqParamList {
+ #[must_use]
pub const fn empty() -> Self {
Self(vec![])
}
@@ -397,10 +399,12 @@ pub struct CoqAttributes {
attrs: Vec<CoqAttribute>,
}
impl CoqAttributes {
+ #[must_use]
pub const fn empty() -> Self {
Self { attrs: vec![] }
}
+ #[must_use]
pub fn new(attrs: Vec<CoqAttribute>) -> Self {
Self { attrs }
}
@@ -463,6 +467,7 @@ impl Display for CoqTopLevelAssertion {
pub struct CoqTopLevelAssertions(pub Vec<CoqTopLevelAssertion>);
impl CoqTopLevelAssertions {
+ #[must_use]
pub const fn empty() -> Self {
Self(vec![])
}
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index 2f45ca1f..3479a36b 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -26,18 +26,22 @@ impl<'def> Display for TypeWithRef<'def> {
}
impl<'def> TypeWithRef<'def> {
+ #[must_use]
pub const fn new(ty: Type<'def>, rfn: String) -> Self {
TypeWithRef(ty, rfn)
}
+ #[must_use]
pub fn make_unit() -> Self {
TypeWithRef(Type::Unit, "()".to_string())
}
+ #[must_use]
pub const fn ty(&self) -> &Type<'def> {
&self.0
}
+ #[must_use]
pub fn rfn(&self) -> &str {
self.1.as_str()
}
@@ -106,6 +110,7 @@ impl Display for IntType {
impl IntType {
/// Get the size in bytes of the Caesium representation.
+ #[must_use]
pub const fn size(&self) -> u32 {
match self {
Self::I8 | Self::U8 => 1,
@@ -117,6 +122,7 @@ impl IntType {
}
/// Get the alignment in bytes of the Caesium representation.
+ #[must_use]
pub const fn alignment(&self) -> u32 {
match self {
Self::I8 | Self::U8 => 1,
@@ -245,11 +251,13 @@ impl SynType {
/// Get a Coq term for the layout of this syntactic type.
/// This may call the Coq-level layout algorithm that we assume.
+ #[must_use]
pub fn layout_term_typaram(&self, env: &[Option<LiteralTyParam>]) -> Layout {
self.layout_term_core(env, |x| Self::Literal(x.syn_type.clone()))
}
/// See `layout_term_typaram`.
+ #[must_use]
pub fn layout_term(&self, env: &[Option<Self>]) -> Layout {
self.layout_term_core(env, |x| x.clone())
}
@@ -284,16 +292,19 @@ impl SynType {
/// Determine the optype used to access a value of this syntactic type.
/// Note that we may also always use `UntypedOp`, but this here computes the more specific
/// `op_type` that triggers more UB on invalid values.
+ #[must_use]
pub fn optype_typaram(&self, env: &[Option<LiteralTyParam>]) -> OpType {
self.optype_core(env, |x| Self::Literal(x.syn_type.clone()))
}
/// See `optype_typaram`.
+ #[must_use]
pub fn optype(&self, env: &[Option<Self>]) -> OpType {
self.optype_core(env, |x| x.clone())
}
/// Check if the `SynType` contains a free variable `Var(i)`.
+ #[must_use]
pub const fn is_closed(&self) -> bool {
!matches!(self, Self::Var(_))
}
@@ -328,10 +339,12 @@ pub struct TypeAnnotMeta {
}
impl TypeAnnotMeta {
+ #[must_use]
pub fn is_empty(&self) -> bool {
self.escaped_lfts.is_empty() && self.escaped_tyvars.is_empty()
}
+ #[must_use]
pub fn empty() -> Self {
Self {
escaped_lfts: HashSet::new(),
@@ -339,6 +352,7 @@ impl TypeAnnotMeta {
}
}
+ #[must_use]
pub const fn new(tyvars: HashSet<LiteralTyParam>, lfts: HashSet<Lft>) -> Self {
Self {
escaped_lfts: lfts,
@@ -381,6 +395,7 @@ pub struct LiteralTypeUse<'def> {
impl<'def> LiteralTypeUse<'def> {
/// `params` should not contain `Var`
+ #[must_use]
pub fn new(s: LiteralTypeRef<'def>, params: Vec<Type<'def>>) -> Self {
LiteralTypeUse {
def: s,
@@ -390,6 +405,7 @@ impl<'def> LiteralTypeUse<'def> {
}
/// `params` should not contain `Var`
+ #[must_use]
pub fn new_with_annot(s: LiteralTypeRef<'def>, params: Vec<Type<'def>>, annot: TypeAnnotMeta) -> Self {
LiteralTypeUse {
def: s,
@@ -412,6 +428,7 @@ impl<'def> LiteralTypeUse<'def> {
/// Get the refinement type of a struct usage.
/// This requires that all type parameters of the struct have been instantiated.
+ #[must_use]
pub fn get_rfn_type(&self) -> String {
let rfn_instantiations: Vec<String> =
self.params.iter().map(|ty| ty.get_rfn_type(&[]).to_string()).collect();
@@ -422,6 +439,7 @@ impl<'def> LiteralTypeUse<'def> {
}
/// Get the `syn_type` term for this struct use.
+ #[must_use]
pub fn generate_raw_syn_type_term(&self) -> SynType {
// first get the syntys for the type params
let mut param_sts = Vec::new();
@@ -433,6 +451,7 @@ impl<'def> LiteralTypeUse<'def> {
SynType::Literal(specialized_spec.to_string())
}
+ #[must_use]
pub fn generate_syn_type_term(&self) -> SynType {
// first get the syntys for the type params
let mut param_sts = Vec::new();
@@ -445,6 +464,7 @@ impl<'def> LiteralTypeUse<'def> {
}
/// Generate a string representation of this struct use.
+ #[must_use]
pub fn generate_type_term(&self) -> String {
let mut param_tys = Vec::new();
for p in &self.params {
@@ -469,6 +489,7 @@ pub struct LiteralTyParam {
impl LiteralTyParam {
/// Make a literal type for this type parameter and a given `st_name`.
+ #[must_use]
pub fn make_literal_type(&self) -> LiteralType {
LiteralType {
rust_name: Some(self.rust_name.clone()),
@@ -549,6 +570,7 @@ impl<'def> Type<'def> {
/// Determines the type this type is refined by.
/// `env` gives the environment for `Var(i)` constructors.
+ #[must_use]
pub fn get_rfn_type(&self, env: &[Option<CoqType>]) -> CoqType {
match self {
Self::Bool => CoqType::Bool,
@@ -595,6 +617,7 @@ impl<'def> Type<'def> {
}
/// Get the layout of a type.
+ #[must_use]
pub fn get_syn_type(&self) -> SynType {
match self {
Self::Bool => SynType::Bool,
@@ -680,6 +703,7 @@ impl<'def> Type<'def> {
}
/// Check if the Type contains a free variable `Var(i)`.
+ #[must_use]
pub fn is_closed(&self) -> bool {
match self {
Self::Var(_) => false,
@@ -742,6 +766,7 @@ pub struct TyOwnSpec {
}
impl TyOwnSpec {
+ #[must_use]
pub const fn new(
loc: String,
rfn: String,
@@ -758,10 +783,12 @@ impl TyOwnSpec {
}
}
+ #[must_use]
pub fn fmt_owned(&self, tid: &str) -> String {
format!("{} â—â‚—[{}, Owned {}] #({}) @ (â— {})", self.loc, tid, self.with_later, self.rfn, self.ty)
}
+ #[must_use]
pub fn fmt_shared(&self, tid: &str, lft: &str) -> String {
format!("{} â—â‚—[{}, Shared {}] #({}) @ (â— {})", self.loc, tid, lft, self.rfn, self.ty)
}
@@ -814,6 +841,7 @@ pub struct InvariantSpec {
}
impl InvariantSpec {
+ #[must_use]
pub fn new(
type_name: String,
flags: InvariantSpecFlags,
@@ -1143,6 +1171,7 @@ impl InvariantSpec {
out
}
+ #[must_use]
pub fn rt_def_name(&self) -> String {
format!("{}_rt", self.type_name)
}
@@ -1202,6 +1231,7 @@ impl Display for UnionRepr {
}
/// Lookup a Rust-level type parameter identifier `name` in the given type parameter environment.
+#[must_use]
pub fn lookup_ty_param<'a>(name: &'_ str, env: &'a [LiteralTyParam]) -> Option<&'a LiteralTyParam> {
env.iter().find(|&names| names.rust_name == name)
}
@@ -1234,11 +1264,13 @@ pub struct AbstractVariant<'def> {
impl<'def> AbstractVariant<'def> {
/// Get the name of this variant
+ #[must_use]
pub fn name(&self) -> &str {
&self.name
}
/// The core of generating the sls definition, without the section + context intro.
+ #[must_use]
pub fn generate_coq_sls_def_core(&self, typarams: &[String], typarams_use: &[String]) -> String {
let mut out = String::with_capacity(200);
let indent = " ";
@@ -1272,6 +1304,7 @@ impl<'def> AbstractVariant<'def> {
}
/// Generate a Coq definition for the struct layout spec.
+ #[must_use]
pub fn generate_coq_sls_def(&self, ty_params: &[LiteralTyParam]) -> String {
let mut out = String::with_capacity(200);
@@ -1295,6 +1328,7 @@ impl<'def> AbstractVariant<'def> {
out
}
+ #[must_use]
pub fn generate_coq_type_term(&self, sls_app: Vec<String>) -> String {
let mut out = String::with_capacity(200);
@@ -1305,6 +1339,7 @@ impl<'def> AbstractVariant<'def> {
out
}
+ #[must_use]
pub fn generate_coq_type_def_core(
&self,
ty_params: &[LiteralTyParam],
@@ -1354,6 +1389,7 @@ impl<'def> AbstractVariant<'def> {
/// Generate a Coq definition for the struct type alias.
/// TODO: maybe we should also generate a separate alias def for the refinement type to make
/// things more readable?
+ #[must_use]
pub fn generate_coq_type_def(&self, ty_params: &[LiteralTyParam], extra_context: &[CoqParam]) -> String {
let mut out = String::with_capacity(200);
let indent = " ";
@@ -1449,6 +1485,7 @@ pub struct AbstractStruct<'def> {
}
impl<'def> AbstractStruct<'def> {
+ #[must_use]
pub fn new(variant_def: AbstractVariant<'def>, ty_params: Vec<LiteralTyParam>) -> Self {
AbstractStruct {
invariant: None,
@@ -1458,28 +1495,34 @@ impl<'def> AbstractStruct<'def> {
}
/// Check if the struct has type parameters.
+ #[must_use]
pub fn has_type_params(&self) -> bool {
!self.ty_params.is_empty()
}
/// Get the name of this struct
+ #[must_use]
pub fn name(&self) -> &str {
self.variant_def.name()
}
+ #[must_use]
pub fn sls_def_name(&self) -> &str {
&self.variant_def.sls_def_name
}
+ #[must_use]
pub fn st_def_name(&self) -> &str {
&self.variant_def.st_def_name
}
+ #[must_use]
pub fn plain_ty_name(&self) -> &str {
&self.variant_def.plain_ty_name
}
/// 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,
@@ -1487,10 +1530,12 @@ impl<'def> AbstractStruct<'def> {
}
}
+ #[must_use]
pub fn plain_rt_def_name(&self) -> &str {
&self.variant_def.plain_rt_def_name
}
+ #[must_use]
pub fn public_rt_def_name(&self) -> String {
match self.invariant {
Some(ref inv) => inv.rt_def_name(),
@@ -1507,11 +1552,13 @@ impl<'def> AbstractStruct<'def> {
}
/// Generate a Coq definition for the struct layout spec.
+ #[must_use]
pub fn generate_coq_sls_def(&self) -> String {
self.variant_def.generate_coq_sls_def(&self.ty_params)
}
/// 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 { &[] };
@@ -1519,6 +1566,7 @@ impl<'def> AbstractStruct<'def> {
}
/// Generate an optional definition for the invariant of this type, if one has been specified.
+ #[must_use]
pub fn generate_optional_invariant_def(&self) -> Option<String> {
self.invariant.as_ref().map(|spec| {
spec.generate_coq_type_def(self.plain_ty_name(), self.plain_rt_def_name(), &self.ty_params)
@@ -1526,6 +1574,7 @@ impl<'def> AbstractStruct<'def> {
}
/// Make a literal type.
+ #[must_use]
pub fn make_literal_type(&self) -> LiteralType {
LiteralType {
rust_name: Some(self.name().to_string()),
@@ -1547,6 +1596,7 @@ pub struct VariantBuilder<'def> {
}
impl<'def> VariantBuilder<'def> {
+ #[must_use]
pub fn finish(self, ty_params: &[LiteralTyParam]) -> AbstractVariant<'def> {
let sls_def_name: String = format!("{}_sls", &self.name);
let st_def_name: String = format!("{}_st", &self.name);
@@ -1586,6 +1636,7 @@ impl<'def> VariantBuilder<'def> {
}
/// Finish building the struct type and generate an abstract struct definition.
+ #[must_use]
pub fn finish_as_struct(self, ty_params: Vec<LiteralTyParam>) -> AbstractStruct<'def> {
let variant = self.finish(&ty_params);
AbstractStruct {
@@ -1597,6 +1648,7 @@ impl<'def> VariantBuilder<'def> {
/// Initialize a struct builder.
/// `ty_params` are the user-facing type parameter names in the Rust code.
+ #[must_use]
pub fn new(name: String, repr: StructRepr) -> VariantBuilder<'def> {
VariantBuilder {
fields: Vec::new(),
@@ -1612,6 +1664,7 @@ impl<'def> VariantBuilder<'def> {
}
/// Create a struct representation of a tuple with `num_fields`, all of which are generic.
+#[must_use]
pub fn make_tuple_struct_repr<'def>(num_fields: usize) -> AbstractStruct<'def> {
let name = format!("tuple{}", num_fields);
@@ -1661,6 +1714,7 @@ impl<'def> AbstractStructUse<'def> {
}
/// Creates a new use of unit.
+ #[must_use]
pub const fn new_unit() -> Self {
AbstractStructUse {
def: None,
@@ -1670,10 +1724,12 @@ impl<'def> AbstractStructUse<'def> {
}
/// Returns true iff this is a use of unit.
+ #[must_use]
pub const fn is_unit(&self) -> bool {
self.def.is_none()
}
+ #[must_use]
pub fn is_raw(&self) -> bool {
self.raw == TypeIsRaw::Yes
}
@@ -1694,6 +1750,7 @@ impl<'def> AbstractStructUse<'def> {
/// Get the refinement type of a struct usage.
/// This requires that all type parameters of the struct have been instantiated.
+ #[must_use]
pub fn get_rfn_type(&self) -> String {
let Some(def) = self.def.as_ref() else {
return CoqType::Unit.to_string();
@@ -1719,6 +1776,7 @@ impl<'def> AbstractStructUse<'def> {
}
/// Generate a term for the `struct_layout` (of type `struct_layout`)
+ #[must_use]
pub fn generate_struct_layout_term(&self) -> String {
let Some(def) = self.def.as_ref() else {
return Layout::UnitLayout.to_string();
@@ -1737,6 +1795,7 @@ impl<'def> AbstractStructUse<'def> {
CoqAppTerm::new("use_struct_layout_alg'".to_string(), vec![specialized_spec]).to_string()
}
+ #[must_use]
pub fn generate_struct_layout_spec_term(&self) -> String {
let Some(def) = self.def.as_ref() else {
panic!("unit has no sls");
@@ -1755,6 +1814,7 @@ impl<'def> AbstractStructUse<'def> {
}
/// Get the `syn_type` term for this struct use.
+ #[must_use]
pub fn generate_syn_type_term(&self) -> SynType {
let Some(def) = self.def.as_ref() else {
return SynType::Unit;
@@ -1774,6 +1834,7 @@ impl<'def> AbstractStructUse<'def> {
}
/// Generate a string representation of this struct use.
+ #[must_use]
pub fn generate_type_term(&self) -> String {
let Some(def) = self.def.as_ref() else {
return Type::Unit.to_string();
@@ -1844,37 +1905,45 @@ pub struct AbstractEnum<'def> {
impl<'def> AbstractEnum<'def> {
/// Check whether this enum has any type parameters.
+ #[must_use]
pub fn has_type_params(&self) -> bool {
!self.ty_params.is_empty()
}
/// Get the name of this enum.
+ #[must_use]
pub fn name(&self) -> &str {
&self.name
}
+ #[must_use]
pub fn public_type_name(&self) -> &str {
&self.plain_ty_name
}
+ #[must_use]
pub fn public_rt_def_name(&self) -> &str {
&self.plain_rt_name
}
+ #[must_use]
pub fn els_def_name(&self) -> &str {
&self.els_def_name
}
+ #[must_use]
pub fn st_def_name(&self) -> &str {
&self.st_def_name
}
+ #[must_use]
pub fn get_variant(&self, i: usize) -> Option<&(String, AbstractStructRef<'def>, i128)> {
self.variants.get(i)
}
/// Generate a Coq definition for the enum layout spec, and all the `struct_layout_specs` for the
/// variants.
+ #[must_use]
pub fn generate_coq_els_def(&self) -> String {
let indent = " ";
@@ -2057,6 +2126,7 @@ impl<'def> AbstractEnum<'def> {
out
}
+ #[must_use]
pub fn generate_coq_type_def(&self) -> String {
let mut out = String::with_capacity(200);
@@ -2192,6 +2262,7 @@ impl<'def> AbstractEnum<'def> {
}
/// Make a literal type.
+ #[must_use]
pub fn make_literal_type(&self) -> LiteralType {
LiteralType {
rust_name: Some(self.name().to_string()),
@@ -2220,6 +2291,7 @@ pub struct EnumBuilder<'def> {
impl<'def> EnumBuilder<'def> {
/// Finish building the enum type and generate an abstract enum definition.
+ #[must_use]
pub fn finish(self, optional_inductive_def: Option<CoqInductive>, spec: EnumSpec) -> AbstractEnum<'def> {
let els_def_name: String = format!("{}_els", &self.name);
let st_def_name: String = format!("{}_st", &self.name);
@@ -2245,6 +2317,7 @@ impl<'def> EnumBuilder<'def> {
/// Initialize an enum builder.
/// `ty_params` are the user-facing type parameter names in the Rust code.
+ #[must_use]
pub fn new(
name: String,
ty_param_defs: Vec<LiteralTyParam>,
@@ -2298,6 +2371,7 @@ impl<'def> AbstractEnumUse<'def> {
/// Get the refinement type of an enum usage.
/// This requires that all type parameters of the enum have been instantiated.
+ #[must_use]
pub fn get_rfn_type(&self) -> CoqType {
let env = Vec::new(); // we use the empty environment per our assumption
let rfn_instantiations: Vec<CoqType> =
@@ -2311,6 +2385,7 @@ impl<'def> AbstractEnumUse<'def> {
}
/// Generate a term for the enum layout (of type `struct_layout`)
+ #[must_use]
pub fn generate_enum_layout_term(&self) -> String {
// first get the syntys for the type params
let mut param_sts = Vec::new();
@@ -2328,6 +2403,7 @@ impl<'def> AbstractEnumUse<'def> {
}
/// Generate a term for the enum layout spec (of type `enum_layout_spec`).
+ #[must_use]
pub fn generate_enum_layout_spec_term(&self) -> String {
// first get the syntys for the type params
let mut param_sts = Vec::new();
@@ -2341,6 +2417,7 @@ impl<'def> AbstractEnumUse<'def> {
}
/// Get the `syn_type` term for this enum use.
+ #[must_use]
pub fn generate_syn_type_term(&self) -> SynType {
// first get the syntys for the type params
let mut param_sts = Vec::new();
@@ -2356,6 +2433,7 @@ impl<'def> AbstractEnumUse<'def> {
}
/// Generate a string representation of this enum use.
+ #[must_use]
pub fn generate_type_term(&self) -> String {
let mut param_tys = Vec::new();
for p in &self.ty_params {
@@ -2405,6 +2483,7 @@ impl Display for Layout {
}
impl Layout {
+ #[must_use]
pub fn size(&self, env: &LayoutEnv) -> Option<u32> {
match self {
Self::UnitLayout => Some(0),
@@ -2423,6 +2502,7 @@ impl Layout {
}
}
+ #[must_use]
pub fn alignment(&self, env: &LayoutEnv) -> Option<u32> {
match self {
Self::BoolLayout | Self::UnitLayout | Self::PadLayout(_) => Some(1),
@@ -2448,6 +2528,7 @@ impl Layout {
#[derive(Clone, Eq, PartialEq, Debug)]
pub struct CoqBinder(CoqName, CoqType);
impl CoqBinder {
+ #[must_use]
pub const fn new(n: CoqName, t: CoqType) -> Self {
Self(n, t)
}
@@ -2526,6 +2607,7 @@ pub struct IPropPredicate {
}
impl IPropPredicate {
+ #[must_use]
pub fn new(binders: Vec<CoqBinder>, prop: IProp) -> Self {
Self { binders, prop }
}
@@ -2558,6 +2640,7 @@ pub struct CoqParam {
}
impl CoqParam {
+ #[must_use]
pub fn new(name: CoqName, ty: CoqType, implicit: bool) -> Self {
let depends_on_sigma = if let CoqType::Literal(ref lit) = ty { lit.contains('Σ') } else { false };
Self {
@@ -2568,6 +2651,7 @@ impl CoqParam {
}
}
+ #[must_use]
pub fn with_name(&self, name: String) -> Self {
Self::new(CoqName::Named(name), self.ty.clone(), self.implicit)
}
@@ -2662,6 +2746,7 @@ impl<'def> FunctionSpec<'def> {
out
}
+ #[must_use]
pub const fn has_spec(&self) -> bool {
self.has_spec
}
@@ -2774,6 +2859,7 @@ pub struct FunctionSpecBuilder<'def> {
}
impl<'def> FunctionSpecBuilder<'def> {
+ #[must_use]
pub fn new() -> Self {
Self {
coq_params: Vec::new(),
diff --git a/rr_frontend/rrconfig/src/launch.rs b/rr_frontend/rrconfig/src/launch.rs
index 44762aab..990cf478 100644
--- a/rr_frontend/rrconfig/src/launch.rs
+++ b/rr_frontend/rrconfig/src/launch.rs
@@ -9,6 +9,7 @@ use std::env;
use std::path::PathBuf;
use std::process::Command;
+#[must_use]
pub fn get_current_executable_dir() -> PathBuf {
env::current_exe()
.expect("current executable path invalid")
diff --git a/rr_frontend/rrconfig/src/lib.rs b/rr_frontend/rrconfig/src/lib.rs
index c8b78355..f59a9fa7 100644
--- a/rr_frontend/rrconfig/src/lib.rs
+++ b/rr_frontend/rrconfig/src/lib.rs
@@ -77,6 +77,7 @@ lazy_static! {
}
/// Generate a dump of the settings
+#[must_use]
pub fn dump() -> String {
format!("{:#?}", SETTINGS.read().unwrap())
}
@@ -121,31 +122,37 @@ fn write_setting<T: Into<config::Value>>(key: &'static str, value: T) {
.unwrap_or_else(|e| panic!("Failed to write setting {key} due to {e}"));
}
+#[must_use]
pub fn work_dir() -> String {
read_setting("work_dir")
}
+#[must_use]
pub fn absolute_work_dir() -> PathBuf {
let s = work_dir();
make_path_absolute(&s)
}
/// Should we dump debug files?
+#[must_use]
pub fn dump_debug_info() -> bool {
read_setting("dump_debug_info")
}
/// Should we dump borrowck info?
+#[must_use]
pub fn dump_borrowck_info() -> bool {
read_setting("dump_borrowck_info")
}
/// In which folder should we store log/dumps?
+#[must_use]
pub fn log_dir() -> PathBuf {
make_path_absolute(&read_setting::<String>("log_dir"))
}
/// Get the paths in which to search for `RefinedRust` library declarations.
+#[must_use]
pub fn lib_load_paths() -> Vec<PathBuf> {
let mut paths = Vec::new();
let s = read_setting::<Vec<String>>("lib_load_paths");
@@ -156,89 +163,107 @@ pub fn lib_load_paths() -> Vec<PathBuf> {
}
/// The hotword with which specification attributes should begin.
+#[must_use]
pub fn spec_hotword() -> String {
read_setting("spec_hotword")
}
/// Should we hide user messages?
+#[must_use]
pub fn quiet() -> bool {
read_setting("quiet")
}
/// Skip features that are unsupported or partially supported
+#[must_use]
pub fn skip_unsupported_features() -> bool {
read_setting("skip_unsupported_features")
}
/// Whether to generate a dune-project file for this project
+#[must_use]
pub fn generate_dune_project() -> bool {
read_setting("generate_dune_project")
}
/// Which attribute parser to use? Currently, only the "verbose" parser is supported.
+#[must_use]
pub fn attribute_parser() -> String {
read_setting("attribute_parser")
}
/// Which directory to write the generated Coq files to?
+#[must_use]
pub fn output_dir() -> Option<PathBuf> {
read_optional_setting("output_dir").map(|s: String| make_path_absolute(&s))
}
/// Whether to admit proofs of functions instead of running Qed.
+#[must_use]
pub fn admit_proofs() -> bool {
read_setting("admit_proofs")
}
/// Post-generation hook
+#[must_use]
pub fn post_generation_hook() -> Option<String> {
read_optional_setting("post_generation_hook")
}
/// Which file to read shims from?
+#[must_use]
pub fn shim_file() -> Option<PathBuf> {
read_optional_setting("shims").map(|s: String| make_path_absolute(&s))
}
/// Which file should we read extra specs from?
+#[must_use]
pub fn extra_specs_file() -> Option<PathBuf> {
read_optional_setting("extra_specs").map(|s: String| make_path_absolute(&s))
}
/// Run the proof checker after generating the Coq code?
+#[must_use]
pub fn check_proofs() -> bool {
read_setting("run_check")
}
/// Which cargo to use?
+#[must_use]
pub fn cargo_path() -> String {
read_setting("cargo_path")
}
/// Which cargo command should cargo-refinedrust hook into?
+#[must_use]
pub fn cargo_command() -> String {
read_setting("cargo_command")
}
/// Should refinedrust-rustc behave like rustc?
+#[must_use]
pub fn be_rustc() -> bool {
read_setting("be_rustc")
}
/// Should also dependencies be verified?
+#[must_use]
pub fn verify_deps() -> bool {
read_setting("verify_deps")
}
/// Should verification be skipped?
+#[must_use]
pub fn no_verify() -> bool {
read_setting("no_verify")
}
+
pub fn set_no_verify(value: bool) {
write_setting("no_verify", value);
}
/// Should we check for overflows?
+#[must_use]
pub fn check_overflows() -> bool {
read_setting("check_overflows")
}
diff --git a/rr_frontend/translation/src/environment/borrowck/facts.rs b/rr_frontend/translation/src/environment/borrowck/facts.rs
index 3d4e5f48..5c3592d5 100644
--- a/rr_frontend/translation/src/environment/borrowck/facts.rs
+++ b/rr_frontend/translation/src/environment/borrowck/facts.rs
@@ -86,10 +86,12 @@ pub struct Interner {
}
impl Interner {
+ #[must_use]
pub const fn new(location_table: LocationTable) -> Self {
Self { location_table }
}
+ #[must_use]
pub fn get_point_index(&self, point: &Point) -> PointIndex {
// self.points.get_index(point)
match point.typ {
@@ -98,6 +100,7 @@ impl Interner {
}
}
+ #[must_use]
pub fn get_point(&self, index: PointIndex) -> Point {
// self.points.get_element(index)
match self.location_table.to_location(index) {
@@ -112,6 +115,7 @@ impl Interner {
}
}
+ #[must_use]
pub fn get_location(&self, index: PointIndex) -> mir::Location {
// self.points.get_element(index)
match self.location_table.to_location(index) {
diff --git a/rr_frontend/translation/src/environment/borrowck/regions.rs b/rr_frontend/translation/src/environment/borrowck/regions.rs
index 02dda04a..a6ddc213 100644
--- a/rr_frontend/translation/src/environment/borrowck/regions.rs
+++ b/rr_frontend/translation/src/environment/borrowck/regions.rs
@@ -36,6 +36,7 @@ impl PlaceRegions {
self.0.insert((local, projections), rvid);
}
+ #[must_use]
pub fn for_local(&self, local: mir::Local) -> Option<facts::Region> {
self.for_place(local.into()).unwrap()
}
diff --git a/rr_frontend/translation/src/environment/loops.rs b/rr_frontend/translation/src/environment/loops.rs
index 1b15a25f..712b0fb1 100644
--- a/rr_frontend/translation/src/environment/loops.rs
+++ b/rr_frontend/translation/src/environment/loops.rs
@@ -359,56 +359,67 @@ impl ProcedureLoops {
}
}
+ #[must_use]
pub fn count_loop_heads(&self) -> usize {
self.loop_heads.len()
}
+ #[must_use]
pub fn max_loop_nesting(&self) -> usize {
self.loop_head_depths.values().max().copied().unwrap_or(0)
}
+ #[must_use]
pub fn is_loop_head(&self, bbi: BasicBlockIndex) -> bool {
self.loop_heads.contains(&bbi)
}
+ #[must_use]
pub fn get_loop_exit_blocks(&self, bbi: BasicBlockIndex) -> &[BasicBlockIndex] {
debug_assert!(self.is_loop_head(bbi));
&self.loop_exit_blocks[&bbi]
}
+ #[must_use]
pub fn is_conditional_branch(&self, loop_head: BasicBlockIndex, bbi: BasicBlockIndex) -> bool {
debug_assert!(self.is_loop_head(loop_head));
!self.nonconditional_loop_blocks[&loop_head].contains(&bbi)
}
+ #[must_use]
pub fn get_enclosing_loop_heads(&self, bbi: BasicBlockIndex) -> &[BasicBlockIndex] {
if let Some(heads) = self.enclosing_loop_heads.get(&bbi) { heads } else { &[] }
}
/// Get the loop head, if any
/// Note: a loop head **is** loop head of itself
+ #[must_use]
pub fn get_loop_head(&self, bbi: BasicBlockIndex) -> Option<BasicBlockIndex> {
self.enclosing_loop_heads.get(&bbi).and_then(|heads| heads.last()).copied()
}
/// Get the depth of a loop head, starting from one for a simple loop
+ #[must_use]
pub fn get_loop_head_depth(&self, bbi: BasicBlockIndex) -> usize {
debug_assert!(self.is_loop_head(bbi));
self.loop_head_depths[&bbi]
}
/// Get the loop-depth of a block (zero if it's not in a loop).
+ #[must_use]
pub fn get_loop_depth(&self, bbi: BasicBlockIndex) -> usize {
self.get_loop_head(bbi).map_or(0, |x| self.get_loop_head_depth(x))
}
/// Get the (topologically ordered) body of a loop, given a loop head
+ #[must_use]
pub fn get_loop_body(&self, loop_head: BasicBlockIndex) -> &[BasicBlockIndex] {
debug_assert!(self.is_loop_head(loop_head));
&self.ordered_loop_bodies[&loop_head]
}
/// Does this edge exit a loop?
+ #[must_use]
pub fn is_out_edge(&self, from: BasicBlockIndex, to: BasicBlockIndex) -> bool {
let Some(from_loop_head) = self.get_loop_head(from) else {
return false;
@@ -426,6 +437,7 @@ impl ProcedureLoops {
}
/// Check if ``block`` is inside a given loop.
+ #[must_use]
pub fn is_block_in_loop(&self, loop_head: BasicBlockIndex, block: BasicBlockIndex) -> bool {
self.dominators.dominates(loop_head, block)
}
diff --git a/rr_frontend/translation/src/environment/mir_analyses/initialization.rs b/rr_frontend/translation/src/environment/mir_analyses/initialization.rs
index 8573576b..19ce2004 100644
--- a/rr_frontend/translation/src/environment/mir_analyses/initialization.rs
+++ b/rr_frontend/translation/src/environment/mir_analyses/initialization.rs
@@ -36,6 +36,7 @@ pub struct AnalysisResult<T> {
impl<T> AnalysisResult<T> {
#[allow(clippy::new_without_default)]
+ #[must_use]
pub fn new() -> Self {
Self {
before_block: FxHashMap::default(),
@@ -45,6 +46,7 @@ impl<T> AnalysisResult<T> {
/// Get the initialization set before the first statement of the
/// basic block.
+ #[must_use]
pub fn get_before_block(&self, bb: mir::BasicBlock) -> &T {
self.before_block
.get(&bb)
@@ -54,6 +56,7 @@ impl<T> AnalysisResult<T> {
/// Get the initialization set after the statement.
/// If `location.statement_index` is equal to the number of statements,
/// returns the initialization set after the terminator.
+ #[must_use]
pub fn get_after_statement(&self, location: mir::Location) -> &T {
self.after_statement
.get(&location)
diff --git a/rr_frontend/translation/src/environment/mir_sets/local_set.rs b/rr_frontend/translation/src/environment/mir_sets/local_set.rs
index 90c57dd0..b2c0cb57 100644
--- a/rr_frontend/translation/src/environment/mir_sets/local_set.rs
+++ b/rr_frontend/translation/src/environment/mir_sets/local_set.rs
@@ -18,10 +18,12 @@ pub struct LocalSet {
}
impl LocalSet {
+ #[must_use]
pub fn new() -> Self {
Self::default()
}
+ #[must_use]
pub fn contains_prefix_of(&self, place: mir::Place) -> bool {
self.locals.contains(&place.local)
}
diff --git a/rr_frontend/translation/src/environment/mir_sets/place_set.rs b/rr_frontend/translation/src/environment/mir_sets/place_set.rs
index 9520711f..651469b0 100644
--- a/rr_frontend/translation/src/environment/mir_sets/place_set.rs
+++ b/rr_frontend/translation/src/environment/mir_sets/place_set.rs
@@ -21,14 +21,17 @@ pub struct PlaceSet<'tcx> {
}
impl<'tcx> PlaceSet<'tcx> {
+ #[must_use]
pub fn new() -> Self {
Self::default()
}
+ #[must_use]
pub fn contains(&self, place: mir::Place<'tcx>) -> bool {
self.places.contains(&place)
}
+ #[must_use]
pub fn contains_prefix_of(&self, place: mir::Place<'tcx>) -> bool {
self.places.iter().any(|potential_prefix| is_prefix(&place, potential_prefix))
}
@@ -133,6 +136,7 @@ impl<'tcx> PlaceSet<'tcx> {
}
/// Compute the intersection of the two place sets.
+ #[must_use]
pub fn merge(place_set1: &PlaceSet<'tcx>, place_set2: &PlaceSet<'tcx>) -> PlaceSet<'tcx> {
place_set1.check_invariant();
place_set2.check_invariant();
@@ -185,6 +189,7 @@ impl<'tcx> PlaceSet<'tcx> {
///
/// Note that this function may break the invariant that we never
/// have a place and its descendants in the set.
+ #[must_use]
pub fn union(place_set1: &PlaceSet<'tcx>, place_set2: &PlaceSet<'tcx>) -> PlaceSet<'tcx> {
let mut places = place_set1.places.clone();
places.extend(place_set2.iter().copied());
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 fc6b6c21..39eb9929 100644
--- a/rr_frontend/translation/src/environment/mir_utils/real_edges.rs
+++ b/rr_frontend/translation/src/environment/mir_utils/real_edges.rs
@@ -32,10 +32,12 @@ impl RealEdges {
}
}
+ #[must_use]
pub fn successors(&self, bb: mir::BasicBlock) -> &[mir::BasicBlock] {
&self.successors[bb]
}
+ #[must_use]
pub fn predecessors(&self, bb: mir::BasicBlock) -> &[mir::BasicBlock] {
&self.predecessors[bb]
}
diff --git a/rr_frontend/translation/src/environment/mod.rs b/rr_frontend/translation/src/environment/mod.rs
index 88c8618c..da670769 100644
--- a/rr_frontend/translation/src/environment/mod.rs
+++ b/rr_frontend/translation/src/environment/mod.rs
@@ -58,6 +58,7 @@ pub struct Environment<'tcx> {
impl<'tcx> Environment<'tcx> {
/// Builds an environment given a compiler state.
+ #[must_use]
pub fn new(tcx: TyCtxt<'tcx>) -> Self {
Environment {
tcx,
diff --git a/rr_frontend/translation/src/environment/polonius_info.rs b/rr_frontend/translation/src/environment/polonius_info.rs
index f6e94f25..69dc3d28 100644
--- a/rr_frontend/translation/src/environment/polonius_info.rs
+++ b/rr_frontend/translation/src/environment/polonius_info.rs
@@ -55,22 +55,27 @@ pub enum AtomicRegion {
}
impl AtomicRegion {
+ #[must_use]
pub const fn is_loan(&self) -> bool {
matches!(*self, Self::Loan(_, _))
}
+ #[must_use]
pub const fn is_universal(&self) -> bool {
matches!(*self, Self::Universal(_, _))
}
+ #[must_use]
pub const fn is_place(&self) -> bool {
matches!(*self, Self::PlaceRegion(_))
}
+ #[must_use]
pub const fn is_value(&self) -> bool {
matches!(*self, Self::Unknown(_))
}
+ #[must_use]
pub const fn get_region(&self) -> facts::Region {
match self {
Self::Loan(_, r) | Self::Universal(_, r) | Self::PlaceRegion(r) | Self::Unknown(r) => *r,
@@ -273,6 +278,7 @@ pub fn graphviz<'tcx>(
}
/// Compute the transitive closure of a vec of constraints between regions.
+#[must_use]
pub fn compute_transitive_closure(
constraints: Vec<(facts::Region, facts::Region)>,
) -> Vec<(facts::Region, facts::Region)> {
@@ -590,6 +596,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
*/
/// Gets the kind of a region: originating from a loan, a universal region, or none of these.
+ #[must_use]
pub fn get_region_kind(&self, region: facts::Region) -> RegionKind {
// check if this region is induced by a loan
let v: Vec<facts::Loan> = self
@@ -639,6 +646,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
if found_region { RegionKind::PlaceRegion } else { RegionKind::Unknown }
}
+ #[must_use]
pub fn mk_atomic_region(&self, r: facts::Region) -> AtomicRegion {
let kind = self.get_region_kind(r);
match kind {
@@ -650,6 +658,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
}
/// Enumerate local universal regions (excluding the function lifetime).
+ #[must_use]
pub fn enumerate_local_universal_regions(&self) -> Vec<facts::Region> {
let mut universals = Vec::new();
for (r, _) in &self.borrowck_in_facts.placeholder {
@@ -668,6 +677,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
}
/// Get new subset constraints generated at a point.
+ #[must_use]
pub fn get_new_subset_constraints_at_point(
&self,
point: facts::PointIndex,
@@ -682,6 +692,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
}
/// `r` is the region induced by the loan `l`.
+ #[must_use]
pub fn get_outliving_atomic_regions_for_loan(
&self,
r: facts::Region,
@@ -736,6 +747,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
}
/// Get regions outliving `r` at point `loc`.
+ #[must_use]
pub fn get_outliving_atomic_regions(
&self,
r: facts::Region,
@@ -781,6 +793,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
}
/// Flips the `subset` relation computed by Polonius for each point.
+ #[must_use]
pub fn compute_superset(
output: &facts::AllOutputFacts,
) -> HashMap<facts::PointIndex, BTreeMap<facts::Region, BTreeSet<facts::Region>>> {
@@ -803,6 +816,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
superset
}
+ #[must_use]
pub fn get_point(&self, location: mir::Location, point_type: facts::PointType) -> facts::PointIndex {
let point = facts::Point {
location,
@@ -811,6 +825,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
self.interner.get_point_index(&point)
}
+ #[must_use]
pub fn get_all_loans_kept_alive_by(
&self,
point: facts::PointIndex,
@@ -850,12 +865,14 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
}
/// Get the atomic region corresponding to a loan.
+ #[must_use]
pub fn atomic_region_of_loan(&self, l: facts::Loan) -> AtomicRegion {
let r = self.get_loan_issued_at_for_loan(l);
AtomicRegion::Loan(l, r)
}
/// Get loans including the zombies ``(all_loans, zombie_loans)``.
+ #[must_use]
pub fn get_all_active_loans(&self, location: mir::Location) -> (Vec<facts::Loan>, Vec<facts::Loan>) {
let mut loans = self.get_active_loans(location, false);
let zombie_loans = self.get_active_loans(location, true);
@@ -872,6 +889,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
}
/// Get loans that are active (including those that are about to die) at the given location.
+ #[must_use]
pub fn get_active_loans(&self, location: mir::Location, zombie: bool) -> Vec<facts::Loan> {
let loan_live_at = self.get_borrow_live_at(zombie);
let start_point = self.get_point(location, facts::PointType::Start);
@@ -906,6 +924,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
}
/// Get loans including the zombies ``(all_loans, zombie_loans)``.
+ #[must_use]
pub fn get_all_loans_dying_at(&self, location: mir::Location) -> (Vec<facts::Loan>, Vec<facts::Loan>) {
let mut loans = self.get_loans_dying_at(location, false);
let zombie_loans = self.get_loans_dying_at(location, true);
@@ -914,6 +933,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
}
/// Get loans including the zombies ``(all_loans, zombie_loans)``.
+ #[must_use]
pub fn get_all_loans_dying_between(
&self,
initial_loc: mir::Location,
@@ -936,6 +956,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
}
/// Get loans that die *at* (that is, exactly after) the given location.
+ #[must_use]
pub fn get_loans_dying_at(&self, location: mir::Location, zombie: bool) -> Vec<facts::Loan> {
// TODO: this needs to change.
// the problem is that we check explcitly that it is currently live, but not at the next
@@ -973,6 +994,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
}
/// Get loans that die between two consecutive locations.
+ #[must_use]
pub fn get_loans_dying_between(
&self,
initial_loc: mir::Location,
@@ -1034,6 +1056,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
// d.into_iter().collect()) .unwrap_or(vec![])
// }
+ #[must_use]
pub fn get_conflicting_loans(&self, loan: facts::Loan) -> Vec<facts::Loan> {
self.loan_conflict_sets
.get(&loan)
@@ -1041,6 +1064,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
.unwrap_or_default()
}
+ #[must_use]
pub fn get_alive_conflicting_loans(
&self,
loan: facts::Loan,
@@ -1063,18 +1087,21 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
}
/// Get the location at which a loan is created, if possible
+ #[must_use]
pub fn get_loan_location(&self, loan: &facts::Loan) -> Option<mir::Location> {
self.loan_position.get(loan).copied()
}
/// Get the loan that gets created at a location.
/// TODO: for aggregates, this only finds one loan
+ #[must_use]
pub fn get_loan_at_location(&self, location: mir::Location) -> facts::Loan {
self.loan_at_position[&location]
}
/// Get the loan that gets created at a location.
/// TODO: for aggregates, this only finds one loan
+ #[must_use]
pub fn get_optional_loan_at_location(&self, location: mir::Location) -> Option<facts::Loan> {
if self.loan_at_position.contains_key(&location) {
Some(self.loan_at_position[&location])
@@ -1084,6 +1111,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
}
/// Get a map from loans to locations at which they were created.
+ #[must_use]
pub fn loan_locations(&self) -> HashMap<facts::Loan, mir::Location> {
self.loan_position.iter().map(|(loan, location)| (*loan, *location)).collect()
}
@@ -1215,6 +1243,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
}
/// Find a variable that has the given region in its type.
+ #[must_use]
pub const fn find_variable(&self, _region: facts::Region) -> Option<mir::Local> {
// TODO
None
@@ -1597,6 +1626,7 @@ impl AdditionalFacts {
}
/// Derive additional facts from the borrow checker facts.
+ #[must_use]
pub fn new(all_facts: &facts::AllInputFacts, output: &facts::AllOutputFacts) -> Self {
let (zombie_requires, zombie_borrow_live_at, borrow_become_zombie_at) =
Self::derive_zombie_requires(all_facts, output);
diff --git a/rr_frontend/translation/src/environment/procedure.rs b/rr_frontend/translation/src/environment/procedure.rs
index 3ab9916a..daebdfd0 100644
--- a/rr_frontend/translation/src/environment/procedure.rs
+++ b/rr_frontend/translation/src/environment/procedure.rs
@@ -70,11 +70,13 @@ impl<'tcx> Procedure<'tcx> {
}
}
+ #[must_use]
pub const fn loop_info(&self) -> &loops::ProcedureLoops {
&self.loop_info
}
/// Returns all the types used in the procedure, and any types reachable from them
+ #[must_use]
pub fn get_declared_types(&self) -> Vec<Ty<'tcx>> {
let _types: HashSet<Ty> = HashSet::new();
// for var in &self.mir.local_decls {
@@ -90,26 +92,31 @@ impl<'tcx> Procedure<'tcx> {
}
/// Get definition ID of the procedure.
+ #[must_use]
pub const fn get_id(&self) -> ProcedureDefId {
self.proc_def_id
}
/// Get the MIR of the procedure
+ #[must_use]
pub fn get_mir(&self) -> &Mir<'tcx> {
&self.mir
}
/// Get the typing context.
+ #[must_use]
pub const fn get_tcx(&self) -> TyCtxt<'tcx> {
self.tcx
}
/// Get the type parameters of this procedure.
+ #[must_use]
pub const fn get_type_params(&self) -> ty::GenericArgsRef<'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();
@@ -128,21 +135,25 @@ impl<'tcx> Procedure<'tcx> {
// }
/// 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()
}
/// 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()
@@ -168,10 +179,12 @@ impl<'tcx> Procedure<'tcx> {
*/
/// Check whether the block is reachable
+ #[must_use]
pub fn is_reachable_block(&self, bbi: BasicBlockIndex) -> bool {
self.reachable_basic_blocks.contains(&bbi)
}
+ #[must_use]
pub fn is_panic_block(&self, bbi: BasicBlockIndex) -> bool {
if let TerminatorKind::Call {
args: ref _args,
@@ -199,11 +212,13 @@ impl<'tcx> Procedure<'tcx> {
}
/// Get the successors of a basic block.
+ #[must_use]
pub fn successors(&self, bbi: mir::BasicBlock) -> &[mir::BasicBlock] {
self.real_edges.successors(bbi)
}
/// Get the predecessors of a basic block.
+ #[must_use]
pub fn predecessors(&self, bbi: mir::BasicBlock) -> &[mir::BasicBlock] {
self.real_edges.predecessors(bbi)
}
--
GitLab