diff --git a/rr_frontend/.cargo/config.toml b/rr_frontend/.cargo/config.toml
index d7d455b49b5e8c4789f1b61f3af473c3f5b8878c..dcd72fea21d1534d5b73eda86ef8d2d596c7b2c8 100644
--- a/rr_frontend/.cargo/config.toml
+++ b/rr_frontend/.cargo/config.toml
@@ -29,7 +29,6 @@ rustflags = [
# clippy::nursery
"-Aclippy::empty_line_after_doc_comments",
"-Aclippy::option_if_let_else",
- "-Aclippy::redundant_clone",
"-Aclippy::redundant_pub_crate",
"-Aclippy::string_lit_as_bytes",
"-Aclippy::type_repetition_in_bounds",
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index f2870503366291b4cd88f2c416398013969d0337..a63c458ac8fa29a6ddcbd251e2f739f2d021541d 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -1535,7 +1535,7 @@ impl<'def> AbstractStruct<'def> {
pub fn public_rt_def_name(&self) -> String {
match self.invariant {
- Some(ref inv) => inv.rt_def_name().to_string(),
+ Some(ref inv) => inv.rt_def_name(),
None => self.plain_rt_def_name().to_string(),
}
}
@@ -1795,9 +1795,7 @@ impl<'def> AbstractStructUse<'def> {
// TODO generates too many apps
// use_struct_layout_alg' ([my_spec] [params])
- let specialized_spec =
- format!("({})", CoqAppTerm::new(def.borrow().as_ref().unwrap().sls_def_name(), param_sts));
- specialized_spec.to_string()
+ format!("({})", CoqAppTerm::new(def.borrow().as_ref().unwrap().sls_def_name(), param_sts))
} else {
panic!("unit has no sls");
}
@@ -2408,11 +2406,7 @@ impl<'def> AbstractEnumUse<'def> {
}
// use_struct_layout_alg' ([my_spec] [params])
- let specialized_spec = format!(
- "({})",
- CoqAppTerm::new(self.def.borrow().as_ref().unwrap().els_def_name.clone(), param_sts)
- );
- specialized_spec.to_string()
+ format!("({})", CoqAppTerm::new(self.def.borrow().as_ref().unwrap().els_def_name.clone(), param_sts))
}
/// Get the syn_type term for this enum use.
diff --git a/rr_frontend/translation/src/function_body.rs b/rr_frontend/translation/src/function_body.rs
index f3816d9b20275704bacd1372a44e0ed760b75f5c..884784ea08507a57c8e799e3d09c4e77bf6635c6 100644
--- a/rr_frontend/translation/src/function_body.rs
+++ b/rr_frontend/translation/src/function_body.rs
@@ -3009,6 +3009,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
let translated_op = self.translate_operand(op, true)?;
Ok(translated_op)
},
+
Rvalue::Ref(region, bk, pl) => {
let translated_pl = self.translate_place(pl)?;
let translated_bk = self.translate_borrow_kind(bk)?;
@@ -3033,9 +3034,9 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
ty: ty_annot,
e: Box::new(translated_pl),
})
- //Err(TranslationError::LoanNotFound(loc))
}
},
+
Rvalue::AddressOf(mt, pl) => {
let translated_pl = self.translate_place(pl)?;
let translated_mt = self.translate_mutability(mt)?;
@@ -3044,6 +3045,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
e: Box::new(translated_pl),
})
},
+
Rvalue::BinaryOp(op, operands) => {
let e1 = &operands.as_ref().0;
let e2 = &operands.as_ref().1;
@@ -3067,6 +3069,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
e2: Box::new(translated_e2),
})
},
+
Rvalue::CheckedBinaryOp(op, operands) => {
let e1 = &operands.as_ref().0;
let e2 = &operands.as_ref().1;
@@ -3090,6 +3093,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
e2: Box::new(translated_e2),
})
},
+
Rvalue::UnaryOp(op, operand) => {
let translated_e1 = self.translate_operand(operand, true)?;
let e1_ty = self.get_type_of_operand(operand)?;
@@ -3102,12 +3106,14 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
e: Box::new(translated_e1),
})
},
+
Rvalue::NullaryOp(op, _ty) => {
// TODO: SizeOf
Err(TranslationError::UnsupportedFeature {
description: "nullary ops (AlignOf, Sizeof) are not supported currently".to_string(),
})
},
+
Rvalue::Discriminant(pl) => {
let ty = self.get_type_of_place(pl)?;
let translated_pl = self.translate_place(pl)?;
@@ -3141,11 +3147,11 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
description: format!(
"We do not support discriminant accesses on non-enum types: {:?}; got type {:?}",
rval, ty.ty
- )
- .to_string(),
+ ),
})
}
},
+
Rvalue::Aggregate(kind, op) => {
// translate operands
let mut translated_ops: Vec<radium::Expr> = Vec::new();
@@ -3235,8 +3241,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
description: format!(
"TODO: implement Aggregate rvalue for other adts: {:?}",
rval
- )
- .to_string(),
+ ),
});
}
},
@@ -3264,20 +3269,21 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
_ => {
// TODO
Err(TranslationError::UnsupportedFeature {
- description: format!("TODO: implement Aggregate rvalue: {:?}", rval).to_string(),
+ description: format!("TODO: implement Aggregate rvalue: {:?}", rval),
})
},
}
},
+
Rvalue::Cast(kind, op, ty) => {
let op_ty = self.get_type_of_operand(op)?;
let translated_op = self.translate_operand(op, true)?;
match kind {
mir::CastKind::PointerExposeAddress => Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported rvalue: {:?}", rval).to_string(),
+ description: format!("unsupported rvalue: {:?}", rval),
}),
mir::CastKind::PointerFromExposedAddress => Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported rvalue: {:?}", rval).to_string(),
+ description: format!("unsupported rvalue: {:?}", rval),
}),
mir::CastKind::PointerCoercion(x) => {
match x {
@@ -3287,48 +3293,48 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
},
ty::adjustment::PointerCoercion::ArrayToPointer => {
Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported rvalue: {:?}", rval).to_string(),
+ description: format!("unsupported rvalue: {:?}", rval),
})
},
ty::adjustment::PointerCoercion::ClosureFnPointer(_) => {
Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported rvalue: {:?}", rval).to_string(),
+ description: format!("unsupported rvalue: {:?}", rval),
})
},
ty::adjustment::PointerCoercion::ReifyFnPointer => {
Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported rvalue: {:?}", rval).to_string(),
+ description: format!("unsupported rvalue: {:?}", rval),
})
},
ty::adjustment::PointerCoercion::UnsafeFnPointer => {
Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported rvalue: {:?}", rval).to_string(),
+ description: format!("unsupported rvalue: {:?}", rval),
})
},
ty::adjustment::PointerCoercion::Unsize => {
Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported rvalue: {:?}", rval).to_string(),
+ description: format!("unsupported rvalue: {:?}", rval),
})
},
}
},
mir::CastKind::DynStar => Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported dyn* cast").to_string(),
+ description: format!("unsupported dyn* cast"),
}),
mir::CastKind::IntToInt => {
// TODO
Err(TranslationError::Unimplemented {
- description: format!("unsupported int-to-int cast").to_string(),
+ description: format!("unsupported int-to-int cast"),
})
},
mir::CastKind::IntToFloat => Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported int-to-float cast").to_string(),
+ description: format!("unsupported int-to-float cast"),
}),
mir::CastKind::FloatToInt => Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported float-to-int cast").to_string(),
+ description: format!("unsupported float-to-int cast"),
}),
mir::CastKind::FloatToFloat => Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported float-to-float cast").to_string(),
+ description: format!("unsupported float-to-float cast"),
}),
mir::CastKind::PtrToPtr => {
match (op_ty.kind(), ty.kind()) {
@@ -3339,34 +3345,38 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
_ => {
// TODO: any other cases we should handle?
Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported ptr-to-ptr cast: {:?}", rval)
- .to_string(),
+ description: format!("unsupported ptr-to-ptr cast: {:?}", rval),
})
},
}
},
mir::CastKind::FnPtrToPtr => Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported fnptr-to-ptr cast: {:?}", rval).to_string(),
+ description: format!("unsupported fnptr-to-ptr cast: {:?}", rval),
}),
mir::CastKind::Transmute => Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported transmute cast: {:?}", rval).to_string(),
+ description: format!("unsupported transmute cast: {:?}", rval),
}),
}
},
+
Rvalue::Len(..) => Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported rvalue: {:?}", rval).to_string(),
+ description: format!("unsupported rvalue: {:?}", rval),
}),
+
Rvalue::Repeat(..) => Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported rvalue: {:?}", rval).to_string(),
+ description: format!("unsupported rvalue: {:?}", rval),
}),
+
Rvalue::ThreadLocalRef(..) => Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported rvalue: {:?}", rval).to_string(),
+ description: format!("unsupported rvalue: {:?}", rval),
}),
+
Rvalue::ShallowInitBox(_, _) => Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported rvalue: {:?}", rval).to_string(),
+ description: format!("unsupported rvalue: {:?}", rval),
}),
+
Rvalue::CopyForDeref(_) => Err(TranslationError::UnsupportedFeature {
- description: format!("unsupported rvalue: {:?}", rval).to_string(),
+ description: format!("unsupported rvalue: {:?}", rval),
}),
}
}
@@ -3491,71 +3501,45 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
}
/// Translate a scalar at a specific type to a radium::Expr.
+ // TODO: Use `TryFrom` instead
fn translate_scalar(&mut self, sc: &Scalar, ty: Ty<'tcx>) -> Result<radium::Expr, TranslationError> {
+ // TODO: Use `TryFrom` instead
+ fn translate_literal<T, U>(
+ sc: Result<T, U>,
+ fptr: fn(T) -> radium::Literal,
+ ) -> Result<radium::Expr, TranslationError> {
+ sc.map_or(Err(TranslationError::InvalidLayout), |lit| Ok(radium::Expr::Literal(fptr(lit))))
+ }
+
match ty.kind() {
TyKind::Int(it) => {
match it {
- ty::IntTy::I8 => sc.to_i8().map_or_else(
- |_| Err(TranslationError::InvalidLayout),
- |i| Ok(radium::Expr::Literal(radium::Literal::LitI8(i))),
- ),
- ty::IntTy::I16 => sc.to_i16().map_or_else(
- |_| Err(TranslationError::InvalidLayout),
- |i| Ok(radium::Expr::Literal(radium::Literal::LitI16(i))),
- ),
- ty::IntTy::I32 => sc.to_i32().map_or_else(
- |_| Err(TranslationError::InvalidLayout),
- |i| Ok(radium::Expr::Literal(radium::Literal::LitI32(i))),
- ),
- ty::IntTy::I64 => sc.to_i64().map_or_else(
- |_| Err(TranslationError::InvalidLayout),
- |i| Ok(radium::Expr::Literal(radium::Literal::LitI64(i))),
- ),
- ty::IntTy::I128 => sc.to_i128().map_or_else(
- |_| Err(TranslationError::InvalidLayout),
- |i| Ok(radium::Expr::Literal(radium::Literal::LitI128(i))),
- ),
+ ty::IntTy::I8 => translate_literal(sc.to_i8(), radium::Literal::LitI8),
+ ty::IntTy::I16 => translate_literal(sc.to_i16(), radium::Literal::LitI16),
+ ty::IntTy::I32 => translate_literal(sc.to_i32(), radium::Literal::LitI32),
+ ty::IntTy::I64 => translate_literal(sc.to_i64(), radium::Literal::LitI64),
+ ty::IntTy::I128 => translate_literal(sc.to_i128(), radium::Literal::LitI128),
// for radium, the pointer size is 8 bytes
- ty::IntTy::Isize => sc.to_i64().map_or_else(
- |_| Err(TranslationError::InvalidLayout),
- |i| Ok(radium::Expr::Literal(radium::Literal::LitI64(i))),
- ),
+ ty::IntTy::Isize => translate_literal(sc.to_i64(), radium::Literal::LitI64),
}
},
+
TyKind::Uint(it) => {
match it {
- ty::UintTy::U8 => sc.to_u8().map_or_else(
- |_| Err(TranslationError::InvalidLayout),
- |i| Ok(radium::Expr::Literal(radium::Literal::LitU8(i))),
- ),
- ty::UintTy::U16 => sc.to_u16().map_or_else(
- |_| Err(TranslationError::InvalidLayout),
- |i| Ok(radium::Expr::Literal(radium::Literal::LitU16(i))),
- ),
- ty::UintTy::U32 => sc.to_u32().map_or_else(
- |_| Err(TranslationError::InvalidLayout),
- |i| Ok(radium::Expr::Literal(radium::Literal::LitU32(i))),
- ),
- ty::UintTy::U64 => sc.to_u64().map_or_else(
- |_| Err(TranslationError::InvalidLayout),
- |i| Ok(radium::Expr::Literal(radium::Literal::LitU64(i))),
- ),
- ty::UintTy::U128 => sc.to_u128().map_or_else(
- |_| Err(TranslationError::InvalidLayout),
- |i| Ok(radium::Expr::Literal(radium::Literal::LitU128(i))),
- ),
+ ty::UintTy::U8 => translate_literal(sc.to_u8(), radium::Literal::LitU8),
+ ty::UintTy::U16 => translate_literal(sc.to_u16(), radium::Literal::LitU16),
+ ty::UintTy::U32 => translate_literal(sc.to_u32(), radium::Literal::LitU32),
+ ty::UintTy::U64 => translate_literal(sc.to_u64(), radium::Literal::LitU64),
+ ty::UintTy::U128 => translate_literal(sc.to_u128(), radium::Literal::LitU128),
// for radium, the pointer size is 8 bytes
- ty::UintTy::Usize => sc.to_u64().map_or_else(
- |_| Err(TranslationError::InvalidLayout),
- |i| Ok(radium::Expr::Literal(radium::Literal::LitU64(i))),
- ),
+ ty::UintTy::Usize => translate_literal(sc.to_u64(), radium::Literal::LitU64),
}
},
- TyKind::Bool => sc.to_bool().map_or_else(
- |_| Err(TranslationError::InvalidLayout),
- |b| Ok(radium::Expr::Literal(radium::Literal::LitBool(b))),
- ),
+
+ TyKind::Bool => translate_literal(sc.to_bool(), radium::Literal::LitBool),
+
TyKind::FnDef(_, _) => self.translate_fn_def_use(ty),
+
TyKind::Tuple(tys) => {
if tys.is_empty() {
Ok(radium::Expr::Literal(radium::Literal::LitZST))
@@ -3568,6 +3552,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
})
}
},
+
TyKind::Ref(_, _, _) => match sc {
Scalar::Int(_) => {
unreachable!();
@@ -3600,6 +3585,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
}
},
},
+
_ => Err(TranslationError::UnsupportedFeature {
description: format!("Unsupported layout for const value: {:?}", ty),
}),
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index 7d24a50328fe260530de103e4abea9f3a9fe9303..f2ba35870876e90a67b5884b6bf46df8e8429161 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -250,7 +250,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
path: interned_path,
refinement_type: lit.refinement_type.to_string(),
syn_type: lit.syn_type.to_string(),
- sem_type: lit.type_term.to_string(),
+ sem_type: lit.type_term,
};
return Some(a);
},
@@ -624,14 +624,11 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
let stem = crate_name.as_str();
// create output directory
- let output_dir_path: std::path::PathBuf = if let Some(output) = rrconfig::output_dir() {
- output
- } else {
+ let Some(mut base_dir_path) = rrconfig::output_dir() else {
info!("No output directory specified, not writing files");
return;
};
- let mut base_dir_path = output_dir_path.clone();
base_dir_path.push(&stem);
if let Err(_) = fs::read_dir(base_dir_path.as_path()) {
diff --git a/rr_frontend/translation/src/spec_parsers/parse_utils.rs b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
index f0e718a9e061bc7005eff3fbf94072cafeb32831..6cf05898a96d898272ee7a2eb1b1f73e676970f9 100644
--- a/rr_frontend/translation/src/spec_parsers/parse_utils.rs
+++ b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
@@ -197,13 +197,13 @@ impl<U> Parse<U> for CoqPath {
let module = module.value();
Ok(CoqPath(specs::CoqPath {
- path: Some(path_or_module.to_string()),
+ path: Some(path_or_module),
module,
}))
} else {
Ok(CoqPath(specs::CoqPath {
path: None,
- module: path_or_module.to_string(),
+ module: path_or_module,
}))
}
}
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 ff91f3909f7664079240eeda0d48698b0ddb01bb..d9f6c91bee1a1a25ee0e16b29aafed12fa37ea63 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
@@ -163,7 +163,7 @@ impl<'a> parse::Parse<ParseMeta<'a>> for MetaIProp {
let term: parse::LitStr = input.parse(meta)?;
let (term, _meta) = process_coq_literal(&term.value(), *meta);
- Ok(MetaIProp::Observe(gname.value().to_string(), term))
+ Ok(MetaIProp::Observe(gname.value(), term))
},
"linktime" => {
let term: parse::LitStr = input.parse(meta)?;
@@ -343,7 +343,7 @@ where
let term: parse::LitStr = buffer.parse(&meta)?;
let (term, _) = process_coq_literal(&term.value(), meta);
- Ok(MetaIProp::Observe(gname.value().to_string(), term))
+ Ok(MetaIProp::Observe(gname.value(), term))
};
let m = m().map_err(str_err)?;
builder.spec.add_postcondition(m.into())?;
diff --git a/rr_frontend/translation/src/type_translator.rs b/rr_frontend/translation/src/type_translator.rs
index 48bac227707642edb3b113a95f6af10cb235e275..2445414ead7dcf3a9cebbdf775cf9fa3cbe651e9 100644
--- a/rr_frontend/translation/src/type_translator.rs
+++ b/rr_frontend/translation/src/type_translator.rs
@@ -732,7 +732,7 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
let struct_name = strip_coq_ident(&ty.ident(tcx).to_string());
self.variant_registry
.borrow_mut()
- .insert(ty.def_id, (struct_name.clone(), &*struct_def_init, ty, false, None));
+ .insert(ty.def_id, (struct_name, &*struct_def_init, ty, false, None));
let translate_adt = || {
let struct_name = strip_coq_ident(&ty.ident(tcx).to_string());