diff --git a/rr_frontend/attribute_parse/src/parse.rs b/rr_frontend/attribute_parse/src/parse.rs
index da1ce9b1ed8084c43fbfd9598ca2bcffb4bd9f3e..20f0991f1d33632e46d3d6d5a9a82a58f104c368 100644
--- a/rr_frontend/attribute_parse/src/parse.rs
+++ b/rr_frontend/attribute_parse/src/parse.rs
@@ -512,23 +512,23 @@ where
U: ?Sized,
{
fn parse(input: ParseStream, _: &U) -> ParseResult<Self> {
- let lit = input.expect_literal()?;
- match lit.0.kind {
+ let (lit, span) = input.expect_literal()?;
+ match lit.kind {
LitKind::Integer => {
- let sym = lit.0.symbol;
+ let sym = lit.symbol;
let Some((digits, suffix)) = value::parse_lit_int(&sym.to_string()) else {
- panic!("Not an integer literal: {}", sym);
+ return Err(ParseError::OtherErr(span, format!("Not an integer literal: {}", sym)));
};
Ok(Self {
- span: lit.1,
- sym: lit.0.symbol,
+ span,
+ sym: lit.symbol,
digits,
suffix,
})
},
- _ => Err(ParseError::UnexpectedLitKind(LitKind::Integer, lit.0.kind)),
+ _ => Err(ParseError::UnexpectedLitKind(LitKind::Integer, lit.kind)),
}
}
}
diff --git a/rr_frontend/radium/src/code.rs b/rr_frontend/radium/src/code.rs
index 1f5c4fc4f904644db5b45445193f929df1274436..2830ce106def0a09cb5d47688ace43254255c5b6 100644
--- a/rr_frontend/radium/src/code.rs
+++ b/rr_frontend/radium/src/code.rs
@@ -685,10 +685,6 @@ impl Display for FunctionCode {
)
}
- if self.basic_blocks.is_empty() {
- panic!("Function has no basic block");
- }
-
let params = display_list!(&self.required_parameters, " ", fmt_params);
let args = display_list!(&self.stack_layout.args, ";\n", fmt_variable);
let locals = display_list!(&self.stack_layout.locals, ";\n", fmt_variable);
diff --git a/rr_frontend/radium/src/coq.rs b/rr_frontend/radium/src/coq.rs
index f12e4d7eb88b7f3bb5b1a91a9d3e458cb7cb5adc..b48e26e8d125cb3a6da0e511ec8831803bc1dd48 100644
--- a/rr_frontend/radium/src/coq.rs
+++ b/rr_frontend/radium/src/coq.rs
@@ -127,7 +127,9 @@ fn fmt_modules(f: &mut fmt::Formatter<'_>, modules: &[&Module], kind: &str) -> f
for path in get_modules_path(modules) {
let modules: Vec<_> = modules.iter().filter_map(|x| is(x, Some(&path))).collect();
- assert!(!modules.is_empty());
+ if modules.is_empty() {
+ unreachable!("get_modules_path() gave the path {path} but no modules matched it.");
+ }
writeln!(f, "From {} Require {} {}.", path, kind, modules.join(" "))?;
}
diff --git a/rr_frontend/translation/src/function_body.rs b/rr_frontend/translation/src/function_body.rs
index ce21a7b859d7b1cf4a3ccde562421184ce08108b..f52cd8a3fe964044454049fb4b4c8ff94d20183a 100644
--- a/rr_frontend/translation/src/function_body.rs
+++ b/rr_frontend/translation/src/function_body.rs
@@ -1608,58 +1608,53 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
/// generics.
fn call_expr_op_split_inst(
&self,
- op: &Operand<'tcx>,
+ constant: &Constant<'tcx>,
) -> Result<(DefId, ty::PolyFnSig<'tcx>, ty::GenericArgsRef<'tcx>, ty::PolyFnSig<'tcx>), TranslationError>
{
- match op {
- Operand::Constant(box Constant { literal, .. }) => {
- match literal {
- ConstantKind::Ty(c) => {
- match c.ty().kind() {
- TyKind::FnDef(def, args) => {
- let ty: ty::EarlyBinder<Ty<'tcx>> = self.env.tcx().type_of(def);
+ match constant.literal {
+ ConstantKind::Ty(c) => {
+ match c.ty().kind() {
+ TyKind::FnDef(def, args) => {
+ let ty: ty::EarlyBinder<Ty<'tcx>> = self.env.tcx().type_of(def);
- let ty_ident = ty.instantiate_identity();
- assert!(ty_ident.is_fn());
- let ident_sig = ty_ident.fn_sig(self.env.tcx());
+ let ty_ident = ty.instantiate_identity();
+ assert!(ty_ident.is_fn());
+ let ident_sig = ty_ident.fn_sig(self.env.tcx());
- let ty_instantiated = ty.instantiate(self.env.tcx(), args.as_slice());
- let instantiated_sig = ty_instantiated.fn_sig(self.env.tcx());
+ let ty_instantiated = ty.instantiate(self.env.tcx(), args.as_slice());
+ let instantiated_sig = ty_instantiated.fn_sig(self.env.tcx());
- Ok((*def, ident_sig, args, instantiated_sig))
- },
- // TODO handle FnPtr, closure
- _ => Err(TranslationError::Unimplemented {
- description: "implement function pointers".to_string(),
- }),
- }
+ Ok((*def, ident_sig, args, instantiated_sig))
},
- ConstantKind::Val(_, ty) => {
- match ty.kind() {
- TyKind::FnDef(def, args) => {
- let ty: ty::EarlyBinder<Ty<'tcx>> = self.env.tcx().type_of(def);
+ // TODO handle FnPtr, closure
+ _ => Err(TranslationError::Unimplemented {
+ description: "implement function pointers".to_string(),
+ }),
+ }
+ },
+ ConstantKind::Val(_, ty) => {
+ match ty.kind() {
+ TyKind::FnDef(def, args) => {
+ let ty: ty::EarlyBinder<Ty<'tcx>> = self.env.tcx().type_of(def);
- let ty_ident = ty.instantiate_identity();
- assert!(ty_ident.is_fn());
- let ident_sig = ty_ident.fn_sig(self.env.tcx());
+ let ty_ident = ty.instantiate_identity();
+ assert!(ty_ident.is_fn());
+ let ident_sig = ty_ident.fn_sig(self.env.tcx());
- let ty_instantiated = ty.instantiate(self.env.tcx(), args.as_slice());
- let instantiated_sig = ty_instantiated.fn_sig(self.env.tcx());
+ let ty_instantiated = ty.instantiate(self.env.tcx(), args.as_slice());
+ let instantiated_sig = ty_instantiated.fn_sig(self.env.tcx());
- Ok((*def, ident_sig, args, instantiated_sig))
- },
- // TODO handle FnPtr, closure
- _ => Err(TranslationError::Unimplemented {
- description: "implement function pointers".to_string(),
- }),
- }
+ Ok((*def, ident_sig, args, instantiated_sig))
},
- ConstantKind::Unevaluated(_, _) => Err(TranslationError::Unimplemented {
- description: "implement ConstantKind::Unevaluated".to_string(),
+ // TODO handle FnPtr, closure
+ _ => Err(TranslationError::Unimplemented {
+ description: "implement function pointers".to_string(),
}),
}
},
- _ => panic!("should not be reachable"),
+ ConstantKind::Unevaluated(_, _) => Err(TranslationError::Unimplemented {
+ description: "implement ConstantKind::Unevaluated".to_string(),
+ }),
}
}
@@ -1759,7 +1754,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
fn compute_call_regions(
&self,
- func: &Operand<'tcx>,
+ func: &Constant<'tcx>,
loc: Location,
) -> Result<CallRegions, TranslationError> {
let midpoint = self.info.interner.get_point_index(&facts::Point {
@@ -1878,7 +1873,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
CallRegionKind::Intersection(s) => {
s.insert(*r1);
},
- _ => panic!("unreachable"),
+ _ => unreachable!(),
}
}
}
@@ -1907,6 +1902,15 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
typ: facts::PointType::Start,
});
+ let Operand::Constant(box func_constant) = func else {
+ return Err(TranslationError::UnsupportedFeature {
+ description: format!(
+ "RefinedRust does currently not support this kind of call operand (got: {:?})",
+ func
+ ),
+ });
+ };
+
// for lifetime annotations:
// 1. get the regions involved here. for that, get the instantiation of the function.
// + if it's a FnDef type, that should be easy.
@@ -1927,7 +1931,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
// substituted regions) should be.
// 6. annotate the return value on assignment and establish constraints.
- let classification = self.compute_call_regions(func, loc)?;
+ let classification = self.compute_call_regions(func_constant, loc)?;
// update the inclusion tracker with the new regions we have introduced
// We just add the inclusions and ignore that we resolve it in a "tight" way.
@@ -1991,7 +1995,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
cont_stmt = self.prepend_endlfts(cont_stmt, dying_loans.iter().copied());
// Get the type of the return value from the function
- let (_, _, _, inst_sig) = self.call_expr_op_split_inst(func)?;
+ let (_, _, _, inst_sig) = self.call_expr_op_split_inst(func_constant)?;
// TODO: do we need to do something with late bounds?
let output_ty = inst_sig.output().skip_binder();
info!("call has instantiated type {:?}", inst_sig);
@@ -2056,7 +2060,12 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
CallRegionKind::Intersection(rs) => {
match rs.len() {
- 0 => panic!("unconstrained lifetime"),
+ 0 => {
+ return Err(TranslationError::UnsupportedFeature {
+ description: "RefinedRust does currently not support unconstrained lifetime"
+ .to_string(),
+ });
+ },
1 => {
// this is really just an equality constraint
if let Some(r2) = rs.iter().next() {
@@ -3395,32 +3404,27 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> {
// 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) => {
// check if this goes to a temporary of a checked op
- let translated_place;
- let ty;
- if self.checked_op_temporaries.contains_key(&place.local) {
+ let place_kind = if self.checked_op_temporaries.contains_key(&place.local) {
assert!(place.projection.len() == 1);
- match place.projection[0] {
- ProjectionElem::Field(f, _0) => {
- if f.index() == 0 {
- // access to the result of the op
- let new_place = self.make_local_place(place.local);
- translated_place = self.translate_place(&new_place)?;
- ty = self.get_type_of_place(place);
- } else {
- // make this a constant false -- our semantics directly checks for overflows
- // and otherwise throws UB.
- return Ok(radium::Expr::Literal(radium::Literal::LitBool(false)));
- }
- },
- _ => {
- panic!("invariant violation for access to checked op temporary");
- },
+ let ProjectionElem::Field(f, _0) = place.projection[0] else {
+ unreachable!("invariant violation for access to checked op temporary");
+ };
+
+ if f.index() != 0 {
+ // make this a constant false -- our semantics directly checks for overflows
+ // and otherwise throws UB.
+ return Ok(radium::Expr::Literal(radium::Literal::LitBool(false)));
}
+
+ // access to the result of the op
+ self.make_local_place(place.local)
} else {
- translated_place = self.translate_place(place)?;
- ty = self.get_type_of_place(place);
- }
+ *place
+ };
+
+ let translated_place = self.translate_place(&place_kind)?;
+ let ty = self.get_type_of_place(place);
let st = self.ty_translator.translate_type_to_syn_type(ty.ty)?;
let ot = self.ty_translator.translate_syn_type_to_op_type(&st);
diff --git a/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs b/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
index 3d69fafa6403e7e36f78e148a8dc6aedcdae1561..e5c00eebc069508ed8f5bd05d7c18a0284fb481f 100644
--- a/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
@@ -118,9 +118,10 @@ impl<'a> parse::Parse<ParseMeta<'a>> for MetaIProp {
let spec = specs::TyOwnSpec::new(loc_str, rfn_str, type_str, true, annot_meta);
Ok(Self::Type(spec))
},
- _ => {
- panic!("invalid macro command: {:?}", macro_cmd.value());
- },
+ _ => Err(parse::ParseError::OtherErr(
+ input.pos().unwrap(),
+ format!("invalid macro command: {:?}", macro_cmd.value()),
+ )),
}
} else {
let name_or_prop_str: parse::LitStr = input.parse(meta)?;
@@ -160,9 +161,7 @@ impl<U> parse::Parse<U> for InvariantSpecFlags {
"plain" => Ok(Self(specs::InvariantSpecFlags::Plain)),
"na" => Ok(Self(specs::InvariantSpecFlags::NonAtomic)),
"atomic" => Ok(Self(specs::InvariantSpecFlags::Atomic)),
- _ => {
- panic!("invalid ADT mode: {:?}", mode.value())
- },
+ _ => Err(parse::ParseError::OtherErr(input.pos().unwrap(), "invalid ADT mode".to_string())),
}
}
}
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 cc4a5a2ad546dfb9a4857e6c56b774503622613f..3bbbc4039153dbbd7838bf4daa4131e90dbe1ae3 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
@@ -169,9 +169,10 @@ impl<'a> parse::Parse<ParseMeta<'a>> for MetaIProp {
let (term, _meta) = process_coq_literal(&term.value(), *meta);
Ok(Self::Linktime(term))
},
- _ => {
- panic!("invalid macro command: {:?}", macro_cmd.value());
- },
+ _ => Err(parse::ParseError::OtherErr(
+ input.pos().unwrap(),
+ format!("invalid macro command: {:?}", macro_cmd.value()),
+ )),
}
} else {
let name_or_prop_str: parse::LitStr = input.parse(meta)?;
diff --git a/rr_frontend/translation/src/type_translator.rs b/rr_frontend/translation/src/type_translator.rs
index 0185f8e5debfb623bf8086a22a65f8c5f8bcbd33..98d2fe42f568c0f785ea127a50ca1e76da24a50e 100644
--- a/rr_frontend/translation/src/type_translator.rs
+++ b/rr_frontend/translation/src/type_translator.rs
@@ -126,7 +126,10 @@ impl<'def> TypeTranslationScope<'def> {
v.push(Some(lit_ty));
},
_ => {
- panic!("enter_generic_scope: not a type parameter");
+ return Err(TranslationError::UnsupportedFeature {
+ description: "RefinedRust does currently not support non-type generic arguments"
+ .to_string(),
+ });
},
},
@@ -1395,9 +1398,13 @@ impl<'def, 'tcx: 'def> TypeTranslator<'def, 'tcx> {
if adt.is_box() {
// extract the type parameter
// the second parameter is the allocator, which we ignore for now
- assert!(substs.len() == 2);
- let ty = substs[0].expect_ty();
- let translated_ty = self.translate_type_with_deps(ty, &mut *state)?;
+ let [ty, _] = substs.as_slice() else {
+ return Err(TranslationError::UnsupportedFeature {
+ description: format!("unsupported ADT {:?}", ty),
+ });
+ };
+
+ let translated_ty = self.translate_type_with_deps(ty.expect_ty(), &mut *state)?;
return Ok(radium::Type::BoxType(Box::new(translated_ty)));
}