diff --git a/case_studies/tests/src/structs.rs b/case_studies/tests/src/structs.rs
index 181449786bba1d642b6df9484cf7d452aec50153..179fc3d078206725b0abe0fd96fc345c576577f9 100644
--- a/case_studies/tests/src/structs.rs
+++ b/case_studies/tests/src/structs.rs
@@ -56,3 +56,23 @@ impl EvenInt {
self.add();
}
}
+
+
+
+pub struct Foo {}
+
+impl Foo {
+ #[rr::params("x", "γ")]
+ #[rr::args("(#x, γ)")]
+ #[rr::returns("()")]
+ pub fn a(&mut self) {
+ assert!(true);
+ }
+
+ #[rr::params("x", "γ")]
+ #[rr::args("(#x, γ)")]
+ #[rr::returns("()")]
+ pub fn b(&mut self) {
+ assert!(true);
+ }
+}
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index b3a42dad9eedee3601b8a3a4ae4eb48069f8021f..5cf086378e6f6919f09cf5e93f6a2dc7ac6a7538 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -629,17 +629,17 @@ fn translate_functions<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) {
// Only generate a spec
match translator.and_then(|t| t.generate_spec()) {
Ok(spec) => {
- info!("Successfully generated spec for {}", fname);
+ println!("Successfully generated spec for {}", fname);
vcx.procedure_registry.provide_specced_function(&f.to_def_id(), spec);
},
Err(function_body::TranslationError::FatalError(err)) => {
- error!("Encountered fatal cross-function error in translation: {:?}", err);
- error!("Aborting...");
+ println!("Encountered fatal cross-function error in translation: {:?}", err);
+ println!("Aborting...");
return;
},
Err(err) => {
- warn!("Encountered error: {:?}", err);
- warn!("Skipping function {}", fname);
+ println!("Encountered error: {:?}", err);
+ println!("Skipping function {}", fname);
if !rrconfig::skip_unsupported_features() {
exit_with_error(&format!("Encountered error when translating function {}, stopping...", fname));
}
@@ -650,17 +650,17 @@ fn translate_functions<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) {
// Fully translate the function
match translator.and_then(|t| t.translate()) {
Ok(fun) => {
- info!("Successfully translated {}", fname);
+ println!("Successfully translated {}", fname);
vcx.procedure_registry.provide_translated_function(&f.to_def_id(), fun);
},
Err(function_body::TranslationError::FatalError(err)) => {
- error!("Encountered fatal cross-function error in translation: {:?}", err);
- error!("Aborting...");
+ println!("Encountered fatal cross-function error in translation: {:?}", err);
+ println!("Aborting...");
return;
},
Err(err) => {
- warn!("Encountered error: {:?}", err);
- warn!("Skipping function {}", fname);
+ println!("Encountered error: {:?}", err);
+ println!("Skipping function {}", fname);
if !rrconfig::skip_unsupported_features() {
exit_with_error(&format!("Encountered error when translating function {}, stopping...", fname));
}
diff --git a/rr_frontend/translation/src/type_translator.rs b/rr_frontend/translation/src/type_translator.rs
index ecb9961ee83b1bcb4648aa223f299fef03b20437..0b98511a1fd6e84357b3e6d9c80853b5de66a602 100644
--- a/rr_frontend/translation/src/type_translator.rs
+++ b/rr_frontend/translation/src/type_translator.rs
@@ -393,19 +393,23 @@ impl <'def, 'tcx : 'def> TypeTranslator<'def, 'tcx> {
let mut generic_syntys = Vec::new();
for arg in args.into_iter() {
- let arg_ty = arg.expect_ty();
- let mut translated_ty;
- if let Some(ref mut adt_deps) = adt_deps {
- translated_ty = self.translate_type_with_deps(&arg_ty, Some(&mut *adt_deps))?;
+ if let Some(arg_ty) = arg.as_type() {
+ let mut translated_ty;
+ if let Some(ref mut adt_deps) = adt_deps {
+ translated_ty = self.translate_type_with_deps(&arg_ty, Some(&mut *adt_deps))?;
+ }
+ else {
+ translated_ty = self.translate_type_with_deps(&arg_ty, None)?;
+ }
+ // we need to substitute in the variables according to the function scope
+ translated_ty.subst(generic_env.as_slice());
+ //translated_ty.subst
+ generic_syntys.push(translated_ty.get_syn_type());
+ params.push(translated_ty);
}
else {
- translated_ty = self.translate_type_with_deps(&arg_ty, None)?;
+ return Err(TranslationError::UnsupportedFeature{ description: "structs with lifetime parameters are not supported".to_string()})
}
- // we need to substitute in the variables according to the function scope
- translated_ty.subst(generic_env.as_slice());
- //translated_ty.subst
- generic_syntys.push(translated_ty.get_syn_type());
- params.push(translated_ty);
}
let struct_use = radium::AbstractStructUse::new(struct_ref, params, radium::TypeIsRaw::No);
@@ -580,27 +584,35 @@ 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));
- let struct_name = strip_coq_ident(&ty.ident(tcx).to_string());
- let (variant_def, invariant_def) = self.make_adt_variant(&struct_name, ty, adt, &ty_param_defs, &st_params, Some(&mut adt_deps))?;
-
- let mut struct_def = radium::AbstractStruct::new(variant_def, ty_param_defs, st_params);
- if let Some(invariant_def) = invariant_def {
- struct_def.add_invariant(invariant_def);
- }
+ let translate_adt = || {
+ let struct_name = strip_coq_ident(&ty.ident(tcx).to_string());
+ let (variant_def, invariant_def) = self.make_adt_variant(&struct_name, ty, adt, &ty_param_defs, &st_params, Some(&mut adt_deps))?;
- // TODO for generating the semtype definition, we will also need to track dependencies
- // between structs so that we know when we need recursive types etc.
+ let mut struct_def = radium::AbstractStruct::new(variant_def, ty_param_defs, st_params);
+ if let Some(invariant_def) = invariant_def {
+ struct_def.add_invariant(invariant_def);
+ }
+ Ok(struct_def)
+ };
- // finalize the definition
- {
- let mut struct_def_ref = struct_def_init.borrow_mut();
- *struct_def_ref = Some(struct_def);
+ match translate_adt() {
+ Ok(struct_def) => {
+ // finalize the definition
+ // TODO for generating the semtype definition, we will also need to track dependencies
+ // between structs so that we know when we need recursive types etc.
+ let mut struct_def_ref = struct_def_init.borrow_mut();
+ *struct_def_ref = Some(struct_def);
- let mut deps_ref = self.adt_deps.borrow_mut();
- deps_ref.insert(adt.did(), adt_deps);
+ let mut deps_ref = self.adt_deps.borrow_mut();
+ deps_ref.insert(adt.did(), adt_deps);
+ Ok(())
+ }
+ Err(err) => {
+ // remove the partial definition
+ self.variant_registry.borrow_mut().remove(&ty.def_id);
+ Err(err)
+ }
}
-
- Ok(())
}
/// Make an ADT variant.
@@ -881,7 +893,6 @@ impl <'def, 'tcx : 'def> TypeTranslator<'def, 'tcx> {
// TODO: currently a hack, I don't know how to query the name properly
let enum_name = strip_coq_ident(format!("{:?}", def).as_str());
- self.enum_registry.borrow_mut().insert(def.did(), (enum_name.clone(), &*enum_def_init, def));
// first thing: figure out the generics we are using here.
// we need to search all of the variant types for that.
@@ -906,131 +917,142 @@ impl <'def, 'tcx : 'def> TypeTranslator<'def, 'tcx> {
info!("enum using generics: {:?}", used_generics);
- // now build masks describing which generics each of the variants uses
- // and register the variants
- let mut variant_masks: HashMap<DefId, Vec<bool>> = HashMap::new();
- let mut variant_attrs = Vec::new();
- for v in def.variants().iter() {
- let mut folder = TyVarFolder::new(self.env.tcx());
- for f in v.fields.iter() {
- let f_ty = self.env.tcx().type_of(f.did).instantiate_identity();
- f_ty.fold_with(&mut folder);
- }
- let variant_generics: HashSet<ty::ParamTy> = folder.get_result();
-
- let mut mask = Vec::new();
- let mut these_param_defs = Vec::new();
- let mut these_st_params = Vec::new();
- for ((param, param_defs), st_param) in used_generics.iter().zip(ty_param_defs.iter()).zip(st_params.iter()) {
- if variant_generics.contains(param) {
- mask.push(true);
- these_param_defs.push(param_defs.clone());
- these_st_params.push(st_param.clone());
+ // insert partial definition for recursive occurrences
+ self.enum_registry.borrow_mut().insert(def.did(), (enum_name.clone(), &*enum_def_init, def));
+
+ let translate_variants = || {
+ // now build masks describing which generics each of the variants uses
+ // and register the variants
+ let mut variant_masks: HashMap<DefId, Vec<bool>> = HashMap::new();
+ let mut variant_attrs = Vec::new();
+ for v in def.variants().iter() {
+ let mut folder = TyVarFolder::new(self.env.tcx());
+ for f in v.fields.iter() {
+ let f_ty = self.env.tcx().type_of(f.did).instantiate_identity();
+ f_ty.fold_with(&mut folder);
}
- else {
- mask.push(false);
+ let variant_generics: HashSet<ty::ParamTy> = folder.get_result();
+
+ let mut mask = Vec::new();
+ let mut these_param_defs = Vec::new();
+ let mut these_st_params = Vec::new();
+ for ((param, param_defs), st_param) in used_generics.iter().zip(ty_param_defs.iter()).zip(st_params.iter()) {
+ if variant_generics.contains(param) {
+ mask.push(true);
+ these_param_defs.push(param_defs.clone());
+ these_st_params.push(st_param.clone());
+ }
+ else {
+ mask.push(false);
+ }
}
- }
- variant_masks.insert(v.def_id, mask);
+ variant_masks.insert(v.def_id, mask);
- // now generate the variant
- let struct_def_init = self.struct_arena.alloc(RefCell::new(None));
+ // now generate the variant
+ let struct_def_init = self.struct_arena.alloc(RefCell::new(None));
- let struct_name = strip_coq_ident(format!("{}_{}", enum_name, v.ident(tcx)).as_str());
- self.variant_registry.borrow_mut().insert(v.def_id, (struct_name.clone(), &*struct_def_init, v, true));
+ let struct_name = strip_coq_ident(format!("{}_{}", enum_name, v.ident(tcx)).as_str());
+ self.variant_registry.borrow_mut().insert(v.def_id, (struct_name.clone(), &*struct_def_init, v, true));
- // IMPORTANT: use the full enum's ty_param_defs to account for indexing
- let (variant_def, invariant_def) = self.make_adt_variant(struct_name.as_str(), v, def, &ty_param_defs, &st_params, Some(&mut adt_deps))?;
+ // IMPORTANT: use the full enum's ty_param_defs to account for indexing
+ let (variant_def, invariant_def) = self.make_adt_variant(struct_name.as_str(), v, def, &ty_param_defs, &st_params, Some(&mut adt_deps))?;
- // IMPORTANT: use the subset of actually used params for the definition
- let mut struct_def = radium::AbstractStruct::new(variant_def, these_param_defs, these_st_params);
- if let Some(invariant_def) = invariant_def {
- struct_def.add_invariant(invariant_def);
- }
+ // IMPORTANT: use the subset of actually used params for the definition
+ let mut struct_def = radium::AbstractStruct::new(variant_def, these_param_defs, these_st_params);
+ if let Some(invariant_def) = invariant_def {
+ struct_def.add_invariant(invariant_def);
+ }
- // also remember the attributes for additional processing
- let outer_attrs = self.env.get_attributes(v.def_id);
- let outer_attrs = crate::utils::filter_tool_attrs(outer_attrs);
- variant_attrs.push(outer_attrs);
+ // also remember the attributes for additional processing
+ let outer_attrs = self.env.get_attributes(v.def_id);
+ let outer_attrs = crate::utils::filter_tool_attrs(outer_attrs);
+ variant_attrs.push(outer_attrs);
- // finalize the definition
- {
- let mut struct_def_ref = struct_def_init.borrow_mut();
- *struct_def_ref = Some(struct_def);
+ // finalize the definition
+ {
+ let mut struct_def_ref = struct_def_init.borrow_mut();
+ *struct_def_ref = Some(struct_def);
+ }
}
- }
- // get the type of the discriminant
- let it = def.repr().discr_type();
- let translated_it = self.translate_integer_type(it)?;
+ // get the type of the discriminant
+ let it = def.repr().discr_type();
+ let translated_it = self.translate_integer_type(it)?;
- // build the discriminant map
- let discrs = self.build_discriminant_map(def)?;
+ // build the discriminant map
+ let discrs = self.build_discriminant_map(def)?;
- // get representation options
- let repr = def.repr();
- let mut repr_opt = radium::EnumRepr::ReprRust;
- if repr.c() {
- repr_opt = radium::EnumRepr::ReprC;
- }
- else if repr.simd() {
- return Err(TranslationError::UnsupportedFeature { description: "The SIMD flag is currently unsupported".to_string() })
- }
- else if repr.packed() {
- return Err(TranslationError::UnsupportedFeature { description: "The repr(packed) flag is currently unsupported".to_string() })
- }
- else if repr.linear() {
- return Err(TranslationError::UnsupportedFeature { description: "The linear flag is currently unsupported".to_string() })
- }
- else if repr.transparent() {
- repr_opt = radium::EnumRepr::ReprTransparent;
- }
+ // get representation options
+ let repr = def.repr();
+ let mut repr_opt = radium::EnumRepr::ReprRust;
+ if repr.c() {
+ repr_opt = radium::EnumRepr::ReprC;
+ }
+ else if repr.simd() {
+ return Err(TranslationError::UnsupportedFeature { description: "The SIMD flag is currently unsupported".to_string() })
+ }
+ else if repr.packed() {
+ return Err(TranslationError::UnsupportedFeature { description: "The repr(packed) flag is currently unsupported".to_string() })
+ }
+ else if repr.linear() {
+ return Err(TranslationError::UnsupportedFeature { description: "The linear flag is currently unsupported".to_string() })
+ }
+ else if repr.transparent() {
+ repr_opt = radium::EnumRepr::ReprTransparent;
+ }
- // parse annotations for enum type
- let enum_spec;
- let mut inductive_decl = None;
- let builtin_spec = self.get_builtin_enum_spec(def.did())?;
- if let Some(spec) = builtin_spec {
- enum_spec = spec;
- }
- else if self.env.has_tool_attribute(def.did(), "refined_by") {
- let attributes = self.env.get_attributes(def.did());
- let attributes = crate::utils::filter_tool_attrs(attributes);
+ // parse annotations for enum type
+ let enum_spec;
+ let mut inductive_decl = None;
+ let builtin_spec = self.get_builtin_enum_spec(def.did())?;
+ if let Some(spec) = builtin_spec {
+ enum_spec = spec;
+ }
+ else if self.env.has_tool_attribute(def.did(), "refined_by") {
+ let attributes = self.env.get_attributes(def.did());
+ let attributes = crate::utils::filter_tool_attrs(attributes);
- // TODO: change once we handle lft parameters properly
- let lft_params: Vec<(Option<String>, radium::Lft)> = Vec::new();
+ // TODO: change once we handle lft parameters properly
+ let lft_params: Vec<(Option<String>, radium::Lft)> = Vec::new();
- let mut parser = VerboseEnumSpecParser::new();
- enum_spec = parser.parse_enum_spec("", &attributes, &variant_attrs, &ty_param_defs, &lft_params)
- .map_err(|err| TranslationError::FatalError(err))?;
- }
- else {
- // generate a specification
- let decl;
- (decl, enum_spec) = self.generate_enum_spec(def, &enum_name);
- inductive_decl = Some(decl);
- }
+ let mut parser = VerboseEnumSpecParser::new();
+ enum_spec = parser.parse_enum_spec("", &attributes, &variant_attrs, &ty_param_defs, &lft_params)
+ .map_err(|err| TranslationError::FatalError(err))?;
+ }
+ else {
+ // generate a specification
+ let decl;
+ (decl, enum_spec) = self.generate_enum_spec(def, &enum_name);
+ inductive_decl = Some(decl);
+ }
- let mut enum_builder = radium::EnumBuilder::new(enum_name, ty_param_defs, st_params, translated_it, repr_opt);
- // now build the enum itself
- for v in def.variants().iter() {
- let variant_ref = self.lookup_adt_variant(v.def_id)?;
- let variant_name = strip_coq_ident(&v.ident(tcx).to_string());
- let discriminant = discrs.get(&variant_name).unwrap();
- enum_builder.add_variant(&variant_name, variant_ref, variant_masks.remove(&v.def_id).unwrap(), *discriminant);
- }
+ let mut enum_builder = radium::EnumBuilder::new(enum_name, ty_param_defs, st_params, translated_it, repr_opt);
+ // now build the enum itself
+ for v in def.variants().iter() {
+ let variant_ref = self.lookup_adt_variant(v.def_id)?;
+ let variant_name = strip_coq_ident(&v.ident(tcx).to_string());
+ let discriminant = discrs.get(&variant_name).unwrap();
+ enum_builder.add_variant(&variant_name, variant_ref, variant_masks.remove(&v.def_id).unwrap(), *discriminant);
+ }
+ Ok(enum_builder.finish(inductive_decl, enum_spec))
+ };
- let enum_def = enum_builder.finish(inductive_decl, enum_spec);
- // finalize the definition
- {
- let mut enum_def_ref = enum_def_init.borrow_mut();
- *enum_def_ref = Some(enum_def);
+ match translate_variants() {
+ Ok(enum_def) => {
+ // finalize the definition
+ let mut enum_def_ref = enum_def_init.borrow_mut();
+ *enum_def_ref = Some(enum_def);
- let mut deps_ref = self.adt_deps.borrow_mut();
- deps_ref.insert(def.did(), adt_deps);
+ let mut deps_ref = self.adt_deps.borrow_mut();
+ deps_ref.insert(def.did(), adt_deps);
+ Ok(())
+ },
+ Err(err) => {
+ // deregister the ADT again
+ self.enum_registry.borrow_mut().remove(&def.did());
+ Err(err)
+ },
}
-
- Ok(())
}
/// Translate type.